rapx/verify/property_checker/
memory.rs

1use rustc_middle::mir::{Local, Operand, Rvalue, StatementKind};
2use rustc_middle::ty::{GenericArgKind, TyKind};
3#[cfg(not(rapx_has_skip_norm_wip))]
4use crate::compat::SkipNormWip;
5use rustc_hash::FxHashSet;
6use z3::{SatResult, Solver, ast::{Ast, Int}};
7use crate::verify::contract::{Property, PropertyArg};
8use crate::verify::report::CheckResult;
9use crate::helpers::mir_scan::Checkpoint;
10use crate::verify::vm::state::{AllocId, VmState, VmValue};
11
12use super::PropertyChecker;
13
14impl PropertyChecker {
15    pub(super) fn check_align<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
16        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
17    {
18        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
19
20        if self.zst_guard(vm_state, checkpoint, property) { return CheckResult::Proved; }
21        if self.is_concrete_zst(vm_state, value.ty) { return CheckResult::Proved; }
22        let ty_arg = property.args().get(1).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
23        let align = ty_arg.map(|ty| vm_state.align_of_ty(ty)).unwrap_or(1);
24        let align = if align <= 1 {
25            ty_arg.and_then(|ty| {
26                let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, ty);
27                let resolved_align = vm_state.align_of_ty(resolved);
28                if resolved_align > 1 {
29                    Some(resolved_align)
30                } else {
31                    let min_a = crate::helpers::mir_utils::min_align_of_generic_param(vm_state.tcx, vm_state.caller_def_id, resolved);
32                    if min_a > 1 { Some(min_a) } else { None }
33                }
34            }).unwrap_or(align)
35        } else {
36            align
37        };
38        if align <= 1 { return CheckResult::Proved; }
39        // Check allocation base alignment with concrete offset
40        if let Some(ref prov) = value.provenance {
41            let alloc = vm_state.alloc(prov.alloc_id);
42            let off_u64 = prov.offset.as_u64()
43                .or_else(|| prov.offset.simplify().as_u64());
44            if let Some(off) = off_u64 {
45                if alloc.align >= align {
46                    if off % align == 0 {
47                        return CheckResult::Proved;
48                    }
49                    if off % align != 0 {
50                        return CheckResult::Failed;
51                    }
52                }
53            }
54        }
55        if value.invariants.aligned {
56            if let Some(known_align) = value.invariants.align_n {
57                if known_align >= align && known_align % align == 0 {
58                    return CheckResult::Proved;
59                }
60            }
61        } else if let Some(known_align) = value.invariants.align_n {
62            if known_align >= align && known_align % align == 0 {
63                return CheckResult::Proved;
64            }
65        }
66        // Packed-struct fast-path: if the allocation is less aligned than
67        // required, the concrete offset alone determines alignment.
68        if let Some(ref prov) = value.provenance {
69            let alloc = vm_state.alloc(prov.alloc_id);
70            if alloc.align < align {
71                if let Some(off) = prov.offset.as_u64() {
72                    if off % align != 0 {
73                        return CheckResult::Failed;
74                    }
75                }
76            }
77        }
78        let align_term = Int::from_u64(vm_state.ctx, align);
79        let zero = Int::from_u64(vm_state.ctx, 0);
80        let local = Solver::new(vm_state.ctx);
81        local.push();
82        if let Some(ref prov) = value.provenance {
83            let alloc = vm_state.alloc(prov.alloc_id);
84            local.assert(&value.term._eq(&Int::add(vm_state.ctx, &[&alloc.base, &prov.offset])));
85            local.assert(&alloc.base._eq(&zero).not());
86            local.assert(&alloc.base.ge(&zero));
87            if alloc.align > 1 {
88                let a = Int::from_u64(vm_state.ctx, alloc.align);
89                local.assert(&alloc.base.rem(&a)._eq(&zero));
90            }
91        }
92        if let Some(known_align) = value.invariants.align_n {
93            let n = Int::from_u64(vm_state.ctx, known_align);
94            local.assert(&value.term.rem(&n)._eq(&zero));
95        }
96        for cond in &vm_state.path_conditions {
97            local.assert(cond);
98        }
99        let negated = value.term.rem(&align_term)._eq(&zero).not();
100        local.assert(&negated);
101        let r = match local.check() {
102            z3::SatResult::Sat => CheckResult::Failed,
103            z3::SatResult::Unsat => CheckResult::Proved,
104            z3::SatResult::Unknown => CheckResult::Unknown,
105        };
106        local.pop(1);
107        if matches!(r, CheckResult::Failed) {
108            rap_debug!("align=Failed vterm={} align_n={:?} aligned={} off={}",
109                value.term.to_string(), value.invariants.align_n, value.invariants.aligned,
110                value.provenance.as_ref().map(|p| p.offset.to_string()).unwrap_or_default());
111        }
112        r
113    }
114
115    pub(super) fn value_aligned_to<'ctx, 'tcx>(
116        vm_state: &VmState<'ctx, 'tcx>,
117        value: &VmValue<'ctx, 'tcx>,
118        align: u64,
119    ) -> bool {
120        if align <= 1 {
121            return true;
122        }
123        if let Some(n) = value.invariants.align_n {
124            if n >= align && n % align == 0 {
125                return true;
126            }
127        }
128        let solver = Solver::new(vm_state.ctx);
129        solver.push();
130        let zero = Int::from_u64(vm_state.ctx, 0);
131        if let Some(ref prov) = value.provenance {
132            let alloc = vm_state.alloc(prov.alloc_id);
133            solver.assert(&value.term._eq(&Int::add(vm_state.ctx, &[&alloc.base, &prov.offset])));
134            solver.assert(&alloc.base.ge(&zero));
135            if alloc.align > 1 {
136                let a = Int::from_u64(vm_state.ctx, alloc.align);
137                solver.assert(&alloc.base.rem(&a)._eq(&zero));
138            }
139        }
140        for cond in &vm_state.path_conditions {
141            solver.assert(cond);
142        }
143        let align_term = Int::from_u64(vm_state.ctx, align);
144        solver.assert(&value.term.rem(&align_term)._eq(&zero).not());
145        let r = solver.check() == SatResult::Unsat;
146        solver.pop(1);
147        r
148    }
149
150    pub(super) fn check_non_null<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, solver: &Solver<'ctx>,
151        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
152    {
153        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
154        if value.invariants.non_null { return CheckResult::Proved; }
155        if value.invariants.in_bounds { return CheckResult::Proved; }
156        // Pointers with non-external provenance point into known stack/heap
157        // allocations whose base addresses are never zero.  Raw-pointer
158        // parameters get external provenance which may be null.
159        if let Some(ref prov) = value.provenance {
160            if !vm_state.alloc(prov.alloc_id).is_external {
161                return CheckResult::Proved;
162            }
163        }
164        let zero = Int::from_u64(vm_state.ctx, 0);
165        self.smt_check(solver, &value.term._eq(&zero))
166    }
167
168    /// Whether `value` is a `MaybeUninit`-typed pointer access into `alloc_id`.
169    ///
170    /// `assume_init_drop` / `as_mut_ptr` (and friends) legitimately consume an
171    /// initialized element from storage that may be going out of scope, so the
172    /// `Init`/`Allocated` requirement concerns the write, not the allocation's
173    /// live/dead flag.
174    fn is_maybe_uninit_ptr<'ctx, 'tcx>(
175        vm_state: &VmState<'ctx, 'tcx>,
176        value: &VmValue<'ctx, 'tcx>,
177        alloc_id: AllocId,
178    ) -> bool {
179        value.invariants.init && value.invariants.non_null && value.invariants.aligned
180            && (matches!(value.ty.kind(), TyKind::RawPtr(..))
181                || matches!(value.ty.kind(), TyKind::Ref(_, inner, _)
182                    if matches!(inner.kind(), TyKind::Adt(adt, _)
183                        if vm_state.tcx.def_path_str(adt.did()).contains("::MaybeUninit"))))
184            && {
185                let a = vm_state.alloc(alloc_id);
186                !a.is_external && a.element_ty.map_or(false, |ty| {
187                    if let TyKind::Adt(adt, _) = ty.kind() {
188                        vm_state.tcx.def_path_str(adt.did()).contains("::MaybeUninit")
189                    } else { false }
190                })
191            }
192    }
193
194    pub(super) fn check_allocated<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
195        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
196    {
197        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
198
199        if self.zst_guard(vm_state, checkpoint, property) { return CheckResult::Proved; }
200        if self.is_concrete_zst(vm_state, value.ty) { return CheckResult::Proved; }
201
202        // Zero-element access (`Allocated(p, T, 0)`) is trivially satisfied:
203        // any pointer is valid for its 0-byte prefix, so this holds even when
204        // provenance has been lost through a cast.  Mirrors the `count == 0`
205        // fast-path in `check_in_bound` and covers `from_raw_parts(ptr, 0)`
206        // (e.g. `Option::as_slice` on `None`).
207        let count_term = property.args().get(2)
208            .and_then(|a| self.resolve_arg_term(vm_state, checkpoint, a));
209        if count_term.as_ref().is_some_and(|ct| ct.as_u64() == Some(0)) {
210            return CheckResult::Proved;
211        }
212
213        let Some(alloc_id) = value.provenance_alloc_id() else { return CheckResult::Unknown };
214
215        if vm_state.alloc(alloc_id).dead {
216            if !Self::is_maybe_uninit_ptr(vm_state, &value, alloc_id) {
217                let is_param_ref = vm_state.resolve_origin(&value)
218                    .map_or(false, |origin| {
219                        origin.local.as_usize() <= vm_state.body.arg_count
220                            && origin.local != Local::from_usize(0)
221                    });
222                if !is_param_ref {
223                    return CheckResult::Failed;
224                }
225            }
226        }
227
228        let required_ty = property.args().get(1)
229            .and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
230
231        let alloc = vm_state.alloc(alloc_id);
232        if let (Some(alloc_elem_ty), Some(req_ty)) = (alloc.element_ty, required_ty) {
233            if self.alloc_elem_is_array_of(alloc_elem_ty, req_ty) {
234                return CheckResult::Proved;
235            }
236            // Cross-type generic fast-path: when allocation element type
237            // and required type are both generic params (e.g. T vs U),
238            // sizes are opaque. If the pointer is derived from the same
239            // function's slice parameter, the byte-level layout is
240            // compatible by Rust's type system.
241            if matches!((alloc_elem_ty.kind(), req_ty.kind()),
242                (TyKind::Param(_), TyKind::Param(_))) {
243                return CheckResult::Proved;
244            }
245        }
246
247        let (Some(base), Some(size)) = (vm_state.allocation_base(alloc_id).cloned(), vm_state.allocation_size(alloc_id).cloned()) else {
248            return CheckResult::Unknown;
249        };
250
251        if vm_state.alloc(alloc_id).is_external {
252            return CheckResult::Proved;
253        }
254
255        let access = self.access_bytes(vm_state, property, 1, 2, checkpoint, &value);
256
257        // Concrete sizes: direct comparison.
258        if let (Some(size_val), Some(access_val)) = (size.as_u64(), access.as_u64()) {
259            if size_val < access_val {
260                return CheckResult::Failed;
261            }
262            return CheckResult::Proved;
263        }
264
265        // Generic element type: both size and access use max(1) fallback,
266        // making the check about element counts. When the pointer's offset
267        // cannot be determined concretely, the byte-level inequality
268        // "offset + count <= total_len" relies on facts (split_at, etc.)
269        // that may not be in path conditions. Fall back to Unknown rather
270        // than Failed for generic-element allocations.
271        let alloc_elem_is_generic = vm_state.alloc(alloc_id)
272            .element_ty.map_or(false, |ty| matches!(ty.kind(), TyKind::Param(_)));
273        if alloc_elem_is_generic && !size.as_u64().is_some() && !access.as_u64().is_some() {
274            return Self::allocation_covers_access(vm_state, &value, &access, &base, &size, CheckResult::Unknown);
275        }
276
277        Self::allocation_covers_access(vm_state, &value, &access, &base, &size, CheckResult::Failed)
278    }
279
280    /// Prove that `value + access` fits within `[base, base + size)`.
281    ///
282    /// `on_sat` is the result when the overflow is satisfiable: `Failed` for
283    /// concrete sizes, `Unknown` for generic-element allocations whose byte
284    /// layout cannot be resolved.
285    fn allocation_covers_access<'ctx, 'tcx>(
286        vm_state: &VmState<'ctx, 'tcx>,
287        value: &VmValue<'ctx, 'tcx>,
288        access: &Int<'ctx>,
289        base: &Int<'ctx>,
290        size: &Int<'ctx>,
291        on_sat: CheckResult,
292    ) -> CheckResult {
293        let solver = Solver::new(vm_state.ctx);
294        solver.push();
295        vm_state.assert_all(&solver);
296        let bound = Int::add(vm_state.ctx, &[base, size]);
297        let covered = Int::add(vm_state.ctx, &[&value.term, access]);
298        solver.assert(&covered.le(&bound).not());
299        let r = match solver.check() {
300            SatResult::Unsat => CheckResult::Proved,
301            SatResult::Sat => on_sat,
302            _ => CheckResult::Unknown,
303        };
304        solver.pop(1);
305        r
306    }
307
308    pub(super) fn check_init<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
309        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
310    {
311        if self.zst_guard(vm_state, checkpoint, property) { return CheckResult::Proved; }
312        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
313        if self.is_concrete_zst(vm_state, value.ty) { return CheckResult::Proved; }
314
315        // Compute the required init range: count * sizeof(T) bytes
316        let access = if property.args().len() >= 3 {
317            Some(self.access_bytes(vm_state, property, 1, 2, checkpoint, &value))
318        } else {
319            None
320        };
321
322        if let Some(id) = value.provenance_alloc_id() {
323            rap_debug!("check_init: alloc={} init_set={} access={:?}",
324                id.0, vm_state.alloc(id).initialized,
325                access.as_ref().and_then(|a| a.as_u64()));
326            if vm_state.alloc(id).dead {
327                // `assume_init_drop` (and other MaybeUninit drop/read ops)
328                // legitimately consume an initialized element from storage that
329                // may be going out of scope; the `Init` requirement concerns
330                // whether the element was written, not whether the allocation is
331                // still live. Mirror the `check_allocated` exception.
332                if !Self::is_maybe_uninit_ptr(vm_state, &value, id) {
333                    return CheckResult::Failed;
334                }
335            }
336            // Verify the entire access range is covered
337            if let Some(ref access_term) = access {
338                if let (Some(access_val), Some(prov)) = (access_term.as_u64(), &value.provenance) {
339                    if let Some(prov_off) = prov.offset.as_u64() {
340                        let end = prov_off + access_val;
341                        let all_init = (prov_off as usize..end as usize).all(|off| vm_state.is_byte_init(id, off));
342                        if all_init && access_val > 0 {
343                            return CheckResult::Proved;
344                        }
345                    }
346                }
347            }
348            if vm_state.alloc(id).initialized {
349                if let (Some(ref access_term), Some(ref size)) = (access, vm_state.allocation_size(id)) {
350                    if let (Some(access_val), Some(size_val)) = (access_term.as_u64(), size.as_u64()) {
351                        // `size_val == 0` means the element type is generic
352                        // (size unknown), so the required access can't exceed a
353                        // meaningful allocation size; skip the bound check.
354                        if size_val > 0 && access_val > size_val {
355                            return CheckResult::Failed;
356                        }
357                    }
358                    if access_term.as_u64().is_some() && size.as_u64().is_some() {
359                        return CheckResult::Proved;
360                    }
361                }
362                return CheckResult::Proved;
363            }
364            // as_ptr/as_mut_ptr on MaybeUninit → write operations don't need pre-init.
365            if value.invariants.init && value.invariants.non_null && value.invariants.aligned
366                && matches!(value.ty.kind(), TyKind::RawPtr(..))
367                && !vm_state.alloc(id).dead
368            {
369                if let Some(callee) = checkpoint.callee {
370                    let p = vm_state.tcx.def_path_str(callee);
371                    if crate::helpers::api_classify::is_mem_copy_or_write_api(&p) {
372                        return CheckResult::Proved;
373                    }
374                }
375            }
376            // Check byte-level init: if all bytes in range are initialized
377            if let Some(size) = vm_state.allocation_size(id).cloned() {
378                if let Some(size_val) = size.as_u64() {
379                    let size_usize = (size_val as usize).min(4096);
380                    let all_init = (0..size_usize).all(|off| vm_state.is_byte_init(id, off));
381                    if all_init && size_val > 0 {
382                        return CheckResult::Proved;
383                    }
384                }
385            }
386        }
387        // Check field-level init for aggregate types
388        if let Some(origin_op) = checkpoint.args.first() {
389            let origin_val = vm_state.value_of_operand(origin_op);
390            if let Some(prov) = &origin_val.provenance {
391                if vm_state.alloc(prov.alloc_id).initialized {
392                    if let Some(ref access_term) = access {
393                        if let Some(size) = vm_state.allocation_size(prov.alloc_id) {
394                            if let (Some(access_val), Some(size_val)) = (access_term.as_u64(), size.as_u64()) {
395                                if access_val <= size_val {
396                                    return CheckResult::Proved;
397                                }
398                                // Required bytes exceed allocation → not fully init
399                            } else {
400                                return CheckResult::Proved;
401                            }
402                        } else {
403                            return CheckResult::Proved;
404                        }
405                    }
406                    // access=None: can't verify size, fall through
407                }
408            }
409            if let Operand::Copy(place) | Operand::Move(place) = origin_op {
410                for alloc_id in self.trace_alloc_ids(vm_state, place.local) {
411                    if vm_state.alloc(alloc_id).initialized {
412                        if let Some(ref access_term) = access {
413                            if let Some(size) = vm_state.allocation_size(alloc_id) {
414                                if let (Some(access_val), Some(size_val)) = (access_term.as_u64(), size.as_u64()) {
415                                    if access_val <= size_val {
416                                        return CheckResult::Proved;
417                                    }
418                                } else {
419                                    return CheckResult::Proved;
420                                }
421                            } else {
422                                return CheckResult::Proved;
423                            }
424                         }
425                    }
426                }
427            }
428        }
429        // A path that evaluated an `Iterator::next` discriminant may be
430        // infeasible when the iterator was empty (e.g. `assume_init_drop` on the
431        // `Some` branch of `next()` that returned `None`). Check feasibility
432        // only for such paths so unrelated over-constrained paths aren't
433        // spuriously marked sound.
434        if vm_state.contract_flags.saw_next_discriminant {
435            let local = Solver::new(vm_state.ctx);
436            local.push();
437            for cond in &vm_state.path_conditions {
438                local.assert(cond);
439            }
440            if local.check() == SatResult::Unsat {
441                local.pop(1);
442                return CheckResult::Proved;
443            }
444            local.pop(1);
445        }
446        CheckResult::Unknown
447    }
448
449    pub(super) fn trace_alloc_ids<'ctx, 'tcx>(
450        &self, vm_state: &VmState<'ctx, 'tcx>, local: Local,
451    ) -> Vec<AllocId> {
452        let mut result = Vec::new();
453        if let Some(id) = vm_state.local_alloc_ids.get(&local) {
454            result.push(*id);
455        }
456        let mut worklist = vec![local];
457        let mut visited = FxHashSet::default();
458        visited.insert(local);
459        while let Some(cur) = worklist.pop() {
460            for block in vm_state.body.basic_blocks.iter() {
461                for stmt in &block.statements {
462                    if let StatementKind::Assign(assign) = &stmt.kind {
463                        let (dest, rvalue) = &**assign;
464                        if dest.local != cur || !dest.projection.is_empty() {
465                            continue;
466                        }
467                        let src_local = match rvalue {
468                            #[cfg(rapx_rvalue_use_with_retag)]
469                            Rvalue::Use(Operand::Copy(p) | Operand::Move(p), _)
470                                if p.projection.is_empty() => Some(p.local),
471                            #[cfg(not(rapx_rvalue_use_with_retag))]
472                            Rvalue::Use(Operand::Copy(p) | Operand::Move(p))
473                                if p.projection.is_empty() => Some(p.local),
474                            Rvalue::CopyForDeref(p) if p.projection.is_empty() => Some(p.local),
475                            Rvalue::Cast(_, Operand::Copy(p) | Operand::Move(p), _)
476                                if p.projection.is_empty() => Some(p.local),
477                            Rvalue::RawPtr(_, p) if p.projection.is_empty() => Some(p.local),
478                            _ => None,
479                        };
480                        if let Some(src) = src_local {
481                            if visited.insert(src) {
482                                if let Some(id) = vm_state.local_alloc_ids.get(&src) {
483                                    result.push(*id);
484                                }
485                                worklist.push(src);
486                            }
487                        }
488                    }
489                }
490            }
491        }
492        result
493    }
494
495    pub(super) fn check_alive<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
496        checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
497    {
498        let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
499        if let Some(id) = value.provenance_alloc_id() {
500            if vm_state.alloc(id).dead {
501                if let Some(origin) = vm_state.resolve_origin(&value) {
502                    let is_param = origin.local.as_usize() <= vm_state.body.arg_count
503                        && origin.local != Local::from_usize(0);
504                    if is_param {
505                        return CheckResult::Proved;
506                    }
507                }
508                return CheckResult::Failed;
509            }
510            if let Some(origin) = vm_state.resolve_origin(&value) {
511                let is_raw_ptr = matches!(origin.kind,
512                    crate::verify::vm::alias::VmOriginKind::RawMutPtr
513                    | crate::verify::vm::alias::VmOriginKind::RawConstPtr);
514                if is_raw_ptr {
515                    let is_field = origin.local.as_usize() > vm_state.body.arg_count;
516                    if is_field {
517                        let mut root_id = id;
518                        while let Some(parent_id) = vm_state.alloc(root_id).parent {
519                            root_id = parent_id;
520                        }
521                        if root_id != id
522                            && vm_state.alloc(root_id).alive_assumed
523                            && !vm_state.alloc(root_id).dead
524                        {
525                            return CheckResult::Proved;
526                        }
527                        if vm_state.allocations.iter().any(|a| a.alive_assumed) {
528                            let root_is_external = vm_state.alloc(root_id).is_external;
529                            if root_is_external {
530                                return CheckResult::Proved;
531                            }
532                        }
533                        // Only fail for raw pointer struct fields when the
534                        // return type has an explicit named lifetime (from
535                        // struct generics) that is not grounded in &self.
536                        let ret_ty = &vm_state.body.local_decls[Local::from_usize(0)].ty;
537                        let is_named = match ret_ty.kind() {
538                            rustc_middle::ty::TyKind::Ref(r, _, _) => {
539                                !matches!(r.kind(), rustc_middle::ty::RegionKind::ReErased)
540                            }
541                            _ => false,
542                        };
543                        if is_named || super::signature_return_has_lifetime(
544                            vm_state.tcx, vm_state.caller_def_id)
545                            .map_or(false, |(_, t)| t.contains('\''))
546                        {
547                            // Named/explicit return lifetime: check whether
548                            // a reference parameter pointee is an ADT that
549                            // carries NO lifetime parameters.  When the
550                            // struct has no lifetimes of its own, the
551                            // returned view's lifetime is guaranteed to be
552                            // caller-chosen and tied to the borrow (e.g.
553                            // &self).  In that case the pointer field's
554                            // provenance is grounded in a live reference.
555                            let body = vm_state.body;
556                            let adt_no_lifetime = (1..=body.arg_count).any(|i| {
557                                let param_ty = body.local_decls[Local::from_usize(i)].ty;
558                                if let rustc_middle::ty::TyKind::Ref(_, pointee, _) = param_ty.kind() {
559                                    if let rustc_middle::ty::TyKind::Adt(_adt_def, substs) = pointee.kind() {
560                                        return !substs.types().any(|t| {
561                                            matches!(t.kind(), rustc_middle::ty::TyKind::Param(_))
562                                        })
563                                        && !substs.iter().any(|g| matches!(g.kind(),
564                                            GenericArgKind::Lifetime(_)));
565                                    }
566                                }
567                                false
568                            });
569                            if !adt_no_lifetime {
570                                return CheckResult::Failed;
571                            }
572                        }
573                        return CheckResult::Proved;
574                    }
575                    // Raw pointer param: check if any ref param shares provenance.
576                    let body = vm_state.body;
577                    let matches_ref_param = (1..=body.arg_count).any(|i| {
578                        let param_local = Local::from_usize(i);
579                        let param_ty = body.local_decls[param_local].ty;
580                        if !matches!(param_ty.kind(), rustc_middle::ty::TyKind::Ref(..)) {
581                            return false;
582                        }
583                        vm_state.local_value(param_local)
584                            .and_then(|v| v.provenance_alloc_id())
585                            .is_some_and(|pid| pid == id)
586                    });
587                    if !matches_ref_param && !vm_state.alloc(id).alive_assumed {
588                        return CheckResult::Failed;
589                    }
590                }
591                return CheckResult::Proved;
592            }
593            return CheckResult::Proved;
594        }
595        if value.invariants.non_null || value.invariants.init { return CheckResult::Proved; }
596        CheckResult::Unknown
597    }
598}
rapx/verify/property_checker/memory.rs

rapx/verify/property_checker/
memory.rs
