Skip to content

Commit

Permalink
Function Contracts: Modify Slices (model-checking#3295)
Browse files Browse the repository at this point in the history 
Using the `__CPROVER_object_upto` function to pass modifies clauses to
asserts clauses in goto for rust slices.

Resolves model-checking#2908

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Matias Scharager <[email protected]>
Co-authored-by: Celina G. Val <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>
  • Loading branch information
@pi314mm @celinval @feliperodri
4 people authored Jul 17, 2024
1 parent b1681e7 commit 852fd8f
Show file tree
Hide file tree
Showing 14 changed files with 314 additions and 29 deletions.
66 changes: 60 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand Down Expand Up @@ -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();
Expand Down
79 changes: 75 additions & 4 deletions kani-compiler/src/kani_middle/transform/contracts.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<FnDef>,
kani_any_modifies: Option<FnDef>,
kani_write_any: Option<FnDef>,
kani_write_any_slim: Option<FnDef>,
kani_write_any_slice: Option<FnDef>,
kani_write_any_str: Option<FnDef>,
stubbed: HashSet<DefId>,
target_fn: Option<InternedString>,
}
Expand Down Expand Up @@ -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 =
Expand All @@ -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,
Expand All @@ -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
Expand All @@ -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)
}
Expand Down
77 changes: 61 additions & 16 deletions library/kani/src/internal.rs
View file
Original file line number Diff line number Diff line change
@@ -1,70 1,69 @@
// 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.
///
/// 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 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)]
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)
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
}
}

Expand Down Expand Up @@ -97,3 96,49 @@ pub fn init_contracts() {}
pub fn apply_closure<T, U: Fn(&T) -> 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<T: ?Sized>(_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<T: Arbitrary>(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<T: Arbitrary>(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`")
}
12 changes: 10 additions & 2 deletions library/kani_macros/src/sysroot/contracts/check.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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::TypeParamBound, syn::token::Plus> =
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,
}));
Expand Down
2 changes: 1 addition & 1 deletion library/kani_macros/src/sysroot/contracts/replace.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
)
Expand Down
5 changes: 5 additions & 0 deletions tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 1,5 @@
assertion\
- Status: SUCCESS\
- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\

VERIFICATION:- SUCCESSFUL
Loading

0 comments on commit 852fd8f

Please sign in to comment.