Draft PR: Winnie enum work

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

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

@@ -570,7 +570,7 @@
                                                              (result ValueRegs))))
 
 (model ConsumesFlags
-      (type
+      (type-ext-enum
             (struct
                   (flags  (named NZCV))
                   (result (named Reg))
@@ -618,6 +618,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

cranelift/isle/veri/veri/src/bin/veri.rs

@@ -9,15 +9,19 @@ use cranelift_isle_veri::runner::{Filter, Runner, SolverBackend, SolverRule};
 struct Opts {
     /// Name of the ISLE compilation.
     #[arg(long, required = true)]
-    name: String,
+    name: Option<String>,
 
     /// Path to codegen crate directory.
     #[arg(long, required = true)]
-    codegen_crate_dir: std::path::PathBuf,
+    codegen_crate_dir: Option<std::path::PathBuf>,
 
     /// Working directory.
     #[arg(long, required = true)]
-    work_dir: std::path::PathBuf,
+    work_dir: Option<std::path::PathBuf>,
+
+    // run verifier on a standalone ISLE file
+    #[arg(long, conflicts_with_all = ["name", "codegen_crate_dir", "work_dir"])]
+    file: Option<std::path::PathBuf>,
 
     /// Filter expansions.
     #[arg(long = "filter", value_name = "FILTER")]
@@ -66,34 +70,80 @@ struct Opts {
 
 impl Opts {
     fn isle_input_files(&self) -> Result<Vec<std::path::PathBuf>> {
-        // Generate ISLE files.
-        let gen_dir = &self.work_dir;
-        generate_isle(gen_dir)?;
+        let name = self.name.as_ref().expect("missing ISLE compilation name");
+
+        let codegen_dir = self
+            .codegen_crate_dir
+            .as_ref()
+            .expect("missing codegen crate directory");
+
+        let work_dir = self.work_dir.as_ref().expect("missing working directory");
+
+        // Generate ISLE files into work_dir
+        // let gen_dir = &self.work_dir;
+        generate_isle(work_dir)?;
 
         // Lookup ISLE compilations.
-        let compilations = get_isle_compilations(&self.codegen_crate_dir, gen_dir);
+        let compilations = get_isle_compilations(codegen_dir, work_dir);
 
         // Return inputs from the matching compilation, if any.
         Ok(compilations
-            .lookup(&self.name)
-            .ok_or(format_err!("unknown ISLE compilation: {}", self.name))?
+            .lookup(name)
+            .ok_or_else(|| format_err!("unknown ISLE compilation: {}", name))?
             .paths()?)
     }
 }
 
 fn main() -> Result<()> {
     env_logger::builder().format_target(false).init();
     let opts = Opts::parse();
-
     // Setup thread pool.
     rayon::ThreadPoolBuilder::new()
         .num_threads(opts.num_threads)
         .build_global()?;
     log::info!("num theads: {}", rayon::current_num_threads());
 
+    // standalone file mode
+    if let Some(file) = opts.file {
+        println!("Running standalone mode on {:?}", file);
+        let inputs = vec![file];
+        let mut runner = Runner::from_files(&inputs, "test")?;
+        runner.include_first_rule_named();
+
+        // Configure runner
+        if !opts.filters.is_empty() {
+            runner.filters(&opts.filters);
+        } else {
+            runner.include_first_rule_named();
+        }
+        if opts.skip_todo {
+            runner.skip_tag("TODO");
+        }
+
+        runner.set_default_solver_backend(opts.solver_backend.into());
+        if !opts.ignore_solver_tags {
+            runner.add_solver_tag_rules();
+        }
+        for solver_rule in opts.solver_rules {
+            runner.add_solver_rule(solver_rule);
+        }
+
+        runner.set_timeout(Duration::from_secs(opts.timeout));
+        if let Some(log_dir) = opts.log_dir {
+            runner.set_log_dir(log_dir);
+        }
+        runner.set_results_to_log_dir(opts.results_to_log_dir);
+        runner.skip_solver(opts.skip_solver);
+        runner.debug(opts.debug);
+
+        return runner.run();
+    }
+
+    // Normal mode -- not standalone file mode
     // Read ISLE inputs.
     let inputs = opts.isle_input_files()?;
-    let root_term = if opts.name != "opt" {
+    // unwrap before comparing
+    let root_term = if opts.name.as_deref() != Some("opt") {
         "lower"
     } else {
         "simplify"

cranelift/isle/veri/veri/src/spec.rs

@@ -9,6 +9,8 @@ use std::{
     fmt::Debug,
 };
 
+use crate::types::Field;
+use crate::types::Enum;
 use crate::types::{Compound, Const};
 
 // QUESTION(mbm): do we need this layer independent of AST spec types and Veri-IR?
@@ -630,6 +632,18 @@ pub struct SpecEnv {
 }
 
 impl SpecEnv {
+    // collect type helper 
+
+    fn collect_types(&mut self, tyenv: &TypeEnv) {
+        for (i, ty) in tyenv.types.iter().enumerate() {
+            let tid = TypeId(i);
+            if let Some(compound) = crate::types::Compound::from_isle(ty, tyenv) {
+                self.type_model.insert(tid, compound);
+            }
+        }
+    }
+
+
     pub fn from_ast(defs: &[Def], termenv: &TermEnv, tyenv: &TypeEnv) -> Result<Self> {
         let mut env = Self {
             term_spec: HashMap::new(),
@@ -644,12 +658,16 @@ impl SpecEnv {
             macros: HashMap::new(),
         };
 
+        // populate type_model with enum from TypeEnv first 
+        env.collect_types(tyenv); 
+
         env.collect_models(defs, tyenv);
         env.derive_type_models(tyenv)?;
+        env.collect_specs(defs, termenv, tyenv)?;
         env.derive_enum_variant_specs(termenv, tyenv)?;
         env.collect_state(defs)?;
         env.collect_instantiations(defs, termenv, tyenv);
-        env.collect_specs(defs, termenv, tyenv)?;
+        // env.collect_specs(defs, termenv, tyenv)?;
         env.collect_attrs(defs, termenv, tyenv)?;
         env.collect_macros(defs);
         env.check_option_return_term_specs_uses_matches(termenv, tyenv)?;
@@ -658,12 +676,31 @@ impl SpecEnv {
         Ok(env)
     }
 
+    // helper function for ExtEnum
+    /// Borrow the base enum for a TypeId if present.
+    fn get_enum_from_typeid(&self, tid: TypeId) -> Option<&crate::types::Enum> {
+        match self.type_model.get(&tid)? {
+            crate::types::Compound::Enum(e) => Some(e),
+            crate::types::Compound::ExtEnum { base, .. } => Some(base),
+            _ => None,
+        }
+    }
+
+    /// Clone out an owned Enum for a TypeId (useful when constructing ExtEnum).
+    fn clone_enum_from_typeid(&self, tid: TypeId) -> Option<crate::types::Enum> {
+        self.get_enum_from_typeid(tid).cloned()
+    }
+
     fn collect_models(&mut self, defs: &[Def], tyenv: &TypeEnv) {
         for def in defs {
             if let ast::Def::Model(Model { name, val }) = def {
                 match val {
                     ast::ModelValue::TypeValue(model_type) => {
-                        self.set_model_type(name, model_type, tyenv);
+                        // only insert if this name hasn't been seen yet 
+                        let tid = tyenv.get_type_by_name(name).expect("type should exist");
+                        if !self.type_model.contains_key(&tid) {
+                            self.set_model_type(name, model_type, tyenv);
+                        }
                     }
                     ast::ModelValue::ConstValue(val) => {
                         // TODO(mbm): error on missing constant name rather than panic
@@ -672,6 +709,30 @@ impl SpecEnv {
                         // TODO(mbm): ensure the type of the expression matches the type of the
                         self.const_value.insert(sym, expr_from_ast(val));
                     }
+                    ast::ModelValue::ExtEnumValue(fields) => {
+                        // 1) Resolve the base type to a TypeId.
+                        let base_tid = tyenv
+                            .get_type_by_name(name)
+                            .expect("ext-enum base type should exist");
+
+                        // 2) Clone the existing base enum compound.
+                        let base_enum = self
+                            .clone_enum_from_typeid(base_tid)
+                            .expect("expected base enum to be defined for type-ext-enum");
+
+                        // 3) Lower the extra fields to veri types::Field.
+                        let extra: Vec<Field> = fields
+                            .iter()
+                            .map(|mf| Field {
+                                name: mf.name.clone(),
+                                ty: Compound::from_ast(&mf.ty),
+                            })
+                            .collect();
+
+                        // 4) Build Compound::ExtEnum and overwrite the entry for this TypeId.
+                        let compound = Compound::ExtEnum { base: base_enum, extra };
+                        self.type_model.insert(base_tid, compound);
+                    }
                 }
             }
         }
@@ -697,7 +758,15 @@ impl SpecEnv {
 
     fn derive_enum_variant_specs(&mut self, termenv: &TermEnv, tyenv: &TypeEnv) -> Result<()> {
         for model in self.type_model.values() {
-            if let Compound::Enum(e) = model {
+
+            // handle both Enum and ExtEnum 
+            let enum_ref: Option<&Enum> = match model {
+                Compound::Enum(e) => Some(e),
+                Compound::ExtEnum { base, .. } => Some(base),
+                _ => None,
+            };
+
+            if let Some(e) = enum_ref {
                 for variant in &e.variants {
                     // Lookup the corresponding term.
                     let full_name = ast::Variant::full_name(&e.name, &variant.name);
@@ -708,6 +777,11 @@ impl SpecEnv {
                                 "could not find variant term {name}",
                                 name = full_name.0
                             ))?;
+
+                    // guard: skip auto-gen if spec already exists for this
+                    if self.term_spec.contains_key(&term_id) {
+                        continue;
+                    }
 
                     // Synthesize spec.
                     let pos = variant.name.1;