diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index d341139be68..a52b6de0264 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -980,7 +980,7 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost) { bool verify = true; if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; } - if (name.Contains("INTERNAL") || name.StartsWith("reveal_")) { return true; } + if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; } } return false; } diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 21e53ea79f1..0b6199ae2bb 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -235,7 +235,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti DesugarElephantStatement(expectExtract, lhsExtract, firstType, resolver, (Method)resolutionContext.CodeContext); ResolvedStatements.ForEach(a => resolver.ResolveStatement(a, resolutionContext)); - resolver.EnsureSupportsErrorHandling(Tok, firstType, expectExtract, KeywordToken != null); + resolver.EnsureSupportsErrorHandling(Tok, firstType, expectExtract, KeywordToken?.Token.val); } public void ResolveKeywordToken(INewOrOldResolver resolver, ResolutionContext resolutionContext) { diff --git a/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs index 7e0c98223fc..cf429919606 100644 --- a/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs @@ -5,6 +5,8 @@ namespace Microsoft.Dafny; public class RevealStmt : Statement, ICloneable, ICanFormat { + public const string RevealLemmaPrefix = "reveal_"; + public readonly List Exprs; [FilledInDuringResolution] public readonly List LabeledAsserts = new List(); // to indicate that "Expr" denotes a labeled assertion [FilledInDuringResolution] public readonly List ResolvedStatements = new List(); diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index d805d398e32..8f45994d178 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2295,6 +2295,9 @@ void InheritedTraitMembers(TopLevelDeclWithMembers cl) { } else if (member.IsGhost != traitMember.IsGhost) { reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' has different ghost/compiled status than in trait '{3}'", traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name); + } else if (!member.IsOpaque && traitMember.IsOpaque) { + reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' must be 'opaque' since the member is 'opaque' in trait '{3}'", + traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name); } else { // Copy trait member's extern attribute onto class member if class does not provide one if (!Attributes.Contains(member.Attributes, "extern") && Attributes.Contains(traitMember.Attributes, "extern")) { @@ -2949,7 +2952,7 @@ public Expression makeTemp(String prefix, AssignOrReturnStmt s, ResolutionContex return id; } - public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, bool hasKeywordToken) { + public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, [CanBeNull] string keyword) { // The "method not found" errors which will be generated here were already reported while // resolving the statement, so we don't want them to reappear and redirect them into a sink. var origReporter = reporter; @@ -2959,23 +2962,22 @@ public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, var propagateFailure = ResolveMember(tok, tp, "PropagateFailure", out _); var extract = ResolveMember(tok, tp, "Extract", out _); - if (hasKeywordToken) { + if (keyword != null) { if (isFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution + var requiredMembers = expectExtract + ? "functions 'IsFailure()' and 'Extract()'" + : "function 'IsFailure()', but not 'Extract()'"; origReporter.Error(MessageSource.Resolver, tok, - "The right-hand side of ':-', which is of type '{0}', with a keyword token must have function{1}", tp, - expectExtract - ? "s 'IsFailure()' and 'Extract()'" - : " 'IsFailure()', but not 'Extract()'"); + $"The right-hand side of ':- {keyword}', which is of type '{tp}', with a keyword token must have {requiredMembers}"); } } else { if (isFailure == null || propagateFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - origReporter.Error(MessageSource.Resolver, tok, - "The right-hand side of ':-', which is of type '{0}', must have function{1}", tp, - expectExtract - ? "s 'IsFailure()', 'PropagateFailure()', and 'Extract()'" - : "s 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"); + var requiredMembers = expectExtract + ? "functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'" + : "functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"; + origReporter.Error(MessageSource.Resolver, tok, $"The right-hand side of ':-', which is of type '{tp}', must have {requiredMembers}"); } } @@ -2995,7 +2997,7 @@ void CheckIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { } CheckIsFunction(isFailure, false); - if (!hasKeywordToken) { + if (keyword == null) { CheckIsFunction(propagateFailure, true); } if (expectExtract) { @@ -3145,7 +3147,7 @@ public void ResolveLetOrFailExpr(LetOrFailExpr expr, ResolutionContext resolutio ResolveExpression(expr.ResolvedExpression, resolutionContext); expr.Type = expr.ResolvedExpression.Type; bool expectExtract = (expr.Lhs != null); - EnsureSupportsErrorHandling(expr.tok, PartiallyResolveTypeForMemberSelection(expr.tok, tempType), expectExtract, false); + EnsureSupportsErrorHandling(expr.tok, PartiallyResolveTypeForMemberSelection(expr.tok, tempType), expectExtract, null); } public static Type SelectAppropriateArrowTypeForFunction(Function function, Dictionary subst, SystemModuleManager systemModuleManager) { diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs index 492569c0f9e..d5f8eb0d73c 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs @@ -189,7 +189,7 @@ protected override void PostVisitOneExpression(Expression expr, TypeInferenceChe ? e.Function.EnclosingClass.TypeArgs[i] : e.Function.TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count]; if (!IsDetermined(p.Normalize())) { - var hint = e.Name.StartsWith("reveal_") + var hint = e.Name.StartsWith(RevealStmt.RevealLemmaPrefix) ? ". If you are making an opaque function, make sure that the function can be called." : ""; resolver.ReportError(ResolutionErrors.ErrorId.r_function_type_parameter_undetermined, e.tok, diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 6375c6efdc6..f541f12dda3 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3535,7 +3535,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext var e = (ApplySuffix)expr; var methodCallInfo = ResolveApplySuffix(e, revealResolutionContext, true); if (methodCallInfo == null) { - reporter.Error(MessageSource.Resolver, expr.tok, "expression has no reveal lemma"); + // error has already been reported } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) { reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context"); } else if (methodCallInfo.Callee.AtLabel != null) { @@ -4550,7 +4550,7 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName if (memberName == "_ctor") { reporter.Error(MessageSource.Resolver, tok, "{0} {1} does not have an anonymous constructor", cd.WhatKind, cd.Name); } else { - reporter.Error(MessageSource.Resolver, tok, "member '{0}' does not exist in {2} '{1}'", memberName, cd.Name, cd.WhatKind); + ReportMemberNotFoundError(tok, memberName, cd); } } else if (!VisibleInScope(member)) { reporter.Error(MessageSource.Resolver, tok, "member '{0}' has not been imported in this scope and cannot be accessed here", memberName); @@ -4567,6 +4567,31 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName return null; } + private void ReportMemberNotFoundError(IToken tok, string memberName, TopLevelDecl receiverDecl) { + if (memberName.StartsWith(RevealStmt.RevealLemmaPrefix)) { + var nameToBeRevealed = memberName[RevealStmt.RevealLemmaPrefix.Length..]; + var members = receiverDecl is TopLevelDeclWithMembers topLevelDeclWithMembers ? GetClassMembers(topLevelDeclWithMembers) : null; + if (members == null) { + reporter.Error(MessageSource.Resolver, tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (!members.TryGetValue(nameToBeRevealed, out var member)) { + reporter.Error(MessageSource.Resolver, tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (member is not (ConstantField or Function)) { + Contract.Assert(!member.IsOpaque); + reporter.Error(MessageSource.Resolver, tok, + $"a {member.WhatKind} ('{nameToBeRevealed}') cannot be revealed; only opaque constants and functions can be revealed"); + } else if (!member.IsOpaque) { + reporter.Error(MessageSource.Resolver, tok, $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it is not opaque"); + } else if (member is Function { Body: null }) { + reporter.Error(MessageSource.Resolver, tok, + $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else { + reporter.Error(MessageSource.Resolver, tok, $"cannot reveal '{nameToBeRevealed}'"); + } + } else { + reporter.Error(MessageSource.Resolver, tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } + } + /// /// Roughly speaking, tries to figure out the head of the type of "t", making as few inference decisions as possible. /// More precisely, returns a type that contains all the members of "t"; or if "memberName" is non-null, a type @@ -5301,7 +5326,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List { if (e.Rhs.PreType.NormalizeWrtScope() is DPreType receiverPreType) { bool expectExtract = e.Lhs != null; - EnsureSupportsErrorHandling(e.tok, receiverPreType, expectExtract); + EnsureSupportsErrorHandling(e.tok, receiverPreType, expectExtract, resolutionContext, null); return true; } return false; @@ -1055,7 +1056,8 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E /// "receiverPreType" is an unresolved proxy type and that, after solving more type constraints, "receiverPreType" /// eventually gets set to a type more specific than "tentativeReceiverType". /// - (MemberDecl/*?*/, DPreType/*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName, bool reportErrorOnMissingMember = true) { + (MemberDecl /*?*/, DPreType /*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName, ResolutionContext resolutionContext, + bool reportErrorOnMissingMember = true) { Contract.Requires(tok != null); Contract.Requires(receiverPreType != null); Contract.Requires(memberName != null); @@ -1077,7 +1079,7 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E } else if (memberName == "_ctor") { ReportError(tok, $"{receiverDecl.WhatKind} '{receiverDecl.Name}' does not have an anonymous constructor"); } else { - ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + ReportMemberNotFoundError(tok, memberName, members, receiverDecl, resolutionContext); } return (null, null); } else if (resolver.VisibleInScope(member)) { @@ -1087,11 +1089,42 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E } } if (reportErrorOnMissingMember) { - ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + ReportMemberNotFoundError(tok, memberName, null, receiverDecl, resolutionContext); } return (null, null); } + private void ReportMemberNotFoundError(IToken tok, string memberName, [CanBeNull] Dictionary members, + TopLevelDecl receiverDecl, ResolutionContext resolutionContext) { + if (memberName.StartsWith(RevealStmt.RevealLemmaPrefix)) { + var nameToBeRevealed = memberName[RevealStmt.RevealLemmaPrefix.Length..]; + if (members == null) { + if (receiverDecl is TopLevelDeclWithMembers receiverDeclWithMembers) { + // try this instead: + members = resolver.GetClassMembers(receiverDeclWithMembers); + } + } + if (members == null) { + ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (!members.TryGetValue(nameToBeRevealed, out var member)) { + ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else if (member is not (ConstantField or Function)) { + Contract.Assert(!member.IsOpaque); + ReportError(tok, + $"a {member.WhatKind} ('{nameToBeRevealed}') cannot be revealed; only opaque constants and functions can be revealed"); + } else if (!member.IsOpaque) { + ReportError(tok, $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it is not opaque"); + } else if (member is Function { Body: null }) { + ReportError(tok, + $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } else { + ReportError(tok, $"cannot reveal '{nameToBeRevealed}'"); + } + } else { + ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'"); + } + } + /// /// Look up expr.Name in the following order: /// 0. Local variable, parameter, or bound variable. @@ -1140,7 +1173,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List pair; - var name = resolutionContext.InReveal ? "reveal_" + expr.Name : expr.Name; + var name = resolutionContext.InReveal ? RevealStmt.RevealLemmaPrefix + expr.Name : expr.Name; var v = scope.Find(name); if (v != null) { // ----- 0. local variable, parameter, or bound variable @@ -1246,7 +1279,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List optTypeArguments, TopLevelDecl decl) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -1394,7 +1438,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List ResolveStatement(a, resolutionContext)); - EnsureSupportsErrorHandling(s.Tok, failureSupportingType, expectExtract, s.KeywordToken != null); + EnsureSupportsErrorHandling(s.Tok, failureSupportingType, expectExtract, s.KeywordToken?.Token.val); } - private void EnsureSupportsErrorHandling(IToken tok, TopLevelDeclWithMembers failureSupportingType, bool expectExtract, bool hasKeywordToken) { + private void EnsureSupportsErrorHandling(IToken tok, TopLevelDeclWithMembers failureSupportingType, bool expectExtract, [CanBeNull] string keyword) { var isFailure = failureSupportingType.Members.Find(x => x.Name == "IsFailure"); var propagateFailure = failureSupportingType.Members.Find(x => x.Name == "PropagateFailure"); var extract = failureSupportingType.Members.Find(x => x.Name == "Extract"); - if (hasKeywordToken) { + if (keyword != null) { if (isFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - ReportError(tok, - "The right-hand side of ':-', which is of type '{0}', with a keyword token must have function{1}", failureSupportingType, - expectExtract ? "s 'IsFailure()' and 'Extract()'" : " 'IsFailure()', but not 'Extract()'"); + var requiredMembers = expectExtract + ? "functions 'IsFailure()' and 'Extract()'" + : "function 'IsFailure()', but not 'Extract()'"; + ReportError(tok, $"The right-hand side of ':- {keyword}', which is of type '{failureSupportingType}', must have {requiredMembers}"); } } else { if (isFailure == null || propagateFailure == null || (extract != null) != expectExtract) { // more details regarding which methods are missing have already been reported by regular resolution - ReportError(tok, - "The right-hand side of ':-', which is of type '{0}', must have function{1}", failureSupportingType, - expectExtract - ? "s 'IsFailure()', 'PropagateFailure()', and 'Extract()'" - : "s 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"); + var requiredMembers = expectExtract + ? "functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'" + : "functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'"; + ReportError(tok, $"The right-hand side of ':-', which is of type '{failureSupportingType}', must have {requiredMembers}"); } } - void checkIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { - if (memberDecl == null || memberDecl is Function) { + void CheckIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { + if (memberDecl is null or Function) { // fine } else if (allowMethod && memberDecl is Method) { // give a deprecation warning, so we will remove this language feature around the Dafny 4 time frame @@ -1153,12 +1153,12 @@ void checkIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) { } } - checkIsFunction(isFailure, false); - if (!hasKeywordToken) { - checkIsFunction(propagateFailure, true); + CheckIsFunction(isFailure, false); + if (keyword == null) { + CheckIsFunction(propagateFailure, true); } if (expectExtract) { - checkIsFunction(extract, true); + CheckIsFunction(extract, true); } } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index 03cae71f617..2956b8f13a5 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -1433,7 +1433,8 @@ void ResolveMethod(Method m) { void ResolveFrameExpression(FrameExpression fe, FrameExpressionUse use, ICodeContext codeContext) { Contract.Requires(fe != null); Contract.Requires(codeContext != null); - ResolveExpression(fe.E, new ResolutionContext(codeContext, codeContext is TwoStateLemma || use == FrameExpressionUse.Unchanged)); + var resolutionContext = new ResolutionContext(codeContext, codeContext is TwoStateLemma || use == FrameExpressionUse.Unchanged); + ResolveExpression(fe.E, resolutionContext); Constraints.AddGuardedConstraint(() => { DPreType dp = fe.E.PreType.NormalizeWrtScope() as DPreType; if (dp == null) { @@ -1489,7 +1490,7 @@ void ResolveFrameExpression(FrameExpression fe, FrameExpressionUse use, ICodeCon } if (fe.FieldName != null) { - var (member, tentativeReceiverType) = FindMember(fe.E.tok, dp, fe.FieldName); + var (member, tentativeReceiverType) = FindMember(fe.E.tok, dp, fe.FieldName, resolutionContext); Contract.Assert((member == null) == (tentativeReceiverType == null)); // follows from contract of FindMember if (member == null) { // error has already been reported by FindMember diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index f6e82185503..b1ce6ecb2ff 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -339,7 +339,7 @@ protected override void VisitOneExpr(Expression expr) { ? e.Function.EnclosingClass.TypeArgs[i] : e.Function.TypeArgs[i - e.PreTypeApplication_AtEnclosingClass.Count]; if (!IsDetermined(p)) { - var hint = e.Name.StartsWith("reveal_") ? ". If you are making an opaque function, make sure that the function can be called." : ""; + var hint = e.Name.StartsWith(RevealStmt.RevealLemmaPrefix) ? ". If you are making an opaque function, make sure that the function can be called." : ""; cus.ReportError(e.tok, $"type parameter '{tp.Name}' (inferred to be '{p}') in the function call to '{e.Name}' could not be determined{hint}"); } else { CheckContainsNoOrdinal(e.tok, p, $"type parameter '{tp.Name}' (passed in as '{p}') to function call '{e.Name}' is not allowed to use ORDINAL"); diff --git a/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs b/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs index 78954d797e8..600dd294e70 100644 --- a/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs +++ b/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs @@ -313,7 +313,7 @@ public static RevealStmt BuildRevealStmt(Function func, IToken tok, ModuleDefini var callableClass = ((TopLevelDeclWithMembers)func.EnclosingClass); - var callableName = "reveal_" + func.Name; + var callableName = RevealStmt.RevealLemmaPrefix + func.Name; var member = callableClass.Members.Find(decl => decl.Name == callableName); Type.PushScope(callableClass.EnclosingModuleDefinition.VisibilityScope); diff --git a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs index a7d78d5a87c..55afa68a9d6 100644 --- a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs +++ b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs @@ -147,12 +147,14 @@ private void GenerateRevealLemma(MemberDecl m, List newDecls) { } Method reveal; if (m is TwoStateFunction) { - reveal = new TwoStateLemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend("reveal_"), isStatic, new List(), new List(), new List(), new List(), + reveal = new TwoStateLemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend(RevealStmt.RevealLemmaPrefix), isStatic, + new List(), new List(), new List(), new List(), new Specification(), new Specification(), ens, new Specification(new List(), null), null, lemma_attrs, null); } else { - reveal = new Lemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend("reveal_"), isStatic, new List(), new List(), new List(), new List(), - new Specification(), new Specification(), ens, + reveal = new Lemma(m.RangeToken.MakeAutoGenerated(), m.NameNode.Prepend(RevealStmt.RevealLemmaPrefix), isStatic, new List(), + new List(), new List(), new List(), + new Specification(), new Specification(), ens, new Specification(new List(), null), null, lemma_attrs, null); } newDecls.Add(reveal); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 4beb245faff..d85264a3933 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -1263,9 +1263,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti reveal = new Boogie.IdentifierExpr(f.tok, revealVar); argsJF.Add(reveal); } else if (overridingFunction.IsOpaque || overridingFunction.IsMadeImplicitlyOpaque(options)) { - // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel. - // Instead, we do the next best thing: use the literal false. - reveal = new Boogie.LiteralExpr(f.tok, false); + reveal = GetRevealConstant(overridingFunction); } // Add heap arguments diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 076720cf9dc..c95a78b7be7 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1039,10 +1039,18 @@ private void CreateRevealableConstant(Function f) { if (!this.functionReveals.ContainsKey(f)) { // const reveal_FunctionA : bool Bpl.Constant revealTrigger = - new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "reveal_" + f.FullName, Bpl.Type.Bool), false); + new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, RevealStmt.RevealLemmaPrefix + f.FullName, Bpl.Type.Bool), false); sink.AddTopLevelDeclaration(revealTrigger); Bpl.Expr revealTrigger_expr = new Bpl.IdentifierExpr(f.tok, revealTrigger); this.functionReveals[f] = revealTrigger_expr; + + // If this is an override, generate: + // axiom reveal_FunctionA ==> reveal_FunctionParent; + if (f.OverriddenFunction is { IsOpaque: true }) { + var revealParent = GetRevealConstant(f.OverriddenFunction); + var implication = BplImp(revealTrigger_expr, revealParent); + AddOtherDefinition(revealTrigger, new Axiom(f.tok, implication)); + } } } diff --git a/Source/DafnyDriver/DafnyDoc.cs b/Source/DafnyDriver/DafnyDoc.cs index 6bc09cd9eb3..5688801be13 100644 --- a/Source/DafnyDriver/DafnyDoc.cs +++ b/Source/DafnyDriver/DafnyDoc.cs @@ -805,7 +805,7 @@ public static string AttrString(Attributes attr) { } public static bool IsGeneratedName(string name) { - return (name.Length > 1 && name[0] == '_') || name.StartsWith("reveal_"); + return (name.Length > 1 && name[0] == '_') || name.StartsWith(RevealStmt.RevealLemmaPrefix); } public string IndentedHtml(string docstring, bool nothingIfNull = false) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect index 85b8080068a..83f1d8d2413 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy.expect @@ -5,9 +5,9 @@ LabeledAssertsResolution.dfy(26,26): Error: assert label shadows a dominating la LabeledAssertsResolution.dfy(28,13): Error: assert label shadows a dominating label LabeledAssertsResolution.dfy(34,24): Error: assert label shadows a dominating label LabeledAssertsResolution.dfy(73,12): Error: break label is undefined or not in scope: ABC -LabeledAssertsResolution.dfy(81,17): Error: cannot reveal 'C' because no constant, assert label, or requires label in the current scope is named 'C' +LabeledAssertsResolution.dfy(81,17): Error: cannot reveal 'C' because no revealable constant, function, assert label, or requires label in the current scope is named 'C' LabeledAssertsResolution.dfy(94,17): Error: no label 'XYZ' in scope at this time -LabeledAssertsResolution.dfy(115,14): Error: cannot reveal 'X' because no constant, assert label, or requires label in the current scope is named 'X' +LabeledAssertsResolution.dfy(115,14): Error: cannot reveal 'X' because no revealable constant, function, assert label, or requires label in the current scope is named 'X' LabeledAssertsResolution.dfy(52,11): Error: assert label shadows a dominating label LabeledAssertsResolution.dfy(54,11): Error: assert label shadows a dominating label LabeledAssertsResolution.dfy(125,6): Error: an assert-by body is not allowed to update a variable it doesn't declare diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy index a646da421d7..36a4fd53cbf 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy @@ -36,15 +36,15 @@ trait BadOutcome3 { } method TestMissingMethods1(o: BadOutcome1) returns (res: BadOutcome1) { - var a :- o; return o; // TODO infers 'BadOutcome1?' for RHS of ':-' instead of 'BadOutcome1' (should not infer nullable) + var a :- o; return o; } method TestMissingMethods2(o: BadOutcome2) returns (res: BadOutcome2) { - var a :- o; return o; // TODO infers 'BadOutcome2?' for RHS of ':-' instead of 'BadOutcome2' (should not infer nullable) + var a :- o; return o; } method TestMissingMethods3(o: BadOutcome3) returns (res: BadOutcome3) { - var a :- o; return o; // TODO infers 'BadOutcome3?' for RHS of ':-' instead of 'BadOutcome3' (should not infer nullable) + var a :- o; return o; } method TestTypecheckingInDesugaredTerm_Void() returns (res: VoidOutcome) { @@ -78,3 +78,13 @@ method TestMissingVoidMethods2(o: BadVoidOutcome2) returns (res: BadVoidOutcome2 method TestMissingVoidMethods3(o: BadVoidOutcome3) returns (res: BadVoidOutcome3) { :- o; return o; } + +method TestMissingMethods2WithKeyword(o: BadOutcome2) returns (res: BadOutcome2) { + var a :- assert o; // with "assert" keyword, it's fine that PropagateFailure is missing + return o; +} + +method TestMissingVoidMethods2WithKeyword(o: BadVoidOutcome2) returns (res: BadVoidOutcome2) { + :- assert o; // with "assert" keyword, it's fine that PropagateFailure is missing + return o; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy.expect index d641ad7253a..0fcffd944ea 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy.expect @@ -94,8 +94,7 @@ ExportResolve.dfy(288,39): Error: member 'u' has not been imported in this scope ExportResolve.dfy(290,18): Error: type of corresponding source/RHS (G.Trait) does not match type of bound variable (object?) ExportResolve.dfy(290,46): Error: type of corresponding source/RHS (G.Klass) does not match type of bound variable (object?) ExportResolve.dfy(298,19): Error: member '_ctor' has not been imported in this scope and cannot be accessed here -ExportResolve.dfy(342,15): Error: unresolved identifier: reveal_OpaqueFunction -ExportResolve.dfy(342,29): Error: expression has no reveal lemma +ExportResolve.dfy(342,15): Error: cannot reveal 'OpaqueFunction' because no revealable constant, function, assert label, or requires label in the current scope is named 'OpaqueFunction' ExportResolve.dfy(414,15): Error: member 'Q' has not been imported in this scope and cannot be accessed here ExportResolve.dfy(410,8): Error: RHS (of type C.X) not assignable to LHS (of type C.Z) ExportResolve.dfy(411,8): Error: RHS (of type A.T) not assignable to LHS (of type C.Z) @@ -118,4 +117,4 @@ ExportResolve.dfy(620,11): Error: new can be applied only to class types (got S. ExportResolve.dfy(624,18): Error: member 'u' has not been imported in this scope and cannot be accessed here ExportResolve.dfy(634,6): Error: when allocating an object of type 'D', one of its constructor methods must be called ExportResolve.dfy(637,10): Error: when allocating an object of imported type 'E', one of its constructor methods must be called -120 resolution/type errors detected in ExportResolve.dfy +119 resolution/type errors detected in ExportResolve.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect index 21fcaa9a765..9396a9549b2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804d.dfy.expect @@ -1,5 +1,5 @@ -git-issue-3804d.dfy(12,37): Error: cannot reveal 'q' because no constant, assert label, or requires label in the current scope is named 'q' -git-issue-3804d.dfy(16,34): Error: cannot reveal 'p' because no constant, assert label, or requires label in the current scope is named 'p' -git-issue-3804d.dfy(18,9): Error: cannot reveal 'q' because no constant, assert label, or requires label in the current scope is named 'q' -git-issue-3804d.dfy(18,12): Error: cannot reveal 'p' because no constant, assert label, or requires label in the current scope is named 'p' +git-issue-3804d.dfy(12,37): Error: cannot reveal 'q' because no revealable constant, function, assert label, or requires label in the current scope is named 'q' +git-issue-3804d.dfy(16,34): Error: cannot reveal 'p' because no revealable constant, function, assert label, or requires label in the current scope is named 'p' +git-issue-3804d.dfy(18,9): Error: cannot reveal 'q' because no revealable constant, function, assert label, or requires label in the current scope is named 'q' +git-issue-3804d.dfy(18,12): Error: cannot reveal 'p' because no revealable constant, function, assert label, or requires label in the current scope is named 'p' 4 resolution/type errors detected in git-issue-3804d.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy new file mode 100644 index 00000000000..bae69ef1d7d --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy @@ -0,0 +1,138 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=datatype + +module True { + trait A { + ghost predicate Valid() + } + + trait B extends A { + ghost opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } +} + +module X { + trait A { + ghost predicate Valid(w: bool) + } + + trait B extends A { + ghost opaque predicate Valid(x: bool) { x } + } + + method TestByRequires(b: B, y: bool) + requires b.Valid(y) + { + var a: A := b; + assert a.Valid(y); + } + + method TestByReveal(b: B, y: bool) { + var a: A := b; + assert a.Valid(y) by { // error: assertion violation + reveal b.Valid(); + } + } +} + +module Parameters { + trait A { + ghost predicate P(t: T) + } + + trait B extends A { + ghost opaque predicate P(t: T) { t == t } + } + + + method TestByRequires(b: B) + requires b.P(5) + { + var a: A := b; + assert a.P(5); + } + + method TestByRequires'(b: B) + requires b.P(6) + { + var a: A := b; + assert a.P(5); // error: assertion violation + } + + method TestByRequires''(b: B) + requires b.P(true) + { + var a: A := b; + assert a.P(5); // error: assertion violation + } + + + method TestByReveal(b: B) { + var a: A := b; + assert a.P(5) by { + reveal b.P(); + } + } + + method TestByReveal'(b: B) { + var a: A := b; + assert a.P(true) by { + reveal b.P(); + } + } +} + +module StayOpaque { + trait A { + opaque predicate Valid() + } + + trait B extends A { + opaque predicate Valid() { true } + } + + trait C extends A { + opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } + + method TestIndependence0(b: B, c: C) { + var a: A := b; + assert b.Valid() by { // error: revealing for C should not affect B + reveal c.Valid(); + } + } + + method TestIndependence1(b: B, c: C) { + var a: A := b; + assert a.Valid() by { // fine: revealing for C also reveals for all A's + reveal c.Valid(); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect new file mode 100644 index 00000000000..8731f53b7d9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017a.dfy.expect @@ -0,0 +1,6 @@ +git-issue-5017a.dfy(45,18): Error: assertion might not hold +git-issue-5017a.dfy(72,14): Error: assertion might not hold +git-issue-5017a.dfy(79,14): Error: assertion might not hold +git-issue-5017a.dfy(127,18): Error: assertion might not hold + +Dafny program verifier finished with 14 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy new file mode 100644 index 00000000000..e3df9d6e840 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy @@ -0,0 +1,147 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype + +module Opaque { + trait A { + predicate Valid() + } + + trait B { + opaque predicate Valid() { true } + } + + trait C { + opaque predicate Valid() + } + + + trait K0 extends A { + predicate Valid() + } + trait K1 extends A { + opaque predicate Valid() + } + trait K2 extends A { + predicate Valid() { true } + } + trait K3 extends A { + opaque predicate Valid() { true } + } + + trait L0 extends B { + predicate Valid() { true } // error: B.Valid already has a body + } + trait L1 extends B { + opaque predicate Valid() { true } // error: B.Valid already has a body + } + + trait M0 extends C { + predicate Valid() // error: must be opaque (since it is in C) + } + trait M1 extends C { + opaque predicate Valid() + } + trait M2 extends C { + predicate Valid() { true } // error: must be opaque (since it is in C) + } + trait M3 extends C { + opaque predicate Valid() { true } + } + + + datatype W0 extends A = W0 { + predicate Valid() { true } + } + class W1 extends A { + predicate Valid() { true } + } + + datatype X0 extends A = X0 { + opaque predicate Valid() { true } + } + class X1 extends A { + opaque predicate Valid() { true } + } + + datatype Y0 extends C = Y0 { + predicate Valid() { true } // error: must be opaque (since it is in C) + } + class Y1 extends C { + predicate Valid() { true } // error: must be opaque (since it is in C) + } + + datatype Z0 extends C = Z0 { + opaque predicate Valid() { true } + } + class Z1 extends C { + opaque predicate Valid() { true } + } +} + +module StayOpaque { + trait A { + opaque predicate Valid() + } + + datatype B extends A = B { + opaque predicate Valid() { true } + } + + class C extends A { + opaque predicate Valid() { true } + } + + method TestA(a: A) { + reveal a.Valid(); // error: cannot reveal (no body) + } + + method TestB(b: B) { + reveal b.Valid(); + } + + method TestC(c: C) { + reveal c.Valid(); + } +} + +module RevealErrorMessages { + trait A { + opaque predicate Valid() + function TransparentFunction(): int { 3 } + const m: int := 10 + opaque const n: int := 10 + opaque const o: int + method Method() { } + opaque function WithBody(x: int): int { x } + + method TestReveal() { + reveal UnknownFunction(); // error: UnknownFunction unresolved + reveal UnknownFunction; // error: UnknownFunction unresolved + reveal Method(); // error: Method unresolved + reveal Method; // error: Method unresolved + reveal m; // error: m unresolved + reveal n; + reveal o; + reveal Valid(); // error: Valid unresolved + reveal Valid; // error: Valid unresolved + reveal WithBody(); + reveal WithBody; // error: missing parens + } + } + + method TestA(a: A) { + reveal x.Valid(); // error: 'x' is unresolved + reveal a.UnknownFunction(); // error: UnknownFunction unresolved + reveal a.UnknownFunction; // error: UnknownFunction unresolved + reveal a.Method(); // error: cannot reveal a method + reveal a.Method; + reveal a.m; // error: cannot reveal (not opaque) + reveal a.n; + reveal a.o; + reveal a.Valid(); // error: cannot reveal (no body) + reveal a.Valid; // error: cannot reveal (no body) + reveal a.WithBody(); + reveal a.WithBody; // error: missing parens + + reveal A.WithBody(); // error: WithBody not found (as static member) in A + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect new file mode 100644 index 00000000000..b0a74d69a31 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.expect @@ -0,0 +1,26 @@ +git-issue-5017b.dfy(31,14): Error: fully defined predicate 'Valid' is inherited from trait 'B' and is not allowed to be re-declared +git-issue-5017b.dfy(34,21): Error: fully defined predicate 'Valid' is inherited from trait 'B' and is not allowed to be re-declared +git-issue-5017b.dfy(34,21): Error: static lemma 'reveal_Valid' is inherited from trait 'B' and is not allowed to be re-declared +git-issue-5017b.dfy(38,14): Error: overridden predicate 'Valid' in 'M0' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(44,14): Error: overridden predicate 'Valid' in 'M2' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(66,14): Error: overridden predicate 'Valid' in 'Y0' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(69,14): Error: overridden predicate 'Valid' in 'Y1' must be 'opaque' since the member is 'opaque' in trait 'C' +git-issue-5017b.dfy(94,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' +git-issue-5017b.dfy(132,11): Error: unresolved identifier: x +git-issue-5017b.dfy(133,13): Error: member 'UnknownFunction' does not exist in trait 'A' +git-issue-5017b.dfy(134,13): Error: member 'UnknownFunction' does not exist in trait 'A' +git-issue-5017b.dfy(135,13): Error: a method ('Method') cannot be revealed; only opaque constants and functions can be revealed +git-issue-5017b.dfy(136,13): Error: a method ('Method') cannot be revealed; only opaque constants and functions can be revealed +git-issue-5017b.dfy(137,13): Error: const field 'm' cannot be revealed, because it is not opaque +git-issue-5017b.dfy(140,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' +git-issue-5017b.dfy(141,13): Error: predicate 'Valid' cannot be revealed, because it has no body in trait 'A' +git-issue-5017b.dfy(143,13): Error: to reveal a function (WithBody), append parentheses +git-issue-5017b.dfy(117,13): Error: cannot reveal 'UnknownFunction' because no revealable constant, function, assert label, or requires label in the current scope is named 'UnknownFunction' +git-issue-5017b.dfy(118,13): Error: cannot reveal 'UnknownFunction' because no revealable constant, function, assert label, or requires label in the current scope is named 'UnknownFunction' +git-issue-5017b.dfy(119,13): Error: cannot reveal 'Method' because no revealable constant, function, assert label, or requires label in the current scope is named 'Method' +git-issue-5017b.dfy(120,13): Error: cannot reveal 'Method' because no revealable constant, function, assert label, or requires label in the current scope is named 'Method' +git-issue-5017b.dfy(121,13): Error: cannot reveal 'm' because no revealable constant, function, assert label, or requires label in the current scope is named 'm' +git-issue-5017b.dfy(124,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid' +git-issue-5017b.dfy(125,13): Error: cannot reveal 'Valid' because no revealable constant, function, assert label, or requires label in the current scope is named 'Valid' +git-issue-5017b.dfy(127,13): Error: to reveal a function (WithBody), append parentheses +25 resolution/type errors detected in git-issue-5017b.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy new file mode 100644 index 00000000000..32f945566c0 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy @@ -0,0 +1,86 @@ +// RUN: %exits-with 4 %verify --type-system-refresh --general-traits=datatype "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Datatype { + trait A { + opaque predicate Valid() + } + + datatype B extends A = B { + opaque predicate Valid() { true } + } + + datatype C extends A = C { + opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } + + method TestIndependence0(b: B, c: C) { + var a: A := b; + assert b.Valid() by { // error: revealing for C should not affect B + reveal c.Valid(); + } + } + + method TestIndependence1(b: B, c: C) { + var a: A := b; + assert a.Valid() by { // fine: revealing for C also reveals for all A's + reveal c.Valid(); + } + } +} + +module Class { + trait A { + opaque predicate Valid() + } + + class B extends A { + opaque predicate Valid() { true } + } + + class C extends A { + opaque predicate Valid() { true } + } + + method TestByRequires(b: B) + requires b.Valid() + { + var a: A := b; + assert a.Valid(); + } + + method TestByReveal(b: B) { + var a: A := b; + assert a.Valid() by { + reveal b.Valid(); + } + } + + method TestIndependence0(b: B, c: C) { + var a: A := b; + assert b.Valid() by { // error: revealing for C should not affect B + reveal c.Valid(); + } + } + + method TestIndependence1(b: B, c: C) { + var a: A := b; + assert a.Valid() by { // fine: revealing for C also reveals for all A's + reveal c.Valid(); + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect new file mode 100644 index 00000000000..a8af3f86f5a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017c.dfy.expect @@ -0,0 +1,4 @@ +git-issue-5017c.dfy(33,18): Error: assertion might not hold +git-issue-5017c.dfy(75,18): Error: assertion might not hold + +Dafny program verifier finished with 11 verified, 2 errors diff --git a/docs/dev/news/5111.fix b/docs/dev/news/5111.fix new file mode 100644 index 00000000000..7f2a4cb3650 --- /dev/null +++ b/docs/dev/news/5111.fix @@ -0,0 +1,3 @@ +Let verifier understand opaque function overrides, supporting both when the overridden function is opaque and non-opaque. Revealing such a function for one overriding type has the effect of revealing it for all overriding types. + +Also, forbid the case where a function is opaque in a parent trait and the function override is not opaque. (Previously, this had caused a crash.)