Streamline tracking of dependencies

creusot/src/backend/clone_map.rs

@@ -1,5 +1,8 @@
 use core::panic;
-use std::cell::RefCell;
+use std::{
+    cell::RefCell,
+    collections::{HashSet, VecDeque},
+};
 
 use crate::{
     backend::{Why3Generator, clone_map::elaborator::Expander, dependency::Dependency},
@@ -313,7 +316,7 @@ impl<'a, 'tcx> Namer<'tcx> for Dependencies<'a, 'tcx> {
     }
 
     fn raw_dependency(&self, key: Dependency<'tcx>) -> &Kind {
-        self.dep_set.borrow_mut().insert(key);
+        self.dep_graph.borrow_mut().add_node(key);
         self.names.raw_dependency(key)
     }
 
@@ -332,9 +335,47 @@ impl<'a, 'tcx> Namer<'tcx> for Dependencies<'a, 'tcx> {
 
 pub(crate) struct Dependencies<'a, 'tcx> {
     names: CloneNames<'a, 'tcx>,
+    dep_graph: RefCell<DepGraphBuilder<'tcx>>,
+}
+
+/// Dependencies of a source item.
+type DepGraph<'tcx> = DiGraphMap<Dependency<'tcx>, Strength>;
 
-    // A hacky thing which is used to remember the dependncies we need to seed the expander with
-    dep_set: RefCell<IndexSet<Dependency<'tcx>>>,
+#[derive(Default)]
+struct DepGraphBuilder<'tcx> {
+    graph: DepGraph<'tcx>,
+    /// Dependencies to process.
+    expansion_queue: VecDeque<Dependency<'tcx>>,
+    /// Set to ensure each dependency is pushed at most once in the queue.
+    visited: HashSet<Dependency<'tcx>>,
+}
+
+impl<'tcx> DepGraphBuilder<'tcx> {
+    /// The source item itself is kept out of the graph.
+    fn new(source: Dependency<'tcx>) -> Self {
+        let mut graph = Self::default();
+        graph.visited.insert(source);
+        graph
+    }
+
+    /// Add a direct dependency of the source item
+    fn add_node(&mut self, d: Dependency<'tcx>) {
+        if self.visited.insert(d) {
+            self.graph.add_node(d);
+            self.expansion_queue.push_back(d);
+        }
+    }
+
+    /// Add `t` as a dependency of `s`
+    fn add_edge(&mut self, s: Dependency<'tcx>, strength: Strength, t: Dependency<'tcx>) {
+        if let Some(old) = self.graph.add_edge(s, t, strength) {
+            if old > strength {
+                self.graph.add_edge(s, t, old);
+            }
+        } else if self.visited.insert(t) {
+            self.expansion_queue.push_back(t);
+        }
+    }
 }
 
 pub(crate) struct CloneNames<'a, 'tcx> {
@@ -357,19 +398,13 @@ pub(crate) struct CloneNames<'a, 'tcx> {
 }
 
 impl<'a, 'tcx> CloneNames<'a, 'tcx> {
-    fn new(
-        ctx: &'a TranslationCtx<'tcx>,
-        source_id: DefId,
-        typing_env: TypingEnv<'tcx>,
-        span_mode: SpanMode,
-        bitwise_mode: bool,
-    ) -> Self {
+    fn new(ctx: &'a TranslationCtx<'tcx>, source_id: DefId) -> Self {
         CloneNames {
             ctx,
             source_id,
-            typing_env,
-            span_mode,
-            bitwise_mode,
+            typing_env: ctx.typing_env(source_id),
+            span_mode: ctx.opts.span_mode.clone(),
+            bitwise_mode: is_bitwise(ctx.tcx, source_id),
             names: Default::default(),
             spans: Default::default(),
             constant_setters: Setters::new(),
@@ -409,11 +444,10 @@ impl Kind {
 
 impl<'a, 'tcx> Dependencies<'a, 'tcx> {
     pub(crate) fn new(ctx: &'a TranslationCtx<'tcx>, self_id: DefId) -> Self {
-        let bw = is_bitwise(ctx.tcx, self_id);
-        let names =
-            CloneNames::new(ctx, self_id, ctx.typing_env(self_id), ctx.opts.span_mode.clone(), bw);
         debug!("cloning self: {:?}", self_id);
-        Dependencies { names, dep_set: Default::default() }
+        let names = CloneNames::new(ctx, self_id);
+        let dep_graph = RefCell::new(DepGraphBuilder::new(names.source_item()));
+        Dependencies { names, dep_graph }
     }
 
     /// Get a name for the `Namespace` type, _without_ adding it to the list of dependencies.
@@ -427,31 +461,13 @@ impl<'a, 'tcx> Dependencies<'a, 'tcx> {
         let mut decls = Vec::new();
         let typing_env = self.typing_env();
         let source_id = self.source_id();
-        let source_item = self.source_item();
         let span = tcx.def_span(source_id);
 
-        let graph = Expander::new(
-            ctx,
-            &mut self.names,
-            typing_env,
-            self.dep_set.into_inner().into_iter().filter(|d| *d != source_item),
-            span,
-        );
-
-        // Update the clone graph with any new entries.
-        let (graph, mut bodies) = graph.update_graph(ctx);
+        let graph =
+            Expander::new(ctx, &mut self.names, self.dep_graph.into_inner(), typing_env, span);
+        let (graph, mut bodies) = graph.update_graph();
 
         for scc in petgraph::algo::tarjan_scc(&graph).into_iter() {
-            if scc.iter().any(|node| node == &source_item) {
-                if scc.len() != 1 {
-                    ctx.dcx().span_bug(
-                        ctx.def_span(source_id),
-                        format!("{} {scc:?}", ctx.def_path_str(source_id)),
-                    )
-                }
-                continue;
-            }
-
             // Then we construct a sub-graph ignoring weak edges.
             let mut subgraph = DiGraphMap::new();
 

creusot/src/backend/clone_map/elaborator.rs

@@ -1,7 +1,7 @@
 use crate::{
     backend::{
         self, Why3Generator,
-        clone_map::{CloneNames, Dependency, Kind, Namer},
+        clone_map::{CloneNames, DepGraphBuilder, Dependency, Kind, Namer},
         closures::{closure_hist_inv, closure_post, closure_pre},
         is_trusted_item,
         logic::{lower_logical_defn, spec_axioms},
@@ -24,19 +24,14 @@ use crate::{
         traits::TraitResolved,
     },
 };
-use petgraph::graphmap::DiGraphMap;
 use rustc_ast::Mutability;
 use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::ty::{
     self, AliasTyKind, Const, GenericArg, GenericArgsRef, TraitRef, Ty, TyCtxt, TyKind, TypingEnv,
 };
 use rustc_span::{DUMMY_SP, Span, Symbol};
 use rustc_type_ir::{AliasTy, ClosureKind, ConstKind, EarlyBinder};
-use std::{
-    assert_matches,
-    cell::RefCell,
-    collections::{HashMap, HashSet, VecDeque},
-};
+use std::{assert_matches, cell::RefCell, collections::HashMap};
 use why3::{
     Exp, Ident, Name,
     coma::{Defn, Expr, Param, Prototype},
@@ -57,12 +52,11 @@ pub enum Strength {
 /// The `Expander` takes a list of 'root' dependencies (items explicitly requested by user code),
 /// and expands this into a complete dependency graph.
 pub(super) struct Expander<'a, 'ctx, 'tcx> {
-    graph: DiGraphMap<Dependency<'tcx>, Strength>,
     dep_bodies: HashMap<Dependency<'tcx>, Vec<Decl>>,
     namer: &'a mut CloneNames<'ctx, 'tcx>,
     ctx: &'a Why3Generator<'tcx>,
     typing_env: TypingEnv<'tcx>,
-    expansion_queue: VecDeque<(Dependency<'tcx>, Strength, Dependency<'tcx>)>,
+    dep_graph: DepGraphBuilder<'tcx>,
     /// Span for the item we are expanding
     root_span: Span,
 }
@@ -75,13 +69,13 @@ impl<'a, 'ctx, 'tcx> HasTyCtxt<'tcx> for Expander<'a, 'ctx, 'tcx> {
 
 struct ExpansionProxy<'a, 'ctx, 'tcx> {
     namer: &'a mut CloneNames<'ctx, 'tcx>,
-    expansion_queue: RefCell<&'a mut VecDeque<(Dependency<'tcx>, Strength, Dependency<'tcx>)>>,
+    dep_graph: RefCell<&'a mut DepGraphBuilder<'tcx>>,
     source: Dependency<'tcx>,
 }
 
 impl<'tcx> Namer<'tcx> for ExpansionProxy<'_, '_, 'tcx> {
     fn raw_dependency(&self, dep: Dependency<'tcx>) -> &Kind {
-        self.expansion_queue.borrow_mut().push_back((self.source, Strength::Strong, dep));
+        self.dep_graph.borrow_mut().add_edge(self.source, Strength::Strong, dep);
         self.namer.raw_dependency(dep)
     }
 
@@ -188,17 +182,10 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
         let dep = Dependency::Item(def_id, subst);
         let ctx = self.ctx;
 
+        let mut add_edge = |axiom| self.dep_graph.add_edge(dep, Strength::Weak, axiom);
         match ctx.intrinsic(def_id) {
-            Intrinsic::Inv => self.expansion_queue.push_back((
-                dep,
-                Strength::Weak,
-                Dependency::TyInvAxiom(subst.type_at(0)),
-            )),
-            Intrinsic::Resolve => self.expansion_queue.push_back((
-                dep,
-                Strength::Weak,
-                Dependency::ResolveAxiom(subst.type_at(0)),
-            )),
+            Intrinsic::Inv => add_edge(Dependency::TyInvAxiom(subst.type_at(0))),
+            Intrinsic::Resolve => add_edge(Dependency::ResolveAxiom(subst.type_at(0))),
             _ => (),
         }
 
@@ -545,53 +532,27 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
     pub(crate) fn new(
         ctx: &'a Why3Generator<'tcx>,
         namer: &'a mut CloneNames<'ctx, 'tcx>,
+        dep_graph: DepGraphBuilder<'tcx>,
         typing_env: TypingEnv<'tcx>,
-        initial: impl Iterator<Item = Dependency<'tcx>>,
         span: Span,
     ) -> Self {
-        let source_item = namer.source_item();
-        Self {
-            graph: Default::default(),
-            namer,
-            ctx,
-            typing_env,
-            expansion_queue: initial.map(|b| (source_item, Strength::Strong, b)).collect(),
-            dep_bodies: Default::default(),
-            root_span: span,
-        }
+        Self { namer, ctx, typing_env, dep_graph, dep_bodies: Default::default(), root_span: span }
     }
 
     fn namer(&mut self, source: Dependency<'tcx>) -> ExpansionProxy<'_, 'ctx, 'tcx> {
-        ExpansionProxy {
-            namer: self.namer,
-            expansion_queue: RefCell::new(&mut self.expansion_queue),
-            source,
-        }
+        ExpansionProxy { namer: self.namer, dep_graph: RefCell::new(&mut self.dep_graph), source }
     }
 
     /// Expand the graph with new entries
-    pub fn update_graph(
-        mut self,
-        ctx: &Why3Generator<'tcx>,
-    ) -> (DiGraphMap<Dependency<'tcx>, Strength>, HashMap<Dependency<'tcx>, Vec<Decl>>) {
-        let mut visited = HashSet::new();
-        while let Some((s, strength, t)) = self.expansion_queue.pop_front() {
-            if let Some(old) = self.graph.add_edge(s, t, strength)
-                && old > strength
-            {
-                self.graph.add_edge(s, t, old);
-            }
-
-            if !visited.insert(t) {
-                continue;
-            }
-            self.expand(ctx, t);
+    pub fn update_graph(mut self) -> (super::DepGraph<'tcx>, HashMap<Dependency<'tcx>, Vec<Decl>>) {
+        while let Some(t) = self.dep_graph.expansion_queue.pop_front() {
+            self.expand(t);
         }
-
-        (self.graph, self.dep_bodies)
+        (self.dep_graph.graph, self.dep_bodies)
     }
 
-    fn expand(&mut self, ctx: &Why3Generator<'tcx>, dep: Dependency<'tcx>) {
+    fn expand(&mut self, dep: Dependency<'tcx>) {
+        let ctx = self.ctx;
         self.expand_laws(dep);
 
         let decls = match dep {
@@ -693,7 +654,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
         for law in self.ctx.laws(item_container) {
             let law_dep = self.namer(dep).resolve_dependency(Dependency::Item(*law, item_subst));
             // We add a weak dep from `dep` to make sure it appears close to the triggering item
-            self.expansion_queue.push_back((dep, Strength::Weak, law_dep));
+            self.dep_graph.add_edge(dep, Strength::Weak, law_dep);
         }
     }
 }