rapx/verify/contract/
query.rs

1//! Centralized contract query service.
2//!
3//! Provides a unified API for querying safety contracts from all sources:
4//!
5//! 1. **Inline `#[rapx::requires(...)]` annotations** — highest priority, parsed
6//!    from HIR attributes.
7//! 2. **`#[rapx::ensures(...)]` on trait methods** — inherited by implementors
8//!    that lack their own annotations.
9//! 3. **Bundled JSON contracts** — embedded backup for standard-library unsafe
10//!    APIs without inline annotations.
11//! 4. **Chain resolution** — follows the call chain to find inherited contracts.
12//!
13//! Contract resolution priority (per `VerifyTargetCollector::get_fn_contracts`):
14//! a. Inline `#[rapx::requires]` on the callee.
15//! b. Trait method `#[rapx::requires]` (if the callee is a trait impl without its
16//!    own annotations).
17//! c. Bundled JSON contracts (for std callees).
18//! d. Recursive chain resolution (`resolve_chain_contracts`) — follows the call
19//!    chain to find inherited contracts.
20
21use rustc_hir::def_id::DefId;
22use rustc_middle::ty::TyCtxt;
23use safety_parser::syn::Expr;
24
25use super::assets::{AnyItem, PropertyEntry, get_std_contracts_from_assets};
26
27use super::types::{Property, PropertyKind};
28
29/// Convert a single [`PropertyEntry`] from JSON into the properties it denotes.
30///
31/// Resolves named parameter references (e.g. `"src"` → `"Arg_0"`), normalizes
32/// explicit JSON tokens (`arg:`, `const:`, `ty:`), and delegates to
33/// [`Property::parse_list`] for tag-based parsing.  A single entry may expand to
34/// several properties (via a compound `def` or `any`), hence the `Vec` return.
35pub fn entry_to_property<'tcx>(
36    tcx: TyCtxt<'tcx>,
37    def_id: DefId,
38    entry: &PropertyEntry,
39    param_names: &[String],
40    has_names: bool,
41) -> Vec<Property<'tcx>> {
42    if entry.tag == "any" {
43        if let Some(disjuncts) = &entry.any {
44            if disjuncts.len() >= 2 {
45                let mut prop = any_entry_to_property(tcx, def_id, disjuncts, param_names, has_names);
46                prop.apply_kind(entry.kind.as_deref());
47                return vec![prop];
48            }
49            rap_error!(
50                "JSON any entry requires at least 2 disjuncts, got {}",
51                disjuncts.len()
52            );
53            return Vec::new();
54        }
55        rap_error!("JSON any entry missing 'any' field");
56        return Vec::new();
57    }
58
59    let exprs = resolve_json_args(&entry.args, param_names, has_names, &entry.tag);
60    if exprs.len() != entry.args.len() {
61        rap_error!(
62            "Parse JSON API args error: Failed to parse arg '{:?}' for tag {}",
63            entry.args, entry.tag
64        );
65        return Vec::new();
66    }
67
68    let properties = Property::parse_list(tcx, def_id, entry.tag.as_str(), &exprs);
69    let mut result = Vec::new();
70    for mut property in properties {
71        property.apply_kind(entry.kind.as_deref());
72        if matches!(property.kind(), Some(PropertyKind::Unknown)) {
73            rap_debug!(
74                "skip unsupported std safety contract tag '{}' for callee {:?}",
75                entry.tag, def_id
76            );
77            continue;
78        }
79        result.push(property);
80    }
81    result
82}
83
84/// Parse an `any` disjunction entry from JSON into a `Property::Or` property.
85///
86/// Each element of `disjuncts` is an [`AnyItem`]:
87/// - `Single(entry)` → one-property disjunct
88/// - `Group(entries)` → conjunction group (all entries must hold for this disjunct)
89fn any_entry_to_property<'tcx>(
90    tcx: TyCtxt<'tcx>,
91    def_id: DefId,
92    disjuncts: &[AnyItem],
93    param_names: &[String],
94    has_names: bool,
95) -> Property<'tcx> {
96    let mut groups: Vec<Vec<Box<Property<'tcx>>>> = Vec::new();
97    for item in disjuncts {
98        match item {
99            AnyItem::Single(entry) => {
100                if entry.tag == "any" {
101                    rap_error!("Nested 'any' inside 'any' is not supported in JSON contracts");
102                    continue;
103                }
104                let exprs =
105                    resolve_json_args(&entry.args, param_names, has_names, &entry.tag);
106                if exprs.len() != entry.args.len() {
107                    rap_error!(
108                        "Parse any entry arg error: Failed to parse arg '{:?}' for tag {}",
109                        entry.args, entry.tag
110                    );
111                    continue;
112                }
113                let props = Property::parse_list(tcx, def_id, entry.tag.as_str(), &exprs);
114                let mut group: Vec<Box<Property<'tcx>>> = Vec::new();
115                for mut prop in props {
116                    prop.apply_kind(entry.kind.as_deref());
117                    group.push(Box::new(prop));
118                }
119                if !group.is_empty() {
120                    groups.push(group);
121                }
122            }
123            AnyItem::Group(entries) => {
124                let mut group: Vec<Box<Property<'tcx>>> = Vec::new();
125                for entry in entries {
126                    if entry.tag == "any" {
127                        rap_error!("Nested 'any' inside 'any' group is not supported");
128                        continue;
129                    }
130                    let exprs =
131                        resolve_json_args(&entry.args, param_names, has_names, &entry.tag);
132                    if exprs.len() != entry.args.len() {
133                        rap_error!(
134                            "Parse any group entry arg error: failed to parse '{:?}' for tag {}",
135                            entry.args, entry.tag
136                        );
137                        continue;
138                    }
139                    let props =
140                        Property::parse_list(tcx, def_id, entry.tag.as_str(), &exprs);
141                    for mut prop in props {
142                        prop.apply_kind(entry.kind.as_deref());
143                        group.push(Box::new(prop));
144                    }
145                }
146                if !group.is_empty() {
147                    groups.push(group);
148                }
149            }
150        }
151    }
152    Property::new_or(groups)
153}
154
155/// Resolve JSON contract argument strings to parsed [`syn::Expr`] values.
156///
157/// Handles:
158/// - Named parameter resolution (e.g. `"src"` → `"arg:0"`)
159/// - Explicit token normalization (`arg:`, `const:`, `ty:` prefixes)
160/// - Lifetime stripping (`'a` → `a`)
161pub fn resolve_json_args(
162    args: &[String],
163    param_names: &[String],
164    has_names: bool,
165    tag: &str,
166) -> Vec<Expr> {
167    let mut exprs: Vec<Expr> = Vec::new();
168    for arg_str in args {
169        let resolved = if has_names {
170            resolve_json_param_name(arg_str, param_names)
171        } else {
172            arg_str.clone()
173        };
174        let normalized_arg = normalize_json_contract_arg(&resolved);
175        match syn::parse_str::<Expr>(&normalized_arg) {
176            Ok(expr) => exprs.push(expr),
177            Err(_) => {
178                if let Some(lifetime) = normalized_arg.strip_prefix('\'') {
179                    if lifetime.chars().all(|c| c.is_alphabetic() || c == '_') {
180                        match syn::parse_str::<Expr>(lifetime) {
181                            Ok(expr) => exprs.push(expr),
182                            Err(_) => {
183                                rap_error!(
184                                    "JSON Contract Error: Failed to parse lifetime \
185                                     '{}' as Rust Expr for tag {}",
186                                    arg_str, tag
187                                );
188                            }
189                        }
190                    } else {
191                        rap_error!(
192                            "JSON Contract Error: Failed to parse arg '{}' as Rust Expr for tag {}",
193                            arg_str, tag
194                        );
195                    }
196                } else {
197                    rap_error!(
198                        "JSON Contract Error: Failed to parse arg '{}' as Rust Expr for tag {}",
199                        arg_str, tag
200                    );
201                }
202            }
203        }
204    }
205    exprs
206}
207
208/// Resolve a simple parameter-name reference in a JSON contract arg string to
209/// the `arg:N` positional form.  Complex expressions (containing function
210/// calls, field access, etc.) are left unchanged — they are handled later by
211/// the expression parser which already knows how to resolve named parameters.
212pub fn resolve_json_param_name(arg: &str, param_names: &[String]) -> String {
213    if arg.starts_with("arg:")
214        || arg.starts_with("const:")
215        || arg.starts_with("ty:")
216        || arg.contains('(')
217        || arg.contains('.')
218        || arg.contains("::")
219        || arg.contains(' ')
220        || arg.starts_with('\'')
221    {
222        return arg.to_string();
223    }
224    if let Some(pos) = param_names.iter().position(|n| n == arg) {
225        format!("arg:{pos}")
226    } else {
227        arg.to_string()
228    }
229}
230
231/// Convert explicit JSON contract tokens into the expression syntax accepted by
232/// the existing property parser.
233///
234/// Supported explicit tokens:
235/// - `arg:N` names callee argument `N` and becomes internal `Arg_N`.
236/// - `const:N` names an integer constant and becomes `N`.
237/// - `ty:T` names a type parameter/type identifier and becomes `T`.
238///
239/// Unprefixed strings are kept unchanged for compatibility with older entries
240/// such as `"0"`, `"T"`, and `"1"`.
241pub fn normalize_json_contract_arg(arg: &str) -> String {
242    let bytes = arg.as_bytes();
243    let mut out = String::with_capacity(arg.len());
244    let mut i = 0;
245
246    while i < bytes.len() {
247        if arg[i..].starts_with("arg:") {
248            let start = i + "arg:".len();
249            let end = scan_while(arg, start, |ch| ch.is_ascii_digit());
250            if end > start {
251                out.push_str("Arg_");
252                out.push_str(&arg[start..end]);
253                i = end;
254                continue;
255            }
256        }
257
258        if arg[i..].starts_with("const:") {
259            let start = i + "const:".len();
260            let end = scan_while(arg, start, is_contract_token_char);
261            if end > start {
262                out.push_str(&arg[start..end]);
263                i = end;
264                continue;
265            }
266        }
267
268        if arg[i..].starts_with("ty:") {
269            let start = i + "ty:".len();
270            let end = scan_while(arg, start, is_contract_token_char);
271            if end > start {
272                out.push_str(&arg[start..end]);
273                i = end;
274                continue;
275            }
276        }
277
278        let ch = arg[i..].chars().next().unwrap();
279        out.push(ch);
280        i += ch.len_utf8();
281    }
282
283    out
284}
285
286fn scan_while(arg: &str, mut index: usize, predicate: impl Fn(char) -> bool) -> usize {
287    while index < arg.len() {
288        let ch = arg[index..].chars().next().unwrap();
289        if !predicate(ch) {
290            break;
291        }
292        index += ch.len_utf8();
293    }
294    index
295}
296
297fn is_contract_token_char(ch: char) -> bool {
298    ch.is_ascii_alphanumeric() || ch == '_' || ch == ':'
299}
300
301/// Query contracts for a function from the bundled JSON backup database.
302///
303/// Uses [`get_std_contracts_from_assets`] for lookup with wildcard fallback,
304/// then parses each entry into a [`Property`] via [`entry_to_property`].
305pub fn query_json_contracts<'tcx>(
306    tcx: TyCtxt<'tcx>,
307    def_id: DefId,
308) -> Vec<Property<'tcx>> {
309    let entries = get_std_contracts_from_assets(tcx, def_id);
310    if entries.is_empty() {
311        return Vec::new();
312    }
313    let (param_names, _) = crate::helpers::name::parse_signature(tcx, def_id);
314    let has_names =
315        !param_names.is_empty() && !param_names[0].chars().all(|c| c.is_ascii_digit());
316
317    let mut results = Vec::new();
318    for entry in entries {
319        results.extend(entry_to_property(tcx, def_id, entry, &param_names, has_names));
320    }
321    results
322}
rapx/verify/contract/query.rs

rapx/verify/contract/
query.rs
