Fix: StorageLocations should return 0 when the zero register is reque…

…sted, not a bitvector const

liblisa/src/semantics/default/smtgen.rs

@@ -137,9 +137,17 @@ impl<'ctx, A: Arch, S: SmtSolver<'ctx>> StorageLocations<'ctx, A, S> {
 
     /// Retrieves the mapping for the provided location `key`.
     /// If the location has no mapping, a new SMT bitvector constant is created.
+    /// If the register is a zero register, a bitvector with value 0 is returned.
     ///
     /// Masks the result by the mask of the location.
     pub fn get(&mut self, context: &mut S, key: FilledLocation<A>, sizes: &Sizes) -> S::BV {
+        match key {
+            FilledLocation::Concrete(Location::Reg(reg)) if reg.is_zero() => {
+                return context.bv_from_u64(0, reg.byte_size() as u32 * 8)
+            }
+            _ => (),
+        }
+
         let mask = match key {
             FilledLocation::Concrete(Location::Reg(reg)) => reg.mask(),
             _ => None,
@@ -158,6 +166,7 @@ impl<'ctx, A: Arch, S: SmtSolver<'ctx>> StorageLocations<'ctx, A, S> {
 
     /// Retrieves the mapping for the provided location `key`.
     /// If the location has no mapping, a new SMT bitvector constant is created.
+    /// If the register is a zero register, a bitvector with value 0 is returned.
     ///
     /// Crops the result to the provided `input_size`.
     pub fn get_sized(
@@ -175,12 +184,21 @@ impl<'ctx, A: Arch, S: SmtSolver<'ctx>> StorageLocations<'ctx, A, S> {
 
     /// Retrieves the mapping for the provided location `key`.
     /// If the location has no mapping, a new SMT bitvector constant is created.
+    /// If the register is a zero register, a bitvector with value 0 is returned.
     ///
     /// Does not mask or crop the result in any way.
-    pub fn get_raw(&mut self, context: &mut S, key: FilledLocation<A>, sizes: &Sizes) -> &S::BV {
+    pub fn get_raw(&mut self, context: &mut S, key: FilledLocation<A>, sizes: &Sizes) -> S::BV {
+        match key {
+            FilledLocation::Concrete(Location::Reg(reg)) if reg.is_zero() => {
+                return context.bv_from_u64(0, reg.byte_size() as u32 * 8)
+            }
+            _ => (),
+        }
+
         self.map
             .entry(key)
             .or_insert_with_key(|key: &FilledLocation<A>| context.new_bv_const(Self::name(key), key.bit_size(sizes)))
+            .clone()
     }
 
     /// Returns the bitvector constant representing the instruction bitstring.
@@ -841,4 +859,4 @@ impl<'ctx, A: Arch, S: SmtSolver<'ctx>> ConcreteZ3Model<'ctx, A, S> {
     pub fn intermediate_values_needed(&self) -> &[usize] {
         &self.intermediate_values_needed
     }
-}
+}

liblisa/src/smt/z3/tests/mod.rs

@@ -10,8 +10,12 @@ mod equivalence;
 
 use std::time::Duration;
 
+use crate::arch::x64::{GpReg, X64Arch, X64Reg};
+use crate::encoding::dataflows::Size;
+use crate::semantics::default::smtgen::{FilledLocation, Sizes, StorageLocations};
 use crate::smt::z3::Z3Solver;
 use crate::smt::{SatResult, SmtBV, SmtBVArray, SmtSolver};
+use crate::state::Location;
 
 #[test]
 pub fn array_store_select_equals() {
@@ -24,3 +28,27 @@ pub fn array_store_select_equals() {
         assert!(matches!(context.check_assertions(&[eq]), SatResult::Unsat));
     });
 }
+
+#[test]
+pub fn zero_register_is_zero() {
+    // Verify that the value of a zero register returned by StorageLocations is, in fact, always zero.
+    Z3Solver::with_thread_local(Duration::from_secs(900), |mut context| {
+        let mut s = StorageLocations::<X64Arch, _>::new(&mut context);
+        let key = FilledLocation::Concrete(Location::Reg(X64Reg::GpReg(GpReg::Riz)));
+
+        // StorageLocations::get
+        let riz = s.get(&mut context, key, &Sizes::default());
+        let eq = !riz._eq(context.bv_from_u64(0, 64));
+        assert!(matches!(context.check_assertions(&[eq]), SatResult::Unsat));
+
+        // StorageLocations::get_sized
+        let riz = s.get_sized(&mut context, key, &Sizes::default(), Size::qword(), false);
+        let eq = !riz._eq(context.bv_from_u64(0, 64));
+        assert!(matches!(context.check_assertions(&[eq]), SatResult::Unsat));
+
+        // StorageLocations::get_raw
+        let riz = s.get_raw(&mut context, key, &Sizes::default());
+        let eq = !riz._eq(context.bv_from_u64(0, 64));
+        assert!(matches!(context.check_assertions(&[eq]), SatResult::Unsat));
+    });
+}