rapx/verify/smt_check/
deref.rs

1//! SMT lowering for the `Deref` safety property.
2//!
3//! `Deref(p, T, n)` is the range-level part of pointer validity:
4//!
5//! ```text
6//! Deref(p, T, n) = Allocated(p, T, n, *) && InBound(p, T, n)
7//! ```
8//!
9//! The star in `Allocated` represents the current allocation object/provenance
10//! abstraction.  This module keeps `Deref` as a composite SP and delegates the
11//! object and bounds checks to their existing lowerings.
12
13use super::{allocated, common::SmtCheckResult, in_bound};
14use crate::verify::{
15    contract::Property, helpers::Checkpoint, report::CheckResult, verifier::ForwardVisitResult,
16};
17
18/// Check `Deref` by proving both allocation and bounds obligations.
19pub(crate) fn check<'tcx>(
20    checker: &super::common::SmtChecker<'tcx>,
21    checkpoint: &Checkpoint<'tcx>,
22    property: &Property<'tcx>,
23    forward: &ForwardVisitResult<'tcx>,
24) -> SmtCheckResult {
25    let allocated = allocated::check(checker, checkpoint, property, forward);
26    let in_bound = in_bound::check(checker, checkpoint, property, forward);
27
28    match (&allocated.result, &in_bound.result) {
29        (CheckResult::Proved, CheckResult::Proved) => {
30            SmtCheckResult::proved("Deref proved: target range is allocated and in bounds")
31        }
32        (CheckResult::Failed, _) | (_, CheckResult::Failed) => SmtCheckResult {
33            result: CheckResult::Failed,
34            query: None,
35            notes: vec![String::from(
36                "Deref failed: Allocated and InBound must both hold",
37            )],
38        },
39        _ => SmtCheckResult::unknown("Deref unknown: Allocated or InBound is not proved"),
40    }
41    .with_note(format!(
42        "primitive Allocated via SMT: {:?}",
43        allocated.result
44    ))
45    .with_note(format!("primitive InBound via SMT: {:?}", in_bound.result))
46}
rapx/verify/smt_check/deref.rs

rapx/verify/smt_check/
deref.rs
