Module memory 

Memory as expressions: loads and stores over an array from addresses to cells, resolved at construction into the operators bitwright already has, so the simplifier, the facts, the prover and SMT-LIB export work on them unchanged.

A load reads each cell through the stores made before it, newest first: a store whose address is equal (the builder or the facts decide it) gives the cell; one whose address is different is skipped; one that may be either becomes a select on the address equality. What no store covers comes from the base: known contents where the address is in a region of them, and otherwise an unknown cell, a fresh symbol per read, made consistent with the earlier reads of unknown cells by selecting on address equality too (so two reads at equal addresses are equal, whatever the addresses are written as).

use bitwright::memory::{Endian, Memory};
use bitwright::{Context, ParseOptions, Width};

let mut cx = Context::new();
let o = ParseOptions::width(Width::W64);
let (sp, x) = (cx.parse("sp", &o)?, cx.parse("x", &o)?);
let mut mem = Memory::new("mem", Width::W64, Width::W8, Endian::Little);
let m0 = mem.initial();
// Spill x to [sp - 8], then read it back and add 1.
let slot = cx.parse("sp - 8", &o)?;
let m1 = mem.store(&mut cx, m0, slot, x)?;
let back = mem.load(&mut cx, m1, slot, 8)?;
assert_eq!(back, x);
// A read at [sp] is not the spill: an unknown cell of memory before it.
let other = mem.load(&mut cx, m1, sp, 1)?;
assert_eq!(cx.display(other).to_string(), "mem.0");

Structs

Memory

A memory (see the module documentation).

Version

A version of a memory: its state after some stores. A clone accepts the versions shared at the time of cloning, but not versions created later on a different clone branch.

Enums

Endian

How a value wider than a cell lies in consecutive cells.