Fix extern contract checking on abstract modules (dafny-lang#4910)

### Description

Previously, compiling an abstract module with an `{:extern}` method
using `--test-assumptions Externs` would cause an assertion failure.
This was due to interleaving between the contract checking wrapper
generator and the module refinement rewriter. This PR fixes the problem
by generating contract checking wrappers for the whole program after
resolution is finished, rather than as each module finishes resolution.

Fixes dafny-lang#4845

### How has this been tested?

Tested by `contract-wrappers/RefineContract.dfy`.

By submitting this pull request, I confirm that my contribution is made
under the terms of the MIT license.

Source/DafnyCore/Rewriters/ExpectContracts.cs

@@ -1,7 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using Microsoft.Extensions.Logging.Abstractions;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny;
@@ -222,39 +221,50 @@ private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers
   }
 
   /// <summary>
-  /// Add wrappers for certain top-level declarations in the given module.
-  /// This runs after the first pass of resolution so that it has access to
-  /// ghostness information, attributes and call targets.
+  /// Adds wrappers for certain top-level declarations in the given
+  /// program and redirects callers to call those wrappers instead of
+  /// the original members.
+  ///
+  /// This runs after resolution so that it has access to ghostness
+  /// information, attributes and call targets and after verification
+  /// because that makes the interaction with the refinement transformer
+  /// more straightforward.
   /// </summary>
-  /// <param name="moduleDefinition">The module to generate wrappers for and in.</param>
-  internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition) {
-    // Keep a list of members to wrap so that we don't modify the collection we're iterating over.
-    List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new();
-
-    moduleDefinition.CallRedirector = new(Reporter);
-
-    // Find module members to wrap.
-    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-      foreach (var decl in topLevelDecl.Members) {
-        if (ShouldGenerateWrapper(decl)) {
-          membersToWrap.Add((topLevelDecl, decl));
+  /// <param name="program">The program to generate wrappers for and in.</param>
+  public override void PostVerification(Program program) {
+    // Create wrappers
+    foreach (var moduleDefinition in program.Modules()) {
+
+      // Keep a list of members to wrap so that we don't modify the collection we're iterating over.
+      List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new();
+
+      moduleDefinition.CallRedirector = new(Reporter);
+
+      // Find module members to wrap.
+      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+        foreach (var decl in topLevelDecl.Members) {
+          if (ShouldGenerateWrapper(decl)) {
+            membersToWrap.Add((topLevelDecl, decl));
+          }
         }
       }
-    }
 
-    // Generate a wrapper for each of the members identified above.
-    foreach (var (topLevelDecl, decl) in membersToWrap) {
-      GenerateWrapper(moduleDefinition, topLevelDecl, decl);
-    }
-    moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations;
-  }
+      // Generate a wrapper for each of the members identified above. This
+      // need to happen after all declarations to wrap have been identified
+      // because it adds new declarations and would invalidate the iterator
+      // used during identification.
+      foreach (var (topLevelDecl, decl) in membersToWrap) {
+        GenerateWrapper(moduleDefinition, topLevelDecl, decl);
+      }
+      moduleDefinition.CallRedirector.NewRedirections = wrappedDeclarations;
 
-  public override void PostVerification(Program program) {
-    foreach (var module in program.CompileModules) {
-      foreach (var topLevelDecl in module.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      // Put redirections in place. Any wrappers to call will be in either
+      // this module or to a previously-processed module, so they'll already
+      // exist.
+      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
         foreach (var decl in topLevelDecl.Members) {
           if (decl is ICallable callable) {
-            module.CallRedirector?.Visit(callable, decl);
+            moduleDefinition.CallRedirector?.Visit(callable, decl);
           }
         }
       }
@@ -264,7 +274,7 @@ public override void PostVerification(Program program) {
       return;
     }
 
-    foreach (var module in program.CompileModules) {
+    foreach (var module in program.Modules()) {
       if (module.CallRedirector == null) {
         continue;
       }

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern1.cs

@@ -0,0 +1,10 @@
+using System.Numerics;
+
+namespace M {
+
+  public partial class __default {
+    public static BigInteger ExternMethod() {
+      return new BigInteger(5);
+    }
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AbstractExtern2.cs

@@ -0,0 +1,10 @@
+using System.Numerics;
+
+namespace M {
+
+  public partial class __default {
+    public static BigInteger ExternMethod() {
+      return new BigInteger(-5);
+    }
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %baredafny test %args --no-verify --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t
+// RUN: ! %baredafny test %args --unicode-char:false --test-assumptions=externs %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s"
 // CHECK: .*Foo____dafny__checked\(x\).*

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/AllExterns.dfy.expect

@@ -1,7 +1,7 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
 CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.
 CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state.
-
-Dafny program verifier did not attempt verification
 FooTest: FAILED
 	CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12)
 BarTest: FAILED

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/RefineContract.dfy

@@ -0,0 +1,14 @@
+// RUN: %run "%s" --input "%S/AbstractExtern1.cs" --test-assumptions Externs
+// RUN: %exits-with 3 %run "%s" --input "%S/AbstractExtern2.cs" --test-assumptions Externs
+abstract module A {
+    method {:extern "ExternMethod"} Method() returns (r: int)
+      ensures r > 0
+}
+
+module M refines A {
+}
+
+method Main() {
+  var x := M.Method();
+  print x, "\n";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy

@@ -1,4 +1,4 @@
-// RUN: ! %dafny /compile:4 /noVerify /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t
+// RUN: ! %dafny /compile:4 /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/TestedExterns.cs" "%s"
 // CHECK-NOT: .*Foo____dafny__checked\(x\).*

Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect

@@ -1,7 +1,7 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
 CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state.
 CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state.
-
-Dafny program verifier did not attempt verification
 TestedExterns.dfy(10,17): Warning: No :test code calls NotCalled
 FooTest: FAILED
 	CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12)