diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs index cc67a34dbe..bf0e80aefb 100644 --- a/creusot/src/backend.rs +++ b/creusot/src/backend.rs @@ -80,7 +80,7 @@ impl<'tcx> Why3Generator<'tcx> { let proof_modl = logic::translate_logic(self, def_id); TranslatedItem::Logic { proof_modl } } - ItemType::Program => { + ItemType::Program | ItemType::Constant => { let modl = program::translate_function(self, def_id); TranslatedItem::Program { modl } } @@ -93,8 +93,7 @@ impl<'tcx> Why3Generator<'tcx> { | ItemType::Trait | ItemType::Type | ItemType::AssocTy - | ItemType::Impl - | ItemType::Constant => return, + | ItemType::Impl => return, }; self.functions.push(translated_item); } diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs index 91ba22b2da..4ab1787d7e 100644 --- a/creusot/src/backend/clone_map.rs +++ b/creusot/src/backend/clone_map.rs @@ -132,6 +132,10 @@ pub(crate) trait Namer<'tcx> { self.dependency(Dependency::PrivateResolve(struct_id, subst)).ident() } + fn opaque_const(&self, name: &str, ty: Ty<'tcx>) -> Ident { + self.dependency(Dependency::OpaqueConst(rustc_span::Symbol::intern(name), ty)).ident() + } + /// Ideally we'd like to avoid caring about normalization in the backend, /// but we still need this for normalizing field types after instantiation. /// Also for normalizing RPITs but that seems easier to get rid of if we ever care to. @@ -625,6 +629,9 @@ fn display_cycle_<'tcx>( &PrivateTyInv(def_id, _args) => { write!(f, "private ty inv {}", tcx.def_path_str(def_id)) } + &OpaqueConst(name, ty) => { + write!(f, "opaque const {name} {ty}") + } }?; f.write_str(";")?; if i < scc.len() - 1 { @@ -669,20 +676,18 @@ impl Setters { Decl::Goal(Goal { name, goal }) } else { let ret = Ident::fresh_local("ret"); - let prototype = Prototype { - name, - attrs: vec![], - params: [Param::Cont(name::return_(), [].into(), [].into())].into(), - }; + let params = args + .into_iter() + .map(|(arg, ty)| Param::Term(arg, ty)) + .chain(std::iter::once(Param::Cont(name::return_(), [].into(), [].into()))) + .collect::>(); + let prototype = Prototype { name, attrs: vec![], params }; let body = self.call_setters(Expr::var(ret)).black_box(); let body = requires .into_iter() .rfold(body, |body, pre| Expr::Assert(pre.boxed(), body.boxed())); let ret_defn = Defn { - prototype: Prototype::new( - ret, - args.into_iter().map(|(arg, ty)| Param::Term(arg, ty)).collect::>(), - ), + prototype: Prototype::new(ret, []), body: Expr::Assert(ensures.boxed(), Expr::var(name::return_()).black_box().boxed()), }; let body = Expr::Defn(body.boxed(), false, [ret_defn].into()); diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs index cfddf45a79..50c059709e 100644 --- a/creusot/src/backend/clone_map/elaborator.rs +++ b/creusot/src/backend/clone_map/elaborator.rs @@ -640,6 +640,14 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> { }; vec![Decl::predicate(sig, None)] } + Dependency::OpaqueConst(_, ty) => { + let name = self.namer.dependency(dep).ident(); + let ty = translate_ty(ctx, self.namer, self.root_span, ty); + vec![Decl::LogicDecl(LogicDecl { + kind: Some(DeclKind::Constant), + sig: Signature::constant(name, ty), + })] + } }; self.dep_bodies.insert(dep, decls); diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs index eced6bb43f..c08e5cd31a 100644 --- a/creusot/src/backend/dependency.rs +++ b/creusot/src/backend/dependency.rs @@ -29,6 +29,8 @@ pub(crate) enum Dependency<'tcx> { PrivateFields(DefId, GenericArgsRef<'tcx>), PrivateResolve(DefId, GenericArgsRef<'tcx>), PrivateTyInv(DefId, GenericArgsRef<'tcx>), + /// An opaque constant from trying to use a non-visible constructor. + OpaqueConst(Symbol, Ty<'tcx>), } impl<'tcx> Dependency<'tcx> { @@ -120,6 +122,7 @@ impl<'tcx> Dependency<'tcx> { Dependency::PreMod(_) => None, Dependency::PrivateResolve(..) => Some(Symbol::intern("resolve__private")), Dependency::PrivateTyInv(..) => Some(Symbol::intern("inv__private")), + Dependency::OpaqueConst(name, _) => Some(name), } } } diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs index d8db321c32..de3a9389de 100644 --- a/creusot/src/backend/program.rs +++ b/creusot/src/backend/program.rs @@ -62,11 +62,27 @@ pub(crate) fn translate_function<'tcx>( ctx: &Why3Generator<'tcx>, def_id: DefId, ) -> Option { + if !def_id.is_local() || !ctx.has_body(def_id) || is_trusted_item(ctx.tcx, def_id) { + return None; + } + let names = Dependencies::new(ctx, def_id); let namespace_ty = names.namespace_ty(); - if !def_id.is_local() || !ctx.has_body(def_id) || is_trusted_item(ctx.tcx, def_id) { - return None; + use DefKind::*; + match ctx.tcx().def_kind(def_id) { + AssocConst { .. } | Const { .. } => { + // Translate const only if there is a non-trivial invariant or postcondition + let sig = ctx.sig(def_id); + let span = ctx.tcx().def_span(def_id); + if is_tyinv_trivial(&ctx.ctx, def_id, names.typing_env(), sig.output, span) + && !sig.contract.has_user_contract + { + return None; + } + } + InlineConst { .. } => return None, + _ => {} } let name = names.source_ident(); diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs index 291499293b..c209af6e0a 100644 --- a/creusot/src/backend/term.rs +++ b/creusot/src/backend/term.rs @@ -4,8 +4,8 @@ use crate::{ program::{PtrCastKind, ptr_cast_kind}, projections::{borrow_generated_id, projections_term}, ty::{ - constructor, floatty_to_prelude, ity_to_prelude, translate_ty, ty_to_prelude, - uty_to_prelude, + classify_adt, constructor, floatty_to_prelude, ity_to_prelude, translate_ty, + ty_to_prelude, uty_to_prelude, }, }, contracts_items::{is_builtin_ascription, is_new_namespace}, @@ -297,6 +297,27 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> { } TermKind::Constructor { variant, fields, .. } => { let TyKind::Adt(adt, subst) = term.ty.kind() else { unreachable!() }; + use crate::backend::ty::AdtKind::*; + if let Opaque { .. } | Struct { partially_opaque: true } = + classify_adt(self.ctx, self.names.source_id(), *adt, subst) + { + self.ctx + .struct_warn( + term.span, + format!( + "encountered non-visible constructor {}", + self.tcx().def_path_str(adt.did()) + ), + ) + .with_span_note( + self.tcx().def_span(self.names.source_id()), + "during the translation of this function", + ) + .emit(); + let name = format!("opaque_{}", self.tcx().item_name(adt.did())); + let ident = self.names.opaque_const(&name, term.ty); + return Exp::var(ident); + } let fields = fields.into_iter().map(|f| self.lower_term(f)).collect(); constructor(self.names, fields, adt.variant(*variant).def_id, subst) } diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs index 79cedebb4e..7c736eaf28 100644 --- a/creusot/src/contracts_items/attributes.rs +++ b/creusot/src/contracts_items/attributes.rs @@ -74,6 +74,7 @@ attribute_functions! { [creusot::clause::check_ghost::trusted] => is_check_ghost_trusted [creusot::bitwise] => is_bitwise [creusot::builtin_ascription] => is_builtin_ascription + [creusot::no_simp] => is_no_simp } pub(crate) fn get_invariant_expl(tcx: TyCtxt, def_id: DefId) -> Option { diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs index f5c5e1f398..e3b434dd07 100644 --- a/creusot/src/ctx.rs +++ b/creusot/src/ctx.rs @@ -147,6 +147,10 @@ pub trait HasTyCtxt<'tcx> { self.tcx().dcx().span_warn(span, msg) } + fn struct_warn(&self, span: Span, msg: impl Into) -> Diag<'tcx, ()> { + self.tcx().dcx().struct_span_warn(span, msg) + } + fn span_bug(&self, span: Span, msg: impl Into) -> ! { self.tcx().dcx().span_bug(span, msg.into()) } @@ -424,7 +428,7 @@ impl<'tcx> TranslationCtx<'tcx> { /// set as their *visibility*. fn mk_opacity(&self, item: DefId) -> Opacity { match self.item_type(item) { - ItemType::Constant => Opacity::Transparent(Visibility::Public), + ItemType::Constant => Opacity::Transparent(self.visibility(item)), ItemType::Logic { .. } if is_opaque(self.tcx, item) => Opacity::Opaque, ItemType::Logic { .. } => { let vis = opacity_witness_name(self.tcx, item).map_or_else( diff --git a/creusot/src/translation/constant.rs b/creusot/src/translation/constant.rs index 33d8e321bb..5e48f8eff5 100644 --- a/creusot/src/translation/constant.rs +++ b/creusot/src/translation/constant.rs @@ -1,4 +1,5 @@ use crate::{ + contracts_items::is_no_simp, ctx::{HasTyCtxt as _, TranslationCtx}, translation::{fmir::Operand, pearlite::Literal, traits::TraitResolved}, }; @@ -130,6 +131,16 @@ fn try_scalar_to_literal<'tcx>( /// Translate constant with a simple body: it can be reduced to a value expressible in /// the logical fragment of Why3, or its body is just a variable. /// `None` if it does not match these cases. +/// +/// We try to normalize consts by default because there are really silly +/// definitions out there that are best hidden from users: +/// +/// ``` +/// const MAX: usize = !0; +/// +/// const MIN: isize = !isize::MAX +/// const MAX: isize = (usize::MAX >> 1) as isize; +/// ``` pub fn try_const_to_term<'tcx>( def_id: DefId, subst: ty::GenericArgsRef<'tcx>, @@ -139,14 +150,16 @@ pub fn try_const_to_term<'tcx>( if ctx.def_kind(def_id) == DefKind::ConstParam { return None; } - let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst); - let ty = ctx.tcx.normalize_erasing_regions(typing_env, ty); - let span = ctx.def_span(def_id); - let uneval = ty::UnevaluatedConst::new(def_id, subst); - match ctx.const_eval_resolve_for_typeck(typing_env, uneval, span) { - Ok(Ok(val)) => valtree_to_term(val, ctx, ty, typing_env, span), - _ => try_const_synonym(def_id, subst, ctx, typing_env), + if !is_no_simp(ctx.tcx, def_id) { + let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst); + let ty = ctx.tcx.normalize_erasing_regions(typing_env, ty); + let span = ctx.def_span(def_id); + let uneval = ty::UnevaluatedConst::new(def_id, subst); + if let Ok(Ok(val)) = ctx.const_eval_resolve_for_typeck(typing_env, uneval, span) { + return valtree_to_term(val, ctx, ty, typing_env, span); + } } + try_const_synonym(def_id, subst, ctx, typing_env) } pub(crate) fn valtree_to_term<'tcx>( diff --git a/creusot/src/validate/opacity.rs b/creusot/src/validate/opacity.rs index b048b83d44..ef6feff6c6 100644 --- a/creusot/src/validate/opacity.rs +++ b/creusot/src/validate/opacity.rs @@ -23,6 +23,12 @@ struct OpacityVisitor<'a, 'tcx> { } impl OpacityVisitor<'_, '_> { + fn assert_visible_enough(&self, id: DefId, span: Span) { + if !self.is_visible_enough(id) { + self.error(id, span) + } + } + fn is_visible_enough(&self, id: DefId) -> bool { let Opacity::Transparent(op) = self.opacity else { return true }; self.ctx.visibility(id).is_at_least(op, self.ctx.tcx) @@ -49,33 +55,23 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { if matches!(self.ctx.def_kind(id), DefKind::ConstParam) { return; } - if !self.is_visible_enough(id) { - self.error(id, term.span) - } + self.assert_visible_enough(id, term.span); } &TermKind::Call { id, .. } => { - if !self.is_visible_enough(id) { - self.error(id, term.span) - } + self.assert_visible_enough(id, term.span); } &TermKind::Constructor { variant, .. } => { if let Some(adt) = term.ty.ty_adt_def() { - if !self.is_visible_enough(adt.did()) { - self.error(adt.did(), term.span); - } + self.assert_visible_enough(adt.did(), term.span); for fld in &adt.variant(variant).fields { - if !self.is_visible_enough(fld.did) { - self.error(fld.did, term.span); - } + self.assert_visible_enough(fld.did, term.span); } } } &TermKind::Projection { idx, ref lhs } => { if let Some(adt) = lhs.ty.ty_adt_def() { let fdid = adt.non_enum_variant().fields[idx].did; - if !self.is_visible_enough(fdid) { - self.error(fdid, term.span); - } + self.assert_visible_enough(fdid, term.span); } } &TermKind::Reborrow { ref projections, ref inner } => { @@ -89,9 +85,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { && adt.is_struct() { let fdid = adt.non_enum_variant().fields[*field_idx].did; - if !self.is_visible_enough(fdid) { - self.error(fdid, term.span); - } + self.assert_visible_enough(fdid, term.span); } } ProjectionElem::Deref | ProjectionElem::Index(_) => (), @@ -111,9 +105,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { let fields_def = &pat.ty.ty_adt_def().unwrap().variants()[*variant_idx].fields; for (fld, _) in patterns { let fdid = fields_def[*fld].did; - if !self.is_visible_enough(fdid) { - self.error(fdid, pat.span); - } + self.assert_visible_enough(fdid, pat.span); } } _ => (), @@ -122,8 +114,10 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> { } } -/// Forbid use of opaque type constructors and fields -struct NoOpaqueTypeAccess<'a, 'tcx> { +/// Opacity check in THIR. Check two things: +/// 1. Forbid use of opaque type constructors and fields (in logic and non-trusted program definitions) +/// 2. In consts, forbid use of less visible functions, constructors, and fields. +struct ThirOpacityVisitor<'a, 'tcx> { ctx: &'a TranslationCtx<'tcx>, thir: &'a Thir<'tcx>, } @@ -147,7 +141,7 @@ impl TranslationCtx<'_> { } } -impl<'thir, 'tcx> Visitor<'thir, 'tcx> for NoOpaqueTypeAccess<'thir, 'tcx> { +impl<'thir, 'tcx> Visitor<'thir, 'tcx> for ThirOpacityVisitor<'thir, 'tcx> { fn thir(&self) -> &'thir Thir<'tcx> { self.thir } @@ -186,7 +180,7 @@ pub(crate) fn validate_opacity<'tcx>(ctx: &TranslationCtx<'tcx>, item: DefId) { if is_logic || !is_trusted(ctx.tcx, item) { let (thir, expr) = ctx.thir_body(item.expect_local()); let thir = &thir.borrow(); - NoOpaqueTypeAccess { ctx, thir }.visit_expr(&thir[expr]); + ThirOpacityVisitor { ctx, thir }.visit_expr(&thir[expr]); } if is_logic && !is_opaque(ctx.tcx, item) { let Some(Scoped(_, term)) = ctx.term(item) else { return }; diff --git a/tests/should_fail/bug/2009.coma b/tests/should_fail/bug/2009.coma new file mode 100644 index 0000000000..df3ab50d77 --- /dev/null +++ b/tests/should_fail/bug/2009.coma @@ -0,0 +1,73 @@ +module M_p__C + use creusot.int.UInt64 + use creusot.prelude.Any + + type t_S = { f0: UInt64.t } + + predicate invariant_S (self: t_S) = UInt64.t'int self.f0 <> 0 + + predicate inv_S (_1: t_S) + + axiom inv_axiom [@rewrite]: forall x: t_S [inv_S x]. inv_S x = invariant_S x + + meta "compute_max_steps" 1000000 + + meta "select_lsinst" "all" + + let rec const_C (return (x: t_S)) = (! bb0 + [ bb0 = s0 [ s0 = [ &_ret <- { f0 = (0: UInt64.t) } ] s1 | s1 = return {_ret} ] ] [ & _ret: t_S = Any.any_l () ]) + [ return (result: t_S) -> {[@stop_split] [@expl:C result type invariant] inv_S result} (! return {result}) ] +end +module M_D + use creusot.prelude.Any + + type t_S + + predicate invariant_S (self: t_S) + + predicate inv_S (_1: t_S) + + axiom inv_axiom: forall x: t_S [inv_S x]. inv_S x -> invariant_S x + + constant opaque_S : t_S + + constant const_C: t_S = opaque_S + + axiom const_C_spec: inv_S const_C + + meta "compute_max_steps" 1000000 + + meta "select_lsinst" "all" + + let rec const_D (return (x: t_S)) = (! bb0 + [ bb0 = s0 [ s0 = [ &_ret <- const_C ] s1 | s1 = return {_ret} ] ] [ & _ret: t_S = Any.any_l () ]) + [ return (result: t_S) -> {[@stop_split] [@expl:D result type invariant] inv_S result} (! return {result}) ] +end +module M_f + use creusot.prelude.Any + + type t_S + + predicate invariant_S (self: t_S) + + predicate inv_S (_1: t_S) + + axiom inv_axiom: forall x: t_S [inv_S x]. inv_S x -> invariant_S x + + constant opaque_S : t_S + + constant const_D: t_S = opaque_S + + axiom const_D_spec: inv_S const_D + + meta "compute_max_steps" 1000000 + + meta "select_lsinst" "all" + + let rec f (return (x: t_S)) = (! bb0 + [ bb0 = s0 [ s0 = [ &_ret <- const_D ] s1 | s1 = return {_ret} ] ] [ & _ret: t_S = Any.any_l () ]) + [ return (result: t_S) -> + {[@stop_split] [@expl:f ensures] ([@stop_split] [@expl:f result type invariant] inv_S result) + /\ ([@stop_split] [@expl:f ensures] result = const_D)} + (! return {result}) ] +end diff --git a/tests/should_fail/bug/2009.rs b/tests/should_fail/bug/2009.rs new file mode 100644 index 0000000000..cd8f155a90 --- /dev/null +++ b/tests/should_fail/bug/2009.rs @@ -0,0 +1,30 @@ +// WHY3PROVE +extern crate creusot_std; +use creusot_std::prelude::*; + +pub mod p { + use creusot_std::prelude::*; + + pub struct S(u64); + + impl Invariant for S { + #[logic] + fn invariant(self) -> bool { + pearlite! { + self.0@ != 0 + } + } + } + + // Must fail to prove the invariant + pub const C: S = S(0); +} + +// Don't translate non-visible constructor of S: +// replace with an opaque constant and emit a warning. +pub const D: p::S = p::C; + +#[ensures(result == D)] +pub fn f() -> p::S { + D +} diff --git a/tests/should_fail/bug/2009.stderr b/tests/should_fail/bug/2009.stderr new file mode 100644 index 0000000000..9465181c53 --- /dev/null +++ b/tests/should_fail/bug/2009.stderr @@ -0,0 +1,26 @@ +warning: encountered non-visible constructor p::S + --> 2009.rs:20:5 + | +20 | pub const C: S = S(0); + | ^^^^^^^^^^^^^^ + | +note: during the translation of this function + --> 2009.rs:25:1 + | +25 | pub const D: p::S = p::C; + | ^^^^^^^^^^^^^^^^^ + +warning: encountered non-visible constructor p::S + --> 2009.rs:25:1 + | +25 | pub const D: p::S = p::C; + | ^^^^^^^^^^^^^^^^^ + | +note: during the translation of this function + --> 2009.rs:28:1 + | +28 | pub fn f() -> p::S { + | ^^^^^^^^^^^^^^^^^^ + +warning: 2 warnings emitted + diff --git a/tests/should_fail/bug/2009/why3session.xml b/tests/should_fail/bug/2009/why3session.xml new file mode 100644 index 0000000000..725e8b385e --- /dev/null +++ b/tests/should_fail/bug/2009/why3session.xml @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/tests/should_fail/bug/2009/why3shapes.gz b/tests/should_fail/bug/2009/why3shapes.gz new file mode 100644 index 0000000000..4d182efb22 Binary files /dev/null and b/tests/should_fail/bug/2009/why3shapes.gz differ diff --git a/why3/src/declaration.rs b/why3/src/declaration.rs index 58eace145f..4d215958f5 100644 --- a/why3/src/declaration.rs +++ b/why3/src/declaration.rs @@ -98,6 +98,12 @@ pub struct Signature { pub args: Box<[(Ident, Type)]>, } +impl Signature { + pub fn constant(name: Ident, ty: Type) -> Self { + Self { name, attrs: vec![], retty: Some(ty), args: [].into() } + } +} + #[derive(Debug, Clone)] #[cfg_attr(feature = "serialize", derive(Serialize, Deserialize))] pub struct LogicDefn {