rapx 0.7.28

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

//! SMT lowering for the `ValidNum` safety property.
//!
//! `ValidNum` carries one or more numeric predicates, for example:
//!
//! ```text
//! ValidNum(i < len)
//! ValidNum(size_of(T) * len <= isize::MAX)
//! ```
//!
//! This module only rebinds callee-side contract expressions to the concrete
//! checkpoint arguments and converts them to common SMT predicates.  The shared
//! backend discharges the query by checking whether the negated predicate is
//! satisfiable under the forward path facts.

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

/// Check `ValidNum` by lowering all predicates to a common predicate obligation.
pub(crate) fn check<'tcx>(
    checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    property: &Property<'tcx>,
    forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult {
    let Some(smt_predicates) =
        checker.property_numeric_smt_predicates(checkpoint, property, Some(forward))
    else {
        return SmtCheckResult::unknown("ValidNum predicate could not be lowered to SMT");
    };

    if checker.validnum_is_slice_size_invariant(checkpoint, property, forward) {
        return SmtCheckResult::proved(
            "ValidNum proved: slice-size language invariant size_of(T) * slice.len() <= isize::MAX",
        );
    }

    // `align_of::<T>()` is always >= 1 for any type.  When a ValidNum predicate
    // is a single `x != 0` and `x` resolves to the align_of call argument at the
    // callsite (e.g. `ptr::align_offset(ptr, align_of::<U>())` requiring `a != 0`),
    // the constraint holds trivially.  The SMT model cannot prove this because
    // `align_of` is a symbolic constant, so we short-circuit here.
    if checker.validnum_is_align_nonzero(checkpoint, property, forward) {
        return SmtCheckResult::proved("ValidNum proved: align_of::<T>() >= 1 for every T");
    }

    if let Some(reason) = super::provenance::vec_from_raw_parts_roundtrip(checker, checkpoint) {
        return SmtCheckResult::proved(format!("ValidNum proved: {reason}"));
    }

    checker.prove_obligation(
        checkpoint,
        forward,
        SmtObligation::Predicate {
            predicates: smt_predicates,
        },
        property.null_guard.as_ref(),
    )
}