rapx 0.7.20

A static analysis platform for Rust program analysis and verification
Documentation 
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

//! SMT lowering for the `Deref` safety property.
//!
//! `Deref(p, T, n)` is the range-level part of pointer validity:
//!
//! ```text
//! Deref(p, T, n) = Allocated(p, T, n, *) && InBound(p, T, n)
//! ```
//!
//! The star in `Allocated` represents the current allocation object/provenance
//! abstraction.  This module keeps `Deref` as a composite SP and delegates the
//! object and bounds checks to their existing lowerings.

use super::{allocated, common::SmtCheckResult, in_bound};
use crate::verify::{
    contract::Property, helpers::Checkpoint, report::CheckResult, verifier::ForwardVisitResult,
};

/// Check `Deref` by proving both allocation and bounds obligations.
pub(crate) fn check<'tcx>(
    checker: &super::common::SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let allocated = allocated::check(checker, checkpoint, property, forward);
    let in_bound = in_bound::check(checker, checkpoint, property, forward);

    match (&allocated.result, &in_bound.result) {
        (CheckResult::Proved, CheckResult::Proved) => {
            SmtCheckResult::proved("Deref proved: target range is allocated and in bounds")
        }
        (CheckResult::Failed, _) | (_, CheckResult::Failed) => SmtCheckResult {
            result: CheckResult::Failed,
            query: None,
            notes: vec![String::from(
                "Deref failed: Allocated and InBound must both hold",
            )],
        },
        _ => SmtCheckResult::unknown("Deref unknown: Allocated or InBound is not proved"),
    }
    .with_note(format!(
        "primitive Allocated via SMT: {:?}",
        allocated.result
    ))
    .with_note(format!("primitive InBound via SMT: {:?}", in_bound.result))
}