rapx/verify/
type_invariants.rs

1//! Standard-library type-invariant generation.
2//!
3//! Type invariants are synthesized obligations that a value of a given type
4//! must satisfy. Unlike user-written `#[rapx::invariant]` struct invariants,
5//! these are generated automatically from the bundled `std-type-invariants.json`
6//! database, keyed by a normalized type path (e.g. `core::num::NonZero`) or by
7//! the built-in `[T]` slice key.
8//!
9//! The results feed the `type_invariants` field of a [`FunctionTarget`]
10//! (see `super::target`), whose entry facts are synthesized by the VM's
11//! `init_parameters` and re-proved at return by `VerifyDriver::verify_type_invariants`.
12
13use rustc_hir::def_id::DefId;
14use rustc_middle::ty::{Ty, TyCtxt};
15
16use super::contract::{
17    ContractExpr, NumericPredicate, Property, PropertyArg, PropertyKind, json::AnyItem,
18};
19
20/// For each function parameter (and the return type), look up the type's
21/// invariants from `std-type-invariants.json` and create preconditions.
22pub(crate) fn build_type_invariants_from_params<'tcx>(
23    tcx: TyCtxt<'tcx>,
24    def_id: DefId,
25) -> Vec<Property<'tcx>> {
26    let db = crate::verify::contract::json::get_std_type_invariants();
27    if db.is_empty() {
28        return Vec::new();
29    }
30
31    let fn_sig = tcx.fn_sig(def_id).skip_binder();
32    let inputs = fn_sig.inputs().skip_binder();
33    let output = fn_sig.output().skip_binder();
34
35    let mut results = Vec::new();
36
37    // Use the existing signature parser for parameter names.
38    let (param_names, _param_tys) = crate::helpers::name::parse_signature(tcx, def_id);
39
40    // Add invariants for each parameter
41    for (index, &param_ty) in inputs.iter().enumerate() {
42        if param_ty.is_primitive() {
43            continue;
44        }
45        let param_name = param_names.get(index).cloned().unwrap_or_default();
46        let (type_path, elem_ty) = type_path_key(tcx, param_ty);
47        collect_type_invariants(
48            tcx,
49            def_id,
50            db,
51            &type_path,
52            &param_name,
53            elem_ty,
54            &mut results,
55        );
56    }
57
58    // Also add invariants for the return type
59    if !output.is_unit() && !output.is_primitive() {
60        let (type_path, elem_ty) = type_path_key(tcx, output);
61        collect_type_invariants(
62            tcx,
63            def_id,
64            db,
65            &type_path,
66            "return",
67            elem_ty,
68            &mut results,
69        );
70    }
71
72    results
73}
74
75/// Look up the type path in the DB and add instantiated invariants to `results`.
76fn collect_type_invariants<'tcx>(
77    tcx: TyCtxt<'tcx>,
78    def_id: DefId,
79    db: &std::collections::HashMap<String, crate::verify::contract::json::TypeInvariantEntry>,
80    type_path: &str,
81    param_name: &str,
82    elem_ty: Option<Ty<'tcx>>,
83    results: &mut Vec<Property<'tcx>>,
84) {
85    if let Some(entry) = db.get(type_path) {
86        for prop_entry in &entry.invariants {
87            results.extend(instantiate_type_invariant(
88                tcx, def_id, prop_entry, param_name, elem_ty,
89            ));
90        }
91    }
92    // Also try with common alloc/std prefixes
93    for prefix in ["alloc::", "std::"] {
94        let prefixed = format!("{prefix}{type_path}");
95        if prefixed != type_path {
96            if let Some(entry) = db.get(&prefixed) {
97                for prop_entry in &entry.invariants {
98                    results.extend(instantiate_type_invariant(
99                        tcx, def_id, prop_entry, param_name, elem_ty,
100                    ));
101                }
102            }
103        }
104    }
105}
106
107/// Create properties from a type invariant entry, substituting the parameter
108/// name (and, for the slice entry, the element type). An entry with an `any`
109/// field expands to a single disjunctive `Property::Or`; otherwise it yields
110/// the properties denoted by its tag.
111fn instantiate_type_invariant<'tcx>(
112    tcx: TyCtxt<'tcx>,
113    def_id: DefId,
114    entry: &crate::verify::contract::json::JsonProperty,
115    param_name: &str,
116    elem_ty: Option<Ty<'tcx>>,
117) -> Vec<Property<'tcx>> {
118    if let Some(disjuncts) = &entry.any {
119        if disjuncts.len() < 2 {
120            return Vec::new();
121        }
122        let mut or_disjuncts: Vec<Property<'tcx>> = Vec::with_capacity(disjuncts.len());
123        for item in disjuncts {
124            let mut group: Vec<Property<'tcx>> = Vec::new();
125            match item {
126                AnyItem::Single(e) => {
127                    group.extend(instantiate_entry(tcx, def_id, e, param_name, elem_ty))
128                }
129                AnyItem::And(es) => {
130                    for e in es {
131                        group.extend(instantiate_entry(tcx, def_id, e, param_name, elem_ty));
132                    }
133                }
134            }
135            if !group.is_empty() {
136                or_disjuncts.push(Property::conjunction(group));
137            }
138        }
139        let mut property = Property::new_or(or_disjuncts);
140        property.apply_kind(entry.kind.as_deref());
141        return vec![property];
142    }
143    instantiate_entry(tcx, def_id, entry, param_name, elem_ty)
144}
145
146/// Placeholder type name substituted for the `$elem` token before parsing. The
147/// JSON `$elem` is a bare type argument (e.g. `Align($self, $elem)`), and the
148/// real element type — which can be a composite like `[T; N]` that has no
149/// resolvable name — is injected afterwards by [`replace_ty_args`]. Any
150/// primitive placeholder resolves cleanly through the name-based type parser.
151const SLICE_ELEM_PLACEHOLDER: &str = "u8";
152
153/// Instantiate a single (non-`any`) type invariant entry.
154fn instantiate_entry<'tcx>(
155    tcx: TyCtxt<'tcx>,
156    def_id: DefId,
157    entry: &crate::verify::contract::json::JsonProperty,
158    param_name: &str,
159    elem_ty: Option<Ty<'tcx>>,
160) -> Vec<Property<'tcx>> {
161    let mut uses_elem = false;
162    let mut exprs: Vec<syn::Expr> = Vec::new();
163    for arg_str in &entry.args {
164        // Substitute the `$self` placeholder with the actual parameter name
165        // (or "return"). `$elem` is a type argument: substitute a resolvable
166        // placeholder and inject the real element type after parsing.
167        let mut substituted = arg_str.replace("$self", param_name);
168        if substituted.contains("$elem") {
169            uses_elem = true;
170            substituted = substituted.replace("$elem", SLICE_ELEM_PLACEHOLDER);
171        }
172        // Substitute struct field references like "0" → "param_name.0"
173        let resolved = if is_numeric_field_access(&substituted) {
174            format!("{}.{}", param_name, substituted)
175        } else {
176            substituted
177        };
178        match syn::parse_str::<syn::Expr>(&resolved) {
179            Ok(expr) => exprs.push(expr),
180            Err(_) => {
181                rap_debug!(
182                    "  [type-invariant] failed to parse arg '{}' for tag {}",
183                    resolved,
184                    entry.tag
185                );
186                return Vec::new();
187            }
188        }
189    }
190    if exprs.is_empty() {
191        return Vec::new();
192    }
193    let mut property = Property::new(tcx, def_id, &entry.tag, &exprs);
194    property.apply_kind(entry.kind.as_deref());
195    if matches!(property.kind(), Some(PropertyKind::Unknown)) {
196        return Vec::new();
197    }
198    if uses_elem {
199        let Some(ty) = elem_ty else {
200            // `$elem` was used but no element type is available: drop it.
201            return Vec::new();
202        };
203        replace_ty_args(&mut property, ty);
204    }
205    vec![property]
206}
207
208/// Replace every type argument in a property tree with the slice element type.
209///
210/// The slice invariant's only type arguments are the `$elem` placeholders, so
211/// this recovers the concrete element type (including composites such as
212/// `[T; N]`) that the name-based JSON type parser cannot express. It also
213/// reaches `size_of`/`align_of` type arguments inside `ValidNum` predicates.
214fn replace_ty_args<'tcx>(property: &mut Property<'tcx>, ty: Ty<'tcx>) {
215    match property {
216        Property::Atom(atom) => {
217            for arg in &mut atom.args {
218                match arg {
219                    PropertyArg::Ty(t) => *t = ty,
220                    PropertyArg::Predicates(preds) => {
221                        for pred in preds {
222                            replace_pred_ty(pred, ty);
223                        }
224                    }
225                    _ => {}
226                }
227            }
228        }
229        Property::And(and) => {
230            for conjunct in &mut and.conjuncts {
231                replace_ty_args(conjunct, ty);
232            }
233        }
234        Property::Or(or) => {
235            for disjunct in &mut or.disjuncts {
236                replace_ty_args(disjunct, ty);
237            }
238        }
239    }
240}
241
242/// Replace `size_of`/`align_of` type arguments inside a numeric predicate.
243fn replace_pred_ty<'tcx>(pred: &mut NumericPredicate<'tcx>, ty: Ty<'tcx>) {
244    replace_expr_ty(&mut pred.lhs, ty);
245    replace_expr_ty(&mut pred.rhs, ty);
246}
247
248/// Replace `size_of`/`align_of` type arguments inside a contract expression.
249fn replace_expr_ty<'tcx>(expr: &mut ContractExpr<'tcx>, ty: Ty<'tcx>) {
250    match expr {
251        ContractExpr::SizeOf(t) | ContractExpr::AlignOf(t) => *t = ty,
252        ContractExpr::Len(inner) => replace_expr_ty(inner, ty),
253        ContractExpr::IndexAccess { slice, index } => {
254            replace_expr_ty(slice, ty);
255            replace_expr_ty(index, ty);
256        }
257        ContractExpr::Binary { lhs, rhs, .. } => {
258            replace_expr_ty(lhs, ty);
259            replace_expr_ty(rhs, ty);
260        }
261        ContractExpr::Unary { expr: inner, .. } => replace_expr_ty(inner, ty),
262        ContractExpr::If {
263            cond,
264            then_expr,
265            else_expr,
266        } => {
267            replace_pred_ty(cond, ty);
268            replace_expr_ty(then_expr, ty);
269            replace_expr_ty(else_expr, ty);
270        }
271        _ => {}
272    }
273}
274
275/// Check if a string looks like a numeric field access (e.g. "0").
276fn is_numeric_field_access(s: &str) -> bool {
277    let trimmed = s.trim();
278    !trimmed.is_empty()
279        && trimmed
280            .split('.')
281            .all(|part| !part.is_empty() && part.chars().all(|c| c.is_ascii_digit()))
282}
283
284/// Generate a normalised type path key for lookups in the type-invariants DB,
285/// together with the element type for the built-in slice entry.
286///
287/// ADTs map to their def path (e.g. `core::num::NonZero`); `&[T]` / `&mut [T]`
288/// slice references map to the built-in `[T]` key and carry their element type
289/// (resolved via `$elem` during instantiation); anything else falls back to the
290/// type's `Debug` representation.
291fn type_path_key<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>) -> (String, Option<Ty<'tcx>>) {
292    match ty.kind() {
293        rustc_middle::ty::TyKind::Adt(adt_def, substs) => {
294            let key = crate::helpers::name::public_def_path(tcx, adt_def.did());
295            // The first type argument is the element type for containers
296            // (`Vec<T>`/`String`); `$elem` in a container invariant resolves to
297            // it (unused by non-container entries like `NonNull`).
298            let elem_ty = substs.first().and_then(|s| s.as_type());
299            (key, elem_ty)
300        }
301        rustc_middle::ty::TyKind::Ref(_, inner, _) => match inner.kind() {
302            rustc_middle::ty::TyKind::Slice(elem) => ("[T]".to_string(), Some(*elem)),
303            _ => (format!("{ty:?}"), None),
304        },
305        _ => (format!("{ty:?}"), None),
306    }
307}
rapx/verify/type_invariants.rs

rapx/verify/
type_invariants.rs
