rapx 0.7.29

A static analysis platform for Rust program analysis and verification
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63

//! SMT lowering for the `Align` safety property.
//!
//! Reduces `Align(p, T)` to `SmtObligation::Aligned { place: p, align: align_of(T) }`.

use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
use crate::verify::{contract::Property, verifier::ForwardVisitResult};
use crate::helpers::mir_scan::Checkpoint;

fn resolve<'tcx>(
    checker: &SmtChecker<'tcx>,
    caller: rustc_hir::def_id::DefId,
    property: &Property<'tcx>,
    opt_checkpoint: Option<&Checkpoint<'tcx>>,
) -> Option<(crate::verify::def_use::PlaceKey, u64, String)> {
    let target = checker.property_target(opt_checkpoint, property)?;
    let required_ty = checker.property_required_ty(opt_checkpoint, property)?;
    let align = checker
        .required_alignment(caller, required_ty)
        .or_else(|| checker.type_layout(caller, required_ty).map(|(a, _)| a))
        .unwrap_or(0);
    Some((target, align, format!("{required_ty:?}")))
}

pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    if checkpoint.is_ref {
        return SmtCheckResult::proved("Align trivially holds for ref-derived pointer");
    }
    if let Some(reason) =
        super::field_invariant::discharge_from_contract_fact_with_checkpoint(
            property, forward, checkpoint,
        )
    {
        return SmtCheckResult::proved(format!("Align proved: {reason}"));
    }
    let Some((target, align, ty_name)) =
        resolve(checker, checkpoint.caller, property, Some(checkpoint))
    else {
        return SmtCheckResult::unknown("SMT Align target/type could not be resolved");
    };
    let obligation = SmtObligation::Aligned { place: target, align, ty_name };
    checker.prove_obligation(checkpoint, forward, obligation, property.null_guard.as_ref())
}

pub(crate) fn check_for_checkpoint<'tcx>(
    checker: &SmtChecker<'tcx>,
    caller: rustc_hir::def_id::DefId,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    if let Some(reason) = super::field_invariant::discharge_from_contract_fact(property, forward) {
        return SmtCheckResult::proved(format!("Align proved: {reason}"));
    }
    let Some((target, align, ty_name)) = resolve(checker, caller, property, None) else {
        return SmtCheckResult::unknown("SMT Align target/type could not be resolved");
    };
    let obligation = SmtObligation::Aligned { place: target, align, ty_name };
    checker.prove_obligation_for_checkpoint(caller, forward, obligation)
}