Prototype extension for translating foreign function specs to VeriFast.

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

@@ -1,16 +1,17 @@
 use crate::{
+    TokenTree,
     common::{HasAttributes, HasSignature},
     extract_prusti_attributes, generate_spec_and_assertions,
     span_overrider::SpanOverrider,
     untyped::AnyFnItem,
     ExternSpecKind, RewritableReceiver, SelfTypeRewriter,
 };
 use itertools::Itertools;
-use proc_macro2::TokenStream;
+use proc_macro2::{TokenStream, Group};
 use quote::{format_ident, quote, quote_spanned, ToTokens};
 use syn::{
     parse_quote_spanned, punctuated::Punctuated, spanned::Spanned, visit::Visit,
-    visit_mut::VisitMut, Expr, FnArg, GenericArgument, GenericParam, Pat, PatType, Token,
+    visit_mut::VisitMut, Expr, FnArg, GenericArgument, GenericParam, Pat, PatType, Token
 };
 
 /// Counts the number of elided lifetimes in receivers and types.
@@ -187,19 +188,60 @@ pub(crate) fn generate_extern_spec_method_stub<T: HasSignature + HasAttributes +
 }
 
 pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttributes + Spanned>(
+    function: &Input,
+    fn_path: &syn::ExprPath,
+    extern_spec_kind: ExternSpecKind,
+    mangle_name: bool,
+    is_unsafe: bool
+) -> TokenStream {
+    generate_extern_spec_function_stub_with_translator(
+        function,
+        fn_path,
+        extern_spec_kind,
+        mangle_name,
+        is_unsafe,
+        None,
+    )
+}
+
+pub(crate) fn generate_extern_spec_function_stub_with_translator<Input: HasSignature + HasAttributes + Spanned>(
     function: &Input,
     fn_path: &syn::ExprPath,
     extern_spec_kind: ExternSpecKind,
     mangle_name: bool,
     is_unsafe: bool,
+    translator: Option<&str>
 ) -> TokenStream {
     let signature = function.sig();
     let mut signature = with_explicit_lifetimes(signature).unwrap_or_else(|| signature.clone());
     if mangle_name {
         signature.ident = format_ident!("prusti_extern_spec_{}", signature.ident);
     }
     // Make elided lifetimes explicit, if necessary.
-    let attrs = function.attrs().clone();
+    let mut attrs = function.attrs().clone();
+
+    if let Some(translator) = translator {
+        attrs.iter_mut().for_each(|attr| {
+
+            if attr.path.is_ident("ensures") || attr.path.is_ident("requires") {
+                let translator = translator.to_owned().replace("\"", "");
+                let mut new_tokens = quote_spanned! {attr.tokens.span()=>
+                    {translator = #translator}
+                };
+                dbg!(&new_tokens);
+                let mut tokens = TokenStream::new();
+                std::mem::swap(&mut attr.tokens, &mut tokens);
+                if let Some(TokenTree::Group(group)) = tokens.into_iter().next() {
+                    new_tokens.extend(group.stream());
+                    attr.tokens = TokenStream::from(TokenTree::Group(
+                        Group::new(group.delimiter(), new_tokens),
+                    ));
+                }
+            }
+
+        })
+    }
+
     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();

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

@@ -1,20 +1,28 @@
 //! Process external specifications in Rust foreign modules marked with
 //! the #[extern_spec] attribute.
 
-use super::functions::rewrite_stub;
+use super::functions::rewrite_stub_with_translator;
 use proc_macro2::TokenStream;
-use quote::ToTokens;
+use quote::{quote_spanned, ToTokens};
 use syn::spanned::Spanned;
+use super::super::properties;
 
 pub fn rewrite_extern_spec(
     item_foreign_mod: &syn::ItemForeignMod,
     path: &syn::Path,
+    properties: properties::SpecProperties,
 ) -> 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);
+                let tokens = rewrite_stub_with_translator(&item_fn.to_token_stream(), path, true, properties.get(&properties::Property::Translator))?;
+                if let Some(extern_source_file) = properties.get(&properties::Property::File) {
+                    let extern_source_file = extern_source_file.to_string().replace("\"", "");
+                    res.extend(quote_spanned! {item_fn.span()=>
+                        #[prusti::extern_source_file = #extern_source_file]
+                    });
+                }
                 res.extend(tokens);
             }
             // eventually: handle specs for foreign variables (statics)

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

@@ -2,16 +2,21 @@
 //! In practice, these will be combined with a module argument to extern_spec
 //! e.g. `#[extern_spec(core::mem)] fn swap`
 
-use super::common::generate_extern_spec_function_stub;
+use super::common::generate_extern_spec_function_stub_with_translator;
 use crate::ExternSpecKind;
 use proc_macro2::{Group, TokenStream, TokenTree};
 use quote::{quote, ToTokens};
 use syn::{parse_quote_spanned, spanned::Spanned};
 
-pub fn rewrite_stub(
+pub fn rewrite_stub(stub_tokens: &TokenStream, path: &syn::Path, is_unsafe: bool) -> syn::Result<TokenStream> {
+    rewrite_stub_with_translator(stub_tokens, path, is_unsafe, None)
+}
+
+pub fn rewrite_stub_with_translator(
     stub_tokens: &TokenStream,
     path: &syn::Path,
     is_unsafe: bool,
+    translator: Option<&str>
 ) -> syn::Result<TokenStream> {
     // Transforms function stubs (functions with a `;` after the
     // signature instead of the body) into functions, then
@@ -38,18 +43,22 @@ pub fn rewrite_stub(
 
     let mut item = res.unwrap();
     if let syn::Item::Fn(item_fn) = &mut item {
-        Ok(rewrite_fn(item_fn, path, is_unsafe))
+        Ok(rewrite_fn_with_translator(item_fn, path, is_unsafe, translator))
     } else {
         Ok(quote!(#item))
     }
 }
 
+pub fn rewrite_fn(item_fn: &syn::ItemFn, path: &syn::Path, is_unsafe: bool) -> TokenStream {
+    rewrite_fn_with_translator(item_fn, path, is_unsafe, None)
+}
+
 /// 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, is_unsafe: bool) -> TokenStream {
+pub fn rewrite_fn_with_translator(item_fn: &syn::ItemFn, path: &syn::Path, is_unsafe: bool, translator: Option<&str>) -> 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, is_unsafe)
+    generate_extern_spec_function_stub_with_translator(item_fn, &path, ExternSpecKind::Method, true, is_unsafe, translator)
 }

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

@@ -22,6 +22,8 @@ pub mod specifications;
 mod type_model;
 mod user_provided_type_params;
 mod print_counterexample;
+mod properties;
+mod spec_translator;
 
 use proc_macro2::{Span, TokenStream, TokenTree};
 use quote::{quote, quote_spanned, ToTokens};
@@ -190,32 +192,39 @@ fn generate_spec_and_assertions(
 
 /// Generate spec items and attributes to typecheck the and later retrieve "requires" annotations.
 fn generate_for_requires(attr: TokenStream, item: &untyped::AnyFnItem) -> GeneratedResult {
-    let mut rewriter = rewriter::AstRewriter::new();
-    let spec_id = rewriter.generate_spec_id();
-    let spec_id_str = spec_id.to_string();
-    let spec_item =
-        rewriter.process_assertion(rewriter::SpecItemType::Precondition, spec_id, attr, item)?;
-    Ok((
-        vec![spec_item],
-        vec![parse_quote_spanned! {item.span()=>
-            #[prusti::pre_spec_id_ref = #spec_id_str]
-        }],
-    ))
+    generate_for(attr, item, rewriter::SpecItemType::Precondition)
 }
 
 /// Generate spec items and attributes to typecheck the and later retrieve "ensures" annotations.
 fn generate_for_ensures(attr: TokenStream, item: &untyped::AnyFnItem) -> GeneratedResult {
+    generate_for(attr, item, rewriter::SpecItemType::Postcondition)
+}
+
+fn generate_for(
+    attr: TokenStream,
+    item: &untyped::AnyFnItem,
+    spec_item_type: rewriter::SpecItemType,
+) -> GeneratedResult {
     let mut rewriter = rewriter::AstRewriter::new();
     let spec_id = rewriter.generate_spec_id();
     let spec_id_str = spec_id.to_string();
-    let spec_item =
-        rewriter.process_assertion(rewriter::SpecItemType::Postcondition, spec_id, attr, item)?;
-    Ok((
-        vec![spec_item],
-        vec![parse_quote_spanned! {item.span()=>
-            #[prusti::post_spec_id_ref = #spec_id_str]
-        }],
-    ))
+    let spec_id_attribute: syn::Attribute = match spec_item_type {
+        rewriter::SpecItemType::Precondition => {
+            parse_quote_spanned! {item.span()=>
+                #[prusti::pre_spec_id_ref = #spec_id_str]
+            }
+        }
+        rewriter::SpecItemType::Postcondition => {
+            parse_quote_spanned! {item.span()=>
+                #[prusti::post_spec_id_ref = #spec_id_str]
+            }
+        }
+        _ => panic!("Unsupported spec item type for assertion generation"),
+    };
+
+    rewriter
+        .process_translatable_assertion(spec_item_type, spec_id, attr, item)
+        .map(|res| (res.0, [vec![spec_id_attribute], res.1].concat()))
 }
 
 /// Generate spec items and attributes to typecheck and later retrieve "after_expiry" annotations.
@@ -775,6 +784,9 @@ pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
 pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
     result_to_tokens!({
         let item: syn::Item = syn::parse2(tokens)?;
+
+        let (properties, attr) = properties::extract_properties(attr)?;
+
         let mod_path: syn::Path = Some(attr)
             .filter(|attr| !attr.is_empty())
             .map(syn::parse2)
@@ -803,6 +815,7 @@ pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
                 extern_spec_rewriter::foreign_mods::rewrite_extern_spec(
                     &item_foreign_mod,
                     &mod_path,
+                    properties,
                 )
             }
             // we're expecting function stubs, so they aren't represented as Item::Fn

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

@@ -0,0 +1,86 @@
+use proc_macro2::{TokenStream, TokenTree};
+use rustc_hash::FxHashMap;
+
+#[derive(Debug, Default)]
+pub(crate) struct SpecProperties {
+    properties: FxHashMap<String, String>,
+}
+
+pub(crate) enum Property {
+    Translator,
+    File,
+}
+
+impl SpecProperties {
+    pub(crate) fn get(&self, property: &Property) -> Option<&str> {
+        self.properties
+            .get(match property {
+                Property::Translator => "translator",
+                Property::File => "file",
+            })
+            .map(String::as_str)
+    }
+}
+
+pub(crate) fn extract_properties(
+    tokens: TokenStream,
+) -> syn::Result<(SpecProperties, TokenStream)> {
+    let mut tokens_iter = tokens.into_iter().peekable();
+    let mut properties = FxHashMap::default();
+
+    let mut matched = false;
+    if let Some(TokenTree::Group(group)) = tokens_iter.peek() {
+        matched = true;
+        let mut tokens_iter = group.stream().into_iter();
+        while let Some(prop_name_token) = tokens_iter.next() {
+            let prop_name = match &prop_name_token {
+                TokenTree::Ident(ident) => ident.to_string(),
+                _ => return Err(build_error(&prop_name_token, "property name expected")),
+            };
+
+            if properties.contains_key(&prop_name) {
+                return Err(build_error(&prop_name_token, "property already defined"));
+            }
+
+            let eq_token = tokens_iter.next();
+            if !matches!(&eq_token, Some(TokenTree::Punct(p)) if p.as_char() == '=') {
+                return Err(build_error(
+                    &eq_token.unwrap_or(prop_name_token),
+                    "'=' expected",
+                ));
+            }
+
+            let value_token = tokens_iter.next();
+            let prop_value = match value_token {
+                Some(TokenTree::Literal(literal)) => literal.to_string(),
+                _ => {
+                    return Err(build_error(
+                        &value_token.unwrap_or(eq_token.unwrap()),
+                        "property value expected",
+                    ))
+                }
+            };
+
+            if let Some(comma_token) = tokens_iter.next() {
+                if !matches!(&comma_token, TokenTree::Punct(p) if p.as_char() == ',') {
+                    return Err(build_error(&comma_token, "',' expected"));
+                }
+            }
+
+            properties.insert(prop_name.to_ascii_lowercase(), prop_value);
+        }
+    }
+
+    if matched {
+        tokens_iter.next();
+    }
+
+    Ok((
+        SpecProperties { properties },
+        tokens_iter.collect::<TokenStream>(),
+    ))
+}
+
+fn build_error(token: &TokenTree, msg: &str) -> syn::Error {
+    syn::Error::new(token.span(), msg)
+}

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

@@ -1,10 +1,12 @@
 use crate::{
     common::HasSignature,
+    properties, spec_translator,
     specifications::{
         common::{SpecificationId, SpecificationIdGenerator},
         preparser::{parse_prusti, parse_prusti_assert_pledge, parse_prusti_pledge},
         untyped,
     },
+    GeneratedResult,
 };
 use proc_macro2::{Span, TokenStream};
 use quote::{format_ident, quote, quote_spanned};
@@ -135,6 +137,25 @@ impl AstRewriter {
         Ok(syn::Item::Fn(spec_item))
     }
 
+    pub fn process_translatable_assertion<T: HasSignature + Spanned>(
+        &mut self,
+        spec_type: SpecItemType,
+        spec_id: SpecificationId,
+        tokens: TokenStream,
+        item: &T,
+    ) -> GeneratedResult {
+        let (props, tokens) = properties::extract_properties(tokens)?;
+        let translated_specs = spec_translator::build_translator(&props)
+            .map(|translator| {
+                translator.translate_spec(item.span(), spec_type.clone(), tokens.clone())
+            })
+            .unwrap_or(Ok(Vec::new()))?;
+        Ok((
+            vec![self.generate_spec_item_fn(spec_type, spec_id, parse_prusti(tokens)?, item)?],
+            translated_specs,
+        ))
+    }
+
     /// Parse an assertion into a Rust expression
     pub fn process_assertion<T: HasSignature + Spanned>(
         &mut self,