rapx/verify/property_checker/
alias.rs

1//! Checkers for `Alias` and `Owning` properties.
2//!
3//! `Alias` delegates to [`crate::verify::vm::alias::check_alias_vm`]; `Owning`
4//! is a simple liveness check on the target allocation.
5
6use crate::helpers::mir_scan::Checkpoint;
7use crate::verify::contract::Property;
8use crate::verify::report::{CheckResult, UnknownReason};
9use crate::verify::vm::state::VmState;
10
11use super::PropertyChecker;
12
13impl PropertyChecker {
14    pub(super) fn check_alias<'z3, 'tcx>(
15        &self,
16        vm_state: &VmState<'z3, 'tcx>,
17        checkpoint: &Checkpoint<'tcx>,
18    ) -> CheckResult {
19        match crate::verify::vm::alias::check_alias_vm(vm_state, checkpoint) {
20            crate::verify::vm::alias::VmAliasResult::Proved => CheckResult::ProvedByRule,
21            crate::verify::vm::alias::VmAliasResult::Failed(_msg) => CheckResult::Failed,
22            crate::verify::vm::alias::VmAliasResult::Unknown => {
23                CheckResult::Unknown(UnknownReason::Unimplemented)
24            }
25        }
26    }
27
28    pub(super) fn check_owning<'z3, 'tcx>(
29        &self,
30        vm_state: &VmState<'z3, 'tcx>,
31        checkpoint: &Checkpoint<'tcx>,
32        property: &Property<'tcx>,
33    ) -> CheckResult {
34        let Some(value) = self.target_value(vm_state, checkpoint, property) else {
35            return CheckResult::Unknown(UnknownReason::Unimplemented);
36        };
37        let value = self.resolve_pointer_provenance(vm_state, value);
38        // `p` may be a pointer just derived from an owner (`Box::into_raw` /
39        // `as_mut_ptr`), whose term still points at the owner's address but whose
40        // own provenance slot is empty. Fall back to the owner's field provenance.
41        let alloc_id = value.provenance_alloc_id().or_else(|| {
42            vm_state
43                .find_local_by_address(&value.z3_term)
44                .and_then(|owner| vm_state.owner_ptr_field(owner))
45                .and_then(|v| v.provenance_alloc_id())
46        });
47        let Some(alloc_id) = alloc_id else {
48            return CheckResult::ProvedByRule;
49        };
50        // `Owning(container.iter())` for_each: every element pointer is the
51        // sole owner of its pointee, so a pointer loaded from the container
52        // (whose provenance names the container allocation) is a valid owner.
53        if vm_state.alloc(alloc_id).facts.for_each.owning {
54            return CheckResult::ProvedByRule;
55        }
56        // A loop-unrolled path repeats the same block (the SCC body), so its
57        // second `DropMemory` is an unrolled iteration rather than a genuine
58        // same-iteration double free. Only the non-unrolled path distinguishes
59        // them (uaf_10 drops twice in one iteration; uaf_false_2 drops once).
60        if vm_state.path_facts.reenter {
61            return CheckResult::ProvedByRule;
62        }
63        // Owning(p): p is the sole carrier of *p's ownership. A live `needs_drop`
64        // owner whose buffer aliases `alloc_id` means a second owner will drop the
65        // same allocation — a double free. The reconstructed owner (the call's
66        // destination) is not a violation, so exclude it.
67        let dest_local = checkpoint.destination.or_else(|| {
68            let body = vm_state.tcx.optimized_mir(checkpoint.caller);
69            match &body.basic_blocks[checkpoint.block].terminator().kind {
70                rustc_middle::mir::TerminatorKind::Call { destination, .. } => {
71                    Some(destination.local)
72                }
73                _ => None,
74            }
75        });
76        // The local the `Owning(p)` argument names (e.g. `raw` in
77        // `Box::from_raw(raw)`), resolved to the caller's local.
78        let raw_local = property.target_place().and_then(|cp| match cp.base {
79            crate::verify::contract::PlaceBase::Arg(n) => checkpoint
80                .args
81                .get(n)
82                .and_then(|op| crate::helpers::mir_utils::operand_mir_place(op).map(|p| p.local)),
83            crate::verify::contract::PlaceBase::Local(n) => {
84                Some(rustc_middle::mir::Local::from_usize(n))
85            }
86            crate::verify::contract::PlaceBase::Return => None,
87        });
88        let live = crate::verify::vm::alias_hazard::live_locals_at(
89            vm_state.tcx,
90            checkpoint.caller,
91            checkpoint.block,
92            // `Owning` fires at a call terminator; scan the whole block so a
93            // `StorageDead` of a consumed parameter (`Box::into_raw(value)`) in
94            // the same block still counts as dead.
95            usize::MAX,
96            true,
97            true,
98        );
99        let typing_env =
100            rustc_middle::ty::TypingEnv::non_body_analysis(vm_state.tcx, checkpoint.caller);
101        // `p`'s term often points at the owner's address (e.g. `s.as_mut_ptr()`
102        // yields a term `addr__1` for `s`). Trace it back to the owner local and
103        // report a second owner directly, without needing its field provenance.
104        // A moved-out source still has the same term but its owner-field
105        // provenance has been invalidated, so it is not counted as an owner.
106        if let Some(owner) = vm_state.find_local_by_address(&value.z3_term) {
107            if live.contains(&owner)
108                && Some(owner) != dest_local
109                && Some(owner) != raw_local
110                && vm_state
111                    .owner_ptr_field(owner)
112                    .is_some_and(|f| f.provenance_alloc_id() == Some(alloc_id))
113            {
114                let oty = vm_state.body().local_decls[owner].ty;
115                if oty.needs_drop(vm_state.tcx, typing_env) {
116                    return CheckResult::Failed;
117                }
118            }
119        }
120        for local in vm_state.current_frame.local_alloc.keys() {
121            if Some(*local) == dest_local {
122                continue;
123            }
124            if !live.contains(local) {
125                continue;
126            }
127            let ty = vm_state.body().local_decls[*local].ty;
128            if !ty.needs_drop(vm_state.tcx, typing_env) {
129                continue;
130            }
131            for path in vm_state.field_paths(*local) {
132                let Some(val) = vm_state.field_value(*local, &path) else {
133                    continue;
134                };
135                if val.provenance_alloc_id() != Some(alloc_id) {
136                    continue;
137                }
138                return CheckResult::Failed;
139            }
140        }
141        CheckResult::ProvedByRule
142    }
143}
144
145
rapx/verify/property_checker/alias.rs

rapx/verify/property_checker/
alias.rs
