Skip to content

Commit 4a928ea

Browse files
authored
Merge pull request #34 from os-checker/cache
Feat: Cache StableMir results and basic compiler ctx
2 parents bb66bd9 + 8f88b51 commit 4a928ea

File tree

16 files changed

+2878
-2811
lines changed

16 files changed

+2878
-2811
lines changed

src/functions/cache.rs

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
//! Access cached data from local thread set for the given Instance.
2+
//! If the data hasn't been available, generate one and insert it.
3+
//! The data is always behind a borrow through the `get_*` callbacks.
4+
5+
use super::utils::{SourceCode, source_code_with};
6+
use rustc_data_structures::fx::FxHashMap;
7+
use rustc_middle::ty::TyCtxt;
8+
use rustc_span::source_map::{SourceMap, get_source_map};
9+
use stable_mir::{
10+
CrateDef, DefId,
11+
mir::{Body, mono::Instance},
12+
};
13+
use std::{cell::RefCell, cmp::Ordering, sync::Arc};
14+
15+
thread_local! {
16+
static CACHE: RefCell<Cache> = RefCell::new(Cache::new());
17+
}
18+
19+
pub fn set_rustc_ctx(tcx: TyCtxt) {
20+
// Safety: TyCtxt<'short> is extended to TyCtxt<'static>,
21+
// and we only use TyCtxt<'static> in stable_mir's callback.
22+
let tcx = unsafe { std::mem::transmute::<TyCtxt<'_>, TyCtxt<'static>>(tcx) };
23+
let src_map = get_source_map().expect("No source map.");
24+
let rustc = RustcCxt { tcx, src_map };
25+
CACHE.with(|c| c.borrow_mut().rustc = Some(rustc));
26+
}
27+
28+
pub fn clear_rustc_ctx() {
29+
CACHE.with(|c| c.borrow_mut().rustc = None);
30+
}
31+
32+
fn get_cache<T>(f: impl FnOnce(&mut Cache) -> T) -> T {
33+
CACHE.with(|c| f(&mut c.borrow_mut()))
34+
}
35+
36+
fn get_cache_func<T>(inst: &Instance, f: impl FnOnce(&CacheFunction) -> T) -> Option<T> {
37+
get_cache(|cache| cache.get_or_insert(inst).map(f))
38+
}
39+
40+
pub fn get_body<T>(inst: &Instance, f: impl FnOnce(&Body) -> T) -> Option<T> {
41+
get_cache_func(inst, |cf| f(&cf.body))
42+
}
43+
44+
pub fn get_source_code(inst: &Instance) -> Option<SourceCode> {
45+
get_cache_func(inst, |cf| cf.src.clone())
46+
}
47+
48+
pub fn cmp_callees(a: &Instance, b: &Instance) -> Ordering {
49+
get_cache(|cache| {
50+
cache.get_or_insert(a);
51+
cache.get_or_insert(b);
52+
let func_a = cache.set.get(&a.def.def_id()).unwrap().as_ref().map(|f| &f.src);
53+
let func_b = cache.set.get(&b.def.def_id()).unwrap().as_ref().map(|f| &f.src);
54+
func_a.cmp(&func_b)
55+
})
56+
}
57+
58+
struct Cache {
59+
set: FxHashMap<DefId, Option<CacheFunction>>,
60+
rustc: Option<RustcCxt>,
61+
path_prefixes: PathPrefixes,
62+
}
63+
64+
impl Cache {
65+
fn new() -> Self {
66+
let (set, rustc) = Default::default();
67+
let path_prefixes = PathPrefixes::new();
68+
Cache { set, rustc, path_prefixes }
69+
}
70+
71+
fn get_or_insert(&mut self, inst: &Instance) -> Option<&CacheFunction> {
72+
self.set
73+
.entry(inst.def.def_id())
74+
.or_insert_with(|| {
75+
let body = inst.body()?;
76+
let rustc = self.rustc.as_ref()?;
77+
let prefix = self.path_prefixes.prefixes();
78+
let src = source_code_with(body.span, rustc.tcx, &rustc.src_map, prefix);
79+
Some(CacheFunction { body, src })
80+
})
81+
.as_ref()
82+
}
83+
}
84+
85+
struct RustcCxt {
86+
tcx: TyCtxt<'static>,
87+
src_map: Arc<SourceMap>,
88+
}
89+
90+
struct CacheFunction {
91+
body: Body,
92+
src: SourceCode,
93+
}
94+
95+
struct PathPrefixes {
96+
pwd: String,
97+
sysroot: String,
98+
}
99+
100+
impl PathPrefixes {
101+
fn new() -> Self {
102+
let mut pwd = std::env::current_dir().unwrap().into_os_string().into_string().unwrap();
103+
pwd.push('/');
104+
105+
let out = std::process::Command::new("rustc").arg("--print=sysroot").output().unwrap();
106+
let sysroot = std::str::from_utf8(&out.stdout).unwrap().trim();
107+
let sysroot = format!("{sysroot}/lib/rustlib/src/rust/");
108+
PathPrefixes { pwd, sysroot }
109+
}
110+
111+
fn prefixes(&self) -> [&str; 2] {
112+
[&*self.pwd, &self.sysroot]
113+
}
114+
}

src/functions/kani/reachability.rs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,6 @@
1717
//! Note that this is a copy of `reachability.rs` that uses StableMIR but the public APIs are still
1818
//! kept with internal APIs.
1919
20-
extern crate rustc_data_structures;
21-
extern crate rustc_session;
22-
2320
use super::coercion;
2421
use indexmap::IndexSet;
2522
use rustc_data_structures::fingerprint::Fingerprint;

src/functions/mod.rs

Lines changed: 12 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,22 @@
11
use indexmap::IndexSet;
22
use kani::{CallGraph, KANI_TOOL_ATTRS, collect_reachable_items};
33
use rustc_middle::ty::TyCtxt;
4-
use rustc_span::source_map::SourceMap;
54
use stable_mir::{
65
CrateDef,
76
crate_def::Attribute,
8-
mir::{
9-
Body,
10-
mono::{Instance, MonoItem},
11-
},
7+
mir::mono::{Instance, MonoItem},
128
};
139

10+
mod cache;
11+
pub use cache::{clear_rustc_ctx, set_rustc_ctx};
12+
1413
mod kani;
14+
mod utils;
15+
1516
mod serialization;
1617
pub use serialization::SerFunction;
17-
mod utils;
1818

19-
pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<SerFunction> {
19+
pub fn analyze(tcx: TyCtxt) -> Vec<SerFunction> {
2020
let local_items = stable_mir::all_local_items();
2121
let cap = local_items.len();
2222

@@ -34,8 +34,8 @@ pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<SerFunction> {
3434
// Filter out non kanitool functions.
3535
let mut proofs: Vec<_> = mono_items
3636
.iter()
37-
.filter_map(|f| Function::new(f, &callgraph, tcx, src_map, |x| !x.attrs.is_empty()))
38-
.map(|fun| SerFunction::new(fun, tcx, src_map))
37+
.filter_map(|f| Function::new(f, &callgraph, |x| !x.attrs.is_empty()))
38+
.map(SerFunction::new)
3939
.collect();
4040
// Sort proofs by file path and source code.
4141
proofs.sort_by(|a, b| a.cmp_by_file_and_func(b));
@@ -51,9 +51,6 @@ pub struct Function {
5151
/// kanitool's attributs.
5252
attrs: Vec<Attribute>,
5353

54-
/// Function body.
55-
body: Body,
56-
5754
/// Recursive fnction calls inside the body.
5855
/// The elements are sorted by file path and fn source code to keep hash value stable.
5956
callees: IndexSet<Instance>,
@@ -63,8 +60,6 @@ impl Function {
6360
pub fn new(
6461
item: &MonoItem,
6562
callgraph: &CallGraph,
66-
tcx: TyCtxt,
67-
src_map: &SourceMap,
6863
filter: impl FnOnce(&Self) -> bool,
6964
) -> Option<Self> {
7065
// Skip non fn items
@@ -73,16 +68,16 @@ impl Function {
7368
};
7469

7570
// Skip if no body.
76-
let body = instance.body()?;
71+
cache::get_body(&instance, |_| ())?;
7772

7873
// Only need kanitool attrs: proof, proof_for_contract, contract, ...
7974
let attrs = KANI_TOOL_ATTRS.iter().flat_map(|v| instance.def.tool_attrs(v)).collect();
8075

8176
let mut callees = IndexSet::new();
8277
callgraph.recursive_callees(item, &mut callees);
83-
callees.sort_by(|a, b| utils::cmp_callees(a, b, tcx, src_map));
78+
callees.sort_by(cache::cmp_callees);
8479

85-
let this = Function { instance, attrs, body, callees };
80+
let this = Function { instance, attrs, callees };
8681
filter(&this).then_some(this)
8782
}
8883
}

src/functions/serialization.rs

Lines changed: 9 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,4 @@
1-
use super::utils::{self, SourceCode};
2-
use rustc_middle::ty::TyCtxt;
3-
use rustc_span::source_map::SourceMap;
1+
use super::{cache, utils::SourceCode};
42
use rustc_stable_hash::{FromStableHash, SipHasher128Hash, StableHasher, hashers::SipHasher128};
53
use serde::Serialize;
64
use stable_mir::{CrateDef, mir::mono::Instance};
@@ -12,9 +10,6 @@ pub struct SerFunction {
1210
hash: String,
1311
/// DefId in stable_mir.
1412
def_id: String,
15-
/// Every funtion must be declared in a specific file, even for those
16-
/// generated by macros.
17-
file: String,
1813
/// Attributes are attached the function, but it seems that attributes
1914
/// and function must be separated to query.
2015
attrs: Vec<String>,
@@ -25,34 +20,31 @@ pub struct SerFunction {
2520
}
2621

2722
impl SerFunction {
28-
pub fn new(fun: super::Function, tcx: TyCtxt, src_map: &SourceMap) -> Self {
23+
pub fn new(fun: super::Function) -> Self {
2924
let inst = fun.instance;
3025
let def_id = format_def_id(&inst);
31-
let file = utils::file_path(&inst);
3226
let attrs: Vec<_> = fun.attrs.iter().map(|a| a.as_str().to_owned()).collect();
3327
// Though this is from body span, fn name and signature are included.
34-
let func = utils::source_code_with(fun.body.span, tcx, src_map);
35-
let callees: Vec<_> = fun.callees.iter().map(|x| Callee::new(x, tcx, src_map)).collect();
28+
let func = cache::get_source_code(&inst).unwrap_or_default();
29+
let callees: Vec<_> = fun.callees.iter().map(Callee::new).collect();
3630

3731
// Hash
3832
let mut hasher = StableHasher::<SipHasher128>::new();
39-
hasher.write_str(&file);
4033
func.with_hasher(&mut hasher);
4134
hasher.write_length_prefix(attrs.len());
4235
attrs.iter().for_each(|a| hasher.write_str(a));
4336
hasher.write_length_prefix(callees.len());
4437
callees.iter().for_each(|c| {
45-
hasher.write_str(&c.file);
4638
c.func.with_hasher(&mut hasher);
4739
});
4840
let Hash128(hash) = hasher.finish();
4941

50-
SerFunction { hash, def_id, file, attrs, func, callees }
42+
SerFunction { hash, def_id, attrs, func, callees }
5143
}
5244

5345
/// Compare by file and func string.
5446
pub fn cmp_by_file_and_func(&self, other: &Self) -> Ordering {
55-
(&*self.file, &self.func).cmp(&(&*other.file, &other.func))
47+
self.func.cmp(&other.func)
5648
}
5749
}
5850

@@ -75,15 +67,13 @@ fn format_def_id(inst: &Instance) -> String {
7567
#[derive(Debug, Serialize)]
7668
pub struct Callee {
7769
def_id: String,
78-
file: String,
7970
func: SourceCode,
8071
}
8172

8273
impl Callee {
83-
fn new(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Self {
74+
fn new(inst: &Instance) -> Self {
8475
let def_id = format_def_id(inst);
85-
let file = utils::file_path(inst);
86-
let func = utils::source_code_of_body(inst, tcx, src_map).unwrap_or_default();
87-
Callee { def_id, file, func }
76+
let func = cache::get_source_code(inst).unwrap_or_default();
77+
Callee { def_id, func }
8878
}
8979
}

src/functions/utils.rs

Lines changed: 24 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -3,24 +3,29 @@ use rustc_smir::rustc_internal::internal;
33
use rustc_span::{Span, source_map::SourceMap};
44
use rustc_stable_hash::{StableHasher, hashers::SipHasher128};
55
use serde::Serialize;
6-
use stable_mir::{CrateDef, mir::mono::Instance};
7-
use std::{cmp::Ordering, hash::Hasher};
6+
use std::hash::Hasher;
87

98
/// Source code and potential source code before expansion.
109
///
11-
/// Refer to
12-
#[derive(Debug, Serialize, PartialEq, Eq, PartialOrd, Ord, Default)]
10+
/// The field order matters, since this struct implements Ord.
11+
#[derive(Clone, Debug, Serialize, PartialEq, Eq, PartialOrd, Ord, Default)]
1312
pub struct SourceCode {
14-
// TODO:
15-
// file: String,
16-
//
13+
// A file path where src lies.
14+
// The path is stripped with pwd or sysroot prefix.
15+
pub file: String,
16+
1717
/// Source that a stable_mir span points to.
1818
pub src: String,
19+
1920
/// Is the stable_mir span from a macro expansion?
2021
/// If it is from an expansion, what's the source code before expansion?
2122
/// * Some(_) happens when the src (stable_mir) span comes from expansion, and tells
2223
/// the source before the expansion.
2324
/// * None if the src is not from a macro expansion.
25+
///
26+
/// Refer to [#31] to know sepecific cases.
27+
///
28+
/// [#31]: https://github.com/os-checker/distributed-verification/issues/31
2429
pub before_expansion: Option<String>,
2530
}
2631

@@ -47,65 +52,27 @@ fn span_to_source(span: Span, src_map: &SourceMap) -> String {
4752
.unwrap()
4853
}
4954

50-
/// Source code for a span.
51-
fn source_code(span: Span, src_map: &SourceMap) -> SourceCode {
52-
let src = span_to_source(span, src_map);
53-
let before_expansion = span.from_expansion().then(|| {
54-
let ancestor_span = span.find_oldest_ancestor_in_same_ctxt();
55-
span_to_source(ancestor_span, src_map)
56-
});
57-
SourceCode { src, before_expansion }
58-
}
59-
6055
/// Source code for a stable_mir span.
6156
pub fn source_code_with(
6257
stable_mir_span: stable_mir::ty::Span,
6358
tcx: TyCtxt,
6459
src_map: &SourceMap,
60+
path_prefixes: [&str; 2],
6561
) -> SourceCode {
6662
let span = internal(tcx, stable_mir_span);
67-
source_code(span, src_map)
68-
}
69-
70-
// FIXME: takes body and returns SourceCode
71-
pub fn source_code_of_body(
72-
inst: &Instance,
73-
tcx: TyCtxt,
74-
src_map: &SourceMap,
75-
) -> Option<SourceCode> {
76-
inst.body().map(|body| source_code_with(body.span, tcx, src_map))
77-
}
78-
79-
pub fn cmp_callees(a: &Instance, b: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Ordering {
80-
let filename_a = file_path(a);
81-
let filename_b = file_path(b);
82-
match filename_a.cmp(&filename_b) {
83-
Ordering::Equal => (),
84-
ord => return ord,
85-
}
86-
87-
let body_a = source_code_of_body(a, tcx, src_map);
88-
let body_b = source_code_of_body(b, tcx, src_map);
89-
body_a.cmp(&body_b)
90-
}
91-
92-
pub fn file_path(inst: &Instance) -> String {
93-
use std::sync::LazyLock;
94-
static PREFIXES: LazyLock<[String; 2]> = LazyLock::new(|| {
95-
let mut pwd = std::env::current_dir().unwrap().into_os_string().into_string().unwrap();
96-
pwd.push('/');
97-
98-
let out = std::process::Command::new("rustc").arg("--print=sysroot").output().unwrap();
99-
let sysroot = std::str::from_utf8(&out.stdout).unwrap().trim();
100-
let sysroot = format!("{sysroot}/lib/rustlib/src/rust/");
101-
[pwd, sysroot]
63+
let src = span_to_source(span, src_map);
64+
let before_expansion = span.from_expansion().then(|| {
65+
let ancestor_span = span.find_oldest_ancestor_in_same_ctxt();
66+
span_to_source(ancestor_span, src_map)
10267
});
10368

104-
let file = inst.def.span().get_filename();
105-
for prefix in &*PREFIXES {
106-
if let Some(file) = file.strip_prefix(prefix) {
107-
return file.to_owned();
69+
let mut file = stable_mir_span.get_filename();
70+
for prefix in path_prefixes {
71+
if let Some(file_stripped) = file.strip_prefix(prefix) {
72+
file = file_stripped.to_owned();
73+
break;
10874
}
10975
}
110-
file
76+
77+
SourceCode { file, src, before_expansion }
11178
}

0 commit comments

Comments
 (0)