Enum model debug2

cranelift/codegen/src/inst_specs.isle

@@ -96,6 +96,16 @@
     ((args (named Type) (bv 64) (bv 64) (bv 64)) (ret (bv 64)))
 )
 
+;;;; i128 bit cases ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(form
+    bv_binary_8_to_128
+    ((args (named Type) (bv  8) (bv  8)) (ret (bv  8)))
+    ((args (named Type) (bv 16) (bv 16)) (ret (bv 16)))
+    ((args (named Type) (bv 32) (bv 32)) (ret (bv 32)))
+    ((args (named Type) (bv 64) (bv 64)) (ret (bv 64)))
+    ((args (named Type) (bv 128) (bv 128)) (ret (bv 128)))
+)
+
 ;;;; CLIF Instruction Specifications ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; Integer Instructions
@@ -327,7 +337,7 @@
 
 (spec (rotl ty x y)
     (provide (= result (rotl x y))))
-(instantiate rotl bv_binary_8_to_64)
+(instantiate rotl bv_binary_8_to_128)
 
 (spec (rotr ty x y)
     (provide (= result (rotr x y))))

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

@@ -1256,7 +1256,7 @@
 )
 
 ;; Registers.
-(model Reg (type (bv)))
+(model Reg (type (bv 64)))
 
 ;; An ALU operation. This can be paired with several instruction formats
 ;; below (see `Inst`) in any combination.
@@ -1394,14 +1394,20 @@
 ))
 
 (type SImm7Scaled (primitive SImm7Scaled))
-
+(model SImm7Scaled (type (bv 1)))
 (type BoxCallInfo (primitive BoxCallInfo))
+(model BoxCallInfo (type (bv 1)))
 (type BoxCallIndInfo (primitive BoxCallIndInfo))
+(model BoxCallIndInfo (type (bv 1)))
 (type BoxReturnCallInfo (primitive BoxReturnCallInfo))
+(model BoxReturnCallInfo (type (bv 1)))
 (type BranchTarget (primitive BranchTarget))
+(model BranchTarget (type (bv 1)))
 (type BoxJTSequenceInfo (primitive BoxJTSequenceInfo))
 (type CodeOffset (primitive CodeOffset))
+(model CodeOffset (type (bv 1)))
 (type VecMachLabel extern (enum))
+(model VecMachLabel (type (bv 1)))
 
 (type CondBrKind extern
   (enum
@@ -1441,7 +1447,7 @@
 ))
 
 (type MemLabel extern (enum))
-(model MemLabel (type !))
+(model MemLabel (type (bv 1)))
 (type SImm9 extern (enum))
 (model SImm9 (type (bv 9)))
 (type UImm12Scaled extern (enum))

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

@@ -1688,7 +1688,7 @@
 ;; General 128-bit case.
 ;;
 ;; TODO: much better codegen is possible with a constant amount.
-(rule (lower (has_type $I128 (rotl _ x y)))
+(rule rotl_i128 (lower (has_type $I128 (rotl _ x y)))
       (let ((val ValueRegs x)
             (amt Reg (value_regs_get y 0))
             (neg_amt Reg (sub $I64 (imm $I64 (ImmExtend.Zero) 128) amt))

cranelift/codegen/src/prelude_lower.isle

@@ -48,6 +48,7 @@
 (type VecReg extern (enum))
 (type VecWritableReg extern (enum))
 (type PReg (primitive PReg))
+(model PReg (type (bv 1)))
 
 ;; Construct a `ValueRegs` of one register.
 (decl value_reg (Reg) ValueRegs)
@@ -61,6 +62,11 @@
 
 ;; Construct a `ValueRegs` of two registers.
 (decl value_regs (Reg Reg) ValueRegs)
+(spec (value_regs arg1 arg2)
+  (provide
+    (= (:lo result) arg1)
+    (= (:hi result) arg2)))
+
 (extern constructor value_regs value_regs)
 
 ;; Construct a `WritableValueRegs` of two registers.
@@ -235,16 +241,23 @@
 ;;;; Common Mach Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (type MachLabel (primitive MachLabel))
+(model MachLabel (type (bv 1)))
 (type ValueLabel (primitive ValueLabel))
 (type UnwindInst (primitive UnwindInst))
+(model UnwindInst (type (bv 1)))
 (type ExternalName (primitive ExternalName))
+(model ExternalName (type (bv 1)))
 (type BoxExternalName (primitive BoxExternalName))
+(model BoxExternalName (type (bv 1)))
 (type RelocDistance (primitive RelocDistance))
 (type VecArgPair extern (enum))
+(model VecArgPair (type (bv 1)))
 (type VecRetPair extern (enum))
+(model VecRetPair (type (bv 1)))
 (type CallArgList extern (enum))
 (type MachLabelSlice extern (enum))
 (type BoxVecMachLabel extern (enum))
+(model BoxVecMachLabel (type (bv 1)))
 
 ;; Extract a the target from a MachLabelSlice with exactly one target.
 (decl single_target (MachLabel) MachLabelSlice)
@@ -425,7 +438,7 @@
 ;; Constant pool emission.
 
 (type VCodeConstant (primitive VCodeConstant))
-(model VCodeConstant (type !))
+(model VCodeConstant (type (bv 1)))
 
 ;; Add a u64 little-endian constant to the in-memory constant pool and
 ;; return a VCodeConstant index that refers to it. This is
@@ -502,7 +515,7 @@
                      (ProducesFlagsReturnsResultWithConsumer (inst MInst) (result Reg))))
 
 (model ProducesFlags
-      (type
+      (type-ext-enum
             (struct
                   (flags  (named NZCV))
                   (result (named Reg))
@@ -515,6 +528,7 @@
       (provide
             (= (:flags result) (:flags_out inst))
             (= (:result result) reg)
+            (= (widthof (:result result)) 64)
             (:has_result result)
       )
 )
@@ -570,7 +584,7 @@
                                                              (result ValueRegs))))
 
 (model ConsumesFlags
-      (type
+      (type-ext-enum
             (struct
                   (flags  (named NZCV))
                   (result (named Reg))
@@ -583,23 +597,52 @@
       (provide
             (= (:flags result) (:flags_in inst))
             (= (:result result) reg)
+            (= (widthof reg) 64)
             (:has_result result)
       )
 )
 
+(spec (ConsumesFlags.ConsumesFlagsSideEffect2 inst1 inst2)
+  (provide
+      (= (:flags result) (:flags_in inst1))
+      (= (:result result) zero_reg)
+      (= (widthof zero_reg) 64)
+      (= (:has_result result) false)))
+
 (spec (ConsumesFlags.ConsumesFlagsReturnsReg inst reg)
-      (provide
-            (= (:flags result) (:flags_in inst))
-            (= (:result result) reg)
-            (:has_result result)
-      )
+  (provide
+        (= (:flags result) (:flags_in inst))
+        (= (:result result) reg)
+        (= (widthof reg) 64)
+        (:has_result result)
+  )
 )
 
 (spec (ConsumesFlags.ConsumesFlagsSideEffect inst)
-      (provide
-            (= (:flags result) (:flags_in inst))
-            (not (:has_result result))
-      )
+  (provide
+        (= (:flags result) (:flags_in inst))
+        (= (:result result) zero_reg)
+        (= (widthof zero_reg) 64)
+        (= (:has_result result) false)
+  )
+)
+
+(spec (ConsumesFlags.ConsumesFlagsTwiceReturnsValueRegs inst1 inst2 regs)
+  (provide
+        (= (:flags result) (:flags_in inst1))
+        (= (:result result) (:lo regs))
+        (= (widthof (:lo regs)) 64)
+        (= (widthof (:hi regs)) 64)
+        (= (:has_result result) true)
+  )
+)
+
+(spec (ConsumesFlags.ConsumesFlagsFourTimesReturnsValueRegs inst1 inst2 inst3 inst4 regs)
+  (provide
+        (= (:flags result) (:flags_in inst1))
+        (= (:result result) (:lo regs))
+        (= (:has_result result) true)
+  )
 )
 
 ;; Get the produced register out of a ProducesFlags.
@@ -618,6 +661,7 @@
 ;; Helper for combining two flags-consumer instructions that return a
 ;; single Reg, giving a ConsumesFlags that returns both values in a
 ;; ValueRegs.
+(attr consumes_flags_concat (veri chain))
 (decl consumes_flags_concat (ConsumesFlags ConsumesFlags) ConsumesFlags)
 (rule (consumes_flags_concat (ConsumesFlags.ConsumesFlagsReturnsReg inst1 reg1)
                              (ConsumesFlags.ConsumesFlagsReturnsReg inst2 reg2))

cranelift/isle/isle/src/ast.rs

@@ -454,6 +454,13 @@ pub enum ModelType {
     Struct(Vec<ModelField>),
     /// Same model as the named type.
     Named(Ident),
+    ExtEnum(Vec<ModelVariant>),
+}
+
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct ModelVariant {
+    pub name: Ident,
+    pub fields: Vec<ModelField>,
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]
@@ -469,6 +476,8 @@ pub enum ModelValue {
     TypeValue(ModelType),
     /// Corresponds to ISLE external constants.
     ConstValue(SpecExpr),
+    // New ExtEnum model value 
+    ExtEnumValue(Vec<ModelField>),
 }
 
 /// A model of a construct into SMT-LIB (currently, types or enums)

cranelift/isle/isle/src/parser.rs

@@ -802,8 +802,26 @@ impl<'a> Parser<'a> {
         } else if self.eat_sym_str("const")? {
             let val = self.parse_spec_expr()?;
             ModelValue::ConstValue(val)
+        } else if self.eat_sym_str("type-ext-enum")? {
+            // Now we should be sitting right before (struct …)
+            self.expect_lparen()?;
+            if !self.eat_sym_str("struct")? {
+                return Err(self.error(pos, "expected (struct ...) inside type-ext-enum".to_string()));
+            }
+
+            let mut fields = Vec::new();
+            while !self.is_rparen() {
+                self.expect_lparen()?;
+                let fname = self.parse_ident()?;
+                let fty   = self.parse_model_type()?;
+                self.expect_rparen()?;
+                fields.push(ModelField { name: fname, ty: fty });
+            }
+            self.expect_rparen()?; 
+
+            ModelValue::ExtEnumValue(fields) 
         } else {
-            return Err(self.error(pos, "Model must be a type, enum or const".to_string()));
+            return Err(self.error(pos, "Model must be a type, enum, type-ext-enum, or const".to_string()));
         };
 
         self.expect_rparen()?; // end body

cranelift/isle/veri/veri/script/veri.sh

@@ -37,11 +37,21 @@ if [[ ! -d "${tmp_dir}" ]]; then
     exit 1
 fi
 
-# Run.
-cargo run --bin veri --profile "${profile}" -- \
-    --codegen-crate-dir ../../../codegen/ \
-    --work-dir "${tmp_dir}" \
-    --name "${arch}" \
-    --log-dir "${output_dir}/log" \
-    "$@" \
-    | tee "${output_dir}/${arch}.veri"
+# Standalone file mode
+# Detect --file in arguments and forward directly to cargo run
+if echo "$@" | grep -q -- "--file"; then
+  echo "[veri.sh] Running in file mode with args: $@"
+  # Write results to output/filemode.veri instead of arch-specific logs
+  cargo run --bin veri --profile "${profile}" -- "$@" \
+    | tee "${output_dir}/filemode.veri"
+else
+    # Normal arch-based single-rule mode 
+  echo "[veri.sh] Running in normal mode with arch=${arch}"
+    cargo run --bin veri --profile "${profile}" -- \
+        --codegen-crate-dir ../../../codegen/ \
+        --work-dir "${tmp_dir}" \
+        --name "${arch}" \
+        --log-dir "${output_dir}/log" \
+        "$@" \
+        | tee "${output_dir}/${arch}.veri"
+fi