rapx/verify/property_checker/
numeric.rs

1use rustc_middle::mir::Operand;
2use rustc_middle::ty::TyKind;
3#[cfg(not(rapx_has_skip_norm_wip))]
4use crate::compat::SkipNormWip;
5use rustc_hash::FxHashSet;
6use z3::{SatResult, Solver, ast::{Ast, Bool, Int}};
7use crate::verify::contract::{ContractExpr, NumericOp, PlaceBase, Property, PropertyArg, RelOp};
8use crate::verify::def_use::PlaceKey;
9use crate::verify::report::CheckResult;
10use crate::helpers::mir_scan::Checkpoint;
11use crate::verify::vm::state::VmState;
12
13use super::PropertyChecker;
14
15impl PropertyChecker {
16    pub(super) fn check_valid_num<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
17        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
18    {
19        if let Some(PropertyArg::Predicates(predicates)) = property.args().first() {
20            if self.all_predicates_are_slice_size_invariant(vm_state, checkpoint, predicates) {
21                return CheckResult::Proved;
22            }
23            for pred in predicates {
24                if let Some(r) = self.eval_numeric_predicate(vm_state, solver, Some(checkpoint), pred) {
25                    if !matches!(r, CheckResult::Proved) {
26                        return r;
27                    }
28                }
29            }
30            return CheckResult::Proved;
31        }
32        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
33        let ty = property.args().get(1).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
34        if let Some(ty) = ty {
35            let size_bits = vm_state.size_of_ty(ty) * 8;
36            if size_bits > 0 && size_bits < 128 {
37                if let TyKind::Int(_) = ty.kind() {
38                    let half = 1u128 << (size_bits - 1);
39                    let min = -(half as i128);
40                    let max = (half - 1) as i128;
41                    solver.push();
42                    let below = value.term.lt(&Int::from_i64(vm_state.ctx, min as i64));
43                    let above = value.term.gt(&Int::from_i64(vm_state.ctx, max as i64));
44                    solver.assert(&Bool::or(vm_state.ctx, &[&below, &above]));
45                    let r = match solver.check() {
46                        SatResult::Unsat => CheckResult::Proved,
47                        SatResult::Sat => CheckResult::Failed,
48                        _ => CheckResult::Unknown,
49                    };
50                    solver.pop(1);
51                    return r;
52                }
53                let max = Int::from_u64(vm_state.ctx, ((1u128 << size_bits) - 1).min(u64::MAX as u128) as u64);
54                solver.push();
55                solver.assert(&value.term.gt(&max));
56                let r = match solver.check() { SatResult::Unsat => CheckResult::Proved, SatResult::Sat => CheckResult::Failed, _ => CheckResult::Unknown };
57                solver.pop(1);
58                return r;
59            }
60            return CheckResult::Proved;
61        }
62        CheckResult::Proved
63    }
64
65    pub(super) fn eval_numeric_predicate<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
66        checkpoint: Option<&Checkpoint<'tcx>>,
67        pred: &crate::verify::contract::NumericPredicate<'tcx>) -> Option<CheckResult>
68    {
69        let lhs = self.eval_contract_expr(vm_state, checkpoint, &pred.lhs)?;
70        let rhs = self.eval_contract_expr(vm_state, checkpoint, &pred.rhs)?;
71        let condition = match pred.op {
72            RelOp::Le => lhs.le(&rhs),
73            RelOp::Lt => lhs.lt(&rhs),
74            RelOp::Ge => lhs.ge(&rhs),
75            RelOp::Gt => lhs.gt(&rhs),
76            RelOp::Eq => lhs._eq(&rhs),
77            RelOp::Ne => lhs._eq(&rhs).not(),
78        };
79        solver.push();
80        vm_state.assert_all(solver);
81        // Bridge the iter_ptr_offset (tracked by post_inc_start) to the
82        // predicate's LHS (typically the loop counter `i` in position).
83        // At the assert_unchecked(i < n) point, tracked_offset == i + 1
84        // because post_inc_start(1) was just called before the check.
85        for (_, off) in vm_state.iter_ptr_offset.iter() {
86            let one = Int::from_u64(vm_state.ctx, 1);
87            solver.assert(&off._eq(&Int::add(vm_state.ctx, &[&lhs, &one])));
88        }
89        // For Iter/IterMut Le predicates with rhs computed from fields,
90        // inject a lower-bound: the field-based len is >= 1 when the
91        // struct's entry contract contains !self.is_empty().
92        // Without this, Z3 cannot deduce (end-ptr)/sz >= 1 from != 0.
93        if matches!(pred.op, RelOp::Le) {
94            if let Some(term) = self.try_get_iter_len_term(vm_state, &pred.rhs) {
95                if let Some(one) = lhs.as_u64().or(rhs.as_u64()) {
96                    if one == 1 {
97                        let one_term = Int::from_u64(vm_state.ctx, 1);
98                        solver.assert(&term.ge(&one_term));
99                    }
100                }
101            }
102        }
103        // NIA helper: inject Euclidean division identity for div operands
104        // to help Z3 prove (X/N)*N <= X via X = (X/N)*N + X%N, X%N >= 0.
105        self.inject_nia_axioms(vm_state, solver, checkpoint, &pred.lhs);
106        self.inject_nia_axioms(vm_state, solver, checkpoint, &pred.rhs);
107        // Walk VM binary op sources for Div/Rem terms used in the
108        // predicate — these are not visible in the ContractExpr tree.
109        self.inject_vm_div_axioms(vm_state, solver, &pred.lhs);
110        self.inject_vm_div_axioms(vm_state, solver, &pred.rhs);
111        // For Ne(pred != 0): assert path conditions so that layout
112        // constants (e.g. align_of >= 1) constrain the solver,
113        // while regular parameters remain unconstrained.
114        if matches!(pred.op, RelOp::Ne) && rhs.as_u64() == Some(0) {
115            // Concrete 0 from compiler-evaluated AlignOf/SizeOf for
116            // generic types — semantically always >= 1 for non-ZST.
117            if lhs.as_u64() == Some(0) {
118                return Some(CheckResult::Proved);
119            }
120            vm_state.assert_all(solver);
121        }
122        solver.assert(&condition.not());
123        let r0 = solver.check();
124        let mut r = match r0 { SatResult::Unsat => Some(CheckResult::Proved), SatResult::Sat => Some(CheckResult::Failed), _ => None };
125        // If Le/Ge check failed, inject a path-condition-level NIA axiom
126        // based on the VM's binary op sources and retry.
127        if matches!(r, Some(CheckResult::Failed)) && matches!(pred.op, RelOp::Le | RelOp::Ge | RelOp::Lt | RelOp::Gt) {
128            solver.pop(1);
129            solver.push();
130            vm_state.assert_all(solver);
131            self.inject_nia_axioms(vm_state, solver, checkpoint, &pred.lhs);
132            self.inject_nia_axioms(vm_state, solver, checkpoint, &pred.rhs);
133            self.inject_vm_div_axioms(vm_state, solver, &pred.lhs);
134            self.inject_vm_div_axioms(vm_state, solver, &pred.rhs);
135            solver.assert(&condition.not());
136            r = match solver.check() { SatResult::Unsat => Some(CheckResult::Proved), SatResult::Sat => Some(CheckResult::Failed), _ => r };
137        }
138        solver.pop(1);
139        r
140    }
141
142    pub(super) fn inject_nia_axioms<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
143        solver: &Solver<'ctx>, checkpoint: Option<&Checkpoint<'tcx>>,
144        expr: &ContractExpr<'tcx>)
145    {
146        match expr {
147            ContractExpr::Binary { op: NumericOp::Div, lhs, rhs } => {
148                if let (Some(l), Some(r)) = (
149                    self.eval_contract_expr(vm_state, checkpoint, lhs),
150                    self.eval_contract_expr(vm_state, checkpoint, rhs),
151                ) {
152                    let zero = Int::from_u64(vm_state.ctx, 0);
153                    let mul_term = Int::mul(vm_state.ctx, &[&l.div(&r), &r]);
154                    let rem_term = l.rem(&r);
155                    let sum_term = Int::add(vm_state.ctx, &[&mul_term, &rem_term]);
156                    solver.assert(&l._eq(&sum_term));
157                    solver.assert(&rem_term.ge(&zero));
158                }
159            }
160            ContractExpr::Binary { op: NumericOp::Mul, lhs, rhs } => {
161                // Recurse into mul operands in case one is a div
162                self.inject_nia_axioms(vm_state, solver, checkpoint, lhs);
163                self.inject_nia_axioms(vm_state, solver, checkpoint, rhs);
164            }
165            ContractExpr::Binary { lhs, rhs, .. } => {
166                self.inject_nia_axioms(vm_state, solver, checkpoint, lhs);
167                self.inject_nia_axioms(vm_state, solver, checkpoint, rhs);
168            }
169            ContractExpr::Unary { expr: inner, .. } => {
170                self.inject_nia_axioms(vm_state, solver, checkpoint, inner);
171            }
172            _ => {}
173        }
174    }
175
176    pub(super) fn inject_vm_div_axioms<'ctx, 'tcx>(&self,
177        vm_state: &VmState<'ctx, 'tcx>,
178        solver: &Solver<'ctx>,
179        expr: &ContractExpr<'tcx>,
180    ) {
181        let Some(val) = self.eval_contract_expr(vm_state, None, expr) else { return };
182        self.inject_div_axioms_for_term(vm_state, solver, &val, 4);
183    }
184
185    pub(super) fn inject_div_axioms_for_term<'ctx, 'tcx>(&self,
186        vm_state: &VmState<'ctx, 'tcx>,
187        solver: &Solver<'ctx>,
188        target: &Int<'ctx>,
189        depth: usize,
190    ) {
191        if depth == 0 { return; }
192
193        // Walk both binary_op_sources (Add, Sub, Div, etc.) and
194        // other_op_sources (select_unpredictable) for destinations
195        // whose term matches target.
196        let op_sources: Vec<&(Option<PlaceKey>, Option<PlaceKey>)> = {
197            let mut src: Vec<&(Option<PlaceKey>, Option<PlaceKey>)> = Vec::new();
198            for (pk, pair) in vm_state.binary_op_sources.iter() {
199                if pk.local().and_then(|l| vm_state.local_value(l))
200                    .map(|v| v.term == *target).unwrap_or(false)
201                {
202                    src.push(pair);
203                }
204            }
205            for (pk, pair) in vm_state.other_op_sources.iter() {
206                if pk.local().and_then(|l| vm_state.local_value(l))
207                    .map(|v| v.term == *target).unwrap_or(false)
208                {
209                    src.push(pair);
210                }
211            }
212            src
213        };
214
215        let mut already_seen = FxHashSet::default();
216
217        // ── Also recurse through Use / Cast chains: search ALL locals
218        // whose term equals target, and for each binary/other-op entry
219        // that *consumes* that local as an operand, walk the destination.
220        for local_idx in 0..vm_state.body.local_decls.len() {
221            let local = rustc_middle::mir::Local::from_usize(local_idx);
222            let Some(val) = vm_state.local_value(local) else { continue };
223            if val.term != *target { continue }
224
225            for (pk, (lhs, rhs)) in vm_state.binary_op_sources.iter()
226                .chain(vm_state.other_op_sources.iter())
227            {
228                if let Some(dest_local) = pk.local() {
229                    if let Some(dest_val) = vm_state.local_value(dest_local) {
230                        let lhs_local = lhs.as_ref().and_then(|pk| pk.local());
231                        let rhs_local = rhs.as_ref().and_then(|pk| pk.local());
232                        if (lhs_local == Some(local) || rhs_local == Some(local))
233                            && !already_seen.contains(&dest_val.term)
234                        {
235                            already_seen.insert(dest_val.term.clone());
236                            self.inject_div_axioms_for_term(
237                                vm_state, solver, &dest_val.term, depth - 1,
238                            );
239                        }
240                    }
241                }
242            }
243        }
244
245        // ── Process direct matches (both binary and other sources) ──
246        for (lhs_pk, rhs_pk) in &op_sources {
247            let (Some(lhs_pk), Some(rhs_pk)) = (lhs_pk, rhs_pk) else { continue };
248            let (Some(lhs_local), Some(rhs_local)) = (lhs_pk.local(), rhs_pk.local()) else { continue };
249            let (Some(lhs_val), Some(rhs_val)) = (vm_state.local_value(lhs_local), vm_state.local_value(rhs_local)) else { continue };
250
251            // Check if lhs is itself a Div / Rem result
252            if let Some((div_lhs_pk, div_rhs_pk)) = vm_state.binary_op_sources.get(lhs_pk).cloned() {
253                let Some(div_lhs_local) = div_lhs_pk.and_then(|pk| pk.local()) else { continue };
254                let Some(div_rhs_local) = div_rhs_pk.and_then(|pk| pk.local()) else { continue };
255                let Some(div_lhs_val) = vm_state.local_value(div_lhs_local) else { continue };
256                let Some(div_rhs_val) = vm_state.local_value(div_rhs_local) else { continue };
257
258                let quot = div_lhs_val.term.div(&div_rhs_val.term);
259                let rem = div_lhs_val.term.rem(&div_rhs_val.term);
260                let mul_term = Int::mul(vm_state.ctx, &[&quot, &div_rhs_val.term]);
261                let sum_term = Int::add(vm_state.ctx, &[&mul_term, &rem]);
262                solver.assert(&div_lhs_val.term._eq(&sum_term));
263                let zero = Int::from_u64(vm_state.ctx, 0);
264                solver.assert(&rem.ge(&zero));
265                solver.assert(&mul_term.le(&div_lhs_val.term));
266            }
267
268            // Recurse into operands
269            self.inject_div_axioms_for_term(vm_state, solver, &lhs_val.term, depth - 1);
270            self.inject_div_axioms_for_term(vm_state, solver, &rhs_val.term, depth - 1);
271        }
272    }
273
274    pub(super) fn try_get_iter_len_term<'ctx, 'tcx>(
275        &self,
276        vm_state: &VmState<'ctx, 'tcx>,
277        expr: &ContractExpr<'tcx>,
278    ) -> Option<Int<'ctx>> {
279        let ContractExpr::Len(_) = expr else { return None };
280        for (_, val) in vm_state.locals.iter() {
281            let is_iter = match val.ty.kind() {
282                TyKind::Ref(_, pointee, _) => match pointee.kind() {
283                    TyKind::Adt(adt_def, _) => {
284                        let name = vm_state.tcx.def_path_str(adt_def.did());
285                        name.ends_with("::Iter") || name == "Iter"
286                            || name.ends_with("::IterMut") || name == "IterMut"
287                    }
288                    _ => false,
289                },
290                _ => false,
291            };
292            if !is_iter { continue; }
293            let alloc_id = val.provenance_alloc_id()?;
294            for (&l, lv) in vm_state.locals.iter() {
295                if lv.provenance_alloc_id() != Some(alloc_id) { continue; }
296                if let (Some(ptr), Some(end)) =
297                    (vm_state.field_value(l, &[0]), vm_state.field_value(l, &[1]))
298                {
299                    if let (Some(pp), Some(ep)) = (&ptr.provenance, &end.provenance) {
300                        if pp.alloc_id == ep.alloc_id {
301                            let elem_ty = match ptr.ty.kind() {
302                                TyKind::Adt(_, substs) => substs.first().and_then(|s| s.as_type()),
303                                _ => None,
304                            };
305                            let elem_size = elem_ty.map(|t| vm_state.size_of_ty(t).max(1)).unwrap_or(1) as u64;
306                            let diff = Int::sub(vm_state.ctx, &[&ep.offset, &pp.offset]);
307                            let sz = Int::from_u64(vm_state.ctx, elem_size);
308                            return Some(diff.div(&sz));
309                        }
310                    }
311                }
312            }
313        }
314        None
315    }
316
317    pub(super) fn try_iter_len_from_fields<'ctx, 'tcx>(
318        &self,
319        vm_state: &VmState<'ctx, 'tcx>,
320        checkpoint: &Checkpoint<'tcx>,
321        expr: &ContractExpr<'tcx>,
322    ) -> Option<Int<'ctx>> {
323        use rustc_middle::mir::Place;
324        let ContractExpr::Place(cp) = expr else { return None };
325        let op: &Operand<'tcx> = match cp.base {
326            PlaceBase::Arg(n) => checkpoint.args.get(n)?,
327            PlaceBase::Local(n) => {
328                let callee = checkpoint.callee?;
329                let idx = crate::helpers::mir_utils::callee_param_index_for_local(
330                    vm_state.tcx, callee, n)?;
331                checkpoint.args.get(idx)?
332            }
333            _ => return None,
334        };
335        let place: &Place<'tcx> = match op {
336            Operand::Copy(p) | Operand::Move(p) => p,
337            _ => return None,
338        };
339        let local = place.local;
340        let local_val = vm_state.locals.get(&local)?;
341        let is_iter = match local_val.ty.kind() {
342            TyKind::Ref(_, pointee, _) => match pointee.kind() {
343                TyKind::Adt(adt_def, _) => {
344                    let name = vm_state.tcx.def_path_str(adt_def.did());
345                    name.ends_with("::Iter") || name == "Iter"
346                        || name.ends_with("::IterMut") || name == "IterMut"
347                }
348                _ => false,
349            },
350            _ => false,
351        };
352        if !is_iter { return None; }
353        // Direct lookup first, then scan by alloc_id for temp copies.
354        if let (Some(ptr), Some(end)) =
355            (vm_state.field_value(local, &[0]), vm_state.field_value(local, &[1]))
356        {
357            if let (Some(pp), Some(ep)) = (&ptr.provenance, &end.provenance) {
358                if pp.alloc_id == ep.alloc_id {
359                    let diff = Int::sub(vm_state.ctx, &[&ep.offset, &pp.offset]);
360                    let sz = Int::from_u64(vm_state.ctx, vm_state.iter_elem_size(ptr));
361                    return Some(diff.div(&sz));
362                }
363            }
364        }
365        // Fallback: scan all locals for one with same struct alloc.
366        let target_alloc = local_val.provenance_alloc_id()?;
367        for (&scan_local, scan_val) in vm_state.locals.iter() {
368            if scan_val.provenance_alloc_id() != Some(target_alloc) { continue; }
369            if let (Some(ptr), Some(end)) =
370                (vm_state.field_value(scan_local, &[0]), vm_state.field_value(scan_local, &[1]))
371            {
372                if let (Some(pp), Some(ep)) = (&ptr.provenance, &end.provenance) {
373                    if pp.alloc_id == ep.alloc_id {
374                        let diff = Int::sub(vm_state.ctx, &[&ep.offset, &pp.offset]);
375                        let sz = Int::from_u64(vm_state.ctx, vm_state.iter_elem_size(ptr));
376                        return Some(diff.div(&sz));
377                    }
378                }
379            }
380        }
381        None
382    }
383}
rapx/verify/property_checker/numeric.rs

rapx/verify/property_checker/
numeric.rs
