Update isla-sail for current Sail, add missing isla-lib primops for RISC-V

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;

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 }
     }

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 }
     }

isla-lib/src/memory.rs

@@ -538,14 +538,20 @@ impl<B: BV> Memory<B> {
                         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)
                         }

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<B: BV>(
             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<Name> = match vec.first() {
+                Some(Val::Struct(fields)) => fields.keys().copied().collect(),
+                _ => unreachable!(),
+            };
+            let mut result_fields: HashMap<Name, Val<B>, 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<B: BV>(
                 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<Name, Val<B>, 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<B: BV>(bv: Val<B>, solver: &mut Solver<B>, 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<B: BV>(_: Val<B>, _solver: &mut Solver<B>, _info: SourceLoc) -> Result<Val<B>, ExecError> {
+    Ok(Val::Unit)
+}
+
+fn valid_reservation<B: BV>(_: Val<B>, _solver: &mut Solver<B>, _info: SourceLoc) -> Result<Val<B>, ExecError> {
+    Ok(Val::Bool(false))
+}
+
+fn match_reservation<B: BV>(_: Val<B>, _solver: &mut Solver<B>, _info: SourceLoc) -> Result<Val<B>, ExecError> {
+    Ok(Val::Bool(false))
+}
+
+fn load_reservation<B: BV>(
+    _addr: Val<B>,
+    _width: Val<B>,
+    _solver: &mut Solver<B>,
+    _info: SourceLoc,
+) -> Result<Val<B>, ExecError> {
+    Ok(Val::Unit)
+}
+
+// Mirrors smt_clz above but checks the low half first instead of the high half.
+fn smt_ctz<B: BV>(bv: Sym, len: u32, solver: &mut Solver<B>, 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<B: BV>(bv: Val<B>, solver: &mut Solver<B>, info: SourceLoc) -> Result<Val<B>, 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<B: BV>(
+    _: Val<B>,
+    _solver: &mut Solver<B>,
+    _info: SourceLoc,
+) -> Result<Val<B>, ExecError> {
+    Ok(Val::Bool(false))
+}
+
 fn primop_ite<B: BV>(
     args: Vec<Val<B>>,
     solver: &mut Solver<B>,
@@ -2503,6 +2673,11 @@ pub fn unary_primops<B: BV>() -> HashMap<String, Unary<B>> {
     primops.insert("print_endline".to_string(), print_endline as Unary<B>);
     primops.insert("prerr_endline".to_string(), prerr_endline as Unary<B>);
     primops.insert("count_leading_zeros".to_string(), count_leading_zeros as Unary<B>);
+    primops.insert("count_trailing_zeros".to_string(), count_trailing_zeros as Unary<B>);
+    primops.insert("cancel_reservation".to_string(), cancel_reservation as Unary<B>);
+    primops.insert("sys_enable_experimental_extensions".to_string(), sys_enable_experimental_extensions as Unary<B>);
+    primops.insert("valid_reservation".to_string(), valid_reservation as Unary<B>);
+    primops.insert("match_reservation".to_string(), match_reservation as Unary<B>);
     primops.insert("undefined_bitvector".to_string(), undefined_bitvector as Unary<B>);
     primops.insert("undefined_bit".to_string(), undefined_bit as Unary<B>);
     primops.insert("undefined_bool".to_string(), undefined_bool as Unary<B>);
@@ -2534,6 +2709,7 @@ pub fn unary_primops<B: BV>() -> HashMap<String, Unary<B>> {
 
 pub fn binary_primops<B: BV>() -> HashMap<String, Binary<B>> {
     let mut primops = HashMap::new();
+    primops.insert("load_reservation".to_string(), load_reservation as Binary<B>);
     primops.insert("optimistic_assert".to_string(), optimistic_assert as Binary<B>);
     primops.insert("pessimistic_assert".to_string(), pessimistic_assert as Binary<B>);
     primops.insert("and_bool".to_string(), and_bool as Binary<B>);
@@ -2594,6 +2770,9 @@ pub fn binary_primops<B: BV>() -> HashMap<String, Binary<B>> {
     primops.insert("string_take".to_string(), string_take as Binary<B>);
     primops.insert("cons".to_string(), cons as Binary<B>);
     primops.insert("undefined_vector".to_string(), undefined_vector as Binary<B>);
+    // 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<B>);
     primops.insert("print_string".to_string(), print_string as Binary<B>);
     primops.insert("prerr_string".to_string(), prerr_string as Binary<B>);
     primops.insert("print_int".to_string(), print_int as Binary<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)

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"));