Add more tests, remove unnecessary nodes from the graph

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

@@ -74,9 +74,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) {
+ fn initialize_start_block(&self, _body: &Body<'tcx>, state: &mut Self::Domain) {
  state.consume(self.initial_graph.clone());
- state.consume(PointsToGraph::from_body(body, self.def_id));
  }
 }
 

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

@@ -5,7 +5,7 @@
 
 use rustc_hir::def_id::DefId;
 use rustc_middle::{
- mir::{Body, Location, Place, ProjectionElem},
+ mir::{Location, Place, ProjectionElem},
  ty::List,
 };
 use rustc_mir_dataflow::{fmt::DebugWithContext, JoinSemiLattice};
@@ -78,16 +78,6 @@ impl<'tcx> PointsToGraph<'tcx> {
  Self { edges: HashMap::new() }
  }
 
- /// Create a new graph, adding all existing places without projections from a body.
- pub fn from_body(body: &Body, def_id: DefId) -> Self {
- let places = (0..body.local_decls.len()).map(|local| {
- let place: LocalMemLoc =
- Place { local: local.into(), projection: List::empty() }.into();
- (place.with_def_id(def_id), HashSet::new())
- });
- Self { edges: HashMap::from_iter(places) }
- }
-
  /// Collect all nodes which have incoming edges from `nodes`.
  pub fn follow(&self, nodes: &HashSet<GlobalMemLoc<'tcx>>) -> HashSet<GlobalMemLoc<'tcx>> {
  nodes.iter().flat_map(|node| self.edges.get(node).cloned().unwrap_or_default()).collect()
@@ -177,10 +167,7 @@ impl<'tcx> PointsToGraph<'tcx> {
 
  /// Retrieve all places to which a given place is pointing to.
  pub fn pointees_of(&self, target: &GlobalMemLoc<'tcx>) -> HashSet<GlobalMemLoc<'tcx>> {
- self.edges
- .get(&target)
- .expect(format!("unable to retrieve {:?} from points-to graph", target).as_str())
- .clone()
+ self.edges.get(&target).unwrap_or(&HashSet::new()).clone()
  }
 
  // Merge the other graph into self, consuming it.

tests/expected/uninit/delayed-ub/delayed-ub.rs

@@ -123,3 +123,44 @@ fn delayed_ub_copy() {
  assert!(value > 0); // UB: This reads a padding value!
  }
 }
+
+struct S {
+ u: U,
+}
+
+struct U {
+ value1: u128,
+ value2: u64,
+ value3: u32,
+}
+
+struct Inner<T>(*mut T);
+
+/// Delayed UB via mutable pointer write into inner fields of structs.
+#[kani::proof]
+fn delayed_ub_structs() {
+ unsafe {
+ // Create a convoluted struct.
+ let mut s: S = S { u: U { value1: 0, value2: 0, value3: 0 } };
+ // Get a pointer to an inner field of the struct. Then, cast between two pointers of
+ // different padding.
+ let inner = Inner(&mut s.u.value2 as *mut _);
+ let inner_cast = Inner(inner.0 as *mut (u8, u32));
+ let ptr = inner_cast.0;
+ *ptr = (4, 4);
+ let u: U = s.u; // UB: This reads a padding value inside the inner struct!
+ }
+}
+
+/// Delayed UB via mutable pointer write into a slice element.
+#[kani::proof]
+fn delayed_ub_slices() {
+ unsafe {
+ // Create an array.
+ let mut arr = [0u128; 4];
+ // Get a pointer to a part of the array.
+ let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32);
+ *ptr = (4, 4);
+ let arr_copy = arr; // UB: This reads a padding value inside the array!
+ }
+}

tests/expected/uninit/delayed-ub/expected

@@ -1,3 +1,15 @@
+Checking harness delayed_ub_slices...
+
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`
+
+VERIFICATION:- FAILED
+
+Checking harness delayed_ub_structs...
+
+Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `U`
+
+VERIFICATION:- FAILED
+
 Checking harness delayed_ub_copy...
 
 Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128`
@@ -41,11 +53,13 @@ Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type
 VERIFICATION:- FAILED
 
 Summary:
+Verification failed for - delayed_ub_slices
+Verification failed for - delayed_ub_structs
 Verification failed for - delayed_ub_copy
 Verification failed for - delayed_ub_closure_capture_laundered
 Verification failed for - delayed_ub_closure_laundered
 Verification failed for - delayed_ub_laundered
 Verification failed for - delayed_ub_static
 Verification failed for - delayed_ub_transmute
 Verification failed for - delayed_ub
-Complete - 0 successfully verified harnesses, 7 failures, 7 total.
+Complete - 0 successfully verified harnesses, 9 failures, 9 total.