use crate::backend::SolverRef;
use crate::error::*;
use crate::solver_utils::bvs_can_be_equal;
use boolector::Btor;
use log::debug;
use reduce::Reduce;
use std::convert::TryInto;
use std::rc::Rc;
type BV = boolector::BV<Rc<Btor>>;
type Array = boolector::Array<Rc<Btor>>;
#[derive(Clone, Debug)]
pub struct Memory {
btor: Rc<Btor>,
mem: Array,
name: String,
null_detection: bool,
cell_bytes_as_bv: BV,
log_bits_in_byte_as_bv: BV,
log_bits_in_byte_as_wide_bv: BV,
}
impl Memory {
pub const INDEX_BITS: u32 = 64;
pub const CELL_BITS: u32 = 64;
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 const LOG_CELL_BYTES: u32 = 3;
pub const CELL_OFFSET_MASK: u32 = 0x7;
pub fn new_uninitialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32,
) -> Self {
assert_eq!(addr_bits, Self::INDEX_BITS, "This `Memory` is only compatible with {}-bit pointers. Try `DefaultBackend` instead of `CellMemoryBackend` for a `Memory` which works with more pointer sizes.", Self::INDEX_BITS);
let log_num_cells = Self::INDEX_BITS - Self::LOG_CELL_BYTES;
let default_name = "mem";
Self {
mem: Array::new(
btor.clone(),
log_num_cells,
Self::CELL_BITS,
name.or(Some(default_name)),
),
name: name.unwrap_or(default_name).into(),
null_detection,
cell_bytes_as_bv: BV::from_u64(
btor.clone(),
u64::from(Self::CELL_BYTES),
Self::INDEX_BITS,
),
log_bits_in_byte_as_bv: BV::from_u64(
btor.clone(),
u64::from(Self::LOG_BITS_IN_BYTE),
Self::CELL_BITS,
),
log_bits_in_byte_as_wide_bv: BV::from_u64(
btor.clone(),
u64::from(Self::LOG_BITS_IN_BYTE),
2 * Self::CELL_BITS,
),
btor,
}
}
pub fn new_zero_initialized(
btor: Rc<Btor>,
null_detection: bool,
name: Option<&str>,
addr_bits: u32,
) -> Self {
assert_eq!(addr_bits, Self::INDEX_BITS, "This `Memory` is only compatible with {}-bit pointers. Try `DefaultBackend` instead of `CellMemoryBackend` for a `Memory` which works with more pointer sizes.", Self::INDEX_BITS);
let log_num_cells = Self::INDEX_BITS - Self::LOG_CELL_BYTES;
let default_name = "mem_initialized";
Self {
mem: Array::new_initialized(
btor.clone(),
log_num_cells,
Self::CELL_BITS,
&BV::zero(btor.clone(), Self::CELL_BITS),
),
name: name.unwrap_or(default_name).into(),
null_detection,
cell_bytes_as_bv: BV::from_u64(
btor.clone(),
u64::from(Self::CELL_BYTES),
Self::INDEX_BITS,
),
log_bits_in_byte_as_bv: BV::from_u64(
btor.clone(),
u64::from(Self::LOG_BITS_IN_BYTE),
Self::CELL_BITS,
),
log_bits_in_byte_as_wide_bv: BV::from_u64(
btor.clone(),
u64::from(Self::LOG_BITS_IN_BYTE),
2 * Self::CELL_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.cell_bytes_as_bv = new_btor.match_bv(&self.cell_bytes_as_bv).unwrap();
self.log_bits_in_byte_as_bv = new_btor.match_bv(&self.log_bits_in_byte_as_bv).unwrap();
self.log_bits_in_byte_as_wide_bv = new_btor
.match_bv(&self.log_bits_in_byte_as_wide_bv)
.unwrap();
self.btor = new_btor;
}
fn read_cell(&self, addr: &BV) -> BV {
assert_eq!(addr.get_width(), Self::INDEX_BITS);
let cell_num = addr.slice(Self::INDEX_BITS - 1, Self::LOG_CELL_BYTES);
self.mem.read(&cell_num)
}
fn write_cell(&mut self, addr: &BV, val: BV) {
assert_eq!(addr.get_width(), Self::INDEX_BITS);
assert_eq!(val.get_width(), Self::CELL_BITS);
let cell_num = addr.slice(Self::INDEX_BITS - 1, Self::LOG_CELL_BYTES);
self.mem = self.mem.write(&cell_num, &val);
}
fn read_within_cell(&self, addr: &BV, bits: u32) -> BV {
let cell_contents = self.read_cell(addr);
assert!(bits <= Self::CELL_BITS);
if bits == Self::CELL_BITS {
cell_contents
} else {
let offset = addr
.slice(Self::LOG_CELL_BYTES - 1, 0)
.uext(Self::CELL_BITS - Self::LOG_CELL_BYTES)
.sll(&self.log_bits_in_byte_as_bv);
cell_contents
.srl(&offset)
.slice(bits - 1, 0)
}
}
fn write_within_cell(&mut self, addr: &BV, val: BV) {
let write_size = val.get_width();
assert!(write_size <= Self::CELL_BITS);
let data_to_write = if write_size == Self::CELL_BITS {
val
} else {
let offset = addr
.slice(Self::LOG_CELL_BYTES - 1, 0)
.uext(Self::CELL_BITS - Self::LOG_CELL_BYTES)
.sll(&self.log_bits_in_byte_as_bv);
let mask_clear = BV::ones(self.btor.clone(), write_size)
.uext(Self::CELL_BITS - write_size)
.sll(&offset)
.not();
let mask_write = val.uext(Self::CELL_BITS - write_size).sll(&offset);
self.read_cell(addr)
.and(&mask_clear)
.or(&mask_write)
};
self.write_cell(addr, data_to_write);
}
fn read_small(&self, addr: &BV, bits: u32) -> BV {
assert!(bits <= Self::CELL_BITS);
if bits <= 8 {
self.read_within_cell(addr, bits)
} else {
let next_cell_addr = addr.add(&self.cell_bytes_as_bv);
let merged_contents = self
.read_cell(&next_cell_addr)
.concat(&self.read_cell(addr));
let offset = addr
.slice(Self::LOG_CELL_BYTES - 1, 0)
.uext(2 * Self::CELL_BITS - Self::LOG_CELL_BYTES)
.sll(&self.log_bits_in_byte_as_wide_bv);
merged_contents
.srl(&offset)
.slice(bits - 1, 0)
}
}
fn write_small(&mut self, addr: &BV, val: BV) {
let write_size = val.get_width();
assert!(write_size <= Self::CELL_BITS);
if write_size <= 8 {
self.write_within_cell(addr, val);
} else {
let next_cell_addr = addr.add(&self.cell_bytes_as_bv);
let offset = addr
.slice(Self::LOG_CELL_BYTES - 1, 0)
.uext(2 * Self::CELL_BITS - Self::LOG_CELL_BYTES)
.sll(&self.log_bits_in_byte_as_wide_bv);
let mask_clear = BV::ones(self.btor.clone(), write_size)
.uext(2 * Self::CELL_BITS - write_size)
.sll(&offset)
.not();
let mask_write = val.uext(2 * Self::CELL_BITS - write_size).sll(&offset);
let data_to_write = self
.read_cell(&next_cell_addr)
.concat(&self.read_cell(addr))
.and(&mask_clear)
.or(&mask_write);
self.write_cell(addr, data_to_write.slice(Self::CELL_BITS - 1, 0));
self.write_cell(
&next_cell_addr,
data_to_write.slice(2 * Self::CELL_BITS - 1, Self::CELL_BITS),
);
}
}
fn read_large_aligned(&self, addr: &BV, bits: u32) -> BV {
assert_ne!(bits, 0);
let num_full_cells = (bits - 1) / Self::CELL_BITS;
let bits_in_last_cell = (bits - 1) % Self::CELL_BITS + 1;
itertools::repeat_n(Self::CELL_BITS, num_full_cells.try_into().unwrap())
.chain(std::iter::once(bits_in_last_cell))
.enumerate()
.map(|(i, sz)| {
let offset_bytes = i as u64 * u64::from(Self::CELL_BYTES);
self.read_within_cell(
&addr.add(&BV::from_u64(
self.btor.clone(),
offset_bytes,
Self::INDEX_BITS,
)),
sz,
)
})
.reduce(|a, b| b.concat(&a))
.unwrap()
}
fn write_large_aligned(&mut self, addr: &BV, val: BV) {
let write_size = val.get_width();
assert_ne!(write_size, 0);
let num_full_cells = (write_size - 1) / Self::CELL_BITS;
let bits_in_last_cell = (write_size - 1) % Self::CELL_BITS + 1;
let write_size_sequence =
itertools::repeat_n(Self::CELL_BITS, num_full_cells.try_into().unwrap())
.chain(std::iter::once(bits_in_last_cell));
for (i, sz) in write_size_sequence.enumerate() {
assert!(sz > 0);
let offset_bytes = i as u64 * u64::from(Self::CELL_BYTES);
let offset_bits = i as u32 * Self::CELL_BITS;
let write_data = val.slice(sz + offset_bits - 1, offset_bits);
self.write_within_cell(
&addr.add(&BV::from_u64(
self.btor.clone(),
offset_bytes,
Self::INDEX_BITS,
)),
write_data,
);
}
}
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::INDEX_BITS, "Read address has wrong 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::CELL_BITS {
self.read_small(addr, bits)
} else {
if let Some(addr_u64) = addr.as_u64() {
let cell_offset = addr_u64 & u64::from(Self::CELL_OFFSET_MASK);
if cell_offset == 0 {
self.read_large_aligned(addr, bits)
} else {
let bytes_till_cell_boundary = u64::from(Self::CELL_BYTES) - cell_offset;
let first =
self.read_small(addr, bytes_till_cell_boundary as u32 * Self::BITS_IN_BYTE);
let next_cell_addr = addr.add(&BV::from_u64(
self.btor.clone(),
bytes_till_cell_boundary,
addr_width,
));
let rest = self.read_large_aligned(
&next_cell_addr,
bits - bytes_till_cell_boundary as u32 * Self::BITS_IN_BYTE,
);
rest.concat(&first)
}
} else {
assert_eq!(bits % Self::BITS_IN_BYTE, 0);
let bytes = bits / Self::BITS_IN_BYTE;
assert!(bytes > 0);
(0 .. bytes)
.map(|byte_num| {
let offset_addr = addr.add(&BV::from_u64(
self.btor.clone(),
u64::from(byte_num),
addr_width,
));
self.read_within_cell(&offset_addr, Self::BITS_IN_BYTE)
})
.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::INDEX_BITS,
"Write address has wrong 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();
if write_size <= Self::CELL_BITS {
self.write_small(addr, val)
} else {
if let Some(addr_u64) = addr.as_u64() {
let cell_offset = addr_u64 & u64::from(Self::CELL_OFFSET_MASK);
if cell_offset == 0 {
self.write_large_aligned(addr, val)
} else {
let bytes_till_cell_boundary = u64::from(Self::CELL_BYTES) - cell_offset;
let first =
val.slice(bytes_till_cell_boundary as u32 * Self::BITS_IN_BYTE - 1, 0);
self.write_small(addr, first);
let rest = val.slice(
val.get_width() - 1,
bytes_till_cell_boundary as u32 * Self::BITS_IN_BYTE,
);
let next_cell_addr = addr.add(&BV::from_u64(
self.btor.clone(),
bytes_till_cell_boundary,
addr_width,
));
self.write_large_aligned(&next_cell_addr, rest);
}
} else {
assert_eq!(write_size % Self::BITS_IN_BYTE, 0);
let write_size_bytes = write_size / Self::BITS_IN_BYTE;
for byte_num in 0 .. write_size_bytes {
let val_byte = val.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_within_cell(&offset_addr, val_byte);
}
}
}
Ok(())
}
}
impl PartialEq for Memory {
fn eq(&self, other: &Self) -> bool {
self.btor == other.btor && self.mem == other.mem
}
}
impl Eq for Memory {}
#[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, Memory::INDEX_BITS);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
let zero = BV::zero(btor.clone(), Memory::CELL_BITS);
let read_bv = mem.read(&addr, Memory::CELL_BITS)?;
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 i64;
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 i64;
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, Memory::INDEX_BITS);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, Memory::CELL_BITS);
let zero = BV::zero(btor.clone(), Memory::INDEX_BITS);
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));
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, Memory::INDEX_BITS);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, Memory::CELL_BITS);
let aligned = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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));
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, Memory::INDEX_BITS);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let data_val = 0x55;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let unaligned = BV::from_u64(btor.clone(), 0x10001, Memory::INDEX_BITS);
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_across_cell_boundaries() -> 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, Memory::INDEX_BITS);
let data_val: u64 = 0x12345678_9abcdef0;
let data = BV::from_u64(btor.clone(), data_val, Memory::CELL_BITS);
let addr = BV::from_u64(btor.clone(), 0x10004, Memory::INDEX_BITS);
mem.write(&addr, data)?;
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(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, Memory::INDEX_BITS);
let data_val: u64 = 0x12345678_9abcdef0;
let data = BV::from_u64(btor.clone(), data_val, Memory::CELL_BITS);
let addr = BV::new(btor.clone(), Memory::INDEX_BITS, Some("symbolic_addr"));
mem.write(&addr, data)?;
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(data_val));
Ok(())
}
#[test]
fn read_and_write_twocells() -> 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, Memory::INDEX_BITS);
let data_val_0: u64 = 0x12345678_9abcdef0;
let data_val_1: u64 = 0x2468ace0_13579bdf;
let write_val = 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(), 2 * Memory::CELL_BITS);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
mem.write(&addr, write_val)?;
let read_bv = mem.read(&addr, 128)?;
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,
"\nGot value 0x{:x}, expected 0x{:x}",
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);
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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(), Memory::INDEX_BITS, 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, Memory::INDEX_BITS);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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_cells() -> 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, Memory::INDEX_BITS);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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_different_places_within_cell() -> 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, Memory::INDEX_BITS);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let data_val = 0x4F;
let data = BV::from_u64(btor.clone(), data_val, 8);
let unaligned = BV::from_u64(btor.clone(), 0x10001, Memory::INDEX_BITS);
mem.write(&unaligned, data.clone())?;
let aligned = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let garbage_addr_2 = BV::from_u64(btor.clone(), 0x10008, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let data_val = 0x1234_5678;
let data = BV::from_u64(btor.clone(), data_val, 32);
let offset_2 = BV::from_u64(btor.clone(), 0x10002, Memory::INDEX_BITS);
mem.write(&offset_2, data.clone())?;
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
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, Memory::INDEX_BITS);
let data = BV::from_u64(btor.clone(), 0x12345678_12345678, Memory::CELL_BITS);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
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, 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(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, Memory::INDEX_BITS);
let data = BV::from_u64(btor.clone(), 0x12345678_12345678, Memory::CELL_BITS);
let addr = BV::from_u64(btor.clone(), 0x10000, Memory::INDEX_BITS);
mem.write(&addr, data)?;
let overwrite_addr = BV::from_u64(btor.clone(), 0x10002, Memory::INDEX_BITS);
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, 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(0x12345678_dcba5678));
let new_addr = BV::from_u64(btor.clone(), 0x10003, Memory::INDEX_BITS);
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(())
}
}