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 mod alias;
9pub mod call;
10pub mod display;
11pub mod exec;
12pub mod memory;
13pub mod state;
14
15use rustc_middle::ty::TyCtxt;
16use z3::Context;
17
18use crate::verify::slicer::ProofGoal;
19
20use self::state::VmState;
21
22/// Entry point for symbolic MIR execution.
23///
24/// Stateless wrapper around a `TyCtxt`; creates `VmState` instances
25/// for each path by executing retained MIR items.
26pub struct SymbolicVm<'tcx> {
27    tcx: TyCtxt<'tcx>,
28}
29
30impl<'tcx> SymbolicVm<'tcx> {
31    /// Create a symbolic VM for the given compiler context.
32    pub fn new(tcx: TyCtxt<'tcx>) -> Self {
33        Self { tcx }
34    }
35
36    /// Execute retained MIR items and produce a symbolic VM state.
37    ///
38    /// The `ctx` parameter provides a shared Z3 context; the resulting
39    /// `VmState` borrows it so that a single context can be reused
40    /// across property checks.
41    pub fn execute<'ctx>(
42        &self,
43        ctx: &'ctx Context,
44        items: &ProofGoal<'tcx>,
45    ) -> VmState<'ctx, 'tcx> {
46        let body = self.tcx.optimized_mir(items.path.target.caller);
47        let mut state = VmState::new(ctx, self.tcx, body, items.path.target.caller);
48        state.path = Some(items.path.clone());
49        state.execute_items(&items.items);
50        state.propagate_from_checkpoint(items.path.target.block);
51        state
52    }
53}
rapx/verify/vm/mod.rs

rapx/verify/vm/
mod.rs
