Implicit type conversions in ISLE (#3807)

Add support for implicit type conversions to ISLE.

This feature allows the DSL user to register to the compiler that a
particular term (used as a constructor or extractor) converts from one
type to another. The compiler will then *automatically* insert this term
whenever a type mismatch involving that specific pair of types occurs.

This significantly cleans up many uses of the ISLE DSL. For example,
when defining the compiler backends, we often have newtypes like `Gpr`
around `Reg` (signifying a particular type of register); we can define
a conversion from Gpr to Reg automatically.

Conversions can also have side-effects, as long as these side-effects
are idempotent. For example, `put_value_in_reg` in a compiler backend
has the effect of marking the value as used, causing codegen to produce
it, and assigns a register to the value; but multiple invocations of
this will return the same register for the same value. Thus it is safe
to use it as an implicit conversion that may be invoked multiple times.
This is documented in the ISLE-Cranelift integration document.

This PR also adds some testing infrastructure to the ISLE compiler,
checking that "pass" tests pass through the DSL compiler, "fail" tests
do not, and "link" tests are able to generate code and link that code
with corresponding Rust code.
This commit is contained in:
Chris Fallin
2022-02-23 13:15:27 -08:00
committed by GitHub
parent 4e26c13bbe
commit 9dbb8c25c5
23 changed files with 492 additions and 9 deletions

View File

@@ -0,0 +1,17 @@
(type i32 (primitive i32))
(type B (enum (B (x i32) (y i32))))
;; `isub` has a constructor and extractor.
(decl isub (i32 i32) B)
(rule (isub x y)
(B.B x y))
(extractor (isub x y)
(B.B x y))
;; `value_array_2` has both an external extractor and an external constructor.
(type Value (primitive Value))
(type ValueArray2 extern (enum))
(decl value_array_2 (Value Value) ValueArray2)
(extern extractor infallible value_array_2 unpack_value_array_2)
(extern constructor value_array_2 pack_value_array_2)

View File

@@ -0,0 +1,28 @@
(type T (enum (A) (B)))
(type U (enum (C) (D)))
(type V (enum (E) (F)))
(type u32 (primitive u32))
(convert T U t_to_u)
(convert U T u_to_t)
(convert U V u_to_v)
(decl t_to_u (T) U)
(decl u_to_t (U) T)
(decl u_to_v (U) V)
(rule (t_to_u (T.A)) (U.C))
(rule (t_to_u (T.B)) (U.D))
(rule (u_to_t (U.C)) (T.A))
(rule (u_to_t (U.D)) (T.B))
(rule (u_to_v (U.C)) (V.E))
(rule (u_to_v (U.D)) (V.F))
(extern extractor u_to_t u_to_t)
(decl X (T U) V)
(rule (X (U.C) (U.D))
(U.D))

View File

@@ -0,0 +1,21 @@
(type u32 (primitive u32))
(type A (enum (Add (x u32) (y u32)) (Sub (x u32) (y u32))))
(type B (enum (B (z u32))))
(decl Sub (u32 u32) u32)
(extern constructor Sub sub)
(decl Add (u32 u32) u32)
(extern constructor Add add)
(decl Lower (A) B)
(rule
(Lower (A.Add x y))
(let ((z u32 (Add x y)))
(B.B z)))
(rule
(Lower (A.Sub x y))
(let ((z u32 (Sub x y)))
(B.B z)))

View File

@@ -0,0 +1,4 @@
(type DoesNotDeriveDebug nodebug
(enum A
B
C))

View File

@@ -0,0 +1,24 @@
(type u32 (primitive u32))
(type A (enum
(A1 (x B) (y B))))
(type B (enum
(B1 (x u32))
(B2 (x u32))))
(decl A2B (A) B)
(rule 1
(A2B (A.A1 _ (B.B1 x)))
(B.B1 x))
(rule 0
(A2B (A.A1 (B.B1 x) _))
(B.B1 x))
(rule 0
(A2B (A.A1 (B.B2 x) _))
(B.B1 x))
(rule -1
(A2B (A.A1 _ _))
(B.B1 42))

View File

@@ -0,0 +1,66 @@
(type Opcode extern (enum
Iadd
Isub
Load
Store))
(type Inst (primitive Inst))
(type InstInput (primitive InstInput))
(type Reg (primitive Reg))
(type u32 (primitive u32))
(decl Op (Opcode) Inst)
(extern extractor infallible Op get_opcode)
(decl InstInput (InstInput u32) Inst)
(extern extractor infallible InstInput get_inst_input (out in))
(decl Producer (Inst) InstInput)
(extern extractor Producer get_input_producer)
(decl UseInput (InstInput) Reg)
(extern constructor UseInput put_input_in_reg)
(type MachInst (enum
(Add (a Reg) (b Reg))
(Add3 (a Reg) (b Reg) (c Reg))
(Sub (a Reg) (b Reg))))
(decl Lower (Inst) MachInst)
;; Extractors that give syntax sugar for (Iadd ra rb), etc.
;;
;; Note that this is somewhat simplistic: it directly connects inputs to
;; MachInst regs; really we'd want to return a VReg or InstInput that we can use
;; another extractor to connect to another (producer) inst.
;;
;; Also, note that while it looks a little indirect, a verification effort could
;; define equivalences across the `rule` LHS/RHS pairs, and the types ensure that
;; we are dealing (at the semantic level) with pure value equivalences of
;; "terms", not arbitrary side-effecting calls.
(decl Iadd (InstInput InstInput) Inst)
(decl Isub (InstInput InstInput) Inst)
(extractor
(Iadd a b)
(and
(Op (Opcode.Iadd))
(InstInput a <0)
(InstInput b <1)))
(extractor
(Isub a b)
(and
(Op (Opcode.Isub))
(InstInput a <0)
(InstInput b <1)))
;; Now the nice syntax-sugar that "end-user" backend authors can write:
(rule
(Lower (Iadd ra rb))
(MachInst.Add (UseInput ra) (UseInput rb)))
(rule
(Lower (Iadd (Producer (Iadd ra rb)) rc))
(MachInst.Add3 (UseInput ra) (UseInput rb) (UseInput rc)))
(rule
(Lower (Isub ra rb))
(MachInst.Sub (UseInput ra) (UseInput rb)))

View File

@@ -0,0 +1,42 @@
(type u32 (primitive u32))
(type bool (primitive bool))
(type A (enum (A1 (x u32))))
(decl Ext1 (u32) A)
(decl Ext2 (u32) A)
(extern extractor Ext1 ext1)
(extern extractor Ext2 ext2)
(extern const $A u32)
(extern const $B u32)
(decl C (bool) A)
(extern constructor C c)
(decl Lower (A) A)
(rule
(Lower
(and
a
(Ext1 x)
(Ext2 =x)))
(C #t))
(type Opcode (enum A B C))
(type MachInst (enum D E F))
(decl Lower2 (Opcode) MachInst)
(rule
(Lower2 (Opcode.A))
(MachInst.D))
(rule
(Lower2 (Opcode.B))
(MachInst.E))
(rule
(Lower2 (Opcode.C))
(MachInst.F))
(decl F (Opcode) u32)
(rule
(F _)
$B)

View File

@@ -0,0 +1,96 @@
;;;; Type Definitions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Declare that we are using the `i32` primitive type from Rust.
(type i32 (primitive i32))
;; Our high-level, RISC-y input IR.
(type HighLevelInst
(enum (Add (a Value) (b Value))
(Load (addr Value))
(Const (c i32))))
;; A value in our high-level IR is a Rust `Copy` type. Values are either defined
;; by an instruction, or are a basic block argument.
(type Value (primitive Value))
;; Our low-level, CISC-y machine instructions.
(type LowLevelInst
(enum (Add (mode AddrMode))
(Load (offset i32) (addr Reg))
(Const (c i32))))
;; Different kinds of addressing modes for operands to our low-level machine
;; instructions.
(type AddrMode
(enum
;; Both operands in registers.
(RegReg (a Reg) (b Reg))
;; The destination/first operand is a register; the second operand is in
;; memory at `[b + offset]`.
(RegMem (a Reg) (b Reg) (offset i32))
;; The destination/first operand is a register, second operand is an
;; immediate.
(RegImm (a Reg) (imm i32))))
;; The register type is a Rust `Copy` type.
(type Reg (primitive Reg))
;;;; Rules ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Declare our top-level lowering function. We will attach rules to this
;; declaration for lowering various patterns of `HighLevelInst` inputs.
(decl lower (HighLevelInst) LowLevelInst)
;; Simple rule for lowering constants.
(rule (lower (HighLevelInst.Const c))
(LowLevelInst.Const c))
;; Declare an external constructor that puts a high-level `Value` into a
;; low-level `Reg`.
(decl put_in_reg (Value) Reg)
(extern constructor put_in_reg put_in_reg)
;; Simple rule for lowering adds.
(rule (lower (HighLevelInst.Add a b))
(LowLevelInst.Add
(AddrMode.RegReg (put_in_reg a) (put_in_reg b))))
;; Simple rule for lowering loads.
(rule (lower (HighLevelInst.Load addr))
(LowLevelInst.Load 0 (put_in_reg addr)))
;; Declare an external extractor for extracting the instruction that defined a
;; given operand value.
(decl inst_result (HighLevelInst) Value)
(extern extractor inst_result inst_result)
;; Rule to sink loads into adds.
(rule (lower (HighLevelInst.Add a (inst_result (HighLevelInst.Load addr))))
(LowLevelInst.Add
(AddrMode.RegMem (put_in_reg a)
(put_in_reg addr)
0)))
;; Rule to sink a load of a base address with a static offset into a single add.
(rule (lower (HighLevelInst.Add
a
(inst_result (HighLevelInst.Load
(inst_result (HighLevelInst.Add
base
(inst_result (HighLevelInst.Const offset))))))))
(LowLevelInst.Add
(AddrMode.RegMem (put_in_reg a)
(put_in_reg base)
offset)))
;; Rule for sinking an immediate into an add.
(rule (lower (HighLevelInst.Add a (inst_result (HighLevelInst.Const c))))
(LowLevelInst.Add
(AddrMode.RegImm (put_in_reg a) c)))
;; Rule for lowering loads of a base address with a static offset.
(rule (lower (HighLevelInst.Load
(inst_result (HighLevelInst.Add
base
(inst_result (HighLevelInst.Const offset))))))
(LowLevelInst.Load offset (put_in_reg base)))