Check that has_logical_alias is used with the correct purities

Author: dianegolfouse

creusot-contracts-proc/src/creusot.rs

@@ -159,7 +159,7 @@ fn ensures_inner(attr: TS1, tokens: TS1, logical_alias_path: bool) -> TS1 {
     let ens_name = generate_unique_ident(&item.name());
     let name_tag = format!("{}", quote! { #ens_name });
     let logical_alias = if logical_alias_path {
-        quote!(#[creusot::decl::logical_alias_path = #name_tag])
+        quote_spanned!(term.span() => #[creusot::decl::logical_alias_path = #name_tag])
     } else {
         quote!()
     };
@@ -624,7 +624,7 @@ pub fn has_logical_alias(attr: TS1, tokens: TS1) -> TS1 {
             quote!(#pat)
         }
     });
-    let ensures_contract = quote!(result == #logic_path(#(#args),*));
+    let ensures_contract = quote_spanned!(logic_path.span() => result == #logic_path(#(#args),*));
     ensures_inner(ensures_contract.into(), tokens, true)
 }
 

creusot/src/contracts_items/attributes.rs

@@ -4,7 +4,7 @@ use crate::{ctx::TranslationCtx, error::CannotFetchThir};
 use rustc_ast::Param;
 use rustc_hir::{AttrArgs, Attribute, def_id::DefId};
 use rustc_middle::ty::TyCtxt;
-use rustc_span::Symbol;
+use rustc_span::{Span, Symbol};
 use why3::declaration::Attribute as WAttribute;
 
 /// Helper macro, converts `creusot::foo::bar` into `["creusot", "foo", "bar"]`.
@@ -157,7 +157,7 @@ pub(crate) fn is_open_inv_param(tcx: TyCtxt, p: &Param) -> bool {
 pub(crate) fn function_has_logical_alias(
     ctx: &mut TranslationCtx,
     def_id: DefId,
-) -> Result<Option<DefId>, CannotFetchThir> {
+) -> Result<Option<(Span, DefId)>, CannotFetchThir> {
     let mut attrs =
         get_attrs(ctx.get_attrs_unchecked(def_id), &["creusot", "decl", "logical_alias_path"]);
     if attrs.len() >= 2 {
@@ -179,7 +179,7 @@ pub(crate) fn function_has_logical_alias(
     let ensures_body = ctx.term(ensures_def_id)?.unwrap();
     match &ensures_body.1.kind {
         crate::translation::pearlite::TermKind::Binary { rhs, .. } => match &rhs.kind {
-            crate::translation::pearlite::TermKind::Call { id, .. } => Ok(Some(*id)),
+            crate::translation::pearlite::TermKind::Call { id, .. } => Ok(Some((attr.span(), *id))),
             _ => unreachable!(),
         },
         _ => unreachable!(),

creusot/src/ctx.rs

@@ -156,7 +156,7 @@ pub struct TranslationCtx<'tcx> {
     laws: OnceMap<DefId, Box<Vec<DefId>>>,
     /// Maps the [`DefId`] of a program function `f` with a `#[has_logical_alias(f')]`
     /// attribute to the logical function `f'`
-    logical_aliases: HashMap<DefId, DefId>,
+    logical_aliases: HashMap<DefId, (Span, DefId)>,
     fmir_body: OnceMap<BodyId, Box<fmir::Body<'tcx>>>,
     terms: OnceMap<DefId, Box<Option<ScopedTerm<'tcx>>>>,
     trait_impl: OnceMap<DefId, Box<TraitImpl<'tcx>>>,
@@ -237,23 +237,24 @@ impl<'tcx> TranslationCtx<'tcx> {
     /// Get the _logical alias_ of the given program function, if any.
     ///
     /// Logical aliases are defined with the `#[has_logical_alias(...)]` attribute.
-    pub(crate) fn logical_alias(&self, def_id: DefId) -> Option<DefId> {
+    ///
+    /// The returned span is the span of the attribute.
+    pub(crate) fn logical_alias(&self, def_id: DefId) -> Option<(Span, DefId)> {
         self.logical_aliases.get(&def_id).copied()
     }
 
     pub(crate) fn load_logical_aliases(&mut self) -> Result<(), CannotFetchThir> {
         // FIXME: what about functions from another crate?
-        // FIXME: ensure here that the functions have the correct purity (program & logical)
         let mut err = None;
         for def_id in self.tcx.hir().body_owners() {
             match function_has_logical_alias(self, def_id.to_def_id()) {
-                Ok(Some(aliased)) => {
+                Ok(Some((span, aliased))) => {
                     trace!(
                         "`{}` is an alias for `{}`",
                         self.def_path_str(def_id),
                         self.def_path_str(aliased),
                     );
-                    self.logical_aliases.insert(def_id.to_def_id(), aliased);
+                    self.logical_aliases.insert(def_id.to_def_id(), (span, aliased));
                 }
                 Ok(None) => {}
                 Err(e) => CannotFetchThir::merge_opt(&mut err, e),

creusot/src/translation/pearlite.rs

@@ -794,7 +794,7 @@ impl<'tcx> ThirTerm<'_, 'tcx> {
                                 .collect::<Result<_, _>>()?;
                             let id = match self.ctx.logical_alias(id) {
                                 None => id,
-                                Some(alias_id) => alias_id,
+                                Some((_, alias_id)) => alias_id,
                             };
                             Ok(Term::call_no_normalize(self.ctx.tcx, id, subst, args).span(span))
                         }

creusot/src/validate/purity.rs

@@ -103,6 +103,22 @@ pub(crate) fn validate_purity(
 
     let def_id = def_id.to_def_id();
     let purity = Purity::of_def_id(ctx, def_id);
+    if let Some((span, alias_id)) = ctx.logical_alias(def_id) {
+        if !matches!(purity, Purity::Program { .. }) {
+            ctx.error(
+                ctx.def_ident_span(def_id).unwrap_or_default(),
+                "Only program functions can use `#[has_logical_alias(...)]`",
+            )
+            .with_span_label(span, "alias defined here")
+            .emit();
+        }
+        let alias_purity = Purity::of_def_id(ctx, alias_id);
+        if !matches!(alias_purity, Purity::Logic { .. }) {
+            ctx.error(span, "Only logic functions can be aliased")
+                .with_note(format!("{} is not a logic function", ctx.def_path_str(alias_id)))
+                .emit();
+        }
+    }
     if matches!(purity, Purity::Program { .. })
         && (is_no_translate(ctx.tcx, def_id) || is_trusted_item(ctx.tcx, def_id))
     {
@@ -198,7 +214,7 @@ impl<'a, 'tcx> thir::visit::Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> {
 
                     let fn_purity = self.purity(fun, func_did, args);
                     let fn_alias_purity = match self.ctx.logical_alias(func_did) {
-                        Some(alias_did) => self.purity(fun, alias_did, args),
+                        Some((_, alias_did)) => self.purity(fun, alias_did, args),
                         None => fn_purity,
                     };
                     if !(self.context.can_call(fn_purity)