use crate::backend::SolverRef;
use crate::error::*;
use crate::solver_utils::bvs_can_be_equal;
use boolector::Btor;
use log::debug;
use std::rc::Rc;
#[rustversion::before(1.51)]
use reduce::Reduce;
type BV = boolector::BV<Rc<Btor>>;
type Array = boolector::Array<Rc<Btor>>;
#[derive(PartialEq, Eq, Clone, Debug)]
pub struct Memory {
btor: Rc<Btor>,
mem: Array,
addr_bits: u32,
name: String,
null_detection: bool,
}
impl Memory {
pub const CELL_BITS: u32 = 8; pub const BITS_IN_BYTE: u32 = 8;
pub const LOG_BITS_IN_BYTE: u32 = 3; pub const CELL_BYTES: u32 = Self::CELL_BITS / Self::BITS_IN_BYTE;
pub fn new_uninitialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32,
) -> Self {
let default_name = "mem";
Self {
mem: Array::new(
btor.clone(),
addr_bits,
Self::CELL_BITS,
name.or(Some(default_name)),
),
name: name.unwrap_or(default_name).into(),
null_detection,
addr_bits,
btor, }
}
pub fn new_zero_initialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32,
) -> Self {
let default_name = "mem_initialized";
Self {
mem: Array::new_initialized(
btor.clone(),
addr_bits,
Self::CELL_BITS,
&BV::zero(btor.clone(), Self::CELL_BITS),
),
name: name.unwrap_or(default_name).into(),
null_detection,
addr_bits,
btor, }
}
pub fn get_solver(&self) -> Rc<Btor> {
self.btor.clone()
}
pub fn change_solver(&mut self, new_btor: Rc<Btor>) {
self.mem = new_btor.match_array(&self.mem).unwrap();
self.btor = new_btor;
}
fn read_byte(&self, addr: &BV) -> BV {
assert_eq!(
addr.get_width(),
self.addr_bits,
"Read address has wrong width: expected {} bits but got {} bits",
self.addr_bits,
addr.get_width(),
);
self.mem.read(addr)
}
fn write_byte(&mut self, addr: &BV, val: &BV) {
assert_eq!(
addr.get_width(),
self.addr_bits,
"Write address has wrong width: expected {} bits but got {} bits",
self.addr_bits,
addr.get_width(),
);
assert_eq!(
val.get_width(),
Self::CELL_BITS,
"write_byte: expected exactly one byte of data to write"
);
self.mem = self.mem.write(addr, val);
}
pub fn read(&self, addr: &BV, bits: u32) -> Result<BV> {
debug!("Reading {} bits from {} at {:?}", bits, &self.name, addr);
let addr_width = addr.get_width();
assert_eq!(
addr_width, self.addr_bits,
"Read address has wrong width: expected {} bits but got {} bits",
self.addr_bits, addr_width
);
if self.null_detection
&& bvs_can_be_equal(&self.btor, addr, &BV::zero(self.btor.clone(), addr_width))?
{
return Err(Error::NullPointerDereference);
}
let rval = if bits < Self::BITS_IN_BYTE {
let byte = self.read_byte(&addr);
byte.slice(bits - 1, 0)
} else {
assert_eq!(bits % Self::BITS_IN_BYTE, 0, "Read with size {} bits", bits);
let bytes = bits / Self::BITS_IN_BYTE;
assert!(bytes > 0, "Read of length 0");
(0 .. bytes)
.map(|byte_num| {
let offset_addr = addr.add(&BV::from_u64(
self.btor.clone(),
u64::from(byte_num),
self.addr_bits,
));
self.read_byte(&offset_addr)
})
.reduce(|a, b| b.concat(&a))
.unwrap() };
debug!("Value read is {:?}", rval);
Ok(rval)
}
pub fn write(&mut self, addr: &BV, val: BV) -> Result<()> {
debug!("Writing {:?} to {} address {:?}", val, &self.name, addr);
let addr_width = addr.get_width();
assert_eq!(
addr_width, self.addr_bits,
"Write address has wrong width: expected {} bits but got {} bits",
self.addr_bits, addr_width,
);
if self.null_detection
&& bvs_can_be_equal(&self.btor, addr, &BV::zero(self.btor.clone(), addr_width))?
{
return Err(Error::NullPointerDereference);
}
let write_size = val.get_width();
let write_data = if write_size < Self::BITS_IN_BYTE {
val.uext(8 - write_size)
} else {
val
};
let write_size = write_data.get_width();
assert_eq!(
write_size % Self::BITS_IN_BYTE,
0,
"Write with size {} bits",
write_size
);
let write_size_bytes = write_size / Self::BITS_IN_BYTE;
for byte_num in 0 .. write_size_bytes {
let data_byte = write_data.slice(
(byte_num + 1) * Self::BITS_IN_BYTE - 1,
byte_num * Self::BITS_IN_BYTE,
);
let offset_addr = addr.add(&BV::from_u64(
self.btor.clone(),
u64::from(byte_num),
addr_width,
));
self.write_byte(&offset_addr, &data_byte);
}
Ok(())
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::error::Result;
use crate::solver_utils::{self, PossibleSolutions};
use boolector::option::{BtorOption, ModelGen};
use boolector::{BVSolution, BV};
use std::rc::Rc;
fn get_a_solution(bv: &BV<Rc<Btor>>) -> Result<Option<BVSolution>> {
let btor = bv.get_btor();
btor.set_opt(BtorOption::ModelGen(ModelGen::All));
let solution = if solver_utils::sat(&btor)? {
Some(bv.get_a_solution())
} else {
None
};
btor.set_opt(BtorOption::ModelGen(ModelGen::Disabled));
Ok(solution)
}
#[test]
fn uninitialized() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
let zero = BV::zero(btor.clone(), 8);
let read_bv = mem.read(&addr, 8)?;
btor.push(1);
read_bv.sgt(&zero).assert();
assert_eq!(solver_utils::sat(&btor), Ok(true));
let read_val = get_a_solution(&read_bv)?
.expect("Expected a solution")
.as_u64()
.unwrap() as i8;
assert!(read_val > 0);
btor.pop(1);
read_bv.slt(&zero).assert();
assert_eq!(solver_utils::sat(&btor), Ok(true));
let read_val = get_a_solution(&read_bv)?
.expect("Expected a solution")
.as_u64()
.unwrap() as i8;
assert!(read_val < 0);
Ok(())
}
#[test]
fn zero_initialized() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mem = Memory::new_zero_initialized(btor.clone(), true, None, 64);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
let read_bv = mem.read(&addr, Memory::CELL_BITS)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0));
Ok(())
}
#[test]
fn read_and_write_to_cell_zero() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), false, None, 64);
let data_val = 0x7c;
let data = BV::from_u32(btor.clone(), data_val, Memory::CELL_BITS);
let zero = BV::zero(btor.clone(), 64);
mem.write(&zero, data)?;
let read_bv = mem.read(&zero, Memory::CELL_BITS)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val as u64));
Ok(())
}
#[test]
fn read_and_write_cell_aligned() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0xba;
let data = BV::from_u32(btor.clone(), data_val, Memory::CELL_BITS);
let aligned = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&aligned, data)?;
let read_bv = mem.read(&aligned, Memory::CELL_BITS)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val as u64));
Ok(())
}
#[test]
fn read_and_write_small() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let read_bv = mem.read(&addr, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
Ok(())
}
#[test]
fn read_and_write_small_32bitaddr() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 32);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, 32);
mem.write(&addr, data)?;
let read_bv = mem.read(&addr, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
Ok(())
}
#[test]
fn read_single_bit() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x55;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let read_bv = mem.read(&addr, 1)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(1));
Ok(())
}
#[test]
fn read_and_write_unaligned() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let unaligned = BV::from_u64(btor.clone(), 0x10001, 64);
mem.write(&unaligned, data)?;
let read_bv = mem.read(&unaligned, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
Ok(())
}
#[test]
fn read_and_write_64_bits() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val: u64 = 0x12345678_9abcdef0;
let data = BV::from_u64(btor.clone(), data_val, 64);
let addr = BV::from_u64(btor.clone(), 0x10004, 64);
mem.write(&addr, data)?;
let read_bv = mem.read(&addr, 64)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
Ok(())
}
#[test]
fn read_and_write_symbolic_addr() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), false, None, 64);
let data_val: u64 = 0x12345678_9abcdef0;
let data = BV::from_u64(btor.clone(), data_val, 64);
let addr = BV::new(btor.clone(), 64, Some("symbolic_addr"));
mem.write(&addr, data)?;
let read_bv = mem.read(&addr, 64)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
Ok(())
}
#[test]
fn read_and_write_200bits() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val_0: u64 = 0x12345678_9abcdef0;
let data_val_1: u64 = 0x2468ace0_13579bdf;
let data_val_2: u64 = 0xfedcba98_76543210;
let data_val_3: u64 = 0xef;
let write_val = BV::from_u64(btor.clone(), data_val_3, 8)
.concat(&BV::from_u64(btor.clone(), data_val_2, 64))
.concat(&BV::from_u64(btor.clone(), data_val_1, 64))
.concat(&BV::from_u64(btor.clone(), data_val_0, 64));
assert_eq!(write_val.get_width(), 200);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, write_val)?;
let read_bv = mem.read(&addr, 200)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let read_val_0 = get_a_solution(&read_bv.slice(63, 0))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_0, data_val_0);
let read_val_1 = get_a_solution(&read_bv.slice(127, 64))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_1, data_val_1);
let read_val_2 = get_a_solution(&read_bv.slice(191, 128))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_2, data_val_2);
let read_val_3 = get_a_solution(&read_bv.slice(199, 192))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_3, data_val_3);
Ok(())
}
#[test]
fn read_and_write_200bits_unaligned() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val_0: u64 = 0x12345678_9abcdef0;
let data_val_1: u64 = 0x2468ace0_13579bdf;
let data_val_2: u64 = 0xfedcba98_76543210;
let data_val_3: u64 = 0xef;
let write_val = BV::from_u64(btor.clone(), data_val_3, 8)
.concat(&BV::from_u64(btor.clone(), data_val_2, 64))
.concat(&BV::from_u64(btor.clone(), data_val_1, 64))
.concat(&BV::from_u64(btor.clone(), data_val_0, 64));
assert_eq!(write_val.get_width(), 200);
let addr = BV::from_u64(btor.clone(), 0x10003, 64);
mem.write(&addr, write_val)?;
let read_bv = mem.read(&addr, 200)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let read_val_0 = get_a_solution(&read_bv.slice(63, 0))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_0, data_val_0);
let read_val_1 = get_a_solution(&read_bv.slice(127, 64))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_1, data_val_1);
let read_val_2 = get_a_solution(&read_bv.slice(191, 128))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_2, data_val_2);
let read_val_3 = get_a_solution(&read_bv.slice(199, 192))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_3, data_val_3);
Ok(())
}
#[test]
fn read_and_write_200bits_symbolic_addr() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), false, None, 64);
let data_val_0: u64 = 0x12345678_9abcdef0;
let data_val_1: u64 = 0x2468ace0_13579bdf;
let data_val_2: u64 = 0xfedcba98_76543210;
let data_val_3: u64 = 0xef;
let write_val = BV::from_u64(btor.clone(), data_val_3, 8)
.concat(&BV::from_u64(btor.clone(), data_val_2, 64))
.concat(&BV::from_u64(btor.clone(), data_val_1, 64))
.concat(&BV::from_u64(btor.clone(), data_val_0, 64));
assert_eq!(write_val.get_width(), 200);
let addr = BV::new(btor.clone(), 64, Some("symbolic_addr"));
mem.write(&addr, write_val)?;
let read_bv = mem.read(&addr, 200)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let read_val_0 = get_a_solution(&read_bv.slice(63, 0))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_0, data_val_0);
let read_val_1 = get_a_solution(&read_bv.slice(127, 64))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_1, data_val_1);
let read_val_2 = get_a_solution(&read_bv.slice(191, 128))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_2, data_val_2);
let read_val_3 = get_a_solution(&read_bv.slice(199, 192))?
.expect("Expected a solution")
.as_u64()
.unwrap();
assert_eq!(read_val_3, data_val_3);
Ok(())
}
#[test]
fn write_twice_read_once() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let data_val = 0x3A;
let data = BV::from_u64(btor.clone(), data_val, 8);
mem.write(&addr, data)?;
let read_bv = mem.read(&addr, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
Ok(())
}
#[test]
fn write_different_locations() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let data_val_2 = 0xfedc_ba98;
let data_2 = BV::from_u64(btor.clone(), data_val_2, 32);
let addr_2 = BV::from_u64(btor.clone(), 0x10008, 64);
mem.write(&addr_2, data_2)?;
let read_bv = mem.read(&addr, 32)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
let read_bv = mem.read(&addr_2, 32)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val_2));
Ok(())
}
#[test]
fn write_adjacent_locations() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let data_val_2 = 0xfedc_ba98;
let data_2 = BV::from_u64(btor.clone(), data_val_2, 32);
let addr_2 = BV::from_u64(btor.clone(), 0x10004, 64);
mem.write(&addr_2, data_2)?;
let read_bv = mem.read(&addr, 32)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val));
let read_bv = mem.read(&addr_2, 32)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(data_val_2));
Ok(())
}
#[test]
fn write_small_read_big() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_zero_initialized(btor.clone(), true, None, 64);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let unaligned = BV::from_u64(btor.clone(), 0x10001, 64);
mem.write(&unaligned, data)?;
let aligned = BV::from_u64(btor.clone(), 0x10000, 64);
let read_bv = mem.read(&aligned, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x4F00));
let read_bv = mem.read(&unaligned, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x004F));
let garbage_addr_1 = BV::from_u64(btor.clone(), 0x10004, 64);
let garbage_addr_2 = BV::from_u64(btor.clone(), 0x10008, 64);
let read_bv_1 = mem.read(&garbage_addr_1, 8)?;
let read_bv_2 = mem.read(&garbage_addr_2, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps_1 = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv_1, 1)?
.as_u64_solutions()
.unwrap();
let ps_2 = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv_2, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps_1, PossibleSolutions::exactly_one(0));
assert_eq!(ps_2, PossibleSolutions::exactly_one(0));
Ok(())
}
#[test]
fn write_big_read_small() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let offset_2 = BV::from_u64(btor.clone(), 0x10002, 64);
mem.write(&offset_2, data)?;
let read_bv = mem.read(&offset_2, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x78));
let offset_5 = BV::from_u64(btor.clone(), 0x10005, 64);
let read_bv = mem.read(&offset_5, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x12));
let offset_3 = BV::from_u64(btor.clone(), 0x10003, 64);
let read_bv = mem.read(&offset_3, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x3456));
Ok(())
}
#[test]
fn write_big_read_small_32bitaddr() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 32);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let offset_2 = BV::from_u64(btor.clone(), 0x10002, 32);
mem.write(&offset_2, data)?;
let read_bv = mem.read(&offset_2, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x78));
let offset_5 = BV::from_u64(btor.clone(), 0x10005, 32);
let read_bv = mem.read(&offset_5, 8)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x12));
let offset_3 = BV::from_u64(btor.clone(), 0x10003, 32);
let read_bv = mem.read(&offset_3, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x3456));
Ok(())
}
#[test]
fn partial_overwrite_aligned() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data = BV::from_u64(btor.clone(), 0x12345678_12345678, 64);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let overwrite_data_val = 0xdcba;
let overwrite_data = BV::from_u64(btor.clone(), overwrite_data_val, 16);
mem.write(&addr, overwrite_data)?;
let read_bv = mem.read(&addr, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(overwrite_data_val));
let read_bv = mem.read(&addr, 64)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x12345678_1234dcba));
Ok(())
}
#[test]
fn partial_overwrite_unaligned() -> Result<()> {
let _ = env_logger::builder().is_test(true).try_init();
let btor = <Rc<Btor> as SolverRef>::new();
let mut mem = Memory::new_uninitialized(btor.clone(), true, None, 64);
let data = BV::from_u64(btor.clone(), 0x12345678_12345678, 64);
let addr = BV::from_u64(btor.clone(), 0x10000, 64);
mem.write(&addr, data)?;
let overwrite_addr = BV::from_u64(btor.clone(), 0x10002, 64);
let overwrite_data_val = 0xdcba;
let overwrite_data = BV::from_u64(btor.clone(), overwrite_data_val, 16);
mem.write(&overwrite_addr, overwrite_data)?;
let read_bv = mem.read(&overwrite_addr, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(overwrite_data_val));
let read_bv = mem.read(&addr, 64)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x12345678_dcba5678));
let new_addr = BV::from_u64(btor.clone(), 0x10003, 64);
let read_bv = mem.read(&new_addr, 16)?;
assert_eq!(solver_utils::sat(&btor), Ok(true));
let ps = solver_utils::get_possible_solutions_for_bv(btor.clone(), &read_bv, 1)?
.as_u64_solutions()
.unwrap();
assert_eq!(ps, PossibleSolutions::exactly_one(0x78dc));
Ok(())
}
}