rapx/verify/property_checker/
auto_trait.rs

1//! Checkers for the `Send`/`Sync` marker-trait predicates.
2//!
3//! These are intentionally *structural/behavioural* approximations
4//! (sound-incomplete): a full proof of "exclusive ownership" / "no cross-thread
5//! aliasing" needs an ownership + concurrency model (e.g. separation logic),
6//! which the current sequential VM does not have.
7//!
8//! The vocabulary follows the Rust model: a raw pointer is `!Send` unless
9//! *tamed* — either the type has no raw pointers at all ([`NoRawPtr`]), or its
10//! raw-pointer field is `Allocated`/`Owning` (discharged via the struct's
11//! `#[rapx::invariant]` annotations) and updated read-only ([`NoInternalMut`]),
12//! exclusively ([`UniInternalMut`]), or under synchronization / atomically
13//! ([`AtomicUpdate`]).  The composition is declared in
14//! `std-trait-ensures.json` + `std-compound-properties.rs`; this module only
15//! implements the primitive type-level checks.
16
17#[cfg(rapx_has_attr_ir)]
18use rustc_attr_ir::LangItem;
19#[cfg(all(not(rapx_has_attr_ir), not(rapx_ge_100)))]
20use rustc_hir::LangItem;
21#[cfg(all(not(rapx_has_attr_ir), rapx_ge_100))]
22use rustc_hir::attrs::lang_items::LangItem;
23use rustc_hir::def::DefKind;
24use rustc_hir::def_id::DefId;
25use rustc_middle::ty::{ClauseKind, GenericArgKind, ParamTy, Ty, TyCtxt, TyKind};
26
27use crate::compat::FxHashMap;
28use crate::helpers::mir_scan::{Checkpoint, has_atomic_call, has_raw_ptr_write};
29use crate::verify::vm::state::VmState;
30use crate::verify::{
31    contract::{Property, PropertyArg, PropertyKind},
32    report::{CheckResult, UnknownReason},
33    target::get_struct_invariants_from_annotation,
34};
35
36use super::PropertyChecker;
37
38/// Three-valued structural verdict: a type definitely contains a negative
39/// (`Yes`), definitely does not (`No`), or contains an unresolved generic
40/// parameter so the answer is unknown (`Maybe`).
41#[derive(Clone, Copy, PartialEq, Eq, Debug)]
42enum Contains {
43    Yes,
44    No,
45    Maybe,
46}
47
48impl Contains {
49    /// `Yes` dominates; `Maybe` dominates `No` (conservative merge).
50    fn join(self, other: Contains) -> Contains {
51        match (self, other) {
52            (Contains::Yes, _) | (_, Contains::Yes) => Contains::Yes,
53            (Contains::Maybe, _) | (_, Contains::Maybe) => Contains::Maybe,
54            (Contains::No, Contains::No) => Contains::No,
55        }
56    }
57
58    /// Map the three-valued verdict to a [`CheckResult`].
59    fn to_check(self) -> CheckResult {
60        match self {
61            Contains::Yes => CheckResult::Failed,
62            Contains::Maybe => CheckResult::Unknown(UnknownReason::Unimplemented),
63            Contains::No => CheckResult::ProvedByRule,
64        }
65    }
66}
67
68impl PropertyChecker {
69    /// `ContainNoType(T, bad1, bad2, ...)`: `T` must not structurally contain any of
70    /// the named negative types.
71    pub(super) fn check_contain_no_type<'z3, 'tcx>(
72        &self,
73        vm_state: &VmState<'z3, 'tcx>,
74        checkpoint: &Checkpoint<'tcx>,
75        property: &Property<'tcx>,
76    ) -> CheckResult {
77        let Some(ty) = Self::ty_arg(property, 0) else {
78            return CheckResult::Unknown(UnknownReason::Unimplemented);
79        };
80        let negatives: Vec<String> = property.args()[1..]
81            .iter()
82            .filter_map(|a| match a {
83                PropertyArg::Ident(name) => Some(name.clone()),
84                _ => None,
85            })
86            .collect();
87        if negatives.is_empty() {
88            return CheckResult::Unknown(UnknownReason::Unimplemented);
89        }
90        contain_no_type_check(vm_state.tcx, ty, &negatives, checkpoint.caller, false)
91    }
92
93    /// `NoRawPtr(T)`: `T` must have no raw pointers.
94    pub(super) fn check_no_raw_ptr<'z3, 'tcx>(
95        &self,
96        vm_state: &VmState<'z3, 'tcx>,
97        checkpoint: &Checkpoint<'tcx>,
98        property: &Property<'tcx>,
99    ) -> CheckResult {
100        let Some(ty) = Self::ty_arg(property, 0) else {
101            return CheckResult::Unknown(UnknownReason::Unimplemented);
102        };
103        no_raw_ptr_check(vm_state.tcx, ty, checkpoint.caller, false)
104    }
105
106    /// `NoInternalMut(T)`: `T` must have no interior mutation through raw pointers.
107    pub(super) fn check_no_internal_mut<'z3, 'tcx>(
108        &self,
109        vm_state: &VmState<'z3, 'tcx>,
110        property: &Property<'tcx>,
111    ) -> CheckResult {
112        let Some(ty) = Self::ty_arg(property, 0) else {
113            return CheckResult::Unknown(UnknownReason::Unimplemented);
114        };
115        no_internal_mut_check(vm_state.tcx, ty)
116    }
117
118    /// `UniInternalMut(T)`: `T`'s interior mutation must be unique (exclusive
119    /// owner, no aliasing `Clone`).
120    pub(super) fn check_uni_internal_mut<'z3, 'tcx>(
121        &self,
122        vm_state: &VmState<'z3, 'tcx>,
123        property: &Property<'tcx>,
124    ) -> CheckResult {
125        let Some(ty) = Self::ty_arg(property, 0) else {
126            return CheckResult::Unknown(UnknownReason::Unimplemented);
127        };
128        uni_internal_mut_check(vm_state.tcx, ty)
129    }
130
131    /// `AtomicUpdate(T)`: `T`'s raw-pointer updates are guarded by a
132    /// synchronization primitive (`Mutex`/`RwLock`) or performed atomically
133    /// (`Atomic*`).
134    pub(super) fn check_atomic_update<'z3, 'tcx>(
135        &self,
136        vm_state: &VmState<'z3, 'tcx>,
137        checkpoint: &Checkpoint<'tcx>,
138        property: &Property<'tcx>,
139    ) -> CheckResult {
140        let Some(ty) = Self::ty_arg(property, 0) else {
141            return CheckResult::Unknown(UnknownReason::Unimplemented);
142        };
143        atomic_update_check(vm_state.tcx, ty, checkpoint.caller, false)
144    }
145
146    /// `RefSend(T)`: every interior-mutability (`UnsafeCell`) / raw-pointer
147    /// field of `T` must be guarded by a synchronization primitive.
148    pub(super) fn check_ref_send<'z3, 'tcx>(
149        &self,
150        vm_state: &VmState<'z3, 'tcx>,
151        checkpoint: &Checkpoint<'tcx>,
152        property: &Property<'tcx>,
153    ) -> CheckResult {
154        let Some(ty) = Self::ty_arg(property, 0) else {
155            return CheckResult::Unknown(UnknownReason::Unimplemented);
156        };
157        ref_send_check(vm_state.tcx, ty, checkpoint.caller, true)
158    }
159}
160
161/// Type-level `ContainNoType` obligation check (no VM state required): returns
162/// `Failed` if `ty` structurally contains any named negative, `Unknown` if a
163/// generic parameter makes the answer unresolved, else `Proved`.
164pub(crate) fn contain_no_type_check<'tcx>(
165    tcx: TyCtxt<'tcx>,
166    ty: Ty<'tcx>,
167    negatives: &[String],
168    impl_def_id: DefId,
169    is_sync: bool,
170) -> CheckResult {
171    let mut defs: Vec<DefId> = Vec::new();
172    for name in negatives {
173        defs.extend_from_slice(crate::def_id::negative_type_defs(name));
174    }
175    type_structurally_contains(tcx, ty, &defs, impl_def_id, is_sync).to_check()
176}
177
178/// Type-level `NoRawPtr` obligation check (no VM state required).
179pub(crate) fn no_raw_ptr_check<'tcx>(
180    tcx: TyCtxt<'tcx>,
181    ty: Ty<'tcx>,
182    impl_def_id: DefId,
183    is_sync: bool,
184) -> CheckResult {
185    find_raw_ptr(tcx, ty, impl_def_id, is_sync).to_check()
186}
187
188/// Type-level `NoInternalMut` obligation check (no VM state required): `Failed`
189/// if any inherent method writes through a raw pointer — either a plain
190/// `*ptr = ...` write or an atomic update (`Atomic*` intrinsic).
191pub(crate) fn no_internal_mut_check<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> CheckResult {
192    if has_raw_ptr_writes(tcx, ty) || has_atomic_ptr_updates(tcx, ty) {
193        CheckResult::Failed
194    } else {
195        CheckResult::ProvedByRule
196    }
197}
198
199/// Type-level `UniInternalMut` obligation check (no VM state required): `Proved`
200/// if the type writes through a raw pointer (plain or atomic) but does not
201/// implement `Clone` (which would copy the pointer and alias the pointee).
202pub(crate) fn uni_internal_mut_check<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> CheckResult {
203    if (has_raw_ptr_writes(tcx, ty) || has_atomic_ptr_updates(tcx, ty))
204        && !type_implements_clone(tcx, ty)
205    {
206        CheckResult::ProvedByRule
207    } else {
208        CheckResult::Failed
209    }
210}
211
212/// Type-level `AtomicUpdate` obligation check (no VM state required): `Proved`
213/// when aliased updates of the type's raw pointers are safe without exclusive
214/// ownership.  Two ways satisfy this:
215///  1. *structural* — every interior-mutability / raw-pointer field is guarded
216///     by a synchronization primitive (`Mutex`/`RwLock`/`Atomic*`), so the
217///     `find_unsynchronized_mutation` scan finds nothing unsynchronized; or
218///  2. *behavioural* — the type's raw-pointer updates go through an atomic
219///     intrinsic (`AtomicUsize::fetch_add` & friends), as in `Arc`-style
220///     reference counting.
221pub(crate) fn atomic_update_check<'tcx>(
222    tcx: TyCtxt<'tcx>,
223    ty: Ty<'tcx>,
224    impl_def_id: DefId,
225    is_sync: bool,
226) -> CheckResult {
227    match find_unsynchronized_mutation(tcx, ty, impl_def_id, is_sync) {
228        Contains::No => CheckResult::ProvedByRule,
229        Contains::Maybe => CheckResult::Unknown(UnknownReason::Unimplemented),
230        Contains::Yes => {
231            if has_atomic_ptr_updates(tcx, ty) {
232                CheckResult::ProvedByRule
233            } else {
234                CheckResult::Failed
235            }
236        }
237    }
238}
239
240/// Type-level `Allocated(ptr, T, n)` / `Owning(ptr)` obligation check (no VM
241/// state required): `Proved` when `T` declares a matching
242/// `#[rapx::invariant(Allocated(ptr))]` / `#[rapx::invariant(Owning(ptr))]`
243/// annotation (optionally restricted to the `field` named in the property) *and*
244/// the already-run struct-invariant verification discharged it.
245/// `invariant_results` carries the per-struct verdict; when a struct's
246/// invariants failed to verify, the check fails too.
247pub(crate) fn field_invariant_check<'tcx>(
248    tcx: TyCtxt<'tcx>,
249    ty: Ty<'tcx>,
250    kind: PropertyKind,
251    field: Option<&str>,
252    invariant_results: &FxHashMap<DefId, CheckResult>,
253) -> CheckResult {
254    let TyKind::Adt(adt_def, _) = ty.kind() else {
255        return CheckResult::Failed;
256    };
257    let adt_def_id = adt_def.did();
258
259    let invariants = get_struct_invariants_from_annotation(tcx, adt_def_id, adt_def_id);
260    let matched = invariants.iter().any(|p| {
261        p.kind() == Some(kind)
262            && field.is_none_or(|f| {
263                p.args()
264                    .first()
265                    .and_then(|a| {
266                        crate::verify::contract::place::field_name_from_arg(tcx, adt_def_id, a)
267                    })
268                    .as_deref()
269                    == Some(f)
270            })
271    });
272    if !matched {
273        return CheckResult::Failed;
274    }
275
276    // The invariant must actually hold, not just be annotated.
277    if let Some(result) = invariant_results.get(&adt_def_id) {
278        if *result != CheckResult::ProvedByRule {
279            return CheckResult::Failed;
280        }
281    }
282    CheckResult::ProvedByRule
283}
284
285/// Type-level `RefSend` obligation check (no VM state required).
286pub(crate) fn ref_send_check<'tcx>(
287    tcx: TyCtxt<'tcx>,
288    ty: Ty<'tcx>,
289    impl_def_id: DefId,
290    is_sync: bool,
291) -> CheckResult {
292    find_unsynchronized_mutation(tcx, ty, impl_def_id, is_sync).to_check()
293}
294
295/// Whether `ty` implements `Clone` (which copies any raw-pointer field, aliasing
296/// the pointee across a move).
297fn type_implements_clone<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool {
298    let Some(clone_did) = tcx.lang_items().clone_trait() else {
299        return false;
300    };
301    tcx.all_impls(clone_did)
302        .any(|impl_did| tcx.impl_trait_ref(impl_did).skip_binder().self_ty() == ty)
303}
304
305/// Whether a generic type parameter carries a `Send`/`Sync` bound on the impl,
306/// letting the checker treat it as satisfied instead of `Unknown`.
307fn param_bound_is_satisfied(
308    tcx: TyCtxt<'_>,
309    impl_def_id: DefId,
310    param_ty: ParamTy,
311    is_sync: bool,
312) -> bool {
313    let trait_did = if is_sync {
314        tcx.get_diagnostic_item(rustc_span::sym::Sync)
315    } else {
316        tcx.get_diagnostic_item(rustc_span::sym::Send)
317    };
318    let Some(trait_did) = trait_did else {
319        return false;
320    };
321    let predicates = crate::compat::predicates_of(tcx, impl_def_id);
322    #[cfg(not(rapx_ge_100))]
323    let iter = predicates.predicates.iter();
324    #[cfg(rapx_ge_100)]
325    let iter = predicates.clauses.iter();
326    for (pred, _) in iter {
327        if let ClauseKind::Trait(trait_ref) = pred.kind().skip_binder() {
328            if trait_ref.def_id() == trait_did {
329                if let TyKind::Param(p) = trait_ref.self_ty().kind() {
330                    if p.index == param_ty.index {
331                        return true;
332                    }
333                }
334            }
335        }
336    }
337    false
338}
339
340/// Whether any inherent method of `ty` writes through a raw pointer.
341fn has_raw_ptr_writes<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool {
342    let TyKind::Adt(adt_def, _) = ty.kind() else {
343        return false;
344    };
345    let adt_def_id = adt_def.did();
346    tcx.inherent_impls(adt_def_id).iter().any(|impl_id| {
347        tcx.associated_item_def_ids(*impl_id).iter().any(|item| {
348            matches!(tcx.def_kind(*item), DefKind::Fn | DefKind::AssocFn)
349                && has_raw_ptr_write(tcx, *item)
350        })
351    })
352}
353
354/// Whether any inherent method of `ty` performs an atomic update through an
355/// atomic intrinsic or an `Atomic*` method (`fetch_add`/`store`/...), e.g. an
356/// `Arc`-style `fetch_add` on a reference count reached via a raw pointer.
357fn has_atomic_ptr_updates<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> bool {
358    let TyKind::Adt(adt_def, _) = ty.kind() else {
359        return false;
360    };
361    let adt_def_id = adt_def.did();
362    tcx.inherent_impls(adt_def_id).iter().any(|impl_id| {
363        tcx.associated_item_def_ids(*impl_id).iter().any(|item| {
364            matches!(tcx.def_kind(*item), DefKind::Fn | DefKind::AssocFn)
365                && has_atomic_call(tcx, *item)
366        })
367    })
368}
369
370/// Structurally check whether `ty` (transitively) contains a raw pointer.
371/// A raw pointer may also appear as a pattern type (`pattern_type!(*const T
372/// is ..)`), so recurse into `TyKind::Pat`.
373fn find_raw_ptr<'tcx>(
374    tcx: TyCtxt<'tcx>,
375    ty: Ty<'tcx>,
376    impl_def_id: DefId,
377    is_sync: bool,
378) -> Contains {
379    match ty.kind() {
380        TyKind::RawPtr(..) => Contains::Yes,
381        TyKind::Pat(inner, _) => find_raw_ptr(tcx, *inner, impl_def_id, is_sync),
382        TyKind::Adt(adt_def, substs) => {
383            let mut result = Contains::No;
384            for field in adt_def.all_fields() {
385                let field_ty = crate::helpers::mir_utils::field_ty(tcx, field, substs);
386                result = result.join(find_raw_ptr(tcx, field_ty, impl_def_id, is_sync));
387                if result == Contains::Yes {
388                    return Contains::Yes;
389                }
390            }
391            for subst in substs.iter() {
392                if let GenericArgKind::Type(subst_ty) = subst.kind() {
393                    result = result.join(find_raw_ptr(tcx, subst_ty, impl_def_id, is_sync));
394                    if result == Contains::Yes {
395                        return Contains::Yes;
396                    }
397                }
398            }
399            result
400        }
401        TyKind::Ref(_, inner, _) | TyKind::Slice(inner) | TyKind::Array(inner, _) => {
402            find_raw_ptr(tcx, *inner, impl_def_id, is_sync)
403        }
404        TyKind::Tuple(tys) => tys.iter().fold(Contains::No, |acc, t| {
405            acc.join(find_raw_ptr(tcx, t, impl_def_id, is_sync))
406        }),
407        TyKind::Param(param_ty) => {
408            if param_bound_is_satisfied(tcx, impl_def_id, *param_ty, is_sync) {
409                Contains::No
410            } else {
411                Contains::Maybe
412            }
413        }
414        _ => Contains::No,
415    }
416}
417
418/// Structurally check whether `ty` (transitively) contains one of the negative
419/// types identified by `negative_defs`.  A synchronization primitive (`Mutex`/
420/// `RwLock`/`Atomic*`) guards its interior, so the scan stops there — a negative
421/// type nested inside one (e.g. `Mutex<UnsafeCell>`) is considered tamed.
422fn type_structurally_contains<'tcx>(
423    tcx: TyCtxt<'tcx>,
424    ty: Ty<'tcx>,
425    negative_defs: &[DefId],
426    impl_def_id: DefId,
427    is_sync: bool,
428) -> Contains {
429    match ty.kind() {
430        TyKind::Adt(adt_def, substs) => {
431            if negative_defs.contains(&adt_def.did()) {
432                return Contains::Yes;
433            }
434            if crate::def_id::sync_primitive_types().contains(&adt_def.did()) {
435                return Contains::No;
436            }
437            let mut result = Contains::No;
438            for field in adt_def.all_fields() {
439                let field_ty = crate::helpers::mir_utils::field_ty(tcx, field, substs);
440                result = result.join(type_structurally_contains(
441                    tcx,
442                    field_ty,
443                    negative_defs,
444                    impl_def_id,
445                    is_sync,
446                ));
447                if result == Contains::Yes {
448                    return Contains::Yes;
449                }
450            }
451            for subst in substs.iter() {
452                if let GenericArgKind::Type(subst_ty) = subst.kind() {
453                    result = result.join(type_structurally_contains(
454                        tcx,
455                        subst_ty,
456                        negative_defs,
457                        impl_def_id,
458                        is_sync,
459                    ));
460                    if result == Contains::Yes {
461                        return Contains::Yes;
462                    }
463                }
464            }
465            result
466        }
467        TyKind::Ref(_, inner, _) | TyKind::Slice(inner) | TyKind::Array(inner, _) => {
468            type_structurally_contains(tcx, *inner, negative_defs, impl_def_id, is_sync)
469        }
470        TyKind::Tuple(tys) => tys.iter().fold(Contains::No, |acc, t| {
471            acc.join(type_structurally_contains(
472                tcx,
473                t,
474                negative_defs,
475                impl_def_id,
476                is_sync,
477            ))
478        }),
479        TyKind::Param(param_ty) => {
480            if param_bound_is_satisfied(tcx, impl_def_id, *param_ty, is_sync) {
481                Contains::No
482            } else {
483                Contains::Maybe
484            }
485        }
486        _ => Contains::No,
487    }
488}
489
490/// Find an interior-mutability / raw-pointer field that is not guarded by a
491/// synchronization primitive.  A raw pointer may also appear as a pattern type
492/// (`pattern_type!(*const T is ..)`), so recurse into `TyKind::Pat`.
493fn find_unsynchronized_mutation<'tcx>(
494    tcx: TyCtxt<'tcx>,
495    ty: Ty<'tcx>,
496    impl_def_id: DefId,
497    is_sync: bool,
498) -> Contains {
499    match ty.kind() {
500        TyKind::RawPtr(..) => Contains::Yes,
501        TyKind::Pat(inner, _) => find_unsynchronized_mutation(tcx, *inner, impl_def_id, is_sync),
502        TyKind::Adt(adt_def, substs) => {
503            let did = adt_def.did();
504            if crate::def_id::sync_primitive_types().contains(&did) {
505                return Contains::No;
506            }
507            if tcx.is_lang_item(did, LangItem::UnsafeCell) {
508                return Contains::Yes;
509            }
510            let mut result = Contains::No;
511            for field in adt_def.all_fields() {
512                let field_ty = crate::helpers::mir_utils::field_ty(tcx, field, substs);
513                result = result.join(find_unsynchronized_mutation(
514                    tcx,
515                    field_ty,
516                    impl_def_id,
517                    is_sync,
518                ));
519                if result == Contains::Yes {
520                    return Contains::Yes;
521                }
522            }
523            for subst in substs.iter() {
524                if let GenericArgKind::Type(subst_ty) = subst.kind() {
525                    result = result.join(find_unsynchronized_mutation(
526                        tcx,
527                        subst_ty,
528                        impl_def_id,
529                        is_sync,
530                    ));
531                    if result == Contains::Yes {
532                        return Contains::Yes;
533                    }
534                }
535            }
536            result
537        }
538        TyKind::Ref(_, inner, _) | TyKind::Slice(inner) | TyKind::Array(inner, _) => {
539            find_unsynchronized_mutation(tcx, *inner, impl_def_id, is_sync)
540        }
541        TyKind::Tuple(tys) => tys.iter().fold(Contains::No, |acc, t| {
542            acc.join(find_unsynchronized_mutation(tcx, t, impl_def_id, is_sync))
543        }),
544        TyKind::Param(param_ty) => {
545            if param_bound_is_satisfied(tcx, impl_def_id, *param_ty, is_sync) {
546                Contains::No
547            } else {
548                Contains::Maybe
549            }
550        }
551        _ => Contains::No,
552    }
553}
rapx/verify/property_checker/auto_trait.rs

rapx/verify/property_checker/
auto_trait.rs
