diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index 91ba22b2da..a15cf471e8 100644 --- a/creusot/src/backend/clone_map.rs +++ b/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>, +} + +/// Dependencies of a source item. +type DepGraph<'tcx> = DiGraphMap, Strength>; - // A hacky thing which is used to remember the dependncies we need to seed the expander with - dep_set: RefCell>>, +#[derive(Default)] +struct DepGraphBuilder<'tcx> { + graph: DepGraph<'tcx>, + /// Dependencies to process. + expansion_queue: VecDeque>, + /// Set to ensure each dependency is pushed at most once in the queue. + visited: HashSet>, +} + +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(); diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs index cfddf45a79..1fa5efd202 100644 --- a/creusot/src/backend/clone_map/elaborator.rs +++ b/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,7 +24,6 @@ use crate::{ traits::TraitResolved, }, }; -use petgraph::graphmap::DiGraphMap; use rustc_ast::Mutability; use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::{ @@ -32,11 +31,7 @@ use rustc_middle::ty::{ }; 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, Strength>, dep_bodies: HashMap, Vec>, 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>, 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, Strength>, HashMap, Vec>) { - 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, Vec>) { + 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); } } }