Check if address is unique in check_overlap

isla-axiomatic/src/axiomatic.rs

@@ -986,7 +986,11 @@ impl<'ev, B: BV> ExecutionInfo<'ev, B> {
                     {
                         // Events must be associated with an instruction
                         if let Some(opcode) = cycle_instr {
-                            let evs = if include_in_smt && !(ignore_ifetch && is_ifetch) { &mut exec.smt_events } else { &mut exec.other_events };
+                            let evs = if include_in_smt && !(ignore_ifetch && is_ifetch) {
+                                &mut exec.smt_events
+                            } else {
+                                &mut exec.other_events
+                            };
 
                             // An event is a translate event if it was
                             // created by the translation function

isla-axiomatic/src/run_litmus.rs

@@ -276,7 +276,8 @@ where
                 .iter()
                 .map(|(loc, exp)| (loc.clone(), reset_eval(exp, all_addrs, &litmus.objdump)))
                 .collect();
-            let task_state = TaskState::new().with_reset_registers(reset).with_zero_announce_exit(isa_config.zero_announce_exit);
+            let task_state =
+                TaskState::new().with_reset_registers(reset).with_zero_announce_exit(isa_config.zero_announce_exit);
             if let Some(limit) = opts.pc_limit {
                 task_state.with_pc_limit(isa_config.pc, limit)
             } else {

isla-lib/src/config.rs

@@ -376,18 +376,15 @@ fn get_const_primops<B: BV>(
     symtab: &Symtab,
     type_info: &IRTypeInfo,
 ) -> Result<HashMap<String, Reset<B>>, String> {
-    let defaults = config
-        .get("const_primops");
+    let defaults = config.get("const_primops");
 
     if let Some(defaults) = defaults {
         if let Some(defaults) = defaults.as_table() {
             defaults
                 .into_iter()
-                .filter_map(|(primop, value)| {
-                    match reset_to_toml_value(value, symtab, type_info) {
-                        Ok(value) => Some(Ok((primop.clone(), value))),
-                        Err(e) => Some(Err(e)),
-                    }
+                .filter_map(|(primop, value)| match reset_to_toml_value(value, symtab, type_info) {
+                    Ok(value) => Some(Ok((primop.clone(), value))),
+                    Err(e) => Some(Err(e)),
                 })
                 .collect()
         } else {
@@ -657,7 +654,7 @@ pub struct ISAConfig<B> {
     /// The default size (in bytes) for memory accesses in litmus tests
     pub default_sizeof: u32,
     /// Exit if sail_instr_announce is called with a zero bitvector
-    pub zero_announce_exit: bool
+    pub zero_announce_exit: bool,
 }
 
 impl<B: BV> ISAConfig<B> {

isla-lib/src/executor.rs

@@ -1664,7 +1664,7 @@ pub struct TaskState<B> {
     // IR program counter in the frame.
     pc_limit: Option<(Name, usize)>,
     // Exit if we ever announce an instruction with all bits set to zero
-    zero_announce_exit: bool
+    zero_announce_exit: bool,
 }
 
 impl<B> TaskState<B> {

isla-lib/src/memory.rs

@@ -236,6 +236,11 @@ pub struct Memory<B> {
 
 static DEFAULT_REGION_NAME: &str = "default";
 
+enum Overlap {
+    Unique(u64),
+    NoOverlap,
+}
+
 impl<B: BV> Memory<B> {
     pub fn new() -> Self {
         Memory { regions: Vec::new(), client_info: None }
@@ -362,14 +367,23 @@ impl<B: BV> Memory<B> {
         }
     }
 
-    fn check_overlap(&self, address: Sym, error: ExecError, solver: &mut Solver<B>) -> Result<(), ExecError> {
+    // Checks that a symbolic address does not overlap with any
+    // concrete regions of memory. If it does, then we won't know what
+    // value should be returned.
+    fn check_concrete_overlap(
+        &self,
+        address: Sym,
+        error: ExecError,
+        solver: &mut Solver<B>,
+    ) -> Result<Overlap, ExecError> {
         use Exp::*;
         use SmtResult::*;
 
         let mut region_constraints = Vec::new();
 
         for region in &self.regions {
             if !matches!(region, Region::Symbolic(_) | Region::SymbolicCode(_)) {
+                eprintln!("{:?}", region);
                 let Range { start, end } = region.region_range();
 
                 region_constraints.push(And(
@@ -383,17 +397,38 @@ impl<B: BV> Memory<B> {
             let constraint = region_constraints.drain(..).fold(r, |r1, r2| Or(Box::new(r1), Box::new(r2)));
             match solver.check_sat_with(&constraint) {
                 Sat => {
-                    let mut model = Model::new(solver);
-                    log!(log::MEMORY, &format!("Overlapping satisfiable address: {:?}", model.get_var(address)?));
-                    probe::taint_info(log::MEMORY, address, None, solver);
-                    return Err(error);
+                    let sat_address = {
+                        let mut model = Model::new(solver);
+                        let Some(Bits64(sat_address)) = model.get_var(address)? else {
+                            return Err(ExecError::Z3Error(
+                                "No bitvector address variable found in model during check_concrete_overlap"
+                                    .to_string(),
+                            ));
+                        };
+                        sat_address
+                    };
+                    // Check if the satisifiable address in the
+                    // concrete region is actually unique, in which
+                    // case the caller could choose to treat it as a
+                    // concrete value.
+                    let uniqueness_constraint = Neq(Box::new(Var(address)), Box::new(Bits64(sat_address)));
+                    match solver.check_sat_with(&uniqueness_constraint) {
+                        Unsat => Ok(Overlap::Unique(sat_address.lower_u64())),
+                        Unknown => Err(ExecError::Z3Unknown),
+                        Sat => {
+                            log!(log::MEMORY, &format!("Overlapping satisfiable address: {:x}", sat_address));
+                            probe::taint_info(log::MEMORY, address, None, solver);
+                            Err(error)
+                        }
+                    }
                 }
                 Unknown => return Err(ExecError::Z3Unknown),
-                Unsat => (),
+                Unsat => Ok(Overlap::NoOverlap),
             }
+        } else {
+            // There are no concrete regions
+            Ok(Overlap::NoOverlap)
         }
-
-        Ok(())
     }
 
     /// Read from the memory region determined by the address. If the address is symbolic the read
@@ -489,8 +524,27 @@ impl<B: BV> Memory<B> {
                 }
 
                 Val::Symbolic(symbolic_addr) => {
-                    self.check_overlap(symbolic_addr, ExecError::BadRead("Possible symbolic address overlap"), solver)?;
-                    self.read_symbolic(read_kind, address, bytes, solver, tag, opts, DEFAULT_REGION_NAME)
+                    // If the symbolic address overlaps a concrete
+                    // region, but actually only has a single unique
+                    // satisfiable value, then we can recursively call
+                    // read again with that satisfiable value.
+                    match self.check_concrete_overlap(
+                        symbolic_addr,
+                        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::NoOverlap => {
+                            self.read_symbolic(read_kind, address, bytes, solver, tag, opts, DEFAULT_REGION_NAME)
+                        }
+                    }
                 }
 
                 _ => Err(ExecError::Type("Non bitvector address in read".to_string(), SourceLoc::unknown())),
@@ -527,7 +581,11 @@ impl<B: BV> Memory<B> {
             }
 
             Val::Symbolic(symbolic_addr) => {
-                self.check_overlap(symbolic_addr, ExecError::BadWrite("possible symbolic address overlap"), solver)?;
+                self.check_concrete_overlap(
+                    symbolic_addr,
+                    ExecError::BadWrite("possible symbolic address overlap"),
+                    solver,
+                )?;
                 self.write_symbolic(write_kind, address, data, solver, tag, opts, DEFAULT_REGION_NAME)
             }
 
@@ -834,3 +892,31 @@ fn read_concrete<B: BV>(
         Err(ExecError::BadRead("Concrete read more than 8 bytes"))
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::bitvector::b64::B64;
+    use crate::error::ExecError;
+    use crate::smt::smtlib::{bits64, Def, Exp, Ty};
+    use crate::smt::{Config, Context, Solver, Sym};
+
+    #[test]
+    fn test_symbolic_overlap() {
+        let mut mem = Memory::<B64>::new();
+        mem.add_zero_region(0x00..0xFF);
+
+        let cfg = Config::new();
+        let ctx = Context::new(cfg);
+        let mut solver = Solver::<B64>::new(&ctx);
+
+        let addr = Sym::from_u32(0);
+        solver.add(Def::DeclareConst(addr, Ty::BitVec(64)));
+        solver.add(Def::Assert(Exp::Eq(Box::new(Exp::Var(addr)), Box::new(bits64(0xA0, 64)))));
+
+        match mem.check_concrete_overlap(addr, ExecError::BadRead("test"), &mut solver) {
+            Ok(Overlap::Unique(0xA0)) => (),
+            _ => panic!("Unexpected result from check_concrete_overlap"),
+        }
+    }
+}

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, UVal, Val, ELF_ENTRY, Reset};
+use crate::ir::{BitsSegment, Reset, UVal, Val, ELF_ENTRY};
 use crate::primop_util::*;
 use crate::smt::smtlib::*;
 use crate::smt::*;
@@ -2665,7 +2665,12 @@ pub struct Primops<B> {
 
 impl<B: BV> Default for Primops<B> {
     fn default() -> Self {
-        Primops { unary: unary_primops(), binary: binary_primops(), variadic: variadic_primops(), consts: HashMap::default() }
+        Primops {
+            unary: unary_primops(),
+            binary: binary_primops(),
+            variadic: variadic_primops(),
+            consts: HashMap::default(),
+        }
     }
 }