rapx 0.7.32

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

//! 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 mod alias;
pub mod call;
pub mod display;
pub mod exec;
pub mod memory;
pub mod state;

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

use crate::verify::slicer::RelevantMirItems;

use self::state::{UnsupportedReason, VmState};

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

impl<'tcx> SymbolicVm<'tcx> {
    /// Create a symbolic VM for the given compiler context.
    pub 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 fn execute<'ctx>(
        &self,
        ctx: &'ctx Context,
        items: &RelevantMirItems<'tcx>,
    ) -> Result<VmState<'ctx, 'tcx>, UnsupportedReason> {
        let body = self.tcx.optimized_mir(items.checkpoint.caller);
        let mut state = VmState::new(ctx, self.tcx, body, items.checkpoint.caller);
        state.path = Some(items.path.clone());
        state.execute_items(&items.items)?;
        state.propagate_from_checkpoint(items.checkpoint.block);
        Ok(state)
    }
}