rapx/check/senryx/verification/
misc.rs

1//! Miscellaneous safety-property placeholders.
2//!
3//! These APIs correspond to contract tags that have not yet gained full graph
4//! or symbolic proof procedures. Lightweight checks live here until they are
5//! promoted into dedicated property modules.
6
7use crate::check::senryx::{
8    contract::{ContractExpr, NumericOp, NumericPredicate, NumericUnaryOp, RelOp},
9    visitor::BodyVisitor,
10};
11
12impl<'tcx> BodyVisitor<'tcx> {
13    /// Placeholder for allocator-consistency checking.
14    pub fn check_allocator_consistency(&self, _func_name: String, _arg: usize) -> bool {
15        true
16    }
17
18    /// Placeholder for UTF-8 string validity checking.
19    pub fn check_valid_string(&self, _arg: usize) -> bool {
20        true
21    }
22
23    /// Placeholder for nul-terminated C string validity checking.
24    pub fn check_valid_cstr(&self, _arg: usize) -> bool {
25        true
26    }
27
28    /// Check numeric predicates that are already fully constant.
29    ///
30    /// Non-constant predicates currently return true to preserve the previous
31    /// placeholder behavior; a later `NumericProver` should discharge them with
32    /// symbolic values and path constraints.
33    pub fn check_valid_num(&self, predicates: &[NumericPredicate<'tcx>]) -> bool {
34        predicates
35            .iter()
36            .all(|predicate| self.check_constant_numeric_predicate(predicate))
37    }
38
39    /// Evaluate one numeric predicate when both sides are constants.
40    fn check_constant_numeric_predicate(&self, predicate: &NumericPredicate<'tcx>) -> bool {
41        let (Some(lhs), Some(rhs)) = (
42            Self::eval_constant_contract_expr(&predicate.lhs),
43            Self::eval_constant_contract_expr(&predicate.rhs),
44        ) else {
45            return true;
46        };
47
48        match predicate.op {
49            RelOp::Eq => lhs == rhs,
50            RelOp::Ne => lhs != rhs,
51            RelOp::Lt => lhs < rhs,
52            RelOp::Le => lhs <= rhs,
53            RelOp::Gt => lhs > rhs,
54            RelOp::Ge => lhs >= rhs,
55        }
56    }
57
58    /// Evaluate a contract expression when it is a literal-only expression.
59    fn eval_constant_contract_expr(expr: &ContractExpr<'tcx>) -> Option<u128> {
60        match expr {
61            ContractExpr::Const(value) => Some(*value),
62            ContractExpr::Binary { op, lhs, rhs } => {
63                let lhs = Self::eval_constant_contract_expr(lhs)?;
64                let rhs = Self::eval_constant_contract_expr(rhs)?;
65                match op {
66                    NumericOp::Add => lhs.checked_add(rhs),
67                    NumericOp::Sub => lhs.checked_sub(rhs),
68                    NumericOp::Mul => lhs.checked_mul(rhs),
69                    NumericOp::Div => {
70                        if rhs == 0 {
71                            None
72                        } else {
73                            Some(lhs / rhs)
74                        }
75                    }
76                    NumericOp::Rem => {
77                        if rhs == 0 {
78                            None
79                        } else {
80                            Some(lhs % rhs)
81                        }
82                    }
83                    NumericOp::BitAnd => Some(lhs & rhs),
84                    NumericOp::BitOr => Some(lhs | rhs),
85                    NumericOp::BitXor => Some(lhs ^ rhs),
86                }
87            }
88            ContractExpr::Unary { op, expr } => {
89                let value = Self::eval_constant_contract_expr(expr)?;
90                match op {
91                    NumericUnaryOp::Not => Some(!value),
92                    NumericUnaryOp::Neg => 0_u128.checked_sub(value),
93                }
94            }
95            _ => None,
96        }
97    }
98
99    /// Placeholder for aliasing constraints.
100    pub fn check_alias(&self, _arg: usize) -> bool {
101        true
102    }
103}
rapx/check/senryx/verification/misc.rs

rapx/check/senryx/verification/
misc.rs
