diff --git a/docs/src/getting-started/verification-results/src/main.rs b/docs/src/getting-started/verification-results/src/main.rs index 72653cf4dc8f..7a03b34f0f9e 100644 --- a/docs/src/getting-started/verification-results/src/main.rs +++ b/docs/src/getting-started/verification-results/src/main.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #[kani::proof] -#[kani::unwind(4)] // ANCHOR: success_example fn success_example() { let mut sum = 0; diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index d4dd458efb4c..7816876d460e 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -166,10 +166,10 @@ forget | Yes | | frem_fast | No | | fsub_fast | Yes | | likely | Yes | | -log10f32 | No | | -log10f64 | No | | -log2f32 | No | | -log2f64 | No | | +log10f32 | Partial | Results are overapproximated | +log10f64 | Partial | Results are overapproximated | +log2f32 | Partial | Results are overapproximated | +log2f64 | Partial | Results are overapproximated | logf32 | Partial | Results are overapproximated | logf64 | Partial | Results are overapproximated | maxnumf32 | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 7f19e5814ce0..b210b2c9333e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -8,27 +8,23 @@ use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::mir::Local; +use stable_mir::mir::{Local, VarDebugInfoContents}; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; 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 /// for which it needs to be enforced. /// - /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance - /// of it. Panics if there are more or less than one instance. - /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function, - /// turns it into a CBMC contract and attaches it to the symbol for the previously resolved - /// instance. + /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one + /// instance of it. Panics if there are more or less than one instance. + /// 2. The additional arguments for the inner checks are locations that may be modified. + /// Add them to the list of CBMC's assigns. /// 3. Returns the mangled name of the symbol it attached the contract to. - /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract` - /// which has `static mut REENTRY : bool` declared inside. - /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is - /// comprised of the file path that `checked_with` is located in, the name of the + /// 4. Returns the full path to the static marked with `#[kanitool::recursion_tracker]` which + /// is passed to the `--nondet-static-exclude` argument. + /// This flag expects the file path that `checked_with` is located in, the name of the /// `checked_with` function and the name of the constant (`REENTRY`). pub fn handle_check_contract( &mut self, @@ -36,86 +32,101 @@ impl<'tcx> GotocCtx<'tcx> { items: &[MonoItem], ) -> AssignsContract { let tcx = self.tcx; - let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract); + let modify = items + .iter() + .find_map(|item| { + // Find the instance under contract + let MonoItem::Fn(instance) = *item else { return None }; + if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { + self.find_modifies(instance) + } else { + None + } + }) + .unwrap(); + self.attach_modifies_contract(modify); + let recursion_tracker = self.find_recursion_tracker(items); + AssignsContract { recursion_tracker, contracted_function_name: modify.mangled_name() } + } - let recursion_wrapper_id = - function_under_contract_attrs.checked_with_id().unwrap().unwrap(); - let expected_name = format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id)); - let mut recursion_tracker = items.iter().filter_map(|i| match i { - MonoItem::Static(recursion_tracker) - if (*recursion_tracker).name().contains(expected_name.as_str()) => + /// The name and location for the recursion tracker should match the exact information added + /// to the symbol table, otherwise our contract instrumentation will silently failed. + /// This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly + /// handle this tracker. CBMC silently fails if there is no match in the symbol table + /// that correspond to the argument of this flag. + /// More details at https://github.com/model-checking/kani/pull/3045. + /// + /// We must use the pretty name of the tracker instead of the mangled name. + /// This restriction comes from `--nondet-static-exclude` in CBMC. + /// Mode details at https://github.com/diffblue/cbmc/issues/8225. + fn find_recursion_tracker(&mut self, items: &[MonoItem]) -> Option { + // Return item tagged with `#[kanitool::recursion_tracker]` + let mut recursion_trackers = items.iter().filter_map(|item| { + let MonoItem::Static(static_item) = item else { return None }; + if !static_item + .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()]) + .is_empty() { - Some(*recursion_tracker) + let span = static_item.span(); + let loc = self.codegen_span_stable(span); + Some(format!( + "{}:{}", + loc.filename().expect("recursion location wrapper should have a file name"), + static_item.name(), + )) + } else { + None } - _ => None, }); - let recursion_tracker_def = recursion_tracker - .next() - .expect("There should be at least one recursion tracker (REENTRY) in scope"); + let recursion_tracker = recursion_trackers.next(); assert!( - recursion_tracker.next().is_none(), - "Only one recursion tracker (REENTRY) may be in scope" + recursion_trackers.next().is_none(), + "Expected up to one recursion tracker (`REENTRY`) in scope" ); + recursion_tracker + } - let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id); - let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper); - // The name and location for the recursion tracker should match the exact information added - // to the symbol table, otherwise our contract instrumentation will silently failed. - // This happens because Kani relies on `--nondet-static-exclude` from CBMC to properly - // handle this tracker. CBMC silently fails if there is no match in the symbol table - // that correspond to the argument of this flag. - // More details at https://github.com/model-checking/kani/pull/3045. - let full_recursion_tracker_name = format!( - "{}:{}", - location_of_recursion_wrapper - .filename() - .expect("recursion location wrapper should have a file name"), - // We must use the pretty name of the tracker instead of the mangled name. - // This restrictions comes from `--nondet-static-exclude` in CBMC. - // Mode details at https://github.com/diffblue/cbmc/issues/8225. - recursion_tracker_def.name(), - ); - - let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap(); - let mut instance_under_contract = items.iter().filter_map(|i| match i { - MonoItem::Fn(instance @ Instance { def, .. }) - if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) => - { - Some(*instance) - } - _ => None, - }); - let instance_of_check = instance_under_contract.next().unwrap(); - assert!( - instance_under_contract.next().is_none(), - "Only one instance of a checked function may be in scope" - ); - let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn); - let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| { - debug!(?instance_of_check, "had no assigns contract specified"); - vec![] - }); - self.attach_modifies_contract(instance_of_check, assigns_contract); - let wrapper_name = instance_of_check.mangled_name(); - - AssignsContract { - recursion_tracker: full_recursion_tracker_name, - contracted_function_name: wrapper_name, - } + /// Find the modifies recursively since we may have a recursion wrapper. + /// I.e.: [recursion_wrapper ->]? check -> modifies. + fn find_modifies(&mut self, instance: Instance) -> Option { + let contract_attrs = + KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?; + let mut find_closure = |inside: Instance, name: &str| { + let body = self.transformer.body(self.tcx, inside); + body.var_debug_info.iter().find_map(|var_info| { + if var_info.name.as_str() == name { + let ty = match &var_info.value { + VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), + VarDebugInfoContents::Const(const_op) => const_op.ty(), + }; + if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { + return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap()); + } + } + None + }) + }; + let check_instance = if contract_attrs.has_recursion { + let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?; + find_closure(recursion_check, contract_attrs.checked_with.as_str())? + } else { + find_closure(instance, contract_attrs.checked_with.as_str())? + }; + find_closure(check_instance, contract_attrs.modifies_wrapper.as_str()) } /// Convert the Kani level contract into a CBMC level contract by creating a /// CBMC lambda. fn codegen_modifies_contract( &mut self, - modified_places: Vec, + goto_annotated_fn_name: &str, + modifies: Instance, loc: Location, ) -> FunctionContract { - let goto_annotated_fn_name = self.current_fn().name(); let goto_annotated_fn_typ = self .symbol_table - .lookup(&goto_annotated_fn_name) + .lookup(goto_annotated_fn_name) .unwrap_or_else(|| panic!("Function '{goto_annotated_fn_name}' is not declared")) .typ .clone(); @@ -141,13 +152,24 @@ impl<'tcx> GotocCtx<'tcx> { }) .unwrap_or_default(); - let assigns = modified_places + // The last argument is a tuple with addresses that can be modified. + let modifies_local = Local::from(modifies.fn_abi().unwrap().args.len()); + let modifies_ty = self.local_ty_stable(modifies_local); + let modifies_args = + self.codegen_place_stable(&modifies_local.into(), loc).unwrap().goto_expr; + let TyKind::RigidTy(RigidTy::Tuple(modifies_tys)) = modifies_ty.kind() else { + unreachable!("found {:?}", modifies_ty.kind()) + }; + let assigns: Vec<_> = modifies_tys .into_iter() - .map(|local| { - if self.is_fat_pointer_stable(self.local_ty_stable(local)) { - let unref = match self.local_ty_stable(local).kind() { - TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => ty, - kind => unreachable!("{:?} is not a reference", kind), + .enumerate() + .map(|(idx, ty)| { + assert!(ty.kind().is_any_ptr(), "Expected pointer, but found {}", ty); + let ptr = modifies_args.clone().member(idx.to_string(), &self.symbol_table); + if self.is_fat_pointer_stable(ty) { + let unref = match ty.kind() { + TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) => pointee_ty, + kind => unreachable!("Expected a raw pointer, but found {:?}", kind), }; let size = match unref.kind() { TyKind::RigidTy(RigidTy::Slice(elt_type)) => { @@ -176,30 +198,17 @@ impl<'tcx> GotocCtx<'tcx> { ), ) .call(vec![ - self.codegen_place_stable(&local.into(), loc) - .unwrap() - .goto_expr + ptr.clone() .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, - )), + ptr.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(), - ) + Lambda::as_contract_for(&goto_annotated_fn_typ, None, ptr.dereference()) } }) .chain(shadow_memory_assign) @@ -212,17 +221,19 @@ impl<'tcx> GotocCtx<'tcx> { /// `instance` must have previously been declared. /// /// This merges with any previously attached contracts. - pub fn attach_modifies_contract(&mut self, instance: Instance, modified_places: Vec) { + pub fn attach_modifies_contract(&mut self, instance: Instance) { // This should be safe, since the contract is pretty much evaluated as // though it was the first (or last) assertion in the function. assert!(self.current_fn.is_none()); - let body = instance.body().unwrap(); + let body = self.transformer.body(self.tcx, instance); self.set_current_fn(instance, &body); - let goto_contract = - self.codegen_modifies_contract(modified_places, self.codegen_span_stable(body.span)); - let name = self.current_fn().name(); - - self.symbol_table.attach_contract(name, goto_contract); - self.reset_current_fn() + let mangled_name = instance.mangled_name(); + let goto_contract = self.codegen_modifies_contract( + &mangled_name, + instance, + self.codegen_span_stable(instance.def.span()), + ); + self.symbol_table.attach_contract(&mangled_name, goto_contract); + self.reset_current_fn(); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index d8efef070a95..57f52dc50b18 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -466,10 +466,10 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place_stable(place, Expr::c_false(), loc) } "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), - "log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)), - "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)), - "log2f32" => unstable_codegen!(codegen_simple_intrinsic!(Log2f)), - "log2f64" => unstable_codegen!(codegen_simple_intrinsic!(Log2)), + "log10f32" => codegen_simple_intrinsic!(Log10f), + "log10f64" => codegen_simple_intrinsic!(Log10), + "log2f32" => codegen_simple_intrinsic!(Log2f), + "log2f64" => codegen_simple_intrinsic!(Log2), "logf32" => codegen_simple_intrinsic!(Logf), "logf64" => codegen_simple_intrinsic!(Log), "maxnumf32" => codegen_simple_intrinsic!(Fmaxf), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 1703335dda51..9baa3c59f4c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1140,7 +1140,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Mapping enums to CBMC types is rather complicated. There are a few cases to consider: /// 1. When there is only 0 or 1 variant, this is straightforward as the code shows - /// 2. When there are more variants, rust might decides to apply the typical encoding which + /// 2. When there are more variants, rust might decide to apply the typical encoding which /// regard enums as tagged union, or an optimized form, called niche encoding. /// /// The direct encoding is straightforward. Enums are just mapped to C as a struct of union of structs. @@ -1242,6 +1242,23 @@ impl<'tcx> GotocCtx<'tcx> { ) }), )); + // Check if any padding is needed for alignment. This is needed for + // https://github.com/model-checking/kani/issues/2857 for example. + // The logic for determining the maximum variant size is taken from: + // https://github.com/rust-lang/rust/blob/e60ebb2f2c1facba87e7971798f3cbdfd309cd23/compiler/rustc_session/src/code_stats.rs#L166 + let max_variant_size = variants + .iter() + .map(|l: &LayoutS| l.size) + .max() + .unwrap(); + let max_variant_size = std::cmp::max(max_variant_size, discr_offset); + if let Some(padding) = gcx.codegen_alignment_padding( + max_variant_size, + &layout, + fields.len(), + ) { + fields.push(padding); + } fields }) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 986cd00e32a5..0a92e07f4ab4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -264,7 +264,7 @@ impl CodegenBackend for GotocCodegenBackend { for harness in &unit.harnesses { let model_path = units.harness_model_path(*harness).unwrap(); let contract_metadata = - contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap(); + contract_metadata_for_harness(tcx, harness.def.def_id()); let (gcx, items, contract_info) = self.codegen_items( tcx, &[MonoItem::Fn(*harness)], @@ -448,12 +448,9 @@ impl CodegenBackend for GotocCodegenBackend { } } -fn contract_metadata_for_harness( - tcx: TyCtxt, - def_id: DefId, -) -> Result, ErrorGuaranteed> { +fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option { let attrs = KaniAttributes::for_def_id(tcx, def_id); - Ok(attrs.interpret_the_for_contract_attribute().transpose()?.map(|(_, id, _)| id)) + attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) } fn check_target(session: &Session) { diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 8c729bbdec9f..f75c0607e1bc 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -6,24 +6,16 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use rustc_ast::{ - attr, - token::Token, - token::TokenKind, - tokenstream::{TokenStream, TokenTree}, - AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, + attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, NestedMetaItem, }; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{ - def::DefKind, - def_id::{DefId, LocalDefId}, -}; +use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; use stable_mir::mir::mono::Instance as InstanceStable; -use stable_mir::mir::Local; use stable_mir::{CrateDef, DefId as StableDefId}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -56,24 +48,27 @@ enum KaniAttributeKind { /// name of the function which was generated as the sound stub from the /// contract of this function. ReplacedWith, + /// Attribute on a function with a contract that identifies the code + /// implementing the recursive check for the harness. + RecursionCheck, /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, - /// Identifies a set of pointer arguments that should be added to the write - /// set when checking a function contract. Placed on the inner check function. - /// - /// Emitted by the expansion of a `modifies` function contract clause. - Modifies, - /// A function used as the inner code of a contract check. + /// A function with contract expanded to include the write set as arguments. /// /// Contains the original body of the contracted function. The signature is /// expanded with additional pointer arguments that are not used in the function /// but referenced by the `modifies` annotation. - InnerCheck, + ModifiesWrapper, /// Attribute used to mark contracts for functions with recursion. /// We use this attribute to properly instantiate `kani::any_modifies` in /// cases when recursion is present given our contracts instrumentation. Recursion, + /// Attribute used to mark the static variable used for tracking recursion check. + RecursionTracker, + /// Generic marker that can be used to mark functions so this list doesn't have to keep growing. + /// This takes a key which is the marker. + FnMarker, /// Used to mark functions where generating automatic pointer checks should be disabled. This is /// used later to automatically attach pragma statements to locations. DisableChecks, @@ -91,11 +86,13 @@ impl KaniAttributeKind { | KaniAttributeKind::StubVerified | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable + | KaniAttributeKind::FnMarker | KaniAttributeKind::Recursion + | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith + | KaniAttributeKind::RecursionCheck | KaniAttributeKind::CheckedWith - | KaniAttributeKind::Modifies - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::DisableChecks => false, } @@ -125,6 +122,21 @@ pub struct KaniAttributes<'tcx> { map: BTreeMap>, } +#[derive(Clone, Debug)] +/// Bundle contract attributes for a function annotated with contracts. +pub struct ContractAttributes { + /// Whether the contract was marked with #[recursion] attribute. + pub has_recursion: bool, + /// The name of the contract recursion check. + pub recursion_check: Symbol, + /// The name of the contract check. + pub checked_with: Symbol, + /// The name of the contract replacement. + pub replaced_with: Symbol, + /// The name of the inner check used to modify clauses. + pub modifies_wrapper: Symbol, +} + impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { f.debug_struct("KaniAttributes") @@ -182,22 +194,28 @@ impl<'tcx> KaniAttributes<'tcx> { /// returned `Symbol` and `DefId` are respectively the name and id of /// `TARGET`. The `Span` is that of the contents of the attribute and used /// for error reporting. - fn interpret_stub_verified_attribute( - &self, - ) -> Vec> { + /// + /// Any error is emitted and the attribute is filtered out. + pub fn interpret_stub_verified_attribute(&self) -> Vec<(Symbol, DefId, Span)> { self.map .get(&KaniAttributeKind::StubVerified) .map_or([].as_slice(), Vec::as_slice) .iter() - .map(|attr| { - let name = expect_key_string_value(self.tcx.sess, attr)?; - let ok = self.resolve_sibling(name.as_str()).map_err(|e| { - self.tcx.dcx().span_err( - attr.span, - format!("Failed to resolve replacement function {}: {e}", name.as_str()), - ) - })?; - Ok((name, ok, attr.span)) + .filter_map(|attr| { + let name = expect_key_string_value(self.tcx.sess, attr).ok()?; + let def = self + .resolve_from_mod(name.as_str()) + .map_err(|e| { + self.tcx.dcx().span_err( + attr.span, + format!( + "Failed to resolve replacement function {}: {e}", + name.as_str() + ), + ) + }) + .ok()?; + Some((name, def, attr.span)) }) .collect() } @@ -209,13 +227,14 @@ impl<'tcx> KaniAttributes<'tcx> { /// 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). - pub(crate) 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)?; - self.resolve_sibling(name.as_str()).map(|ok| (name, ok, target.span)).map_err( - |resolve_err| { + /// + /// In the case of an error, this function will emit the error and return `None`. + pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> { + self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { + let name = expect_key_string_value(self.tcx.sess, target).ok()?; + self.resolve_from_mod(name.as_str()) + .map(|ok| (name, ok, target.span)) + .map_err(|resolve_err| { self.tcx.dcx().span_err( target.span, format!( @@ -223,81 +242,62 @@ impl<'tcx> KaniAttributes<'tcx> { name.as_str() ), ) - }, - ) + }) + .ok() }) } - /// Extract the name of the sibling function this function's contract is - /// checked with (if any). - /// - /// `None` indicates this function does not use a contract, `Some(Err(_))` - /// indicates a contract does exist but an error occurred during resolution. - pub fn checked_with(&self) -> Option> { - self.expect_maybe_one(KaniAttributeKind::CheckedWith) - .map(|target| expect_key_string_value(self.tcx.sess, target)) - } - pub fn proof_for_contract(&self) -> Option> { self.expect_maybe_one(KaniAttributeKind::ProofForContract) .map(|target| expect_key_string_value(self.tcx.sess, target)) } - pub fn inner_check(&self) -> Option> { - self.eval_sibling_attribute(KaniAttributeKind::InnerCheck) + /// Extract the name of the local that represents this function's contract is + /// checked with (if any). + /// + /// `None` indicates this function does not use a contract, or an error was found. + /// Note that the error will already be emitted, so we don't return an error. + pub fn contract_attributes(&self) -> Option { + let has_recursion = self.has_recursion(); + let recursion_check = self.attribute_value(KaniAttributeKind::RecursionCheck); + let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith); + let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith); + let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper); + + let total = recursion_check + .iter() + .chain(&checked_with) + .chain(&replace_with) + .chain(&modifies_wrapper) + .count(); + if total != 0 && total != 4 { + self.tcx.sess.dcx().err(format!( + "Failed to parse contract instrumentation tags in function `{}`.\ + Expected `4` attributes, but was only able to process `{total}`", + self.tcx.def_path_str(self.item) + )); + } + Some(ContractAttributes { + has_recursion, + recursion_check: recursion_check?, + checked_with: checked_with?, + replaced_with: replace_with?, + modifies_wrapper: modifies_wrapper?, + }) } - pub fn replaced_with(&self) -> Option> { - self.expect_maybe_one(KaniAttributeKind::ReplacedWith) - .map(|target| expect_key_string_value(self.tcx.sess, target)) + /// Return a function marker if any. + pub fn fn_marker(&self) -> Option { + self.attribute_value(KaniAttributeKind::FnMarker) } - /// Retrieves the global, static recursion tracker variable. - pub fn checked_with_id(&self) -> Option> { - self.eval_sibling_attribute(KaniAttributeKind::CheckedWith) + /// Check if function is annotated with any contract attribute. + pub fn has_contract(&self) -> bool { + self.map.contains_key(&KaniAttributeKind::CheckedWith) } - /// Find the `mod` that `self.item` is defined in, then search in the items defined in this - /// `mod` for an item that is named after the `name` in the `#[kanitool:: = ""]` - /// annotation on `self.item`. - /// - /// This is similar to [`resolve_fn`] but more efficient since it only looks inside one `mod`. - fn eval_sibling_attribute( - &self, - kind: KaniAttributeKind, - ) -> Option> { - use rustc_hir::{Item, ItemKind, Mod, Node}; - self.expect_maybe_one(kind).map(|target| { - let name = expect_key_string_value(self.tcx.sess, target)?; - let hir_map = self.tcx.hir(); - let hir_id = self.tcx.local_def_id_to_hir_id(self.item.expect_local()); - let find_in_mod = |md: &Mod<'_>| { - md.item_ids - .iter() - .find(|it| hir_map.item(**it).ident.name == name) - .unwrap() - .hir_id() - }; - - let result = match self.tcx.parent_hir_node(hir_id) { - Node::Item(Item { kind, .. }) => match kind { - ItemKind::Mod(m) => find_in_mod(m), - ItemKind::Impl(imp) => { - imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id() - } - other => panic!("Odd parent item kind {other:?}"), - }, - Node::Crate(m) => find_in_mod(m), - other => panic!("Odd parent node type {other:?}"), - } - .expect_owner() - .def_id - .to_def_id(); - Ok(result) - }) - } - - fn resolve_sibling(&self, path_str: &str) -> Result> { + /// Resolve a path starting from this item's module context. + fn resolve_from_mod(&self, path_str: &str) -> Result> { resolve_fn( self.tcx, self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), @@ -371,20 +371,20 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::StubVerified => { expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => { - self.expect_maybe_one(kind) - .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); + KaniAttributeKind::FnMarker + | KaniAttributeKind::CheckedWith + | KaniAttributeKind::ModifiesWrapper + | KaniAttributeKind::RecursionCheck + | KaniAttributeKind::ReplacedWith => { + self.attribute_value(kind); } 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. } - KaniAttributeKind::Modifies => { - self.modifies_contract(); - } - KaniAttributeKind::InnerCheck => { - self.inner_check(); + KaniAttributeKind::RecursionTracker => { + // Nothing to do here. This is used by contract instrumentation. } KaniAttributeKind::DisableChecks => { // Ignored here, because it should be an internal attribute. Actual validation @@ -394,6 +394,17 @@ impl<'tcx> KaniAttributes<'tcx> { } } + /// Get the value of an attribute if one exists. + /// + /// This expects up to one attribute with format `#[kanitool::("")]`. + /// + /// Any format or expectation error is emitted already, and does not need to be handled + /// upstream. + fn attribute_value(&self, kind: KaniAttributeKind) -> Option { + self.expect_maybe_one(kind) + .and_then(|target| expect_key_string_value(self.tcx.sess, target).ok()) + } + /// Check that any unstable API has been enabled. Otherwise, emit an error. /// /// TODO: Improve error message by printing the span of the harness instead of the definition. @@ -499,8 +510,9 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated - | KaniAttributeKind::Modifies - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper + | KaniAttributeKind::RecursionCheck + | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } @@ -508,6 +520,9 @@ impl<'tcx> KaniAttributes<'tcx> { // Internal attribute which shouldn't exist here. unreachable!() } + KaniAttributeKind::FnMarker => { + /* no-op */ + } }; harness }) @@ -515,15 +530,14 @@ impl<'tcx> KaniAttributes<'tcx> { fn handle_proof_for_contract(&self, harness: &mut HarnessAttributes) { let dcx = self.tcx.dcx(); - let (name, id, span) = match self.interpret_the_for_contract_attribute() { - None => unreachable!( - "impossible, was asked to handle `proof_for_contract` but didn't find such an attribute." - ), - Some(Err(_)) => return, // This error was already emitted - Some(Ok(values)) => values, + let (name, id, span) = match self.interpret_for_contract_attribute() { + None => return, // This error was already emitted + Some(values) => values, }; - let Some(Ok(replacement_name)) = KaniAttributes::for_item(self.tcx, id).checked_with() - else { + assert!(matches!( + &harness.kind, HarnessKind::ProofForContract { target_fn } + if *target_fn == name.to_string())); + if KaniAttributes::for_item(self.tcx, id).contract_attributes().is_none() { dcx.struct_span_err( span, format!( @@ -533,24 +547,14 @@ impl<'tcx> KaniAttributes<'tcx> { ) .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.") .emit(); - return; - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); + } } fn handle_stub_verified(&self, harness: &mut HarnessAttributes) { let dcx = self.tcx.dcx(); - for contract in self.interpret_stub_verified_attribute() { - let Ok((name, def_id, span)) = contract else { - // This error has already been emitted so we can ignore it now. - // Later the session will fail anyway so we can just - // optimistically forge on and try to find more errors. - continue; - }; - let replacement_name = match KaniAttributes::for_item(self.tcx, def_id).replaced_with() - { - None => { - dcx.struct_span_err( + for (name, def_id, span) in self.interpret_stub_verified_attribute() { + if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() { + dcx.struct_span_err( span, format!( "Failed to generate verified stub: Function `{}` has no contract.", @@ -564,13 +568,10 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::Stub.as_ref(), ), ) - .emit(); - continue; - } - Some(Ok(replacement_name)) => replacement_name, - Some(Err(_)) => continue, - }; - harness.stubs.push(self.stub_for_relative_item(name, replacement_name)) + .emit(); + return; + } + harness.verified_stubs.push(name.to_string()) } } @@ -595,92 +596,6 @@ 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 } - } - - /// Parse and interpret the `kanitool::modifies(var1, var2, ...)` annotation into the vector - /// `[var1, var2, ...]`. - pub fn modifies_contract(&self) -> Option> { - let local_def_id = self.item.expect_local(); - self.map.get(&KaniAttributeKind::Modifies).map(|attr| { - attr.iter() - .flat_map(|clause| match &clause.get_normal_item().args { - AttrArgs::Delimited(lvals) => { - parse_modify_values(self.tcx, local_def_id, &lvals.tokens) - } - _ => unreachable!(), - }) - .collect() - }) - } -} - -/// Pattern macro for the comma token used in attributes. -macro_rules! comma_tok { - () => { - TokenTree::Token(Token { kind: TokenKind::Comma, .. }, _) - }; -} - -/// Parse the token stream inside an attribute (like `kanitool::modifies`) as a comma separated -/// sequence of function parameter names on `local_def_id` (must refer to a function). Then -/// translates the names into [`Local`]s. -fn parse_modify_values<'a>( - tcx: TyCtxt<'a>, - local_def_id: LocalDefId, - t: &'a TokenStream, -) -> impl Iterator + 'a { - let mir = tcx.optimized_mir(local_def_id); - let mut iter = t.trees(); - std::iter::from_fn(move || { - let tree = iter.next()?; - let wrong_token_err = - || tcx.sess.dcx().span_err(tree.span(), "Unexpected token. Expected identifier."); - let result = match tree { - TokenTree::Token(token, _) => { - if let TokenKind::Ident(id, _) = &token.kind { - let hir = tcx.hir(); - let bid = hir.body_owned_by(local_def_id).id(); - Some( - hir.body_param_names(bid) - .zip(mir.args_iter()) - .find(|(name, _decl)| name.name == *id) - .unwrap() - .1 - .as_usize(), - ) - } else { - wrong_token_err(); - None - } - } - _ => { - wrong_token_err(); - None - } - }; - match iter.next() { - None | Some(comma_tok!()) => (), - Some(not_comma) => { - tcx.sess.dcx().span_err( - not_comma.span(), - "Unexpected token, expected end of attribute or comma", - ); - iter.by_ref().skip_while(|t| !matches!(t, comma_tok!())).count(); - } - } - result - }) } /// An efficient check for the existence for a particular [`KaniAttributeKind`]. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index b4ea06c8d5db..d16e4d2b93d1 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -11,23 +11,24 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::metadata::gen_proof_metadata; use crate::kani_middle::reachability::filter_crate_items; +use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; -use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata}; -use rustc_hir::def_id::{DefId, DefPathHash}; +use kani_metadata::{ArtifactType, AssignsContract, HarnessKind, HarnessMetadata, KaniMetadata}; +use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind}; use stable_mir::CrateDef; -use std::collections::{BTreeMap, HashMap, HashSet}; +use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; use std::path::{Path, PathBuf}; use tracing::debug; -/// A stable (across compilation sessions) identifier for the harness function. +/// An identifier for the harness function. type Harness = Instance; /// A set of stubs. @@ -124,20 +125,21 @@ fn stub_def(tcx: TyCtxt, def_id: DefId) -> FnDef { } } -/// Group the harnesses by their stubs. +/// Group the harnesses by their stubs and contract usage. fn group_by_stubs( tcx: TyCtxt, all_harnesses: &HashMap, ) -> Vec { - let mut per_stubs: HashMap, CodegenUnit> = - HashMap::default(); + let mut per_stubs: HashMap<_, CodegenUnit> = HashMap::default(); for (harness, metadata) in all_harnesses { let stub_ids = harness_stub_map(tcx, *harness, metadata); + let contracts = extract_contracts(tcx, *harness, metadata); let stub_map = stub_ids .iter() .map(|(k, v)| (tcx.def_path_hash(*k), tcx.def_path_hash(*v))) .collect::>(); - if let Some(unit) = per_stubs.get_mut(&stub_map) { + let key = (contracts, stub_map); + if let Some(unit) = per_stubs.get_mut(&key) { unit.harnesses.push(*harness); } else { let stubs = stub_ids @@ -145,12 +147,43 @@ fn group_by_stubs( .map(|(from, to)| (stub_def(tcx, *from), stub_def(tcx, *to))) .collect::>(); let stubs = apply_transitivity(tcx, *harness, stubs); - per_stubs.insert(stub_map, CodegenUnit { stubs, harnesses: vec![*harness] }); + per_stubs.insert(key, CodegenUnit { stubs, harnesses: vec![*harness] }); } } per_stubs.into_values().collect() } +#[derive(Copy, Clone, Debug, Ord, PartialOrd, PartialEq, Eq, Hash)] +enum ContractUsage { + Stub(usize), + Check(usize), +} + +/// Extract the contract related usages. +/// +/// Note that any error interpreting the result is emitted, but we delay aborting, so we emit as +/// many errors as possible. +fn extract_contracts( + tcx: TyCtxt, + harness: Harness, + metadata: &HarnessMetadata, +) -> BTreeSet { + let def = harness.def; + let mut result = BTreeSet::new(); + if let HarnessKind::ProofForContract { target_fn } = &metadata.attributes.kind { + if let Ok(check_def) = expect_resolve_fn(tcx, def, target_fn, "proof_for_contract") { + result.insert(ContractUsage::Check(check_def.def_id().to_index())); + } + } + + for stub in &metadata.attributes.verified_stubs { + let Ok(stub_def) = expect_resolve_fn(tcx, def, stub, "stub_verified") else { continue }; + result.insert(ContractUsage::Stub(stub_def.def_id().to_index())); + } + + result +} + /// Extract the filename for the metadata file. fn metadata_output_path(tcx: TyCtxt) -> PathBuf { let filepath = tcx.output_filenames(()).path(OutputType::Object); diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 816f25343fe3..ca4e8e749b75 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -9,14 +9,18 @@ //! //! Note that glob use statements can form loops. The paths can also walk through the loop. +use rustc_smir::rustc_internal; use std::collections::HashSet; use std::fmt; use std::iter::Peekable; +use rustc_errors::ErrorGuaranteed; use rustc_hir::def::{DefKind, Res}; use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE}; use rustc_hir::{ItemKind, UseKind}; use rustc_middle::ty::TyCtxt; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use stable_mir::CrateDef; use tracing::debug; /// Attempts to resolve a simple path (in the form of a string) to a function / method `DefId`. @@ -47,6 +51,33 @@ pub fn resolve_fn<'tcx>( } } +/// Resolve the name of a function from the context of the definition provided. +/// +/// Ideally this should pass a more precise span, but we don't keep them around. +pub fn expect_resolve_fn( + tcx: TyCtxt, + res_cx: T, + name: &str, + reason: &str, +) -> Result { + let internal_def_id = rustc_internal::internal(tcx, res_cx.def_id()); + let current_module = tcx.parent_module_from_def_id(internal_def_id.as_local().unwrap()); + let maybe_resolved = resolve_fn(tcx, current_module.to_local_def_id(), name); + let resolved = maybe_resolved.map_err(|err| { + tcx.dcx().span_err( + rustc_internal::internal(tcx, res_cx.span()), + format!("Failed to resolve `{name}` for `{reason}`: {err}"), + ) + })?; + let ty_internal = tcx.type_of(resolved).instantiate_identity(); + let ty = rustc_internal::stable(ty_internal); + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = ty.kind() { + Ok(def) + } else { + unreachable!("Expected function for `{name}`, but found: {ty}") + } +} + /// Attempts to resolve a simple path (in the form of a string) to a `DefId`. /// The current module is provided as an argument in order to resolve relative /// paths. diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index d3f2afc15d31..3d110c4e9656 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -54,6 +54,10 @@ impl MutableBody { &self.locals } + pub fn arg_count(&self) -> usize { + self.arg_count + } + /// Create a mutable body from the original MIR body. pub fn from(body: Body) -> Self { MutableBody { @@ -147,6 +151,19 @@ impl MutableBody { result } + /// Add a new assignment to an existing place. + pub fn assign_to( + &mut self, + place: Place, + rvalue: Rvalue, + source: &mut SourceInstruction, + position: InsertPosition, + ) { + let span = source.span(&self.blocks); + let stmt = Statement { kind: StatementKind::Assign(place, rvalue), span }; + self.insert_stmt(stmt, source, position); + } + /// Add a new assert to the basic block indicated by the given index. /// /// The new assertion will have the same span as the source instruction, and the basic block @@ -402,12 +419,21 @@ impl MutableBody { /// by the compiler. This function allow us to delete the dummy body before /// creating a new one. /// - /// Note: We do not prune the local variables today for simplicity. - pub fn clear_body(&mut self) { + /// Keep all the locals untouched, so they can be reused by the passes if needed. + pub fn clear_body(&mut self, kind: TerminatorKind) { self.blocks.clear(); - let terminator = Terminator { kind: TerminatorKind::Return, span: self.span }; + let terminator = Terminator { kind, span: self.span }; self.blocks.push(BasicBlock { statements: Vec::default(), terminator }) } + + /// Replace a terminator from the given basic block + pub fn replace_terminator( + &mut self, + source_instruction: &SourceInstruction, + new_term: Terminator, + ) { + self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term; + } } #[derive(Clone, Debug)] @@ -469,6 +495,12 @@ impl SourceInstruction { SourceInstruction::Terminator { bb } => blocks[bb].terminator.span, } } + + pub fn bb(&self) -> BasicBlockIdx { + match *self { + SourceInstruction::Statement { bb, .. } | SourceInstruction::Terminator { bb } => bb, + } + } } fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 3a835c7f3cb6..71e06f5c49cd 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -3,16 +3,21 @@ //! This module contains code related to the MIR-to-MIR pass to enable contracts. use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; -use crate::kani_middle::transform::body::MutableBody; +use crate::kani_middle::find_fn_def; +use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; +use rustc_hir::def_id::DefId as InternalDefId; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; +use rustc_span::Symbol; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind}; -use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind, TypeAndMut}; -use stable_mir::{CrateDef, DefId}; +use stable_mir::mir::{ + Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents, +}; +use stable_mir::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy}; +use stable_mir::CrateDef; use std::collections::HashSet; use std::fmt::Debug; use tracing::{debug, trace}; @@ -34,7 +39,6 @@ pub struct AnyModifiesPass { kani_write_any_slim: Option, kani_write_any_slice: Option, kani_write_any_str: Option, - stubbed: HashSet, target_fn: Option, } @@ -50,7 +54,7 @@ impl TransformPass for AnyModifiesPass { where Self: Sized, { - // TODO: Check if this is the harness has proof_for_contract + // TODO: Check if the harness has proof_for_contract query_db.args().unstable_features.contains(&"function-contracts".to_string()) && self.kani_any.is_some() } @@ -62,8 +66,8 @@ impl TransformPass for AnyModifiesPass { if instance.def.def_id() == self.kani_any.unwrap().def_id() { // Ensure kani::any is valid. self.any_body(tcx, body) - } else if self.should_apply(tcx, instance) { - // Replace any modifies occurrences. + } else if instance.ty().kind().is_closure() { + // Replace any modifies occurrences. They should only happen in the contract closures. self.replace_any_modifies(body) } else { (false, body) @@ -74,38 +78,19 @@ impl TransformPass for AnyModifiesPass { impl AnyModifiesPass { /// Build the pass with non-extern function stubs. pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> AnyModifiesPass { - let item_fn_def = |item| { - let TyKind::RigidTy(RigidTy::FnDef(def, _)) = - rustc_internal::stable(tcx.type_of(item)).value.kind() - else { - unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item)) - }; - def - }; - let kani_any = - tcx.get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny")).map(item_fn_def); - 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 kani_any = find_fn_def(tcx, "KaniAny"); + let kani_any_modifies = find_fn_def(tcx, "KaniAnyModifies"); + let kani_write_any = find_fn_def(tcx, "KaniWriteAny"); + let kani_write_any_slim = find_fn_def(tcx, "KaniWriteAnySlim"); + let kani_write_any_slice = find_fn_def(tcx, "KaniWriteAnySlice"); + let kani_write_any_str = find_fn_def(tcx, "KaniWriteAnyStr"); + let target_fn = if let Some(harness) = unit.harnesses.first() { let attributes = KaniAttributes::for_instance(tcx, *harness); let target_fn = attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern()); - (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::>()) + target_fn } else { - (None, HashSet::new()) + None }; AnyModifiesPass { kani_any, @@ -115,27 +100,17 @@ impl AnyModifiesPass { kani_write_any_slice, kani_write_any_str, target_fn, - stubbed, } } - /// If we apply `transform_any_modifies` in all contract-generated items, - /// we will end up instantiating `kani::any_modifies` for the replace function - /// every time, even if we are only checking the contract, because the function - /// is always included during contract instrumentation. Thus, we must only apply - /// the transformation if we are using a verified stub or in the presence of recursion. - fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool { - let item_attributes = - KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id())); - self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion() - } - /// Replace calls to `any_modifies` by calls to `any`. fn replace_any_modifies(&self, mut body: Body) -> (bool, Body) { let mut changed = false; let locals = body.locals().to_vec(); for bb in body.blocks.iter_mut() { - let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else { continue }; + 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 @@ -199,7 +174,9 @@ impl AnyModifiesPass { let mut valid = true; 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, .. } = &mut bb.terminator.kind else { + continue; + }; if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = func.ty(&locals).unwrap().kind() { match Instance::resolve(def, &args) { Ok(_) => {} @@ -232,8 +209,306 @@ impl AnyModifiesPass { (true, body) } else { let mut new_body = MutableBody::from(body); - new_body.clear_body(); - (false, new_body.into()) + new_body.clear_body(TerminatorKind::Unreachable); + (true, new_body.into()) } } } + +/// This pass will transform functions annotated with contracts based on the harness configuration. +/// +/// Functions with contract will always follow the same structure: +/// +/// ```ignore +/// #[kanitool::recursion_check = "__kani_recursion_check_modify"] +/// #[kanitool::checked_with = "__kani_check_modify"] +/// #[kanitool::replaced_with = "__kani_replace_modify"] +/// #[kanitool::modifies_wrapper = "__kani_modifies_modify"] +/// fn name_fn(ptr: &mut u32) { +/// #[kanitool::fn_marker = "kani_register_contract"] +/// pub const fn kani_register_contract T>(f: F) -> T { +/// kani::panic("internal error: entered unreachable code: ") +/// } +/// let kani_contract_mode = kani::internal::mode(); +/// match kani_contract_mode { +/// kani::internal::RECURSION_CHECK => { +/// #[kanitool::is_contract_generated(recursion_check)] +/// let mut __kani_recursion_check_name_fn = || { /* recursion check body */ }; +/// kani_register_contract(__kani_recursion_check_modify) +/// } +/// kani::internal::REPLACE => { +/// #[kanitool::is_contract_generated(replace)] +/// let mut __kani_replace_name_fn = || { /* replace body */ }; +/// kani_register_contract(__kani_replace_name_fn) +/// } +/// kani::internal::SIMPLE_CHECK => { +/// #[kanitool::is_contract_generated(check)] +/// let mut __kani_check_name_fn = || { /* check body */ }; +/// kani_register_contract(__kani_check_name_fn) +/// } +/// _ => { /* original body */ } +/// } +/// } +/// ``` +/// +/// This pass will perform the following operations: +/// 1. For functions with contract that are not being used for check or replacement: +/// - Set `kani_contract_mode` to the value ORIGINAL. +/// - Replace the generated closures body with unreachable. +/// 2. For functions with contract that are being used: +/// - Set `kani_contract_mode` to the value corresponding to the expected usage. +/// - Replace the non-used generated closures body with unreachable. +/// 3. Replace the body of `kani_register_contract` by `kani::internal::run_contract_fn` to +/// invoke the closure. +#[derive(Debug, Default)] +pub struct FunctionWithContractPass { + /// Function that is being checked, if any. + check_fn: Option, + /// Functions that should be stubbed by their contract. + replace_fns: HashSet, + /// Functions annotated with contract attributes will contain contract closures even if they + /// are not to be used in this harness. + /// In order to avoid bringing unnecessary logic, we clear their body. + unused_closures: HashSet, + /// Cache KaniRunContract function used to implement contracts. + run_contract_fn: Option, +} + +impl TransformPass for FunctionWithContractPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, _query_db: &QueryDb) -> bool + where + Self: Sized, + { + true + } + + /// Transform the function body by replacing it with the stub body. + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "FunctionWithContractPass::transform"); + match instance.ty().kind().rigid().unwrap() { + RigidTy::FnDef(def, args) => { + if let Some(mode) = self.contract_mode(tcx, *def) { + self.mark_unused(tcx, *def, &body, mode); + let new_body = self.set_mode(tcx, body, mode); + (true, new_body) + } else if KaniAttributes::for_instance(tcx, instance).fn_marker() + == Some(Symbol::intern("kani_register_contract")) + { + let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); + (true, run.body().unwrap()) + } else { + // Not a contract annotated function + (false, body) + } + } + RigidTy::Closure(def, _args) => { + if self.unused_closures.contains(def) { + // Delete body and mark it as unreachable. + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Unreachable); + (true, new_body.into()) + } else { + // Not a contract annotated function + (false, body) + } + } + _ => { + /* static variables case */ + (false, body) + } + } + } +} + +impl FunctionWithContractPass { + /// Build the pass by collecting which functions we are stubbing and which ones we are + /// verifying. + pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> FunctionWithContractPass { + if let Some(harness) = unit.harnesses.first() { + let attrs = KaniAttributes::for_instance(tcx, *harness); + let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); + let replace_fns: HashSet<_> = attrs + .interpret_stub_verified_attribute() + .iter() + .map(|(_, def_id, _)| *def_id) + .collect(); + let run_contract_fn = find_fn_def(tcx, "KaniRunContract"); + assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); + FunctionWithContractPass { + check_fn, + replace_fns, + unused_closures: Default::default(), + run_contract_fn, + } + } else { + // If reachability mode is PubFns or Tests, we just remove any contract logic. + // Note that in this path there is no proof harness. + FunctionWithContractPass::default() + } + } + + /// Functions with contract have the following structure: + /// ```ignore + /// fn original([self], args*) { + /// let kani_contract_mode = kani::internal::mode(); // ** Replace this call + /// match kani_contract_mode { + /// kani::internal::RECURSION_CHECK => { + /// let closure = |/*args*/|{ /*body*/}; + /// kani_register_contract(closure) // ** Replace this call + /// } + /// kani::internal::REPLACE => { + /// // same as above + /// } + /// kani::internal::SIMPLE_CHECK => { + /// // same as above + /// } + /// _ => { /* original code */} + /// } + /// } + /// ``` + /// See function `handle_untouched` inside `kani_macros`. + /// + /// Thus, we need to: + /// 1. Initialize `kani_contract_mode` variable to the value corresponding to the mode. + /// + /// Thus replace this call: + /// ```ignore + /// let kani_contract_mode = kani::internal::mode(); // ** Replace this call + /// ``` + /// by: + /// ```ignore + /// let kani_contract_mode = mode_const; + /// goto bbX; + /// ``` + /// 2. Replace `kani_register_contract` by the call to the closure. + fn set_mode(&self, tcx: TyCtxt, body: Body, mode: ContractMode) -> Body { + debug!(?mode, "set_mode"); + let mut new_body = MutableBody::from(body); + let (mut mode_call, ret, target) = new_body + .blocks() + .iter() + .enumerate() + .find_map(|(bb_idx, bb)| { + if let TerminatorKind::Call { func, target, destination, .. } = &bb.terminator.kind + { + let (callee, _) = func.ty(new_body.locals()).unwrap().kind().fn_def()?; + let marker = KaniAttributes::for_def_id(tcx, callee.def_id()).fn_marker(); + if marker.is_some_and(|s| s.as_str() == "kani_contract_mode") { + return Some(( + SourceInstruction::Terminator { bb: bb_idx }, + destination.clone(), + target.unwrap(), + )); + } + } + None + }) + .unwrap(); + + let span = mode_call.span(new_body.blocks()); + let mode_const = new_body.new_uint_operand(mode as _, UintTy::U8, span); + new_body.assign_to( + ret.clone(), + Rvalue::Use(mode_const), + &mut mode_call, + InsertPosition::Before, + ); + new_body.replace_terminator( + &mode_call, + Terminator { kind: TerminatorKind::Goto { target }, span }, + ); + + new_body.into() + } + + /// Return which contract mode to use for this function if any. + fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option { + let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id()); + kani_attributes.has_contract().then(|| { + let fn_def_id = rustc_internal::internal(tcx, fn_def.def_id()); + if self.check_fn == Some(fn_def_id) { + if kani_attributes.has_recursion() { + ContractMode::RecursiveCheck + } else { + ContractMode::SimpleCheck + } + } else if self.replace_fns.contains(&fn_def_id) { + ContractMode::Replace + } else { + ContractMode::Original + } + }) + } + + /// Select any unused closure for body deletion. + fn mark_unused(&mut self, tcx: TyCtxt, fn_def: FnDef, body: &Body, mode: ContractMode) { + let contract = + KaniAttributes::for_def_id(tcx, fn_def.def_id()).contract_attributes().unwrap(); + let recursion_closure = find_closure(tcx, fn_def, &body, contract.recursion_check.as_str()); + let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str()); + let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str()); + match mode { + ContractMode::Original => { + // No contract instrumentation needed. Add all closures to the list of unused. + self.unused_closures.insert(recursion_closure); + self.unused_closures.insert(check_closure); + self.unused_closures.insert(replace_closure); + } + ContractMode::RecursiveCheck => { + self.unused_closures.insert(replace_closure); + self.unused_closures.insert(check_closure); + } + ContractMode::SimpleCheck => { + self.unused_closures.insert(replace_closure); + self.unused_closures.insert(recursion_closure); + } + ContractMode::Replace => { + self.unused_closures.insert(recursion_closure); + self.unused_closures.insert(check_closure); + } + } + } +} + +/// Enumeration that store the value of which implementation should be selected. +/// +/// Keep the discriminant values in sync with [kani::internal::mode]. +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +enum ContractMode { + Original = 0, + RecursiveCheck = 1, + SimpleCheck = 2, + Replace = 3, +} + +fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef { + body.var_debug_info + .iter() + .find_map(|var_info| { + if var_info.name.as_str() == name { + let ty = match &var_info.value { + VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), + VarDebugInfoContents::Const(const_op) => const_op.ty(), + }; + if let TyKind::RigidTy(RigidTy::Closure(def, _args)) = ty.kind() { + return Some(def); + } + } + None + }) + .unwrap_or_else(|| { + tcx.sess.dcx().err(format!( + "Failed to find contract closure `{name}` in function `{}`", + fn_def.name() + )); + tcx.sess.dcx().abort_if_errors(); + unreachable!() + }) +} diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index d6475465d1b1..82ff25bb2442 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -19,7 +19,8 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, + BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, + RETURN_LOCAL, }; use stable_mir::target::MachineInfo; use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy}; @@ -86,7 +87,7 @@ impl IntrinsicGeneratorPass { /// ``` fn valid_value_body(&self, tcx: TyCtxt, body: Body) -> Body { let mut new_body = MutableBody::from(body); - new_body.clear_body(); + new_body.clear_body(TerminatorKind::Return); // Initialize return variable with True. let ret_var = RETURN_LOCAL; @@ -163,7 +164,7 @@ impl IntrinsicGeneratorPass { /// ``` fn is_initialized_body(&mut self, tcx: TyCtxt, body: Body) -> Body { let mut new_body = MutableBody::from(body); - new_body.clear_body(); + new_body.clear_body(TerminatorKind::Return); // Initialize return variable with True. let ret_var = RETURN_LOCAL; diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 5b497b09619d..4f3125e59868 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -21,7 +21,7 @@ use crate::kani_middle::reachability::CallGraph; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_uninit::UninitPass; use crate::kani_middle::transform::check_values::ValidValuePass; -use crate::kani_middle::transform::contracts::AnyModifiesPass; +use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass}; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; @@ -66,7 +66,9 @@ impl BodyTransformation { let check_type = CheckType::new_assert_assume(tcx); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); - // This has to come after stubs since we want this to replace the stubbed body. + transformer.add_pass(queries, FunctionWithContractPass::new(tcx, &unit)); + // This has to come after the contract pass since we want this to only replace the closure + // body that is relevant for this harness. transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index ae76be150871..d31d4dae90f6 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -167,18 +167,20 @@ impl KaniSession { pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { let Some(assigns) = harness.contract.as_ref() else { return Ok(()) }; - let args: &[std::ffi::OsString] = &[ + let mut args: Vec = vec![ "--dfcc".into(), (&harness.mangled_name).into(), "--enforce-contract".into(), assigns.contracted_function_name.as_str().into(), - "--nondet-static-exclude".into(), - assigns.recursion_tracker.as_str().into(), "--no-malloc-may-fail".into(), file.into(), file.into(), ]; - self.call_goto_instrument(args) + if let Some(tracker) = &assigns.recursion_tracker { + args.push("--nondet-static-exclude".into()); + args.push(tracker.as_str().into()); + } + self.call_goto_instrument(&args) } /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 41eb4eb20919..426cf8d9e960 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -11,7 +11,8 @@ pub struct AssignsContract { /// The target of the contract pub contracted_function_name: String, /// A static global variable used to track recursion that must not be havocked. - pub recursion_tracker: String, + /// This is only needed if the function is tagged with `#[kani::recursive]` + pub recursion_tracker: Option, } /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find. @@ -50,6 +51,8 @@ pub struct HarnessAttributes { pub unwind_value: Option, /// The stubs used in this harness. pub stubs: Vec, + /// The name of the functions being stubbed by their contract. + pub verified_stubs: Vec, } #[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)] @@ -71,6 +74,7 @@ impl HarnessAttributes { solver: None, unwind_value: None, stubs: vec![], + verified_stubs: vec![], } } diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 22026065106a..68b15316b4c1 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -8,60 +8,39 @@ use std::ptr; /// /// We allow the user to provide us with a pointer-like object that we convert as needed. #[doc(hidden)] -pub trait Pointer<'a> { +pub trait Pointer { /// Type of the pointed-to data 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) -> *mut Self::Inner; } -impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { +impl Pointer for &T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - std::mem::transmute(*self) - } - unsafe fn assignable(self) -> *mut Self::Inner { - std::mem::transmute(self as *const T) + self as *const T as *mut T } } -impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { +impl Pointer for &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) -> *mut Self::Inner { self as *mut T } } -impl<'a, T: ?Sized> Pointer<'a> for *const T { +impl Pointer for *const T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } unsafe fn assignable(self) -> *mut Self::Inner { - std::mem::transmute(self) + self as *mut T } } -impl<'a, T: ?Sized> Pointer<'a> for *mut T { +impl Pointer for *mut T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } - unsafe fn assignable(self) -> *mut Self::Inner { self } @@ -69,6 +48,8 @@ impl<'a, T: ?Sized> Pointer<'a> for *mut T { /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. +/// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if +/// they really need to. See . #[inline(never)] #[doc(hidden)] #[rustc_diagnostic_item = "KaniUntrackedDeref"] @@ -92,6 +73,8 @@ pub fn init_contracts() {} /// This should only be used within contracts. The intent is to /// perform type inference on a closure's argument +/// TODO: This should be generated inside the function that has contract. This is used for +/// remembers. #[doc(hidden)] pub fn apply_closure bool>(f: U, x: &T) -> bool { f(x) @@ -142,3 +125,36 @@ pub unsafe fn write_any_str(_s: *mut str) { //TODO: String validation unimplemented!("Kani does not support creating arbitrary `str`") } + +/// Function that calls a closure used to implement contracts. +/// +/// In contracts, we cannot invoke the generated closures directly, instead, we call register +/// contract. This function is a no-op. However, in the reality, we do want to call the closure, +/// so we swap the register body by this function body. +#[doc(hidden)] +#[allow(dead_code)] +#[rustc_diagnostic_item = "KaniRunContract"] +#[crate::unstable( + feature = "function-contracts", + issue = "none", + reason = "internal function required to run contract closure" +)] +fn run_contract_fn T>(func: F) -> T { + func() +} + +/// This is used by contracts to select which version of the contract to use during codegen. +#[doc(hidden)] +pub type Mode = u8; + +/// Keep the original body. +pub const ORIGINAL: Mode = 0; + +/// Run the check with recursion support. +pub const RECURSION_CHECK: Mode = 1; + +/// Run the simple check with no recursion support. +pub const SIMPLE_CHECK: Mode = 2; + +/// Stub the body with its contract. +pub const REPLACE: Mode = 3; diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 9baba1abe886..b7263816800a 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -306,60 +306,39 @@ macro_rules! kani_intrinsics { /// /// We allow the user to provide us with a pointer-like object that we convert as needed. #[doc(hidden)] - pub trait Pointer<'a> { + pub trait Pointer { /// Type of the pointed-to data 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) -> *mut Self::Inner; } - impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { + impl Pointer for &T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - core::mem::transmute(*self) - } - unsafe fn assignable(self) -> *mut Self::Inner { - core::mem::transmute(self as *const T) + self as *const T as *mut T } } - impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { + impl Pointer for &mut T { type Inner = T; - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - core::mem::transmute::<_, &&'a T>(self) - } - unsafe fn assignable(self) -> *mut Self::Inner { self as *mut T } } - impl<'a, T: ?Sized> Pointer<'a> for *const T { + impl Pointer for *const T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } unsafe fn assignable(self) -> *mut Self::Inner { - core::mem::transmute(self) + self as *mut T } } - impl<'a, T: ?Sized> Pointer<'a> for *mut T { + impl Pointer for *mut T { type Inner = T; - unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - &**self as &'a T - } - unsafe fn assignable(self) -> *mut Self::Inner { self } @@ -436,6 +415,34 @@ macro_rules! kani_intrinsics { //TODO: String validation unimplemented!("Kani does not support creating arbitrary `str`") } + + /// Function that calls a closure used to implement contracts. + /// + /// In contracts, we cannot invoke the generated closures directly, instead, we call register + /// contract. This function is a no-op. However, in the reality, we do want to call the closure, + /// so we swap the register body by this function body. + #[doc(hidden)] + #[allow(dead_code)] + #[rustc_diagnostic_item = "KaniRunContract"] + fn run_contract_fn T>(func: F) -> T { + func() + } + + /// This is used by contracts to select which version of the contract to use during codegen. + #[doc(hidden)] + pub type Mode = u8; + + /// Keep the original body. + pub const ORIGINAL: Mode = 0; + + /// Run the check with recursion support. + pub const RECURSION_CHECK: Mode = 1; + + /// Run the simple check with no recursion support. + pub const SIMPLE_CHECK: Mode = 2; + + /// Stub the body with its contract. + pub const REPLACE: Mode = 3; } }; } diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index dee0bca42c54..8ad21e8a9c6b 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -4,106 +4,152 @@ //! Special way we handle the first time we encounter a contract attribute on a //! function. -use proc_macro2::{Ident, Span}; +use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; -use syn::ItemFn; +use syn::{Expr, ItemFn, Stmt}; -use super::{ - helpers::*, shared::identifier_for_generated_function, ContractConditionsHandler, - INTERNAL_RESULT_IDENT, -}; +use super::{helpers::*, ContractConditionsHandler, INTERNAL_RESULT_IDENT}; impl<'a> ContractConditionsHandler<'a> { - /// The complex case. We are the first time a contract is handled on this function, so - /// we're responsible for + /// Generate initial contract. /// - /// 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 + /// 1. Generating the body for the recursion closure used by contracts. + /// - The recursion closure body will contain the check and replace closure. pub fn handle_untouched(&mut self) { - // We'll be using this to postfix the generated names for the "check" - // and "replace" functions. - let item_hash = self.hash.unwrap(); - - let original_function_name = self.annotated_fn.sig.ident.clone(); - - let check_fn_name = - identifier_for_generated_function(&original_function_name, "check", item_hash); - let replace_fn_name = - identifier_for_generated_function(&original_function_name, "replace", item_hash); - let recursion_wrapper_name = identifier_for_generated_function( - &original_function_name, - "recursion_wrapper", - item_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 replace_fn_name_str = syn::LitStr::new(&replace_fn_name.to_string(), Span::call_site()); - let wrapper_fn_name_str = - syn::LitStr::new(&self.make_wrapper_name().to_string(), Span::call_site()); - let recursion_wrapper_name_str = - syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site()); + let replace_name = &self.replace_name; + let modifies_name = &self.modify_name; + let recursion_name = &self.recursion_name; + let check_name = &self.check_name; + + let replace_closure = self.replace_closure(); + let check_closure = self.check_closure(); + let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure); + + let span = Span::call_site(); + let replace_ident = Ident::new(&self.replace_name, span); + let check_ident = Ident::new(&self.check_name, span); + let recursion_ident = Ident::new(&self.recursion_name, span); // 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 attributes and can use them to determine // `function_state`. - // - // The same care is taken when we emit check and replace functions. - // emit the check function. - let is_impl_fn = is_probably_impl_fn(&self.annotated_fn); let ItemFn { attrs, vis, sig, block } = &self.annotated_fn; self.output.extend(quote!( #(#attrs)* - #[kanitool::checked_with = #recursion_wrapper_name_str] - #[kanitool::replaced_with = #replace_fn_name_str] - #[kanitool::inner_check = #wrapper_fn_name_str] + #[kanitool::recursion_check = #recursion_name] + #[kanitool::checked_with = #check_name] + #[kanitool::replaced_with = #replace_name] + #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { - #block + // Dummy function used to force the compiler to capture the environment. + // We cannot call closures inside constant functions. + // This function gets replaced by `kani::internal::call_closure`. + #[inline(never)] + #[kanitool::fn_marker = "kani_register_contract"] + const fn kani_register_contract T>(f: F) -> T { + unreachable!() + } + // Dummy function that we replace to pick the contract mode. + // By default, return ORIGINAL + #[inline(never)] + #[kanitool::fn_marker = "kani_contract_mode"] + const fn kani_contract_mode() -> kani::internal::Mode { + kani::internal::ORIGINAL + } + let kani_contract_mode = kani_contract_mode(); + match kani_contract_mode { + kani::internal::RECURSION_CHECK => { + #recursion_closure; + kani_register_contract(#recursion_ident) + } + kani::internal::REPLACE => { + #replace_closure; + kani_register_contract(#replace_ident) + } + kani::internal::SIMPLE_CHECK => { + #check_closure; + kani_register_contract(#check_ident) + } + _ => #block + } } )); + } + + /// Handle subsequent contract attributes. + /// + /// Find the closures added by the initial setup, parse them and expand their body according + /// to the attribute being handled. + pub fn handle_expanded(&mut self) { + let mut annotated_fn = self.annotated_fn.clone(); + let ItemFn { block, .. } = &mut annotated_fn; + let recursion_closure = expect_closure_in_match(&mut block.stmts, "recursion_check"); + self.expand_recursion(recursion_closure); - let mut wrapper_sig = sig.clone(); - wrapper_sig.ident = recursion_wrapper_name; - // We use non-constant functions, thus, the wrapper cannot be constant. - wrapper_sig.constness = None; + let replace_closure = expect_closure_in_match(&mut block.stmts, "replace"); + self.expand_replace(replace_closure); - let args = pats_to_idents(&mut wrapper_sig.inputs).collect::>(); - let also_args = args.iter(); - let (call_check, call_replace) = if is_impl_fn { - (quote!(Self::#check_fn_name), quote!(Self::#replace_fn_name)) - } else { - (quote!(#check_fn_name), quote!(#replace_fn_name)) - }; + let check_closure = expect_closure_in_match(&mut block.stmts, "check"); + self.expand_check(check_closure); - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - self.output.extend(quote!( + self.output.extend(quote!(#annotated_fn)); + } + + /// Generate the tokens for the recursion closure. + fn new_recursion_closure( + &self, + replace_closure: &TokenStream, + check_closure: &TokenStream, + ) -> TokenStream { + let ItemFn { ref sig, .. } = self.annotated_fn; + let output = &sig.output; + let span = Span::call_site(); + let result = Ident::new(INTERNAL_RESULT_IDENT, span); + let replace_ident = Ident::new(&self.replace_name, span); + let check_ident = Ident::new(&self.check_name, span); + let recursion_ident = Ident::new(&self.recursion_name, span); + + quote!( + #[kanitool::is_contract_generated(recursion_check)] #[allow(dead_code, unused_variables, unused_mut)] - #[kanitool::is_contract_generated(recursion_wrapper)] - #wrapper_sig { + let mut #recursion_ident = || #output + { + #[kanitool::recursion_tracker] static mut REENTRY: bool = false; if unsafe { REENTRY } { - #call_replace(#(#args),*) + #replace_closure + #replace_ident() } else { unsafe { REENTRY = true }; - let #result = #call_check(#(#also_args),*); + #check_closure + let #result = #check_ident(); unsafe { REENTRY = false }; #result } - } - )); + }; + ) + } + + /// Expand an existing recursion closure with the new condition. + fn expand_recursion(&self, closure: &mut Stmt) { + // TODO: Need to enter if / else. Make this traverse body and return list statements :( + let body = closure_body(closure); + let stmts = &mut body.block.stmts; + let if_reentry = stmts + .iter_mut() + .find_map(|stmt| { + if let Stmt::Expr(Expr::If(if_expr), ..) = stmt { Some(if_expr) } else { None } + }) + .unwrap(); + + let replace_closure = expect_closure(&mut if_reentry.then_branch.stmts, "replace"); + self.expand_replace(replace_closure); - self.emit_check_function(Some(check_fn_name)); - self.emit_replace_function(Some(replace_fn_name)); - self.emit_augmented_modifies_wrapper(); + let else_branch = if_reentry.else_branch.as_mut().unwrap(); + let Expr::Block(else_block) = else_branch.1.as_mut() else { unreachable!() }; + let check_closure = expect_closure(&mut else_block.block.stmts, "check"); + self.expand_check(check_closure); } } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index f804fc70c5f5..69f280ad9335 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -5,33 +5,28 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; -use syn::{Expr, FnArg, ItemFn, Token}; +use std::mem; +use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; use super::{ - helpers::*, - shared::{build_ensures, try_as_result_assign_mut}, - ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + helpers::*, shared::build_ensures, ContractConditionsData, ContractConditionsHandler, + INTERNAL_RESULT_IDENT, }; -const WRAPPER_ARG_PREFIX: &str = "_wrapper_arg_"; +const WRAPPER_ARG: &str = "_wrapper_arg"; impl<'a> ContractConditionsHandler<'a> { /// Create the body of a check function. /// /// Wraps the conditions from this attribute around `self.body`. - /// - /// Mutable because a `modifies` clause may need to extend the inner call to - /// the wrapper with new arguments. - pub fn make_check_body(&mut self) -> TokenStream2 { - let mut inner = self.ensure_bootstrapped_check_body(); + pub fn make_check_body(&self, mut body_stmts: Vec) -> TokenStream2 { let Self { attr_copy, .. } = self; - match &self.condition_type { ContractConditionsData::Requires { attr } => { - quote!( + quote!({ kani::assume(#attr); - #(#inner)* - ) + #(#body_stmts)* + }) } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); @@ -42,257 +37,157 @@ impl<'a> ContractConditionsHandler<'a> { kani::assert(#ensures_clause, stringify!(#attr_copy)); ); - assert!(matches!( - inner.pop(), - Some(syn::Stmt::Expr(syn::Expr::Path(pexpr), None)) - if pexpr.path.get_ident().map_or(false, |id| id == INTERNAL_RESULT_IDENT) - )); - - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + let return_expr = body_stmts.pop(); + quote!({ #remembers - #(#inner)* + #(#body_stmts)* #exec_postconditions - #result - ) + #return_expr + }) } ContractConditionsData::Modifies { attr } => { - let wrapper_name = self.make_wrapper_name().to_string(); - - let wrapper_args = if let Some(wrapper_call_args) = - inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) - { - let wrapper_args = make_wrapper_idents( - wrapper_call_args.len(), - attr.len(), - WRAPPER_ARG_PREFIX, - ); - wrapper_call_args - .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a)))); - wrapper_args + let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); + let wrapper_tuple = body_stmts.iter_mut().find_map(|stmt| { + if let Stmt::Local(Local { + pat: Pat::Ident(PatIdent { ident, .. }), + init: Some(LocalInit { expr, .. }), + .. + }) = stmt + { + (ident == &wrapper_arg_ident).then_some(expr.as_mut()) + } else { + None + } + }); + if let Some(Expr::Tuple(values)) = wrapper_tuple { + values.elems.extend(attr.iter().map(|attr| { + let expr: Expr = parse_quote!(#attr + as *const _); + expr + })); } else { - unreachable!( - "Invariant broken, check function did not contain a call to the wrapper function" - ) - }; - - quote!( - #(let #wrapper_args = unsafe { kani::internal::Pointer::decouple_lifetime(&#attr) };)* - #(#inner)* - ) + unreachable!("Expected tuple but found `{wrapper_tuple:?}`") + } + quote!({#(#body_stmts)*}) } } } - /// Get the sequence of statements of the previous check body or create the default one. - fn ensure_bootstrapped_check_body(&self) -> Vec { - let wrapper_name = self.make_wrapper_name(); + /// Initialize the list of statements for the check closure body. + fn initial_check_stmts(&self) -> Vec { + let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); + let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site()); let return_type = return_type_to_type(&self.annotated_fn.sig.output); - if self.is_first_emit() { - let args = exprs_for_args(&self.annotated_fn.sig.inputs); - let wrapper_call = if is_probably_impl_fn(self.annotated_fn) { - quote!(Self::#wrapper_name) - } else { - quote!(#wrapper_name) - }; - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - syn::parse_quote!( - let #result : #return_type = #wrapper_call(#(#args),*); - #result - ) - } else { - self.annotated_fn.block.stmts.clone() - } + let mut_recv = self.has_mutable_receiver().then(|| quote!(core::ptr::addr_of!(self),)); + let redefs = self.arg_redefinitions(); + let modifies_closure = + self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs); + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + parse_quote!( + let #wrapper_arg_ident = (#mut_recv); + #modifies_closure + let #result : #return_type = #modifies_ident(#wrapper_arg_ident); + #result + ) } - /// Emit the check function into the output stream. + /// Generate a token stream that represents the check closure. /// /// See [`Self::make_check_body`] for the most interesting parts of this /// function. - pub fn emit_check_function(&mut self, override_function_dent: Option) { - self.emit_common_header(); - - if self.function_state.emit_tag_attr() { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - self.output.extend(quote!(#[kanitool::is_contract_generated(check)])); - } - let body = self.make_check_body(); - let mut sig = self.annotated_fn.sig.clone(); - // We use non-constant functions, thus, the wrapper cannot be constant. - sig.constness = None; - if let Some(ident) = override_function_dent { - sig.ident = ident; - } - self.output.extend(quote!( - #sig { - #body - } - )) + pub fn check_closure(&self) -> TokenStream2 { + let check_ident = Ident::new(&self.check_name, Span::call_site()); + let sig = &self.annotated_fn.sig; + let output = &sig.output; + let body_stmts = self.initial_check_stmts(); + let body = self.make_check_body(body_stmts); + + quote!( + #[kanitool::is_contract_generated(check)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut #check_ident = || #output #body; + ) } - /// Emit a modifies wrapper, possibly augmenting a prior, existing one. + /// Expand the check body. /// - /// We only augment if this clause is a `modifies` clause. Before, - /// we annotated the wrapper arguments with `impl kani::Arbitrary`, - /// so Rust would infer the proper types for each argument. - /// We want to remove the restriction that these arguments must - /// implement `kani::Arbitrary` for checking. Now, we annotate each - /// argument with a generic type parameter, so the compiler can - /// continue inferring the correct types. - pub fn emit_augmented_modifies_wrapper(&mut self) { - if let ContractConditionsData::Modifies { attr } = &self.condition_type { - let wrapper_args = make_wrapper_idents( - self.annotated_fn.sig.inputs.len(), - attr.len(), - WRAPPER_ARG_PREFIX, - ); - // Generate a unique type parameter identifier - let type_params = make_wrapper_idents( - self.annotated_fn.sig.inputs.len(), - attr.len(), - "WrapperArgType", - ); - 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: Some(Token![:](Span::call_site())), - bounds: bounds, - eq_token: None, - default: None, - })); - let lifetime = syn::Lifetime { apostrophe: Span::call_site(), ident: arg.clone() }; - sig.inputs.push(FnArg::Typed(syn::PatType { - attrs: vec![], - colon_token: Token![:](Span::call_site()), - pat: Box::new(syn::Pat::Verbatim(quote!(#arg))), - ty: Box::new(syn::parse_quote! { &#arg_type }), - })); - sig.generics.params.push(syn::GenericParam::Lifetime(syn::LifetimeParam { - lifetime, - colon_token: None, - bounds: Default::default(), - attrs: vec![], - })); - } - - self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)])) - } - self.emit_common_header(); - - if self.function_state.emit_tag_attr() { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - self.output.extend(quote!(#[kanitool::is_contract_generated(wrapper)])); - } - - let name = self.make_wrapper_name(); - let ItemFn { vis, sig, block, .. } = self.annotated_fn; - - let mut sig = sig.clone(); - sig.ident = name; - self.output.extend(quote!( - #vis #sig #block + /// First find the modifies body and expand that. Then expand the rest of the body. + pub fn expand_check(&self, closure: &mut Stmt) { + let body = closure_body(closure); + self.expand_modifies(find_contract_closure(&mut body.block.stmts, "wrapper").expect( + &format!("Internal Failure: Expected to find `wrapper` closure, but found none"), )); + *body = syn::parse2(self.make_check_body(mem::take(&mut body.block.stmts))).unwrap(); } -} - -/// Try to interpret this statement as `let result : <...> = (args ...);` and -/// return a mutable reference to the parameter list. -fn try_as_wrapper_call_args<'a>( - stmt: &'a mut syn::Stmt, - wrapper_fn_name: &str, -) -> Option<&'a mut syn::punctuated::Punctuated> { - let syn::LocalInit { diverge: None, expr: init_expr, .. } = try_as_result_assign_mut(stmt)? - else { - return None; - }; - - match init_expr.as_mut() { - Expr::Call(syn::ExprCall { func: box_func, args, .. }) => match box_func.as_ref() { - syn::Expr::Path(syn::ExprPath { qself: None, path, .. }) - if path.get_ident().map_or(false, |id| id == wrapper_fn_name) => - { - Some(args) - } - _ => None, - }, - _ => None, - } -} -/// Make `num` [`Ident`]s with the names `prefix{i}` with `i` starting at `low` and -/// increasing by one each time. -fn make_wrapper_idents( - low: usize, - num: usize, - prefix: &'static str, -) -> impl Iterator + Clone + 'static { - (low..).map(move |i| Ident::new(&format!("{prefix}{i}"), Span::mixed_site())).take(num) -} - -#[cfg(test)] -mod test { - macro_rules! detect_impl_fn { - ($expect_pass:expr, $($tt:tt)*) => {{ - let syntax = stringify!($($tt)*); - let ast = syn::parse_str(syntax).unwrap(); - assert!($expect_pass == super::is_probably_impl_fn(&ast), - "Incorrect detection.\nExpected is_impl_fun: {}\nInput Expr; {}\nParsed: {:?}", - $expect_pass, - syntax, - ast - ); - }} + /// Emit a modifies wrapper. It's only argument is the list of addresses that may be modified. + pub fn modifies_closure( + &self, + output: &ReturnType, + body: &Block, + redefs: TokenStream2, + ) -> TokenStream2 { + // Filter receiver + let wrapper_ident = Ident::new(WRAPPER_ARG, Span::call_site()); + let modifies_ident = Ident::new(&self.modify_name, Span::call_site()); + let stmts = &body.stmts; + quote!( + #[kanitool::is_contract_generated(wrapper)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut #modifies_ident = |#wrapper_ident: _| #output { + #redefs + #(#stmts)* + }; + ) } - #[test] - fn detect_impl_fn_by_receiver() { - detect_impl_fn!(true, fn self_by_ref(&self, u: usize) -> bool {}); - - detect_impl_fn!(true, fn self_by_self(self, u: usize) -> bool {}); + /// Expand the modifies closure if we are handling a modifies attribute. Otherwise, no-op. + pub fn expand_modifies(&self, closure_stmt: &mut Stmt) { + if matches!(&self.condition_type, ContractConditionsData::Modifies { .. }) { + let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure_stmt else { + unreachable!() + }; + let Expr::Closure(closure) = expr.as_ref() else { unreachable!() }; + let Expr::Block(body) = closure.body.as_ref() else { unreachable!() }; + let stream = self.modifies_closure(&closure.output, &body.block, TokenStream2::new()); + *closure_stmt = syn::parse2(stream).unwrap(); + } } - #[test] - fn detect_impl_fn_by_self_ty() { - detect_impl_fn!(true, fn self_by_construct(u: usize) -> Self {}); - detect_impl_fn!(true, fn self_by_wrapped_construct(u: usize) -> Arc {}); - - detect_impl_fn!(true, fn self_by_other_arg(u: usize, slf: Self) {}); - - detect_impl_fn!(true, fn self_by_other_wrapped_arg(u: usize, slf: Vec) {}) + /// Return whether the original function has a mutable receiver. + fn has_mutable_receiver(&self) -> bool { + let first_arg = self.annotated_fn.sig.inputs.first(); + first_arg + .map(|arg| { + matches!( + arg, + FnArg::Receiver(syn::Receiver { mutability: Some(_), reference: None, .. },) + ) + }) + .unwrap_or(false) } - #[test] - fn detect_impl_fn_by_qself() { - detect_impl_fn!( - true, - fn self_by_mention(u: usize) { - Self::other(u) + /// Generate argument re-definitions for mutable arguments. + /// + /// This is used so Kani doesn't think that modifying a local argument value is a side effect. + fn arg_redefinitions(&self) -> TokenStream2 { + let mut result = TokenStream2::new(); + for (mutability, ident) in self.arg_bindings() { + if mutability == MutBinding::Mut { + result.extend(quote!(let mut #ident = #ident;)) + } else { + // This would make some replace some temporary variables from error messages. + //result.extend(quote!(let #ident = #ident; )) } - ); + } + result } - #[test] - fn detect_no_impl_fn() { - detect_impl_fn!( - false, - fn self_by_mention(u: usize) { - let self_name = 18; - let self_lit = "self"; - let self_lit = "Self"; - } - ); + /// Extract all arguments bindings and their mutability. + fn arg_bindings(&self) -> impl Iterator { + self.annotated_fn.sig.inputs.iter().flat_map(|arg| match arg { + FnArg::Receiver(_) => vec![], + FnArg::Typed(typed) => pat_to_bindings(typed.pat.as_ref()), + }) } } diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 174f0f9483d7..410c2d971c44 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -5,9 +5,9 @@ //! specific to Kani and contracts. use proc_macro2::{Ident, Span}; -use quote::{quote, ToTokens}; use std::borrow::Cow; -use syn::{spanned::Spanned, visit::Visit, Expr, FnArg, ItemFn}; +use syn::spanned::Spanned; +use syn::{parse_quote, Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { @@ -20,10 +20,16 @@ pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { } } -/// Create an expression that reconstructs a struct that was matched in a pattern. +#[derive(Copy, Clone, Eq, PartialEq)] +pub enum MutBinding { + Mut, + NotMut, +} + +/// Extract all local bindings from a given pattern. /// -/// Does not support enums, wildcards, pattern alternatives (`|`), range patterns, or verbatim. -pub fn pat_to_expr(pat: &syn::Pat) -> Expr { +/// Does not support range patterns, or verbatim. +pub fn pat_to_bindings(pat: &syn::Pat) -> Vec<(MutBinding, &Ident)> { use syn::Pat; let mk_err = |typ| { pat.span() @@ -33,167 +39,90 @@ pub fn pat_to_expr(pat: &syn::Pat) -> Expr { unreachable!() }; match pat { - Pat::Const(c) => Expr::Const(c.clone()), - Pat::Ident(id) => Expr::Verbatim(id.ident.to_token_stream()), - Pat::Lit(lit) => Expr::Lit(lit.clone()), - Pat::Reference(rf) => Expr::Reference(syn::ExprReference { - attrs: vec![], - and_token: rf.and_token, - mutability: rf.mutability, - expr: Box::new(pat_to_expr(&rf.pat)), - }), - Pat::Tuple(tup) => Expr::Tuple(syn::ExprTuple { - attrs: vec![], - paren_token: tup.paren_token, - elems: tup.elems.iter().map(pat_to_expr).collect(), - }), - Pat::Slice(slice) => Expr::Reference(syn::ExprReference { - attrs: vec![], - and_token: syn::Token!(&)(Span::call_site()), - mutability: None, - expr: Box::new(Expr::Array(syn::ExprArray { - attrs: vec![], - bracket_token: slice.bracket_token, - elems: slice.elems.iter().map(pat_to_expr).collect(), - })), - }), - Pat::Path(pth) => Expr::Path(pth.clone()), - Pat::Or(_) => mk_err("or"), - Pat::Rest(_) => mk_err("rest"), - Pat::Wild(_) => mk_err("wildcard"), - Pat::Paren(inner) => pat_to_expr(&inner.pat), - Pat::Range(_) => mk_err("range"), + Pat::Const(_) => vec![], + Pat::Ident(PatIdent { ident, subpat: Some(subpat), mutability, .. }) => { + let mut idents = pat_to_bindings(subpat.1.as_ref()); + idents.push((mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)); + idents + } + Pat::Ident(PatIdent { ident, mutability, .. }) => { + vec![(mutability.map_or(MutBinding::NotMut, |_| MutBinding::Mut), ident)] + } + Pat::Lit(_) => vec![], + Pat::Reference(_) => vec![], + Pat::Tuple(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(), + Pat::Slice(slice) => slice.elems.iter().flat_map(pat_to_bindings).collect(), + Pat::Path(_) => { + vec![] + } + Pat::Or(pat_or) => { + // Note: Patterns are not accepted in function arguments. + // No matter what, the same bindings must exist in all the patterns. + pat_or.cases.first().map(pat_to_bindings).unwrap_or_default() + } + Pat::Rest(_) => vec![], + Pat::Wild(_) => vec![], + Pat::Paren(inner) => pat_to_bindings(&inner.pat), + Pat::Range(_) => vec![], Pat::Struct(strct) => { - if strct.rest.is_some() { - mk_err(".."); - } - Expr::Struct(syn::ExprStruct { - attrs: vec![], - path: strct.path.clone(), - brace_token: strct.brace_token, - dot2_token: None, - rest: None, - qself: strct.qself.clone(), - fields: strct - .fields - .iter() - .map(|field_pat| syn::FieldValue { - attrs: vec![], - member: field_pat.member.clone(), - colon_token: field_pat.colon_token, - expr: pat_to_expr(&field_pat.pat), - }) - .collect(), - }) + strct.fields.iter().flat_map(|field_pat| pat_to_bindings(&field_pat.pat)).collect() } Pat::Verbatim(_) => mk_err("verbatim"), - Pat::Type(pt) => pat_to_expr(pt.pat.as_ref()), - Pat::TupleStruct(_) => mk_err("tuple struct"), + Pat::Type(pt) => pat_to_bindings(pt.pat.as_ref()), + Pat::TupleStruct(tup) => tup.elems.iter().flat_map(pat_to_bindings).collect(), _ => mk_err("unknown"), } } -/// For each argument create an expression that passes this argument along unmodified. -/// -/// Reconstructs structs that may have been deconstructed with patterns. -pub fn exprs_for_args( - args: &syn::punctuated::Punctuated, -) -> impl Iterator + Clone + '_ { - args.iter().map(|arg| match arg { - FnArg::Receiver(_) => Expr::Verbatim(quote!(self)), - FnArg::Typed(typed) => pat_to_expr(&typed.pat), +/// Find a closure statement attached with `kanitool::is_contract_generated` attribute. +pub fn find_contract_closure<'a>( + stmts: &'a mut [Stmt], + name: &'static str, +) -> Option<&'a mut Stmt> { + stmts.iter_mut().find(|stmt| { + if let Stmt::Local(local) = stmt { + let ident = Ident::new(name, Span::call_site()); + let attr: Attribute = parse_quote!(#[kanitool::is_contract_generated(#ident)]); + local.attrs.contains(&attr) + } else { + false + } }) } -/// The visitor used by [`is_probably_impl_fn`]. See function documentation for -/// more information. -struct SelfDetector(bool); - -impl<'ast> Visit<'ast> for SelfDetector { - fn visit_ident(&mut self, i: &'ast syn::Ident) { - self.0 |= i == &Ident::from(syn::Token![Self](Span::mixed_site())) - } - - fn visit_receiver(&mut self, _node: &'ast syn::Receiver) { - self.0 = true; - } +/// Find a closure defined in one of the provided statements. +/// +/// Panic if no closure was found. +pub fn expect_closure<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { + find_contract_closure(stmts, name) + .expect(&format!("Internal Failure: Expected to find `{name}` closure, but found none")) } -/// Try to determine if this function is part of an `impl`. -/// -/// Detects *methods* by the presence of a receiver argument. Heuristically -/// detects *associated functions* by the use of `Self` anywhere. -/// -/// Why do we need this? It's because if we want to call this `fn`, or any other -/// `fn` we generate into the same context we need to use `foo()` or -/// `Self::foo()` respectively depending on whether this is a plain or -/// associated function or Rust will complain. For the contract machinery we -/// need to generate and then call various functions we generate as well as the -/// original contracted function and so we need to determine how to call them -/// correctly. -/// -/// We can only solve this heuristically. The fundamental problem with Rust -/// macros is that they only see the syntax that's given to them and no other -/// context. It is however that context (of an `impl` block) that definitively -/// determines whether the `fn` is a plain function or an associated function. +/// Find a closure inside a match block. /// -/// The heuristic itself is flawed, but it's the best we can do. For instance -/// this is perfectly legal -/// -/// ``` -/// struct S; -/// impl S { -/// #[i_want_to_call_you] -/// fn helper(u: usize) -> bool { -/// u < 8 -/// } -/// } -/// ``` -/// -/// This function would have to be called `S::helper()` but to the -/// `#[i_want_to_call_you]` attribute this function looks just like a bare -/// function because it never mentions `self` or `Self`. While this is a rare -/// case, the following is much more likely and suffers from the same problem, -/// because we can't know that `Vec == Self`. -/// -/// ``` -/// impl Vec { -/// fn new() -> Vec { -/// Vec { cap: 0, buf: NonNull::dangling() } -/// } -/// } -/// ``` -/// -/// **Side note:** You may be tempted to suggest that we could try and parse -/// `syn::ImplItemFn` and distinguish that from `syn::ItemFn` to distinguish -/// associated function from plain functions. However parsing in an attribute -/// placed on *any* `fn` will always succeed for *both* `syn::ImplItemFn` and -/// `syn::ItemFn`, thus not letting us distinguish between the two. -pub fn is_probably_impl_fn(fun: &ItemFn) -> bool { - let mut self_detector = SelfDetector(false); - self_detector.visit_item_fn(fun); - self_detector.0 +/// Panic if no closure was found. +pub fn expect_closure_in_match<'a>(stmts: &'a mut [Stmt], name: &'static str) -> &'a mut Stmt { + let closure = stmts.iter_mut().find_map(|stmt| { + if let Stmt::Expr(Expr::Match(match_expr), ..) = stmt { + match_expr.arms.iter_mut().find_map(|arm| { + let Expr::Block(block) = arm.body.as_mut() else { return None }; + find_contract_closure(&mut block.block.stmts, name) + }) + } else { + None + } + }); + closure.expect(&format!("Internal Failure: Expected to find `{name}` closure, but found none")) } -/// Convert every use of a pattern in this signature to a simple, fresh, binding-only -/// argument ([`syn::PatIdent`]) and return the [`Ident`] that was generated. -pub fn pats_to_idents

( - sig: &mut syn::punctuated::Punctuated, -) -> impl Iterator + '_ { - sig.iter_mut().enumerate().map(|(i, arg)| match arg { - syn::FnArg::Receiver(_) => Ident::from(syn::Token![self](Span::call_site())), - syn::FnArg::Typed(syn::PatType { pat, .. }) => { - let ident = Ident::new(&format!("arg{i}"), Span::mixed_site()); - *pat.as_mut() = syn::Pat::Ident(syn::PatIdent { - attrs: vec![], - by_ref: None, - mutability: None, - ident: ident.clone(), - subpat: None, - }); - ident - } - }) +/// Extract the body of a closure declaration. +pub fn closure_body(closure: &mut Stmt) -> &mut ExprBlock { + let Stmt::Local(Local { init: Some(LocalInit { expr, .. }), .. }) = closure else { + unreachable!() + }; + let Expr::Closure(closure) = expr.as_mut() else { unreachable!() }; + let Expr::Block(body) = closure.body.as_mut() else { unreachable!() }; + body } /// Does the provided path have the same chain of identifiers as `mtch` (match) @@ -240,35 +169,6 @@ pub fn chunks_by<'a, T, C: Default + Extend>( }) } -/// 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), - } - } -} - -/// Hash this `TokenStream` and return an integer that is at most digits -/// long when hex formatted. -pub fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { - const SIX_HEX_DIGITS_MASK: u64 = 0x1_000_000; - 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 % SIX_HEX_DIGITS_MASK -} - macro_rules! assert_spanned_err { ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => { if !$condition { diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index 73621b2aeec5..50c63173b601 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -4,8 +4,8 @@ //! Initialization routine for the contract handler use proc_macro::{Diagnostic, TokenStream}; -use proc_macro2::{Ident, TokenStream as TokenStream2}; -use syn::{spanned::Spanned, ItemFn}; +use proc_macro2::TokenStream as TokenStream2; +use syn::ItemFn; use super::{ helpers::{chunks_by, is_token_stream_2_comma, matches_path}, @@ -19,24 +19,9 @@ impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { /// Find out if this attribute could be describing a "contract handling" /// state and if so return it. fn try_from(attribute: &'a syn::Attribute) -> Result { - if let syn::Meta::List(lst) = &attribute.meta { - if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) { - let ident = syn::parse2::(lst.tokens.clone()) - .map_err(|e| Some(lst.span().unwrap().error(format!("{e}"))))?; - let ident_str = ident.to_string(); - return match ident_str.as_str() { - "check" => Ok(Self::Check), - "replace" => Ok(Self::Replace), - "wrapper" => Ok(Self::ModifiesWrapper), - _ => { - Err(Some(lst.span().unwrap().error("Expected `check` or `replace` ident"))) - } - }; - } - } if let syn::Meta::NameValue(nv) = &attribute.meta { if matches_path(&nv.path, &["kanitool", "checked_with"]) { - return Ok(ContractFunctionState::Original); + return Ok(ContractFunctionState::Expanded); } } Err(None) @@ -66,12 +51,10 @@ impl<'a> ContractConditionsHandler<'a> { /// Initialize the handler. Constructs the required /// [`ContractConditionsType`] depending on `is_requires`. pub fn new( - function_state: ContractFunctionState, is_requires: ContractConditionsType, attr: TokenStream, annotated_fn: &'a mut ItemFn, attr_copy: TokenStream2, - hash: Option, ) -> Result { let mut output = TokenStream2::new(); let condition_type = match is_requires { @@ -86,7 +69,23 @@ impl<'a> ContractConditionsHandler<'a> { } }; - Ok(Self { function_state, condition_type, annotated_fn, attr_copy, output, hash }) + let fn_name = &annotated_fn.sig.ident; + let generate_name = |purpose| format!("__kani_{purpose}_{fn_name}"); + let check_name = generate_name("check"); + let replace_name = generate_name("replace"); + let recursion_name = generate_name("recursion_check"); + let modifies_name = generate_name("modifies"); + + Ok(Self { + condition_type, + annotated_fn, + attr_copy, + output, + check_name, + replace_name, + recursion_name, + modify_name: modifies_name, + }) } } impl ContractConditionsData { diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 12a1215de2c7..db5f30131405 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -10,7 +10,7 @@ //! implements a state machine in order to be able to handle multiple attributes //! on the same function correctly. //! -//! ## How the handling for `requires` and `ensures` works. +//! ## How the handling for `requires`, `modifies`, and `ensures` works. //! //! Our aim is to generate a "check" function that can be used to verify the //! validity of the contract and a "replace" function that can be used as a @@ -26,102 +26,48 @@ //! instead of throwing a hard error but this means we cannot detect if a given //! function has further contract attributes placed on it during any given //! expansion. As a result every expansion needs to leave the code in a valid -//! state that could be used for all contract functionality but it must alow +//! state that could be used for all contract functionality, but it must allow //! further contract attributes to compose with what was already generated. In -//! addition we also want to make sure to support non-contract attributes on +//! addition, we also want to make sure to support non-contract attributes on //! functions with contracts. //! -//! To this end we use a state machine. The initial state is an "untouched" -//! function with possibly multiple contract attributes, none of which have been -//! expanded. When we expand the first (outermost) `requires` or `ensures` -//! attribute on such a function we re-emit the function unchanged but we also -//! generate fresh "check" and "replace" functions that enforce the condition -//! carried by the attribute currently being expanded. -//! -//! We don't copy all attributes from the original function since they may have -//! unintended consequences for the stubs, such as `inline` or `rustc_diagnostic_item`. -//! -//! We also add new marker attributes to -//! advance the state machine. The "check" function gets a -//! `kanitool::is_contract_generated(check)` attributes and analogous for -//! replace. The re-emitted original meanwhile is decorated with -//! `kanitool::checked_with(name_of_generated_check_function)` and an analogous -//! `kanittool::replaced_with` attribute also. The next contract attribute that -//! is expanded will detect the presence of these markers in the attributes of -//! the item and be able to determine their position in the state machine this -//! way. If the state is either a "check" or "replace" then the body of the -//! function is augmented with the additional conditions carried by the macro. -//! If the state is the "original" function, no changes are performed. -//! -//! We place marker attributes at the bottom of the attribute stack (innermost), -//! otherwise they would not be visible to the future macro expansions. +//! To this end we generate attributes in a two-phase approach: initial and subsequent expansions. //! -//! Below you can see a graphical rendering where boxes are states and each -//! arrow represents the expansion of a `requires` or `ensures` macro. -//! -//! ```plain -//! │ Start -//! ▼ -//! ┌───────────┐ -//! │ Untouched │ -//! │ Function │ -//! └─────┬─────┘ -//! │ -//! Emit │ Generate + Copy Attributes -//! ┌─────────────────┴─────┬──────────┬─────────────────┐ -//! │ │ │ │ -//! │ │ │ │ -//! ▼ ▼ ▼ ▼ -//! ┌──────────┐ ┌───────────┐ ┌───────┐ ┌─────────┐ -//! │ Original │◄─┐ │ Recursion │ │ Check │◄─┐ │ Replace │◄─┐ -//! └──┬───────┘ │ │ Wrapper │ └───┬───┘ │ └────┬────┘ │ -//! │ │ Ignore └───────────┘ │ │ Augment │ │ Augment -//! └──────────┘ └──────┘ └───────┘ -//! -//! │ │ │ │ -//! └───────────────┘ └─────────────────────────────────────────────┘ -//! -//! Presence of Presence of -//! "checked_with" "is_contract_generated" -//! -//! State is detected via -//! ``` +//! The initial expansion modifies the original function to contains all necessary instrumentation +//! contracts need to be analyzed. It will do the following: +//! 1. Annotate the function with extra `kanitool` attributes +//! 2. Generate closures for each contract processing scenario (recursive check, simple check, +//! replacement, and regular execution). //! -//! All named arguments of the annotated function are unsafely shallow-copied -//! with the `kani::internal::untracked_deref` function to circumvent the borrow checker -//! for postconditions. The case where this is relevant is if you want to return -//! a mutable borrow from the function which means any immutable borrow in the -//! postcondition would be illegal. We must ensure that those copies are not -//! dropped (causing a double-free) so after the postconditions we call -//! `mem::forget` on each copy. +//! Subsequent expansions will detect the existence of the extra `kanitool` attributes, +//! and they will only expand the body of the closures generated in the initial phase. //! -//! ## Check function +//! Note: We place marker attributes at the bottom of the attribute stack (innermost), +//! otherwise they would not be visible to the future macro expansions. //! -//! Generates a `_check_` function that assumes preconditions -//! and asserts postconditions. The check function is also marked as generated +//! ## Check closure +//! +//! Generates a `__kani__check` closure that assumes preconditions +//! and asserts postconditions. The check closure is also marked as generated //! with the `#[kanitool::is_contract_generated(check)]` attribute. //! //! Decorates the original function with `#[kanitool::checked_by = -//! "_check_"]`. +//! "__kani_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. +//! every `return` (see [`PostconditionInjector`]). All arguments are captured +//! by the closure. //! //! ## Replace Function //! -//! As the mirror to that also generates a `_replace_` -//! function that asserts preconditions and assumes postconditions. The replace +//! As the mirror to that also generates a `__kani_replace_` +//! closure that asserts preconditions and assumes postconditions. The replace //! function is also marked as generated with the //! `#[kanitool::is_contract_generated(replace)]` attribute. //! //! Decorates the original function with `#[kanitool::replaced_by = -//! "_replace_"]`. -//! -//! The replace function has the same signature as the original function but its -//! body is replaced by `kani::any()`, which generates a non-deterministic -//! value. +//! "__kani_replace_"]`. //! //! ## Inductive Verification //! @@ -148,26 +94,27 @@ //! flip the tracker variable back to `false` in case the function is called //! more than once in its harness. //! -//! To facilitate all this we generate a `_recursion_wrapper_` -//! function with the following shape: +//! To facilitate all this we generate a `__kani_recursion_check_` +//! closure with the following shape: //! //! ```ignored -//! fn recursion_wrapper_...(fn args ...) { +//! let __kani_recursion_check_func = || { //! static mut REENTRY: bool = false; //! //! if unsafe { REENTRY } { -//! call_replace(fn args...) +//! let __kani_replace_func = || { /* replace body */ } +//! __kani_replace_func() //! } else { //! unsafe { reentry = true }; -//! let result_kani_internal = call_check(fn args...); +//! let __kani_check_func = || { /* check body */ } +//! let result_kani_internal = __kani_check_func(); //! unsafe { reentry = false }; //! result_kani_internal //! } -//! } +//! }; //! ``` //! -//! We register this function as `#[kanitool::checked_with = -//! "recursion_wrapper_..."]` instead of the check function. +//! We register this closure as `#[kanitool::recursion_check = "__kani_recursion_..."]`. //! //! # Complete example //! @@ -180,56 +127,106 @@ //! ``` //! //! Turns into -//! //! ``` -//! #[kanitool::checked_with = "div_recursion_wrapper_965916"] -//! #[kanitool::replaced_with = "div_replace_965916"] -//! fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } -//! -//! #[allow(dead_code, unused_variables)] -//! #[kanitool :: is_contract_generated(check)] fn -//! div_check_b97df2(dividend : u32, divisor : u32) -> u32 -//! { -//! let dividend_renamed = kani::internal::untracked_deref(& dividend); -//! let divisor_renamed = kani::internal::untracked_deref(& divisor); -//! kani::assume(divisor != 0); -//! let result_kani_internal : u32 = div_wrapper_b97df2(dividend, divisor); -//! kani::assert( -//! (| result : & u32 | *result <= dividend_renamed)(& result_kani_internal), -//! stringify!(|result : &u32| *result <= dividend)); -//! std::mem::forget(dividend_renamed); -//! std::mem::forget(divisor_renamed); -//! result_kani_internal -//! } -//! -//! #[allow(dead_code, unused_variables)] -//! #[kanitool :: is_contract_generated(replace)] fn -//! div_replace_b97df2(dividend : u32, divisor : u32) -> u32 -//! { -//! let divisor_renamed = kani::internal::untracked_deref(& divisor); -//! let dividend_renamed = kani::internal::untracked_deref(& dividend); -//! kani::assert(divisor != 0, stringify! (divisor != 0)); -//! let result_kani_internal : u32 = kani::any_modifies(); -//! kani::assume( -//! (|result : & u32| *result <= dividend_renamed)(&result_kani_internal)); -//! std::mem::forget(divisor_renamed); -//! std::mem::forget(dividend_renamed); -//! result_kani_internal -//! } -//! -//! #[allow(dead_code)] -//! #[allow(unused_variables)] -//! #[kanitool::is_contract_generated(recursion_wrapper)] -//! fn div_recursion_wrapper_965916(dividend: u32, divisor: u32) -> u32 { -//! static mut REENTRY: bool = false; -//! -//! if unsafe { REENTRY } { -//! div_replace_b97df2(dividend, divisor) -//! } else { -//! unsafe { reentry = true }; -//! let result_kani_internal = div_check_b97df2(dividend, divisor); -//! unsafe { reentry = false }; -//! result_kani_internal +//! #[kanitool::recursion_check = "__kani_recursion_check_div"] +//! #[kanitool::checked_with = "__kani_check_div"] +//! #[kanitool::replaced_with = "__kani_replace_div"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_div"] +//! fn div(dividend: u32, divisor: u32) -> u32 { +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_register_contract"] +//! pub const fn kani_register_contract T>(f: F) -> T { +//! kani::panic("internal error: entered unreachable code: ") +//! } +//! let kani_contract_mode = kani::internal::mode(); +//! match kani_contract_mode { +//! kani::internal::RECURSION_CHECK => { +//! #[kanitool::is_contract_generated(recursion_check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_recursion_check_div = +//! || -> u32 +//! { +//! #[kanitool::recursion_tracker] +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_div = +//! || -> u32 +//! { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let result_kani_internal: u32 = kani::any_modifies(); +//! kani::assume(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal)); +//! result_kani_internal +//! }; +//! __kani_replace_div() +//! } else { +//! unsafe { REENTRY = true }; +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_div = +//! || -> u32 +//! { +//! kani::assume(divisor != 0); +//! let _wrapper_arg = (); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_div = +//! |_wrapper_arg| -> u32 { dividend / divisor }; +//! let result_kani_internal: u32 = +//! __kani_modifies_div(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal), +//! "|result : &u32| *result <= dividend"); +//! result_kani_internal +//! }; +//! let result_kani_internal = __kani_check_div(); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! }; +//! ; +//! kani_register_contract(__kani_recursion_check_div) +//! } +//! kani::internal::REPLACE => { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_div = +//! || -> u32 +//! { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let result_kani_internal: u32 = kani::any_modifies(); +//! kani::assume(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal)); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_replace_div) +//! } +//! kani::internal::SIMPLE_CHECK => { +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_div = +//! || -> u32 +//! { +//! kani::assume(divisor != 0); +//! let _wrapper_arg = (); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_div = +//! |_wrapper_arg| -> u32 { dividend / divisor }; +//! let result_kani_internal: u32 = +//! __kani_modifies_div(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal), +//! "|result : &u32| *result <= dividend"); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_check_div) +//! } +//! _ => { dividend / divisor } //! } //! } //! ``` @@ -264,78 +261,140 @@ //! This expands to //! //! ``` -//! #[kanitool::checked_with = "modify_recursion_wrapper_633496"] -//! #[kanitool::replaced_with = "modify_replace_633496"] -//! #[kanitool::inner_check = "modify_wrapper_633496"] -//! fn modify(ptr: &mut u32) { { *ptr += 1; } } -//! #[allow(dead_code, unused_variables, unused_mut)] -//! #[kanitool::is_contract_generated(recursion_wrapper)] -//! fn modify_recursion_wrapper_633496(arg0: &mut u32) { -//! static mut REENTRY: bool = false; -//! if unsafe { REENTRY } { -//! modify_replace_633496(arg0) -//! } else { -//! unsafe { REENTRY = true }; -//! let result_kani_internal = modify_check_633496(arg0); -//! unsafe { REENTRY = false }; -//! result_kani_internal -//! } -//! } -//! #[allow(dead_code, unused_variables, unused_mut)] -//! #[kanitool::is_contract_generated(check)] -//! fn modify_check_633496(ptr: &mut u32) { -//! let _wrapper_arg_1 = -//! unsafe { kani::internal::Pointer::decouple_lifetime(&ptr) }; -//! kani::assume(*ptr < 100); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let result_kani_internal: () = modify_wrapper_633496(ptr, _wrapper_arg_1); -//! kani::assert((|result| -//! (remember_kani_internal_92cc419d8aca576c) == -//! *ptr)(&result_kani_internal), -//! "|result| old(*ptr + 1) == *ptr"); -//! kani::assert((|result| -//! (remember_kani_internal_92cc419d8aca576c) == -//! *ptr)(&result_kani_internal), -//! "|result| old(*ptr + 1) == *ptr"); -//! result_kani_internal -//! } -//! #[allow(dead_code, unused_variables, unused_mut)] -//! #[kanitool::is_contract_generated(replace)] -//! fn modify_replace_633496(ptr: &mut u32) { -//! kani::assert(*ptr < 100, "*ptr < 100"); -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; -//! let result_kani_internal: () = kani::any_modifies(); -//! *unsafe { -//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) -//! } = kani::any_modifies(); -//! kani::assume((|result| -//! (remember_kani_internal_92cc419d8aca576c) == -//! *ptr)(&result_kani_internal)); -//! kani::assume((|result| -//! (remember_kani_internal_92cc419d8aca576c) == -//! *ptr)(&result_kani_internal)); -//! result_kani_internal -//! } -//! #[kanitool::modifies(_wrapper_arg_1)] -//! #[allow(dead_code, unused_variables, unused_mut)] -//! #[kanitool::is_contract_generated(wrapper)] -//! fn modify_wrapper_633496<'_wrapper_arg_1, -//! WrapperArgType1>(ptr: &mut u32, _wrapper_arg_1: &WrapperArgType1) { -//! *ptr += 1; -//! } -//! #[allow(dead_code)] -//! #[kanitool::proof_for_contract = "modify"] -//! fn main() { -//! kani::internal::init_contracts(); -//! { let mut i = kani::any(); modify(&mut i); } +//! #[kanitool::recursion_check = "__kani_recursion_check_modify"] +//! #[kanitool::checked_with = "__kani_check_modify"] +//! #[kanitool::replaced_with = "__kani_replace_modify"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_modify"] +//! fn modify(ptr: &mut u32) { +//! #[inline(never)] +//! #[kanitool::fn_marker = "kani_register_contract"] +//! pub const fn kani_register_contract T>(f: F) -> T { +//! kani::panic("internal error: entered unreachable code: ") +//! } +//! let kani_contract_mode = kani::internal::mode(); +//! match kani_contract_mode { +//! kani::internal::RECURSION_CHECK => { +//! #[kanitool::is_contract_generated(recursion_check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_recursion_check_modify = +//! || +//! { +//! #[kanitool::recursion_tracker] +//! static mut REENTRY: bool = false; +//! if unsafe { REENTRY } { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_modify = +//! || +//! { +//! kani::assert(*ptr < 100, "*ptr < 100"); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let result_kani_internal: () = kani::any_modifies(); +//! *unsafe { +//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) +//! } = kani::any_modifies(); +//! kani::assume(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! kani::assume(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! result_kani_internal +//! }; +//! __kani_replace_modify() +//! } else { +//! unsafe { REENTRY = true }; +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_modify = +//! || +//! { +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let _wrapper_arg = (ptr as *const _,); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_modify = +//! |_wrapper_arg| { *ptr += 1; }; +//! let result_kani_internal: () = +//! __kani_modifies_modify(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! result_kani_internal +//! }; +//! let result_kani_internal = __kani_check_modify(); +//! unsafe { REENTRY = false }; +//! result_kani_internal +//! } +//! }; +//! ; +//! kani_register_contract(__kani_recursion_check_modify) +//! } +//! kani::internal::REPLACE => { +//! #[kanitool::is_contract_generated(replace)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_replace_modify = +//! || +//! { +//! kani::assert(*ptr < 100, "*ptr < 100"); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let result_kani_internal: () = kani::any_modifies(); +//! *unsafe { +//! kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(ptr))) +//! } = kani::any_modifies(); +//! kani::assume(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! kani::assume(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal)); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_replace_modify) +//! } +//! kani::internal::SIMPLE_CHECK => { +//! #[kanitool::is_contract_generated(check)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_check_modify = +//! || +//! { +//! kani::assume(*ptr < 100); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let _wrapper_arg = (ptr as *const _,); +//! #[kanitool::is_contract_generated(wrapper)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_modifies_modify = +//! |_wrapper_arg| { *ptr += 1; }; +//! let result_kani_internal: () = +//! __kani_modifies_modify(_wrapper_arg); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_check_modify) +//! } +//! _ => { *ptr += 1; } +//! } //! } //! ``` use proc_macro::TokenStream; use proc_macro2::{Ident, TokenStream as TokenStream2}; -use quote::{quote, ToTokens}; +use quote::quote; use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn}; mod bootstrap; @@ -397,36 +456,35 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { .into() } -/// Classifies the state a function is in in the contract handling pipeline. +/// 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 function already expanded with the closures. + Expanded, /// 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, - /// This is a replace function that was generated from a previous evaluation - /// of a contract attribute. - Replace, - ModifiesWrapper, } /// The information needed to generate the bodies of check and replacement /// functions that integrate the conditions from this contract attribute. struct ContractConditionsHandler<'a> { - function_state: ContractFunctionState, /// Information specific to the type of contract attribute we're expanding. condition_type: ContractConditionsData, /// Body of the function this attribute was found on. - annotated_fn: &'a mut ItemFn, + annotated_fn: &'a ItemFn, /// An unparsed, unmodified copy of `attr`, used in the error messages. attr_copy: TokenStream2, /// The stream to which we should write the generated code. output: TokenStream2, - hash: Option, + /// The name of the check closure. + check_name: String, + /// The name of the replace closure. + replace_name: String, + /// The name of the recursion closure. + recursion_name: String, + /// The name of the modifies closure. + modify_name: String, } /// Which kind of contract attribute are we dealing with? @@ -460,23 +518,8 @@ impl<'a> ContractConditionsHandler<'a> { /// Handle the contract state and return the generated code fn dispatch_on(mut self, state: ContractFunctionState) -> TokenStream2 { match state { - ContractFunctionState::ModifiesWrapper => self.emit_augmented_modifies_wrapper(), - ContractFunctionState::Check => { - // The easy cases first: If we are on a check or replace function - // emit them again but with additional conditions layered on. - // - // Since we are already on the check function, it will have an - // appropriate, unique generated name which we are just going to - // pass on. - self.emit_check_function(None); - } - ContractFunctionState::Replace => { - // Analogous to above - self.emit_replace_function(None); - } - ContractFunctionState::Original => { - unreachable!("Impossible: This is handled via short circuiting earlier.") - } + // We are on the already expanded function. + ContractFunctionState::Expanded => self.handle_expanded(), ContractFunctionState::Untouched => self.handle_untouched(), } self.output @@ -493,35 +536,9 @@ fn contract_main( is_requires: ContractConditionsType, ) -> TokenStream { let attr_copy = TokenStream2::from(attr.clone()); - - let item_stream_clone = item.clone(); let mut item_fn = parse_macro_input!(item as ItemFn); - let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); - - 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 ourselves unchanged. - // - // Since this is the only function state case that doesn't need a - // handler to be constructed, we do this match early, separately. - return item_fn.into_token_stream().into(); - } - - let hash = matches!(function_state, ContractFunctionState::Untouched) - .then(|| helpers::short_hash_of_token_stream(&item_stream_clone)); - - let handler = match ContractConditionsHandler::new( - function_state, - is_requires, - attr, - &mut item_fn, - attr_copy, - hash, - ) { + let handler = match ContractConditionsHandler::new(is_requires, attr, &mut item_fn, attr_copy) { Ok(handler) => handler, Err(e) => return e.into_compile_error().into(), }; diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 280839dcafca..02ac4a772348 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -3,8 +3,10 @@ //! Logic used for generating the code that replaces a function with its contract. -use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; +use std::mem; +use syn::Stmt; use super::{ helpers::*, @@ -13,6 +15,13 @@ use super::{ }; impl<'a> ContractConditionsHandler<'a> { + /// Create initial set of replace statements which is the return havoc. + fn initial_replace_stmts(&self) -> Vec { + let return_type = return_type_to_type(&self.annotated_fn.sig.output); + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)] + } + /// Split an existing replace body of the form /// /// ```ignore @@ -35,26 +44,21 @@ impl<'a> ContractConditionsHandler<'a> { /// Such that the first vector contains everything up to and including the single result havoc /// and the second one the rest, excluding the return. /// - /// If this is the first time we're emitting replace we create the return havoc and nothing else. - fn ensure_bootstrapped_replace_body(&self) -> (Vec, Vec) { - if self.is_first_emit() { - let return_type = return_type_to_type(&self.annotated_fn.sig.output); - let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - (vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)], vec![]) - } else { - let stmts = &self.annotated_fn.block.stmts; - let idx = stmts - .iter() - .enumerate() - .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i)) - .unwrap_or_else(|| { - panic!("ICE: Could not find result let binding in statement sequence") - }); - // We want the result assign statement to end up as the last statement in the first - // vector, hence the `+1`. - let (before, after) = stmts.split_at(idx + 1); - (before.to_vec(), after.split_last().unwrap().1.to_vec()) - } + fn split_replace(&self, mut stmts: Vec) -> (Vec, Vec) { + // Pop the return result since we always re-add it. + stmts.pop(); + + let idx = stmts + .iter() + .enumerate() + .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i)) + .unwrap_or_else(|| { + panic!("ICE: Could not find result let binding in statement sequence") + }); + // We want the result assign statement to end up as the last statement in the first + // vector, hence the `+1`. + let (before, after) = stmts.split_at_mut(idx + 1); + (before.to_vec(), after.to_vec()) } /// Create the body of a stub for this contract. @@ -65,69 +69,65 @@ impl<'a> ContractConditionsHandler<'a> { /// /// `use_nondet_result` will only be true if this is the first time we are /// generating a replace function. - fn make_replace_body(&self) -> TokenStream2 { - let (before, after) = self.ensure_bootstrapped_replace_body(); - + fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream { match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + quote!({ kani::assert(#attr, stringify!(#attr_copy)); #(#before)* #(#after)* #result - ) + }) } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + quote!({ #remembers #(#before)* #(#after)* kani::assume(#ensures_clause); #result - ) + }) } ContractConditionsData::Modifies { attr } => { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - quote!( + quote!({ #(#before)* #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)* #(#after)* #result - ) + }) } } } - /// Emit the replace funtion into the output stream. + /// Emit the replace function into the output stream. /// - /// See [`Self::make_replace_body`] for the most interesting parts of this + /// See [`Self::expand_replace_body`] for the most interesting parts of this /// function. - pub fn emit_replace_function(&mut self, override_function_ident: Option) { - self.emit_common_header(); + pub fn replace_closure(&self) -> TokenStream { + let replace_ident = Ident::new(&self.replace_name, Span::call_site()); + let sig = &self.annotated_fn.sig; + let output = &sig.output; + let before = self.initial_replace_stmts(); + let body = self.expand_replace_body(&before, &vec![]); - if self.function_state.emit_tag_attr() { - // If it's the first time we also emit this marker. Again, order is - // important so this happens as the last emitted attribute. - self.output.extend(quote!(#[kanitool::is_contract_generated(replace)])); - } - let mut sig = self.annotated_fn.sig.clone(); - // We use non-constant functions, thus, the wrapper cannot be constant. - sig.constness = None; - let body = self.make_replace_body(); - if let Some(ident) = override_function_ident { - sig.ident = ident; - } + quote!( + #[kanitool::is_contract_generated(replace)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut #replace_ident = || #output #body; + ) + } - // Finally emit the check function itself. - self.output.extend(quote!( - #sig { - #body - } - )); + /// Expand the `replace` body with the new attribute. + pub fn expand_replace(&self, closure: &mut Stmt) { + let body = closure_body(closure); + let (before, after) = self.split_replace(mem::take(&mut body.block.stmts)); + let stream = self.expand_replace_body(&before, &after); + *body = syn::parse2(stream).unwrap(); } } diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index 1ab791d9a117..f189a9f98b0c 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -10,96 +10,11 @@ use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; -use quote::{quote, ToTokens}; +use quote::quote; use std::hash::{DefaultHasher, Hash, Hasher}; -use syn::{ - spanned::Spanned, visit_mut::VisitMut, Attribute, Expr, ExprCall, ExprClosure, ExprPath, Path, -}; +use syn::{spanned::Spanned, visit_mut::VisitMut, Expr, ExprCall, ExprClosure, ExprPath, Path}; -use super::{ContractConditionsHandler, ContractFunctionState, INTERNAL_RESULT_IDENT}; - -impl ContractFunctionState { - /// Do we need to emit the `is_contract_generated` tag attribute on the - /// generated function(s)? - pub fn emit_tag_attr(self) -> bool { - matches!(self, ContractFunctionState::Untouched) - } -} - -impl<'a> ContractConditionsHandler<'a> { - pub fn is_first_emit(&self) -> bool { - matches!(self.function_state, ContractFunctionState::Untouched) - } - - /// Create a new name for the assigns wrapper function *or* get the name of - /// the wrapper we must have already generated. This is so that we can - /// recognize a call to that wrapper inside the check function. - pub fn make_wrapper_name(&self) -> Ident { - if let Some(hash) = self.hash { - identifier_for_generated_function(&self.annotated_fn.sig.ident, "wrapper", hash) - } else { - let str_name = self.annotated_fn.sig.ident.to_string(); - let splits = str_name.rsplitn(3, '_').collect::>(); - let [hash, _, base] = splits.as_slice() else { - unreachable!("Odd name for function {str_name}, splits were {}", splits.len()); - }; - - Ident::new(&format!("{base}_wrapper_{hash}"), Span::call_site()) - } - } - - /// Emit attributes common to check or replace function into the output - /// stream. - pub fn emit_common_header(&mut self) { - if self.function_state.emit_tag_attr() { - self.output.extend(quote!( - #[allow(dead_code, unused_variables, unused_mut)] - )); - } - - #[cfg(not(feature = "no_core"))] - self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); - - // When verifying core and standard library, we need to add an unstable attribute to - // the functions generated by Kani. - // We also need to filter `rustc_diagnostic_item` attribute. - // We should consider a better strategy than just duplicating all attributes. - #[cfg(feature = "no_core")] - { - self.output.extend(quote!( - #[unstable(feature="kani", issue="none")] - )); - self.output.extend( - self.annotated_fn - .attrs - .iter() - .filter(|attr| { - if let Some(ident) = attr.path().get_ident() { - let name = ident.to_string(); - !name.starts_with("rustc") - && !(name == "stable") - && !(name == "unstable") - } else { - true - } - }) - .flat_map(Attribute::to_token_stream), - ); - } - } -} - -/// Makes consistent names for a generated function which was created for -/// `purpose`, from an attribute that decorates `related_function` with the -/// hash `hash`. -pub fn identifier_for_generated_function( - related_function_name: &Ident, - purpose: &str, - hash: u64, -) -> Ident { - let identifier = format!("{}_{purpose}_{hash:x}", related_function_name); - Ident::new(&identifier, proc_macro2::Span::mixed_site()) -} +use super::INTERNAL_RESULT_IDENT; /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`] /// since we can't abstract over mutability. Input is the object to match on and the name of the @@ -147,19 +62,6 @@ pub fn try_as_result_assign(stmt: &syn::Stmt) -> Option<&syn::LocalInit> { try_as_result_assign_pat!(stmt, as_ref) } -/// Try to parse this statement as `let result : <...> = ;` and return a mutable reference to -/// `init`. -/// -/// This is the shape of statement we create in check functions (with `init` being a call to check -/// function with additional pointer arguments for the `modifies` clause) and we need to recognize -/// it to then edit this call if we find another `modifies` clause and add its additional arguments. -/// additional conditions. -/// -/// It's a thin wrapper around [`try_as_result_assign_pat!`] to create a mutable match. -pub fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalInit> { - try_as_result_assign_pat!(stmt, as_mut) -} - /// When a `#[kani::ensures(|result|expr)]` is expanded, this function is called on with `build_ensures(|result|expr)`. /// This function goes through the expr and extracts out all the `old` expressions and creates a sequence /// of statements that instantiate these expressions as `let remember_kani_internal_x = old_expr;` diff --git a/tests/cargo-kani/iss2857/Cargo.toml b/tests/cargo-kani/iss2857/Cargo.toml new file mode 100644 index 000000000000..9f2a72342c19 --- /dev/null +++ b/tests/cargo-kani/iss2857/Cargo.toml @@ -0,0 +1,9 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "iss2857" +version = "0.1.0" +edition = "2021" + +[dependencies] +sec1 = "0.7.3" diff --git a/tests/cargo-kani/iss2857/expected b/tests/cargo-kani/iss2857/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/cargo-kani/iss2857/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/iss2857/src/main.rs b/tests/cargo-kani/iss2857/src/main.rs new file mode 100644 index 000000000000..6a0ed40a006e --- /dev/null +++ b/tests/cargo-kani/iss2857/src/main.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks that https://github.com/model-checking/kani/issues/2857 is +// fixed + +#[kani::proof] +fn check_der_error() { + let e = sec1::der::Error::incomplete(sec1::der::Length::ZERO); + let _ = format!("{e:?}"); +} + +fn main() {} diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs index 39c0b0efb54f..2941ec126f3c 100644 --- a/tests/coverage/unreachable/abort/main.rs +++ b/tests/coverage/unreachable/abort/main.rs @@ -5,7 +5,7 @@ use std::process; -#[cfg_attr(kani, kani::proof, kani::unwind(5))] +#[kani::proof] fn main() { for i in 0..4 { if i == 1 { diff --git a/tests/expected/abort/main.rs b/tests/expected/abort/main.rs index 9e2f5b7a808c..2941ec126f3c 100644 --- a/tests/expected/abort/main.rs +++ b/tests/expected/abort/main.rs @@ -6,7 +6,6 @@ use std::process; #[kani::proof] -#[kani::unwind(5)] fn main() { for i in 0..4 { if i == 1 { diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.expected b/tests/expected/function-contract/gcd_rec_replacement_pass.expected index 29c61cf9437c..b522716cc001 100644 --- a/tests/expected/function-contract/gcd_rec_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_rec_replacement_pass.expected @@ -10,7 +10,7 @@ Frac::check_equals.assertion\ - Status: SUCCESS\ - Description: "assertion failed: gcd1 == gcd2" -gcd.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "x != 0 && y != 0" diff --git a/tests/expected/function-contract/gcd_replacement_pass.expected b/tests/expected/function-contract/gcd_replacement_pass.expected index 48d3565ef9f1..1c6df8455267 100644 --- a/tests/expected/function-contract/gcd_replacement_pass.expected +++ b/tests/expected/function-contract/gcd_replacement_pass.expected @@ -1,4 +1,4 @@ -gcd.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "x != 0 && y != 0" diff --git a/tests/expected/function-contract/modifies/global_fail.expected b/tests/expected/function-contract/modifies/global_fail.expected index 04e0359ad8a4..a9ecaf689376 100644 --- a/tests/expected/function-contract/modifies/global_fail.expected +++ b/tests/expected/function-contract/modifies/global_fail.expected @@ -1,9 +1,9 @@ assigns\ - Status: FAILURE\ -- Description: "Check that *var_1 is assignable"\ -in function modify_wrapper +- Description: "Check that *var_3 is assignable"\ +in function modify -Failed Checks: Check that *var_1 is assignable\ -in modify_wrapper +Failed Checks: Check that *var_3 is assignable\ +in modify VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected index 02ce972ef370..d5679f71b74c 100644 --- a/tests/expected/function-contract/modifies/havoc_pass.expected +++ b/tests/expected/function-contract/modifies/havoc_pass.expected @@ -1,38 +1,13 @@ -copy_replace.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "equality"\ in function copy_replace VERIFICATION:- SUCCESSFUL -copy.assigns\ +.assigns\ - Status: SUCCESS\ - Description: "Check that var_4 is assignable"\ in function copy -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_3 is assignable"\ -in function copy\ - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_5 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_5 is assignable"\ -in function copy\ - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_7 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_7 is assignable"\ -in function copy - VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected index 02ce972ef370..2ea601aa26a0 100644 --- a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected @@ -5,34 +5,9 @@ in function copy_replace VERIFICATION:- SUCCESSFUL -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_4 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_3 is assignable"\ -in function copy\ - copy.assigns\ - Status: SUCCESS\ - Description: "Check that var_5 is assignable"\ in function copy -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_5 is assignable"\ -in function copy\ - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that var_7 is assignable"\ -in function copy - -copy.assigns\ -- Status: SUCCESS\ -- Description: "Check that *var_7 is assignable"\ -in function copy - VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/simple_fail.expected b/tests/expected/function-contract/modifies/simple_fail.expected index ffaee2293931..269ffa6cc2e2 100644 --- a/tests/expected/function-contract/modifies/simple_fail.expected +++ b/tests/expected/function-contract/modifies/simple_fail.expected @@ -1,7 +1,7 @@ assigns\ - Status: FAILURE\ -- Description: "Check that *ptr is assignable" +- Description: "Check that *var_6 is assignable" -Failed Checks: Check that *ptr is assignable +Failed Checks: Check that *var_6 is assignable VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected index 4d5407fdd850..4ac03d025558 100644 --- a/tests/expected/function-contract/modifies/vec_pass.expected +++ b/tests/expected/function-contract/modifies/vec_pass.expected @@ -1,17 +1,17 @@ -modify.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "v.len() > 0"\ in function modify -modify_replace.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "element set"\ -in function modify_replace +in function modify -modify_replace.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "vector tail equality"\ -in function modify_replace +in function modify assertion\ - Status: SUCCESS\ diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs index ead1c1538b4d..b02cc776d299 100644 --- a/tests/expected/function-contract/pattern_use.rs +++ b/tests/expected/function-contract/pattern_use.rs @@ -1,9 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts +//! Test that contracts supports function args with pattern use and mut declaration. #[kani::ensures(|result : &u32| *result <= dividend)] -fn div((dividend, divisor): (u32, u32)) -> u32 { +fn div((mut dividend, divisor): (u32, u32)) -> u32 { dividend / divisor } diff --git a/tests/expected/function-contract/simple_replace_pass.expected b/tests/expected/function-contract/simple_replace_pass.expected index e1fc78ca462f..7dbc9bae68bd 100644 --- a/tests/expected/function-contract/simple_replace_pass.expected +++ b/tests/expected/function-contract/simple_replace_pass.expected @@ -1,4 +1,4 @@ -div.assertion\ +.assertion\ - Status: SUCCESS\ - Description: "divisor != 0" diff --git a/tests/expected/function-contract/trait_impls/associated_fn.expected b/tests/expected/function-contract/trait_impls/associated_fn.expected new file mode 100644 index 000000000000..c6f4c6382f17 --- /dev/null +++ b/tests/expected/function-contract/trait_impls/associated_fn.expected @@ -0,0 +1,7 @@ +Checking harness check_foo_b... +VERIFICATION:- SUCCESSFUL + +Checking harness check_foo_a... +VERIFICATION:- SUCCESSFUL + +Complete - 2 successfully verified harnesses, 0 failures, 2 total diff --git a/tests/expected/function-contract/trait_impls/associated_fn.rs b/tests/expected/function-contract/trait_impls/associated_fn.rs new file mode 100644 index 000000000000..807469bcc7e3 --- /dev/null +++ b/tests/expected/function-contract/trait_impls/associated_fn.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! Check that we can add contracts to associated functions. + +extern crate kani; + +#[derive(PartialEq, Eq)] +enum Foo { + A(u8), + B(char), +} + +impl Foo { + #[kani::ensures(|result| *result == Foo::A(inner))] + pub fn new_a(inner: u8) -> Foo { + Foo::A(inner) + } + + #[kani::requires(char::from_u32(inner).is_some())] + #[kani::ensures(|result| matches!(*result, Foo::B(c) if u32::from(c) == inner))] + pub unsafe fn new_b(inner: u32) -> Foo { + Foo::B(char::from_u32_unchecked(inner)) + } +} + +#[kani::proof_for_contract(Foo::new_a)] +fn check_foo_a() { + let _ = Foo::new_a(kani::any()); +} + +#[kani::proof_for_contract(Foo::new_b)] +fn check_foo_b() { + let _ = unsafe { Foo::new_b(kani::any()) }; +} diff --git a/tests/expected/function-contract/trait_impls/methods.expected b/tests/expected/function-contract/trait_impls/methods.expected new file mode 100644 index 000000000000..3906a6fd7a10 --- /dev/null +++ b/tests/expected/function-contract/trait_impls/methods.expected @@ -0,0 +1,17 @@ +Checking harness check_next_y... + +Status: SUCCESS\ +Description: "|result| result.y == old(self.y) + 1"\ +in function Point::next_y + +VERIFICATION:- SUCCESSFUL + +Checking harness check_add_x... + +Status: SUCCESS\ +Description: "|_| val < 0 || self.x >= old(self.x)"\ +in function Point::add_x + +VERIFICATION:- SUCCESSFUL + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/function-contract/trait_impls/methods.rs b/tests/expected/function-contract/trait_impls/methods.rs new file mode 100644 index 000000000000..128710f1436d --- /dev/null +++ b/tests/expected/function-contract/trait_impls/methods.rs @@ -0,0 +1,67 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. +// kani-flags: -Zfunction-contracts + +//! Check that we can add contract to methods and trait implementations. +//! Original code taken from: +//! + +use std::ops::Add; + +#[derive(Debug, Copy, Clone, PartialEq, kani::Arbitrary)] +struct Point { + x: i32, + y: i32, +} + +impl Add for Point { + type Output = Self; + + #[kani::requires(!self.x.overflowing_add(other.x).1)] + #[kani::requires(!self.y.overflowing_add(other.y).1)] + #[kani::ensures(|result| result.x == self.x + other.x)] + #[kani::ensures(|result| result.y == self.y + other.y)] + fn add(self, other: Self) -> Self { + Self { x: self.x + other.x, y: self.y + other.y } + } +} + +impl Point { + #[kani::modifies(&mut self.x)] + #[kani::requires(!self.x.overflowing_add(val).1)] + #[kani::ensures(|_| val < 0 || self.x >= old(self.x))] + #[kani::ensures(|_| val > 0 || self.x <= old(self.x))] + pub fn add_x(&mut self, val: i32) { + self.x += val; + } + + #[kani::requires(self.y < i32::MAX)] + #[kani::ensures(|result| result.y == old(self.y) + 1)] + pub fn next_y(mut self) -> Self { + self.y += 1; + self + } +} + +#[kani::proof_for_contract(Point::add_x)] +fn check_add_x() { + let mut p1: Point = kani::any(); + let _ = p1.add_x(kani::any()); +} + +#[kani::proof_for_contract(Point::next_y)] +fn check_next_y() { + let p1: Point = kani::any(); + let _ = p1.next_y(); +} + +/// We should enable this once we add support to specifying trait methods: +/// +#[cfg(ignore)] +#[kani::proof_for_contract(Point::add)] +fn check_add() { + let (p1, p2): (Point, Point) = kani::any(); + let _ = p1.add(p2); +} diff --git a/tests/expected/iterator/main.rs b/tests/expected/iterator/main.rs index 5cf9402bcb23..b1cb4a89cfbf 100644 --- a/tests/expected/iterator/main.rs +++ b/tests/expected/iterator/main.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #[kani::proof] -#[kani::unwind(4)] fn main() { let mut z = 1; for i in 1..4 { diff --git a/tests/kani/Coroutines/main.rs b/tests/kani/Coroutines/main.rs index e059305a6da2..0742d14a6ada 100644 --- a/tests/kani/Coroutines/main.rs +++ b/tests/kani/Coroutines/main.rs @@ -10,7 +10,6 @@ use std::ops::{Coroutine, CoroutineState}; use std::pin::Pin; #[kani::proof] -#[kani::unwind(3)] fn main() { let mut add_one = #[coroutine] |mut resume: u8| { diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs new file mode 100644 index 000000000000..b485ddf2b32b --- /dev/null +++ b/tests/kani/FunctionContracts/fn_params.rs @@ -0,0 +1,73 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Checks that function contracts work with different type of parameter expressions: +//! Source: +//! +//! Note: See `receiver_contracts` for receiver parameters. +// kani-flags: -Zfunction-contracts + +extern crate kani; +use std::convert::TryFrom; + +/// Dummy structure to check different patterns in contract. +#[derive(Copy, Clone, PartialEq, Eq, kani::Arbitrary)] +struct MyStruct { + c: char, + u: u32, +} + +/// Add contracts to ensure that all parameters are representing the same pair (char, u32). +#[kani::requires(val.u == second)] +#[kani::requires(val.u == tup_u)] +#[kani::requires(Ok(val.c) == char::try_from(first))] +#[kani::requires(val.c == tup_c)] +/// We need this extra clause due to . +#[kani::requires(char::try_from(first).is_ok())] +pub fn odd_parameters_eq( + [first, second]: [u32; 2], + (tup_c, tup_u): (char, u32), + val @ MyStruct { c: val_c, u }: MyStruct, +) { + assert_eq!(tup_c, char::try_from(first).unwrap()); + assert_eq!(tup_c, val_c); + + assert_eq!(tup_u, second); + assert_eq!(tup_u, u); + assert_eq!(val, MyStruct { c: val_c, u }); +} + +/// Similar to the function above, but with one requirement missing. +#[kani::requires(val.u == second)] +#[kani::requires(val.u == tup_u)] +#[kani::requires(Ok(val.c) == char::try_from(first))] +// MISSING: #[kani::requires(val.c == tup_c)] +// We need this extra clause due to . +#[kani::requires(char::try_from(first).is_ok())] +pub fn odd_parameters_eq_wrong( + [first, second]: [u32; 2], + (tup_c, tup_u): (char, u32), + val @ MyStruct { c: val_c, u }: MyStruct, +) { + assert_eq!(tup_c, char::try_from(first).unwrap()); + assert_eq!(tup_c, val_c); + + assert_eq!(tup_u, second); + assert_eq!(tup_u, u); + assert_eq!(val, MyStruct { c: val_c, u }); +} + +mod verify { + use super::*; + use kani::Arbitrary; + + #[kani::proof_for_contract(odd_parameters_eq)] + fn check_params() { + odd_parameters_eq(kani::any(), kani::any(), kani::any()) + } + + #[kani::should_panic] + #[kani::proof_for_contract(odd_parameters_eq_wrong)] + fn check_params_wrong() { + odd_parameters_eq_wrong(kani::any(), kani::any(), kani::any()) + } +} diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/receiver_contracts.rs new file mode 100644 index 000000000000..5ca63f1558c3 --- /dev/null +++ b/tests/kani/FunctionContracts/receiver_contracts.rs @@ -0,0 +1,155 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Checks that function contracts work with different types of receivers. I.e.: +//! - &Self (i.e. &self) +//! - &mut Self (i.e &mut self) +//! - Box +//! - Rc +//! - Arc +//! - Pin

where P is one of the types above +//! Source: +// compile-flags: --edition 2021 +// kani-flags: -Zfunction-contracts + +#![feature(rustc_attrs)] + +extern crate kani; + +use std::boxed::Box; +use std::pin::Pin; +use std::rc::Rc; +use std::sync::Arc; + +/// Type representing a valid ASCII value going from `0..=128`. +#[derive(Copy, Clone, PartialEq, Eq)] +#[rustc_layout_scalar_valid_range_start(0)] +#[rustc_layout_scalar_valid_range_end(128)] +struct CharASCII(u8); + +impl kani::Arbitrary for CharASCII { + fn any() -> CharASCII { + let val = kani::any_where(|inner: &u8| *inner <= 128); + unsafe { CharASCII(val) } + } +} + +/// This type contains unsafe setter functions with the same contract but different type of +/// receivers. +impl CharASCII { + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_val(&mut self, new_val: u8) { + self.0 = new_val + } + + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_mut_ref(self: &mut Self, new_val: u8) { + self.0 = new_val + } + + #[kani::modifies(&self.as_ref().0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.as_ref().0 == new_val)] + unsafe fn set_box(mut self: Box, new_val: u8) { + self.as_mut().0 = new_val + } + + #[kani::modifies(&self.as_ref().0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.as_ref().0 == new_val)] + unsafe fn set_rc(mut self: Rc, new_val: u8) { + Rc::<_>::get_mut(&mut self).unwrap().0 = new_val + } + + /// We cannot specify the counter today which is modified in this function. + /// + #[kani::modifies(&self.as_ref().0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.as_ref().0 == new_val)] + unsafe fn set_arc(mut self: Arc, new_val: u8) { + Arc::<_>::get_mut(&mut self).unwrap().0 = new_val; + } + + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_pin(mut self: Pin<&mut Self>, new_val: u8) { + self.0 = new_val + } + + #[kani::modifies(&self.0)] + #[kani::requires(new_val <= 128)] + #[kani::ensures(|_| self.0 == new_val)] + unsafe fn set_pin_box(mut self: Pin>, new_val: u8) { + self.0 = new_val + } +} + +mod verify { + use super::*; + use kani::Arbitrary; + + #[kani::proof_for_contract(CharASCII::set_val)] + fn check_set_val() { + let mut obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { obj.set_val(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_mut_ref)] + fn check_mut_ref() { + let mut obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { obj.set_mut_ref(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_box)] + fn check_box() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Box::new(obj).set_box(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_rc)] + fn check_rc() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Rc::new(obj).set_rc(new_val) }; + } + + /// This test currently fails because we cannot specify that the counter will be modified. + /// The counter is behind a pointer, but `Arc` only provide access to the data portion of + /// the allocation. + /// + #[cfg(arc_fails)] + #[kani::proof_for_contract(CharASCII::set_arc)] + fn check_arc() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Arc::new(obj).set_arc(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_pin)] + fn check_pin() { + let mut obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Pin::new(&mut obj).set_pin(new_val) }; + } + + #[kani::proof_for_contract(CharASCII::set_pin_box)] + fn check_pin_box() { + let obj = CharASCII::any(); + let original = obj.0; + let new_val = kani::any_where(|new| *new != original); + unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) }; + } +} diff --git a/tests/kani/Intrinsics/Math/Arith/log10.rs b/tests/kani/Intrinsics/Math/Arith/log10.rs new file mode 100644 index 000000000000..4670c72cfeb3 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log10.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_log10_32() { + let ten = 10.0f32; + + // log10(10) - 1 == 0 + let abs_difference = (ten.log10() - 1.0).abs(); + + // should be <= f32::EPSILON, but CBMC's approximation of log10 makes results less precise + assert!(abs_difference <= 0.03); +} + +#[kani::proof] +fn verify_log10_64() { + let hundred = 100.0_f64; + + // log10(100) - 2 == 0 + let abs_difference = (hundred.log10() - 2.0).abs(); + + assert!(abs_difference < 0.03); +} diff --git a/tests/kani/Intrinsics/Math/Arith/log2.rs b/tests/kani/Intrinsics/Math/Arith/log2.rs new file mode 100644 index 000000000000..52153f8b368a --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log2.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_log2_32() { + let two = 2.0f32; + + // log2(2) - 1 == 0 + let abs_difference = (two.log2() - 1.0).abs(); + + // should be <= f32::EPSILON, but CBMC's approximation of log2 makes results less precise + assert!(abs_difference <= 0.09); +} + +#[kani::proof] +fn verify_log2_64() { + let four = 4.0_f64; + + // log2(4) - 2 == 0 + let abs_difference = (four.log2() - 2.0).abs(); + + assert!(abs_difference < 0.09); +} diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 2d5e891f3fdc..75afd77dfa88 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 2d5e891f3fdc8a88b2d457baceedea5751efaa0d +Subproject commit 75afd77dfa88d696900f12ee747409ddb208a745