From 33be6183efde8b73a6d2d31ee24716ddc50d996c Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 25 Jun 2024 17:12:44 -0400 Subject: [PATCH 01/23] initial working for bytesize --- .../codegen_cprover_gotoc/codegen/contract.rs | 45 ++++++++++-- library/kani/src/internal.rs | 70 ++++++++++++++++--- .../src/sysroot/contracts/check.rs | 12 +++- .../src/sysroot/contracts/replace.rs | 2 +- 4 files changed, 110 insertions(+), 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 0f27d3f119f7..b56cf746adff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -3,7 +3,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::attributes::KaniAttributes; use cbmc::goto_program::FunctionContract; -use cbmc::goto_program::{Lambda, Location}; +use cbmc::goto_program::{Expr, Lambda, Location, Type}; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; @@ -121,11 +121,44 @@ impl<'tcx> GotocCtx<'tcx> { let assigns = modified_places .into_iter() .map(|local| { - Lambda::as_contract_for( - &goto_annotated_fn_typ, - None, - self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(), - ) + if self.is_fat_pointer_stable(self.local_ty_stable(local)) { + Lambda::as_contract_for( + &goto_annotated_fn_typ, + None, + Expr::symbol_expression( + "__CPROVER_object_upto", + Type::code( + vec![ + Type::empty() + .to_pointer() + .as_parameter(None, Some("ptr".into())), + Type::size_t().as_parameter(None, Some("size".into())), + ], + Type::empty(), + ), + ) + .call(vec![ + self.codegen_place_stable(&local.into(), loc) + .unwrap() + .goto_expr + .member("data", &self.symbol_table) + .cast_to(Type::empty().to_pointer()), + self.codegen_place_stable(&local.into(), loc) + .unwrap() + .goto_expr + .member("len", &self.symbol_table), + ]), + ) + } else { + Lambda::as_contract_for( + &goto_annotated_fn_typ, + None, + self.codegen_place_stable(&local.into(), loc) + .unwrap() + .goto_expr + .dereference(), + ) + } }) .collect(); diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index a910c333b112..cc676cadb8cb 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -7,7 +7,7 @@ #[doc(hidden)] pub trait Pointer<'a> { /// Type of the pointed-to data - type Inner; + type Inner: ?Sized; /// Used for checking assigns contracts where we pass immutable references to the function. /// @@ -16,7 +16,7 @@ pub trait Pointer<'a> { unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> &'a mut Self::Inner; + unsafe fn fill_any(self); } impl<'a, 'b, T> Pointer<'a> for &'b T { @@ -26,8 +26,8 @@ impl<'a, 'b, T> Pointer<'a> for &'b T { } #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - std::mem::transmute(self as *const T) + unsafe fn fill_any(self) { + *std::mem::transmute::<*const T, &mut T>(self as *const T) = crate::any_modifies(); } } @@ -39,8 +39,8 @@ impl<'a, 'b, T> Pointer<'a> for &'b mut T { std::mem::transmute::<_, &&'a T>(self) } - unsafe fn assignable(self) -> &'a mut Self::Inner { - std::mem::transmute(self) + unsafe fn fill_any(self) { + *std::mem::transmute::<&mut T, &mut T>(self) = crate::any_modifies(); } } @@ -51,8 +51,8 @@ impl<'a, T> Pointer<'a> for *const T { } #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - std::mem::transmute(self) + unsafe fn fill_any(self) { + *std::mem::transmute::<*const T, &mut T>(self) = crate::any_modifies(); } } @@ -63,8 +63,58 @@ impl<'a, T> Pointer<'a> for *mut T { } #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - std::mem::transmute(self) + unsafe fn fill_any(self) { + *std::mem::transmute::<*mut T, &mut T>(self) = crate::any_modifies(); + } +} + +impl<'a, 'b, T> Pointer<'a> for &'b [T] { + type Inner = [T]; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + std::mem::transmute(*self) + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn fill_any(self) { + std::mem::transmute::<*const [T], &mut [T]>(self as *const [T]) + .fill_with(|| crate::any_modifies::()); + } +} + +impl<'a, 'b, T> Pointer<'a> for &'b mut [T] { + type Inner = [T]; + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + std::mem::transmute::<_, &&'a [T]>(self) + } + + unsafe fn fill_any(self) { + std::mem::transmute::<&mut [T], &mut [T]>(self).fill_with(|| crate::any_modifies::()); + } +} + +impl<'a, T> Pointer<'a> for *const [T] { + type Inner = [T]; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + &**self as &'a [T] + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn fill_any(self) { + std::mem::transmute::<*const [T], &mut [T]>(self).fill_with(|| crate::any_modifies::()); + } +} + +impl<'a, T> Pointer<'a> for *mut [T] { + type Inner = [T]; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + &**self as &'a [T] + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn fill_any(self) { + std::mem::transmute::<*mut [T], &mut [T]>(self).fill_with(|| crate::any_modifies::()); } } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index e76286b398cb..f804fc70c5f5 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -156,11 +156,19 @@ impl<'a> ContractConditionsHandler<'a> { let sig = &mut self.annotated_fn.sig; for (arg, arg_type) in wrapper_args.clone().zip(type_params) { // Add the type parameter to the function signature's generic parameters list + let mut bounds: syn::punctuated::Punctuated = + syn::punctuated::Punctuated::new(); + bounds.push(syn::TypeParamBound::Trait(syn::TraitBound { + paren_token: None, + modifier: syn::TraitBoundModifier::Maybe(Token![?](Span::call_site())), + lifetimes: None, + path: syn::Ident::new("Sized", Span::call_site()).into(), + })); sig.generics.params.push(syn::GenericParam::Type(syn::TypeParam { attrs: vec![], ident: arg_type.clone(), - colon_token: None, - bounds: Default::default(), + colon_token: Some(Token![:](Span::call_site())), + bounds: bounds, eq_token: None, default: None, })); diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 7a522ea98e08..07c4e06ffbd1 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -94,7 +94,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(*unsafe { kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(#attr))) } = kani::any_modifies();)* + #(unsafe {kani::internal::Pointer::fill_any(kani::internal::untracked_deref(&#attr))};)* #(#after)* #result ) From 3437710cf2d1ed67a8d27cd82c02382e82efb5e8 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 25 Jun 2024 17:17:08 -0400 Subject: [PATCH 02/23] add tests --- .../nondeterministic_size.expected | 5 +++++ .../modifies_slice/nondeterministic_size.rs | 17 +++++++++++++++++ .../modifies_slice/u8slice.expected | 5 +++++ .../function-contract/modifies_slice/u8slice.rs | 17 +++++++++++++++++ 4 files changed, 44 insertions(+) create mode 100644 tests/expected/function-contract/modifies_slice/nondeterministic_size.expected create mode 100644 tests/expected/function-contract/modifies_slice/nondeterministic_size.rs create mode 100644 tests/expected/function-contract/modifies_slice/u8slice.expected create mode 100644 tests/expected/function-contract/modifies_slice/u8slice.rs diff --git a/tests/expected/function-contract/modifies_slice/nondeterministic_size.expected b/tests/expected/function-contract/modifies_slice/nondeterministic_size.expected new file mode 100644 index 000000000000..cff437881d00 --- /dev/null +++ b/tests/expected/function-contract/modifies_slice/nondeterministic_size.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_slice/nondeterministic_size.rs b/tests/expected/function-contract/modifies_slice/nondeterministic_size.rs new file mode 100644 index 000000000000..9eb01b2a3244 --- /dev/null +++ b/tests/expected/function-contract/modifies_slice/nondeterministic_size.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test that modifies a slice of nondeterministic size + +#[kani::modifies(x)] +#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +fn zero(x: &mut [u8]) { + x.fill(0) +} + +#[kani::proof_for_contract(zero)] +fn harness() { + let mut x = [0..kani::any()].map(|_| kani::any()); + zero(&mut x); +} diff --git a/tests/expected/function-contract/modifies_slice/u8slice.expected b/tests/expected/function-contract/modifies_slice/u8slice.expected new file mode 100644 index 000000000000..cff437881d00 --- /dev/null +++ b/tests/expected/function-contract/modifies_slice/u8slice.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_slice/u8slice.rs b/tests/expected/function-contract/modifies_slice/u8slice.rs new file mode 100644 index 000000000000..d249949e7a9a --- /dev/null +++ b/tests/expected/function-contract/modifies_slice/u8slice.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test that modifies a slice containing bytesize data + +#[kani::modifies(x)] +#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +fn zero(x: &mut [u8]) { + x.fill(0) +} + +#[kani::proof_for_contract(zero)] +fn harness() { + let mut x = [kani::any(), kani::any(), kani::any()]; + zero(&mut x); +} From 90a5d3fa3b9776b2de9ad5df13457c7527ab3028 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 26 Jun 2024 15:14:50 -0400 Subject: [PATCH 03/23] arbitrary size slices --- .../codegen_cprover_gotoc/codegen/contract.rs | 23 ++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index b56cf746adff..5a056410c5f8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -12,6 +12,8 @@ use stable_mir::mir::Local; use stable_mir::CrateDef; use tracing::debug; +use stable_mir::ty::{RigidTy, TyKind}; + impl<'tcx> GotocCtx<'tcx> { /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`, /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol @@ -122,6 +124,21 @@ impl<'tcx> GotocCtx<'tcx> { .into_iter() .map(|local| { if self.is_fat_pointer_stable(self.local_ty_stable(local)) { + let unref = match self.local_ty_stable(local).kind() { + TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => ty, + kind => unreachable!("{:?} is not a reference", kind), + }; + let size = match unref.kind() { + TyKind::RigidTy(RigidTy::Slice(elt_type)) => { + elt_type.layout().unwrap().shape().size.bytes() + } + TyKind::RigidTy(RigidTy::Str) => 8, + // For adt, see https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp + TyKind::RigidTy(RigidTy::Adt(..)) => { + todo!("Adt fat pointers not implemented") + } + kind => unreachable!("Generating a slice fat pointer to {:?}", kind), + }; Lambda::as_contract_for( &goto_annotated_fn_typ, None, @@ -146,7 +163,11 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_place_stable(&local.into(), loc) .unwrap() .goto_expr - .member("len", &self.symbol_table), + .member("len", &self.symbol_table) + .mul(Expr::size_constant( + size.try_into().unwrap(), + &self.symbol_table, + )), ]), ) } else { From 13ebd4e3e756bbe63af5b6dfdcf537e063fd907d Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 26 Jun 2024 15:17:02 -0400 Subject: [PATCH 04/23] new test --- .../nondeterministic_size.expected | 0 .../nondeterministic_size.rs | 0 .../u32slice.expected} | 0 .../modifies_fat_pointer/u32slice.rs | 17 +++++++++++++++++ .../modifies_fat_pointer/u8slice.expected | 5 +++++ .../u8slice.rs | 0 6 files changed, 22 insertions(+) rename tests/expected/function-contract/{modifies_slice => modifies_fat_pointer}/nondeterministic_size.expected (100%) rename tests/expected/function-contract/{modifies_slice => modifies_fat_pointer}/nondeterministic_size.rs (100%) rename tests/expected/function-contract/{modifies_slice/u8slice.expected => modifies_fat_pointer/u32slice.expected} (100%) create mode 100644 tests/expected/function-contract/modifies_fat_pointer/u32slice.rs create mode 100644 tests/expected/function-contract/modifies_fat_pointer/u8slice.expected rename tests/expected/function-contract/{modifies_slice => modifies_fat_pointer}/u8slice.rs (100%) diff --git a/tests/expected/function-contract/modifies_slice/nondeterministic_size.expected b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected similarity index 100% rename from tests/expected/function-contract/modifies_slice/nondeterministic_size.expected rename to tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected diff --git a/tests/expected/function-contract/modifies_slice/nondeterministic_size.rs b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs similarity index 100% rename from tests/expected/function-contract/modifies_slice/nondeterministic_size.rs rename to tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs diff --git a/tests/expected/function-contract/modifies_slice/u8slice.expected b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected similarity index 100% rename from tests/expected/function-contract/modifies_slice/u8slice.expected rename to tests/expected/function-contract/modifies_fat_pointer/u32slice.expected diff --git a/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs b/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs new file mode 100644 index 000000000000..403cd7c48fdd --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test that modifies a slice containing bytesize data + +#[kani::modifies(x)] +#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +fn zero(x: &mut [u32]) { + x.fill(0) +} + +#[kani::proof_for_contract(zero)] +fn harness() { + let mut x = [kani::any(), kani::any(), kani::any()]; + zero(&mut x); +} diff --git a/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected new file mode 100644 index 000000000000..cff437881d00 --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_slice/u8slice.rs b/tests/expected/function-contract/modifies_fat_pointer/u8slice.rs similarity index 100% rename from tests/expected/function-contract/modifies_slice/u8slice.rs rename to tests/expected/function-contract/modifies_fat_pointer/u8slice.rs From c1163ff50988ffde5f9f48ede39bce583d7acdaa Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 26 Jun 2024 15:40:15 -0400 Subject: [PATCH 05/23] any instead of any_modifies --- library/kani/src/internal.rs | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index cc676cadb8cb..3149fc15e4a2 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -19,7 +19,7 @@ pub trait Pointer<'a> { unsafe fn fill_any(self); } -impl<'a, 'b, T> Pointer<'a> for &'b T { +impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute(*self) @@ -27,11 +27,11 @@ impl<'a, 'b, T> Pointer<'a> for &'b T { #[allow(clippy::transmute_ptr_to_ref)] unsafe fn fill_any(self) { - *std::mem::transmute::<*const T, &mut T>(self as *const T) = crate::any_modifies(); + *std::mem::transmute::<*const T, &mut T>(self as *const T) = crate::any(); } } -impl<'a, 'b, T> Pointer<'a> for &'b mut T { +impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b mut T { type Inner = T; #[allow(clippy::transmute_ptr_to_ref)] @@ -40,11 +40,11 @@ impl<'a, 'b, T> Pointer<'a> for &'b mut T { } unsafe fn fill_any(self) { - *std::mem::transmute::<&mut T, &mut T>(self) = crate::any_modifies(); + *std::mem::transmute::<&mut T, &mut T>(self) = crate::any(); } } -impl<'a, T> Pointer<'a> for *const T { +impl<'a, T: crate::Arbitrary> Pointer<'a> for *const T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T @@ -52,11 +52,11 @@ impl<'a, T> Pointer<'a> for *const T { #[allow(clippy::transmute_ptr_to_ref)] unsafe fn fill_any(self) { - *std::mem::transmute::<*const T, &mut T>(self) = crate::any_modifies(); + *std::mem::transmute::<*const T, &mut T>(self) = crate::any(); } } -impl<'a, T> Pointer<'a> for *mut T { +impl<'a, T: crate::Arbitrary> Pointer<'a> for *mut T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T @@ -64,11 +64,11 @@ impl<'a, T> Pointer<'a> for *mut T { #[allow(clippy::transmute_ptr_to_ref)] unsafe fn fill_any(self) { - *std::mem::transmute::<*mut T, &mut T>(self) = crate::any_modifies(); + *std::mem::transmute::<*mut T, &mut T>(self) = crate::any(); } } -impl<'a, 'b, T> Pointer<'a> for &'b [T] { +impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b [T] { type Inner = [T]; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute(*self) @@ -77,11 +77,11 @@ impl<'a, 'b, T> Pointer<'a> for &'b [T] { #[allow(clippy::transmute_ptr_to_ref)] unsafe fn fill_any(self) { std::mem::transmute::<*const [T], &mut [T]>(self as *const [T]) - .fill_with(|| crate::any_modifies::()); + .fill_with(|| crate::any::()); } } -impl<'a, 'b, T> Pointer<'a> for &'b mut [T] { +impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b mut [T] { type Inner = [T]; #[allow(clippy::transmute_ptr_to_ref)] @@ -90,11 +90,11 @@ impl<'a, 'b, T> Pointer<'a> for &'b mut [T] { } unsafe fn fill_any(self) { - std::mem::transmute::<&mut [T], &mut [T]>(self).fill_with(|| crate::any_modifies::()); + std::mem::transmute::<&mut [T], &mut [T]>(self).fill_with(|| crate::any::()); } } -impl<'a, T> Pointer<'a> for *const [T] { +impl<'a, T: crate::Arbitrary> Pointer<'a> for *const [T] { type Inner = [T]; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a [T] @@ -102,11 +102,11 @@ impl<'a, T> Pointer<'a> for *const [T] { #[allow(clippy::transmute_ptr_to_ref)] unsafe fn fill_any(self) { - std::mem::transmute::<*const [T], &mut [T]>(self).fill_with(|| crate::any_modifies::()); + std::mem::transmute::<*const [T], &mut [T]>(self).fill_with(|| crate::any::()); } } -impl<'a, T> Pointer<'a> for *mut [T] { +impl<'a, T: crate::Arbitrary> Pointer<'a> for *mut [T] { type Inner = [T]; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a [T] @@ -114,7 +114,7 @@ impl<'a, T> Pointer<'a> for *mut [T] { #[allow(clippy::transmute_ptr_to_ref)] unsafe fn fill_any(self) { - std::mem::transmute::<*mut [T], &mut [T]>(self).fill_with(|| crate::any_modifies::()); + std::mem::transmute::<*mut [T], &mut [T]>(self).fill_with(|| crate::any::()); } } From 0248c7706793c0ba8e06fff50154f005dd328b98 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Mon, 1 Jul 2024 15:32:17 -0400 Subject: [PATCH 06/23] new compilation phase --- .../src/kani_middle/transform/contracts.rs | 91 +++++++++++++++++++ .../src/kani_middle/transform/mod.rs | 3 +- library/kani/src/internal.rs | 58 ++---------- library/kani/src/lib.rs | 14 +++ .../src/sysroot/contracts/replace.rs | 2 +- 5 files changed, 116 insertions(+), 52 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index f5760bd4d829..4c54ad33b53d 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -166,3 +166,94 @@ impl AnyModifiesPass { } } } + +/// Check if we can replace calls to havoc. +/// +/// This pass will replace the entire body, and it should only be applied to stubs +/// that have a body. +#[derive(Debug)] +pub struct HavocPass { + kani_any_modifies: Option, + kani_havoc: Option, + stubbed: HashSet, + target_fn: Option, +} + +impl TransformPass for HavocPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + // TODO: Check if this is the harness has proof_for_contract + query_db.args().unstable_features.contains(&"function-contracts".to_string()) + } + + /// Transform the function body by replacing it with the stub body. + fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "HavocPass::transform"); + + if self.should_apply(tcx, instance) { self.replace_havoc(body) } else { (false, body) } + } +} + +impl HavocPass { + /// Build the pass with non-extern function stubs. + pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> HavocPass { + let item_fn_def = |item| { + let TyKind::RigidTy(RigidTy::FnDef(def, _)) = + rustc_internal::stable(tcx.type_of(item)).value.kind() + else { + unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item)) + }; + def + }; + let kani_havoc = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavoc")) + .map(item_fn_def); + let kani_any_modifies = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) + .map(item_fn_def); + let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() { + let attributes = KaniAttributes::for_instance(tcx, *harness); + let target_fn = + attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern()); + (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::>()) + } else { + (None, HashSet::new()) + }; + HavocPass { kani_any_modifies, kani_havoc, target_fn, stubbed } + } + + fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool { + let item_attributes = + KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id())); + self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion() + } + + /// Replace calls to `any_modifies` by calls to `any`. + fn replace_havoc(&self, mut body: Body) -> (bool, Body) { + let mut changed = false; + let locals = body.locals().to_vec(); + for bb in body.blocks.iter_mut() { + let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else { continue }; + if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = + func.ty(&locals).unwrap().kind() + && Some(def) == self.kani_havoc + { + if args.len() != 1 { + panic!("kani::havoc should have exactly one arg") + } + // TODO: create an MIR bb to replace bb with the proper stuff + // changed = true; + } + } + (changed, body) + } +} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 8d5c61f55c92..b6ea0f582e69 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -19,7 +19,7 @@ use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_values::ValidValuePass; -use crate::kani_middle::transform::contracts::AnyModifiesPass; +use crate::kani_middle::transform::contracts::{AnyModifiesPass, HavocPass}; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; @@ -62,6 +62,7 @@ impl BodyTransformation { transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); // This has to come after stubs since we want this to replace the stubbed body. + transformer.add_pass(queries, HavocPass::new(tcx, &unit)); transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); transformer.add_pass(queries, IntrinsicGeneratorPass { check_type }); diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index b35a74c29343..d09a86ad804f 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -14,108 +14,66 @@ pub trait Pointer<'a> { /// We're using a reference to self here, because the user can use just a plain function /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; - - /// used for havocking on replecement of a `modifies` clause. - unsafe fn fill_any(self); } -impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b T { +impl<'a, 'b, T> Pointer<'a> for &'b T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute(*self) } - - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn fill_any(self) { - *std::mem::transmute::<*const T, &mut T>(self as *const T) = crate::any(); - } } -impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b mut T { +impl<'a, 'b, T> Pointer<'a> for &'b mut T { type Inner = T; #[allow(clippy::transmute_ptr_to_ref)] unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute::<_, &&'a T>(self) } - - unsafe fn fill_any(self) { - *std::mem::transmute::<&mut T, &mut T>(self) = crate::any(); - } } -impl<'a, T: crate::Arbitrary> Pointer<'a> for *const T { +impl<'a, T> Pointer<'a> for *const T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } - - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn fill_any(self) { - *std::mem::transmute::<*const T, &mut T>(self) = crate::any(); - } } -impl<'a, T: crate::Arbitrary> Pointer<'a> for *mut T { +impl<'a, T> Pointer<'a> for *mut T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } - - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn fill_any(self) { - *std::mem::transmute::<*mut T, &mut T>(self) = crate::any(); - } } -impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b [T] { +impl<'a, 'b, T> Pointer<'a> for &'b [T] { type Inner = [T]; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute(*self) } - - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn fill_any(self) { - std::mem::transmute::<*const [T], &mut [T]>(self as *const [T]) - .fill_with(|| crate::any::()); - } } -impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b mut [T] { +impl<'a, 'b, T> Pointer<'a> for &'b mut [T] { type Inner = [T]; #[allow(clippy::transmute_ptr_to_ref)] unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute::<_, &&'a [T]>(self) } - - unsafe fn fill_any(self) { - std::mem::transmute::<&mut [T], &mut [T]>(self).fill_with(|| crate::any::()); - } } -impl<'a, T: crate::Arbitrary> Pointer<'a> for *const [T] { +impl<'a, T> Pointer<'a> for *const [T] { type Inner = [T]; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a [T] } - - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn fill_any(self) { - std::mem::transmute::<*const [T], &mut [T]>(self).fill_with(|| crate::any::()); - } } -impl<'a, T: crate::Arbitrary> Pointer<'a> for *mut [T] { +impl<'a, T> Pointer<'a> for *mut [T] { type Inner = [T]; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a [T] } - - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn fill_any(self) { - std::mem::transmute::<*mut [T], &mut [T]>(self).fill_with(|| crate::any::()); - } } /// A way to break the ownerhip rules. Only used by contracts where we can diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index acf1e08e0441..00c5a944e24b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -180,6 +180,20 @@ pub fn any_modifies() -> T { unreachable!() } +/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. +/// Only for use within function contracts and will not be replaced if the recursive or function stub +/// replace contracts are not used. +#[rustc_diagnostic_item = "KaniHavoc"] +#[inline(never)] +#[doc(hidden)] +pub fn havoc(_pointer: &T) { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() +} + /// This creates a symbolic *valid* value of type `T`. /// The value is constrained to be a value accepted by the predicate passed to the filter. /// You can assign the return value of this function to a variable that you want to make symbolic. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 07c4e06ffbd1..b2c08f902224 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -94,7 +94,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(unsafe {kani::internal::Pointer::fill_any(kani::internal::untracked_deref(&#attr))};)* + #(kani::havoc(&#attr);)* #(#after)* #result ) From 1fd0849f1bbde857fb8d4fad501aaacd09ce0989 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Mon, 8 Jul 2024 14:51:53 -0400 Subject: [PATCH 07/23] hack --- .../src/kani_middle/transform/contracts.rs | 155 +++++++----------- .../src/kani_middle/transform/mod.rs | 3 +- library/kani/src/internal.rs | 49 +++--- library/kani/src/lib.rs | 20 ++- .../src/sysroot/contracts/replace.rs | 2 +- .../nondeterministic_size.expected | 2 +- .../nondeterministic_size.rs | 2 +- .../modifies_fat_pointer/u32slice.expected | 2 +- .../modifies_fat_pointer/u32slice.rs | 2 +- .../modifies_fat_pointer/u8slice.expected | 2 +- .../modifies_fat_pointer/u8slice.rs | 2 +- 11 files changed, 108 insertions(+), 133 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 4c54ad33b53d..b5a962377400 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind}; -use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; +use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind, TypeAndMut}; use stable_mir::{CrateDef, DefId}; use std::collections::HashSet; use std::fmt::Debug; @@ -25,6 +25,10 @@ use tracing::{debug, trace}; pub struct AnyModifiesPass { kani_any: Option, kani_any_modifies: Option, + kani_havoc: Option, + kani_havoc_slim: Option, + kani_havoc_slice: Option, + kani_havoc_str: Option, stubbed: HashSet, target_fn: Option, } @@ -78,6 +82,18 @@ impl AnyModifiesPass { let kani_any_modifies = tcx .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) .map(item_fn_def); + let kani_havoc = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavoc")) + .map(item_fn_def); + let kani_havoc_slim = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocSlim")) + .map(item_fn_def); + let kani_havoc_slice = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocSlice")) + .map(item_fn_def); + let kani_havoc_str = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocStr")) + .map(item_fn_def); let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() { let attributes = KaniAttributes::for_instance(tcx, *harness); let target_fn = @@ -86,7 +102,16 @@ impl AnyModifiesPass { } else { (None, HashSet::new()) }; - AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed } + AnyModifiesPass { + kani_any, + kani_any_modifies, + kani_havoc, + kani_havoc_slim, + kani_havoc_slice, + kani_havoc_str, + target_fn, + stubbed, + } } /// If we apply `transform_any_modifies` in all contract-generated items, @@ -105,7 +130,7 @@ impl AnyModifiesPass { let mut changed = false; let locals = body.locals().to_vec(); for bb in body.blocks.iter_mut() { - let TerminatorKind::Call { func, .. } = &mut bb.terminator.kind else { continue }; + let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else { continue }; if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = func.ty(&locals).unwrap().kind() && Some(def) == self.kani_any_modifies @@ -117,6 +142,39 @@ impl AnyModifiesPass { *func = Operand::Constant(new_func); changed = true; } + + if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = + func.ty(&locals).unwrap().kind() + && Some(def) == self.kani_havoc + && args.len() == 1 + && let Some(fn_sig) = func.ty(&locals).unwrap().kind().fn_sig() + && let Some(TypeAndMut { ty: internal_type, mutability: _ }) = + fn_sig.skip_binder().inputs()[0].kind().builtin_deref(true) + { + if let TyKind::RigidTy(RigidTy::Slice(_)) = internal_type.kind() { + let instance = + Instance::resolve(self.kani_havoc_slice.unwrap(), &instance_args).unwrap(); + let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); + let span = bb.terminator.span; + let new_func = ConstOperand { span, user_ty: None, const_: literal }; + *func = Operand::Constant(new_func); + } else if let TyKind::RigidTy(RigidTy::Str) = internal_type.kind() { + let instance = + Instance::resolve(self.kani_havoc_str.unwrap(), &instance_args).unwrap(); + let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); + let span = bb.terminator.span; + let new_func = ConstOperand { span, user_ty: None, const_: literal }; + *func = Operand::Constant(new_func); + } else { + let instance = + Instance::resolve(self.kani_havoc_slim.unwrap(), &instance_args).unwrap(); + let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); + let span = bb.terminator.span; + let new_func = ConstOperand { span, user_ty: None, const_: literal }; + *func = Operand::Constant(new_func); + } + changed = true; + } } (changed, body) } @@ -166,94 +224,3 @@ impl AnyModifiesPass { } } } - -/// Check if we can replace calls to havoc. -/// -/// This pass will replace the entire body, and it should only be applied to stubs -/// that have a body. -#[derive(Debug)] -pub struct HavocPass { - kani_any_modifies: Option, - kani_havoc: Option, - stubbed: HashSet, - target_fn: Option, -} - -impl TransformPass for HavocPass { - fn transformation_type() -> TransformationType - where - Self: Sized, - { - TransformationType::Stubbing - } - - fn is_enabled(&self, query_db: &QueryDb) -> bool - where - Self: Sized, - { - // TODO: Check if this is the harness has proof_for_contract - query_db.args().unstable_features.contains(&"function-contracts".to_string()) - } - - /// Transform the function body by replacing it with the stub body. - fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { - trace!(function=?instance.name(), "HavocPass::transform"); - - if self.should_apply(tcx, instance) { self.replace_havoc(body) } else { (false, body) } - } -} - -impl HavocPass { - /// Build the pass with non-extern function stubs. - pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> HavocPass { - let item_fn_def = |item| { - let TyKind::RigidTy(RigidTy::FnDef(def, _)) = - rustc_internal::stable(tcx.type_of(item)).value.kind() - else { - unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item)) - }; - def - }; - let kani_havoc = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavoc")) - .map(item_fn_def); - let kani_any_modifies = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) - .map(item_fn_def); - let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() { - let attributes = KaniAttributes::for_instance(tcx, *harness); - let target_fn = - attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern()); - (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::>()) - } else { - (None, HashSet::new()) - }; - HavocPass { kani_any_modifies, kani_havoc, target_fn, stubbed } - } - - fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool { - let item_attributes = - KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id())); - self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion() - } - - /// Replace calls to `any_modifies` by calls to `any`. - fn replace_havoc(&self, mut body: Body) -> (bool, Body) { - let mut changed = false; - let locals = body.locals().to_vec(); - for bb in body.blocks.iter_mut() { - let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else { continue }; - if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = - func.ty(&locals).unwrap().kind() - && Some(def) == self.kani_havoc - { - if args.len() != 1 { - panic!("kani::havoc should have exactly one arg") - } - // TODO: create an MIR bb to replace bb with the proper stuff - // changed = true; - } - } - (changed, body) - } -} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index b6ea0f582e69..8d5c61f55c92 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -19,7 +19,7 @@ use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_values::ValidValuePass; -use crate::kani_middle::transform::contracts::{AnyModifiesPass, HavocPass}; +use crate::kani_middle::transform::contracts::AnyModifiesPass; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; @@ -62,7 +62,6 @@ impl BodyTransformation { transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); // This has to come after stubs since we want this to replace the stubbed body. - transformer.add_pass(queries, HavocPass::new(tcx, &unit)); transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); transformer.add_pass(queries, IntrinsicGeneratorPass { check_type }); diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index d09a86ad804f..0825ef4c6a5f 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -14,65 +14,56 @@ pub trait Pointer<'a> { /// We're using a reference to self here, because the user can use just a plain function /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; + + unsafe fn assignable(self) -> &'a mut Self::Inner; } -impl<'a, 'b, T> Pointer<'a> for &'b T { +impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute(*self) } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self as *const T) + } } -impl<'a, 'b, T> Pointer<'a> for &'b mut T { +impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { type Inner = T; #[allow(clippy::transmute_ptr_to_ref)] unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { std::mem::transmute::<_, &&'a T>(self) } -} -impl<'a, T> Pointer<'a> for *const T { - type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self) } } -impl<'a, T> Pointer<'a> for *mut T { +impl<'a, T: ?Sized> Pointer<'a> for *const T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } -} - -impl<'a, 'b, T> Pointer<'a> for &'b [T] { - type Inner = [T]; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - std::mem::transmute(*self) - } -} - -impl<'a, 'b, T> Pointer<'a> for &'b mut [T] { - type Inner = [T]; #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - std::mem::transmute::<_, &&'a [T]>(self) + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self) } } -impl<'a, T> Pointer<'a> for *const [T] { - type Inner = [T]; +impl<'a, T: ?Sized> Pointer<'a> for *mut T { + type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a [T] + &**self as &'a T } -} -impl<'a, T> Pointer<'a> for *mut [T] { - type Inner = [T]; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a [T] + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self) } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 00c5a944e24b..b3407a91467b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -186,7 +186,7 @@ pub fn any_modifies() -> T { #[rustc_diagnostic_item = "KaniHavoc"] #[inline(never)] #[doc(hidden)] -pub fn havoc(_pointer: &T) { +pub fn havoc(_pointer: &T) { // This function should not be reacheable. // Users must include `#[kani::recursion]` in any function contracts for recursive functions; // otherwise, this might not be properly instantiate. We mark this as unreachable to make @@ -194,6 +194,24 @@ pub fn havoc(_pointer: &T) { unreachable!() } +#[rustc_diagnostic_item = "KaniHavocSlice"] +#[inline(always)] +pub fn havoc_slice(slice: &mut [T]) { + slice.fill_with(|| T::any()) +} + +#[rustc_diagnostic_item = "KaniHavocSlim"] +#[inline(always)] +pub fn havoc_slim(pointer: &mut T) { + *pointer = T::any() +} + +#[rustc_diagnostic_item = "KaniHavocStr"] +#[inline(always)] +pub fn havoc_str(s: &mut str) { + todo!() +} + /// This creates a symbolic *valid* value of type `T`. /// The value is constrained to be a value accepted by the predicate passed to the filter. /// You can assign the return value of this function to a variable that you want to make symbolic. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index b2c08f902224..6bd91950f379 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -94,7 +94,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(kani::havoc(&#attr);)* + #(kani::havoc(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)* #(#after)* #result ) diff --git a/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected index cff437881d00..2fab679b5cba 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs index 9eb01b2a3244..faf1d9d44581 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs +++ b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs @@ -5,7 +5,7 @@ // Test that modifies a slice of nondeterministic size #[kani::modifies(x)] -#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))] fn zero(x: &mut [u8]) { x.fill(0) } diff --git a/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected index cff437881d00..2fab679b5cba 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs b/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs index 403cd7c48fdd..4f6177ebec75 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs +++ b/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs @@ -5,7 +5,7 @@ // Test that modifies a slice containing bytesize data #[kani::modifies(x)] -#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))] fn zero(x: &mut [u32]) { x.fill(0) } diff --git a/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected index cff437881d00..2fab679b5cba 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected +++ b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected @@ -1,5 +1,5 @@ assertion\ - Status: SUCCESS\ -- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ +- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/u8slice.rs b/tests/expected/function-contract/modifies_fat_pointer/u8slice.rs index d249949e7a9a..07e213db0adc 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u8slice.rs +++ b/tests/expected/function-contract/modifies_fat_pointer/u8slice.rs @@ -5,7 +5,7 @@ // Test that modifies a slice containing bytesize data #[kani::modifies(x)] -#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))] fn zero(x: &mut [u8]) { x.fill(0) } From d3706a77b732b199234d370cbec2c0b1e385b896 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Mon, 8 Jul 2024 15:04:38 -0400 Subject: [PATCH 08/23] strings --- library/kani/src/lib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index b3407a91467b..96fe3c4a7dbd 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -209,7 +209,8 @@ pub fn havoc_slim(pointer: &mut T) { #[rustc_diagnostic_item = "KaniHavocStr"] #[inline(always)] pub fn havoc_str(s: &mut str) { - todo!() + unsafe{s.as_bytes_mut()}.fill_with(|| u8::any()) + //TODO: String validation } /// This creates a symbolic *valid* value of type `T`. From f28023d61a8cafbbc8118a8ce43a2f8daeda9b8c Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Mon, 8 Jul 2024 15:08:11 -0400 Subject: [PATCH 09/23] fmt --- library/kani/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index a806db2c4c43..5745211d00ec 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -212,7 +212,7 @@ pub fn havoc_slim(pointer: &mut T) { #[rustc_diagnostic_item = "KaniHavocStr"] #[inline(always)] pub fn havoc_str(s: &mut str) { - unsafe{s.as_bytes_mut()}.fill_with(|| u8::any()) + unsafe { s.as_bytes_mut() }.fill_with(|| u8::any()) //TODO: String validation } From 1e336d38e29563733d92ff32d5506eef693187ae Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Mon, 8 Jul 2024 15:15:32 -0400 Subject: [PATCH 10/23] unnecessary closure --- library/kani/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 5745211d00ec..9969ac41d166 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -200,7 +200,7 @@ pub fn havoc(_pointer: &T) { #[rustc_diagnostic_item = "KaniHavocSlice"] #[inline(always)] pub fn havoc_slice(slice: &mut [T]) { - slice.fill_with(|| T::any()) + slice.fill_with(T::any) } #[rustc_diagnostic_item = "KaniHavocSlim"] @@ -212,7 +212,7 @@ pub fn havoc_slim(pointer: &mut T) { #[rustc_diagnostic_item = "KaniHavocStr"] #[inline(always)] pub fn havoc_str(s: &mut str) { - unsafe { s.as_bytes_mut() }.fill_with(|| u8::any()) + unsafe { s.as_bytes_mut() }.fill_with(u8::any) //TODO: String validation } From 96ca60327e9137939cbc9445ceac7a31875902b3 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 9 Jul 2024 13:29:38 -0400 Subject: [PATCH 11/23] move functions --- .../src/kani_middle/transform/contracts.rs | 43 ++++++++------- library/kani/src/internal.rs | 55 +++++++++++++++++++ library/kani/src/lib.rs | 48 ---------------- .../src/sysroot/contracts/replace.rs | 14 +++-- 4 files changed, 88 insertions(+), 72 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 2e307eda7903..e45b5436204b 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -25,10 +25,10 @@ use tracing::{debug, trace}; pub struct AnyModifiesPass { kani_any: Option, kani_any_modifies: Option, - kani_havoc: Option, - kani_havoc_slim: Option, - kani_havoc_slice: Option, - kani_havoc_str: Option, + kani_write_any: Option, + kani_write_any_slim: Option, + kani_write_any_slice: Option, + kani_write_any_str: Option, stubbed: HashSet, target_fn: Option, } @@ -82,17 +82,17 @@ impl AnyModifiesPass { let kani_any_modifies = tcx .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) .map(item_fn_def); - let kani_havoc = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavoc")) + let kani_write_any = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAny")) .map(item_fn_def); - let kani_havoc_slim = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocSlim")) + let kani_write_any_slim = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlim")) .map(item_fn_def); - let kani_havoc_slice = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocSlice")) + let kani_write_any_slice = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlice")) .map(item_fn_def); - let kani_havoc_str = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocStr")) + let kani_write_any_str = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnyStr")) .map(item_fn_def); let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() { let attributes = KaniAttributes::for_instance(tcx, *harness); @@ -105,10 +105,10 @@ impl AnyModifiesPass { AnyModifiesPass { kani_any, kani_any_modifies, - kani_havoc, - kani_havoc_slim, - kani_havoc_slice, - kani_havoc_str, + kani_write_any, + kani_write_any_slim, + kani_write_any_slice, + kani_write_any_str, target_fn, stubbed, } @@ -145,7 +145,7 @@ impl AnyModifiesPass { if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = func.ty(&locals).unwrap().kind() - && Some(def) == self.kani_havoc + && Some(def) == self.kani_write_any && args.len() == 1 && let Some(fn_sig) = func.ty(&locals).unwrap().kind().fn_sig() && let Some(TypeAndMut { ty: internal_type, mutability: _ }) = @@ -153,21 +153,24 @@ impl AnyModifiesPass { { if let TyKind::RigidTy(RigidTy::Slice(_)) = internal_type.kind() { let instance = - Instance::resolve(self.kani_havoc_slice.unwrap(), &instance_args).unwrap(); + Instance::resolve(self.kani_write_any_slice.unwrap(), &instance_args) + .unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); let span = bb.terminator.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } else if let TyKind::RigidTy(RigidTy::Str) = internal_type.kind() { let instance = - Instance::resolve(self.kani_havoc_str.unwrap(), &instance_args).unwrap(); + Instance::resolve(self.kani_write_any_str.unwrap(), &instance_args) + .unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); let span = bb.terminator.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } else { let instance = - Instance::resolve(self.kani_havoc_slim.unwrap(), &instance_args).unwrap(); + Instance::resolve(self.kani_write_any_slim.unwrap(), &instance_args) + .unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); let span = bb.terminator.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 0825ef4c6a5f..d894180f28ba 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::arbitrary::Arbitrary; + /// Helper trait for code generation for `modifies` contracts. /// /// We allow the user to provide us with a pointer-like object that we convert as needed. @@ -96,3 +98,56 @@ pub fn init_contracts() {} pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } + +/// This function is only used for function contract instrumentation. +/// It behaves exaclty like `kani::any()`, except it will check for the trait bounds +/// at compilation time. It allows us to avoid type checking errors while using function +/// contracts only for verification. +#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[rustc_diagnostic_item = "KaniAnyModifies"] +#[inline(never)] +#[doc(hidden)] +pub fn any_modifies() -> T { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() +} + +/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. +/// Only for use within function contracts and will not be replaced if the recursive or function stub +/// replace contracts are not used. +#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[rustc_diagnostic_item = "KaniWriteAny"] +#[inline(never)] +#[doc(hidden)] +pub fn write_any(_pointer: &T) { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() +} + +#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[rustc_diagnostic_item = "KaniWriteAnySlice"] +#[inline(always)] +pub fn write_any_slice(slice: &mut [T]) { + slice.fill_with(T::any) +} + +#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[rustc_diagnostic_item = "KaniWriteAnySlim"] +#[inline(always)] +pub fn write_any_slim(pointer: &mut T) { + *pointer = T::any() +} + +#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[rustc_diagnostic_item = "KaniWriteAnyStr"] +#[inline(always)] +pub fn write_any_str(s: &mut str) { + unsafe { s.as_bytes_mut() }.fill_with(u8::any) + //TODO: String validation +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 9969ac41d166..dedb32846b2d 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -168,54 +168,6 @@ pub fn any() -> T { T::any() } -/// This function is only used for function contract instrumentation. -/// It behaves exaclty like `kani::any()`, except it will check for the trait bounds -/// at compilation time. It allows us to avoid type checking errors while using function -/// contracts only for verification. -#[rustc_diagnostic_item = "KaniAnyModifies"] -#[inline(never)] -#[doc(hidden)] -pub fn any_modifies() -> T { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - -/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. -/// Only for use within function contracts and will not be replaced if the recursive or function stub -/// replace contracts are not used. -#[rustc_diagnostic_item = "KaniHavoc"] -#[inline(never)] -#[doc(hidden)] -pub fn havoc(_pointer: &T) { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - -#[rustc_diagnostic_item = "KaniHavocSlice"] -#[inline(always)] -pub fn havoc_slice(slice: &mut [T]) { - slice.fill_with(T::any) -} - -#[rustc_diagnostic_item = "KaniHavocSlim"] -#[inline(always)] -pub fn havoc_slim(pointer: &mut T) { - *pointer = T::any() -} - -#[rustc_diagnostic_item = "KaniHavocStr"] -#[inline(always)] -pub fn havoc_str(s: &mut str) { - unsafe { s.as_bytes_mut() }.fill_with(u8::any) - //TODO: String validation -} - /// This creates a symbolic *valid* value of type `T`. /// The value is constrained to be a value accepted by the predicate passed to the filter. /// You can assign the return value of this function to a variable that you want to make symbolic. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 6bd91950f379..2172f20fca66 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -40,7 +40,12 @@ impl<'a> ContractConditionsHandler<'a> { if self.is_first_emit() { let return_type = return_type_to_type(&self.annotated_fn.sig.output); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![]) + ( + vec![ + syn::parse_quote!(let #result : #return_type = kani::internal::any_modifies();), + ], + vec![], + ) } else { let stmts = &self.annotated_fn.block.stmts; let idx = stmts @@ -94,7 +99,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(kani::havoc(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)* + #(kani::internal::write_any(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)* #(#after)* #result ) @@ -152,9 +157,10 @@ fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool { path, attrs, }) - if path.segments.len() == 2 + if path.segments.len() == 3 && path.segments[0].ident == "kani" - && path.segments[1].ident == "any_modifies" + && path.segments[1].ident == "internal" + && path.segments[2].ident == "any_modifies" && attrs.is_empty() ) ) From 6cef19b3efc8ca3695647d1ea9f1c4b95e4f4f7b Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 9 Jul 2024 13:37:37 -0400 Subject: [PATCH 12/23] fmt --- library/kani/src/internal.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index d894180f28ba..8ee4a1562244 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -103,7 +103,7 @@ pub fn apply_closure bool>(f: U, x: &T) -> bool { /// It behaves exaclty like `kani::any()`, except it will check for the trait bounds /// at compilation time. It allows us to avoid type checking errors while using function /// contracts only for verification. -#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniAnyModifies"] #[inline(never)] #[doc(hidden)] @@ -118,7 +118,7 @@ pub fn any_modifies() -> T { /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. /// Only for use within function contracts and will not be replaced if the recursive or function stub /// replace contracts are not used. -#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAny"] #[inline(never)] #[doc(hidden)] @@ -130,21 +130,21 @@ pub fn write_any(_pointer: &T) { unreachable!() } -#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlice"] #[inline(always)] pub fn write_any_slice(slice: &mut [T]) { slice.fill_with(T::any) } -#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlim"] #[inline(always)] pub fn write_any_slim(pointer: &mut T) { *pointer = T::any() } -#[crate::unstable(feature="function-contracts", issue="none", reason="function-contracts")] +#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnyStr"] #[inline(always)] pub fn write_any_str(s: &mut str) { From c28bad7dec2ba6ce7e2f0ab4afd1de555500cfee Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 10 Jul 2024 13:40:13 -0400 Subject: [PATCH 13/23] raw pointer --- library/kani/src/internal.rs | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 8ee4a1562244..e8c58bf9545d 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::arbitrary::Arbitrary; +use std::ptr; /// Helper trait for code generation for `modifies` contracts. /// @@ -17,7 +18,7 @@ pub trait Pointer<'a> { /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; - unsafe fn assignable(self) -> &'a mut Self::Inner; + unsafe fn assignable(self) -> *mut Self::Inner; } impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { @@ -27,7 +28,7 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { } #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { + unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self as *const T) } } @@ -40,7 +41,7 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { std::mem::transmute::<_, &&'a T>(self) } - unsafe fn assignable(self) -> &'a mut Self::Inner { + unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self) } } @@ -52,7 +53,7 @@ impl<'a, T: ?Sized> Pointer<'a> for *const T { } #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { + unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self) } } @@ -64,7 +65,7 @@ impl<'a, T: ?Sized> Pointer<'a> for *mut T { } #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { + unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self) } } @@ -122,7 +123,7 @@ pub fn any_modifies() -> T { #[rustc_diagnostic_item = "KaniWriteAny"] #[inline(never)] #[doc(hidden)] -pub fn write_any(_pointer: &T) { +pub fn write_any(_pointer: *mut T) { // This function should not be reacheable. // Users must include `#[kani::recursion]` in any function contracts for recursive functions; // otherwise, this might not be properly instantiate. We mark this as unreachable to make @@ -133,21 +134,21 @@ pub fn write_any(_pointer: &T) { #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlice"] #[inline(always)] -pub fn write_any_slice(slice: &mut [T]) { - slice.fill_with(T::any) +pub fn write_any_slice(slice: *mut [T]) { + unsafe { (*slice).fill_with(T::any) } } #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlim"] #[inline(always)] -pub fn write_any_slim(pointer: &mut T) { - *pointer = T::any() +pub fn write_any_slim(pointer: *mut T) { + unsafe { ptr::write(pointer, T::any()) } } #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnyStr"] #[inline(always)] -pub fn write_any_str(s: &mut str) { - unsafe { s.as_bytes_mut() }.fill_with(u8::any) +pub fn write_any_str(s: *mut str) { + unsafe { (*s).as_bytes_mut() }.fill_with(u8::any) //TODO: String validation } From 52d383970640e34257e161b70a6636a03a778ad7 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 10 Jul 2024 13:48:59 -0400 Subject: [PATCH 14/23] clippy --- library/kani/src/internal.rs | 21 ++++++++----------- .../src/sysroot/contracts/replace.rs | 2 +- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index e8c58bf9545d..7565520fb820 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -27,7 +27,6 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { std::mem::transmute(*self) } - #[allow(clippy::transmute_ptr_to_ref)] unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self as *const T) } @@ -42,7 +41,7 @@ impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { } unsafe fn assignable(self) -> *mut Self::Inner { - std::mem::transmute(self) + self as *mut T } } @@ -52,7 +51,6 @@ impl<'a, T: ?Sized> Pointer<'a> for *const T { &**self as &'a T } - #[allow(clippy::transmute_ptr_to_ref)] unsafe fn assignable(self) -> *mut Self::Inner { std::mem::transmute(self) } @@ -64,9 +62,8 @@ impl<'a, T: ?Sized> Pointer<'a> for *mut T { &**self as &'a T } - #[allow(clippy::transmute_ptr_to_ref)] unsafe fn assignable(self) -> *mut Self::Inner { - std::mem::transmute(self) + self } } @@ -123,7 +120,7 @@ pub fn any_modifies() -> T { #[rustc_diagnostic_item = "KaniWriteAny"] #[inline(never)] #[doc(hidden)] -pub fn write_any(_pointer: *mut T) { +pub unsafe fn write_any(_pointer: *mut T) { // This function should not be reacheable. // Users must include `#[kani::recursion]` in any function contracts for recursive functions; // otherwise, this might not be properly instantiate. We mark this as unreachable to make @@ -134,21 +131,21 @@ pub fn write_any(_pointer: *mut T) { #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlice"] #[inline(always)] -pub fn write_any_slice(slice: *mut [T]) { - unsafe { (*slice).fill_with(T::any) } +pub unsafe fn write_any_slice(slice: *mut [T]) { + (*slice).fill_with(T::any) } #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlim"] #[inline(always)] -pub fn write_any_slim(pointer: *mut T) { - unsafe { ptr::write(pointer, T::any()) } +pub unsafe fn write_any_slim(pointer: *mut T) { + ptr::write(pointer, T::any()) } #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnyStr"] #[inline(always)] -pub fn write_any_str(s: *mut str) { - unsafe { (*s).as_bytes_mut() }.fill_with(u8::any) +pub unsafe fn write_any_str(s: *mut str) { + (*s).as_bytes_mut().fill_with(u8::any) //TODO: String validation } diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 2172f20fca66..852193bce9bb 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -99,7 +99,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); quote!( #(#before)* - #(kani::internal::write_any(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)* + #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)* #(#after)* #result ) From 0bd765ef68dae7c265751db74246d122003a8962 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 10 Jul 2024 17:37:09 -0400 Subject: [PATCH 15/23] change any_modifies back --- library/kani/src/internal.rs | 16 ---------------- library/kani/src/lib.rs | 15 +++++++++++++++ .../kani_macros/src/sysroot/contracts/replace.rs | 10 ++-------- 3 files changed, 17 insertions(+), 24 deletions(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 7565520fb820..35550f2895e6 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -97,22 +97,6 @@ pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } -/// This function is only used for function contract instrumentation. -/// It behaves exaclty like `kani::any()`, except it will check for the trait bounds -/// at compilation time. It allows us to avoid type checking errors while using function -/// contracts only for verification. -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniAnyModifies"] -#[inline(never)] -#[doc(hidden)] -pub fn any_modifies() -> T { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. /// Only for use within function contracts and will not be replaced if the recursive or function stub /// replace contracts are not used. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index dedb32846b2d..6eab2a331811 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -168,6 +168,21 @@ pub fn any() -> T { T::any() } +/// This function is only used for function contract instrumentation. +/// It behaves exaclty like `kani::any()`, except it will check for the trait bounds +/// at compilation time. It allows us to avoid type checking errors while using function +/// contracts only for verification. +#[rustc_diagnostic_item = "KaniAnyModifies"] +#[inline(never)] +#[doc(hidden)] +pub fn any_modifies() -> T { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() +} + /// This creates a symbolic *valid* value of type `T`. /// The value is constrained to be a value accepted by the predicate passed to the filter. /// You can assign the return value of this function to a variable that you want to make symbolic. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 852193bce9bb..354d7a01f0b6 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -40,12 +40,7 @@ impl<'a> ContractConditionsHandler<'a> { if self.is_first_emit() { let return_type = return_type_to_type(&self.annotated_fn.sig.output); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - ( - vec![ - syn::parse_quote!(let #result : #return_type = kani::internal::any_modifies();), - ], - vec![], - ) + (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![]) } else { let stmts = &self.annotated_fn.block.stmts; let idx = stmts @@ -157,9 +152,8 @@ fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool { path, attrs, }) - if path.segments.len() == 3 + if path.segments.len() == 2 && path.segments[0].ident == "kani" - && path.segments[1].ident == "internal" && path.segments[2].ident == "any_modifies" && attrs.is_empty() ) From e038b0f7643301a7bc330ade954b54bd4bcd9547 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Wed, 10 Jul 2024 18:05:52 -0400 Subject: [PATCH 16/23] Update replace.rs --- library/kani_macros/src/sysroot/contracts/replace.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 354d7a01f0b6..280839dcafca 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -154,7 +154,7 @@ fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool { }) if path.segments.len() == 2 && path.segments[0].ident == "kani" - && path.segments[2].ident == "any_modifies" + && path.segments[1].ident == "any_modifies" && attrs.is_empty() ) ) From 9c2b7e854773e4c52f5c3f0d53d52a9c6e418517 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Thu, 11 Jul 2024 16:23:44 -0400 Subject: [PATCH 17/23] strings todo --- library/kani/src/internal.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 35550f2895e6..7141aa915682 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -130,6 +130,8 @@ pub unsafe fn write_any_slim(pointer: *mut T) { #[rustc_diagnostic_item = "KaniWriteAnyStr"] #[inline(always)] pub unsafe fn write_any_str(s: *mut str) { - (*s).as_bytes_mut().fill_with(u8::any) + //TODO: strings introduce new UB + //(*s).as_bytes_mut().fill_with(u8::any) //TODO: String validation + unreachable!("strings are not yet implemented") } From 55ca498d37e061e4be537f2e76e0259aa2a1e686 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Thu, 11 Jul 2024 16:39:58 -0400 Subject: [PATCH 18/23] strings todo --- library/kani/src/internal.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 7141aa915682..ff741992fab5 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -129,7 +129,7 @@ pub unsafe fn write_any_slim(pointer: *mut T) { #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnyStr"] #[inline(always)] -pub unsafe fn write_any_str(s: *mut str) { +pub unsafe fn write_any_str(_s: *mut str) { //TODO: strings introduce new UB //(*s).as_bytes_mut().fill_with(u8::any) //TODO: String validation From 310c6b4b107a498b1b7a9e36c9e02826ed1cdb1f Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Thu, 11 Jul 2024 21:05:00 -0400 Subject: [PATCH 19/23] Update library/kani/src/internal.rs Co-authored-by: Celina G. Val --- library/kani/src/internal.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index ff741992fab5..38cb2a2558a7 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -133,5 +133,5 @@ pub unsafe fn write_any_str(_s: *mut str) { //TODO: strings introduce new UB //(*s).as_bytes_mut().fill_with(u8::any) //TODO: String validation - unreachable!("strings are not yet implemented") + unimplemented!("Kani does not support creating arbitrary `str`") } From dff4d7cd97dddb54abf68b54711241c3d9dc9758 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 16 Jul 2024 15:03:16 -0400 Subject: [PATCH 20/23] string test fails --- .../codegen_cprover_gotoc/codegen/contract.rs | 2 +- .../string_rewrite_ignore.rs | 19 +++++++++++++++++++ .../modifies_fat_pointer/u32slice.rs | 2 +- 3 files changed, 21 insertions(+), 2 deletions(-) create mode 100644 tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index d8ed4678b728..7f19e5814ce0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -153,7 +153,7 @@ impl<'tcx> GotocCtx<'tcx> { TyKind::RigidTy(RigidTy::Slice(elt_type)) => { elt_type.layout().unwrap().shape().size.bytes() } - TyKind::RigidTy(RigidTy::Str) => 8, + TyKind::RigidTy(RigidTy::Str) => 1, // For adt, see https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp TyKind::RigidTy(RigidTy::Adt(..)) => { todo!("Adt fat pointers not implemented") diff --git a/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs b/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs new file mode 100644 index 000000000000..6b304f9e53fe --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test that modifies a string + +#[kani::requires(x == "aaa")] +#[kani::modifies(x)] +#[kani::ensures(|_| x == "AAA")] +fn to_upper(x: &mut str) { + x.make_ascii_uppercase(); +} + +#[kani::proof_for_contract(to_upper)] +fn harness() { + let mut s = String::from("aaa"); + let x : &mut str = s.as_mut_str(); + to_upper(x); +} diff --git a/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs b/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs index 4f6177ebec75..ea61de83e969 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs +++ b/tests/expected/function-contract/modifies_fat_pointer/u32slice.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -// Test that modifies a slice containing bytesize data +// Test that modifies a slice containing u32 size data #[kani::modifies(x)] #[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))] From ff56fc17712ca6c89c5ab63ae6df801cad0cc2f8 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 16 Jul 2024 15:31:58 -0400 Subject: [PATCH 21/23] new test --- .../slice_of_array.expected | 5 +++++ .../modifies_fat_pointer/slice_of_array.rs | 17 +++++++++++++++++ .../string_rewrite_ignore.rs | 2 +- 3 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected create mode 100644 tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs diff --git a/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected new file mode 100644 index 000000000000..d0fc296ef4d7 --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| x[0..3].iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs new file mode 100644 index 000000000000..e38807228155 --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test that modifies a slice containing u32 size data + +#[kani::modifies(x[0..3])] +#[kani::ensures(|_| x[0..3].iter().map(|v| *v == 0).fold(true,|a,b|a&b))] +fn zero(x: &mut [u32; 6]) { + x[0..3].fill(0) +} + +#[kani::proof_for_contract(zero)] +fn harness() { + let mut x = [kani::any(), kani::any(), kani::any()]; + zero(&mut x); +} diff --git a/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs b/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs index 6b304f9e53fe..d8780068a0da 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs +++ b/tests/expected/function-contract/modifies_fat_pointer/string_rewrite_ignore.rs @@ -14,6 +14,6 @@ fn to_upper(x: &mut str) { #[kani::proof_for_contract(to_upper)] fn harness() { let mut s = String::from("aaa"); - let x : &mut str = s.as_mut_str(); + let x: &mut str = s.as_mut_str(); to_upper(x); } From 9478594971c25acd178e43c3ed1f439d38d22ecd Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 16 Jul 2024 15:42:46 -0400 Subject: [PATCH 22/23] comments --- kani-compiler/src/kani_middle/transform/contracts.rs | 12 +++++++++++- library/kani/src/internal.rs | 7 +++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index e45b5436204b..3a835c7f3cb6 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -17,10 +17,15 @@ use std::collections::HashSet; use std::fmt::Debug; use tracing::{debug, trace}; -/// Check if we can replace calls to any_modifies. +/// Check if we can replace calls to any_modifies or write_any. /// /// This pass will replace the entire body, and it should only be applied to stubs /// that have a body. +/// +/// write_any is replaced with one of write_any_slim, write_any_slice, or write_any_str +/// depending on what the type of the input it +/// +/// any_modifies is replaced with any #[derive(Debug)] pub struct AnyModifiesPass { kani_any: Option, @@ -143,6 +148,7 @@ impl AnyModifiesPass { changed = true; } + // if this is a valid kani::write_any function if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = func.ty(&locals).unwrap().kind() && Some(def) == self.kani_write_any @@ -151,7 +157,9 @@ impl AnyModifiesPass { && let Some(TypeAndMut { ty: internal_type, mutability: _ }) = fn_sig.skip_binder().inputs()[0].kind().builtin_deref(true) { + // case on the type of the input if let TyKind::RigidTy(RigidTy::Slice(_)) = internal_type.kind() { + //if the input is a slice, use write_any_slice let instance = Instance::resolve(self.kani_write_any_slice.unwrap(), &instance_args) .unwrap(); @@ -160,6 +168,7 @@ impl AnyModifiesPass { let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } else if let TyKind::RigidTy(RigidTy::Str) = internal_type.kind() { + //if the input is a str, use write_any_str let instance = Instance::resolve(self.kani_write_any_str.unwrap(), &instance_args) .unwrap(); @@ -168,6 +177,7 @@ impl AnyModifiesPass { let new_func = ConstOperand { span, user_ty: None, const_: literal }; *func = Operand::Constant(new_func); } else { + //otherwise, use write_any_slim let instance = Instance::resolve(self.kani_write_any_slim.unwrap(), &instance_args) .unwrap(); diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 38cb2a2558a7..22026065106a 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -112,6 +112,8 @@ pub unsafe fn write_any(_pointer: *mut T) { unreachable!() } +/// Fill in a slice with kani::any. +/// Intended as a post compilation replacement for write_any #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlice"] #[inline(always)] @@ -119,6 +121,8 @@ pub unsafe fn write_any_slice(slice: *mut [T]) { (*slice).fill_with(T::any) } +/// Fill in a pointer with kani::any. +/// Intended as a post compilation replacement for write_any #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnySlim"] #[inline(always)] @@ -126,6 +130,9 @@ pub unsafe fn write_any_slim(pointer: *mut T) { ptr::write(pointer, T::any()) } +/// Fill in a str with kani::any. +/// Intended as a post compilation replacement for write_any. +/// Not yet implemented #[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] #[rustc_diagnostic_item = "KaniWriteAnyStr"] #[inline(always)] From 7bd56347a4c9b3535b3debd6cc4a7e46c677089c Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 16 Jul 2024 15:45:13 -0400 Subject: [PATCH 23/23] new test --- .../function-contract/modifies_fat_pointer/slice_of_array.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs index e38807228155..a0f6c10ad694 100644 --- a/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs +++ b/tests/expected/function-contract/modifies_fat_pointer/slice_of_array.rs @@ -4,7 +4,7 @@ // Test that modifies a slice containing u32 size data -#[kani::modifies(x[0..3])] +#[kani::modifies(&x[0..3])] #[kani::ensures(|_| x[0..3].iter().map(|v| *v == 0).fold(true,|a,b|a&b))] fn zero(x: &mut [u32; 6]) { x[0..3].fill(0) @@ -12,6 +12,6 @@ fn zero(x: &mut [u32; 6]) { #[kani::proof_for_contract(zero)] fn harness() { - let mut x = [kani::any(), kani::any(), kani::any()]; + let mut x = [kani::any(), kani::any(), kani::any(), kani::any(), kani::any(), kani::any()]; zero(&mut x); }