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

//! SMT lowering for the composite `ValidPtr` safety property.
//!
//! `ValidPtr(p, T, n)` is not a primitive SMT obligation.  The verifier treats
//! it as a bundle of smaller safety properties.  This module keeps that
//! decomposition local to the `ValidPtr` SP and delegates implemented pieces to
//! the corresponding SMT modules:
//!
//! ```text
//! ValidPtr(p, T, n)
//!   -> NonNull(p)
//!   -> Align(p, T)
//!   -> Allocated(p, T, n)  // future
//!   -> InBound(p, T, n)    // future
//!   -> Init(p, T, n)       // future
//!   -> Typed(p, T)         // future
//! ```
//!
//! Until all pieces are implemented, the composite result remains `Unknown`,
//! but the report shows which implemented primitive SMT obligations already
//! succeed.

use super::{
    align,
    common::{SmtCheckResult, SmtChecker},
    in_bound, init, non_null,
};
use crate::verify::{
    contract::{Property, PropertyKind},
    forward_visit::ForwardVisitResult,
    helpers::Callsite,
};

/// Check the implemented primitive pieces of `ValidPtr`.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    callsite: &Callsite<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let non_null_property = primitive_property(property, PropertyKind::NonNull);
    let align_property = primitive_property(property, PropertyKind::Align);
    let in_bound_property = primitive_property(property, PropertyKind::InBound);
    let init_property = primitive_property(property, PropertyKind::Init);

    let non_null = non_null::check(checker, callsite, &non_null_property, forward);
    let align = align::check(checker, callsite, &align_property, forward);
    let in_bound = in_bound::check(checker, callsite, &in_bound_property, forward);
    let init = init::check(checker, callsite, &init_property, forward);

    SmtCheckResult::unknown(
        "ValidPtr is decomposed, but not all primitive obligations are implemented yet",
    )
    .with_note(format!("primitive NonNull via SMT: {:?}", non_null.result))
    .with_note(format!("primitive Align via SMT: {:?}", align.result))
    .with_note(format!("primitive InBound via SMT: {:?}", in_bound.result))
    .with_note(format!("primitive Init via SMT: {:?}", init.result))
    .with_note("missing primitive SMT lowerings: Allocated, Typed")
}

/// Reuse the original arguments while checking one primitive component.
fn primitive_property<'tcx>(property: &Property<'tcx>, kind: PropertyKind) -> Property<'tcx> {
    Property {
        kind,
        args: property.args.clone(),
    }
}