Correctness fixes and performance improvements

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);
  }
  }
 

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);

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<Place<'tcx>> 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<GlobalMemLoc<'tcx>>) -> 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.