rapx/verify/
engine.rs

1//! Symbolic-VM-based verification engine.
2//!
3//! Uses a semantic MIR executor to build symbolic state,
4//! then checks safety properties with a unified property checker.
5
6use z3::Config;
7
8use rustc_hir::def_id::DefId;
9use rustc_middle::mir::{BasicBlock, TerminatorKind};
10use rustc_middle::ty::TyCtxt;
11
12use crate::analysis::path::PathTree;
13use crate::compat::FxHashSet;
14
15use super::{
16    contract::{LeafProperty, OrProperty, Property},
17    report::CheckResult,
18    slicer::{RelevantItem, BackwardSlicer},
19};
20use crate::helpers::mir_scan::{Checkpoint, CheckpointLocation};
21
22use super::{vm::SymbolicVm, property_checker::PropertyChecker};
23
24const ENGINE_INLINE_DEPTH: usize = 3;
25
26pub struct VerifyEngine<'tcx> {
27    slicer: BackwardSlicer<'tcx>,
28    vm: SymbolicVm<'tcx>,
29    checker: PropertyChecker,
30}
31
32impl<'tcx> VerifyEngine<'tcx> {
33    pub fn new(tcx: TyCtxt<'tcx>) -> Self {
34        Self {
35            slicer: BackwardSlicer::new(tcx),
36            vm: SymbolicVm::new(tcx),
37            checker: PropertyChecker,
38        }
39    }
40
41    fn new_z3_context() -> z3::Context {
42        let mut cfg = Config::new();
43        cfg.set_timeout_msec(10000);
44        z3::Context::new(&cfg)
45    }
46
47    pub fn check_callsite_from_tree(
48        &self,
49        tree: &PathTree,
50        checkpoint: &Checkpoint<'tcx>,
51        property: &Property<'tcx>,
52        caller_contracts: &[Property<'tcx>],
53    ) -> Vec<(CheckResult, String)> {
54        let target_block = checkpoint.block.as_usize();
55        let mut results = Vec::new();
56        let backward_items = self
57            .slicer
58            .visit_path_tree(tree, target_block, checkpoint, property);
59
60        let bound_property = Self::bind_property_to_checkpoint(property, checkpoint);
61
62        let ctx = Self::new_z3_context();
63
64        // Accumulate checked-bounds facts across checkpoints.
65        // A ChecksIndexBoundsDisjoint call in an earlier checkpoint
66        // can discharge InBound checks in a later checkpoint.
67        let mut accumulated_has_checked: bool = false;
68
69        // Process checkpoints in forward (MIR) order so that facts
70        // collected by earlier calls are available to later checks.
71        let backward_items: Vec<_> = backward_items.into_iter().rev().collect();
72        for backward in backward_items {
73            let path_desc = backward.path.describe_indices();
74
75            let mut items = Vec::new();
76            if !caller_contracts.is_empty() {
77                items.extend(
78                    caller_contracts
79                        .iter()
80                        .filter(|c| !matches!(c.kind(), Some(super::contract::PropertyKind::Unknown)))
81                        .map(|c| RelevantItem::ContractFact { property: c.clone() }),
82                );
83            }
84            items.extend(backward.items);
85
86            // Inject inline callees for unsupported calls.
87            let items = self.inject_inline_callees(
88                items,
89                checkpoint.caller,
90                ENGINE_INLINE_DEPTH,
91            );
92
93            let wrapped = crate::verify::slicer::ProofGoal {
94                path: backward.path,
95                items,
96            };
97
98            let vm_state = self.vm.execute(&ctx, &wrapped);
99
100            // Accumulate checked bounds/disjointness facts across
101            // checkpoints so that a validator called in one checkpoint
102            // can discharge InBound checks in a later checkpoint.
103            accumulated_has_checked = accumulated_has_checked || vm_state.contract_flags.has_checked_bounds;
104            let mut vm_state = vm_state;
105            vm_state.contract_flags.has_checked_bounds = accumulated_has_checked;
106
107            let result = self.checker.check(&vm_state, checkpoint, &bound_property);
108            results.push((result, path_desc));
109        }
110
111        results
112    }
113
114    fn callee_is_simple(tcx: TyCtxt<'_>, callee_def_id: DefId) -> bool {
115        crate::helpers::mir_utils::callee_is_linear(tcx, callee_def_id, 3)
116    }
117
118    /// Scan the relevant items for unsupported Call terminators whose callee
119    /// has available MIR. For each such call, inject `CalleeEntry` + callee
120    /// MIR items + `CalleeExit`, replacing the original terminator.
121    fn inject_inline_callees(
122        &self,
123        mut items: Vec<RelevantItem<'tcx>>,
124        caller_def_id: DefId,
125        depth: usize,
126    ) -> Vec<RelevantItem<'tcx>> {
127        if depth == 0 {
128            return items;
129        }
130
131        let tcx = self.slicer.tcx();
132        let body = tcx.optimized_mir(caller_def_id);
133        let mut result: Vec<RelevantItem<'tcx>> = Vec::new();
134
135        for item in items.drain(..) {
136            match &item {
137                RelevantItem::Terminator { block, .. } => {
138                    let terminator = body.basic_blocks[*block].terminator();
139                    if let TerminatorKind::Call { func, args, destination, .. } = &terminator.kind {
140                        if let Some(callee) = crate::helpers::mir_utils::dep_callee_def_id(func) {
141                            if tcx.is_mir_available(callee) {
142                                let summary = crate::verify::call_summary::effect_summary(
143                                    tcx, caller_def_id, func, destination.local,
144                                );
145
146                                if summary.unsupported && Self::callee_is_simple(tcx, callee) {
147                                    let arg_locals: Vec<rustc_middle::mir::Local> = args.iter()
148                                        .filter_map(|arg| match &arg.node {
149                                            rustc_middle::mir::Operand::Copy(p)
150                                            | rustc_middle::mir::Operand::Move(p)
151                                                if p.projection.is_empty() => Some(p.local),
152                                            _ => None,
153                                        })
154                                        .collect();
155                                    if arg_locals.len() == args.len() {
156                                        let callee_items = self.build_callee_items(callee, depth - 1);
157                                        result.push(RelevantItem::CalleeEntry {
158                                            callee,
159                                            args: arg_locals,
160                                        });
161                                        result.extend(callee_items);
162                                        result.push(RelevantItem::CalleeExit {
163                                            dest: destination.local,
164                                        });
165                                        continue; // Skip original Terminator item
166                                    }
167                                }
168                            }
169                        }
170                    }
171                }
172                _ => {}
173            }
174            result.push(item);
175        }
176
177        result
178    }
179
180    /// Build a linear sequence of relevant items for a callee's MIR body.
181    /// Walks BFS from the entry block, collecting statements and terminators.
182    fn build_callee_items(
183        &self,
184        callee_def_id: DefId,
185        depth: usize,
186    ) -> Vec<RelevantItem<'tcx>> {
187        let mut items: Vec<RelevantItem<'tcx>> = Vec::new();
188        let tcx = self.slicer.tcx();
189        let body = tcx.optimized_mir(callee_def_id);
190
191        let mut visited = FxHashSet::default();
192        let mut queue: Vec<BasicBlock> = Vec::new();
193        queue.push(BasicBlock::from_usize(0));
194
195        while let Some(block) = queue.pop() {
196            if !visited.insert(block) {
197                continue;
198            }
199
200            let bb_data = &body.basic_blocks[block];
201
202            for (si, _) in bb_data.statements.iter().enumerate() {
203                items.push(RelevantItem::Statement {
204                    block,
205                    statement_index: si,
206                });
207            }
208
209            let terminator = bb_data.terminator();
210
211            // Recursively inline calls in the callee's terminators
212            match &terminator.kind {
213                TerminatorKind::Call { func, args, destination, target, .. } => {
214                    if let Some(inner_callee) = crate::helpers::mir_utils::dep_callee_def_id(func) {
215                        if tcx.is_mir_available(inner_callee) {
216                            let summary = crate::verify::call_summary::effect_summary(
217                                tcx, callee_def_id, func, destination.local,
218                            );
219
220                            if summary.unsupported && Self::callee_is_simple(tcx, inner_callee) && depth > 0 {
221                                let arg_locals: Vec<rustc_middle::mir::Local> = args.iter()
222                                    .filter_map(|arg| match &arg.node {
223                                        rustc_middle::mir::Operand::Copy(p)
224                                        | rustc_middle::mir::Operand::Move(p)
225                                            if p.projection.is_empty() => Some(p.local),
226                                        _ => None,
227                                    })
228                                    .collect();
229                                if arg_locals.len() == args.len() {
230                                    let inner_items = self.build_callee_items(inner_callee, depth - 1);
231                                    items.push(RelevantItem::CalleeEntry {
232                                        callee: inner_callee,
233                                        args: arg_locals,
234                                    });
235                                    items.extend(inner_items);
236                                    items.push(RelevantItem::CalleeExit {
237                                        dest: destination.local,
238                                    });
239                                    if let Some(t) = target {
240                                        queue.push(*t);
241                                    }
242                                    continue;
243                                }
244                            }
245                        }
246                    }
247                    items.push(RelevantItem::Terminator {
248                        block,
249                    });
250                    if let Some(t) = target {
251                        queue.push(*t);
252                    }
253                }
254                TerminatorKind::Goto { target } => {
255                    queue.push(*target);
256                    items.push(RelevantItem::Terminator {
257                        block,
258                    });
259                }
260                TerminatorKind::Return => {
261                    items.push(RelevantItem::Terminator {
262                        block,
263                    });
264                }
265                TerminatorKind::Assert { target, .. } => {
266                    queue.push(*target);
267                    items.push(RelevantItem::Terminator {
268                        block,
269                    });
270                }
271                TerminatorKind::SwitchInt { targets, .. } => {
272                    for (_, t) in targets.iter() {
273                        queue.push(t);
274                    }
275                    queue.push(targets.otherwise());
276                    items.push(RelevantItem::Terminator {
277                        block,
278                    });
279                }
280                TerminatorKind::Drop { target, .. } => {
281                    queue.push(*target);
282                    items.push(RelevantItem::Terminator {
283                        block,
284                    });
285                }
286                _ => {
287                    items.push(RelevantItem::Terminator {
288                        block,
289                    });
290                }
291            }
292        }
293
294        items
295    }
296
297    fn bind_property_to_checkpoint(
298        property: &Property<'tcx>,
299        checkpoint: &Checkpoint<'tcx>,
300    ) -> Property<'tcx> {
301        match property {
302            Property::Leaf(leaf) => {
303                let new_args: Vec<super::contract::PropertyArg<'tcx>> = leaf
304                    .args
305                    .iter()
306                    .map(|a| match a {
307                        super::contract::PropertyArg::Expr(expr) => {
308                            super::contract::PropertyArg::Expr(Self::rebind_contract_expr(
309                                expr,
310                                checkpoint,
311                            ))
312                        }
313                        super::contract::PropertyArg::Predicates(predicates) => {
314                            let rebound: Vec<_> = predicates
315                                .iter()
316                                .map(|p| {
317                                    let lhs = Self::rebind_contract_expr(&p.lhs, checkpoint);
318                                    let rhs = Self::rebind_contract_expr(&p.rhs, checkpoint);
319                                    super::contract::NumericPredicate::new(lhs, p.op, rhs)
320                                })
321                                .collect();
322                            super::contract::PropertyArg::Predicates(rebound)
323                        }
324                        _ => a.clone(),
325                    })
326                    .collect();
327                Property::Leaf(LeafProperty {
328                    kind: leaf.kind,
329                    args: new_args,
330                    contract_kind: leaf.contract_kind,
331                    null_guard: leaf.null_guard.clone(),
332                    for_each: leaf.for_each.clone(),
333                    origin_name: None,
334                    origin_args: None,
335                    origin_meaning: None,
336                })
337            }
338            Property::Or(or) => {
339                let new_groups: Vec<Vec<Box<Property<'tcx>>>> = or
340                    .groups
341                    .iter()
342                    .map(|group| {
343                        group
344                            .iter()
345                            .map(|p| Box::new(Self::bind_property_to_checkpoint(p, checkpoint)))
346                            .collect()
347                    })
348                    .collect();
349                Property::Or(OrProperty {
350                    groups: new_groups,
351                    contract_kind: or.contract_kind,
352                    origin_name: None,
353                    origin_args: None,
354                    origin_meaning: None,
355                })
356            }
357        }
358    }
359
360    fn rebind_place(
361        place: &super::contract::ContractPlace<'tcx>,
362        checkpoint: &Checkpoint<'tcx>,
363    ) -> super::contract::ContractPlace<'tcx> {
364        let new_base = match place.base {
365            super::contract::PlaceBase::Return => super::contract::PlaceBase::Return,
366            super::contract::PlaceBase::Arg(n) => super::contract::PlaceBase::Arg(n),
367            super::contract::PlaceBase::Local(n) => {
368                if n > 0 && n <= checkpoint.args.len() {
369                    super::contract::PlaceBase::Arg(n - 1)
370                } else {
371                    super::contract::PlaceBase::Local(n)
372                }
373            }
374        };
375        super::contract::ContractPlace {
376            base: new_base,
377            projections: place.projections.clone(),
378        }
379    }
380
381    fn rebind_contract_expr(
382        expr: &super::contract::ContractExpr<'tcx>,
383        checkpoint: &Checkpoint<'tcx>,
384    ) -> super::contract::ContractExpr<'tcx> {
385        match expr {
386            super::contract::ContractExpr::Place(place) => {
387                super::contract::ContractExpr::Place(Self::rebind_place(place, checkpoint))
388            }
389            super::contract::ContractExpr::Len(inner) => {
390                super::contract::ContractExpr::Len(Box::new(Self::rebind_contract_expr(inner, checkpoint)))
391            }
392            super::contract::ContractExpr::SizeOf(_) | super::contract::ContractExpr::AlignOf(_)
393            | super::contract::ContractExpr::Const(_) | super::contract::ContractExpr::ConstParam { .. }
394            | super::contract::ContractExpr::Unknown => expr.clone(),
395            super::contract::ContractExpr::IndexAccess { slice, index } => {
396                super::contract::ContractExpr::IndexAccess {
397                    slice: Box::new(Self::rebind_contract_expr(slice, checkpoint)),
398                    index: Box::new(Self::rebind_contract_expr(index, checkpoint)),
399                }
400            }
401            super::contract::ContractExpr::Binary { op, lhs, rhs } => {
402                super::contract::ContractExpr::Binary {
403                    op: *op,
404                    lhs: Box::new(Self::rebind_contract_expr(lhs, checkpoint)),
405                    rhs: Box::new(Self::rebind_contract_expr(rhs, checkpoint)),
406                }
407            }
408            super::contract::ContractExpr::Unary { op, expr: inner } => {
409                super::contract::ContractExpr::Unary {
410                    op: *op,
411                    expr: Box::new(Self::rebind_contract_expr(inner, checkpoint)),
412                }
413            }
414            super::contract::ContractExpr::Min { a, b } => {
415                super::contract::ContractExpr::Min {
416                    a: Box::new(Self::rebind_contract_expr(a, checkpoint)),
417                    b: Box::new(Self::rebind_contract_expr(b, checkpoint)),
418                }
419            }
420            super::contract::ContractExpr::Max { a, b } => {
421                super::contract::ContractExpr::Max {
422                    a: Box::new(Self::rebind_contract_expr(a, checkpoint)),
423                    b: Box::new(Self::rebind_contract_expr(b, checkpoint)),
424                }
425            }
426            super::contract::ContractExpr::If {
427                cond,
428                then_expr,
429                else_expr,
430            } => {
431                super::contract::ContractExpr::If {
432                    cond: Box::new(super::contract::NumericPredicate::new(
433                        Self::rebind_contract_expr(&cond.lhs, checkpoint),
434                        cond.op,
435                        Self::rebind_contract_expr(&cond.rhs, checkpoint),
436                    )),
437                    then_expr: Box::new(Self::rebind_contract_expr(then_expr, checkpoint)),
438                    else_expr: Box::new(Self::rebind_contract_expr(else_expr, checkpoint)),
439                }
440            }
441        }
442    }
443
444    pub fn check_invariant_from_tree(
445        &self,
446        def_id: DefId,
447        tree: &PathTree,
448        checkpoint: CheckpointLocation,
449        invariant: &Property<'tcx>,
450        entry_facts: &[RelevantItem<'tcx>],
451    ) -> Vec<(CheckResult, String)> {
452        let target_block = checkpoint.block.as_usize();
453        let mut results = Vec::new();
454        let backward_items = self.slicer.visit_path_tree_for_checkpoint(
455            tree,
456            target_block,
457            def_id,
458            checkpoint,
459            invariant,
460        );
461
462        let ctx = Self::new_z3_context();
463
464        for mut backward in backward_items {
465            let path_desc = backward.path.describe_indices();
466
467            if !entry_facts.is_empty() {
468                let mut items: Vec<RelevantItem<'tcx>> = entry_facts.to_vec();
469                items.extend(backward.items.drain(..));
470                backward.items = items;
471            }
472
473            let vm_state = self.vm.execute(&ctx, &backward);
474
475            let fake_checkpoint = Checkpoint {
476                caller: def_id,
477                callee: None,
478                block: checkpoint.block,
479                span: rustc_span::DUMMY_SP,
480                args: Vec::new(),
481                kind: crate::helpers::mir_scan::CheckpointKind::UnsafeCall,
482                is_ref: false,
483                is_mut_ref: false,
484                destination: None,
485            };
486            let result = self.checker.check(&vm_state, &fake_checkpoint, invariant);
487            results.push((result, path_desc));
488        }
489
490        results
491    }
492}
rapx/verify/engine.rs

rapx/verify/
engine.rs
