Ensure that intermediate union field accesses are instrumented

model-checking · Aug 22, 2024 · 0f2ed21 · 0f2ed21
1 parent 8ef14f0
commit 0f2ed21
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 9 deletions.
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
@@ -407,9 +407,15 @@ impl MirVisitor for CheckUninitVisitor {
                     if intermediate_place.ty(&self.locals).unwrap().kind().is_union()
                         && !ptx.is_mutating()
                     {
+                        // Generate a place which includes all projections until (and including)
+                        // union field access.
+                        let union_field_access_place = Place {
+                            local: place.local,
+                            projection: place.projection[..idx + 1].to_vec(),
+                        };
                         // Accessing a place inside the union, need to check if it is initialized.
                         self.push_target(MemoryInitOp::CheckRef {
-                            operand: Operand::Copy(place.clone()),
+                            operand: Operand::Copy(union_field_access_place.clone()),
                         });
                     }
                 }

diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected
@@ -4,14 +4,19 @@ union_update_should_fail.assertion.1\
 
 union_complex_subfields_should_fail.assertion.1\
 	 - Status: FAILURE\
-	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`"
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `(u32, u16, u8)`"
 
 basic_union_should_fail.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`"
 
+union_uninit_inside_projection_should_fail.assertion.1\
+	 - Status: FAILURE\
+	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `(u32, u16, u8)`"
+
 Summary:
 Verification failed for - union_update_should_fail
+Verification failed for - union_uninit_inside_projection_should_fail
 Verification failed for - union_complex_subfields_should_fail
 Verification failed for - basic_union_should_fail
-Complete - 3 successfully verified harnesses, 3 failures, 6 total.
+Complete - 2 successfully verified harnesses, 4 failures, 6 total.
diff --git a/tests/expected/uninit/unions.rs b/tests/expected/uninit/unions.rs
@@ -35,18 +35,18 @@ union U1 {
     b: (u32, u16, u8),
 }
 
-/// Tests accessing initialized data via subfields of a union.
+/// Tests accessing uninit data via subfields of a union.
 #[kani::proof]
-unsafe fn union_complex_subfields_should_pass() {
+unsafe fn union_complex_subfields_should_fail() {
     let u = U1 { a: (0, 0) };
-    let non_padding = u.b.0;
+    let non_padding = u.b.1;
 }
 
-/// Tests accessing uninit data via subfields of a union.
+/// Tests accessing uninitialized data inside a place projection.
 #[kani::proof]
-unsafe fn union_complex_subfields_should_fail() {
+unsafe fn union_uninit_inside_projection_should_fail() {
     let u = U1 { a: (0, 0) };
-    let non_padding = u.b.1;
+    let non_padding = u.b.0;
 }
 
 /// Tests overwriting data inside unions.