rapx/verify/property_checker/
bounds.rs

1use rustc_middle::mir::{Local, Operand, Rvalue, StatementKind};
2use rustc_middle::ty::{Ty, TyKind};
3#[cfg(not(rapx_has_skip_norm_wip))]
4use crate::compat::SkipNormWip;
5use z3::{SatResult, Solver, ast::{Ast, Bool, Int}};
6use crate::verify::contract::{ContractExpr, NumericOp, PlaceBase, Property, PropertyArg, RelOp};
7use crate::verify::report::CheckResult;
8use crate::helpers::mir_scan::Checkpoint;
9use crate::verify::vm::state::{VmState, VmValue};
10
11use super::PropertyChecker;
12
13impl PropertyChecker {
14    pub(super) fn check_in_bound<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
15        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
16    {
17        // Fast-path: if a prior ChecksIndexBoundsDisjoint call already
18        // validated bounds for this function, the InBound holds.
19        if vm_state.contract_flags.has_checked_bounds {
20            return CheckResult::Proved;
21        }
22        // Fast-path: contract with for_each guarantees all elements
23        // of the index array are in bounds.
24        if property.for_each().is_some() {
25            return CheckResult::Proved;
26        }
27
28        if let Some(PropertyArg::Expr(ContractExpr::IndexAccess { index: _, .. }))
29            = property.args().first()
30        {
31            return self.check_in_bound_slice(vm_state, solver, checkpoint, property);
32        }
33
34        let required_ty = property.args().get(1)
35            .and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
36        if self.zst_guard(vm_state, checkpoint, property) {
37            return CheckResult::Proved;
38        }
39
40        let Some(value) = self.target_value(vm_state, checkpoint, property) else {
41            return CheckResult::Unknown;
42        };
43        if matches!(value.ty.kind(), TyKind::Ref(..)) {
44            return CheckResult::Proved;
45        }
46        if value.provenance.is_some() {
47            if let TyKind::Adt(adt_def, _) = value.ty.kind() {
48                let path = vm_state.tcx.def_path_str(adt_def.did());
49                if path.contains("::NonNull") {
50                    return CheckResult::Proved;
51                }
52            }
53        }
54        if value.invariants.in_bounds {
55            return CheckResult::Proved;
56        }
57        // `byte_add(offset_of!(Container, field))` always keeps the pointer
58        // within the container allocation, because the byte offset of a field
59        // never exceeds `size_of::<Container>()`.  This covers patterns such
60        // as `Option::as_slice`.
61        if self.count_is_offset_of(vm_state, checkpoint, property, &value) {
62            return CheckResult::Proved;
63        }
64        // When the contract expression for the element count evaluates to
65        // zero (e.g. div-by-sizeof for ZST generic params), the byte-level
66        // access is zero and limits checking is trivial.
67        let count_term = property.args().get(2)
68            .and_then(|a| self.resolve_arg_term(vm_state, checkpoint, a));
69        if let Some(ref ct) = count_term {
70            if ct.as_u64() == Some(0) {
71                return CheckResult::Proved;
72            }
73        }
74        let access = self.access_bytes(vm_state, property, 1, 2, checkpoint, &value);
75        let Some(alloc_id) = value.provenance_alloc_id() else {
76            return CheckResult::Unknown;
77        };
78        let (Some(base), Some(size)) = (vm_state.allocation_base(alloc_id).cloned(), vm_state.allocation_size(alloc_id).cloned()) else {
79            return CheckResult::Unknown;
80        };
81
82        let alloc = vm_state.alloc(alloc_id);
83        if let (Some(alloc_elem_ty), Some(req_ty)) = (alloc.element_ty, required_ty) {
84            if self.alloc_elem_is_array_of(alloc_elem_ty, req_ty) {
85                return CheckResult::Proved;
86            }
87        }
88
89        // External allocations have unbounded size.
90        if vm_state.alloc(alloc_id).is_external {
91            return CheckResult::Proved;
92        }
93
94        let alloc_elem_is_generic = vm_state.alloc(alloc_id)
95            .element_ty.map_or(false, |ty| matches!(ty.kind(), TyKind::Param(_)));
96        let fallback_for_generic = alloc_elem_is_generic && !size.as_u64().is_some() && !access.as_u64().is_some();
97
98        solver.push();
99        let bound = Int::add(vm_state.ctx, &[&base, &size]);
100        let covered = Int::add(vm_state.ctx, &[&value.term, &access]);
101        // A field-offset provenance (`offset_of!`) is always within the
102        // container together with the accessed range: the field plus its own
103        // size fits inside the container.  Assert this layout fact so the
104        // in-bounds check below can be discharged.
105        if value.provenance.as_ref().is_some_and(|prov| prov.is_field_offset) {
106            let prov = value.provenance.as_ref().unwrap();
107            let zero = Int::from_u64(vm_state.ctx, 0);
108            solver.assert(&prov.offset.ge(&zero));
109            solver.assert(&Int::add(vm_state.ctx, &[&prov.offset, &access]).le(&size));
110        }
111        // Upper bound: value + access > base + size
112        let above_negated = covered.le(&bound).not();
113        // Lower bound: value < base (pointer below allocation start)
114        let below_negated = value.term.lt(&base);
115        solver.assert(&z3::ast::Bool::or(vm_state.ctx, &[&above_negated, &below_negated]));
116        let sat_result = solver.check();
117        let r = match sat_result {
118            SatResult::Unsat => CheckResult::Proved,
119            SatResult::Sat if fallback_for_generic => CheckResult::Unknown,
120            SatResult::Sat => CheckResult::Failed,
121            _ => CheckResult::Unknown,
122        };
123        solver.pop(1);
124        r
125    }
126
127    pub(super) fn count_is_offset_of<'ctx, 'tcx>(
128        &self,
129        vm_state: &VmState<'ctx, 'tcx>,
130        checkpoint: &Checkpoint<'tcx>,
131        property: &Property<'tcx>,
132        value: &VmValue<'ctx, 'tcx>,
133    ) -> bool {
134        let Some(count_arg) = property.args().get(2) else {
135            return false;
136        };
137        let PropertyArg::Expr(ContractExpr::Place(cp)) = count_arg else {
138            return false;
139        };
140        let PlaceBase::Arg(n) = cp.base else {
141            return false;
142        };
143        let Some(operand) = checkpoint.args.get(n) else {
144            return false;
145        };
146        let Operand::Constant(c) = operand else {
147            return false;
148        };
149        let Some(container) = crate::helpers::mir_utils::offset_of_container(vm_state.tcx, &c.const_)
150        else {
151            return false;
152        };
153        // The pointer must be the base of its allocation (offset 0), otherwise
154        // adding the field offset could overflow the container end.
155        let at_base = value
156            .provenance
157            .as_ref()
158            .is_some_and(|p| p.offset.as_u64() == Some(0));
159        if !at_base {
160            return false;
161        }
162        // The allocation must be the same container the offset was computed on.
163        crate::helpers::mir_utils::pointee_ty(value.ty)
164            .is_some_and(|pointee| pointee == container)
165    }
166
167    pub(super) fn resolve_index_access_args(
168        property: &Property<'_>,
169    ) -> (Option<usize>, Option<usize>) {
170        if let Some(PropertyArg::Expr(ContractExpr::IndexAccess { slice, index })) = property.args().first() {
171            let slice_idx = Self::extract_place_arg_index(slice);
172            let index_idx = Self::extract_place_arg_index(index);
173            (slice_idx, index_idx)
174        } else {
175            (Some(0), Some(1))
176        }
177    }
178
179    pub(super) fn extract_place_arg_index(expr: &ContractExpr<'_>) -> Option<usize> {
180        match expr {
181            ContractExpr::Place(cp) => match cp.base {
182                PlaceBase::Arg(n) => Some(n),
183                _ => None,
184            },
185            _ => None,
186        }
187    }
188
189    pub(super) fn check_in_bound_slice<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
190        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
191    {
192        let (slice_arg_idx, index_arg_idx) = Self::resolve_index_access_args(property);
193
194        let slice_val = match slice_arg_idx.and_then(|idx| checkpoint.args.get(idx)) {
195            Some(op) => vm_state.value_of_operand(op),
196            None => return CheckResult::Unknown,
197        };
198        if slice_val.invariants.in_bounds {
199            return CheckResult::Proved;
200        }
201
202        let (index_val, is_range) = match index_arg_idx.and_then(|idx| checkpoint.args.get(idx)) {
203            Some(op) => {
204                if let Some(end_val) = self.extract_range_end(vm_state, op, checkpoint) {
205                    (end_val, true)
206                } else {
207                    (vm_state.value_of_operand(op), false)
208                }
209            }
210            None => return CheckResult::Unknown,
211        };
212
213        let data_alloc_id = slice_val.provenance_alloc_id();
214        let Some(data_alloc_id) = data_alloc_id else { return CheckResult::Unknown };
215
216        let Some(size) = vm_state.allocation_size(data_alloc_id).cloned() else { return CheckResult::Unknown };
217
218        let elem_size = vm_state.alloc(data_alloc_id)
219            .element_ty
220            .map(|ty| vm_state.size_of_ty(ty) as u64)
221            .unwrap_or(1)
222            .max(1);
223
224        let elem_sz = Int::from_u64(vm_state.ctx, elem_size);
225        let len = size.div(&elem_sz);
226
227        solver.push();
228        // Assert accumulated path conditions (e.g. the loop-carried
229        // `initialized < N` guard that makes `idx < N` hold at this call site)
230        // so the bound check below can be discharged symbolically.
231        for cond in &vm_state.path_conditions {
232            solver.assert(cond);
233        }
234        let negated = if is_range {
235            // For range-based InBound (start..end), check end <= len
236            index_val.term.le(&len).not()
237        } else {
238            // For single-element InBound (index), check index + 1 <= len
239            let one = Int::from_u64(vm_state.ctx, 1);
240            let index_plus_one = Int::add(vm_state.ctx, &[&index_val.term, &one]);
241            index_plus_one.le(&len).not()
242        };
243        solver.assert(&negated);
244        let r = match solver.check() { SatResult::Unsat => CheckResult::Proved, SatResult::Sat => CheckResult::Failed, _ => CheckResult::Unknown };
245        solver.pop(1);
246        r
247    }
248
249    pub(super) fn extract_range_end<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>,
250        op: &Operand<'tcx>, _checkpoint: &Checkpoint<'tcx>) -> Option<VmValue<'ctx, 'tcx>>
251    {
252        let place = match op {
253            Operand::Copy(p) | Operand::Move(p) => p,
254            _ => return None,
255        };
256        if !place.projection.is_empty() { return None; }
257        let range_local = place.local;
258        let ty = vm_state.body.local_decls[range_local].ty;
259        let is_range = format!("{:?}", ty.kind()).contains("Range");
260        if !is_range { return None; }
261        for block in vm_state.body.basic_blocks.iter() {
262            for stmt in &block.statements {
263                if let StatementKind::Assign(assign) = &stmt.kind {
264                    let (dest, rvalue) = &**assign;
265                    if dest.local == range_local && dest.projection.is_empty() {
266                        if let Rvalue::Aggregate(_kind, operands) = rvalue {
267                            let end_idx = rustc_abi::FieldIdx::from_usize(1);
268                            if let Some(end_op) = operands.get(end_idx) {
269                                return Some(self.trace_value(vm_state, end_op));
270                            }
271                        }
272                    }
273                }
274            }
275        }
276        None
277    }
278
279    pub(super) fn check_non_overlap<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
280        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
281    {
282        let Some(v1) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
283        // Get the second pointer from the property args (not from checkpoint directly).
284        // The property may reference the two pointers in any order (e.g. dst at args[0]).
285        let v2 = property.args().get(1)
286            .and_then(|a| {
287                let cp = match a {
288                    PropertyArg::Expr(ContractExpr::Place(cp)) => cp.clone(),
289                    _ => return None,
290                };
291                match cp.base {
292                    PlaceBase::Arg(n) => checkpoint.args.get(n).map(|op| vm_state.value_of_operand(op)),
293                    PlaceBase::Local(n) => vm_state.local_value(Local::from_usize(n)).cloned(),
294                    _ => None,
295                }
296            })
297            .or_else(|| checkpoint.args.get(1).map(|op| vm_state.value_of_operand(op)));
298        let Some(v2) = v2 else {
299            if v1.provenance.is_some() { return CheckResult::Proved; }
300            return CheckResult::Unknown;
301        };
302        if v1.provenance_alloc_id() != v2.provenance_alloc_id() { return CheckResult::Proved; }
303
304        // Try range-based overlap detection when count and element size are available.
305        if let Some(count_term) = checkpoint.args.get(2).map(|op| vm_state.value_of_operand(op).term) {
306            // Use the pointee element size from either pointer type.
307            let elem_size = vm_state.pointee_elem_size(v1.ty).max(vm_state.pointee_elem_size(v2.ty)).max(1) as u64;
308            let _elem_size_term = Int::from_u64(vm_state.ctx, elem_size);
309            if let Some(count) = count_term.simplify().as_u64() {
310                let range = Int::from_u64(vm_state.ctx, elem_size * count.max(1));
311                let src_end = Int::add(vm_state.ctx, &[&v1.term, &range]);
312                let dst_end = Int::add(vm_state.ctx, &[&v2.term, &range]);
313                solver.push();
314                let overlap = Bool::and(vm_state.ctx, &[
315                    &v1.term.lt(&dst_end),
316                    &v2.term.lt(&src_end),
317                ]);
318                solver.assert(&overlap);
319                let r = match solver.check() {
320                    SatResult::Unsat => CheckResult::Proved,
321                    SatResult::Sat => CheckResult::Failed,
322                    _ => CheckResult::Unknown,
323                };
324                solver.pop(1);
325                return r;
326            }
327        }
328
329        // Fallback: check pointer-distinctness.
330        solver.push();
331        let ne = v1.term._eq(&v2.term).not();
332        solver.assert(&ne);
333        let r = match solver.check() { SatResult::Unsat => CheckResult::Proved, SatResult::Sat => CheckResult::Failed, _ => CheckResult::Unknown };
334        solver.pop(1);
335        r
336    }
337
338    pub(super) fn all_predicates_are_slice_size_invariant<'ctx, 'tcx>(&self,
339        vm_state: &VmState<'ctx, 'tcx>,
340        checkpoint: &Checkpoint<'tcx>,
341        predicates: &[crate::verify::contract::NumericPredicate<'tcx>],
342    ) -> bool {
343        !predicates.is_empty() && predicates.iter().all(|p| {
344            self.predicate_is_slice_size_invariant(vm_state, checkpoint, p)
345        })
346    }
347
348    pub(super) fn predicate_is_slice_size_invariant<'ctx, 'tcx>(&self,
349        vm_state: &VmState<'ctx, 'tcx>,
350        checkpoint: &Checkpoint<'tcx>,
351        pred: &crate::verify::contract::NumericPredicate<'tcx>,
352    ) -> bool {
353        if !matches!(pred.op, RelOp::Le | RelOp::Lt) {
354            return false;
355        }
356        // rhs must be >= isize::MAX (the language invaraint bound)
357        let ContractExpr::Const(bound) = &pred.rhs else { return false };
358        if *bound < i64::MAX as u128 {
359            return false;
360        }
361        // lhs must be size_of(T) * count
362        let ContractExpr::Binary { op: NumericOp::Mul, lhs, rhs } = &pred.lhs else {
363            return false;
364        };
365        let (size_ty, count_expr) = match (lhs.as_ref(), rhs.as_ref()) {
366            (ContractExpr::SizeOf(ty), count) => (*ty, count),
367            (count, ContractExpr::SizeOf(ty)) => (*ty, count),
368            _ => return false,
369        };
370        // Resolve SizeOf type via callsite substitutions
371        let resolved_ty = self.instantiate_callsite_ty(vm_state, checkpoint, size_ty);
372        // count must be a Place referencing a callsite arg
373        self.count_derives_from_slice_param(vm_state, checkpoint, count_expr, resolved_ty)
374    }
375
376    pub(super) fn count_derives_from_slice_param<'ctx, 'tcx>(&self,
377        vm_state: &VmState<'ctx, 'tcx>,
378        checkpoint: &Checkpoint<'tcx>,
379        count_expr: &ContractExpr<'tcx>,
380        elem_ty: Ty<'tcx>,
381    ) -> bool {
382        // Must be a Place, not a constant literal
383        let ContractExpr::Place(cp) = count_expr else { return false };
384        if !cp.projections.is_empty() { return false; }
385        let Some(local) = cp.local_base() else { return false };
386        if local == 0 { return false; }
387        let Some(callee) = checkpoint.callee else { return false };
388        let Some(arg_idx) = crate::helpers::mir_utils::callee_param_index_for_local(
389            vm_state.tcx, callee, local) else { return false };
390        // Reject constant literal arguments (like usize::MAX)
391        if matches!(checkpoint.args.get(arg_idx), Some(Operand::Constant(_))) {
392            return false;
393        }
394        // Check caller has a matching slice reference parameter.
395        let body = vm_state.body;
396        let has_slice_param = (1..=body.arg_count).any(|i| {
397            let param_ty = body.local_decls[Local::from_usize(i)].ty;
398            self.is_slice_ref_with_elem(param_ty, elem_ty, vm_state, checkpoint)
399        });
400        if has_slice_param {
401            return true;
402        }
403        // No direct slice param — check if the pointer has provenance from
404        // an external allocation (raw pointer params get this in init_parameters).
405        if let Some(op) = checkpoint.args.first() {
406            let target_val = vm_state.value_of_operand(op);
407            if target_val.provenance.is_some() {
408                return true;
409            }
410        }
411        false
412    }
413
414    pub(super) fn is_slice_ref_with_elem<'ctx, 'tcx>(&self, ty: Ty<'tcx>, elem_ty: Ty<'tcx>,
415        vm_state: &VmState<'ctx, 'tcx>, checkpoint: &Checkpoint<'tcx>) -> bool
416    {
417        let rustc_middle::ty::TyKind::Ref(_, inner, _) = ty.kind() else { return false };
418        match inner.kind() {
419            rustc_middle::ty::TyKind::Slice(slice_elem) => {
420                let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, *slice_elem);
421                self.same_erased_ty(vm_state, resolved, elem_ty)
422            }
423            _ => false,
424        }
425    }
426
427    pub(super) fn same_erased_ty<'ctx, 'tcx>(&self,
428        vm_state: &VmState<'ctx, 'tcx>,
429        a: Ty<'tcx>, b: Ty<'tcx>,
430    ) -> bool {
431        vm_state.size_of_ty(a) > 0 && vm_state.size_of_ty(b) > 0
432            && vm_state.size_of_ty(a) == vm_state.size_of_ty(b)
433    }
434
435    pub(super) fn is_caller_type_param<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, ty: Ty<'tcx>) -> bool {
436        let rustc_middle::ty::TyKind::Param(param_ty) = ty.kind() else { return false };
437        let generics = vm_state.tcx.generics_of(vm_state.caller_def_id);
438        generics.own_params.iter().any(|p| {
439            matches!(p.kind, rustc_middle::ty::GenericParamDefKind::Type { .. })
440                && p.name == param_ty.name
441        })
442    }
443}
rapx/verify/property_checker/bounds.rs

rapx/verify/property_checker/
bounds.rs
