rust_verify/src/profiler.rs
Line | Count | Source |
1 | | use vir::{ast::Fun, ast_util::fun_as_friendly_rust_name}; |
2 | | |
3 | | use crate::buckets::BucketId; |
4 | | use crate::commands::Op; |
5 | | use crate::verifier::module_name; |
6 | | |
7 | | use std::{ |
8 | | collections::{HashMap, HashSet}, |
9 | | fs::File, |
10 | | }; |
11 | | |
12 | 0 | pub fn write_instantiation_graph( |
13 | 0 | bucket_id: &BucketId, |
14 | 0 | op: Option<&Op>, |
15 | 0 | func_map: &HashMap<Fun, vir::ast::Function>, |
16 | 0 | instantiation_graph: &air::profiler::InstantiationGraph, |
17 | 0 | qid_map: &HashMap<String, vir::sst::BndInfo>, |
18 | 0 | profile_file_name: std::path::PathBuf, |
19 | 0 | ) { |
20 | 0 | let air::profiler::InstantiationGraph { edges, nodes, names } = instantiation_graph; |
21 | | use internals_interface::*; |
22 | 0 | let name_strs: HashSet<String> = names.values().cloned().collect(); |
23 | 0 | let quantifiers: HashMap<String, Quantifier> = name_strs |
24 | 0 | .iter() |
25 | 0 | .map(|n| { |
26 | 0 | let bnd_info = qid_map.get(n); |
27 | 0 | let kind = if n.starts_with(air::profiler::USER_QUANT_PREFIX) { |
28 | 0 | QuantifierKind::User(UserQuantifier { |
29 | 0 | span: bnd_info.as_ref().unwrap().user.as_ref().unwrap().span.as_string.clone(), |
30 | 0 | }) |
31 | | } else { |
32 | 0 | QuantifierKind::Internal |
33 | | }; |
34 | | ( |
35 | 0 | n.clone(), |
36 | 0 | std::rc::Rc::new(QuantifierX { |
37 | 0 | qid: n.clone(), |
38 | 0 | module: bnd_info.map(|b| { |
39 | 0 | module_name( |
40 | 0 | &func_map[&b.fun].x.owning_module.as_ref().expect("owning module"), |
41 | | ) |
42 | 0 | }), |
43 | 0 | kind, |
44 | | }), |
45 | | ) |
46 | 0 | }) |
47 | 0 | .collect(); |
48 | 0 | let instantiations: HashMap<(u64, usize), Instantiation> = nodes |
49 | 0 | .iter() |
50 | 0 | .map(|n| { |
51 | 0 | ( |
52 | 0 | n.clone(), |
53 | 0 | std::rc::Rc::new(InstantiationX { |
54 | 0 | quantifier: quantifiers[&names[n]].clone(), |
55 | 0 | id: *n, |
56 | 0 | }), |
57 | 0 | ) |
58 | 0 | }) |
59 | 0 | .collect(); |
60 | 0 | let mut graph: HashMap<Instantiation, HashSet<((), Instantiation)>> = HashMap::new(); |
61 | 0 | for (src, tgts) in edges { |
62 | 0 | let graph_src = graph.entry(instantiations[src].clone()).or_insert(HashSet::new()); |
63 | 0 | for tgt in tgts { |
64 | 0 | graph_src.insert(((), instantiations[tgt].clone())); |
65 | 0 | } |
66 | | } |
67 | 0 | let instantiations: HashSet<Instantiation> = instantiations.values().cloned().collect(); |
68 | 0 | let quantifiers = quantifiers.into_values().collect(); |
69 | 0 | let instantiation_graph = InstantiationGraph { |
70 | 0 | bucket_name: bucket_id.to_log_string(), |
71 | 0 | module: module_name(bucket_id.module()), |
72 | 0 | function: op.map(|op| fun_as_friendly_rust_name(&op.get_function().x.name)), |
73 | 0 | quantifiers, |
74 | 0 | instantiations, |
75 | 0 | graph: Graph(graph), |
76 | | }; |
77 | 0 | let file_name = profile_file_name.with_extension("graph"); |
78 | 0 | let f = File::create(&file_name).unwrap_or_else(|e| { |
79 | 0 | panic!("failed to open instantiation graph file {}: {}", file_name.display(), e) |
80 | | }); |
81 | 0 | instantiation_graph.serialize(f).expect("failed to write instantiation graph"); |
82 | 0 | } |