Logical functions aliases

creusot-contracts-dummy/src/lib.rs

@@ -52,6 +52,11 @@ pub fn pure(_: TS1, tokens: TS1) -> TS1 {
     tokens
 }
 
+#[proc_macro_attribute]
+pub fn has_logical_alias(_: TS1, tokens: TS1) -> TS1 {
+    tokens
+}
+
 #[proc_macro_attribute]
 pub fn logic(_: TS1, _: TS1) -> TS1 {
     TS1::new()

creusot-contracts-proc/src/lib.rs

@@ -256,6 +256,10 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 {
 
 #[proc_macro_attribute]
 pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
+    ensures_inner(attr, tokens, false)
+}
+
+fn ensures_inner(attr: TS1, tokens: TS1, logical_alias_path: bool) -> TS1 {
     let documentation = document_spec("ensures", doc::LogicBody::Some(attr.clone()));
 
     let mut item = parse_macro_input!(tokens as ContractSubject);
@@ -264,6 +268,11 @@ pub fn ensures(attr: TS1, tokens: TS1) -> 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])
+    } else {
+        quote!()
+    };
 
     match item {
         ContractSubject::FnOrMethod(mut s) if s.is_trait_signature() => {
@@ -278,7 +287,8 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
             let ensures_tokens = sig_spec_item(ens_name, sig, term);
             TS1::from(quote! {
               #ensures_tokens
-              #[creusot::clause::ensures=#name_tag]
+              #[creusot::clause::ensures = #name_tag]
+              #logical_alias
               #(#attrs)*
               #documentation
               #s
@@ -296,13 +306,15 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 {
                 b.stmts.insert(0, Stmt::Item(Item::Verbatim(ensures_tokens)))
             }
             TS1::from(quote! {
-                #[creusot::clause::ensures=#name_tag]
+                #[creusot::clause::ensures = #name_tag]
+                #logical_alias
                 #(#attrs)*
                 #documentation
                 #f
             })
         }
         ContractSubject::Closure(mut clos) => {
+            // TODO: forbid logical aliases in this case
             let req_body = req_body(&term);
             let attrs = spec_attrs(&ens_name);
             let body = &clos.body;
@@ -435,6 +447,27 @@ pub fn pure(_: TS1, tokens: TS1) -> TS1 {
     .into()
 }
 
+#[proc_macro_attribute]
+pub fn has_logical_alias(attr: TS1, tokens: TS1) -> TS1 {
+    let logic_path = match syn::parse::<Path>(attr.clone()) {
+        Ok(path) => path,
+        Err(err) => {
+            return syn::Error::new(err.span(), "`has_logical_alias` should contain a path to a logical function with the same signature").to_compile_error().into()
+        }
+    };
+    let tokens_2 = tokens.clone();
+    let func = parse_macro_input!(tokens_2 as ImplItemFn);
+    let args = func.sig.inputs.iter().map(|a| match a {
+        FnArg::Receiver(receiver) => quote_spanned!(receiver.span() => self),
+        FnArg::Typed(pat_type) => {
+            let pat = &pat_type.pat;
+            quote!(#pat)
+        }
+    });
+    let ensures_contract = quote!(result == #logic_path(#(#args),*));
+    ensures_inner(ensures_contract.into(), tokens, true)
+}
+
 #[proc_macro]
 pub fn ghost(body: TS1) -> TS1 {
     let body = proc_macro2::TokenStream::from(ghost::ghost_preprocess(body));

creusot-contracts/src/lib.rs

@@ -369,6 +369,39 @@ pub mod macros {
     /// This attribute can be used on a function or closure to instruct Creusot not to ensure as a postcondition that the
     /// return value of the function satisfies its [type invariant](crate::Invariant).
     pub use base_macros::open_inv_result;
+
+    /// Defines a _logical alias_ for a program function.
+    ///
+    /// Logical aliases allow you to use the same name for a program and a [`logic`] function.
+    /// Creusot will generate a proof obligation to show that the two functions return
+    /// the same results.
+    ///
+    /// # Example
+    ///
+    /// ```rust
+    /// use creusot_contracts::*;
+    /// pub struct S<T> {
+    ///     t: T,
+    /// }
+    /// impl<T> S<T> {
+    ///     #[has_logical_alias(Self::read_t_logic)]
+    ///     pub fn read_t(&self) -> &T {
+    ///         &self.t
+    ///     }
+    ///
+    ///     #[logic]
+    ///     #[open(self)]
+    ///     pub fn read_t_logic(&self) -> &T {
+    ///         &self.t
+    ///     }
+    /// }
+    ///
+    /// // ...
+    ///
+    /// #[requires(s.read_t().view() == 1)]
+    /// pub fn foo(s: S<i32>) { /* ... */ }
+    /// ```
+    pub use base_macros::has_logical_alias;
 }
 
 #[doc(hidden)]

creusot/src/contracts_items/attributes.rs

@@ -5,6 +5,8 @@ use rustc_hir::{def_id::DefId, AttrArgs, Attribute};
 use rustc_middle::ty::TyCtxt;
 use rustc_span::Symbol;
 
+use crate::{ctx::TranslationCtx, error::CannotFetchThir};
+
 /// Helper macro, converts `creusot::foo::bar` into `["creusot", "foo", "bar"]`.
 macro_rules! path_to_str {
     ([ :: $($p:tt)* ] ; [ $($acc:expr,)* ]) => {
@@ -114,6 +116,37 @@ pub(crate) fn creusot_clause_attrs<'tcx>(
         .map(|a| &a.get_normal_item().args)
 }
 
+/// If a function is annotated with `#[has_logical_alias(f)]`, return the [`DefId`] of `f`.
+pub(crate) fn function_has_logical_alias(
+    ctx: &mut TranslationCtx,
+    def_id: DefId,
+) -> Result<Option<DefId>, CannotFetchThir> {
+    let mut attrs =
+        get_attrs(ctx.get_attrs_unchecked(def_id), &["creusot", "decl", "logical_alias_path"]);
+    if attrs.len() >= 2 {
+        let _ = ctx.dcx().span_err(
+            attrs.iter().map(|attr| attr.span()).collect::<Vec<_>>(),
+            "A function cannot have multiple logical aliases",
+        );
+        return Err(CannotFetchThir);
+    }
+    let Some(attr) = attrs.pop() else { return Ok(None) };
+    let symbol = match &attr.get_normal_item().args {
+        AttrArgs::Eq { expr, .. } => expr.symbol,
+        _ => unreachable!(),
+    };
+    // the `ensures(result == f(args))` clause
+    let ensures_def_id = ctx.creusot_item(symbol).unwrap();
+    let ensures_body = ctx.term(ensures_def_id)?.unwrap();
+    match &ensures_body.kind {
+        crate::pearlite::TermKind::Binary { rhs, .. } => match &rhs.kind {
+            crate::pearlite::TermKind::Call { id, .. } => Ok(Some(*id)),
+            _ => unreachable!(),
+        },
+        _ => unreachable!(),
+    }
+}
+
 pub(crate) fn get_creusot_item(tcx: TyCtxt, def_id: DefId) -> Option<Symbol> {
     Some(
         get_attr(tcx, tcx.get_attrs_unchecked(def_id), &["creusot", "item"])?
@@ -122,7 +155,7 @@ pub(crate) fn get_creusot_item(tcx: TyCtxt, def_id: DefId) -> Option<Symbol> {
     )
 }
 
-pub(crate) fn is_open_inv_param<'tcx>(tcx: TyCtxt<'tcx>, p: &Param) -> bool {
+pub(crate) fn is_open_inv_param(tcx: TyCtxt, p: &Param) -> bool {
     let mut found = false;
     for a in &p.attrs {
         if a.is_doc_comment() {
@@ -150,7 +183,7 @@ pub(crate) fn is_open_inv_param<'tcx>(tcx: TyCtxt<'tcx>, p: &Param) -> bool {
         }
     }
 
-    return found;
+    found
 }
 
 fn get_attrs<'a>(attrs: &'a [Attribute], path: &[&str]) -> Vec<&'a Attribute> {
@@ -176,15 +209,11 @@ fn get_attrs<'a>(attrs: &'a [Attribute], path: &[&str]) -> Vec<&'a Attribute> {
     matched
 }
 
-fn get_attr<'a, 'tcx>(
-    tcx: TyCtxt<'tcx>,
-    attrs: &'a [Attribute],
-    path: &[&str],
-) -> Option<&'a Attribute> {
+fn get_attr<'a>(tcx: TyCtxt, attrs: &'a [Attribute], path: &[&str]) -> Option<&'a Attribute> {
     let matched = get_attrs(attrs, path);
     match matched.len() {
-        0 => return None,
-        1 => return Some(matched[0]),
+        0 => None,
+        1 => Some(matched[0]),
         _ => tcx.dcx().span_fatal(matched[0].span, "Unexpected duplicate attribute.".to_string()),
     }
 }

creusot/src/ctx.rs

@@ -2,8 +2,8 @@ use crate::{
     backend::ty_inv::is_tyinv_trivial,
     callbacks,
     contracts_items::{
-        get_inv_function, is_extern_spec, is_logic, is_open_inv_param, is_predicate, is_prophetic,
-        opacity_witness_name,
+        function_has_logical_alias, get_inv_function, is_extern_spec, is_logic, is_open_inv_param,
+        is_predicate, is_prophetic, opacity_witness_name,
     },
     creusot_items::{self, CreusotItems},
     error::{CannotFetchThir, CreusotResult, Error},
@@ -157,6 +157,9 @@ pub struct TranslationCtx<'tcx> {
     creusot_items: CreusotItems,
     extern_specs: HashMap<DefId, ExternSpec<'tcx>>,
     extern_spec_items: HashMap<LocalDefId, 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>,
     trait_impl: HashMap<DefId, TraitImpl<'tcx>>,
     sig: HashMap<DefId, PreSignature<'tcx>>,
     bodies: HashMap<LocalDefId, Rc<BodyWithBorrowckFacts<'tcx>>>,
@@ -175,7 +178,7 @@ impl<'tcx> Deref for TranslationCtx<'tcx> {
 
 fn gather_params_open_inv(tcx: TyCtxt) -> HashMap<DefId, Vec<usize>> {
     struct VisitFns<'tcx, 'a>(TyCtxt<'tcx>, HashMap<DefId, Vec<usize>>, &'a ResolverAstLowering);
-    impl<'tcx, 'a> Visitor<'a> for VisitFns<'tcx, 'a> {
+    impl<'a> Visitor<'a> for VisitFns<'_, 'a> {
         fn visit_fn(&mut self, fk: FnKind<'a>, _: Span, node: NodeId) {
             let decl = match fk {
                 FnKind::Fn(_, _, _, Fn { sig: FnSig { decl, .. }, .. }) => decl,
@@ -214,6 +217,7 @@ impl<'tcx> TranslationCtx<'tcx> {
             opts,
             extern_specs: Default::default(),
             extern_spec_items: Default::default(),
+            logical_aliases: Default::default(),
             fmir_body: Default::default(),
             trait_impl: Default::default(),
             sig: Default::default(),
@@ -520,6 +524,38 @@ impl<'tcx> TranslationCtx<'tcx> {
         Ok(())
     }
 
+    /// 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> {
+        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 has_err = false;
+        for def_id in self.tcx.hir().body_owners() {
+            match function_has_logical_alias(self, def_id.to_def_id()) {
+                Ok(Some(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);
+                }
+                Ok(None) => {}
+                Err(_) => has_err = true,
+            }
+        }
+        if has_err {
+            Err(CannotFetchThir)
+        } else {
+            Ok(())
+        }
+    }
+
     pub(crate) fn item_type(&self, def_id: DefId) -> ItemType {
         match self.tcx.def_kind(def_id) {
             DefKind::Trait => ItemType::Trait,

creusot/src/translation.rs

@@ -58,6 +58,9 @@ pub(crate) fn before_analysis(ctx: &mut TranslationCtx) -> Result<(), Box<dyn st
         Err(Error::MustPrint(msg)) => msg.emit(ctx.tcx),
         Err(Error::TypeCheck(_)) => ctx.tcx.dcx().abort_if_errors(),
     };
+    // OK to ignore this error, because we abort just below.
+    let _ = ctx.load_logical_aliases();
+    ctx.tcx.dcx().abort_if_errors();
 
     for def_id in ctx.tcx.hir().body_owners() {
         // OK to ignore this error, because we abort after the loop.
@@ -214,7 +217,7 @@ fn remove_coma_files(dir: &PathBuf) -> std::io::Result<()> {
             if path.is_dir() {
                 remove_coma_files(&path)?;
                 let _ = std::fs::remove_dir(path); // remove the directory if it's empty, do nothing otherwise
-            } else if path.extension().map_or(false, |ext| ext == "coma") {
+            } else if path.extension().is_some_and(|ext| ext == "coma") {
                 std::fs::remove_file(&path)?;
             }
         }