rapx/verify/smt_check/
typed.rs

1//! Path-local checking for the `Typed` safety property.
2//!
3//! `Typed(p, T)` is not a pure numeric SMT fact.  The first verifier model
4//! proves it by following the path-local provenance facts produced by the
5//! forward visitor: references and slices carry their Rust element type,
6//! pointer arithmetic preserves the base pointee type, same-type casts preserve
7//! typedness, and `ptr.write(value)` establishes one initialized `T` element.
8
9use std::collections::HashSet;
10
11use rustc_abi::FieldIdx;
12use rustc_hir::def_id::DefId;
13use rustc_middle::ty::{Ty, TyCtxt, TyKind};
14
15use super::common::{SmtCheckResult, SmtChecker};
16use crate::verify::{
17    call_summary::CallEffect,
18    contract::Property,
19    def_use::PlaceKey,
20    helpers::Checkpoint,
21    verifier::{AbstractValue, ForwardVisitResult, StateFact},
22};
23
24const MAX_TYPED_TRACE_DEPTH: usize = 32;
25
26/// Check `Typed` using path-local provenance and initialization facts.
27pub(crate) fn check<'tcx>(
28    checker: &SmtChecker<'tcx>,
29    checkpoint: &Checkpoint<'tcx>,
30    property: &Property<'tcx>,
31    forward: &ForwardVisitResult<'tcx>,
32) -> SmtCheckResult {
33    let Some(target) = checker.property_target(checkpoint, property) else {
34        return SmtCheckResult::unknown("Typed target could not be resolved");
35    };
36    let Some(required_ty) = checker.property_required_ty(checkpoint, property) else {
37        return SmtCheckResult::unknown("Typed type could not be resolved");
38    };
39
40    let mut context = TypedContext {
41        checker,
42        caller: checkpoint.caller,
43        forward,
44        required_ty,
45    };
46
47    let mut seen = HashSet::new();
48    if context.place_is_typed(&target, &mut seen, 0) {
49        SmtCheckResult::proved(format!(
50            "typed provenance proved for {} as {:?}",
51            place_debug(&target),
52            required_ty
53        ))
54    } else {
55        SmtCheckResult::unknown(format!(
56            "current path facts do not prove {} is typed as {:?}",
57            place_debug(&target),
58            required_ty
59        ))
60    }
61}
62
63struct TypedContext<'a, 'tcx> {
64    checker: &'a SmtChecker<'tcx>,
65    caller: DefId,
66    forward: &'a ForwardVisitResult<'tcx>,
67    required_ty: Ty<'tcx>,
68}
69
70impl<'a, 'tcx> TypedContext<'a, 'tcx> {
71    /// Prove that a place denotes storage or a pointer whose dynamic type is `required_ty`.
72    fn place_is_typed(
73        &mut self,
74        place: &PlaceKey,
75        seen: &mut HashSet<PlaceKey>,
76        depth: usize,
77    ) -> bool {
78        if depth > MAX_TYPED_TRACE_DEPTH || !seen.insert(place.clone()) {
79            return false;
80        }
81
82        if self.known_init_matches(place) {
83            return true;
84        }
85
86        if let Some(value) = self.latest_value_for_place(place)
87            && self.value_is_typed(&value, seen, depth + 1)
88        {
89            return true;
90        }
91
92        if let Some(value) = self.latest_cast_source_for_place(place)
93            && self.value_is_typed(&value, seen, depth + 1)
94        {
95            return true;
96        }
97
98        if let Some(source) = self.latest_points_to_source(place) {
99            if self.storage_place_is_typed(&source) {
100                return true;
101            }
102            if self.place_is_typed(&source, seen, depth + 1) {
103                return true;
104            }
105        }
106
107        self.storage_place_is_typed(place)
108    }
109
110    /// Prove that an abstract value carries `required_ty` typed provenance.
111    fn value_is_typed(
112        &mut self,
113        value: &AbstractValue<'tcx>,
114        seen: &mut HashSet<PlaceKey>,
115        depth: usize,
116    ) -> bool {
117        if depth > MAX_TYPED_TRACE_DEPTH {
118            return false;
119        }
120
121        match value {
122            AbstractValue::Place(place) => self.place_is_typed(place, seen, depth + 1),
123            AbstractValue::Ref(place) | AbstractValue::RawPtr(place) => {
124                self.storage_place_is_typed(place) || self.place_is_typed(place, seen, depth + 1)
125            }
126            AbstractValue::Cast(inner, ty) => {
127                self.ty_has_required_payload(*ty) && self.value_is_typed(inner, seen, depth + 1)
128            }
129            AbstractValue::CallResult(call) => call.effects.iter().any(|effect| match effect {
130                CallEffect::ReturnPointerFromArg { arg }
131                | CallEffect::ReturnAliasArg { arg }
132                | CallEffect::ReturnPointerAdd { base_arg: arg, .. }
133                | CallEffect::ReturnPointerSub { base_arg: arg, .. } => call
134                    .args
135                    .get(*arg)
136                    .is_some_and(|arg_value| self.value_is_typed(arg_value, seen, depth + 1)),
137                _ => false,
138            }),
139            _ => false,
140        }
141    }
142
143    /// Return the latest value assigned to a place in the retained path slice.
144    fn latest_value_for_place(&self, place: &PlaceKey) -> Option<AbstractValue<'tcx>> {
145        if !place.fields.is_empty() {
146            return None;
147        }
148        let local = place.local()?;
149        self.forward
150            .latest_value_definition_before(local, self.forward.value_definitions.len())
151            .map(|definition| definition.value.clone())
152    }
153
154    /// Return the latest cast source retained for a target place.
155    fn latest_cast_source_for_place(&self, place: &PlaceKey) -> Option<AbstractValue<'tcx>> {
156        self.forward.facts.iter().rev().find_map(|fact| {
157            let StateFact::Cast { target, source, ty } = fact else {
158                return None;
159            };
160            if target == place && self.ty_has_required_payload(*ty) {
161                Some(source.clone())
162            } else {
163                None
164            }
165        })
166    }
167
168    /// Return the latest provenance source retained for a pointer place.
169    fn latest_points_to_source(&self, place: &PlaceKey) -> Option<PlaceKey> {
170        self.forward.facts.iter().rev().find_map(|fact| {
171            let StateFact::PointsTo { pointer, source } = fact else {
172                return None;
173            };
174            (pointer == place).then(|| source.clone())
175        })
176    }
177
178    /// Return true when a previous write initialized this place as `required_ty`.
179    fn known_init_matches(&self, place: &PlaceKey) -> bool {
180        if self.forward.facts.iter().rev().any(|fact| {
181            let StateFact::KnownInit { place: init_place, ty_name, elements, .. } = fact else { return false };
182            init_place == place && *elements > 0 && self.ty_name_matches(ty_name)
183        }) {
184            return true;
185        }
186        if !place.fields.is_empty() {
187            let mut ancestor = place.clone();
188            while !ancestor.fields.is_empty() {
189                ancestor.fields.pop();
190                if self.forward.facts.iter().rev().any(|fact| {
191                    let StateFact::KnownInit { place: init_place, ty_name, elements, .. } = fact else { return false };
192                    init_place == &ancestor && *elements > 0 && self.ty_name_matches(ty_name)
193                }) {
194                    return true;
195                }
196            }
197        }
198        false
199    }
200
201    /// Return true when a Rust storage place itself is known to contain `required_ty`.
202    fn storage_place_is_typed(&self, place: &PlaceKey) -> bool {
203        let Some(ty) = self.place_ty(place) else {
204            return false;
205        };
206
207        match *ty.kind() {
208            TyKind::RawPtr(_, _) => false,
209            TyKind::Ref(_, inner, _) => self.ty_matches(payload_ty(inner)),
210            TyKind::Slice(element) | TyKind::Array(element, _) => self.ty_matches(element),
211            _ => self.ty_matches(ty),
212        }
213    }
214
215    /// Resolve a place type from MIR locals and field projections.
216    fn place_ty(&self, place: &PlaceKey) -> Option<Ty<'tcx>> {
217        let local = place.local()?;
218        let body = self.checker.tcx.optimized_mir(self.caller);
219        let mut ty = body.local_decls.get(local)?.ty;
220
221        for field in &place.fields {
222            ty = field_ty(self.checker.tcx, ty, *field)?;
223        }
224
225        Some(ty)
226    }
227
228    /// Return true when `ty` or its pointer/reference payload is `required_ty`.
229    fn ty_has_required_payload(&self, ty: Ty<'tcx>) -> bool {
230        self.ty_matches(payload_ty(ty))
231    }
232
233    /// Return true when two compiler types are the same for current verifier purposes.
234    fn ty_matches(&self, ty: Ty<'tcx>) -> bool {
235        ty == self.required_ty || format!("{ty:?}") == format!("{:?}", self.required_ty)
236    }
237
238    /// Return true when a stringly fact type name matches `required_ty`.
239    fn ty_name_matches(&self, ty_name: &str) -> bool {
240        ty_name == format!("{:?}", self.required_ty)
241    }
242}
243
244/// Return the Rust payload type carried by references, pointers, slices, and arrays.
245fn payload_ty<'tcx>(ty: Ty<'tcx>) -> Ty<'tcx> {
246    match *ty.kind() {
247        TyKind::RawPtr(inner, _) | TyKind::Ref(_, inner, _) => payload_ty(inner),
248        TyKind::Slice(element) | TyKind::Array(element, _) => element,
249        _ => ty,
250    }
251}
252
253/// Resolve one field projection through an aggregate type.
254fn field_ty<'tcx>(tcx: TyCtxt<'tcx>, base_ty: Ty<'tcx>, field: usize) -> Option<Ty<'tcx>> {
255    let peeled_ty = base_ty.peel_refs();
256    match *peeled_ty.kind() {
257        TyKind::Adt(adt_def, args) => {
258            if !adt_def.is_struct() && !adt_def.is_union() {
259                return None;
260            }
261            let variant = adt_def.non_enum_variant();
262            if field >= variant.fields.len() {
263                return None;
264            }
265            #[cfg(not(rapx_rustc_ge_198))]
266            let ty = variant.fields[FieldIdx::from_usize(field)].ty(tcx, args);
267            #[cfg(rapx_rustc_ge_198)]
268            let ty = variant.fields[FieldIdx::from_usize(field)]
269                .ty(tcx, args)
270                .skip_norm_wip();
271            Some(ty)
272        }
273        TyKind::Tuple(fields) => fields.get(field).copied(),
274        _ => None,
275    }
276}
277
278/// Return a compact label for a verifier place.
279fn place_debug(place: &PlaceKey) -> String {
280    format!("{place:?}")
281}
rapx/verify/smt_check/typed.rs

rapx/verify/smt_check/
typed.rs
