rapx/verify/
engine.rs

1//! Shared verification engine for the staged verifier pipeline.
2//!
3//! This module extracts the common backward-visit → forward-visit → SMT-check
4//! flow that is shared between unsafe-checkpoint verification and struct-invariant
5//! verification, keeping both pipelines thin and focused on their own
6//! path-preparation logic.
7
8use rustc_hir::def_id::DefId;
9use rustc_middle::ty::TyCtxt;
10
11use crate::analysis::path_analysis::PathTree;
12
13use super::{
14    contract::Property,
15    helpers::{Checkpoint, CheckpointLocation},
16    report::CheckResult,
17    slicer::{BackwardItem, BackwardSlicer},
18    smt_check::{SmtCheckResult, SmtChecker},
19    verifier::{ForwardVerifier, ForwardVisitResult},
20};
21
22/// Result of checking one invariant along one reachability path.
23pub struct InvariantCheckResult {
24    /// Whether the invariant was proved, violated, or undecided.
25    pub result: CheckResult,
26    /// Backward slicing summary (MIR items kept along this path).
27    pub slicing_diag: String,
28    /// Combined forward verification and SMT check summary.
29    pub verification_diag: String,
30}
31
32/// Thin wrapper around the three-stage verification pipeline.
33///
34/// Each structural check (checkpoint or invariant) delegates to one of the two
35/// public methods; the engine handles visitor bookkeeping internally.
36pub struct VerifyEngine<'tcx> {
37    slicer: BackwardSlicer<'tcx>,
38    verifier: ForwardVerifier<'tcx>,
39    checker: SmtChecker<'tcx>,
40}
41
42impl<'tcx> VerifyEngine<'tcx> {
43    /// Create an engine for the current compiler type context.
44    pub fn new(tcx: TyCtxt<'tcx>) -> Self {
45        Self {
46            slicer: BackwardSlicer::new(tcx),
47            verifier: ForwardVerifier::new(tcx),
48            checker: SmtChecker::new(tcx),
49        }
50    }
51
52    /// Run the invariant-check pipeline in bulk using a per-checkpoint path tree.
53    ///
54    /// Calls `visit_path_tree_for_checkpoint` once, then forward + SMT per
55    /// path.  The tree already contains only paths reaching `checkpoint`;
56    /// common prefixes are shared to avoid redundant backward analysis.
57    pub fn check_invariant_from_tree(
58        &self,
59        def_id: DefId,
60        tree: &PathTree,
61        checkpoint: CheckpointLocation,
62        invariant: &Property<'tcx>,
63        entry_facts: &[BackwardItem<'tcx>],
64    ) -> Vec<InvariantCheckResult> {
65        let target_block = checkpoint.block.as_usize();
66        let mut results = Vec::new();
67        let backward_items = self.slicer.visit_path_tree_for_checkpoint(
68            tree,
69            target_block,
70            def_id,
71            checkpoint,
72            invariant,
73        );
74
75        for mut backward in backward_items {
76            if !entry_facts.is_empty() {
77                let mut items: Vec<BackwardItem<'tcx>> = entry_facts.to_vec();
78                items.extend(backward.items.clone());
79                backward.items = items;
80            }
81            let forward = self.verifier.visit(&backward);
82            let smt = self
83                .checker
84                .check_for_checkpoint(def_id, invariant, &forward);
85
86            let tcx = self.slicer.tcx();
87            let slicing_diag = backward.describe_for_checkpoint(tcx, checkpoint, 0);
88            let verification_diag = format!("{}\n{}", forward.describe(), smt.describe());
89
90            results.push(InvariantCheckResult {
91                result: smt.result,
92                slicing_diag,
93                verification_diag,
94            });
95        }
96
97        results
98    }
99
100    /// Run the checkpoint-check pipeline in bulk using a per-checkpoint path tree.
101    ///
102    /// Calls `visit_path_tree` once, then forward + SMT per path.
103    pub fn check_callsite_from_tree(
104        &self,
105        tree: &PathTree,
106        checkpoint: &Checkpoint<'tcx>,
107        property: &Property<'tcx>,
108        caller_contracts: &[Property<'tcx>],
109    ) -> Vec<(ForwardVisitResult<'tcx>, SmtCheckResult)> {
110        let target_block = checkpoint.block.as_usize();
111        let mut results = Vec::new();
112        let backward_items = self
113            .slicer
114            .visit_path_tree(tree, target_block, checkpoint, property);
115
116        for mut backward in backward_items {
117            if !caller_contracts.is_empty() {
118                let mut items: Vec<BackwardItem<'tcx>> = caller_contracts
119                    .iter()
120                    .filter(|c| !matches!(c.kind, super::contract::PropertyKind::Unknown))
121                    .map(|c| BackwardItem::ContractFact {
122                        property: c.clone(),
123                    })
124                    .collect();
125                items.extend(backward.items.clone());
126                backward.items = items;
127            }
128            let forward = self.verifier.visit(&backward);
129            let smt = self.checker.check(checkpoint, property, &forward);
130            results.push((forward, smt));
131        }
132
133        results
134    }
135}
rapx/verify/engine.rs

rapx/verify/
engine.rs
