From c426d888f6644d6b4090656e92ec19a073aac37e Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 17 Oct 2024 11:40:40 -0700 Subject: [PATCH 1/6] Emit an error when proof_for_contract function is not found --- .../codegen_cprover_gotoc/codegen/contract.rs | 45 ++++++++++++------- .../compiler_interface.rs | 10 +++-- tests/ui/unknown-contract-harness/expected | 6 +++ tests/ui/unknown-contract-harness/test.rs | 14 ++++++ 4 files changed, 55 insertions(+), 20 deletions(-) create mode 100644 tests/ui/unknown-contract-harness/expected create mode 100644 tests/ui/unknown-contract-harness/test.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 254fc854e8b5..74f64b6d0189 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -7,6 +7,7 @@ use cbmc::goto_program::{Expr, Lambda, Location, Type}; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; +use rustc_span::Span; use stable_mir::CrateDef; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::mir::{Local, VarDebugInfoContents}; @@ -18,7 +19,8 @@ impl GotocCtx<'_> { /// for which it needs to be enforced. /// /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one - /// instance of it. Panics if there are more or less than one instance. + /// instance of it. Returns `None` if the target was not found. Panics if there are more + /// than one instance. /// 2. The additional arguments for the inner checks are locations that may be modified. /// Add them to the list of CBMC's assigns. /// 3. Returns the mangled name of the symbol it attached the contract to. @@ -29,24 +31,35 @@ impl GotocCtx<'_> { pub fn handle_check_contract( &mut self, function_under_contract: InternalDefId, + span: Span, items: &[MonoItem], - ) -> AssignsContract { + ) -> Option { let tcx = self.tcx; - let modify = items - .iter() - .find_map(|item| { - // Find the instance under contract - let MonoItem::Fn(instance) = *item else { return None }; - if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { - self.find_modifies(instance) - } else { - None - } + let modify = items.iter().find_map(|item| { + // Find the instance under contract + let MonoItem::Fn(instance) = *item else { return None }; + if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { + self.find_modifies(instance) + } else { + None + } + }); + if let Some(modify) = modify { + self.attach_modifies_contract(modify); + let recursion_tracker = self.find_recursion_tracker(items); + Some(AssignsContract { + recursion_tracker, + contracted_function_name: modify.mangled_name(), }) - .unwrap(); - self.attach_modifies_contract(modify); - let recursion_tracker = self.find_recursion_tracker(items); - AssignsContract { recursion_tracker, contracted_function_name: modify.mangled_name() } + } else { + let name = tcx.def_path_str(function_under_contract); + let err_msg = format!( + "The function specified in the `proof_for_contract` attribute, `{name}`, was not found.\ + \nMake sure the function is reachable from the harness." + ); + tcx.dcx().span_err(span, err_msg); + None + } } /// The name and location for the recursion tracker should match the exact information added diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 25bc0cbe8ad1..3a3efccf901a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -40,6 +40,7 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; +use rustc_span::Span; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; @@ -81,7 +82,7 @@ impl GotocCodegenBackend { starting_items: &[MonoItem], symtab_goto: &Path, machine_model: &MachineModel, - check_contract: Option, + check_contract: Option<(InternalDefId, Span)>, mut transformer: BodyTransformation, ) -> (GotocCtx<'tcx>, Vec, Option) { // This runs reachability analysis before global passes are applied. @@ -180,7 +181,8 @@ impl GotocCodegenBackend { } } - check_contract.map(|check_id| gcx.handle_check_contract(check_id, &items)) + check_contract + .and_then(|(check_id, span)| gcx.handle_check_contract(check_id, span, &items)) }, "codegen", ); @@ -452,9 +454,9 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { } } -fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option { +fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<(InternalDefId, Span)> { let attrs = KaniAttributes::for_def_id(tcx, def_id); - attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) + attrs.interpret_for_contract_attribute().map(|(_, id, span)| (id, span)) } fn check_target(session: &Session) { diff --git a/tests/ui/unknown-contract-harness/expected b/tests/ui/unknown-contract-harness/expected new file mode 100644 index 000000000000..dec02f9b0a50 --- /dev/null +++ b/tests/ui/unknown-contract-harness/expected @@ -0,0 +1,6 @@ +error: The function specified in the `proof_for_contract` attribute, `foo`, was not found.\ +Make sure the function is reachable from the harness. +test.rs:\ +|\ +| #[kani::proof_for_contract(foo)]\ +| ^^^^^^^^^^^^^^ diff --git a/tests/ui/unknown-contract-harness/test.rs b/tests/ui/unknown-contract-harness/test.rs new file mode 100644 index 000000000000..70c323c144aa --- /dev/null +++ b/tests/ui/unknown-contract-harness/test.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// This test checks Kani's error when function specified in `proof_for_contract` +// harness is not found (e.g. because it's not reachable from the harness) + +#[kani::requires(true)] +fn foo() {} + +#[kani::proof_for_contract(foo)] +fn check_foo() { + assert!(true); +} From abdbeb89256baca90d2177b15c7aadf4a5f6b6ff Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 18 Oct 2024 15:38:10 -0700 Subject: [PATCH 2/6] Move the check to kani_middle --- .../codegen_cprover_gotoc/codegen/contract.rs | 45 +++++++------------ .../compiler_interface.rs | 10 ++--- kani-compiler/src/kani_middle/attributes.rs | 16 ++++++- kani-compiler/src/kani_middle/mod.rs | 14 ++++-- 4 files changed, 45 insertions(+), 40 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 74f64b6d0189..254fc854e8b5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -7,7 +7,6 @@ use cbmc::goto_program::{Expr, Lambda, Location, Type}; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; -use rustc_span::Span; use stable_mir::CrateDef; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::mir::{Local, VarDebugInfoContents}; @@ -19,8 +18,7 @@ impl GotocCtx<'_> { /// for which it needs to be enforced. /// /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one - /// instance of it. Returns `None` if the target was not found. Panics if there are more - /// than one instance. + /// instance of it. Panics if there are more or less than one instance. /// 2. The additional arguments for the inner checks are locations that may be modified. /// Add them to the list of CBMC's assigns. /// 3. Returns the mangled name of the symbol it attached the contract to. @@ -31,35 +29,24 @@ impl GotocCtx<'_> { pub fn handle_check_contract( &mut self, function_under_contract: InternalDefId, - span: Span, items: &[MonoItem], - ) -> Option { + ) -> AssignsContract { let tcx = self.tcx; - let modify = items.iter().find_map(|item| { - // Find the instance under contract - let MonoItem::Fn(instance) = *item else { return None }; - if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { - self.find_modifies(instance) - } else { - None - } - }); - if let Some(modify) = modify { - self.attach_modifies_contract(modify); - let recursion_tracker = self.find_recursion_tracker(items); - Some(AssignsContract { - recursion_tracker, - contracted_function_name: modify.mangled_name(), + let modify = items + .iter() + .find_map(|item| { + // Find the instance under contract + let MonoItem::Fn(instance) = *item else { return None }; + if rustc_internal::internal(tcx, instance.def.def_id()) == function_under_contract { + self.find_modifies(instance) + } else { + None + } }) - } else { - let name = tcx.def_path_str(function_under_contract); - let err_msg = format!( - "The function specified in the `proof_for_contract` attribute, `{name}`, was not found.\ - \nMake sure the function is reachable from the harness." - ); - tcx.dcx().span_err(span, err_msg); - None - } + .unwrap(); + self.attach_modifies_contract(modify); + let recursion_tracker = self.find_recursion_tracker(items); + AssignsContract { recursion_tracker, contracted_function_name: modify.mangled_name() } } /// The name and location for the recursion tracker should match the exact information added diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 3a3efccf901a..25bc0cbe8ad1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -40,7 +40,6 @@ use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; -use rustc_span::Span; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; @@ -82,7 +81,7 @@ impl GotocCodegenBackend { starting_items: &[MonoItem], symtab_goto: &Path, machine_model: &MachineModel, - check_contract: Option<(InternalDefId, Span)>, + check_contract: Option, mut transformer: BodyTransformation, ) -> (GotocCtx<'tcx>, Vec, Option) { // This runs reachability analysis before global passes are applied. @@ -181,8 +180,7 @@ impl GotocCodegenBackend { } } - check_contract - .and_then(|(check_id, span)| gcx.handle_check_contract(check_id, span, &items)) + check_contract.map(|check_id| gcx.handle_check_contract(check_id, &items)) }, "codegen", ); @@ -454,9 +452,9 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { } } -fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option<(InternalDefId, Span)> { +fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option { let attrs = KaniAttributes::for_def_id(tcx, def_id); - attrs.interpret_for_contract_attribute().map(|(_, id, span)| (id, span)) + attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) } fn check_target(session: &Session) { diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 0085928a37d0..ba3cc09c2b62 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains code for processing Rust attributes (like `kani::proof`). -use std::collections::BTreeMap; +use std::collections::{BTreeMap, HashSet}; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; @@ -474,6 +474,20 @@ impl<'tcx> KaniAttributes<'tcx> { || self.map.contains_key(&KaniAttributeKind::ProofForContract) } + pub fn check_proof_for_contract(&self, functions: &HashSet) { + if let Some((symbol, id, span)) = self.interpret_for_contract_attribute() { + if !functions.contains(&id) { + let err_msg = format!( + "The function specified in the `proof_for_contract` attribute, `{symbol}`, was not found.\ + \nMake sure the function is reachable from the harness." + ); + self.tcx.dcx().span_err(span, err_msg); + } + } + } + + /// Check that the `proof` attribute is valid. + /// Extract harness attributes for a given `def_id`. /// /// We only extract attributes for harnesses that are local to the current crate. diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 5fead860320c..617b85839375 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -18,8 +18,8 @@ use rustc_span::Span; use rustc_span::source_map::respan; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use stable_mir::CrateDef; -use stable_mir::mir::mono::MonoItem; +use stable_mir::{CrateDef, DefId}; +use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; use std::ops::ControlFlow; @@ -101,6 +101,10 @@ impl TyVisitor for FindUnsafeCell<'_> { pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); + let functions: HashSet = items.iter().filter_map(|i| match i { + MonoItem::Fn(instance) => Some(rustc_internal::internal(tcx, instance.def.def_id())), + _ => None, + }).collect(); for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) { let def_id = match item { MonoItem::Fn(instance) => instance.def.def_id(), @@ -110,9 +114,11 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) } }; if !def_ids.contains(&def_id) { + let attributes = KaniAttributes::for_def_id(tcx, def_id); // Check if any unstable attribute was reached. - KaniAttributes::for_def_id(tcx, def_id) - .check_unstable_features(&queries.args().unstable_features); + attributes.check_unstable_features(&queries.args().unstable_features); + // Check whether all `proof_for_contract` functions are reachable + attributes.check_proof_for_contract(&functions); def_ids.insert(def_id); } } From 4c8b3fe4000c9b4585b2f7ab975a202fedff2aeb Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 18 Oct 2024 15:42:24 -0700 Subject: [PATCH 3/6] Format --- kani-compiler/src/kani_middle/attributes.rs | 8 +++++--- kani-compiler/src/kani_middle/mod.rs | 17 ++++++++++------- 2 files changed, 15 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index ba3cc09c2b62..ab24615883df 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -474,9 +474,11 @@ impl<'tcx> KaniAttributes<'tcx> { || self.map.contains_key(&KaniAttributeKind::ProofForContract) } - pub fn check_proof_for_contract(&self, functions: &HashSet) { - if let Some((symbol, id, span)) = self.interpret_for_contract_attribute() { - if !functions.contains(&id) { + /// Check that the function specified in the `proof_for_contract` attribute + /// is reachable and emit an error if it isn't + pub fn check_proof_for_contract(&self, reachable_functions: &HashSet) { + if let Some((symbol, function, span)) = self.interpret_for_contract_attribute() { + if !reachable_functions.contains(&function) { let err_msg = format!( "The function specified in the `proof_for_contract` attribute, `{symbol}`, was not found.\ \nMake sure the function is reachable from the harness." diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 617b85839375..3f095cdad659 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -18,10 +18,10 @@ use rustc_span::Span; use rustc_span::source_map::respan; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use stable_mir::{CrateDef, DefId}; -use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::mir::mono::MonoItem; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; +use stable_mir::{CrateDef, DefId}; use std::ops::ControlFlow; use self::attributes::KaniAttributes; @@ -101,10 +101,13 @@ impl TyVisitor for FindUnsafeCell<'_> { pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); - let functions: HashSet = items.iter().filter_map(|i| match i { - MonoItem::Fn(instance) => Some(rustc_internal::internal(tcx, instance.def.def_id())), - _ => None, - }).collect(); + let reachable_functions: HashSet = items + .iter() + .filter_map(|i| match i { + MonoItem::Fn(instance) => Some(rustc_internal::internal(tcx, instance.def.def_id())), + _ => None, + }) + .collect(); for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) { let def_id = match item { MonoItem::Fn(instance) => instance.def.def_id(), @@ -118,7 +121,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) // Check if any unstable attribute was reached. attributes.check_unstable_features(&queries.args().unstable_features); // Check whether all `proof_for_contract` functions are reachable - attributes.check_proof_for_contract(&functions); + attributes.check_proof_for_contract(&reachable_functions); def_ids.insert(def_id); } } From a8d06dd6b8955d0da0aa45acd74c7e453418a63c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 18 Oct 2024 15:59:42 -0700 Subject: [PATCH 4/6] clippy --- kani-compiler/src/kani_middle/attributes.rs | 2 -- kani-compiler/src/kani_middle/mod.rs | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index ab24615883df..368e0ec91495 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -488,8 +488,6 @@ impl<'tcx> KaniAttributes<'tcx> { } } - /// Check that the `proof` attribute is valid. - /// Extract harness attributes for a given `def_id`. /// /// We only extract attributes for harnesses that are local to the current crate. diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 3f095cdad659..21744b2daaea 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -21,7 +21,7 @@ use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::mono::MonoItem; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; -use stable_mir::{CrateDef, DefId}; +use stable_mir::CrateDef; use std::ops::ControlFlow; use self::attributes::KaniAttributes; From fdb7b2a9c5fedffe3e7028124036ab7b73c084a4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 18 Oct 2024 16:00:20 -0700 Subject: [PATCH 5/6] Format --- kani-compiler/src/kani_middle/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 21744b2daaea..3e1c7e3b4fca 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -18,10 +18,10 @@ use rustc_span::Span; use rustc_span::source_map::respan; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use stable_mir::CrateDef; use stable_mir::mir::mono::MonoItem; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; -use stable_mir::CrateDef; use std::ops::ControlFlow; use self::attributes::KaniAttributes; From adce91cb8f24b20b1c2eadc1a54fe4b3f2926c12 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 18 Oct 2024 17:03:18 -0700 Subject: [PATCH 6/6] Trigger rebuild