rapx/check/senryx/verification/
pointer.rs

1//! Composite pointer-safety contract checkers.
2//!
3//! This module owns `Allocated`, `Deref`, `ValidPtr`, and pointer-to-reference
4//! conversion checks. Several leaf predicates are still conservative
5//! placeholders, but the composite APIs keep the contract structure explicit.
6
7use crate::check::senryx::{contract::ContractExpr, visitor::BodyVisitor};
8use rustc_middle::ty::Ty;
9
10impl<'tcx> BodyVisitor<'tcx> {
11    /// Placeholder for allocation provenance checking.
12    pub fn check_allocated(&self, _arg: usize) -> bool {
13        true
14    }
15
16    /// Check the composite `ValidPtr` contract.
17    pub fn check_valid_ptr(
18        &self,
19        arg: usize,
20        length_arg: ContractExpr<'tcx>,
21        contract_ty: Ty<'tcx>,
22    ) -> bool {
23        !self.check_non_zst(arg)
24            || (self.check_non_zst(arg) && self.check_deref(arg, length_arg, contract_ty))
25    }
26
27    /// Check that a pointer can be dereferenced for the requested extent.
28    pub fn check_deref(
29        &self,
30        arg: usize,
31        length_arg: ContractExpr<'tcx>,
32        contract_ty: Ty<'tcx>,
33    ) -> bool {
34        self.check_allocated(arg) && self.check_inbound(arg, length_arg, contract_ty)
35    }
36
37    /// Check the composite pointer-to-reference conversion contract.
38    pub fn check_ref_to_ptr(
39        &self,
40        arg: usize,
41        length_arg: ContractExpr<'tcx>,
42        contract_ty: Ty<'tcx>,
43    ) -> bool {
44        self.check_deref(arg, length_arg, contract_ty)
45            && self.check_init(arg)
46            && self.check_align(arg, contract_ty)
47            && self.check_alias(arg)
48    }
49}
rapx/check/senryx/verification/pointer.rs

rapx/check/senryx/verification/
pointer.rs
