rapx/verify/contract/
assets.rs

1use rustc_hir::def_id::DefId;
2use rustc_middle::ty::TyCtxt;
3use serde::{Deserialize, Serialize};
4use std::collections::HashMap;
5use std::sync::OnceLock;
6
7use crate::helpers::name::get_cleaned_def_path_name;
8
9/// Structure of JSON entries.
10///
11/// When `tag == "any"` and `any` is present, the entry represents a
12/// disjunction (logical OR) of property groups.  Each element in `any`
13/// is either a single [`PropertyEntry`] (one disjunct) or an array of
14/// entries (a conjunction group — all must hold).
15///
16/// JSON format for `any` (flat OR):
17/// ```json
18/// {
19///   "tag": "any",
20///   "any": [
21///     {"tag": "Trait", "args": ["T", "Copy"]},
22///     {"tag": "Alias", "args": ["T", "return"]}
23///   ]
24/// }
25/// ```
26///
27/// JSON format for `any` with conjunction group (null-guard):
28/// ```json
29/// {
30///   "tag": "any",
31///   "any": [
32///     {"tag": "Null", "args": ["head"]},
33///     [
34///       {"tag": "Align", "args": ["head", "Node"]},
35///       {"tag": "ValidPtr", "args": ["head", "Node", "1"]}
36///     ]
37///   ]
38/// }
39/// ```
40#[derive(Debug, Serialize, Deserialize, Clone)]
41pub struct PropertyEntry {
42    pub tag: String,
43    #[serde(default)]
44    pub args: Vec<String>,
45    #[serde(default)]
46    pub kind: Option<String>,
47    /// When `tag == "any"`, the list of disjuncts (OR alternatives).
48    /// Each element is either a single entry or a conjunction group.
49    #[serde(default)]
50    pub any: Option<Vec<AnyItem>>,
51}
52
53/// One disjunct inside a JSON `any` entry.
54///
55/// `Single` is one property; `Group` is a conjunction of properties
56/// (all must hold together, forming one OR alternative).
57#[derive(Debug, Serialize, Deserialize, Clone)]
58#[serde(untagged)]
59pub enum AnyItem {
60    Single(PropertyEntry),
61    Group(Vec<PropertyEntry>),
62}
63
64/// Looks up backup contracts for a standard-library function by its normalized path.
65/// For trait-method impls, resolves to the trait method's path first so that
66/// all impls share the same contracts.
67///
68/// After exact-path lookup, falls back to wildcard patterns by progressively
69/// replacing the tail segment with `*`.  For example, for
70/// `core::slice::<impl [T]>::as_chunks`, the fallback chain is:
71///
72/// 1. `core::slice::<impl [T]>::as_chunks`  (exact)
73/// 2. `core::slice::<impl [T]>::*`          (all methods of `[T]`)
74/// 3. `core::slice::*`                      (all functions in slice module)
75/// 4. `core::*`                             (anything in core crate)
76pub fn get_std_contracts_from_assets(tcx: TyCtxt<'_>, def_id: DefId) -> &'static [PropertyEntry] {
77    let lookup_def_id = resolve_trait_method(tcx, def_id);
78    let cleaned_path_name = get_cleaned_def_path_name(tcx, lookup_def_id);
79    let db = get_std_contracts_from_json();
80
81    // Exact match first.
82    if let Some(entries) = db.get(&cleaned_path_name) {
83        return entries.as_slice();
84    }
85
86    // Strip intra-path type segments that appear in impl blocks.
87    // E.g. `core::slice::[T]::as_chunks_unchecked` → `core::slice::as_chunks_unchecked`.
88    {
89        let stripped: Vec<&str> = cleaned_path_name
90            .split("::")
91            .filter(|s| !s.starts_with('[') && !s.starts_with('<'))
92            .collect();
93        if stripped.len() != cleaned_path_name.matches("::").count() + 1 {
94            let stripped_path = stripped.join("::");
95            if let Some(entries) = db.get(&stripped_path) {
96                return entries.as_slice();
97            }
98        }
99    }
100
101    // Wildcard fallback: progressively replace tail segments with `*`.
102    let mut segments: Vec<&str> = cleaned_path_name.split("::").collect();
103    for i in (1..segments.len()).rev() {
104        segments[i] = "*";
105        if segments[i..].iter().all(|s| *s == "*") {
106            segments.truncate(i + 1);
107        }
108        let pattern = segments.join("::");
109        if let Some(entries) = db.get(&pattern) {
110            return entries.as_slice();
111        }
112    }
113
114    // Try bare `*` for any function.
115    if let Some(entries) = db.get("*") {
116        return entries.as_slice();
117    }
118
119    &[]
120}
121
122/// If `def_id` is a trait-method implementation, returns the corresponding
123/// trait method's [`DefId`]; otherwise returns `def_id` unchanged.
124fn resolve_trait_method(tcx: TyCtxt<'_>, def_id: DefId) -> DefId {
125    if let Some(assoc_item) = tcx.opt_associated_item(def_id) {
126        if let Some(trait_def_id) = assoc_item.trait_item_def_id() {
127            return trait_def_id;
128        }
129    }
130    def_id
131}
132
133/// Lazily loads the backup contract database for standard-library APIs.
134fn get_std_contracts_from_json() -> &'static HashMap<String, Vec<PropertyEntry>> {
135    static STD_CONTRACTS: OnceLock<HashMap<String, Vec<PropertyEntry>>> = OnceLock::new();
136    STD_CONTRACTS.get_or_init(|| {
137        serde_json::from_str(include_str!("assets/std-public-contracts.json"))
138            .unwrap_or_else(|err| panic!("failed to parse verify std contracts backup: {err}"))
139    })
140}
141
142/// Serialisation-friendly struct for the type-invariants JSON.
143#[derive(Debug, Serialize, Deserialize, Clone)]
144pub struct TypeInvariantEntry {
145    #[serde(default)]
146    pub comment: Option<String>,
147    pub invariants: Vec<PropertyEntry>,
148}
149
150/// Returns the std-type-invariants database, mapping a type path key
151/// (e.g. `"alloc::boxed::Box<T>"`) to its invariant entries.
152pub fn get_std_type_invariants() -> &'static HashMap<String, TypeInvariantEntry> {
153    static TYPE_INVARIANTS: OnceLock<HashMap<String, TypeInvariantEntry>> = OnceLock::new();
154    TYPE_INVARIANTS.get_or_init(|| {
155        serde_json::from_str(include_str!("assets/std-type-invariants.json"))
156            .unwrap_or_else(|err| panic!("failed to parse std type invariants: {err}"))
157    })
158}
rapx/verify/contract/assets.rs

rapx/verify/contract/
assets.rs
