rapx/verify/property_checker/typed.rs
1use rustc_middle::ty::{Ty, TyKind};
2#[cfg(not(rapx_has_skip_norm_wip))]
3use crate::compat::SkipNormWip;
4use z3::{Solver, ast::Ast};
5use crate::verify::contract::{ContractExpr, Property, PropertyArg};
6use crate::verify::report::CheckResult;
7use crate::helpers::mir_scan::Checkpoint;
8use crate::verify::vm::state::VmState;
9
10use super::PropertyChecker;
11
12impl PropertyChecker {
13 pub(super) fn check_typed<'ctx, 'tcx>(&self, vm_state: &VmState<'ctx, 'tcx>, _solver: &Solver<'ctx>,
14 checkpoint: &Checkpoint<'tcx>, property: &Property<'tcx>) -> CheckResult
15 {
16 let Some(value) = self.target_value(vm_state, checkpoint, property) else { return CheckResult::Unknown };
17 let expected = property.args().get(1).and_then(|a| if let PropertyArg::Ty(ty) = a { Some(*ty) } else { None });
18 if let Some(expected_ty) = expected {
19 let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, expected_ty);
20 let expected_ty = if resolved != expected_ty { resolved } else { expected_ty };
21
22 let value_elem_ty = match value.ty.kind() {
23 TyKind::RawPtr(inner, _) | TyKind::Ref(_, inner, _) => *inner,
24 _ => value.ty,
25 };
26
27 // `MaybeUninit<T>` (and slices/arrays of it) carries no validity
28 // invariant: any byte pattern is a valid `MaybeUninit<T>`. A byte
29 // buffer reinterpreted as `[MaybeUninit<T>]` (e.g. the slice handed
30 // to `Box::from_raw_in` by `RawVec::into_box`) is therefore always
31 // "typed" — alignment/size are discharged by the separate
32 // `Align`/`Allocated` facts.
33 if Self::ty_is_maybe_uninit(vm_state.tcx, expected_ty) {
34 return CheckResult::Proved;
35 }
36
37 // Check provenance: does the allocation's element type match the expected type?
38 if let Some(alloc_id) = value.provenance_alloc_id() {
39 let alloc = vm_state.alloc(alloc_id);
40 if let Some(mut elem_ty) = alloc.element_ty {
41 // Resolve generic type param to concrete callsite type.
42 elem_ty = self.resolve_ty_params(vm_state, checkpoint, elem_ty);
43 if matches!(elem_ty.kind(), TyKind::Param(_)) {
44 let resolved = self.instantiate_callsite_ty(vm_state, checkpoint, elem_ty);
45 if resolved != elem_ty {
46 elem_ty = resolved;
47 }
48 }
49 if elem_ty == expected_ty {
50 return CheckResult::Proved;
51 }
52 // MaybeUninit<T> accessed via raw pointer from as_mut_ptr:
53 // treat as T for write ops where caller will initialize it.
54 if let TyKind::Adt(adt_def, substs) = elem_ty.kind() {
55 let dp = vm_state.tcx.def_path_str(adt_def.did());
56 if dp.contains("::MaybeUninit")
57 && matches!(value.ty.kind(), TyKind::RawPtr(..))
58 {
59 if let Some(inner) = substs.first().and_then(|s| s.as_type()) {
60 if inner == expected_ty {
61 if let Some(c) = checkpoint.callee {
62 let cp = vm_state.tcx.def_path_str(c);
63 if crate::helpers::api_classify::is_mem_copy_or_write_api(&cp)
64 { return CheckResult::Proved; }
65 }
66 }
67 }
68 }
69 }
70 // Struct/enum field: check if expected_ty matches a field at the provenance offset.
71 if let TyKind::Adt(adt_def, substs) = elem_ty.kind() {
72 if !adt_def.is_enum() {
73 let off_u64 = value.provenance.as_ref()
74 .and_then(|p| p.offset.simplify().as_u64());
75 let variant = adt_def.non_enum_variant();
76 let mut accum: u64 = 0;
77 for (i, field_def) in variant.fields.iter().enumerate() {
78 let field_off = vm_state.field_offset_in_bytes(elem_ty, i);
79 if i > 0 && field_off == 0 {
80 accum = 0;
81 }
82 let field_ty: Ty<'tcx> = field_def.ty(vm_state.tcx, substs).skip_norm_wip();
83 if field_ty == expected_ty {
84 if off_u64 == Some(accum) {
85 if value.invariants.init {
86 return CheckResult::Proved;
87 }
88 return CheckResult::Failed;
89 }
90 } else if off_u64 == Some(accum) {
91 // Unwrap ManuallyDrop<T> → T for unions like MaybeUninit.
92 if let TyKind::Adt(wrap_adt, wrap_substs) = field_ty.kind() {
93 if !wrap_adt.is_enum() {
94 let did = format!("{:?}", wrap_adt.did());
95 if (did.contains("ManuallyDrop") || did.contains("UnsafeCell"))
96 && wrap_substs.first().and_then(|s| s.as_type()) == Some(expected_ty)
97 {
98 if vm_state.alloc(alloc_id).initialized {
99 return CheckResult::Proved;
100 }
101 return CheckResult::Failed;
102 }
103 }
104 }
105 }
106 accum += vm_state.size_of_ty(field_ty).max(1);
107 }
108 }
109 }
110 // IterElements: the allocation stores pointers, but the invariant
111 // applies to the pointee type. Unwrap *const/*mut to match.
112 if self.has_iter_elements(property) {
113 if let TyKind::RawPtr(inner, _) = elem_ty.kind() {
114 if *inner == expected_ty {
115 return CheckResult::Proved;
116 }
117 }
118 }
119 // Transmute to an all-bit-valid destination type
120 // (integers, floats, raw pointers): any byte pattern is
121 // a valid value, so a reinterpretation from a
122 // differently-typed allocation is sound (e.g. memchr
123 // reads `[u8]` as `usize`). This is only sound when the
124 // pointer is also correctly aligned to the destination
125 // type: a raw `*const u8 as *const u32` cast over
126 // align-1 storage is misaligned and must stay UNSOUND.
127 if Self::all_bit_patterns_valid(expected_ty) {
128 let expected_align = vm_state.align_of_ty(expected_ty).max(1);
129 if Self::value_aligned_to(vm_state, &value, expected_align) {
130 return CheckResult::Proved;
131 }
132 }
133 // Non-ADT element type that doesn't match → Failed.
134 if !matches!(elem_ty.kind(), TyKind::Adt(..)) {
135 return CheckResult::Failed;
136 }
137 // ADT type with no matching field and no init → Failed.
138 if !value.invariants.init {
139 return CheckResult::Failed;
140 }
141 }
142 }
143
144 // No provenance: fall back to init and size checks.
145 if value.invariants.init {
146 if vm_state.size_of_ty(value_elem_ty) > 0
147 && vm_state.size_of_ty(expected_ty) > 0
148 && vm_state.size_of_ty(value_elem_ty) == vm_state.size_of_ty(expected_ty)
149 {
150 return CheckResult::Proved;
151 }
152 }
153
154 // For IterElements (for_each) properties, the invariant applies to
155 // individual elements loaded from a container. The VM may not track
156 // provenance through memory loads from heap allocations. When sizes
157 // match, trust the type.
158 if self.has_iter_elements(property) {
159 if vm_state.size_of_ty(value_elem_ty) > 0
160 && vm_state.size_of_ty(expected_ty) > 0
161 && vm_state.size_of_ty(value_elem_ty) == vm_state.size_of_ty(expected_ty)
162 {
163 return CheckResult::Proved;
164 }
165 }
166
167 // When we have provenance but the element type doesn't match and
168 // sizes match, assume the type is correct. This handles pointers
169 // loaded from container elements where individual provenance is lost.
170 let vs = vm_state.size_of_ty(value_elem_ty);
171 let es = vm_state.size_of_ty(expected_ty);
172 if let Some(alloc_id) = value.provenance_alloc_id()
173 && vs == es
174 {
175 if vm_state.alloc(alloc_id).element_ty.is_some()
176 {
177 return CheckResult::Proved;
178 }
179 }
180
181 if vs > 0 && es > 0 && vs != es {
182 return CheckResult::Failed;
183 }
184 }
185 CheckResult::Unknown
186 }
187
188 pub(super) fn ty_is_maybe_uninit(tcx: rustc_middle::ty::TyCtxt<'_>, ty: Ty<'_>) -> bool {
189 let mut t = ty;
190 loop {
191 match t.kind() {
192 TyKind::Slice(e) | TyKind::Array(e, _) => t = *e,
193 TyKind::RawPtr(e, _) | TyKind::Ref(_, e, _) => t = *e,
194 TyKind::Adt(adt, _) => {
195 return tcx.def_path_str(adt.did()).contains("::MaybeUninit");
196 }
197 _ => return false,
198 }
199 }
200 }
201
202 pub(super) fn check_size<'ctx, 'tcx>(
203 &self,
204 vm_state: &VmState<'ctx, 'tcx>,
205 property: &Property<'tcx>,
206 ) -> CheckResult {
207 let ty = match property.args().iter().find_map(|a| match a {
208 PropertyArg::Ty(t) => Some(*t),
209 _ => None,
210 }) {
211 Some(t) => t,
212 None => return CheckResult::Unknown,
213 };
214
215 match property.args().last() {
216 Some(PropertyArg::Ident(id)) if id == "sized" => {
217 // For a generic type parameter (`T: Sized`) the concrete size is
218 // unknown, but the `non-ZST` constraint is a caller obligation
219 // (mirroring the `inject_layout_constraints` convention that a
220 // generic `SizeOf(T)` term is `>= 1`). Functions that panic on
221 // ZST — `offset_from`, `size_of_val`, ... — are sound for every
222 // `T`, so treating the constraint as satisfied is safe.
223 if self.is_generic_ty(ty) {
224 return CheckResult::Proved;
225 }
226 if vm_state.size_of_ty(ty) == 0 {
227 CheckResult::Failed
228 } else {
229 CheckResult::Proved
230 }
231 }
232 Some(PropertyArg::Ident(id)) if id == "unsized" => {
233 match ty.kind() {
234 TyKind::Slice(_) | TyKind::Str | TyKind::Dynamic(..) => CheckResult::Proved,
235 _ => CheckResult::Unknown,
236 }
237 }
238 Some(PropertyArg::Expr(ContractExpr::Const(c))) => {
239 if self.is_generic_ty(ty) {
240 return CheckResult::Unknown;
241 }
242 if vm_state.size_of_ty(ty) as u128 == *c {
243 CheckResult::Proved
244 } else {
245 CheckResult::Failed
246 }
247 }
248 _ => CheckResult::Unknown,
249 }
250 }
251}