Module state 

Symbolic VM state types.

The data structures that represent the symbolic execution state: symbolic values and their invariants, memory allocations, and the full execution state at a program point.

Structs

AllocFacts 🔒

Per-allocation lifecycle facts (dead/liveness/for_each), kept apart from the allocation’s shape metadata and parent edge so identity/layout and facts are separated at the type level. The content facts (readability, C-string/UTF-8 trust) live on ContentFacts instead.

AllocId 🔒

Unique identifier for a heap or stack allocation.

Allocation 🔒

A memory allocation: a stack local, a heap object (Box/Vec), or an external raw-pointer placeholder.

Constraints 🔒

Accumulated solver state for the current path.

ContentFacts 🔒

Per-allocation content facts: whether the allocation’s contents are readable, and whether they were asserted to be a valid C string / UTF-8. These describe the stored bytes/values, so they live on MemoryContent next to that data, rather than on AllocFacts (lifecycle).

ForEachFacts 🔒

Uniform facts about the pointer elements of a container, established by x.iter() for_each invariants.

FrameState 🔒

The frame-scoped subset of VmState: the name → allocation binding keyed by MIR Local, which the callee reuses, so it must be swapped out for the duration of an inlined callee and swapped back afterwards.

InlineCtx 🔒

Scratch state for the recursive inlined-callee mechanism ([crate::verify::vm::call::exec_inline_call]), which unwinds via the Rust call stack, is bounded by inline_depth, and stashes its per-call bindings in arg_referents/deferred_field_writes.

MemoryContent 🔒

The per-allocation contents: the byte layer, the typed-value layer, and the content facts.

MemoryUnit 🔒

A single allocation: its shape metadata (Allocation) plus its contents (MemoryContent). Splitting the two keeps the identity/layout facts apart from the mutable memory the values live in, while colocating them in one unit so no parallel table can drift out of sync. Facts live in three anchored layers — lifecycle (AllocFacts), content (ContentFacts), and value (ValueFacts on each VmValue) — see each type’s doc.

PathFacts 🔒

Per-path facts, read afterwards by the property checker.

Provenance 🔒

Pointer provenance: which allocation, at what byte offset, and (when known) what structure that offset has.

TermCaches 🔒

Term-provenance caches, one per phenomenon the VM must shape by hand.

ValueFacts 🔒

Value-level facts about a single symbolic value (nullness, alignment, bounds, and whether it has been written). These travel with the value — a VmValue leaves its allocation when passed as an operand or stashed in InlineCtx::deferred_field_writes — so they live on the value, not the allocation. The allocation-level counterpart to init is ContentFacts::initialized, kept in sync by VmState::mark_initialized.

VmState 🔒

The full symbolic execution state at a program point.

VmValue 🔒

A symbolic value tracked by the VM.

Enums

AllocKind 🔒

The shape of an allocation: a single object, a slice/array buffer, or an external raw-pointer parameter. element_ty (typed vs untyped) and the parent sub-view edge stay separate fields.

ElementTy 🔒

The element type of an allocation’s contents, either a concrete [Ty] or symbolic (Generic).

OffsetKind 🔒

The structure of a pointer’s byte offset, when it has one.

ValueSource 🔒

The extra semantics attached to a value, beyond its term/type/provenance.