aarch64: verify subset of store rules (bytecodealliance#148)

Provide specs for store rules and verify a subset of expansions.

Updates avanhatt#34

cranelift/codegen/src/inst_specs.isle

@@ -39,6 +39,28 @@
     )
 )
 
+; Parameters of a CLIF store operation.
+(state clif_store
+    (type
+        (struct
+            (active Bool)
+            (size_bits Int)
+            (addr (bv 64))
+            (value (bv 64))
+        )
+    )
+    (default
+        (and
+            ; Store is not active.
+            (not (:active clif_store))
+
+            ; Must provide a fixed size in the default case, otherwise type
+            ; inference is underconstrained.
+            (= (:size_bits clif_store) 1)
+        )
+    )
+)
+
 ;;;; Common Term Forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (form
@@ -148,6 +170,32 @@
     ((args (named MemFlags) (named Value) (named Offset32)) (ret (bv 64)))
 )
 
+(spec (store flags value p offset)
+    (modifies clif_store)
+    (provide
+        ; Activate the CLIF store effect
+        (:active clif_store)
+
+        ; TODO(mbm): store flags
+
+        ; Store size is the width of the stored value.
+        (= (:size_bits clif_store) (widthof value))
+
+        ; Address calculation.
+        (= (:addr clif_store) (bvadd p (sign_ext 64 offset)))
+
+        ; Stored value is set to the low bits of the CLIF store value.
+        (= (conv_to (widthof value) (:value clif_store)) value)
+
+        ; HACK: Result of the store is a 1-bit vector.
+        (= result #b1)
+    )
+)
+(instantiate store
+    ((args (named MemFlags) (bv 32) (named Value) (named Offset32)) (ret (bv 1)))
+    ((args (named MemFlags) (bv 64) (named Value) (named Offset32)) (ret (bv 1)))
+)
+
 (form extend
     ((args (bv  8)) (ret (bv  8)))
     ((args (bv  8)) (ret (bv 16)))

cranelift/codegen/src/isa/aarch64/lower.isle

@@ -16,6 +16,22 @@
 
             ; If active, their parameters must match.
             (=> (:active clif_load) (= clif_load isa_load))
+
+            ; Store effects
+
+            ; Either both active, or both not.
+            (= (:active clif_store) (:active isa_store))
+            ; If active, their parameters must agree.
+            (=> (:active clif_store)
+                  (and
+                        (= (:size_bits clif_store) (:size_bits isa_store))
+                        (= (:addr clif_store) (:addr isa_store))
+                        (=
+                              (conv_to (:size_bits clif_store) (:value clif_store))
+                              (conv_to (:size_bits clif_store) (:value isa_store))
+                        )
+                  )
+            )
       )
 )
 
@@ -2433,19 +2449,23 @@
 
 ;;;; Rules for stores ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(rule (lower
+(rule store_i8
+      (lower
        (store flags value @ (value_type $I8) address offset))
       (side_effect
        (aarch64_store8 (amode $I8 address offset) flags value)))
-(rule (lower
+(rule store_i16
+      (lower
        (store flags value @ (value_type $I16) address offset))
       (side_effect
        (aarch64_store16 (amode $I16 address offset) flags value)))
-(rule (lower
+(rule store_i32
+      (lower
        (store flags value @ (value_type $I32) address offset))
       (side_effect
        (aarch64_store32 (amode $I32 address offset) flags value)))
-(rule (lower
+(rule store_i64
+      (lower
        (store flags value @ (value_type $I64) address offset))
       (side_effect
        (aarch64_store64 (amode $I64 address offset) flags value)))

cranelift/codegen/src/isa/aarch64/spec/state.isle

@@ -23,6 +23,13 @@
         )
     )
     (default
-        (not (:active isa_store))
+        (and
+            ; Store is not active.
+            (not (:active isa_store))
+
+            ; Must provide a fixed size in the default case, otherwise type
+            ; inference is underconstrained.
+            (= (:size_bits isa_store) 1)
+        )
     )
 )

cranelift/codegen/src/prelude_lower.isle

@@ -74,6 +74,7 @@
 ;; Construct an empty `InstOutput`.
 (decl output_none () InstOutput)
 (extern constructor output_none output_none)
+(spec (output_none) (provide (= result #b1)))
 
 ;; Construct a single-element `InstOutput`.
 (decl output (ValueRegs) InstOutput)
@@ -443,6 +444,7 @@
 
 ;; Emit given side-effectful instruction.
 (decl emit_side_effect (SideEffectNoResult) Unit)
+(spec (emit_side_effect arg) (provide true))
 (rule (emit_side_effect (SideEffectNoResult.Inst inst))
       (emit inst))
 (rule (emit_side_effect (SideEffectNoResult.Inst2 inst1 inst2))