Skip to content

Commit 80c0976

Browse files
committed
feat: replace func string with SourceCode
Each function can contain two kinds of source code. close #31
1 parent 5418783 commit 80c0976

File tree

4 files changed

+75
-25
lines changed

4 files changed

+75
-25
lines changed

src/functions/serialization.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use super::utils;
1+
use super::utils::{self, SourceCode};
22
use rustc_middle::ty::TyCtxt;
33
use rustc_span::source_map::SourceMap;
44
use rustc_stable_hash::{FromStableHash, SipHasher128Hash, StableHasher, hashers::SipHasher128};
@@ -19,7 +19,7 @@ pub struct SerFunction {
1919
/// and function must be separated to query.
2020
attrs: Vec<String>,
2121
/// Raw function string, including name, signature, and body.
22-
func: String,
22+
func: SourceCode,
2323
/// Recursive function calls inside the proof.
2424
callees: Vec<Callee>,
2525
}
@@ -37,13 +37,13 @@ impl SerFunction {
3737
// Hash
3838
let mut hasher = StableHasher::<SipHasher128>::new();
3939
hasher.write_str(&file);
40-
hasher.write_str(&func);
40+
func.with_hasher(&mut hasher);
4141
hasher.write_length_prefix(attrs.len());
4242
attrs.iter().for_each(|a| hasher.write_str(a));
4343
hasher.write_length_prefix(callees.len());
4444
callees.iter().for_each(|c| {
4545
hasher.write_str(&c.file);
46-
hasher.write_str(&c.func);
46+
c.func.with_hasher(&mut hasher);
4747
});
4848
let Hash128(hash) = hasher.finish();
4949

@@ -52,7 +52,7 @@ impl SerFunction {
5252

5353
/// Compare by file and func string.
5454
pub fn cmp_by_file_and_func(&self, other: &Self) -> Ordering {
55-
(&*self.file, &*self.func).cmp(&(&*other.file, &*other.func))
55+
(&*self.file, &self.func).cmp(&(&*other.file, &other.func))
5656
}
5757
}
5858

@@ -76,7 +76,7 @@ fn format_def_id(inst: &Instance) -> String {
7676
pub struct Callee {
7777
def_id: String,
7878
file: String,
79-
func: String,
79+
func: SourceCode,
8080
}
8181

8282
impl Callee {

src/functions/utils.rs

Lines changed: 51 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,43 @@
11
use rustc_middle::ty::TyCtxt;
22
use rustc_smir::rustc_internal::internal;
33
use rustc_span::{Span, source_map::SourceMap};
4+
use rustc_stable_hash::{StableHasher, hashers::SipHasher128};
5+
use serde::Serialize;
46
use stable_mir::{CrateDef, mir::mono::Instance};
5-
use std::cmp::Ordering;
7+
use std::{cmp::Ordering, hash::Hasher};
68

7-
/// Source code for a span.
8-
fn source_code(span: Span, src_map: &SourceMap) -> String {
9-
// println!("{span:?}\n{:?}\n\n", span.find_oldest_ancestor_in_same_ctxt());
10-
// _ = src_map.span_to_source(span, |text, x, y| {
11-
// println!("(stable_mir span to internal span) [{span:?}]\n{}", &text[x..y]);
12-
// Ok(())
13-
// });
14-
// let ancestor_span = span.find_oldest_ancestor_in_same_ctxt();
15-
// dbg!(span.from_expansion(), ancestor_span.from_expansion());
16-
// _ = src_map.span_to_source(ancestor_span, |text, x, y| {
17-
// println!("(find_oldest_ancestor_in_same_ctxt) [{ancestor_span:?}]\n{}\n\n", &text[x..y]);
18-
// Ok(())
19-
// });
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+
}
2039

40+
fn span_to_source(span: Span, src_map: &SourceMap) -> String {
2141
src_map
2242
.span_to_source(span, |text, x, y| {
2343
let src = &text[x..y];
@@ -27,17 +47,32 @@ fn source_code(span: Span, src_map: &SourceMap) -> String {
2747
.unwrap()
2848
}
2949

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+
3060
/// Source code for a stable_mir span.
3161
pub fn source_code_with(
3262
stable_mir_span: stable_mir::ty::Span,
3363
tcx: TyCtxt,
3464
src_map: &SourceMap,
35-
) -> String {
65+
) -> SourceCode {
3666
let span = internal(tcx, stable_mir_span);
3767
source_code(span, src_map)
3868
}
3969

40-
pub fn source_code_of_body(inst: &Instance, tcx: TyCtxt, src_map: &SourceMap) -> Option<String> {
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> {
4176
inst.body().map(|body| source_code_with(body.span, tcx, src_map))
4277
}
4378

src/lib.rs

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ pub struct SerFunction {
1313
/// and function must be separated to query.
1414
pub attrs: Vec<String>,
1515
/// Raw function string, including name, signature, and body.
16-
pub func: String,
16+
pub func: SourceCode,
1717
/// Recursive function calls inside the body.
1818
pub callees: Vec<Callee>,
1919
}
@@ -22,7 +22,22 @@ pub struct SerFunction {
2222
pub struct Callee {
2323
pub def_id: String,
2424
pub file: String,
25-
pub func: String,
25+
pub func: SourceCode,
26+
}
27+
28+
#[derive(Debug, Serialize, Deserialize)]
29+
pub struct SourceCode {
30+
// TODO:
31+
// file: String,
32+
//
33+
/// Source that a stable_mir span points to.
34+
pub src: String,
35+
/// Is the stable_mir span from a macro expansion?
36+
/// If it is from an expansion, what's the source code before expansion?
37+
/// * Some(_) happens when the src (stable_mir) span comes from expansion, and tells
38+
/// the source before the expansion.
39+
/// * None if the src is not from a macro expansion.
40+
pub before_expansion: Option<String>,
2641
}
2742

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

tests/compare.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use utils::{assert_eq, cmd, expect_file};
77
fn get(text: &str, start: &str) -> SerFunction {
88
let json = &text[text.find("[\n").unwrap()..];
99
let v: Vec<SerFunction> = serde_json::from_str(json).unwrap();
10-
v.into_iter().find(|f| f.func.starts_with(start)).unwrap()
10+
v.into_iter().find(|f| f.func.src.starts_with(start)).unwrap()
1111
}
1212

1313
const COMPARE: &str = "tests/compare";

0 commit comments

Comments
 (0)