Fix: Compiled disjunctive nested pattern matching no longer crashing (#…

…5574) This PR fixes #5572 I added the corresponding test. <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: Remy Willems <[email protected]>
dafny-lang · Jun 26, 2024 · eb2d95b · eb2d95b
1 parent 992cbf8
commit eb2d95b
Show file tree

Hide file tree

Showing 9 changed files with 2,714 additions and 2,764 deletions.
diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs
diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs
@@ -22,10 +22,12 @@ public class IdPattern : ExtendedPattern, IHasReferences {
   public DatatypeCtor Ctor;
 
   public bool IsWildcardPattern =>
-    Arguments == null && Id.StartsWith("_");
+    Arguments == null && Id.StartsWith(WildcardString);
 
   public bool IsWildcardExact =>
-    Arguments == null && Id == "_";
+    Arguments == null && Id == WildcardString;
+
+  public const string WildcardString = "_";
 
   public void MakeAConstructor() {
     this.Arguments = new List<ExtendedPattern>();

diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs
@@ -594,6 +594,10 @@ private ConcreteSyntaxTree EmitNestedMatchCaseConditions(string sourceName,
         writer = thenWriter;
       } else if (pattern is IdPattern idPattern) {
         if (idPattern.BoundVar != null) {
+          if (idPattern.BoundVar.Tok.val.StartsWith(IdPattern.WildcardString)) {
+            return writer;
+          }
+
           var boundVar = idPattern.BoundVar;
           var valueWriter = DeclareLocalVar(IdName(boundVar), boundVar.Type, idPattern.Tok, writer);
           valueWriter.Write(sourceName);
@@ -651,9 +655,11 @@ private ConcreteSyntaxTree EmitNestedMatchStmtCaseConstructor(string sourceName,
           var childPattern = idPattern.Arguments[index];
           if (childPattern is IdPattern { BoundVar: not null } childIdPattern) {
             var boundVar = childIdPattern.BoundVar;
-            newSourceName = IdName(boundVar);
-            var valueWriter = DeclareLocalVar(newSourceName, boundVar.Type, idPattern.Tok, result);
-            valueWriter.Append(destructor);
+            if (!childIdPattern.BoundVar.Name.StartsWith(IdPattern.WildcardString)) {
+              newSourceName = IdName(boundVar);
+              var valueWriter = DeclareLocalVar(newSourceName, boundVar.Type, idPattern.Tok, result);
+              valueWriter.Append(destructor);
+            }
           } else {
             newSourceName = ProtectedFreshId(arg.CompileName);
             var valueWriter = DeclareLocalVar(newSourceName, type, idPattern.Tok, result);

diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs b/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs
@@ -17,12 +17,12 @@ public static BigInteger SeqToHeight<__T>(Dafny.ISequence<__T> s, Func<__T, BigI
       if ((new BigInteger((s).Count)).Sign == 0) {
         return BigInteger.Zero;
       } else {
-        BigInteger _763_i = Dafny.Helpers.Id<Func<__T, BigInteger>>(f)((s).Select(BigInteger.Zero));
-        BigInteger _764_j = DAST.Format.__default.SeqToHeight<__T>((s).Drop(BigInteger.One), f);
-        if ((_763_i) < (_764_j)) {
-          return _764_j;
+        BigInteger _759_i = Dafny.Helpers.Id<Func<__T, BigInteger>>(f)((s).Select(BigInteger.Zero));
+        BigInteger _760_j = DAST.Format.__default.SeqToHeight<__T>((s).Drop(BigInteger.One), f);
+        if ((_759_i) < (_760_j)) {
+          return _760_j;
         } else {
-          return _763_i;
+          return _759_i;
         }
       }
     }

diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
diff --git a/Source/DafnyCore/GeneratedFromDafny/RAST.cs b/Source/DafnyCore/GeneratedFromDafny/RAST.cs
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5572.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5572.dfy
@@ -0,0 +1,14 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+datatype D = A(int) | C(int) {
+  function Test(): D {
+    match this{
+      case A(_) | C(_) =>
+        this
+    }
+  }
+}
+method Main() {
+  var x := C(0).Test();
+  print "ok";
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5572.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5572.dfy.expect
@@ -0,0 +1 @@
+ok
diff --git a/docs/dev/news/5572.fix b/docs/dev/news/5572.fix
@@ -0,0 +1 @@
+Compiled disjunctive nested pattern matching no longer crashing
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Compiled disjunctive nested pattern matching no longer crashing