rapx 0.7.40

A static analysis platform for Rust program analysis and verification
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54

//! Symbolic MIR Virtual Machine.
//!
//! This module replaces the pattern-matching `ForwardVerifier` with a
//! semantic MIR executor.  Instead of deriving ad-hoc `StateFact`s from
//! MIR patterns, the VM executes retained MIR items and directly builds
//! symbolic state (`VmState`) with Z3 terms for every value.

pub(crate) mod alias;
pub(crate) mod alias_hazard;
pub(crate) mod call;
pub(crate) mod display;
pub(crate) mod exec;
pub(crate) mod memory;
pub(crate) mod state;

use rustc_middle::ty::TyCtxt;
use z3::Context;

use crate::verify::slicer::ProofGoal;

use self::state::VmState;

/// Entry point for symbolic MIR execution.
///
/// Stateless wrapper around a `TyCtxt`; creates `VmState` instances
/// for each path by executing retained MIR items.
pub(crate) struct SymbolicVm<'tcx> {
    tcx: TyCtxt<'tcx>,
}

impl<'tcx> SymbolicVm<'tcx> {
    /// Create a symbolic VM for the given compiler context.
    pub(crate) fn new(tcx: TyCtxt<'tcx>) -> Self {
        Self { tcx }
    }

    /// Execute retained MIR items and produce a symbolic VM state.
    ///
    /// The `ctx` parameter provides a shared Z3 context; the resulting
    /// `VmState` borrows it so that a single context can be reused
    /// across property checks.
    pub(crate) fn execute<'ctx>(
        &self,
        ctx: &'ctx Context,
        items: &ProofGoal<'tcx>,
    ) -> VmState<'ctx, 'tcx> {
        let body = self.tcx.optimized_mir(items.path.target.caller);
        let mut state = VmState::new(ctx, self.tcx, body, items.path.target.caller);
        state.path = Some(items.path.clone());
        state.execute_items(&items.items);
        state.propagate_from_checkpoint(items.path.target.block);
        state
    }
}