diff --git a/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs index b3f86cdce39..47b8c197898 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 e2bffc357bf..11de95a29f0 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 2a4c3db9ff0..c3d5d415ee9 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs @@ -571,12 +571,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); } } @@ -1228,7 +1228,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 f2828b49b0f..b6c76c5fc53 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 302ccba9711..e7076751bb4 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.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index 92470ef44f2..dffe4000596 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -558,6 +558,9 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree case TryRecoverStatement h: EmitHaltRecoveryStmt(h.TryBody, IdName(h.HaltMessageVar), h.RecoverBody, wr); break; + case BlockByProofStmt blockByProofStmt: + TrStmt(blockByProofStmt.Body, wr, wStmts); + break; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 0d3c5a7b5f2..c500840ef55 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 42d1a6064b7..0a1ece212b3 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 d1dcd0cb0c2..e963fbc48d9 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 dec019e8be5..e632340d547 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 00000000000..d3696de66bd --- /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/DetectUnsoundFunctionReferences_Visitor.cs b/Source/DafnyCore/Resolver/DetectUnsoundFunctionReferences_Visitor.cs deleted file mode 100644 index 7adffdd4624..00000000000 --- a/Source/DafnyCore/Resolver/DetectUnsoundFunctionReferences_Visitor.cs +++ /dev/null @@ -1,37 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Dafny; - -class DetectUnsoundFunctionReferences_Visitor : ResolverBottomUpVisitor { - private readonly ICallable context; - public bool DoDecreasesChecks; - public DetectUnsoundFunctionReferences_Visitor(ModuleResolver resolver, ICallable context) - : base(resolver) { - Contract.Requires(resolver != null); - Contract.Requires(context != null); - this.context = context; - } - - protected override void VisitOneExpr(Expression expr) { - if (!DoDecreasesChecks && expr is MemberSelectExpr { Member: Function fn }) { - if (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) { - if (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/ExtremeLemmaChecks_Visitor.cs b/Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs similarity index 90% rename from Source/DafnyCore/Resolver/ExtremeLemmaChecks_Visitor.cs rename to Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs index 7c28a0a7599..a67f8b38013 100644 --- a/Source/DafnyCore/Resolver/ExtremeLemmaChecks_Visitor.cs +++ b/Source/DafnyCore/Resolver/ExtremeLemmaChecksVisitor.cs @@ -2,9 +2,9 @@ namespace Microsoft.Dafny; -class ExtremeLemmaChecks_Visitor : ResolverBottomUpVisitor { +class ExtremeLemmaChecksVisitor : ResolverBottomUpVisitor { ExtremeLemma context; - public ExtremeLemmaChecks_Visitor(ModuleResolver resolver, ExtremeLemma context) + public ExtremeLemmaChecksVisitor(ModuleResolver resolver, ExtremeLemma context) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(context != null); 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 68a1ab8f4af..c7155662feb 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 687c66bb912..8d65bd814a2 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 5a27d2024e3..ef34b1e9208 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 bac90d5e16e..b2749f62797 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 33dfa463b8a..0aa3a165156 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,13 +1262,10 @@ public void ResolveTopLevelDecls_Core(List declarations, FillInPostConditionsAndBodiesOfPrefixLemmas(declarations); } - // A function is not allowed to be used naked in its own SCC. Also, a function is not allowed to be used - // in any way inside a "decreases" clause its its own SCC. + // 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)) { - var visitor = new DetectUnsoundFunctionReferences_Visitor(this, function); - visitor.Visit(function); - visitor.DoDecreasesChecks = true; - visitor.Visit(function.Decreases.Expressions); + DetectUnsoundFunctionReferencesVisitor.Check(function, this); } // An inductive datatype is allowed to be defined as an empty type. For example, in @@ -1501,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 }) { @@ -2024,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) { @@ -2040,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); } @@ -2051,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); } @@ -3331,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); @@ -3972,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 3c1116b0166..ac71d0f166d 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 a47b2b984da..a59d27959e8 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 736e1896055..9f247883582 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 de9973dd671..4970aa86d9f 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 b2aef414d99..cf5b4bd0a9a 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 b95ea0ffd81..311e7462bd9 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 cd60768d590..e41e5935038 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1103,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/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs index f454e35a7b1..f60ac153bdd 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/comp/Arrays.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy index cd1247526f6..cd35cc00ca0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy @@ -492,7 +492,9 @@ module NativeArrays { var iIndex: int, bIndex: byte, bvIndex: bv9 := 3, 4, 5; m[iIndex, bIndex] := arr[iIndex]; arr[iIndex] := m[iIndex, bvIndex - 1]; - assert arr[iIndex] == 17; + assert arr[iIndex] == 17 by { + assert true; + } print arr[iIndex], " "; // 17 m[bIndex, iIndex] := arr[bIndex]; arr[bIndex] := m[bvIndex - 1, iIndex]; 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 909f929815c..34fc88fa5b1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect @@ -1,4 +1,4 @@ -parser_combinators.dfy(39,33): Error: cannot prove termination; try supplying a decreases clause +parser_combinators.dfy(39,35): Error: cannot prove termination; try supplying a decreases clause Dafny program verifier finished with 8 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy index 8a356da3c22..ac1919accfa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy @@ -8,7 +8,9 @@ include "../exceptions/NatOutcomeDt.dfy" include "../exceptions/GenericOutcomeDt.dfy" method TestAssignOrHalt() { - var stmt1: nat :- expect NatSuccess(42); + var stmt1: nat :- expect NatSuccess(42) by { + assert true; + } // Regression test for when assign-or-halt was also calling PropagateFailure, which led // to the error "type variable 'U' in the function call to 'PropagateFailure' could not be determined" // (because of the lack of type constraints). diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect index 572284717d0..cb29b57833f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect @@ -1,12 +1,12 @@ Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") 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 index fa33686af07..c79d8eeca66 100644 --- 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 @@ -1,6 +1,6 @@ -git-issue-6043.dfy(5,12): Error: the decreases clause of function 'F' is not allowed to call 'G', because they are mutually recursive -git-issue-6043.dfy(11,12): Error: the decreases clause of function 'G' is not allowed to call 'F', because they are mutually recursive -git-issue-6043.dfy(17,38): Error: a decreases clause is not allowed to call the enclosing function +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. 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 0e6e2ff12af..401e2e91ee9 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,2 +1,2 @@ -git-issue-847.dfy(48,14): Error: the decreases clause of function 'O.fr' is not allowed to call 'level', because they are mutually recursive +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/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect index 18fac6636f6..4ac29e24bf2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect @@ -1,15 +1,15 @@ Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) diff --git a/docs/dev/news/6050.fix b/docs/dev/news/6050.fix new file mode 100644 index 00000000000..c9e1028c8d6 --- /dev/null +++ b/docs/dev/news/6050.fix @@ -0,0 +1 @@ +Fix a bug that caused a crash when translating by blocks \ No newline at end of file diff --git a/docs/news/fix.3809 b/docs/news/fix.3809 new file mode 100644 index 00000000000..177fb99de1b --- /dev/null +++ b/docs/news/fix.3809 @@ -0,0 +1 @@ +Fix C#, Java and Go generated code when a datatype contains a method named 'Default'