11use indexmap:: IndexSet ;
2- use kani:: collect_reachable_items;
2+ use kani:: { CallGraph , collect_reachable_items} ;
33use rustc_middle:: ty:: TyCtxt ;
44use rustc_smir:: rustc_internal:: internal;
55use rustc_span:: { Span , source_map:: SourceMap } ;
66use serde:: Serialize ;
77use stable_mir:: {
8- CrateDef , CrateItem , DefId , ItemKind ,
8+ CrateDef , DefId ,
99 mir:: mono:: { Instance , MonoItem } ,
1010 ty:: { FnDef , RigidTy , Ty , TyKind } ,
1111} ;
@@ -17,7 +17,6 @@ pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<Function> {
1717 let local_items = stable_mir:: all_local_items ( ) ;
1818 let cap = local_items. len ( ) ;
1919
20- let mut outputs = Vec :: with_capacity ( cap) ;
2120 let mut entries = Vec :: with_capacity ( cap) ;
2221
2322 for item in local_items {
@@ -29,7 +28,7 @@ pub fn analyze(tcx: TyCtxt, src_map: &SourceMap) -> Vec<Function> {
2928
3029 let ( mono_items, callgraph) = collect_reachable_items ( tcx, & entries) ;
3130
32- outputs
31+ mono_items . iter ( ) . filter_map ( |item| Function :: new ( item , & callgraph , tcx , src_map ) ) . collect ( )
3332}
3433
3534/// A Rust funtion with its file source, attributes, and raw function content.
@@ -48,37 +47,39 @@ pub struct Function {
4847}
4948
5049impl Function {
51- pub fn new ( item : CrateItem , tcx : TyCtxt , src_map : & SourceMap ) -> Option < Self > {
52- if !matches ! ( item. kind( ) , ItemKind :: Fn ) {
53- // skip non fn items
50+ pub fn new (
51+ item : & MonoItem ,
52+ callgraph : & CallGraph ,
53+ tcx : TyCtxt ,
54+ src_map : & SourceMap ,
55+ ) -> Option < Self > {
56+ // skip non fn items
57+ let & MonoItem :: Fn ( inst) = item else {
5458 return None ;
55- }
56- // item.emit_mir(&mut std::io::stdout()).unwrap(); // MIR body
57- let inst = Instance :: try_from ( item) . inspect_err ( |err| error ! ( ?err) ) . ok ( ) ?;
59+ } ;
60+
5861 let fn_def = ty_to_fndef ( inst. ty ( ) ) ?;
59- let file = item. span ( ) . get_filename ( ) ;
62+ let inst_def = inst. def ;
63+ let span = inst_def. span ( ) ;
64+
65+ let file = span. get_filename ( ) ;
6066 let body = fn_def. body ( ) ?;
6167
6268 let mut callees = IndexSet :: new ( ) ;
63- // retrieve direct calls
64- callees. extend ( callees:: calls_in_body ( & body) ) ;
65- // recursive calls
66- let direct_calls: Vec < _ > = callees. iter ( ) . copied ( ) . collect ( ) ;
67- for call in direct_calls {
68- callees:: recursive_callees ( call, & mut callees) ;
69- }
70- let callees = callees. into_iter ( ) . map ( |x| format ! ( "{x:?}" ) ) . collect ( ) ;
69+ callgraph. recursive_callees ( item, & mut callees) ;
70+ let callees = callees. into_iter ( ) . map ( |x| format ! ( "{:?}" , x. def. def_id( ) ) ) . collect ( ) ;
7171
7272 let func = source_code_with ( body. span , tcx, src_map) ;
73- info ! ( " - {:?} ({:?}): {func}" , item . name( ) , item . span ( ) ) ;
73+ info ! ( " - {:?} ({span :?}): {func}" , inst_def . name( ) ) ;
7474
7575 // FIXME: kanitool and some other proc-macors attributes are generated by parsing,
7676 // and these generated attrs share with span of hand-written attrs in source code.
7777 // As a result, get_all_attributes through source span will emit duplicated attrs.
7878 // Need to fix this in the future, by analyzing Symbols of these attrs.
79- let attrs = get_all_attributes ( item. def_id ( ) , tcx, src_map) ;
79+ // let attrs = get_all_attributes(inst_def.def_id(), tcx, src_map);
80+ let attrs = vec ! [ ] ;
8081
81- // TODO: kanitool kind: proof, proof_for_contract, contract, ...
82+ // TODO: filter in kanitool kind: proof, proof_for_contract, contract, ...
8283
8384 Some ( Function { file, attrs, func, callees } )
8485 }
0 commit comments