diff --git a/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs index b3f86cdce3..47b8c19789 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs @@ -66,16 +66,16 @@ public override bool IsImplicit { /// gives a way to distinguish this receiver from other receivers, which /// plays a role in checking the restrictions on divided block statements. /// -public class ImplicitThisExpr_ConstructorCall : ImplicitThisExpr, ICloneable { - public ImplicitThisExpr_ConstructorCall(Cloner cloner, ImplicitThisExpr_ConstructorCall original) : base(cloner, original) { +public class ImplicitThisExprConstructorCall : ImplicitThisExpr, ICloneable { + public ImplicitThisExprConstructorCall(Cloner cloner, ImplicitThisExprConstructorCall original) : base(cloner, original) { } - public ImplicitThisExpr_ConstructorCall(IOrigin tok) + public ImplicitThisExprConstructorCall(IOrigin tok) : base(tok) { Contract.Requires(tok != null); } - public new ImplicitThisExpr_ConstructorCall Clone(Cloner cloner) { - return new ImplicitThisExpr_ConstructorCall(cloner, this); + public new ImplicitThisExprConstructorCall Clone(Cloner cloner) { + return new ImplicitThisExprConstructorCall(cloner, this); } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs similarity index 75% rename from Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs rename to Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs index e2bffc357b..11de95a29f 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; /// /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments. /// -class Resolver_IdentifierExpr : Expression, IHasReferences, ICloneable { +class ResolverIdentifierExpr : Expression, IHasReferences, ICloneable { public readonly TopLevelDecl Decl; public readonly List TypeArgs; [ContractInvariantMethod] @@ -16,10 +16,10 @@ void ObjectInvariant() { Contract.Invariant(Decl != null); Contract.Invariant(TypeArgs != null); Contract.Invariant(TypeArgs.Count == Decl.TypeArgs.Count); - Contract.Invariant(Type is ResolverType_Module || Type is ResolverType_Type); + Contract.Invariant(Type is ResolverTypeModule or ResolverTypeType); } - public Resolver_IdentifierExpr(Cloner cloner, Resolver_IdentifierExpr original) : base(cloner, original) { + public ResolverIdentifierExpr(Cloner cloner, ResolverIdentifierExpr original) : base(cloner, original) { Decl = original.Decl; TypeArgs = original.TypeArgs; } @@ -38,38 +38,38 @@ public override Type ReplaceTypeArguments(List arguments) { throw new NotSupportedException(); } } - public class ResolverType_Module : ResolverType { + public class ResolverTypeModule : ResolverType { [System.Diagnostics.Contracts.Pure] public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) { Contract.Assert(parseAble == false); return "#module"; } public override bool Equals(Type that, bool keepConstraints = false) { - return that.NormalizeExpand(keepConstraints) is ResolverType_Module; + return that.NormalizeExpand(keepConstraints) is ResolverTypeModule; } } - public class ResolverType_Type : ResolverType { + public class ResolverTypeType : ResolverType { [System.Diagnostics.Contracts.Pure] public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) { Contract.Assert(parseAble == false); return "#type"; } public override bool Equals(Type that, bool keepConstraints = false) { - return that.NormalizeExpand(keepConstraints) is ResolverType_Type; + return that.NormalizeExpand(keepConstraints) is ResolverTypeType; } } - public Resolver_IdentifierExpr(IOrigin origin, TopLevelDecl decl, List typeArgs) + public ResolverIdentifierExpr(IOrigin origin, TopLevelDecl decl, List typeArgs) : base(origin) { Contract.Requires(origin != null); Contract.Requires(decl != null); Contract.Requires(typeArgs != null && typeArgs.Count == decl.TypeArgs.Count); Decl = decl; TypeArgs = typeArgs; - Type = decl is ModuleDecl ? (Type)new ResolverType_Module() : new ResolverType_Type(); + Type = decl is ModuleDecl ? (Type)new ResolverTypeModule() : new ResolverTypeType(); PreType = decl is ModuleDecl ? new PreTypePlaceholderModule() : new PreTypePlaceholderType(); } - public Resolver_IdentifierExpr(IOrigin origin, TypeParameter tp) + public ResolverIdentifierExpr(IOrigin origin, TypeParameter tp) : this(origin, tp, new List()) { Contract.Requires(origin != null); Contract.Requires(tp != null); @@ -79,7 +79,7 @@ public IEnumerable GetReferences() { return new[] { new Reference(Center, Decl) }; } - public Resolver_IdentifierExpr Clone(Cloner cloner) { - return new Resolver_IdentifierExpr(cloner, this); + public ResolverIdentifierExpr Clone(Cloner cloner) { + return new ResolverIdentifierExpr(cloner, this); } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs index 40f9aeee6e..a8c95483aa 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs @@ -576,12 +576,12 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, if (parensNeeded) { wr.Write("("); } if (!e.Lhs.IsImplicit) { PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword); - if (e.Lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) { + if (e.Lhs.Type is ResolverIdentifierExpr.ResolverTypeType) { Contract.Assert(e.Lhs is NameSegment || e.Lhs is ExprDotName); // these are the only expressions whose .Type can be ResolverType_Type if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) { // The printing of e.Lhs printed the type arguments only if they were given explicitly in the input. var optionalTypeArgs = e.Lhs is NameSegment ns ? ns.OptTypeArguments : ((ExprDotName)e.Lhs).OptTypeArguments; - if (optionalTypeArgs == null && e.Lhs.Resolved is Resolver_IdentifierExpr ri) { + if (optionalTypeArgs == null && e.Lhs.Resolved is ResolverIdentifierExpr ri) { PrintTypeInstantiation(ri.TypeArgs); } } @@ -1238,7 +1238,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, wr.Write("[BoogieWrapper]"); // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here } else if (expr is BoogieGenerator.BoogieFunctionCall) { wr.Write("[BoogieFunctionCall]"); // this prevents debugger watch window crash - } else if (expr is Resolver_IdentifierExpr) { + } else if (expr is ResolverIdentifierExpr) { wr.Write("[Resolver_IdentifierExpr]"); // we can get here in the middle of a debugging session } else if (expr is DecreasesToExpr decreasesToExpr) { var opBindingStrength = BindingStrengthDecreasesTo; diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index f2828b49b0..b6c76c5fc5 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -1145,10 +1145,10 @@ public static bool Equal_Improved(Type a, Type b) { return true; } } - } else if (a is Resolver_IdentifierExpr.ResolverType_Module) { - return b is Resolver_IdentifierExpr.ResolverType_Module; - } else if (a is Resolver_IdentifierExpr.ResolverType_Type) { - return b is Resolver_IdentifierExpr.ResolverType_Type; + } else if (a is ResolverIdentifierExpr.ResolverTypeModule) { + return b is ResolverIdentifierExpr.ResolverTypeModule; + } else if (a is ResolverIdentifierExpr.ResolverTypeType) { + return b is ResolverIdentifierExpr.ResolverTypeType; } else { // this is an unexpected type; however, it may be that we get here during the resolution of an erroneous // program, so we'll just return false @@ -2232,7 +2232,7 @@ public void AddSubtype(TypeConstraint c) { public enum Family { Unknown, Bool, Char, IntLike, RealLike, Ordinal, BitVector, ValueType, Ref, Opaque } public Family family = Family.Unknown; public static Family GetFamily(Type t) { - Contract.Ensures(Contract.Result() != Family.Unknown || t is TypeProxy || t is Resolver_IdentifierExpr.ResolverType); // return Unknown ==> t is TypeProxy || t is ResolverType + Contract.Ensures(Contract.Result() != Family.Unknown || t is TypeProxy || t is ResolverIdentifierExpr.ResolverType); // return Unknown ==> t is TypeProxy || t is ResolverType if (t.IsBoolType) { return Family.Bool; } else if (t.IsCharType) { diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs index 302ccba971..e7076751bb 100644 --- a/Source/DafnyCore/AST/Types/UserDefinedType.cs +++ b/Source/DafnyCore/AST/Types/UserDefinedType.cs @@ -165,7 +165,7 @@ public UserDefinedType(IOrigin origin, string name, TopLevelDecl cd, [Captured] this.TypeArgs = typeArgs; if (namePath == null) { var ns = new NameSegment(origin, name, typeArgs.Count == 0 ? null : typeArgs); - var r = new Resolver_IdentifierExpr(origin, cd, typeArgs); + var r = new ResolverIdentifierExpr(origin, cd, typeArgs); ns.ResolvedExpression = r; ns.Type = r.Type; this.NamePath = ns; @@ -218,7 +218,7 @@ public UserDefinedType(IOrigin origin, TypeParameter tp) : base(origin) { this.TypeArgs = new List(); this.ResolvedClass = tp; var ns = new NameSegment(origin, tp.Name, null); - var r = new Resolver_IdentifierExpr(origin, tp); + var r = new ResolverIdentifierExpr(origin, tp); ns.ResolvedExpression = r; ns.Type = r.Type; this.NamePath = ns; diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 0d3c5a7b5f..c500840ef5 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -1606,7 +1606,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD Contract.Assert(enclosingModule == null); enclosingModule = module; var wr = CreateModule(module, module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode); - var v = new CheckHasNoAssumes_Visitor(this, wr); + var v = new CheckHasNoAssumesVisitor(this, wr); foreach (TopLevelDecl d in module.TopLevelDecls) { if (!ProgramResolver.ShouldCompile(d)) { continue; @@ -2151,7 +2151,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite Contract.Ensures(thisContext == null); var errorWr = classWriter.ErrorWriter(); - var v = new CheckHasNoAssumes_Visitor(this, errorWr); + var v = new CheckHasNoAssumesVisitor(this, errorWr); var inheritedMembers = c.InheritedMembers; OrderedBySCC(inheritedMembers, c); @@ -3263,10 +3263,10 @@ protected string DefaultValueCoercedIfNecessary(Type type, ConcreteSyntaxTree wr // ----- Stmt --------------------------------------------------------------------------------- - public class CheckHasNoAssumes_Visitor : BottomUpVisitor { + public class CheckHasNoAssumesVisitor : BottomUpVisitor { readonly SinglePassCodeGenerator codeGenerator; ConcreteSyntaxTree wr; - public CheckHasNoAssumes_Visitor(SinglePassCodeGenerator c, ConcreteSyntaxTree wr) { + public CheckHasNoAssumesVisitor(SinglePassCodeGenerator c, ConcreteSyntaxTree wr) { Contract.Requires(c != null); codeGenerator = c; this.wr = wr; diff --git a/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs b/Source/DafnyCore/Resolver/CheckDividedConstructorInitVisitor.cs similarity index 96% rename from Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs rename to Source/DafnyCore/Resolver/CheckDividedConstructorInitVisitor.cs index 42d1a6064b..0a1ece212b 100644 --- a/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckDividedConstructorInitVisitor.cs @@ -4,8 +4,8 @@ namespace Microsoft.Dafny; -class CheckDividedConstructorInit_Visitor : ResolverTopDownVisitor { - public CheckDividedConstructorInit_Visitor(ErrorReporter reporter) +class CheckDividedConstructorInitVisitor : ResolverTopDownVisitor { + public CheckDividedConstructorInitVisitor(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } @@ -65,7 +65,7 @@ protected override bool VisitOneExpr(Expression expr, ref int unused) { } } else if (expr is UnaryOpExpr { Op: UnaryOpExpr.Opcode.Assigned }) { return false; // don't continue the recursion - } else if (expr is ThisExpr && !(expr is ImplicitThisExpr_ConstructorCall)) { + } else if (expr is ThisExpr && !(expr is ImplicitThisExprConstructorCall)) { reporter.Error(MessageSource.Resolver, expr.Origin, "in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fields"); } return base.VisitOneExpr(expr, ref unused); diff --git a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs b/Source/DafnyCore/Resolver/CheckTypeCharacteristicsVisitor.cs similarity index 99% rename from Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs rename to Source/DafnyCore/Resolver/CheckTypeCharacteristicsVisitor.cs index d1dcd0cb0c..e963fbc48d 100644 --- a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckTypeCharacteristicsVisitor.cs @@ -9,8 +9,8 @@ namespace Microsoft.Dafny; /// In addition, this visitor checks that operations that require equality are applied to /// types that really do support equality; this, too, is checked only in compiled contexts. /// -class CheckTypeCharacteristics_Visitor : ResolverTopDownVisitor { - public CheckTypeCharacteristics_Visitor(ErrorReporter reporter) +class CheckTypeCharacteristicsVisitor : ResolverTopDownVisitor { + public CheckTypeCharacteristicsVisitor(ErrorReporter reporter) : base(reporter) { Contract.Requires(reporter != null); } diff --git a/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs b/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpecVisitor.cs similarity index 89% rename from Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs rename to Source/DafnyCore/Resolver/CollectFriendlyCallsInSpecVisitor.cs index dec019e8be..e632340d54 100644 --- a/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs +++ b/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpecVisitor.cs @@ -3,10 +3,10 @@ namespace Microsoft.Dafny; -class CollectFriendlyCallsInSpec_Visitor : FindFriendlyCalls_Visitor { +class CollectFriendlyCallsInSpecVisitor : FindFriendlyCallsVisitor { readonly ISet friendlyCalls; readonly ExtremeLemma Context; - public CollectFriendlyCallsInSpec_Visitor(ErrorReporter reporter, ISet friendlyCalls, bool co, ExtremeLemma context) + public CollectFriendlyCallsInSpecVisitor(ErrorReporter reporter, ISet friendlyCalls, bool co, ExtremeLemma context) : base(reporter, co, context.KNat) { Contract.Requires(reporter != null); Contract.Requires(friendlyCalls != null); diff --git a/Source/DafnyCore/Resolver/DetectUnsoundFunctionReferencesVisitor.cs b/Source/DafnyCore/Resolver/DetectUnsoundFunctionReferencesVisitor.cs new file mode 100644 index 0000000000..d3696de66b --- /dev/null +++ b/Source/DafnyCore/Resolver/DetectUnsoundFunctionReferencesVisitor.cs @@ -0,0 +1,41 @@ +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny; + +class DetectUnsoundFunctionReferencesVisitor : ResolverBottomUpVisitor { + private readonly ICallable context; + private bool doDecreasesChecks; + private DetectUnsoundFunctionReferencesVisitor(ModuleResolver resolver, ICallable context) + : base(resolver) { + Contract.Requires(resolver != null); + Contract.Requires(context != null); + this.context = context; + } + + public static void Check(Function function, ModuleResolver resolver) { + var visitor = new DetectUnsoundFunctionReferencesVisitor(resolver, function); + visitor.doDecreasesChecks = false; + visitor.Visit(function); + visitor.doDecreasesChecks = true; + visitor.Visit(function.Decreases.Expressions); + } + + protected override void VisitOneExpr(Expression expr) { + if (!doDecreasesChecks && expr is MemberSelectExpr { Member: Function fn } && ModuleDefinition.InSameSCC(context, fn)) { + resolver.reporter.Error(MessageSource.Resolver, expr.Origin, + "cannot use naked function in recursive setting. Possible solution: eta expansion."); + } + + if (doDecreasesChecks && expr is FunctionCallExpr callExpr && ModuleDefinition.InSameSCC(context, callExpr.Function)) { + string msg; + if (context == callExpr.Function) { + msg = "a decreases clause is not allowed to call the enclosing function"; + } else { + msg = $"the decreases clause of {context.WhatKind} '{context.NameRelativeToModule}' is not allowed to call '{callExpr.Function}', " + + "because they are mutually recursive"; + } + + resolver.reporter.Error(MessageSource.Resolver, callExpr.Origin, msg); + } + } +} diff --git a/Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs b/Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs new file mode 100644 index 0000000000..a67f8b3801 --- /dev/null +++ b/Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs @@ -0,0 +1,35 @@ +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny; + +class ExtremeLemmaChecksVisitor : ResolverBottomUpVisitor { + ExtremeLemma context; + public ExtremeLemmaChecksVisitor(ModuleResolver resolver, ExtremeLemma context) + : base(resolver) { + Contract.Requires(resolver != null); + Contract.Requires(context != null); + this.context = context; + } + protected override void VisitOneStmt(Statement stmt) { + if (stmt is CallStmt callStmt) { + if (callStmt.Method is ExtremeLemma or PrefixLemma) { + // all is cool + } else { + // the call goes from an extreme lemma context to a non-extreme-lemma callee + if (ModuleDefinition.InSameSCC(context, callStmt.Method)) { + // we're looking at a recursive call (to a non-extreme-lemma) + resolver.reporter.Error(MessageSource.Resolver, callStmt.Origin, "a recursive call from a {0} can go only to other {0}s and prefix lemmas", context.WhatKind); + } + } + } + } + protected override void VisitOneExpr(Expression expr) { + if (expr is FunctionCallExpr callExpr) { + // the call goes from a greatest lemma context to a non-greatest-lemma callee + if (ModuleDefinition.InSameSCC(context, callExpr.Function)) { + // we're looking at a recursive call (to a non-greatest-lemma) + resolver.reporter.Error(MessageSource.Resolver, callExpr.Origin, "a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas"); + } + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/ExtremeLemmaChecks_Visitor.cs b/Source/DafnyCore/Resolver/ExtremeLemmaChecks_Visitor.cs deleted file mode 100644 index d5277d01b2..0000000000 --- a/Source/DafnyCore/Resolver/ExtremeLemmaChecks_Visitor.cs +++ /dev/null @@ -1,37 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Dafny; - -class ExtremeLemmaChecks_Visitor : ResolverBottomUpVisitor { - ExtremeLemma context; - public ExtremeLemmaChecks_Visitor(ModuleResolver resolver, ExtremeLemma context) - : base(resolver) { - Contract.Requires(resolver != null); - Contract.Requires(context != null); - this.context = context; - } - protected override void VisitOneStmt(Statement stmt) { - if (stmt is CallStmt) { - var s = (CallStmt)stmt; - if (s.Method is ExtremeLemma || s.Method is PrefixLemma) { - // all is cool - } else { - // the call goes from an extreme lemma context to a non-extreme-lemma callee - if (ModuleDefinition.InSameSCC(context, s.Method)) { - // we're looking at a recursive call (to a non-extreme-lemma) - resolver.reporter.Error(MessageSource.Resolver, s.Origin, "a recursive call from a {0} can go only to other {0}s and prefix lemmas", context.WhatKind); - } - } - } - } - protected override void VisitOneExpr(Expression expr) { - if (expr is FunctionCallExpr) { - var e = (FunctionCallExpr)expr; - // the call goes from a greatest lemma context to a non-greatest-lemma callee - if (ModuleDefinition.InSameSCC(context, e.Function)) { - // we're looking at a recursive call (to a non-greatest-lemma) - resolver.reporter.Error(MessageSource.Resolver, e.Origin, "a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas"); - } - } - } -} \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/ExtremePredicateChecks_Visitor.cs b/Source/DafnyCore/Resolver/ExtremePredicateChecksVisitor.cs similarity index 94% rename from Source/DafnyCore/Resolver/ExtremePredicateChecks_Visitor.cs rename to Source/DafnyCore/Resolver/ExtremePredicateChecksVisitor.cs index 68a1ab8f4a..c7155662fe 100644 --- a/Source/DafnyCore/Resolver/ExtremePredicateChecks_Visitor.cs +++ b/Source/DafnyCore/Resolver/ExtremePredicateChecksVisitor.cs @@ -2,9 +2,9 @@ namespace Microsoft.Dafny; -class ExtremePredicateChecks_Visitor : FindFriendlyCalls_Visitor { +class ExtremePredicateChecksVisitor : FindFriendlyCallsVisitor { readonly ExtremePredicate context; - public ExtremePredicateChecks_Visitor(ErrorReporter reporter, ExtremePredicate context) + public ExtremePredicateChecksVisitor(ErrorReporter reporter, ExtremePredicate context) : base(reporter, context is GreatestPredicate, context.KNat) { Contract.Requires(reporter != null); Contract.Requires(context != null); diff --git a/Source/DafnyCore/Resolver/FillInDefaultLoopDecreases_Visitor.cs b/Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs similarity index 98% rename from Source/DafnyCore/Resolver/FillInDefaultLoopDecreases_Visitor.cs rename to Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs index 687c66bb91..8d65bd814a 100644 --- a/Source/DafnyCore/Resolver/FillInDefaultLoopDecreases_Visitor.cs +++ b/Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs @@ -3,9 +3,9 @@ namespace Microsoft.Dafny; -class FillInDefaultLoopDecreases_Visitor : ResolverBottomUpVisitor { +class FillInDefaultLoopDecreasesVisitor : ResolverBottomUpVisitor { readonly ICallable EnclosingMethod; - public FillInDefaultLoopDecreases_Visitor(ModuleResolver resolver, ICallable enclosingMethod) + public FillInDefaultLoopDecreasesVisitor(ModuleResolver resolver, ICallable enclosingMethod) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(enclosingMethod != null); diff --git a/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs b/Source/DafnyCore/Resolver/FindFriendlyCallsVisitor.cs similarity index 96% rename from Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs rename to Source/DafnyCore/Resolver/FindFriendlyCallsVisitor.cs index 5a27d2024e..ef34b1e920 100644 --- a/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs +++ b/Source/DafnyCore/Resolver/FindFriendlyCallsVisitor.cs @@ -4,10 +4,10 @@ namespace Microsoft.Dafny; public enum CallingPosition { Positive, Negative, Neither } -class FindFriendlyCalls_Visitor : ResolverTopDownVisitor { +class FindFriendlyCallsVisitor : ResolverTopDownVisitor { public readonly bool IsCoContext; public readonly bool ContinuityIsImportant; - public FindFriendlyCalls_Visitor(ErrorReporter reporter, bool co, bool continuityIsImportant) + public FindFriendlyCallsVisitor(ErrorReporter reporter, bool co, bool continuityIsImportant) : base(reporter) { Contract.Requires(reporter != null); this.IsCoContext = co; diff --git a/Source/DafnyCore/Resolver/FuelAdjustment.cs b/Source/DafnyCore/Resolver/FuelAdjustment.cs index bac90d5e16..b2749f6279 100644 --- a/Source/DafnyCore/Resolver/FuelAdjustment.cs +++ b/Source/DafnyCore/Resolver/FuelAdjustment.cs @@ -18,16 +18,16 @@ public static void CheckForFuelAdjustments(ErrorReporter reporter, ModuleDefinit CheckForFuelAdjustments(reporter, clbl.Origin, iteratorDecl.Attributes, module); } else if (clbl is Function function) { CheckForFuelAdjustments(reporter, clbl.Origin, function.Attributes, module); - var c = new FuelAdjustment_Visitor(reporter); + var c = new FuelAdjustmentVisitor(reporter); var bodyExpr = function.Body; if (bodyExpr != null) { - c.Visit(bodyExpr, new FuelAdjustment_Context(module)); + c.Visit(bodyExpr, new FuelAdjustmentContext(module)); } } if (body != null) { - var c = new FuelAdjustment_Visitor(reporter); - c.Visit(body, new FuelAdjustment_Context(module)); + var c = new FuelAdjustmentVisitor(reporter); + c.Visit(body, new FuelAdjustmentContext(module)); } } } @@ -68,22 +68,22 @@ public static void CheckForFuelAdjustments(ErrorReporter reporter, IOrigin tok, } } -class FuelAdjustment_Visitor : ResolverTopDownVisitor { +class FuelAdjustmentVisitor : ResolverTopDownVisitor { - public FuelAdjustment_Visitor(ErrorReporter reporter) + public FuelAdjustmentVisitor(ErrorReporter reporter) : base(reporter) { } - protected override bool VisitOneStmt(Statement stmt, ref FuelAdjustment_Context st) { + protected override bool VisitOneStmt(Statement stmt, ref FuelAdjustmentContext st) { FuelAdjustment.CheckForFuelAdjustments(reporter, stmt.Origin, stmt.Attributes, st.currentModule); return true; } } -public class FuelAdjustment_Context { +public class FuelAdjustmentContext { public ModuleDefinition currentModule; - public FuelAdjustment_Context(ModuleDefinition currentModule) { + public FuelAdjustmentContext(ModuleDefinition currentModule) { this.currentModule = currentModule; } } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index f90e8df3fb..0aa3a16515 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -115,7 +115,7 @@ public void FillInAdditionalInformation(ModuleDefinition module) { } if (body != null) { - var c = new ReportOtherAdditionalInformation_Visitor(this); + var c = new ReportOtherAdditionalInformationVisitor(this); c.Visit(body); } } @@ -134,7 +134,7 @@ public void FillInDecreasesClauses(ModuleDefinition module) { } if (body != null) { - var c = new FillInDefaultLoopDecreases_Visitor(this, clbl); + var c = new FillInDefaultLoopDecreasesVisitor(this, clbl); c.Visit(body); } } @@ -1262,6 +1262,12 @@ public void ResolveTopLevelDecls_Core(List declarations, FillInPostConditionsAndBodiesOfPrefixLemmas(declarations); } + // A function is not allowed to be used naked (that is, without being applied to arguments) in its own SCC. + // Also, a function is not allowed to be used in any way inside a "decreases" clause its its own SCC. + foreach (var function in ModuleDefinition.AllFunctions(declarations)) { + DetectUnsoundFunctionReferencesVisitor.Check(function, this); + } + // An inductive datatype is allowed to be defined as an empty type. For example, in // predicate P(x: int) { false } // type Subset = x: int | P(x) witness * @@ -1492,7 +1498,7 @@ public void ResolveTopLevelDecls_Core(List declarations, // Check that usage of "this" is restricted before "new;" in constructor bodies, // and that a class without any constructor only has fields with known initializers. // Also check that static fields (which are necessarily const) have initializers. - var cdci = new CheckDividedConstructorInit_Visitor(reporter); + var cdci = new CheckDividedConstructorInitVisitor(reporter); foreach (var cl in ModuleDefinition.AllTypesWithMembers(declarations)) { // only reference types (classes and reference-type traits) are allowed to declare mutable fields if (cl is not ClassLikeDecl { IsReferenceTypeDecl: true }) { @@ -2015,14 +2021,14 @@ void CheckExpression(Statement stmt, ModuleResolver resolver, ICodeContext codeC void ExtremePredicateChecks(Expression expr, ExtremePredicate context, CallingPosition cp) { Contract.Requires(expr != null); Contract.Requires(context != null); - var v = new ExtremePredicateChecks_Visitor(reporter, context); + var v = new ExtremePredicateChecksVisitor(reporter, context); v.Visit(expr, cp); } void ExtremeLemmaChecks(Statement stmt, ExtremeLemma context) { Contract.Requires(stmt != null); Contract.Requires(context != null); - var v = new ExtremeLemmaChecks_Visitor(this, context); + var v = new ExtremeLemmaChecksVisitor(this, context); v.Visit(stmt); } void ExtremeLemmaChecks(Expression expr, ExtremeLemma context) { @@ -2031,7 +2037,7 @@ void ExtremeLemmaChecks(Expression expr, ExtremeLemma context) { return; } - var v = new ExtremeLemmaChecks_Visitor(this, context); + var v = new ExtremeLemmaChecksVisitor(this, context); v.Visit(expr); } @@ -2042,8 +2048,8 @@ public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, [CanBeNull codeContext is Method, false); } - class ReportOtherAdditionalInformation_Visitor : ResolverBottomUpVisitor { - public ReportOtherAdditionalInformation_Visitor(ModuleResolver resolver) + class ReportOtherAdditionalInformationVisitor : ResolverBottomUpVisitor { + public ReportOtherAdditionalInformationVisitor(ModuleResolver resolver) : base(resolver) { Contract.Requires(resolver != null); } @@ -3322,11 +3328,11 @@ void CheckLocalityUpdatesLhs(Expression lhs, ISet localsAllowedIn } } - class LazyString_OnTypeEquals { + class LazyStringOnTypeEquals { Type t0; Type t1; string s; - public LazyString_OnTypeEquals(Type t0, Type t1, string s) { + public LazyStringOnTypeEquals(Type t0, Type t1, string s) { Contract.Requires(t0 != null); Contract.Requires(t1 != null); Contract.Requires(s != null); @@ -3963,7 +3969,7 @@ public static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type lef void CollectFriendlyCallsInExtremeLemmaSpecification(Expression expr, bool position, ISet friendlyCalls, bool co, ExtremeLemma context) { Contract.Requires(expr != null); Contract.Requires(friendlyCalls != null); - var visitor = new CollectFriendlyCallsInSpec_Visitor(reporter, friendlyCalls, co, context); + var visitor = new CollectFriendlyCallsInSpecVisitor(reporter, friendlyCalls, co, context); visitor.Visit(expr, position ? CallingPosition.Positive : CallingPosition.Negative); } } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 3c1116b016..ac71d0f166 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -540,10 +540,10 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont var e = (NameSegment)expr; ResolveNameSegment(e, true, null, resolutionContext, false); - if (e.Type is Resolver_IdentifierExpr.ResolverType_Module) { + if (e.Type is ResolverIdentifierExpr.ResolverTypeModule) { reporter.Error(MessageSource.Resolver, e.Origin, "name of module ({0}) is used as a variable", e.Name); e.ResetTypeAssignment(); // the rest of type checking assumes actual types - } else if (e.Type is Resolver_IdentifierExpr.ResolverType_Type) { + } else if (e.Type is ResolverIdentifierExpr.ResolverTypeType) { reporter.Error(MessageSource.Resolver, e.Origin, "name of type ({0}) is used as a variable", e.Name); e.ResetTypeAssignment(); // the rest of type checking assumes actual types } @@ -551,10 +551,10 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont } else if (expr is ExprDotName) { var e = (ExprDotName)expr; ResolveDotSuffix(e, false, true, null, resolutionContext, false); - if (e.Type is Resolver_IdentifierExpr.ResolverType_Module) { + if (e.Type is ResolverIdentifierExpr.ResolverTypeModule) { reporter.Error(MessageSource.Resolver, e.Origin, "name of module ({0}) is used as a variable", e.SuffixName); e.ResetTypeAssignment(); // the rest of type checking assumes actual types - } else if (e.Type is Resolver_IdentifierExpr.ResolverType_Type) { + } else if (e.Type is ResolverIdentifierExpr.ResolverTypeType) { reporter.Error(MessageSource.Resolver, e.Origin, "name of type ({0}) is used as a variable", e.SuffixName); e.ResetTypeAssignment(); // the rest of type checking assumes actual types } @@ -709,7 +709,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont var arrowType = new ArrowType(e.Origin, SystemModuleManager.ArrowTypeDecls[1], new List() { SystemModuleManager.Nat() }, elementType); var hintString = " (perhaps write '_ =>' in front of the expression you gave in order to make it an arrow type)"; ConstrainSubtypeRelation(arrowType, e.Initializer.Type, e.Initializer, "sequence-construction initializer expression expected to have type '{0}' (instead got '{1}'){2}", - arrowType, e.Initializer.Type, new LazyString_OnTypeEquals(elementType, e.Initializer.Type, hintString)); + arrowType, e.Initializer.Type, new LazyStringOnTypeEquals(elementType, e.Initializer.Type, hintString)); expr.Type = new SeqType(elementType); } else if (expr is MultiSetFormingExpr) { @@ -3410,8 +3410,8 @@ ResolveTypeReturn ResolveDotSuffix_Type(ExprDotName expr, ResolutionContext reso Expression r = null; // the resolved expression, if successful var lhs = expr.Lhs.Resolved; - if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) { - var ri = (Resolver_IdentifierExpr)lhs; + if (lhs != null && lhs.Type is ResolverIdentifierExpr.ResolverTypeModule) { + var ri = (ResolverIdentifierExpr)lhs; var sig = ((ModuleDecl)ri.Decl).AccessibleSignature(false); sig = GetSignature(sig); // For 0: @@ -3441,8 +3441,8 @@ ResolveTypeReturn ResolveDotSuffix_Type(ExprDotName expr, ResolutionContext reso reporter.Error(MessageSource.Resolver, expr.Origin, "module '{0}' does not declare a type '{1}'", ri.Decl.Name, expr.SuffixName); } - } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) { - var ri = (Resolver_IdentifierExpr)lhs; + } else if (lhs != null && lhs.Type is ResolverIdentifierExpr.ResolverTypeType) { + var ri = (ResolverIdentifierExpr)lhs; // ----- 2. Look up name in type var ty = new UserDefinedType(ri.Origin, ri.Decl.Name, ri.Decl, ri.TypeArgs); if (allowDanglingDotName && ty.IsRefType) { @@ -3463,11 +3463,11 @@ ResolveTypeReturn ResolveDotSuffix_Type(ExprDotName expr, ResolutionContext reso return null; } - internal Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IOrigin tok, string name, List optTypeArguments, TopLevelDecl decl) { + internal ResolverIdentifierExpr CreateResolver_IdentifierExpr(IOrigin tok, string name, List optTypeArguments, TopLevelDecl decl) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(decl != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); if (!moduleInfo.IsAbstract) { if (decl is ModuleDecl md && md.Signature.IsAbstract) { @@ -3485,7 +3485,7 @@ internal Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IOrigin tok, stri for (int i = 0; i < decl.TypeArgs.Count; i++) { tpArgs.Add(i < n ? optTypeArguments[i] : new InferredTypeProxy()); } - return new Resolver_IdentifierExpr(tok, decl, tpArgs); + return new ResolverIdentifierExpr(tok, decl, tpArgs); } public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext) { @@ -4191,10 +4191,10 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo ResolveNameSegment_Type(s, resolutionContext, option, defaultTypeArguments); } if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { - var r = t.NamePath.Resolved as Resolver_IdentifierExpr; - if (r == null || !(r.Type is Resolver_IdentifierExpr.ResolverType_Type)) { + var r = t.NamePath.Resolved as ResolverIdentifierExpr; + if (r == null || !(r.Type is ResolverIdentifierExpr.ResolverTypeType)) { reporter.Error(MessageSource.Resolver, t.Origin, "expected type"); - } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type) { + } else if (r.Type is ResolverIdentifierExpr.ResolverTypeType) { var d = r.Decl; if (d is AbstractTypeDecl) { // resolve like a type parameter, and it may have type parameters if it's an abstract type @@ -4366,7 +4366,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut } var hintString = string.Format(" (perhaps write '{0} =>' in front of the expression you gave in order to make it an arrow type)", underscores); ConstrainSubtypeRelation(arrowType, rr.ElementInit.Type, rr.ElementInit, "array-allocation initialization expression expected to have type '{0}' (instead got '{1}'){2}", - arrowType, rr.ElementInit.Type, new LazyString_OnTypeEquals(rr.EType, rr.ElementInit.Type, hintString)); + arrowType, rr.ElementInit.Type, new LazyStringOnTypeEquals(rr.EType, rr.ElementInit.Type, hintString)); } else if (rr.InitDisplay != null) { foreach (var v in rr.InitDisplay) { ResolveExpression(v, resolutionContext); @@ -4412,7 +4412,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut // We want to create a MemberSelectExpr for the initializing method. To do that, we create a throw-away receiver of the appropriate // type, create a dot-suffix expression around this receiver, and then resolve it in the usual way for dot-suffix expressions. - var lhs = new ImplicitThisExpr_ConstructorCall(initCallTok) { Type = rr.EType }; + var lhs = new ImplicitThisExprConstructorCall(initCallTok) { Type = rr.EType }; var callLhs = new ExprDotName(((UserDefinedType)rr.EType).Origin, lhs, new Name(initCallName), ret == null ? null : ret.LastComponent.OptTypeArguments); ResolveDotSuffix(callLhs, false, true, rr.Bindings.ArgumentBindings, resolutionContext, true); if (prevErrorCount == reporter.Count(ErrorLevel.Error)) { @@ -5477,7 +5477,7 @@ void ResolveNameSegment_Type(NameSegment expr, ResolutionContext resolutionConte if (tp != null) { // ----- 0. type parameter if (expr.OptTypeArguments == null) { - r = new Resolver_IdentifierExpr(expr.Origin, tp); + r = new ResolverIdentifierExpr(expr.Origin, tp); } else { reporter.Error(MessageSource.Resolver, expr.Origin, "Type parameter expects no type arguments: {0}", expr.Name); } @@ -5603,8 +5603,8 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceTo return null; } var lhs = expr.Lhs.Resolved; - if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) { - var ri = (Resolver_IdentifierExpr)lhs; + if (lhs != null && lhs.Type is ResolverIdentifierExpr.ResolverTypeModule) { + var ri = (ResolverIdentifierExpr)lhs; var sig = ((ModuleDecl)ri.Decl).AccessibleSignature(false); sig = GetSignature(sig); // For 0: @@ -5663,8 +5663,8 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceTo ReportUnresolvedIdentifierError(expr.Origin, name, resolutionContext); } - } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) { - var ri = (Resolver_IdentifierExpr)lhs; + } else if (lhs != null && lhs.Type is ResolverIdentifierExpr.ResolverTypeType) { + var ri = (ResolverIdentifierExpr)lhs; // ----- 3. Look up name in type // expand any synonyms var ty = new UserDefinedType(expr.Origin, ri.Decl.Name, ri.Decl, ri.TypeArgs).NormalizeExpand(); @@ -5877,10 +5877,10 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext var fnType = improvedType.AsArrowType; if (fnType == null) { var lhs = e.Lhs.Resolved; - if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Module) { - reporter.Error(MessageSource.Resolver, e.Origin, "name of module ({0}) is used as a function", ((Resolver_IdentifierExpr)lhs).Decl.Name); - } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) { - var ri = (Resolver_IdentifierExpr)lhs; + if (lhs != null && lhs.Type is ResolverIdentifierExpr.ResolverTypeModule) { + reporter.Error(MessageSource.Resolver, e.Origin, "name of module ({0}) is used as a function", ((ResolverIdentifierExpr)lhs).Decl.Name); + } else if (lhs != null && lhs.Type is ResolverIdentifierExpr.ResolverTypeType) { + var ri = (ResolverIdentifierExpr)lhs; reporter.Error(MessageSource.Resolver, e.Origin, "name of {0} ({1}) is used as a function", ri.Decl.WhatKind, ri.Decl.Name); } else { if (lhs is MemberSelectExpr mse && mse.Member is Method) { diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/XConstraint.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/XConstraint.cs index a47b2b984d..a59d27959e 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/XConstraint.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/XConstraint.cs @@ -349,7 +349,7 @@ public bool Confirm(ModuleResolver resolver, bool fullstrength, out bool convert Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); var cl = a is UserDefinedType ? ((UserDefinedType)a).ResolvedClass : null; for (int i = 0; i < a.TypeArgs.Count; i++) { - resolver.AllXConstraints.Add(new XConstraint_EquatableArg(tok, + resolver.AllXConstraints.Add(new XConstraintEquatableArg(tok, a.TypeArgs[i], b.TypeArgs[i], a is CollectionType || (cl != null && cl.TypeArgs[i].Variance != TypeParameter.TPVariance.Non), a.IsRefType, @@ -362,7 +362,7 @@ public bool Confirm(ModuleResolver resolver, bool fullstrength, out bool convert case "EquatableArg": { t = Types[0].NormalizeExpandKeepConstraints(); var u = Types[1].NormalizeExpandKeepConstraints(); - var moreExactThis = (XConstraint_EquatableArg)this; + var moreExactThis = (XConstraintEquatableArg)this; if (t is TypeProxy && u is TypeProxy) { return false; // not enough information to do anything sensible } else if (t is TypeProxy || u is TypeProxy) { @@ -409,7 +409,7 @@ public bool Confirm(ModuleResolver resolver, bool fullstrength, out bool convert Contract.Assert(a.TypeArgs.Count == b.TypeArgs.Count); var cl = a is UserDefinedType ? ((UserDefinedType)a).ResolvedClass : null; for (int i = 0; i < a.TypeArgs.Count; i++) { - resolver.AllXConstraints.Add(new XConstraint_EquatableArg(tok, + resolver.AllXConstraints.Add(new XConstraintEquatableArg(tok, a.TypeArgs[i], b.TypeArgs[i], a is CollectionType || (cl != null && cl.TypeArgs[i].Variance != TypeParameter.TPVariance.Non), false, @@ -565,10 +565,10 @@ public XConstraintWithExprs(IOrigin tok, string constraintName, Type[] types, Ex } } -public class XConstraint_EquatableArg : XConstraint { +public class XConstraintEquatableArg : XConstraint { public bool AllowSuperSub; public bool TreatTypeParamAsWild; - public XConstraint_EquatableArg(IOrigin tok, Type a, Type b, bool allowSuperSub, bool treatTypeParamAsWild, TypeConstraint.ErrorMsg errMsg) + public XConstraintEquatableArg(IOrigin tok, Type a, Type b, bool allowSuperSub, bool treatTypeParamAsWild, TypeConstraint.ErrorMsg errMsg) : base(tok, "EquatableArg", new Type[] { a, b }, errMsg) { Contract.Requires(tok != null); Contract.Requires(a != null); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 736e189605..9f24788358 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -1350,11 +1350,11 @@ private void ReportUnresolvedIdentifierError(IOrigin tok, string name, Resolutio } } - private Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IOrigin tok, string name, List optTypeArguments, TopLevelDecl decl) { + private ResolverIdentifierExpr CreateResolver_IdentifierExpr(IOrigin tok, string name, List optTypeArguments, TopLevelDecl decl) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(decl != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); if (!resolver.moduleInfo.IsAbstract) { if (decl is ModuleDecl md && md.Signature.IsAbstract) { @@ -1372,7 +1372,7 @@ private Resolver_IdentifierExpr CreateResolver_IdentifierExpr(IOrigin tok, strin for (var i = 0; i < decl.TypeArgs.Count; i++) { typeArguments.Add(i < n ? optTypeArguments[i] : new InferredTypeProxy()); } - return new Resolver_IdentifierExpr(tok, decl, typeArguments); + return new ResolverIdentifierExpr(tok, decl, typeArguments); } private bool ResolveDatatypeConstructor(NameSegment expr, List/*?*/ args, ResolutionContext resolutionContext, bool complain, @@ -1480,7 +1480,7 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceTo var name = resolutionContext.InReveal ? HideRevealStmt.RevealLemmaPrefix + expr.SuffixName : expr.SuffixName; var lhs = expr.Lhs.Resolved ?? expr.Lhs; // Sometimes resolution comes later, but pre-types have already been set if (lhs is { PreType: PreTypePlaceholderModule }) { - var ri = (Resolver_IdentifierExpr)lhs; + var ri = (ResolverIdentifierExpr)lhs; var sig = ((ModuleDecl)ri.Decl).AccessibleSignature(false); sig = ModuleResolver.GetSignatureExt(sig); @@ -1538,7 +1538,7 @@ public Expression ResolveDotSuffix(ExprDotName expr, bool allowStaticReferenceTo } } else if (lhs is { PreType: PreTypePlaceholderType }) { - var ri = (Resolver_IdentifierExpr)lhs; + var ri = (ResolverIdentifierExpr)lhs; // ----- 3. Look up name in type // expand any synonyms var ty = new UserDefinedType(expr.Origin, ri.Decl.Name, ri.Decl, ri.TypeArgs).NormalizeExpand(); @@ -1794,9 +1794,9 @@ public MethodCallInformation ResolveApplySuffix(ApplySuffix e, ResolutionContext // e.Lhs is used as if it were a function value, but it isn't var lhs = e.Lhs.Resolved; if (lhs != null && lhs.PreType is PreTypePlaceholderModule) { - ReportError(e.Origin, "name of module ({0}) is used as a function", ((Resolver_IdentifierExpr)lhs).Decl.Name); + ReportError(e.Origin, "name of module ({0}) is used as a function", ((ResolverIdentifierExpr)lhs).Decl.Name); } else if (lhs != null && lhs.PreType is PreTypePlaceholderType) { - var ri = (Resolver_IdentifierExpr)lhs; + var ri = (ResolverIdentifierExpr)lhs; ReportError(e.Origin, "name of {0} ({1}) is used as a function", ri.Decl.WhatKind, ri.Decl.Name); } else { if (lhs is MemberSelectExpr mse && mse.Member is Method) { diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index de9973dd67..4970aa86d9 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -1189,7 +1189,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut // down to resolve this "lhs"; that's a no-op if the .PreType is already filled in, whereas it could cause a "'this' not allowed in // static context" error if the code tried to resolve this "this" against the enclosing environment. rr.PreType = Type2PreType(rr.EType); - var lhs = new ImplicitThisExpr_ConstructorCall(initCallTok) { + var lhs = new ImplicitThisExprConstructorCall(initCallTok) { Type = rr.EType, PreType = rr.PreType }; diff --git a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs index b2aef414d9..cf5b4bd0a9 100644 --- a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs +++ b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs @@ -211,7 +211,7 @@ private static bool InferRequiredEqualitySupport(TypeParameter tp, Type type) { } private static void Check(List declarations, bool isAnExport, ErrorReporter reporter) { - var visitor = new CheckTypeCharacteristics_Visitor(reporter); + var visitor = new CheckTypeCharacteristicsVisitor(reporter); foreach (var d in declarations) { CheckAttributes(d.Attributes, visitor); @@ -238,7 +238,7 @@ private static void Check(List declarations, bool isAnExport, Erro if (!isAnExport) { if (syn.SupportsEquality && !syn.Rhs.SupportsEquality) { reporter.Error(MessageSource.Resolver, syn.Origin, "type '{0}' declared as supporting equality, but the RHS type ({1}) might not{2}", - syn.Name, syn.Rhs, CheckTypeCharacteristics_Visitor.TypeEqualityErrorMessageHint(syn.Rhs)); + syn.Name, syn.Rhs, CheckTypeCharacteristicsVisitor.TypeEqualityErrorMessageHint(syn.Rhs)); } if (syn.Characteristics.IsNonempty && !syn.Rhs.IsNonempty) { reporter.Error(MessageSource.Resolver, syn.Origin, "type '{0}' declared as being nonempty, but the RHS type ({1}) may be empty", @@ -298,13 +298,13 @@ private static void Check(List declarations, bool isAnExport, Erro } } - private static void CheckAttributes(Attributes attributes, CheckTypeCharacteristics_Visitor visitor) { + private static void CheckAttributes(Attributes attributes, CheckTypeCharacteristicsVisitor visitor) { for (var attr = attributes; attr != null; attr = attr.Prev) { attr.Args.ForEach(e => visitor.Visit(e, true)); } } - private static void CheckFormals(List formals, bool isGhostContext, CheckTypeCharacteristics_Visitor visitor) { + private static void CheckFormals(List formals, bool isGhostContext, CheckTypeCharacteristicsVisitor visitor) { foreach (var p in formals) { visitor.VisitType(p.Origin, p.Type, isGhostContext || p.IsGhost); if (p.DefaultValue != null) { @@ -315,7 +315,7 @@ private static void CheckFormals(List formals, bool isGhostContext, Chec private static void CheckSpecification(List requires, Specification frame, List ensures, [CanBeNull] Specification decreases, - CheckTypeCharacteristics_Visitor visitor) { + CheckTypeCharacteristicsVisitor visitor) { foreach (var aexpr in requires) { CheckAttributes(aexpr.Attributes, visitor); diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index b95ea0ffd8..311e7462bd 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -336,7 +336,7 @@ private void MergeTopLevelDecls(ModuleDefinition m, IPointer nwPoi // check that od's type characteristics are respected by nw's var newType = UserDefinedType.FromTopLevelDecl(nw.Origin, nw is ClassLikeDecl { NonNullTypeDecl: { } nonNullTypeDecl } ? nonNullTypeDecl : nw); - if (!CheckTypeCharacteristics_Visitor.CheckCharacteristics(od.Characteristics, newType, false, out var whatIsNeeded, out var hint, out var errorId)) { + if (!CheckTypeCharacteristicsVisitor.CheckCharacteristics(od.Characteristics, newType, false, out var whatIsNeeded, out var hint, out var errorId)) { var typeCharacteristicsSyntax = od.Characteristics.ToString(); Error(errorId, nw.Origin, $"to be a refinement of {od.WhatKind} '{od.EnclosingModuleDefinition.Name}.{od.Name}' declared with {typeCharacteristicsSyntax}, " + diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 0f2c684412..e86d61308b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -332,7 +332,6 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, } case MemberSelectExpr selectExpr: { MemberSelectExpr e = selectExpr; - CheckFunctionSelectWF("naked function", builder, etran, e, " Possible solution: eta expansion."); CheckWellformed(e.Obj, wfOptions, locals, builder, etran); if (e.Obj.Type.IsRefType) { if (inBodyInitContext && Expression.AsThis(e.Obj) != null && !e.Member.IsInstanceIndependentConstant) { @@ -681,8 +680,6 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, CheckWellformed(e.Receiver, wfOptions, locals, builder, etran); if (!e.Function.IsStatic && !(e.Receiver is ThisExpr) && !e.Receiver.Type.IsArrowType) { CheckNonNull(callExpr.Origin, e.Receiver, builder, etran, wfOptions.AssertKv); - } else if (e.Receiver.Type.IsArrowType) { - CheckFunctionSelectWF("function specification", builder, etran, e.Receiver, ""); } if (!e.Function.IsStatic && !etran.UsesOldHeap) { // the argument can't be assumed to be allocated for the old heap @@ -1106,7 +1103,7 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, case BinaryExpr.ResolvedOpcode.NeqCommon: CheckWellformed(e.E1, wfOptions, locals, builder, etran); if (e.InCompiledContext) { - if (CheckTypeCharacteristics_Visitor.CanCompareWith(e.E0) || CheckTypeCharacteristics_Visitor.CanCompareWith(e.E1)) { + if (CheckTypeCharacteristicsVisitor.CanCompareWith(e.E0) || CheckTypeCharacteristicsVisitor.CanCompareWith(e.E1)) { // everything's fine } else { Contract.Assert(!e.E0.Type.SupportsEquality); // otherwise, CanCompareWith would have returned "true" above diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index f993107711..d3c754f315 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2447,13 +2447,6 @@ void CheckNonNull(IOrigin tok, Expression e, BoogieStmtListBuilder builder, Expr } } - void CheckFunctionSelectWF(string what, BoogieStmtListBuilder builder, ExpressionTranslator etran, Expression e, string hint) { - if (e is MemberSelectExpr sel && sel.Member is Function fn) { - Bpl.Expr assertion = !InVerificationScope(fn) ? Bpl.Expr.True : Bpl.Expr.Not(etran.HeightContext(fn)); - builder.Add(Assert(GetToken(e), assertion, new ValidInRecursion(what, hint), builder.Context)); - } - } - void CloneVariableAsBoundVar(IOrigin tok, IVariable iv, string prefix, out BoundVar bv, out IdentifierExpr ie) { Contract.Requires(tok != null); Contract.Requires(iv != null); diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 065dcf126a..d388a27ffa 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -1423,26 +1423,6 @@ public override Expression GetAssertedExpr(DafnyOptions options) { } } -public class ValidInRecursion : ProofObligationDescription { - public override string SuccessDescription => - $"{what} is valid in recursive setting"; - - public override string FailureDescription => - $"cannot use {what} in recursive setting.{hint ?? ""}"; - - public override string ShortDescription => "valid in recursion"; - - public override bool ProvedOutsideUserCode => true; - - private readonly string what; - private readonly string hint; - - public ValidInRecursion(string what, string hint) { - this.what = what; - this.hint = hint; - } -} - public class IsNonRecursive : ProofObligationDescription { public override string SuccessDescription => "default value is non-recursive"; diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index f454e35a7b..f60ac153bd 100644 --- a/Source/DafnyTestGeneration/DafnyInfo.cs +++ b/Source/DafnyTestGeneration/DafnyInfo.cs @@ -478,7 +478,7 @@ public override Expression CloneExpr(Expression expr) { return null; } switch (expr) { - case ImplicitThisExpr_ConstructorCall: + case ImplicitThisExprConstructorCall: isValidExpression = false; return base.CloneExpr(expr); case ThisExpr: diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect index a861091b06..5898f59f00 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass4.dfy.expect @@ -1,6 +1,4 @@ ReadPreconditionBypass4.dfy(30,2): Error: assertion might not hold -ReadPreconditionBypass4.dfy(31,2): Error: assertion might not hold ReadPreconditionBypass4.dfy(44,2): Error: assertion might not hold -ReadPreconditionBypass4.dfy(45,2): Error: assertion might not hold -Dafny program verifier finished with 2 verified, 4 errors +Dafny program verifier finished with 2 verified, 2 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect index 2995c7a496..574de04656 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect @@ -91,5 +91,5 @@ SubsetTypes.dfy(459,6): Error: assertion might not hold SubsetTypes.dfy(464,4): Error: assertion might not hold Dafny program verifier finished with 13 verified, 91 errors -Total resources used is 739000 +Total resources used is 738700 Max resources used by VC is 75000 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy index 631e74547d..4f43f10f3c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy @@ -168,7 +168,7 @@ function U(x: int, ghost y: int): nat function {:tailrecursion} Q(n: nat): nat { if n % 5 == 0 then - var s := Q; // error: this use of Q is not a tail call + var s := Q; // error (x2): this use of Q is not a tail call, and cannot use Q as naked function here 10 else if n % 5 == 1 then Q(Q(n - 1)) // error: inner Q is not a tail call diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy.expect index 98cbc54547..b456484c8d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TailCalls.dfy.expect @@ -28,4 +28,5 @@ TailCalls.dfy(462,15): Error: a recursive call in this context is not recognized TailCalls.dfy(110,14): Error: the recursive call to '_ctor' is not tail recursive, because the assignment of the LHS happens after the call TailCalls.dfy(126,19): Error: the recursive call to 'Compute' is not tail recursive because the actual type argument is not the formal type parameter 'G' TailCalls.dfy(139,17): Error: the recursive call to 'Run' is not tail recursive because the actual type argument 1 is not the formal type parameter 'G' -30 resolution/type errors detected in TailCalls.dfy +TailCalls.dfy(171,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +31 resolution/type errors detected in TailCalls.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeParameters.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeParameters.dfy.expect index e99329ad15..2c19e37519 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeParameters.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeParameters.dfy.expect @@ -16,4 +16,4 @@ TypeParameters.dfy(175,23): Error: this invariant could not be proved to be main TypeParameters.dfy(175,37): Related location: this proposition could not be proved TypeParameters.dfy(376,20): Error: assertion might not hold -Dafny program verifier finished with 31 verified, 9 errors +Dafny program verifier finished with 30 verified, 9 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy index 3b8e5250be..7917e361b0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy @@ -1,11 +1,11 @@ // RUN: %testDafnyForEachResolver "%s" -ghost function {:opaque} Reverse(id:int) : int +ghost opaque function Reverse(id: int): int -ghost function RefineToMap(ReverseKey:int->int) : bool +ghost function RefineToMap(ReverseKey: int -> int): bool -ghost function RefineToMapOfSeqNums() : bool +ghost function RefineToMapOfSeqNums(): bool { - RefineToMap(Reverse) + RefineToMap(Reverse) } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy.expect index 823a60a105..012f5b9937 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug82.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 1 verified, 0 errors +Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/MonadicLaws.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/MonadicLaws.dfy.expect index 0825601cd9..ee799665b5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/MonadicLaws.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/MonadicLaws.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 9 verified, 0 errors +Dafny program verifier finished with 8 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue182.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue182.dfy.expect index 649b395ad0..592125f1b0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue182.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue182.dfy.expect @@ -1,2 +1,3 @@ git-issue182.dfy(5,8): Error: Postcondition must be a boolean (got () -> bool) -1 resolution/type errors detected in git-issue182.dfy +git-issue182.dfy(5,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +2 resolution/type errors detected in git-issue182.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/induction-principle-code/AST.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/induction-principle-code/AST.dfy.expect index ba00363fc0..00a51f822d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/induction-principle-code/AST.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/induction-principle-code/AST.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 4 verified, 0 errors +Dafny program verifier finished with 3 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy index f9e1d10dc8..5c0327cfae 100755 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy @@ -31,11 +31,11 @@ /// anonymous functions (“lambdas”) modularly: every time a lambda is created, /// as with `(fun () -> parentheses' ())`, Dafny checks that the function can be /// called in any context. To see why, consider the function `Apply` below and -/// the following two uses of it: +/// the following two uses of it (see also parser_combinators_error.dfy): function Apply(f: () -> int): int { f() } -function F0(): int { Apply(F0) } +// function F0(): int { Apply(F0) } // cannot use F0 naked here (see parser_combinators_error.dfy) function F1(): int { Apply(() => F1()) } /// Dafny rejects `F0` because it does not allow using “naked” recursive diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect index 696866c1d4..34fc88fa5b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect @@ -1,7 +1,6 @@ -parser_combinators.dfy(38,27): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. parser_combinators.dfy(39,35): Error: cannot prove termination; try supplying a decreases clause -Dafny program verifier finished with 8 verified, 2 errors +Dafny program verifier finished with 8 verified, 1 error Dafny program verifier did not attempt verification "((()))": 3 nested parentheses diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators_error.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators_error.dfy new file mode 100644 index 0000000000..faf3027270 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators_error.dfy @@ -0,0 +1,6 @@ +// RUN: %exits-with 2 %verify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function Apply(f: () -> int): int { f() } + +function F0(): int { Apply(F0) } // error: cannot use F0 naked here diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators_error.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators_error.dfy.expect new file mode 100644 index 0000000000..e2de9f70d3 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators_error.dfy.expect @@ -0,0 +1,2 @@ +parser_combinators_error.dfy(6,27): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +1 resolution/type errors detected in parser_combinators_error.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6043.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6043.dfy new file mode 100644 index 0000000000..3b0510a2ae --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6043.dfy @@ -0,0 +1,42 @@ +// RUN: %exits-with 2 %verify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function F(x: int): int + decreases G(x) // error: decreases clause cannot use mutually recursive function +{ + G(x) - 1 +} + +function G(x: int): int + decreases F(x) // error: decreases clause cannot use mutually recursive function +{ + F(x) +} + +function K(x: nat): int + decreases if x == 0 then 0 else 1 + K(x - 1) // error: decreases clause is not allowed to call enclosing function +{ + if x == 0 then 200 else 1 + K(x - 1) +} + +function Id(x: int): int { + IdBuddy(x) +} + +function IdBuddy(x: int): int + decreases x, 0 +{ + if x <= 0 then x else + var id := Id; // error: cannot use Id naked here + id(x - 1) +} + +ghost function H(x: int): int { + if H != (H) then 0 else 3 // error (x2): cannot use H naked here +} + +datatype Dt = Dt { + ghost function J(x: int): int { + if (this).J == J then 0 else 3 // error (x2): cannot use J naked here + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6043.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6043.dfy.expect new file mode 100644 index 0000000000..c79d8eeca6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6043.dfy.expect @@ -0,0 +1,9 @@ +git-issue-6043.dfy(5,13): Error: the decreases clause of function 'F' is not allowed to call 'G', because they are mutually recursive +git-issue-6043.dfy(11,13): Error: the decreases clause of function 'G' is not allowed to call 'F', because they are mutually recursive +git-issue-6043.dfy(17,39): Error: a decreases clause is not allowed to call the enclosing function +git-issue-6043.dfy(30,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +git-issue-6043.dfy(35,5): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +git-issue-6043.dfy(35,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +git-issue-6043.dfy(40,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +git-issue-6043.dfy(40,19): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. +8 resolution/type errors detected in git-issue-6043.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy index 4419ae4d10..676f897f1f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy @@ -2,51 +2,51 @@ // RUN: %diff "%s.expect" "%t" trait O extends object { - var rep:set - ghost function union(s:set>):set { + var rep: set + + ghost function union(s: set>): set { set o,o1 | o in s && o1 in o :: o1 } least predicate ag() reads * { - rep=={} || (forall o:O | o in rep :: o.ag()) + rep=={} || (forall o: O | o in rep :: o.ag()) } - ghost predicate ldp(n:ORDINAL) + ghost predicate ldp(n: ORDINAL) reads * { - ag#[n]() && (forall n1:ORDINAL | n1 < n:: !ag#[n1]()) + ag#[n]() && (forall n1: ORDINAL | n1 < n :: !ag#[n1]()) } - ghost function ld(n:ORDINAL):ORDINAL + ghost function ld(n: ORDINAL): ORDINAL reads * requires ag#[n]() ensures ldp(ld(n)) { - if ldp(n) then n else var n1:ORDINAL :| n1 < n && ag#[n1](); ld(n1) + if ldp(n) then n else var n1: ORDINAL :| n1 < n && ag#[n1](); ld(n1) } - ghost function level():ORDINAL + ghost function level(): ORDINAL reads fr() requires ag() ensures ldp(level()) { - var n:ORDINAL :| ag#[n](); ld(n) + var n: ORDINAL :| ag#[n](); ld(n) } least lemma l1() requires ag() - ensures forall o:O | o in rep :: o.level() < level() + ensures forall o: O | o in rep :: o.level() < level() decreases level() {} - ghost function fr():set + ghost function fr(): set requires ag() reads * - decreases level() + decreases level() // error: fr and level are mutually recursive, so fr is not allowed to use level in its decreases clause { - {this} + union(set o:O | o in rep :: l1(); o.fr()) + {this} + union(set o: O | o in rep :: l1(); o.fr()) } } - diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy.expect index d39065e6bb..401e2e91ee 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-847.dfy.expect @@ -1,4 +1,2 @@ -git-issue-847.dfy(40,44): Error: a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas -git-issue-847.dfy(40,54): Error: a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas -git-issue-847.dfy(41,19): Error: a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas -3 resolution/type errors detected in git-issue-847.dfy +git-issue-847.dfy(48,19): Error: the decreases clause of function 'O.fr' is not allowed to call 'level', because they are mutually recursive +1 resolution/type errors detected in git-issue-847.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy index a81ed26c22..a821bee543 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy @@ -61,3 +61,37 @@ method AllocationTest(oldcell: Cell) case true => assert old(k(y, b)) < 50; // error: argument y is not allocated in old state } } + +module TwoStateFunctions { + method Apply(ghost f: int -> int, x: int) returns (ghost y: int) + ensures y == f(x) + { + y := f(x); + } + + class Cell { + var data: int + + twostate function F(x: int): int { + old(data) + x + } + } + + method Caller(c: Cell) + requires c.data == 9 + modifies c + { + c.data := c.data + 1; + label L: + assert c.F(11) == 20; + + var y := Apply(c.F, 11); + assert y == 20; + + assert c.F@L(11) == 21; + y := Apply(u => c.F@L(u), 11); + assert y == 21; + + assert c.F(100) == 0; // error + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect index 1be7ec6e5d..1a63b6a43d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect @@ -1,6 +1,7 @@ +Apply.dfy(95,4): Error: assertion might not hold Apply.dfy(46,23): Error: function could not be proved to be allocated in the state in which the function is invoked Apply.dfy(57,31): Error: argument could not be proved to be allocated in the state in which the function is invoked Apply.dfy(58,31): Error: argument could not be proved to be allocated in the state in which the function is invoked Apply.dfy(61,31): Error: argument could not be proved to be allocated in the state in which the function is invoked -Dafny program verifier finished with 4 verified, 4 errors +Dafny program verifier finished with 7 verified, 5 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Monads.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Monads.dfy.expect index 4bb1c2c725..66ffe3665d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Monads.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Monads.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 18 verified, 0 errors +Dafny program verifier finished with 14 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy index c08a19a9c4..cdafe1d123 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy @@ -1,4 +1,4 @@ -// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --allow-deprecation +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" module Functions { @@ -19,86 +19,52 @@ module Functions { module Requires { ghost function t(x: nat): nat - requires !t.requires(x); // error: use of naked function in its own SCC + requires !t.requires(x) // error: use of naked function in its own SCC { x } ghost function g(x: nat): nat - requires !(g).requires(x); // error: use of naked function in its own SCC + requires !(g).requires(x) // error: use of naked function in its own SCC { x } ghost function D(x: int): int // used so termination errors don't mask other errors - ghost function g2(x: int): int decreases D(x) { h(x) } // error: precondition violation + ghost function g2(x: int): int decreases D(x) { h(x) } ghost function h(x: int): int - requires !g2.requires(x); // error: use of naked function in its own SCC + requires !g2.requires(x) // error: use of naked function in its own SCC { x } } module Reads { ghost function t(x: nat): nat - reads t.reads(x); + reads t.reads(x) { x } ghost function g(x: nat): nat - reads (g).reads(x); + reads (g).reads(x) { x } ghost function g2(x: int): int { h(x) } ghost function h(x: int): int - reads g2.reads(x); + reads g2.reads(x) { x } } module ReadsGenerics { class Cl { ghost function t(a: A, b: B): (A, B) - reads t.reads(a, b); + reads t.reads(a, b) { (a, b) } ghost function g(a: A, b: B): (A, B) - reads (g).reads(a, b); + reads (g).reads(a, b) { (a, b) } ghost function g2(a: A, b: B): (A, B) { h(a, b) } ghost function h(a: A, b: B): (A, B) - reads g2.reads(a, b); + reads g2.reads(a, b) { (a, b) } } } - -module TwoStateFunctions { - method Apply(ghost f: int -> int, x: int) returns (ghost y: int) - ensures y == f(x) - { - y := f(x); - } - - class Cell { - var data: int - - twostate function F(x: int): int { - old(data) + x - } - } - - method Caller(c: Cell) - requires c.data == 9 - modifies c - { - c.data := c.data + 1; - label L: - assert c.F(11) == 20; - - var y := Apply(c.F, 11); - assert y == 20; - - assert c.F@L(11) == 21; - y := Apply(u => c.F@L(u), 11); - assert y == 21; - - assert c.F(100) == 0; // error - } -} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy.expect index 59e7e9af64..4a32660e2e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Naked.dfy.expect @@ -3,16 +3,11 @@ Naked.dfy(12,7): Error: cannot use naked function in recursive setting. Possible Naked.dfy(17,58): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(22,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(26,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. -Naked.dfy(30,51): Error: function precondition could not be proved -Naked.dfy(32,13): Related location: this proposition could not be proved Naked.dfy(32,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(38,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(42,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. -Naked.dfy(46,5): Error: cannot prove termination; try supplying a decreases clause Naked.dfy(49,10): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(56,12): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(60,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Naked.dfy(67,12): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. -Naked.dfy(102,4): Error: assertion might not hold - -Dafny program verifier finished with 5 verified, 15 errors +12 resolution/type errors detected in Naked.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy index 6b7a819da2..c8b94e8f4c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %verify --show-hints "%s" > "%t" +// RUN: %exits-with 2 %verify --show-hints "%s" > "%t" // RUN: %diff "%s.expect" "%t" ghost function fact(n: int): int diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy.expect index 7517f0bf9b..87ee58bf21 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/naked-function-in-recursive-setting.dfy.expect @@ -1,5 +1,3 @@ naked-function-in-recursive-setting.dfy(4,15): Info: auto-accumulator tail recursive -naked-function-in-recursive-setting.dfy(4,15): Info: decreases n naked-function-in-recursive-setting.dfy(10,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. - -Dafny program verifier finished with 0 verified, 1 error +1 resolution/type errors detected in naked-function-in-recursive-setting.dfy diff --git a/docs/HowToFAQ/Errors-Resolver2.md b/docs/HowToFAQ/Errors-Resolver2.md index 8fd0c832ac..ae804063a4 100644 --- a/docs/HowToFAQ/Errors-Resolver2.md +++ b/docs/HowToFAQ/Errors-Resolver2.md @@ -168,7 +168,7 @@ and optimizing tail-recursion opportunities in mutually recursive functions. ```dafny function {:tailrecursion} f(n: nat): nat { - if n == 0 then n else var ff := f; ff(n-1) + if n == 0 then n else var r := f(n-1); r } ```