rapx 0.7.1

A static analysis platform for use-after-free, memory leakage detection, etc
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
64
65
66
67
68
69
70
71
72
73
74
75

//! SMT lowering for the `Align` safety property.
//!
//! This module reduces:
//!
//! ```text
//! Align(p, T)
//! ```
//!
//! to the common SMT obligation:
//!
//! ```text
//! Aligned { place: p, align: align_of(T) }
//! ```
//!
//! The common model then proves the obligation by asking whether the path facts
//! plus the negated alignment goal are satisfiable.

use super::common::{SmtCheckResult, SmtChecker, SmtObligation};
use crate::verify::{contract::Property, forward_visit::ForwardVisitResult, helpers::Callsite};

/// Check `Align` by lowering it to `SmtObligation::Aligned`.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    callsite: &Callsite<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let Some(target) = checker.property_target(callsite, property) else {
        return SmtCheckResult::unknown("SMT Align target could not be resolved");
    };
    let Some(required_ty) = checker.property_required_ty(callsite, property) else {
        return SmtCheckResult::unknown("SMT Align type could not be resolved");
    };
    let Some((required_align, _)) = checker.type_layout(callsite.caller, required_ty) else {
        return SmtCheckResult::unknown(format!(
            "SMT Align layout unavailable for {:?}",
            required_ty
        ));
    };

    let obligation = SmtObligation::Aligned {
        place: target,
        align: required_align,
        ty_name: format!("{required_ty:?}"),
    };
    checker.prove_obligation(callsite, forward, obligation)
}

/// Check `Align` at a return checkpoint for struct invariant verification.
pub(crate) fn check_for_checkpoint<'tcx>(
    checker: &SmtChecker<'tcx>,
    caller: rustc_hir::def_id::DefId,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let Some(target) = checker.property_target_direct(property) else {
        return SmtCheckResult::unknown("SMT Align target could not be resolved");
    };
    let Some(required_ty) = checker.property_required_ty_direct(property) else {
        return SmtCheckResult::unknown("SMT Align type could not be resolved");
    };
    let Some((required_align, _)) = checker.type_layout(caller, required_ty) else {
        return SmtCheckResult::unknown(format!(
            "SMT Align layout unavailable for {:?}",
            required_ty
        ));
    };

    let obligation = SmtObligation::Aligned {
        place: target,
        align: required_align,
        ty_name: format!("{required_ty:?}"),
    };
    checker.prove_obligation_for_checkpoint(caller, forward, obligation)
}