rapx 0.7.55

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
55
56
57
58
59

//! Data types for the path-refinement layer.
//!
//! These structures are produced by the backward visitor and consumed by the
//! forward visitor, engine, and diagnostic formatting.  `ContractFact` is the
//! only variant never produced by the backward visitor itself — it is injected
//! by the engine before the forward visit.

use crate::verify::{contract, path_extractor::Path};
use rustc_hir::def_id::DefId;
use rustc_middle::mir::BasicBlock;

/// A proof goal for one `(checkpoint, path)` item: the set of relevant items
/// plus the path context needed to verify the target property.
#[derive(Clone, Debug)]
pub(crate) struct ProofGoal<'tcx> {
    /// Path being visited; `path.target` identifies the checkpoint.
    pub path: Path,
    /// Items kept from the path.
    pub items: Vec<RelevantItem<'tcx>>,
    /// Per-global-block function ownership `(def_id, local_index)`, populated
    /// for inlined multi-function paths. Empty for single-function goals.
    pub block_fn: Vec<(DefId, usize)>,
}

/// One relevant item kept from the backward slice.
#[derive(Clone, Debug)]
pub(crate) enum RelevantItem<'tcx> {
    /// A MIR statement retained from a basic block. `def_id` identifies the
    /// function owning `block` (differs from the caller for inlined callees).
    Statement {
        def_id: DefId,
        block: BasicBlock,
        statement_index: usize,
    },
    /// A MIR terminator retained from a basic block.  For a `SwitchInt`, `block`
    /// is the switch block and `switch_succ` is the successor taken along this
    /// path (so the VM need not re-resolve it from the path); for any other
    /// terminator — or when the path ends at the checkpoint — `switch_succ` is
    /// `None`.
    Terminator {
        def_id: DefId,
        block: BasicBlock,
        switch_succ: Option<BasicBlock>,
    },
    /// Enter an inlined callee: bind the caller's argument locals to the callee
    /// parameters. `args` holds the caller's argument local indices.
    CalleeEntry { callee: DefId, args: Vec<usize> },
    /// Return from an inlined callee: write the callee's `_0` to the caller's
    /// destination local.
    CalleeExit { dest: usize },
    /// A contract fact injected by the engine before the forward visit.
    /// Never produced by the backward visitor itself.
    ContractFact { property: contract::Property<'tcx> },
    /// An unknown call with no summary (`unsupported`): its effects cannot be
    /// modeled, so the slicer keeps the terminator but conservatively drops
    /// precision on the relevant state it touches. The forward VM is a no-op on
    /// this marker.
    UnknownCall,
}