From 85a550a53d373d593c72d814ac17d27549bb5f37 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 26 Jul 2024 11:24:09 -0700 Subject: [PATCH] Correctness fixes and performance improvements --- .../transform/check_uninit/delayed_ub/mod.rs | 3 +- .../delayed_ub/points_to_analysis.rs | 28 ++++++++------- .../delayed_ub/points_to_graph.rs | 34 +++++++++++++------ 3 files changed, 39 insertions(+), 26 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index e390b8ec030d..e31aa8826ab7 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs @@ -24,7 +24,6 @@ use points_to_graph::GlobalMemLoc; use points_to_graph::LocalMemLoc; use points_to_graph::PointsToGraph; use rustc_middle::ty::TyCtxt; -use rustc_mir_dataflow::JoinSemiLattice; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; @@ -113,7 +112,7 @@ impl GlobalPass for DelayedUbPass { call_graph, PointsToGraph::empty(), ); - global_points_to_graph.join(&results); + global_points_to_graph.consume(results); } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs index 971ec1b108a8..c18719c380c8 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs @@ -21,7 +21,7 @@ use rustc_middle::{ }, ty::{Instance, InstanceKind, List, ParamEnv, TyCtxt, TyKind}, }; -use rustc_mir_dataflow::{Analysis, AnalysisDomain, Forward, JoinSemiLattice}; +use rustc_mir_dataflow::{Analysis, AnalysisDomain, Forward}; use rustc_smir::rustc_internal; use rustc_span::source_map::Spanned; use std::collections::HashSet; @@ -50,9 +50,11 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { let mut cursor = analysis.into_engine(tcx, &body).iterate_to_fixpoint().into_results_cursor(&body); let mut results = PointsToGraph::empty(); - for (idx, _) in body.basic_blocks.iter().enumerate() { - cursor.seek_to_block_end(idx.into()); - results.join(cursor.get()); + for (idx, bb) in body.basic_blocks.iter().enumerate() { + if let TerminatorKind::Return = bb.terminator().kind { + cursor.seek_to_block_end(idx.into()); + results.consume(cursor.get().clone()); + } } results } @@ -73,8 +75,8 @@ impl<'a, 'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'a, 'tcx> { /// Dataflow state instantiated at the entry into the body, this should be the current dataflow /// graph. fn initialize_start_block(&self, body: &Body<'tcx>, state: &mut Self::Domain) { - state.join(&self.initial_graph); - state.join(&PointsToGraph::from_body(body, self.def_id)); + state.consume(self.initial_graph.clone()); + state.consume(PointsToGraph::from_body(body, self.def_id)); } } @@ -209,7 +211,7 @@ impl<'a, 'tcx> Analysis<'tcx> for PointsToAnalysis<'a, 'tcx> { &mut self, state: &mut Self::Domain, terminator: &'mir Terminator<'tcx>, - _location: Location, + location: Location, ) -> TerminatorEdges<'mir, 'tcx> { if let TerminatorKind::Call { func, args, destination, .. } = &terminator.kind { let instance = match try_resolve_instance(&self.body, func, self.tcx) { @@ -382,9 +384,9 @@ impl<'a, 'tcx> Analysis<'tcx> for PointsToAnalysis<'a, 'tcx> { // which creates a new node we need to add to the points-to graph. "alloc::alloc::__rust_alloc" | "alloc::alloc::__rust_alloc_zeroed" => { let lvalue_set = state.follow_from_place(*destination, self.def_id); - let rvalue_set = HashSet::from([ - LocalMemLoc::new_alloc().with_def_id(self.def_id) - ]); + let rvalue_set = + HashSet::from([LocalMemLoc::new_alloc(self.def_id, location) + .with_def_id(self.def_id)]); state.extend(&lvalue_set, &rvalue_set); } _ => {} @@ -504,8 +506,8 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { for arg in args.iter() { match arg.node { Operand::Copy(place) | Operand::Move(place) => { - initial_graph.join( - &state.transitive_closure(state.follow_from_place(place, self.def_id)), + initial_graph.consume( + state.transitive_closure(state.follow_from_place(place, self.def_id)), ); } Operand::Constant(_) => {} @@ -560,7 +562,7 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { initial_graph, ); // Merge the results into the current state. - state.join(&new_result); + state.consume(new_result); // Connect the return value to the return destination. let lvalue_set = state.follow_from_place(*destination, self.def_id); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_graph.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_graph.rs index abf8615784e8..e6c28fa48a8b 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_graph.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_graph.rs @@ -5,19 +5,17 @@ use rustc_hir::def_id::DefId; use rustc_middle::{ - mir::{Body, Place, ProjectionElem}, + mir::{Body, Location, Place, ProjectionElem}, ty::List, }; use rustc_mir_dataflow::{fmt::DebugWithContext, JoinSemiLattice}; -use std::{ - collections::{HashMap, HashSet, VecDeque}, - sync::atomic::{AtomicUsize, Ordering}, -}; +use std::collections::{HashMap, HashSet, VecDeque}; /// A node in the points-to graph, which could be a place on the stack or a heap allocation. #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq)] pub enum LocalMemLoc<'tcx> { - Alloc(usize), + /// Using a combination of DefId + Location implements allocation-site abstraction. + Alloc(DefId, Location), Place(Place<'tcx>), } @@ -52,9 +50,8 @@ impl<'tcx> From> for LocalMemLoc<'tcx> { impl<'tcx> LocalMemLoc<'tcx> { /// Generate a new alloc with increasing allocation id. - pub fn new_alloc() -> Self { - static NEXT_ALLOC_ID: AtomicUsize = AtomicUsize::new(0); - LocalMemLoc::Alloc(NEXT_ALLOC_ID.fetch_add(1, Ordering::Relaxed)) + pub fn new_alloc(def_id: DefId, location: Location) -> Self { + LocalMemLoc::Alloc(def_id, location) } /// Tag the node with a DefId. @@ -160,7 +157,12 @@ impl<'tcx> PointsToGraph<'tcx> { /// Find a transitive closure of the graph starting from a given place. pub fn transitive_closure(&self, targets: HashSet>) -> PointsToGraph<'tcx> { let mut result = PointsToGraph::empty(); + // Working queue. let mut queue = VecDeque::from_iter(targets); + // Add all statics, as they can be accessed at any point. + let statics = self.edges.keys().filter(|node| matches!(node, GlobalMemLoc::Global(_))); + queue.extend(statics); + // Add all entries. while !queue.is_empty() { let next_target = queue.pop_front().unwrap(); result.edges.entry(next_target).or_insert_with(|| { @@ -180,6 +182,14 @@ impl<'tcx> PointsToGraph<'tcx> { .expect(format!("unable to retrieve {:?} from points-to graph", target).as_str()) .clone() } + + // Merge the other graph into self, consuming it. + pub fn consume(&mut self, other: PointsToGraph<'tcx>) { + for (from, to) in other.edges { + let existing_to = self.edges.entry(from).or_default(); + existing_to.extend(to); + } + } } /// Since we are performing the analysis using a dataflow, we need to implement a proper monotonous @@ -195,10 +205,12 @@ impl<'tcx> JoinSemiLattice for PointsToGraph<'tcx> { if self.edges.contains_key(from) { // Check if there are any edges that are in the other graph but not in the original // graph. - if to.difference(self.edges.get(from).unwrap()).count() != 0 { + let difference: HashSet<_> = + to.difference(self.edges.get(from).unwrap()).cloned().collect(); + if difference.len() != 0 { updated = true; // Add all edges to the original graph. - self.edges.get_mut(from).unwrap().extend(to.iter()); + self.edges.get_mut(from).unwrap().extend(difference); } } else { // If node does not exist, add the node and all edges from it.