From 92be5c1418442bc7a716005d6a95a9be4b5a0ddd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 8 May 2023 15:10:18 -0700 Subject: [PATCH 1/3] Add a few options to dump the reachability graph This is for debugging purpose only. All this logic will be disabled in release builds. For simplicity, I'm just using an environment variable. --- docs/src/cheat-sheets.md | 16 ++ kani-compiler/src/kani_middle/reachability.rs | 159 ++++++++++++++++-- 2 files changed, 160 insertions(+), 15 deletions(-) diff --git a/docs/src/cheat-sheets.md b/docs/src/cheat-sheets.md index 8eac5e0486e6..c58c1df4ca3f 100644 --- a/docs/src/cheat-sheets.md +++ b/docs/src/cheat-sheets.md @@ -81,6 +81,22 @@ kani --gen-c file.rs RUSTFLAGS="--emit mir" kani ${INPUT}.rs ``` +The `KANI_REACH_DEBUG` environment variable can be used to debug Kani's reachability analysis. +If defined, Kani will print generate a DOT graph `${INPUT}.dot` with the graph traversed during reachability analysis. +If defined and not empty, the graph will be filtered to end at functions that contains the substring +from `KANI_REACH_DEBUG`. + +Note that this will only work on debug builds. + +```bash +# Generate a DOT graph ${INPUT}.dot with the graph traversed during reachability analysis +KANI_REACH_DEBUG= kani ${INPUT}.rs + +# Generate a DOT graph ${INPUT}.dot with the sub-graph traversed during the reachability analysis +# that connect to the given target. +KANI_REACH_DEBUG="${TARGET_ITEM}" kani ${INPUT}.rs +``` + ## CBMC ```bash diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 7845f4bab4ca..7a7dbf79bce1 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -44,10 +44,17 @@ pub fn collect_reachable_items<'tcx>( ) -> Vec> { // For each harness, collect items using the same collector. // I.e.: This will return any item that is reachable from one or more of the starting points. - let mut collector = MonoItemsCollector { tcx, collected: FxHashSet::default(), queue: vec![] }; + let mut collector = MonoItemsCollector::new(tcx); for item in starting_points { collector.collect(*item); } + + #[cfg(debug_assertions)] + collector + .call_graph + .dump_dot(tcx) + .unwrap_or_else(|e| tracing::error!("Failed to dump call graph: {e}")); + tcx.sess.abort_if_errors(); // Sort the result so code generation follows deterministic order. @@ -140,9 +147,20 @@ struct MonoItemsCollector<'tcx> { collected: FxHashSet>, /// Items enqueued for visiting. queue: Vec>, + #[cfg(debug_assertions)] + call_graph: debug::CallGraph<'tcx>, } impl<'tcx> MonoItemsCollector<'tcx> { + pub fn new(tcx: TyCtxt<'tcx>) -> Self { + MonoItemsCollector { + tcx, + collected: FxHashSet::default(), + queue: vec![], + #[cfg(debug_assertions)] + call_graph: debug::CallGraph::default(), + } + } /// Collects all reachable items starting from the given root. pub fn collect(&mut self, root: MonoItem<'tcx>) { debug!(?root, "collect"); @@ -156,52 +174,56 @@ impl<'tcx> MonoItemsCollector<'tcx> { while let Some(to_visit) = self.queue.pop() { if !self.collected.contains(&to_visit) { self.collected.insert(to_visit); - match to_visit { - MonoItem::Fn(instance) => { - self.visit_fn(instance); - } - MonoItem::Static(def_id) => { - self.visit_static(def_id); - } + let next_items = match to_visit { + MonoItem::Fn(instance) => self.visit_fn(instance), + MonoItem::Static(def_id) => self.visit_static(def_id), MonoItem::GlobalAsm(_) => { self.visit_asm(to_visit); + vec![] } - } + }; + #[cfg(debug_assertions)] + self.call_graph.add_edges(to_visit, &next_items); + + self.queue + .extend(next_items.into_iter().filter(|item| !self.collected.contains(item))); } } } /// Visit a function and collect all mono-items reachable from its instructions. - fn visit_fn(&mut self, instance: Instance<'tcx>) { + fn visit_fn(&mut self, instance: Instance<'tcx>) -> Vec> { let _guard = debug_span!("visit_fn", function=?instance).entered(); let body = self.tcx.instance_mir(instance.def); let mut collector = MonoItemsFnCollector { tcx: self.tcx, collected: FxHashSet::default(), instance, body }; collector.visit_body(body); - self.queue.extend(collector.collected.iter().filter(|item| !self.collected.contains(item))); + collector.collected.into_iter().collect() } /// Visit a static object and collect drop / initialization functions. - fn visit_static(&mut self, def_id: DefId) { + fn visit_static(&mut self, def_id: DefId) -> Vec> { let _guard = debug_span!("visit_static", ?def_id).entered(); let instance = Instance::mono(self.tcx, def_id); + let mut next_items = vec![]; // Collect drop function. let static_ty = instance.ty(self.tcx, ParamEnv::reveal_all()); let instance = Instance::resolve_drop_in_place(self.tcx, static_ty); - self.queue.push(MonoItem::Fn(instance.polymorphize(self.tcx))); + next_items.push(MonoItem::Fn(instance.polymorphize(self.tcx))); // Collect initialization. let alloc = self.tcx.eval_static_initializer(def_id).unwrap(); for id in alloc.inner().provenance().provenances() { - self.queue.extend(collect_alloc_items(self.tcx, id).iter()); + next_items.extend(collect_alloc_items(self.tcx, id).iter()); } + + next_items } /// Visit global assembly and collect its item. fn visit_asm(&mut self, item: MonoItem<'tcx>) { debug!(?item, "visit_asm"); - self.collected.insert(item); } } @@ -626,3 +648,110 @@ impl<'a, 'tcx> MirVisitor<'tcx> for ConstMonoItemExtractor<'a, 'tcx> { self.super_rvalue(rvalue, location); } } + +#[cfg(debug_assertions)] +mod debug { + #![allow(dead_code)] + + use std::{ + collections::{HashMap, HashSet}, + fs::File, + io::{BufWriter, Write}, + }; + + use rustc_session::config::OutputType; + + use super::*; + + #[derive(Debug, Default)] + pub struct CallGraph<'tcx> { + // Nodes of the graph. + nodes: HashSet>, + edges: HashMap, Vec>>, + back_edges: HashMap, Vec>>, + } + + type Node<'tcx> = MonoItem<'tcx>; + + impl<'tcx> CallGraph<'tcx> { + pub fn add_node(&mut self, item: Node<'tcx>) { + self.nodes.insert(item); + self.edges.entry(item).or_default(); + self.back_edges.entry(item).or_default(); + } + + /// Add a new edge "from" -> "to". + pub fn add_edge(&mut self, from: Node<'tcx>, to: Node<'tcx>) { + self.add_node(from); + self.add_node(to); + self.edges.get_mut(&from).unwrap().push(to); + self.back_edges.get_mut(&to).unwrap().push(from); + } + + /// Add multiple new edges for the "from" node. + pub fn add_edges(&mut self, from: Node<'tcx>, to: &[Node<'tcx>]) { + self.add_node(from); + for item in to { + self.add_edge(from, *item); + } + } + + /// Print the graph in DOT format to a file. + /// See for more information. + pub fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> { + if let Ok(target) = std::env::var("KANI_REACH_DEBUG") { + let outputs = tcx.output_filenames(()); + let path = outputs.output_path(OutputType::Metadata).with_extension("dot"); + let out_file = File::create(&path)?; + let mut writer = BufWriter::new(out_file); + writeln!(writer, "digraph ReachabilityGraph {{")?; + if target.is_empty() { + self.dump_all(&mut writer)?; + } else { + // Only dump nodes that led the reachability analysis to the target node. + self.dump_reason(&mut writer, &target)?; + } + writeln!(writer, "}}")?; + } + + Ok(()) + } + + /// Write all notes to the given writer. + fn dump_all(&self, writer: &mut W) -> std::io::Result<()> { + for node in &self.nodes { + writeln!(writer, r#""{node}""#)?; + for succ in self.edges.get(node).unwrap() { + writeln!(writer, r#""{node}" -> "{succ}" "#)?; + } + } + Ok(()) + } + + /// Write all notes that may have led to the discovery of the given target. + fn dump_reason(&self, writer: &mut W, target: &str) -> std::io::Result<()> { + let mut queue = self + .nodes + .iter() + .filter(|item| item.to_string().contains(target)) + .collect::>(); + let mut visited: HashSet<&MonoItem> = HashSet::default(); + while let Some(to_visit) = queue.pop() { + if !visited.contains(to_visit) { + visited.insert(to_visit); + queue.extend(self.back_edges.get(to_visit).unwrap()); + } + } + + for node in &visited { + writeln!(writer, r#""{node}""#)?; + for succ in + self.edges.get(node).unwrap().iter().filter(|item| visited.contains(item)) + { + writeln!(writer, r#""{node}" -> "{succ}" "#)?; + } + } + Ok(()) + } + } +} From ec1a2d9cacc34820ee9d59e86f74ef612ce6aa2d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 8 May 2023 18:41:00 -0700 Subject: [PATCH 2/3] Add some debugging to the debug code o.O --- kani-compiler/src/kani_middle/reachability.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 7a7dbf79bce1..2847c9285e7c 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -700,6 +700,7 @@ mod debug { /// See for more information. pub fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> { if let Ok(target) = std::env::var("KANI_REACH_DEBUG") { + debug!(?target, "dump_dot"); let outputs = tcx.output_filenames(()); let path = outputs.output_path(OutputType::Metadata).with_extension("dot"); let out_file = File::create(&path)?; @@ -719,6 +720,7 @@ mod debug { /// Write all notes to the given writer. fn dump_all(&self, writer: &mut W) -> std::io::Result<()> { + tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all"); for node in &self.nodes { writeln!(writer, r#""{node}""#)?; for succ in self.edges.get(node).unwrap() { @@ -736,6 +738,7 @@ mod debug { .filter(|item| item.to_string().contains(target)) .collect::>(); let mut visited: HashSet<&MonoItem> = HashSet::default(); + tracing::info!(target=?queue, nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_reason"); while let Some(to_visit) = queue.pop() { if !visited.contains(to_visit) { visited.insert(to_visit); From ee1b90e3084bd0a1dc4e9f3330206c4a0a406cda Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 10 May 2023 23:33:28 -0700 Subject: [PATCH 3/3] Update docs/src/cheat-sheets.md Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- docs/src/cheat-sheets.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/src/cheat-sheets.md b/docs/src/cheat-sheets.md index c58c1df4ca3f..95cc9991e46f 100644 --- a/docs/src/cheat-sheets.md +++ b/docs/src/cheat-sheets.md @@ -82,7 +82,7 @@ RUSTFLAGS="--emit mir" kani ${INPUT}.rs ``` The `KANI_REACH_DEBUG` environment variable can be used to debug Kani's reachability analysis. -If defined, Kani will print generate a DOT graph `${INPUT}.dot` with the graph traversed during reachability analysis. +If defined, Kani will generate a DOT graph `${INPUT}.dot` with the graph traversed during reachability analysis. If defined and not empty, the graph will be filtered to end at functions that contains the substring from `KANI_REACH_DEBUG`.