Collect specifications of foreign function declarations.

prusti-contracts/prusti-specs/src/common.rs

@@ -13,8 +13,8 @@ use uuid::Uuid;
 /// These allow for writing of generic code over these types.
 mod syn_extensions {
     use syn::{
-        Attribute, Generics, ImplItemMacro, ImplItemMethod, ItemFn, ItemImpl, ItemStruct,
-        ItemTrait, Macro, Signature, TraitItemMacro, TraitItemMethod,
+        Attribute, ForeignItemFn, Generics, ImplItemMacro, ImplItemMethod, ItemFn, ItemImpl,
+        ItemStruct, ItemTrait, Macro, Signature, TraitItemMacro, TraitItemMethod,
     };
 
     /// Trait which signals that the corresponding syn item contains generics
@@ -105,6 +105,16 @@ mod syn_extensions {
         }
     }
 
+    impl HasSignature for ForeignItemFn {
+        fn sig(&self) -> &Signature {
+            &self.sig
+        }
+
+        fn sig_mut(&mut self) -> &mut Signature {
+            &mut self.sig
+        }
+    }
+
     /// Abstraction over everything that has a [syn::Macro]
     pub(crate) trait HasMacro {
         fn mac(&self) -> &Macro;
@@ -144,6 +154,12 @@ mod syn_extensions {
             &self.attrs
         }
     }
+
+    impl HasAttributes for ForeignItemFn {
+        fn attrs(&self) -> &Vec<Attribute> {
+            &self.attrs
+        }
+    }
 }
 
 /// See [SelfTypeRewriter]

prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs

@@ -214,6 +214,24 @@ pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttrib
     }
 }
 
+pub(crate) fn generate_extern_spec_foreign_function_stub<Input: HasSignature + HasAttributes + Spanned, Output: syn::parse::Parse>(
+    function: &Input,
+    extern_spec_kind: ExternSpecKind,
+) -> Output {
+    let signature = function.sig();
+    // Make elided lifetimes explicit, if necessary.
+    let signature = with_explicit_lifetimes(signature).unwrap_or_else(|| signature.clone());
+    let attrs: Vec<syn::Attribute> = function.attrs().clone();
+    let extern_spec_kind_string: String = extern_spec_kind.into();
+
+    parse_quote_spanned! {function.span()=>
+        #[trusted]
+        #[prusti::extern_spec = #extern_spec_kind_string]
+        #(#attrs)*
+        #signature;
+    }
+}
+
 /// Given a method signature with parameters, this function returns all typed parameters
 /// as they were used as arguments for the function call.
 /// # Example

prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs

@@ -0,0 +1,37 @@
+//! Process external specifications in Rust foreign modules marked with
+//! the #[extern_spec] attribute.
+
+use super::common::generate_extern_spec_foreign_function_stub;
+use crate::{
+    extract_prusti_attributes, generate_spec_and_assertions, specifications::untyped::AnyFnItem,
+    ExternSpecKind,
+};
+use proc_macro2::TokenStream;
+use quote::{quote, ToTokens};
+
+pub fn rewrite_extern_spec(item_foreign_mod: &mut syn::ItemForeignMod) -> syn::Result<TokenStream> {
+    let mut specs = vec![];
+    for item in item_foreign_mod.items.iter_mut() {
+        if let syn::ForeignItem::Fn(item_fn) = item {
+            specs.extend(rewrite_fn(item_fn)?);
+        }
+        // eventually: handle specs for foreign variables
+    }
+
+    let mut res = TokenStream::new();
+    res.extend(specs.iter().map(syn::Item::to_token_stream));
+    res.extend(quote!(#item_foreign_mod));
+    Ok(res)
+}
+
+fn rewrite_fn(item_fn: &mut syn::ForeignItemFn) -> Result<Vec<syn::Item>, syn::Error> {
+    let stub_fn: syn::ForeignItemFn =
+        generate_extern_spec_foreign_function_stub(item_fn, ExternSpecKind::Method);
+    let mut stub_fn = AnyFnItem::ForeignFn(stub_fn);
+    let prusti_attributes = extract_prusti_attributes(&mut stub_fn);
+    let (spec_items, generated_attributes) =
+        generate_spec_and_assertions(prusti_attributes, &stub_fn)?;
+    stub_fn.attrs_mut().extend(generated_attributes);
+    *item_fn = stub_fn.expect_foreign_item_fn();
+    Ok(spec_items)
+}

prusti-contracts/prusti-specs/src/extern_spec_rewriter/mod.rs

@@ -4,6 +4,7 @@ pub mod impls;
 pub mod mods;
 pub mod traits;
 pub mod functions;
+pub mod foreign_mods;
 mod common;
 
 #[derive(Debug, Clone, Copy)]

prusti-contracts/prusti-specs/src/lib.rs

@@ -779,6 +779,9 @@ pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
             syn::Item::Mod(item_mod) => {
                 extern_spec_rewriter::mods::rewrite_mod(&item_mod, mod_path)
             }
+            syn::Item::ForeignMod(item_foreign_mod) => {
+                extern_spec_rewriter::foreign_mods::rewrite_extern_spec(&item_foreign_mod)
+            }
             // we're expecting function stubs, so they aren't represented as Item::Fn
             syn::Item::Verbatim(stub_tokens) => {
                 extern_spec_rewriter::functions::rewrite_stub(&stub_tokens, &mod_path)

prusti-contracts/prusti-specs/src/specifications/untyped.rs

@@ -14,6 +14,7 @@ pub enum AnyFnItem {
     Fn(syn::ItemFn),
     TraitMethod(syn::TraitItemMethod),
     ImplMethod(syn::ImplItemMethod),
+    ForeignFn(syn::ForeignItemFn),
 }
 
 impl syn::parse::Parse for AnyFnItem {
@@ -42,6 +43,7 @@ impl AnyFnItem {
             AnyFnItem::Fn(item) => &mut item.attrs,
             AnyFnItem::TraitMethod(item) => &mut item.attrs,
             AnyFnItem::ImplMethod(item) => &mut item.attrs,
+            AnyFnItem::ForeignFn(item) => &mut item.attrs,
         }
     }
 
@@ -50,6 +52,7 @@ impl AnyFnItem {
             AnyFnItem::Fn(item) => Some(&item.block),
             AnyFnItem::ImplMethod(item) => Some(&item.block),
             AnyFnItem::TraitMethod(item) => item.default.as_ref(),
+            AnyFnItem::ForeignFn(_) => None,
         }
     }
 
@@ -58,6 +61,7 @@ impl AnyFnItem {
             AnyFnItem::Fn(item) => Some(&item.vis),
             AnyFnItem::ImplMethod(item) => Some(&item.vis),
             AnyFnItem::TraitMethod(_) => None,
+            AnyFnItem::ForeignFn(item) => Some(&item.vis),
         }
     }
 
@@ -67,6 +71,13 @@ impl AnyFnItem {
             _ => unreachable!(),
         }
     }
+
+    pub fn expect_foreign_item_fn(self) -> syn::ForeignItemFn {
+        match self {
+            AnyFnItem::ForeignFn(f) => f,
+            _ => unreachable!(),
+        }
+    }
 }
 
 impl HasSignature for AnyFnItem {
@@ -75,6 +86,7 @@ impl HasSignature for AnyFnItem {
             Self::Fn(item) => item.sig(),
             Self::ImplMethod(item) => item.sig(),
             Self::TraitMethod(item) => item.sig(),
+            Self::ForeignFn(item) => item.sig(),
         }
     }
 
@@ -83,6 +95,7 @@ impl HasSignature for AnyFnItem {
             Self::Fn(item) => item.sig_mut(),
             Self::ImplMethod(item) => item.sig_mut(),
             Self::TraitMethod(item) => item.sig_mut(),
+            Self::ForeignFn(item) => item.sig_mut(),
         }
     }
 }
@@ -93,6 +106,7 @@ impl ToTokens for AnyFnItem {
             AnyFnItem::Fn(item) => item.to_tokens(tokens),
             AnyFnItem::TraitMethod(item) => item.to_tokens(tokens),
             AnyFnItem::ImplMethod(item) => item.to_tokens(tokens),
+            AnyFnItem::ForeignFn(item) => item.to_tokens(tokens),
         }
     }
 }

prusti-interface/src/specs/mod.rs

@@ -436,6 +436,20 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> {
         self.env.query.hir()
     }
 
+    fn visit_foreign_item(&mut self, fi: &'tcx prusti_rustc_interface::hir::ForeignItem) {
+        intravisit::walk_foreign_item(self, fi);
+
+        let id = fi.hir_id();
+        let local_id = self.env.query.as_local_def_id(id);
+        let def_id = local_id.to_def_id();
+        let attrs = self.env.query.get_local_attributes(fi.owner_id.def_id);
+
+        // Collect procedure specifications
+        if let Some(procedure_spec_ref) = get_procedure_spec_ids(def_id, attrs) {
+            self.procedure_specs.insert(local_id, procedure_spec_ref);
+        }
+    }
+
     fn visit_trait_item(&mut self, ti: &'tcx prusti_rustc_interface::hir::TraitItem) {
         intravisit::walk_trait_item(self, ti);
 

prusti-tests/tests/parse/pass/extern-spec/foreign_mods.rs

@@ -0,0 +1,24 @@
+use prusti_contracts::*;
+
+#[extern_spec]
+extern "C" {
+    #[ensures(a >= b ==> result == a)]
+    #[ensures(b >= a ==> result == b)]
+    fn max(a: i32, b: i32) -> i32;
+
+    fn unannotated();
+
+    #[ensures(a < 0 ==> result == -a)]
+    #[ensures(a >= 0 ==> result == a)]
+    fn abs(a: i32) -> i32;
+}
+
+fn main() {
+    assert!(unsafe { max(1, 2) } == 2);
+    assert!(unsafe { max(2, 1) } == 2);
+    unsafe {
+        unannotated();
+    };
+    assert!(unsafe { abs(-1) } == 1);
+    assert!(unsafe { abs(1) == 1 });
+}

prusti-tests/tests/parse/ui/foreign_mods.rs

@@ -0,0 +1,16 @@
+use prusti_contracts::*;
+
+#[extern_spec]
+extern "C" {
+    #[ensures(a >= b ==> result = a)]
+    #[ensures(b >= a ==> result == b)]
+    fn max(a: i32, b: i32) -> i32;
+
+    fn unannotated();
+
+    #[ensures(a < 0 ==> result == -a)]
+    #[ensures(a >= 0 ==> result = a)]
+    fn abs(a: i32) -> i32;
+}
+
+fn main() {}

prusti-tests/tests/parse/ui/foreign_mods.stderr

@@ -0,0 +1,37 @@
+error[E0308]: mismatched types
+ --> $DIR/foreign_mods.rs:5:26
+  |
+5 |     #[ensures(a >= b ==> result = a)]
+  |                          ^^^^^^ expected `bool`, found `i32`
+
+error[E0308]: mismatched types
+ --> $DIR/foreign_mods.rs:5:22
+  |
+5 |     #[ensures(a >= b ==> result = a)]
+  |                      ^^^^^^^^^^^^^^ expected `bool`, found `()`
+  |
+help: you might have meant to compare for equality
+  |
+5 |     #[ensures(a >= b ==> result == a)]
+  |                                  +
+
+error[E0308]: mismatched types
+  --> $DIR/foreign_mods.rs:12:26
+   |
+12 |     #[ensures(a >= 0 ==> result = a)]
+   |                          ^^^^^^ expected `bool`, found `i32`
+
+error[E0308]: mismatched types
+  --> $DIR/foreign_mods.rs:12:22
+   |
+12 |     #[ensures(a >= 0 ==> result = a)]
+   |                      ^^^^^^^^^^^^^^ expected `bool`, found `()`
+   |
+help: you might have meant to compare for equality
+   |
+12 |     #[ensures(a >= 0 ==> result == a)]
+   |                                  +
+
+error: aborting due to 4 previous errors
+
+For more information about this error, try `rustc --explain E0308`.