fix: Account for the optional equality support of map/seq inside newt…

…ypes (#5980) This PR extends fix #5973 of issue #5972 to also handle newtypes, subset types, and type synonyms wrapped around map and sequence types. Fixes #5978 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Mikael Mayer <[email protected]> Co-authored-by: Mikaël Mayer <[email protected]>
dafny-lang · Dec 17, 2024 · 648da0e · 648da0e
1 parent 883ae1a
commit 648da0e
Show file tree

Hide file tree

Showing 19 changed files with 616 additions and 115 deletions.
diff --git a/Makefile b/Makefile
@@ -30,27 +30,16 @@ boogie: ${DIR}/boogie/Binaries/Boogie.exe
 tests:
 	(cd "${DIR}"; dotnet test Source/IntegrationTests)
 
-# make test name=<part of the path of an integration test>
+# make test name=<integration test filter>
+# make test name=<integration test filter> update=true                to update the test
+# make test name=<integration test filter>              build=false   don't build the solution
 test:
-	(cd "${DIR}"; [ -z "${name}" ] && echo "Syntax: make test name=<integration test filter>" && exit 1; dotnet test Source/IntegrationTests --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-run name=<part of the path> action="run ..."
+# make test-dafny name=<part of the path> 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
@@ -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
diff --git a/Scripts/test.sh 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=<integration test filter> [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 -regex '.*\.\(check\|dfy\|expect\)' -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/$file"
+  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
@@ -96,13 +96,21 @@ public Type RhsWithArgument(List<Type> 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/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/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 "";
   }
 }
diff --git 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
@@ -2884,8 +2880,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);
           }
         }
       }
@@ -2925,30 +2920,75 @@ void MarkSCCAsNotSupportingEquality() {
       }
     }
 
-    private static void DetermineEqualitySupportType(Type type, ref bool thingsChanged) {
+    public static bool SurelyNeverSupportEqualityTypeParameters(IndDatatypeDecl.ES equalitySupport, List<TypeParameter> typeParams, List<Type> 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.NormalizeExpand();
+      return
+        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);
+    }
+
+    public static void DetermineEqualitySupportType(Type type, ref bool thingsChanged) {
       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.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) {
+          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/DafnyCore/Resolver/TypeCharacteristicChecker.cs b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs
@@ -237,8 +237,8 @@ private static void Check(List<TopLevelDecl> 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",