Trait haybale::backend::Memory[−][src]

pub trait Memory: Clone + PartialEq + Eq {
    type SolverRef: SolverRef<BV = Self::Index>;
    type Index: BV<SolverRef = Self::SolverRef>;
    type Value: BV;
    fn new_uninitialized(
        solver: Self::SolverRef, 
        null_detection: bool, 
        name: Option<&str>, 
        addr_bits: u32
    ) -> Self;

    fn new_zero_initialized(
        solver: Self::SolverRef, 
        null_detection: bool, 
        name: Option<&str>, 
        addr_bits: u32
    ) -> Self;

    fn read(&self, index: &Self::Index, bits: u32) -> Result<Self::Value>;

    fn write(&mut self, index: &Self::Index, value: Self::Value) -> Result<()>;

    fn get_solver(&self) -> Self::SolverRef;

    fn change_solver(&mut self, new_solver: Self::SolverRef);
}
Expand description

Trait for things which can act like ‘memories’, that is, maps from bitvector (addresses) to bitvector (values)

Associated Types

Required methods

A new Memory, whose contents at all addresses are completely uninitialized (unconstrained)

null_detection: if true, all memory accesses will be checked to ensure their addresses cannot be NULL, throwing Error::NullPointerDereference if NULL is a possible solution for the address

name: a name for this Memory, or None to use the default name (as of this writing, ‘mem’)

addr_bits: e.g. 64 for a Memory which uses 64-bit addresses

A new Memory, whose contents at all addresses are initialized to be 0

null_detection: if true, all memory accesses will be checked to ensure their addresses cannot be NULL, throwing Error::NullPointerDereference if NULL is a possible solution for the address

name: a name for this Memory, or None to use the default name (as of this writing, ‘mem’)

addr_bits: e.g. 64 for a Memory which uses 64-bit addresses

Read any number (>0) of bits of memory, at any alignment. Returned BV will have size bits.

Write any number (>0) of bits of memory, at any alignment.

Get a reference to the solver instance this Memory belongs to

Adapt the Memory to a new solver instance.

The new solver instance should have been created (possibly transitively) via SolverRef::duplicate() from the SolverRef this Memory was originally created with (or most recently changed to). Further, no new variables should have been added since the call to SolverRef::duplicate().

Implementors