rapx/verify/smt_check/
allocated.rs

1//! SMT lowering for the `Allocated` safety property.
2//!
3//! `Allocated(p, T, n)` means the whole `n`-element range starting at `p`
4//! belongs to a single live allocation object.  The lowering is intentionally
5//! object-sensitive: adjacent stack locals do not form one larger allocation
6//! even when their addresses happen to be close.
7
8use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
9use crate::verify::{contract::Property, helpers::Checkpoint, verifier::ForwardVisitResult};
10
11/// Check `Allocated` by lowering it to a common allocation obligation.
12pub(crate) fn check<'tcx>(
13    checker: &SmtChecker<'tcx>,
14    checkpoint: &Checkpoint<'tcx>,
15    property: &Property<'tcx>,
16    forward: &ForwardVisitResult<'tcx>,
17) -> SmtCheckResult {
18    let Some(target) = checker.property_target(checkpoint, property) else {
19        return SmtCheckResult::unknown("Allocated target could not be resolved");
20    };
21    if checker.property_required_ty(checkpoint, property).is_none()
22        && checker.property_len_expr(checkpoint, property).is_none()
23    {
24        if checker.is_len_carrying_place_for_caller(checkpoint.caller, &target) {
25            return SmtCheckResult::proved(
26                "allocation proved: safe slice/reference target carries one live allocation object",
27            );
28        }
29        return SmtCheckResult::unknown(
30            "Allocated target has no type/count arguments and is not a supported slice/reference",
31        );
32    }
33    let Some(required_ty) = checker.property_required_ty(checkpoint, property) else {
34        return SmtCheckResult::unknown("Allocated type could not be resolved");
35    };
36    let Some(elements_expr) = checker.property_len_expr(checkpoint, property) else {
37        return SmtCheckResult::unknown("Allocated element-count argument could not be resolved");
38    };
39    let Some(elements) = checker.contract_expr_to_smt_term(checkpoint.caller, &elements_expr)
40    else {
41        return SmtCheckResult::unknown(
42            "Allocated element-count argument could not be lowered to SMT",
43        );
44    };
45
46    checker.prove_obligation(
47        checkpoint,
48        forward,
49        SmtObligation::Allocated {
50            place: target,
51            ty_name: format!("{required_ty:?}"),
52            elements,
53        },
54    )
55}
rapx/verify/smt_check/allocated.rs

rapx/verify/smt_check/
allocated.rs
