Skip to content

Commit bb66bd9

Browse files
authored
Merge pull request #32 from os-checker/test-macro-expansion
Feat: support spans on macro expansion
2 parents 1c0a6f9 + 561af07 commit bb66bd9

17 files changed

+12245
-3841
lines changed

kani

Submodule kani updated 96 files

src/functions/mod.rs

Lines changed: 25 additions & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,20 @@
11
use indexmap::IndexSet;
22
use kani::{CallGraph, KANI_TOOL_ATTRS, collect_reachable_items};
33
use rustc_middle::ty::TyCtxt;
4-
use rustc_smir::rustc_internal::internal;
5-
use rustc_span::{Span, source_map::SourceMap};
4+
use rustc_span::source_map::SourceMap;
65
use stable_mir::{
7-
CrateDef, DefId,
6+
CrateDef,
87
crate_def::Attribute,
9-
mir::mono::{Instance, MonoItem},
10-
ty::{FnDef, RigidTy, Ty, TyKind},
8+
mir::{
9+
Body,
10+
mono::{Instance, MonoItem},
11+
},
1112
};
12-
use std::cmp::Ordering;
1313

1414
mod kani;
1515
mod serialization;
1616
pub use serialization::SerFunction;
17+
mod utils;
1718

1819
pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<SerFunction> {
1920
let local_items = stable_mir::all_local_items();
@@ -34,25 +35,25 @@ pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<SerFunction> {
3435
let mut proofs: Vec<_> = mono_items
3536
.iter()
3637
.filter_map(|f| Function::new(f, &callgraph, tcx, src_map, |x| !x.attrs.is_empty()))
38+
.map(|fun| SerFunction::new(fun, tcx, src_map))
3739
.collect();
3840
// Sort proofs by file path and source code.
39-
proofs.sort_by(|a, b| (&*a.file, &*a.func).cmp(&(&*b.file, &*b.func)));
40-
proofs.into_iter().map(|fun| SerFunction::new(fun, tcx, src_map)).collect()
41+
proofs.sort_by(|a, b| a.cmp_by_file_and_func(b));
42+
proofs
4143
}
4244

4345
/// A Rust funtion with its file source, attributes, and raw function content.
4446
#[derive(Debug)]
4547
pub struct Function {
46-
/// DefId in stable_mir.
47-
def_id: DefId,
48-
/// Every funtion must be declared in a specific file, even for those
49-
/// generated by macros.
50-
file: String,
51-
/// Attributes are attached the function, but it seems that attributes
52-
/// and function must be separated to query.
48+
/// Instance of the function.
49+
instance: Instance,
50+
51+
/// kanitool's attributs.
5352
attrs: Vec<Attribute>,
54-
/// Raw function string, including name, signature, and body.
55-
func: String,
53+
54+
/// Function body.
55+
body: Body,
56+
5657
/// Recursive fnction calls inside the body.
5758
/// The elements are sorted by file path and fn source code to keep hash value stable.
5859
callees: IndexSet<Instance>,
@@ -66,98 +67,22 @@ impl Function {
6667
src_map: &SourceMap,
6768
filter: impl FnOnce(&Self) -> bool,
6869
) -> Option<Self> {
69-
// skip non fn items
70-
let &MonoItem::Fn(inst) = item else {
70+
// Skip non fn items
71+
let &MonoItem::Fn(instance) = item else {
7172
return None;
7273
};
7374

74-
let inst_def = inst.def;
75+
// Skip if no body.
76+
let body = instance.body()?;
7577

7678
// Only need kanitool attrs: proof, proof_for_contract, contract, ...
77-
let attrs = KANI_TOOL_ATTRS.iter().flat_map(|v| inst_def.tool_attrs(v)).collect();
78-
79-
let span = inst_def.span();
80-
let file = file_path(&inst);
81-
82-
let fn_def = ty_to_fndef(inst.ty())?;
83-
let body = fn_def.body()?;
79+
let attrs = KANI_TOOL_ATTRS.iter().flat_map(|v| instance.def.tool_attrs(v)).collect();
8480

8581
let mut callees = IndexSet::new();
8682
callgraph.recursive_callees(item, &mut callees);
87-
callees.sort_by(|a, b| cmp_callees(a, b, tcx, src_map));
88-
89-
let func = source_code_with(body.span, tcx, src_map);
90-
info!(" - {:?} ({span:?}): {func}", inst_def.name());
83+
callees.sort_by(|a, b| utils::cmp_callees(a, b, tcx, src_map));
9184

92-
let def_id = inst_def.def_id();
93-
let this = Function { def_id, file, attrs, func, callees };
85+
let this = Function { instance, attrs, body, callees };
9486
filter(&this).then_some(this)
9587
}
9688
}
97-
98-
/// Extract FnDef from Ty.
99-
fn ty_to_fndef(ty: Ty) -> Option<FnDef> {
100-
let TyKind::RigidTy(RigidTy::FnDef(fn_def, _)) = ty.kind() else {
101-
return None;
102-
};
103-
Some(fn_def)
104-
}
105-
106-
/// Source code for a span.
107-
fn source_code(span: Span, src_map: &SourceMap) -> String {
108-
src_map
109-
.span_to_source(span, |text, x, y| {
110-
let src = &text[x..y];
111-
debug!("[{x}:{y}]\n{src}");
112-
Ok(src.to_owned())
113-
})
114-
.unwrap()
115-
}
116-
117-
/// Source code for a stable_mir span.
118-
fn source_code_with(
119-
stable_mir_span: stable_mir::ty::Span,
120-
tcx: TyCtxt,
121-
src_map: &SourceMap,
122-
) -> String {
123-
let span = internal(tcx, stable_mir_span);
124-
source_code(span, src_map)
125-
}
126-
127-
fn source_code_of_body(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Option<String> {
128-
inst.body().map(|body| source_code_with(body.span, tcx, src_map))
129-
}
130-
131-
fn cmp_callees(a: &Instance, b: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Ordering {
132-
let filename_a = file_path(a);
133-
let filename_b = file_path(b);
134-
match filename_a.cmp(&filename_b) {
135-
Ordering::Equal => (),
136-
ord => return ord,
137-
}
138-
139-
let body_a = source_code_of_body(a, tcx, src_map);
140-
let body_b = source_code_of_body(b, tcx, src_map);
141-
body_a.cmp(&body_b)
142-
}
143-
144-
fn file_path(inst: &Instance) -> String {
145-
use std::sync::LazyLock;
146-
static PREFIXES: LazyLock<[String; 2]> = LazyLock::new(|| {
147-
let mut pwd = std::env::current_dir().unwrap().into_os_string().into_string().unwrap();
148-
pwd.push('/');
149-
150-
let out = std::process::Command::new("rustc").arg("--print=sysroot").output().unwrap();
151-
let sysroot = std::str::from_utf8(&out.stdout).unwrap().trim();
152-
let sysroot = format!("{sysroot}/lib/rustlib/src/rust/");
153-
[pwd, sysroot]
154-
});
155-
156-
let file = inst.def.span().get_filename();
157-
for prefix in &*PREFIXES {
158-
if let Some(file) = file.strip_prefix(prefix) {
159-
return file.to_owned();
160-
}
161-
}
162-
file
163-
}

src/functions/serialization.rs

Lines changed: 22 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
1+
use super::utils::{self, SourceCode};
12
use rustc_middle::ty::TyCtxt;
23
use rustc_span::source_map::SourceMap;
34
use rustc_stable_hash::{FromStableHash, SipHasher128Hash, StableHasher, hashers::SipHasher128};
45
use serde::Serialize;
5-
use stable_mir::{CrateDef, DefId, mir::mono::Instance};
6-
use std::hash::Hasher;
6+
use stable_mir::{CrateDef, mir::mono::Instance};
7+
use std::{cmp::Ordering, hash::Hasher};
78

89
/// A Rust funtion with its file source, attributes, and raw function content.
910
#[derive(Debug, Serialize)]
@@ -18,34 +19,41 @@ pub struct SerFunction {
1819
/// and function must be separated to query.
1920
attrs: Vec<String>,
2021
/// Raw function string, including name, signature, and body.
21-
func: String,
22+
func: SourceCode,
2223
/// Recursive function calls inside the proof.
2324
callees: Vec<Callee>,
2425
}
2526

2627
impl SerFunction {
2728
pub fn new(fun: super::Function, tcx: TyCtxt, src_map: &SourceMap) -> Self {
28-
let def_id = format_def_id(&fun.def_id);
29-
let file = fun.file;
29+
let inst = fun.instance;
30+
let def_id = format_def_id(&inst);
31+
let file = utils::file_path(&inst);
3032
let attrs: Vec<_> = fun.attrs.iter().map(|a| a.as_str().to_owned()).collect();
31-
let func = fun.func;
33+
// 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);
3235
let callees: Vec<_> = fun.callees.iter().map(|x| Callee::new(x, tcx, src_map)).collect();
3336

3437
// Hash
3538
let mut hasher = StableHasher::<SipHasher128>::new();
3639
hasher.write_str(&file);
37-
hasher.write_str(&func);
40+
func.with_hasher(&mut hasher);
3841
hasher.write_length_prefix(attrs.len());
3942
attrs.iter().for_each(|a| hasher.write_str(a));
4043
hasher.write_length_prefix(callees.len());
4144
callees.iter().for_each(|c| {
4245
hasher.write_str(&c.file);
43-
hasher.write_str(&c.func);
46+
c.func.with_hasher(&mut hasher);
4447
});
4548
let Hash128(hash) = hasher.finish();
4649

4750
SerFunction { hash, def_id, file, attrs, func, callees }
4851
}
52+
53+
/// Compare by file and func string.
54+
pub fn cmp_by_file_and_func(&self, other: &Self) -> Ordering {
55+
(&*self.file, &self.func).cmp(&(&*other.file, &other.func))
56+
}
4957
}
5058

5159
// ************* hash *************
@@ -60,23 +68,22 @@ impl FromStableHash for Hash128 {
6068
}
6169
// ************* hash *************
6270

63-
fn format_def_id(def_id: &DefId) -> String {
64-
format!("{def_id:?}")
71+
fn format_def_id(inst: &Instance) -> String {
72+
format!("{:?}", inst.def.def_id())
6573
}
6674

6775
#[derive(Debug, Serialize)]
6876
pub struct Callee {
6977
def_id: String,
7078
file: String,
71-
func: String,
79+
func: SourceCode,
7280
}
7381

7482
impl Callee {
7583
fn new(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Self {
76-
let inst_def = &inst.def;
77-
let def_id = format_def_id(&inst_def.def_id());
78-
let file = super::file_path(inst);
79-
let func = super::source_code_of_body(inst, tcx, src_map).unwrap_or_default();
84+
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();
8087
Callee { def_id, file, func }
8188
}
8289
}

src/functions/utils.rs

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
use rustc_middle::ty::TyCtxt;
2+
use rustc_smir::rustc_internal::internal;
3+
use rustc_span::{Span, source_map::SourceMap};
4+
use rustc_stable_hash::{StableHasher, hashers::SipHasher128};
5+
use serde::Serialize;
6+
use stable_mir::{CrateDef, mir::mono::Instance};
7+
use std::{cmp::Ordering, hash::Hasher};
8+
9+
/// Source code and potential source code before expansion.
10+
///
11+
/// Refer to
12+
#[derive(Debug, Serialize, PartialEq, Eq, PartialOrd, Ord, Default)]
13+
pub struct SourceCode {
14+
// TODO:
15+
// file: String,
16+
//
17+
/// Source that a stable_mir span points to.
18+
pub src: String,
19+
/// Is the stable_mir span from a macro expansion?
20+
/// If it is from an expansion, what's the source code before expansion?
21+
/// * Some(_) happens when the src (stable_mir) span comes from expansion, and tells
22+
/// the source before the expansion.
23+
/// * None if the src is not from a macro expansion.
24+
pub before_expansion: Option<String>,
25+
}
26+
27+
impl SourceCode {
28+
pub fn with_hasher(&self, hasher: &mut StableHasher<SipHasher128>) {
29+
hasher.write_str(&self.src);
30+
match &self.before_expansion {
31+
Some(text) => {
32+
hasher.write_u8(1);
33+
hasher.write_str(text);
34+
}
35+
None => hasher.write_u8(0),
36+
}
37+
}
38+
}
39+
40+
fn span_to_source(span: Span, src_map: &SourceMap) -> String {
41+
src_map
42+
.span_to_source(span, |text, x, y| {
43+
let src = &text[x..y];
44+
debug!("[{x}:{y}]\n{src}");
45+
Ok(src.to_owned())
46+
})
47+
.unwrap()
48+
}
49+
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+
60+
/// Source code for a stable_mir span.
61+
pub fn source_code_with(
62+
stable_mir_span: stable_mir::ty::Span,
63+
tcx: TyCtxt,
64+
src_map: &SourceMap,
65+
) -> SourceCode {
66+
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]
102+
});
103+
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();
108+
}
109+
}
110+
file
111+
}

0 commit comments

Comments
 (0)