rapx/verify/
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 super::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.
18pub fn get_std_contracts_from_assets(tcx: TyCtxt<'_>, def_id: DefId) -> &'static [PropertyEntry] {
19    let cleaned_path_name = get_cleaned_def_path_name(tcx, def_id);
20    get_std_contracts_from_json()
21        .get(&cleaned_path_name)
22        .map(Vec::as_slice)
23        .unwrap_or(&[])
24}
25
26/// Lazily loads the backup contract database for standard-library APIs.
27fn get_std_contracts_from_json() -> &'static HashMap<String, Vec<PropertyEntry>> {
28    static STD_CONTRACTS: OnceLock<HashMap<String, Vec<PropertyEntry>>> = OnceLock::new();
29    STD_CONTRACTS.get_or_init(|| {
30        let raw = include_str!("assets/std-contracts.json");
31        let normalized = normalize_json_trailing_commas(raw);
32        serde_json::from_str(normalized.as_str())
33            .unwrap_or_else(|err| panic!("failed to parse verify std contracts backup: {err}"))
34    })
35}
36
37/// Removes trailing commas that appear immediately before `}` or `]` in JSON text.
38///
39/// This allows the embedded backup JSON file to remain slightly permissive while
40/// still being parsed by `serde_json`.
41fn normalize_json_trailing_commas(input: &str) -> String {
42    let mut normalized = String::with_capacity(input.len());
43    let mut iter = input.char_indices().peekable();
44
45    while let Some((_, ch)) = iter.next() {
46        if ch == ',' {
47            let mut lookahead = iter.clone();
48            while let Some((_, next_ch)) = lookahead.peek() {
49                if next_ch.is_whitespace() {
50                    lookahead.next();
51                } else {
52                    break;
53                }
54            }
55            if let Some((_, next_ch)) = lookahead.peek()
56                && (*next_ch == '}' || *next_ch == ']')
57            {
58                continue;
59            }
60        }
61        normalized.push(ch);
62    }
63
64    normalized
65}
rapx/verify/assets_parser.rs

rapx/verify/
assets_parser.rs
