diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index c7e7d5b817bd..7f19e5814ce0 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; @@ -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 @@ -142,11 +144,63 @@ 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)) { + 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) => 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") + } + kind => unreachable!("Generating a slice fat pointer to {:?}", kind), + }; + 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) + .mul(Expr::size_constant( + size.try_into().unwrap(), + &self.symbol_table, + )), + ]), + ) + } else { + Lambda::as_contract_for( + &goto_annotated_fn_typ, + None, + self.codegen_place_stable(&local.into(), loc) + .unwrap() + .goto_expr + .dereference(), + ) + } }) .chain(shadow_memory_assign) .collect(); diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index eb5266e0a0eb..3a835c7f3cb6 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -11,20 +11,29 @@ 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; 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, kani_any_modifies: 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, } @@ -78,6 +87,18 @@ impl AnyModifiesPass { let kani_any_modifies = tcx .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) .map(item_fn_def); + let kani_write_any = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAny")) + .map(item_fn_def); + let kani_write_any_slim = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlim")) + .map(item_fn_def); + let kani_write_any_slice = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlice")) + .map(item_fn_def); + 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); let target_fn = @@ -86,7 +107,16 @@ impl AnyModifiesPass { } else { (None, HashSet::new()) }; - AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed } + AnyModifiesPass { + kani_any, + kani_any_modifies, + kani_write_any, + kani_write_any_slim, + kani_write_any_slice, + kani_write_any_str, + target_fn, + stubbed, + } } /// If we apply `transform_any_modifies` in all contract-generated items, @@ -105,7 +135,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 +147,47 @@ impl AnyModifiesPass { *func = Operand::Constant(new_func); 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 + && 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) + { + // 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(); + 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() { + //if the input is a str, use write_any_str + let instance = + 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 { + //otherwise, use write_any_slim + let instance = + 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 }; + *func = Operand::Constant(new_func); + } + changed = true; + } } (changed, body) } diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 509f2cf51962..22026065106a 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -1,13 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::arbitrary::Arbitrary; +use std::ptr; + /// 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. #[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. /// @@ -15,23 +18,21 @@ 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; - /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> &'a mut Self::Inner; + unsafe fn assignable(self) -> *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 { + unsafe fn assignable(self) -> *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)] @@ -39,32 +40,30 @@ 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 assignable(self) -> *mut Self::Inner { + self as *mut T } } -impl<'a, T> Pointer<'a> for *const 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 } - #[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) } } -impl<'a, T> Pointer<'a> for *mut 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 } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - std::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self } } @@ -97,3 +96,49 @@ pub fn init_contracts() {} pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) } + +/// 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 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 + // sure Kani doesn't report any false positives. + 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)] +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)] +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)] +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 + unimplemented!("Kani does not support creating arbitrary `str`") +} 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..280839dcafca 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::write_any(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 new file mode 100644 index 000000000000..2fab679b5cba --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- 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 new file mode 100644 index 000000000000..faf1d9d44581 --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/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.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_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..a0f6c10ad694 --- /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(), 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 new file mode 100644 index 000000000000..d8780068a0da --- /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.expected b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected new file mode 100644 index 000000000000..2fab679b5cba --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/u32slice.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- 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 new file mode 100644 index 000000000000..ea61de83e969 --- /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 u32 size data + +#[kani::modifies(x)] +#[kani::ensures(|_| x.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..2fab679b5cba --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/u8slice.expected @@ -0,0 +1,5 @@ +assertion\ +- Status: SUCCESS\ +- 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 new file mode 100644 index 000000000000..07e213db0adc --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/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.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); +}