From 07fd118d463d466be4faf1d56bf9ab587a07ef0d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 12 Dec 2024 15:23:25 -0800 Subject: [PATCH 01/10] Fix 5972 also for newtype/subset type/type synonyms --- Source/DafnyCore/AST/Types/UserDefinedType.cs | 8 +- Source/DafnyCore/Resolver/ModuleResolver.cs | 52 ++-- .../LitTest/git-issues/git-issue-5972.dfy | 261 +++++++++++++++--- .../git-issues/git-issue-5972.dfy.expect | 12 +- .../LitTest/git-issues/git-issue-5972a.dfy | 124 +++++++++ .../git-issues/git-issue-5972a.dfy.expect | 5 + 6 files changed, 401 insertions(+), 61 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs index 2dea4e86ba..d97ab765c1 100644 --- a/Source/DafnyCore/AST/Types/UserDefinedType.cs +++ b/Source/DafnyCore/AST/Types/UserDefinedType.cs @@ -376,7 +376,7 @@ public override string TypeName(DafnyOptions options, ModuleDefinition context, public override bool SupportsEquality { get { - if (ResolvedClass is ClassLikeDecl { IsReferenceTypeDecl: true } or NewtypeDecl) { + if (ResolvedClass is ClassLikeDecl { IsReferenceTypeDecl: true }) { return ResolvedClass.IsRevealedInScope(Type.GetScope()); } else if (ResolvedClass is TraitDecl) { return false; @@ -400,6 +400,12 @@ public override bool SupportsEquality { i++; } return true; + } else if (ResolvedClass is NewtypeDecl newtypeDecl) { + if (newtypeDecl.IsRevealedInScope(Type.GetScope())) { + return newtypeDecl.RhsWithArgument(TypeArgs).SupportsEquality; + } else { + return false; + } } else if (ResolvedClass is TypeSynonymDeclBase) { var t = (TypeSynonymDeclBase)ResolvedClass; if (t.SupportsEquality) { diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 9be547760f..b26221dedf 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2884,8 +2884,7 @@ void MarkSCCAsNotSupportingEquality() { } foreach (var ctor in dt.Ctors) { foreach (var arg in ctor.Formals) { - var type = arg.Type; - DetermineEqualitySupportType(type, ref thingsChanged); + DetermineEqualitySupportType(arg.Type, ref thingsChanged); } } } @@ -2929,26 +2928,43 @@ private static void DetermineEqualitySupportType(Type type, ref bool thingsChang if (type.AsTypeParameter is { } typeArg) { typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; thingsChanged = true; - } else if (type.AsMapType is { } typeMap) { - DetermineEqualitySupportType(typeMap.Range, ref thingsChanged); - } else if (type.AsSeqType is { } typeSeq) { - DetermineEqualitySupportType(typeSeq.Arg, ref thingsChanged); - } else if (type.AsIndDatatype is { } otherDt) { - if (otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { // datatype is in a different SCC - var otherUdt = (UserDefinedType)type.NormalizeExpand(); - var i = 0; - foreach (var otherTp in otherDt.TypeArgs) { - if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) { - var tp = otherUdt.TypeArgs[i].AsTypeParameter; - if (tp != null) { - tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; - thingsChanged = true; + } else if (type.SupportsEquality) { + // nothing to do + } else if (type.Normalize() is UserDefinedType userDefinedType) { + if (userDefinedType.ResolvedClass is TypeSynonymDeclBase typeSynonymDecl) { + if (typeSynonymDecl.IsRevealedInScope(Type.GetScope())) { + DetermineEqualitySupportType(typeSynonymDecl.RhsWithArgument(userDefinedType.TypeArgs), ref thingsChanged); + } + } else if (userDefinedType.ResolvedClass is NewtypeDecl newtypeDecl) { + if (newtypeDecl.IsRevealedInScope(Type.GetScope())) { + DetermineEqualitySupportType(newtypeDecl.RhsWithArgument(userDefinedType.TypeArgs), ref thingsChanged); + } + } else if (userDefinedType.ResolvedClass is IndDatatypeDecl otherDt) { + if (otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { + // datatype is in a different SCC + var otherUdt = (UserDefinedType)type.NormalizeExpand(); + var i = 0; + foreach (var otherTp in otherDt.TypeArgs) { + if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) { + var tp = otherUdt.TypeArgs[i].AsTypeParameter; + if (tp != null) { + tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; + thingsChanged = true; + } } - } - i++; + i++; + } } } + } else if (type.AsMapType is { } typeMap) { + // A map type's Domain type is required to support equality (just like the argument type for sets and multisets), but + // it is optional for the map type's Range type to support equality. Thus, we need to determine the equality support for just the Range type. + DetermineEqualitySupportType(typeMap.Range, ref thingsChanged); + } else if (type.AsSeqType is { } typeSeq) { + // Like the Range type of a map, it is optional for a sequence type's argument type to support equality. So, we make a call + // to determine it. + DetermineEqualitySupportType(typeSeq.Arg, ref thingsChanged); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy index 0f227353f4..ec8e41fc8d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy @@ -1,57 +1,240 @@ -// RUN: %exits-with 2 %baredafny verify %args "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -datatype M = M(m: map) +module Issue5972 { + datatype M = M(m: map) -method CompareAnything(f: A, g: A) returns (b: bool) - ensures b <==> f == g -{ - var m1 := M(map[0 := f]); - var m2 := M(map[0 := g]); - assert m1 == m2 <==> f == g by { - if f == g { - assert m1 == m2; + method CompareAnything(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := M(map[0 := f]); + var m2 := M(map[0 := g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.m[0] == m2.m[0]; + } } - if m1 == m2 { - assert m1.m[0] == m2.m[0]; + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + datatype S = S(s: seq) + + method CompareAnythingS(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := S([f]); + var m2 := S([g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.s[0] == m2.s[0]; + } + } + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + + codatatype Stream = Stream(head: int, tail: Stream) + { + static function From(i: int): Stream { + Stream(i, From(i + 1)) + } + } + + method Main() { + var s1 := Stream.From(0); + var s2 := Stream.From(0); + var b := CompareAnything(s1, s2); + var b2 := CompareAnythingS(s1, s2); + if !b || !b2 { + assert false; + print 1/0; } } - return m1 == m2; } -datatype S = S(s: seq) +// This module is like Issue5972 above, but uses type synonyms around the map/seq types +module TypeSynonyms { + type MyMap = map + type MySeq = seq + + datatype M = M(m: MyMap) -method CompareAnythingS(f: A, g: A) returns (b: bool) - ensures b <==> f == g -{ - var m1 := S([f]); - var m2 := S([g]); - assert m1 == m2 <==> f == g by { - if f == g { - assert m1 == m2; + method CompareAnything(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := M(map[0 := f]); + var m2 := M(map[0 := g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.m[0] == m2.m[0]; + } } - if m1 == m2 { - assert m1.s[0] == m2.s[0]; + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + datatype S = S(s: MySeq) + + method CompareAnythingS(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := S([f]); + var m2 := S([g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.s[0] == m2.s[0]; + } + } + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + codatatype Stream = Stream(head: int, tail: Stream) + { + static function From(i: int): Stream { + Stream(i, From(i + 1)) + } + } + + method Test() { + var s1 := Stream.From(0); + var s2 := Stream.From(0); + var b := CompareAnything(s1, s2); + var b2 := CompareAnythingS(s1, s2); + if !b || !b2 { + assert false; + print 1/0; } } - return m1 == m2; } +// This module is like TypeSynonyms above, but the two type synonyms are declared to definitely support equality. +// The fact that their RHSs don't gives rise to errors, but in the process of fixing issue 5972, this program +// had caused a crash, so it seems good to include as a test case. +module TypeSynonymsWithGuaranteedEqualitySupport { + type MyMap(==) = map // error: RHS does not support equality as promised + type MySeq(==) = seq // error: RHS does not support equality as promised + + datatype M = M(m: MyMap) + + method CompareAnything(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := M(map[0 := f]); + var m2 := M(map[0 := g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.m[0] == m2.m[0]; + } + } + return m1 == m2; + } + + datatype S = S(s: MySeq) + + method CompareAnythingS(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := S([f]); + var m2 := S([g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.s[0] == m2.s[0]; + } + } + return m1 == m2; + } + + codatatype Stream = Stream(head: int, tail: Stream) + { + static function From(i: int): Stream { + Stream(i, From(i + 1)) + } + } -codatatype Stream = Stream(head: int, tail: Stream) -{ - static function From(i: int): Stream { - Stream(i, From(i + 1)) + method Test() { + var s1 := Stream.From(0); + var s2 := Stream.From(0); + var b := CompareAnything(s1, s2); + var b2 := CompareAnythingS(s1, s2); + if !b || !b2 { + assert false; + print 1/0; + } } } -method Main() { - var s1 := Stream.From(0); - var s2 := Stream.From(0); - var b := CompareAnything(s1, s2); - var b2 := CompareAnythingS(s1, s2); - if !b || !b2 { - assert false; - print 1/0; +// This module is like TypeSynonyms above, but uses subset types around the map/seq types +module SubsetTypes { + type MyMap = m: map | true + type MySeq = s: seq | true + + datatype M = M(m: MyMap) + + method CompareAnything(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := M(map[0 := f]); + var m2 := M(map[0 := g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.m[0] == m2.m[0]; + } + } + return m1 == m2; // error: the types of m1 and m2 do not support equality } -} \ No newline at end of file + + datatype S = S(s: MySeq) + + method CompareAnythingS(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := S([f]); + var m2 := S([g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.s[0] == m2.s[0]; + } + } + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + codatatype Stream = Stream(head: int, tail: Stream) + { + static function From(i: int): Stream { + Stream(i, From(i + 1)) + } + } + + method Test() { + var s1 := Stream.From(0); + var s2 := Stream.From(0); + var b := CompareAnything(s1, s2); + var b2 := CompareAnythingS(s1, s2); + if !b || !b2 { + assert false; + print 1/0; + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect index 9545b0df35..87bc374870 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect @@ -1,3 +1,9 @@ -git-issue-5972.dfy(19,9): Error: == can only be applied to expressions of types that support equality (got M) -git-issue-5972.dfy(37,9): Error: == can only be applied to expressions of types that support equality (got S) -2 resolution/type errors detected in git-issue-5972.dfy +git-issue-5972.dfy(19,11): Error: == can only be applied to expressions of types that support equality (got M) +git-issue-5972.dfy(37,11): Error: == can only be applied to expressions of types that support equality (got S) +git-issue-5972.dfy(80,11): Error: == can only be applied to expressions of types that support equality (got M) +git-issue-5972.dfy(98,11): Error: == can only be applied to expressions of types that support equality (got S) +git-issue-5972.dfy(124,7): Error: type 'MyMap' declared as supporting equality, but the RHS type (map) might not +git-issue-5972.dfy(125,7): Error: type 'MySeq' declared as supporting equality, but the RHS type (seq) might not +git-issue-5972.dfy(202,11): Error: == can only be applied to expressions of types that support equality (got M) +git-issue-5972.dfy(220,11): Error: == can only be applied to expressions of types that support equality (got S) +8 resolution/type errors detected in git-issue-5972.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy new file mode 100644 index 0000000000..96e9bb4ae6 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy @@ -0,0 +1,124 @@ +// RUN: %exits-with 2 %verify --type-system-refresh --general-newtypes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This module is like SubsetTypes in git-issue-5972.dfy, but uses newtypes around the map/seq types +module Newtypes { + newtype MyMap = map + newtype MySeq = seq + + datatype M = M(m: MyMap) + + method CompareAnything(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := M(map[0 := f]); + var m2 := M(map[0 := g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.m[0] == m2.m[0]; + } + } + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + datatype S = S(s: MySeq) + + method CompareAnythingS(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := S([f]); + var m2 := S([g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.s[0] == m2.s[0]; + } + } + return m1 == m2; // error: the types of m1 and m2 do not support equality + } + + codatatype Stream = Stream(head: int, tail: Stream) + { + static function From(i: int): Stream { + Stream(i, From(i + 1)) + } + } + + method Main() { + var s1 := Stream.From(0); + var s2 := Stream.From(0); + var b := CompareAnything(s1, s2); + var b2 := CompareAnythingS(s1, s2); + if !b || !b2 { + assert false; + print 1/0; + } + } +} + +// This module is like Newtypes above, but the two newtypes are declared to definitely support equality. +// The fact that their RHSs don't gives rise to errors. This was not properly handled before the fix +// of issue 5972. +module NewtypesWithGuaranteedEqualitySupport { + type MyMap(==) = map // error: RHS does not support equality as promised + type MySeq(==) = seq // error: RHS does not support equality as promised + + datatype M = M(m: MyMap) + + method CompareAnything(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := M(map[0 := f]); + var m2 := M(map[0 := g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.m[0] == m2.m[0]; + } + } + return m1 == m2; + } + + datatype S = S(s: MySeq) + + method CompareAnythingS(f: A, g: A) returns (b: bool) + ensures b <==> f == g + { + var m1 := S([f]); + var m2 := S([g]); + assert m1 == m2 <==> f == g by { + if f == g { + assert m1 == m2; + } + if m1 == m2 { + assert m1.s[0] == m2.s[0]; + } + } + return m1 == m2; + } + + codatatype Stream = Stream(head: int, tail: Stream) + { + static function From(i: int): Stream { + Stream(i, From(i + 1)) + } + } + + method Test() { + var s1 := Stream.From(0); + var s2 := Stream.From(0); + var b := CompareAnything(s1, s2); + var b2 := CompareAnythingS(s1, s2); + if !b || !b2 { + assert false; + print 1/0; + } + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect new file mode 100644 index 0000000000..3e7f79ac8a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect @@ -0,0 +1,5 @@ +git-issue-5972a.dfy(24,11): Error: == can only be applied to expressions of types that support equality (got M) +git-issue-5972a.dfy(42,11): Error: == can only be applied to expressions of types that support equality (got S) +git-issue-5972a.dfy(68,7): Error: type 'MyMap' declared as supporting equality, but the RHS type (map) might not +git-issue-5972a.dfy(69,7): Error: type 'MySeq' declared as supporting equality, but the RHS type (seq) might not +4 resolution/type errors detected in git-issue-5972a.dfy From 8dcde4248df4bd4a38bb8758534bc925fd2d5452 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 12 Dec 2024 17:16:20 -0600 Subject: [PATCH 02/10] Makefile updated --- Makefile | 28 +++++++++++----------------- Scripts/test-dafny.sh | 38 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 17 deletions(-) create mode 100644 Scripts/test-dafny.sh diff --git a/Makefile b/Makefile index 12aff38306..ce12a728ea 100644 --- a/Makefile +++ b/Makefile @@ -30,27 +30,21 @@ boogie: ${DIR}/boogie/Binaries/Boogie.exe tests: (cd "${DIR}"; dotnet test Source/IntegrationTests) -# make test name= +# make test name= +# make test name= update=true to update the test +# make test name= build=false don't build the solution test: - (cd "${DIR}"; [ -z "${name}" ] && echo "Syntax: make test name=" && exit 1; dotnet test Source/IntegrationTests --filter "DisplayName~${name}") + (cd "${DIR}"; \ + [ -z "${name}" ] && echo "Syntax: make test name= [update=true] [build=false]" && exit 1; \ + build_flag=$${build:-true}; \ + update_flag=$${update:-false}; \ + DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE=$$update_flag \ + dotnet test Source/IntegrationTests $$( [ "$$build_flag" = "false" ] && echo "--no-build" ) --filter "DisplayName~${name}") # Run Dafny on an integration test case directly in the folder itself. -# make test-run name= action="run ..." +# make test-dafny name= action="run ..." [build=false] test-dafny: - name="$(name)"; \ - files=$$(cd "${DIR}"/Source/IntegrationTests/TestFiles/LitTests/LitTest; find . -type f -wholename "*$$name*" | grep -E '\.dfy$$'); \ - count=$$(echo "$$files" | wc -l); \ - echo "$${files}"; \ - if [ "$$count" -eq 0 ]; then \ - echo "No files found matching pattern: $$name"; \ - exit 1; \ - else \ - echo "$$count test files found."; \ - for file in $$files; do \ - filedir=$$(dirname "$$file"); \ - (cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; dotnet run --project "${DIR}"/Source/Dafny -- $(action) "$$(basename $$file)" ); \ - done; \ - fi + @name="$(name)" DIR="$(DIR)" action="$(action)" NO_BUILD=$$( [ "${build}" = "false" ] && echo "true" || echo "false" ) bash scripts/test-dafny.sh tests-verbose: (cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests ) diff --git a/Scripts/test-dafny.sh b/Scripts/test-dafny.sh new file mode 100644 index 0000000000..cb684eea9a --- /dev/null +++ b/Scripts/test-dafny.sh @@ -0,0 +1,38 @@ +#!/bin/bash + +# Check for required environment variables +if [ -z "$DIR" ]; then + echo "Error: DIR environment variable is not set." + exit 1 +fi + +if [ -z "$name" ]; then + echo "Error: name environment variable is not set." + exit 1 +fi + +# Set the default build flag +NO_BUILD=${NO_BUILD:-false} + +# Locate files matching the specified pattern +files=$(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest" && find . -type f -wholename "*$name*" | grep -E '\.dfy$') + +if [ -z "$files" ]; then + echo "No files found matching pattern: $name" + exit 1 +else + count=$(echo "$files" | wc -l) + echo "$files" + echo "$count test files found." + for file in $files; do + filedir=$(dirname "$file") + ( + cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$filedir" || exit + + build_flag="" + [ "$NO_BUILD" = "true" ] && build_flag="--no-build" + + dotnet run $build_flag --project "${DIR}/Source/Dafny" -- ${action} "$(basename "$file")" + ) + done +fi \ No newline at end of file From 59b1df875b39ff80564e131b12ac8145665155e3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 13 Dec 2024 14:01:13 -0600 Subject: [PATCH 03/10] Quick fixes --- Makefile | 7 +---- .../CheckTypeCharacteristics_Visitor.cs | 31 +++++++++++++++++-- Source/DafnyCore/Resolver/ModuleResolver.cs | 4 +-- .../Resolver/TypeCharacteristicChecker.cs | 4 +-- .../git-issues/git-issue-5972.dfy.expect | 16 +++++----- .../git-issues/git-issue-5972a.dfy.expect | 8 ++--- 6 files changed, 45 insertions(+), 25 deletions(-) diff --git a/Makefile b/Makefile index ce12a728ea..413c6d75a6 100644 --- a/Makefile +++ b/Makefile @@ -34,12 +34,7 @@ tests: # make test name= update=true to update the test # make test name= build=false don't build the solution test: - (cd "${DIR}"; \ - [ -z "${name}" ] && echo "Syntax: make test name= [update=true] [build=false]" && exit 1; \ - build_flag=$${build:-true}; \ - update_flag=$${update:-false}; \ - DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE=$$update_flag \ - dotnet test Source/IntegrationTests $$( [ "$$build_flag" = "false" ] && echo "--no-build" ) --filter "DisplayName~${name}") + @DIR="$(DIR)" name="$(name)" update="$(update)" build="$(build)" bash scripts/test.sh # Run Dafny on an integration test case directly in the folder itself. # make test-dafny name= action="run ..." [build=false] diff --git a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs index 5474cba297..d3c22ea6e4 100644 --- a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs @@ -399,13 +399,40 @@ public static bool CheckCharacteristics(TypeParameter.TypeParameterCharacteristi return true; } - static string TypeEqualityErrorMessageHint(Type argType) { + public static string TypeEqualityErrorMessageHint(Type argType) { Contract.Requires(argType != null); - var cl = (argType.Normalize() as UserDefinedType)?.ResolvedClass; + argType = argType.Normalize(); + var cl = (argType as UserDefinedType)?.ResolvedClass; var tp = (TopLevelDecl)(cl as TypeParameter) ?? cl as AbstractTypeDecl; if (tp != null) { return string.Format(" (perhaps try declaring {2} '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line, tp.WhatKind); } + + var typeArgs = argType.TypeArgs; + + if (argType.AsSeqType != null && typeArgs.Count >= 1) { + if (TypeEqualityErrorMessageHint(typeArgs[0]) is var messageSeq and not "") { + return messageSeq; + } + } + if (argType.AsMapType != null && + typeArgs.Count >= 2 && + TypeEqualityErrorMessageHint(typeArgs[1]) is var messageMap and not "") { + return messageMap; + } + if (argType.AsIndDatatype is { EqualitySupport: IndDatatypeDecl.ES.ConsultTypeArguments } decl) { + var i = 0; + foreach (var tParam in decl.TypeArgs) { + if (tParam.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && i < typeArgs.Count && !typeArgs[i].SupportsEquality && TypeEqualityErrorMessageHint(typeArgs[i]) is var message and not "") { + return message; + } + i++; + } + } + + if (argType.AsNewtype is { } newTypeDecl) { + return TypeEqualityErrorMessageHint(newTypeDecl.RhsWithArgument(argType.TypeArgs)); + } return ""; } } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index b26221dedf..58be564a2c 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1669,7 +1669,7 @@ private void CheckForCyclesAmongRedirectingTypes(RedirectingTypeDecl dd, HashSet if (cycleErrorHasBeenReported.Contains(r)) { // An error has already been reported for this cycle, so don't report another. // Note, the representative, "r", may itself not be a const. - } else if (dd is NewtypeDecl or SubsetTypeDecl) { + } else if (dd is SubsetTypeDecl or NewtypeDecl) { ReportCallGraphCycleError(dd, $"recursive constraint dependency involving a {dd.WhatKind}"); cycleErrorHasBeenReported.Add(r); } @@ -2928,8 +2928,6 @@ private static void DetermineEqualitySupportType(Type type, ref bool thingsChang if (type.AsTypeParameter is { } typeArg) { typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; thingsChanged = true; - } else if (type.SupportsEquality) { - // nothing to do } else if (type.Normalize() is UserDefinedType userDefinedType) { if (userDefinedType.ResolvedClass is TypeSynonymDeclBase typeSynonymDecl) { if (typeSynonymDecl.IsRevealedInScope(Type.GetScope())) { diff --git a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs index 52cef103e6..c5d5fe6dc6 100644 --- a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs +++ b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs @@ -237,8 +237,8 @@ private static void Check(List declarations, bool isAnExport, Erro visitor.VisitType(syn.tok, syn.Rhs, false); if (!isAnExport) { if (syn.SupportsEquality && !syn.Rhs.SupportsEquality) { - reporter.Error(MessageSource.Resolver, syn.tok, "type '{0}' declared as supporting equality, but the RHS type ({1}) might not", - syn.Name, syn.Rhs); + reporter.Error(MessageSource.Resolver, syn.tok, "type '{0}' declared as supporting equality, but the RHS type ({1}) might not{2}", + syn.Name, syn.Rhs, CheckTypeCharacteristics_Visitor.TypeEqualityErrorMessageHint(syn.Rhs)); } if (syn.Characteristics.IsNonempty && !syn.Rhs.IsNonempty) { reporter.Error(MessageSource.Resolver, syn.tok, "type '{0}' declared as being nonempty, but the RHS type ({1}) may be empty", diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect index 87bc374870..35d393053a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972.dfy.expect @@ -1,9 +1,9 @@ -git-issue-5972.dfy(19,11): Error: == can only be applied to expressions of types that support equality (got M) -git-issue-5972.dfy(37,11): Error: == can only be applied to expressions of types that support equality (got S) -git-issue-5972.dfy(80,11): Error: == can only be applied to expressions of types that support equality (got M) -git-issue-5972.dfy(98,11): Error: == can only be applied to expressions of types that support equality (got S) -git-issue-5972.dfy(124,7): Error: type 'MyMap' declared as supporting equality, but the RHS type (map) might not -git-issue-5972.dfy(125,7): Error: type 'MySeq' declared as supporting equality, but the RHS type (seq) might not -git-issue-5972.dfy(202,11): Error: == can only be applied to expressions of types that support equality (got M) -git-issue-5972.dfy(220,11): Error: == can only be applied to expressions of types that support equality (got S) +git-issue-5972.dfy(19,11): Error: == can only be applied to expressions of types that support equality (got M) (perhaps try declaring type parameter 'A' on line 6 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(37,11): Error: == can only be applied to expressions of types that support equality (got S) (perhaps try declaring type parameter 'A' on line 24 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(80,11): Error: == can only be applied to expressions of types that support equality (got M) (perhaps try declaring type parameter 'A' on line 67 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(98,11): Error: == can only be applied to expressions of types that support equality (got S) (perhaps try declaring type parameter 'A' on line 85 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(124,7): Error: type 'MyMap' declared as supporting equality, but the RHS type (map) might not (perhaps try declaring type parameter 'U' on line 124 as 'U(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(125,7): Error: type 'MySeq' declared as supporting equality, but the RHS type (seq) might not (perhaps try declaring type parameter 'T' on line 125 as 'T(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(202,11): Error: == can only be applied to expressions of types that support equality (got M) (perhaps try declaring type parameter 'A' on line 189 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972.dfy(220,11): Error: == can only be applied to expressions of types that support equality (got S) (perhaps try declaring type parameter 'A' on line 207 as 'A(==)', which says it can only be instantiated with a type that supports equality) 8 resolution/type errors detected in git-issue-5972.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect index 3e7f79ac8a..54f54d2f93 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972a.dfy.expect @@ -1,5 +1,5 @@ -git-issue-5972a.dfy(24,11): Error: == can only be applied to expressions of types that support equality (got M) -git-issue-5972a.dfy(42,11): Error: == can only be applied to expressions of types that support equality (got S) -git-issue-5972a.dfy(68,7): Error: type 'MyMap' declared as supporting equality, but the RHS type (map) might not -git-issue-5972a.dfy(69,7): Error: type 'MySeq' declared as supporting equality, but the RHS type (seq) might not +git-issue-5972a.dfy(24,11): Error: == can only be applied to expressions of types that support equality (got M) (perhaps try declaring type parameter 'A' on line 11 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972a.dfy(42,11): Error: == can only be applied to expressions of types that support equality (got S) (perhaps try declaring type parameter 'A' on line 29 as 'A(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972a.dfy(68,7): Error: type 'MyMap' declared as supporting equality, but the RHS type (map) might not (perhaps try declaring type parameter 'U' on line 68 as 'U(==)', which says it can only be instantiated with a type that supports equality) +git-issue-5972a.dfy(69,7): Error: type 'MySeq' declared as supporting equality, but the RHS type (seq) might not (perhaps try declaring type parameter 'T' on line 69 as 'T(==)', which says it can only be instantiated with a type that supports equality) 4 resolution/type errors detected in git-issue-5972a.dfy From caad6dd1e2632375e4bcb652b96beb2484cbfe48 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 16 Dec 2024 14:11:47 -0600 Subject: [PATCH 04/10] Fixed second soundness issue + missing test script --- Scripts/test.sh | 59 +++++++++++++++++++ .../AST/TypeDeclarations/NewtypeDecl.cs | 18 ++++-- Source/DafnyCore/Resolver/ModuleResolver.cs | 22 +++++-- .../LitTest/git-issues/git-issue-5972c.dfy | 14 +++++ .../git-issues/git-issue-5972c.dfy.expect | 2 + 5 files changed, 104 insertions(+), 11 deletions(-) create mode 100644 Scripts/test.sh create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy.expect diff --git a/Scripts/test.sh b/Scripts/test.sh new file mode 100644 index 0000000000..24225f4fdc --- /dev/null +++ b/Scripts/test.sh @@ -0,0 +1,59 @@ +#!/bin/bash +set -e + +# Ensure name is provided +if [ -z "$name" ]; then + echo "Syntax: make test name= [update=true] [build=false]" + exit 1 +fi + +# Default values for update and build +update_flag=${update:-false} +build_flag=${build:-true} + +# Set the integration tests folder +integration_tests_dir="${DIR}/Source/IntegrationTests" +lit_tests_dir="${integration_tests_dir}/TestFiles/LitTests/LitTest" + +# Handle no-build logic +if [ "$build_flag" = "false" ]; then + echo "" + echo "Build is disabled. Copying test files to the output directory..." + + framework_dir=$(find "${integration_tests_dir}/bin/Debug" -maxdepth 1 -type d -name "net*" | sort | tail -n 1) + if [ -z "$framework_dir" ]; then + echo "Error: Could not find target framework directory in bin/Debug. Please run at least once with build=true." + exit 1 + fi + output_dir="${framework_dir}/TestFiles/LitTests/LitTest" + + # Find and copy all matching files to the output directory + files=$(cd "$lit_tests_dir" && find . -type f -wholename "*$name*") + if [ -z "$files" ]; then + echo "No files found matching pattern: $name" + exit 1 + fi + + # Create output directory if it doesn't exist + mkdir -p "$output_dir" + + # Copy files + echo "$files" | while IFS= read -r file; do + echo "Copying $file to $output_dir" + cp "$lit_tests_dir/$file" "$output_dir/" + done +fi + +# Check if update flag is true +if [ "$update_flag" = "true" ]; then + echo "" + echo "Update mode enabled." + echo "Going to update the .expect files to match the current Dafny output." +fi + +# Run dotnet test +echo "Running integration tests..." +DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE="$update_flag" \ +dotnet test "$integration_tests_dir" \ + $( [ "$build_flag" = "false" ] && echo "--no-build" ) \ + --filter "DisplayName~$name" diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index f58836510a..fd3ba11742 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -96,13 +96,21 @@ public Type RhsWithArgument(List typeArgs) { public TopLevelDecl AsTopLevelDecl => this; public TypeDeclSynonymInfo SynonymInfo { get; set; } - public TypeParameter.EqualitySupportValue EqualitySupport { + private IndDatatypeDecl.ES equalitySupport = IndDatatypeDecl.ES.NotYetComputed; + + public IndDatatypeDecl.ES EqualitySupport { get { - if (this.BaseType.SupportsEquality) { - return TypeParameter.EqualitySupportValue.Required; - } else { - return TypeParameter.EqualitySupportValue.Unspecified; + if (equalitySupport == IndDatatypeDecl.ES.NotYetComputed) { + var thingsChanged = false; + if (ModuleResolver.SurelyNeverSupportEquality(BaseType)) { + equalitySupport = IndDatatypeDecl.ES.Never; + } else { + ModuleResolver.DetermineEqualitySupportType(BaseType, ref thingsChanged); + equalitySupport = IndDatatypeDecl.ES.ConsultTypeArguments; + } } + + return equalitySupport; } } diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 58be564a2c..a8431bbd04 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2861,11 +2861,7 @@ void MarkSCCAsNotSupportingEquality() { return; // we are done } foreach (var arg in ctor.Formals) { - var anotherIndDt = arg.Type.AsIndDatatype; - if (arg.IsGhost || - (anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || - arg.Type.IsCoDatatype || - arg.Type.IsArrowType) { + if (arg.IsGhost || SurelyNeverSupportEquality(arg.Type)) { // arg.Type is known never to support equality MarkSCCAsNotSupportingEquality(); return; // we are done @@ -2924,7 +2920,21 @@ void MarkSCCAsNotSupportingEquality() { } } - private static void DetermineEqualitySupportType(Type type, ref bool thingsChanged) { + // If returns true, the given type never supports equality + // If return false, then the type must support equality if type parameters support equality + // It is unsound for a type to make this function return false when there is no type parameter + // assignment that amkes this type support equality + public static bool SurelyNeverSupportEquality(Type type) { + type = type.Normalize(); + return + type.AsNewtype is { EqualitySupport: IndDatatypeDecl.ES.Never } || + type.AsIndDatatype is { EqualitySupport: IndDatatypeDecl.ES.Never } || + type.IsCoDatatype || type.IsArrowType || + type.AsSeqType is { Arg: var argType } && SurelyNeverSupportEquality(argType) || + type.AsMapType is { Range: var rangeType } && SurelyNeverSupportEquality(rangeType); + } + + public static void DetermineEqualitySupportType(Type type, ref bool thingsChanged) { if (type.AsTypeParameter is { } typeArg) { typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; thingsChanged = true; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy new file mode 100644 index 0000000000..9d87a61d24 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy @@ -0,0 +1,14 @@ +// RUN: %exits-with 2 %baredafny verify %args --type-system-refresh --general-newtypes "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +newtype FunMap = s: map T> | true {} + +datatype A = A(a: FunMap) + +method Test() { + +} + +method Main() { + Test>(); // Error: A does not support equality +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy.expect new file mode 100644 index 0000000000..abe28f371f --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5972c.dfy.expect @@ -0,0 +1,2 @@ +git-issue-5972c.dfy(13,14): Error: type parameter (T) passed to method Test must support equality (got A) +1 resolution/type errors detected in git-issue-5972c.dfy From a66a597602187290ad8cd689809e377aaeaa8b3f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 16 Dec 2024 14:24:42 -0600 Subject: [PATCH 05/10] Fixed review --- Source/DafnyCore/Resolver/ModuleResolver.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index a8431bbd04..20c3de7ccc 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1669,7 +1669,7 @@ private void CheckForCyclesAmongRedirectingTypes(RedirectingTypeDecl dd, HashSet if (cycleErrorHasBeenReported.Contains(r)) { // An error has already been reported for this cycle, so don't report another. // Note, the representative, "r", may itself not be a const. - } else if (dd is SubsetTypeDecl or NewtypeDecl) { + } else if (dd is NewtypeDecl or SubsetTypeDecl) { ReportCallGraphCycleError(dd, $"recursive constraint dependency involving a {dd.WhatKind}"); cycleErrorHasBeenReported.Add(r); } @@ -2923,7 +2923,7 @@ void MarkSCCAsNotSupportingEquality() { // If returns true, the given type never supports equality // If return false, then the type must support equality if type parameters support equality // It is unsound for a type to make this function return false when there is no type parameter - // assignment that amkes this type support equality + // assignment that makes this type support equality public static bool SurelyNeverSupportEquality(Type type) { type = type.Normalize(); return From 52c304a29184bc195d78bb0d754105e2b1201ce3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 16 Dec 2024 16:24:56 -0600 Subject: [PATCH 06/10] Fixed CI --- Scripts/test.sh | 4 ++-- Source/DafnyCore/Resolver/ModuleResolver.cs | 3 +++ .../LitTest/dafny0/EqualityTypes.dfy.expect | 18 +++++++++--------- .../EqualityTypesModuleExports.dfy.expect | 8 ++++---- 4 files changed, 18 insertions(+), 15 deletions(-) diff --git a/Scripts/test.sh b/Scripts/test.sh index 24225f4fdc..c094b52c53 100644 --- a/Scripts/test.sh +++ b/Scripts/test.sh @@ -28,7 +28,7 @@ if [ "$build_flag" = "false" ]; then output_dir="${framework_dir}/TestFiles/LitTests/LitTest" # Find and copy all matching files to the output directory - files=$(cd "$lit_tests_dir" && find . -type f -wholename "*$name*") + files=$(cd "$lit_tests_dir" && find . -type f -regex '.*\.\(check\|dfy\|expect\)' -wholename "*$name*") if [ -z "$files" ]; then echo "No files found matching pattern: $name" exit 1 @@ -40,7 +40,7 @@ if [ "$build_flag" = "false" ]; then # Copy files echo "$files" | while IFS= read -r file; do echo "Copying $file to $output_dir" - cp "$lit_tests_dir/$file" "$output_dir/" + cp "$lit_tests_dir/$file" "$output_dir/$file" done fi diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 20c3de7ccc..da1c712ad8 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2941,6 +2941,9 @@ public static void DetermineEqualitySupportType(Type type, ref bool thingsChange } else if (type.Normalize() is UserDefinedType userDefinedType) { if (userDefinedType.ResolvedClass is TypeSynonymDeclBase typeSynonymDecl) { if (typeSynonymDecl.IsRevealedInScope(Type.GetScope())) { + if (typeSynonymDecl.Characteristics.EqualitySupport == TypeParameter.EqualitySupportValue.Required) { + return; // It's guaranteed that this type synonym requires equality + } DetermineEqualitySupportType(typeSynonymDecl.RhsWithArgument(userDefinedType.TypeArgs), ref thingsChanged); } } else if (userDefinedType.ResolvedClass is NewtypeDecl newtypeDecl) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypes.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypes.dfy.expect index 2064c93913..a25a0eccfb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypes.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypes.dfy.expect @@ -4,7 +4,7 @@ EqualityTypes.dfy(40,11): Error: datatype 'X' is declared with a different numbe EqualityTypes.dfy(41,8): Error: class 'Y' is declared with a different number of type parameters (1 instead of 0) than the corresponding class in the module it refines EqualityTypes.dfy(45,11): Error: to be a refinement of abstract type 'C.X' declared with (==), datatype 'G.X' must support equality EqualityTypes.dfy(46,11): Error: to be a refinement of abstract type 'C.Y' declared with (==), datatype 'G.Y' must support equality -EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) +EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt) (perhaps try declaring type parameter 'T' on line 65 as 'T(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(85,9): Error: type parameter (T) passed to method M must support equality (got _T0) (perhaps try declaring type parameter '_T0' on line 81 as '_T0(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D) EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D) @@ -69,17 +69,17 @@ EqualityTypes.dfy(340,16): Error: in can only be applied to expressions of seque EqualityTypes.dfy(359,11): Error: type parameter (A) passed to type JustOpaque must support equality (got ABC) (perhaps try declaring abstract type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(360,11): Error: type parameter (A) passed to type Synonym must support equality (got ABC) (perhaps try declaring abstract type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(361,11): Error: type parameter (A) passed to type Subset must support equality (got ABC) (perhaps try declaring abstract type 'ABC' on line 354 as 'ABC(==)', which says it can only be instantiated with a type that supports equality) -EqualityTypes.dfy(376,9): Error: == can only be applied to expressions of types that support equality (got List) -EqualityTypes.dfy(378,9): Error: == can only be applied to expressions of types that support equality (got List) -EqualityTypes.dfy(381,9): Error: == can only be applied to expressions of types that support equality (got List) -EqualityTypes.dfy(386,9): Error: == can only be applied to expressions of types that support equality (got (A, List)) +EqualityTypes.dfy(376,9): Error: == can only be applied to expressions of types that support equality (got List) (perhaps try declaring type parameter 'A' on line 373 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(378,9): Error: == can only be applied to expressions of types that support equality (got List) (perhaps try declaring type parameter 'A' on line 373 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(381,9): Error: == can only be applied to expressions of types that support equality (got List) (perhaps try declaring type parameter 'A' on line 373 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(386,9): Error: == can only be applied to expressions of types that support equality (got (A, List)) (perhaps try declaring type parameter 'A' on line 384 as 'A(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(392,9): Error: == can only be applied to expressions of types that support equality (got GhostRecord) EqualityTypes.dfy(397,9): Error: == can only be applied to expressions of types that support equality (got Co) EqualityTypes.dfy(412,8): Error: set argument type must support equality (got A) (perhaps try declaring type parameter 'A' on line 410 as 'A(==)', which says it can only be instantiated with a type that supports equality) -EqualityTypes.dfy(416,12): Error: in can only be applied to expressions of sequence types that support equality (got seq) -EqualityTypes.dfy(419,20): Error: in can only be applied to expressions of sequence types that support equality (got seq) -EqualityTypes.dfy(423,15): Error: <= can only be applied to expressions of sequence types that support equality (got seq) -EqualityTypes.dfy(427,8): Error: set argument type must support equality (got (A, B)) +EqualityTypes.dfy(416,12): Error: in can only be applied to expressions of sequence types that support equality (got seq) (perhaps try declaring type parameter 'A' on line 414 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(419,20): Error: in can only be applied to expressions of sequence types that support equality (got seq) (perhaps try declaring type parameter 'A' on line 414 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(423,15): Error: <= can only be applied to expressions of sequence types that support equality (got seq) (perhaps try declaring type parameter 'A' on line 414 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypes.dfy(427,8): Error: set argument type must support equality (got (A, B)) (perhaps try declaring type parameter 'B' on line 425 as 'B(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(429,8): Error: set argument type must support equality (got B) (perhaps try declaring type parameter 'B' on line 425 as 'B(==)', which says it can only be instantiated with a type that supports equality) EqualityTypes.dfy(436,8): Error: map domain type must support equality (got A) (perhaps try declaring type parameter 'A' on line 434 as 'A(==)', which says it can only be instantiated with a type that supports equality) 84 resolution/type errors detected in EqualityTypes.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy.expect index cc5719be68..3a65091043 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy.expect @@ -20,8 +20,8 @@ EqualityTypesModuleExports.dfy(13,23): Error: set argument type must support equ EqualityTypesModuleExports.dfy(32,15): Error: type parameter (X) passed to function Fib must support equality (got Y) (perhaps try declaring type parameter 'Y' on line 26 as 'Y(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(32,23): Error: set argument type must support equality (got Y) (perhaps try declaring type parameter 'Y' on line 26 as 'Y(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(34,13): Error: set argument type must support equality (got GG) (perhaps try declaring type parameter 'GG' on line 21 as 'GG(==)', which says it can only be instantiated with a type that supports equality) -EqualityTypesModuleExports.dfy(84,7): Error: type 'Syn4' declared as supporting equality, but the RHS type ((real, A)) might not -EqualityTypesModuleExports.dfy(92,7): Error: type 'Subset4' declared as supporting equality, but the RHS type ((A, int)) might not +EqualityTypesModuleExports.dfy(84,7): Error: type 'Syn4' declared as supporting equality, but the RHS type ((real, A)) might not (perhaps try declaring type parameter 'A' on line 84 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypesModuleExports.dfy(92,7): Error: type 'Subset4' declared as supporting equality, but the RHS type ((A, int)) might not (perhaps try declaring type parameter 'A' on line 92 as 'A(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(149,7): Error: recursive constraint dependency involving a subset type: SubsetCo -> Co -> SubsetCo EqualityTypesModuleExports.dfy(162,11): Error: type parameter (A) passed to type MyClass must support equality (got Noeq) EqualityTypesModuleExports.dfy(163,11): Error: type parameter (A) passed to type Dt must support equality (got Noeq) @@ -47,8 +47,8 @@ EqualityTypesModuleExports.dfy(287,7): Error: == can only be applied to expressi EqualityTypesModuleExports.dfy(290,7): Error: == can only be applied to expressions of types that support equality (got WWW0.ZT) EqualityTypesModuleExports.dfy(293,7): Error: == can only be applied to expressions of types that support equality (got WWW0.WT) EqualityTypesModuleExports.dfy(318,7): Error: type 'A' declared as supporting equality, but the RHS type (QQQ1.Syn) might not -EqualityTypesModuleExports.dfy(333,7): Error: type 'ExportedType' declared as supporting equality, but the RHS type (PrivateType) might not -EqualityTypesModuleExports.dfy(381,4): Error: == can only be applied to expressions of types that support equality (got List) +EqualityTypesModuleExports.dfy(333,7): Error: type 'ExportedType' declared as supporting equality, but the RHS type (PrivateType) might not (perhaps try declaring type parameter 'A' on line 333 as 'A(==)', which says it can only be instantiated with a type that supports equality) +EqualityTypesModuleExports.dfy(381,4): Error: == can only be applied to expressions of types that support equality (got List) (perhaps try declaring type parameter 'A' on line 379 as 'A(==)', which says it can only be instantiated with a type that supports equality) EqualityTypesModuleExports.dfy(401,9): Warning: this export set is empty (did you perhaps forget the 'provides' or 'reveals' keyword?) EqualityTypesModuleExports.dfy(444,7): Error: type 'Synonym' declared as being nonempty, but the RHS type (Empty) may be empty EqualityTypesModuleExports.dfy(445,7): Error: type 'AnotherSynonym' declared as being nonempty, but the RHS type (Empty) may be empty From 9e0336645f8b54ba6c9b39157c8feb864992cf63 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 16 Dec 2024 17:06:57 -0600 Subject: [PATCH 07/10] Fixed CI --- .../LitTests/LitTest/dafny0/ResolutionErrors7.dfy.expect | 8 ++++---- .../LitTest/dafny0/ResolutionErrors7.dfy.refresh.expect | 8 ++++---- .../LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect | 2 +- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.expect index 1626ac4890..2f9f7d8468 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.expect @@ -36,10 +36,10 @@ ResolutionErrors7.dfy(175,19): Error: type parameter (T) passed to function GetI ResolutionErrors7.dfy(183,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(188,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(190,23): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) -ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) -ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) -ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) +ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(202,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 199 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(211,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 199 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(229,11): Error: type parameter (T) passed to function MustBeNonempty must be nonempty (got PossiblyEmpty) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.refresh.expect index 1626ac4890..2f9f7d8468 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors7.dfy.refresh.expect @@ -36,10 +36,10 @@ ResolutionErrors7.dfy(175,19): Error: type parameter (T) passed to function GetI ResolutionErrors7.dfy(183,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(188,13): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(190,23): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) -ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) -ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) -ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) -ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) +ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors7.dfy(192,14): Error: type parameter 0 (T) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) +ResolutionErrors7.dfy(193,15): Error: type parameter 1 (U) passed to type QuadEq must support equality (got seq) (perhaps try declaring type parameter 'T' on line 182 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(202,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 199 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(211,15): Error: == can only be applied to expressions of types that support equality (got T) (perhaps try declaring type parameter 'T' on line 199 as 'T(==)', which says it can only be instantiated with a type that supports equality) ResolutionErrors7.dfy(229,11): Error: type parameter (T) passed to function MustBeNonempty must be nonempty (got PossiblyEmpty) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect index 505d7f7f15..3d5af051e0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeInstantiations.dfy.expect @@ -15,7 +15,7 @@ TypeInstantiations.dfy(57,15): Error: type parameters are not allowed to be rena TypeInstantiations.dfy(34,11): Error: to be a refinement of abstract type 'M0.C' declared with (==), datatype 'M1.C' must support equality TypeInstantiations.dfy(35,7): Error: to be a refinement of abstract type 'M0.D' declared with (==), type synonym 'M1.D' must support equality TypeInstantiations.dfy(36,13): Error: to be a refinement of abstract type 'M0.E' declared with (==), codatatype 'M1.E' must support equality -TypeInstantiations.dfy(48,7): Error: to be a refinement of abstract type 'M0.N' declared with (==), type synonym 'M1.N' must support equality +TypeInstantiations.dfy(48,7): Error: to be a refinement of abstract type 'M0.N' declared with (==), type synonym 'M1.N' must support equality (perhaps try declaring type parameter 'U' on line 48 as 'U(==)', which says it can only be instantiated with a type that supports equality) TypeInstantiations.dfy(69,29): Error: RHS (of type List) not assignable to LHS (of type MyList.List) (non-variant type parameter would require real = int) TypeInstantiations.dfy(81,8): Error: the type of this variable is underspecified TypeInstantiations.dfy(82,8): Error: the type of this variable is underspecified From c938b2bd1b96567b836f7d0ed2726e84c3665415 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 17 Dec 2024 14:12:35 -0600 Subject: [PATCH 08/10] More precise return of SurelyNeverSupportEquality --- Source/DafnyCore/Resolver/ModuleResolver.cs | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index c359f6efed..ede05b5191 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2920,15 +2920,27 @@ void MarkSCCAsNotSupportingEquality() { } } + public static bool SurelyNeverSupportEqualityTypeParameters(IndDatatypeDecl.ES equalitySupport, List typeParams, List typeArgs) { + return + equalitySupport == IndDatatypeDecl.ES.Never || + equalitySupport == IndDatatypeDecl.ES.ConsultTypeArguments && + typeArgs.Zip(typeParams).Any(tt => + tt.Item2.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && SurelyNeverSupportEquality(tt.Item1)); + } + // If returns true, the given type never supports equality // If return false, then the type must support equality if type parameters support equality // It is unsound for a type to make this function return false when there is no type parameter // assignment that makes this type support equality public static bool SurelyNeverSupportEquality(Type type) { - type = type.Normalize(); + type = type.NormalizeExpand(); return - type.AsNewtype is { EqualitySupport: IndDatatypeDecl.ES.Never } || - type.AsIndDatatype is { EqualitySupport: IndDatatypeDecl.ES.Never } || + type.AsNewtype is { EqualitySupport: var equalitySupport, TypeArgs: var typeParams } + && SurelyNeverSupportEqualityTypeParameters(equalitySupport, typeParams, type.TypeArgs) + || + type.AsIndDatatype is { EqualitySupport: var equalitySupport2, TypeArgs: var typeParams2 } + && SurelyNeverSupportEqualityTypeParameters(equalitySupport2, typeParams2, type.TypeArgs) + || type.IsCoDatatype || type.IsArrowType || type.AsSeqType is { Arg: var argType } && SurelyNeverSupportEquality(argType) || type.AsMapType is { Range: var rangeType } && SurelyNeverSupportEquality(rangeType); From d7b7f072292fd1891627aaa7703c5ea0bf2c132d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 12 Dec 2024 15:27:37 -0800 Subject: [PATCH 09/10] Format comment better --- Source/DafnyCore/Resolver/ModuleResolver.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index ede05b5191..dcdfaa3dbf 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2982,7 +2982,8 @@ public static void DetermineEqualitySupportType(Type type, ref bool thingsChange } } else if (type.AsMapType is { } typeMap) { // A map type's Domain type is required to support equality (just like the argument type for sets and multisets), but - // it is optional for the map type's Range type to support equality. Thus, we need to determine the equality support for just the Range type. + // it is optional for the map type's Range type to support equality. Thus, we need to determine the equality support + // for just the Range type. DetermineEqualitySupportType(typeMap.Range, ref thingsChanged); } else if (type.AsSeqType is { } typeSeq) { // Like the Range type of a map, it is optional for a sequence type's argument type to support equality. So, we make a call From ec2ab42871fa59fb0df96b29d9dfc02cddc82e02 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 17 Dec 2024 12:36:16 -0800 Subject: [PATCH 10/10] chore: Use parens around || vs && --- Source/DafnyCore/Resolver/ModuleResolver.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index dcdfaa3dbf..c919823ac4 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -2923,9 +2923,9 @@ void MarkSCCAsNotSupportingEquality() { public static bool SurelyNeverSupportEqualityTypeParameters(IndDatatypeDecl.ES equalitySupport, List typeParams, List typeArgs) { return equalitySupport == IndDatatypeDecl.ES.Never || - equalitySupport == IndDatatypeDecl.ES.ConsultTypeArguments && - typeArgs.Zip(typeParams).Any(tt => - tt.Item2.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && SurelyNeverSupportEquality(tt.Item1)); + (equalitySupport == IndDatatypeDecl.ES.ConsultTypeArguments && + typeArgs.Zip(typeParams).Any(tt => + tt.Item2.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && SurelyNeverSupportEquality(tt.Item1))); } // If returns true, the given type never supports equality