Skip to content

Commit

Permalink
Fix #[extern_spec] on extern "C"
Browse files Browse the repository at this point in the history
have to be declared separately elsewhere

move the foreign_mods test from parse to cargo_verify; add a C source
file that is compiled a linked to it

add a parse fail test having #[extern_spec] instead of
  • Loading branch information
vfukala authored and Aurel300 committed Apr 3, 2023
1 parent f38a7fe commit 8b07095
Show file tree
Hide file tree
Showing 15 changed files with 129 additions and 92 deletions.
29 changes: 9 additions & 20 deletions prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ pub(crate) fn generate_extern_spec_method_stub<T: HasSignature + HasAttributes +

// Build the method stub
let stub_method =
generate_extern_spec_function_stub(method, &method_path, extern_spec_kind, false);
generate_extern_spec_function_stub(method, &method_path, extern_spec_kind, false, false);
let stub_method: syn::ImplItemMethod = syn::parse2(stub_method)?;

// Eagerly extract and process specifications
Expand Down Expand Up @@ -191,6 +191,7 @@ pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttrib
fn_path: &syn::ExprPath,
extern_spec_kind: ExternSpecKind,
mangle_name: bool,
is_unsafe: bool,
) -> TokenStream {
let signature = function.sig();
let mut signature = with_explicit_lifetimes(signature).unwrap_or_else(|| signature.clone());
Expand All @@ -202,36 +203,24 @@ pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttrib
let generic_params = &signature.generic_params_as_call_args();
let args = &signature.params_as_call_args();
let extern_spec_kind_string: String = extern_spec_kind.into();
let fn_call = quote! { #fn_path :: < #generic_params > ( #args ) };
let stub_body = if is_unsafe {
quote! { unsafe { #fn_call } }
} else {
quote! { #fn_call }
};

quote_spanned! {function.span()=>
#[trusted]
#[prusti::extern_spec = #extern_spec_kind_string]
#(#attrs)*
#[allow(unused, dead_code)]
#signature {
#fn_path :: < #generic_params > ( #args )
#stub_body
}
}
}

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
Expand Down
Original file line number Diff line number Diff line change
@@ -1,37 +1,25 @@
//! 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 super::functions::rewrite_stub;
use proc_macro2::TokenStream;
use quote::{quote, ToTokens};
use quote::ToTokens;
use syn::spanned::Spanned;

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)?);
pub fn rewrite_extern_spec(
item_foreign_mod: &syn::ItemForeignMod,
path: &syn::Path,
) -> syn::Result<TokenStream> {
let mut res = TokenStream::new();
for item in item_foreign_mod.items.iter() {
match item {
syn::ForeignItem::Fn(item_fn) => {
let tokens = rewrite_stub(&item_fn.to_token_stream(), path, true);
res.extend(tokens);
}
// eventually: handle specs for foreign variables (statics)
_ => return Err(syn::Error::new(item.span(), "unexpected item")),
}
// 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)
}
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,11 @@ use proc_macro2::{Group, TokenStream, TokenTree};
use quote::{quote, ToTokens};
use syn::{parse_quote_spanned, spanned::Spanned};

pub fn rewrite_stub(stub_tokens: &TokenStream, path: &syn::Path) -> syn::Result<TokenStream> {
pub fn rewrite_stub(
stub_tokens: &TokenStream,
path: &syn::Path,
is_unsafe: bool,
) -> syn::Result<TokenStream> {
// Transforms function stubs (functions with a `;` after the
// signature instead of the body) into functions, then
// processes them.
Expand All @@ -34,18 +38,18 @@ pub fn rewrite_stub(stub_tokens: &TokenStream, path: &syn::Path) -> syn::Result<

let mut item = res.unwrap();
if let syn::Item::Fn(item_fn) = &mut item {
Ok(rewrite_fn(item_fn, path))
Ok(rewrite_fn(item_fn, path, is_unsafe))
} else {
Ok(quote!(#item))
}
}

/// Rewrite a specification function to a call to the specified function.
/// The result of this rewriting is then parsed in `ExternSpecResolver`.
pub fn rewrite_fn(item_fn: &syn::ItemFn, path: &syn::Path) -> TokenStream {
pub fn rewrite_fn(item_fn: &syn::ItemFn, path: &syn::Path, is_unsafe: bool) -> TokenStream {
let ident = &item_fn.sig.ident;
let path_span = item_fn.sig.ident.span();
let path = parse_quote_spanned!(path_span=> #path :: #ident);

generate_extern_spec_function_stub(item_fn, &path, ExternSpecKind::Method, true)
generate_extern_spec_function_stub(item_fn, &path, ExternSpecKind::Method, true, is_unsafe)
}
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,10 @@ pub fn rewrite_mod(item_mod: &syn::ItemMod, mut path: syn::Path) -> syn::Result<
match item {
syn::Item::Fn(ref item_fn) => {
check_is_stub(&item_fn.block)?;
rewritten_fns.extend(rewrite_fn(item_fn, &path));
rewritten_fns.extend(rewrite_fn(item_fn, &path, false));
}
syn::Item::Mod(ref inner_mod) => rewritten_fns.extend(rewrite_mod(inner_mod, path.clone())?),
syn::Item::Verbatim(ref tokens) => rewritten_fns.extend(rewrite_stub(tokens, &path)?),
syn::Item::Verbatim(ref tokens) => rewritten_fns.extend(rewrite_stub(tokens, &path, false)?),
syn::Item::Use(_) => rewritten_fns.extend(syn::Error::new(
item.span(),
"`use` statements have no effect in #[extern_spec] modules; module contents share the outer scope.",
Expand Down
7 changes: 5 additions & 2 deletions prusti-contracts/prusti-specs/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -780,11 +780,14 @@ pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
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)
extern_spec_rewriter::foreign_mods::rewrite_extern_spec(
&item_foreign_mod,
&mod_path,
)
}
// 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)
extern_spec_rewriter::functions::rewrite_stub(&stub_tokens, &mod_path, false)
}
_ => Err(syn::Error::new(
Span::call_site(), // this covers the entire macro invocation, unlike attr.span() which changes to only cover arguments if possible
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ impl AnyFnItem {
_ => unreachable!(),
}
}

pub fn expect_foreign_item_fn(self) -> syn::ForeignItemFn {
match self {
AnyFnItem::ForeignFn(f) => f,
Expand Down
14 changes: 0 additions & 14 deletions prusti-interface/src/specs/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -436,20 +436,6 @@ 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);

Expand Down
14 changes: 14 additions & 0 deletions prusti-tests/tests/cargo_verify/foreign_mods/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
[package]
name = "foreign_mods"
version = "0.1.0"
edition = "2021"
build = "build.rs"

[dependencies]
prusti-contracts = { path = "prusti-contracts/prusti-contracts" } # The test suite will prepare a symbolic link for this

[build-dependencies]
cc = "1.0"

# Declare that this crate is not part of a workspace
[workspace]
5 changes: 5 additions & 0 deletions prusti-tests/tests/cargo_verify/foreign_mods/build.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
fn main() {
cc::Build::new()
.file("src/clib.c")
.compile("clib");
}
12 changes: 12 additions & 0 deletions prusti-tests/tests/cargo_verify/foreign_mods/src/clib.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#include <stdint.h>

int32_t max(int32_t a, int32_t b) {
return a > b ? a : b;
}

void unannotated(void) {
}

int32_t abs(int32_t a) {
return a >= 0 ? a : -a;
}
Original file line number Diff line number Diff line change
@@ -1,6 +1,14 @@
use prusti_contracts::*;

#[extern_spec]
extern "C" {
fn max(a: i32, b: i32) -> i32;

fn unannotated();

fn abs(a: i32) -> i32;
}

#[extern_spec(crate)]
extern "C" {
#[ensures(a >= b ==> result == a)]
#[ensures(b >= a ==> result == b)]
Expand Down
5 changes: 5 additions & 0 deletions prusti-tests/tests/cargotest.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,11 @@ fn test_failing_stable_toolchain() {
test_local_project("failing_stable_toolchain");
}

#[cargo_test]
fn test_foreign_mods() {
test_local_project("foreign_mods");
}

#[cargo_test]
fn test_library_contracts_test() {
test_local_project("library_contracts_test");
Expand Down
11 changes: 11 additions & 0 deletions prusti-tests/tests/parse/fail/extern-spec/on-function.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
use prusti_contracts::*;

fn identity(a: i32) -> i32 {
a
}

#[extern_spec] // should be #[extern_spec(crate)] in this case
#[ensures(a == 0 ==> result == 0)]
fn identity(a: i32) -> i32; //~ ERROR: cannot find crate `identity` in the list of imported crates

fn main() {}
10 changes: 9 additions & 1 deletion prusti-tests/tests/parse/ui/foreign_mods.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,14 @@
use prusti_contracts::*;

#[extern_spec]
extern "C" {
fn max(a: i32, b: i32) -> i32;

fn unannotated();

fn abs(a: i32) -> i32;
}

#[extern_spec(crate)]
extern "C" {
#[ensures(a >= b ==> result = a)]
#[ensures(b >= a ==> result == b)]
Expand Down
42 changes: 23 additions & 19 deletions prusti-tests/tests/parse/ui/foreign_mods.stderr
Original file line number Diff line number Diff line change
@@ -1,35 +1,39 @@
error[E0308]: mismatched types
--> $DIR/foreign_mods.rs:5:26
|
5 | #[ensures(a >= b ==> result = a)]
| ^^^^^^ expected `bool`, found `i32`
--> $DIR/foreign_mods.rs:13:26
|
13 | #[ensures(a >= b ==> result = a)]
| ------ ^^^^^^ expected `bool`, found `i32`
| |
| expected because this is `bool`

error[E0308]: mismatched types
--> $DIR/foreign_mods.rs:5:22
|
5 | #[ensures(a >= b ==> result = a)]
| ^^^^^^^^^^^^^^ expected `bool`, found `()`
|
--> $DIR/foreign_mods.rs:13:15
|
13 | #[ensures(a >= b ==> result = a)]
| ^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `()`
|
help: you might have meant to compare for equality
|
5 | #[ensures(a >= b ==> result == a)]
| +
|
13 | #[ensures(a >= b ==> result == a)]
| +

error[E0308]: mismatched types
--> $DIR/foreign_mods.rs:12:26
--> $DIR/foreign_mods.rs:20:26
|
12 | #[ensures(a >= 0 ==> result = a)]
| ^^^^^^ expected `bool`, found `i32`
20 | #[ensures(a >= 0 ==> result = a)]
| ------ ^^^^^^ expected `bool`, found `i32`
| |
| expected because this is `bool`

error[E0308]: mismatched types
--> $DIR/foreign_mods.rs:12:22
--> $DIR/foreign_mods.rs:20:15
|
12 | #[ensures(a >= 0 ==> result = a)]
| ^^^^^^^^^^^^^^ expected `bool`, found `()`
20 | #[ensures(a >= 0 ==> result = a)]
| ^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `()`
|
help: you might have meant to compare for equality
|
12 | #[ensures(a >= 0 ==> result == a)]
20 | #[ensures(a >= 0 ==> result == a)]
| +

error: aborting due to 4 previous errors
Expand Down

0 comments on commit 8b07095

Please sign in to comment.