rapx/verify/attribute/
assets_parser.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::verify::helpers::get_cleaned_def_path_name;
8
9/// Structure of JSON entries.
10///
11#[derive(Debug, Serialize, Deserialize, Clone)]
12pub struct PropertyEntry {
13    pub tag: String,
14    pub args: Vec<String>,
15}
16
17/// Looks up backup contracts for a standard-library function by its normalized path.
18/// For trait-method impls, resolves to the trait method's path first so that
19/// all impls share the same contracts.
20///
21/// After exact-path lookup, falls back to wildcard patterns by progressively
22/// replacing the tail segment with `*`.  For example, for
23/// `core::slice::<impl [T]>::as_chunks`, the fallback chain is:
24///
25/// 1. `core::slice::<impl [T]>::as_chunks`  (exact)
26/// 2. `core::slice::<impl [T]>::*`          (all methods of `[T]`)
27/// 3. `core::slice::*`                      (all functions in slice module)
28/// 4. `core::*`                             (anything in core crate)
29pub fn get_std_contracts_from_assets(tcx: TyCtxt<'_>, def_id: DefId) -> &'static [PropertyEntry] {
30    let lookup_def_id = resolve_trait_method(tcx, def_id);
31    let cleaned_path_name = get_cleaned_def_path_name(tcx, lookup_def_id);
32    let db = get_std_contracts_from_json();
33
34    // Exact match first.
35    if let Some(entries) = db.get(&cleaned_path_name) {
36        return entries.as_slice();
37    }
38
39    // Strip intra-path type segments that appear in impl blocks.
40    // E.g. `core::slice::[T]::as_chunks_unchecked` → `core::slice::as_chunks_unchecked`.
41    {
42        let stripped: Vec<&str> = cleaned_path_name
43            .split("::")
44            .filter(|s| !s.starts_with('[') && !s.starts_with('<'))
45            .collect();
46        if stripped.len() != cleaned_path_name.matches("::").count() + 1 {
47            let stripped_path = stripped.join("::");
48            if let Some(entries) = db.get(&stripped_path) {
49                return entries.as_slice();
50            }
51        }
52    }
53
54    // Wildcard fallback: progressively replace tail segments with `*`.
55    let mut segments: Vec<&str> = cleaned_path_name.split("::").collect();
56    for i in (1..segments.len()).rev() {
57        segments[i] = "*";
58        if segments[i..].iter().all(|s| *s == "*") {
59            segments.truncate(i + 1);
60        }
61        let pattern = segments.join("::");
62        if let Some(entries) = db.get(&pattern) {
63            return entries.as_slice();
64        }
65    }
66
67    // Try bare `*` for any function.
68    if let Some(entries) = db.get("*") {
69        return entries.as_slice();
70    }
71
72    &[]
73}
74
75/// If `def_id` is a trait-method implementation, returns the corresponding
76/// trait method's [`DefId`]; otherwise returns `def_id` unchanged.
77fn resolve_trait_method(tcx: TyCtxt<'_>, def_id: DefId) -> DefId {
78    if let Some(assoc_item) = tcx.opt_associated_item(def_id) {
79        if let Some(trait_def_id) = assoc_item.trait_item_def_id() {
80            return trait_def_id;
81        }
82    }
83    def_id
84}
85
86/// Lazily loads the backup contract database for standard-library APIs.
87fn get_std_contracts_from_json() -> &'static HashMap<String, Vec<PropertyEntry>> {
88    static STD_CONTRACTS: OnceLock<HashMap<String, Vec<PropertyEntry>>> = OnceLock::new();
89    STD_CONTRACTS.get_or_init(|| {
90        let raw = include_str!("assets/std-public-contracts.json");
91        let normalized = normalize_json_trailing_commas(raw);
92        serde_json::from_str(normalized.as_str())
93            .unwrap_or_else(|err| panic!("failed to parse verify std contracts backup: {err}"))
94    })
95}
96
97/// Removes trailing commas that appear immediately before `}` or `]` in JSON text.
98///
99/// This allows the embedded backup JSON file to remain slightly permissive while
100/// still being parsed by `serde_json`.
101fn normalize_json_trailing_commas(input: &str) -> String {
102    let mut normalized = String::with_capacity(input.len());
103    let mut iter = input.char_indices().peekable();
104
105    while let Some((_, ch)) = iter.next() {
106        if ch == ',' {
107            let mut lookahead = iter.clone();
108            while let Some((_, next_ch)) = lookahead.peek() {
109                if next_ch.is_whitespace() {
110                    lookahead.next();
111                } else {
112                    break;
113                }
114            }
115            if let Some((_, next_ch)) = lookahead.peek()
116                && (*next_ch == '}' || *next_ch == ']')
117            {
118                continue;
119            }
120        }
121        normalized.push(ch);
122    }
123
124    normalized
125}
rapx/verify/attribute/assets_parser.rs

rapx/verify/attribute/
assets_parser.rs
