diff --git a/cranelift/codegen/src/inst_specs.isle b/cranelift/codegen/src/inst_specs.isle index a45e545e4112..c7a6edf229ac 100644 --- a/cranelift/codegen/src/inst_specs.isle +++ b/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)))) diff --git a/cranelift/codegen/src/isa/aarch64/inst.isle b/cranelift/codegen/src/isa/aarch64/inst.isle index dd3e4bfee9d9..29954f52af30 100644 --- a/cranelift/codegen/src/isa/aarch64/inst.isle +++ b/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)) diff --git a/cranelift/codegen/src/isa/aarch64/lower.isle b/cranelift/codegen/src/isa/aarch64/lower.isle index d3402a8e3af7..6bcf9d8b28be 100644 --- a/cranelift/codegen/src/isa/aarch64/lower.isle +++ b/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)) diff --git a/cranelift/codegen/src/prelude_lower.isle b/cranelift/codegen/src/prelude_lower.isle index ab5dcac22a12..24ab07d25800 100644 --- a/cranelift/codegen/src/prelude_lower.isle +++ b/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)) diff --git a/cranelift/isle/isle/src/ast.rs b/cranelift/isle/isle/src/ast.rs index 0d3f84624e45..92f653a1c3f3 100644 --- a/cranelift/isle/isle/src/ast.rs +++ b/cranelift/isle/isle/src/ast.rs @@ -454,6 +454,13 @@ pub enum ModelType { Struct(Vec), /// Same model as the named type. Named(Ident), + ExtEnum(Vec), +} + +#[derive(Clone, PartialEq, Eq, Debug)] +pub struct ModelVariant { + pub name: Ident, + pub fields: Vec, } #[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), } /// A model of a construct into SMT-LIB (currently, types or enums) diff --git a/cranelift/isle/isle/src/parser.rs b/cranelift/isle/isle/src/parser.rs index ef747d2cc72e..5fe74ee051c6 100644 --- a/cranelift/isle/isle/src/parser.rs +++ b/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 diff --git a/cranelift/isle/veri/veri/script/veri.sh b/cranelift/isle/veri/veri/script/veri.sh index bf3ba763dd91..12eb5436022f 100755 --- a/cranelift/isle/veri/veri/script/veri.sh +++ b/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 diff --git a/cranelift/isle/veri/veri/src/bin/veri.rs b/cranelift/isle/veri/veri/src/bin/veri.rs index ee6346a0c5e2..1932d2790914 100644 --- a/cranelift/isle/veri/veri/src/bin/veri.rs +++ b/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, /// Path to codegen crate directory. #[arg(long, required = true)] - codegen_crate_dir: std::path::PathBuf, + codegen_crate_dir: Option, /// Working directory. #[arg(long, required = true)] - work_dir: std::path::PathBuf, + work_dir: Option, + + // run verifier on a standalone ISLE file + #[arg(long, conflicts_with_all = ["name", "codegen_crate_dir", "work_dir"])] + file: Option, /// Filter expansions. #[arg(long = "filter", value_name = "FILTER")] @@ -66,17 +70,26 @@ struct Opts { impl Opts { fn isle_input_files(&self) -> Result> { - // 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()?) } } @@ -84,16 +97,53 @@ impl Opts { 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" diff --git a/cranelift/isle/veri/veri/src/solver.rs b/cranelift/isle/veri/veri/src/solver.rs index 41aec640f203..5a6271235e74 100644 --- a/cranelift/isle/veri/veri/src/solver.rs +++ b/cranelift/isle/veri/veri/src/solver.rs @@ -168,7 +168,45 @@ impl<'a> Solver<'a> { // Check let verdict = match self.check()? { - Response::Sat => Verification::Failure(self.model()?), + Response::Sat => { + // Winnie TODO: iterate over &self.conditions.assertions, determine which ones + // are False in the SMT model, display them to user + // let as_exprs: Vec = self.conditions.assertions.iter().map(|x| self.expr_atom(*x)).collect(); + + // store both original assertion ID and SMT expression created from it + let assertion_exprs: Vec<(ExprId, SExpr)> = + self.conditions.assertions + .iter() + .map(|id| (*id, self.expr_atom(*id))) + .collect(); + + // let vals = self.smt.get_value(as_exprs).unwrap(); + let exprs: Vec = assertion_exprs.iter().map(|(_, e)| e.clone()).collect(); + + let vals = self.smt.get_value(exprs)?; + + // for (variable, value) in vals { + // if value == self.smt.false_() { + // // Winnie TODO: try to use the print_model logic to print something useful here + // println!("Failed assertion:\n{}", self.smt.display(variable)); + // } + // } + + // iterate while keeping context + for ((assert_id, _s_expr), (_, value)) in + assertion_exprs.iter().zip(vals.into_iter()) + { + if value == self.smt.false_() { + // Now we know exactly WHICH assertion failed + // let assertion = self.conditions.assertions.get(assert_id.index()); + let ir_expr = &self.conditions.exprs[assert_id.index()]; + // print human-readable assertion + println!("Failed assertion: {}", ir_expr); + } + } + + Verification::Failure(self.model()?) + } Response::Unsat => Verification::Success, Response::Unknown => Verification::Unknown, }; diff --git a/cranelift/isle/veri/veri/src/spec.rs b/cranelift/isle/veri/veri/src/spec.rs index 0c5c212ac641..685ed5d27bee 100644 --- a/cranelift/isle/veri/veri/src/spec.rs +++ b/cranelift/isle/veri/veri/src/spec.rs @@ -1,6 +1,6 @@ use anyhow::{bail, format_err, Ok, Result}; use cranelift_isle::{ - ast::{self, AttrKind, AttrTarget, Def, Ident, Model, ModelType, Modifies, SpecOp}, + ast::{self, AttrKind, AttrTarget, Def, Ident, Model, Modifies, SpecOp}, lexer::Pos, sema::{ReturnKind, RuleId, Sym, Term, TermEnv, TermId, TypeEnv, TypeId}, }; @@ -9,6 +9,8 @@ use std::{ fmt::Debug, }; +use crate::types::Enum; +use crate::types::Field; use crate::types::{Compound, Const}; // QUESTION(mbm): do we need this layer independent of AST spec types and Veri-IR? @@ -513,6 +515,7 @@ impl FieldInit { // QUESTION(mbm): should we make the result explicit in the spec syntax? static RESULT: &str = "result"; +#[derive(Clone)] pub struct Spec { pub args: Vec, pub ret: Ident, @@ -622,6 +625,9 @@ pub struct SpecEnv { /// Model for the given type. pub type_model: HashMap, + // Track which types are derived (auto-generated) + pub derived_types: HashSet, + /// Value for the given constant. pub const_value: HashMap, @@ -640,16 +646,17 @@ impl SpecEnv { priority: HashSet::new(), rule_tags: HashMap::new(), type_model: HashMap::new(), + derived_types: HashSet::new(), const_value: HashMap::new(), macros: HashMap::new(), }; - env.collect_models(defs, tyenv); + env.collect_specs(defs, termenv, tyenv)?; env.derive_type_models(tyenv)?; + env.collect_models(defs, 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_attrs(defs, termenv, tyenv)?; env.collect_macros(defs); env.check_option_return_term_specs_uses_matches(termenv, tyenv)?; @@ -658,12 +665,58 @@ 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 { + 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"); + + // new model compound + let new_model = Compound::from_ast(model_type); + + if let Some(_existing) = self.type_model.get(&tid) { + // --- CASE 1: ext-enum --- + if let Compound::ExtEnum { .. } = new_model { + if self.derived_types.contains(&tid) { + // good: upgrade derived enum → ext-enum + self.type_model.insert(tid, new_model); + self.derived_types.remove(&tid); + continue; + } else { + panic!("cannot ext-enum a non-enum type: {}", name.0); + } + } + + // --- CASE 2: replacing a derived enum --- + if self.derived_types.contains(&tid) { + self.type_model.insert(tid, new_model); + self.derived_types.remove(&tid); + continue; + } + + // --- CASE 3: any other duplicate --- + panic!("duplicate type model: {}", name.0); + } else { + // first definition + self.type_model.insert(tid, new_model); + } } ast::ModelValue::ConstValue(val) => { // TODO(mbm): error on missing constant name rather than panic @@ -672,6 +725,33 @@ 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 = 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); + } } } } @@ -679,25 +759,26 @@ impl SpecEnv { fn derive_type_models(&mut self, tyenv: &TypeEnv) -> Result<()> { for ty in &tyenv.types { - // Has an explicit model already been specified? - if self.has_model(ty.id()) { - continue; - } - // Derive a model from ISLE type, if possible. - let Some(derived_type) = Compound::from_isle(ty, tyenv) else { - continue; + if let Some(derived_type) = Compound::from_isle(ty, tyenv) { + // register derived type and mark derived + self.type_model.insert(ty.id(), derived_type); + self.derived_types.insert(ty.id()); }; - - // Register derived. - self.type_model.insert(ty.id(), derived_type); } Ok(()) } 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); @@ -709,7 +790,12 @@ impl SpecEnv { name = full_name.0 ))?; - // Synthesize spec. + // If the user wrote a spec already, do not autogenerate + if self.term_spec.contains_key(&term_id) { + continue; + } + + // build a fresh synthesize spec for the variant. let pos = variant.name.1; let args: Vec = variant.fields.iter().map(|f| f.name.clone()).collect(); let constructor = Positioned::new( @@ -722,7 +808,7 @@ impl SpecEnv { ); let mut spec = Spec::new(); - spec.args = args; + spec.args = args.clone(); let ret = var_from_ident(spec.ret.clone()); spec.provides .push(Positioned::new(pos, ExprKind::Eq(ret, constructor))); @@ -737,20 +823,37 @@ impl SpecEnv { Ok(()) } - fn set_model_type(&mut self, name: &Ident, model_type: &ModelType, tyenv: &TypeEnv) { - // TODO(mbm): error on missing type rather than panic - let type_id = tyenv - .get_type_by_name(name) - .expect("type name should be defined"); - // TODO(mbm): error on duplicate model - assert!( - !self.type_model.contains_key(&type_id), - "duplicate type model: {name}", - name = name.0 - ); - self.type_model - .insert(type_id, Compound::from_ast(model_type)); - } + // fn set_model_type(&mut self, name: &Ident, model_type: &ModelType, tyenv: &TypeEnv) { + // // TODO(mbm): error on missing type rather than panic + // let type_id = tyenv + // .get_type_by_name(name) + // .expect("type name should be defined"); + // // TODO(mbm): error on duplicate model + // let compound = Compound::from_ast(model_type); + + // if let Some(existing) = self.type_model.get(&type_id) { + // match (existing, &compound) { + // (Compound::Enum(_), Compound::ExtEnum { .. }) => { + // // replace Enum with ExtEnum + // self.type_model.insert(type_id, compound); + // return; + // } + // // if already enum and the new one is also enum -> error + // (Compound::Enum(_), Compound::Enum(_)) =>{ + // panic!("duplicate enum model: {}", name.0); + // } + // (Compound::ExtEnum{..}, Compound::ExtEnum{..}) =>{ + // panic!("duplicate extenum model: {}", name.0); + // } + // // otherwise: real conflict + // _ => { + // panic!("duplicate type model: {}", name.0); + // } + // } + // } else { + // self.type_model.insert(type_id, compound); + // } + // } fn collect_state(&mut self, defs: &[Def]) -> Result<()> { // Collect states. diff --git a/cranelift/isle/veri/veri/src/type_inference.rs b/cranelift/isle/veri/veri/src/type_inference.rs index 062ea33afd62..8e7c418f1a5a 100644 --- a/cranelift/isle/veri/veri/src/type_inference.rs +++ b/cranelift/isle/veri/veri/src/type_inference.rs @@ -910,6 +910,13 @@ impl Solver { let status = if self.assignment.is_concrete() { Status::Solved } else { + log::debug!("Underconstrained: listing all non-concrete type variables:"); + + for (var, tv) in self.assignment.expr_type_value.iter() { + if !tv.ty().is_concrete() { + log::debug!(" var {:?}: {:?}", var, tv.ty()); + } + } Status::Underconstrained }; return vec![Solution { @@ -976,6 +983,13 @@ impl Solver { format!("concrete type error between types:\n\t{existing}\n\t{tv}"), )) } else { + // debug for inapplicable + log::debug!( + "INAPPLICABLE: failed to merge type values at ExprId({}): existing={:?}, new={:?}", + x.index(), + existing, + tv + ); Status::Inapplicable(Conflict::new( x, format!("inapplicable set type value: {existing:?} = {tv:?}"), diff --git a/cranelift/isle/veri/veri/src/types.rs b/cranelift/isle/veri/veri/src/types.rs index 156703790f27..b58ddac24519 100644 --- a/cranelift/isle/veri/veri/src/types.rs +++ b/cranelift/isle/veri/veri/src/types.rs @@ -114,6 +114,7 @@ pub enum Compound { Primitive(Type), Struct(Vec), Enum(Enum), + ExtEnum { base: Enum, extra: Vec }, // new compound type: ExtEnum // TODO(mbm): intern name identifier Named(Ident), } @@ -263,6 +264,39 @@ impl Compound { .collect(), ), ModelType::Named(name) => Self::Named(name.clone()), + ModelType::ExtEnum(variants) => { + // Build `types::Variant`s + let lowered_variants: Vec = variants + .iter() + .enumerate() + .map(|(i, mv)| { + let fields = mv + .fields + .iter() + .map(|mf| Field { + name: mf.name.clone(), + ty: Self::from_ast(&mf.ty), + }) + .collect(); + + Variant { + name: mv.name.clone(), + id: VariantId(i), + fields, + } + }) + .collect(); + + // Wrap in our Compound::ExtEnum + Self::ExtEnum { + base: Enum { + id: TypeId(0), // placeholder, depends on type assignment + name: Ident("anon_extenum".to_string(), Pos::default()), // minimal Ident + variants: lowered_variants, + }, + extra: vec![], // can fill later if ExtEnum carries extras + } + } } } @@ -299,6 +333,7 @@ impl Compound { pub fn as_enum(&self) -> Option<&Enum> { match self { Compound::Enum(e) => Some(e), + Compound::ExtEnum { base, .. } => Some(base), _ => None, } } @@ -317,6 +352,14 @@ impl Compound { .collect::>()?, )), Compound::Enum(e) => Ok(Compound::Enum(e.resolve(lookup)?)), + Compound::ExtEnum { base, extra } => { + let base = base.resolve(lookup)?; + let extra = extra + .iter() + .map(|f| f.resolve(lookup)) + .collect::>()?; + Ok(Compound::ExtEnum { base, extra }) + } Compound::Named(name) => { // TODO(mbm): named type model cycle detection let ty = lookup(name)?; @@ -342,6 +385,19 @@ impl std::fmt::Display for Compound { Compound::Enum(e) => { write!(f, "enum({name})", name = e.name.0,) } + Compound::ExtEnum { base, extra } => { + // format: "extenum(EnumName { ...extra fields... })" + write!( + f, + "extenum({} + [{}])", + base.name.0, + extra + .iter() + .map(|f| format!("{}: {}", f.name.0, f.ty)) + .collect::>() + .join(", ") + ) + } Compound::Named(name) => write!(f, "{}", name.0), } } diff --git a/cranelift/isle/veri/veri/src/veri.rs b/cranelift/isle/veri/veri/src/veri.rs index fc4d55883aa2..879f10f261e0 100644 --- a/cranelift/isle/veri/veri/src/veri.rs +++ b/cranelift/isle/veri/veri/src/veri.rs @@ -456,6 +456,7 @@ pub enum Symbolic { Scalar(ExprId), Struct(Vec), Enum(SymbolicEnum), + ExtEnum(SymbolicEnum, Vec), // ext enum with extra fields Option(SymbolicOption), Tuple(Vec), Macro(Macro), @@ -472,6 +473,7 @@ impl Symbolic { fn as_struct(&self) -> Option<&Vec> { match self { Self::Struct(fields) => Some(fields), + // Self::ExtEnum(_, fields) => Some (fields), _ => None, } } @@ -479,6 +481,7 @@ impl Symbolic { fn as_enum(&self) -> Option<&SymbolicEnum> { match self { Self::Enum(e) => Some(e), + Self::ExtEnum(e, _) => Some(e), _ => None, } } @@ -539,6 +542,41 @@ impl Symbolic { value: variant.value.eval(model)?, }))) } + Symbolic::ExtEnum(e, extra) => { + // 1. Same as Enum: resolve discriminant and variant + let discriminant: usize = model + .get(&e.discriminant) + .ok_or(format_err!("undefined discriminant in model"))? + .as_int() + .ok_or(format_err!( + "model value for discriminant is not an integer" + ))? + .try_into() + .unwrap(); + let variant = e + .variants + .iter() + .find(|v| v.discriminant == discriminant) + .ok_or(format_err!("no variant with discriminant {discriminant}"))?; + + let base_value = Value::Enum(Box::new(VariantValue { + name: variant.name.clone(), + value: variant.value.eval(model)?, + })); + + // 2. Evaluate extra fields like a struct + let extra_values = extra + .iter() + .map(|f| f.eval(model)) + .collect::>>()?; + + // 3. Wrap into a new Value variant (you’ll need a `Value::ExtEnum` to store this) + Ok(Value::ExtEnum { + base: Box::new(base_value), + extra: extra_values, + }) + } + Symbolic::Option(opt) => match model.get(&opt.some) { Some(Const::Bool(true)) => { Ok(Value::Option(Some(Box::new(opt.inner.eval(model)?)))) @@ -674,6 +712,24 @@ impl std::fmt::Display for Symbolic { .collect::>() .join(", ") ), + Symbolic::ExtEnum(base_enum, extra_fields) => { + write!( + f, + "extenum({discriminant}, {variants}, extras: {{{extras}}})", + discriminant = base_enum.discriminant.index(), + variants = base_enum + .variants + .iter() + .map(|v| v.to_string()) + .collect::>() + .join(", "), + extras = extra_fields + .iter() + .map(|f| format!("{}: {}", f.name, f.value)) + .collect::>() + .join(", ") + ) + } Symbolic::Option(SymbolicOption { some, inner }) => { write!(f, "Option{{some: {}, inner: {inner}}}", some.index()) } @@ -696,6 +752,10 @@ pub enum Value { Const(Const), Struct(Vec), Enum(Box), + ExtEnum { + base: Box, // base enum value + extra: Vec, // evaluated extra fields + }, Option(Option>), Tuple(Vec), } @@ -726,6 +786,18 @@ impl std::fmt::Display for Value { .join(", ") ), Value::Enum(v) => write!(f, "{name} {value}", name = v.name, value = v.value), + Value::ExtEnum { base, extra } => { + write!( + f, + "extenum({base}, extras: {{{extras}}})", + base = base, + extras = extra + .iter() + .map(|f| format!("{}: {}", f.name, f.value)) + .collect::>() + .join(", ") + ) + } Value::Option(Some(v)) => write!(f, "Some({v})"), Value::Option(None) => write!(f, "None"), Value::Tuple(elements) => write!( @@ -907,6 +979,12 @@ impl Conditions { ); } + // TODO winnie: this might be a smarter place to print + + // still print everything from before + // then print + // FAILED ASSERTIONS: + Ok(()) } @@ -1874,21 +1952,42 @@ impl<'a> ConditionsBuilder<'a> { } fn spec_field(&mut self, name: &Ident, v: Symbolic) -> Result { - log::trace!("access field {name} from {v}", name = name.0); + log::trace!("access field {} from {}", name.0, v); - let fields = v - .as_struct() - .ok_or(self.error("field access from non-struct value"))?; + // 1. If ExtEnum: check extra fields FIRST + if let Symbolic::ExtEnum(_base_enum, extra_fields) = &v { + if let Some(f) = extra_fields.iter().find(|f| f.name == name.0) { + return Ok(f.value.clone()); + } - let field = fields - .iter() - .find(|f| f.name == name.0) - .ok_or(self.error(format!( - "attempt to access nonexistent struct field: {}", - name.0 - )))?; + // 2. If not found, fall through to base enum variant payload + if let Some(e) = v.as_enum() { + for variant in &e.variants { + if let Ok(fields) = variant.fields() { + if let Some(f) = fields.iter().find(|f| f.name == name.0) { + return Ok(f.value.clone()); + } + } + } + } + + // 3. Otherwise: truly nonexistent + return Err(self.error(format!("attempt to access nonexistent field: {}", name.0))); + } + + // Normal struct case + if let Some(fields) = v.as_struct() { + if let Some(f) = fields.iter().find(|f| f.name == name.0) { + return Ok(f.value.clone()); + } else { + return Err(self.error(format!( + "attempt to access nonexistent struct field: {}", + name.0 + ))); + } + } - Ok(field.value.clone()) + Err(self.error(format!("field access from non-struct value: {}", name.0))) } fn spec_discriminator(&mut self, name: &Ident, v: Symbolic) -> Result { @@ -2128,6 +2227,27 @@ impl<'a> ConditionsBuilder<'a> { Ok(self.all(equalities)) } + (Symbolic::Enum(u), Symbolic::ExtEnum(v, _extra)) + | (Symbolic::ExtEnum(v, _extra), Symbolic::Enum(u)) => { + // Discriminant equality + let discriminants_eq = self.exprs_equal(u.discriminant, v.discriminant); + let mut equalities = vec![discriminants_eq]; + + // Compare only the base variant payloads + assert_eq!(u.variants.len(), v.variants.len()); + let variants_eq = zip(&u.variants, &v.variants) + .map(|(uv, vv)| { + assert_eq!(uv.name, vv.name); + let ud = self.discriminator(&u, uv); + let eq = self.values_equal(uv.value.clone(), vv.value.clone())?; + Ok(self.dedup_expr(Expr::Imp(ud, eq))) + }) + .collect::>>()?; + + equalities.extend(variants_eq); + Ok(self.all(equalities)) + } + (Symbolic::Tuple(us), Symbolic::Tuple(vs)) => { // Field-wise equality. // TODO(mbm): can we expect that tuples are the same length? @@ -2232,6 +2352,43 @@ impl<'a> ConditionsBuilder<'a> { .collect::>()?; Ok(self.new_enum(e.id, discriminant, variants)?) } + Compound::ExtEnum { base, extra } => { + // Build the SymbolicEnum exactly like the `Enum` arm does. + + // 1) discriminator variable for the enum + let discriminant = + self.alloc_variable(Type::Int, Variable::component_name(&name, "discriminant")); + + // 2) per-variant payloads + let variants = base + .variants + .iter() + .map(|v| self.alloc_variant(v, name.clone())) + .collect::>()?; + + // 3) assemble a SymbolicEnum (same fields your `Enum` arm uses) + let sym_enum = SymbolicEnum { + ty: base.id, + discriminant, + variants, + }; + + // Now allocate the extra struct-like fields. + let extra_syms = extra + .iter() + .map(|f| { + Ok(SymbolicField { + name: f.name.0.clone(), + value: self + .alloc_value(&f.ty, Variable::component_name(&name, &f.name.0))?, + }) + }) + .collect::>>()?; + + // `Symbolic::ExtEnum` is a *tuple* variant: (SymbolicEnum, Vec) + Ok(Symbolic::ExtEnum(sym_enum, extra_syms)) + } + Compound::Named(_) => { let ty = self.prog.specenv.resolve_type(ty, &self.prog.tyenv)?; self.alloc_value(&ty, name)