aarch64: ineg spec (bytecodealliance#124)

Specify and verify `ineg` on AArch64. Updates avanhatt#34
wellesley-prog-sys · Oct 9, 2024 · a9bb0eb · a9bb0eb
1 parent 230d96c
commit a9bb0eb
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/cranelift/codegen/src/inst_specs.isle b/cranelift/codegen/src/inst_specs.isle
@@ -41,6 +41,14 @@
 
 ;;;; Common Term Forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(form
+    bv_unary_8_to_64
+    ((args (bv  8)) (ret (bv  8)))
+    ((args (bv 16)) (ret (bv 16)))
+    ((args (bv 32)) (ret (bv 32)))
+    ((args (bv 64)) (ret (bv 64)))
+)
+
 (form
   bv_ternary_8_to_64
   ((args (bv  8) (bv  8) (bv  8)) (ret (bv  8)))
@@ -68,6 +76,10 @@
     ((args (bv 64) (bv 64)) (ret (bv 64)))
 )
 
+(spec (ineg x)
+    (provide (= result (bvneg x))))
+(instantiate ineg bv_unary_8_to_64)
+
 (spec (imul x y)
     (provide (= result (bvmul x y))))
 (instantiate imul

diff --git a/cranelift/codegen/src/isa/aarch64/lower.isle b/cranelift/codegen/src/isa/aarch64/lower.isle
@@ -792,7 +792,7 @@
 ;;;; Rules for `ineg` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; `i64` and smaller.
-(rule 1 (lower (has_type (fits_in_64 ty) (ineg x)))
+(rule ineg_base_case 1 (lower (has_type (fits_in_64 ty) (ineg x)))
       (sub ty (zero_reg) x))
 
 ;; `i128`