From e980aa2f233b37fed53f446a720a45ca2af19956 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 1 Aug 2024 13:00:16 -0700 Subject: [PATCH 1/4] Enable contracts in associated functions (#3363) Contracts could not be used with associated function unless they used Self. This is because at a proc-macro level, we cannot determine if we are inside a associated function or not, except in cases where `Self` is used. In cases where the contract generation could not identify an associated function, it would generate incorrect call, triggering a compilation error. Another problem with our encoding is that users could not annotate trait implementations with contract attributes. This would try to create new functions inside the trait implementation context, which is not allowed. In order to solve these issues, we decided to wrap contract logic using closures instead of functions. See the discussion in the original issue (#3206) for more details. The new solution is still split in two: 1. The proc-macro will now expand the code inside the original function to encode all possible scenarios (check, replace, recursive check, and original body). 2. Instead of using stub, we introduced a new transformation pass that chooses which scenario to pick according to the target harness configuration, and cleanup unused logic. The expanded function will have the following structure: ```rust #[kanitool::recursion_check = "__kani_recursion_check_modify"] #[kanitool::checked_with = "__kani_check_modify"] #[kanitool::replaced_with = "__kani_replace_modify"] #[kanitool::inner_check = "__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 */ } } } ``` In runtime, `kani::internal::mode()` will return kani::internal::ORIGINAL, which runs the original body. The transformation will replace this call by a different assignment in case the function needs to be replaced. The body of the unused closures will be replaced by a `UNREACHABLE` statement to avoid unnecessary code to be analyzed. This is still fairly hacky, but hopefully we can cleanup this logic once Rust adds contract support. :crossed_fingers: Resolves #3206 --- .../codegen_cprover_gotoc/codegen/contract.rs | 227 ++++---- .../compiler_interface.rs | 9 +- kani-compiler/src/kani_middle/attributes.rs | 363 +++++------- .../src/kani_middle/codegen_units.rs | 53 +- kani-compiler/src/kani_middle/resolve.rs | 31 + .../src/kani_middle/transform/body.rs | 38 +- .../src/kani_middle/transform/contracts.rs | 379 +++++++++++-- .../kani_middle/transform/kani_intrinsics.rs | 7 +- .../src/kani_middle/transform/mod.rs | 6 +- kani-driver/src/call_goto_instrument.rs | 10 +- kani_metadata/src/harness.rs | 6 +- library/kani/src/internal.rs | 74 ++- library/kani_core/src/lib.rs | 65 ++- .../src/sysroot/contracts/bootstrap.rs | 188 +++--- .../src/sysroot/contracts/check.rs | 367 +++++------- .../src/sysroot/contracts/helpers.rs | 260 +++------ .../src/sysroot/contracts/initialize.rs | 41 +- .../kani_macros/src/sysroot/contracts/mod.rs | 533 +++++++++--------- .../src/sysroot/contracts/replace.rs | 104 ++-- .../src/sysroot/contracts/shared.rs | 104 +--- .../gcd_rec_replacement_pass.expected | 2 +- .../gcd_replacement_pass.expected | 2 +- .../modifies/global_fail.expected | 8 +- .../modifies/havoc_pass.expected | 29 +- .../modifies/havoc_pass_reordered.expected | 25 - .../modifies/simple_fail.expected | 4 +- .../modifies/vec_pass.expected | 10 +- .../expected/function-contract/pattern_use.rs | 3 +- .../simple_replace_pass.expected | 2 +- .../trait_impls/associated_fn.expected | 7 + .../trait_impls/associated_fn.rs | 36 ++ .../trait_impls/methods.expected | 17 + .../function-contract/trait_impls/methods.rs | 67 +++ tests/kani/FunctionContracts/fn_params.rs | 73 +++ .../FunctionContracts/receiver_contracts.rs | 155 +++++ tests/perf/s2n-quic | 2 +- 36 files changed, 1849 insertions(+), 1458 deletions(-) create mode 100644 tests/expected/function-contract/trait_impls/associated_fn.expected create mode 100644 tests/expected/function-contract/trait_impls/associated_fn.rs create mode 100644 tests/expected/function-contract/trait_impls/methods.expected create mode 100644 tests/expected/function-contract/trait_impls/methods.rs create mode 100644 tests/kani/FunctionContracts/fn_params.rs create mode 100644 tests/kani/FunctionContracts/receiver_contracts.rs 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/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/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/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/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 From d6d1ebfdeeb691e3dd8ba86f60ce3663c387af1c Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Thu, 1 Aug 2024 14:18:55 -0700 Subject: [PATCH 2/4] Add missing padding needded for alignment (#3401) This PR adds extra padding for enums when needed for alignment. The missing alignment was exposed in #2857 where the layout size from MIR for `der::error::ErrorKind` was 48 bytes, and from `codegen_enum` was only 41 bytes. The difference turned out to be caused by an 8-byte alignment that the compiler uses for this enum. Resolves #2857 Resolves #3318 --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 19 ++++++++++++++++++- tests/cargo-kani/iss2857/Cargo.toml | 9 +++++++++ tests/cargo-kani/iss2857/expected | 1 + tests/cargo-kani/iss2857/src/main.rs | 13 +++++++++++++ 4 files changed, 41 insertions(+), 1 deletion(-) create mode 100644 tests/cargo-kani/iss2857/Cargo.toml create mode 100644 tests/cargo-kani/iss2857/expected create mode 100644 tests/cargo-kani/iss2857/src/main.rs 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/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() {} From e0141cf09819e90752dca6bf4d1b3cbb59997f17 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 00:05:20 +0200 Subject: [PATCH 3/4] Remove unwind attributes that are no longer needed with CBMC v6 (#3403) CBMC v6 includes https://github.com/diffblue/cbmc/pull/8247, which fixes the need for unwind attributes that were newly found to be necessary when upgrading to nightly-2024-03-15 (#3084). Resolves: #3088 --- docs/src/getting-started/verification-results/src/main.rs | 1 - tests/coverage/unreachable/abort/main.rs | 2 +- tests/expected/abort/main.rs | 1 - tests/expected/iterator/main.rs | 1 - tests/kani/Coroutines/main.rs | 1 - 5 files changed, 1 insertion(+), 5 deletions(-) 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/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/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| { From c7b315f22fa225132c87ab4051a1159b0b8ca08b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 15:18:34 +0200 Subject: [PATCH 4/4] Enable log2*, log10* intrinsics (#3001) Implemented in CBMC in https://github.com/diffblue/cbmc/pull/8195. --- docs/src/rust-feature-support/intrinsics.md | 8 +++---- .../codegen/intrinsic.rs | 8 +++---- tests/kani/Intrinsics/Math/Arith/log10.rs | 23 +++++++++++++++++++ tests/kani/Intrinsics/Math/Arith/log2.rs | 23 +++++++++++++++++++ 4 files changed, 54 insertions(+), 8 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/log10.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/log2.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 49a1f0845ecc..501a9952f05e 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/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 29ea69eeb39b..12352190e6e2 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/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); +}