Fix a bug related to abstract imports and match expressions (#5811)

Fixes #5808

### Description
- Add a call to `new MatchFlattener(reporter).PostResolve(module);`
after cloning elements for abstract imports, so `.Flattened` is set.
- Fix the behavior of the `afterChildren` parameter in `Node.Visit`, so
that closure is actually only called after the children are visited.

### How has this been tested?
Added a CLI 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>

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs

@@ -28,6 +28,7 @@ public NestedMatchExpr(Cloner cloner, NestedMatchExpr original) : base(cloner, o
     this.Source = cloner.CloneExpr(original.Source);
     this.Cases = original.Cases.Select(cloner.CloneNestedMatchCaseExpr).ToList();
     this.UsesOptionalBraces = original.UsesOptionalBraces;
+
     if (cloner.CloneResolvedFields) {
       Flattened = cloner.CloneExpr(original.Flattened);
     }

Source/DafnyCore/Generic/Node.cs

@@ -6,6 +6,7 @@
 using System.Text.RegularExpressions;
 using Microsoft.Boogie;
 using Microsoft.Dafny.Auditor;
+using Action = System.Action;
 
 namespace Microsoft.Dafny;
 
@@ -144,37 +145,44 @@ public virtual IEnumerable<Assumption> Assumptions(Declaration decl) {
   public ISet<INode> Visit(Func<INode, bool> beforeChildren = null, Action<INode> afterChildren = null, Action<Exception> reportError = null) {
     reportError ??= _ => { };
     beforeChildren ??= node => true;
-    afterChildren ??= node => { };
 
     var visited = new HashSet<INode>();
-    var toVisit = new LinkedList<INode>();
+    var toVisit = new LinkedList<object>();
     toVisit.AddFirst(this);
     while (toVisit.Any()) {
       var current = toVisit.First();
       toVisit.RemoveFirst();
-      if (!visited.Add(current)) {
-        continue;
-      }
-
-      if (!beforeChildren(current)) {
-        continue;
-      }
+      if (current is INode currentNode) {
+        if (!visited.Add(currentNode)) {
+          continue;
+        }
 
-      var nodeAfterChildren = toVisit.First;
-      foreach (var child in current.Children) {
-        if (child == null) {
-          reportError(new InvalidOperationException($"Object of type {current.GetType()} has null child"));
+        if (!beforeChildren(currentNode)) {
           continue;
         }
 
-        if (nodeAfterChildren == null) {
-          toVisit.AddLast(child);
-        } else {
-          toVisit.AddBefore(nodeAfterChildren, child);
+        if (afterChildren != null) {
+          void AfterNodeChildren() => afterChildren(currentNode);
+          toVisit.AddFirst((Action)AfterNodeChildren);
         }
-      }
+        var nodeAfterChildren = toVisit.First;
+        foreach (var child in currentNode.Children) {
+          if (child == null) {
+            reportError(new InvalidOperationException($"Object of type {current.GetType()} has null child"));
+            continue;
+          }
 
-      afterChildren(current);
+          if (nodeAfterChildren == null) {
+            toVisit.AddLast(child);
+          } else {
+            // Depth-first, but with children in unreversed order
+            toVisit.AddBefore(nodeAfterChildren, child);
+          }
+        }
+      } else {
+        var currentAction = (Action)current;
+        currentAction();
+      }
     }
 
     return visited;

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -811,38 +811,55 @@ public void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) {
       f.ByMethodDecl = method;
     }
 
-    private ModuleSignature MakeAbstractSignature(ModuleSignature p, string name, int height,
-      Dictionary<ModuleDefinition, ModuleSignature> mods) {
-      Contract.Requires(p != null);
+    private ModuleSignature MakeAbstractSignature(ModuleSignature origin, string name, int height,
+      Dictionary<ModuleDefinition, ModuleSignature> moduleSignatures) {
+      Contract.Requires(origin != null);
       Contract.Requires(name != null);
-      Contract.Requires(mods != null);
+      Contract.Requires(moduleSignatures != null);
       var errCount = reporter.Count(ErrorLevel.Error);
 
-      var mod = new ModuleDefinition(RangeToken.NoToken, new Name(name + ".Abs"), new List<IToken>(), ModuleKindEnum.Abstract, true, null, null, null);
-      mod.Height = height;
-      foreach (var kv in p.TopLevels) {
+      var module = new ModuleDefinition(RangeToken.NoToken, new Name(name + ".Abs"), new List<IToken>(), ModuleKindEnum.Abstract, true, null, null, null);
+      module.Height = height;
+      foreach (var kv in origin.TopLevels) {
         if (!(kv.Value is NonNullTypeDecl or DefaultClassDecl)) {
-          var clone = CloneDeclaration(p.VisibilityScope, kv.Value, mod, mods, name);
-          mod.SourceDecls.Add(clone);
+          var clone = CloneDeclarationForAbstractSignature(origin.VisibilityScope, kv.Value, module, moduleSignatures, name);
+          module.SourceDecls.Add(clone);
         }
       }
 
-      var defaultClassDecl = new DefaultClassDecl(mod, p.StaticMembers.Values.ToList());
-      mod.DefaultClass = (DefaultClassDecl)CloneDeclaration(p.VisibilityScope, defaultClassDecl, mod, mods, name);
+      var defaultClassDecl = new DefaultClassDecl(module, origin.StaticMembers.Values.ToList());
+      module.DefaultClass = (DefaultClassDecl)CloneDeclarationForAbstractSignature(origin.VisibilityScope, defaultClassDecl, module, moduleSignatures, name);
+
+      var sig = module.RegisterTopLevelDecls(this, true);
+      sig.Refines = origin.Refines;
+      sig.IsAbstract = origin.IsAbstract;
+      moduleSignatures.Add(module, sig);
 
-      var sig = mod.RegisterTopLevelDecls(this, true);
-      sig.Refines = p.Refines;
-      sig.IsAbstract = p.IsAbstract;
-      mods.Add(mod, sig);
-      var good = mod.Resolve(sig, this);
+      var good = module.Resolve(sig, this);
       if (good && reporter.Count(ErrorLevel.Error) == errCount) {
-        mod.SuccessfullyResolved = true;
+        module.SuccessfullyResolved = true;
       }
 
+      /* A bug we ran into was that cloning done for abstract modules,
+        did not clone the resolved field,
+        so the .Flattened field of NestedMatchExpr was not set.
+        Also, rewriters.PostResolve was not run, so .Flattened was not set after cloning
+        which led to a crash during Boogie generation.
+       
+        Cloning with resolved fields is not an option, 
+        because then internal references of the cloned code can point to the old code.
+       
+        I(keyboardDrummer) think it would be better altogether if no cloning was done for abstract modules,
+        But until that happens here is code that explicitly calls MatchFlattener which sets .Flattened
+        Alternatively, we could call all the rewriter.PostResolve methods
+      */
+
+      new MatchFlattener(reporter).PostResolve(module);
+
       return sig;
     }
 
-    TopLevelDecl CloneDeclaration(VisibilityScope scope, TopLevelDecl d, ModuleDefinition newParent,
+    TopLevelDecl CloneDeclarationForAbstractSignature(VisibilityScope scope, TopLevelDecl d, ModuleDefinition newParent,
       Dictionary<ModuleDefinition, ModuleSignature> mods, string name) {
       Contract.Requires(d != null);
       Contract.Requires(newParent != null);

Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/abstractModuleAndMatchFlattening.dfy

@@ -0,0 +1,14 @@
+// RUN: %verify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+abstract module FooM {
+
+  method Foo(x: int) returns (r: int) modifies match x { case 0 => {} case _ => {} } ensures r == 3
+}
+
+abstract module Bla {
+  import Operations : FooM
+
+  method Foo(x: int) returns (r: int) {
+    r := Operations.Foo(3);
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/abstractModuleAndMatchFlattening.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/5808.fix

@@ -0,0 +1 @@
+Enable abstract imports to work well with match expression that occur in specifications