rapx/verify/vm/
mod.rs

1//! Symbolic MIR Virtual Machine.
2//!
3//! This module replaces the pattern-matching `ForwardVerifier` with a
4//! semantic MIR executor.  Instead of deriving ad-hoc `StateFact`s from
5//! MIR patterns, the VM executes retained MIR items and directly builds
6//! symbolic state (`VmState`) with Z3 terms for every value.
7
8pub(crate) mod alias;
9pub(crate) mod alias_hazard;
10pub(crate) mod alias_tree;
11pub(crate) mod call;
12pub(crate) mod display;
13pub(crate) mod exec;
14pub(crate) mod memory;
15pub(crate) mod region;
16pub(crate) mod state;
17
18use rustc_middle::ty::TyCtxt;
19use z3::Context;
20
21use crate::verify::slicer::ProofGoal;
22
23pub(crate) use self::state::VmState;
24
25/// Entry point for symbolic MIR execution.
26///
27/// Stateless: the inputs to a run (the Z3 context, compiler type context, and
28/// the sliced program) are passed to [`run`], so this struct carries no state
29/// of its own.
30pub(crate) struct SymbolicVm;
31
32impl SymbolicVm {
33    /// Create a symbolic VM.
34    pub(crate) fn new() -> Self {
35        Self
36    }
37
38    /// Run the sliced program `goal` (the path and its retained MIR items) and
39    /// produce the resulting symbolic state.
40    ///
41    /// The Z3 context is borrowed (not owned) so a single context can be reused
42    /// across property checks; `run` is a pure `input -> state` mapping — the
43    /// program to execute (`goal`) is consumed here and is never stored in the
44    /// returned [`VmState`].
45    pub(crate) fn run<'z3, 'tcx>(
46        &self,
47        z3_ctx: &'z3 Context,
48        tcx: TyCtxt<'tcx>,
49        goal: ProofGoal<'tcx>,
50    ) -> VmState<'z3, 'tcx> {
51        let mut state = VmState::new(z3_ctx, tcx, &goal.path, goal.path.target.caller);
52        state.execute_items(&goal.items);
53        state
54    }
55}
rapx/verify/vm/mod.rs

rapx/verify/vm/
mod.rs
