From a90d17fa8625b5c93de7cee58bb2193e43873d4a Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 9 Mar 2026 13:17:02 +0100 Subject: [PATCH 1/4] Refactor resolve_item to separate the handling of traits from methods --- creusot/src/translation/traits.rs | 278 +++++++++++++++++------------- 1 file changed, 155 insertions(+), 123 deletions(-) diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs index 2d60730d3a..a612caddd9 100644 --- a/creusot/src/translation/traits.rs +++ b/creusot/src/translation/traits.rs @@ -191,6 +191,155 @@ pub(crate) fn evaluate_additional_predicates<'tcx>( if !errors.is_empty() { Err(errors) } else { Ok(()) } } +pub enum ImplSelection<'tcx> { + Found(&'tcx ImplSource<'tcx, ()>), + UnknownFound, + None, +} + +pub fn select_trait_impl<'tcx>( + tcx: TyCtxt<'tcx>, + typing_env: TypingEnv<'tcx>, + trait_ref: TraitRef<'tcx>, +) -> ImplSelection<'tcx> { + use ImplSelection::*; + let trait_ref = tcx.normalize_erasing_regions(typing_env, trait_ref); + + let source = tcx.codegen_select_candidate(typing_env.as_query_input(trait_ref)); + match source { + // FIXME: if there are several instances available, `codegen_select_candidate` + // returns an error, while we would like it to return any of the instances. + // We need to find another entry point of the trait solver. + // In the meantime, pretend that we have an instance that we do not know + Err(CodegenObligationError::Ambiguity) => return UnknownFound, + Err(_) => return None, + Ok(source) => Found(source), + } +} + +pub fn select_method<'tcx>( + tcx: TyCtxt<'tcx>, + typing_env: TypingEnv<'tcx>, + trait_ref: TraitRef<'tcx>, + trait_item_def_id: DefId, + substs: GenericArgsRef<'tcx>, + source: &'tcx ImplSource<'tcx, ()>, +) -> TraitResolved<'tcx> { + match source { + ImplSource::UserDefined(impl_data) => { + // Find the id of the actual associated method we will be running + let leaf_def = tcx + .trait_def(trait_ref.def_id) + .ancestors(tcx, impl_data.impl_def_id) + .unwrap() + .leaf_def(tcx, trait_item_def_id) + .unwrap_or_else(|| { + panic!("{:?} not found in {:?}", trait_item_def_id, impl_data.impl_def_id); + }); + + if !(leaf_def.is_final() || is_sealed(tcx, leaf_def.item.def_id)) { + // The instance we found is not final nor sealed. There might be a speciallized + // matching instance. + // We have found a user-defined instance, so we know for sure that there is no + // matching instance in a future crate. Hence we explore the descendents of the + // current node to make sure that there is no specialized matching instances. + + let Ok(gt) = GraphTraversal::new(tcx, typing_env.param_env, trait_ref) else { + // Cannot find graph because of an error. Return a dummy value. + return TraitResolved::UnknownFound; + }; + + let r = gt.traverse_descendants(impl_data.impl_def_id, |node| { + if tcx.impl_item_implementor_ids(node).get(&trait_item_def_id).is_some() { + // This is a matching instance + GraphTraversalAction::Interrupt + } else if tcx.defaultness(node).is_final() { + // This is a final instance without a matching implementation + // We know that a specializing impl cannot have an implementation + // for our method + GraphTraversalAction::Skip + } else { + GraphTraversalAction::Traverse + } + }); + if !r { + return TraitResolved::UnknownFound; + } + } + + // Translate the original substitution into one on the selected impl method + let infcx = tcx.infer_ctxt().build(TypingMode::non_body_analysis()); + let args = rustc_trait_selection::traits::translate_args( + &infcx, + typing_env.param_env, + impl_data.impl_def_id, + impl_data.args, + leaf_def.defining_node, + ); + let substs = substs.rebase_onto(tcx, trait_ref.def_id, args); + + let leaf_substs = tcx.erase_and_anonymize_regions(substs); + + TraitResolved::Instance { + def: (leaf_def.item.def_id, leaf_substs), + impl_: ImplSource_::Impl(impl_data.impl_def_id, impl_data.args), + } + } + ImplSource::Param(_) => { + // Check whether the default impl from the trait def is sealed + if is_sealed(tcx, trait_item_def_id) { + return TraitResolved::Instance { + def: (trait_item_def_id, substs), + impl_: ImplSource_::Param, + }; + } + + // TODO: we could try to explore the graph to determine if we can be sure + // that another impl is guaranteed to be the one we are seaching for + + TraitResolved::UnknownFound + } + ImplSource::Builtin(_, _) => { + if matches!(substs.type_at(0).kind(), rustc_middle::ty::Dynamic(_, _)) { + // These types are not supported, but we want to display a proper error message because + // they are rather common in real Rust code, and this is not the right place to emit + // such an error message. + return TraitResolved::UnknownFound; + } + + if [ + tcx.lang_items().fn_trait(), + tcx.lang_items().fn_mut_trait(), + tcx.lang_items().fn_once_trait(), + ] + .contains(&Some(trait_ref.def_id)) + { + match *substs.type_at(0).kind() { + TyKind::Closure(closure_def_id, closure_substs) => { + return TraitResolved::Instance { + def: (closure_def_id, closure_substs), + impl_: ImplSource_::Fn, + }; + } + TyKind::FnDef(did, subst) => { + return TraitResolved::Instance { + def: (did, subst), + impl_: ImplSource_::Fn, + }; + } + _ => (), + } + } + + unimplemented!( + "Cannot handle builtin implementation of `{}` for `{}`", + tcx.def_path_str(trait_ref.def_id), + substs.type_at(0) + ) + } + } +} + #[derive(Debug, Clone, Copy)] pub(crate) enum ImplSource_<'tcx> { /// The id and substitution of the impl block, if any. @@ -244,132 +393,15 @@ impl<'tcx> TraitResolved<'tcx> { }; let trait_ref = tcx.normalize_erasing_regions(typing_env, Unnormalized::new(trait_ref)); - let source = tcx.codegen_select_candidate(typing_env.as_query_input(trait_ref)); - if let Err(err) = source { - if let CodegenObligationError::Ambiguity = err { - // FIXME: if there are several instances available, `codegen_select_candidate` - // returns an error, while we would like it to return any of the instances. - // We need to find another entry point of the trait solver. - // In the meantime, pretend that we have an instance that we do not know - return TraitResolved::UnknownFound; + let source = match select_trait_impl(tcx, typing_env, trait_ref) { + ImplSelection::Found(source) => source, + ImplSelection::UnknownFound => return Self::UnknownFound, + ImplSelection::None => { + return Self::NoInstance(NoInstance { tcx, typing_env, trait_ref }); } - return TraitResolved::NoInstance(NoInstance { tcx, typing_env, trait_ref }); }; trace!("TraitResolved::resolve {source:?}",); - - match source.unwrap() { - ImplSource::UserDefined(impl_data) => { - // Find the id of the actual associated method we will be running - let leaf_def = tcx - .trait_def(trait_ref.def_id) - .ancestors(tcx, impl_data.impl_def_id) - .unwrap() - .leaf_def(tcx, trait_item_def_id) - .unwrap_or_else(|| { - panic!("{:?} not found in {:?}", trait_item_def_id, impl_data.impl_def_id); - }); - - if !(leaf_def.is_final() || is_sealed(tcx, leaf_def.item.def_id)) { - // The instance we found is not final nor sealed. There might be a speciallized - // matching instance. - // We have found a user-defined instance, so we know for sure that there is no - // matching instance in a future crate. Hence we explore the descendents of the - // current node to make sure that there is no specialized matching instances. - - let Ok(gt) = GraphTraversal::new(tcx, typing_env.param_env, trait_ref) else { - // Cannot find graph because of an error. Return a dummy value. - return TraitResolved::UnknownFound; - }; - - let r = gt.traverse_descendants(impl_data.impl_def_id, |node| { - if tcx.impl_item_implementor_ids(node).get(&trait_item_def_id).is_some() { - // This is a matching instance - GraphTraversalAction::Interrupt - } else if tcx.defaultness(node).is_final() { - // This is a final instance without a matching implementation - // We know that a specializing impl cannot have an implementation - // for our method - GraphTraversalAction::Skip - } else { - GraphTraversalAction::Traverse - } - }); - if !r { - return TraitResolved::UnknownFound; - } - } - - // Translate the original substitution into one on the selected impl method - let infcx = tcx.infer_ctxt().build(TypingMode::non_body_analysis()); - let args = rustc_trait_selection::traits::translate_args( - &infcx, - typing_env.param_env, - impl_data.impl_def_id, - impl_data.args, - leaf_def.defining_node, - ); - let substs = substs.rebase_onto(tcx, trait_ref.def_id, args); - - let leaf_substs = tcx.erase_and_anonymize_regions(substs); - - TraitResolved::Instance { - def: (leaf_def.item.def_id, leaf_substs), - impl_: ImplSource_::Impl(impl_data.impl_def_id, impl_data.args), - } - } - ImplSource::Param(_) => { - // Check whether the default impl from the trait def is sealed - if is_sealed(tcx, trait_item_def_id) { - return TraitResolved::Instance { - def: (trait_item_def_id, substs), - impl_: ImplSource_::Param, - }; - } - - // TODO: we could try to explore the graph to determine if we can be sure - // that another impl is guaranteed to be the one we are seaching for - - TraitResolved::UnknownFound - } - ImplSource::Builtin(_, _) => { - if matches!(substs.type_at(0).kind(), rustc_middle::ty::Dynamic(_, _)) { - // These types are not supported, but we want to display a proper error message because - // they are rather common in real Rust code, and this is not the right place to emit - // such an error message. - return TraitResolved::UnknownFound; - } - - if [ - tcx.lang_items().fn_trait(), - tcx.lang_items().fn_mut_trait(), - tcx.lang_items().fn_once_trait(), - ] - .contains(&Some(trait_ref.def_id)) - { - match *substs.type_at(0).kind() { - TyKind::Closure(closure_def_id, closure_substs) => { - return TraitResolved::Instance { - def: (closure_def_id, closure_substs), - impl_: ImplSource_::Fn, - }; - } - TyKind::FnDef(did, subst) => { - return TraitResolved::Instance { - def: (did, subst), - impl_: ImplSource_::Fn, - }; - } - _ => (), - } - } - - unimplemented!( - "Cannot handle builtin implementation of `{}` for `{}`", - tcx.def_path_str(trait_ref.def_id), - substs.type_at(0) - ) - } - } + select_method(tcx, typing_env, trait_ref, trait_item_def_id, substs, source) } pub(crate) fn to_opt( From 24b4abc14dba3062f21eb4123f977885f01ada82 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Thu, 26 Mar 2026 10:55:12 +0100 Subject: [PATCH 2/4] Handle proof trees in termination check --- creusot-std-proc/src/creusot.rs | 64 ++- creusot-std-proc/src/creusot/specs.rs | 18 +- creusot-std/src/ghost/fn_ghost.rs | 6 +- creusot/src/contracts_items/attributes.rs | 3 +- creusot/src/translation/specification.rs | 78 +++- creusot/src/translation/traits.rs | 2 +- creusot/src/validate/purity.rs | 171 +++++--- creusot/src/validate/terminates.rs | 395 ++++++++++++------ creusot/src/validate/traits.rs | 6 +- tests/should_fail/bug/1565.stderr | 7 +- tests/should_fail/bug/459.stderr | 7 +- .../complicated_traits_recursion.stderr | 7 +- .../default_function_non_logic.stderr | 7 +- .../default_function_non_open.stderr | 7 +- 14 files changed, 535 insertions(+), 243 deletions(-) diff --git a/creusot-std-proc/src/creusot.rs b/creusot-std-proc/src/creusot.rs index cf7707d9d8..827acd357c 100644 --- a/creusot-std-proc/src/creusot.rs +++ b/creusot-std-proc/src/creusot.rs @@ -20,11 +20,12 @@ pub(crate) use self::{ use crate::common::{ContractSubject, FnOrMethod}; use proc_macro::TokenStream as TS1; use proc_macro2::{Span, TokenStream}; -use quote::quote; +use quote::{TokenStreamExt as _, quote}; use syn::{ Error, FnArg, Ident, LitStr, Macro, Result, Token, parse, parse::{Parse, ParseStream}, parse_macro_input, parse_quote, + punctuated::Punctuated, spanned::Spanned as _, }; @@ -36,21 +37,66 @@ pub fn open_inv_result(_: TS1, tokens: TS1) -> TS1 { }) } -pub fn trusted(_: TS1, tokens: TS1) -> TS1 { +pub fn trusted(arg: TS1, tokens: TS1) -> TS1 { match from_proof_assert(tokens.clone()) { Ok(Some(assertion)) => proof_assert_(assertion, true), Ok(None) => { - let tokens = TokenStream::from(tokens); - TS1::from(quote! { - #[creusot::decl::trusted] - #[allow(creusot::experimental)] - #tokens - }) + if arg.is_empty() { + let tokens = TokenStream::from(tokens); + TS1::from(quote! { + #[creusot::decl::trusted] + #[allow(creusot::experimental)] + #tokens + }) + } else { + let args = parse_macro_input!( + arg with Punctuated::::parse_separated_nonempty + ); + let mut tokens = tokens.into(); + for arg in args { + tokens = quote! { #arg #tokens }; + } + TS1::from(tokens) + } } Err(e) => e.into_compile_error().into(), } } +enum TrustedArg { + /// #[trusted(ghost)] + Ghost, + /// #[trusted(terminates)] + Terminates, +} + +impl Parse for TrustedArg { + fn parse(src: ParseStream) -> syn::Result { + use TrustedArg::*; + let ident = src.parse::()?; + if ident == "ghost" { + Ok(Ghost) + } else if ident == "terminates" { + Ok(Terminates) + } else { + Err(Error::new( + ident.span(), + "Unexpected `#[trusted]` argument: expected `terminates` or nothing", + )) + } + } +} + +impl quote::ToTokens for TrustedArg { + fn to_tokens(&self, stream: &mut TokenStream) { + use TrustedArg::*; + stream.append_all(match self { + Ghost => quote! { #[creusot::decl::trusted_ghost] }, + Terminates => quote! { #[creusot::decl::trusted_terminates] }, + }) + } +} + /// Try to extract the body of a `proof_assert!`. /// Error if it is a macro different from `proof_assert!`. fn from_proof_assert(tokens: TS1) -> Result> { @@ -60,7 +106,7 @@ fn from_proof_assert(tokens: TS1) -> Result> { } else { Err(Error::new( m.path.span(), - "Unexpected #[trusted] item: expected `proof_assert!` or a declaration or a closure", + "Unexpected `#[trusted]` item: expected `proof_assert!` or a declaration or a closure", )) } } diff --git a/creusot-std-proc/src/creusot/specs.rs b/creusot-std-proc/src/creusot/specs.rs index 76e96b247d..4ddeb760bb 100644 --- a/creusot-std-proc/src/creusot/specs.rs +++ b/creusot-std-proc/src/creusot/specs.rs @@ -159,28 +159,22 @@ pub fn maintains(attr: TS1, body: TS1) -> TS1 { pub fn check(args: TS1, tokens: TS1) -> TS1 { let mode = parse_macro_input!(args as Ident); - let (terminates, ghost, ghost_trusted) = if mode == "terminates" { - (true, false, false) + let ghost = if mode == "terminates" { + false } else if mode == "ghost" { - (true, true, false) - } else if mode == "ghost_trusted" { - (true, true, true) + true } else { let msg = format!("unknown mode `{mode}`. Accepted modes are `terminates` or `ghost`"); return quote! { compile_error!(#msg) }.into(); }; let mut documentation = TokenStream::new(); let mut clauses = TokenStream::new(); - if terminates { - documentation.extend(document_spec("terminates", doc::LogicBody::None)); - clauses.extend(quote!(#[creusot::clause::check_terminates])); - } if ghost { documentation.extend(document_spec("ghost", doc::LogicBody::None)); clauses.extend(quote!(#[creusot::clause::check_ghost])); - } - if ghost_trusted { - clauses.extend(quote!(#[creusot::clause::check_ghost::trusted])) + } else { + documentation.extend(document_spec("terminates", doc::LogicBody::None)); + clauses.extend(quote!(#[creusot::clause::check_terminates])); } let item = tokens.clone(); let item = parse_macro_input!(item as ContractSubject); diff --git a/creusot-std/src/ghost/fn_ghost.rs b/creusot-std/src/ghost/fn_ghost.rs index ca48def433..5a495c6d70 100644 --- a/creusot-std/src/ghost/fn_ghost.rs +++ b/creusot-std/src/ghost/fn_ghost.rs @@ -40,9 +40,9 @@ impl> FnOnce for FnGhostWrapper { type Output = F::Output; #[trusted] + #[trusted(ghost)] #[requires(self.precondition(args))] #[ensures(self.postcondition_once(args, result))] - #[check(ghost_trusted)] extern "rust-call" fn call_once(self, args: I) -> Self::Output { self.0.call_once(args) } @@ -50,9 +50,9 @@ impl> FnOnce for FnGhostWrapper { #[cfg(creusot)] impl> FnMut for FnGhostWrapper { #[trusted] + #[trusted(ghost)] #[requires((*self).precondition(args))] #[ensures((*self).postcondition_mut(args, ^self, result))] - #[check(ghost_trusted)] extern "rust-call" fn call_mut(&mut self, args: I) -> Self::Output { self.0.call_mut(args) } @@ -60,9 +60,9 @@ impl> FnMut for FnGhostWrapper { #[cfg(creusot)] impl> Fn for FnGhostWrapper { #[trusted] + #[trusted(ghost)] #[requires((*self).precondition(args))] #[ensures((*self).postcondition(args, result))] - #[check(ghost_trusted)] extern "rust-call" fn call(&self, args: I) -> Self::Output { self.0.call(args) } diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs index 79cedebb4e..192dd49734 100644 --- a/creusot/src/contracts_items/attributes.rs +++ b/creusot/src/contracts_items/attributes.rs @@ -64,6 +64,8 @@ attribute_functions! { [creusot::decl::logic::inline] => is_inline [creusot::decl::opaque] => is_opaque [creusot::decl::trusted] => is_trusted + [creusot::decl::trusted_ghost] => is_trusted_ghost + [creusot::decl::trusted_terminates] => is_trusted_terminates [creusot::decl::new_namespace] => is_new_namespace [creusot::decl::open_inv_result] => is_open_inv_result [creusot::extern_spec] => is_extern_spec @@ -71,7 +73,6 @@ attribute_functions! { [creusot::clause::variant] => has_variant_clause [creusot::clause::check_terminates] => is_check_terminates [creusot::clause::check_ghost] => is_check_ghost - [creusot::clause::check_ghost::trusted] => is_check_ghost_trusted [creusot::bitwise] => is_bitwise [creusot::builtin_ascription] => is_builtin_ascription } diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs index 90652bcdbc..3ff44395bf 100644 --- a/creusot/src/translation/specification.rs +++ b/creusot/src/translation/specification.rs @@ -1,6 +1,9 @@ use crate::{ backend::closures::ClosSubst, - contracts_items::{Intrinsic, creusot_clause_attrs, is_check_ghost, is_check_terminates}, + contracts_items::{ + Intrinsic, creusot_clause_attrs, is_check_ghost, is_check_terminates, is_trusted_ghost, + is_trusted_terminates, + }, ctx::*, lints::{Diagnostics, RESULT_PARAM}, naming::{lowercase_prefix, name}, @@ -17,6 +20,49 @@ use rustc_span::{DUMMY_SP, Span}; use rustc_type_ir::ClosureKind; use std::iter::repeat; +#[derive( + Eq, + PartialEq, + Ord, + PartialOrd, + Clone, + Copy, + Debug, + TypeFoldable, + TypeVisitable, + TyEncodable, + TyDecodable, +)] +pub enum ProgramPurity { + /// Default purity + Impure, + /// Terminates (but might panic, e.g., `Vec` overflow) + Terminates, + /// Callable in ghost context (must terminate successfully) + Ghost, +} + +impl ProgramPurity { + pub fn is_ghost(self) -> bool { + self == ProgramPurity::Ghost + } + + pub fn is_terminates(self) -> bool { + self >= ProgramPurity::Terminates + } +} + +impl std::fmt::Display for ProgramPurity { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + use ProgramPurity::*; + match self { + Impure => write!(f, "impure"), + Terminates => write!(f, "terminates"), + Ghost => write!(f, "ghost"), + } + } +} + /// A term with an "expl:" label (includes the "expl:" prefix) #[derive(Clone, Debug, TypeFoldable, TypeVisitable)] pub struct Condition<'tcx> { @@ -32,8 +78,8 @@ pub struct PreContract<'tcx> { pub(crate) variant: Option>, pub(crate) requires: Vec>, pub(crate) ensures: Vec<(Box<[Trigger<'tcx>]>, Condition<'tcx>)>, - pub(crate) check_ghost: bool, - pub(crate) check_terminates: bool, + /// Ignored for logic functions + pub(crate) purity: ProgramPurity, pub(crate) extern_no_spec: bool, /// Are any of the contract clauses here user provided? or merely Creusot inferred / provided? pub(crate) has_user_contract: bool, @@ -105,8 +151,7 @@ pub struct ContractClauses { variant: Option, requires: Vec, ensures: Vec, - pub(crate) check_ghost: bool, - pub(crate) check_terminates: bool, + pub(crate) purity: ProgramPurity, } impl ContractClauses { @@ -115,8 +160,7 @@ impl ContractClauses { variant: None, requires: Vec::new(), ensures: Vec::new(), - check_ghost: false, - check_terminates: false, + purity: ProgramPurity::Impure, } } @@ -167,14 +211,12 @@ impl ContractClauses { log::trace!("variant clause {:?}", var_id); ctx.term(var_id).unwrap().rename(bound) }); - log::trace!("ghost: {}", self.check_ghost); - log::trace!("terminates: {}", self.check_terminates); + log::trace!("purity: {}", self.purity); EarlyBinder::bind(PreContract { variant, requires, ensures, - check_ghost: self.check_ghost, - check_terminates: self.check_terminates, + purity: self.purity, extern_no_spec: false, has_user_contract, }) @@ -214,10 +256,15 @@ pub(crate) fn contract_clauses_of( if it_variant.next().transpose()?.is_some() { return Err(MultipleVariant { id: def_id }); } - let check_terminates = is_check_terminates(ctx.tcx, def_id); - let check_ghost = is_check_ghost(ctx.tcx, def_id); + let purity = if is_check_ghost(ctx.tcx, def_id) || is_trusted_ghost(ctx.tcx, def_id) { + ProgramPurity::Ghost + } else if is_check_terminates(ctx.tcx, def_id) || is_trusted_terminates(ctx.tcx, def_id) { + ProgramPurity::Terminates + } else { + ProgramPurity::Impure + }; - Ok(ContractClauses { requires, ensures, variant, check_terminates, check_ghost }) + Ok(ContractClauses { requires, ensures, variant, purity }) } pub(crate) fn inherited_extern_spec<'tcx>( @@ -356,8 +403,7 @@ pub(crate) fn pre_sig_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Pre variant: None, requires: vec![], ensures: vec![], - check_ghost: true, - check_terminates: true, + purity: ProgramPurity::Ghost, extern_no_spec: false, has_user_contract: false, }; diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs index a612caddd9..57dabb18b3 100644 --- a/creusot/src/translation/traits.rs +++ b/creusot/src/translation/traits.rs @@ -203,7 +203,7 @@ pub fn select_trait_impl<'tcx>( trait_ref: TraitRef<'tcx>, ) -> ImplSelection<'tcx> { use ImplSelection::*; - let trait_ref = tcx.normalize_erasing_regions(typing_env, trait_ref); + let trait_ref = tcx.normalize_erasing_regions(typing_env, Unnormalized::new(trait_ref)); let source = tcx.codegen_select_candidate(typing_env.as_query_input(trait_ref)); match source { diff --git a/creusot/src/validate/purity.rs b/creusot/src/validate/purity.rs index 8f630ab3a5..779895e902 100644 --- a/creusot/src/validate/purity.rs +++ b/creusot/src/validate/purity.rs @@ -1,10 +1,10 @@ use crate::{ contracts_items::{ - Intrinsic, is_check_ghost_trusted, is_erasure, is_logic, is_prophetic, is_snapshot_closure, - is_spec, is_trusted, + Intrinsic, is_check_ghost, is_check_terminates, is_erasure, is_logic, is_prophetic, + is_snapshot_closure, is_spec, is_trusted, is_trusted_ghost, is_trusted_terminates, }, ctx::{HasTyCtxt, TranslationCtx}, - translation::traits::TraitResolved, + translation::{specification::ProgramPurity, traits::TraitResolved}, }; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_infer::infer::TyCtxtInferExt; @@ -17,62 +17,101 @@ use rustc_trait_selection::infer::InferCtxtExt; #[derive(Clone, Copy, PartialEq, Eq, Debug)] pub(crate) enum Purity { - /// Same as `Program { terminates: true, ghost: true }`, but can also call the few + /// The context of ghost blocks. + /// Similar to `Program { purity: Ghost }`, but can also call the few /// ghost-only functions (e.g. `Ghost::new`). Ghost, Program { - terminates: bool, - ghost: bool, + purity: ProgramPurity, }, Logic { prophetic: bool, }, } -impl Purity { +// Purity of the function being checked +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +enum LocalPurity { + Purity(Purity), + TrustedTerminates, + TrustedGhost, +} + +impl LocalPurity { pub(crate) fn of_def_id<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Self { + use self::Purity::*; + use LocalPurity::*; if is_logic(ctx.tcx, def_id) { - Purity::Logic { prophetic: is_prophetic(ctx.tcx, def_id) } + Self::logic(is_prophetic(ctx.tcx, def_id)) } else if is_spec(ctx.tcx, def_id) { - Purity::Logic { prophetic: !is_snapshot_closure(ctx.tcx, def_id) } + Self::logic(!is_snapshot_closure(ctx.tcx, def_id)) + } else if is_trusted_ghost(ctx.tcx, def_id) + || is_check_ghost(ctx.tcx, def_id) && is_trusted(ctx.tcx, def_id) + { + TrustedGhost + } else if is_trusted_terminates(ctx.tcx, def_id) + || is_check_terminates(ctx.tcx, def_id) && is_trusted(ctx.tcx, def_id) + { + TrustedTerminates } else { - let contract = &ctx.sig(def_id).contract; - Purity::Program { terminates: contract.check_terminates, ghost: contract.check_ghost } + Purity(Program { purity: ctx.sig(def_id).contract.purity }) } } - /// If `logic_only` is `true`, this only checks for `Purity::Logic` VS `Purity::Program`. - fn can_call(self, other: Purity, logic_only: bool) -> bool { + fn can_call(self, other: Purity) -> bool { + use self::Purity::*; + use LocalPurity::*; match (self, other) { - (Purity::Ghost | Purity::Program { .. }, Purity::Ghost | Purity::Program { .. }) - if logic_only => - { - true - } - (Purity::Logic { prophetic }, Purity::Logic { prophetic: prophetic2 }) => { + (Purity(Logic { prophetic }), Logic { prophetic: prophetic2 }) => { prophetic || !prophetic2 } - ( - Purity::Program { ghost, terminates }, - Purity::Program { ghost: ghost2, terminates: terminates2 }, - ) => ghost <= ghost2 && terminates <= terminates2, - (Purity::Ghost, Purity::Ghost | Purity::Program { ghost: true, terminates: true }) => { - true - } + (Purity(Program { purity }), Program { purity: purity2 }) => purity <= purity2, + (Purity(Ghost), Ghost | Program { purity: ProgramPurity::Ghost }) => true, + (TrustedTerminates, Program { .. }) => true, + (TrustedGhost, Ghost | Program { .. }) => true, (_, _) => false, } } + fn logic(prophetic: bool) -> Self { + LocalPurity::Purity(Purity::Logic { prophetic }) + } + + fn ghost() -> Self { + LocalPurity::Purity(Purity::Ghost) + } + + fn is_logic(self) -> bool { + matches!(self, LocalPurity::Purity(Purity::Logic { .. })) + } + + fn is_program(self) -> bool { + use LocalPurity::*; + matches!(self, Purity(self::Purity::Program { .. }) | TrustedTerminates | TrustedGhost) + } + + fn as_str(self) -> &'static str { + use LocalPurity::*; + match self { + Purity(purity) => purity.as_str(), + TrustedTerminates => "program (terminates)", + TrustedGhost => "program (ghost)", + } + } +} + +impl Purity { fn as_str(&self) -> &'static str { + use Purity::*; match self { - Purity::Ghost => "ghost", - Purity::Program { terminates, ghost } => match (*terminates, *ghost) { - (_, true) => "program (ghost)", - (true, false) => "program (terminates)", - (false, false) => "program", + Ghost => "ghost", + Program { purity } => match purity { + ProgramPurity::Ghost => "program (ghost)", + ProgramPurity::Terminates => "program (terminates)", + ProgramPurity::Impure => "program", }, - Purity::Logic { prophetic: false } => "logic", - Purity::Logic { prophetic: true } => "prophetic logic", + Logic { prophetic: false } => "logic", + Logic { prophetic: true } => "prophetic logic", } } } @@ -84,25 +123,34 @@ pub(crate) fn validate_purity<'tcx>( ) { // Only start traversing from top-level definitions. Closures will be visited during the traversal // of their parents so that they can inherit the context from their parent. - if ctx.tcx.is_closure_like(def_id) || is_check_ghost_trusted(ctx.tcx, def_id) { + if ctx.tcx.is_closure_like(def_id) { + return; + } + let is_trusted_ghost = is_trusted_ghost(ctx.tcx, def_id); + let is_trusted_terminates = is_trusted_ghost || is_trusted_terminates(ctx.tcx, def_id); + if is_trusted_terminates && (is_logic(ctx.tcx, def_id) || is_spec(ctx.tcx, def_id)) { + ctx.error( + ctx.def_span(def_id), + if is_trusted_ghost { + "Logic functions can't be `#[trusted(ghost)]`" + } else { + "Logic functions can't be `#[trusted(terminates)]`" + }, + ) + .emit(); return; } - let is_trusted = is_trusted(ctx.tcx, def_id); let typing_env = ctx.typing_env(def_id); - PurityVisitor { ctx, thir, context: Purity::of_def_id(ctx, def_id), typing_env, is_trusted } + PurityVisitor { ctx, thir, context: LocalPurity::of_def_id(ctx, def_id), typing_env } .visit_expr(&thir[expr]); } struct PurityVisitor<'a, 'tcx> { ctx: &'a TranslationCtx<'tcx>, thir: &'a Thir<'tcx>, - context: Purity, + context: LocalPurity, /// Typing environment of the caller function typing_env: TypingEnv<'tcx>, - /// The caller function is `#[trusted]`. - /// - /// This mean we should only check `logic`/program calls, NOT the `check(...)`. - is_trusted: bool, } enum ClosureKind { @@ -121,11 +169,12 @@ impl PurityVisitor<'_, '_> { { Purity::Ghost } else { - let contract = &self.ctx.sig(func_did).contract; - let is_ghost = self.implements_fn_ghost(func_did, args); - let terminates = contract.check_terminates || is_ghost; - let ghost = contract.check_ghost || is_ghost; - Purity::Program { terminates, ghost } + let purity = if self.implements_fn_ghost(func_did, args) { + ProgramPurity::Ghost + } else { + self.ctx.sig(func_did).contract.purity + }; + Purity::Program { purity } } } @@ -172,7 +221,7 @@ impl PurityVisitor<'_, '_> { fn validate_spec_purity(&mut self, closure_id: LocalDefId, prophetic: bool) { let (thir, expr) = self.ctx.thir_body(closure_id); let thir = &thir.borrow(); - PurityVisitor { thir, context: Purity::Logic { prophetic }, ..*self } + PurityVisitor { thir, context: LocalPurity::logic(prophetic), ..*self } .visit_expr(&thir[expr]); } @@ -220,7 +269,7 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { .unwrap(); let fn_purity = self.purity(func_did, args); - if matches!(self.context, Purity::Logic { .. }) + if self.context.is_logic() && ( // These methods are allowed to cheat the purity restrictions self.ctx.is_diagnostic_item(sym::box_new, func_did) @@ -230,11 +279,9 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { ) ) { - } else if !self.context.can_call(fn_purity, self.is_trusted) { + } else if !self.context.can_call(fn_purity) { // Emit a nicer error specifically for calls of ghost functions. - if fn_purity == Purity::Ghost - && matches!(self.context, Purity::Program { .. }) - { + if fn_purity == Purity::Ghost && self.context.is_program() { match self.ctx.intrinsic(func_did) { Intrinsic::GhostIntoInner => self .error(expr.span, "trying to access the contents of a ghost variable in program context").emit(), @@ -263,13 +310,17 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { }; } else { let (caller, callee) = match (self.context, fn_purity) { - (Purity::Program { .. } | Purity::Ghost, Purity::Logic { .. }) => { - ("program", "logic") - } - (Purity::Ghost, Purity::Program { .. }) => ("ghost", "non-ghost"), - (Purity::Logic { .. }, Purity::Program { .. } | Purity::Ghost) => { - ("logic", "program") + ( + LocalPurity::Purity(Purity::Program { .. } | Purity::Ghost), + Purity::Logic { .. }, + ) => ("program", "logic"), + (LocalPurity::Purity(Purity::Ghost), Purity::Program { .. }) => { + ("ghost", "non-ghost") } + ( + LocalPurity::Purity(Purity::Logic { .. }), + Purity::Program { .. } | Purity::Ghost, + ) => ("logic", "program"), _ => (self.context.as_str(), fn_purity.as_str()), }; let msg = format!( @@ -292,7 +343,7 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { self.validate_spec_purity(closure_id, false); return; } - } else if matches!(self.context, Purity::Logic { .. }) { + } else if self.context.is_logic() { // TODO Add a "code" back in self.ctx.dcx().span_fatal(expr.span, "non function call in logical context") } @@ -310,7 +361,7 @@ impl<'a, 'tcx> Visitor<'a, 'tcx> for PurityVisitor<'a, 'tcx> { } ExprKind::Scope { region_scope: _, hir_id, value: _ } => { if super::is_ghost_block(self.ctx.tcx, hir_id) { - let old_context = std::mem::replace(&mut self.context, Purity::Ghost); + let old_context = std::mem::replace(&mut self.context, LocalPurity::ghost()); thir::visit::walk_expr(self, expr); self.context = old_context; return; diff --git a/creusot/src/validate/terminates.rs b/creusot/src/validate/terminates.rs index 951cda72cb..92a2c10fdc 100644 --- a/creusot/src/validate/terminates.rs +++ b/creusot/src/validate/terminates.rs @@ -38,6 +38,7 @@ use crate::{ backend::is_trusted_item, contracts_items::{ has_variant_clause, is_logic, is_loop_variant, is_no_translate, is_pearlite, + is_trusted_ghost, is_trusted_terminates, }, ctx::{HasTyCtxt as _, TranslationCtx}, translation::{ @@ -45,31 +46,30 @@ use crate::{ Ident, PIdent, Pattern, Scoped, Term, TermKind, visit::{TermVisitor, super_visit_term}, }, - traits::{ImplSource_, TraitResolved}, + traits::{ImplSelection, ImplSource_, TraitResolved, select_trait_impl}, }, util::erased_identity_for_item, }; use indexmap::{IndexMap, IndexSet}; -use petgraph::{ - algo::tarjan_scc, - graph, - visit::{Control, DfsEvent, EdgeRef as _, depth_first_search}, -}; +use petgraph::{algo::tarjan_scc, graph}; use rustc_hir::{ def::DefKind, - def_id::{DefId, LocalDefId}, + def_id::{CRATE_DEF_ID, DefId, LocalDefId}, }; use rustc_index::bit_set::DenseBitSet; -use rustc_infer::infer::TyCtxtInferExt as _; +use rustc_infer::{infer::TyCtxtInferExt as _, traits::ImplSource}; use rustc_middle::{ thir::{self, visit::Visitor}, ty::{ - Clauses, EarlyBinder, FnDef, GenericArgs, GenericArgsRef, ParamEnv, TypingEnv, TypingMode, + self, Clauses, EarlyBinder, FnDef, GenericArgs, GenericArgsRef, ParamEnv, TyCtxt, + TypingEnv, TypingMode, }, }; use rustc_span::Span; -use rustc_trait_selection::traits::{specialization_graph, translate_args}; -use std::{collections::HashMap, iter::repeat}; +use rustc_trait_selection::traits::{ + normalize_param_env_or_error, specialization_graph, translate_args, +}; +use std::collections::{HashMap, HashSet}; pub(crate) type RecursiveCalls = IndexMap>; @@ -86,15 +86,13 @@ pub(crate) type RecursiveCalls = IndexMap>; /// which the variant should have decreased. #[must_use] pub(crate) fn validate_terminates(ctx: &TranslationCtx) -> RecursiveCalls { - let mut recursive_calls = RecursiveCalls::new(); - // Check for ghost loops for local_id in ctx.hir_body_owners() { let def_id = local_id.to_def_id(); - if is_no_translate(ctx.tcx, def_id) { - continue; - } - if !is_logic(ctx.tcx, def_id) && is_trusted_item(ctx.tcx, def_id) { + if is_no_translate(ctx.tcx, def_id) + || !is_logic(ctx.tcx, def_id) && is_trusted_item(ctx.tcx, def_id) + || is_trusted_terminates(ctx.tcx, def_id) + { continue; } let (thir, expr) = ctx.thir_body(local_id); @@ -105,33 +103,36 @@ pub(crate) fn validate_terminates(ctx: &TranslationCtx) -> RecursiveCalls { let CallGraph { graph: mut call_graph } = CallGraph::build(ctx); + let mut recursive_calls = RecursiveCalls::new(); + // Detect simple recursion for fun_index in call_graph.node_indices() { let def_id = call_graph.node_weight(fun_index).unwrap().def_id(); - if let Some(self_edge) = call_graph.edges_connecting(fun_index, fun_index).next() { - assert!(def_id.is_local()); - let (self_edge, call) = (self_edge.id(), *self_edge.weight()); - let CallKind::Direct(span) = call else { continue }; - call_graph.remove_edge(self_edge); - if has_variant_clause(ctx.tcx, def_id) { - recursive_calls.entry(def_id).or_default().insert(def_id); - continue; - } - let pearlite = is_pearlite(ctx.tcx, def_id); - if pearlite && is_structurally_recursive(ctx, def_id) { - // Termination is guaranteed, we can forget that this function is recursive. - continue; - } - let fun_span = ctx.def_span(def_id); - let msg = if pearlite { - "Recursive logic function without a #[variant] clause or a structurally decreasing argument" - } else { - "Recursive program function without a `#[variant]` clause" - }; - let mut error = ctx.error(fun_span, msg); - error.span_note(span, "Recursive call happens here"); - error.emit(); + let Some(self_edge) = call_graph.find_edge(fun_index, fun_index) else { + continue; }; + assert!(def_id.is_local()); + let call = call_graph[self_edge]; + let CallKind::Direct(span) = call else { continue }; + call_graph.remove_edge(self_edge); + if has_variant_clause(ctx.tcx, def_id) { + recursive_calls.entry(def_id).or_default().insert(def_id); + continue; + } + let pearlite = is_pearlite(ctx.tcx, def_id); + if pearlite && is_structurally_recursive(ctx, def_id) { + // Termination is guaranteed, we can forget that this function is recursive. + continue; + } + let fun_span = ctx.def_span(def_id); + let msg = if pearlite { + "Recursive logic function without a #[variant] clause or a structurally decreasing argument" + } else { + "Recursive program function without a `#[variant]` clause" + }; + let mut error = ctx.error(fun_span, msg); + error.span_note(span, "Recursive call happens here"); + error.emit(); } // detect mutual recursion @@ -155,23 +156,9 @@ pub(crate) fn validate_terminates(ctx: &TranslationCtx) -> RecursiveCalls { // Need more than 2 components. continue; } - let in_cycle: IndexSet<_> = cycle.into_iter().collect(); - let mut cycle = Vec::new(); - // Build the cycle in the right order. - depth_first_search(&call_graph, [root], |n| match n { - DfsEvent::Discover(n, _) => { - if in_cycle.contains(&n) { - cycle.push(n); - Control::Continue - } else { - Control::Prune - } - } - DfsEvent::BackEdge(_, n) if n == root => Control::Break(()), - _ => Control::Continue, - }); - - let root_def_id = call_graph.node_weight(root).unwrap().def_id(); + let in_cycle: HashSet<_> = cycle.into_iter().collect(); + let cycle = find_path(&call_graph, &in_cycle, root, root); + let root_def_id = call_graph[root].def_id(); let mut error = ctx.error( ctx.def_span(root_def_id), format!( @@ -181,30 +168,38 @@ pub(crate) fn validate_terminates(ctx: &TranslationCtx) -> RecursiveCalls { ); let mut next_node = root; let mut current_node; - assert!(cycle[0] == root); - for (&node, last) in cycle.iter().skip(1).zip(repeat(false)).chain([(&root, true)]) { + for (index, &node) in cycle.iter().enumerate() { current_node = next_node; next_node = node; - if let Some(e) = call_graph.edges_connecting(current_node, next_node).next() { - let call = *e.weight(); - let adverb = if last && cycle.len() > 1 { "finally" } else { "then" }; - let punct = if last { "." } else { "..." }; - let f1 = ctx.def_path_str(call_graph.node_weight(current_node).unwrap().def_id()); - let f2 = ctx.def_path_str(call_graph.node_weight(next_node).unwrap().def_id()); - - match call { - CallKind::Direct(span) => { - error.span_note(span, format!("{adverb} `{f1}` calls `{f2}`{punct}")); - } - CallKind::GenericBound(indirect_id, span) => { - let f3 = ctx.def_path_str(indirect_id); - error.span_note( - span, - format!( - "{adverb} `{f1}` might call `{f2}` via the call to `{f3}`{punct}" - ), - ); - } + let last = index == cycle.len() - 1; + let Some(e) = call_graph.find_edge(current_node, next_node) else { + continue; + }; + let call = call_graph[e]; + let adverb = if last && cycle.len() > 1 { "finally" } else { "then" }; + let punct = if last { "." } else { "..." }; + let f1 = ctx.def_path_str(call_graph[current_node].def_id()); + let next_node = call_graph[next_node].def_id(); + let f2 = ctx.def_path_str(next_node); + + match call { + CallKind::Direct(span) => { + error.span_note(span, format!("{adverb} `{f1}` calls `{f2}`{punct}")); + } + CallKind::GenericBound(indirect_id, span) => { + let f3 = ctx.def_path_str(indirect_id); + error.span_note( + span, + format!( + "{adverb} `{f1}` uses the impl `{f2}` via the call to `{f3}`{punct}" + ), + ); + } + CallKind::ImplMember => { + error.span_note( + ctx.def_span(next_node), + format!("{adverb} the method `{f2}` might be called"), + ); } } } @@ -230,9 +225,15 @@ struct BuildFunctionsGraph<'tcx> { } #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] -enum GraphNode { +struct GraphNode { + def_id: DefId, + kind: GraphNodeKind, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +enum GraphNodeKind { /// A normal function. - Function(DefId), + Function, /// This node is used in the following case: /// ``` /// # macro_rules! ignore { ($($t:tt)*) => {}; } @@ -254,19 +255,29 @@ enum GraphNode { /// Then we feel this is justified to do this transformation, precisely because the /// default function is transparent at the point of the impl, so the user can 'see' /// its definition. + /// + /// The `def_id` in the `GraphNode` will be the default implementation selected for the impl block. ImplDefaultTransparent { - /// The default implementation selected for the impl block. - item_id: DefId, impl_id: LocalDefId, }, + Impl, } impl GraphNode { fn def_id(&self) -> DefId { - match self { - GraphNode::Function(def_id) => *def_id, - GraphNode::ImplDefaultTransparent { item_id, .. } => *item_id, - } + self.def_id + } + + fn function(def_id: DefId) -> Self { + Self { def_id, kind: GraphNodeKind::Function } + } + + fn impl_default(def_id: DefId, impl_id: LocalDefId) -> Self { + Self { def_id, kind: GraphNodeKind::ImplDefaultTransparent { impl_id: impl_id } } + } + + fn impl_(def_id: DefId) -> Self { + Self { def_id, kind: GraphNodeKind::Impl } } } @@ -283,11 +294,13 @@ enum CallKind { /// /// The `DefId` is the one for the generic function, here `f`. GenericBound(DefId, Span), + /// Edge from an impl block to its member + ImplMember, } impl<'tcx> BuildFunctionsGraph<'tcx> { /// Insert a new node in the graph, or fetch an existing node id. - fn insert_function(&mut self, graph_node: GraphNode) -> graph::NodeIndex { + fn insert_node(&mut self, graph_node: GraphNode) -> graph::NodeIndex { *self .graph_node_to_index .entry(graph_node) @@ -327,46 +340,23 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { .skip_normalization() } else { let subst_r; - (called_id, subst_r) = res.to_opt(called_id, subst).unwrap(); - called_node = self.insert_function(GraphNode::Function(called_id)); + // Note: we may get `NoInstance` here because termination checking of trait methods happens in a modified context (see `CallGraph::build`) + (called_id, subst_r) = if let TraitResolved::Instance { def, .. } = res { + def + } else { + (called_id, subst) + }; + called_node = self.insert_node(GraphNode::function(called_id)); bounds = EarlyBinder::bind(ctx.param_env(called_id).caller_bounds()) .instantiate(ctx.tcx, subst_r) .skip_normalization() } self.graph.update_edge(node, called_node, CallKind::Direct(call_span)); - - // Iterate over the trait bounds of the called function, and assume we call all functions - // of the corresponding trait if they are specialized. - for bound in bounds { - // WARNING: `bound`` is not normalized (but we don't seem to use the fact that it should be) - let Some(clause) = bound.as_trait_clause() else { continue }; - let trait_ref = ctx.instantiate_bound_regions_with_erased(clause).trait_ref; - if !matches!(ctx.def_kind(trait_ref.def_id), DefKind::Trait) { - // Some bounds can be trait aliases and we skip them. - // The implied bounds should already appear separately. - continue; - } - // FIXME: this only handle the primary goal of the proof tree. We need to handle all the instances - // used by this trait solving, including those that are used indirectly. - for &item in ctx.associated_item_def_ids(trait_ref.def_id) { - if !matches!(ctx.def_kind(item), DefKind::AssocFn) { - continue; - } - let TraitResolved::Instance { def: (item_id, _), impl_ } = - TraitResolved::resolve_item(ctx.tcx, typing_env, item, trait_ref.args) - else { - continue; - }; - if matches!(impl_, ImplSource_::Param) { - continue; - } - let item_node = self.insert_function(GraphNode::Function(item_id)); - self.graph.update_edge( - node, - item_node, - CallKind::GenericBound(called_id, call_span), - ); - } + // TODO eprintln!("{call_span:?} {bounds:?}"); + for impl_id in proof_tree_nodes(ctx.tcx, typing_env, bounds) { + // TODO eprintln!("{call_span:?} depends on {impl_id:?}"); + let item_node = self.insert_node(GraphNode::impl_(impl_id)); + self.graph.update_edge(node, item_node, CallKind::GenericBound(called_id, call_span)); } } @@ -396,7 +386,7 @@ impl<'tcx> BuildFunctionsGraph<'tcx> { impl_id: LocalDefId, item_id: DefId, ) -> (graph::NodeIndex, Clauses<'tcx>) { - let node = self.insert_function(GraphNode::ImplDefaultTransparent { item_id, impl_id }); + let node = self.insert_node(GraphNode::impl_default(item_id, impl_id)); if let Some(bounds) = self.default_functions_bounds.get(&node) { return (node, bounds); } @@ -460,24 +450,24 @@ impl CallGraph { /// Build the call graph of all functions appearing in the current crate, /// exclusively for the purpose of termination checking. /// - /// In particular, this means it only contains `#[check(terminates)]` functions. + /// In particular, this means it only contains `#[check(terminates)]` or `#[trusted(terminates)]` functions. fn build(ctx: &TranslationCtx) -> Self { + let tcx = ctx.tcx; let mut build_call_graph = BuildFunctionsGraph::default(); for local_id in ctx.hir_body_owners() { let def_id = local_id.to_def_id(); - if is_no_translate(ctx.tcx, def_id) { - // Cut all arcs from this function. - continue; - } - - if !is_logic(ctx.tcx, def_id) && is_trusted_item(ctx.tcx, def_id) { + if is_no_translate(ctx.tcx, def_id) + || !is_logic(ctx.tcx, def_id) && is_trusted_item(ctx.tcx, def_id) + || is_trusted_ghost(ctx.tcx, def_id) + || is_trusted_terminates(ctx.tcx, def_id) + { continue; } let contract = &ctx.sig(def_id).contract; - if !is_pearlite(ctx.tcx, def_id) && !contract.check_terminates { + if !is_pearlite(ctx.tcx, def_id) && !contract.purity.is_terminates() { // Only consider functions marked with `terminates`: we already ensured // that a `terminates` functions only calls other `terminates` functions. if let Some(variant) = &contract.variant { @@ -487,9 +477,15 @@ impl CallGraph { } continue; } - let node = build_call_graph.insert_function(GraphNode::Function(def_id)); + let node = build_call_graph.insert_node(GraphNode::function(def_id)); - let typing_env = ctx.typing_env(def_id); + // For termination checking of trait impl members, `typing_env` should be the one from the trait definition. + // This prevents smuggling recursive constraints within redundant trait bounds. + let typing_env = if let Some(trait_item_id) = tcx.trait_item_of(def_id) { + ctx.typing_env_with(def_id, param_env_for_termination(tcx, trait_item_id, def_id)) + } else { + ctx.typing_env(def_id) + }; let (thir, expr) = ctx.thir_body(local_id); let thir = &thir.borrow(); @@ -509,6 +505,28 @@ impl CallGraph { } } + // Add an edge from every trait impl to its methods. + for (&trait_id, impls) in tcx.all_local_trait_impls(()) { + let trait_def = tcx.trait_def(trait_id); + for &impl_id in impls { + let ancestors = trait_def.ancestors(tcx, impl_id.to_def_id()).unwrap(); + for &item in tcx.associated_item_def_ids(trait_id) { + if let DefKind::AssocFn = tcx.def_kind(item) { + let leaf_def = ancestors.leaf_def(tcx, item).unwrap(); + let impl_node = + build_call_graph.insert_node(GraphNode::impl_(impl_id.to_def_id())); + let item_node = + build_call_graph.insert_node(GraphNode::function(leaf_def.item.def_id)); + build_call_graph.graph.update_edge( + impl_node, + item_node, + CallKind::ImplMember, + ); + } + } + } + } + Self { graph: build_call_graph.graph } } } @@ -772,3 +790,112 @@ fn is_structurally_recursive<'tcx>(ctx: &TranslationCtx<'tcx>, self_id: DefId) - s.valid() } + +fn as_predicates<'tcx>( + tcx: TyCtxt<'tcx>, + clauses: impl IntoIterator>, +) -> impl Iterator> { + clauses.into_iter().filter_map(move |clause| { + // WARNING: `clause` is not normalized (but we don't seem to use the fact that it should be) + let Some(clause) = clause.as_trait_clause() else { return None }; + let ty::PredicatePolarity::Positive = clause.polarity() else { return None }; + let trait_ref = tcx.instantiate_bound_regions_with_erased(clause).trait_ref; + if !matches!(tcx.def_kind(trait_ref.def_id), DefKind::Trait) { + // Some bounds can be trait aliases and we skip them. + // The implied bounds should already appear separately. + return None; + } + Some(trait_ref) + }) +} + +/// Return all the trait impls that appear in the proof trees of `clauses`. +pub(crate) fn proof_tree_nodes<'tcx>( + tcx: TyCtxt<'tcx>, + typing_env: TypingEnv<'tcx>, + clauses: impl IntoIterator>, +) -> Vec { + let mut nodes = Vec::new(); + let mut predicates: Vec<_> = as_predicates(tcx, clauses).collect(); + while let Some(trait_ref) = predicates.pop() { + let ImplSelection::Found(source) = select_trait_impl(tcx, typing_env, trait_ref) else { + continue; + }; + let ImplSource::UserDefined(source) = source else { continue }; + nodes.push(source.impl_def_id); + let bounds = EarlyBinder::bind(tcx.param_env(source.impl_def_id).caller_bounds()) + .instantiate(tcx, source.args) + .skip_normalization(); + predicates.extend(as_predicates(tcx, bounds)); + } + nodes +} + +/// For a method in a trait impl (`impl_item_id`), construct a `ParamEnv` that +/// combines bounds from the parent impl and bounds from the original declaration (`trait_item_id`) +fn param_env_for_termination(tcx: TyCtxt, trait_item_id: DefId, impl_item_id: DefId) -> ParamEnv { + let impl_id = tcx.impl_of_assoc(impl_item_id).unwrap(); + let trait_ref = tcx.impl_trait_ref(impl_id).instantiate_identity().skip_normalization(); + let trait_item_args = GenericArgs::identity_for_item(tcx, trait_item_id); + let args = tcx.mk_args_from_iter( + trait_ref.args.iter().chain(trait_item_args.iter().skip(trait_ref.args.len())), + ); + + // Reverse engineered from `GenericPredicates::instantiate_into` + let predicates = tcx.predicates_of(impl_id).instantiate_identity(tcx).predicates.into_iter(); + let predicates = predicates.chain( + tcx.predicates_of(trait_item_id) + .predicates + .iter() + .map(|(p, _)| EarlyBinder::bind(*p).instantiate(tcx, args)), + ); + let predicates: Vec<_> = predicates.map(|p| p.skip_normalization()).collect(); + let unnormalized_env = ty::ParamEnv::new(tcx.mk_clauses(&predicates)); + + // Code from `param_env` in `rustc_ty_utils/src/ty.rs` + let local_did = impl_item_id.as_local(); + let body_id = local_did.unwrap_or(CRATE_DEF_ID); + let cause = + rustc_trait_selection::traits::ObligationCause::misc(tcx.def_span(impl_item_id), body_id); + // FIXME: We probably should not use this to normalize... + normalize_param_env_or_error(tcx, unnormalized_env, cause) +} + +/// Find path from `src` to `tgt` with at least one edge. +/// Returned path excludes `src` and includes `tgt`. +pub(crate) fn find_path( + graph: &graph::DiGraph, + scc: &HashSet, + src: graph::NodeIndex, + tgt: graph::NodeIndex, +) -> Vec { + let mut path = Vec::new(); + let mut visited = HashSet::new(); + let found = find_path_from(graph, scc, src, tgt, &mut path, &mut visited).is_err(); + assert!(found); + path +} + +/// Find path from src to tgt with at least one edge. +fn find_path_from( + graph: &graph::DiGraph, + scc: &HashSet, + src: graph::NodeIndex, + tgt: graph::NodeIndex, + path: &mut Vec, + visited: &mut HashSet, +) -> Result<(), ()> { + if !scc.contains(&src) || visited.contains(&src) { + return Ok(()); + } + visited.insert(src); + for n in graph.neighbors(src) { + path.push(n); + if n == tgt { + return Err(()); + } + find_path_from(graph, scc, n, tgt, path, visited)?; + path.pop(); + } + Ok(()) +} diff --git a/creusot/src/validate/traits.rs b/creusot/src/validate/traits.rs index 7568f7a4a6..25c1c7ea6c 100644 --- a/creusot/src/validate/traits.rs +++ b/creusot/src/validate/traits.rs @@ -128,7 +128,7 @@ pub(crate) fn validate_impls<'tcx>(ctx: &TranslationCtx<'tcx>) { } else { let item_contract = &ctx.sig(impl_item).contract; let trait_contract = &ctx.sig(trait_item).contract; - if trait_contract.check_ghost && !item_contract.check_ghost { + if trait_contract.purity.is_ghost() && !item_contract.purity.is_ghost() { ctx.error( ctx.def_span(impl_item), format!( @@ -137,7 +137,9 @@ pub(crate) fn validate_impls<'tcx>(ctx: &TranslationCtx<'tcx>) { ), ) .emit(); - } else if trait_contract.check_terminates && !item_contract.check_terminates { + } else if trait_contract.purity.is_terminates() + && !item_contract.purity.is_terminates() + { ctx.error( ctx.def_span(impl_item), format!( diff --git a/tests/should_fail/bug/1565.stderr b/tests/should_fail/bug/1565.stderr index 3e4aae23a8..acdf1fb122 100644 --- a/tests/should_fail/bug/1565.stderr +++ b/tests/should_fail/bug/1565.stderr @@ -4,11 +4,16 @@ error: Mutually recursive functions: when calling `::f`... 11 | fn f(self) -> Int { | ^^^^^^^^^^^^^^^^^ | -note: then `::f` might call `::f` via the call to `g`. +note: then `::f` uses the impl `` via the call to `g`... --> 1565.rs:12:9 | 12 | g() | ^^^ +note: finally the method `::f` might be called + --> 1565.rs:11:5 + | +11 | fn f(self) -> Int { + | ^^^^^^^^^^^^^^^^^ error: aborting due to 1 previous error diff --git a/tests/should_fail/bug/459.stderr b/tests/should_fail/bug/459.stderr index 8345438bfb..e685d6e32f 100644 --- a/tests/should_fail/bug/459.stderr +++ b/tests/should_fail/bug/459.stderr @@ -4,11 +4,16 @@ error: Mutually recursive functions: when calling ` Self::DeepModelTy { | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | -note: then `::deep_model` might call `::deep_model` via the call to `creusot_std::std::boxed::>::deep_model`. +note: then `::deep_model` uses the impl `` via the call to `creusot_std::std::boxed::>::deep_model`... --> 459.rs:14:28 | 14 | A::Cons(a) => *a.deep_model() + 1, | ^^^^^^^^^^^^^^ +note: finally the method `::deep_model` might be called + --> 459.rs:12:5 + | +12 | fn deep_model(self) -> Self::DeepModelTy { + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: aborting due to 1 previous error diff --git a/tests/should_fail/terminates/complicated_traits_recursion.stderr b/tests/should_fail/terminates/complicated_traits_recursion.stderr index 7c53ccb0bf..c15046f6d8 100644 --- a/tests/should_fail/terminates/complicated_traits_recursion.stderr +++ b/tests/should_fail/terminates/complicated_traits_recursion.stderr @@ -4,11 +4,16 @@ error: Mutually recursive functions: when calling `::foo`... 12 | fn foo() { | ^^^^^^^^ | -note: then `::foo` might call `::foo` via the call to `bar`. +note: then `::foo` uses the impl `` via the call to `bar`... --> complicated_traits_recursion.rs:13:9 | 13 | bar::>(std::iter::once(1i32)); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +note: finally the method `::foo` might be called + --> complicated_traits_recursion.rs:12:5 + | +12 | fn foo() { + | ^^^^^^^^ error: aborting due to 1 previous error diff --git a/tests/should_fail/terminates/default_function_non_logic.stderr b/tests/should_fail/terminates/default_function_non_logic.stderr index ea1dc75740..4f400083a5 100644 --- a/tests/should_fail/terminates/default_function_non_logic.stderr +++ b/tests/should_fail/terminates/default_function_non_logic.stderr @@ -4,11 +4,16 @@ error: Mutually recursive functions: when calling `::g`... 13 | fn g() { | ^^^^^^ | -note: then `::g` might call `::g` via the call to `Foo::f`. +note: then `::g` uses the impl `` via the call to `Foo::f`... --> default_function_non_logic.rs:14:9 | 14 | Self::f(); // this assumes f could call g | ^^^^^^^^^ +note: finally the method `::g` might be called + --> default_function_non_logic.rs:13:5 + | +13 | fn g() { + | ^^^^^^ error: aborting due to 1 previous error diff --git a/tests/should_fail/terminates/default_function_non_open.stderr b/tests/should_fail/terminates/default_function_non_open.stderr index fe476da094..2ebf86e21f 100644 --- a/tests/should_fail/terminates/default_function_non_open.stderr +++ b/tests/should_fail/terminates/default_function_non_open.stderr @@ -4,11 +4,16 @@ error: Mutually recursive functions: when calling `::g` 16 | fn g() { | ^^^^^^ | -note: then `::g` might call `::g` via the call to `inner::Foo::f`. +note: then `::g` uses the impl `` via the call to `inner::Foo::f`... --> default_function_non_open.rs:17:9 | 17 | Self::f(); // this assumes f could call g | ^^^^^^^^^ +note: finally the method `::g` might be called + --> default_function_non_open.rs:16:5 + | +16 | fn g() { + | ^^^^^^ error: aborting due to 1 previous error From 805ecc8eaf9ac6eb82add14df5b06b5a1ad1766f Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Thu, 26 Mar 2026 10:56:23 +0100 Subject: [PATCH 3/4] Add recursive type check --- creusot-std-proc/Cargo.toml | 2 +- creusot-std-proc/src/creusot.rs | 10 +- creusot-std-proc/src/creusot/extern_spec.rs | 119 +++- creusot-std/src/cell/permcell.rs | 3 +- creusot-std/src/cell/predcell.rs | 1 + creusot-std/src/logic/mapping.rs | 1 + creusot-std/src/std/rc.rs | 3 + creusot/src/contracts_items/attributes.rs | 24 + creusot/src/ctx.rs | 70 ++- creusot/src/metadata.rs | 31 +- creusot/src/translation.rs | 3 +- creusot/src/translation/external.rs | 62 ++- creusot/src/validate.rs | 7 +- creusot/src/validate/recursive_types.rs | 515 ++++++++++++++++++ .../recursive_types/abstract_types.rs | 9 + .../recursive_types/abstract_types.stderr | 8 + tests/should_fail/recursive_types/impl_arg.rs | 22 + .../recursive_types/impl_arg.stderr | 14 + .../recursive_types/nonpositive.rs | 14 + .../recursive_types/nonpositive.stderr | 8 + .../should_fail/recursive_types/via_impls.rs | 21 + .../recursive_types/via_impls.stderr | 19 + tests/should_fail/terminates/trait_impl.rs | 35 ++ .../should_fail/terminates/trait_impl.stderr | 19 + .../terminates/trait_impl_where.rs | 31 ++ .../terminates/trait_impl_where.stderr | 23 + tests/should_fail/terminates/trait_where.rs | 29 + .../should_fail/terminates/trait_where.stderr | 14 + .../terminates/trait_where_supertrait.rs | 31 ++ .../terminates/trait_where_supertrait.stderr | 19 + .../bug/unnormalized_projection.coma | 5 +- .../bug/unnormalized_projection.rs | 2 +- .../should_succeed/specification/trusted.coma | 252 +++++++++ tests/should_succeed/specification/trusted.rs | 27 + .../specification/trusted/proof.json | 24 +- 35 files changed, 1424 insertions(+), 53 deletions(-) create mode 100644 creusot/src/validate/recursive_types.rs create mode 100644 tests/should_fail/recursive_types/abstract_types.rs create mode 100644 tests/should_fail/recursive_types/abstract_types.stderr create mode 100644 tests/should_fail/recursive_types/impl_arg.rs create mode 100644 tests/should_fail/recursive_types/impl_arg.stderr create mode 100644 tests/should_fail/recursive_types/nonpositive.rs create mode 100644 tests/should_fail/recursive_types/nonpositive.stderr create mode 100644 tests/should_fail/recursive_types/via_impls.rs create mode 100644 tests/should_fail/recursive_types/via_impls.stderr create mode 100644 tests/should_fail/terminates/trait_impl.rs create mode 100644 tests/should_fail/terminates/trait_impl.stderr create mode 100644 tests/should_fail/terminates/trait_impl_where.rs create mode 100644 tests/should_fail/terminates/trait_impl_where.stderr create mode 100644 tests/should_fail/terminates/trait_where.rs create mode 100644 tests/should_fail/terminates/trait_where.stderr create mode 100644 tests/should_fail/terminates/trait_where_supertrait.rs create mode 100644 tests/should_fail/terminates/trait_where_supertrait.stderr diff --git a/creusot-std-proc/Cargo.toml b/creusot-std-proc/Cargo.toml index a5da095c00..bfed930fc9 100644 --- a/creusot-std-proc/Cargo.toml +++ b/creusot-std-proc/Cargo.toml @@ -28,7 +28,7 @@ creusot = ["dep:uuid", "dep:pearlite-syn", "proc-macro2/span-locations"] quote = "1.0" uuid = { version = "1.12", features = ["v4"], optional = true } pearlite-syn = { version = "0.12.0-dev", path = "../pearlite-syn", features = ["full"], optional = true } -syn = { version = "2.0", features = ["full", "visit", "visit-mut"] } +syn = { version = "2.0", features = ["parsing", "full", "visit", "visit-mut"] } proc-macro2 = { version = "1.0" } [lints.rust] diff --git a/creusot-std-proc/src/creusot.rs b/creusot-std-proc/src/creusot.rs index 827acd357c..8ccf034722 100644 --- a/creusot-std-proc/src/creusot.rs +++ b/creusot-std-proc/src/creusot.rs @@ -68,6 +68,8 @@ enum TrustedArg { Ghost, /// #[trusted(terminates)] Terminates, + /// #[trusted(positive(T, U))] + Positive(Punctuated), } impl Parse for TrustedArg { @@ -78,10 +80,15 @@ impl Parse for TrustedArg { Ok(Ghost) } else if ident == "terminates" { Ok(Terminates) + } else if ident == "positive" { + let content; + syn::parenthesized!(content in src); + let params = Punctuated::::parse_separated_nonempty(&content)?; + Ok(Positive(params)) } else { Err(Error::new( ident.span(), - "Unexpected `#[trusted]` argument: expected `terminates` or nothing", + "Unexpected `#[trusted]` argument: expected `terminates`, `positive(PARAM)`, or nothing", )) } } @@ -93,6 +100,7 @@ impl quote::ToTokens for TrustedArg { stream.append_all(match self { Ghost => quote! { #[creusot::decl::trusted_ghost] }, Terminates => quote! { #[creusot::decl::trusted_terminates] }, + Positive(params) => quote! { #[creusot::decl::trusted_positive(#params)] }, }) } } diff --git a/creusot-std-proc/src/creusot/extern_spec.rs b/creusot-std-proc/src/creusot/extern_spec.rs index a8837d4aa5..4de03427bb 100644 --- a/creusot-std-proc/src/creusot/extern_spec.rs +++ b/creusot-std-proc/src/creusot/extern_spec.rs @@ -17,24 +17,35 @@ use syn::{ /// The `extern_spec!` macro. pub fn extern_spec(tokens: TS1) -> TS1 { let externs: ExternSpecs = parse_macro_input!(tokens); + match extern_spec_(externs) { + Ok(specs) => TS1::from(quote! { #(#specs)* }), + Err(err) => err.to_compile_error().into(), + } +} +fn extern_spec_(externs: ExternSpecs) -> Result> { let mut specs = Vec::new(); - let externs = match externs.flatten() { - Ok(externs) => externs, - Err(err) => return TS1::from(err.to_compile_error()), - }; - - for spec in externs { - specs.push(spec.into_tokens()); + for item in externs.0 { + match item { + ExternSpecItem::Fun(f) => { + for spec in f.flatten()? { + specs.push(spec.into_tokens()) + } + } + ExternSpecItem::Type(ty) => specs.push(ty.to_token_stream()), + } } - - TS1::from(quote! { - #(#specs)* - }) + Ok(specs) } #[derive(Debug)] -struct ExternSpecs(Vec); +struct ExternSpecs(Vec); + +#[derive(Debug)] +enum ExternSpecItem { + Fun(ExternSpec), + Type(ExternType), +} /// An extern spec is either: /// - A module of extern specs @@ -116,23 +127,20 @@ struct FlatSpec { body: Option, } -impl ExternSpecs { +impl ExternSpec { fn flatten(self) -> Result> { let mut specs = Vec::new(); - - for spec in self.0 { - flatten( - spec, - ExprPath { - attrs: Vec::new(), - qself: None, - path: Path { leading_colon: None, segments: Punctuated::new() }, - }, - DocItemName(String::from("extern_spec")), - None, - &mut specs, - )? - } + flatten( + self, + ExprPath { + attrs: Vec::new(), + qself: None, + path: Path { leading_colon: None, segments: Punctuated::new() }, + }, + DocItemName(String::from("extern_spec")), + None, + &mut specs, + )?; Ok(specs) } } @@ -778,6 +786,25 @@ impl Parse for ExternSpecs { } } +impl Parse for ExternSpecItem { + fn parse(input: parse::ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + + let lookahead = input.lookahead1(); + if lookahead.peek(Token![type]) { + let mut ty = input.call(ExternType::parse)?; + ty.attrs = attrs; + Ok(ExternSpecItem::Type(ty)) + } else { + let mut e = input.call(ExternSpec::parse)?; + if let ExternSpec::Fn(ref mut f) = e { + f.attrs = attrs + } + Ok(ExternSpecItem::Fun(e)) + } + } +} + impl Parse for ExternSpec { fn parse(input: parse::ParseStream) -> Result { let attrs = input.call(Attribute::parse_outer)?; @@ -793,7 +820,7 @@ impl Parse for ExternSpec { || (lookahead.peek(Token![unsafe]) && input.peek2(Token![fn])) { let mut f: ExternMethod = input.parse()?; - f.attrs.extend(attrs); + f.attrs = attrs; Ok(ExternSpec::Fn(f)) } else { Err(lookahead.error()) @@ -963,3 +990,39 @@ impl Parse for ExternMethod { Ok(ExternMethod { span, attrs, sig, body }) } } + +#[derive(Debug)] +struct ExternType { + attrs: Vec, + path: Path, +} + +impl Parse for ExternType { + fn parse(input: parse::ParseStream) -> Result { + let attrs = input.call(Attribute::parse_outer)?; + input.parse::()?; + let path = input.parse()?; + input.parse::()?; + Ok(Self { attrs, path }) + } +} + +impl ToTokens for ExternType { + fn to_tokens(&self, tokens: &mut TokenStream) { + let span = self.path.span(); + let ident = crate::creusot::generate_unique_ident("extern_type", span); + let attrs = &self.attrs; + let path = &self.path; + let generics = match self.path.segments.last().unwrap().arguments { + syn::PathArguments::AngleBracketed(ref generics) => Some(generics), + _ => None, + }; + tokens.extend(quote_spanned! { span=> + #[allow(dead_code, non_camel_case_types)] + #[creusot::extern_type] + #[doc(hidden)] + #(#attrs)* + struct #ident #generics (#path); + }) + } +} diff --git a/creusot-std/src/cell/permcell.rs b/creusot-std/src/cell/permcell.rs index 592f622bd4..4a2cb0747e 100644 --- a/creusot-std/src/cell/permcell.rs +++ b/creusot-std/src/cell/permcell.rs @@ -22,8 +22,9 @@ use alloc::boxed::Box; /// Creusot ensures that every operation on the inner value uses the right [`Perm`] object /// created by [`PermCell::new`], ensuring safety in a manner similar to /// [ghost_cell](https://docs.rs/ghost-cell/latest/ghost_cell/). -#[repr(transparent)] +#[trusted(positive(T))] #[opaque] +#[repr(transparent)] pub struct PermCell(UnsafeCell); impl Container for PermCell { diff --git a/creusot-std/src/cell/predcell.rs b/creusot-std/src/cell/predcell.rs index 84201c1787..59a4a20712 100644 --- a/creusot-std/src/cell/predcell.rs +++ b/creusot-std/src/cell/predcell.rs @@ -7,6 +7,7 @@ use crate::{logic::Mapping, prelude::*}; /// Cell over predicates /// /// A wrapper around `std::cell::Cell` that allows predicates to be used to specify the contents of the cell. +#[trusted(positive(T))] #[opaque] #[repr(transparent)] pub struct PredCell(core::cell::Cell); diff --git a/creusot-std/src/logic/mapping.rs b/creusot-std/src/logic/mapping.rs index 685a6ea8de..e18c9636a5 100644 --- a/creusot-std/src/logic/mapping.rs +++ b/creusot-std/src/logic/mapping.rs @@ -17,6 +17,7 @@ use core::marker::PhantomData; /// proof_assert!(map.get(1) == 4); /// ``` #[builtin("map.Map.map")] +#[trusted(positive(B))] pub struct Mapping(PhantomData B>); impl Mapping { diff --git a/creusot-std/src/std/rc.rs b/creusot-std/src/std/rc.rs index c58cad731c..7fdcfb3772 100644 --- a/creusot-std/src/std/rc.rs +++ b/creusot-std/src/std/rc.rs @@ -47,6 +47,9 @@ impl View for Rc { } extern_spec! { + #[trusted(positive(T))] + type Rc; + impl Rc { #[check(ghost)] #[ensures(*result@ == value)] diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs index 192dd49734..ff5c6dd67a 100644 --- a/creusot/src/contracts_items/attributes.rs +++ b/creusot/src/contracts_items/attributes.rs @@ -69,6 +69,7 @@ attribute_functions! { [creusot::decl::new_namespace] => is_new_namespace [creusot::decl::open_inv_result] => is_open_inv_result [creusot::extern_spec] => is_extern_spec + [creusot::extern_type] => is_extern_type [creusot::trusted_trivial_if_param_trivial] => is_trivial_if_param_trivial [creusot::clause::variant] => has_variant_clause [creusot::clause::check_terminates] => is_check_terminates @@ -273,6 +274,29 @@ pub(crate) fn is_open_inv_param(tcx: TyCtxt, p: &Param) -> bool { found } +pub(crate) fn get_trusted_positive(tcx: TyCtxt, def_id: DefId) -> Option> { + let attr = get_attrs(tcx, def_id, &["creusot", "decl", "trusted_positive"]).pop()?; + let Attribute::Unparsed(attr) = attr else { unreachable!() }; + match &attr.args { + AttrArgs::Delimited(args) => Some(parse_trusted_positive(&args.tokens)), + _ => tcx.crash_and_error(tcx.def_span(def_id), "Bad #[trusted_positive] attribute"), + } +} + +fn parse_trusted_positive(tokens: &TokenStream) -> Vec { + let mut params = Vec::new(); + for token in tokens.iter() { + let TokenTree::Token(token, _) = token else { + continue; + }; + let TokenKind::Ident(sym, _) = token.kind else { + continue; + }; + params.push(sym) + } + params +} + fn get_attrs<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, path: &[&str]) -> Vec<&'tcx Attribute> { let path = path.into_iter().map(|s| Symbol::intern(s)).collect::>(); tcx.get_attrs_by_path(def_id, &path).collect::>() diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index f5c5e1f398..2e8cf30248 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -2,16 +2,17 @@ use crate::{ backend::resolve::is_resolve_trivial, callbacks, contracts_items::{ - Intrinsic, gather_intrinsics, get_creusot_item, is_extern_spec, is_logic, is_opaque, - is_open_inv_param, is_prophetic, is_trusted, opacity_witness_name, + Intrinsic, gather_intrinsics, get_creusot_item, is_extern_spec, is_extern_type, is_logic, + is_opaque, is_open_inv_param, is_prophetic, is_trusted, opacity_witness_name, }, metadata::{BinaryMetadata, Metadata, encode_def_ids, get_erasure_required}, naming::{ComaNames, ModulePath, lowercase_prefix}, translation::{ self, external::{ - ExternSpec, extract_erasure_from_child, extract_erasure_from_item, - extract_extern_specs_from_item, + ExternSpec, TrustedPositivity, extract_erasure_from_child, extract_erasure_from_item, + extract_extern_specs_from_item, extract_extern_trusted_positivity, + extract_trusted_positivity, }, fmir, pearlite::{self, Scoped, Term, TermWithTriggers}, @@ -175,6 +176,7 @@ pub struct TranslationCtx<'tcx> { erasure_required: RefCell>, extern_specs: HashMap>, extern_spec_items: HashMap, + trusted_positivity: HashMap, erased_local_defid: HashMap>>, erasures_to_check: IndexSet, coma_names: ComaNames, @@ -266,6 +268,7 @@ impl<'tcx> TranslationCtx<'tcx> { erasure_required: Default::default(), extern_specs: Default::default(), extern_spec_items: Default::default(), + trusted_positivity: Default::default(), erased_local_defid: Default::default(), erasures_to_check: Default::default(), coma_names: ComaNames::new(tcx), @@ -416,6 +419,17 @@ impl<'tcx> TranslationCtx<'tcx> { self.extern_specs.get(&def_id).or_else(|| self.externs.extern_spec(def_id)) } + pub(crate) fn trusted_positivity(&self, def_id: DefId, index: usize) -> bool { + let Some(tp) = self.get_trusted_positivity(def_id) else { + return false; + }; + tp.positivity.contains(index) + } + + pub(crate) fn get_trusted_positivity(&self, def_id: DefId) -> Option<&TrustedPositivity> { + self.trusted_positivity.get(&def_id).or_else(|| self.externs.trusted_positivity(def_id)) + } + pub(crate) fn opacity(&self, item: DefId) -> &Opacity { self.opacity.insert(item, |&item| Box::new(self.mk_opacity(item))) } @@ -487,6 +501,7 @@ impl<'tcx> TranslationCtx<'tcx> { self.creusot_items, self.raw_intrinsics, self.extern_specs, + self.trusted_positivity, self.params_open_inv, erased_thir, self.erased_local_defid, @@ -543,7 +558,13 @@ impl<'tcx> TranslationCtx<'tcx> { } } - pub(crate) fn load_extern_specs(&mut self) { + pub(crate) fn load_specs(&mut self) { + self.load_extern_specs(); + self.load_trusted_positivity(); + self.load_erasures(); + } + + fn load_extern_specs(&mut self) { let mut traits_or_impls = Vec::new(); for def_id in self.tcx.hir_body_owners() { @@ -590,7 +611,44 @@ impl<'tcx> TranslationCtx<'tcx> { } } - pub(crate) fn load_erasures(&mut self) { + fn load_trusted_positivity(&mut self) { + for id in self.tcx.hir_free_items() { + let item = self.tcx.hir_item(id); + let def_id = item.owner_id.to_def_id(); + use rustc_hir::ItemKind::*; + match item.kind { + Struct(..) if is_extern_type(self.tcx, def_id) => { + let (extern_id, tp) = extract_extern_trusted_positivity(self.tcx, def_id); + if self.trusted_positivity.insert(extern_id, tp).is_some() { + self.crash_and_error( + self.def_span(def_id), + format!( + "duplicate extern type specification for {}", + self.def_path_str(extern_id) + ), + ) + } + } + Struct(..) | Enum(..) | Union(..) => { + let Some(tp) = extract_trusted_positivity(self.tcx, def_id) else { + continue; + }; + if self.trusted_positivity.insert(def_id, tp).is_some() { + self.crash_and_error( + self.def_span(def_id), + format!( + "duplicate extern type specification for {}", + self.def_path_str(def_id) + ), + ) + } + } + _ => {} + } + } + } + + fn load_erasures(&mut self) { for def_id in self.tcx.hir_body_owners() { let thir = self.tcx.thir_body(def_id).unwrap_or_else(|err| err.raise_fatal()); let Some((eraser, erasure)) = extract_erasure_from_item(self, def_id, thir) else { diff --git a/creusot/src/metadata.rs b/creusot/src/metadata.rs index 6ee26a3952..77a30fb503 100644 --- a/creusot/src/metadata.rs +++ b/creusot/src/metadata.rs @@ -1,7 +1,7 @@ use crate::{ ctx::Erasure, translation::{ - external::ExternSpec, + external::{ExternSpec, TrustedPositivity}, pearlite::{Scoped, Term, TermWithTriggers}, }, validate::AnfBlock, @@ -23,12 +23,14 @@ use std::{ }; type ExternSpecs<'tcx> = HashMap>; +type ExternTypes<'tcx> = HashMap; // TODO: this should lazily load the metadata. #[derive(Default)] pub struct Metadata<'tcx> { crates: HashMap>, extern_specs: ExternSpecs<'tcx>, + trusted_positivity: ExternTypes<'tcx>, erased_thir: HashMap>, erased_defid: HashMap>>, } @@ -74,6 +76,10 @@ impl<'tcx> Metadata<'tcx> { self.extern_specs.get(&id) } + pub(crate) fn trusted_positivity(&self, id: DefId) -> Option<&TrustedPositivity> { + self.trusted_positivity.get(&id) + } + pub(crate) fn erased_thir(&self, id: DefId) -> Option<&AnfBlock<'tcx>> { self.erased_thir.get(&id) } @@ -92,7 +98,7 @@ impl<'tcx> Metadata<'tcx> { if cnum == LOCAL_CRATE { continue; } - let Some((cmeta, ext_specs, erased_thir, erased_defid)) = + let Some((cmeta, ext_specs, ext_types, erased_thir, erased_defid)) = CrateMetadata::load(tcx, overrides, cnum) else { continue; @@ -103,6 +109,14 @@ impl<'tcx> Metadata<'tcx> { panic!("duplicate external spec found for {:?} while loading {:?}", id, cnum); } } + for (id, spec) in ext_types { + if self.trusted_positivity.insert(id, spec).is_some() { + panic!( + "duplicate extern type spec found for {:?} while loading {:?}", + id, cnum + ); + } + } for (id, erased) in erased_thir { self.erased_thir.insert(id, erased); } @@ -156,6 +170,7 @@ impl<'tcx> CrateMetadata<'tcx> { ) -> Option<( Self, ExternSpecs<'tcx>, + ExternTypes<'tcx>, Vec<(DefId, AnfBlock<'tcx>)>, Vec<(DefId, Option>)>, )> { @@ -171,7 +186,13 @@ impl<'tcx> CrateMetadata<'tcx> { is_external_crate: metadata.is_external_crate, }; - Some((meta, metadata.extern_specs, metadata.erased_thir, metadata.erased_defid)) + Some(( + meta, + metadata.extern_specs, + metadata.trusted_positivity, + metadata.erased_thir, + metadata.erased_defid, + )) } } @@ -186,6 +207,7 @@ pub(crate) struct BinaryMetadata<'tcx> { creusot_items: HashMap, intrinsics: HashMap, extern_specs: HashMap>, + trusted_positivity: HashMap, params_open_inv: HashMap>, erased_thir: Vec<(DefId, AnfBlock<'tcx>)>, erased_defid: Vec<(DefId, Option>)>, @@ -199,6 +221,7 @@ impl<'tcx> BinaryMetadata<'tcx> { creusot_items: HashMap, intrinsics: HashMap, extern_specs: HashMap>, + trusted_positivity: HashMap, params_open_inv: HashMap>, erased_thir: Vec<(DefId, AnfBlock<'tcx>)>, erased_local_defid: HashMap>>, @@ -221,6 +244,7 @@ impl<'tcx> BinaryMetadata<'tcx> { creusot_items, intrinsics, extern_specs, + trusted_positivity, params_open_inv, erased_thir, erased_defid, @@ -235,6 +259,7 @@ impl<'tcx> BinaryMetadata<'tcx> { creusot_items: HashMap::new(), intrinsics: HashMap::new(), extern_specs: HashMap::new(), + trusted_positivity: HashMap::new(), params_open_inv: HashMap::new(), erased_thir, erased_defid: Vec::new(), diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs index 8c1e84e10e..acdb42bb8c 100644 --- a/creusot/src/translation.rs +++ b/creusot/src/translation.rs @@ -56,8 +56,7 @@ pub(crate) fn after_analysis<'tcx>( let start = Instant::now(); silence_unused_features_warnings(tcx); let mut ctx = TranslationCtx::new(tcx, opts.clone(), params_open_inv); - ctx.load_extern_specs(); - ctx.load_erasures(); + ctx.load_specs(); validate(&ctx); debug!("after_analysis_validate: {:?}", start.elapsed()); if let Some(err) = tcx.dcx().has_errors_or_delayed_bugs() { diff --git a/creusot/src/translation/external.rs b/creusot/src/translation/external.rs index 54e8b1b08e..e3aaf9a750 100644 --- a/creusot/src/translation/external.rs +++ b/creusot/src/translation/external.rs @@ -1,6 +1,6 @@ use super::specification::inputs_and_output_from_thir; use crate::{ - contracts_items::{ErasureKind, get_erasure, is_trusted}, + contracts_items::{ErasureKind, get_erasure, get_trusted_positive, is_trusted}, ctx::*, translation::{ pearlite::PIdent, @@ -14,13 +14,17 @@ use rustc_hir::{ def::DefKind, def_id::{DefId, LocalDefId}, }; +use rustc_index::bit_set::DenseBitSet; use rustc_macros::{TyDecodable, TyEncodable}; use rustc_middle::{ thir::{self, Expr, ExprKind, Thir, visit::Visitor}, - ty::{EarlyBinder, GenericArgKind, GenericArgsRef, Predicate, Ty, TyCtxt, TyKind, TypingEnv}, + ty::{ + self, EarlyBinder, GenericArgKind, GenericArgs, GenericArgsRef, Predicate, Ty, TyCtxt, + TyKind, TypingEnv, + }, }; -use rustc_span::Span; -use rustc_type_ir::ConstKind; +use rustc_span::{Span, Symbol}; +use rustc_type_ir::{ConstKind, inherent::AdtDef as _}; #[derive(Clone, Debug, TyEncodable, TyDecodable)] pub(crate) struct ExternSpec<'tcx> { @@ -381,3 +385,53 @@ fn eq_erased_ty<'tcx>(tcx: TyCtxt<'tcx>, ty1: Ty<'tcx>, ty2: Ty<'tcx>) -> bool { _ => false, } } + +#[derive(Clone, Debug, TyEncodable, TyDecodable)] +pub(crate) struct TrustedPositivity { + pub(crate) positivity: DenseBitSet, +} + +pub(crate) fn extract_extern_trusted_positivity( + tcx: TyCtxt, + def_id: DefId, +) -> (DefId, TrustedPositivity) { + let Some(positive_params) = get_trusted_positive(tcx, def_id) else { + tcx.crash_and_error( + tcx.def_span(def_id), + "No `#[trusted_positive(...)]` attribute found on extern type spec", + ) + }; + let bad_extern_spec = || tcx.span_bug(tcx.def_span(def_id), "Badly formed extern type spec"); + let adt = tcx.adt_def(def_id); + let Some(ty) = adt.all_field_tys(tcx).skip_binder().into_iter().next() else { + bad_extern_spec() + }; + let ty::TyKind::Adt(adt, args) = ty.kind() else { bad_extern_spec() }; + (adt.did(), mk_trusted_positivity(positive_params, args)) +} + +pub(crate) fn extract_trusted_positivity(tcx: TyCtxt, def_id: DefId) -> Option { + let positive_params = get_trusted_positive(tcx, def_id)?; + let args = GenericArgs::identity_for_item(tcx, def_id); + Some(mk_trusted_positivity(positive_params, args)) +} + +fn mk_trusted_positivity<'tcx>( + positive_params: Vec, + args: GenericArgsRef<'tcx>, +) -> TrustedPositivity { + let arity = args.len(); + let mut positivity = DenseBitSet::new_empty(arity); + for (i, arg) in args.iter().enumerate() { + let Some(arg) = arg.as_type() else { + continue; + }; + match arg.kind() { + ty::TyKind::Param(param) if positive_params.contains(¶m.name) => { + positivity.insert(i); + } + _ => {} + } + } + TrustedPositivity { positivity } +} diff --git a/creusot/src/validate.rs b/creusot/src/validate.rs index 0b72c490f4..a1b32cde03 100644 --- a/creusot/src/validate.rs +++ b/creusot/src/validate.rs @@ -5,6 +5,7 @@ mod ghost; mod incorrect_attributes; mod opacity; mod purity; +mod recursive_types; mod terminates; mod tokens_new; mod traits; @@ -31,7 +32,10 @@ use crate::{ backend::is_trusted_item, contracts_items::{get_builtin, get_intrinsic, is_extern_spec, is_no_translate, is_spec}, ctx::TranslationCtx, - validate::{erasure::validate_erasures, tokens_new::validate_tokens_new}, + validate::{ + erasure::validate_erasures, recursive_types::validate_recursive_types, + tokens_new::validate_tokens_new, + }, }; fn is_ghost_block(tcx: TyCtxt, id: HirId) -> bool { @@ -71,6 +75,7 @@ pub(crate) fn validate(ctx: &TranslationCtx) { validate_opacity(ctx, def_id); } } + validate_recursive_types(ctx); let variant_calls = validate_terminates(ctx); *ctx.variant_calls.borrow_mut() = variant_calls; validate_traits(ctx); diff --git a/creusot/src/validate/recursive_types.rs b/creusot/src/validate/recursive_types.rs new file mode 100644 index 0000000000..d873dbb7c9 --- /dev/null +++ b/creusot/src/validate/recursive_types.rs @@ -0,0 +1,515 @@ +use crate::{ + backend::ty::classify_adt, + contracts_items::{get_creusot_item, is_opaque, is_trusted, is_trusted_terminates}, + ctx::{HasTyCtxt as _, TranslationCtx}, + validate::terminates::{find_path, proof_tree_nodes}, +}; +use petgraph::{algo::tarjan_scc, graph}; +use rustc_hir::def_id::DefId; +use rustc_index::bit_set::DenseBitSet; +use rustc_middle::ty::{self, AliasTyKind, AssocKind, EarlyBinder, Unnormalized}; +use rustc_span::Span; +use std::collections::{HashMap, HashSet}; + +pub fn validate_recursive_types(ctx: &TranslationCtx) { + let graph = build_type_graph(ctx); + let mut positivity = StrictPositivity::new(); + + for scc in tarjan_scc(&graph.graph) { + // Not a cycle: SCC with a single node and no self edge + if scc.len() == 1 + && let node = scc[0] + && graph.graph.find_edge(node, node).is_none() + { + continue; + } + let in_scc: HashSet<_> = scc.iter().cloned().collect(); + let Err((node, (err, recnode))) = scc.iter().try_for_each(|&node| { + check_recursion(ctx, &mut positivity, &graph, &in_scc, node).map_err(|err| (node, err)) + }) else { + continue; + }; + let node_label = graph.graph[node]; + let span = ctx.def_span(node_label.did()); + let recnode_name = ctx.def_path_str(graph.graph[recnode].did()); + use IllegalRecursion::*; + let mut error = match err { + RecursiveTrait => ctx.error(span, "Illegal recursive trait"), + RecursiveAssocType => ctx.error(span, "Illegal recursive associated type"), + NotStrictlyPositive(field_span, forbidder) => { + let mut error = ctx.error(span, "Illegal recursive type"); + let forbidder = forbidder.display(ctx); + error.span_label( + field_span, + format!("Recursive occurrence of {recnode_name} under {forbidder}"), + ); + error + } + }; + let cycle = find_path(&graph.graph, &in_scc, recnode, node); + let cycle_len = cycle.len(); + let mut current = recnode; + let mut current_name = recnode_name; + for next in cycle.iter().cloned() { + let next_name = ctx.def_path_str(graph.graph[next].did()); + use TypeEdge::*; + match graph.graph[graph.graph.find_edge(current, next).unwrap()] { + // Trivial cycle + AdtDef(_) | Supertrait(_) if cycle_len == 1 => {} + AdtDef(span) => { + error.span_note( + span, + format!("`{next_name}` occurs in this field of `{current_name}`"), + ); + } + AdtDefBound(span, middle) => { + let middle = ctx.def_path_str(middle); + error.span_note( + span, + format!("`{next_name}` is used in this field of `{current_name}`, when resolving a bound of `{middle}`"), + ); + } + AssocType(assoc_id) => { + let assoc = ctx.def_path_str(assoc_id); + error.span_note( + ctx.def_span(assoc_id), + format!("`{next_name}` occurs in the definition of `{assoc}`"), + ); + } + Supertrait(span) => { + error.span_note( + span, + format!("`{next_name}` is a supertrait of `{current_name}`"), + ); + } + FnBound(method, span) => { + let meth = ctx.def_path_str(method); + error.span_note(span, format!("`{next_name}` is a bound of `{meth}`")); + } + } + current = next; + current_name = next_name; + } + error.emit(); + } +} + +enum IllegalRecursion { + RecursiveTrait, + RecursiveAssocType, + NotStrictlyPositive(Span, ForbidsRecursion), +} + +enum ForbidsRecursion { + Abstract(DefId), + NotStrictlyPositive(DefId, usize), + Impl(DefId), + Assoc(DefId), + Other(String), +} + +impl ForbidsRecursion { + fn display(self, ctx: &TranslationCtx) -> String { + use ForbidsRecursion::*; + match self { + Abstract(def_id) => format!("abstract type `{}`", ctx.def_path_str(def_id)), + NotStrictlyPositive(def_id, index) => { + format!("parameter {index} of type `{}`", ctx.def_path_str(def_id)) + } + Impl(impl_id) => format!("trait bound using `{}`", ctx.def_path_str(impl_id)), + Assoc(def_id) => format!("associated type `{}`", ctx.def_path_str(def_id)), + Other(desc) => desc, + } + } +} + +/// Return `Err` if illegal recursion is found, with span that locates the problem. +fn check_recursion( + ctx: &TranslationCtx, + positivity: &mut StrictPositivity, + graph: &TypeGraph, + scc: &HashSet, + node: graph::NodeIndex, +) -> Result<(), (IllegalRecursion, graph::NodeIndex)> { + use IllegalRecursion::*; + use TypeNode::*; + match graph.graph[node] { + Trait(_) => Err((RecursiveTrait, node)), + Type(type_id) => walk_adt(ctx, type_id, |tgt, path, span| { + let index = graph.node_map[&tgt]; + if scc.contains(&index) { + use TypeNode::*; + match tgt { + Type(_) => forbid_recursion(ctx, positivity, type_id, path), + TraitImpl(impl_id) => Err(ForbidsRecursion::Impl(impl_id)), + Trait(_) => unreachable!(), + } + .map_err(|e| (NotStrictlyPositive(span, e), index)) + } else { + Ok(()) + } + }), + TraitImpl(_) => Err((RecursiveAssocType, node)), + } +} + +/// Check whether the given `path` forbids recursion, +/// using visibility relative to `type_id`. +fn forbid_recursion<'tcx>( + ctx: &TranslationCtx<'tcx>, + positivity: &mut StrictPositivity, + type_id: DefId, + path: &[(ty::Ty<'tcx>, Option)], +) -> Result<(), ForbidsRecursion> { + use ForbidsRecursion::*; + use rustc_type_ir::TyKind::*; + path.iter().try_for_each(|(ty, index)| match ty.kind() { + &Adt(def, subst) => { + use crate::backend::ty::AdtKind::*; + match classify_adt(ctx, type_id, def, subst) { + Opaque { .. } | Struct { partially_opaque: true } | Builtin(_) => { + if ctx.trusted_positivity(def.did(), index.unwrap()) { + Ok(()) + } else { + Err(Abstract(def.did())) + } + } + Unit | Empty | Snapshot(_) | Box(_) | Identity(_) => Ok(()), + Enum | Struct { partially_opaque: false } => { + let index = index.unwrap(); + if positivity.get(ctx, def.did(), index) { + Ok(()) + } else { + Err(NotStrictlyPositive(def.did(), index)) + } + } + Namespace => unreachable!(), + } + } + // recursion through arrays and slices is not yet supported + Array(_, _) => Err(Other("array".into())), + Slice(_) => Err(Other("slice".into())), + Alias(alias) => { + let (AliasTyKind::Projection { def_id } + | AliasTyKind::Inherent { def_id } + | AliasTyKind::Opaque { def_id } + | AliasTyKind::Free { def_id }) = alias.kind; + Err(Assoc(def_id)) + } + _ => Ok(()), + }) +} + +/// Map each ADT to a vector indicating the "strict positivity" of its arguments. +/// +/// That an ADT `W` is strictly positive in its first argument (`X`), +/// whatever that means, must imply that it can contain a recursive occurrence of a type. +/// +/// ```ignored +/// // Valid if `W` is strictly positive in its first argument +/// struct A(W); +/// ``` +struct StrictPositivity { + positivity: HashMap>, +} + +impl StrictPositivity { + fn new() -> Self { + Self { positivity: HashMap::new() } + } + + fn get(&mut self, ctx: &TranslationCtx, def_id: DefId, index: usize) -> bool { + self.positivity + .entry(def_id) + .or_insert_with(|| { + ctx.get_trusted_positivity(def_id) + .map(|tp| tp.positivity.clone()) + .unwrap_or_else(|| get_positivity(ctx, def_id)) + }) + .contains(index) + } +} + +fn get_positivity(ctx: &TranslationCtx, def_id: DefId) -> DenseBitSet { + struct ArgPositivity(DenseBitSet); + + use rustc_type_ir::TyKind::Param; + use ty::{TypeSuperVisitable as _, TypeVisitor}; + impl<'tcx> TypeVisitor> for ArgPositivity { + type Result = (); + + fn visit_ty(&mut self, t: ty::Ty) { + use rustc_type_ir::inherent::ParamLike as _; + match t.kind() { + &Param(param) => { + let index = param.index() as usize; + self.0.remove(index); + } + _ => t.super_visit_with(self), + } + } + } + + let generics = ctx.generics_of(def_id); + let mut positivity = ArgPositivity(DenseBitSet::new_filled(generics.count())); + for field in ctx.adt_def(def_id).variants().iter().flat_map(|vdef| vdef.fields.iter()) { + let mut ty = ctx.type_of(field.did).instantiate_identity().skip_normalization(); + // "Strictly positive" parameters are those that appear only naked or under `Box`, + // `Ghost`, `Snapshot`, and `&`. + // FIXME: allow nesting under other "strictly positive" types + loop { + use crate::backend::ty::AdtKind as K; + use rustc_type_ir::TyKind::*; + match ty.kind() { + &Adt(def, args) + if let K::Box(arg) | K::Snapshot(arg) = + classify_adt(ctx, def_id, def, args) => + { + ty = arg + } + &Ref(_, arg, _) => ty = arg, + Param(_) => break, + _ => { + // Mark all parameters that appear here as not strictly positive + positivity.visit_ty(ty); + break; + } + } + } + } + positivity.0 +} + +/// Graph of types and traits +struct TypeGraph { + node_map: HashMap, + graph: graph::DiGraph, +} + +impl TypeGraph { + fn new() -> Self { + Self { node_map: HashMap::new(), graph: graph::DiGraph::new() } + } + + fn node(&mut self, node: TypeNode) -> graph::NodeIndex { + *self.node_map.entry(node).or_insert_with(|| self.graph.add_node(node)) + } + + fn add_edge(&mut self, source: graph::NodeIndex, target: TypeNode, edge: TypeEdge) { + let target = self.node(target); + if let None = self.graph.find_edge(source, target) { + self.graph.add_edge(source, target, edge); + } + } +} + +/// Nodes for `TypeGraph` +#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)] +enum TypeNode { + Type(DefId), + Trait(DefId), + /// Types may depend on trait impls for their associated types + TraitImpl(DefId), +} + +impl TypeNode { + fn did(self) -> DefId { + use TypeNode::*; + match self { + Type(did) | Trait(did) | TraitImpl(did) => did, + } + } +} + +/// Edges for `TypeGraph` +/// Metainformation about the kind of dependency this edge represents. +#[derive(Debug)] +enum TypeEdge { + AdtDef(Span), + /// The target impl was used when instantiating the ADT given by `DefId`. + AdtDefBound(Span, DefId), + /// The target type occurs in an associated type of the source trait impl + AssocType(DefId), + /// A trait mentions another trait in its supertraits + Supertrait(Span), + /// A trait mentions another trait in the signature of a method. + FnBound(DefId, Span), +} + +fn build_type_graph(ctx: &TranslationCtx) -> TypeGraph { + let mut graph = TypeGraph::new(); + + for id in ctx.hir_free_items() { + let item = ctx.hir_item(id); + use rustc_hir::ItemKind::*; + match item.kind { + Struct(..) | Enum(..) | Union(..) => { + add_type(ctx, item.owner_id.to_def_id(), &mut graph) + } + Trait(..) => add_trait(ctx, item.owner_id.to_def_id(), &mut graph), + _ => {} + } + } + + // Add an edge from every trait impl to types that occur in its associated type definitions. + for (&_trait_id, impls) in ctx.all_local_trait_impls(()) { + for &impl_id in impls { + add_trait_impl(ctx, impl_id.to_def_id(), &mut graph); + } + } + + graph +} + +fn add_type(ctx: &TranslationCtx, def_id: DefId, graph: &mut TypeGraph) { + if is_opaque(ctx.tcx, def_id) + || is_trusted(ctx.tcx, def_id) + || is_trusted_terminates(ctx.tcx, def_id) + { + return; + } + let node = graph.node(TypeNode::Type(def_id)); + walk_adt(ctx, def_id, |tgt, path, span| { + let edge = if let TypeNode::TraitImpl(_) = tgt { + let ty::TyKind::Adt(adt, _) = path.last().unwrap().0.kind() else { unreachable!() }; + TypeEdge::AdtDefBound(span, adt.did()) + } else { + TypeEdge::AdtDef(span) + }; + Ok::<(), !>(graph.add_edge(node, tgt, edge)) + }) + .unwrap() +} + +fn add_trait(ctx: &TranslationCtx, def_id: DefId, graph: &mut TypeGraph) { + if is_trusted(ctx.tcx, def_id) { + return; + } + let node = graph.node(TypeNode::Trait(def_id)); + + for &(clause, span) in + ctx.trait_explicit_predicates_and_bounds(def_id.expect_local()).predicates + { + if let ty::ClauseKind::Trait(predicate) = clause.kind().skip_binder() { + graph.add_edge( + node, + TypeNode::Trait(predicate.trait_ref.def_id), + TypeEdge::Supertrait(span), + ); + } + } + + for item in ctx.associated_items(def_id).in_definition_order() { + if get_creusot_item(ctx.tcx, item.def_id).is_some() { + // Skip fake methods + continue; + } + for &(clause, span) in ctx.predicates_of(item.def_id.expect_local()).predicates { + if let ty::ClauseKind::Trait(predicate) = clause.kind().skip_binder() { + graph.add_edge( + node, + TypeNode::Trait(predicate.trait_ref.def_id), + TypeEdge::FnBound(item.def_id, span), + ); + } + } + } +} + +fn add_trait_impl(ctx: &TranslationCtx, def_id: DefId, graph: &mut TypeGraph) { + let node = graph.node(TypeNode::TraitImpl(def_id)); + for &item in ctx.associated_items(def_id).in_definition_order() { + if let AssocKind::Type { .. } = item.kind { + let typing_env = ctx.typing_env(item.def_id); + let ty = ctx.normalize_erasing_regions( + typing_env, + Unnormalized::new(ctx.type_of(item.def_id).skip_binder()), + ); + let mut path = Vec::new(); + walk_type(ctx, typing_env, ty, &mut path, &mut |tgt, _| { + Ok::<(), !>(graph.add_edge(node, tgt, TypeEdge::AssocType(item.def_id))) + }); + } + } +} + +fn walk_adt<'tcx, E>( + ctx: &TranslationCtx<'tcx>, + def_id: DefId, + mut f: impl for<'a> FnMut(TypeNode, &'a [(ty::Ty<'tcx>, Option)], Span) -> Result<(), E>, +) -> Result<(), E> { + let def = ctx.adt_def(def_id); + let typing_env = ctx.typing_env(def.did()); + let mut path = Vec::new(); + for fdef in def.variants().iter().flat_map(|vdef| vdef.fields.iter()) { + let span = ctx.def_span(fdef.did); + let field_ty = + ctx.normalize_erasing_regions(typing_env, ctx.type_of(fdef.did).instantiate_identity()); + walk_type(ctx, typing_env, field_ty, &mut path, &mut |tgt, path| f(tgt, path, span))?; + assert! { path.is_empty() }; + } + Ok(()) +} + +/// Find all type constructors and trait impls that occur in `ty` (must be normalized). +/// +/// Accumulate a `path` of types from the root to the current subterm +/// (with an optional index of the type argument of an ADT). +/// Primitive types that always allow recursion are omitted from the `path`: `&`, `Box`, tuples. +/// +/// This path is ignored in `add_type`, but used for checking recursive occurrences in `check_recursion`. +fn walk_type<'tcx, E>( + ctx: &TranslationCtx<'tcx>, + typing_env: ty::TypingEnv<'tcx>, + ty: ty::Ty<'tcx>, + path: &mut Vec<(ty::Ty<'tcx>, Option)>, + f: &mut impl for<'a> FnMut(TypeNode, &'a [(ty::Ty<'tcx>, Option)]) -> Result<(), E>, +) -> Result<(), E> { + use rustc_type_ir::TyKind::*; + match ty.kind() { + &Adt(adt, args) => { + f(TypeNode::Type(adt.did()), path)?; + // Add edges to impls used to resolve bounds on this ADT's generic arguments + let clauses = ctx.predicates_of(adt.did()).predicates.iter().map(|&(clause, _)| { + ctx.normalize_erasing_regions( + typing_env, + EarlyBinder::bind(clause).instantiate(ctx.tcx, args), + ) + }); + path.push((ty, None)); // Pass the current type to f (for more precise errors) + for trait_impl in proof_tree_nodes(ctx.tcx, typing_env, clauses) { + f(TypeNode::TraitImpl(trait_impl), path)?; + } + path.pop(); + // Iterate through all arguments to get the right indices + args.iter().enumerate().try_for_each(|(index, arg)| { + let Some(arg) = arg.as_type() else { return Ok(()) }; + path.push((ty, Some(index))); + walk_type(ctx, typing_env, arg, path, f)?; + path.pop(); + Ok(()) + })?; + } + &Array(arg, _) | &Slice(arg) => { + path.push((ty, None)); + walk_type(ctx, typing_env, arg, path, f)?; + path.pop(); + } + &Ref(_, arg, _) => walk_type(ctx, typing_env, arg, path, f)?, + &Tuple(args) => { + args.iter().try_for_each(|arg| walk_type(ctx, typing_env, arg, path, f))?; + } + Alias(alias) => { + // Types are normalized, so the only case left should be unresolved associated types. + // FIXME: Figure out how to handle this properly. + path.push((ty, None)); + alias.args.types().try_for_each(|arg| walk_type(ctx, typing_env, arg, path, f))?; + path.pop(); + } + &Dynamic(_predicates, _) => { + // FIXME: Handle this + } + _ => {} + } + Ok(()) +} diff --git a/tests/should_fail/recursive_types/abstract_types.rs b/tests/should_fail/recursive_types/abstract_types.rs new file mode 100644 index 0000000000..66407b8992 --- /dev/null +++ b/tests/should_fail/recursive_types/abstract_types.rs @@ -0,0 +1,9 @@ +#![allow(unused)] +extern crate creusot_std; +use creusot_std::prelude::*; + +mod opaque { + pub struct AbstractBox(Box); +} + +pub struct Bad(opaque::AbstractBox); diff --git a/tests/should_fail/recursive_types/abstract_types.stderr b/tests/should_fail/recursive_types/abstract_types.stderr new file mode 100644 index 0000000000..aab99a27f5 --- /dev/null +++ b/tests/should_fail/recursive_types/abstract_types.stderr @@ -0,0 +1,8 @@ +error: Illegal recursive type + --> abstract_types.rs:9:1 + | +9 | pub struct Bad(opaque::AbstractBox); + | ^^^^^^^^^^^^^^ ------------------------ Recursive occurrence of Bad under abstract type `opaque::AbstractBox` + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/recursive_types/impl_arg.rs b/tests/should_fail/recursive_types/impl_arg.rs new file mode 100644 index 0000000000..aa140b192f --- /dev/null +++ b/tests/should_fail/recursive_types/impl_arg.rs @@ -0,0 +1,22 @@ +extern crate creusot_std; +use creusot_std::prelude::*; + +pub trait Q { + #[logic] + #[ensures(false)] + fn f(self, x: impl Q); +} + +impl Q for i32 { + #[logic] + #[ensures(false)] + fn f(self, x: impl Q) { + x.f(x) + } +} + +#[logic] +#[ensures(false)] +pub fn g() { + 0i32.f(0i32) +} diff --git a/tests/should_fail/recursive_types/impl_arg.stderr b/tests/should_fail/recursive_types/impl_arg.stderr new file mode 100644 index 0000000000..d8b8281cdd --- /dev/null +++ b/tests/should_fail/recursive_types/impl_arg.stderr @@ -0,0 +1,14 @@ +error: Illegal recursive trait + --> impl_arg.rs:4:1 + | +4 | pub trait Q { + | ^^^^^^^^^^^ + | +note: `Q` is a bound of `Q::f` + --> impl_arg.rs:7:24 + | +7 | fn f(self, x: impl Q); + | ^ + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/recursive_types/nonpositive.rs b/tests/should_fail/recursive_types/nonpositive.rs new file mode 100644 index 0000000000..1661457a7d --- /dev/null +++ b/tests/should_fail/recursive_types/nonpositive.rs @@ -0,0 +1,14 @@ +#![allow(unused)] +extern crate creusot_std; +use creusot_std::prelude::*; + +mod opaque { + pub struct AbstractBox(Box); +} + +enum SemiopaqueOption { + None, + Some(opaque::AbstractBox), +} + +pub struct Bad(SemiopaqueOption); diff --git a/tests/should_fail/recursive_types/nonpositive.stderr b/tests/should_fail/recursive_types/nonpositive.stderr new file mode 100644 index 0000000000..731a89257a --- /dev/null +++ b/tests/should_fail/recursive_types/nonpositive.stderr @@ -0,0 +1,8 @@ +error: Illegal recursive type + --> nonpositive.rs:14:1 + | +14 | pub struct Bad(SemiopaqueOption); + | ^^^^^^^^^^^^^^ --------------------- Recursive occurrence of Bad under parameter 0 of type `SemiopaqueOption` + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/recursive_types/via_impls.rs b/tests/should_fail/recursive_types/via_impls.rs new file mode 100644 index 0000000000..f2e0a4eab2 --- /dev/null +++ b/tests/should_fail/recursive_types/via_impls.rs @@ -0,0 +1,21 @@ +#![allow(unused)] +extern crate creusot_std; +use creusot_std::prelude::*; + +pub trait P { + type A; +} + +pub struct S>(pub T::A); + +pub struct Bad(Box>); + +impl P for Bad { + type A = Bad; +} + +pub struct Sneaky; + +impl P for Sneaky { + type A = Bad; +} diff --git a/tests/should_fail/recursive_types/via_impls.stderr b/tests/should_fail/recursive_types/via_impls.stderr new file mode 100644 index 0000000000..ad5e0c731c --- /dev/null +++ b/tests/should_fail/recursive_types/via_impls.stderr @@ -0,0 +1,19 @@ +error: Illegal recursive associated type + --> via_impls.rs:19:1 + | +19 | impl P for Sneaky { + | ^^^^^^^^^^^^^^^^^ + | +note: `Bad` occurs in the definition of `::A` + --> via_impls.rs:20:5 + | +20 | type A = Bad; + | ^^^^^^ +note: `` is used in this field of `Bad`, when resolving a bound of `S` + --> via_impls.rs:11:16 + | +11 | pub struct Bad(Box>); + | ^^^^^^^^^^^^^^ + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/terminates/trait_impl.rs b/tests/should_fail/terminates/trait_impl.rs new file mode 100644 index 0000000000..cd432b612f --- /dev/null +++ b/tests/should_fail/terminates/trait_impl.rs @@ -0,0 +1,35 @@ +// Recursion through trait impls (issue #1232) +extern crate creusot_std; +use creusot_std::prelude::*; + +pub trait Tr1 { + #[logic] + fn f(); +} + +pub trait Tr2 { + #[logic] + fn g(); +} + +impl Tr1 for T +where + T: Tr2, +{ + #[logic] + fn f() { + T::g() + } +} + +impl Tr2 for u32 { + #[logic] + fn g() { + f0::() + } +} + +#[logic] +pub fn f0() { + T::f() +} diff --git a/tests/should_fail/terminates/trait_impl.stderr b/tests/should_fail/terminates/trait_impl.stderr new file mode 100644 index 0000000000..300cba01cb --- /dev/null +++ b/tests/should_fail/terminates/trait_impl.stderr @@ -0,0 +1,19 @@ +error: Mutually recursive functions: when calling `::g`... + --> trait_impl.rs:27:5 + | +27 | fn g() { + | ^^^^^^ + | +note: then `::g` uses the impl `` via the call to `f0`... + --> trait_impl.rs:28:9 + | +28 | f0::() + | ^^^^^^^^^^^ +note: finally the method `::g` might be called + --> trait_impl.rs:27:5 + | +27 | fn g() { + | ^^^^^^ + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/terminates/trait_impl_where.rs b/tests/should_fail/terminates/trait_impl_where.rs new file mode 100644 index 0000000000..bcdb97991c --- /dev/null +++ b/tests/should_fail/terminates/trait_impl_where.rs @@ -0,0 +1,31 @@ +// Similar to `trait_where.rs` but the where clause is only in the impl. +extern crate creusot_std; +use creusot_std::prelude::*; + +// This trait is fine +pub trait Tr { + #[logic] + #[ensures(false)] + fn f(&self); +} + +impl Tr for i32 { + // A too naive termination checker might accept this definition + // because it just calls a parameter, the `f` provided by `i32: Tr`. + // To prevent this, the termination checker resolves the call in the + // typing context of the original function declaration (where there is no bound). + #[logic] + #[ensures(false)] + fn f(&self) + where + i32: Tr, + { + self.f() + } +} + +#[logic] +#[ensures(false)] +pub fn g() { + 1i32.f() +} diff --git a/tests/should_fail/terminates/trait_impl_where.stderr b/tests/should_fail/terminates/trait_impl_where.stderr new file mode 100644 index 0000000000..50c3a78eef --- /dev/null +++ b/tests/should_fail/terminates/trait_impl_where.stderr @@ -0,0 +1,23 @@ +error: Mutually recursive functions: when calling `::f`... + --> trait_impl_where.rs:19:5 + | +19 | / fn f(&self) +20 | | where +21 | | i32: Tr, + | |________________^ + | +note: then `::f` uses the impl `` via the call to `::f`... + --> trait_impl_where.rs:23:9 + | +23 | self.f() + | ^^^^^^^^ +note: finally the method `::f` might be called + --> trait_impl_where.rs:19:5 + | +19 | / fn f(&self) +20 | | where +21 | | i32: Tr, + | |________________^ + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/terminates/trait_where.rs b/tests/should_fail/terminates/trait_where.rs new file mode 100644 index 0000000000..b4fd46b12d --- /dev/null +++ b/tests/should_fail/terminates/trait_where.rs @@ -0,0 +1,29 @@ +// Trait definition is recursive through a where clause of a method +extern crate creusot_std; +use creusot_std::prelude::*; + +// Recursive trait definition +pub trait Tr: Sized { + #[logic] + #[ensures(false)] + fn f(&self, x: &T) + where + Self: Tr; +} + +impl Tr for U { + #[logic] + #[ensures(false)] + fn f(&self, x: &i32) + where + U: Tr, + { + self.f(self) + } +} + +#[logic] +#[ensures(false)] +pub fn g() { + 1i32.f(&1i32) +} diff --git a/tests/should_fail/terminates/trait_where.stderr b/tests/should_fail/terminates/trait_where.stderr new file mode 100644 index 0000000000..fac678c0f1 --- /dev/null +++ b/tests/should_fail/terminates/trait_where.stderr @@ -0,0 +1,14 @@ +error: Illegal recursive trait + --> trait_where.rs:6:1 + | + 6 | pub trait Tr: Sized { + | ^^^^^^^^^^^^^^^^^^^^^^ + | +note: `Tr` is a bound of `Tr::f` + --> trait_where.rs:11:15 + | +11 | Self: Tr; + | ^^^^^^^^ + +error: aborting due to 1 previous error + diff --git a/tests/should_fail/terminates/trait_where_supertrait.rs b/tests/should_fail/terminates/trait_where_supertrait.rs new file mode 100644 index 0000000000..398d7faa57 --- /dev/null +++ b/tests/should_fail/terminates/trait_where_supertrait.rs @@ -0,0 +1,31 @@ +// Same as `trait_where.rs` but recursion goes through a supertrait +extern crate creusot_std; +use creusot_std::prelude::*; + +trait Q: Sized { + #[logic] + fn f(self, x: T) + where + Self: P; +} + +trait P: Q {} + +impl Q for T { + #[logic] + #[ensures(false)] + fn f(self, x: i32) + where + Self: P, + { + self.f(self) + } +} + +impl P for i32 {} + +#[logic] +#[ensures(false)] +pub fn g() { + 0i32.f(0i32) +} diff --git a/tests/should_fail/terminates/trait_where_supertrait.stderr b/tests/should_fail/terminates/trait_where_supertrait.stderr new file mode 100644 index 0000000000..aa68bb1f59 --- /dev/null +++ b/tests/should_fail/terminates/trait_where_supertrait.stderr @@ -0,0 +1,19 @@ +error: Illegal recursive trait + --> trait_where_supertrait.rs:12:1 + | +12 | trait P: Q {} + | ^^^^^^^^^^^^^^^^ + | +note: `Q` is a supertrait of `P` + --> trait_where_supertrait.rs:12:13 + | +12 | trait P: Q {} + | ^^^^ +note: `P` is a bound of `Q::f` + --> trait_where_supertrait.rs:9:15 + | + 9 | Self: P; + | ^^^^^^^ + +error: aborting due to 1 previous error + diff --git a/tests/should_succeed/bug/unnormalized_projection.coma b/tests/should_succeed/bug/unnormalized_projection.coma index 3b5572ae6a..9762e860c8 100644 --- a/tests/should_succeed/bug/unnormalized_projection.coma +++ b/tests/should_succeed/bug/unnormalized_projection.coma @@ -1,9 +1,8 @@ module M_q use creusot.prelude.Any - type t_Vec_B_Global - - type t_B = { f0: t_Vec_B_Global } + type t_Option_Box_B_Global = None | Some t_B + with t_B = { f0: t_Option_Box_B_Global } meta "compute_max_steps" 1000000 diff --git a/tests/should_succeed/bug/unnormalized_projection.rs b/tests/should_succeed/bug/unnormalized_projection.rs index 8f34bbe380..9d47c70ef9 100644 --- a/tests/should_succeed/bug/unnormalized_projection.rs +++ b/tests/should_succeed/bug/unnormalized_projection.rs @@ -9,7 +9,7 @@ pub trait P { pub struct B(::A); impl P for B { - type A = Vec; + type A = Option>; } pub fn q(x: B) { diff --git a/tests/should_succeed/specification/trusted.coma b/tests/should_succeed/specification/trusted.coma index 04075585b8..9f71735832 100644 --- a/tests/should_succeed/specification/trusted.coma +++ b/tests/should_succeed/specification/trusted.coma @@ -37,3 +37,255 @@ module M_innocent_victim [ return (result: UInt32.t) -> {[@stop_split] [@expl:innocent_victim ensures] result = (10: UInt32.t)} (! return {result}) ] end +module M_rose + use seq.Seq + use creusot.int.UInt64 + use creusot.prelude.MutBorrow + use creusot.prelude.Any + use int.Int + + type t_T + + predicate inv_T (_1: t_T) + + type t_Vec_Rose_T_Global + + type t_Rose_T = { f0: t_T; f1: t_Vec_Rose_T_Global } + + predicate resolve_T (_1: t_T) + + type t_IntoIter_Rose_T_Global + + constant const_MAX: UInt64.t = (18446744073709551615: UInt64.t) + + function view_Vec_Rose_T_Global (self: t_Vec_Rose_T_Global) : Seq.seq t_Rose_T + + axiom view_Vec_Rose_T_Global_spec: + forall self: t_Vec_Rose_T_Global [view_Vec_Rose_T_Global self]. Seq.length (view_Vec_Rose_T_Global self) + <= UInt64.t'int const_MAX + + predicate inv_Rose_T (_1: t_Rose_T) + + predicate inv_Vec_Rose_T_Global (_1: t_Vec_Rose_T_Global) + + axiom inv_axiom [@rewrite]: forall x: t_Rose_T [inv_Rose_T x]. inv_Rose_T x + = (inv_T x.f0 /\ inv_Vec_Rose_T_Global x.f1) + + predicate invariant_ref_Rose_T [@inline:trivial] (self: t_Rose_T) = inv_Rose_T self + + meta "rewrite_def" predicate invariant_ref_Rose_T + + predicate inv_ref_Rose_T [@inline:trivial] (_1: t_Rose_T) = invariant_ref_Rose_T _1 + + meta "rewrite_def" predicate inv_ref_Rose_T + + predicate invariant_Seq_Rose_T [@inline:trivial] (self: Seq.seq t_Rose_T) = + forall i: int. 0 <= i /\ i < Seq.length self -> inv_ref_Rose_T (Seq.get self i) + + meta "rewrite_def" predicate invariant_Seq_Rose_T + + predicate inv_Seq_Rose_T [@inline:trivial] (_1: Seq.seq t_Rose_T) = invariant_Seq_Rose_T _1 + + meta "rewrite_def" predicate inv_Seq_Rose_T + + predicate invariant_Vec_Rose_T_Global (self: t_Vec_Rose_T_Global) = inv_Seq_Rose_T (view_Vec_Rose_T_Global self) + + axiom inv_axiom'0: forall x: t_Vec_Rose_T_Global [inv_Vec_Rose_T_Global x]. inv_Vec_Rose_T_Global x + -> invariant_Vec_Rose_T_Global x + + predicate inv_IntoIter_Rose_T_Global (_1: t_IntoIter_Rose_T_Global) + + function view_IntoIter_Rose_T_Global (self: t_IntoIter_Rose_T_Global) : Seq.seq t_Rose_T + + let rec into_iter_Vec_Rose_T_Global (self_: t_Vec_Rose_T_Global) (return (x: t_IntoIter_Rose_T_Global)) = + {[@stop_split] [@expl:into_iter 'self_' type invariant] inv_Vec_Rose_T_Global self_} + any + [ return (result: t_IntoIter_Rose_T_Global) -> + {[@stop_split] [@expl:into_iter_Vec_Rose_T_Global ensures] ([@stop_split] [@expl:into_iter result type invariant] inv_IntoIter_Rose_T_Global result) + /\ ([@stop_split] [@expl:into_iter ensures] view_Vec_Rose_T_Global self_ = view_IntoIter_Rose_T_Global result)} + (! return {result}) ] + + type t_Option_Rose_T = None | Some t_Rose_T + + predicate invariant_refmut_IntoIter_Rose_T_Global [@inline:trivial] (self: MutBorrow.t t_IntoIter_Rose_T_Global) = + inv_IntoIter_Rose_T_Global self.current /\ inv_IntoIter_Rose_T_Global self.final + + meta "rewrite_def" predicate invariant_refmut_IntoIter_Rose_T_Global + + predicate inv_refmut_IntoIter_Rose_T_Global [@inline:trivial] (_1: MutBorrow.t t_IntoIter_Rose_T_Global) = + invariant_refmut_IntoIter_Rose_T_Global _1 + + meta "rewrite_def" predicate inv_refmut_IntoIter_Rose_T_Global + + predicate inv_Option_Rose_T (_1: t_Option_Rose_T) + + axiom inv_axiom'1 [@rewrite]: forall x: t_Option_Rose_T [inv_Option_Rose_T x]. inv_Option_Rose_T x + = match x with + | None -> true + | Some f0'0 -> inv_Rose_T f0'0 + end + + predicate produces_IntoIter_Rose_T_Global (self: t_IntoIter_Rose_T_Global) (visited: Seq.seq t_Rose_T) (rhs: t_IntoIter_Rose_T_Global) = + view_IntoIter_Rose_T_Global self = Seq.(++) visited (view_IntoIter_Rose_T_Global rhs) + + function produces_trans_IntoIter_Rose_T_Global (a: t_IntoIter_Rose_T_Global) (ab: Seq.seq t_Rose_T) (b: t_IntoIter_Rose_T_Global) (bc: Seq.seq t_Rose_T) (c: t_IntoIter_Rose_T_Global) : () + = () + + axiom produces_trans_IntoIter_Rose_T_Global_spec: + forall a: t_IntoIter_Rose_T_Global, ab: Seq.seq t_Rose_T, b: t_IntoIter_Rose_T_Global, bc: Seq.seq t_Rose_T, c: t_IntoIter_Rose_T_Global. produces_IntoIter_Rose_T_Global a ab b + -> produces_IntoIter_Rose_T_Global b bc c -> produces_IntoIter_Rose_T_Global a (Seq.(++) ab bc) c + + function produces_refl_IntoIter_Rose_T_Global (self: t_IntoIter_Rose_T_Global) : () = () + + axiom produces_refl_IntoIter_Rose_T_Global_spec: + forall self: t_IntoIter_Rose_T_Global. produces_IntoIter_Rose_T_Global self (Seq.empty: Seq.seq t_Rose_T) self + + predicate resolve_refmut_IntoIter_Rose_T_Global [@inline:trivial] (_1: MutBorrow.t t_IntoIter_Rose_T_Global) = + _1.final = _1.current + + meta "rewrite_def" predicate resolve_refmut_IntoIter_Rose_T_Global + + predicate completed_IntoIter_Rose_T_Global (self: MutBorrow.t t_IntoIter_Rose_T_Global) = + resolve_refmut_IntoIter_Rose_T_Global self + /\ view_IntoIter_Rose_T_Global self.current = (Seq.empty: Seq.seq t_Rose_T) + + let rec next_IntoIter_Rose_T_Global (self_: MutBorrow.t t_IntoIter_Rose_T_Global) (return (x: t_Option_Rose_T)) = + {[@stop_split] [@expl:next 'self_' type invariant] inv_refmut_IntoIter_Rose_T_Global self_} + any + [ return (result: t_Option_Rose_T) -> + {[@stop_split] [@expl:next_IntoIter_Rose_T_Global ensures] ([@stop_split] [@expl:next result type invariant] inv_Option_Rose_T result) + /\ ([@stop_split] [@expl:next ensures] match result with + | None -> completed_IntoIter_Rose_T_Global self_ + | Some v -> produces_IntoIter_Rose_T_Global self_.current (Seq.singleton v) self_.final + end)} + (! return {result}) ] + + let rec elim_Some (_x: t_Option_Rose_T) (return (f0'0: t_Rose_T)) = any + [ _k (f0'0: t_Rose_T) -> {Some f0'0 = _x} (! return {f0'0}) + | _chk -> (! {[@expl:elim Some] match _x with + | Some _ -> true + | _ -> false + end} + any) ] + + function index_Vec_Rose_T_Global [@inline:trivial] (self: t_Vec_Rose_T_Global) (ix: int) : t_Rose_T = + Seq.get (view_Vec_Rose_T_Global self) ix + + meta "rewrite_def" function index_Vec_Rose_T_Global + + predicate resolve_Rose_T (_1: t_Rose_T) + + predicate resolve_Vec_Rose_T_Global [@inline:trivial] (self: t_Vec_Rose_T_Global) = + forall i: int. 0 <= i /\ i < Seq.length (view_Vec_Rose_T_Global self) + -> resolve_Rose_T (index_Vec_Rose_T_Global self i) + + meta "rewrite_def" predicate resolve_Vec_Rose_T_Global + + predicate resolve_Vec_Rose_T_Global'0 (_1: t_Vec_Rose_T_Global) + + axiom resolve_axiom: forall x: t_Vec_Rose_T_Global [resolve_Vec_Rose_T_Global'0 x]. resolve_Vec_Rose_T_Global'0 x + -> resolve_Vec_Rose_T_Global x + + axiom resolve_axiom'0 [@rewrite]: forall x: t_Rose_T [resolve_Rose_T x]. resolve_Rose_T x + = (resolve_T x.f0 /\ resolve_Vec_Rose_T_Global'0 x.f1) + + predicate resolve_IntoIter_Rose_T_Global [@inline:trivial] (self: t_IntoIter_Rose_T_Global) = + forall i: int. 0 <= i /\ i < Seq.length (view_IntoIter_Rose_T_Global self) + -> resolve_Rose_T (Seq.get (view_IntoIter_Rose_T_Global self) i) + + meta "rewrite_def" predicate resolve_IntoIter_Rose_T_Global + + predicate resolve_IntoIter_Rose_T_Global'0 (_1: t_IntoIter_Rose_T_Global) + + axiom resolve_axiom'1: + forall x: t_IntoIter_Rose_T_Global [resolve_IntoIter_Rose_T_Global'0 x]. resolve_IntoIter_Rose_T_Global'0 x + -> resolve_IntoIter_Rose_T_Global x + + meta "compute_max_steps" 1000000 + + meta "select_lsinst" "all" + + let rec rose_T (r: t_Rose_T) (return (x: UInt64.t)) = {[@stop_split] [@expl:rose 'r' type invariant] inv_Rose_T r} + (! bb0 + [ bb0 = s0 + [ s0 = s1 [ _ck -> (! {[@expl:type invariant] inv_T r.f0} any) ] + | s1 = -{resolve_T r.f0}- s2 + | s2 = into_iter_Vec_Rose_T_Global {r.f1} (fun (_x: t_IntoIter_Rose_T_Global) -> [ &_4 <- _x ] s3) + | s3 = [ &iter <- _4 ] s4 + | s4 = bb2 ] + | bb2 = bb2 + [ bb2 = {[@expl:inferred invariant: type invariant] inv_IntoIter_Rose_T_Global iter} + (! s0) + [ s0 = MutBorrow.borrow_mut {iter} + (fun (_bor: MutBorrow.t t_IntoIter_Rose_T_Global) -> + [ &_11 <- _bor ] -{inv_IntoIter_Rose_T_Global _bor.final}- + [ &iter <- _bor.final ] s1) [ _ck -> (! {[@expl:type invariant] inv_IntoIter_Rose_T_Global iter} any) ] + | s1 = MutBorrow.borrow_final {_11.current} {MutBorrow.get_id _11} + (fun (_bor: MutBorrow.t t_IntoIter_Rose_T_Global) -> + [ &_10 <- _bor ] -{inv_IntoIter_Rose_T_Global _bor.final}- + [ &_11 <- { _11 with current = _bor.final } ] s2) + [ _ck -> (! {[@expl:type invariant] inv_IntoIter_Rose_T_Global _11.current} any) ] + | s2 = next_IntoIter_Rose_T_Global {_10} (fun (_x: t_Option_Rose_T) -> [ &_9 <- _x ] s3) + | s3 = s4 [ _ck -> (! {[@expl:type invariant] inv_refmut_IntoIter_Rose_T_Global _11} any) ] + | s4 = -{resolve_refmut_IntoIter_Rose_T_Global _11}- s5 + | s5 = any [ br0 -> {_9 = None} (! bb6) | br1 (x0: t_Rose_T) -> {_9 = Some x0} (! bb7) ] ] + [ bb7 = s0 + [ s0 = elim_Some {_9} (fun (r0: t_Rose_T) -> [ &r'0 <- r0 ] s1) + | s1 = rose_T {r'0} (fun (_x: UInt64.t) -> [ &_15 <- _x ] s2) + | s2 = bb2 ] ] ] + | bb6 = s0 + [ s0 = s1 [ _ck -> (! {[@expl:type invariant] inv_IntoIter_Rose_T_Global iter} any) ] + | s1 = -{resolve_IntoIter_Rose_T_Global'0 iter}- s2 + | s2 = [ &_ret <- (0: UInt64.t) ] s3 + | s3 = return {_ret} ] ] + [ & _ret: UInt64.t = Any.any_l () + | & r: t_Rose_T = r + | & _4: t_IntoIter_Rose_T_Global = Any.any_l () + | & iter: t_IntoIter_Rose_T_Global = Any.any_l () + | & _9: t_Option_Rose_T = Any.any_l () + | & _10: MutBorrow.t t_IntoIter_Rose_T_Global = Any.any_l () + | & _11: MutBorrow.t t_IntoIter_Rose_T_Global = Any.any_l () + | & r'0: t_Rose_T = Any.any_l () + | & _15: UInt64.t = Any.any_l () ]) + [ return (result: UInt64.t) -> {[@stop_split] [@expl:rose ensures] UInt64.t'int result = 0} (! return {result}) ] +end +module M_carnation + use creusot.int.UInt64 + use creusot.prelude.Any + + type t_Vec_Rose_Box_Carnation_Global_Global + + type t_Vec_Rose_Rose_Box_Carnation_Global_Global + + type t_Carnation = Branch t_Rose_Rose_Box_Carnation_Global | Leaf + with t_Rose_Box_Carnation_Global = { f0: t_Carnation; f1: t_Vec_Rose_Box_Carnation_Global_Global } + with t_Rose_Rose_Box_Carnation_Global = { + f0'0: t_Rose_Box_Carnation_Global; + f1'0: t_Vec_Rose_Rose_Box_Carnation_Global_Global } + + let rec elim_Branch (_x: t_Carnation) (return (f0'1: t_Rose_Rose_Box_Carnation_Global)) = any + [ _k (f0'1: t_Rose_Rose_Box_Carnation_Global) -> {Branch f0'1 = _x} (! return {f0'1}) + | _chk -> (! {[@expl:elim Branch] match _x with + | Branch _ -> true + | _ -> false + end} + any) ] + + let rec rose_Rose_Box_Carnation_Global (r: t_Rose_Rose_Box_Carnation_Global) (return (x: UInt64.t)) = any + [ return (result: UInt64.t) -> {[@stop_split] [@expl:rose ensures] UInt64.t'int result = 0} (! return {result}) ] + + meta "compute_max_steps" 1000000 + + meta "select_lsinst" "all" + + let rec carnation (c: t_Carnation) (return (x: UInt64.t)) = (! bb0 + [ bb0 = any [ br0 (x0: t_Rose_Rose_Box_Carnation_Global) -> {c = Branch x0} (! bb4) | br1 -> {c = Leaf} (! bb3) ] + | bb3 = s0 [ s0 = [ &_ret <- (0: UInt64.t) ] s1 | s1 = return {_ret} ] + | bb4 = s0 + [ s0 = elim_Branch {c} (fun (r0: t_Rose_Rose_Box_Carnation_Global) -> [ &r <- r0 ] s1) + | s1 = rose_Rose_Box_Carnation_Global {r} (fun (_x: UInt64.t) -> [ &_ret <- _x ] s2) + | s2 = return {_ret} ] ] + [ & _ret: UInt64.t = Any.any_l () | & c: t_Carnation = c | & r: t_Rose_Rose_Box_Carnation_Global = Any.any_l () ]) + [ return (result: UInt64.t) -> {[@stop_split] [@expl:carnation ensures] UInt64.t'int result = 0} + (! return {result}) ] +end diff --git a/tests/should_succeed/specification/trusted.rs b/tests/should_succeed/specification/trusted.rs index bb4980198b..4e2040f6e7 100644 --- a/tests/should_succeed/specification/trusted.rs +++ b/tests/should_succeed/specification/trusted.rs @@ -54,3 +54,30 @@ pub struct Opaque; pub fn xray() -> Opaque { Opaque } + +#[trusted(terminates, positive(T))] +pub struct Rose(T, Vec>); + +pub enum Carnation { + Branch(Rose>>), + Leaf, +} + +#[trusted(terminates)] +#[ensures(result@ == 0)] +pub fn rose(r: Rose) -> usize { + for r in r.1 { + rose(r); + } + 0 +} + +#[check(terminates)] +#[ensures(result@ == 0)] +pub fn carnation(c: Carnation) -> usize { + use Carnation::*; + match c { + Branch(r) => rose(r), + Leaf => 0, + } +} diff --git a/tests/should_succeed/specification/trusted/proof.json b/tests/should_succeed/specification/trusted/proof.json index ee3efa4f1a..9109c9cf9d 100644 --- a/tests/should_succeed/specification/trusted/proof.json +++ b/tests/should_succeed/specification/trusted/proof.json @@ -6,14 +6,34 @@ { "prover": "cvc4@1.8", "size": 40, "time": 0.506 } ], "proofs": { + "M_carnation": { + "vc_carnation": { "prover": "alt-ergo@2.6.2", "time": 0.025 }, + "vc_elim_Branch": { "prover": "alt-ergo@2.6.2", "time": 0.014 }, + "vc_rose_Rose_Box_Carnation_Global": { + "prover": "alt-ergo@2.6.2", + "time": 0.011 + } + }, "M_innocent_victim": { "vc_im_out_of_control": { "prover": "cvc5@1.3.1", "time": 0.014 }, "vc_innocent_victim": { "prover": "cvc5@1.3.1", "time": 0.026 }, - "vc_my_unverified_code": { "prover": "cvc5@1.3.1", "time": 0.024 } + "vc_my_unverified_code": { "prover": "cvc5@1.3.1", "time": 0.011 } + }, + "M_rose": { + "vc_elim_Some": { "prover": "alt-ergo@2.6.2", "time": 0.042 }, + "vc_into_iter_Vec_Rose_T_Global": { + "prover": "alt-ergo@2.6.2", + "time": 0.043 + }, + "vc_next_IntoIter_Rose_T_Global": { + "prover": "alt-ergo@2.6.2", + "time": 0.027 + }, + "vc_rose_T": { "prover": "alt-ergo@2.6.2", "time": 0.032 } }, "M_victim_of_lie": { "vc_lie": { "prover": "cvc5@1.3.1", "time": 0.015 }, - "vc_victim_of_lie": { "prover": "cvc5@1.3.1", "time": 0.028 } + "vc_victim_of_lie": { "prover": "cvc5@1.3.1", "time": 0.007 } } } } From 2d0241650c53f6f7d945e1811b50a6d057e355be Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 23 Mar 2026 17:00:55 +0100 Subject: [PATCH 4/4] guide: Add more details about termination check --- guide/src/termination.md | 268 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 248 insertions(+), 20 deletions(-) diff --git a/guide/src/termination.md b/guide/src/termination.md index 16381c7acb..f5512e30a3 100644 --- a/guide/src/termination.md +++ b/guide/src/termination.md @@ -1,6 +1,37 @@ # Termination -By default, Creusot does not require that program functions terminate, which may lead to surprising situations: +## Motivations + +There are several reasons why Creusot cares about termination: + +- Termination of logic functions (in Pearlite) is crucial for soundness. Otherwise you could prove `false` as follows: + + ```rust + #[logic] + #[ensures(false)] + fn falso() { + falso() + } + ``` + +- Termination of ghost program functions is also necessary for soundness. + Erasing ghost code must not change the observable behavior of the program. + +- Termination of non-ghost program functions is optional, but desirable. + + - By default, we prove *partial correctness*: for all inputs satisfying the precondition, + **if** the function terminates, **then** its postcondition holds. + + - Adding the attribute `#[check(terminates)]` changes the goal to *total correctness*: + for all inputs satisfying the precondition, the function terminates **and** its postcondition holds. + + Total correctness of non-ghost programs is opt-in because it is often cumbersome + (requiring `#[variant]` annotations, no support for mutually recursive functions (yet)...) + and sometimes significantly harder than partial correctness. + +## Terminating program functions: `#[check(terminates)]` + +Non-terminating functions may lead to surprising situations: ```rust #[ensures(result@ == 42)] @@ -24,8 +55,7 @@ fn nonsense() -> u64 { // Fails to compile now ! A function with the `check(terminates)` attribute cannot: - Call a non-`terminates` function. -- Use a loop construct (`for`, `while`, `loop`). This restriction may be lifted in the future. -- Use simple recursion without the `variant` attribute. +- Use direct recursion or loops without the `variant` attribute. This means that this function will not be accepted: @@ -56,7 +86,201 @@ A function with the `check(terminates)` attribute cannot: fn g() { f() } ``` -## Mutual recursion through traits +## Dependencies + +The recursion check explores the body of the functions in the current crate, but it cannot do so with the dependencies, whose function bodies are not visible. + +Thus, it assumes two things: + +1. The recursion check passed on the dependencies of the current crate. +2. If a function in a dependency has a trait bound, the recursion check pessimistically assumes that all the functions of the trait are called. + +Example: + +```rust +// dependency/src/lib.rs +trait Tr { + fn f(); +} +fn g() { + // It does not matter if `::f` is called or not, since we cannot see it +} + +// lib.rs +impl Tr for i32 { + fn f() { + g::(); // Error ! + } +} +``` + +## Termination check in detail + +To ensure that declarations are well-defined: + +1. we check recursion between types; +2. we check recursion between terminating functions: logic functions and program functions marked `#[check(ghost)]` or `#[check(terminates)]`; +3. in terminating program functions, we check that all loops have variants. + +For steps 1 and 2, we construct two dependency graphs of items. +For the type recursion check (step 1), the graph contains types, traits, and impls. +For the function recursion check (step 2), the graph contains functions and impls. +These graphs contain an edge from item A to item B if A mentions B. +Each strongly connected component in that graph is either: + +- a single item with no edge to itself, that is a non-recursive item which + requires no further check: it is well-defined if all of its dependencies are well-founded; +- otherwise, the strongly connected component is a *recursive group*, + and we have to look at the kind of items it contains. + +### Recursive types and strict positivity + +In the definition of a recursive type, other types from its recursive group +can only appear in *strictly positive* positions. + +At the moment, this allows the defined type to occur only in a field type, +either directly or under `Box`, `&`, or `&mut`. For example: + +```rust +pub enum Peano { + Zero, + Suc(Box), // Peano in strictly positive position ==> OK +} +``` + + + +There is some experimental support for allowing recursive occurrences through other type constructors. +For example, the argument of `Option<_>` is strictly positive, allowing this type: + +```rust +pub enum List(T, Option>>); +``` + +The attribute `#[trusted(positive(T))]` can be used on a `struct` or `enum` +to postulate that certain arguments are strictly positive. + +#### Counterexample + +Recursive types are indeed a possible source of unsoundness if left unchecked. + +The standard counterexample is that a type `L` which is equivalent to `L -> bool` +(written `Mapping` in Creusot) easily leads to a contradiction +without writing an explicitly recursive function: + +```rust +// This type is rejected by Creusot, +// otherwise we could prove a contradiction via the function below. +pub struct L(Mapping); + +#[logic] +#[ensures(result == !result)] // false! +pub fn infinity() -> bool { + pearlite! { + let suc: Mapping = |f: L| !f.0[f]; + suc[L(suc)] + } +} +``` + +### Recursive traits: not allowed + +A trait cannot belong to a recursive group. +In other words, a trait must not mention itself in its supertrait bounds +or in the bounds of its methods. + +#### Counterexample + +A proof of `false` using a recursive trait: + +```rust +pub trait Tr: Sized { + #[logic] + #[ensures(false)] + fn f(&self, x: &T) where Self: Tr; +} + +impl Tr for U { + #[logic] + #[ensures(false)] + fn f(&self, x: &i32) where Self: Tr { + self.f(self) + } +} + +#[logic] +#[ensures(false)] +fn g() { + 1i32.f(&1i32) +} +``` + +### Recursive associated types: not allowed + +These corresponds to impl items in the type dependency graph. + +#### Counterexample + +While the Rust type checker already forbids some recursive associated types, +it still allows a form of indirect recursion. +Those are subsequently rejected by Creusot: + +```rust +trait P { + type A; +} + +// This alone is not recursive, +// but we must remain careful about how `T: P` is instantiated. +struct B(::A); + +struct Dummy; + +impl P for Dummy { + // This associated type is recursive through the instantiation of `B`. + type A = Mapping, bool>; +} +``` + +If this were accepted by Creusot, the associated type `Dummy::A` would be equivalent to +`Mapping`, which would be unsound as explained in a [previous counterexample](#counterexample). + +### Recursive functions + +Functions that must terminate are `#[logic]` functions and +program functions annotated with `#[check(ghost)]` or `#[check(terminates)]`. + +Currently, mutually recursive functions are not supported. + +A recursive function must have a variant (a quantity that decreases at every recursive call) +which implements a [`WellFounded`][well-founded] relation. +Variants are given using the `#[variant(_)]` attribute. + +Similarly, within a terminating program function, all loops must also have a `#[variant(_)]`. + +The `#[trusted(terminates)]` attribute can be used to disable termination checking +for a function, while allowing calling it in other `#[check(terminates)]` function. + +[well-founded]: https://doc.creusot.rs/creusot_std/logic/trait.WellFounded.html + +### Mutual recursion through traits Traits complicate the recursion analysis. Indeed, if we have a function like @@ -90,30 +314,34 @@ impl Tr for i32 { does not, because we know that `g::` calls `::f()`, causing a cycle. -## Dependencies +### Trait impl methods with bounds -The recursion check explores the body of the functions in the current crate, but it cannot do so with the dependencies, whose function bodies are not visible. +When termination checking a trait impl method, we use the bounds from its trait definition. -Thus, it assumes two things: +#### Counterexample -1. The recursion check passed on the dependencies of the current crate. -2. If a function in a dependency has a trait bound, the recursion check pessimistically assumes that all the functions of the trait are called. - -Example: +In the following example, the call `self.f()` will be checked in an environment +without the `i32: Tr` bound of the enclosing function, because it is not present +in the declaration of `f` in `trait Tr`. ```rust -// dependency/src/lib.rs -trait Tr { - fn f(); -} -fn g() { - // It does not matter if `::f` is called or not, since we cannot see it +pub trait Tr { + #[logic] + #[ensures(false)] + fn f(self) -> Self; } -// lib.rs impl Tr for i32 { - fn f() { - g::(); // Error ! + #[logic] + #[ensures(false)] + fn f(self) -> Self where i32: Tr { + self.f() } } + +#[logic] +#[ensures(false)] +pub fn contra() -> i32 { + 0i32.f() +} ```