Struct VerifyEngine 

pub(crate) struct VerifyEngine<'tcx> {
    tcx: TyCtxt<'tcx>,
    slicer: BackwardSlicer<'tcx>,
    vm: SymbolicVm,
    checker: PropertyChecker,
}

The three verification stages: a backward BackwardSlicer, a SymbolicVm, and a PropertyChecker.

Fields

tcx: TyCtxt<'tcx>

slicer: BackwardSlicer<'tcx>

vm: SymbolicVm

checker: PropertyChecker

Implementations

impl<'tcx> VerifyEngine<'tcx>

pub(crate) fn new(tcx: TyCtxt<'tcx>) -> Self

Construct a fresh engine wired to tcx.

fn new_z3_context() -> Context

Create a fresh Z3 context with a fixed 10s solver timeout.

A new context is created per top-level check so that each verification runs in isolation (no shared solver state leaks between checks).

pub(crate) fn check_callsite_from_tree( &self, tree: &PathTree, checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>, caller_contracts: &[Property<'tcx>], ) -> Vec<(CheckResult, String)>

Verify a property against every path reaching checkpoint, one result per path. Each path is sliced backward from the checkpoint, replayed symbolically by the VM, and finally discharged by the property checker.

Returns (result, path_description) pairs in forward MIR order.

pub(crate) fn check_drop_from_tree( &self, tree: &PathTree, checkpoint: &Checkpoint<'tcx>, ) -> Vec<(CheckResult, String)>

Path-sensitive forward scan for the Drop hazard.

manually_drop::drop(&mut slot) frees the heap behind slot, but slot (a ManuallyDrop wrapper) stays live. A later use of slot reads through the freed allocation — a use-after-free. Unlike the other properties (checked at the checkpoint by the VM over a backward-sliced path), this is a forward obligation, so it walks the complete paths of the shared PathTree and checks the suffix after the drop call.

fn drop_referent_local(&self, checkpoint: &Checkpoint<'tcx>) -> Option<Local>

Resolve the &mut slot borrow operand of a Drop(slot) checkpoint to the referent local (slot itself, e.g. _1). The optimized MIR lowers drop(&mut slot) to a reborrow chain (_7 = &mut (*_8), _8 = &mut _1), so follow both direct borrows (&mut _1) and deref reborrows (&mut (*_8)) back to the ultimate referent.

fn block_uses_local( tcx: TyCtxt<'tcx>, caller: DefId, block: usize, local: Local, ) -> bool

Whether any statement or terminator in block reads/writes local.

fn inject_inline_boundaries( items: Vec<RelevantItem<'tcx>>, tree: &PathTree, local_to_global: &HashMap<(DefId, usize), Vec<usize>>, caller: DefId, ) -> Vec<RelevantItem<'tcx>>

Insert CalleeEntry/CalleeExit markers into a forward item stream by detecting def_id transitions (caller → callee → caller). Each inlined callee entry carries its argument binding; each exit writes the callee’s return value back to the caller’s destination.

local_to_global maps (def_id, local_block) pairs to the list of their global block indices in tree (a callee inlined at multiple call sites has several entries, in path order); it is precomputed by the caller so it can be reused across every checkpoint instead of rebuilt per path.

fn bind_property_to_checkpoint( property: &Property<'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> Property<'tcx>

Rewrite a property so its contract expressions refer to the caller’s argument positions at checkpoint rather than the callee’s local numbering. Recurses through Atom/And/Or nodes and clears origin metadata (which only applies to the source-level property).

fn rebind_place( place: &ContractPlace<'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> ContractPlace<'tcx>

Rewrite a contract place’s base to the checkpoint’s view.

Return and Arg bases are unchanged; a Local(n) that falls within the checkpoint’s argument range is remapped to Arg(n - 1) (locals 1..=k correspond to the callee’s arguments in order).

fn rebind_contract_expr( expr: &ContractExpr<'tcx>, checkpoint: &Checkpoint<'tcx>, ) -> ContractExpr<'tcx>

Recursively rewrite every place embedded in a contract expression, rebinding Local bases to argument positions via Self::rebind_place.

pub(crate) fn check_invariant_from_tree( &self, def_id: DefId, tree: &PathTree, checkpoint: CheckpointLocation, invariant: &Property<'tcx>, entry_facts: &[RelevantItem<'tcx>], ) -> Vec<(CheckResult, String)>

Verify an invariant against every path reaching checkpoint.

Unlike Self::check_callsite_from_tree, there is no callsite to bind against, so entry_facts are prepended to each sliced path and the checker runs directly against the invariant. Returns (result, path_description) pairs.