From 28d1288af4e0ad18b51e522bc6e32a7a4eb80d1b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 23 Oct 2024 11:29:53 -0400 Subject: [PATCH 1/2] fix issue 3631 --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 11 +++++ tests/expected/issue-3631/issue-3631.expected | 1 + tests/expected/issue-3631/issue-3631.rs | 44 +++++++++++++++++++ 3 files changed, 56 insertions(+) create mode 100644 tests/expected/issue-3631/issue-3631.expected create mode 100644 tests/expected/issue-3631/issue-3631.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 779874f2ff77..7f578940d98e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -726,6 +726,17 @@ impl GotocCtx<'_> { dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) } } + TyKind::RigidTy(RigidTy::Dynamic(..)) => { + let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); + let data_cast = + data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); + let meta = self.codegen_operand_stable(&operands[1]); + let vtable_expr = meta + .member("_vtable_ptr", &self.symbol_table) + .member("pointer", &self.symbol_table) + .cast_to(typ.lookup_field_type("vtable", &self.symbol_table).unwrap()); + dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + } _ => { let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }) diff --git a/tests/expected/issue-3631/issue-3631.expected b/tests/expected/issue-3631/issue-3631.expected new file mode 100644 index 000000000000..f9a64dc8af9a --- /dev/null +++ b/tests/expected/issue-3631/issue-3631.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESS \ No newline at end of file diff --git a/tests/expected/issue-3631/issue-3631.rs b/tests/expected/issue-3631/issue-3631.rs new file mode 100644 index 000000000000..6f1d2d2c6aa0 --- /dev/null +++ b/tests/expected/issue-3631/issue-3631.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(ptr_metadata)] + +use std::ptr::NonNull; + +trait SampleTrait { + fn get_value(&self) -> i32; +} + +struct SampleStruct { + value: i32, +} + +impl SampleTrait for SampleStruct { + fn get_value(&self) -> i32 { + self.value + } +} + +#[cfg(kani)] +#[kani::proof] +fn main() { + // Create a SampleTrait object from SampleStruct + let sample_struct = SampleStruct { value: kani::any() }; + let trait_object: &dyn SampleTrait = &sample_struct; + + // Get the raw data pointer and metadata for the trait object + let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); + let metadata = std::ptr::metadata(trait_object); + + // Create NonNull from the data pointer and metadata + let nonnull_trait_object: NonNull = + NonNull::from_raw_parts(trait_ptr, metadata); + + unsafe { + // Ensure trait method and member is preserved + kani::assert( + trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), + "trait method and member must correctly preserve", + ); + } +} From 0c82f57ded8841737ec385d07e208081d810e31f Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 23 Oct 2024 14:03:14 -0400 Subject: [PATCH 2/2] move test --- tests/expected/issue-3631/issue-3631.expected | 1 - .../CodegenAggregateRawPtrTraitObject/main.rs} | 4 +++- 2 files changed, 3 insertions(+), 2 deletions(-) delete mode 100644 tests/expected/issue-3631/issue-3631.expected rename tests/{expected/issue-3631/issue-3631.rs => kani/CodegenAggregateRawPtrTraitObject/main.rs} (86%) diff --git a/tests/expected/issue-3631/issue-3631.expected b/tests/expected/issue-3631/issue-3631.expected deleted file mode 100644 index f9a64dc8af9a..000000000000 --- a/tests/expected/issue-3631/issue-3631.expected +++ /dev/null @@ -1 +0,0 @@ -VERIFICATION:- SUCCESS \ No newline at end of file diff --git a/tests/expected/issue-3631/issue-3631.rs b/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs similarity index 86% rename from tests/expected/issue-3631/issue-3631.rs rename to tests/kani/CodegenAggregateRawPtrTraitObject/main.rs index 6f1d2d2c6aa0..92ffb413ae70 100644 --- a/tests/expected/issue-3631/issue-3631.rs +++ b/tests/kani/CodegenAggregateRawPtrTraitObject/main.rs @@ -1,5 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// Test that Kani can verify code that produces a aggregate raw pointer to trait objects +// c.f. https://github.com/model-checking/kani/issues/3631 #![feature(ptr_metadata)] @@ -21,7 +23,7 @@ impl SampleTrait for SampleStruct { #[cfg(kani)] #[kani::proof] -fn main() { +fn check_nonnull_dyn_from_raw_parts() { // Create a SampleTrait object from SampleStruct let sample_struct = SampleStruct { value: kani::any() }; let trait_object: &dyn SampleTrait = &sample_struct;