From 32b37f3957923ad7e909def7f940c30dc3a54888 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 2 Aug 2023 17:24:34 -0700 Subject: [PATCH 01/36] Everything needed for requires/ensures checking --- Cargo.lock | 21 + kani-compiler/Cargo.toml | 1 + .../codegen_cprover_gotoc/overrides/hooks.rs | 35 ++ kani-compiler/src/kani_compiler.rs | 9 +- kani-compiler/src/kani_middle/attributes.rs | 425 +++++++++++----- kani-compiler/src/kani_middle/metadata.rs | 14 +- kani-compiler/src/kani_middle/mod.rs | 11 +- kani-compiler/src/kani_middle/resolve.rs | 8 +- .../src/kani_middle/stubbing/transform.rs | 6 + kani-compiler/src/kani_queries/mod.rs | 6 + kani-compiler/src/parser.rs | 9 + kani-driver/src/args/common.rs | 2 + kani-driver/src/args/mod.rs | 23 +- kani-driver/src/call_single_file.rs | 2 +- kani-driver/src/harness_runner.rs | 2 +- kani-driver/src/metadata.rs | 4 +- library/kani/src/lib.rs | 14 + library/kani_macros/Cargo.toml | 2 +- library/kani_macros/src/lib.rs | 178 ++----- library/kani_macros/src/sysroot.rs | 457 ++++++++++++++++++ .../arbitrary_ensures_fail.expected | 6 + .../arbitrary_ensures_fail.rs | 14 + .../arbitrary_ensures_pass.expected | 6 + .../arbitrary_ensures_pass.rs | 14 + .../arbitrary_requires_fail.expected | 4 + .../arbitrary_requires_fail.rs | 14 + .../arbitrary_requires_pass.expected | 1 + .../arbitrary_requires_pass.rs | 14 + .../checking_from_external_mod.expected | 5 + .../checking_from_external_mod.rs | 17 + .../checking_in_impl.expected | 5 + .../function-contract/checking_in_impl.rs | 21 + .../gcd_failure_code.expected | 9 + .../function-contract/gcd_failure_code.rs | 72 +++ .../gcd_failure_contract.expected | 8 + .../function-contract/gcd_failure_contract.rs | 72 +++ .../function-contract/gcd_success.expected | 6 + .../expected/function-contract/gcd_success.rs | 71 +++ .../simple_ensures_fail.expected | 8 + .../function-contract/simple_ensures_fail.rs | 14 + .../simple_ensures_pass.expected | 6 + .../function-contract/simple_ensures_pass.rs | 14 + tools/compiletest/src/runtest.rs | 42 +- 43 files changed, 1369 insertions(+), 303 deletions(-) create mode 100644 library/kani_macros/src/sysroot.rs create mode 100644 tests/expected/function-contract/arbitrary_ensures_fail.expected create mode 100644 tests/expected/function-contract/arbitrary_ensures_fail.rs create mode 100644 tests/expected/function-contract/arbitrary_ensures_pass.expected create mode 100644 tests/expected/function-contract/arbitrary_ensures_pass.rs create mode 100644 tests/expected/function-contract/arbitrary_requires_fail.expected create mode 100644 tests/expected/function-contract/arbitrary_requires_fail.rs create mode 100644 tests/expected/function-contract/arbitrary_requires_pass.expected create mode 100644 tests/expected/function-contract/arbitrary_requires_pass.rs create mode 100644 tests/expected/function-contract/checking_from_external_mod.expected create mode 100644 tests/expected/function-contract/checking_from_external_mod.rs create mode 100644 tests/expected/function-contract/checking_in_impl.expected create mode 100644 tests/expected/function-contract/checking_in_impl.rs create mode 100644 tests/expected/function-contract/gcd_failure_code.expected create mode 100644 tests/expected/function-contract/gcd_failure_code.rs create mode 100644 tests/expected/function-contract/gcd_failure_contract.expected create mode 100644 tests/expected/function-contract/gcd_failure_contract.rs create mode 100644 tests/expected/function-contract/gcd_success.expected create mode 100644 tests/expected/function-contract/gcd_success.rs create mode 100644 tests/expected/function-contract/simple_ensures_fail.expected create mode 100644 tests/expected/function-contract/simple_ensures_fail.rs create mode 100644 tests/expected/function-contract/simple_ensures_pass.expected create mode 100644 tests/expected/function-contract/simple_ensures_pass.rs diff --git a/Cargo.lock b/Cargo.lock index c1579b23041d..2423a6746ec7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -357,6 +357,26 @@ version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" +[[package]] +name = "enum-map" +version = "2.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9705d8de4776df900a4a0b2384f8b0ab42f775e93b083b42f8ce71bdc32a47e3" +dependencies = [ + "enum-map-derive", +] + +[[package]] +name = "enum-map-derive" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ccb14d927583dd5c2eac0f2cf264fc4762aefe1ae14c47a8a20fc1939d3a5fc0" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.27", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -495,6 +515,7 @@ version = "0.33.0" dependencies = [ "clap", "cprover_bindings", + "enum-map", "home", "itertools", "kani_metadata", diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 23a6b96d18de..6a35fdfff8ea 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -24,6 +24,7 @@ strum_macros = "0.24.0" shell-words = "1.0.0" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} +enum-map = "2.6" # Future proofing: enable backend dependencies using feature. [features] diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 5254394ccbc8..8cb9fa36a8f3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -325,6 +325,40 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { } } +/// A builtin that is essentially a C-style dereference operation. Takes in a +/// `&T` reference and returns a `T` (like clone would but without cloning). +/// Breaks ownership rules and is only used in the context of function contracts +/// where we can structurally guarantee the use is safe. +struct UntrackedDeref; + +impl<'tcx> GotocHook<'tcx> for UntrackedDeref { + fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { + matches_function(tcx, instance, "KaniUntrackedDeref") + } + + fn handle( + &self, + tcx: &mut GotocCtx<'tcx>, + _instance: Instance<'tcx>, + mut fargs: Vec, + assign_to: Place<'tcx>, + _target: Option, + span: Option, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let loc = tcx.codegen_span_option(span); + Stmt::block( + vec![Stmt::assign( + unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) + .goto_expr, + fargs.pop().unwrap().dereference(), + loc, + )], + loc, + ) + } +} + pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { GotocHooks { hooks: vec![ @@ -335,6 +369,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { Rc::new(Nondet), Rc::new(RustAlloc), Rc::new(MemCmp), + Rc::new(UntrackedDeref), ], } } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index a1e231301566..a3157dea8b6d 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -400,6 +400,9 @@ impl Callbacks for KaniCompiler { queries.unstable_features = features.cloned().collect::>(); } + queries.function_contracts_enabled = + queries.unstable_features.iter().any(|s| s == "function-contracts"); + if matches.get_flag(parser::ENABLE_STUBBING) && queries.reachability_analysis == ReachabilityType::Harnesses { @@ -419,7 +422,11 @@ impl Callbacks for KaniCompiler { ) -> Compilation { if self.stage.is_init() { self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| { - check_crate_items(tcx, self.queries.lock().unwrap().ignore_global_asm); + // Extra block necessary to unlock queries + { + let queries = self.queries.lock().unwrap(); + check_crate_items(tcx, &queries); + } self.process_harnesses(tcx) }); } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6ee5136e12e5..c0dbe43406a6 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -5,19 +5,29 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; -use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem}; +use rustc_ast::{ + attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, + NestedMetaItem, +}; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; -use rustc_span::Span; +use rustc_session::Session; +use rustc_span::{Span, Symbol}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; use tracing::{debug, trace}; -use super::resolve; +use crate::kani_queries::QueryDb; -#[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] +use super::resolve::{self, resolve_fn}; + +extern crate enum_map; + +use enum_map::{Enum, EnumMap}; + +#[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord, Enum)] #[strum(serialize_all = "snake_case")] enum KaniAttributeKind { Proof, @@ -27,6 +37,9 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + ProofForContract, + CheckedWith, + ReplacedWith, } impl KaniAttributeKind { @@ -37,66 +50,296 @@ impl KaniAttributeKind { | KaniAttributeKind::ShouldPanic | KaniAttributeKind::Solver | KaniAttributeKind::Stub + | KaniAttributeKind::ProofForContract | KaniAttributeKind::Unwind => true, - KaniAttributeKind::Unstable => false, + KaniAttributeKind::Unstable + | KaniAttributeKind::CheckedWith + | KaniAttributeKind::ReplacedWith => false, } } + + /// Is this attribute kind one of the suite of attributes that form the function contracts API + pub fn is_function_contract_attribute(self) -> bool { + use KaniAttributeKind::*; + matches!(self, CheckedWith | ReplacedWith | ProofForContract) + } } -/// Check that all attributes assigned to an item is valid. -/// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate -/// the session and emit all errors found. -pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) { - let attributes = extract_kani_attributes(tcx, def_id); +/// Bundles together common data used when evaluating the attributes of a given +/// function. +#[derive(Clone)] +pub struct KaniAttributes<'tcx> { + /// Rustc type context/queries + tcx: TyCtxt<'tcx>, + /// The function which these attributes decorate. + item: DefId, + /// All attributes we found in raw format. + map: EnumMap>>, +} - // Check that all attributes are correctly used and well formed. - let is_harness = attributes.contains_key(&KaniAttributeKind::Proof); - for (kind, attrs) in attributes { - if !is_harness && kind.is_harness_only() { - tcx.sess.span_err( - attrs[0].span, - format!( - "the `{}` attribute also requires the `#[kani::proof]` attribute", - kind.as_ref() - ), - ); - } - match kind { - KaniAttributeKind::ShouldPanic => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| { - expect_no_args(tcx, kind, attr); - }) +impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("KaniAttributes") + .field("item", &self.tcx.def_path_debug_str(self.item)) + .field("map", &self.map) + .finish() + } +} + +impl<'tcx> KaniAttributes<'tcx> { + /// Perform preliminary parsing and checking for the attributes on this + /// function + pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self { + let all_attributes = tcx.get_attrs_unchecked(def_id); + let map = all_attributes.iter().fold( + enum_map::enum_map! { _ => >>::None }, + |mut result, attribute| { + // Get the string the appears after "kanitool::" in each attribute string. + // Ex - "proof" | "unwind" etc. + if let Some(kind) = attr_kind(tcx, attribute) { + result[kind].get_or_insert_with(Default::default).push(attribute) + } + result + }, + ); + Self { map, tcx, item: def_id } + } + + /// Expect that at most one attribute of this kind exists on the function + /// and return it. + fn expect_maybe_one(&self, kind: KaniAttributeKind) -> Option<&'tcx Attribute> { + match self.map[kind].as_ref()?.as_slice() { + [one] => Some(one), + _ => { + self.tcx.sess.err(format!( + "Too many {} attributes on {}, expected 0 or 1", + kind.as_ref(), + self.tcx.def_path_debug_str(self.item) + )); + None } - KaniAttributeKind::Solver => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| { - parse_solver(tcx, attr); - }) + } + } + + /// 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 fn for_contract(&self) -> Option<(Symbol, DefId, Span)> { + self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { + let name = expect_key_string_value(self.tcx.sess, target); + let resolved = resolve_fn( + self.tcx, + self.tcx.parent_module_from_def_id(self.item.expect_local()), + name.as_str(), + ); + match resolved { + Err(e) => { + self.tcx.sess.span_err( + target.span, + format!( + "Sould not resolve replacement function {} because {e}", + name.as_str() + ), + ); + None + } + Ok(ok) => Some((name, ok, target.span)), } - KaniAttributeKind::Stub => { - parse_stubs(tcx, def_id, attrs); + }) + } + + /// Check that all attributes assigned to an item is valid. + /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate + /// the session and emit all errors found. + pub(super) fn check_attributes(&self, queries: &QueryDb) { + // Check that all attributes are correctly used and well formed. + let is_harness = self.is_harness(); + for (kind, attrs) in self.map.iter().filter_map(|(k, v)| Some((k, v.as_ref()?))) { + if !is_harness && kind.is_harness_only() { + self.tcx.sess.span_err( + attrs[0].span, + format!( + "the `{}` attribute also requires the `#[kani::proof]` attribute", + kind.as_ref() + ), + ); } - KaniAttributeKind::Unwind => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| { - parse_unwind(tcx, attr); - }) + if kind.is_function_contract_attribute() && !queries.function_contracts_enabled() { + let msg = format!( + "Using the {} attribute requires activating the unstable `function-contracts` feature", + kind.as_ref() + ); + if let Some(attr) = attrs.first() { + self.tcx.sess.span_err(attr.span, msg); + } else { + self.tcx.sess.err(msg); + } } - KaniAttributeKind::Proof => { - expect_single(tcx, kind, &attrs); - attrs.iter().for_each(|attr| check_proof_attribute(tcx, def_id, attr)) + match kind { + KaniAttributeKind::ShouldPanic => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| { + expect_no_args(self.tcx, kind, attr); + }) + } + KaniAttributeKind::Solver => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| { + parse_solver(self.tcx, attr); + }) + } + KaniAttributeKind::Stub => { + parse_stubs(self.tcx, self.item, attrs); + } + KaniAttributeKind::Unwind => { + expect_single(self.tcx, kind, &attrs); + attrs.iter().for_each(|attr| { + parse_unwind(self.tcx, attr); + }) + } + KaniAttributeKind::Proof => { + expect_single(self.tcx, kind, &attrs); + assert!(self.map[KaniAttributeKind::ProofForContract].is_none()); + attrs.iter().for_each(|attr| check_proof_attribute(self.tcx, self.item, attr)) + } + KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { + let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx)); + }), + KaniAttributeKind::ProofForContract => { + assert!(self.map[KaniAttributeKind::Proof].is_none()); + expect_single(self.tcx, kind, &attrs); + } + KaniAttributeKind::ReplacedWith | KaniAttributeKind::CheckedWith => { + self.expect_maybe_one(kind) + .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); + } + }; + } + } + + /// 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. + pub fn check_unstable_features(&self, enabled_features: &[String]) { + if !matches!(self.tcx.type_of(self.item).skip_binder().kind(), TyKind::FnDef(..)) { + // skip closures due to an issue with rustc. + // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 + return; + } + if let Some(unstable_attrs) = self.map[KaniAttributeKind::Unstable].as_ref() { + for attr in unstable_attrs { + let unstable_attr = UnstableAttribute::try_from(*attr).unwrap(); + if !enabled_features.contains(&unstable_attr.feature) { + // Reached an unstable attribute that was not enabled. + report_unstable_forbidden(self.tcx, self.item, &unstable_attr); + } else { + debug!(enabled=?attr, def_id=?self.item, "check_unstable_features"); + } } - KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| { - let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(tcx)); - }), + } + } + + /// Extact the name of the sibling function this contract is checked with + /// (if any) + pub fn checked_with(&self) -> Option { + self.expect_maybe_one(KaniAttributeKind::CheckedWith) + .map(|target| expect_key_string_value(self.tcx.sess, target)) + } + + /// Is this item a harness? (either `proof` or `proof_for_contract` + /// attribute are present) + fn is_harness(&self) -> bool { + self.map[KaniAttributeKind::Proof].is_some() + || self.map[KaniAttributeKind::ProofForContract].is_some() + } + + /// Extract harness attributes for a given `def_id`. + /// + /// We only extract attributes for harnesses that are local to the current crate. + /// Note that all attributes should be valid by now. + pub fn harness_attributes(&self) -> HarnessAttributes { + // Abort if not local. + let Some(local_id) = self.item.as_local() else { + panic!("Expected a local item, but got: {:?}", self.item); }; + trace!(?self, "extract_harness_attributes"); + assert!(self.is_harness()); + let mut attrs = self.map.iter().fold( + HarnessAttributes::default(), + |mut harness, (kind, attributes)| { + let Some(attributes) = attributes.as_ref() else { + return harness; + }; + match kind { + KaniAttributeKind::ShouldPanic => harness.should_panic = true, + KaniAttributeKind::Solver => { + harness.solver = parse_solver(self.tcx, attributes[0]); + } + KaniAttributeKind::Stub => { + harness.stubs = parse_stubs(self.tcx, self.item, attributes); + } + KaniAttributeKind::Unwind => { + harness.unwind_value = parse_unwind(self.tcx, attributes[0]) + } + KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract => { + harness.proof = true + } + KaniAttributeKind::Unstable => { + // Internal attribute which shouldn't exist here. + unreachable!() + } + KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => { + todo!("Contract attributes are not supported on proofs") + } + }; + harness + }, + ); + + let current_module = self.tcx.parent_module_from_def_id(local_id); + attrs.stubs.extend( + self.for_contract() + .and_then(|(name, id, span)| { + let replacement_name = KaniAttributes::for_item(self.tcx, id).checked_with(); + if replacement_name.is_none() { + self.tcx + .sess + .span_err(span, "Target function for this check has no contract"); + } + Some((name, replacement_name?)) + }) + .map(|(original, replacement)| { + let replace_str = replacement.as_str(); + let original_str = original.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, &replacement).unwrap(); + Stub { original: original_str.to_string(), replacement } + }), + ); + attrs } } +fn has_kani_attribute bool>( + tcx: TyCtxt, + def_id: DefId, + predicate: F, +) -> bool { + tcx.get_attrs_unchecked(def_id) + .iter() + .filter_map(|a| attr_kind(tcx, a)) + .any(|attr| predicate(attr)) +} + +/// Same as [`KaniAttributes::is_harness`] but more efficient because less +/// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool { - let attributes = extract_kani_attributes(tcx, def_id); - attributes.contains_key(&KaniAttributeKind::Proof) + has_kani_attribute(tcx, def_id, |a| { + matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract) + }) } /// Does this `def_id` have `#[rustc_test_marker]`? @@ -112,56 +355,24 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { parse_str_value(&marker).unwrap() } -/// Extract harness attributes for a given `def_id`. -/// -/// We only extract attributes for harnesses that are local to the current crate. -/// Note that all attributes should be valid by now. -pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttributes { - // Abort if not local. - assert!(def_id.is_local(), "Expected a local item, but got: {def_id:?}"); - let attributes = extract_kani_attributes(tcx, def_id); - trace!(?def_id, ?attributes, "extract_harness_attributes"); - assert!(attributes.contains_key(&KaniAttributeKind::Proof)); - attributes.into_iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { - match kind { - KaniAttributeKind::ShouldPanic => harness.should_panic = true, - KaniAttributeKind::Solver => { - harness.solver = parse_solver(tcx, attributes[0]); - } - KaniAttributeKind::Stub => { - harness.stubs = parse_stubs(tcx, def_id, attributes); - } - KaniAttributeKind::Unwind => harness.unwind_value = parse_unwind(tcx, attributes[0]), - KaniAttributeKind::Proof => harness.proof = true, - KaniAttributeKind::Unstable => { - // Internal attribute which shouldn't exist here. - unreachable!() - } - }; - harness - }) -} - -/// 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. -pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) { - if !matches!(tcx.type_of(def_id).skip_binder().kind(), TyKind::FnDef(..)) { - // skip closures due to an issue with rustc. - // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 - return; - } - let attributes = extract_kani_attributes(tcx, def_id); - if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) { - for attr in unstable_attrs { - let unstable_attr = UnstableAttribute::try_from(*attr).unwrap(); - if !enabled_features.contains(&unstable_attr.feature) { - // Reached an unstable attribute that was not enabled. - report_unstable_forbidden(tcx, def_id, &unstable_attr); - } else { - debug!(enabled=?attr, ?def_id, "check_unstable_features"); - } - } +/// Expect the contents of this attribute to be of the format #[attribute = +/// "value"] and return the `"value"` +pub fn expect_key_string_value(sess: &Session, attr: &Attribute) -> rustc_span::Symbol { + let span = attr.span; + let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else { + sess.span_fatal(span, "Expected attribute of the form #[attr = \"value\"]") + }; + let maybe_str = match it { + AttrArgsEq::Ast(expr) => match expr.kind { + ExprKind::Lit(tok) => LitKind::from_token_lit(tok).unwrap().str(), + _ => sess.span_fatal(span, "Expected literal string as right hand side of `=`"), + }, + AttrArgsEq::Hir(lit) => lit.kind.str(), + }; + if let Some(str) = maybe_str { + str + } else { + sess.span_fatal(span, "Expected literal string as right hand side of `=`") } } @@ -216,22 +427,6 @@ fn check_proof_attribute(tcx: TyCtxt, def_id: DefId, proof_attribute: &Attribute } } -/// Partition all the attributes according to their kind. -fn extract_kani_attributes( - tcx: TyCtxt, - def_id: DefId, -) -> BTreeMap> { - let all_attributes = tcx.get_attrs_unchecked(def_id); - all_attributes.iter().fold(BTreeMap::default(), |mut result, attribute| { - // Get the string the appears after "kanitool::" in each attribute string. - // Ex - "proof" | "unwind" etc. - if let Some(kind) = attr_kind(tcx, attribute) { - result.entry(kind).or_default().push(attribute) - } - result - }) -} - /// Attribute used to mark a Kani lib API unstable. #[derive(Debug)] struct UnstableAttribute { @@ -328,7 +523,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { } } -fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: Vec<&Attribute>) -> Vec { +fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { let current_module = tcx.parent_module_from_def_id(harness.expect_local()); let check_resolve = |attr: &Attribute, name: &str| { let result = resolve::resolve_fn(tcx, current_module, name); diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 506779001689..d245e934f8a7 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -10,23 +10,23 @@ use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata}; use rustc_hir::def_id::DefId; use rustc_middle::ty::{Instance, InstanceDef, TyCtxt}; -use super::{attributes::extract_harness_attributes, SourceLocation}; +use super::{attributes, SourceLocation}; /// Create the harness metadata for a proof harness for a given function. pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata { - let attributes = extract_harness_attributes(tcx, def_id); + let attributes = attributes::KaniAttributes::for_item(tcx, def_id).harness_attributes(); let pretty_name = tcx.def_path_str(def_id); + let mut mangled_name = tcx.symbol_name(Instance::mono(tcx, def_id)).to_string(); // Main function a special case in order to support `--function main` // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 - let mangled_name = if pretty_name == "main" { - pretty_name.clone() - } else { - tcx.symbol_name(Instance::mono(tcx, def_id)).to_string() + if pretty_name == "main" { + mangled_name = pretty_name.clone() }; let body = tcx.instance_mir(InstanceDef::Item(def_id)); let loc = SourceLocation::new(tcx, &body.span); - let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + let file_stem = + format!("{}_{}", base_name.file_stem().unwrap().to_str().unwrap(), mangled_name); let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); HarnessMetadata { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index ba235db26805..4aca669cddfc 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -25,7 +25,7 @@ use std::fs::File; use std::io::BufWriter; use std::io::Write; -use self::attributes::{check_attributes, check_unstable_features}; +use self::attributes::KaniAttributes; pub mod analysis; pub mod attributes; @@ -39,13 +39,13 @@ pub mod stubbing; /// Check that all crate items are supported and there's no misconfiguration. /// This method will exhaustively print any error / warning and it will abort at the end if any /// error was found. -pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { +pub fn check_crate_items(tcx: TyCtxt, queries: &QueryDb) { let krate = tcx.crate_name(LOCAL_CRATE); for item in tcx.hir_crate_items(()).items() { let def_id = item.owner_id.def_id.to_def_id(); - check_attributes(tcx, def_id); + KaniAttributes::for_item(tcx, def_id).check_attributes(queries); if tcx.def_kind(def_id) == DefKind::GlobalAsm { - if !ignore_asm { + if !queries.ignore_global_asm { let error_msg = format!( "Crate {krate} contains global ASM, which is not supported by Kani. Rerun with \ `--enable-unstable --ignore-global-asm` to suppress this error \ @@ -72,7 +72,8 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) let def_id = item.def_id(); if !def_ids.contains(&def_id) { // Check if any unstable attribute was reached. - check_unstable_features(tcx, &queries.unstable_features, def_id); + KaniAttributes::for_item(tcx, def_id) + .check_unstable_features(&queries.unstable_features); def_ids.insert(def_id); } } diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 5c04089cd200..be9ac1088dba 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -90,6 +90,12 @@ pub enum ResolveError<'tcx> { UnexpectedType { tcx: TyCtxt<'tcx>, item: DefId, expected: &'static str }, } +impl<'tcx> fmt::Debug for ResolveError<'tcx> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + std::fmt::Display::fmt(self, f) + } +} + impl<'tcx> fmt::Display for ResolveError<'tcx> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { @@ -154,7 +160,7 @@ fn resolve_prefix<'tcx>( debug!(?name, ?current_module, "resolve_prefix"); // Split the string into segments separated by `::`. - let mut segments = name.split("::").map(str::to_string).peekable(); + let mut segments = name.split("::").map(|s| s.trim().to_string()).peekable(); assert!(segments.peek().is_some(), "expected identifier, found `{name}`"); // Resolve qualifiers `crate`, initial `::`, and `self`. The qualifier diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs index 2a164623ba24..6e344bd3bebe 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -13,6 +13,7 @@ use regex::Regex; use rustc_data_structures::fingerprint::Fingerprint; use rustc_hir::{def_id::DefId, definitions::DefPathHash}; use rustc_middle::{mir::Body, ty::TyCtxt}; +use tracing::debug; /// Returns the `DefId` of the stub for the function/method identified by the /// parameter `def_id`, and `None` if the function/method is not stubbed. @@ -29,6 +30,11 @@ pub fn transform<'tcx>( old_body: &'tcx Body<'tcx>, ) -> &'tcx Body<'tcx> { if let Some(replacement) = get_stub(tcx, def_id) { + debug!( + original = tcx.def_path_debug_str(def_id), + replaced = tcx.def_path_debug_str(replacement), + "transform" + ); let new_body = tcx.optimized_mir(replacement).clone(); if check_compatibility(tcx, def_id, old_body, replacement, &new_body) { return tcx.arena.alloc(new_body); diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 44573bf124d8..fa88cd0666c4 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -36,6 +36,7 @@ pub struct QueryDb { pub write_json_symtab: bool, pub reachability_analysis: ReachabilityType, pub stubbing_enabled: bool, + pub function_contracts_enabled: bool, pub unstable_features: Vec, /// Information about all target harnesses. @@ -56,4 +57,9 @@ impl QueryDb { pub fn harness_model_path(&self, harness: &DefPathHash) -> Option<&PathBuf> { self.harnesses_info.get(harness) } + + /// Has the `-Zfunction-contracts` option been passed to the driver + pub fn function_contracts_enabled(&self) -> bool { + self.function_contracts_enabled + } } diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index a947fdc61eaa..44945cd80470 100644 --- a/kani-compiler/src/parser.rs +++ b/kani-compiler/src/parser.rs @@ -46,6 +46,9 @@ pub const REACHABILITY: &str = "reachability"; /// Option name used to enable stubbing. pub const ENABLE_STUBBING: &str = "enable-stubbing"; +/// Option name used to enable function contracts +pub const ENABLE_FUNCTION_CONTRACTS: &str = "enable-function-contracts"; + /// Option name used to define unstable features. pub const UNSTABLE_FEATURE: &str = "unstable"; @@ -140,6 +143,12 @@ pub fn parser() -> Command { .help("Instruct the compiler to perform stubbing.") .action(ArgAction::SetTrue), ) + .arg( + Arg::new(ENABLE_FUNCTION_CONTRACTS) + .long(ENABLE_FUNCTION_CONTRACTS) + .help("Allow function contract specification, checking and replacement") + .action(ArgAction::SetTrue), + ) .arg( Arg::new("check-version") .long("check-version") diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index a4325ca610fa..0fb750169750 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -46,6 +46,8 @@ pub enum UnstableFeatures { AsyncLib, /// Enable line coverage instrumentation/reports LineCoverage, + /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) + FunctionContracts, } impl ValidateArgs for CommonArgs { diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 626f2d81be93..905580f0e071 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -24,7 +24,9 @@ use strum::VariantNames; /// Trait used to perform extra validation after parsing. pub trait ValidateArgs { /// Perform post-parsing validation but do not abort. - fn validate(&self) -> Result<(), Error>; + fn validate(&self) -> Result<(), Error> { + Ok(()) + } } /// Validate a set of arguments and ensure they are in a valid state. @@ -180,7 +182,7 @@ pub struct VerificationArgs { /// When specified, the harness filter will only match the exact fully qualified name of a harness #[arg(long, requires("harnesses"))] - pub exact: bool, + exact: bool, /// Link external C files referenced by Rust code. /// This is an experimental feature and requires `-Z c-ffi` to be used @@ -298,7 +300,7 @@ pub struct VerificationArgs { requires("enable_unstable"), conflicts_with("concrete_playback") )] - pub enable_stubbing: bool, + enable_stubbing: bool, /// Enable Kani coverage output alongside verification result #[arg(long, hide_short_help = true)] @@ -344,6 +346,21 @@ impl VerificationArgs { Some(Some(x)) => Some(x), // -j=x } } + + /// Public access to the value set for the `--exact` flag + pub fn exact(&self) -> bool { + self.exact + } + + /// Are experimental function contracts enabled? + pub fn function_contracts_enabled(&self) -> bool { + self.common_args.unstable_features.contains(&UnstableFeatures::FunctionContracts) + } + + /// Is experimental stubing enabled? Implied if function contracts are enabled. + pub fn stubbing_enabled(&self) -> bool { + self.enable_stubbing || self.function_contracts_enabled() + } } #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)] diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 1522071fdefd..299589a31340 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -92,7 +92,7 @@ impl KaniSession { flags.push("--write-json-symtab".into()); } - if self.args.enable_stubbing { + if self.args.stubbing_enabled() { flags.push("--enable-stubbing".into()); } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index fa1aef3d763a..6846a227ea83 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -111,7 +111,7 @@ impl KaniSession { /// Prints a warning at the end of the verification if harness contained a stub but stubs were /// not enabled. fn stubbing_statuses(&self, results: &[HarnessResult]) { - if !self.args.enable_stubbing { + if !self.args.stubbing_enabled() { let ignored_stubs: Vec<_> = results .iter() .filter_map(|result| { diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 871be621c6b0..3e9bc8972897 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -128,10 +128,10 @@ impl KaniSession { Ok(Vec::from(all_harnesses)) } else { let harnesses_found: Vec<&HarnessMetadata> = - find_proof_harnesses(&harnesses, all_harnesses, self.args.exact); + find_proof_harnesses(&harnesses, all_harnesses, self.args.exact()); // If even one harness was not found with --exact, return an error to user - if self.args.exact && harnesses_found.len() < total_harnesses { + if self.args.exact() && harnesses_found.len() < total_harnesses { let harness_found_names: BTreeSet<&String> = harnesses_found.iter().map(|&h| &h.pretty_name).collect(); diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 5ab09d69f9bb..de757cd473b0 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -65,6 +65,20 @@ pub fn assume(cond: bool) { assert!(cond, "`kani::assume` should always hold"); } +/// If the `premise` is true, so must be the `conclusion` +pub fn implies(premise: bool, conclusion: bool) -> bool { + !premise || conclusion +} + +/// A way to break the ownerhip rules. Only used by contracts where we can +/// guarantee it is done safely. +#[inline(never)] +#[doc(hidden)] +#[rustc_diagnostic_item = "KaniUntrackedDeref"] +pub fn untracked_deref(_: &T) -> T { + todo!() +} + /// Creates an assertion of the specified condition and message. /// /// # Example: diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index d4b3ccdc0325..ac4146d63614 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -15,4 +15,4 @@ proc-macro = true proc-macro2 = "1.0" proc-macro-error = "1.0.4" quote = "1.0.20" -syn = { version = "2.0.18", features = ["full"] } +syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 858efc6388d0..8d4e526d9cca 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -7,6 +7,7 @@ // downstream crates to enable these features as well. // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" +#![feature(let_chains, proc_macro_diagnostic, box_patterns)] mod derive; @@ -94,151 +95,43 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } -/// This module implements Kani attributes in a way that only Kani's compiler can understand. -/// This code should only be activated when pre-building Kani's sysroot. -#[cfg(kani_sysroot)] -mod sysroot { - use proc_macro_error::{abort, abort_call_site}; - - use super::*; - - use { - quote::{format_ident, quote}, - syn::parse::{Parse, ParseStream}, - syn::{parse_macro_input, ItemFn}, - }; - - /// Annotate the harness with a #[kanitool::] with optional arguments. - macro_rules! kani_attribute { - ($name:ident) => { - pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { - let args = proc_macro2::TokenStream::from(attr); - let fn_item = parse_macro_input!(item as ItemFn); - let attribute = format_ident!("{}", stringify!($name)); - quote!( - #[kanitool::#attribute(#args)] - #fn_item - ).into() - } - }; - ($name:ident, no_args) => { - pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { - assert!(attr.is_empty(), "`#[kani::{}]` does not take any arguments currently", stringify!($name)); - let fn_item = parse_macro_input!(item as ItemFn); - let attribute = format_ident!("{}", stringify!($name)); - quote!( - #[kanitool::#attribute] - #fn_item - ).into() - } - }; - } - - struct ProofOptions { - schedule: Option, - } - - impl Parse for ProofOptions { - fn parse(input: ParseStream) -> syn::Result { - if input.is_empty() { - Ok(ProofOptions { schedule: None }) - } else { - let ident = input.parse::()?; - if ident != "schedule" { - abort_call_site!("`{}` is not a valid option for `#[kani::proof]`.", ident; - help = "did you mean `schedule`?"; - note = "for now, `schedule` is the only option for `#[kani::proof]`."; - ); - } - let _ = input.parse::()?; - let schedule = Some(input.parse::()?); - Ok(ProofOptions { schedule }) - } - } - } - - pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { - let proof_options = parse_macro_input!(attr as ProofOptions); - let fn_item = parse_macro_input!(item as ItemFn); - let attrs = fn_item.attrs; - let vis = fn_item.vis; - let sig = fn_item.sig; - let body = fn_item.block; - - let kani_attributes = quote!( - #[allow(dead_code)] - #[kanitool::proof] - ); +/// Add a precondition to this function. +/// +/// This is part of the function contract API, together with [`ensures`]. +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function. All Rust syntax is supported, even calling other +/// functions, but the computations must be side effect free, e.g. it cannot +/// perform I/O or use mutable memory. +#[proc_macro_attribute] +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::requires(attr, item) +} - if sig.asyncness.is_none() { - if proof_options.schedule.is_some() { - abort_call_site!( - "`#[kani::proof(schedule = ...)]` can only be used with `async` functions."; - help = "did you mean to make this function `async`?"; - ); - } - // Adds `#[kanitool::proof]` and other attributes - quote!( - #kani_attributes - #(#attrs)* - #vis #sig #body - ) - .into() - } else { - // For async functions, it translates to a synchronous function that calls `kani::block_on`. - // Specifically, it translates - // ```ignore - // #[kani::proof] - // #[attribute] - // pub async fn harness() { ... } - // ``` - // to - // ```ignore - // #[kanitool::proof] - // #[attribute] - // pub fn harness() { - // async fn harness() { ... } - // kani::block_on(harness()) - // // OR - // kani::spawnable_block_on(harness(), schedule) - // // where `schedule` was provided as an argument to `#[kani::proof]`. - // } - // ``` - if !sig.inputs.is_empty() { - abort!( - sig.inputs, - "`#[kani::proof]` cannot be applied to async functions that take arguments for now"; - help = "try removing the arguments"; - ); - } - let mut modified_sig = sig.clone(); - modified_sig.asyncness = None; - let fn_name = &sig.ident; - let schedule = proof_options.schedule; - let block_on_call = if let Some(schedule) = schedule { - quote!(kani::block_on_with_spawn(#fn_name(), #schedule)) - } else { - quote!(kani::block_on(#fn_name())) - }; - quote!( - #kani_attributes - #(#attrs)* - #vis #modified_sig { - #sig #body - #block_on_call - } - ) - .into() - } - } +/// Add a postcondition to this function. +/// +/// This is part of the function contract API, together with [`requires`]. +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function *and* its return value, accessible as a variable called +/// `result`. All Rust syntax is supported, even calling other functions, but +/// the computations must be side effect free, e.g. it cannot perform I/O or use +/// mutable memory. +#[proc_macro_attribute] +pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::ensures(attr, item) +} - kani_attribute!(should_panic, no_args); - kani_attribute!(solver); - kani_attribute!(stub); - kani_attribute!(unstable); - kani_attribute!(unwind); +#[proc_macro_attribute] +pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::proof_for_contract(attr, item) } +/// This module implements Kani attributes in a way that only Kani's compiler can understand. +/// This code should only be activated when pre-building Kani's sysroot. +#[cfg(kani_sysroot)] +mod sysroot; + /// This module provides dummy implementations of Kani attributes which cannot be interpreted by /// other tools such as MIRI and the regular rust compiler. /// @@ -269,4 +162,7 @@ mod regular { no_op!(stub); no_op!(unstable); no_op!(unwind); + no_op!(requires); + no_op!(ensures); + no_op!(proof_for_contract); } diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot.rs new file mode 100644 index 000000000000..763a6ce58598 --- /dev/null +++ b/library/kani_macros/src/sysroot.rs @@ -0,0 +1,457 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +use std::collections::{HashMap, HashSet}; + +use super::*; + +use proc_macro_error::{abort, abort_call_site}; +use { + quote::{format_ident, quote, ToTokens}, + syn::{ + parse::{Parse, ParseStream}, + parse_macro_input, + spanned::Spanned, + visit::Visit, + Expr, ItemFn, PathSegment, + }, +}; + +use proc_macro2::{Ident, Span}; + +/// 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), + } + } +} + +/// Annotate the harness with a #[kanitool::] with optional arguments. +macro_rules! kani_attribute { + ($name:ident) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let fn_item = parse_macro_input!(item as ItemFn); + let attribute = format_ident!("{}", stringify!($name)); + quote!( + #[kanitool::#attribute(#args)] + #fn_item + ).into() + } + }; + ($name:ident, no_args) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + assert!(attr.is_empty(), "`#[kani::{}]` does not take any arguments currently", stringify!($name)); + let fn_item = parse_macro_input!(item as ItemFn); + let attribute = format_ident!("{}", stringify!($name)); + quote!( + #[kanitool::#attribute] + #fn_item + ).into() + } + }; +} + +struct ProofOptions { + schedule: Option, +} + +impl Parse for ProofOptions { + fn parse(input: ParseStream) -> syn::Result { + if input.is_empty() { + Ok(ProofOptions { schedule: None }) + } else { + let ident = input.parse::()?; + if ident != "schedule" { + abort_call_site!("`{}` is not a valid option for `#[kani::proof]`.", ident; + help = "did you mean `schedule`?"; + note = "for now, `schedule` is the only option for `#[kani::proof]`."; + ); + } + let _ = input.parse::()?; + let schedule = Some(input.parse::()?); + Ok(ProofOptions { schedule }) + } + } +} + +pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { + let proof_options = parse_macro_input!(attr as ProofOptions); + let fn_item = parse_macro_input!(item as ItemFn); + let attrs = fn_item.attrs; + let vis = fn_item.vis; + let sig = fn_item.sig; + let body = fn_item.block; + + let kani_attributes = quote!( + #[allow(dead_code)] + #[kanitool::proof] + ); + + if sig.asyncness.is_none() { + if proof_options.schedule.is_some() { + abort_call_site!( + "`#[kani::proof(schedule = ...)]` can only be used with `async` functions."; + help = "did you mean to make this function `async`?"; + ); + } + // Adds `#[kanitool::proof]` and other attributes + quote!( + #kani_attributes + #(#attrs)* + #vis #sig #body + ) + .into() + } else { + // For async functions, it translates to a synchronous function that calls `kani::block_on`. + // Specifically, it translates + // ```ignore + // #[kani::proof] + // #[attribute] + // pub async fn harness() { ... } + // ``` + // to + // ```ignore + // #[kanitool::proof] + // #[attribute] + // pub fn harness() { + // async fn harness() { ... } + // kani::block_on(harness()) + // // OR + // kani::spawnable_block_on(harness(), schedule) + // // where `schedule` was provided as an argument to `#[kani::proof]`. + // } + // ``` + if !sig.inputs.is_empty() { + abort!( + sig.inputs, + "`#[kani::proof]` cannot be applied to async functions that take arguments for now"; + help = "try removing the arguments"; + ); + } + let mut modified_sig = sig.clone(); + modified_sig.asyncness = None; + let fn_name = &sig.ident; + let schedule = proof_options.schedule; + let block_on_call = if let Some(schedule) = schedule { + quote!(kani::block_on_with_spawn(#fn_name(), #schedule)) + } else { + quote!(kani::block_on(#fn_name())) + }; + quote!( + #kani_attributes + #(#attrs)* + #vis #modified_sig { + #sig #body + #block_on_call + } + ) + .into() + } +} + +use syn::visit_mut::VisitMut; + +/// Hash this `TokenStream` and return an integer that is at most digits +/// long when hex formatted. +fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { + use std::hash::Hasher; + let mut hasher = std::collections::hash_map::DefaultHasher::default(); + hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone())); + let long_hash = hasher.finish(); + long_hash % 0x1_000_000 // six hex digits +} + +/// Makes consistent names for a generated function which was created for +/// `purpose`, from an attribute that decorates `related_function` with the +/// hash `hash`. +fn identifier_for_generated_function(related_function: &ItemFn, purpose: &str, hash: u64) -> Ident { + let identifier = format!("{}_{purpose}_{hash:x}", related_function.sig.ident); + Ident::new(&identifier, proc_macro2::Span::mixed_site()) +} + +pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { + //handle_requires_ensures("requires", false, attr, item) + requires_ensures_alt(attr, item, true) +} + +pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { + //handle_requires_ensures("ensures", true, attr, item) + requires_ensures_alt(attr, item, false) +} + +struct SelfDetector(bool); + +impl<'ast> Visit<'ast> for SelfDetector { + fn visit_path(&mut self, i: &'ast syn::Path) { + self.0 |= i.get_ident().map_or(false, |i| i == "self") + || i.get_ident().map_or(false, |i| i == "Self") + } +} + +/// Heyristic to determine if this item originated in some kind of `impl` +fn is_probably_impl_fn(item_fn: &ItemFn) -> bool { + let mut vis = SelfDetector(false); + vis.visit_signature(&item_fn.sig); + vis.0 +} + +/// Collect all named identifiers used in the argument patterns of a function. +struct ArgumentIdentCollector(HashSet); + +impl ArgumentIdentCollector { + fn new() -> Self { + Self(HashSet::new()) + } +} + +impl<'ast> Visit<'ast> for ArgumentIdentCollector { + fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) { + self.0.insert(i.ident.clone()); + syn::visit::visit_pat_ident(self, i) + } + fn visit_receiver(&mut self, _: &'ast syn::Receiver) { + self.0.insert(Ident::new("self", proc_macro2::Span::call_site())); + } +} + +/// Applies the contained renaming to everything visited. +struct Renamer<'a>(&'a HashMap); + +impl<'a> VisitMut for Renamer<'a> { + fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { + if i.path.segments.len() == 1 + && let Some(p) = i.path.segments.first_mut() + && let Some(new) = self.0.get(&p.ident) { + p.ident = new.clone(); + } + } + + /// This restores shadowing. Without this we would rename all ident + /// occurrences, but not the binding location. This is because our + /// [`visit_expr_path_mut`] is scope-unaware. + fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { + if let Some(new) = self.0.get(&i.ident) { + i.ident = new.clone(); + } + } +} + +/// Does the provided path have the same chain of identifiers as `mtch` (match) +/// and no arguments anywhere? +fn matches_path(path: &syn::Path, mtch: &[E]) -> bool +where + Ident: std::cmp::PartialEq, +{ + path.segments.len() == mtch.len() + && path.segments.iter().all(|s| s.arguments.is_empty()) + && path.leading_colon.is_none() + && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) +} + +/// The main meat of handling requires/ensures contracts. +/// +/// Generates a `check__` function that assumes preconditions +/// and asserts postconditions. +/// +/// Decorates the original function with `#[checked_by = +/// "check__"] +/// +/// Each clause (requires or ensures) creates its own check function that calls +/// the prior check function inside. The innermost check function calls a copy +/// of the originally decorated function. It is a copy, because the compiler +/// later replaces all invocations of the original function with this check and +/// that would also apply to the inner check. We need that to be the untouched +/// function though so we make a copy that will survive the replacement from the +/// compiler. +fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { + use syn::{FnArg, Pat, PatIdent, PatType}; + let attr_copy = proc_macro2::TokenStream::from(attr.clone()); + let mut attr = parse_macro_input!(attr as Expr); + + let mut output = proc_macro2::TokenStream::new(); + + let a_short_hash = short_hash_of_token_stream(&item); + + let item_fn = &mut parse_macro_input!(item as ItemFn); + + let item_name = &item_fn.sig.ident.to_string(); + + let mut attrs = std::mem::replace(&mut item_fn.attrs, vec![]); + + let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); + + let mut check_fn_sig = item_fn.sig.clone(); + + check_fn_sig.ident = check_fn_name.clone(); + + // This just collects all the arguments and passes them on. + // TODO: Support patterns. + let args: Vec<_> = item_fn + .sig + .inputs + .iter() + .map(|arg| { + Expr::Path(syn::ExprPath { + attrs: vec![], + qself: None, + path: syn::Path { + leading_colon: None, + segments: [PathSegment { + ident: match arg { + FnArg::Receiver(_) => Ident::new("self", Span::call_site()), + FnArg::Typed(PatType { pat, .. }) => match &**pat { + Pat::Ident(PatIdent { ident, .. }) => ident.clone(), + _ => { + pat.span().unwrap().error("Unexpected pattern").emit(); + unreachable!() + } + }, + }, + arguments: syn::PathArguments::None, + }] + .into_iter() + .collect(), + }, + }) + }) + .collect(); + let is_impl_fn = is_probably_impl_fn(item_fn); + + let mut prior_check = None; + + // We remove any prior `checked_with` or `replaced_with` and use the + // identifiers stored there as the inner functions we will call to in the + // checking and replacing track respectively. + // + // This also maintains the invariant that there is always at most one + // annotation each of `kanitool::{checked_with, replaced_with}` on the + // function, e.g. there is a canonical check/replace. + attrs.retain(|attr| { + if let syn::Meta::NameValue(nv) = &attr.meta { + if matches_path(&nv.path, &["kanitool", "checked_with"]) { + if let syn::Expr::Lit(syn::ExprLit { lit: syn::Lit::Str(strlit), .. }) = &nv.value { + assert!(prior_check.replace(strlit.value()).is_none()); + return false; + } + } + } + true + }); + + let prior_check_fn_name = prior_check.map_or_else( + || { + // If there was no prior check we make a copy and use its name. + let copy_fn_name = identifier_for_generated_function(&item_fn, "copy", a_short_hash); + let mut copy_fn = item_fn.clone(); + copy_fn.sig.ident = copy_fn_name.clone(); + output.extend(copy_fn.into_token_stream()); + copy_fn_name + }, + |prior| Ident::new(&prior, Span::call_site()), + ); + + let call_to_prior = if is_impl_fn { + // If we're in an `impl`, we need to call it with `Self::` + quote!(Self::#prior_check_fn_name(#(#args),*)) + } else { + quote!(#prior_check_fn_name(#(#args),*)) + }; + + let check_body = if is_requires { + quote!( + kani::assume(#attr); + #call_to_prior + ) + } else { + let mut arg_ident_collector = ArgumentIdentCollector::new(); + arg_ident_collector.visit_signature(&item_fn.sig); + + let mk_new_ident_for = + |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); + let arg_idents = arg_ident_collector + .0 + .into_iter() + .map(|i| { + let new = mk_new_ident_for(&i); + (i, new) + }) + .collect::>(); + + let mut ident_rewriter = Renamer(&arg_idents); + ident_rewriter.visit_expr_mut(&mut attr); + + let arg_copy_names = arg_idents.values(); + let arg_idents = arg_idents.keys(); + + quote!( + #(let #arg_copy_names = kani::untracked_deref(&#arg_idents);)* + let result = #call_to_prior; + kani::assert(#attr, stringify!(#attr_copy)); + result + ) + }; + + // Constructing string literals explicitly here, because if we call + // `stringify!` in the generated code that is passed on as that expression to + // the next expansion of a contract, not as the literal. + let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + + // The order of `attrs` and `kanitool::checked_with` is + // important here, because macros are expanded outside in. This way other + // contract annotations in `attrs` sees the `checked_with` + // attribute and can use them. + // + // This way we generate a clean chain of checking and replacing calls. + output.extend(quote!( + #(#attrs)* + #[kanitool::checked_with = #check_fn_name_str] + #item_fn + + #[allow(dead_code)] + #[allow(unused_variables)] + #check_fn_sig { + #check_body + } + )); + output.into() +} + +macro_rules! passthrough { + ($name:ident, $allow_dead_code:ident) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let fn_item = proc_macro2::TokenStream::from(item); + let name = Ident::new(stringify!($name), proc_macro2::Span::call_site()); + let extra_attrs = if $allow_dead_code { + quote!(#[allow(dead_code)]) + } else { + quote!() + }; + quote!( + #extra_attrs + #[kanitool::#name = stringify!(#args)] + #fn_item + ) + .into() + } + } +} + +passthrough!(proof_for_contract, true); + +kani_attribute!(should_panic, no_args); +kani_attribute!(solver); +kani_attribute!(stub); +kani_attribute!(unstable); +kani_attribute!(unwind); diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected new file mode 100644 index 000000000000..50c4de67d4e4 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -0,0 +1,6 @@ +max.assertion + - Status: FAILURE + - Description: "result == x" + arbitrary_ensures_fail.rs:5:1 in function max + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs new file mode 100644 index 000000000000..f0ee72d93da7 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn main() { + let _ = Box::new(9_usize); + max(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected new file mode 100644 index 000000000000..de9de5c66900 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -0,0 +1,6 @@ +max.assertion\ + - Status: SUCCESS\ + - Description: "result == x || result == y"\ + arbitrary_ensures_pass.rs:5:1 in function max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs new file mode 100644 index 000000000000..6611d8f870f7 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_ensures_pass.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result == x || result == y)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn main() { + let _ = Box::new(()); + max(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected new file mode 100644 index 000000000000..e952091ea7ba --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -0,0 +1,4 @@ +assertion\ + - Status: FAILURE\ + - Description: "attempt to divide by zero"\ + arbitrary_requires_fail.rs:7:5 \ No newline at end of file diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs new file mode 100644 index 000000000000..f6729ccab808 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof_for_contract(div)] +fn main() { + let _ = Box::new(()); + div(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/arbitrary_requires_pass.rs b/tests/expected/function-contract/arbitrary_requires_pass.rs new file mode 100644 index 000000000000..eca48fd60fc0 --- /dev/null +++ b/tests/expected/function-contract/arbitrary_requires_pass.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(divisor != 0)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof_for_contract(div)] +fn main() { + let _ = Box::new(()); + div(kani::any(), kani::any()); +} diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected new file mode 100644 index 000000000000..e8a26f75add1 --- /dev/null +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -0,0 +1,5 @@ + - Status: SUCCESS\ + - Description: "(result == x) | (result == y)"\ + checking_from_external_mod.rs:4:1 in function max + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/checking_from_external_mod.rs b/tests/expected/function-contract/checking_from_external_mod.rs new file mode 100644 index 000000000000..ae8ee7869e66 --- /dev/null +++ b/tests/expected/function-contract/checking_from_external_mod.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures((result == x) | (result == y))] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +mod harnesses { + #[kani::proof_for_contract(super::max)] + fn main() { + let _ = Box::new(9_usize); + super::max(7, 6); + } +} + diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected new file mode 100644 index 000000000000..7c89edab9861 --- /dev/null +++ b/tests/expected/function-contract/checking_in_impl.expected @@ -0,0 +1,5 @@ + - Status: SUCCESS\ + - Description: "(result == self) | (result == y)"\ + in function WrappedInt::max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_in_impl.rs b/tests/expected/function-contract/checking_in_impl.rs new file mode 100644 index 000000000000..d4003fd3759c --- /dev/null +++ b/tests/expected/function-contract/checking_in_impl.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +extern crate kani; + +#[derive(Copy, Clone, PartialEq, Eq, kani::Arbitrary)] +struct WrappedInt(u32); + +impl WrappedInt { + #[kani::ensures((result == self) | (result == y))] + fn max(self, y: WrappedInt) -> WrappedInt { + Self(if self.0 > y.0 { self.0 } else { y.0 }) + } +} + +#[kani::proof_for_contract(WrappedInt::max)] +fn main() { + let _ = Box::new(9_usize); + WrappedInt(7).max(WrappedInt(6)); +} diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected new file mode 100644 index 000000000000..3667060a0d14 --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -0,0 +1,9 @@ +gcd.assertion\ + - Status: FAILURE\ + - Description: "result != 0 && x % result == 0 && y % result == 0"\ + gcd_failure_code.rs:8:1 in function gcd + +Failed Checks: result != 0 && x % result == 0 && y % result == 0 + +VERIFICATION:- FAILED + diff --git a/tests/expected/function-contract/gcd_failure_code.rs b/tests/expected/function-contract/gcd_failure_code.rs new file mode 100644 index 000000000000..3b18e168268f --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_code.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + // Added a +1 below to make it no longer satisfy the contract + min = res + 1; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::unwind(12)] +#[kani::proof_for_contract(gcd)] +fn main() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected new file mode 100644 index 000000000000..d87ac1f2ea33 --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -0,0 +1,8 @@ +gcd.assertion\ + - Status: FAILURE\ + - Description: "result != 0 && x % result == 1 && y % result == 0"\ + gcd_failure_contract.rs:9:1 in function gcd\ + +Failed Checks: result != 0 && x % result == 1 && y % result == 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/gcd_failure_contract.rs b/tests/expected/function-contract/gcd_failure_contract.rs new file mode 100644 index 000000000000..633f7cb053fc --- /dev/null +++ b/tests/expected/function-contract/gcd_failure_contract.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +// Changed `0` to `1` in `x % result == 0` to mess with this contract +#[kani::ensures(result != 0 && x % result == 1 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn main() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected new file mode 100644 index 000000000000..c0f567abe518 --- /dev/null +++ b/tests/expected/function-contract/gcd_success.expected @@ -0,0 +1,6 @@ +gcd.assertion\ + - Status: SUCCESS\ + - Description: "result != 0 && x % result == 0 && y % result == 0"\ + gcd_success.rs:8:1 in function gcd + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs new file mode 100644 index 000000000000..dbd2a8c9d90e --- /dev/null +++ b/tests/expected/function-contract/gcd_success.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +type T = u8; + +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(result != 0 && x % result == 0 && y % result == 0)] +fn gcd(x: T, y: T) -> T { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + loop { + let res = max % min; + if res == 0 { + return min; + } + + max = min; + min = res; + } +} + +struct Frac { + pub num: T, + pub den: T, +} + +impl Frac { + // constructor + pub fn new(num: T, den: T) -> Self { + Frac { num, den } + } + + /// Method to simplify fraction + /// For example, `Frac { num: 10, den: 15 }` gets simplified to + /// `Frac { num: 2, num: 3 }` + pub fn simplify(&self) -> Frac { + let gcd = gcd(self.num, self.den); + Frac::new(self.num / gcd, self.den / gcd) + } + + pub fn check_equals(&self, f2: Frac) { + assert_eq!(self.num % f2.num, 0); + assert_eq!(self.den % f2.den, 0); + let gcd1 = self.num / f2.num; + let gcd2 = self.den / f2.den; + assert_eq!(gcd1, gcd2); + } +} + +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn main() { + // Needed to avoid having `free` be removed as unused function. This is + // because DFCC contract enforcement assumes that a definition for `free` + // exists. + let _ = Box::new(9_usize); + let num: T = kani::any(); + let den: T = kani::any(); + kani::assume(num != 0); + kani::assume(den != 0); + let frac = Frac::new(num, den); + let simplified_frac = frac.simplify(); + frac.check_equals(simplified_frac); +} diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected new file mode 100644 index 000000000000..3bae72c0766c --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -0,0 +1,8 @@ +max.assertion\ + - Status: FAILURE\ + - Description: "result == x"\ + simple_ensures_fail.rs:5:1 in function max + +Failed Checks: result == x + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs new file mode 100644 index 000000000000..442a5e962168 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result == x)] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn main() { + let _ = Box::new(9_usize); + max(7, 9); +} diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected new file mode 100644 index 000000000000..395b7c75fc05 --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -0,0 +1,6 @@ +max.assertion\ + - Status: SUCCESS\ + - Description: "(result == x) | (result == y)"\ + simple_ensures_pass.rs:5:1 in function max + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs new file mode 100644 index 000000000000..63b22d3eccdc --- /dev/null +++ b/tests/expected/function-contract/simple_ensures_pass.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures((result == x) | (result == y))] +fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } +} + +#[kani::proof_for_contract(max)] +fn main() { + let _ = Box::new(9_usize); + max(7, 6); +} diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 7fad336dffdc..d914d1a0970f 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -395,7 +395,12 @@ impl<'test> TestCx<'test> { /// the expected output in `expected` file. fn run_expected_test(&self) { let proc_res = self.run_kani(); - let expected_path = self.testpaths.file.parent().unwrap().join("expected"); + let dot_expected_path = self.testpaths.file.with_extension("expected"); + let expected_path = if dot_expected_path.exists() { + dot_expected_path + } else { + self.testpaths.file.parent().unwrap().join("expected") + }; self.verify_output(&proc_res, &expected_path); } @@ -475,35 +480,22 @@ impl<'test> TestCx<'test> { consecutive_lines.clear(); } } - None + // Someone may add a `\` to the last line (probably by accident) but + // that would mean this test would succeed without actually testing so + // we add a check here again. + (!consecutive_lines.is_empty() && !TestCx::contains(str, &consecutive_lines)) + .then_some(consecutive_lines) } /// Check if there is a set of consecutive lines in `str` where each line /// contains a line from `lines` fn contains(str: &[&str], lines: &[&str]) -> bool { - let mut i = str.iter(); - while let Some(output_line) = i.next() { - if output_line.contains(&lines[0]) { - // Check if the rest of the lines in `lines` are contained in - // the subsequent lines in `str` - let mut matches = true; - // Clone the iterator so that we keep i unchanged - let mut j = i.clone(); - for line in lines.iter().skip(1) { - if let Some(output_line) = j.next() { - if output_line.contains(line) { - continue; - } - } - matches = false; - break; - } - if matches { - return true; - } - } - } - false + // Does *any* subslice of length `lines.len()` satisfy the containment of + // *all* `lines` + // `trim()` added to ignore trailing and preceding whitespace + str.windows(lines.len()).any(|subslice| { + subslice.iter().zip(lines).all(|(output, expected)| output.contains(expected.trim())) + }) } fn create_stamp(&self) { From a2535d71aaec589ccc0a3968fe974c9038197e69 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 2 Aug 2023 20:40:25 -0700 Subject: [PATCH 02/36] Formatting --- library/kani_macros/src/sysroot.rs | 6 +++--- .../function-contract/checking_from_external_mod.rs | 1 - 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot.rs index 763a6ce58598..b05c41083508 100644 --- a/library/kani_macros/src/sysroot.rs +++ b/library/kani_macros/src/sysroot.rs @@ -260,13 +260,13 @@ where } /// The main meat of handling requires/ensures contracts. -/// +/// /// Generates a `check__` function that assumes preconditions /// and asserts postconditions. -/// +/// /// Decorates the original function with `#[checked_by = /// "check__"] -/// +/// /// Each clause (requires or ensures) creates its own check function that calls /// the prior check function inside. The innermost check function calls a copy /// of the originally decorated function. It is a copy, because the compiler diff --git a/tests/expected/function-contract/checking_from_external_mod.rs b/tests/expected/function-contract/checking_from_external_mod.rs index ae8ee7869e66..c26be92ed5e9 100644 --- a/tests/expected/function-contract/checking_from_external_mod.rs +++ b/tests/expected/function-contract/checking_from_external_mod.rs @@ -14,4 +14,3 @@ mod harnesses { super::max(7, 6); } } - From 624f406aae015808a70b6ef4a1bca9e9828ad4c5 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 2 Aug 2023 21:22:30 -0700 Subject: [PATCH 03/36] =?UTF-8?q?The=20only=20clippy=20suggestion=20?= =?UTF-8?q?=F0=9F=99=8C=F0=9F=8F=BB?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- kani-compiler/src/kani_middle/attributes.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index c0dbe43406a6..d43e03974490 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -331,7 +331,7 @@ fn has_kani_attribute bool>( tcx.get_attrs_unchecked(def_id) .iter() .filter_map(|a| attr_kind(tcx, a)) - .any(|attr| predicate(attr)) + .any(predicate) } /// Same as [`KaniAttributes::is_harness`] but more efficient because less From 5a4ad83eadf936a5935bbedaba894a13ea0b581b Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 2 Aug 2023 21:24:44 -0700 Subject: [PATCH 04/36] Adjust test case --- .../function-contract/checking_from_external_mod.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected index e8a26f75add1..baafd591ad2e 100644 --- a/tests/expected/function-contract/checking_from_external_mod.expected +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -1,5 +1,5 @@ - Status: SUCCESS\ - Description: "(result == x) | (result == y)"\ - checking_from_external_mod.rs:4:1 in function max + checking_from_external_mod.rs:5:1 in function max VERIFICATION:- SUCCESSFUL \ No newline at end of file From a272350200fee15048aafa0a1e20486b7a8bce13 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 2 Aug 2023 21:32:27 -0700 Subject: [PATCH 05/36] Seriously? --- kani-compiler/src/kani_middle/attributes.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d43e03974490..b7cde838a464 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -328,10 +328,7 @@ fn has_kani_attribute bool>( def_id: DefId, predicate: F, ) -> bool { - tcx.get_attrs_unchecked(def_id) - .iter() - .filter_map(|a| attr_kind(tcx, a)) - .any(predicate) + tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) } /// Same as [`KaniAttributes::is_harness`] but more efficient because less From f0a011b5389b37df59bdaf76a3ddd804a51ec31a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 3 Aug 2023 13:16:25 -0700 Subject: [PATCH 06/36] A check for mutable pointers --- kani-compiler/src/kani_middle/attributes.rs | 86 ++++++++++++++++++- .../prohibit_pointers.expected | 5 ++ .../function-contract/prohibit_pointers.rs | 51 +++++++++++ 3 files changed, 138 insertions(+), 4 deletions(-) create mode 100644 tests/expected/function-contract/prohibit_pointers.expected create mode 100644 tests/expected/function-contract/prohibit_pointers.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index b7cde838a464..d7a8d9ef30c4 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -11,7 +11,10 @@ use rustc_ast::{ }; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; -use rustc_middle::ty::{Instance, TyCtxt, TyKind}; +use rustc_middle::{ + mir, + ty::{self, Instance, TyCtxt, TyKind}, +}; use rustc_session::Session; use rustc_span::{Span, Symbol}; use std::str::FromStr; @@ -59,9 +62,16 @@ impl KaniAttributeKind { } /// Is this attribute kind one of the suite of attributes that form the function contracts API - pub fn is_function_contract_attribute(self) -> bool { + pub fn is_function_contract_api(self) -> bool { + use KaniAttributeKind::*; + self.is_function_contract() || matches!(self, ProofForContract) + } + + /// Would this attribute be placed on a function as part of a function + /// contract. + pub fn is_function_contract(self) -> bool { use KaniAttributeKind::*; - matches!(self, CheckedWith | ReplacedWith | ProofForContract) + matches!(self, CheckedWith | ReplacedWith) } } @@ -164,7 +174,7 @@ impl<'tcx> KaniAttributes<'tcx> { ), ); } - if kind.is_function_contract_attribute() && !queries.function_contracts_enabled() { + if kind.is_function_contract_api() && !queries.function_contracts_enabled() { let msg = format!( "Using the {} attribute requires activating the unstable `function-contracts` feature", kind.as_ref() @@ -175,6 +185,9 @@ impl<'tcx> KaniAttributes<'tcx> { self.tcx.sess.err(msg); } } + if kind.is_function_contract() { + check_is_contract_safe(self.tcx, self.item); + } match kind { KaniAttributeKind::ShouldPanic => { expect_single(self.tcx, kind, &attrs); @@ -323,6 +336,71 @@ impl<'tcx> KaniAttributes<'tcx> { } } +/// A basic check that ensures a function with a contract does not receive +/// mutable pointers in its input and does not return raw pointers of any kind. +/// +/// This is a temporary safety measure because contracts cannot yet reasona +/// about those structures. +fn check_is_contract_safe(tcx: TyCtxt, item: DefId) { + use ty::TypeVisitor; + struct NoMutPtr<'tcx> { + tcx: TyCtxt<'tcx>, + span: Span, + is_prohibited: fn(ty::Ty<'tcx>) -> bool, + r#where: &'static str, + what: &'static str, + } + + impl<'tcx> TypeVisitor> for NoMutPtr<'tcx> { + fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> std::ops::ControlFlow { + use ty::TypeSuperVisitable; + if (self.is_prohibited)(t) { + self.tcx.sess.span_err(self.span, format!("{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); + } + + // Rust's type visitor only recursese into basically generics. Which + // menas it won't look at the field types of e.g. a struct or enum. + // So we override it here and do that ourselves. + // + // Since the field types also go over all the type variables + // implicitly we don't need to call back to `super` in this case. + if let ty::TyKind::Adt(adt_def, generics) = t.kind() { + for variant in adt_def.variants() { + for field in &variant.fields { + let ctrl = self.visit_ty(field.ty(self.tcx, generics)); + if ctrl.is_break() { + // Technically we can just ignore this because we + // know this case will never happen, but just to be + // safe. + return ctrl; + } + } + } + std::ops::ControlFlow::Continue(()) + } else { + t.super_visit_with(self) + } + } + } + + fn is_raw_mutable_ptr(t: ty::Ty) -> bool { + matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) + } + + let body = tcx.optimized_mir(item); + + for (arg, (is_prohibited, r#where, what)) in body + .args_iter() + .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable "))) + .chain([(mir::RETURN_PLACE, (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))]) + { + let decl = &body.local_decls[arg]; + let span = decl.source_info.span; + let mut v = NoMutPtr { tcx, span, is_prohibited, r#where, what }; + v.visit_ty(decl.ty); + } +} + fn has_kani_attribute bool>( tcx: TyCtxt, def_id: DefId, diff --git a/tests/expected/function-contract/prohibit_pointers.expected b/tests/expected/function-contract/prohibit_pointers.expected new file mode 100644 index 000000000000..fd4c9cc4d9c9 --- /dev/null +++ b/tests/expected/function-contract/prohibit_pointers.expected @@ -0,0 +1,5 @@ +error: Function argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. + +error: Function argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. + +error: Function argument contains a return pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit_pointers.rs b/tests/expected/function-contract/prohibit_pointers.rs new file mode 100644 index 000000000000..e6e4ed25bf90 --- /dev/null +++ b/tests/expected/function-contract/prohibit_pointers.rs @@ -0,0 +1,51 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +struct HidesAPointer(*mut u32); + +#[kani::ensures(true)] +fn hidden_pointer(h: HidesAPointer) {} + +#[kani::proof_for_contract(hidden_pointer)] +fn harness() {} + +#[kani::ensures(true)] +fn plain_pointer(t: *mut i32) {} + +#[kani::proof_for_contract(plain_pointer)] +fn plain_ptr_harness() {} + +#[kani::ensures(true)] +fn return_pointer() -> *const usize { + unreachable!() +} + +#[kani::proof_for_contract(return_pointer)] +fn return_ptr_harness() {} + +#[kani::ensures(true)] +fn allowed_pointer(t: *const bool) {} + +#[kani::proof_for_contract(allowed_pointer)] +fn allowed_pointer_harness() {} + +#[kani::ensures(true)] +fn allowed_mut_ref(t: &mut bool) {} + +#[kani::proof_for_contract(allowed_mut_ref)] +fn allowed_mut_ref_harness() {} + +#[kani::ensures(true)] +fn allowed_ref(t: &bool) {} + +#[kani::proof_for_contract(allowed_ref)] +fn allowed_ref_harness() {} + +#[kani::ensures(true)] +fn allowed_mut_return_ref<'a>() -> &'a mut bool { + unreachable!() +} + +#[kani::proof_for_contract(allowed_mut_return_ref)] +fn allowed_mut_return_ref_harness() {} From 14295645c5ad454c30f5cb638d7d6807a0161876 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 3 Aug 2023 14:31:20 -0700 Subject: [PATCH 07/36] Whoops had forgotten to update the test case after updating the error message --- .../expected/function-contract/prohibit_pointers.expected | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/expected/function-contract/prohibit_pointers.expected b/tests/expected/function-contract/prohibit_pointers.expected index fd4c9cc4d9c9..a0f864710118 100644 --- a/tests/expected/function-contract/prohibit_pointers.expected +++ b/tests/expected/function-contract/prohibit_pointers.expected @@ -1,5 +1,3 @@ -error: Function argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. - -error: Function argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. - -error: Function argument contains a return pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file +error: This argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. +error: This argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. +error: The return contains a pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file From 1dd96dc949122ef95efd757d06f5294835d56611 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 3 Aug 2023 21:52:18 -0700 Subject: [PATCH 08/36] Last minute pivot in check function implementation --- kani-compiler/src/kani_middle/attributes.rs | 26 ++- library/kani_macros/src/sysroot.rs | 216 ++++++++---------- .../function-contract/pattern_use.expected | 4 + .../expected/function-contract/pattern_use.rs | 14 ++ 4 files changed, 138 insertions(+), 122 deletions(-) create mode 100644 tests/expected/function-contract/pattern_use.expected create mode 100644 tests/expected/function-contract/pattern_use.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d7a8d9ef30c4..b823924b37f1 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -43,6 +43,7 @@ enum KaniAttributeKind { ProofForContract, CheckedWith, ReplacedWith, + IsContractGenerated, } impl KaniAttributeKind { @@ -57,6 +58,7 @@ impl KaniAttributeKind { | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable | KaniAttributeKind::CheckedWith + | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::ReplacedWith => false, } } @@ -71,7 +73,7 @@ impl KaniAttributeKind { /// contract. pub fn is_function_contract(self) -> bool { use KaniAttributeKind::*; - matches!(self, CheckedWith | ReplacedWith) + matches!(self, CheckedWith | ReplacedWith | IsContractGenerated) } } @@ -226,6 +228,11 @@ impl<'tcx> KaniAttributes<'tcx> { self.expect_maybe_one(kind) .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); } + KaniAttributeKind::IsContractGenerated => { + // Ignored here because this is only used by the proc macros + // to communicate with one another. So by the time it gets + // here we don't care if it's valid or not. + } }; } } @@ -301,7 +308,9 @@ impl<'tcx> KaniAttributes<'tcx> { // Internal attribute which shouldn't exist here. unreachable!() } - KaniAttributeKind::CheckedWith | KaniAttributeKind::ReplacedWith => { + KaniAttributeKind::CheckedWith + | KaniAttributeKind::ReplacedWith + | KaniAttributeKind::IsContractGenerated => { todo!("Contract attributes are not supported on proofs") } }; @@ -358,12 +367,14 @@ fn check_is_contract_safe(tcx: TyCtxt, item: DefId) { self.tcx.sess.span_err(self.span, format!("{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); } - // Rust's type visitor only recursese into basically generics. Which - // menas it won't look at the field types of e.g. a struct or enum. - // So we override it here and do that ourselves. + // Rust's type visitor only recurses into type arguments, (e.g. + // `generics` in this match). This is enough for may types, but it + // won't look at the field types of structs or enums. So we override + // it here and do that ourselves. // - // Since the field types also go over all the type variables - // implicitly we don't need to call back to `super` in this case. + // Since the field types also must contain in some form all the type + // arguments the visitor will see them as it inspects the fields and + // we don't need to call back to `super`. if let ty::TyKind::Adt(adt_def, generics) = t.kind() { for variant in adt_def.variants() { for field in &variant.fields { @@ -378,6 +389,7 @@ fn check_is_contract_safe(tcx: TyCtxt, item: DefId) { } std::ops::ControlFlow::Continue(()) } else { + // For every other type t.super_visit_with(self) } } diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot.rs index b05c41083508..e8216667e217 100644 --- a/library/kani_macros/src/sysroot.rs +++ b/library/kani_macros/src/sysroot.rs @@ -12,7 +12,7 @@ use { parse_macro_input, spanned::Spanned, visit::Visit, - Expr, ItemFn, PathSegment, + Expr, ItemFn, }, }; @@ -190,22 +190,6 @@ pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { requires_ensures_alt(attr, item, false) } -struct SelfDetector(bool); - -impl<'ast> Visit<'ast> for SelfDetector { - fn visit_path(&mut self, i: &'ast syn::Path) { - self.0 |= i.get_ident().map_or(false, |i| i == "self") - || i.get_ident().map_or(false, |i| i == "Self") - } -} - -/// Heyristic to determine if this item originated in some kind of `impl` -fn is_probably_impl_fn(item_fn: &ItemFn) -> bool { - let mut vis = SelfDetector(false); - vis.visit_signature(&item_fn.sig); - vis.0 -} - /// Collect all named identifiers used in the argument patterns of a function. struct ArgumentIdentCollector(HashSet); @@ -259,6 +243,37 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } +#[derive(Clone, Copy, PartialEq, Eq)] +enum ContractFunctionState { + Original, + Untouched, + Check, +} + +impl ContractFunctionState { + fn from_attribute(attribute: &syn::Attribute) -> Option { + if let syn::Meta::List(lst) = &attribute.meta { + if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) { + match syn::parse2::(lst.tokens.clone()) { + Err(e) => { + lst.span().unwrap().error(format!("{e}")).emit(); + } + Ok(ident) => { + if ident.to_string() == "check" { + return Some(Self::Check); + } else { + lst.span().unwrap().error("Expected `check` ident").emit(); + } + } + } + } else if matches_path(&lst.path, &["kanitool", "checked_with"]) { + return Some(ContractFunctionState::Original); + } + } + None + } +} + /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions @@ -274,8 +289,10 @@ where /// that would also apply to the inner check. We need that to be the untouched /// function though so we make a copy that will survive the replacement from the /// compiler. +/// +/// # Complete example +/// fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { - use syn::{FnArg, Pat, PatIdent, PatType}; let attr_copy = proc_macro2::TokenStream::from(attr.clone()); let mut attr = parse_macro_input!(attr as Expr); @@ -285,88 +302,64 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let item_fn = &mut parse_macro_input!(item as ItemFn); - let item_name = &item_fn.sig.ident.to_string(); - - let mut attrs = std::mem::replace(&mut item_fn.attrs, vec![]); - - let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); - - let mut check_fn_sig = item_fn.sig.clone(); - - check_fn_sig.ident = check_fn_name.clone(); - - // This just collects all the arguments and passes them on. - // TODO: Support patterns. - let args: Vec<_> = item_fn - .sig - .inputs + // If we didn't find any other contract handling related attributes we + // assume this function has not been touched by a contract before. + let function_state = item_fn + .attrs .iter() - .map(|arg| { - Expr::Path(syn::ExprPath { - attrs: vec![], - qself: None, - path: syn::Path { - leading_colon: None, - segments: [PathSegment { - ident: match arg { - FnArg::Receiver(_) => Ident::new("self", Span::call_site()), - FnArg::Typed(PatType { pat, .. }) => match &**pat { - Pat::Ident(PatIdent { ident, .. }) => ident.clone(), - _ => { - pat.span().unwrap().error("Unexpected pattern").emit(); - unreachable!() - } - }, - }, - arguments: syn::PathArguments::None, - }] - .into_iter() - .collect(), - }, - }) - }) - .collect(); - let is_impl_fn = is_probably_impl_fn(item_fn); - - let mut prior_check = None; - - // We remove any prior `checked_with` or `replaced_with` and use the - // identifiers stored there as the inner functions we will call to in the - // checking and replacing track respectively. - // - // This also maintains the invariant that there is always at most one - // annotation each of `kanitool::{checked_with, replaced_with}` on the - // function, e.g. there is a canonical check/replace. - attrs.retain(|attr| { - if let syn::Meta::NameValue(nv) = &attr.meta { - if matches_path(&nv.path, &["kanitool", "checked_with"]) { - if let syn::Expr::Lit(syn::ExprLit { lit: syn::Lit::Str(strlit), .. }) = &nv.value { - assert!(prior_check.replace(strlit.value()).is_none()); - return false; - } - } - } - true - }); - - let prior_check_fn_name = prior_check.map_or_else( - || { - // If there was no prior check we make a copy and use its name. - let copy_fn_name = identifier_for_generated_function(&item_fn, "copy", a_short_hash); - let mut copy_fn = item_fn.clone(); - copy_fn.sig.ident = copy_fn_name.clone(); - output.extend(copy_fn.into_token_stream()); - copy_fn_name - }, - |prior| Ident::new(&prior, Span::call_site()), - ); + .find_map(ContractFunctionState::from_attribute) + .unwrap_or(ContractFunctionState::Untouched); + + if matches!(function_state, ContractFunctionState::Original) { + // If we're the original function that means we're *not* the first time + // that a contract attribute is handled on this function. This means + // there must exist a generated check function somewhere onto which the + // attributes have been copied and where they will be expanded into more + // checks. So we just return outselves unchanged. + return item_fn.into_token_stream().into(); + } - let call_to_prior = if is_impl_fn { - // If we're in an `impl`, we need to call it with `Self::` - quote!(Self::#prior_check_fn_name(#(#args),*)) - } else { - quote!(#prior_check_fn_name(#(#args),*)) - }; + let attrs = std::mem::replace(&mut item_fn.attrs, vec![]); + + if matches!(function_state, ContractFunctionState::Untouched) { + // We are the first time a contract is handled on this function, so + // we're responsible for + // + // 1. Generating a name for the check function + // 2. Emitting the original, unchanged item and register the check + // function on it via attribute + // 3. Renaming our item to the new name + // 4. And adding #[kanitool::is_contract_generated(check)], + // #[allow(dead_code)] and #[allow(unused_variables)] to the check + // function attributes + + // The order of `attrs` and `kanitool::{checked_with, + // is_contract_generated}` is important here, because macros are + // expanded outside in. This way other contract annotations in + // `attrs` sees those attribuites which they need to determine + // `function_state` attribute and can use them. + // + // The same applies later when we emit the check function. + let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); + + // Constructing string literals explicitly here, because if we call + // `stringify!` in the generated code that is passed on as that + // expression to the next expansion of a contract, not as the + // literal. + let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + output.extend(quote!( + #(#attrs)* + #[kanitool::checked_with = #check_fn_name_str] + #item_fn + + #[allow(dead_code)] + #[allow(unused_variables)] + #[kanitool::is_contract_generated(check)] + )); + item_fn.sig.ident = check_fn_name; + } + + let call_to_prior = &item_fn.block; let check_body = if is_requires { quote!( @@ -374,6 +367,10 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) #call_to_prior ) } else { + // This machinery here is responsible for making shallow, unsafe copies + // of the arguments that are accessed by the postconditions. This is so + // that the return value can mutably borrow from the arguments without + // Rust complaining. let mut arg_ident_collector = ArgumentIdentCollector::new(); arg_ident_collector.visit_signature(&item_fn.sig); @@ -392,35 +389,24 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) ident_rewriter.visit_expr_mut(&mut attr); let arg_copy_names = arg_idents.values(); + let also_arg_copy_names = arg_copy_names.clone(); let arg_idents = arg_idents.keys(); quote!( #(let #arg_copy_names = kani::untracked_deref(&#arg_idents);)* let result = #call_to_prior; kani::assert(#attr, stringify!(#attr_copy)); + #(std::mem::forget(#also_arg_copy_names);)* result ) }; - // Constructing string literals explicitly here, because if we call - // `stringify!` in the generated code that is passed on as that expression to - // the next expansion of a contract, not as the literal. - let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); - - // The order of `attrs` and `kanitool::checked_with` is - // important here, because macros are expanded outside in. This way other - // contract annotations in `attrs` sees the `checked_with` - // attribute and can use them. - // - // This way we generate a clean chain of checking and replacing calls. + let sig = &item_fn.sig; + + // Finally emit the check function. output.extend(quote!( #(#attrs)* - #[kanitool::checked_with = #check_fn_name_str] - #item_fn - - #[allow(dead_code)] - #[allow(unused_variables)] - #check_fn_sig { + #sig { #check_body } )); diff --git a/tests/expected/function-contract/pattern_use.expected b/tests/expected/function-contract/pattern_use.expected new file mode 100644 index 000000000000..0b42466d5cac --- /dev/null +++ b/tests/expected/function-contract/pattern_use.expected @@ -0,0 +1,4 @@ +assertion\ + - Status: FAILURE\ + - Description: "attempt to divide by zero"\ + pattern_use.rs:7:5 \ No newline at end of file diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs new file mode 100644 index 000000000000..98ff9d27e39a --- /dev/null +++ b/tests/expected/function-contract/pattern_use.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(result <= dividend)] +fn div((dividend, divisor): (u32, u32)) -> u32 { + dividend / divisor +} + +#[kani::proof_for_contract(div)] +fn main() { + let _ = Box::new(()); + div((kani::any(), kani::any())); +} From 78739d85bcdb3f345329ff63296e1e41b240cd39 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 3 Aug 2023 23:13:29 -0700 Subject: [PATCH 09/36] Postcondition injection on every return --- library/kani_macros/src/lib.rs | 2 +- library/kani_macros/src/sysroot.rs | 72 +++++++++++++++++++++++++----- 2 files changed, 62 insertions(+), 12 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 8d4e526d9cca..1bdb8bb3b49c 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -129,7 +129,7 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. -#[cfg(kani_sysroot)] +//#[cfg(kani_sysroot)] mod sysroot; /// This module provides dummy implementations of Kani attributes which cannot be interpreted by diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot.rs index e8216667e217..3ae620f2e5a8 100644 --- a/library/kani_macros/src/sysroot.rs +++ b/library/kani_macros/src/sysroot.rs @@ -16,7 +16,7 @@ use { }, }; -use proc_macro2::{Ident, Span}; +use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; /// Create a unique hash for a token stream (basically a [`std::hash::Hash`] /// impl for `proc_macro2::TokenStream`). @@ -160,7 +160,7 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { } } -use syn::visit_mut::VisitMut; +use syn::{visit_mut::VisitMut, ExprBlock}; /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. @@ -243,14 +243,22 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } +/// Classifies the state a function is in in the contract handling pipeline. #[derive(Clone, Copy, PartialEq, Eq)] enum ContractFunctionState { + /// This is the original code, re-emitted from a contract attribute Original, + /// This is the first time a contract attribute is evaluated on this + /// function Untouched, + /// This is a check function that was generated from a previous evaluation + /// of a contract attribute Check, } impl ContractFunctionState { + /// Find out if this attribute could be describing a "contract handling" + /// state and if so return it. fn from_attribute(attribute: &syn::Attribute) -> Option { if let syn::Meta::List(lst) = &attribute.meta { if matches_path(&lst.path, &["kanitool", "is_contract_generated"]) { @@ -266,7 +274,10 @@ impl ContractFunctionState { } } } - } else if matches_path(&lst.path, &["kanitool", "checked_with"]) { + } + } + if let syn::Meta::NameValue(nv) = &attribute.meta { + if matches_path(&nv.path, &["kanitool", "checked_with"]) { return Some(ContractFunctionState::Original); } } @@ -274,6 +285,32 @@ impl ContractFunctionState { } } +struct PostconditionInjector(TokenStream2); + +impl VisitMut for PostconditionInjector { + fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) { + // Empty because inside the closure we don't want to inject + } + + fn visit_expr_mut(&mut self, i: &mut Expr) { + if let syn::Expr::Return(r) = i { + let tokens = self.0.clone(); + let mut output = TokenStream2::new(); + if let Some(expr) = &mut r.expr { + output.extend(quote!(let result = #expr;)); + *expr = Box::new(Expr::Verbatim(quote!(result))); + } + *i = syn::Expr::Verbatim(quote!( + #output + #tokens + #i + )) + } else { + syn::visit_mut::visit_expr_mut(self, i) + } + } +} + /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions @@ -329,9 +366,8 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) // 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 adding #[kanitool::is_contract_generated(check)], - // #[allow(dead_code)] and #[allow(unused_variables)] to the check - // function attributes + // 4. And (minor point) adding #[allow(dead_code)] and + // #[allow(unused_variables)] to the check function attributes // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are @@ -354,12 +390,11 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) #[allow(dead_code)] #[allow(unused_variables)] - #[kanitool::is_contract_generated(check)] )); item_fn.sig.ident = check_fn_name; } - let call_to_prior = &item_fn.block; + let call_to_prior = &mut item_fn.block; let check_body = if is_requires { quote!( @@ -392,20 +427,35 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let also_arg_copy_names = arg_copy_names.clone(); let arg_idents = arg_idents.keys(); + let exec_postconditions = quote!( + kani::assert(#attr, stringify!(#attr_copy)); + #(std::mem::forget(#also_arg_copy_names);)* + ); + + let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); + + inject_conditions.visit_block_mut(&mut *call_to_prior); + quote!( #(let #arg_copy_names = kani::untracked_deref(&#arg_idents);)* let result = #call_to_prior; - kani::assert(#attr, stringify!(#attr_copy)); - #(std::mem::forget(#also_arg_copy_names);)* + #exec_postconditions result ) }; let sig = &item_fn.sig; - // Finally emit the check function. output.extend(quote!( #(#attrs)* + )); + + if matches!(function_state, ContractFunctionState::Untouched) { + output.extend(quote!(#[kanitool::is_contract_generated(check)])); + } + + // Finally emit the check function. + output.extend(quote!( #sig { #check_body } From 81cd5c8eca4efaca2e4dc7ecaf3e6b23729e8e78 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 3 Aug 2023 23:18:19 -0700 Subject: [PATCH 10/36] Whoops --- library/kani_macros/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 1bdb8bb3b49c..8d4e526d9cca 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -129,7 +129,7 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. -//#[cfg(kani_sysroot)] +#[cfg(kani_sysroot)] mod sysroot; /// This module provides dummy implementations of Kani attributes which cannot be interpreted by From e07eec9639a91b83c635529b6fd46065e3c76474 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 4 Aug 2023 10:19:49 -0700 Subject: [PATCH 11/36] Documentation and emit block in injector --- library/kani_macros/src/sysroot.rs | 62 +++++++++++++++++++++++++----- 1 file changed, 53 insertions(+), 9 deletions(-) diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot.rs index 3ae620f2e5a8..cf7525f4c21e 100644 --- a/library/kani_macros/src/sysroot.rs +++ b/library/kani_macros/src/sysroot.rs @@ -285,6 +285,24 @@ impl ContractFunctionState { } } +/// A visitor which injects a copy of the token stream it holds before every +/// `return` expression. +/// +/// This is intended to be used with postconditions and for that purpose it also +/// performs a rewrite where the return value is first bound to `result` so the +/// postconditions can access it. +/// +/// # Example +/// +/// The expression `return x;` turns into +/// +/// ```rs +/// { // Always opens a new block +/// let result = x; +/// +/// return result; +/// } +/// ``` struct PostconditionInjector(TokenStream2); impl VisitMut for PostconditionInjector { @@ -300,11 +318,11 @@ impl VisitMut for PostconditionInjector { output.extend(quote!(let result = #expr;)); *expr = Box::new(Expr::Verbatim(quote!(result))); } - *i = syn::Expr::Verbatim(quote!( + *i = syn::Expr::Verbatim(quote!({ #output #tokens #i - )) + })) } else { syn::visit_mut::visit_expr_mut(self, i) } @@ -319,16 +337,42 @@ impl VisitMut for PostconditionInjector { /// Decorates the original function with `#[checked_by = /// "check__"] /// -/// Each clause (requires or ensures) creates its own check function that calls -/// the prior check function inside. The innermost check function calls a copy -/// of the originally decorated function. It is a copy, because the compiler -/// later replaces all invocations of the original function with this check and -/// that would also apply to the inner check. We need that to be the untouched -/// function though so we make a copy that will survive the replacement from the -/// compiler. +/// The check function is a copy of the original function with pre and +/// postconditions added before and after respectively. Each clause (requires or +/// ensures) adds new layers of pre or postconditions to the check function. +/// +/// Postconditions are also injected before every `return` expression, see also +/// [`PostconditionInjector`]. +/// +/// All arguments of the function are unsafely shallow-copied with the +/// `kani::unsafe_deref` function. We must ensure that those copies are not +/// dropped so after the postconditions we call `mem::forget` on each copy. /// /// # Complete example +/// +/// ```rs +/// +/// ``` +/// +/// Turns into /// +/// ```rs +/// #[kanitool::checked_with = "div_check_965916"] +/// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +/// +/// #[allow(dead_code)] +/// #[allow(unused_variables)] +/// #[kanitool::is_contract_generated(check)] +/// fn div_check_965916(dividend: u32, divisor: u32) -> u32 { +/// let dividend_renamed = kani::untracked_deref(÷nd); +/// let divisor_renamed = kani::untracked_deref(&divisor); +/// let result = { kani::assume(divisor != 0); { dividend / divisor } }; +/// kani::assert(result <= dividend_renamed, "result <= dividend"); +/// std::mem::forget(dividend_renamed); +/// std::mem::forget(divisor_renamed); +/// result +/// } +/// ``` fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { let attr_copy = proc_macro2::TokenStream::from(attr.clone()); let mut attr = parse_macro_input!(attr as Expr); From 9b2d9a0f91622b2f3a66afe685b8aaf9504cda08 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 4 Aug 2023 10:39:39 -0700 Subject: [PATCH 12/36] Incorporate more sysroot comments. --- library/kani_macros/src/sysroot.rs | 93 +++++++++++++++++------------- 1 file changed, 53 insertions(+), 40 deletions(-) diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot.rs index cf7525f4c21e..78a7e6603f32 100644 --- a/library/kani_macros/src/sysroot.rs +++ b/library/kani_macros/src/sysroot.rs @@ -160,7 +160,7 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { } } -use syn::{visit_mut::VisitMut, ExprBlock}; +use syn::visit_mut::VisitMut; /// Hash this `TokenStream` and return an integer that is at most digits /// long when hex formatted. @@ -209,15 +209,20 @@ impl<'ast> Visit<'ast> for ArgumentIdentCollector { } } -/// Applies the contained renaming to everything visited. +/// Applies the contained renaming to every ident pattern and ident expr +/// visited. +/// +/// In each case if the path has only one segments that corresponds to a key, it +/// is replaced by the ident in the value. struct Renamer<'a>(&'a HashMap); impl<'a> VisitMut for Renamer<'a> { fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { - if i.path.segments.len() == 1 - && let Some(p) = i.path.segments.first_mut() - && let Some(new) = self.0.get(&p.ident) { - p.ident = new.clone(); + if i.path.segments.len() == 1 { + i.path + .segments + .first_mut() + .and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone())); } } @@ -286,16 +291,16 @@ impl ContractFunctionState { } /// A visitor which injects a copy of the token stream it holds before every -/// `return` expression. -/// +/// `return` expression. +/// /// This is intended to be used with postconditions and for that purpose it also /// performs a rewrite where the return value is first bound to `result` so the /// postconditions can access it. -/// +/// /// # Example -/// +/// /// The expression `return x;` turns into -/// +/// /// ```rs /// { // Always opens a new block /// let result = x; @@ -329,6 +334,34 @@ impl VisitMut for PostconditionInjector { } } +/// A supporting function for creating shallow, unsafe copies of the arguments +/// for the postconditions. +/// +/// This function +/// - collects all [`Ident`]s found in the argument patterns +/// - creates new names for them +/// - Replaces all occurrences of those idents in `attrs` with the new names and +/// - Returns the mapping of old names to new names so the macro can emit the +/// code that makes the copies. +fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { + let mut arg_ident_collector = ArgumentIdentCollector::new(); + arg_ident_collector.visit_signature(&sig); + + let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); + let arg_idents = arg_ident_collector + .0 + .into_iter() + .map(|i| { + let new = mk_new_ident_for(&i); + (i, new) + }) + .collect::>(); + + let mut ident_rewriter = Renamer(&arg_idents); + ident_rewriter.visit_expr_mut(attr); + arg_idents +} + /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions @@ -339,27 +372,27 @@ impl VisitMut for PostconditionInjector { /// /// The check function is a copy of the original function with pre and /// postconditions added before and after respectively. Each clause (requires or -/// ensures) adds new layers of pre or postconditions to the check function. -/// +/// ensures) adds new layers of pre or postconditions to the check function. +/// /// Postconditions are also injected before every `return` expression, see also /// [`PostconditionInjector`]. -/// +/// /// All arguments of the function are unsafely shallow-copied with the -/// `kani::unsafe_deref` function. We must ensure that those copies are not +/// `kani::untracked_deref` function. We must ensure that those copies are not /// dropped so after the postconditions we call `mem::forget` on each copy. /// /// # Complete example -/// +/// /// ```rs -/// +/// /// ``` -/// +/// /// Turns into /// /// ```rs /// #[kanitool::checked_with = "div_check_965916"] /// fn div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } -/// +/// /// #[allow(dead_code)] /// #[allow(unused_variables)] /// #[kanitool::is_contract_generated(check)] @@ -380,7 +413,6 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let mut output = proc_macro2::TokenStream::new(); let a_short_hash = short_hash_of_token_stream(&item); - let item_fn = &mut parse_macro_input!(item as ItemFn); // If we didn't find any other contract handling related attributes we @@ -446,26 +478,7 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) #call_to_prior ) } else { - // This machinery here is responsible for making shallow, unsafe copies - // of the arguments that are accessed by the postconditions. This is so - // that the return value can mutably borrow from the arguments without - // Rust complaining. - let mut arg_ident_collector = ArgumentIdentCollector::new(); - arg_ident_collector.visit_signature(&item_fn.sig); - - let mk_new_ident_for = - |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); - let arg_idents = arg_ident_collector - .0 - .into_iter() - .map(|i| { - let new = mk_new_ident_for(&i); - (i, new) - }) - .collect::>(); - - let mut ident_rewriter = Renamer(&arg_idents); - ident_rewriter.visit_expr_mut(&mut attr); + let arg_idents = rename_argument_occurences(&item_fn.sig, &mut attr); let arg_copy_names = arg_idents.values(); let also_arg_copy_names = arg_copy_names.clone(); From 01dfbc04a57d21ecfec687391848bc5fe552562e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 4 Aug 2023 10:50:49 -0700 Subject: [PATCH 13/36] More comments addressed --- .../src/codegen_cprover_gotoc/overrides/hooks.rs | 11 +++++++---- kani-compiler/src/kani_compiler.rs | 6 +----- kani-driver/src/args/mod.rs | 6 +++--- kani-driver/src/call_single_file.rs | 2 +- kani-driver/src/harness_runner.rs | 2 +- 5 files changed, 13 insertions(+), 14 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 8cb9fa36a8f3..f91ea60a0e60 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -325,10 +325,13 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { } } -/// A builtin that is essentially a C-style dereference operation. Takes in a -/// `&T` reference and returns a `T` (like clone would but without cloning). -/// Breaks ownership rules and is only used in the context of function contracts -/// where we can structurally guarantee the use is safe. +/// A builtin that is essentially a C-style dereference operation, creating an +/// unsafe challow copy. Importantly either this copy or the original needs to +/// be `mem::forget`en or a double-free will occur. +/// +/// Takes in a `&T` reference and returns a `T` (like clone would but without +/// cloning). Breaks ownership rules and is only used in the context of function +/// contracts where we can structurally guarantee the use is safe. struct UntrackedDeref; impl<'tcx> GotocHook<'tcx> for UntrackedDeref { diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index a3157dea8b6d..2d4966f9ce2a 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -422,11 +422,7 @@ impl Callbacks for KaniCompiler { ) -> Compilation { if self.stage.is_init() { self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| { - // Extra block necessary to unlock queries - { - let queries = self.queries.lock().unwrap(); - check_crate_items(tcx, &queries); - } + check_crate_items(tcx, &self.queries.lock().unwrap()); self.process_harnesses(tcx) }); } diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 905580f0e071..e73ff931523c 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -353,13 +353,13 @@ impl VerificationArgs { } /// Are experimental function contracts enabled? - pub fn function_contracts_enabled(&self) -> bool { + pub fn is_function_contracts_enabled(&self) -> bool { self.common_args.unstable_features.contains(&UnstableFeatures::FunctionContracts) } /// Is experimental stubing enabled? Implied if function contracts are enabled. - pub fn stubbing_enabled(&self) -> bool { - self.enable_stubbing || self.function_contracts_enabled() + pub fn is_stubbing_enabled(&self) -> bool { + self.enable_stubbing || self.is_function_contracts_enabled() } } diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 299589a31340..30cdf88db835 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -92,7 +92,7 @@ impl KaniSession { flags.push("--write-json-symtab".into()); } - if self.args.stubbing_enabled() { + if self.args.is_stubbing_enabled() { flags.push("--enable-stubbing".into()); } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 6846a227ea83..7730168de63f 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -111,7 +111,7 @@ impl KaniSession { /// Prints a warning at the end of the verification if harness contained a stub but stubs were /// not enabled. fn stubbing_statuses(&self, results: &[HarnessResult]) { - if !self.args.stubbing_enabled() { + if !self.args.is_stubbing_enabled() { let ignored_stubs: Vec<_> = results .iter() .filter_map(|result| { From 16b9cc565af3bf37978d02218595264bf6794819 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 4 Aug 2023 10:51:09 -0700 Subject: [PATCH 14/36] Whitespace --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index f91ea60a0e60..3d99f8cdeb3a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -328,7 +328,7 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { /// A builtin that is essentially a C-style dereference operation, creating an /// unsafe challow copy. Importantly either this copy or the original needs to /// be `mem::forget`en or a double-free will occur. -/// +/// /// Takes in a `&T` reference and returns a `T` (like clone would but without /// cloning). Breaks ownership rules and is only used in the context of function /// contracts where we can structurally guarantee the use is safe. From 5ee744ca53487d1c9d430a433f7ba3b6afd60c55 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 9 Aug 2023 11:34:37 -0700 Subject: [PATCH 15/36] Reverting proc macro refactoring --- library/kani_macros/src/lib.rs | 146 +++++++++++++++++- .../src/{sysroot.rs => sysroot/contracts.rs} | 138 +---------------- 2 files changed, 149 insertions(+), 135 deletions(-) rename library/kani_macros/src/{sysroot.rs => sysroot/contracts.rs} (76%) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 8d4e526d9cca..53f235ba2699 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -130,7 +130,151 @@ pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] -mod sysroot; +mod sysroot { + use proc_macro_error::{abort, abort_call_site}; + + mod contracts; + + pub use contracts::{proof_for_contract, requires, ensures}; + + use super::*; + + use { + quote::{format_ident, quote}, + syn::parse::{Parse, ParseStream}, + syn::{parse_macro_input, ItemFn}, + }; + + /// Annotate the harness with a #[kanitool::] with optional arguments. + macro_rules! kani_attribute { + ($name:ident) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let fn_item = parse_macro_input!(item as ItemFn); + let attribute = format_ident!("{}", stringify!($name)); + quote!( + #[kanitool::#attribute(#args)] + #fn_item + ).into() + } + }; + ($name:ident, no_args) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + assert!(attr.is_empty(), "`#[kani::{}]` does not take any arguments currently", stringify!($name)); + let fn_item = parse_macro_input!(item as ItemFn); + let attribute = format_ident!("{}", stringify!($name)); + quote!( + #[kanitool::#attribute] + #fn_item + ).into() + } + }; + } + + struct ProofOptions { + schedule: Option, + } + + impl Parse for ProofOptions { + fn parse(input: ParseStream) -> syn::Result { + if input.is_empty() { + Ok(ProofOptions { schedule: None }) + } else { + let ident = input.parse::()?; + if ident != "schedule" { + abort_call_site!("`{}` is not a valid option for `#[kani::proof]`.", ident; + help = "did you mean `schedule`?"; + note = "for now, `schedule` is the only option for `#[kani::proof]`."; + ); + } + let _ = input.parse::()?; + let schedule = Some(input.parse::()?); + Ok(ProofOptions { schedule }) + } + } + } + + pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { + let proof_options = parse_macro_input!(attr as ProofOptions); + let fn_item = parse_macro_input!(item as ItemFn); + let attrs = fn_item.attrs; + let vis = fn_item.vis; + let sig = fn_item.sig; + let body = fn_item.block; + + let kani_attributes = quote!( + #[allow(dead_code)] + #[kanitool::proof] + ); + + if sig.asyncness.is_none() { + if proof_options.schedule.is_some() { + abort_call_site!( + "`#[kani::proof(schedule = ...)]` can only be used with `async` functions."; + help = "did you mean to make this function `async`?"; + ); + } + // Adds `#[kanitool::proof]` and other attributes + quote!( + #kani_attributes + #(#attrs)* + #vis #sig #body + ) + .into() + } else { + // For async functions, it translates to a synchronous function that calls `kani::block_on`. + // Specifically, it translates + // ```ignore + // #[kani::proof] + // #[attribute] + // pub async fn harness() { ... } + // ``` + // to + // ```ignore + // #[kanitool::proof] + // #[attribute] + // pub fn harness() { + // async fn harness() { ... } + // kani::block_on(harness()) + // // OR + // kani::spawnable_block_on(harness(), schedule) + // // where `schedule` was provided as an argument to `#[kani::proof]`. + // } + // ``` + if !sig.inputs.is_empty() { + abort!( + sig.inputs, + "`#[kani::proof]` cannot be applied to async functions that take arguments for now"; + help = "try removing the arguments"; + ); + } + let mut modified_sig = sig.clone(); + modified_sig.asyncness = None; + let fn_name = &sig.ident; + let schedule = proof_options.schedule; + let block_on_call = if let Some(schedule) = schedule { + quote!(kani::block_on_with_spawn(#fn_name(), #schedule)) + } else { + quote!(kani::block_on(#fn_name())) + }; + quote!( + #kani_attributes + #(#attrs)* + #vis #modified_sig { + #sig #body + #block_on_call + } + ) + .into() + } + } + + kani_attribute!(should_panic, no_args); + kani_attribute!(solver); + kani_attribute!(stub); + kani_attribute!(unstable); + kani_attribute!(unwind); +} /// This module provides dummy implementations of Kani attributes which cannot be interpreted by /// other tools such as MIRI and the regular rust compiler. diff --git a/library/kani_macros/src/sysroot.rs b/library/kani_macros/src/sysroot/contracts.rs similarity index 76% rename from library/kani_macros/src/sysroot.rs rename to library/kani_macros/src/sysroot/contracts.rs index 78a7e6603f32..f7faa9fd797b 100644 --- a/library/kani_macros/src/sysroot.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -4,11 +4,9 @@ use std::collections::{HashMap, HashSet}; use super::*; -use proc_macro_error::{abort, abort_call_site}; use { - quote::{format_ident, quote, ToTokens}, + quote::{quote, ToTokens}, syn::{ - parse::{Parse, ParseStream}, parse_macro_input, spanned::Spanned, visit::Visit, @@ -36,130 +34,6 @@ fn hash_of_token_stream(hasher: &mut H, stream: proc_macro } } -/// Annotate the harness with a #[kanitool::] with optional arguments. -macro_rules! kani_attribute { - ($name:ident) => { - pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { - let args = proc_macro2::TokenStream::from(attr); - let fn_item = parse_macro_input!(item as ItemFn); - let attribute = format_ident!("{}", stringify!($name)); - quote!( - #[kanitool::#attribute(#args)] - #fn_item - ).into() - } - }; - ($name:ident, no_args) => { - pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { - assert!(attr.is_empty(), "`#[kani::{}]` does not take any arguments currently", stringify!($name)); - let fn_item = parse_macro_input!(item as ItemFn); - let attribute = format_ident!("{}", stringify!($name)); - quote!( - #[kanitool::#attribute] - #fn_item - ).into() - } - }; -} - -struct ProofOptions { - schedule: Option, -} - -impl Parse for ProofOptions { - fn parse(input: ParseStream) -> syn::Result { - if input.is_empty() { - Ok(ProofOptions { schedule: None }) - } else { - let ident = input.parse::()?; - if ident != "schedule" { - abort_call_site!("`{}` is not a valid option for `#[kani::proof]`.", ident; - help = "did you mean `schedule`?"; - note = "for now, `schedule` is the only option for `#[kani::proof]`."; - ); - } - let _ = input.parse::()?; - let schedule = Some(input.parse::()?); - Ok(ProofOptions { schedule }) - } - } -} - -pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { - let proof_options = parse_macro_input!(attr as ProofOptions); - let fn_item = parse_macro_input!(item as ItemFn); - let attrs = fn_item.attrs; - let vis = fn_item.vis; - let sig = fn_item.sig; - let body = fn_item.block; - - let kani_attributes = quote!( - #[allow(dead_code)] - #[kanitool::proof] - ); - - if sig.asyncness.is_none() { - if proof_options.schedule.is_some() { - abort_call_site!( - "`#[kani::proof(schedule = ...)]` can only be used with `async` functions."; - help = "did you mean to make this function `async`?"; - ); - } - // Adds `#[kanitool::proof]` and other attributes - quote!( - #kani_attributes - #(#attrs)* - #vis #sig #body - ) - .into() - } else { - // For async functions, it translates to a synchronous function that calls `kani::block_on`. - // Specifically, it translates - // ```ignore - // #[kani::proof] - // #[attribute] - // pub async fn harness() { ... } - // ``` - // to - // ```ignore - // #[kanitool::proof] - // #[attribute] - // pub fn harness() { - // async fn harness() { ... } - // kani::block_on(harness()) - // // OR - // kani::spawnable_block_on(harness(), schedule) - // // where `schedule` was provided as an argument to `#[kani::proof]`. - // } - // ``` - if !sig.inputs.is_empty() { - abort!( - sig.inputs, - "`#[kani::proof]` cannot be applied to async functions that take arguments for now"; - help = "try removing the arguments"; - ); - } - let mut modified_sig = sig.clone(); - modified_sig.asyncness = None; - let fn_name = &sig.ident; - let schedule = proof_options.schedule; - let block_on_call = if let Some(schedule) = schedule { - quote!(kani::block_on_with_spawn(#fn_name(), #schedule)) - } else { - quote!(kani::block_on(#fn_name())) - }; - quote!( - #kani_attributes - #(#attrs)* - #vis #modified_sig { - #sig #body - #block_on_call - } - ) - .into() - } -} - use syn::visit_mut::VisitMut; /// Hash this `TokenStream` and return an integer that is at most digits @@ -520,6 +394,8 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) output.into() } +/// This is very similar to the kani_attribute macro, but it instead creates +/// key-value style attributes which I find a little easier to parse. macro_rules! passthrough { ($name:ident, $allow_dead_code:ident) => { pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { @@ -541,10 +417,4 @@ macro_rules! passthrough { } } -passthrough!(proof_for_contract, true); - -kani_attribute!(should_panic, no_args); -kani_attribute!(solver); -kani_attribute!(stub); -kani_attribute!(unstable); -kani_attribute!(unwind); +passthrough!(proof_for_contract, true); \ No newline at end of file From fe71b62bb4a605d147ab934bfef8342f02ef197b Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 10 Aug 2023 15:14:16 -0700 Subject: [PATCH 16/36] Apply suggestions from code review Co-authored-by: Celina G. Val --- kani-compiler/src/kani_middle/attributes.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index d1a19895bda6..99448d9629f6 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -147,7 +147,7 @@ impl<'tcx> KaniAttributes<'tcx> { self.tcx.sess.span_err( target.span, format!( - "Sould not resolve replacement function {} because {e}", + "Failed to resolve replacement function {} because {e}", name.as_str() ), ); From 387280f7293e7fdca3ae65d4b25816a3fd92827e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 10 Aug 2023 15:02:23 -0700 Subject: [PATCH 17/36] Reformatting tests after celina's feeback --- kani-driver/src/args/mod.rs | 7 +------ kani-driver/src/metadata.rs | 4 ++-- library/kani/src/lib.rs | 9 +++++++++ .../function-contract/arbitrary_ensures_fail.expected | 8 ++++---- .../function-contract/arbitrary_ensures_pass.expected | 6 +++--- .../function-contract/arbitrary_requires_fail.expected | 6 +++--- .../checking_from_external_mod.expected | 6 +++--- .../expected/function-contract/checking_in_impl.expected | 6 +++--- .../expected/function-contract/gcd_failure_code.expected | 6 +++--- .../function-contract/gcd_failure_contract.expected | 6 +++--- tests/expected/function-contract/gcd_success.expected | 6 +++--- tests/expected/function-contract/pattern_use.expected | 5 ++--- .../function-contract/simple_ensures_fail.expected | 6 +++--- .../function-contract/simple_ensures_pass.expected | 6 +++--- 14 files changed, 45 insertions(+), 42 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 5e36272e5b72..0ce6e5571664 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -182,7 +182,7 @@ pub struct VerificationArgs { /// When specified, the harness filter will only match the exact fully qualified name of a harness #[arg(long, requires("harnesses"))] - exact: bool, + pub exact: bool, /// Link external C files referenced by Rust code. /// This is an experimental feature and requires `-Z c-ffi` to be used @@ -348,11 +348,6 @@ impl VerificationArgs { } } - /// Public access to the value set for the `--exact` flag - pub fn exact(&self) -> bool { - self.exact - } - /// Are experimental function contracts enabled? pub fn is_function_contracts_enabled(&self) -> bool { self.common_args.unstable_features.contains(&UnstableFeatures::FunctionContracts) diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 3e9bc8972897..871be621c6b0 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -128,10 +128,10 @@ impl KaniSession { Ok(Vec::from(all_harnesses)) } else { let harnesses_found: Vec<&HarnessMetadata> = - find_proof_harnesses(&harnesses, all_harnesses, self.args.exact()); + find_proof_harnesses(&harnesses, all_harnesses, self.args.exact); // If even one harness was not found with --exact, return an error to user - if self.args.exact() && harnesses_found.len() < total_harnesses { + if self.args.exact && harnesses_found.len() < total_harnesses { let harness_found_names: BTreeSet<&String> = harnesses_found.iter().map(|&h| &h.pretty_name).collect(); diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index de757cd473b0..fada07b38305 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -66,6 +66,15 @@ pub fn assume(cond: bool) { } /// If the `premise` is true, so must be the `conclusion` +/// +/// Note that boolean operators (such as `||`) are evaluated lazily by Rust. +/// This function is not and both conditions will be evaluated always. As a +/// reult this function is not intended to be used in regular code. Instead it +/// is intended to make implications in a function function contract +/// ([`requires`], [`ensures`]) more readable. For eample +/// `implies(self.is_empty(), self.len() == 0)` is a little easier to understand +/// than `!self.is_empty() || self.len() == 0` (which is the inlined definition +/// of this function). pub fn implies(premise: bool, conclusion: bool) -> bool { !premise || conclusion } diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.expected b/tests/expected/function-contract/arbitrary_ensures_fail.expected index 50c4de67d4e4..587dc3f46975 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.expected +++ b/tests/expected/function-contract/arbitrary_ensures_fail.expected @@ -1,6 +1,6 @@ -max.assertion - - Status: FAILURE - - Description: "result == x" - arbitrary_ensures_fail.rs:5:1 in function max +max.assertion\ +- Status: FAILURE\ +- Description: "result == x"\ +in function max VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.expected b/tests/expected/function-contract/arbitrary_ensures_pass.expected index de9de5c66900..af1e09d1fe62 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.expected +++ b/tests/expected/function-contract/arbitrary_ensures_pass.expected @@ -1,6 +1,6 @@ max.assertion\ - - Status: SUCCESS\ - - Description: "result == x || result == y"\ - arbitrary_ensures_pass.rs:5:1 in function max +- Status: SUCCESS\ +- Description: "result == x || result == y"\ +in function max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected index e952091ea7ba..d388a4b084f4 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.expected +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -1,4 +1,4 @@ assertion\ - - Status: FAILURE\ - - Description: "attempt to divide by zero"\ - arbitrary_requires_fail.rs:7:5 \ No newline at end of file +- Status: FAILURE\ +- Description: "attempt to divide by zero"\ +arbitrary_requires_fail.rs:7:5 \ No newline at end of file diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected index baafd591ad2e..99a44f49ab82 100644 --- a/tests/expected/function-contract/checking_from_external_mod.expected +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -1,5 +1,5 @@ - - Status: SUCCESS\ - - Description: "(result == x) | (result == y)"\ - checking_from_external_mod.rs:5:1 in function max +- Status: SUCCESS\ +- Description: "(result == x) | (result == y)"\ +in function max VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/checking_in_impl.expected b/tests/expected/function-contract/checking_in_impl.expected index 7c89edab9861..d5a390be8425 100644 --- a/tests/expected/function-contract/checking_in_impl.expected +++ b/tests/expected/function-contract/checking_in_impl.expected @@ -1,5 +1,5 @@ - - Status: SUCCESS\ - - Description: "(result == self) | (result == y)"\ - in function WrappedInt::max +- Status: SUCCESS\ +- Description: "(result == self) | (result == y)"\ +in function WrappedInt::max VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected index 3667060a0d14..4112115e2a01 100644 --- a/tests/expected/function-contract/gcd_failure_code.expected +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -1,7 +1,7 @@ gcd.assertion\ - - Status: FAILURE\ - - Description: "result != 0 && x % result == 0 && y % result == 0"\ - gcd_failure_code.rs:8:1 in function gcd +- Status: FAILURE\ +- Description: "result != 0 && x % result == 0 && y % result == 0"\ +in function gcd Failed Checks: result != 0 && x % result == 0 && y % result == 0 diff --git a/tests/expected/function-contract/gcd_failure_contract.expected b/tests/expected/function-contract/gcd_failure_contract.expected index d87ac1f2ea33..3ae94b199d6e 100644 --- a/tests/expected/function-contract/gcd_failure_contract.expected +++ b/tests/expected/function-contract/gcd_failure_contract.expected @@ -1,7 +1,7 @@ gcd.assertion\ - - Status: FAILURE\ - - Description: "result != 0 && x % result == 1 && y % result == 0"\ - gcd_failure_contract.rs:9:1 in function gcd\ +- Status: FAILURE\ +- Description: "result != 0 && x % result == 1 && y % result == 0"\ +in function gcd\ Failed Checks: result != 0 && x % result == 1 && y % result == 0 diff --git a/tests/expected/function-contract/gcd_success.expected b/tests/expected/function-contract/gcd_success.expected index c0f567abe518..d75b31b151df 100644 --- a/tests/expected/function-contract/gcd_success.expected +++ b/tests/expected/function-contract/gcd_success.expected @@ -1,6 +1,6 @@ gcd.assertion\ - - Status: SUCCESS\ - - Description: "result != 0 && x % result == 0 && y % result == 0"\ - gcd_success.rs:8:1 in function gcd +- Status: SUCCESS\ +- Description: "result != 0 && x % result == 0 && y % result == 0"\ +in function gcd VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/pattern_use.expected b/tests/expected/function-contract/pattern_use.expected index 0b42466d5cac..086baf514cc8 100644 --- a/tests/expected/function-contract/pattern_use.expected +++ b/tests/expected/function-contract/pattern_use.expected @@ -1,4 +1,3 @@ assertion\ - - Status: FAILURE\ - - Description: "attempt to divide by zero"\ - pattern_use.rs:7:5 \ No newline at end of file +- Status: FAILURE\ +- Description: "attempt to divide by zero"\ \ No newline at end of file diff --git a/tests/expected/function-contract/simple_ensures_fail.expected b/tests/expected/function-contract/simple_ensures_fail.expected index 3bae72c0766c..a65fff824ea6 100644 --- a/tests/expected/function-contract/simple_ensures_fail.expected +++ b/tests/expected/function-contract/simple_ensures_fail.expected @@ -1,7 +1,7 @@ max.assertion\ - - Status: FAILURE\ - - Description: "result == x"\ - simple_ensures_fail.rs:5:1 in function max +- Status: FAILURE\ +- Description: "result == x"\ +in function max Failed Checks: result == x diff --git a/tests/expected/function-contract/simple_ensures_pass.expected b/tests/expected/function-contract/simple_ensures_pass.expected index 395b7c75fc05..b3e15aefcb9d 100644 --- a/tests/expected/function-contract/simple_ensures_pass.expected +++ b/tests/expected/function-contract/simple_ensures_pass.expected @@ -1,6 +1,6 @@ max.assertion\ - - Status: SUCCESS\ - - Description: "(result == x) | (result == y)"\ - simple_ensures_pass.rs:5:1 in function max +- Status: SUCCESS\ +- Description: "(result == x) | (result == y)"\ +in function max VERIFICATION:- SUCCESSFUL From a8f0929fd815b41e819e5fb06246d7fe84360380 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 10 Aug 2023 15:07:12 -0700 Subject: [PATCH 18/36] Rename harnesses --- tests/expected/function-contract/arbitrary_ensures_fail.rs | 2 +- tests/expected/function-contract/arbitrary_ensures_pass.rs | 2 +- tests/expected/function-contract/arbitrary_requires_fail.rs | 2 +- tests/expected/function-contract/arbitrary_requires_pass.rs | 2 +- tests/expected/function-contract/checking_from_external_mod.rs | 2 +- tests/expected/function-contract/checking_in_impl.rs | 2 +- tests/expected/function-contract/gcd_failure_code.rs | 2 +- tests/expected/function-contract/gcd_failure_contract.rs | 2 +- tests/expected/function-contract/gcd_success.rs | 2 +- tests/expected/function-contract/pattern_use.rs | 2 +- tests/expected/function-contract/simple_ensures_fail.rs | 2 +- tests/expected/function-contract/simple_ensures_pass.rs | 2 +- 12 files changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs index f0ee72d93da7..91638b1cc037 100644 --- a/tests/expected/function-contract/arbitrary_ensures_fail.rs +++ b/tests/expected/function-contract/arbitrary_ensures_fail.rs @@ -8,7 +8,7 @@ fn max(x: u32, y: u32) -> u32 { } #[kani::proof_for_contract(max)] -fn main() { +fn max_harness() { let _ = Box::new(9_usize); max(kani::any(), kani::any()); } diff --git a/tests/expected/function-contract/arbitrary_ensures_pass.rs b/tests/expected/function-contract/arbitrary_ensures_pass.rs index 6611d8f870f7..df8d3a2361fb 100644 --- a/tests/expected/function-contract/arbitrary_ensures_pass.rs +++ b/tests/expected/function-contract/arbitrary_ensures_pass.rs @@ -8,7 +8,7 @@ fn max(x: u32, y: u32) -> u32 { } #[kani::proof_for_contract(max)] -fn main() { +fn max_harness() { let _ = Box::new(()); max(kani::any(), kani::any()); } diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs index f6729ccab808..d052e19b0335 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.rs +++ b/tests/expected/function-contract/arbitrary_requires_fail.rs @@ -8,7 +8,7 @@ fn div(dividend: u32, divisor: u32) -> u32 { } #[kani::proof_for_contract(div)] -fn main() { +fn div_harness() { let _ = Box::new(()); div(kani::any(), kani::any()); } diff --git a/tests/expected/function-contract/arbitrary_requires_pass.rs b/tests/expected/function-contract/arbitrary_requires_pass.rs index eca48fd60fc0..a9bb08d467b8 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.rs +++ b/tests/expected/function-contract/arbitrary_requires_pass.rs @@ -8,7 +8,7 @@ fn div(dividend: u32, divisor: u32) -> u32 { } #[kani::proof_for_contract(div)] -fn main() { +fn div_harness() { let _ = Box::new(()); div(kani::any(), kani::any()); } diff --git a/tests/expected/function-contract/checking_from_external_mod.rs b/tests/expected/function-contract/checking_from_external_mod.rs index c26be92ed5e9..43d1551f9aef 100644 --- a/tests/expected/function-contract/checking_from_external_mod.rs +++ b/tests/expected/function-contract/checking_from_external_mod.rs @@ -9,7 +9,7 @@ fn max(x: u32, y: u32) -> u32 { mod harnesses { #[kani::proof_for_contract(super::max)] - fn main() { + fn max_harness() { let _ = Box::new(9_usize); super::max(7, 6); } diff --git a/tests/expected/function-contract/checking_in_impl.rs b/tests/expected/function-contract/checking_in_impl.rs index d4003fd3759c..7d5c0506d9df 100644 --- a/tests/expected/function-contract/checking_in_impl.rs +++ b/tests/expected/function-contract/checking_in_impl.rs @@ -15,7 +15,7 @@ impl WrappedInt { } #[kani::proof_for_contract(WrappedInt::max)] -fn main() { +fn max_harness() { let _ = Box::new(9_usize); WrappedInt(7).max(WrappedInt(6)); } diff --git a/tests/expected/function-contract/gcd_failure_code.rs b/tests/expected/function-contract/gcd_failure_code.rs index 3b18e168268f..f76e04b75fee 100644 --- a/tests/expected/function-contract/gcd_failure_code.rs +++ b/tests/expected/function-contract/gcd_failure_code.rs @@ -57,7 +57,7 @@ impl Frac { #[kani::unwind(12)] #[kani::proof_for_contract(gcd)] -fn main() { +fn gcd_harness() { // Needed to avoid having `free` be removed as unused function. This is // because DFCC contract enforcement assumes that a definition for `free` // exists. diff --git a/tests/expected/function-contract/gcd_failure_contract.rs b/tests/expected/function-contract/gcd_failure_contract.rs index 633f7cb053fc..6b835466c5a0 100644 --- a/tests/expected/function-contract/gcd_failure_contract.rs +++ b/tests/expected/function-contract/gcd_failure_contract.rs @@ -57,7 +57,7 @@ impl Frac { #[kani::proof_for_contract(gcd)] #[kani::unwind(12)] -fn main() { +fn gcd_harness() { // Needed to avoid having `free` be removed as unused function. This is // because DFCC contract enforcement assumes that a definition for `free` // exists. diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs index dbd2a8c9d90e..d3a2c75b7d20 100644 --- a/tests/expected/function-contract/gcd_success.rs +++ b/tests/expected/function-contract/gcd_success.rs @@ -56,7 +56,7 @@ impl Frac { #[kani::proof_for_contract(gcd)] #[kani::unwind(12)] -fn main() { +fn gcd_harness() { // Needed to avoid having `free` be removed as unused function. This is // because DFCC contract enforcement assumes that a definition for `free` // exists. diff --git a/tests/expected/function-contract/pattern_use.rs b/tests/expected/function-contract/pattern_use.rs index 98ff9d27e39a..a51312acd2f0 100644 --- a/tests/expected/function-contract/pattern_use.rs +++ b/tests/expected/function-contract/pattern_use.rs @@ -8,7 +8,7 @@ fn div((dividend, divisor): (u32, u32)) -> u32 { } #[kani::proof_for_contract(div)] -fn main() { +fn div_harness() { let _ = Box::new(()); div((kani::any(), kani::any())); } diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs index 442a5e962168..687853612dcc 100644 --- a/tests/expected/function-contract/simple_ensures_fail.rs +++ b/tests/expected/function-contract/simple_ensures_fail.rs @@ -8,7 +8,7 @@ fn max(x: u32, y: u32) -> u32 { } #[kani::proof_for_contract(max)] -fn main() { +fn max_harness() { let _ = Box::new(9_usize); max(7, 9); } diff --git a/tests/expected/function-contract/simple_ensures_pass.rs b/tests/expected/function-contract/simple_ensures_pass.rs index 63b22d3eccdc..2d36f5c96e88 100644 --- a/tests/expected/function-contract/simple_ensures_pass.rs +++ b/tests/expected/function-contract/simple_ensures_pass.rs @@ -8,7 +8,7 @@ fn max(x: u32, y: u32) -> u32 { } #[kani::proof_for_contract(max)] -fn main() { +fn max_harness() { let _ = Box::new(9_usize); max(7, 6); } From ac73461187ffe098b318f4609ba1b67b5ff78919 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 10 Aug 2023 15:13:46 -0700 Subject: [PATCH 19/36] Remove enum map dependency --- Cargo.lock | 21 --------------------- kani-compiler/Cargo.toml | 1 - kani-compiler/src/kani_middle/attributes.rs | 6 ++---- 3 files changed, 2 insertions(+), 26 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index d2080af893e5..01c577439b62 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -360,26 +360,6 @@ version = "0.3.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" -[[package]] -name = "enum-map" -version = "2.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9705d8de4776df900a4a0b2384f8b0ab42f775e93b083b42f8ce71bdc32a47e3" -dependencies = [ - "enum-map-derive", -] - -[[package]] -name = "enum-map-derive" -version = "0.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ccb14d927583dd5c2eac0f2cf264fc4762aefe1ae14c47a8a20fc1939d3a5fc0" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.28", -] - [[package]] name = "equivalent" version = "1.0.1" @@ -518,7 +498,6 @@ version = "0.34.0" dependencies = [ "clap", "cprover_bindings", - "enum-map", "home", "itertools", "kani_metadata", diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 310ccaf2007f..fae829ce9713 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -24,7 +24,6 @@ strum_macros = "0.25.2" shell-words = "1.0.0" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} -enum-map = "2.6" # Future proofing: enable backend dependencies using feature. [features] diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 99448d9629f6..ae54a1ecb72a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -26,8 +26,6 @@ use crate::kani_queries::QueryDb; use super::resolve::{self, resolve_fn}; -extern crate enum_map; - #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] enum KaniAttributeKind { @@ -378,8 +376,8 @@ impl<'tcx> KaniAttributes<'tcx> { /// A basic check that ensures a function with a contract does not receive /// mutable pointers in its input and does not return raw pointers of any kind. /// -/// This is a temporary safety measure because contracts cannot yet reasona -/// about those structures. +/// This is a temporary safety measure because contracts cannot yet reason +/// about the heap. fn check_is_contract_safe(tcx: TyCtxt, item: DefId) { use ty::TypeVisitor; struct NoMutPtr<'tcx> { From e5582267123bd528e6cc0cd9444cc9b5610f0cde Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 10 Aug 2023 16:04:12 -0700 Subject: [PATCH 20/36] Lots of docuemntation expansion and a few fixes --- kani-compiler/src/kani_middle/metadata.rs | 10 +-- kani-compiler/src/kani_middle/resolve.rs | 4 +- kani-driver/src/args/mod.rs | 4 +- library/kani/src/lib.rs | 2 +- library/kani_macros/src/lib.rs | 37 ++++++++- library/kani_macros/src/sysroot/contracts.rs | 84 ++++++++++++-------- 6 files changed, 94 insertions(+), 47 deletions(-) diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 79372efadacf..fbf69c2d4fa4 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -16,17 +16,17 @@ use super::{attributes::KaniAttributes, SourceLocation}; pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata { let attributes = KaniAttributes::for_item(tcx, def_id).harness_attributes(); let pretty_name = tcx.def_path_str(def_id); - let mut mangled_name = tcx.symbol_name(Instance::mono(tcx, def_id)).to_string(); // Main function a special case in order to support `--function main` // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 - if pretty_name == "main" { - mangled_name = pretty_name.clone() + let mangled_name = if pretty_name == "main" { + pretty_name.clone() + } else { + tcx.symbol_name(Instance::mono(tcx, def_id)).to_string() }; let body = tcx.instance_mir(InstanceDef::Item(def_id)); let loc = SourceLocation::new(tcx, &body.span); - let file_stem = - format!("{}_{}", base_name.file_stem().unwrap().to_str().unwrap(), mangled_name); + let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); HarnessMetadata { diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index be9ac1088dba..814e5fd3700f 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -159,7 +159,9 @@ fn resolve_prefix<'tcx>( ) -> Result> { debug!(?name, ?current_module, "resolve_prefix"); - // Split the string into segments separated by `::`. + // Split the string into segments separated by `::`. Trim the whitespace + // since path strings generated from macros sometimes add spaces around + // `::`. let mut segments = name.split("::").map(|s| s.trim().to_string()).peekable(); assert!(segments.peek().is_some(), "expected identifier, found `{name}`"); diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 0ce6e5571664..d050baf12b75 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -24,9 +24,7 @@ use strum::VariantNames; /// Trait used to perform extra validation after parsing. pub trait ValidateArgs { /// Perform post-parsing validation but do not abort. - fn validate(&self) -> Result<(), Error> { - Ok(()) - } + fn validate(&self) -> Result<(), Error>; } /// Validate a set of arguments and ensure they are in a valid state. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index fada07b38305..94c19433ab48 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -66,7 +66,7 @@ pub fn assume(cond: bool) { } /// If the `premise` is true, so must be the `conclusion` -/// +/// /// Note that boolean operators (such as `||`) are evaluated lazily by Rust. /// This function is not and both conditions will be evaluated always. As a /// reult this function is not intended to be used in regular code. Instead it diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index ca1c615850a6..4b9e21d4be8c 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -7,7 +7,7 @@ // downstream crates to enable these features as well. // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" -#![feature(let_chains, proc_macro_diagnostic, box_patterns)] +#![feature(proc_macro_diagnostic)] mod derive; @@ -97,7 +97,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } -/// Add a precondition to this function. +/// Add a precondition to this function. /// /// This is part of the function contract API, together with [`ensures`]. /// @@ -105,6 +105,13 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// annotated function. All Rust syntax is supported, even calling other /// functions, but the computations must be side effect free, e.g. it cannot /// perform I/O or use mutable memory. +/// +/// Kani requires each function that uses a contract (this attribute or +/// [`ensures`]) to have at least one designated [`proof_for_contract`] harness +/// for checking the contract. +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. #[proc_macro_attribute] pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::requires(attr, item) @@ -119,11 +126,37 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { /// `result`. All Rust syntax is supported, even calling other functions, but /// the computations must be side effect free, e.g. it cannot perform I/O or use /// mutable memory. +/// +/// Kani requires each function that uses a contract (this attribute or +/// [`requires`]) to have at least one designated [`proof_for_contract`] harness +/// for checking the contract. +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. #[proc_macro_attribute] pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::ensures(attr, item) } +/// Designates this function as a harness to check a function contract. +/// +/// The argument to this macro is the relative path (e.g. `foo` or +/// `super::some_mod::foo` or `crate::SomeStruct::foo`) to the function, the +/// contract of which should be checked. +/// +/// The harness is expected to set up the arguments that `foo` should be called +/// with and initialzied any `static mut` globals that are reachable. All of +/// these should be initialized to as general a value as possible, usually +/// achieved using `kani::any`. The harness must call e.g. `foo` at least once +/// and if `foo` has type parameters, only one instantiation of those parameters +/// is admissable. Violating either results in a compile error. +/// +/// If any of those types have special invariants you can use `kani::assume` to +/// enforce them, but other than condition on inputs and checks of outputs +/// should be in the contract, not the harness for maximum soundness. +/// +/// This attribute is part of the unstable contracts API and requires +/// `-Zfunction-contracts` flag to be used. #[proc_macro_attribute] pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof_for_contract(attr, item) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index f28e03ad523d..d99fb527b937 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -50,12 +50,10 @@ fn identifier_for_generated_function(related_function: &ItemFn, purpose: &str, h } pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { - //handle_requires_ensures("requires", false, attr, item) requires_ensures_alt(attr, item, true) } pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { - //handle_requires_ensures("ensures", true, attr, item) requires_ensures_alt(attr, item, false) } @@ -78,11 +76,8 @@ impl<'ast> Visit<'ast> for ArgumentIdentCollector { } } -/// Applies the contained renaming to every ident pattern and ident expr -/// visited. -/// -/// In each case if the path has only one segments that corresponds to a key, it -/// is replaced by the ident in the value. +/// Applies the contained renaming (key renamed to value) to every ident pattern +/// and ident expr visited. struct Renamer<'a>(&'a HashMap); impl<'a> VisitMut for Renamer<'a> { @@ -96,7 +91,7 @@ impl<'a> VisitMut for Renamer<'a> { } /// This restores shadowing. Without this we would rename all ident - /// occurrences, but not the binding location. This is because our + /// occurrences, but not rebinding location. This is because our /// [`visit_expr_path_mut`] is scope-unaware. fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { if let Some(new) = self.0.get(&i.ident) { @@ -180,15 +175,19 @@ impl ContractFunctionState { struct PostconditionInjector(TokenStream2); impl VisitMut for PostconditionInjector { - fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) { - // Empty because inside the closure we don't want to inject - } + /// We leave this emtpy to stop the recursion here. We don't want to look + /// inside the closure, because the return statements contained within are + /// for a different function, duh. + fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) {} fn visit_expr_mut(&mut self, i: &mut Expr) { if let syn::Expr::Return(r) = i { let tokens = self.0.clone(); let mut output = TokenStream2::new(); if let Some(expr) = &mut r.expr { + // In theory the return expression can contain itself a `return` + // so we need to recurse here. + self.visit_expr_mut(expr); output.extend(quote!(let result = #expr;)); *expr = Box::new(Expr::Verbatim(quote!(result))); } @@ -207,11 +206,10 @@ impl VisitMut for PostconditionInjector { /// for the postconditions. /// /// This function -/// - collects all [`Ident`]s found in the argument patterns -/// - creates new names for them +/// - Collects all [`Ident`]s found in the argument patterns +/// - Creates new names for them /// - Replaces all occurrences of those idents in `attrs` with the new names and -/// - Returns the mapping of old names to new names so the macro can emit the -/// code that makes the copies. +/// - Returns the mapping of old names to new names fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { let mut arg_ident_collector = ArgumentIdentCollector::new(); arg_ident_collector.visit_signature(&sig); @@ -234,26 +232,35 @@ fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap< /// The main meat of handling requires/ensures contracts. /// /// Generates a `check__` function that assumes preconditions -/// and asserts postconditions. +/// and asserts postconditions. The check function is also marked as generated +/// with the `#[kanitool::is_contract_generated(check)]` attribute. /// -/// Decorates the original function with `#[checked_by = +/// Decorates the original function with `#[kanitool::checked_by = /// "check__"] /// -/// The check function is a copy of the original function with pre and -/// postconditions added before and after respectively. Each clause (requires or -/// ensures) adds new layers of pre or postconditions to the check function. +/// The check function is a copy of the original function with preconditions +/// added before the body and postconditions after as well as injected before +/// every `return` (see [`PostconditionInjector`]). Attributes on the original +/// function are also copied to the check function. Each clause (requires or +/// ensures) after the first will be ignored on the original function (detected +/// by finding the `kanitool::checked_with` attribute). On the check function +/// (detected by finding the `kanitool::is_contract_generated` attribute) it +/// expands into a new layer of pre- or postconditions. This state machine is +/// also explained in more detail in comments in the body of this macro. /// -/// Postconditions are also injected before every `return` expression, see also -/// [`PostconditionInjector`]. -/// -/// All arguments of the function are unsafely shallow-copied with the -/// `kani::untracked_deref` function. We must ensure that those copies are not +/// In the check function all named arguments of the function are unsafely +/// shallow-copied with the `kani::untracked_deref` function to circumvent the +/// borrow checker for postconditions. We must ensure that those copies are not /// dropped so after the postconditions we call `mem::forget` on each copy. /// /// # Complete example /// /// ```rs -/// +/// #[kani::requires(divisor != 0)] +/// #[kani::ensures(result <= dividend)] +/// fn div(dividend: u32, divisor: u32) -> u32 { +/// dividend / divisor +/// } /// ``` /// /// Turns into @@ -314,13 +321,6 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) // 4. And (minor point) adding #[allow(dead_code)] and // #[allow(unused_variables)] to the check function attributes - // The order of `attrs` and `kanitool::{checked_with, - // is_contract_generated}` is important here, because macros are - // expanded outside in. This way other contract annotations in - // `attrs` sees those attribuites which they need to determine - // `function_state` attribute and can use them. - // - // The same applies later when we emit the check function. let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); // Constructing string literals explicitly here, because if we call @@ -328,6 +328,15 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) // expression to the next expansion of a contract, not as the // literal. let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); + + // The order of `attrs` and `kanitool::{checked_with, + // is_contract_generated}` is important here, because macros are + // expanded outside in. This way other contract annotations in `attrs` + // sees those attribuites and can use them to determine + // `function_state`. + // + // We're emitting the original here but the same applies later when we + // emit the check function. output.extend(quote!( #(#attrs)* #[kanitool::checked_with = #check_fn_name_str] @@ -353,13 +362,14 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let also_arg_copy_names = arg_copy_names.clone(); let arg_idents = arg_idents.keys(); + // The code that enforces the postconditions and cleans up the shallow + // argument copies (with `mem::forget`). let exec_postconditions = quote!( kani::assert(#attr, stringify!(#attr_copy)); #(std::mem::forget(#also_arg_copy_names);)* ); let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); - inject_conditions.visit_block_mut(&mut *call_to_prior); quote!( @@ -372,15 +382,19 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let sig = &item_fn.sig; + // Prepare emitting the check function by emitting the rest of the + // attributes. output.extend(quote!( #(#attrs)* )); if matches!(function_state, ContractFunctionState::Untouched) { + // If it's the first time we also emit this marker. Again, order is + // important so this happens as the last emitted attribute. output.extend(quote!(#[kanitool::is_contract_generated(check)])); } - // Finally emit the check function. + // Finally emit the check function itself. output.extend(quote!( #sig { #check_body From ba845996e16e121173fd6290221e7dc5e237b9f6 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 10 Aug 2023 16:45:43 -0700 Subject: [PATCH 21/36] Yes I didn't need this --- library/kani_macros/src/sysroot/contracts.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index d99fb527b937..94c3fe155249 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::collections::{HashMap, HashSet}; -use super::*; +use proc_macro::TokenStream; use { quote::{quote, ToTokens}, From c8b137c6ce484aeb42fb3730fb95fa0440549a0e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 19:27:46 -0700 Subject: [PATCH 22/36] Update library/kani/src/lib.rs Co-authored-by: Celina G. Val --- library/kani/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 94c19433ab48..dd4921ff0c4f 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -70,7 +70,7 @@ pub fn assume(cond: bool) { /// Note that boolean operators (such as `||`) are evaluated lazily by Rust. /// This function is not and both conditions will be evaluated always. As a /// reult this function is not intended to be used in regular code. Instead it -/// is intended to make implications in a function function contract +/// is intended to make implications in a function contract /// ([`requires`], [`ensures`]) more readable. For eample /// `implies(self.is_empty(), self.len() == 0)` is a little easier to understand /// than `!self.is_empty() || self.len() == 0` (which is the inlined definition From d53a5a80ee327d4007d1e5efa3350fa5566af74d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 18:29:10 -0700 Subject: [PATCH 23/36] Add documentation for attribute enum and remove unused attribute --- kani-compiler/src/kani_middle/attributes.rs | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index ae54a1ecb72a..3d09183d2871 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -36,9 +36,15 @@ enum KaniAttributeKind { /// Attribute used to mark unstable APIs. Unstable, Unwind, + /// A harness, similar to [`Self::Proof`], but for checking a function + /// contract, e.g. the contract check is substituted for the target function + /// before the the verification runs. ProofForContract, + /// Attribute on a function with a contract that identifies the code + /// implementing the check for this contract. CheckedWith, - ReplacedWith, + /// Attribute on a function that was auto-generated from expanding a + /// function contract. IsContractGenerated, } @@ -54,8 +60,7 @@ impl KaniAttributeKind { | KaniAttributeKind::Unwind => true, KaniAttributeKind::Unstable | KaniAttributeKind::CheckedWith - | KaniAttributeKind::IsContractGenerated - | KaniAttributeKind::ReplacedWith => false, + | KaniAttributeKind::IsContractGenerated => false, } } @@ -69,7 +74,7 @@ impl KaniAttributeKind { /// contract. pub fn is_function_contract(self) -> bool { use KaniAttributeKind::*; - matches!(self, CheckedWith | ReplacedWith | IsContractGenerated) + matches!(self, CheckedWith | IsContractGenerated) } } @@ -227,7 +232,7 @@ impl<'tcx> KaniAttributes<'tcx> { assert!(!self.map.contains_key(&KaniAttributeKind::Proof)); expect_single(self.tcx, kind, &attrs); } - KaniAttributeKind::ReplacedWith | KaniAttributeKind::CheckedWith => { + KaniAttributeKind::CheckedWith => { self.expect_maybe_one(kind) .map(|attr| expect_key_string_value(&self.tcx.sess, attr)); } @@ -320,9 +325,7 @@ impl<'tcx> KaniAttributes<'tcx> { // Internal attribute which shouldn't exist here. unreachable!() } - KaniAttributeKind::CheckedWith - | KaniAttributeKind::ReplacedWith - | KaniAttributeKind::IsContractGenerated => { + KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { todo!("Contract attributes are not supported on proofs") } }; From b81c45ad31728ce18ceff3c742df895ac29fc86c Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 19:28:29 -0700 Subject: [PATCH 24/36] Adding requested changes --- kani-compiler/src/kani_compiler.rs | 5 +- kani-compiler/src/kani_middle/attributes.rs | 130 ++++++-------------- kani-compiler/src/kani_middle/mod.rs | 91 +++++++++++++- kani-compiler/src/kani_queries/mod.rs | 6 - 4 files changed, 124 insertions(+), 108 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 2d4966f9ce2a..a1e231301566 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -400,9 +400,6 @@ impl Callbacks for KaniCompiler { queries.unstable_features = features.cloned().collect::>(); } - queries.function_contracts_enabled = - queries.unstable_features.iter().any(|s| s == "function-contracts"); - if matches.get_flag(parser::ENABLE_STUBBING) && queries.reachability_analysis == ReachabilityType::Harnesses { @@ -422,7 +419,7 @@ impl Callbacks for KaniCompiler { ) -> Compilation { if self.stage.is_init() { self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| { - check_crate_items(tcx, &self.queries.lock().unwrap()); + check_crate_items(tcx, self.queries.lock().unwrap().ignore_global_asm); self.process_harnesses(tcx) }); } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 3d09183d2871..79a9b7eadf84 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -11,10 +11,7 @@ use rustc_ast::{ }; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; -use rustc_middle::{ - mir, - ty::{self, Instance, TyCtxt, TyKind}, -}; +use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_span::{Span, Symbol}; use std::str::FromStr; @@ -22,7 +19,7 @@ use strum_macros::{AsRefStr, EnumString}; use tracing::{debug, trace}; -use crate::kani_queries::QueryDb; +use crate::parser::ENABLE_FUNCTION_CONTRACTS; use super::resolve::{self, resolve_fn}; @@ -64,14 +61,16 @@ impl KaniAttributeKind { } } - /// Is this attribute kind one of the suite of attributes that form the function contracts API + /// Is this attribute kind one of the suite of attributes that form the + /// function contracts API. E.g. where [`Self::is_function_contract`] is + /// true but also auto harness attributes like `proof_for_contract` pub fn is_function_contract_api(self) -> bool { use KaniAttributeKind::*; self.is_function_contract() || matches!(self, ProofForContract) } /// Would this attribute be placed on a function as part of a function - /// contract. + /// contract. E.g. created by `requires`, `ensures` pub fn is_function_contract(self) -> bool { use KaniAttributeKind::*; matches!(self, CheckedWith | IsContractGenerated) @@ -137,7 +136,7 @@ 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 fn for_contract(&self) -> Option<(Symbol, DefId, Span)> { + fn interpret_the_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); let resolved = resolve_fn( @@ -171,7 +170,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Check that all attributes assigned to an item is valid. /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate /// the session and emit all errors found. - pub(super) fn check_attributes(&self, queries: &QueryDb) { + pub(super) fn check_attributes(&self) { // Check that all attributes are correctly used and well formed. let is_harness = self.is_harness(); for (&kind, attrs) in self.map.iter() { @@ -184,20 +183,6 @@ impl<'tcx> KaniAttributes<'tcx> { ), ); } - if kind.is_function_contract_api() && !queries.function_contracts_enabled() { - let msg = format!( - "Using the {} attribute requires activating the unstable `function-contracts` feature", - kind.as_ref() - ); - if let Some(attr) = attrs.first() { - self.tcx.sess.span_err(attr.span, msg); - } else { - self.tcx.sess.err(msg); - } - } - if kind.is_function_contract() { - check_is_contract_safe(self.tcx, self.item); - } match kind { KaniAttributeKind::ShouldPanic => { expect_single(self.tcx, kind, &attrs); @@ -255,6 +240,27 @@ impl<'tcx> KaniAttributes<'tcx> { // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 return; } + + if !enabled_features.iter().any(|feature| feature == ENABLE_FUNCTION_CONTRACTS) { + for kind in self + .map + .keys() + .copied() + .filter(|a| a.is_function_contract_api()) + .collect::>() + { + let msg = format!( + "Using the {} attribute requires activating the unstable `function-contracts` feature", + kind.as_ref() + ); + if let Some(attr) = self.map.get(&kind).unwrap().first() { + self.tcx.sess.span_err(attr.span, msg); + } else { + self.tcx.sess.err(msg); + } + } + } + if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) { for attr in unstable_attrs { let unstable_attr = UnstableAttribute::try_from(*attr).unwrap(); @@ -334,7 +340,7 @@ impl<'tcx> KaniAttributes<'tcx> { ); let current_module = self.tcx.parent_module_from_def_id(local_id); attrs.stubs.extend( - self.for_contract() + self.interpret_the_for_contract_attribute() .and_then(|(name, id, span)| { let replacement_name = KaniAttributes::for_item(self.tcx, id).checked_with(); if replacement_name.is_none() { @@ -376,74 +382,6 @@ impl<'tcx> KaniAttributes<'tcx> { } } -/// A basic check that ensures a function with a contract does not receive -/// mutable pointers in its input and does not return raw pointers of any kind. -/// -/// This is a temporary safety measure because contracts cannot yet reason -/// about the heap. -fn check_is_contract_safe(tcx: TyCtxt, item: DefId) { - use ty::TypeVisitor; - struct NoMutPtr<'tcx> { - tcx: TyCtxt<'tcx>, - span: Span, - is_prohibited: fn(ty::Ty<'tcx>) -> bool, - r#where: &'static str, - what: &'static str, - } - - impl<'tcx> TypeVisitor> for NoMutPtr<'tcx> { - fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> std::ops::ControlFlow { - use ty::TypeSuperVisitable; - if (self.is_prohibited)(t) { - self.tcx.sess.span_err(self.span, format!("{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); - } - - // Rust's type visitor only recurses into type arguments, (e.g. - // `generics` in this match). This is enough for may types, but it - // won't look at the field types of structs or enums. So we override - // it here and do that ourselves. - // - // Since the field types also must contain in some form all the type - // arguments the visitor will see them as it inspects the fields and - // we don't need to call back to `super`. - if let ty::TyKind::Adt(adt_def, generics) = t.kind() { - for variant in adt_def.variants() { - for field in &variant.fields { - let ctrl = self.visit_ty(field.ty(self.tcx, generics)); - if ctrl.is_break() { - // Technically we can just ignore this because we - // know this case will never happen, but just to be - // safe. - return ctrl; - } - } - } - std::ops::ControlFlow::Continue(()) - } else { - // For every other type - t.super_visit_with(self) - } - } - } - - fn is_raw_mutable_ptr(t: ty::Ty) -> bool { - matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) - } - - let body = tcx.optimized_mir(item); - - for (arg, (is_prohibited, r#where, what)) in body - .args_iter() - .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable "))) - .chain([(mir::RETURN_PLACE, (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))]) - { - let decl = &body.local_decls[arg]; - let span = decl.source_info.span; - let mut v = NoMutPtr { tcx, span, is_prohibited, r#where, what }; - v.visit_ty(decl.ty); - } -} - /// An efficient check for the existence for a particular [`KaniAttributeKind`]. /// Unlike querying [`KaniAttributes`] this method builds no new heap data /// structures and has short circuiting. @@ -455,6 +393,12 @@ fn has_kani_attribute bool>( tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) } +/// Test is this function was generated by expanding a contract attribute like +/// `requires` and `ensures` +pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool { + has_kani_attribute(tcx, def_id, KaniAttributeKind::is_function_contract) +} + /// Same as [`KaniAttributes::is_harness`] but more efficient because less /// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool { @@ -478,7 +422,7 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { /// Expect the contents of this attribute to be of the format #[attribute = /// "value"] and return the `"value"` -pub fn expect_key_string_value(sess: &Session, attr: &Attribute) -> rustc_span::Symbol { +fn expect_key_string_value(sess: &Session, attr: &Attribute) -> rustc_span::Symbol { let span = attr.span; let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else { sess.span_fatal(span, "Expected attribute of the form #[attr = \"value\"]") diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 4aca669cddfc..11cc7cea094a 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -15,7 +15,7 @@ use rustc_middle::ty::layout::{ FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, TyAndLayout, }; -use rustc_middle::ty::{self, Instance, InstanceDef, Ty, TyCtxt}; +use rustc_middle::ty::{self, Instance, InstanceDef, ParamEnv, Ty, TyCtxt}; use rustc_session::config::OutputType; use rustc_span::source_map::respan; use rustc_span::Span; @@ -39,13 +39,13 @@ pub mod stubbing; /// Check that all crate items are supported and there's no misconfiguration. /// This method will exhaustively print any error / warning and it will abort at the end if any /// error was found. -pub fn check_crate_items(tcx: TyCtxt, queries: &QueryDb) { +pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { let krate = tcx.crate_name(LOCAL_CRATE); for item in tcx.hir_crate_items(()).items() { let def_id = item.owner_id.def_id.to_def_id(); - KaniAttributes::for_item(tcx, def_id).check_attributes(queries); + KaniAttributes::for_item(tcx, def_id).check_attributes(); if tcx.def_kind(def_id) == DefKind::GlobalAsm { - if !queries.ignore_global_asm { + if !ignore_asm { let error_msg = format!( "Crate {krate} contains global ASM, which is not supported by Kani. Rerun with \ `--enable-unstable --ignore-global-asm` to suppress this error \ @@ -65,7 +65,7 @@ pub fn check_crate_items(tcx: TyCtxt, queries: &QueryDb) { /// Check that all given items are supported and there's no misconfiguration. /// This method will exhaustively print any error / warning and it will abort at the end if any /// error was found. -pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { +pub fn check_reachable_items<'tcx>(tcx: TyCtxt<'tcx>, queries: &QueryDb, items: &[MonoItem<'tcx>]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) { @@ -76,10 +76,91 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) .check_unstable_features(&queries.unstable_features); def_ids.insert(def_id); } + + // We don't short circuit here since this is a type check and can shake + // out differently depending on generic parameters + if let MonoItem::Fn(instance) = item { + if attributes::is_function_contract_generated(tcx, instance.def_id()) { + check_is_contract_safe(tcx, *instance); + } + } } tcx.sess.abort_if_errors(); } +/// A basic check that ensures a function with a contract does not receive +/// mutable pointers in its input and does not return raw pointers of any kind. +/// +/// This is a temporary safety measure because contracts cannot yet reason +/// about the heap. +fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { + use ty::TypeVisitor; + struct NoMutPtr<'tcx> { + tcx: TyCtxt<'tcx>, + is_prohibited: fn(ty::Ty<'tcx>) -> bool, + /// Where (top level) did the type we're analyzing come from. Used for + /// composing error messages. + r#where: &'static str, + /// Adjective to describe the kind of pointer we're prohibiting. + /// Essentially `is_prohibited` but in english + what: &'static str, + } + + impl<'tcx> TypeVisitor> for NoMutPtr<'tcx> { + fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> std::ops::ControlFlow { + use ty::TypeSuperVisitable; + if (self.is_prohibited)(t) { + // TODO make this more user friendly + self.tcx.sess.err(format!("{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); + } + + // Rust's type visitor only recurses into type arguments, (e.g. + // `generics` in this match). This is enough for may types, but it + // won't look at the field types of structs or enums. So we override + // it here and do that ourselves. + // + // Since the field types also must contain in some form all the type + // arguments the visitor will see them as it inspects the fields and + // we don't need to call back to `super`. + if let ty::TyKind::Adt(adt_def, generics) = t.kind() { + for variant in adt_def.variants() { + for field in &variant.fields { + let ctrl = self.visit_ty(field.ty(self.tcx, generics)); + if ctrl.is_break() { + // Technically we can just ignore this because we + // know this case will never happen, but just to be + // safe. + return ctrl; + } + } + } + std::ops::ControlFlow::Continue(()) + } else { + // For every other type + t.super_visit_with(self) + } + } + } + + fn is_raw_mutable_ptr(t: ty::Ty) -> bool { + matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) + } + + let fn_typ = + instance.ty(tcx, ParamEnv::reveal_all()).fn_sig(tcx).no_bound_vars().expect("impossible"); + + for (typ, (is_prohibited, r#where, what)) in fn_typ + .inputs() + .iter() + .copied() + .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable "))) + .chain([(fn_typ.output(), (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))]) + { + let mut v = NoMutPtr { tcx, is_prohibited, r#where, what }; + v.visit_ty(typ); + } +} + /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc. pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { /// Convert MonoItem into a DefId. diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index fa88cd0666c4..44573bf124d8 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -36,7 +36,6 @@ pub struct QueryDb { pub write_json_symtab: bool, pub reachability_analysis: ReachabilityType, pub stubbing_enabled: bool, - pub function_contracts_enabled: bool, pub unstable_features: Vec, /// Information about all target harnesses. @@ -57,9 +56,4 @@ impl QueryDb { pub fn harness_model_path(&self, harness: &DefPathHash) -> Option<&PathBuf> { self.harnesses_info.get(harness) } - - /// Has the `-Zfunction-contracts` option been passed to the driver - pub fn function_contracts_enabled(&self) -> bool { - self.function_contracts_enabled - } } From 6aa6b221abdc53105f23b3192f8973f09cfb892d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 19:36:43 -0700 Subject: [PATCH 25/36] Remove unused compiler flag --- kani-compiler/src/kani_middle/attributes.rs | 4 +--- kani-compiler/src/parser.rs | 9 --------- 2 files changed, 1 insertion(+), 12 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 79a9b7eadf84..23d9150e895a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -19,8 +19,6 @@ use strum_macros::{AsRefStr, EnumString}; use tracing::{debug, trace}; -use crate::parser::ENABLE_FUNCTION_CONTRACTS; - use super::resolve::{self, resolve_fn}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] @@ -241,7 +239,7 @@ impl<'tcx> KaniAttributes<'tcx> { return; } - if !enabled_features.iter().any(|feature| feature == ENABLE_FUNCTION_CONTRACTS) { + if !enabled_features.iter().any(|feature| feature == "function-contracts") { for kind in self .map .keys() diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs index 44945cd80470..a947fdc61eaa 100644 --- a/kani-compiler/src/parser.rs +++ b/kani-compiler/src/parser.rs @@ -46,9 +46,6 @@ pub const REACHABILITY: &str = "reachability"; /// Option name used to enable stubbing. pub const ENABLE_STUBBING: &str = "enable-stubbing"; -/// Option name used to enable function contracts -pub const ENABLE_FUNCTION_CONTRACTS: &str = "enable-function-contracts"; - /// Option name used to define unstable features. pub const UNSTABLE_FEATURE: &str = "unstable"; @@ -143,12 +140,6 @@ pub fn parser() -> Command { .help("Instruct the compiler to perform stubbing.") .action(ArgAction::SetTrue), ) - .arg( - Arg::new(ENABLE_FUNCTION_CONTRACTS) - .long(ENABLE_FUNCTION_CONTRACTS) - .help("Allow function contract specification, checking and replacement") - .action(ArgAction::SetTrue), - ) .arg( Arg::new("check-version") .long("check-version") From 4c475b6cd754cd832bfb5138adae445379d34f53 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 19:38:51 -0700 Subject: [PATCH 26/36] Expand test case --- .../arbitrary_requires_pass.expected | 5 + tests/expected/function-contract/out.txt | 258 ++++++++++++++++++ 2 files changed, 263 insertions(+) create mode 100644 tests/expected/function-contract/out.txt diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index 880f00714b32..2954b60fecd1 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -1 +1,6 @@ +div.arithmetic_overflow\ +- Status: SUCCESS\ +- Description: "attempt to divide by zero"\ +in function div + VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/out.txt b/tests/expected/function-contract/out.txt new file mode 100644 index 000000000000..6f95e232cd7a --- /dev/null +++ b/tests/expected/function-contract/out.txt @@ -0,0 +1,258 @@ +Kani Rust Verifier 0.34.0 (standalone) +Checking harness div_harness... +CBMC 5.88.1 (cbmc-5.88.1) +CBMC version 5.88.1 (cbmc-5.88.1) 64-bit arm64 macos +Reading GOTO program from file /Users/justbldr/research/kani/tests/expected/function-contract/arbitrary_requires_pass__RNvCs6zRRqCRMgBy_23arbitrary_requires_pass11div_harness.out +Generating GOTO Program +Adding CPROVER library (arm64) +Removal of function pointers and virtual functions +Generic Property Instrumentation +Running with 16 object bits, 48 offset bits (user-specified) +Starting Bounded Model Checking +Runtime Symex: 0.0207943s +size of program expression: 733 steps +slicing removed 435 assignments +Generated 23 VCC(s), 7 remaining after simplification +Runtime Postprocess Equation: 6.0625e-05s +Passing problem to propositional reduction +converting SSA +Runtime Convert SSA: 0.0008905s +Running propositional reduction +Post-processing +Runtime Post-process: 5.541e-06s +Solving with CaDiCaL sc2021 +625 variables, 647 clauses +SAT checker: instance is SATISFIABLE +Runtime Solver: 7.8584e-05s +Runtime decision procedure: 0.00102646s +Running propositional reduction +Solving with CaDiCaL sc2021 +625 variables, 648 clauses +SAT checker: instance is UNSATISFIABLE +Runtime Solver: 3.8291e-05s +Runtime decision procedure: 7.0834e-05s + +RESULTS: +Check 1: __rust_dealloc.assertion.1 + - Status: SUCCESS + - Description: "Alignment is power of two" + - Location: ../../../library/kani/kani_lib.c:84 in function __rust_dealloc + +Check 2: __rust_dealloc.assertion.2 + - Status: SUCCESS + - Description: "rust_dealloc must be called on an object whose allocated size matches its layout" + - Location: ../../../library/kani/kani_lib.c:86 in function __rust_dealloc + +Check 3: div.assertion.1 + - Status: SUCCESS + - Description: "attempt to divide by zero" + - Location: arbitrary_requires_pass.rs:7:5 in function div + +Check 4: div.arithmetic_overflow.1 + - Status: SUCCESS + - Description: "attempt to divide by zero" + - Location: arbitrary_requires_pass.rs:7:5 in function div + +Check 5: core::panicking::panic_nounwind_fmt.unsupported_construct.1 + - Status: SUCCESS + - Description: "call to foreign "Rust" function `rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panicking.rs:89:9 in function core::panicking::panic_nounwind_fmt + +Check 6: core::panicking::panic_nounwind_fmt.assertion.1 + - Status: SUCCESS + - Description: "reached intrinsic::abort" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panicking.rs:82:9 in function core::panicking::panic_nounwind_fmt + +Check 7: malloc.assertion.1 + - Status: SUCCESS + - Description: "max allocation size exceeded" + - Location: :31 in function malloc + +Check 8: malloc.assertion.2 + - Status: SUCCESS + - Description: "max allocation may fail" + - Location: :36 in function malloc + +Check 9: std::panic::Location::<'_>::caller.unsupported_construct.1 + - Status: SUCCESS + - Description: "caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panic/location.rs:88:9 in function std::panic::Location::<'_>::caller + +Check 10: std::ptr::Alignment::as_usize.assume.1 + - Status: SUCCESS + - Description: "assumption failed" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs:96:9 in function std::ptr::Alignment::as_usize + +Check 11: std::fmt::Arguments::<'_>::new_const.assertion.1 + - Status: SUCCESS + - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:299:13 in function std::fmt::Arguments::<'_>::new_const + +Check 12: std::fmt::Arguments::<'_>::new_const.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:301:34 in function std::fmt::Arguments::<'_>::new_const + +Check 13: __rust_dealloc.precondition_instance.1 + - Status: SUCCESS + - Description: "free argument must be NULL or valid pointer" + - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc + +Check 14: __rust_dealloc.precondition_instance.2 + - Status: SUCCESS + - Description: "free argument must be dynamic object" + - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc + +Check 15: __rust_dealloc.precondition_instance.3 + - Status: SUCCESS + - Description: "free argument has offset zero" + - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc + +Check 16: __rust_dealloc.precondition_instance.4 + - Status: SUCCESS + - Description: "double free" + - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc + +Check 17: __rust_dealloc.precondition_instance.5 + - Status: SUCCESS + - Description: "free called for new[] object" + - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc + +Check 18: __rust_dealloc.precondition_instance.6 + - Status: SUCCESS + - Description: "free called for stack-allocated object" + - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc + +Check 19: std::ptr::drop_in_place::>.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> + +Check 20: std::ptr::drop_in_place::>.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> + +Check 21: std::ptr::drop_in_place::>.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> + +Check 22: std::ptr::drop_in_place::>.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> + +Check 23: std::ptr::drop_in_place::>.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> + +Check 24: std::ptr::drop_in_place::>.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> + +Check 25: as std::ops::Drop>::drop.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop + +Check 26: as std::ops::Drop>::drop.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop + +Check 27: as std::ops::Drop>::drop.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop + +Check 28: as std::ops::Drop>::drop.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop + +Check 29: as std::ops::Drop>::drop.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop + +Check 30: as std::ops::Drop>::drop.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop + +Check 31: std::alloc::Layout::align.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align + +Check 32: std::alloc::Layout::align.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align + +Check 33: std::alloc::Layout::align.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align + +Check 34: std::alloc::Layout::align.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align + +Check 35: std::alloc::Layout::align.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align + +Check 36: std::alloc::Layout::align.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align + +Check 37: div.division-by-zero.1 + - Status: SUCCESS + - Description: "division by zero" + - Location: arbitrary_requires_pass.rs:7:5 in function div + +Check 38: std::alloc::Layout::size.pointer_dereference.1 + - Status: SUCCESS + - Description: "dereference failure: pointer NULL" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size + +Check 39: std::alloc::Layout::size.pointer_dereference.2 + - Status: SUCCESS + - Description: "dereference failure: pointer invalid" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size + +Check 40: std::alloc::Layout::size.pointer_dereference.3 + - Status: SUCCESS + - Description: "dereference failure: deallocated dynamic object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size + +Check 41: std::alloc::Layout::size.pointer_dereference.4 + - Status: SUCCESS + - Description: "dereference failure: dead object" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size + +Check 42: std::alloc::Layout::size.pointer_dereference.5 + - Status: SUCCESS + - Description: "dereference failure: pointer outside object bounds" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size + +Check 43: std::alloc::Layout::size.pointer_dereference.6 + - Status: SUCCESS + - Description: "dereference failure: invalid integer address" + - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size + + +SUMMARY: + ** 0 of 43 failed + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.44933715s + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. From 71711a0cf8ff242e7e020c89c5cb4edeb52dcb35 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 19:41:51 -0700 Subject: [PATCH 27/36] An unused collect --- kani-compiler/src/kani_middle/attributes.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 23d9150e895a..995bdc20a3cb 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -239,13 +239,14 @@ impl<'tcx> KaniAttributes<'tcx> { return; } + // If the `function-contracts` unstable feature is not enabled then no + // function should use any of those APIs. if !enabled_features.iter().any(|feature| feature == "function-contracts") { for kind in self .map .keys() .copied() .filter(|a| a.is_function_contract_api()) - .collect::>() { let msg = format!( "Using the {} attribute requires activating the unstable `function-contracts` feature", From 98ccfa5c6af3b1b83b3fc4561424741c92552710 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 21 Aug 2023 12:27:14 -0700 Subject: [PATCH 28/36] Split pointer prohibition tests --- .../allowed_const_ptr.expected | 1 + .../prohibit-pointers/allowed_const_ptr.rs | 15 ++++++ .../allowed_mut_ref.expected | 1 + .../prohibit-pointers/allowed_mut_ref.rs | 15 ++++++ .../allowed_mut_return_ref.expected | 1 + .../allowed_mut_return_ref.rs | 18 +++++++ .../prohibit-pointers/allowed_ref.expected | 1 + .../prohibit-pointers/allowed_ref.rs | 16 ++++++ .../prohibit-pointers/hidden.expected | 1 + .../prohibit-pointers/hidden.rs | 17 +++++++ .../prohibit-pointers/plain_pointer.expected | 1 + .../prohibit-pointers/plain_pointer.rs | 14 +++++ .../prohibit-pointers/return_pointer.expected | 1 + .../prohibit-pointers/return_pointer.rs | 16 ++++++ .../prohibit_pointers.expected | 3 -- .../function-contract/prohibit_pointers.rs | 51 ------------------- 16 files changed, 118 insertions(+), 54 deletions(-) create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_ref.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/allowed_ref.rs create mode 100644 tests/expected/function-contract/prohibit-pointers/hidden.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/hidden.rs create mode 100644 tests/expected/function-contract/prohibit-pointers/plain_pointer.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/plain_pointer.rs create mode 100644 tests/expected/function-contract/prohibit-pointers/return_pointer.expected create mode 100644 tests/expected/function-contract/prohibit-pointers/return_pointer.rs delete mode 100644 tests/expected/function-contract/prohibit_pointers.expected delete mode 100644 tests/expected/function-contract/prohibit_pointers.rs diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs new file mode 100644 index 000000000000..666ff3c6af56 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn allowed_pointer(t: *const bool) {} + +#[kani::proof_for_contract(allowed_pointer)] +fn allowed_pointer_harness() { + let _ = Box::new(()); + let mut a = Box::new(true); + allowed_pointer(Box::into_raw(a)) +} \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs new file mode 100644 index 000000000000..c70dddf5b84f --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn allowed_mut_ref(t: &mut bool) {} + +#[kani::proof_for_contract(allowed_mut_ref)] +fn allowed_mut_ref_harness() { + let _ = Box::new(()); + let mut a = true; + allowed_mut_ref(&mut a) +} \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs new file mode 100644 index 000000000000..07da23e907a3 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +static mut B: bool = false; + +#[kani::ensures(true)] +fn allowed_mut_return_ref<'a>() -> &'a mut bool { + unsafe { &mut B as &'a mut bool } +} + +#[kani::proof_for_contract(allowed_mut_return_ref)] +fn allowed_mut_return_ref_harness() { + let _ = Box::new(()); + allowed_mut_return_ref(); +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs new file mode 100644 index 000000000000..34c2a9bdac6c --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn allowed_ref(t: &bool) {} + +#[kani::proof_for_contract(allowed_ref)] +fn allowed_ref_harness() { + let _ = Box::new(()); + let a = true; + allowed_ref(&a) +} + diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.expected b/tests/expected/function-contract/prohibit-pointers/hidden.expected new file mode 100644 index 000000000000..ccc1120292d8 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/hidden.expected @@ -0,0 +1 @@ +error: This argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.rs b/tests/expected/function-contract/prohibit-pointers/hidden.rs new file mode 100644 index 000000000000..846b2c25df3a --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/hidden.rs @@ -0,0 +1,17 @@ + +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +struct HidesAPointer(*mut u32); + +#[kani::ensures(true)] +fn hidden_pointer(h: HidesAPointer) {} + +#[kani::proof_for_contract(hidden_pointer)] +fn harness() { + let mut a = 0; + hidden_pointer(HidesAPointer(&mut a)) +} \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected b/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected new file mode 100644 index 000000000000..eb9669c21348 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected @@ -0,0 +1 @@ +error: This argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs new file mode 100644 index 000000000000..24e9d006a9c0 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn plain_pointer(t: *mut i32) {} + +#[kani::proof_for_contract(plain_pointer)] +fn plain_ptr_harness() { + let mut a = 0; + plain_pointer(&mut a) +} diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.expected b/tests/expected/function-contract/prohibit-pointers/return_pointer.expected new file mode 100644 index 000000000000..ebf53e6afff1 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.expected @@ -0,0 +1 @@ +error: The return contains a pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs new file mode 100644 index 000000000000..ecadb49b9d72 --- /dev/null +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![allow(unreachable_code, unused_variables)] + +#[kani::ensures(true)] +fn return_pointer() -> *const usize { + unreachable!() +} + +#[kani::proof_for_contract(return_pointer)] +fn return_ptr_harness() { + return_pointer(); +} + diff --git a/tests/expected/function-contract/prohibit_pointers.expected b/tests/expected/function-contract/prohibit_pointers.expected deleted file mode 100644 index a0f864710118..000000000000 --- a/tests/expected/function-contract/prohibit_pointers.expected +++ /dev/null @@ -1,3 +0,0 @@ -error: This argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. -error: This argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. -error: The return contains a pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file diff --git a/tests/expected/function-contract/prohibit_pointers.rs b/tests/expected/function-contract/prohibit_pointers.rs deleted file mode 100644 index e6e4ed25bf90..000000000000 --- a/tests/expected/function-contract/prohibit_pointers.rs +++ /dev/null @@ -1,51 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zfunction-contracts - -struct HidesAPointer(*mut u32); - -#[kani::ensures(true)] -fn hidden_pointer(h: HidesAPointer) {} - -#[kani::proof_for_contract(hidden_pointer)] -fn harness() {} - -#[kani::ensures(true)] -fn plain_pointer(t: *mut i32) {} - -#[kani::proof_for_contract(plain_pointer)] -fn plain_ptr_harness() {} - -#[kani::ensures(true)] -fn return_pointer() -> *const usize { - unreachable!() -} - -#[kani::proof_for_contract(return_pointer)] -fn return_ptr_harness() {} - -#[kani::ensures(true)] -fn allowed_pointer(t: *const bool) {} - -#[kani::proof_for_contract(allowed_pointer)] -fn allowed_pointer_harness() {} - -#[kani::ensures(true)] -fn allowed_mut_ref(t: &mut bool) {} - -#[kani::proof_for_contract(allowed_mut_ref)] -fn allowed_mut_ref_harness() {} - -#[kani::ensures(true)] -fn allowed_ref(t: &bool) {} - -#[kani::proof_for_contract(allowed_ref)] -fn allowed_ref_harness() {} - -#[kani::ensures(true)] -fn allowed_mut_return_ref<'a>() -> &'a mut bool { - unreachable!() -} - -#[kani::proof_for_contract(allowed_mut_return_ref)] -fn allowed_mut_return_ref_harness() {} From 1938aa51a6f6671105035004641ff6c3962c4aea Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 21 Aug 2023 14:24:13 -0700 Subject: [PATCH 29/36] Format? --- .../function-contract/prohibit-pointers/allowed_const_ptr.rs | 2 +- .../function-contract/prohibit-pointers/allowed_mut_ref.rs | 2 +- .../expected/function-contract/prohibit-pointers/allowed_ref.rs | 1 - tests/expected/function-contract/prohibit-pointers/hidden.rs | 2 +- .../function-contract/prohibit-pointers/return_pointer.rs | 1 - 5 files changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs index 666ff3c6af56..3d88fc0926ed 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.rs @@ -12,4 +12,4 @@ fn allowed_pointer_harness() { let _ = Box::new(()); let mut a = Box::new(true); allowed_pointer(Box::into_raw(a)) -} \ No newline at end of file +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs index c70dddf5b84f..22771f76632d 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.rs @@ -12,4 +12,4 @@ fn allowed_mut_ref_harness() { let _ = Box::new(()); let mut a = true; allowed_mut_ref(&mut a) -} \ No newline at end of file +} diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs index 34c2a9bdac6c..3dd4145eff9c 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.rs @@ -13,4 +13,3 @@ fn allowed_ref_harness() { let a = true; allowed_ref(&a) } - diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.rs b/tests/expected/function-contract/prohibit-pointers/hidden.rs index 846b2c25df3a..a28479d2ac5e 100644 --- a/tests/expected/function-contract/prohibit-pointers/hidden.rs +++ b/tests/expected/function-contract/prohibit-pointers/hidden.rs @@ -14,4 +14,4 @@ fn hidden_pointer(h: HidesAPointer) {} fn harness() { let mut a = 0; hidden_pointer(HidesAPointer(&mut a)) -} \ No newline at end of file +} diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs index ecadb49b9d72..44e57ed9bc9d 100644 --- a/tests/expected/function-contract/prohibit-pointers/return_pointer.rs +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.rs @@ -13,4 +13,3 @@ fn return_pointer() -> *const usize { fn return_ptr_harness() { return_pointer(); } - From 36b0dee1dc27ca69222811a5f96c807780f0adef Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 22 Aug 2023 16:03:35 -0700 Subject: [PATCH 30/36] Seriously? --- tests/expected/function-contract/prohibit-pointers/hidden.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.rs b/tests/expected/function-contract/prohibit-pointers/hidden.rs index a28479d2ac5e..9ca23fe6b2e1 100644 --- a/tests/expected/function-contract/prohibit-pointers/hidden.rs +++ b/tests/expected/function-contract/prohibit-pointers/hidden.rs @@ -1,4 +1,3 @@ - // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts From 107b582101d7141e3d03d883695cac709d38c74b Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 22 Aug 2023 18:22:17 -0700 Subject: [PATCH 31/36] Comply with lifetime variables in fun sigs --- kani-compiler/src/kani_middle/mod.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index d734d7952f0b..8b6789084ead 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -147,8 +147,18 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) } - let fn_typ = - instance.ty(tcx, ParamEnv::reveal_all()).fn_sig(tcx).no_bound_vars().expect("impossible"); + let bound_fn_sig = instance.ty(tcx, ParamEnv::reveal_all()).fn_sig(tcx); + + for v in bound_fn_sig.bound_vars() { + if let ty::BoundVariableKind::Ty(t) = v { + tcx.sess.span_err( + tcx.def_span(instance.def_id()), + format!("Found a bound type variable {t:?} after monomorphization"), + ); + } + } + + let fn_typ = bound_fn_sig.skip_binder(); for (typ, (is_prohibited, r#where, what)) in fn_typ .inputs() From c6a4a0e89d88374970efca57ea217079ea24ced4 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 22 Aug 2023 18:44:51 -0700 Subject: [PATCH 32/36] Only complain for active contract attributes --- kani-compiler/src/kani_middle/attributes.rs | 17 ++++++++++------- .../attribute_complain.expected | 1 + .../function-contract/attribute_complain.rs | 11 +++++++++++ .../attribute_no_complain.expected | 1 + .../function-contract/attribute_no_complain.rs | 8 ++++++++ 5 files changed, 31 insertions(+), 7 deletions(-) create mode 100644 tests/expected/function-contract/attribute_complain.expected create mode 100644 tests/expected/function-contract/attribute_complain.rs create mode 100644 tests/expected/function-contract/attribute_no_complain.expected create mode 100644 tests/expected/function-contract/attribute_no_complain.rs diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index f0e2c0849e21..b52e82781a1e 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -59,12 +59,15 @@ impl KaniAttributeKind { } } - /// Is this attribute kind one of the suite of attributes that form the - /// function contracts API. E.g. where [`Self::is_function_contract`] is - /// true but also auto harness attributes like `proof_for_contract` - pub fn is_function_contract_api(self) -> bool { - use KaniAttributeKind::*; - self.is_function_contract() || matches!(self, ProofForContract) + /// Is this an "active" function contract attribute? This means it is is + /// part of the function contract interface *and* it implies that a contract + /// will be used (stubbed or checked) in some way, thus requiring that the + /// user activate the unstable feature. + /// + /// If we find an "inactive" contract attribute we chose not to error, + /// because it wouldn't have any effect anyway. + pub fn demands_function_contract_use(self) -> bool { + matches!(self, KaniAttributeKind::ProofForContract) } /// Would this attribute be placed on a function as part of a function @@ -242,7 +245,7 @@ impl<'tcx> KaniAttributes<'tcx> { // If the `function-contracts` unstable feature is not enabled then no // function should use any of those APIs. if !enabled_features.iter().any(|feature| feature == "function-contracts") { - for kind in self.map.keys().copied().filter(|a| a.is_function_contract_api()) { + for kind in self.map.keys().copied().filter(|a| a.demands_function_contract_use()) { let msg = format!( "Using the {} attribute requires activating the unstable `function-contracts` feature", kind.as_ref() diff --git a/tests/expected/function-contract/attribute_complain.expected b/tests/expected/function-contract/attribute_complain.expected new file mode 100644 index 000000000000..5e5253c34ac8 --- /dev/null +++ b/tests/expected/function-contract/attribute_complain.expected @@ -0,0 +1 @@ +error: Using the proof_for_contract attribute requires activating the unstable `function-contracts` feature \ No newline at end of file diff --git a/tests/expected/function-contract/attribute_complain.rs b/tests/expected/function-contract/attribute_complain.rs new file mode 100644 index 000000000000..f16e975c2001 --- /dev/null +++ b/tests/expected/function-contract/attribute_complain.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(true)] +fn always() {} + +#[kani::proof_for_contract(always)] +fn always_harness() { + let _ = Box::new(()); + always(); +} diff --git a/tests/expected/function-contract/attribute_no_complain.expected b/tests/expected/function-contract/attribute_no_complain.expected new file mode 100644 index 000000000000..880f00714b32 --- /dev/null +++ b/tests/expected/function-contract/attribute_no_complain.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/function-contract/attribute_no_complain.rs b/tests/expected/function-contract/attribute_no_complain.rs new file mode 100644 index 000000000000..bcf1f0cadafd --- /dev/null +++ b/tests/expected/function-contract/attribute_no_complain.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::ensures(true)] +fn always() {} + +#[kani::proof] +fn random_harness() {} From e1fadd4eb948656367d96fe8cb1692a38c600192 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 25 Aug 2023 16:39:06 -0700 Subject: [PATCH 33/36] Addressing more comments --- kani-compiler/src/kani_middle/attributes.rs | 170 ++++++++++--------- library/kani/src/lib.rs | 28 +-- library/kani_macros/src/sysroot/contracts.rs | 8 + 3 files changed, 117 insertions(+), 89 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index b52e82781a1e..3ca508e5aa8a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -137,33 +137,31 @@ 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). - fn interpret_the_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); + fn interpret_the_for_contract_attribute( + &self, + ) -> Option> { + self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { + let name = expect_key_string_value(self.tcx.sess, target)?; let resolved = resolve_fn( self.tcx, self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), name.as_str(), ); - match resolved { - Err(e) => { - self.tcx.sess.span_err( - target.span, - format!( - "Failed to resolve replacement function {} because {e}", - name.as_str() - ), - ); - None - } - Ok(ok) => Some((name, ok, target.span)), - } + resolved.map(|ok| (name, ok, target.span)).map_err(|resolve_err| { + self.tcx.sess.span_err( + target.span, + format!( + "Failed to resolve replacement function {} because {resolve_err}", + name.as_str() + ), + ) + }) }) } - /// Extact the name of the sibling function this contract is checked with + /// Extract the name of the sibling function this contract is checked with /// (if any) - pub fn checked_with(&self) -> Option { + pub fn checked_with(&self) -> Option> { self.expect_maybe_one(KaniAttributeKind::CheckedWith) .map(|target| expect_key_string_value(self.tcx.sess, target)) } @@ -302,64 +300,54 @@ impl<'tcx> KaniAttributes<'tcx> { /// Note that all attributes should be valid by now. pub fn harness_attributes(&self) -> HarnessAttributes { // Abort if not local. - let Some(local_id) = self.item.as_local() else { + if !self.item.is_local() { panic!("Expected a local item, but got: {:?}", self.item); }; trace!(?self, "extract_harness_attributes"); assert!(self.is_harness()); - let mut attrs = self.map.iter().fold( - HarnessAttributes::default(), - |mut harness, (kind, attributes)| { - match kind { - KaniAttributeKind::ShouldPanic => harness.should_panic = true, - KaniAttributeKind::Solver => { - harness.solver = parse_solver(self.tcx, attributes[0]); - } - KaniAttributeKind::Stub => { - harness.stubs = parse_stubs(self.tcx, self.item, attributes); - } - KaniAttributeKind::Unwind => { - harness.unwind_value = parse_unwind(self.tcx, attributes[0]) - } - KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract => { - harness.proof = true - } - KaniAttributeKind::Unstable => { - // Internal attribute which shouldn't exist here. - unreachable!() - } - KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { - todo!("Contract attributes are not supported on proofs") - } - }; - harness - }, - ); - let current_module = self.tcx.parent_module_from_def_id(local_id); - attrs.stubs.extend( - self.interpret_the_for_contract_attribute() - .and_then(|(name, id, span)| { - let replacement_name = KaniAttributes::for_item(self.tcx, id).checked_with(); - if replacement_name.is_none() { + self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { + match kind { + KaniAttributeKind::ShouldPanic => harness.should_panic = true, + KaniAttributeKind::Solver => { + harness.solver = parse_solver(self.tcx, attributes[0]); + } + KaniAttributeKind::Stub => { + harness.stubs.extend_from_slice(&parse_stubs(self.tcx, self.item, attributes)); + } + KaniAttributeKind::Unwind => { + harness.unwind_value = parse_unwind(self.tcx, attributes[0]) + } + KaniAttributeKind::Proof => harness.proof = true, + KaniAttributeKind::ProofForContract => { + harness.proof = true; + let Some(Ok((name, id, span))) = self.interpret_the_for_contract_attribute() + else { + self.tcx.sess.span_err( + self.tcx.def_span(self.item), + format!("Invalid `{}` attribute format", kind.as_ref()), + ); + return harness; + }; + let Some(Ok(replacement_name)) = + KaniAttributes::for_item(self.tcx, id).checked_with() + else { self.tcx .sess .span_err(span, "Target function for this check has no contract"); - } - Some((name, replacement_name?)) - }) - .map(|(original, replacement)| { - let replace_str = replacement.as_str(); - let original_str = original.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 } - }), - ); - attrs + return harness; + }; + harness.stubs.push(self.stub_for_relative_item(name, replacement_name)); + } + KaniAttributeKind::Unstable => { + // Internal attribute which shouldn't exist here. + unreachable!() + } + KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated => { + todo!("Contract attributes are not supported on proofs") + } + }; + harness + }) } /// Check that if this item is tagged with a proof_attribute, it is a valid harness. @@ -378,6 +366,18 @@ impl<'tcx> KaniAttributes<'tcx> { } } } + + fn stub_for_relative_item(&self, anchor: Symbol, replacement: Symbol) -> Stub { + let local_id = self.item.expect_local(); + let current_module = self.tcx.parent_module_from_def_id(local_id); + let replace_str = replacement.as_str(); + let original_str = anchor.as_str(); + let replacement = original_str + .rsplit_once("::") + .map_or_else(|| replace_str.to_string(), |t| t.0.to_string() + "::" + replace_str); + resolve::resolve_fn(self.tcx, current_module.to_local_def_id(), &replacement).unwrap(); + Stub { original: original_str.to_string(), replacement } + } } /// An efficient check for the existence for a particular [`KaniAttributeKind`]. @@ -420,22 +420,38 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { /// Expect the contents of this attribute to be of the format #[attribute = /// "value"] and return the `"value"` -fn expect_key_string_value(sess: &Session, attr: &Attribute) -> rustc_span::Symbol { +fn expect_key_string_value( + sess: &Session, + attr: &Attribute, +) -> Result { let span = attr.span; let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else { - sess.span_fatal(span, "Expected attribute of the form #[attr = \"value\"]") + return Err(sess.span_err(span, "Expected attribute of the form #[attr = \"value\"]")); }; let maybe_str = match it { - AttrArgsEq::Ast(expr) => match expr.kind { - ExprKind::Lit(tok) => LitKind::from_token_lit(tok).unwrap().str(), - _ => sess.span_fatal(span, "Expected literal string as right hand side of `=`"), - }, + AttrArgsEq::Ast(expr) => { + if let ExprKind::Lit(tok) = expr.kind { + match LitKind::from_token_lit(tok) { + Ok(l) => l.str(), + Err(err) => { + return Err(sess.span_err( + span, + format!("Invalid string literal on right hand side of `=` {err:?}"), + )); + } + } + } else { + return Err( + sess.span_err(span, "Expected literal string as right hand side of `=`") + ); + } + } AttrArgsEq::Hir(lit) => lit.kind.str(), }; if let Some(str) = maybe_str { - str + Ok(str) } else { - sess.span_fatal(span, "Expected literal string as right hand side of `=`") + Err(sess.span_err(span, "Expected literal string as right hand side of `=`")) } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 91ab123335aa..a91c89ecbceb 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -74,18 +74,22 @@ pub fn assume(cond: bool) { assert!(cond, "`kani::assume` should always hold"); } -/// If the `premise` is true, so must be the `conclusion` -/// -/// Note that boolean operators (such as `||`) are evaluated lazily by Rust. -/// This function is not and both conditions will be evaluated always. As a -/// reult this function is not intended to be used in regular code. Instead it -/// is intended to make implications in a function contract -/// ([`requires`], [`ensures`]) more readable. For eample -/// `implies(self.is_empty(), self.len() == 0)` is a little easier to understand -/// than `!self.is_empty() || self.len() == 0` (which is the inlined definition -/// of this function). -pub fn implies(premise: bool, conclusion: bool) -> bool { - !premise || conclusion +/// `implies!(premise => conclusion)` means that if the `premise` is true, so +/// must be the `conclusion`. +/// +/// This simply expands to `!premise || conclusion` and is intended to be used +/// in function contracts to make them more readable, as the concept of an +/// implication is more natural to think about than its expansion. +/// +/// For further convenience multiple comma separated premises are allowed, and +/// are joined with `||` in the expansion. E.g. `implies!(a, b => c)` expands to +/// `!a || !b || c` and says that `c` is true if both `a` and `b` are true (see +/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)) +#[macro_export] +macro_rules! implies { + ($($premise:expr),+ => $conclusion:expr) => { + $(!$premise)||+ || ($conclusion) + }; } /// A way to break the ownerhip rules. Only used by contracts where we can diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 94c3fe155249..b17bd2bfa928 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -102,6 +102,14 @@ impl<'a> VisitMut for Renamer<'a> { /// Does the provided path have the same chain of identifiers as `mtch` (match) /// and no arguments anywhere? +/// +/// So for instance (using some pseudo-syntax for the [`syn::Path`]s) +/// `matches_path(std::vec::Vec, &["std", "vec", "Vec"]) == true` but +/// `matches_path(std::Vec::::contains, &["std", "Vec", "contains"]) != +/// true`. +/// +/// This is intended to be used to match the internal `kanitool` family of +/// attributes which we know to have a regular structure and no arguments. fn matches_path(path: &syn::Path, mtch: &[E]) -> bool where Ident: std::cmp::PartialEq, From a0b00a2a4a412ed8c91e427eafb9923488ad1a3a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Fri, 25 Aug 2023 17:11:14 -0700 Subject: [PATCH 34/36] I always forget to run thi script instead of `cargo fmt` --- library/kani_macros/src/sysroot/contracts.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index b17bd2bfa928..bce77529ac18 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -102,12 +102,12 @@ impl<'a> VisitMut for Renamer<'a> { /// Does the provided path have the same chain of identifiers as `mtch` (match) /// and no arguments anywhere? -/// +/// /// So for instance (using some pseudo-syntax for the [`syn::Path`]s) /// `matches_path(std::vec::Vec, &["std", "vec", "Vec"]) == true` but /// `matches_path(std::Vec::::contains, &["std", "Vec", "contains"]) != /// true`. -/// +/// /// This is intended to be used to match the internal `kanitool` family of /// attributes which we know to have a regular structure and no arguments. fn matches_path(path: &syn::Path, mtch: &[E]) -> bool From 5447973844e8443926db62c3961abf4205896db3 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 6 Sep 2023 15:12:09 -0700 Subject: [PATCH 35/36] Apply suggestions from code review Co-authored-by: Felipe R. Monteiro --- .../codegen_cprover_gotoc/overrides/hooks.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 14 ++++----- kani-compiler/src/kani_middle/mod.rs | 8 ++--- library/kani/src/lib.rs | 2 +- library/kani_macros/src/lib.rs | 4 +-- library/kani_macros/src/sysroot/contracts.rs | 31 +++++++++---------- 6 files changed, 30 insertions(+), 31 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 3d99f8cdeb3a..1f0125c03446 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -326,7 +326,7 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { } /// A builtin that is essentially a C-style dereference operation, creating an -/// unsafe challow copy. Importantly either this copy or the original needs to +/// unsafe shallow copy. Importantly either this copy or the original needs to /// be `mem::forget`en or a double-free will occur. /// /// Takes in a `&T` reference and returns a `T` (like clone would but without diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 3ca508e5aa8a..11d1e63fb5cc 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -59,7 +59,7 @@ impl KaniAttributeKind { } } - /// Is this an "active" function contract attribute? This means it is is + /// Is this an "active" function contract attribute? This means it is /// part of the function contract interface *and* it implies that a contract /// will be used (stubbed or checked) in some way, thus requiring that the /// user activate the unstable feature. @@ -71,7 +71,7 @@ impl KaniAttributeKind { } /// Would this attribute be placed on a function as part of a function - /// contract. E.g. created by `requires`, `ensures` + /// contract. E.g. created by `requires`, `ensures`. pub fn is_function_contract(self) -> bool { use KaniAttributeKind::*; matches!(self, CheckedWith | IsContractGenerated) @@ -135,7 +135,7 @@ 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`, + /// returned symbol and DefId are respectively the name and id of `TARGET`, /// the span in the span for the attribute (contents). fn interpret_the_for_contract_attribute( &self, @@ -160,7 +160,7 @@ impl<'tcx> KaniAttributes<'tcx> { } /// Extract the name of the sibling function this contract is checked with - /// (if any) + /// (if any). pub fn checked_with(&self) -> Option> { self.expect_maybe_one(KaniAttributeKind::CheckedWith) .map(|target| expect_key_string_value(self.tcx.sess, target)) @@ -391,8 +391,8 @@ fn has_kani_attribute bool>( tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) } -/// Test is this function was generated by expanding a contract attribute like -/// `requires` and `ensures` +/// Test if this function was generated by expanding a contract attribute like +/// `requires` and `ensures`. pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool { has_kani_attribute(tcx, def_id, KaniAttributeKind::is_function_contract) } @@ -419,7 +419,7 @@ pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { } /// Expect the contents of this attribute to be of the format #[attribute = -/// "value"] and return the `"value"` +/// "value"] and return the `"value"`. fn expect_key_string_value( sess: &Session, attr: &Attribute, diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 8b6789084ead..27afd1d7185f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -79,7 +79,7 @@ pub fn check_reachable_items<'tcx>(tcx: TyCtxt<'tcx>, queries: &QueryDb, items: } // We don't short circuit here since this is a type check and can shake - // out differently depending on generic parameters + // out differently depending on generic parameters. if let MonoItem::Fn(instance) = item { if attributes::is_function_contract_generated(tcx, instance.def_id()) { check_is_contract_safe(tcx, *instance); @@ -103,7 +103,7 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { /// composing error messages. r#where: &'static str, /// Adjective to describe the kind of pointer we're prohibiting. - /// Essentially `is_prohibited` but in english + /// Essentially `is_prohibited` but in English. what: &'static str, } @@ -116,7 +116,7 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { } // Rust's type visitor only recurses into type arguments, (e.g. - // `generics` in this match). This is enough for may types, but it + // `generics` in this match). This is enough for many types, but it // won't look at the field types of structs or enums. So we override // it here and do that ourselves. // @@ -137,7 +137,7 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { } std::ops::ControlFlow::Continue(()) } else { - // For every other type + // For every other type. t.super_visit_with(self) } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index a91c89ecbceb..6125c589a957 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -84,7 +84,7 @@ pub fn assume(cond: bool) { /// For further convenience multiple comma separated premises are allowed, and /// are joined with `||` in the expansion. E.g. `implies!(a, b => c)` expands to /// `!a || !b || c` and says that `c` is true if both `a` and `b` are true (see -/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)) +/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)). #[macro_export] macro_rules! implies { ($($premise:expr),+ => $conclusion:expr) => { diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 4b9e21d4be8c..3b4ea87636f3 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -146,10 +146,10 @@ pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { /// /// The harness is expected to set up the arguments that `foo` should be called /// with and initialzied any `static mut` globals that are reachable. All of -/// these should be initialized to as general a value as possible, usually +/// these should be initialized to as general value as possible, usually /// achieved using `kani::any`. The harness must call e.g. `foo` at least once /// and if `foo` has type parameters, only one instantiation of those parameters -/// is admissable. Violating either results in a compile error. +/// is admissible. Violating either results in a compile error. /// /// If any of those types have special invariants you can use `kani::assume` to /// enforce them, but other than condition on inputs and checks of outputs diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index bce77529ac18..6e6ee3ec75a7 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -120,16 +120,16 @@ where && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) } -/// 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 + /// This is the original code, re-emitted from a contract attribute. Original, /// This is the first time a contract attribute is evaluated on this - /// function + /// function. Untouched, /// This is a check function that was generated from a previous evaluation - /// of a contract attribute + /// of a contract attribute. Check, } @@ -185,7 +185,7 @@ struct PostconditionInjector(TokenStream2); impl VisitMut for PostconditionInjector { /// We leave this emtpy to stop the recursion here. We don't want to look /// inside the closure, because the return statements contained within are - /// for a different function, duh. + /// for a different function. fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) {} fn visit_expr_mut(&mut self, i: &mut Expr) { @@ -213,11 +213,11 @@ impl VisitMut for PostconditionInjector { /// A supporting function for creating shallow, unsafe copies of the arguments /// for the postconditions. /// -/// This function -/// - Collects all [`Ident`]s found in the argument patterns -/// - Creates new names for them -/// - Replaces all occurrences of those idents in `attrs` with the new names and -/// - Returns the mapping of old names to new names +/// This function: +/// - Collects all [`Ident`]s found in the argument patterns; +/// - Creates new names for them; +/// - Replaces all occurrences of those idents in `attrs` with the new names and; +/// - Returns the mapping of old names to new names. fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { let mut arg_ident_collector = ArgumentIdentCollector::new(); arg_ident_collector.visit_signature(&sig); @@ -320,14 +320,13 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) if matches!(function_state, ContractFunctionState::Untouched) { // We are the first time a contract is handled on this function, so - // we're responsible for - // - // 1. Generating a name for the check function + // we're responsible for: + // 1. Generating a name for the check function; // 2. Emitting the original, unchanged item and register the check - // function on it via attribute - // 3. Renaming our item to the new name + // 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 + // #[allow(unused_variables)] to the check function attributes. let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); From e424b263d59454284ba99f81a6074a1732de61b1 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 6 Sep 2023 15:11:58 -0700 Subject: [PATCH 36/36] Suggestions from code review --- .../codegen_cprover_gotoc/overrides/hooks.rs | 8 +- kani-compiler/src/kani_middle/attributes.rs | 25 +- library/kani_macros/src/sysroot/contracts.rs | 21 +- .../arbitrary_requires_fail.expected | 2 +- .../arbitrary_requires_pass.expected | 2 +- .../attribute_complain.expected | 2 +- .../attribute_no_complain.expected | 2 +- .../checking_from_external_mod.expected | 2 +- .../gcd_failure_code.expected | 1 - tests/expected/function-contract/out.txt | 258 ------------------ .../function-contract/pattern_use.expected | 2 +- .../allowed_const_ptr.expected | 2 +- .../allowed_mut_ref.expected | 2 +- .../allowed_mut_return_ref.expected | 2 +- .../prohibit-pointers/allowed_ref.expected | 2 +- .../prohibit-pointers/hidden.expected | 2 +- .../prohibit-pointers/plain_pointer.expected | 2 +- .../prohibit-pointers/return_pointer.expected | 2 +- 18 files changed, 48 insertions(+), 291 deletions(-) delete mode 100644 tests/expected/function-contract/out.txt diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 1f0125c03446..0287e4b9b01f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -348,7 +348,13 @@ impl<'tcx> GotocHook<'tcx> for UntrackedDeref { _target: Option, span: Option, ) -> Stmt { - assert_eq!(fargs.len(), 1); + assert_eq!( + fargs.len(), + 1, + "Invariant broken. `untracked_deref` should only be given one argument. \ + This function should only be called from code generated by kani macros, \ + as such this is likely a code-generation error." + ); let loc = tcx.codegen_span_option(span); Stmt::block( vec![Stmt::assign( diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 11d1e63fb5cc..d1ef8fdf33e3 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -173,14 +173,13 @@ impl<'tcx> KaniAttributes<'tcx> { // Check that all attributes are correctly used and well formed. let is_harness = self.is_harness(); for (&kind, attrs) in self.map.iter() { + let local_error = |msg| self.tcx.sess.span_err(attrs[0].span, msg); + if !is_harness && kind.is_harness_only() { - self.tcx.sess.span_err( - attrs[0].span, - format!( - "the `{}` attribute also requires the `#[kani::proof]` attribute", - kind.as_ref() - ), - ); + local_error(format!( + "the `{}` attribute also requires the `#[kani::proof]` attribute", + kind.as_ref() + )); } match kind { KaniAttributeKind::ShouldPanic => { @@ -205,7 +204,11 @@ impl<'tcx> KaniAttributes<'tcx> { }) } KaniAttributeKind::Proof => { - assert!(!self.map.contains_key(&KaniAttributeKind::ProofForContract)); + if self.map.contains_key(&KaniAttributeKind::ProofForContract) { + local_error( + "`proof` and `proof_for_contract` may not be used on the same function.".to_string(), + ); + } expect_single(self.tcx, kind, &attrs); attrs.iter().for_each(|attr| self.check_proof_attribute(attr)) } @@ -213,7 +216,11 @@ impl<'tcx> KaniAttributes<'tcx> { let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx)); }), KaniAttributeKind::ProofForContract => { - assert!(!self.map.contains_key(&KaniAttributeKind::Proof)); + if self.map.contains_key(&KaniAttributeKind::Proof) { + local_error( + "`proof` and `proof_for_contract` may not be used on the same function.".to_string(), + ); + } expect_single(self.tcx, kind, &attrs); } KaniAttributeKind::CheckedWith => { diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index 6e6ee3ec75a7..856f25b7d597 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -250,11 +250,12 @@ fn rename_argument_occurences(sig: &syn::Signature, attr: &mut Expr) -> HashMap< /// added before the body and postconditions after as well as injected before /// every `return` (see [`PostconditionInjector`]). Attributes on the original /// function are also copied to the check function. Each clause (requires or -/// ensures) after the first will be ignored on the original function (detected -/// by finding the `kanitool::checked_with` attribute). On the check function -/// (detected by finding the `kanitool::is_contract_generated` attribute) it -/// expands into a new layer of pre- or postconditions. This state machine is -/// also explained in more detail in comments in the body of this macro. +/// ensures) after the first clause will be ignored on the original function +/// (detected by finding the `kanitool::checked_with` attribute). On the check +/// function (detected by finding the `kanitool::is_contract_generated` +/// attribute) it expands into a new layer of pre- or postconditions. This state +/// machine is also explained in more detail in comments in the body of this +/// macro. /// /// In the check function all named arguments of the function are unsafely /// shallow-copied with the `kani::untracked_deref` function to circumvent the @@ -330,10 +331,12 @@ fn requires_ensures_alt(attr: TokenStream, item: TokenStream, is_requires: bool) let check_fn_name = identifier_for_generated_function(item_fn, "check", a_short_hash); - // Constructing string literals explicitly here, because if we call - // `stringify!` in the generated code that is passed on as that - // expression to the next expansion of a contract, not as the - // literal. + // Constructing string literals explicitly here, because `stringify!` + // doesn't work. Let's say we have an identifier `check_fn` and we were + // to do `quote!(stringify!(check_fn))` to try to have it expand to + // `"check_fn"` in the generated code. Then when the next macro parses + // this it will *not* see the literal `"check_fn"` as you may expect but + // instead the *expression* `stringify!(check_fn)`. let check_fn_name_str = syn::LitStr::new(&check_fn_name.to_string(), Span::call_site()); // The order of `attrs` and `kanitool::{checked_with, diff --git a/tests/expected/function-contract/arbitrary_requires_fail.expected b/tests/expected/function-contract/arbitrary_requires_fail.expected index d388a4b084f4..179430b8a249 100644 --- a/tests/expected/function-contract/arbitrary_requires_fail.expected +++ b/tests/expected/function-contract/arbitrary_requires_fail.expected @@ -1,4 +1,4 @@ assertion\ - Status: FAILURE\ - Description: "attempt to divide by zero"\ -arbitrary_requires_fail.rs:7:5 \ No newline at end of file +arbitrary_requires_fail.rs:7:5 diff --git a/tests/expected/function-contract/arbitrary_requires_pass.expected b/tests/expected/function-contract/arbitrary_requires_pass.expected index 2954b60fecd1..814fe6757ca3 100644 --- a/tests/expected/function-contract/arbitrary_requires_pass.expected +++ b/tests/expected/function-contract/arbitrary_requires_pass.expected @@ -3,4 +3,4 @@ div.arithmetic_overflow\ - Description: "attempt to divide by zero"\ in function div -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/attribute_complain.expected b/tests/expected/function-contract/attribute_complain.expected index 5e5253c34ac8..8edcde3df910 100644 --- a/tests/expected/function-contract/attribute_complain.expected +++ b/tests/expected/function-contract/attribute_complain.expected @@ -1 +1 @@ -error: Using the proof_for_contract attribute requires activating the unstable `function-contracts` feature \ No newline at end of file +error: Using the proof_for_contract attribute requires activating the unstable `function-contracts` feature diff --git a/tests/expected/function-contract/attribute_no_complain.expected b/tests/expected/function-contract/attribute_no_complain.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/attribute_no_complain.expected +++ b/tests/expected/function-contract/attribute_no_complain.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/checking_from_external_mod.expected b/tests/expected/function-contract/checking_from_external_mod.expected index 99a44f49ab82..c31b5c389fc8 100644 --- a/tests/expected/function-contract/checking_from_external_mod.expected +++ b/tests/expected/function-contract/checking_from_external_mod.expected @@ -2,4 +2,4 @@ - Description: "(result == x) | (result == y)"\ in function max -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/gcd_failure_code.expected b/tests/expected/function-contract/gcd_failure_code.expected index 4112115e2a01..9488e9dcac9a 100644 --- a/tests/expected/function-contract/gcd_failure_code.expected +++ b/tests/expected/function-contract/gcd_failure_code.expected @@ -6,4 +6,3 @@ in function gcd Failed Checks: result != 0 && x % result == 0 && y % result == 0 VERIFICATION:- FAILED - diff --git a/tests/expected/function-contract/out.txt b/tests/expected/function-contract/out.txt deleted file mode 100644 index 6f95e232cd7a..000000000000 --- a/tests/expected/function-contract/out.txt +++ /dev/null @@ -1,258 +0,0 @@ -Kani Rust Verifier 0.34.0 (standalone) -Checking harness div_harness... -CBMC 5.88.1 (cbmc-5.88.1) -CBMC version 5.88.1 (cbmc-5.88.1) 64-bit arm64 macos -Reading GOTO program from file /Users/justbldr/research/kani/tests/expected/function-contract/arbitrary_requires_pass__RNvCs6zRRqCRMgBy_23arbitrary_requires_pass11div_harness.out -Generating GOTO Program -Adding CPROVER library (arm64) -Removal of function pointers and virtual functions -Generic Property Instrumentation -Running with 16 object bits, 48 offset bits (user-specified) -Starting Bounded Model Checking -Runtime Symex: 0.0207943s -size of program expression: 733 steps -slicing removed 435 assignments -Generated 23 VCC(s), 7 remaining after simplification -Runtime Postprocess Equation: 6.0625e-05s -Passing problem to propositional reduction -converting SSA -Runtime Convert SSA: 0.0008905s -Running propositional reduction -Post-processing -Runtime Post-process: 5.541e-06s -Solving with CaDiCaL sc2021 -625 variables, 647 clauses -SAT checker: instance is SATISFIABLE -Runtime Solver: 7.8584e-05s -Runtime decision procedure: 0.00102646s -Running propositional reduction -Solving with CaDiCaL sc2021 -625 variables, 648 clauses -SAT checker: instance is UNSATISFIABLE -Runtime Solver: 3.8291e-05s -Runtime decision procedure: 7.0834e-05s - -RESULTS: -Check 1: __rust_dealloc.assertion.1 - - Status: SUCCESS - - Description: "Alignment is power of two" - - Location: ../../../library/kani/kani_lib.c:84 in function __rust_dealloc - -Check 2: __rust_dealloc.assertion.2 - - Status: SUCCESS - - Description: "rust_dealloc must be called on an object whose allocated size matches its layout" - - Location: ../../../library/kani/kani_lib.c:86 in function __rust_dealloc - -Check 3: div.assertion.1 - - Status: SUCCESS - - Description: "attempt to divide by zero" - - Location: arbitrary_requires_pass.rs:7:5 in function div - -Check 4: div.arithmetic_overflow.1 - - Status: SUCCESS - - Description: "attempt to divide by zero" - - Location: arbitrary_requires_pass.rs:7:5 in function div - -Check 5: core::panicking::panic_nounwind_fmt.unsupported_construct.1 - - Status: SUCCESS - - Description: "call to foreign "Rust" function `rust_begin_unwind` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panicking.rs:89:9 in function core::panicking::panic_nounwind_fmt - -Check 6: core::panicking::panic_nounwind_fmt.assertion.1 - - Status: SUCCESS - - Description: "reached intrinsic::abort" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panicking.rs:82:9 in function core::panicking::panic_nounwind_fmt - -Check 7: malloc.assertion.1 - - Status: SUCCESS - - Description: "max allocation size exceeded" - - Location: :31 in function malloc - -Check 8: malloc.assertion.2 - - Status: SUCCESS - - Description: "max allocation may fail" - - Location: :36 in function malloc - -Check 9: std::panic::Location::<'_>::caller.unsupported_construct.1 - - Status: SUCCESS - - Description: "caller_location is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/374" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/panic/location.rs:88:9 in function std::panic::Location::<'_>::caller - -Check 10: std::ptr::Alignment::as_usize.assume.1 - - Status: SUCCESS - - Description: "assumption failed" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/alignment.rs:96:9 in function std::ptr::Alignment::as_usize - -Check 11: std::fmt::Arguments::<'_>::new_const.assertion.1 - - Status: SUCCESS - - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:299:13 in function std::fmt::Arguments::<'_>::new_const - -Check 12: std::fmt::Arguments::<'_>::new_const.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/fmt/mod.rs:301:34 in function std::fmt::Arguments::<'_>::new_const - -Check 13: __rust_dealloc.precondition_instance.1 - - Status: SUCCESS - - Description: "free argument must be NULL or valid pointer" - - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc - -Check 14: __rust_dealloc.precondition_instance.2 - - Status: SUCCESS - - Description: "free argument must be dynamic object" - - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc - -Check 15: __rust_dealloc.precondition_instance.3 - - Status: SUCCESS - - Description: "free argument has offset zero" - - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc - -Check 16: __rust_dealloc.precondition_instance.4 - - Status: SUCCESS - - Description: "double free" - - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc - -Check 17: __rust_dealloc.precondition_instance.5 - - Status: SUCCESS - - Description: "free called for new[] object" - - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc - -Check 18: __rust_dealloc.precondition_instance.6 - - Status: SUCCESS - - Description: "free called for stack-allocated object" - - Location: ../../../library/kani/kani_lib.c:88 in function __rust_dealloc - -Check 19: std::ptr::drop_in_place::>.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> - -Check 20: std::ptr::drop_in_place::>.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> - -Check 21: std::ptr::drop_in_place::>.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> - -Check 22: std::ptr::drop_in_place::>.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> - -Check 23: std::ptr::drop_in_place::>.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> - -Check 24: std::ptr::drop_in_place::>.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs:497:1 in function std::ptr::drop_in_place::> - -Check 25: as std::ops::Drop>::drop.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop - -Check 26: as std::ops::Drop>::drop.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop - -Check 27: as std::ops::Drop>::drop.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop - -Check 28: as std::ops::Drop>::drop.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop - -Check 29: as std::ops::Drop>::drop.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop - -Check 30: as std::ops::Drop>::drop.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1230:19 in function as std::ops::Drop>::drop - -Check 31: std::alloc::Layout::align.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align - -Check 32: std::alloc::Layout::align.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align - -Check 33: std::alloc::Layout::align.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align - -Check 34: std::alloc::Layout::align.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align - -Check 35: std::alloc::Layout::align.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align - -Check 36: std::alloc::Layout::align.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:140:9 in function std::alloc::Layout::align - -Check 37: div.division-by-zero.1 - - Status: SUCCESS - - Description: "division by zero" - - Location: arbitrary_requires_pass.rs:7:5 in function div - -Check 38: std::alloc::Layout::size.pointer_dereference.1 - - Status: SUCCESS - - Description: "dereference failure: pointer NULL" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size - -Check 39: std::alloc::Layout::size.pointer_dereference.2 - - Status: SUCCESS - - Description: "dereference failure: pointer invalid" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size - -Check 40: std::alloc::Layout::size.pointer_dereference.3 - - Status: SUCCESS - - Description: "dereference failure: deallocated dynamic object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size - -Check 41: std::alloc::Layout::size.pointer_dereference.4 - - Status: SUCCESS - - Description: "dereference failure: dead object" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size - -Check 42: std::alloc::Layout::size.pointer_dereference.5 - - Status: SUCCESS - - Description: "dereference failure: pointer outside object bounds" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size - -Check 43: std::alloc::Layout::size.pointer_dereference.6 - - Status: SUCCESS - - Description: "dereference failure: invalid integer address" - - Location: ../../../../../.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/alloc/layout.rs:129:9 in function std::alloc::Layout::size - - -SUMMARY: - ** 0 of 43 failed - -VERIFICATION:- SUCCESSFUL -Verification Time: 0.44933715s - -Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/function-contract/pattern_use.expected b/tests/expected/function-contract/pattern_use.expected index 086baf514cc8..1485191557db 100644 --- a/tests/expected/function-contract/pattern_use.expected +++ b/tests/expected/function-contract/pattern_use.expected @@ -1,3 +1,3 @@ assertion\ - Status: FAILURE\ -- Description: "attempt to divide by zero"\ \ No newline at end of file +- Description: "attempt to divide by zero"\ diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected +++ b/tests/expected/function-contract/prohibit-pointers/allowed_const_ptr.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_ref.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected +++ b/tests/expected/function-contract/prohibit-pointers/allowed_mut_return_ref.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected b/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected index 880f00714b32..34c886c358cb 100644 --- a/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected +++ b/tests/expected/function-contract/prohibit-pointers/allowed_ref.expected @@ -1 +1 @@ -VERIFICATION:- SUCCESSFUL \ No newline at end of file +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/prohibit-pointers/hidden.expected b/tests/expected/function-contract/prohibit-pointers/hidden.expected index ccc1120292d8..59e40d5aadc8 100644 --- a/tests/expected/function-contract/prohibit-pointers/hidden.expected +++ b/tests/expected/function-contract/prohibit-pointers/hidden.expected @@ -1 +1 @@ -error: This argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file +error: This argument contains a mutable pointer (*mut u32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. diff --git a/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected b/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected index eb9669c21348..916854aa3131 100644 --- a/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected +++ b/tests/expected/function-contract/prohibit-pointers/plain_pointer.expected @@ -1 +1 @@ -error: This argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file +error: This argument contains a mutable pointer (*mut i32). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. diff --git a/tests/expected/function-contract/prohibit-pointers/return_pointer.expected b/tests/expected/function-contract/prohibit-pointers/return_pointer.expected index ebf53e6afff1..8f3689888d92 100644 --- a/tests/expected/function-contract/prohibit-pointers/return_pointer.expected +++ b/tests/expected/function-contract/prohibit-pointers/return_pointer.expected @@ -1 +1 @@ -error: The return contains a pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior. \ No newline at end of file +error: The return contains a pointer (*const usize). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.