rapx/check/senryx/verification/
bounds.rs

1//! Boundary and size-related contract helpers.
2//!
3//! This module owns checks that reason about object extents, element counts,
4//! and zero-sized types. `InBound` is currently conservative because the graph
5//! now stores expression-shaped length contracts but does not yet discharge all
6//! numeric relationships.
7
8use crate::check::senryx::{
9    contract::ContractExpr,
10    visitor::{BodyVisitor, PlaceTy},
11};
12use rustc_middle::ty::Ty;
13
14impl<'tcx> BodyVisitor<'tcx> {
15    /// Return true when the modeled object reached by `arg` is zero-sized.
16    ///
17    /// The API name is kept for compatibility with existing call sites, but the
18    /// current implementation returns `true` for ZST objects.
19    pub fn check_non_zst(&self, arg: usize) -> bool {
20        let obj_ty = self.chains.get_obj_ty_through_chain(arg);
21        if obj_ty.is_none() {
22            self.show_error_info(arg);
23        }
24        let ori_ty = self.visit_ty_and_get_layout(obj_ty.unwrap());
25        match ori_ty {
26            PlaceTy::Ty(_align, size) => size == 0,
27            PlaceTy::GenericTy(_, _, tys) => {
28                if tys.is_empty() {
29                    return false;
30                }
31                for (_, size) in tys {
32                    if size != 0 {
33                        return false;
34                    }
35                }
36                true
37            }
38            _ => false,
39        }
40    }
41
42    /// Check the in-bounds contract for a pointer and element count.
43    ///
44    /// This is intentionally conservative until length constraints from
45    /// contract facts and symbolic values are connected into one proof procedure.
46    pub fn check_inbound(
47        &self,
48        _arg: usize,
49        _length_arg: ContractExpr<'tcx>,
50        _contract_ty: Ty<'tcx>,
51    ) -> bool {
52        false
53    }
54}
rapx/check/senryx/verification/bounds.rs

rapx/check/senryx/verification/
bounds.rs
