diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 5254394ccbc8..0287e4b9b01f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -325,6 +325,49 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { } } +/// A builtin that is essentially a C-style dereference operation, creating an +/// unsafe shallow copy. Importantly either this copy or the original needs to +/// be `mem::forget`en or a double-free will occur. +/// +/// Takes in a `&T` reference and returns a `T` (like clone would but without +/// cloning). Breaks ownership rules and is only used in the context of function +/// contracts where we can structurally guarantee the use is safe. +struct UntrackedDeref; + +impl<'tcx> GotocHook<'tcx> for UntrackedDeref { + fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { + matches_function(tcx, instance, "KaniUntrackedDeref") + } + + fn handle( + &self, + tcx: &mut GotocCtx<'tcx>, + _instance: Instance<'tcx>, + mut fargs: Vec, + assign_to: Place<'tcx>, + _target: Option, + span: Option, + ) -> Stmt { + assert_eq!( + fargs.len(), + 1, + "Invariant broken. `untracked_deref` should only be given one argument. \ + This function should only be called from code generated by kani macros, \ + as such this is likely a code-generation error." + ); + let loc = tcx.codegen_span_option(span); + Stmt::block( + vec![Stmt::assign( + unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) + .goto_expr, + fargs.pop().unwrap().dereference(), + loc, + )], + loc, + ) + } +} + pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { GotocHooks { hooks: vec![ @@ -335,6 +378,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { Rc::new(Nondet), Rc::new(RustAlloc), Rc::new(MemCmp), + Rc::new(UntrackedDeref), ], } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 86fd79135af9..d1ef8fdf33e3 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -5,17 +5,21 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; -use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem}; +use rustc_ast::{ + attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, + NestedMetaItem, +}; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; -use rustc_span::Span; +use rustc_session::Session; +use rustc_span::{Span, Symbol}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; use tracing::{debug, trace}; -use super::resolve; +use super::resolve::{self, resolve_fn}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] @@ -27,6 +31,16 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + /// A harness, similar to [`Self::Proof`], but for checking a function + /// contract, e.g. the contract check is substituted for the target function + /// before the the verification runs. + ProofForContract, + /// Attribute on a function with a contract that identifies the code + /// implementing the check for this contract. + CheckedWith, + /// Attribute on a function that was auto-generated from expanding a + /// function contract. + IsContractGenerated, } impl KaniAttributeKind { @@ -37,10 +51,31 @@ impl KaniAttributeKind { | KaniAttributeKind::ShouldPanic | KaniAttributeKind::Solver | KaniAttributeKind::Stub + | KaniAttributeKind::ProofForContract | KaniAttributeKind::Unwind => true, - KaniAttributeKind::Unstable => false, + KaniAttributeKind::Unstable + | KaniAttributeKind::CheckedWith + | KaniAttributeKind::IsContractGenerated => false, } } + + /// Is this an "active" function contract attribute? This means it is + /// part of the function contract interface *and* it implies that a contract + /// will be used (stubbed or checked) in some way, thus requiring that the + /// user activate the unstable feature. + /// + /// If we find an "inactive" contract attribute we chose not to error, + /// because it wouldn't have any effect anyway. + pub fn demands_function_contract_use(self) -> bool { + matches!(self, KaniAttributeKind::ProofForContract) + } + + /// Would this attribute be placed on a function as part of a function + /// contract. E.g. created by `requires`, `ensures`. + pub fn is_function_contract(self) -> bool { + use KaniAttributeKind::*; + matches!(self, CheckedWith | IsContractGenerated) + } } /// Bundles together common data used when evaluating the attributes of a given @@ -83,6 +118,54 @@ impl<'tcx> KaniAttributes<'tcx> { Self { map, tcx, item: def_id } } + /// Expect that at most one attribute of this kind exists on the function + /// and return it. + fn expect_maybe_one(&self, kind: KaniAttributeKind) -> Option<&'tcx Attribute> { + match self.map.get(&kind)?.as_slice() { + [one] => Some(one), + _ => { + self.tcx.sess.err(format!( + "Too many {} attributes on {}, expected 0 or 1", + kind.as_ref(), + self.tcx.def_path_debug_str(self.item) + )); + None + } + } + } + + /// Parse and extract the `proof_for_contract(TARGET)` attribute. The + /// returned symbol and DefId are respectively the name and id of `TARGET`, + /// the span in the span for the attribute (contents). + fn interpret_the_for_contract_attribute( + &self, + ) -> Option> { + self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { + let name = expect_key_string_value(self.tcx.sess, target)?; + let resolved = resolve_fn( + self.tcx, + self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), + name.as_str(), + ); + resolved.map(|ok| (name, ok, target.span)).map_err(|resolve_err| { + self.tcx.sess.span_err( + target.span, + format!( + "Failed to resolve replacement function {} because {resolve_err}", + name.as_str() + ), + ) + }) + }) + } + + /// Extract the name of the sibling function this contract is checked with + /// (if any). + pub fn checked_with(&self) -> Option> { + self.expect_maybe_one(KaniAttributeKind::CheckedWith) + .map(|target| expect_key_string_value(self.tcx.sess, target)) + } + /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. @@ -90,14 +173,13 @@ impl<'tcx> KaniAttributes<'tcx> { // Check that all attributes are correctly used and well formed. let is_harness = self.is_harness(); for (&kind, attrs) in self.map.iter() { + let local_error = |msg| self.tcx.sess.span_err(attrs[0].span, msg); + if !is_harness && kind.is_harness_only() { - self.tcx.sess.span_err( - attrs[0].span, - format!( - "the `{}` attribute also requires the `#[kani::proof]` attribute", - kind.as_ref() - ), - ); + local_error(format!( + "the `{}` attribute also requires the `#[kani::proof]` attribute", + kind.as_ref() + )); } match kind { KaniAttributeKind::ShouldPanic => { @@ -122,12 +204,34 @@ impl<'tcx> KaniAttributes<'tcx> { }) } KaniAttributeKind::Proof => { + if self.map.contains_key(&KaniAttributeKind::ProofForContract) { + local_error( + "`proof` and `proof_for_contract` may not be used on the same function.".to_string(), + ); + } expect_single(self.tcx, kind, &attrs); attrs.iter().for_each(|attr| self.check_proof_attribute(attr)) } KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx)); }), + KaniAttributeKind::ProofForContract => { + if self.map.contains_key(&KaniAttributeKind::Proof) { + local_error( + "`proof` and `proof_for_contract` may not be used on the same function.".to_string(), + ); + } + expect_single(self.tcx, kind, &attrs); + } + KaniAttributeKind::CheckedWith => { + self.expect_maybe_one(kind) + .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); + } + KaniAttributeKind::IsContractGenerated => { + // Ignored here because this is only used by the proc macros + // to communicate with one another. So by the time it gets + // here we don't care if it's valid or not. + } } } } @@ -142,6 +246,23 @@ impl<'tcx> KaniAttributes<'tcx> { // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 return; } + + // If the `function-contracts` unstable feature is not enabled then no + // function should use any of those APIs. + if !enabled_features.iter().any(|feature| feature == "function-contracts") { + for kind in self.map.keys().copied().filter(|a| a.demands_function_contract_use()) { + let msg = format!( + "Using the {} attribute requires activating the unstable `function-contracts` feature", + kind.as_ref() + ); + if let Some(attr) = self.map.get(&kind).unwrap().first() { + self.tcx.sess.span_err(attr.span, msg); + } else { + self.tcx.sess.err(msg); + } + } + } + if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) { for attr in unstable_attrs { let unstable_attr = UnstableAttribute::try_from(*attr).unwrap(); @@ -176,7 +297,8 @@ impl<'tcx> KaniAttributes<'tcx> { /// Is this item a harness? (either `proof` or `proof_for_contract` /// attribute are present) fn is_harness(&self) -> bool { - self.map.get(&KaniAttributeKind::Proof).is_some() + self.map.contains_key(&KaniAttributeKind::Proof) + || self.map.contains_key(&KaniAttributeKind::ProofForContract) } /// Extract harness attributes for a given `def_id`. @@ -185,7 +307,9 @@ impl<'tcx> KaniAttributes<'tcx> { /// Note that all attributes should be valid by now. pub fn harness_attributes(&self) -> HarnessAttributes { // Abort if not local. - assert!(self.item.is_local(), "Expected a local item, but got: {:?}", self.item); + if !self.item.is_local() { + panic!("Expected a local item, but got: {:?}", self.item); + }; trace!(?self, "extract_harness_attributes"); assert!(self.is_harness()); self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { @@ -195,16 +319,39 @@ impl<'tcx> KaniAttributes<'tcx> { harness.solver = parse_solver(self.tcx, attributes[0]); } KaniAttributeKind::Stub => { - harness.stubs = parse_stubs(self.tcx, self.item, attributes); + harness.stubs.extend_from_slice(&parse_stubs(self.tcx, self.item, attributes)); } KaniAttributeKind::Unwind => { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } KaniAttributeKind::Proof => harness.proof = true, + KaniAttributeKind::ProofForContract => { + harness.proof = true; + let Some(Ok((name, id, span))) = self.interpret_the_for_contract_attribute() + else { + self.tcx.sess.span_err( + self.tcx.def_span(self.item), + format!("Invalid `{}` attribute format", kind.as_ref()), + ); + return harness; + }; + let Some(Ok(replacement_name)) = + KaniAttributes::for_item(self.tcx, id).checked_with() + else { + self.tcx + .sess + .span_err(span, "Target function for this check has no contract"); + return harness; + }; + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); + } KaniAttributeKind::Unstable => { // Internal attribute which shouldn't exist here. unreachable!() } + KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { + todo!("Contract attributes are not supported on proofs") + } }; harness }) @@ -226,6 +373,18 @@ impl<'tcx> KaniAttributes<'tcx> { } } } + + fn stub_for_relative_item(&self, anchor: Symbol, replacement: Symbol) -> Stub { + let local_id = self.item.expect_local(); + let current_module = self.tcx.parent_module_from_def_id(local_id); + let replace_str = replacement.as_str(); + let original_str = anchor.as_str(); + let replacement = original_str + .rsplit_once("::") + .map_or_else(|| replace_str.to_string(), |t| t.0.to_string() + "::" + replace_str); + resolve::resolve_fn(self.tcx, current_module.to_local_def_id(), &replacement).unwrap(); + Stub { original: original_str.to_string(), replacement } + } } /// An efficient check for the existence for a particular [`KaniAttributeKind`]. @@ -239,10 +398,18 @@ fn has_kani_attribute bool>( tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) } +/// Test if this function was generated by expanding a contract attribute like +/// `requires` and `ensures`. +pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool { + has_kani_attribute(tcx, def_id, KaniAttributeKind::is_function_contract) +} + /// Same as [`KaniAttributes::is_harness`] but more efficient because less /// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool { - has_kani_attribute(tcx, def_id, |a| matches!(a, KaniAttributeKind::Proof)) + has_kani_attribute(tcx, def_id, |a| { + matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract) + }) } /// Does this `def_id` have `#[rustc_test_marker]`? @@ -258,6 +425,43 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { parse_str_value(&marker).unwrap() } +/// Expect the contents of this attribute to be of the format #[attribute = +/// "value"] and return the `"value"`. +fn expect_key_string_value( + sess: &Session, + attr: &Attribute, +) -> Result { + let span = attr.span; + let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else { + return Err(sess.span_err(span, "Expected attribute of the form #[attr = \"value\"]")); + }; + let maybe_str = match it { + AttrArgsEq::Ast(expr) => { + if let ExprKind::Lit(tok) = expr.kind { + match LitKind::from_token_lit(tok) { + Ok(l) => l.str(), + Err(err) => { + return Err(sess.span_err( + span, + format!("Invalid string literal on right hand side of `=` {err:?}"), + )); + } + } + } else { + return Err( + sess.span_err(span, "Expected literal string as right hand side of `=`") + ); + } + } + AttrArgsEq::Hir(lit) => lit.kind.str(), + }; + if let Some(str) = maybe_str { + Ok(str) + } else { + Err(sess.span_err(span, "Expected literal string as right hand side of `=`")) + } +} + fn expect_single<'a>( tcx: TyCtxt, kind: KaniAttributeKind, diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index d087aa76c7c4..0aec0c448219 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -15,7 +15,7 @@ use rustc_middle::ty::layout::{ FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, TyAndLayout, }; -use rustc_middle::ty::{self, Instance, InstanceDef, Ty, TyCtxt}; +use rustc_middle::ty::{self, Instance, InstanceDef, ParamEnv, Ty, TyCtxt}; use rustc_session::config::OutputType; use rustc_span::source_map::respan; use rustc_span::Span; @@ -66,7 +66,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { /// Check that all given items are supported and there's no misconfiguration. /// This method will exhaustively print any error / warning and it will abort at the end if any /// error was found. -pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { +pub fn check_reachable_items<'tcx>(tcx: TyCtxt<'tcx>, queries: &QueryDb, items: &[MonoItem<'tcx>]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) { @@ -77,10 +77,101 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) .check_unstable_features(&queries.args().unstable_features); def_ids.insert(def_id); } + + // We don't short circuit here since this is a type check and can shake + // out differently depending on generic parameters. + if let MonoItem::Fn(instance) = item { + if attributes::is_function_contract_generated(tcx, instance.def_id()) { + check_is_contract_safe(tcx, *instance); + } + } } tcx.sess.abort_if_errors(); } +/// A basic check that ensures a function with a contract does not receive +/// mutable pointers in its input and does not return raw pointers of any kind. +/// +/// This is a temporary safety measure because contracts cannot yet reason +/// about the heap. +fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { + use ty::TypeVisitor; + struct NoMutPtr<'tcx> { + tcx: TyCtxt<'tcx>, + is_prohibited: fn(ty::Ty<'tcx>) -> bool, + /// Where (top level) did the type we're analyzing come from. Used for + /// composing error messages. + r#where: &'static str, + /// Adjective to describe the kind of pointer we're prohibiting. + /// Essentially `is_prohibited` but in English. + what: &'static str, + } + + impl<'tcx> TypeVisitor> for NoMutPtr<'tcx> { + fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> std::ops::ControlFlow { + use ty::TypeSuperVisitable; + if (self.is_prohibited)(t) { + // TODO make this more user friendly + self.tcx.sess.err(format!("{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); + } + + // Rust's type visitor only recurses into type arguments, (e.g. + // `generics` in this match). This is enough for many types, but it + // won't look at the field types of structs or enums. So we override + // it here and do that ourselves. + // + // Since the field types also must contain in some form all the type + // arguments the visitor will see them as it inspects the fields and + // we don't need to call back to `super`. + if let ty::TyKind::Adt(adt_def, generics) = t.kind() { + for variant in adt_def.variants() { + for field in &variant.fields { + let ctrl = self.visit_ty(field.ty(self.tcx, generics)); + if ctrl.is_break() { + // Technically we can just ignore this because we + // know this case will never happen, but just to be + // safe. + return ctrl; + } + } + } + std::ops::ControlFlow::Continue(()) + } else { + // For every other type. + t.super_visit_with(self) + } + } + } + + fn is_raw_mutable_ptr(t: ty::Ty) -> bool { + matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) + } + + let bound_fn_sig = instance.ty(tcx, ParamEnv::reveal_all()).fn_sig(tcx); + + for v in bound_fn_sig.bound_vars() { + if let ty::BoundVariableKind::Ty(t) = v { + tcx.sess.span_err( + tcx.def_span(instance.def_id()), + format!("Found a bound type variable {t:?} after monomorphization"), + ); + } + } + + let fn_typ = bound_fn_sig.skip_binder(); + + for (typ, (is_prohibited, r#where, what)) in fn_typ + .inputs() + .iter() + .copied() + .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable "))) + .chain([(fn_typ.output(), (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))]) + { + let mut v = NoMutPtr { tcx, is_prohibited, r#where, what }; + v.visit_ty(typ); + } +} + /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc. pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { /// Convert MonoItem into a DefId. diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 6d956b53f5ed..0cc3ee0b7f3a 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -90,6 +90,12 @@ pub enum ResolveError<'tcx> { UnexpectedType { tcx: TyCtxt<'tcx>, item: DefId, expected: &'static str }, } +impl<'tcx> fmt::Debug for ResolveError<'tcx> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + std::fmt::Display::fmt(self, f) + } +} + impl<'tcx> fmt::Display for ResolveError<'tcx> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { @@ -153,8 +159,10 @@ fn resolve_prefix<'tcx>( ) -> Result> { debug!(?name, ?current_module, "resolve_prefix"); - // Split the string into segments separated by `::`. - let mut segments = name.split("::").map(str::to_string).peekable(); + // Split the string into segments separated by `::`. Trim the whitespace + // since path strings generated from macros sometimes add spaces around + // `::`. + let mut segments = name.split("::").map(|s| s.trim().to_string()).peekable(); assert!(segments.peek().is_some(), "expected identifier, found `{name}`"); // Resolve qualifiers `crate`, initial `::`, and `self`. The qualifier diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs index c8c508ad94ac..3774d0afc148 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -19,6 +19,8 @@ use rustc_middle::mir::{ }; use rustc_middle::ty::{self, TyCtxt}; +use tracing::debug; + /// Returns the `DefId` of the stub for the function/method identified by the /// parameter `def_id`, and `None` if the function/method is not stubbed. pub fn get_stub(tcx: TyCtxt, def_id: DefId) -> Option { @@ -30,6 +32,11 @@ pub fn get_stub(tcx: TyCtxt, def_id: DefId) -> Option { /// otherwise, returns the old body. pub fn transform<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, old_body: &'tcx Body<'tcx>) -> Body<'tcx> { if let Some(replacement) = get_stub(tcx, def_id) { + debug!( + original = tcx.def_path_debug_str(def_id), + replaced = tcx.def_path_debug_str(replacement), + "transform" + ); let new_body = tcx.optimized_mir(replacement).clone(); if check_compatibility(tcx, def_id, old_body, replacement, &new_body) { return new_body; diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 04c64dd574da..eeb72c0be598 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -346,10 +346,16 @@ impl VerificationArgs { } } + /// Are experimental function contracts enabled? + pub fn is_function_contracts_enabled(&self) -> bool { + self.common_args.unstable_features.contains(UnstableFeature::FunctionContracts) + } + /// Is experimental stubbing enabled? pub fn is_stubbing_enabled(&self) -> bool { self.enable_stubbing || self.common_args.unstable_features.contains(UnstableFeature::Stubbing) + || self.is_function_contracts_enabled() } } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 6cd3816103ef..060508666735 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -80,6 +80,8 @@ pub enum UnstableFeature { AsyncLib, /// Enable line coverage instrumentation/reports. LineCoverage, + /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) + FunctionContracts, } impl UnstableFeature { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index d955e204a833..6125c589a957 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -74,6 +74,33 @@ pub fn assume(cond: bool) { assert!(cond, "`kani::assume` should always hold"); } +/// `implies!(premise => conclusion)` means that if the `premise` is true, so +/// must be the `conclusion`. +/// +/// This simply expands to `!premise || conclusion` and is intended to be used +/// in function contracts to make them more readable, as the concept of an +/// implication is more natural to think about than its expansion. +/// +/// For further convenience multiple comma separated premises are allowed, and +/// are joined with `||` in the expansion. E.g. `implies!(a, b => c)` expands to +/// `!a || !b || c` and says that `c` is true if both `a` and `b` are true (see +/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)). +#[macro_export] +macro_rules! implies { + ($($premise:expr),+ => $conclusion:expr) => { + $(!$premise)||+ || ($conclusion) + }; +} + +/// A way to break the ownerhip rules. Only used by contracts where we can +/// guarantee it is done safely. +#[inline(never)] +#[doc(hidden)] +#[rustc_diagnostic_item = "KaniUntrackedDeref"] +pub fn untracked_deref(_: &T) -> T { + todo!() +} + /// Creates an assertion of the specified condition and message. /// /// # Example: diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index a97b67b352b4..dfa776f9ce7c 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -15,4 +15,4 @@ proc-macro = true proc-macro2 = "1.0" proc-macro-error = "1.0.4" quote = "1.0.20" -syn = { version = "2.0.18", features = ["full"] } +syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 509fd78c03ee..3b4ea87636f3 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -7,6 +7,7 @@ // downstream crates to enable these features as well. // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" +#![feature(proc_macro_diagnostic)] mod derive; @@ -96,12 +97,81 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } +/// Add a precondition to this function. +/// +/// This is part of the function contract API, together with [`ensures`]. +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function. All Rust syntax is supported, even calling other +/// functions, but the computations must be side effect free, e.g. it cannot +/// perform I/O or use mutable memory. +/// +/// Kani requires each function that uses a contract (this attribute or +/// [`ensures`]) to have at least one designated [`proof_for_contract`] harness +/// for checking the contract. +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. +#[proc_macro_attribute] +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::requires(attr, item) +} + +/// Add a postcondition to this function. +/// +/// This is part of the function contract API, together with [`requires`]. +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function *and* its return value, accessible as a variable called +/// `result`. All Rust syntax is supported, even calling other functions, but +/// the computations must be side effect free, e.g. it cannot perform I/O or use +/// mutable memory. +/// +/// Kani requires each function that uses a contract (this attribute or +/// [`requires`]) to have at least one designated [`proof_for_contract`] harness +/// for checking the contract. +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. +#[proc_macro_attribute] +pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::ensures(attr, item) +} + +/// Designates this function as a harness to check a function contract. +/// +/// The argument to this macro is the relative path (e.g. `foo` or +/// `super::some_mod::foo` or `crate::SomeStruct::foo`) to the function, the +/// contract of which should be checked. +/// +/// The harness is expected to set up the arguments that `foo` should be called +/// with and initialzied any `static mut` globals that are reachable. All of +/// these should be initialized to as general value as possible, usually +/// achieved using `kani::any`. The harness must call e.g. `foo` at least once +/// and if `foo` has type parameters, only one instantiation of those parameters +/// is admissible. Violating either results in a compile error. +/// +/// If any of those types have special invariants you can use `kani::assume` to +/// enforce them, but other than condition on inputs and checks of outputs +/// should be in the contract, not the harness for maximum soundness. +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. +#[proc_macro_attribute] +pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::proof_for_contract(attr, item) +} + /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] mod sysroot { use proc_macro_error::{abort, abort_call_site}; + mod contracts; + + pub use contracts::{ensures, proof_for_contract, requires}; + use super::*; use { @@ -271,4 +341,7 @@ mod regular { no_op!(stub); no_op!(unstable); no_op!(unwind); + no_op!(requires); + no_op!(ensures); + no_op!(proof_for_contract); } diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs new file mode 100644 index 000000000000..856f25b7d597 --- /dev/null +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -0,0 +1,439 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +use std::collections::{HashMap, HashSet}; + +use proc_macro::TokenStream; + +use { + quote::{quote, ToTokens}, + syn::{parse_macro_input, spanned::Spanned, visit::Visit, Expr, ItemFn}, +}; + +use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; + +/// Create a unique hash for a token stream (basically a [`std::hash::Hash`] +/// impl for `proc_macro2::TokenStream`). +fn hash_of_token_stream(hasher: &mut H, stream: proc_macro2::TokenStream) { + use proc_macro2::TokenTree; + use std::hash::Hash; + for token in stream { + match token { + TokenTree::Ident(i) => i.hash(hasher), + TokenTree::Punct(p) => p.as_char().hash(hasher), + TokenTree::Group(g) => { + std::mem::discriminant(&g.delimiter()).hash(hasher); + hash_of_token_stream(hasher, g.stream()); + } + TokenTree::Literal(lit) => lit.to_string().hash(hasher), + } + } +} + +use syn::visit_mut::VisitMut; + +/// Hash this `TokenStream` and return an integer that is at most digits +/// long when hex formatted. +fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { + use std::hash::Hasher; + let mut hasher = std::collections::hash_map::DefaultHasher::default(); + hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone())); + let long_hash = hasher.finish(); + long_hash % 0x1_000_000 // six hex digits +} + +/// Makes consistent names for a generated function which was created for +/// `purpose`, from an attribute that decorates `related_function` with the +/// hash `hash`. +fn identifier_for_generated_function(related_function: &ItemFn, purpose: &str, hash: u64) -> Ident { + let identifier = format!("{}_{purpose}_{hash:x}", related_function.sig.ident); + Ident::new(&identifier, proc_macro2::Span::mixed_site()) +} + +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + requires_ensures_alt(attr, item, true) +} + +pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + requires_ensures_alt(attr, item, false) +} + +/// Collect all named identifiers used in the argument patterns of a function. +struct ArgumentIdentCollector(HashSet); + +impl ArgumentIdentCollector { + fn new() -> Self { + Self(HashSet::new()) + } +} + +impl<'ast> Visit<'ast> for ArgumentIdentCollector { + fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) { + self.0.insert(i.ident.clone()); + syn::visit::visit_pat_ident(self, i) + } + fn visit_receiver(&mut self, _: &'ast syn::Receiver) { + self.0.insert(Ident::new("self", proc_macro2::Span::call_site())); + } +} + +/// Applies the contained renaming (key renamed to value) to every ident pattern +/// and ident expr visited. +struct Renamer<'a>(&'a HashMap); + +impl<'a> VisitMut for Renamer<'a> { + fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { + if i.path.segments.len() == 1 { + i.path + .segments + .first_mut() + .and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone())); + } + } + + /// This restores shadowing. Without this we would rename all ident + /// occurrences, but not rebinding location. This is because our + /// [`visit_expr_path_mut`] is scope-unaware. + fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { + if let Some(new) = self.0.get(&i.ident) { + i.ident = new.clone(); + } + } +} + +/// Does the provided path have the same chain of identifiers as `mtch` (match) +/// and no arguments anywhere? +/// +/// So for instance (using some pseudo-syntax for the [`syn::Path`]s) +/// `matches_path(std::vec::Vec, &["std", "vec", "Vec"]) == true` but +/// `matches_path(std::Vec::::contains, &["std", "Vec", "contains"]) != +/// true`. +/// +/// This is intended to be used to match the internal `kanitool` family of +/// attributes which we know to have a regular structure and no arguments. +fn matches_path(path: &syn::Path, mtch: &[E]) -> bool +where + Ident: std::cmp::PartialEq, +{ + path.segments.len() == mtch.len() + && path.segments.iter().all(|s| s.arguments.is_empty()) + && path.leading_colon.is_none() + && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) +} + +/// Classifies the state a function is in the contract handling pipeline. +#[derive(Clone, Copy, PartialEq, Eq)] +enum ContractFunctionState { + /// This is the original code, re-emitted from a contract attribute. + Original, + /// This is the first time a contract attribute is evaluated on this + /// function. + Untouched, + /// This is a check function that was generated from a previous evaluation + /// of a contract attribute. + Check, +} + +impl ContractFunctionState { + /// Find out if this attribute could be describing a "contract handling" + /// state and if so return it. + fn from_attribute(attribute: &syn::Attribute) -> Option { + if let syn::Meta::List(lst) = &attribute.meta { + if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) { + match syn::parse2::(lst.tokens.clone()) { + Err(e) => { + lst.span().unwrap().error(format!("{e}")).emit(); + } + Ok(ident) => { + if ident.to_string() == "check" { + return Some(Self::Check); + } else { + lst.span().unwrap().error("Expected `check` ident").emit(); + } + } + } + } + } + if let syn::Meta::NameValue(nv) = &attribute.meta { + if matches_path(&nv.path, &["kanitool", "checked_with"]) { + return Some(ContractFunctionState::Original); + } + } + None + } +} + +/// A visitor which injects a copy of the token stream it holds before every +/// `return` expression. +/// +/// This is intended to be used with postconditions and for that purpose it also +/// performs a rewrite where the return value is first bound to `result` so the +/// postconditions can access it. +/// +/// # Example +/// +/// The expression `return x;` turns into +/// +/// ```rs +/// { // Always opens a new block +/// let result = x; +/// +/// return result; +/// } +/// ``` +struct PostconditionInjector(TokenStream2); + +impl VisitMut for PostconditionInjector { + /// We leave this emtpy to stop the recursion here. We don't want to look + /// inside the closure, because the return statements contained within are + /// for a different function. + fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) {} + + fn visit_expr_mut(&mut self, i: &mut Expr) { + if let syn::Expr::Return(r) = i { + let tokens = self.0.clone(); + let mut output = TokenStream2::new(); + if let Some(expr) = &mut r.expr { + // In theory the return expression can contain itself a `return` + // so we need to recurse here. + self.visit_expr_mut(expr); + output.extend(quote!(let result = #expr;)); + *expr = Box::new(Expr::Verbatim(quote!(result))); + } + *i = syn::Expr::Verbatim(quote!({ + #output + #tokens + #i + })) + } else { + syn::visit_mut::visit_expr_mut(self, i) + } + } +} + +/// A supporting function for creating shallow, unsafe copies of the arguments +/// for the postconditions. +/// +/// This function: +/// - Collects all [`Ident`]s found in the argument patterns; +/// - Creates new names for them; +/// - Replaces all occurrences of those idents in `attrs` with the new names and; +/// - Returns the mapping of old names to new names. +fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { + let mut arg_ident_collector = ArgumentIdentCollector::new(); + arg_ident_collector.visit_signature(&sig); + + let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); + let arg_idents = arg_ident_collector + .0 + .into_iter() + .map(|i| { + let new = mk_new_ident_for(&i); + (i, new) + }) + .collect::>(); + + let mut ident_rewriter = Renamer(&arg_idents); + ident_rewriter.visit_expr_mut(attr); + arg_idents +} + +/// The main meat of handling requires/ensures contracts. +/// +/// Generates a `check__` function that assumes preconditions +/// and asserts postconditions. The check function is also marked as generated +/// with the `#[kanitool::is_contract_generated(check)]` attribute. +/// +/// Decorates the original function with `#[kanitool::checked_by = +/// "check__"] +/// +/// The check function is a copy of the original function with preconditions +/// added before the body and postconditions after as well as injected before +/// every `return` (see [`PostconditionInjector`]). Attributes on the original +/// function are also copied to the check function. Each clause (requires or +/// ensures) after the first clause will be ignored on the original function +/// (detected by finding the `kanitool::checked_with` attribute). On the check +/// function (detected by finding the `kanitool::is_contract_generated` +/// attribute) it expands into a new layer of pre- or postconditions. This state +/// machine is also explained in more detail in comments in the body of this +/// macro. +/// +/// In the check function all named arguments of the function are unsafely +/// shallow-copied with the `kani::untracked_deref` function to circumvent the +/// borrow checker for postconditions. We must ensure that those copies are not +/// dropped so after the postconditions we call `mem::forget` on each copy. +/// +/// # Complete example +/// +/// ```rs +/// #[kani::requires(divisor != 0)] +/// #[kani::ensures(result <= dividend)] +/// fn div(dividend: u32, divisor: u32) -> u32 { +/// dividend / divisor +/// } +/// ``` +/// +/// Turns into +/// +/// ```rs +/// #[kanitool::checked_with = "div_check_965916"] +/// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +/// +/// #[allow(dead_code)] +/// #[allow(unused_variables)] +/// #[kanitool::is_contract_generated(check)] +/// fn div_check_965916(dividend: u32, divisor: u32) -> u32 { +/// let dividend_renamed = kani::untracked_deref(÷nd); +/// let divisor_renamed = kani::untracked_deref(&divisor); +/// let result = { kani::assume(divisor != 0); { dividend / divisor } }; +/// kani::assert(result <= dividend_renamed, "result <= dividend"); +/// std::mem::forget(dividend_renamed); +/// std::mem::forget(divisor_renamed); +/// result +/// } +/// ``` +fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { + let attr_copy = proc_macro2::TokenStream::from(attr.clone()); + let mut attr = parse_macro_input!(attr as Expr); + + let mut output = proc_macro2::TokenStream::new(); + + let a_short_hash = short_hash_of_token_stream(&item); + let item_fn = &mut parse_macro_input!(item as ItemFn); + + // If we didn't find any other contract handling related attributes we + // assume this function has not been touched by a contract before. + let function_state = item_fn + .attrs + .iter() + .find_map(ContractFunctionState::from_attribute) + .unwrap_or(ContractFunctionState::Untouched); + + if matches!(function_state, ContractFunctionState::Original) { + // If we're the original function that means we're *not* the first time + // that a contract attribute is handled on this function. This means + // there must exist a generated check function somewhere onto which the + // attributes have been copied and where they will be expanded into more + // checks. So we just return outselves unchanged. + return item_fn.into_token_stream().into(); + } + + let attrs = std::mem::replace(&mut item_fn.attrs, vec![]); + + if matches!(function_state, ContractFunctionState::Untouched) { + // We are the first time a contract is handled on this function, so + // we're responsible for: + // 1. Generating a name for the check function; + // 2. Emitting the original, unchanged item and register the check + // function on it via attribute; + // 3. Renaming our item to the new name; + // 4. And (minor point) adding #[allow(dead_code)] and + // #[allow(unused_variables)] to the check function attributes. + + let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); + + // Constructing string literals explicitly here, because `stringify!` + // doesn't work. Let's say we have an identifier `check_fn` and we were + // to do `quote!(stringify!(check_fn))` to try to have it expand to + // `"check_fn"` in the generated code. Then when the next macro parses + // this it will *not* see the literal `"check_fn"` as you may expect but + // instead the *expression* `stringify!(check_fn)`. + let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + + // The order of `attrs` and `kanitool::{checked_with, + // is_contract_generated}` is important here, because macros are + // expanded outside in. This way other contract annotations in `attrs` + // sees those attribuites and can use them to determine + // `function_state`. + // + // We're emitting the original here but the same applies later when we + // emit the check function. + output.extend(quote!( + #(#attrs)* + #[kanitool::checked_with = #check_fn_name_str] + #item_fn + + #[allow(dead_code)] + #[allow(unused_variables)] + )); + item_fn.sig.ident = check_fn_name; + } + + let call_to_prior = &mut item_fn.block; + + let check_body = if is_requires { + quote!( + kani::assume(#attr); + #call_to_prior + ) + } else { + let arg_idents = rename_argument_occurences(&item_fn.sig, &mut attr); + + let arg_copy_names = arg_idents.values(); + let also_arg_copy_names = arg_copy_names.clone(); + let arg_idents = arg_idents.keys(); + + // The code that enforces the postconditions and cleans up the shallow + // argument copies (with `mem::forget`). + let exec_postconditions = quote!( + kani::assert(#attr, stringify!(#attr_copy)); + #(std::mem::forget(#also_arg_copy_names);)* + ); + + let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); + inject_conditions.visit_block_mut(&mut *call_to_prior); + + quote!( + #(let #arg_copy_names = kani::untracked_deref(&#arg_idents);)* + let result = #call_to_prior; + #exec_postconditions + result + ) + }; + + let sig = &item_fn.sig; + + // Prepare emitting the check function by emitting the rest of the + // attributes. + output.extend(quote!( + #(#attrs)* + )); + + if matches!(function_state, ContractFunctionState::Untouched) { + // If it's the first time we also emit this marker. Again, order is + // important so this happens as the last emitted attribute. + output.extend(quote!(#[kanitool::is_contract_generated(check)])); + } + + // Finally emit the check function itself. + output.extend(quote!( + #sig { + #check_body + } + )); + output.into() +} + +/// This is very similar to the kani_attribute macro, but it instead creates +/// key-value style attributes which I find a little easier to parse. +macro_rules! passthrough { + ($name:ident, $allow_dead_code:ident) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let fn_item = proc_macro2::TokenStream::from(item); + let name = Ident::new(stringify!($name), proc_macro2::Span::call_site()); + let extra_attrs = if $allow_dead_code { + quote!(#[allow(dead_code)]) + } else { + quote!() + }; + quote!( + #extra_attrs + #[kanitool::#name = stringify!(#args)] + #fn_item + ) + .into() + } + } +} + +passthrough!(proof_for_contract, true); diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected new file mode 100644 index 000000000000..587dc3f46975 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -0,0 +1,6 @@ +max.assertion\ +- Status: FAILURE\ +- Description: "result == x"\ +in function max + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs new file mode 100644 index 000000000000..91638b1cc037 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn max_harness() { + let _ = Box::new(9_usize); + max(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected new file mode 100644 index 000000000000..af1e09d1fe62 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -0,0 +1,6 @@ +max.assertion\ +- Status: SUCCESS\ +- Description: "result == x || result == y"\ +in function max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs new file mode 100644 index 000000000000..df8d3a2361fb --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result == x || result == y)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn max_harness() { + let _ = Box::new(()); + max(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected new file mode 100644 index 000000000000..179430b8a249 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -0,0 +1,4 @@ +assertion\ +- Status: FAILURE\ +- Description: "attempt to divide by zero"\ +arbitrary_requires_fail.rs:7:5 diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs new file mode 100644 index 000000000000..d052e19b0335 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof_for_contract(div)] +fn div_harness() { + let _ = Box::new(()); + div(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected new file mode 100644 index 000000000000..814fe6757ca3 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -0,0 +1,6 @@ +div.arithmetic_overflow\ +- Status: SUCCESS\ +- Description: "attempt to divide by zero"\ +in function div + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/arbitrary_requires_pass.rs b/tests/expected/function-contract/arbitrary_requires_pass.rs new file mode 100644 index 000000000000..a9bb08d467b8 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(divisor != 0)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof_for_contract(div)] +fn div_harness() { + let _ = Box::new(()); + div(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/attribute_complain.expected b/tests/expected/function-contract/attribute_complain.expected new file mode 100644 index 000000000000..8edcde3df910 --- /dev/null +++ b/tests/expected/function-contract/attribute_complain.expected @@ -0,0 +1 @@ +error: Using the proof_for_contract attribute requires activating the unstable `function-contracts` feature diff --git a/tests/expected/function-contract/attribute_complain.rs b/tests/expected/function-contract/attribute_complain.rs new file mode 100644 index 000000000000..f16e975c2001 --- /dev/null +++ b/tests/expected/function-contract/attribute_complain.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(true)] +fn always() {} + +#[kani::proof_for_contract(always)] +fn always_harness() { + let _ = Box::new(()); + always(); +} diff --git a/tests/expected/function-contract/attribute_no_complain.expected b/tests/expected/function-contract/attribute_no_complain.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/attribute_no_complain.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/attribute_no_complain.rs b/tests/expected/function-contract/attribute_no_complain.rs new file mode 100644 index 000000000000..bcf1f0cadafd --- /dev/null +++ b/tests/expected/function-contract/attribute_no_complain.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(true)] +fn always() {} + +#[kani::proof] +fn random_harness() {} diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected new file mode 100644 index 000000000000..c31b5c389fc8 --- /dev/null +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -0,0 +1,5 @@ +- Status: SUCCESS\ +- Description: "(result == x) | (result == y)"\ +in function max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_from_external_mod.rs b/tests/expected/function-contract/checking_from_external_mod.rs new file mode 100644 index 000000000000..43d1551f9aef --- /dev/null +++ b/tests/expected/function-contract/checking_from_external_mod.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures((result == x) | (result == y))] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +mod harnesses { + #[kani::proof_for_contract(super::max)] + fn max_harness() { + let _ = Box::new(9_usize); + super::max(7, 6); + } +} diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected new file mode 100644 index 000000000000..d5a390be8425 --- /dev/null +++ b/tests/expected/function-contract/checking_in_impl.expected @@ -0,0 +1,5 @@ +- Status: SUCCESS\ +- Description: "(result == self) | (result == y)"\ +in function WrappedInt::max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_in_impl.rs b/tests/expected/function-contract/checking_in_impl.rs new file mode 100644 index 000000000000..7d5c0506d9df --- /dev/null +++ b/tests/expected/function-contract/checking_in_impl.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +extern crate kani; + +#[derive(Copy, Clone, PartialEq, Eq, kani::Arbitrary)] +struct WrappedInt(u32); + +impl WrappedInt { + #[kani::ensures((result == self) | (result == y))] + fn max(self, y: WrappedInt) -> WrappedInt { + Self(if self.0 > y.0 { self.0 } else { y.0 }) + } +} + +#[kani::proof_for_contract(WrappedInt::max)] +fn max_harness() { + let _ = Box::new(9_usize); + WrappedInt(7).max(WrappedInt(6)); +} diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected new file mode 100644 index 000000000000..9488e9dcac9a --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -0,0 +1,8 @@ +gcd.assertion\ +- Status: FAILURE\ +- Description: "result != 0 && x % result == 0 && y % result == 0"\ +in function gcd + +Failed Checks: result != 0 && x % result == 0 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_failure_code.rs b/tests/expected/function-contract/gcd_failure_code.rs new file mode 100644 index 000000000000..f76e04b75fee --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_code.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + // Added a +1 below to make it no longer satisfy the contract + min = res + 1; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::unwind(12)] +#[kani::proof_for_contract(gcd)] +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected new file mode 100644 index 000000000000..3ae94b199d6e --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -0,0 +1,8 @@ +gcd.assertion\ +- Status: FAILURE\ +- Description: "result != 0 && x % result == 1 && y % result == 0"\ +in function gcd\ + +Failed Checks: result != 0 && x % result == 1 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_failure_contract.rs b/tests/expected/function-contract/gcd_failure_contract.rs new file mode 100644 index 000000000000..6b835466c5a0 --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_contract.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +// Changed `0` to `1` in `x % result == 0` to mess with this contract +#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected new file mode 100644 index 000000000000..d75b31b151df --- /dev/null +++ b/tests/expected/function-contract/gcd_success.expected @@ -0,0 +1,6 @@ +gcd.assertion\ +- Status: SUCCESS\ +- Description: "result != 0 && x % result == 0 && y % result == 0"\ +in function gcd + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs new file mode 100644 index 000000000000..d3a2c75b7d20 --- /dev/null +++ b/tests/expected/function-contract/gcd_success.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn gcd_harness() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/pattern_use.expected b/tests/expected/function-contract/pattern_use.expected new file mode 100644 index 000000000000..1485191557db --- /dev/null +++ b/tests/expected/function-contract/pattern_use.expected @@ -0,0 +1,3 @@ +assertion\ +- Status: FAILURE\ +- Description: "attempt to divide by zero"\ diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs new file mode 100644 index 000000000000..a51312acd2f0 --- /dev/null +++ b/tests/expected/function-contract/pattern_use.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result <= dividend)] +fn div((dividend, divisor): (u32, u32)) -> u32 { + dividend / divisor +} + +#[kani::proof_for_contract(div)] +fn div_harness() { + let _ = Box::new(()); + div((kani::any(), kani::any())); +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs new file mode 100644 index 000000000000..3d88fc0926ed --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn allowed_pointer(t: *const bool) {} + +#[kani::proof_for_contract(allowed_pointer)] +fn allowed_pointer_harness() { + let _ = Box::new(()); + let mut a = Box::new(true); + allowed_pointer(Box::into_raw(a)) +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs new file mode 100644 index 000000000000..22771f76632d --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn allowed_mut_ref(t: &mut bool) {} + +#[kani::proof_for_contract(allowed_mut_ref)] +fn allowed_mut_ref_harness() { + let _ = Box::new(()); + let mut a = true; + allowed_mut_ref(&mut a) +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs new file mode 100644 index 000000000000..07da23e907a3 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +static mut B: bool = false; + +#[kani::ensures(true)] +fn allowed_mut_return_ref<'a>() -> &'a mut bool { + unsafe { &mut B as &'a mut bool } +} + +#[kani::proof_for_contract(allowed_mut_return_ref)] +fn allowed_mut_return_ref_harness() { + let _ = Box::new(()); + allowed_mut_return_ref(); +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs new file mode 100644 index 000000000000..3dd4145eff9c --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn allowed_ref(t: &bool) {} + +#[kani::proof_for_contract(allowed_ref)] +fn allowed_ref_harness() { + let _ = Box::new(()); + let a = true; + allowed_ref(&a) +} diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.expected b/tests/expected/function-contract/prohibit-pointers/hidden.expected new file mode 100644 index 000000000000..59e40d5aadc8 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/hidden.expected @@ -0,0 +1 @@ +error: This argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.rs b/tests/expected/function-contract/prohibit-pointers/hidden.rs new file mode 100644 index 000000000000..9ca23fe6b2e1 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/hidden.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +struct HidesAPointer(*mut u32); + +#[kani::ensures(true)] +fn hidden_pointer(h: HidesAPointer) {} + +#[kani::proof_for_contract(hidden_pointer)] +fn harness() { + let mut a = 0; + hidden_pointer(HidesAPointer(&mut a)) +} diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected b/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected new file mode 100644 index 000000000000..916854aa3131 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected @@ -0,0 +1 @@ +error: This argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs new file mode 100644 index 000000000000..24e9d006a9c0 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn plain_pointer(t: *mut i32) {} + +#[kani::proof_for_contract(plain_pointer)] +fn plain_ptr_harness() { + let mut a = 0; + plain_pointer(&mut a) +} diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.expected b/tests/expected/function-contract/prohibit-pointers/return_pointer.expected new file mode 100644 index 000000000000..8f3689888d92 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.expected @@ -0,0 +1 @@ +error: The return contains a pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs new file mode 100644 index 000000000000..44e57ed9bc9d --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn return_pointer() -> *const usize { + unreachable!() +} + +#[kani::proof_for_contract(return_pointer)] +fn return_ptr_harness() { + return_pointer(); +} diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected new file mode 100644 index 000000000000..a65fff824ea6 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -0,0 +1,8 @@ +max.assertion\ +- Status: FAILURE\ +- Description: "result == x"\ +in function max + +Failed Checks: result == x + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs new file mode 100644 index 000000000000..687853612dcc --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn max_harness() { + let _ = Box::new(9_usize); + max(7, 9); +} diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected new file mode 100644 index 000000000000..b3e15aefcb9d --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -0,0 +1,6 @@ +max.assertion\ +- Status: SUCCESS\ +- Description: "(result == x) | (result == y)"\ +in function max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs new file mode 100644 index 000000000000..2d36f5c96e88 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures((result == x) | (result == y))] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn max_harness() { + let _ = Box::new(9_usize); + max(7, 6); +}