diff --git a/prusti-contracts/prusti-specs/src/common.rs b/prusti-contracts/prusti-specs/src/common.rs index 1d8ad331c8b..787eef8f21b 100644 --- a/prusti-contracts/prusti-specs/src/common.rs +++ b/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 { + &self.attrs + } + } } /// See [SelfTypeRewriter] diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs index 69e00ba7ed5..d1276f2db76 100644 --- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs +++ b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs @@ -214,6 +214,24 @@ pub(crate) fn generate_extern_spec_function_stub( + 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 = 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 diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs new file mode 100644 index 00000000000..cbd75e15bb7 --- /dev/null +++ b/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 { + 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, 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) +} diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mod.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mod.rs index 119ce3f9dfc..40974d8c6f6 100644 --- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mod.rs +++ b/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)] diff --git a/prusti-contracts/prusti-specs/src/lib.rs b/prusti-contracts/prusti-specs/src/lib.rs index 0d00f218f71..e60490cf028 100644 --- a/prusti-contracts/prusti-specs/src/lib.rs +++ b/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) diff --git a/prusti-contracts/prusti-specs/src/specifications/untyped.rs b/prusti-contracts/prusti-specs/src/specifications/untyped.rs index 0d434409f2e..dcc5f067f2b 100644 --- a/prusti-contracts/prusti-specs/src/specifications/untyped.rs +++ b/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), } } } diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs index 25b70c57e22..86e50f79fa6 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/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); diff --git a/prusti-tests/tests/parse/pass/extern-spec/foreign_mods.rs b/prusti-tests/tests/parse/pass/extern-spec/foreign_mods.rs new file mode 100644 index 00000000000..cefb3196f55 --- /dev/null +++ b/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 }); +} diff --git a/prusti-tests/tests/parse/ui/foreign_mods.rs b/prusti-tests/tests/parse/ui/foreign_mods.rs new file mode 100644 index 00000000000..97413afe99e --- /dev/null +++ b/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() {} \ No newline at end of file diff --git a/prusti-tests/tests/parse/ui/foreign_mods.stderr b/prusti-tests/tests/parse/ui/foreign_mods.stderr new file mode 100644 index 00000000000..d8ff43fc2ca --- /dev/null +++ b/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`.