diff --git a/cranelift/codegen/src/inst_specs.isle b/cranelift/codegen/src/inst_specs.isle index a45e545e4112..7fac40d5e3cc 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 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..8fd46463ba65 100644 --- a/cranelift/codegen/src/prelude_lower.isle +++ b/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)) 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/spec.rs b/cranelift/isle/veri/veri/src/spec.rs index 0c5c212ac641..d2af49c5ded5 100644 --- a/cranelift/isle/veri/veri/src/spec.rs +++ b/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 { 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 { + 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 = 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; diff --git a/cranelift/isle/veri/veri/src/types.rs b/cranelift/isle/veri/veri/src/types.rs index 156703790f27..c1b89d7c0dad 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,38 @@ 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 +332,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 +351,11 @@ 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 +381,18 @@ 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..110083d36c38 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), @@ -479,6 +480,7 @@ impl Symbolic { fn as_enum(&self) -> Option<&SymbolicEnum> { match self { Self::Enum(e) => Some(e), + Self::ExtEnum(e, _) => Some(e), // unwrap ExtEnum _ => None, } } @@ -539,6 +541,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 +711,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 +751,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 +785,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!( @@ -2232,6 +2303,48 @@ 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)