diff --git a/isla-lib/src/bitvector.rs b/isla-lib/src/bitvector.rs index fa26e6ab..8d6e0601 100644 --- a/isla-lib/src/bitvector.rs +++ b/isla-lib/src/bitvector.rs @@ -214,6 +214,8 @@ where fn leading_zeros(self) -> u32; + fn trailing_zeros(self) -> u32; + fn from_u8(value: u8) -> Self; fn from_u16(value: u16) -> Self; diff --git a/isla-lib/src/bitvector/b129.rs b/isla-lib/src/bitvector/b129.rs index ffa7e6f2..4c2d7fee 100644 --- a/isla-lib/src/bitvector/b129.rs +++ b/isla-lib/src/bitvector/b129.rs @@ -247,6 +247,18 @@ impl BV for B129 { } } + fn trailing_zeros(self) -> u32 { + if self.bits == 0 { + if self.tag { + self.len - 1 + } else { + self.len + } + } else { + self.bits.trailing_zeros() + } + } + fn from_u8(value: u8) -> Self { B129 { len: 8, tag: false, bits: value as u128 } } diff --git a/isla-lib/src/bitvector/b64.rs b/isla-lib/src/bitvector/b64.rs index 2664aba5..7c861623 100644 --- a/isla-lib/src/bitvector/b64.rs +++ b/isla-lib/src/bitvector/b64.rs @@ -191,6 +191,14 @@ impl BV for B64 { self.bits.leading_zeros() - (64 - self.len) } + fn trailing_zeros(self) -> u32 { + if self.bits == 0 { + self.len + } else { + self.bits.trailing_zeros() + } + } + fn from_u8(value: u8) -> Self { B64 { len: 8, bits: value as u64 } } diff --git a/isla-lib/src/memory.rs b/isla-lib/src/memory.rs index 75536d88..eac1e202 100644 --- a/isla-lib/src/memory.rs +++ b/isla-lib/src/memory.rs @@ -538,14 +538,20 @@ impl Memory { ExecError::BadRead("Possible symbolic address overlap"), solver, )? { - Overlap::Unique(concrete_addr) => self.read( - read_kind, - Val::Bits(B::new(concrete_addr, 64)), - Val::I128(bytes as i128), - solver, - tag, - opts, - ), + Overlap::Unique(concrete_addr) => { + // Use the symbolic address's own width, not a hardcoded 64 — + // that assumption held while every target was a 64-bit + // architecture, but breaks for a 32-bit target's addresses. + let addr_width = solver.length(symbolic_addr).unwrap_or(64); + self.read( + read_kind, + Val::Bits(B::new(concrete_addr, addr_width)), + Val::I128(bytes as i128), + solver, + tag, + opts, + ) + } Overlap::NoOverlap => { self.read_symbolic(read_kind, address, bytes, solver, tag, opts, DEFAULT_REGION_NAME) } diff --git a/isla-lib/src/primop.rs b/isla-lib/src/primop.rs index 6be9e51d..740bab84 100644 --- a/isla-lib/src/primop.rs +++ b/isla-lib/src/primop.rs @@ -52,7 +52,7 @@ use crate::bitvector::b64::B64; use crate::bitvector::BV; use crate::error::ExecError; use crate::executor::LocalFrame; -use crate::ir::{BitsSegment, Reset, UVal, Val, ELF_ENTRY}; +use crate::ir::{BitsSegment, Name, Reset, UVal, Val, ELF_ENTRY}; use crate::primop_util::*; use crate::smt::smtlib::*; use crate::smt::*; @@ -1433,6 +1433,50 @@ pub(crate) fn vector_access( Some(elem) => Ok(elem.clone()), None => Err(ExecError::OutOfBounds("vector_access")), }, + // Struct-typed vector elements (e.g. RISC-V's `vector(64, Pmpcfg_ent)`, + // a vector of bitfield structs) can't go through the scalar + // smt_value path below — smt_value has no case for Val::Struct, it + // only knows how to turn a single bitvector-shaped value into an + // SMT expression. Build the ITE selection per field instead, + // producing a new Val::Struct whose every field is its own ITE + // chain over that field across all elements. Every other element + // shape (the common case — plain bitvectors) keeps the original + // single-expression ITE chain below. + (Val::Vector(vec), Val::Symbolic(n)) if matches!(vec.first(), Some(Val::Struct(_))) => { + let field_names: Vec = match vec.first() { + Some(Val::Struct(fields)) => fields.keys().copied().collect(), + _ => unreachable!(), + }; + let mut result_fields: HashMap, ahash::RandomState> = HashMap::default(); + for field_name in field_names { + let mut it = vec.iter().enumerate().rev(); + let (_, last_item) = it.next().unwrap(); + let last_field = match last_item { + Val::Struct(fields) => fields + .get(&field_name) + .ok_or_else(|| ExecError::Type(format!("vector_access missing struct field {:?}", field_name), info))?, + _ => return Err(ExecError::Type(format!("vector_access {:?} {:?}: inconsistent element types", &vec, &n), info)), + }; + let mut exp = smt_value(last_field, info)?; + for (i, item) in it { + let field_val = match item { + Val::Struct(fields) => fields + .get(&field_name) + .ok_or_else(|| ExecError::Type(format!("vector_access missing struct field {:?}", field_name), info))?, + _ => return Err(ExecError::Type(format!("vector_access {:?} {:?}: inconsistent element types", &vec, &n), info)), + }; + exp = Exp::Ite( + Box::new(Exp::Eq(Box::new(Exp::Var(n)), Box::new(bits64(i as u64, 128)))), + Box::new(smt_value(field_val, info)?), + Box::new(exp), + ); + } + let var = solver.fresh(); + solver.add(Def::DefineConst(var, exp)); + result_fields.insert(field_name, Val::Symbolic(var)); + } + Ok(Val::Struct(result_fields)) + } (Val::Vector(vec), Val::Symbolic(n)) => { let mut it = vec.iter().enumerate().rev(); if let Some((_, last_item)) = it.next() { @@ -1722,6 +1766,43 @@ pub fn vector_update( Ok(Val::Vector(vec)) } Val::Symbolic(n) => { + // Struct-typed vector elements (e.g. RISC-V's + // `vector(64, Pmpcfg_ent)`) can't go through the scalar + // smt_value path below — smt_value has no case for + // Val::Struct. Build the ITE per field instead: each + // element becomes a fresh Val::Struct whose every field is + // `if n == i then new_value.field else old_elem.field`. See + // the analogous fix in vector_access above, and PMP_PLAN.md. + if matches!(vec.first(), Some(Val::Struct(_))) { + let new_fields = match &args[2] { + Val::Struct(fields) => fields.clone(), + _ => return Err(ExecError::Type(format!("vector_update {:?}: new value is not a struct", &args[2]), info)), + }; + for (i, item) in vec.iter_mut().enumerate() { + let old_fields = match item { + Val::Struct(fields) => fields.clone(), + _ => return Err(ExecError::Type(format!("vector_update {:?}: inconsistent element types", item), info)), + }; + let mut result_fields: HashMap, ahash::RandomState> = HashMap::default(); + for (field_name, new_field_val) in &new_fields { + let old_field_val = old_fields + .get(field_name) + .ok_or_else(|| ExecError::Type(format!("vector_update missing struct field {:?}", field_name), info))?; + let var = solver.fresh(); + solver.add(Def::DefineConst( + var, + Exp::Ite( + Box::new(Exp::Eq(Box::new(Exp::Var(n)), Box::new(bits64(i as u64, 128)))), + Box::new(smt_value(new_field_val, info)?), + Box::new(smt_value(old_field_val, info)?), + ), + )); + result_fields.insert(*field_name, Val::Symbolic(var)); + } + *item = Val::Struct(result_fields); + } + return Ok(Val::Vector(vec)); + } for (i, item) in vec.iter_mut().enumerate() { let var = solver.fresh(); solver.add(Def::DefineConst( @@ -2471,6 +2552,95 @@ fn count_leading_zeros(bv: Val, solver: &mut Solver, info: SourceLo } } +// LR/SC reservation-set primops (RISC-V `sys/sys_reservation.sail`): the model +// declares these as externs with no isla-specific implementation, and treats +// reservation state as maintained entirely outside the model. Stubbed here as +// stateless, conservative defaults (reservation never valid/matched) — correct +// for any test that doesn't exercise LR/SC itself, and calls unblock elsewhere +// (e.g. reset_sys()'s unconditional cancel_reservation()) that would otherwise +// fail with VariableNotFound since the primop was previously entirely absent. +fn cancel_reservation(_: Val, _solver: &mut Solver, _info: SourceLoc) -> Result, ExecError> { + Ok(Val::Unit) +} + +fn valid_reservation(_: Val, _solver: &mut Solver, _info: SourceLoc) -> Result, ExecError> { + Ok(Val::Bool(false)) +} + +fn match_reservation(_: Val, _solver: &mut Solver, _info: SourceLoc) -> Result, ExecError> { + Ok(Val::Bool(false)) +} + +fn load_reservation( + _addr: Val, + _width: Val, + _solver: &mut Solver, + _info: SourceLoc, +) -> Result, ExecError> { + Ok(Val::Unit) +} + +// Mirrors smt_clz above but checks the low half first instead of the high half. +fn smt_ctz(bv: Sym, len: u32, solver: &mut Solver, info: SourceLoc) -> Sym { + if len == 1 { + solver.define_const( + Exp::Ite( + Box::new(Exp::Eq(Box::new(Exp::Var(bv)), Box::new(smt_zeros(1)))), + Box::new(smt_i128(1)), + Box::new(smt_i128(0)), + ), + info, + ) + } else { + let low_len = len / 2; + let top_len = len - low_len; + + let top = solver.define_const(Exp::Extract(len - 1, low_len, Box::new(Exp::Var(bv))), info); + let low = solver.define_const(Exp::Extract(low_len - 1, 0, Box::new(Exp::Var(bv))), info); + + let low_bits_are_zero = Exp::Eq(Box::new(Exp::Var(low)), Box::new(smt_zeros(low_len as i128))); + + let top_ctz = smt_ctz(top, top_len, solver, info); + let low_ctz = smt_ctz(low, low_len, solver, info); + + solver.define_const( + Exp::Ite( + Box::new(low_bits_are_zero), + Box::new(Exp::Bvadd(Box::new(smt_i128(low_len as i128)), Box::new(Exp::Var(top_ctz)))), + Box::new(Exp::Var(low_ctz)), + ), + info, + ) + } +} + +fn count_trailing_zeros(bv: Val, solver: &mut Solver, info: SourceLoc) -> Result, ExecError> { + let bv = replace_mixed_bits(bv, solver, info)?; + match bv { + Val::Bits(bv) => Ok(Val::I128(bv.trailing_zeros() as i128)), + Val::Symbolic(bv) => { + if let Some(len) = solver.length(bv) { + smt_ctz(bv, len, solver, info).into() + } else { + Err(ExecError::Type("count_trailing_zeros (solver could not determine length)".to_string(), info)) + } + } + _ => Err(ExecError::Type(format!("count_trailing_zeros {:?}", &bv), info)), + } +} + +// RISC-V `sys_enable_experimental_extensions() : unit -> bool` (prelude.sail) gates +// hartSupports() for in-development extensions (Zibi, Zvabd). No isla-specific +// extern exists upstream; stubbed to false (experimental extensions off), the +// same default a real deployment would use. +fn sys_enable_experimental_extensions( + _: Val, + _solver: &mut Solver, + _info: SourceLoc, +) -> Result, ExecError> { + Ok(Val::Bool(false)) +} + fn primop_ite( args: Vec>, solver: &mut Solver, @@ -2503,6 +2673,11 @@ pub fn unary_primops() -> HashMap> { primops.insert("print_endline".to_string(), print_endline as Unary); primops.insert("prerr_endline".to_string(), prerr_endline as Unary); primops.insert("count_leading_zeros".to_string(), count_leading_zeros as Unary); + primops.insert("count_trailing_zeros".to_string(), count_trailing_zeros as Unary); + primops.insert("cancel_reservation".to_string(), cancel_reservation as Unary); + primops.insert("sys_enable_experimental_extensions".to_string(), sys_enable_experimental_extensions as Unary); + primops.insert("valid_reservation".to_string(), valid_reservation as Unary); + primops.insert("match_reservation".to_string(), match_reservation as Unary); primops.insert("undefined_bitvector".to_string(), undefined_bitvector as Unary); primops.insert("undefined_bit".to_string(), undefined_bit as Unary); primops.insert("undefined_bool".to_string(), undefined_bool as Unary); @@ -2534,6 +2709,7 @@ pub fn unary_primops() -> HashMap> { pub fn binary_primops() -> HashMap> { let mut primops = HashMap::new(); + primops.insert("load_reservation".to_string(), load_reservation as Binary); primops.insert("optimistic_assert".to_string(), optimistic_assert as Binary); primops.insert("pessimistic_assert".to_string(), pessimistic_assert as Binary); primops.insert("and_bool".to_string(), and_bool as Binary); @@ -2594,6 +2770,9 @@ pub fn binary_primops() -> HashMap> { primops.insert("string_take".to_string(), string_take as Binary); primops.insert("cons".to_string(), cons as Binary); primops.insert("undefined_vector".to_string(), undefined_vector as Binary); + // vector_init(n, x) builds a length-n vector of copies of x — same + // (len, elem) -> Vector(vec![elem; len]) construction as undefined_vector. + primops.insert("vector_init".to_string(), undefined_vector as Binary); primops.insert("print_string".to_string(), print_string as Binary); primops.insert("prerr_string".to_string(), prerr_string as Binary); primops.insert("print_int".to_string(), print_int as Binary); diff --git a/isla-sail/jib_ir.ml b/isla-sail/jib_ir.ml index 9d904b38..3bb767e7 100644 --- a/isla-sail/jib_ir.ml +++ b/isla-sail/jib_ir.ml @@ -175,9 +175,9 @@ module Ir_formatter = struct add_instr n buf indent (C.keyword "end") | I_copy (clexp, cval) -> add_instr n buf indent (string_of_clexp clexp ^ " = " ^ C.value cval ^ output_loc l) - | I_funcall (creturn, false, id, args) -> + | I_funcall (creturn, Call, id, args) -> add_instr n buf indent (string_of_creturn creturn ^ " = " ^ string_of_uid id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")" ^ output_loc l) - | I_funcall (creturn, true, id, args) -> + | I_funcall (creturn, Extern _, id, args) -> add_instr n buf indent (string_of_creturn creturn ^ " = $" ^ string_of_uid id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")" ^ output_loc l) | I_return cval -> add_instr n buf indent (C.keyword "return" ^ " " ^ C.value cval) diff --git a/isla-sail/sail_plugin_isla.ml b/isla-sail/sail_plugin_isla.ml index 3ba62605..383ab4b4 100644 --- a/isla-sail/sail_plugin_isla.ml +++ b/isla-sail/sail_plugin_isla.ml @@ -51,6 +51,7 @@ open Libsail open Ast +open Ast_compare open Ast_util open Interactive.State open Jib @@ -80,10 +81,20 @@ let isla_rewrites = ("atoms_to_singletons", [String_arg "c"; If_mono_arg]); ("recheck_defs", [If_mono_arg]); ("undefined", [Bool_arg false]); - ("vector_string_pats_to_bit_list", []); + (* "vector_string_pats_to_bit_list" removed upstream — its functionality (converting + vector-string patterns via vector_string_to_bit_list) was folded into + rewrite_ast_pat_lits, i.e. the "pattern_literals" pass already present below. *) ("remove_not_pats", []); + (* remove_vector_subrange_pats moved ahead of remove_vector_concat: named bit-slice + patterns (e.g. `uimm[5] @ ...`) must be desugared before remove_vector_concat + processes the surrounding concat pattern, otherwise it crashes trying to resolve + the slice as a vector name. Confirmed empirically — running it after (matching the + registry's declaration order, which is not necessarily invocation order) still + crashed on the same input. *) + ("remove_vector_subrange_pats", []); ("remove_vector_concat", []); ("remove_bitvector_pats", []); + ("remove_numeral_pats", []); ("pattern_literals", [Literal_arg "all"]); ("tuple_assignments", []); ("vector_concat_assignments", []); @@ -105,7 +116,7 @@ module Ir_config : Jib_compile.CONFIG = struct let rec convert_typ ctx typ = let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.local_env typ in match typ_aux with - | Typ_id id when string_of_id id = "bit" -> CT_bit + | Typ_id id when string_of_id id = "bit" -> CT_fbits 1 | Typ_id id when string_of_id id = "bool" -> CT_bool | Typ_id id when string_of_id id = "int" -> CT_lint | Typ_id id when string_of_id id = "nat" -> CT_lint @@ -262,7 +273,7 @@ let remove_casts cdefs = else ( let fid = Printf.sprintf "%s->%s" (string_of_ctyp ctyp_from) (string_of_ctyp ctyp_to) in conversions := StringMap.add fid (ctyp_from, ctyp_to) !conversions; - [I_aux (I_funcall (CR_one clexp, false, (mk_id fid, []), [cval]), aux)] + [I_aux (I_funcall (CR_one clexp, Call, (mk_id fid, []), [cval]), aux)] ) | I_aux (I_init (ctyp_to, id, Init_cval cval), aux) -> let ctyp_from = cval_ctyp cval in @@ -309,10 +320,10 @@ let fix_cons cdefs = let cons_name ctyp = mk_id ("cons#" ^ string_of_ctyp ctyp) in let collect_cons_ctyps list_ctyps = function - | I_aux (I_funcall (clexp, true, (id, [ctyp]), args), aux) when string_of_id id = "sail_cons" -> + | I_aux (I_funcall (clexp, Extern _, (id, [ctyp]), args), aux) when string_of_id id = "sail_cons" -> list_ctyps := CTSet.add ctyp !list_ctyps; list_ctyps := CTSet.add ctyp !all_list_ctyps; - I_aux (I_funcall (clexp, false, (cons_name ctyp, []), args), aux) + I_aux (I_funcall (clexp, Call, (cons_name ctyp, []), args), aux) | instr -> instr in @@ -351,7 +362,9 @@ let isla_initialize () = Nl_flow.opt_nl_flow := true; Type_check.opt_no_lexp_bounds_check := true; Reporting.opt_warnings := false; - Initial_check.opt_magic_hash := true; + (* Initial_check.opt_magic_hash removed upstream in current Sail; the + magic_hash feature it toggled no longer exists, so there is nothing + to set here. *) Specialize.add_initial_calls (IdSet.singleton (mk_id "isla_footprint")); Specialize.add_initial_calls (IdSet.singleton (mk_id "isla_footprint_no_init"));