Merge pull request #145 from karenhong/external_specs

External specs

prusti-contracts-impl/src/lib.rs

@@ -42,3 +42,8 @@ pub fn body_invariant(_tokens: TokenStream) -> TokenStream {
 pub fn closure(tokens: TokenStream) -> TokenStream {
     prusti_specs::closure(tokens.into(), true).into()
 }
+
+#[proc_macro_attribute]
+pub fn extern_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    tokens
+}

prusti-contracts-internal/src/lib.rs

@@ -42,3 +42,8 @@ pub fn body_invariant(tokens: TokenStream) -> TokenStream {
 pub fn closure(tokens: TokenStream) -> TokenStream {
     prusti_specs::closure(tokens.into(), false).into()
 }
+
+#[proc_macro_attribute]
+pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    prusti_specs::extern_spec(attr.into(), tokens.into()).into()
+}

prusti-contracts/src/lib.rs

@@ -25,6 +25,9 @@ mod private {
 
     /// A macro for defining a closure with a specification.
     pub use prusti_contracts_impl::closure;
+
+    /// A macro for specifying external functions.
+    pub use prusti_contracts_impl::extern_spec;
 }
 
 #[cfg(feature = "prusti")]
@@ -52,6 +55,9 @@ mod private {
 
     /// A macro for defining a closure with a specification.
     pub use prusti_contracts_internal::closure;
+
+    /// A macro for specifying external functions.
+    pub use prusti_contracts_internal::extern_spec;
 }
 
 

prusti-interface/src/environment/collect_prusti_spec_visitor.rs

@@ -14,7 +14,7 @@ use std::collections::HashSet;
 use std::iter::FromIterator;
 use log::{trace, debug};
 use rustc_ast::ast;
-use crate::utils::has_spec_only_attr;
+use crate::utils::{has_spec_only_attr, has_extern_spec_attr};
 
 pub struct CollectPrustiSpecVisitor<'a, 'tcx: 'a> {
     env: &'a Environment<'tcx>,
@@ -41,7 +41,7 @@ impl<'a, 'tcx> CollectPrustiSpecVisitor<'a, 'tcx> {
 
 impl<'a, 'tcx> ItemLikeVisitor<'tcx> for CollectPrustiSpecVisitor<'a, 'tcx> {
     fn visit_item(&mut self, item: &hir::Item) {
-        if has_spec_only_attr(&item.attrs) {
+        if has_spec_only_attr(&item.attrs) || has_extern_spec_attr(&item.attrs) {
             return;
         }
         if let hir::ItemKind::Fn(..) = item.kind {
@@ -53,7 +53,7 @@ impl<'a, 'tcx> ItemLikeVisitor<'tcx> for CollectPrustiSpecVisitor<'a, 'tcx> {
     }
 
     fn visit_trait_item(&mut self, trait_item: &hir::TraitItem) {
-        if has_spec_only_attr(&trait_item.attrs) {
+        if has_spec_only_attr(&trait_item.attrs) || has_extern_spec_attr(&trait_item.attrs) {
             return;
         }
 
@@ -75,7 +75,7 @@ impl<'a, 'tcx> ItemLikeVisitor<'tcx> for CollectPrustiSpecVisitor<'a, 'tcx> {
     }
 
     fn visit_impl_item(&mut self, impl_item: &hir::ImplItem) {
-        if has_spec_only_attr(&impl_item.attrs) {
+        if has_spec_only_attr(&impl_item.attrs) || has_extern_spec_attr(&impl_item.attrs) {
             return;
         }
 

prusti-interface/src/lib.rs

@@ -57,3 +57,7 @@ pub mod data;
 pub mod environment;
 pub mod specs;
 pub mod utils;
+
+pub use prusti_error::*;
+
+mod prusti_error;

prusti-viper/src/encoder/errors/prusti_error.rs → prusti-interface/src/prusti_error.rs

@@ -5,13 +5,14 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 use rustc_span::MultiSpan;
-use prusti_interface::environment::Environment;
+use crate::environment::Environment;
 use prusti_common::config;
 use ::log::warn;
 
 /// The Prusti message that will be reported to the user.
 ///
 /// A Prusti message can originate from:
+/// * invalid usage detected during specification collection
 /// * an encoding error (see the `EncodingError` type)
 /// * a Viper verification error
 ///

prusti-interface/src/specs/external.rs

@@ -0,0 +1,144 @@
+use rustc_hir::intravisit::{self, Visitor};
+use rustc_hir::def_id::DefId;
+use rustc_middle::hir::map::Map;
+use rustc_middle::ty::TyCtxt;
+use rustc_span::{Span, MultiSpan};
+
+use std::collections::HashMap;
+use crate::specs::typed::ExternSpecificationMap;
+use crate::environment::Environment;
+use crate::PrustiError;
+
+/// This struct is used to build a mapping of external functions to their
+/// Prusti specifications (see `extern_fn_map`).
+pub struct ExternSpecResolver<'tcx> {
+    tcx: TyCtxt<'tcx>,
+
+    /// Maps real functions (keyed by their `DefId`) to Prusti-generated fake
+    /// functions with specifications. The mapping may also optionally contain
+    /// the `DefId` of the implementing type to account for trait
+    /// implementations.
+    extern_fn_map: ExternSpecificationMap<'tcx>,
+
+    /// Duplicate specifications detected, keyed by the `DefId` of the function
+    /// to be specified.
+    spec_duplicates: HashMap<DefId, Vec<(DefId, Span)>>,
+}
+
+impl<'tcx> ExternSpecResolver<'tcx> {
+    pub fn new(tcx: TyCtxt<'tcx>) -> Self {
+        Self {
+            tcx: tcx,
+            extern_fn_map: HashMap::new(),
+            spec_duplicates: HashMap::new(),
+        }
+    }
+
+    /// Registers an external function specification. The arguments for this
+    /// function are the same as arguments given to a function visit in an
+    /// intravisit visitor.
+    ///
+    /// In case of duplicates, the function is added to `spec_duplicates`, and
+    /// will later (in `check_duplicates`) be reported as an error. Otherwise,
+    /// the function is added to `extern_fn_map`.
+    pub fn add_extern_fn(
+        &mut self,
+        fn_kind: intravisit::FnKind<'tcx>,
+        fn_decl: &'tcx rustc_hir::FnDecl,
+        body_id: rustc_hir::BodyId,
+        span: Span,
+        id: rustc_hir::hir_id::HirId
+    ) {
+        let mut visitor = ExternSpecVisitor {
+            tcx: self.tcx,
+            spec_found: None,
+        };
+        visitor.visit_fn(fn_kind, fn_decl, body_id, span, id);
+        let current_def_id = self.tcx.hir().local_def_id(id).to_def_id();
+        if let Some((def_id, impl_ty, span)) = visitor.spec_found {
+            match self.extern_fn_map.get(&def_id) {
+                Some((existing_impl_ty, _)) if existing_impl_ty == &impl_ty => {
+                    match self.spec_duplicates.get_mut(&def_id) {
+                        Some(dups) => {
+                            dups.push((current_def_id, span));
+                        }
+                        None => {
+                            self.spec_duplicates.insert(def_id, vec![(current_def_id, span)]);
+                        }
+                    }
+                }
+                _ => {
+                    // TODO: what if def_id was present, but impl_ty was different?
+                    self.extern_fn_map.insert(def_id, (impl_ty, current_def_id));
+                }
+            }
+        }
+    }
+
+    /// Report errors for duplicate specifications found during specification
+    /// collection.
+    pub fn check_duplicates(&self, env: &Environment<'tcx>) {
+        for (def_id, specs) in self.spec_duplicates.iter() {
+            PrustiError::incorrect(
+                format!("duplicate specification for {:?}", def_id),
+                MultiSpan::from_spans(specs.iter()
+                    .map(|s| s.1)
+                    .collect())
+            ).emit(env);
+        }
+    }
+
+    pub fn get_extern_fn_map(&self) -> ExternSpecificationMap<'tcx> {
+        self.extern_fn_map.clone()
+    }
+}
+
+/// A visitor that is called on external specification methods, as generated by
+/// the external spec rewriter, looking specifically for the call to the
+/// external function.
+///
+/// TODO: is the HIR representation stable enought that this could be
+/// accomplished by a nested match rather than a full visitor?
+struct ExternSpecVisitor<'tcx> {
+    tcx: TyCtxt<'tcx>,
+    spec_found: Option<(DefId, Option<DefId>, Span)>,
+}
+
+/// Gets the `DefId` from the given path.
+fn get_impl_type<'tcx>(qself: &rustc_hir::QPath<'tcx>) -> Option<DefId> {
+    if let rustc_hir::QPath::TypeRelative(ty, _) = qself {
+        if let rustc_hir::TyKind::Path(qpath) = &ty.kind {
+            if let rustc_hir::QPath::Resolved(_, path) = qpath {
+                if let rustc_hir::def::Res::Def(_, id) = path.res {
+                    return Some(id);
+                }
+            }
+        }
+    }
+    return None;
+}
+
+impl<'tcx> Visitor<'tcx> for ExternSpecVisitor<'tcx> {
+    type Map = Map<'tcx>;
+
+    fn nested_visit_map<'this>(&'this mut self) -> intravisit::NestedVisitorMap<Self::Map> {
+        let map = self.tcx.hir();
+        intravisit::NestedVisitorMap::All(map)
+    }
+
+    fn visit_expr(&mut self, ex: &'tcx rustc_hir::Expr<'tcx>) {
+        if self.spec_found.is_some() {
+            return;
+        }
+        if let rustc_hir::ExprKind::Call(ref callee_expr, ref arguments) = ex.kind {
+            if let rustc_hir::ExprKind::Path(ref qself) = callee_expr.kind {
+                let res = self.tcx.typeck(callee_expr.hir_id.owner).qpath_res(qself, callee_expr.hir_id);
+                if let rustc_hir::def::Res::Def(_, def_id) = res {
+                    self.spec_found = Some((def_id, get_impl_type(qself), ex.span.source_callsite()));
+                    return;
+                }
+            }
+        }
+        intravisit::walk_expr(self, ex);
+    }
+}

prusti-interface/src/specs/mod.rs

@@ -8,12 +8,15 @@ use rustc_span::symbol::Symbol;
 use rustc_hir::def_id::LocalDefId;
 use std::collections::HashMap;
 use std::convert::TryInto;
-use crate::utils::has_spec_only_attr;
+use crate::utils::{has_spec_only_attr, has_extern_spec_attr};
+use crate::environment::Environment;
 
+pub mod external;
 pub mod typed;
 
 use typed::StructuralToTyped;
 use std::fmt;
+use crate::specs::external::ExternSpecResolver;
 
 struct SpecItem {
     spec_id: typed::SpecificationId,
@@ -39,6 +42,7 @@ pub struct SpecCollector<'tcx> {
     spec_items: Vec<SpecItem>,
     current_spec_item: Option<SpecItem>,
     typed_expressions: HashMap<String, LocalDefId>,
+    extern_resolver: ExternSpecResolver<'tcx>,
 }
 
 impl<'tcx> SpecCollector<'tcx> {
@@ -48,6 +52,7 @@ impl<'tcx> SpecCollector<'tcx> {
             spec_items: Vec::new(),
             current_spec_item: None,
             typed_expressions: HashMap::new(),
+            extern_resolver: ExternSpecResolver::new(tcx),
         }
     }
     pub fn determine_typed_procedure_specs(self) -> typed::SpecificationMap<'tcx> {
@@ -65,7 +70,8 @@ impl<'tcx> SpecCollector<'tcx> {
             })
             .collect()
     }
-    fn process_item(&mut self, item: Item){
+
+    fn process_item(&mut self, item: Item) {
         if has_spec_only_attr(item.attrs) {
             assert!(
                 self.current_spec_item.is_none(),
@@ -91,6 +97,11 @@ impl<'tcx> SpecCollector<'tcx> {
             self.current_spec_item = Some(spec_item);
         }
     }
+
+    pub fn determine_extern_procedure_specs(&self, env: &Environment<'tcx>) -> typed::ExternSpecificationMap<'tcx> {
+        self.extern_resolver.check_duplicates(env);
+        self.extern_resolver.get_extern_fn_map()
+    }
 }
 
 fn reconstruct_typed_assertion<'tcx>(
@@ -148,6 +159,7 @@ impl<'tcx> intravisit::Visitor<'tcx> for SpecCollector<'tcx> {
         let map = self.tcx.hir();
         intravisit::NestedVisitorMap::All(map)
     }
+
     fn visit_item(&mut self, item: &'tcx rustc_hir::Item<'tcx>) {
         if let ItemKind::Impl {items, ..} = &item.kind {
             for impl_item_ref in items.iter() {
@@ -168,6 +180,7 @@ impl<'tcx> intravisit::Visitor<'tcx> for SpecCollector<'tcx> {
             self.spec_items.push(spec_item);
         }
     }
+
     fn visit_fn(
         &mut self,
         fn_kind: intravisit::FnKind<'tcx>,
@@ -182,9 +195,12 @@ impl<'tcx> intravisit::Visitor<'tcx> for SpecCollector<'tcx> {
                 let local_id = self.tcx.hir().local_def_id(id);
                 self.typed_expressions.insert(expr_id, local_id);
             }
+        } else if has_extern_spec_attr(fn_kind.attrs()) {
+            self.extern_resolver.add_extern_fn(fn_kind, fn_decl, body_id, span, id);
         }
         intravisit::walk_fn(self, fn_kind, fn_decl, body_id, span, id);
     }
+
     fn visit_local(&mut self, local: &'tcx rustc_hir::Local<'tcx>) {
         let mut clean_spec_item = false;
         if has_spec_only_attr(&local.attrs) {

prusti-interface/src/specs/typed.rs

@@ -7,6 +7,7 @@ use rustc_span::Span;
 use std::collections::HashMap;
 
 pub use common::{ExpressionId, SpecType, SpecificationId};
+use crate::data::ProcedureDefId;
 
 #[derive(Debug, Clone)]
 pub enum SpecificationMapElement<'tcx> {
@@ -33,6 +34,8 @@ pub type LoopSpecification<'tcx> = common::LoopSpecification<ExpressionId, Local
 pub type ProcedureSpecification<'tcx> = common::ProcedureSpecification<ExpressionId, LocalDefId, (mir::Local, ty::Ty<'tcx>)>;
 /// A map of untyped specifications for a specific crate.
 pub type SpecificationMap<'tcx> = HashMap<common::SpecificationId, SpecificationMapElement<'tcx>>;
+/// A map of untyped external specifications.
+pub type ExternSpecificationMap<'tcx> = HashMap<ProcedureDefId, (Option<ProcedureDefId>, ProcedureDefId)>;
 /// An assertion that has no types associated with it.
 pub type Assertion<'tcx> = common::Assertion<ExpressionId, LocalDefId, (mir::Local, ty::Ty<'tcx>)>;
 /// An assertion kind that has no types associated with it.

prusti-interface/src/utils.rs

@@ -291,6 +291,11 @@ pub fn has_spec_only_attr(attrs: &[ast::Attribute]) -> bool {
     has_prusti_attr(attrs, "spec_only")
 }
 
+/// Check if `prusti::extern_spec` is among the attributes.
+pub fn has_extern_spec_attr(attrs: &[ast::Attribute]) -> bool {
+    has_prusti_attr(attrs, "extern_spec")
+}
+
 // pub fn get_attr_value(attr: &ast::Attribute) -> String {
 //     use syntax::parse::token;
 //     use syntax::tokenstream::TokenTree;