rapx/verify/smt_check/
in_bound.rs

1//! SMT lowering for the `InBound` safety property.
2//!
3//! The current implementation handles the common slice pattern:
4//!
5//! ```text
6//! ptr = slice.as_ptr()
7//! current = ptr.add(index)
8//! guard: index < slice.len()
9//! property: InBound(current, T, n)
10//! ```
11//!
12//! The module only lowers the property to `SmtObligation::InBounds`.  The
13//! common SMT model is responsible for matching `as_ptr`, `ptr.add`, `len`, and
14//! branch facts from the forward visit result.
15
16use super::common::{SmtCheckResult, SmtChecker, SmtObligation, SmtTerm};
17use crate::verify::{
18    contract::Property, helpers::Checkpoint, primitive::PrimitiveCall, verifier::ForwardVisitResult,
19};
20
21/// Check `InBound` by lowering it to a common bounds obligation.
22pub(crate) fn check<'tcx>(
23    checker: &SmtChecker<'tcx>,
24    checkpoint: &Checkpoint<'tcx>,
25    property: &Property<'tcx>,
26    forward: &ForwardVisitResult<'tcx>,
27) -> SmtCheckResult {
28    if let Some(predicates) =
29        checker.property_index_access_in_bound_predicates(checkpoint, property)
30    {
31        return checker.prove_obligation(
32            checkpoint,
33            forward,
34            SmtObligation::Predicate { predicates },
35        );
36    }
37
38    let Some(target) = checker.property_target(checkpoint, property) else {
39        rap_debug!("  [SMT InBound] target could not be resolved");
40        return SmtCheckResult::unknown("InBound target could not be resolved");
41    };
42    let Some(required_ty) = checker
43        .property_required_ty(checkpoint, property)
44        .or_else(|| checker.infer_pointee_ty(checkpoint.caller, &target))
45    else {
46        rap_debug!("  [SMT InBound] type could not be resolved");
47        return SmtCheckResult::unknown("InBound type could not be resolved");
48    };
49    let elem_size = checker
50        .type_layout(checkpoint.caller, required_ty)
51        .map(|(_, s)| s)
52        .unwrap_or(0);
53    let access_count = checker
54        .property_len_expr(checkpoint, property)
55        .and_then(|expr| checker.contract_expr_to_smt_term(checkpoint.caller, &expr))
56        .unwrap_or(SmtTerm::Const(1));
57
58    if let Some(obligation) =
59        pointer_arithmetic_obligation(checker, checkpoint, required_ty, access_count.clone())
60    {
61        return checker.prove_obligation(checkpoint, forward, obligation);
62    }
63
64    checker.prove_obligation(
65        checkpoint,
66        forward,
67        SmtObligation::InBounds {
68            place: target,
69            ty_name: format!("{required_ty:?}"),
70            elem_size,
71            access_count,
72        },
73    )
74}
75
76fn pointer_arithmetic_obligation<'tcx>(
77    checker: &SmtChecker<'tcx>,
78    checkpoint: &Checkpoint<'tcx>,
79    required_ty: rustc_middle::ty::Ty<'tcx>,
80    count: SmtTerm,
81) -> Option<SmtObligation> {
82    let callee_name = checker.tcx.def_path_str(checkpoint.callee?);
83    let primitive = PrimitiveCall::classify(&callee_name)?;
84    if !primitive.is_pointer_arithmetic() {
85        return None;
86    }
87
88    let base = checker.callsite_arg_place(checkpoint, 0)?;
89    let zero = SmtTerm::Const(0);
90    let negative_count = SmtTerm::Sub(Box::new(zero.clone()), Box::new(count.clone()));
91    let (lower_delta, upper_delta) = if primitive.is_pointer_sub_like() {
92        (negative_count, zero)
93    } else if primitive.is_signed_pointer_arithmetic() {
94        (count.clone(), count)
95    } else {
96        (zero, count)
97    };
98
99    Some(SmtObligation::PointerRangeInBounds {
100        place: base,
101        ty_name: format!("{required_ty:?}"),
102        lower_delta,
103        upper_delta,
104    })
105}
106
107/// Check `InBound` at a return checkpoint for struct invariant verification.
108pub(crate) fn check_for_checkpoint<'tcx>(
109    checker: &SmtChecker<'tcx>,
110    caller: rustc_hir::def_id::DefId,
111    property: &Property<'tcx>,
112    forward: &ForwardVisitResult<'tcx>,
113) -> SmtCheckResult {
114    let Some(target) = checker.property_target_direct(property) else {
115        return SmtCheckResult::unknown("InBound target could not be resolved");
116    };
117    let Some(required_ty) = checker.property_required_ty_direct(property) else {
118        return SmtCheckResult::unknown("InBound type could not be resolved");
119    };
120    let elem_size = checker
121        .type_layout(caller, required_ty)
122        .map(|(_, s)| s)
123        .unwrap_or(0);
124    let Some(access_count_expr) = checker.property_len_expr_direct(property) else {
125        return SmtCheckResult::unknown("InBound length argument could not be resolved");
126    };
127    let Some(access_count) = checker.contract_expr_to_smt_term(caller, &access_count_expr) else {
128        return SmtCheckResult::unknown("InBound length argument could not be lowered to SMT");
129    };
130
131    checker.prove_obligation_for_checkpoint(
132        caller,
133        forward,
134        SmtObligation::InBounds {
135            place: target,
136            ty_name: format!("{required_ty:?}"),
137            elem_size,
138            access_count,
139        },
140    )
141}
rapx/verify/smt_check/in_bound.rs

rapx/verify/smt_check/
in_bound.rs
