diff --git a/creusot-contracts-proc/src/creusot.rs b/creusot-contracts-proc/src/creusot.rs index d5e981cb1b..5f0dd78bda 100644 --- a/creusot-contracts-proc/src/creusot.rs +++ b/creusot-contracts-proc/src/creusot.rs @@ -14,7 +14,7 @@ pub(crate) use self::{ extern_spec::extern_spec, logic::{logic, pearlite}, proof::{ghost, ghost_let, invariant, proof_assert, snapshot}, - specs::{bitwise_proof, check, ensures, maintains, requires, variant}, + specs::{bitwise_proof, check, ensures, has_logical_alias, maintains, requires, variant}, }; use crate::common::{ContractSubject, FnOrMethod}; diff --git a/creusot-contracts-proc/src/creusot/specs.rs b/creusot-contracts-proc/src/creusot/specs.rs index 2e3dd0e881..bdd398a3e1 100644 --- a/creusot-contracts-proc/src/creusot/specs.rs +++ b/creusot-contracts-proc/src/creusot/specs.rs @@ -10,7 +10,7 @@ use crate::{ use pearlite_syn::{Term, TermPath}; use proc_macro::TokenStream as TS1; use proc_macro2::{Span, TokenStream}; -use quote::quote; +use quote::{quote, quote_spanned}; use syn::{ Attribute, Ident, Item, Path, ReturnType, Signature, Stmt, Token, Type, parenthesized, parse::{self, Parse}, @@ -72,6 +72,10 @@ pub fn requires(attr: TS1, tokens: TS1) -> TS1 { } 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); @@ -80,6 +84,12 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 { let ens_name = crate::creusot::generate_unique_ident(&item.name(), Span::call_site()); let name_tag = ens_name.to_string(); + let logical_alias = if logical_alias_path { + quote_spanned! {term.span()=> #[creusot::decl::logical_alias_path = #name_tag]} + } else { + quote!() + }; + match item { ContractSubject::FnOrMethod(mut s) if s.is_trait_signature() => { let attrs = std::mem::take(&mut s.attrs); @@ -96,6 +106,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 { TS1::from(quote! { #ensures_tokens #[creusot::clause::ensures=#name_tag] + #logical_alias #(#attrs)* #documentation #s @@ -113,6 +124,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 { } TS1::from(quote! { #[creusot::clause::ensures=#name_tag] + #logical_alias #(#attrs)* #documentation #f @@ -129,6 +141,7 @@ pub fn ensures(attr: TS1, tokens: TS1) -> TS1 { #ensures_tokens #res_id }); + // FIXME: forbid logical aliases in this case TS1::from(quote! { #[creusot::clause::ensures=#name_tag] #clos @@ -224,6 +237,29 @@ pub fn check(args: TS1, tokens: TS1) -> TS1 { result.into() } +pub fn has_logical_alias(attr: TS1, tokens: TS1) -> TS1 { + let logic_path = match syn::parse::(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 syn::ImplItemFn); + let args = func.sig.inputs.iter().map(|a| match a { + syn::FnArg::Receiver(receiver) => { + let self_t = receiver.self_token; + quote!(#self_t) + } + syn::FnArg::Typed(pat_type) => { + let pat = &pat_type.pat; + quote!(#pat) + } + }); + let ensures_contract = quote_spanned! {logic_path.span()=> result == #logic_path(#(#args),*)}; + ensures_inner(ensures_contract.into(), tokens, true) +} + pub fn bitwise_proof(_: TS1, tokens: TS1) -> TS1 { let tokens: TokenStream = tokens.into(); TS1::from(quote! { diff --git a/creusot-contracts-proc/src/dummy.rs b/creusot-contracts-proc/src/dummy.rs index e00a2f7f5c..5dd1d35683 100644 --- a/creusot-contracts-proc/src/dummy.rs +++ b/creusot-contracts-proc/src/dummy.rs @@ -112,6 +112,10 @@ pub fn bitwise_proof(_: TS1, tokens: TS1) -> TS1 { tokens } +pub fn has_logical_alias(_: TS1, tokens: TS1) -> TS1 { + tokens +} + pub fn derive_deep_model(_: TS1) -> TS1 { TS1::new() } diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs index 5c1e29e134..284ab25f7d 100644 --- a/creusot-contracts-proc/src/lib.rs +++ b/creusot-contracts-proc/src/lib.rs @@ -66,6 +66,7 @@ proc_macro_attributes! { bitwise_proof maintains erasure + has_logical_alias } macro_rules! proc_macros { diff --git a/creusot-contracts/src/lib.rs b/creusot-contracts/src/lib.rs index 4ce8b69535..38430679bf 100644 --- a/creusot-contracts/src/lib.rs +++ b/creusot-contracts/src/lib.rs @@ -487,6 +487,38 @@ pub mod macros { pub use base_macros::erasure; pub(crate) use base_macros::intrinsic; + + /// 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, + /// } + /// impl S { + /// #[has_logical_alias(Self::read_t_logic)] + /// pub fn read_t(&self) -> &T { + /// &self.t + /// } + /// + /// #[logic] + /// pub fn read_t_logic(&self) -> &T { + /// &self.t + /// } + /// } + /// + /// // ... + /// + /// #[requires(s.read_t().view() == 1)] + /// pub fn foo(s: S) { /* ... */ } + /// ``` + pub use base_macros::has_logical_alias; } #[doc(hidden)] diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs index 11105a4f29..a8b2ff1cb1 100644 --- a/creusot/src/contracts_items/attributes.rs +++ b/creusot/src/contracts_items/attributes.rs @@ -1,5 +1,6 @@ //! Defines all the internal creusot attributes. +use crate::ctx::{HasTyCtxt as _, TranslationCtx}; use rustc_ast::{ LitKind, MetaItemInner, Param, token::TokenKind, @@ -13,8 +14,6 @@ use why3::{ declaration::{Attribute as WAttribute, Meta, MetaArg, MetaIdent}, }; -use crate::ctx::HasTyCtxt as _; - /// Helper macro, converts `creusot::foo::bar` into `["creusot", "foo", "bar"]`. macro_rules! path_to_str { ([ :: $($p:tt)* ] ; [ $($acc:expr,)* ]) => { @@ -258,6 +257,40 @@ pub(crate) fn is_open_inv_param(tcx: TyCtxt, p: &Param) -> bool { found } +/// 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, +) -> Option<(Span, DefId)> { + let attrs = get_attrs(ctx.get_all_attrs(def_id), &["creusot", "decl", "logical_alias_path"]); + let attr = match attrs.as_slice() { + [] => return None, + [a] => a, + _ => { + ctx.dcx().span_err( + attrs.iter().map(|attr| attr.span()).collect::>(), + "A function cannot have multiple logical aliases", + ); + return 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).expect("no ensures clause associated with this alias"); + match &ensures_body.1.kind { + crate::translation::pearlite::TermKind::Binary { rhs, .. } => match &rhs.kind { + crate::translation::pearlite::TermKind::Call { id, .. } => Some((attr.span(), *id)), + _ => unreachable!("this should be a function call"), + }, + _ => unreachable!("this should be an equality"), + } +} + fn get_attrs<'a>(attrs: &'a [Attribute], path: &[&str]) -> Vec<&'a Attribute> { let mut matched = Vec::new(); diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index 2d050438bd..5bc35f84b6 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -2,8 +2,8 @@ use crate::{ backend::ty_inv::is_tyinv_trivial, callbacks, contracts_items::{ - Intrinsic, gather_intrinsics, get_creusot_item, is_extern_spec, is_logic, is_opaque, - is_open_inv_param, is_prophetic, opacity_witness_name, + Intrinsic, function_has_logical_alias, gather_intrinsics, get_creusot_item, is_extern_spec, + is_logic, is_opaque, is_open_inv_param, is_prophetic, opacity_witness_name, }, metadata::{BinaryMetadata, Metadata, encode_def_ids, get_erasure_required}, naming::variable_name, @@ -41,8 +41,8 @@ use rustc_middle::{ mir::Promoted, thir, ty::{ - Clause, GenericArg, GenericArgsRef, ParamEnv, Predicate, ResolverAstLowering, Ty, TyCtxt, - TypingEnv, TypingMode, Visibility, + Clause, GenericArg, GenericArgKind, GenericArgsRef, ParamEnv, Predicate, + ResolverAstLowering, Ty, TyCtxt, TypingEnv, TypingMode, Visibility, }, }; use rustc_span::{DUMMY_SP, Span, Symbol}; @@ -191,6 +191,9 @@ pub struct TranslationCtx<'tcx> { erasures_to_check: Vec<(LocalDefId, Erasure<'tcx>)>, params_open_inv: HashMap>, laws: OnceMap>>, + /// Maps the [`DefId`] of a program function `f` with a `#[has_logical_alias(f')]` + /// attribute to the logical function `f'` + logical_aliases: HashMap, fmir_body: OnceMap>>, terms: OnceMap>>>, trait_impl: OnceMap>>>, @@ -263,6 +266,7 @@ impl<'tcx> TranslationCtx<'tcx> { did2intrinsic, laws: Default::default(), externs, + logical_aliases: Default::default(), terms: Default::default(), creusot_items, variant_calls: RefCell::new(IndexMap::new()), @@ -318,6 +322,168 @@ impl<'tcx> TranslationCtx<'tcx> { self.local_thir.iter() } + /// Get the _logical alias_ of the given program function, if any. + /// + /// Logical aliases are defined with the `#[has_logical_alias(...)]` attribute. + /// + /// 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() + } + + /// Load all the logical aliases defined in the current crate + /// + /// They can later be retrieved using [`Self::logical_alias`]. + pub(crate) fn load_logical_aliases(&mut self) { + // FIXME: what about functions from another crate? + let tcx = self.tcx; + for local_id in self.hir_body_owners() { + let def_id = local_id.to_def_id(); + // TODO: Put this in another file for better organisation + if let Some((span, logic_id)) = function_has_logical_alias(self, def_id) { + let program_span = tcx.def_span(def_id); + let logic_span = tcx.def_span(logic_id); + let program_subst = erased_identity_for_item(tcx, def_id); + let logic_subst = erased_identity_for_item(tcx, logic_id); + let mut program_subst = program_subst.iter().map(|arg| arg.kind()); + let mut logic_subst = logic_subst.iter().map(|arg| arg.kind()); + loop { + let prog_arg = program_subst.next(); + let logic_arg = logic_subst.next(); + match (prog_arg, logic_arg) { + (None, None) => break, + (Some(arg), None) | (None, Some(arg)) => { + tcx.dcx() + .struct_span_err( + span, + format!( + "mismatched generic parameters for logical alias: {} parameter {arg:?} in the alias", + if prog_arg.is_some() { + "missing" + } else { + "additional" + }), + ) + .with_span_note(program_span, "function defined here") + .with_span_note(logic_span, "logical alias defined here") + .emit(); + } + (Some(GenericArgKind::Type(t1)), Some(GenericArgKind::Type(t2))) => { + if t1 != t2 { + tcx.dcx().struct_span_err(span, format!("mismatched types in logical alias: expected {t1}, got {t2}")) + .with_span_note(program_span, "function defined here") + .with_span_note(logic_span, "logical alias defined here") + .emit(); + } + } + (Some(GenericArgKind::Const(c1)), Some(GenericArgKind::Const(c2))) => { + let (t1, name1) = match c1.kind() { + rustc_type_ir::ConstKind::Param(p) => { + (p.find_const_ty_from_env(tcx.param_env(def_id)), p.name) + } + _ => unreachable!(), + }; + let (t2, name2) = match c2.kind() { + rustc_type_ir::ConstKind::Param(p) => { + (p.find_const_ty_from_env(tcx.param_env(logic_id)), p.name) + } + _ => unreachable!(), + }; + if t1 != t2 { + tcx.dcx() + .struct_span_err( + span, + format!("mismatched types of constants: expected {t1} (constant {name1}), got {t2} (constant {name2})"), + ) + .with_span_note(program_span, "function defined here") + .with_span_note(logic_span, "logical function defined here") + .emit(); + } + } + ( + Some(GenericArgKind::Lifetime(l1)), + Some(GenericArgKind::Lifetime(l2)), + ) => { + if l1 != l2 { + tcx.dcx() + .struct_span_err( + span, + "mismatched lifetime parameters for logical alias: expected {l1}, got {l2}", + ) + .with_span_note(program_span, "function defined here") + .with_span_note(logic_span, "logical function defined here") + .emit(); + } + } + (Some(a1), Some(a2)) => { + tcx.dcx() + .struct_span_err(span, format!("mismatched parameter kinds for logical alias: expected {a1:?}, got {a2:?}")) + .with_span_note(program_span, "function defined here") + .with_span_note(logic_span, "logical function defined here") + .emit(); + } + } + } + let bounds1 = tcx.param_env(def_id).caller_bounds(); + let bounds2 = tcx.param_env(logic_id).caller_bounds(); + if bounds1 != bounds2 { + let mut err = tcx + .dcx() + .struct_span_err(span, "mismatched trait bounds for logical alias"); + for (b1, b2) in std::iter::zip(bounds1.iter().rev(), bounds2.iter().rev()) { + if b1 != b2 { + err.note(format!("{b1} != {b2}")); + } + } + if bounds1.len() < bounds2.len() { + for b in bounds2.iter().rev().skip(bounds1.len()) { + err.note(format!("additional bound {b} found")); + } + } else if bounds1.len() > bounds2.len() { + for b in bounds1.iter().rev().skip(bounds2.len()) { + err.note(format!("missing bound {b}")); + } + } + err.with_span_note(program_span, "function defined here") + .with_span_note(logic_span, "logical function defined here") + .emit(); + } + + // the aliased function must also comes from the current crate + if !logic_id.is_local() { + tcx.dcx() + .struct_span_err( + program_span, + "The aliased logical function should be defined in the same crate", + ) + .with_span_note(logic_span, "aliased function defined here") + .emit(); + } + // When defining an alias, neither functions must be a trait function + if tcx.trait_of_assoc(def_id).is_some() { + tcx.dcx().span_err( + program_span, + "Cannot make a logical alias from a trait function", + ); + } + if tcx.trait_of_assoc(logic_id).is_some() { + tcx.dcx() + .span_err(logic_span, "Cannot make a logical alias to a trait function"); + } + if tcx.dcx().has_errors().is_some() { + continue; + } + + trace!( + "`{}` is an alias for `{}`", + self.def_path_str(local_id), + self.def_path_str(logic_id), + ); + self.logical_aliases.insert(def_id, (span, logic_id)); + } + } + } + queryish!(trait_impl, DefId, Vec>, translate_impl); queryish!(fmir_body, BodyId, fmir::Body<'tcx>, translation::function::fmir); diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs index b0e37491ad..0985ae9d8f 100644 --- a/creusot/src/translation.rs +++ b/creusot/src/translation.rs @@ -74,6 +74,7 @@ pub(crate) fn after_analysis<'tcx>( let start = Instant::now(); let mut ctx = TranslationCtx::new(tcx, opts.clone(), thir, params_open_inv); ctx.load_extern_specs(); + ctx.load_logical_aliases(); ctx.load_erasures(); validate(&ctx); ctx.dcx().abort_if_errors(); diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs index f12a6c5815..9746a06ac5 100644 --- a/creusot/src/translation/pearlite.rs +++ b/creusot/src/translation/pearlite.rs @@ -182,6 +182,9 @@ pub enum TermKind<'tcx> { trigger: Box<[Trigger<'tcx>]>, body: Box>, }, + /// A function call. + /// + /// Be careful when building this case, that it respects [logical aliases](TranslationCtx::logical_alias). // TODO: Get rid of (id, subst). Call { id: DefId, @@ -796,6 +799,10 @@ impl<'tcx> ThirTerm<'_, 'tcx> { .iter() .map(|arg| self.expr_term(*arg)) .collect::>()?; + let id = match self.ctx.logical_alias(id) { + None => id, + Some((_, alias_id)) => alias_id, + }; Ok(Term::call_no_normalize(self.ctx.tcx, id, subst, args).span(span)) } } @@ -1444,6 +1451,7 @@ impl<'tcx> Term<'tcx> { Term { ty, kind: TermKind::Tuple { fields }, span } } + /// Same as [`Self::call`], but does not normalize the type of the result. pub(crate) fn call_no_normalize( tcx: TyCtxt<'tcx>, def_id: DefId, @@ -1456,6 +1464,11 @@ impl<'tcx> Term<'tcx> { Term { ty: result, span: DUMMY_SP, kind: TermKind::Call { id: def_id, subst, args } } } + /// Generate a [`TermKind::Call`] for a special function described by `(def_id, subst)` + /// (e.g. `resolve`, `inv`, etc) + /// + /// Note that this should not be used for regular function calls, in particular because + /// it does not consider [logical aliases](TranslationCtx::logical_alias). pub(crate) fn call( tcx: TyCtxt<'tcx>, typing_env: TypingEnv<'tcx>, diff --git a/creusot/src/util.rs b/creusot/src/util.rs index e499d763da..5e98753c14 100644 --- a/creusot/src/util.rs +++ b/creusot/src/util.rs @@ -1,5 +1,4 @@ -use std::{hash::Hash as _, path::Path}; - +use creusot_args::options::SpanMode; use rustc_hir::{ def::DefKind, def_id::{DefId, DefPathHash, LOCAL_CRATE}, @@ -14,8 +13,7 @@ use rustc_middle::{ }; use rustc_serialize::{Decodable, Decoder, Encodable, Encoder}; use rustc_span::{Span, Symbol}; - -use creusot_args::options::SpanMode; +use std::{hash::Hash as _, path::Path}; pub(crate) fn erased_identity_for_item(tcx: TyCtxt, did: DefId) -> GenericArgsRef { tcx.erase_and_anonymize_regions(GenericArgs::identity_for_item(tcx, did)) diff --git a/creusot/src/validate/purity.rs b/creusot/src/validate/purity.rs index 4a662c2f29..2abb9cbc6a 100644 --- a/creusot/src/validate/purity.rs +++ b/creusot/src/validate/purity.rs @@ -81,10 +81,26 @@ pub(crate) fn validate_purity<'tcx>( if ctx.tcx.is_closure_like(def_id) { return; } - if !is_logic(ctx.tcx, def_id) && is_trusted_item(ctx.tcx, def_id) { return; } + if let Some((span, alias_id)) = ctx.logical_alias(def_id) { + if is_logic(ctx.tcx, def_id) { + ctx.dcx() + .struct_span_err( + 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(); + } + if !is_logic(ctx.tcx, alias_id) { + ctx.dcx() + .struct_span_err(span, "Only logic functions can be aliased") + .with_note(format!("{} is not a logic function", ctx.def_path_str(alias_id))) + .emit(); + } + } let typing_env = ctx.typing_env(def_id); PurityVisitor { ctx, thir, context: Purity::of_def_id(ctx, def_id), typing_env } @@ -215,6 +231,12 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { .unwrap(); let fn_purity = self.purity(func_did, args); + let fn_purity = match self.ctx.logical_alias(func_did) { + Some((_, alias_did)) if !self.context.can_call(fn_purity) => { + self.purity(alias_did, args) + } + _ => fn_purity, + }; if matches!(self.context, Purity::Logic { .. }) && ( // These methods are allowed to cheat the purity restrictions diff --git a/tests/should_succeed/logical_aliases.rs b/tests/should_succeed/logical_aliases.rs new file mode 100644 index 0000000000..651dffd02c --- /dev/null +++ b/tests/should_succeed/logical_aliases.rs @@ -0,0 +1,46 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +#[has_logical_alias(add_logic)] +#[check(ghost)] +fn add(x: Int, y: Int) -> Int { + x + y +} +#[logic] +fn add_logic(x: Int, y: Int) -> Int { + x + y +} + +pub fn test_add() { + ghost! { + let x = 3int; + let y = add(x, 5int); + proof_assert!(y == add(x, 5)); + }; +} + +struct Seq2(Seq); + +impl Seq2 { + #[has_logical_alias(Self::len_logic)] + #[check(ghost)] + fn len(&self) -> Int { + self.0.len_ghost() + } + #[logic] + fn len_logic(&self) -> Int { + self.0.len() + } +} + +pub fn test_seq() { + ghost! { + let mut s = Seq2(Seq::new().into_inner()); + s.0.push_back_ghost(2int); + let l1 = s.len(); + proof_assert!(l1 == s.len()); + s.0.push_back_ghost(4int); + let l2 = s.len(); + proof_assert!(l2 == s.len()); + }; +}