Improve #[kani::proof] handling

- Change `#[kani::proof]` expansion so it doesn't include `#[no_mangle]`
but includes `[allow(dead_code)]`. Fixes model-checking#661 and fixes model-checking#689.

- Add a check for harnesses with arguments and merge the checks into one
  function. Fixes model-checking#1919

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -13,6 +13,7 @@ use rustc_ast::Attribute;
 use rustc_hir::def::DefKind;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::{HasLocalDecls, Local};
+use rustc_middle::ty::layout::FnAbiOf;
 use rustc_middle::ty::{self, Instance};
 use std::collections::BTreeMap;
 use std::convert::TryInto;
@@ -232,11 +233,14 @@ impl<'tcx> GotocCtx<'tcx> {
         self.reset_current_fn();
     }
 
-    pub fn is_proof_harness(&self, def_id: DefId) -> bool {
-        let all_attributes = self.tcx.get_attrs_unchecked(def_id);
-        let (proof_attributes, _) = partition_kanitool_attributes(all_attributes);
+    /// Check that if an item is tagged with a proof_attribute, it is a valid harness.
+    fn check_proof_attribute(&self, def_id: DefId, proof_attributes: Vec<&Attribute>) {
         if !proof_attributes.is_empty() {
             let span = proof_attributes.first().unwrap().span;
+            if proof_attributes.len() > 1 {
+                self.tcx.sess.span_warn(proof_attributes[0].span, "Duplicated attribute");
+            }
+
             if self.tcx.def_kind(def_id) != DefKind::Fn {
                 self.tcx
                     .sess
@@ -245,33 +249,37 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.tcx
                     .sess
                     .span_err(span, "The proof attribute cannot be applied to generic functions.");
+            } else {
+                let instance = Instance::mono(self.tcx, def_id);
+                if !self.fn_abi_of_instance(instance, ty::List::empty()).args.is_empty() {
+                    self.tcx
+                        .sess
+                        .span_err(span, "Functions used as harnesses can not have any arguments.");
+                }
             }
+        }
+    }
+
+    pub fn is_proof_harness(&self, def_id: DefId) -> bool {
+        let all_attributes = self.tcx.get_attrs_unchecked(def_id);
+        let (proof_attributes, _) = partition_kanitool_attributes(all_attributes);
+        if !proof_attributes.is_empty() {
+            self.check_proof_attribute(def_id, proof_attributes);
             self.tcx.sess.abort_if_errors();
             true
         } else {
             false
         }
     }
 
-    // Check that all attributes assigned to an item is valid.
+    /// 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 in case of an error.
     pub fn check_attributes(&self, def_id: DefId) {
         let all_attributes = self.tcx.get_attrs_unchecked(def_id);
         let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes);
         if !proof_attributes.is_empty() {
-            let span = proof_attributes.first().unwrap().span;
-            if self.tcx.def_kind(def_id) != DefKind::Fn {
-                self.tcx
-                    .sess
-                    .span_err(span, "The kani::proof attribute can only be applied to functions.");
-            } else if self.tcx.generics_of(def_id).requires_monomorphization(self.tcx) {
-                self.tcx
-                    .sess
-                    .span_err(span, "The proof attribute cannot be applied to generic functions.");
-            } else if proof_attributes.len() > 1 {
-                self.tcx
-                    .sess
-                    .span_warn(proof_attributes[0].span, "Only one '#[kani::proof]' allowed");
-            }
+            self.check_proof_attribute(def_id, proof_attributes);
         } else if !other_attributes.is_empty() {
             self.tcx.sess.span_err(
                 other_attributes[0].1.span,

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -29,11 +29,15 @@ use rustc_data_structures::rustc_erase_owner;
 use rustc_data_structures::sync::MetadataRef;
 use rustc_middle::mir::interpret::Allocation;
 use rustc_middle::span_bug;
-use rustc_middle::ty::layout::{HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, TyAndLayout};
+use rustc_middle::ty::layout::{
+    FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers,
+    TyAndLayout,
+};
 use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
 use rustc_session::cstore::MetadataLoader;
 use rustc_session::Session;
-use rustc_span::source_map::Span;
+use rustc_span::source_map::{respan, Span};
+use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::Endian;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use rustc_target::spec::Target;
@@ -380,6 +384,39 @@ impl<'tcx> HasDataLayout for GotocCtx<'tcx> {
         self.tcx.data_layout()
     }
 }
+
+/// Implement error handling for extracting function ABI information.
+impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
+    type FnAbiOfResult = &'tcx FnAbi<'tcx, Ty<'tcx>>;
+
+    #[inline]
+    fn handle_fn_abi_err(
+        &self,
+        err: FnAbiError<'tcx>,
+        span: Span,
+        fn_abi_request: FnAbiRequest<'tcx>,
+    ) -> ! {
+        if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
+            self.tcx.sess.emit_fatal(respan(span, err))
+        } else {
+            match fn_abi_request {
+                FnAbiRequest::OfFnPtr { sig, extra_args } => {
+                    span_bug!(
+                        span,
+                        "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
+                    );
+                }
+                FnAbiRequest::OfInstance { instance, extra_args } => {
+                    span_bug!(
+                        span,
+                        "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
+                    );
+                }
+            }
+        }
+    }
+}
+
 pub struct GotocMetadataLoader();
 impl MetadataLoader for GotocMetadataLoader {
     fn get_rlib_metadata(&self, _: &Target, _filename: &Path) -> Result<MetadataRef, String> {

library/kani_macros/src/lib.rs

@@ -44,16 +44,12 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     let fn_item = parse_macro_input!(item as ItemFn);
     let attrs = fn_item.attrs;
     let vis = fn_item.vis;
-    let fn_name = fn_item.sig.ident.clone();
-    let test_name = quote!(#fn_name);
     let sig = fn_item.sig;
     let body = fn_item.block;
 
     let kani_attributes = quote!(
+        #[allow(dead_code)]
         #[kanitool::proof]
-        #[export_name = concat!(module_path!(), "::", stringify!(#test_name))]
-        // no_mangle is a temporary hack to make the function "public" so it gets codegen'd
-        #[no_mangle]
     );
 
     assert!(attr.is_empty(), "#[kani::proof] does not take any arguments for now");

tests/ui/logging/warning/expected

@@ -1 +1 @@
-warning: Only one '#[kani::proof]' allowed
+warning: Duplicated attribute

tests/ui/multiple-proof-attributes/expected

@@ -1 +1,5 @@
-warning: Only one '#[kani::proof]' allowed
+warning: Duplicated attribute\
+main.rs:\
+|\
+| #[kani::proof]\
+| ^^^^^^^^^^^^^^