rapx 0.7.19

A static analysis platform for Rust program analysis and verification
Documentation 
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

//! 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,
    def_use::RelevantPlaces,
    helpers::CheckpointLocation,
    path_extractor::{Path, PathStep},
};
use rustc_middle::mir::BasicBlock;

/// MIR items relevant to one `(checkpoint, path, property)` item.
#[derive(Clone, Debug)]
pub struct RelevantMirItems<'tcx> {
    /// Unsafe checkpoint whose obligation is being checked.
    pub checkpoint: CheckpointLocation,
    /// Required property that determines the relevance roots.
    pub property: contract::Property<'tcx>,
    /// Path being visited.
    pub path: Path,
    /// Items kept from the path.
    pub items: Vec<BackwardItem<'tcx>>,
    /// Initial roots extracted from the property.
    pub roots: RelevantPlaces,
}

impl<'tcx> RelevantMirItems<'tcx> {
    /// Append one kept item to the visited path.
    pub fn push(&mut self, item: BackwardItem<'tcx>) {
        self.items.push(item);
    }

    /// Return true when no MIR/path item has been kept yet.
    pub fn is_empty(&self) -> bool {
        self.items.is_empty()
    }
}

/// One item kept while walking a path backward.
#[derive(Clone, Debug)]
pub enum BackwardItem<'tcx> {
    /// A MIR statement retained from a basic block.
    Statement {
        block: BasicBlock,
        statement_index: usize,
        kind: KeepReason,
    },
    /// A MIR terminator retained from a basic block.
    Terminator { block: BasicBlock, kind: KeepReason },
    /// A path-level step retained as structural context.
    PathStep { step: PathStep, kind: KeepReason },
    /// A contract fact injected by the engine before the forward visit.
    /// Never produced by the backward visitor itself.
    ContractFact { property: contract::Property<'tcx> },
    /// A conservative loss of precision for relevant state.
    Forget { reason: ForgetReason },
}

/// Why a retained item is relevant.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum KeepReason {
    /// The item defines a relevant place.
    Definition,
    /// The item contributes a branch/path condition.
    PathCondition,
    /// The item contributes pointer provenance or pointer arithmetic.
    PointerFlow,
    /// The item refines state through a runtime check.
    RuntimeCheck,
    /// The item is the unsafe checkpoint being checked.
    Checkpoint,
    /// The item represents a loop summary or loop exit.
    LoopExit,
    /// The item may invalidate a relevant fact.
    Invalidation,
    /// The item may affect relevant state but is not modeled precisely yet.
    UnknownEffect,
}

/// Reason for conservatively forgetting relevant state.
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum ForgetReason {
    /// A call may modify relevant state but has no summary yet.
    UnknownCall,
    /// An SCC region may modify relevant state but has no summary yet.
    SccWithoutSummary,
    /// A write may alias relevant state.
    MayAliasWrite,
    /// A relevant statement or terminator is not supported yet.
    UnsupportedEffect,
}