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 c18719c380c8..75eabc754ba5 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 @@ -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)); } } 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 e6c28fa48a8b..82f059b20716 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,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>) -> HashSet> { 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> { - 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. diff --git a/tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs b/tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs deleted file mode 100644 index df769e39a8b2..000000000000 --- a/tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs +++ /dev/null @@ -1,14 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z uninit-checks - -/// Checks that Kani rejects mutable pointer casts between types of different padding. -#[kani::proof] -fn invalid_value() { - unsafe { - let mut value: u128 = 0; - let ptr: *mut (u8, u32, u64) = std::mem::transmute(&mut value as *mut _); - *ptr = (4, 4, 4); // This assignment itself does not cause UB... - let c: u128 = value; // ...but this reads a padding value! - } -} diff --git a/tests/expected/uninit/delayed-ub-transmute/expected b/tests/expected/uninit/delayed-ub-transmute/expected deleted file mode 100644 index 960efcdade40..000000000000 --- a/tests/expected/uninit/delayed-ub-transmute/expected +++ /dev/null @@ -1,5 +0,0 @@ -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128` - -VERIFICATION:- FAILED - -Complete - 0 successfully verified harnesses, 1 failures, 1 total. \ No newline at end of file diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index 74196d144f0a..feee4bcd161f 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/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(*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! + } +} diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected index d0145966b002..06dc9e24ea12 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/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,6 +53,8 @@ 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 @@ -48,4 +62,4 @@ 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.