Mitigate issues with non-deterministic memory initialization instrume…

…ntation

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -267,8 +267,8 @@ impl CodegenBackend for GotocCodegenBackend {
                     for unit in units.iter() {
                         // We reset the body cache for now because each codegen unit has different
                         // configurations that affect how we transform the instance body.
-                        let mut transformer = BodyTransformation::new(&queries, tcx, &unit);
                         for harness in &unit.harnesses {
+                            let transformer = BodyTransformation::new(&queries, tcx, &unit);
                             let model_path = units.harness_model_path(*harness).unwrap();
                             let contract_metadata =
                                 contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap();
@@ -280,7 +280,7 @@ impl CodegenBackend for GotocCodegenBackend {
                                 contract_metadata,
                                 transformer,
                             );
-                            transformer = results.extend(gcx, items, None);
+                            results.extend(gcx, items, None);
                             if let Some(assigns_contract) = contract_info {
                                 modifies_instances.push((*harness, assigns_contract));
                             }

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs

@@ -111,8 +111,6 @@ impl GlobalPass for DelayedUbPass {
                         tcx,
                         internal_def_id,
                         call_graph,
-                        &instances,
-                        transformer,
                         PointsToGraph::empty(),
                     );
                     global_points_to_graph.join(&results);

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs

@@ -9,7 +9,6 @@ use crate::kani_middle::{
     transform::{
         check_uninit::delayed_ub::points_to_graph::{GlobalMemLoc, LocalMemLoc, PointsToGraph},
         internal_mir::RustcInternalMir,
-        BodyTransformation,
     },
 };
 use rustc_ast::Mutability;
@@ -25,7 +24,6 @@ use rustc_middle::{
 use rustc_mir_dataflow::{Analysis, AnalysisDomain, Forward, JoinSemiLattice};
 use rustc_smir::rustc_internal;
 use rustc_span::source_map::Spanned;
-use stable_mir::mir::mono::Instance as StableInstance;
 use std::collections::HashSet;
 
 /// Main points-to analysis object. Since this one will be created anew for each instance analysis,
@@ -35,8 +33,6 @@ pub struct PointsToAnalysis<'a, 'tcx> {
     body: Body<'tcx>,
     tcx: TyCtxt<'tcx>,
     call_graph: &'a CallGraph,
-    instances: &'a Vec<StableInstance>,
-    transformer: &'a mut BodyTransformation,
     initial_graph: PointsToGraph<'tcx>,
 }
 
@@ -48,19 +44,9 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
         tcx: TyCtxt<'tcx>,
         def_id: DefId,
         call_graph: &'a CallGraph,
-        instances: &'a Vec<StableInstance>,
-        transformer: &'a mut BodyTransformation,
         initial_graph: PointsToGraph<'tcx>,
     ) -> PointsToGraph<'tcx> {
-        let analysis = Self {
-            body: body.clone(),
-            tcx,
-            def_id,
-            call_graph,
-            instances,
-            transformer,
-            initial_graph,
-        };
+        let analysis = Self { body: body.clone(), tcx, def_id, call_graph, initial_graph };
         let mut cursor =
             analysis.into_engine(tcx, &body).iterate_to_fixpoint().into_results_cursor(&body);
         let mut results = PointsToGraph::empty();
@@ -86,11 +72,7 @@ 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: &rustc_middle::mir::Body<'tcx>,
-        state: &mut Self::Domain,
-    ) {
+    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));
     }
@@ -511,9 +493,8 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
     ) {
         // Here we simply call another function, so need to retrieve internal body for it.
         let new_body = {
-            let internal_instance = rustc_internal::stable(instance);
-            assert!(self.instances.contains(&internal_instance));
-            let stable_body = self.transformer.body(self.tcx, rustc_internal::stable(instance));
+            let stable_instance = rustc_internal::stable(instance);
+            let stable_body = stable_instance.body().unwrap();
             stable_body.internal_mir(self.tcx)
         };
 
@@ -576,8 +557,6 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
             self.tcx,
             instance.def_id(),
             self.call_graph,
-            self.instances,
-            self.transformer,
             initial_graph,
         );
         // Merge the results into the current state.

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_graph.rs

@@ -135,10 +135,12 @@ impl<'tcx> PointsToGraph<'tcx> {
 
     /// Dump the graph into a file using the graphviz format for later visualization.
     pub fn dump(&self, file_path: &str) {
-        let nodes: Vec<String> =
+        let mut nodes: Vec<String> =
             self.edges.keys().map(|from| format!("\t\"{:?}\"", from)).collect();
+        nodes.sort();
         let nodes_str = nodes.join("\n");
-        let edges: Vec<String> = self
+
+        let mut edges: Vec<String> = self
             .edges
             .iter()
             .flat_map(|(from, to)| {
@@ -149,7 +151,9 @@ impl<'tcx> PointsToGraph<'tcx> {
                 })
             })
             .collect();
+        edges.sort();
         let edges_str = edges.join("\n");
+
         std::fs::write(file_path, format!("digraph {{\n{}\n{}\n}}", nodes_str, edges_str)).unwrap();
     }
 

kani-compiler/src/kani_middle/transform/mod.rs

@@ -192,8 +192,8 @@ pub struct GlobalPasses {
 impl GlobalPasses {
     pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self {
         let mut global_passes = GlobalPasses { global_passes: vec![] };
-        global_passes.add_global_pass(queries, DumpMirPass::new(tcx));
         global_passes.add_global_pass(queries, DelayedUbPass::new(CheckType::new_assert(tcx)));
+        global_passes.add_global_pass(queries, DumpMirPass::new(tcx));
         global_passes
     }