From 117950957c8e96bcd70ab0dae19f71cd720e4237 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 1 Aug 2024 17:17:57 -0400 Subject: [PATCH 1/4] test for modifies attribute with zst --- .../modifies/zst_pass.expected | 6 +++++ .../function-contract/modifies/zst_pass.rs | 24 +++++++++++++++++++ 2 files changed, 30 insertions(+) create mode 100644 tests/expected/function-contract/modifies/zst_pass.expected create mode 100644 tests/expected/function-contract/modifies/zst_pass.rs diff --git a/tests/expected/function-contract/modifies/zst_pass.expected b/tests/expected/function-contract/modifies/zst_pass.expected new file mode 100644 index 000000000000..b9fc25648279 --- /dev/null +++ b/tests/expected/function-contract/modifies/zst_pass.expected @@ -0,0 +1,6 @@ +.assertion\ +- Status: SUCCESS\ +- Description: "ptr NULL or writable up to size"\ +in function __CPROVER_contracts_car_set_insert + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/zst_pass.rs b/tests/expected/function-contract/modifies/zst_pass.rs new file mode 100644 index 000000000000..0d6aa2772444 --- /dev/null +++ b/tests/expected/function-contract/modifies/zst_pass.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// #[kani::requires(assert_valid_ptr(dst) && has_valid_value(dst))] +#[kani::requires(true)] +#[kani::modifies(dst)] +pub unsafe fn replace(dst: *mut T, src: T) -> T { + std::ptr::replace(dst, src) +} + +#[kani::proof_for_contract(replace)] +pub fn check_replace_unit() { + check_replace_impl::<()>(); +} + +fn check_replace_impl() { + let mut dst = T::any(); + let orig = dst.clone(); + let src = T::any(); + let ret = unsafe { replace(&mut dst, src.clone()) }; + assert_eq!(ret, orig); + assert_eq!(dst, src); +} \ No newline at end of file From b04a47abe126570e1cca91d5a82fd6332b55fe14 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 5 Aug 2024 09:26:56 -0400 Subject: [PATCH 2/4] filter out zsts for cmbc assigns for contracts --- .../src/codegen_cprover_gotoc/codegen/contract.rs | 10 ++++++++-- tests/expected/function-contract/modifies/zst_pass.rs | 4 +--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index b210b2c9333e..a871cd58f94f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::codegen_cprover_gotoc::GotocCtx; +use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx}; use crate::kani_middle::attributes::KaniAttributes; use cbmc::goto_program::FunctionContract; use cbmc::goto_program::{Expr, Lambda, Location, Type}; @@ -160,11 +160,17 @@ impl<'tcx> GotocCtx<'tcx> { let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else { unreachable!("found {:?}", modifies_ty.kind()) }; + + for ty in &modifies_tys { + assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty); + } + let assigns: Vec<_> = modifies_tys .into_iter() + // do not attempt to dereference (and assign) a ZST + .filter(|ty| !self.is_zst_stable(pointee_type_stable(*ty).unwrap())) .enumerate() .map(|(idx, ty)| { - assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty); let ptr = modifies_args.clone().member(idx.to_string(), &self.symbol_table); if self.is_fat_pointer_stable(ty) { let unref = match ty.kind() { diff --git a/tests/expected/function-contract/modifies/zst_pass.rs b/tests/expected/function-contract/modifies/zst_pass.rs index 0d6aa2772444..89efd85a75f9 100644 --- a/tests/expected/function-contract/modifies/zst_pass.rs +++ b/tests/expected/function-contract/modifies/zst_pass.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -// #[kani::requires(assert_valid_ptr(dst) && has_valid_value(dst))] -#[kani::requires(true)] #[kani::modifies(dst)] pub unsafe fn replace(dst: *mut T, src: T) -> T { std::ptr::replace(dst, src) @@ -21,4 +19,4 @@ fn check_replace_impl() { let ret = unsafe { replace(&mut dst, src.clone()) }; assert_eq!(ret, orig); assert_eq!(dst, src); -} \ No newline at end of file +} From 66a40c9b4e420dfa10ff07e4489576e0e48c976c Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 5 Aug 2024 09:41:55 -0400 Subject: [PATCH 3/4] remove function from expected output --- tests/expected/function-contract/modifies/zst_pass.expected | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/expected/function-contract/modifies/zst_pass.expected b/tests/expected/function-contract/modifies/zst_pass.expected index b9fc25648279..ba2a8eb7decd 100644 --- a/tests/expected/function-contract/modifies/zst_pass.expected +++ b/tests/expected/function-contract/modifies/zst_pass.expected @@ -1,6 +1,5 @@ .assertion\ - Status: SUCCESS\ - Description: "ptr NULL or writable up to size"\ -in function __CPROVER_contracts_car_set_insert VERIFICATION:- SUCCESSFUL From 61515b6d9a4c5a5284cbb5bfcf9980152c73b4f2 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 5 Aug 2024 10:55:12 -0400 Subject: [PATCH 4/4] update tests to reflect fix --- tests/std-checks/core/mem.expected | 6 +----- tests/std-checks/core/ptr.expected | 3 +-- tests/std-checks/core/src/mem.rs | 2 -- tests/std-checks/core/src/ptr.rs | 2 -- 4 files changed, 2 insertions(+), 11 deletions(-) diff --git a/tests/std-checks/core/mem.expected b/tests/std-checks/core/mem.expected index 1484c83901fc..285a887307f8 100644 --- a/tests/std-checks/core/mem.expected +++ b/tests/std-checks/core/mem.expected @@ -1,7 +1,3 @@ Checking harness mem::verify::check_swap_unit... -Failed Checks: ptr NULL or writable up to size - -Summary: -Verification failed for - mem::verify::check_swap_unit -Complete - 6 successfully verified harnesses, 1 failures, 7 total. +Complete - 7 successfully verified harnesses, 0 failures, 7 total. diff --git a/tests/std-checks/core/ptr.expected b/tests/std-checks/core/ptr.expected index 43d3bd6baf60..d6c2aff26442 100644 --- a/tests/std-checks/core/ptr.expected +++ b/tests/std-checks/core/ptr.expected @@ -1,4 +1,3 @@ Summary: -Verification failed for - ptr::verify::check_replace_unit Verification failed for - ptr::verify::check_as_ref_dangling -Complete - 4 successfully verified harnesses, 2 failures, 6 total. +Complete - 5 successfully verified harnesses, 1 failures, 6 total. diff --git a/tests/std-checks/core/src/mem.rs b/tests/std-checks/core/src/mem.rs index b0400d0a75f5..67b03d7a6188 100644 --- a/tests/std-checks/core/src/mem.rs +++ b/tests/std-checks/core/src/mem.rs @@ -48,8 +48,6 @@ mod verify { contracts::swap(&mut x, &mut y) } - /// FIX-ME: Modifies clause fail with pointer to ZST. - /// #[kani::proof_for_contract(contracts::swap)] pub fn check_swap_unit() { let mut x: () = kani::any(); diff --git a/tests/std-checks/core/src/ptr.rs b/tests/std-checks/core/src/ptr.rs index 49cf9e168214..1560889b56b3 100644 --- a/tests/std-checks/core/src/ptr.rs +++ b/tests/std-checks/core/src/ptr.rs @@ -89,8 +89,6 @@ mod verify { let _rf = unsafe { contracts::as_ref(&non_null) }; } - /// FIX-ME: Modifies clause fail with pointer to ZST. - /// #[kani::proof_for_contract(contracts::replace)] pub fn check_replace_unit() { check_replace_impl::<()>();