From 0f2ed21446a005f42d92588202005d9476c08984 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 22 Aug 2024 15:57:14 -0400 Subject: [PATCH] Ensure that intermediate union field accesses are instrumented --- .../check_uninit/ptr_uninit/uninit_visitor.rs | 8 +++++++- tests/expected/uninit/unions.expected | 9 +++++++-- tests/expected/uninit/unions.rs | 12 ++++++------ 3 files changed, 20 insertions(+), 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 index 745605478505..8b4812fbafa8 100644 --- 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 index 05fdac3a8765..e0c543a89665 100644 --- 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 index faf92578aa1e..04b00c5ebf10 100644 --- 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.