Reject proof harnesses with arguments (rust-lang#2132)

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

- Add a check for harnesses with arguments and merge the checks into one function (rust-lang#1919). 

Co-authored-by: Zyad Hassan <[email protected]>

Author: celinval

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,46 +233,46 @@ 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);
-        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) {
+    /// 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>) {
+        assert!(!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, "Duplicate attribute");
+        }
+
+        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 {
+            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, "The proof attribute cannot be applied to generic functions.");
+                    .span_err(span, "Functions used as harnesses can not have any arguments.");
             }
-            self.tcx.sess.abort_if_errors();
-            true
-        } else {
-            false
         }
     }
 
-    // Check that all attributes assigned to an item is valid.
+    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);
+        !proof_attributes.is_empty()
+    }
+
+    /// 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/expected/reach/assert/unreachable/test.rs

@@ -2,7 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #[kani::proof]
-fn foo(x: i32) {
+fn foo() {
+    let x: i32 = kani::any();
     if x > 5 {
         // fails
         assert!(x < 4);

tests/kani/Intrinsics/PtrGuaranteedCmp/cmp.rs

@@ -6,14 +6,20 @@
 #![feature(core_intrinsics)]
 use std::intrinsics::ptr_guaranteed_cmp;
 
-#[kani::proof]
-fn test_ptr_eq(ptr1: *const u8, ptr2: *const u8) {
-    kani::assume(ptr1 == ptr2);
-    assert_eq!(ptr_guaranteed_cmp(ptr1, ptr2), 1);
+fn ptr_eq(ptr1: *const u8, ptr2: *const u8) -> bool {
+    ptr_guaranteed_cmp(ptr1, ptr2) == 1
+}
+
+fn ptr_ne(ptr1: *const u8, ptr2: *const u8) -> bool {
+    ptr_guaranteed_cmp(ptr1, ptr2) == 0
 }
 
 #[kani::proof]
-fn test_ptr_ne(ptr1: *const u8, ptr2: *const u8) {
-    kani::assume(ptr1 != ptr2);
-    assert_eq!(ptr_guaranteed_cmp(ptr1, ptr2), 0);
+fn check_ptr_guaranteed_cmp() {
+    let v1: u8 = kani::any();
+    let v2: u8 = kani::any();
+    assert!(ptr_eq(&v1, &v1));
+    assert!(ptr_eq(&v2, &v2));
+    assert!(ptr_ne(&v2, &v1));
+    assert!(ptr_ne(&v1, &v2));
 }

tests/ui/invalid-harnesses/expected

@@ -0,0 +1,17 @@
+warning: Duplicate attribute\
+invalid.rs:\
+|\
+| #[kani::proof]\
+| ^^^^^^^^^^^^^^
+
+error: Functions used as harnesses can not have any arguments.\
+invalid.rs:\
+|\
+| #[kani::proof]
+| ^^^^^^^^^^^^^^
+
+error: The proof attribute cannot be applied to generic functions.\
+invalid.rs:\
+|\
+| #[kani::proof]\
+| ^^^^^^^^^^^^^^

tests/ui/invalid-harnesses/invalid.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test is to check Kani's error handling of invalid usages of the `proof` harness.
+// We also ensure that all errors and warnings are printed in one compilation.
+
+#[kani::proof]
+#[kani::proof]
+fn multiple_proof_annotations() {}
+
+#[kani::proof]
+fn proof_with_arg(arg: bool) {
+    assert!(arg);
+}
+
+#[kani::proof]
+fn generic_harness<T: Default>() {
+    let _ = T::default();
+}

tests/ui/logging/warning/expected

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

tests/ui/multiple-proof-attributes/expected

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