diff --git a/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs b/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs index 831ef5bc0ad..5b958f4a9c5 100644 --- a/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Heap/WildcardExpr.cs @@ -7,6 +7,7 @@ public class WildcardExpr : Expression, ICloneable { // a Wildcar public WildcardExpr(Cloner cloner, WildcardExpr original) : base(cloner, original) { } + [SyntaxConstructor] public WildcardExpr(IOrigin origin) : base(origin) { Contract.Requires(origin != null); diff --git a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs index cbe324e58e6..0d218410012 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs @@ -1,3 +1,4 @@ +#nullable enable using System.Collections.Generic; using System.Diagnostics.Contracts; using Microsoft.Dafny.Auditor; @@ -12,7 +13,8 @@ public AssumeStmt Clone(Cloner cloner) { public AssumeStmt(Cloner cloner, AssumeStmt original) : base(cloner, original) { } - public AssumeStmt(IOrigin origin, Expression expr, Attributes attributes) + [SyntaxConstructor] + public AssumeStmt(IOrigin origin, Expression expr, Attributes? attributes) : base(origin, expr, attributes) { Contract.Requires(origin != null); Contract.Requires(expr != null); @@ -43,7 +45,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co public override void ResolveGhostness(ModuleResolver resolver, ErrorReporter reporter, bool mustBeErasable, ICodeContext codeContext, - string proofContext, bool allowAssumptionVariables, bool inConstructorInitializationPhase) { + string? proofContext, bool allowAssumptionVariables, bool inConstructorInitializationPhase) { IsGhost = true; } } diff --git a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs index 7c6d7d5e673..4fb16dc9998 100644 --- a/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs +++ b/Source/DafnyCore/AST/SyntaxDeserializer/Generated.cs @@ -306,6 +306,22 @@ public CharLiteralExpr ReadCharLiteralExprOption() return ReadCharLiteralExpr(); } + public WildcardExpr ReadWildcardExpr() + { + var parameter0 = ReadAbstract(); + return new WildcardExpr(parameter0); + } + + public WildcardExpr ReadWildcardExprOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadWildcardExpr(); + } + public UnchangedExpr ReadUnchangedExpr() { var parameter0 = ReadAbstract(); @@ -587,6 +603,24 @@ public ExpectStmt ReadExpectStmtOption() return ReadExpectStmt(); } + public AssumeStmt ReadAssumeStmt() + { + var parameter0 = ReadAbstract(); + var parameter2 = ReadAttributesOption(); + var parameter1 = ReadAbstract(); + return new AssumeStmt(parameter0, parameter1, parameter2); + } + + public AssumeStmt ReadAssumeStmtOption() + { + if (ReadIsNull()) + { + return default; + } + + return ReadAssumeStmt(); + } + public AssertStmt ReadAssertStmt() { var parameter0 = ReadAbstract(); @@ -2319,6 +2353,11 @@ private object ReadObject(System.Type actualType) return ReadCharLiteralExpr(); } + if (actualType == typeof(WildcardExpr)) + { + return ReadWildcardExpr(); + } + if (actualType == typeof(UnchangedExpr)) { return ReadUnchangedExpr(); @@ -2394,6 +2433,11 @@ private object ReadObject(System.Type actualType) return ReadExpectStmt(); } + if (actualType == typeof(AssumeStmt)) + { + return ReadAssumeStmt(); + } + if (actualType == typeof(AssertStmt)) { return ReadAssertStmt(); diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 206bf2cf53b..36e321d48f8 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1696,7 +1696,8 @@ private void ComputeGhostInterestAndMisc(List declarations) { private void CheckForCyclesAmongRedirectingTypes(RedirectingTypeDecl dd, HashSet cycleErrorHasBeenReported) { var enclosingModule = dd.EnclosingModule; - if (enclosingModule.CallGraph.GetSCCSize(dd) != 1) { + if (enclosingModule.CallGraph.GetSCCSize(dd) != 1 || + enclosingModule.CallGraph.FindVertex(dd).Successors.Any(v => v.N == dd)) { var r = enclosingModule.CallGraph.GetSCCRepresentative(dd); if (cycleErrorHasBeenReported.Contains(r)) { // An error has already been reported for this cycle, so don't report another. diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 619fab6fcb8..7a5c2aa900e 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4222,15 +4222,14 @@ public ResolveTypeReturn ResolveTypeLenient(IOrigin tok, Type type, ResolutionCo t.ResolvedClass = d; // Store the decl, so the compiler will generate the fully qualified name } else if (d is RedirectingTypeDecl) { var dd = (RedirectingTypeDecl)d; - var caller = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) as ICallable; - if (caller != null && !(d is SubsetTypeDecl && caller is SpecialFunction)) { - if (caller != d) { - } else if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) { - // detect self-loops here, since they don't show up in the graph's SCC methods - reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); - } else { - // detect self-loops here, since they don't show up in the graph's SCC methods - reporter.Error(MessageSource.Resolver, d.Origin, "recursive constraint dependency involving a {0}: {1} -> {1}", d.WhatKind, d.Name); + var parent = CodeContextWrapper.Unwrap(resolutionContext.CodeContext) as ICallable; + if (parent != null && !(d is SubsetTypeDecl && parent is SpecialFunction)) { + var cycleFound = parent == d; + if (cycleFound) { + if (d is TypeSynonymDecl && !(d is SubsetTypeDecl)) { + // detect self-loops here, since they don't show up in the graph's SCC methods + reporter.Error(MessageSource.Resolver, d.Origin, "type-synonym cycle: {0} -> {0}", d.Name); + } } } t.ResolvedClass = d; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy new file mode 100644 index 00000000000..9b9532f445c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy @@ -0,0 +1,11 @@ +// RUN: ! %testDafnyForEachResolver "%s" -- --allow-axioms=false + +type Even = x: int | x % 2 == 0 +opaque const ten: Even := 10 + +const twoHundred: LessThanTwoHundred := 200 +type LessThanTwoHundred = k | 0 <= k < twoHundred + +const twoHundred_2: LessThanHundredNinetyNine := 200 +const hundredNinetyNine: int := twoHundred_2 as int - 1 +type LessThanHundredNinetyNine = k | 0 <= k < hundredNinetyNine \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect new file mode 100644 index 00000000000..90fb86cfac9 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constResolution.dfy.expect @@ -0,0 +1,3 @@ +constResolution.dfy(7,5): Error: recursive constraint dependency involving a subset type: LessThanTwoHundred -> twoHundred -> LessThanTwoHundred +constResolution.dfy(11,5): Error: recursive constraint dependency involving a subset type: LessThanHundredNinetyNine -> hundredNinetyNine -> twoHundred_2 -> LessThanHundredNinetyNine +2 resolution/type errors detected in constResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/constVerification.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy new file mode 100644 index 00000000000..16ab37ec0c8 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy @@ -0,0 +1,9 @@ +// RUN: ! %verify --type-system-refresh --general-traits=datatype %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +datatype Stmt = + | Skip + | Block(stmts: seq) + | If(b: bool, thn: BlockStmt, els: BlockStmt) + +type BlockStmt = s: Stmt | s.Block? witness Block([]) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect new file mode 100644 index 00000000000..7e54a5efe76 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/subsetTypes/cycles.dfy.expect @@ -0,0 +1,2 @@ +cycles.dfy(9,5): Error: recursive constraint dependency involving a subset type: BlockStmt -> Stmt -> BlockStmt +1 resolution/type errors detected in cycles.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy new file mode 100644 index 00000000000..903850941fb --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy @@ -0,0 +1,8 @@ +// RUN: %verify --type-system-refresh --general-traits=datatype %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +trait SelfConstraintDep> {} +trait SelfConstraintDep2> extends object {} + +datatype D extends SelfConstraintDep = D {} +class C extends SelfConstraintDep2 {} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect new file mode 100644 index 00000000000..012f5b99379 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/typeBounds/cycles.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect index f6399331691..c2f6cfe5065 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect @@ -191,11 +191,13 @@ GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed t GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') -GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A -GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(939,10): Error: a newtype ('W') must be based on some numeric type (got X) +GeneralNewtypeResolution.dfy(940,10): Error: Cyclic dependency among declarations: A -> A +GeneralNewtypeResolution.dfy(944,10): Error: a newtype ('W') must be based on some numeric type (got X) +GeneralNewtypeResolution.dfy(945,10): Error: Cyclic dependency among declarations: A -> A GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A -GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A -197 resolution/type errors detected in GeneralNewtypeResolution.dfy +GeneralNewtypeResolution.dfy(955,10): Error: Cyclic dependency among declarations: A -> A +199 resolution/type errors detected in GeneralNewtypeResolution.dfy GeneralNewtypeResolution.dfy(34,10): Error: a newtype ('MyOrdinal') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got ORDINAL) GeneralNewtypeResolution.dfy(40,10): Error: a newtype ('MyObject') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got object) GeneralNewtypeResolution.dfy(41,10): Error: a newtype ('MyTrait') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got Trait) @@ -355,8 +357,8 @@ GeneralNewtypeResolution.dfy(927,4): Error: type parameter 'ZZ' is not allowed t GeneralNewtypeResolution.dfy(932,5): Error: type parameter 'A' is not allowed to change variance (here, from '+' to '-') GeneralNewtypeResolution.dfy(933,5): Error: type parameter 'B' is not allowed to change variance (here, from '=' to '+') GeneralNewtypeResolution.dfy(934,4): Error: type parameter 'C' is not allowed to change variance (here, from '-' to '=') -GeneralNewtypeResolution.dfy(940,10): Error: recursive constraint dependency involving a newtype: A -> A -GeneralNewtypeResolution.dfy(945,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(940,10): Error: Cyclic dependency among declarations: A -> A +GeneralNewtypeResolution.dfy(945,10): Error: Cyclic dependency among declarations: A -> A GeneralNewtypeResolution.dfy(950,7): Error: type-synonym cycle: A -> A -GeneralNewtypeResolution.dfy(955,10): Error: recursive constraint dependency involving a newtype: A -> A +GeneralNewtypeResolution.dfy(955,10): Error: Cyclic dependency among declarations: A -> A 162 resolution/type errors detected in GeneralNewtypeResolution.dfy diff --git a/Source/Scripts/Syntax.cs-schema b/Source/Scripts/Syntax.cs-schema index 901831c7c67..5899a4d1e5c 100644 --- a/Source/Scripts/Syntax.cs-schema +++ b/Source/Scripts/Syntax.cs-schema @@ -184,6 +184,10 @@ class CharLiteralExpr : LiteralExpr { } +class WildcardExpr : Expression +{ +} + class UnchangedExpr : Expression { List frame; @@ -313,6 +317,10 @@ class ExpectStmt : PredicateStmt Expression? message; } +class AssumeStmt : PredicateStmt +{ +} + class AssertStmt : PredicateStmt { AssertLabel? label;