Skip to content

Commit 14b7f02

Browse files
committed
feat: before_expansion => macro_backtrace and macro_backtrace_len
This commit adds both callsite and defsite along all macro invocations for a function. Close #47
1 parent 4860011 commit 14b7f02

File tree

2 files changed

+54
-28
lines changed

2 files changed

+54
-28
lines changed

src/functions/utils.rs

Lines changed: 38 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,9 @@ pub struct SourceCode {
2929
/// Source that a stable_mir span points to.
3030
pub src: String,
3131

32+
/// The count of macro backtraces.
33+
pub macro_backtrace_len: usize,
34+
3235
/// Is the stable_mir span from a macro expansion?
3336
/// If it is from an expansion, what's the source code before expansion?
3437
/// * Some(_) happens when the src (stable_mir) span comes from expansion, and tells
@@ -38,7 +41,7 @@ pub struct SourceCode {
3841
/// Refer to [#31] to know sepecific cases.
3942
///
4043
/// [#31]: https://github.com/os-checker/distributed-verification/issues/31
41-
pub before_expansion: Option<String>,
44+
pub macro_backtrace: Vec<MacroBacktrace>,
4245
}
4346

4447
impl SourceCode {
@@ -48,16 +51,20 @@ impl SourceCode {
4851
hasher.write_str(&self.kind);
4952
hasher.write_str(&self.file);
5053
hasher.write_str(&self.src);
51-
match &self.before_expansion {
52-
Some(text) => {
53-
hasher.write_u8(1);
54-
hasher.write_str(text);
55-
}
56-
None => hasher.write_u8(0),
54+
hasher.write_length_prefix(self.macro_backtrace_len);
55+
for m in &self.macro_backtrace {
56+
hasher.write_str(&m.callsite);
57+
hasher.write_str(&m.defsite);
5758
}
5859
}
5960
}
6061

62+
#[derive(Clone, Debug, Serialize, PartialEq, Eq, PartialOrd, Ord, Default)]
63+
pub struct MacroBacktrace {
64+
callsite: String,
65+
defsite: String,
66+
}
67+
6168
fn span_to_source(span: Span, src_map: &SourceMap) -> String {
6269
src_map
6370
.span_to_source(span, |text, x, y| {
@@ -78,25 +85,30 @@ pub fn source_code_with(
7885
) -> SourceCode {
7986
let span = internal(tcx, stable_mir_span);
8087
let src = span_to_source(span, src_map);
81-
let before_expansion = span.from_expansion().then(|| {
82-
{
83-
debug!(
84-
"[find_oldest_ancestor_in_same_ctxt] {}",
85-
span_to_source(span.find_oldest_ancestor_in_same_ctxt(), src_map)
86-
);
87-
debug!("[source_callsite] {}", span_to_source(span.source_callsite(), src_map));
88-
if let Some(parent_callsite) = span.parent_callsite() {
89-
debug!("[parent_callsite] {}", span_to_source(parent_callsite, src_map));
90-
}
91-
for m in span.macro_backtrace() {
92-
debug!("[macro_backtrace - callsite] {}", span_to_source(m.call_site, src_map));
93-
debug!("[macro_backtrace - defsite ] {}", span_to_source(m.def_site, src_map));
94-
}
95-
debug!("\n");
88+
89+
if span.from_expansion() {
90+
debug!(
91+
"[find_oldest_ancestor_in_same_ctxt] {}",
92+
span_to_source(span.find_oldest_ancestor_in_same_ctxt(), src_map)
93+
);
94+
debug!("[source_callsite] {}", span_to_source(span.source_callsite(), src_map));
95+
if let Some(parent_callsite) = span.parent_callsite() {
96+
debug!("[parent_callsite] {}", span_to_source(parent_callsite, src_map));
97+
}
98+
for m in span.macro_backtrace() {
99+
debug!("[macro_backtrace - callsite] {}", span_to_source(m.call_site, src_map));
100+
debug!("[macro_backtrace - defsite ] {}", span_to_source(m.def_site, src_map));
96101
}
97-
let ancestor_span = span.find_oldest_ancestor_in_same_ctxt();
98-
span_to_source(ancestor_span, src_map)
99-
});
102+
debug!("\n");
103+
}
104+
let macro_backtrace: Vec<_> = span
105+
.macro_backtrace()
106+
.map(|m| MacroBacktrace {
107+
callsite: span_to_source(m.call_site, src_map),
108+
defsite: span_to_source(m.def_site, src_map),
109+
})
110+
.collect();
111+
let macro_backtrace_len = macro_backtrace.len();
100112

101113
let mut file = stable_mir_span.get_filename();
102114
for prefix in path_prefixes {
@@ -109,5 +121,5 @@ pub fn source_code_with(
109121
let name = inst.name();
110122
let mangled_name = inst.mangled_name();
111123
let kind = format!("{:?}", inst.kind);
112-
SourceCode { name, mangled_name, kind, file, src, before_expansion }
124+
SourceCode { name, mangled_name, kind, file, src, macro_backtrace_len, macro_backtrace }
113125
}

src/lib.rs

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,16 +38,30 @@ pub struct SourceCode {
3838

3939
// A file path where src lies.
4040
// The path is stripped with pwd or sysroot prefix.
41-
file: String,
41+
pub file: String,
4242

4343
/// Source that a stable_mir span points to.
4444
pub src: String,
45+
46+
/// The count of macro backtraces.
47+
pub macro_backtrace_len: usize,
48+
4549
/// Is the stable_mir span from a macro expansion?
4650
/// If it is from an expansion, what's the source code before expansion?
4751
/// * Some(_) happens when the src (stable_mir) span comes from expansion, and tells
4852
/// the source before the expansion.
4953
/// * None if the src is not from a macro expansion.
50-
pub before_expansion: Option<String>,
54+
///
55+
/// Refer to [#31] to know sepecific cases.
56+
///
57+
/// [#31]: https://github.com/os-checker/distributed-verification/issues/31
58+
pub macro_backtrace: Vec<MacroBacktrace>,
59+
}
60+
61+
#[derive(Debug, Default, Serialize, Deserialize, Clone)]
62+
pub struct MacroBacktrace {
63+
callsite: String,
64+
defsite: String,
5165
}
5266

5367
/// A local path to kani's artifacts.

0 commit comments

Comments
 (0)