aarch64: verify bitselect, bnot rules (avanhatt#100)

Quick implementation of `bitselect`, `bnot` basically worked
out-of-the-box!

Updates avanhatt#34

cranelift/codegen/src/inst_specs.isle

@@ -25,6 +25,16 @@
     (default true)
 )
 
+;;;; Common Term Forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(form
+  bv_ternary_8_to_64
+  ((args (bv  8) (bv  8) (bv  8)) (ret (bv  8)))
+  ((args (bv 16) (bv 16) (bv 16)) (ret (bv 16)))
+  ((args (bv 32) (bv 32) (bv 32)) (ret (bv 32)))
+  ((args (bv 64) (bv 64) (bv 64)) (ret (bv 64)))
+)
+
 ;;;; CLIF Instruction Specifications ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (spec (iadd x y)
@@ -97,3 +107,7 @@
     ((args (bv 32)) (ret (bv 32)))
     ((args (bv 64)) (ret (bv 64)))
 )
+
+(spec (bitselect c x y)
+    (provide (= result (bvor (bvand c x) (bvand (bvnot c) y)))))
+(instantiate bitselect bv_ternary_8_to_64)

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

@@ -2162,6 +2162,7 @@
 ;; Instruction creation helpers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; Helper for creating the zero register.
+(spec (zero_reg) (provide (= (zero_ext (widthof result) #b0) result)))
 (decl zero_reg () Reg)
 (extern constructor zero_reg zero_reg)
 

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

@@ -1252,12 +1252,12 @@
 ;; Note that bitwise negation is implemented here as
 ;;
 ;;      NOT rd, rm ==> ORR_NOT rd, zero, rm
-(rule -1 (lower (has_type (fits_in_64 ty) (bnot x)))
+(rule bnot_base_case -1 (lower (has_type (fits_in_64 ty) (bnot x)))
       (orr_not ty (zero_reg) x))
 
 ;; Special case to use `orr_not_shift` if it's a `bnot` of a const-left-shifted
 ;; value.
-(rule 1 (lower (has_type (fits_in_64 ty)
+(rule bnot_ishl 1 (lower (has_type (fits_in_64 ty)
                        (bnot (ishl x (iconst k)))))
       (if-let amt (lshl_from_imm64 ty k))
       (orr_not_shift ty (zero_reg) x amt))
@@ -1885,7 +1885,7 @@
 
 ;;;; Rules for `bitselect` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(rule (lower (has_type ty (bitselect c x y)))
+(rule bitselect (lower (has_type ty (bitselect c x y)))
       (if (ty_int_ref_scalar_64 ty))
       (let ((tmp1 Reg (and_reg ty x c))
             (tmp2 Reg (bic ty y c)))

cranelift/codegen/src/prelude.isle

@@ -586,6 +586,14 @@
 
 ;; A pure constructor/extractor that only matches scalar integers, and
 ;; references that can fit in 64 bits.
+(spec (ty_int_ref_scalar_64 ty) 
+      (provide (= result ty))
+      (require 
+            (or 
+                  (= ty 8)
+                  (= ty 16)
+                  (= ty 32)
+                  (= ty 64))))
 (decl pure partial ty_int_ref_scalar_64 (Type) Type)
 (extern constructor ty_int_ref_scalar_64 ty_int_ref_scalar_64)
 (extern extractor ty_int_ref_scalar_64 ty_int_ref_scalar_64_extract)