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 rustc_hir::def_id::DefId;
9use rustc_middle::ty::TyCtxt;
10use z3::{
11    Solver,
12    ast::{Ast, Bool, Int},
13};
14
15use crate::verify::{
16    contract::{Property, PropertyKind},
17    report::CheckResult,
18};
19use crate::helpers::mir_scan::Checkpoint;
20use crate::verify::vm::state::VmState;
21
22mod alias;
23mod bounds;
24mod cstr;
25mod memory;
26mod numeric;
27mod string;
28mod transmute;
29mod typed;
30mod util;
31
32pub struct PropertyChecker;
33
34impl PropertyChecker {
35    pub fn check<'ctx, 'tcx>(
36        &self,
37        vm_state: &VmState<'ctx, 'tcx>,
38        checkpoint: &Checkpoint<'tcx>,
39        property: &Property<'tcx>,
40    ) -> CheckResult {
41        let solver = Solver::new(vm_state.ctx);
42        vm_state.assert_all(&solver);
43        self.check_inner(vm_state, &solver, checkpoint, property)
44    }
45
46    fn check_inner<'ctx, 'tcx>(
47        &self,
48        vm_state: &VmState<'ctx, 'tcx>,
49        solver: &Solver<'ctx>,
50        checkpoint: &Checkpoint<'tcx>,
51        property: &Property<'tcx>,
52    ) -> CheckResult {
53        // Null guard: property is vacuously true when the guarded place is null.
54        if let Some(guard_key) = property.null_guard() {
55            if self.is_guard_null(vm_state, checkpoint, guard_key) {
56                return CheckResult::Proved;
57            }
58        }
59        // Vacuous truth: properties with unwrap_some() / iter() projections
60        // are trivially true when the container value cannot be resolved to
61        // a meaningful pointer (e.g. Option::None has no provenance).
62        if self.is_vacuously_true_for_nullable(vm_state, checkpoint, property) {
63            return CheckResult::Proved;
64        }
65        match property {
66            Property::Or(_) => self.check_or(vm_state, solver, checkpoint, property),
67            Property::Leaf(leaf) => match leaf.kind {
68                PropertyKind::Align => self.check_align(vm_state, solver, checkpoint, property),
69                PropertyKind::NonNull => self.check_non_null(vm_state, solver, checkpoint, property),
70                PropertyKind::Allocated => self.check_allocated(vm_state, solver, checkpoint, property),
71                PropertyKind::InBound => self.check_in_bound(vm_state, solver, checkpoint, property),
72                PropertyKind::Init => self.check_init(vm_state, solver, checkpoint, property),
73                PropertyKind::Typed => self.check_typed(vm_state, solver, checkpoint, property),
74                PropertyKind::Alias => self.check_alias(vm_state, solver, checkpoint, property),
75                PropertyKind::Owning => self.check_owning(vm_state, solver, checkpoint, property),
76                PropertyKind::Alive => self.check_alive(vm_state, solver, checkpoint, property),
77                PropertyKind::NonOverlap => self.check_non_overlap(vm_state, solver, checkpoint, property),
78                PropertyKind::NonVolatile => CheckResult::Proved,
79                PropertyKind::ValidNum => self.check_valid_num(vm_state, solver, checkpoint, property),
80                PropertyKind::ValidString => self.check_valid_string(vm_state, solver, checkpoint, property),
81                PropertyKind::ValidCStr => self.check_valid_cstr(vm_state, solver, checkpoint, property),
82                PropertyKind::ValidTransmute => {
83                    self.check_valid_transmute(vm_state, solver, checkpoint, property)
84                }
85                PropertyKind::SplitTransmute => {
86                    self.check_split_transmute(vm_state, solver, checkpoint, property)
87                }
88                PropertyKind::Trait => self.check_trait(vm_state, solver, checkpoint, property),
89                PropertyKind::Size => self.check_size(vm_state, property),
90
91                _ => CheckResult::Unknown,
92            },
93        }
94    }
95
96    fn check_or<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
97        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
98    {
99        // OR semantics: proved if any group is fully proved; failed only if
100        // *every* group is definitely violated; unknown otherwise.
101        let mut overall: Option<CheckResult> = None;
102        for group in property.groups() {
103            let mut group_acc: Option<CheckResult> = None;
104            for p in group {
105                let result = self.check_inner(vm_state, solver, checkpoint, p);
106                group_acc = Some(match group_acc {
107                    Some(prev) => prev.and(result),
108                    None => result,
109                });
110            }
111            // An empty group is vacuously proved.
112            let group_result = group_acc.unwrap_or(CheckResult::Proved);
113            overall = Some(match overall {
114                Some(prev) => prev.or(group_result),
115                None => group_result,
116            });
117        }
118        overall.unwrap_or(CheckResult::Failed)
119    }
120}
121
122/// Check if the source-level function signature has a named lifetime in return type.
123pub(super) fn signature_return_has_lifetime(tcx: TyCtxt<'_>, def_id: DefId) -> Option<(String, String)> {
124    let local = def_id.as_local()?;
125    let hir_id = tcx.local_def_id_to_hir_id(local);
126    let span = tcx.hir_span(hir_id);
127    let snippet = tcx.sess.source_map().span_to_snippet(span).ok()?;
128    let start = snippet.find("fn ")?;
129    let rest = &snippet[start..];
130    let end = rest.find('{').unwrap_or(rest.len());
131    let sig = &rest[..end];
132    // Extract return type after "->"
133    let ret = sig.split("->").nth(1)?;
134    let ret = ret.split("where").next()?.trim();
135    Some((sig.to_string(), ret.to_string()))
136}
137
138/// Build the boolean expression "`bytes` form a valid UTF-8 sequence".
139///
140/// Encodes the UTF-8 DFA over the per-byte Z3 terms: every byte is ASCII, a
141/// continuation byte, or a valid lead byte, and a `k`-byte lead must be
142/// followed by exactly `k-1` continuation bytes.  Value-range refinements
143/// reject overlong encodings, surrogates (U+D800..=U+DFFF), and code points
144/// above U+10FFFF.
145pub(super) fn utf8_validity<'ctx>(ctx: &'ctx z3::Context, bytes: &[Int<'ctx>]) -> Bool<'ctx> {
146    let zero = Int::from_u64(ctx, 0);
147    let one = Int::from_u64(ctx, 1);
148    let two = Int::from_u64(ctx, 2);
149    let three = Int::from_u64(ctx, 3);
150
151    let c_0x80 = Int::from_u64(ctx, 0x80);
152    let c_0xc0 = Int::from_u64(ctx, 0xC0);
153    let c_0xc2 = Int::from_u64(ctx, 0xC2);
154    let c_0xe0 = Int::from_u64(ctx, 0xE0);
155    let c_0xf0 = Int::from_u64(ctx, 0xF0);
156    let c_0xf5 = Int::from_u64(ctx, 0xF5);
157    let c_0xa0 = Int::from_u64(ctx, 0xA0);
158    let c_0x90 = Int::from_u64(ctx, 0x90);
159    let c_0xed = Int::from_u64(ctx, 0xED);
160    let c_0xf4 = Int::from_u64(ctx, 0xF4);
161
162    let mut valid = Bool::from_bool(ctx, true);
163    // Number of continuation bytes still pending for the current multi-byte
164    // sequence (0..=3).  `lead` holds the lead byte (only meaningful while a
165    // multi-byte sequence is open).
166    let mut state = zero.clone();
167    let mut lead = zero.clone();
168
169    for b in bytes {
170        let is_ascii = b.lt(&c_0x80);
171        let is_cont = b.ge(&c_0x80) & b.lt(&c_0xc0);
172        let is_2lead = b.ge(&c_0xc2) & b.lt(&c_0xe0);
173        let is_3lead = b.ge(&c_0xe0) & b.lt(&c_0xf0);
174        let is_4lead = b.ge(&c_0xf0) & b.lt(&c_0xf5);
175
176        // Overlong / surrogate / >U+10FFFF refinements on the first
177        // continuation byte.  Each disjunct is vacuous unless `lead` equals the
178        // constrained lead byte.
179        let refine_3 = (lead._eq(&c_0xe0).not() | b.ge(&c_0xa0))
180            & (lead._eq(&c_0xed).not() | b.lt(&c_0xa0));
181        let refine_4 = (lead._eq(&c_0xf0).not() | b.ge(&c_0x90))
182            & (lead._eq(&c_0xf4).not() | b.lt(&c_0x90));
183
184        let valid_s0 = is_ascii.clone() | is_2lead.clone() | is_3lead.clone() | is_4lead.clone();
185        let valid_s1 = is_cont.clone();
186        let valid_s2 = is_cont.clone() & refine_3;
187        let valid_s3 = is_cont.clone() & refine_4;
188
189        let state0 = state._eq(&zero);
190        let state1 = state._eq(&one);
191        let state2 = state._eq(&two);
192
193        let byte_valid = Bool::ite(
194            &state0,
195            &valid_s0,
196            &Bool::ite(&state1, &valid_s1, &Bool::ite(&state2, &valid_s2, &valid_s3)),
197        );
198
199        let new_state_s0 = Bool::ite(
200            &is_ascii,
201            &zero,
202            &Bool::ite(&is_2lead, &one, &Bool::ite(&is_3lead, &two, &three)),
203        );
204        let new_state_cont = Bool::ite(&state1, &zero, &Bool::ite(&state2, &one, &two));
205        let new_state = Bool::ite(&state0, &new_state_s0, &new_state_cont);
206
207        valid = valid & byte_valid;
208        // Remember a 3-/4-byte lead so its first continuation is refined.
209        let is_lead34 = is_3lead | is_4lead;
210        lead = Bool::ite(&(state0 & is_lead34), b, &lead);
211        state = new_state;
212    }
213
214    valid = valid & state._eq(&zero);
215    valid
216}
rapx/verify/property_checker/mod.rs

rapx/verify/property_checker/
mod.rs
