rapx/verify/property_checker/
mod.rs

1//! Unified property checker for the symbolic VM.
2//!
3//! `PropertyChecker::check` is the entry point; `check_inner` dispatches each
4//! `PropertyKind` to a per-family `check_*` method living in one of the sibling
5//! submodules (`memory`, `bounds`, `typed`, `numeric`, `string`, `alias`,
6//! `cstr`, `transmute`).  Shared helpers live in `util`.
7
8use z3::Solver;
9
10use crate::helpers::mir_scan::Checkpoint;
11use crate::verify::vm::state::VmState;
12use crate::verify::{
13    contract::{Property, PropertyKind},
14    report::{CheckResult, UnknownReason},
15};
16
17mod alias;
18mod auto_trait;
19mod bounds;
20mod cstr;
21mod memory;
22mod numeric;
23mod string;
24mod transmute;
25mod typed;
26mod util;
27
28pub(crate) use auto_trait::{
29    atomic_update_check, contain_no_type_check, field_invariant_check, no_internal_mut_check,
30    no_raw_ptr_check, ref_send_check, uni_internal_mut_check,
31};
32
33pub(crate) struct PropertyChecker;
34
35impl PropertyChecker {
36    pub(crate) fn check<'z3, 'tcx>(
37        &self,
38        vm_state: &VmState<'z3, 'tcx>,
39        checkpoint: &Checkpoint<'tcx>,
40        property: &Property<'tcx>,
41    ) -> CheckResult {
42        let solver = Solver::new(vm_state.z3_ctx);
43        vm_state.assert_all(&solver);
44        self.check_inner(vm_state, &solver, checkpoint, property)
45    }
46
47    fn check_inner<'z3, 'tcx>(
48        &self,
49        vm_state: &VmState<'z3, 'tcx>,
50        solver: &Solver<'z3>,
51        checkpoint: &Checkpoint<'tcx>,
52        property: &Property<'tcx>,
53    ) -> CheckResult {
54        // Vacuous truth (implicit): a property whose target place carries an
55        // `unwrap_some()` / `iter()` projection is trivially satisfied when the
56        // container resolves to no allocation (e.g. `Option::None`).  This is
57        // distinct from the explicit `Null(p)` guard in `any(Null(p), …)`,
58        // which is a `PropertyKind::Null` disjunct handled by `check_null`.
59        if self.is_vacuously_true_for_nullable(vm_state, checkpoint, property) {
60            return CheckResult::ProvedByRule;
61        }
62        match property {
63            Property::Or(_) => self.check_or(vm_state, solver, checkpoint, property),
64            Property::And(_) => self.check_and(vm_state, solver, checkpoint, property),
65            Property::Atom(atom) => match atom.kind {
66                PropertyKind::Align => self.check_align(vm_state, checkpoint, property),
67                PropertyKind::NonNull => {
68                    self.check_non_null(vm_state, checkpoint, property)
69                }
70                PropertyKind::Null => self.check_null(vm_state, checkpoint, property),
71                PropertyKind::Allocated => {
72                    self.check_allocated(vm_state, checkpoint, property)
73                }
74                PropertyKind::InBound => {
75                    self.check_in_bound(vm_state, solver, checkpoint, property)
76                }
77                PropertyKind::Init => self.check_init(vm_state, checkpoint, property),
78                PropertyKind::Typed => self.check_typed(vm_state, checkpoint, property),
79                PropertyKind::Alias => self.check_alias(vm_state, checkpoint),
80                PropertyKind::Owning => self.check_owning(vm_state, checkpoint, property),
81                PropertyKind::Alive => self.check_alive(vm_state, checkpoint, property),
82                PropertyKind::NonOverlap => {
83                    self.check_non_overlap(vm_state, solver, checkpoint, property)
84                }
85                // `NonVolatile` is uncheckable: the VM does not model volatile
86                // access, so there is nothing to disprove.  Treated as
87                // satisfied (Proved) as a documented soundness assumption —
88                // analysed code is assumed not to mix volatile and non-volatile
89                // access.  Revisit if volatile tracking is ever added.
90                PropertyKind::NonVolatile => CheckResult::ProvedByRule,
91                PropertyKind::ValidNum => {
92                    self.check_valid_num(vm_state, solver, checkpoint, property)
93                }
94                PropertyKind::ValidString => {
95                    self.check_valid_string(vm_state, solver, checkpoint, property)
96                }
97                PropertyKind::ValidCStr => {
98                    self.check_valid_cstr(vm_state, solver, checkpoint, property)
99                }
100                PropertyKind::ValidTransmute => {
101                    self.check_valid_transmute(vm_state, property)
102                }
103                PropertyKind::SplitTransmute => {
104                    self.check_split_transmute(vm_state, checkpoint, property)
105                }
106                PropertyKind::Trait => self.check_trait(vm_state, checkpoint, property),
107                PropertyKind::Size => self.check_size(vm_state, checkpoint, property),
108                PropertyKind::NoPadding => {
109                    self.check_no_padding(vm_state, checkpoint, property)
110                }
111                PropertyKind::ContainNoType => {
112                    self.check_contain_no_type(vm_state, checkpoint, property)
113                }
114                PropertyKind::NoRawPtr => {
115                    self.check_no_raw_ptr(vm_state, checkpoint, property)
116                }
117                PropertyKind::NoInternalMut => {
118                    self.check_no_internal_mut(vm_state, property)
119                }
120                PropertyKind::UniInternalMut => {
121                    self.check_uni_internal_mut(vm_state, property)
122                }
123                PropertyKind::AtomicUpdate => {
124                    self.check_atomic_update(vm_state, checkpoint, property)
125                }
126                PropertyKind::RefSend => {
127                    self.check_ref_send(vm_state, checkpoint, property)
128                }
129
130                _ => CheckResult::Unknown(UnknownReason::Unimplemented),
131            },
132        }
133    }
134
135    fn check_or<'z3, 'tcx>(
136        &self,
137        vm_state: &VmState<'z3, 'tcx>,
138        solver: &Solver<'z3>,
139        checkpoint: &Checkpoint<'tcx>,
140        property: &Property<'tcx>,
141    ) -> CheckResult {
142        // OR semantics: proved if any disjunct is proved; failed only if every
143        // disjunct is definitely violated; otherwise unknown.  An empty
144        // disjunction is unsatisfiable, hence Failed.
145        let mut overall = CheckResult::Failed;
146        for disjunct in property.disjuncts() {
147            let result = self.check_inner(vm_state, solver, checkpoint, disjunct);
148            overall = overall.or(result);
149        }
150        overall
151    }
152
153    fn check_and<'z3, 'tcx>(
154        &self,
155        vm_state: &VmState<'z3, 'tcx>,
156        solver: &Solver<'z3>,
157        checkpoint: &Checkpoint<'tcx>,
158        property: &Property<'tcx>,
159    ) -> CheckResult {
160        // AND semantics: proved if every conjunct is proved; failed if any is
161        // definitely violated; otherwise unknown.  An empty conjunction is
162        // vacuously proved.
163        let mut overall = CheckResult::ProvedByRule;
164        for conjunct in property.conjuncts() {
165            let result = self.check_inner(vm_state, solver, checkpoint, conjunct);
166            overall = overall.and(result);
167        }
168        overall
169    }
170}
rapx/verify/property_checker/mod.rs

rapx/verify/property_checker/
mod.rs
