From 5f4fd1321896e2733292140908a737430f046815 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 29 Jul 2022 17:10:38 -0700
Subject: [PATCH 01/31] Basic contract-checking wrapper generator

This works on one example, but is know to fail for polymorphic code and
probably many other types, as well.
---
 Source/Dafny/AST/DafnyAst.cs             |   2 +-
 Source/Dafny/Cloner.cs                   |   2 +
 Source/Dafny/Resolver.cs                 |   3 +
 Source/Dafny/Resolver/ExpectContracts.cs | 135 +++++++++++++++++++++++
 4 files changed, 141 insertions(+), 1 deletion(-)
 create mode 100644 Source/Dafny/Resolver/ExpectContracts.cs

diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs
index 5e96d1610a0..8efd6025275 100644
--- a/Source/Dafny/AST/DafnyAst.cs
+++ b/Source/Dafny/AST/DafnyAst.cs
@@ -3184,7 +3184,7 @@ public static string IdProtect(string name) {
     public IToken BodyEndTok = Token.NoToken;
     public IToken StartToken = Token.NoToken;
     public IToken TokenWithTrailingDocString = Token.NoToken;
-    public readonly string Name;
+    public string Name;
     public bool IsRefining;
     IToken IRegion.BodyStartTok { get { return BodyStartTok; } }
     IToken IRegion.BodyEndTok { get { return BodyEndTok; } }
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index d405ce344cb..e865bb5bf85 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -673,6 +673,8 @@ public virtual Statement CloneStmt(Statement stmt) {
         var body = s.Body == null ? null : CloneBlockStmt(s.Body);
         r = new ModifyStmt(Tok(s.Tok), Tok(s.EndTok), mod.Expressions, mod.Attributes, body);
 
+      } else if (stmt is CallStmt s) {
+        r = new CallStmt(Tok(s.Tok), Tok(s.EndTok), s.Lhs, s.MethodSelect, s.Args);
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index adc0be0736d..168e6298a14 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -430,6 +430,9 @@ public void ResolveProgram(Program prog) {
         rewriters.Add(new TriggerGeneratingRewriter(reporter));
       }
 
+      // TODO: check option
+      rewriters.Add(new ExpectContracts(reporter));
+
       if (DafnyOptions.O.RunAllTests) {
         rewriters.Add(new RunAllTestsMainMethod(reporter));
       }
diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
new file mode 100644
index 00000000000..5fafc45b30c
--- /dev/null
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -0,0 +1,135 @@
+using System;
+using System.Collections.Generic;
+using System.Data;
+using System.Linq;
+using Microsoft.Boogie;
+using Microsoft.CodeAnalysis.CSharp.Syntax;
+
+namespace Microsoft.Dafny; 
+
+public class ExpectContracts : IRewriter {
+  private readonly ClonerButDropMethodBodies cloner = new();
+
+  public ExpectContracts(ErrorReporter reporter) : base(reporter) {
+  }
+
+  /// <summary>
+  /// Create an expect statement that checks the given contract clause
+  /// expression and fails with a message that points to the original
+  /// location of the contract clause if it is not true at runtime.
+  /// </summary>
+  /// <param name="expr">The contract clause expression to evaluate.</param>
+  /// <param name="exprType">Either "requires" or "ensures", to use in the
+  /// failure message.</param>
+  /// <returns>The newly-created expect statement.</returns>
+  private static Statement CreateContractExpectStatement(AttributedExpression expr, string exprType) {
+    var tok = expr.E.tok;
+    var msg = $"Runtime failure of {exprType} clause from {tok.filename}:{tok.line}:{tok.col}";
+    var msgExpr = Expression.CreateStringLiteral(tok, msg);
+    return new ExpectStmt(tok, expr.E.EndToken, expr.E, msgExpr, null);
+  }
+
+  /// <summary>
+  /// Creates a block statement that includes an expect statement for every
+  /// requires clause, followed by the provided call statement, followed by
+  /// an expect statement for every ensures clause.
+  /// </summary>
+  /// <param name="requires">The list of requires clause expressions.</param>
+  /// <param name="ensures">The list of ensures clause expressions.</param>
+  /// <param name="callStmt">The call statement to include.</param>
+  /// <returns>The newly-created block statement.</returns>
+  private static BlockStmt MakeContractCheckingBody(List<AttributedExpression> requires, List<AttributedExpression> ensures, Statement callStmt) {
+    var expectRequiresStmts = requires.Select(req =>
+      CreateContractExpectStatement(req, "requires"));
+    var expectEnsuresStmts = ensures.Select(ens =>
+      CreateContractExpectStatement(ens, "ensures"));
+    var callStmtList = new List<Statement>() { callStmt };
+    var bodyStatements = expectRequiresStmts.Concat(callStmtList).Concat(expectEnsuresStmts);
+    return new BlockStmt(callStmt.Tok, callStmt.EndTok, bodyStatements.ToList());
+  }
+
+  private bool ShouldGenerateWrapper(MemberDecl decl) {
+    // TODO: make this more discriminating
+    // TODO: could work for ghost statements eventually
+    return !decl.IsGhost && decl is not Constructor;
+  }
+
+  private void AddWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
+    var tok = decl.tok; // TODO: do better
+
+    if (decl is Method origMethod) {
+      var newMethod = cloner.CloneMethod(origMethod);
+      newMethod.Name = origMethod.Name + "_checked";
+
+      var args = newMethod.Ins.Select(Expression.CreateIdentExpr).ToList();
+      var outs = newMethod.Outs.Select(Expression.CreateIdentExpr).ToList();
+      var receiver = origMethod.IsStatic
+        ? (Expression)new StaticReceiverExpr(tok, parent, false)
+        : (Expression)new ThisExpr(parent);
+      var selector = new MemberSelectExpr(tok, receiver, origMethod.Name) {
+        Member = origMethod,
+        TypeApplication_JustMember = new List<Type>(), // TODO: fill in properly
+        TypeApplication_AtEnclosingClass = new List<Type>() // TODO: fill in properly
+      };
+      var callStmt = new CallStmt(tok, tok, outs, selector, args);
+
+      var body = MakeContractCheckingBody(origMethod.Req, origMethod.Ens, callStmt);
+      newMethod.Body = body;
+      parent.Members.Add(newMethod);
+    } else if (decl is Function origFunc) {
+      var newFunc = cloner.CloneFunction(origFunc);
+      newFunc.Name = origFunc.Name + "_checked";
+
+      var args = origFunc.Formals.Select(Expression.CreateIdentExpr).ToList();
+      var callExpr = new FunctionCallExpr(tok, origFunc.Name, new ThisExpr(tok), tok, tok, args);
+      newFunc.Body = callExpr;
+      var receiver = origFunc.IsStatic ?
+        (Expression)new StaticReceiverExpr(tok, parent, false) :
+        (Expression)new ThisExpr(parent);
+      var selector = new MemberSelectExpr(tok, receiver, origFunc.Name) {
+        Member = origFunc,
+        TypeApplication_JustMember = new List<Type>(), // TODO: fill in properly
+        TypeApplication_AtEnclosingClass = new List<Type>() // TODO: fill in properly
+      };
+
+      var localName = origFunc.Result?.Name ?? "__result";
+      var local = new LocalVariable(tok, tok, localName, origFunc.ResultType, false);
+      var localExpr = new IdentifierExpr(tok, localName);
+      var callRhs = new ExprRhs(callExpr);
+
+      var lhss = new List<Expression> { localExpr };
+      var locs = new List<LocalVariable> { local };
+      var rhss = new List<AssignmentRhs> { callRhs };
+
+      var callStmt = origFunc.Result?.Name is null
+        ? (Statement)new VarDeclStmt(tok, tok, locs, new UpdateStmt(tok, tok, lhss, rhss))
+        : (Statement)new AssignStmt(tok, tok, localExpr, callRhs);
+
+      var body = MakeContractCheckingBody(origFunc.Req, origFunc.Ens, callStmt);
+      body.AppendStmt(new ReturnStmt(tok, tok, new List<AssignmentRhs> { new ExprRhs(localExpr) }));
+      newFunc.ByMethodBody = body;
+      parent.Members.Add(newFunc);
+    }
+  }
+
+  internal override void PreResolve(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();
+
+    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      foreach (var decl in topLevelDecl.Members) {
+        if (ShouldGenerateWrapper(decl)) {
+          membersToWrap.Add((topLevelDecl, decl));
+        }
+      }
+    }
+
+    foreach (var (topLevelDecl, decl) in membersToWrap) {
+      AddWrapper(topLevelDecl, decl);
+    }
+  }
+
+  internal override void PostResolve(ModuleDefinition moduleDefinition) {
+    // TODO: replace calls as dictated by the policy currently enabled
+  }
+}

From e9f9f3993d237089dd099186b4a8930c86fe8b2f Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 15 Aug 2022 14:59:50 -0700
Subject: [PATCH 02/31] Start implementing redirection to wrappers

---
 Source/Dafny/AST/DafnyAst.cs             |  4 +-
 Source/Dafny/Resolver/ExpectContracts.cs | 97 +++++++++++++++++++-----
 2 files changed, 82 insertions(+), 19 deletions(-)

diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs
index 8efd6025275..670ea6a5d3a 100644
--- a/Source/Dafny/AST/DafnyAst.cs
+++ b/Source/Dafny/AST/DafnyAst.cs
@@ -10132,7 +10132,7 @@ public SeqDisplayExpr(IToken tok, List<Expression> elements)
 
   public class MemberSelectExpr : Expression {
     public readonly Expression Obj;
-    public readonly string MemberName;
+    public string MemberName;
     [FilledInDuringResolution] public MemberDecl Member;    // will be a Field or Function
     [FilledInDuringResolution] public Label /*?*/ AtLabel;  // non-null for a two-state selection
 
@@ -10493,7 +10493,7 @@ public ApplyExpr(IToken tok, Expression fn, List<Expression> args, IToken closeP
   }
 
   public class FunctionCallExpr : Expression {
-    public readonly string Name;
+    public string Name;
     public readonly Expression Receiver;
     public readonly IToken OpenParen;  // can be null if Args.Count == 0
     public readonly IToken CloseParen;
diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 5fafc45b30c..37ba5478020 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -9,6 +9,8 @@ namespace Microsoft.Dafny;
 
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
+  private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
+  private CallRedirector callRedirector;
 
   public ExpectContracts(ErrorReporter reporter) : base(reporter) {
   }
@@ -57,15 +59,18 @@ private bool ShouldGenerateWrapper(MemberDecl decl) {
   private void AddWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     var tok = decl.tok; // TODO: do better
 
+    var receiver = decl.IsStatic
+      ? (Expression)new StaticReceiverExpr(tok, parent, false)
+      : (Expression)new ThisExpr(parent);
+    var newName = decl.Name + "_checked";
+    MemberDecl newDecl = null;
+
     if (decl is Method origMethod) {
       var newMethod = cloner.CloneMethod(origMethod);
-      newMethod.Name = origMethod.Name + "_checked";
+      newMethod.Name = newName;
 
       var args = newMethod.Ins.Select(Expression.CreateIdentExpr).ToList();
       var outs = newMethod.Outs.Select(Expression.CreateIdentExpr).ToList();
-      var receiver = origMethod.IsStatic
-        ? (Expression)new StaticReceiverExpr(tok, parent, false)
-        : (Expression)new ThisExpr(parent);
       var selector = new MemberSelectExpr(tok, receiver, origMethod.Name) {
         Member = origMethod,
         TypeApplication_JustMember = new List<Type>(), // TODO: fill in properly
@@ -75,22 +80,14 @@ private void AddWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
 
       var body = MakeContractCheckingBody(origMethod.Req, origMethod.Ens, callStmt);
       newMethod.Body = body;
-      parent.Members.Add(newMethod);
+      newDecl = newMethod;
     } else if (decl is Function origFunc) {
       var newFunc = cloner.CloneFunction(origFunc);
-      newFunc.Name = origFunc.Name + "_checked";
+      newFunc.Name = newName;
 
       var args = origFunc.Formals.Select(Expression.CreateIdentExpr).ToList();
-      var callExpr = new FunctionCallExpr(tok, origFunc.Name, new ThisExpr(tok), tok, tok, args);
+      var callExpr = new FunctionCallExpr(tok, origFunc.Name, receiver, tok, tok, args);
       newFunc.Body = callExpr;
-      var receiver = origFunc.IsStatic ?
-        (Expression)new StaticReceiverExpr(tok, parent, false) :
-        (Expression)new ThisExpr(parent);
-      var selector = new MemberSelectExpr(tok, receiver, origFunc.Name) {
-        Member = origFunc,
-        TypeApplication_JustMember = new List<Type>(), // TODO: fill in properly
-        TypeApplication_AtEnclosingClass = new List<Type>() // TODO: fill in properly
-      };
 
       var localName = origFunc.Result?.Name ?? "__result";
       var local = new LocalVariable(tok, tok, localName, origFunc.ResultType, false);
@@ -108,7 +105,12 @@ private void AddWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
       var body = MakeContractCheckingBody(origFunc.Req, origFunc.Ens, callStmt);
       body.AppendStmt(new ReturnStmt(tok, tok, new List<AssignmentRhs> { new ExprRhs(localExpr) }));
       newFunc.ByMethodBody = body;
-      parent.Members.Add(newFunc);
+      newDecl = newFunc;
+    }
+
+    if (newDecl is not null) {
+      parent.Members.Add(newDecl);
+      wrappedDeclarations.Add(decl, newDecl);
     }
   }
 
@@ -127,9 +129,70 @@ internal override void PreResolve(ModuleDefinition moduleDefinition) {
     foreach (var (topLevelDecl, decl) in membersToWrap) {
       AddWrapper(topLevelDecl, decl);
     }
+
+    callRedirector = new CallRedirector(wrappedDeclarations);
+  }
+
+  class CallRedirector : TopDownVisitor<MemberDecl> {
+    private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations;
+
+    public CallRedirector(Dictionary<MemberDecl, MemberDecl> wrappedDeclarations) {
+      this.wrappedDeclarations = wrappedDeclarations;
+    }
+
+    private bool HasTestAttribute(MemberDecl decl) {
+      return Attributes.Contains(decl.Attributes, "test");
+    }
+
+    private bool HasExternAttribute(MemberDecl decl) {
+      return Attributes.Contains(decl.Attributes, "extern");
+    }
+
+    private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
+      // TODO: make this configurable
+      return (HasTestAttribute(caller) || HasExternAttribute(callee)) &&
+             wrappedDeclarations.ContainsKey(caller);
+    }
+
+    protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
+      if (expr is FunctionCallExpr fce) {
+        if (ShouldCallWrapper(decl, fce.Function)) {
+          var target = fce.Function;
+          var newTarget = wrappedDeclarations[target];
+          Console.WriteLine($"Call (expression) to {target.Name} redirecting to {newTarget.Name}");
+          // TODO: apparently the following isn't enough
+          fce.Function = (Function)newTarget;
+          fce.Name = newTarget.Name;
+        }
+      }
+
+      return true;
+    }
+
+    protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
+      if (stmt is CallStmt cs) {
+        if (ShouldCallWrapper(decl, cs.Method)) {
+          var target = cs.MethodSelect.Member;
+          var newTarget = wrappedDeclarations[target];
+          Console.WriteLine($"Call (statement) to {target.Name} redirecting to {newTarget.Name}");
+          // TODO: apparently the following isn't enough
+          cs.MethodSelect.Member = newTarget;
+          cs.MethodSelect.MemberName = newTarget.Name;
+        }
+      }
+
+      return true;
+    }
   }
 
   internal override void PostResolve(ModuleDefinition moduleDefinition) {
-    // TODO: replace calls as dictated by the policy currently enabled
+    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      foreach (var decl in topLevelDecl.Members) {
+        if (decl is ICallable callable) {
+          Console.WriteLine($"Visiting {decl.Name}");
+          callRedirector.Visit(callable, decl);
+        }
+      }
+    }
   }
 }

From 86b5e0a62841fe79411e0c7869c362fe51afa20a Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 22 Aug 2022 14:00:40 -0700
Subject: [PATCH 03/31] Various cleanups

---
 Source/Dafny/Resolver/ExpectContracts.cs | 53 +++++++++++++++---------
 1 file changed, 33 insertions(+), 20 deletions(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 37ba5478020..be8a3afd6be 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -5,15 +5,14 @@
 using Microsoft.Boogie;
 using Microsoft.CodeAnalysis.CSharp.Syntax;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
   private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
   private CallRedirector callRedirector;
 
-  public ExpectContracts(ErrorReporter reporter) : base(reporter) {
-  }
+  public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
 
   /// <summary>
   /// Create an expect statement that checks the given contract clause
@@ -40,7 +39,8 @@ private static Statement CreateContractExpectStatement(AttributedExpression expr
   /// <param name="ensures">The list of ensures clause expressions.</param>
   /// <param name="callStmt">The call statement to include.</param>
   /// <returns>The newly-created block statement.</returns>
-  private static BlockStmt MakeContractCheckingBody(List<AttributedExpression> requires, List<AttributedExpression> ensures, Statement callStmt) {
+  private static BlockStmt MakeContractCheckingBody(List<AttributedExpression> requires,
+    List<AttributedExpression> ensures, Statement callStmt) {
     var expectRequiresStmts = requires.Select(req =>
       CreateContractExpectStatement(req, "requires"));
     var expectEnsuresStmts = ensures.Select(ens =>
@@ -56,7 +56,7 @@ private bool ShouldGenerateWrapper(MemberDecl decl) {
     return !decl.IsGhost && decl is not Constructor;
   }
 
-  private void AddWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
+  private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     var tok = decl.tok; // TODO: do better
 
     var receiver = decl.IsStatic
@@ -109,25 +109,36 @@ private void AddWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     }
 
     if (newDecl is not null) {
-      parent.Members.Add(newDecl);
       wrappedDeclarations.Add(decl, newDecl);
     }
   }
 
-  internal override void PreResolve(ModuleDefinition moduleDefinition) {
+  internal override void PreResolve(Program program) {
+
     // Keep a list of members to wrap so that we don't modify the collection we're iterating over.
     List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new();
 
-    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-      foreach (var decl in topLevelDecl.Members) {
-        if (ShouldGenerateWrapper(decl)) {
-          membersToWrap.Add((topLevelDecl, decl));
+    // Find module members to wrap
+    foreach (var moduleDefinition in program.RawModules()) {
+      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(topLevelDecl, decl);
+    }
+
+    // Add the generated wrappers to the module
     foreach (var (topLevelDecl, decl) in membersToWrap) {
-      AddWrapper(topLevelDecl, decl);
+      if (wrappedDeclarations.ContainsKey(decl)) {
+        topLevelDecl.Members.Add(wrappedDeclarations[decl]);
+      }
     }
 
     callRedirector = new CallRedirector(wrappedDeclarations);
@@ -141,11 +152,11 @@ public CallRedirector(Dictionary<MemberDecl, MemberDecl> wrappedDeclarations) {
     }
 
     private bool HasTestAttribute(MemberDecl decl) {
-      return Attributes.Contains(decl.Attributes, "test");
+      return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "test");
     }
 
     private bool HasExternAttribute(MemberDecl decl) {
-      return Attributes.Contains(decl.Attributes, "extern");
+      return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "extern");
     }
 
     private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
@@ -185,12 +196,14 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
     }
   }
 
-  internal override void PostResolve(ModuleDefinition moduleDefinition) {
-    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-      foreach (var decl in topLevelDecl.Members) {
-        if (decl is ICallable callable) {
-          Console.WriteLine($"Visiting {decl.Name}");
-          callRedirector.Visit(callable, decl);
+  internal override void PostResolve(Program program) {
+    foreach (var moduleDefinition in program.Modules()) {
+      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+        foreach (var decl in topLevelDecl.Members) {
+          if (decl is ICallable callable) {
+            Console.WriteLine($"Visiting {decl.Name}");
+            callRedirector.Visit(callable, decl);
+          }
         }
       }
     }

From 5036db9ff78cf787f313d91411dd4db41b837213 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 22 Aug 2022 15:50:30 -0700
Subject: [PATCH 04/31] More cleanup

* Generate fewer resolved AST nodes before resolution happens
* Don't run the redirection code while it's not working
---
 Source/Dafny/Resolver/ExpectContracts.cs | 33 +++++++++++++++---------
 1 file changed, 21 insertions(+), 12 deletions(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index be8a3afd6be..23c5849f2cb 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -50,6 +50,12 @@ private static BlockStmt MakeContractCheckingBody(List<AttributedExpression> req
     return new BlockStmt(callStmt.Tok, callStmt.EndTok, bodyStatements.ToList());
   }
 
+  private static Expression MakeApplySuffix(IToken tok, string name, List<Expression> args) {
+    var nameExpr = new NameSegment(tok, name, null);
+    var argBindings = args.ConvertAll(arg => new ActualBinding(null, arg));
+    return new ApplySuffix(tok, null, nameExpr, argBindings, tok);
+  }
+
   private bool ShouldGenerateWrapper(MemberDecl decl) {
     // TODO: make this more discriminating
     // TODO: could work for ghost statements eventually
@@ -59,9 +65,6 @@ private bool ShouldGenerateWrapper(MemberDecl decl) {
   private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     var tok = decl.tok; // TODO: do better
 
-    var receiver = decl.IsStatic
-      ? (Expression)new StaticReceiverExpr(tok, parent, false)
-      : (Expression)new ThisExpr(parent);
     var newName = decl.Name + "_checked";
     MemberDecl newDecl = null;
 
@@ -71,12 +74,9 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
 
       var args = newMethod.Ins.Select(Expression.CreateIdentExpr).ToList();
       var outs = newMethod.Outs.Select(Expression.CreateIdentExpr).ToList();
-      var selector = new MemberSelectExpr(tok, receiver, origMethod.Name) {
-        Member = origMethod,
-        TypeApplication_JustMember = new List<Type>(), // TODO: fill in properly
-        TypeApplication_AtEnclosingClass = new List<Type>() // TODO: fill in properly
-      };
-      var callStmt = new CallStmt(tok, tok, outs, selector, args);
+      var applyExpr = MakeApplySuffix(tok, origMethod.Name, args);
+      var applyRhs = new ExprRhs(applyExpr);
+      var callStmt = new UpdateStmt(tok, tok, outs, new List<AssignmentRhs>() { applyRhs });
 
       var body = MakeContractCheckingBody(origMethod.Req, origMethod.Ens, callStmt);
       newMethod.Body = body;
@@ -86,7 +86,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
       newFunc.Name = newName;
 
       var args = origFunc.Formals.Select(Expression.CreateIdentExpr).ToList();
-      var callExpr = new FunctionCallExpr(tok, origFunc.Name, receiver, tok, tok, args);
+      var callExpr = MakeApplySuffix(tok, origFunc.Name, args);
       newFunc.Body = callExpr;
 
       var localName = origFunc.Result?.Name ?? "__result";
@@ -100,10 +100,13 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
 
       var callStmt = origFunc.Result?.Name is null
         ? (Statement)new VarDeclStmt(tok, tok, locs, new UpdateStmt(tok, tok, lhss, rhss))
-        : (Statement)new AssignStmt(tok, tok, localExpr, callRhs);
+        : (Statement)new UpdateStmt(tok, tok, lhss, rhss);
 
       var body = MakeContractCheckingBody(origFunc.Req, origFunc.Ens, callStmt);
-      body.AppendStmt(new ReturnStmt(tok, tok, new List<AssignmentRhs> { new ExprRhs(localExpr) }));
+
+      if (origFunc.Result?.Name is null) {
+        body.AppendStmt(new ReturnStmt(tok, tok, new List<AssignmentRhs> { new ExprRhs(localExpr) }));
+      }
       newFunc.ByMethodBody = body;
       newDecl = newFunc;
     }
@@ -166,6 +169,7 @@ private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
     }
 
     protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
+      /*
       if (expr is FunctionCallExpr fce) {
         if (ShouldCallWrapper(decl, fce.Function)) {
           var target = fce.Function;
@@ -176,11 +180,13 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
           fce.Name = newTarget.Name;
         }
       }
+      */
 
       return true;
     }
 
     protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
+      /*
       if (stmt is CallStmt cs) {
         if (ShouldCallWrapper(decl, cs.Method)) {
           var target = cs.MethodSelect.Member;
@@ -191,12 +197,14 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
           cs.MethodSelect.MemberName = newTarget.Name;
         }
       }
+      */
 
       return true;
     }
   }
 
   internal override void PostResolve(Program program) {
+    /*
     foreach (var moduleDefinition in program.Modules()) {
       foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
         foreach (var decl in topLevelDecl.Members) {
@@ -207,5 +215,6 @@ internal override void PostResolve(Program program) {
         }
       }
     }
+    */
   }
 }

From 5e6d886cf530837e1941969cf823e2428e3dad5e Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 22 Aug 2022 16:19:23 -0700
Subject: [PATCH 05/31] Further redirection progress

Still doesn't work, though
---
 Source/Dafny/Resolver/ExpectContracts.cs | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 23c5849f2cb..89ca8abb7e0 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -165,11 +165,11 @@ private bool HasExternAttribute(MemberDecl decl) {
     private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
       // TODO: make this configurable
       return (HasTestAttribute(caller) || HasExternAttribute(callee)) &&
-             wrappedDeclarations.ContainsKey(caller);
+             wrappedDeclarations.ContainsKey(callee) &&
+             !wrappedDeclarations.ContainsValue(caller);
     }
 
     protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
-      /*
       if (expr is FunctionCallExpr fce) {
         if (ShouldCallWrapper(decl, fce.Function)) {
           var target = fce.Function;
@@ -178,15 +178,16 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
           // TODO: apparently the following isn't enough
           fce.Function = (Function)newTarget;
           fce.Name = newTarget.Name;
+          var resolved = (FunctionCallExpr)fce.Resolved;
+          resolved.Function = (Function)newTarget;
+          resolved.Name = newTarget.Name;
         }
       }
-      */
 
       return true;
     }
 
     protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
-      /*
       if (stmt is CallStmt cs) {
         if (ShouldCallWrapper(decl, cs.Method)) {
           var target = cs.MethodSelect.Member;
@@ -195,16 +196,17 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
           // TODO: apparently the following isn't enough
           cs.MethodSelect.Member = newTarget;
           cs.MethodSelect.MemberName = newTarget.Name;
+          var resolved = (MemberSelectExpr)cs.MethodSelect;
+          resolved.Member = newTarget;
+          resolved.MemberName = newTarget.Name;
         }
       }
-      */
 
       return true;
     }
   }
 
   internal override void PostResolve(Program program) {
-    /*
     foreach (var moduleDefinition in program.Modules()) {
       foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
         foreach (var decl in topLevelDecl.Members) {
@@ -215,6 +217,5 @@ internal override void PostResolve(Program program) {
         }
       }
     }
-    */
   }
 }

From 2c0df470e707a7a019f0da6c06ed7a705e44a621 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 25 Aug 2022 14:36:36 -0700
Subject: [PATCH 06/31] Tiny tweak

---
 Source/Dafny/Resolver/ExpectContracts.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 89ca8abb7e0..f430e58654f 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -196,7 +196,7 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
           // TODO: apparently the following isn't enough
           cs.MethodSelect.Member = newTarget;
           cs.MethodSelect.MemberName = newTarget.Name;
-          var resolved = (MemberSelectExpr)cs.MethodSelect;
+          var resolved = (MemberSelectExpr)cs.MethodSelect.Resolved;
           resolved.Member = newTarget;
           resolved.MemberName = newTarget.Name;
         }

From e151a6b371fed83fa42d7b23f3e6f9339e2313dd Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 26 Aug 2022 16:42:40 -0700
Subject: [PATCH 07/31] Functional but messy call redirection

---
 Source/Dafny/Resolver.cs                 |  5 ++
 Source/Dafny/Resolver/ExpectContracts.cs | 64 ++++++++++++++----------
 Source/Dafny/Rewriter.cs                 | 26 +++++++---
 3 files changed, 61 insertions(+), 34 deletions(-)

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 168e6298a14..33da1633b4c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -547,6 +547,11 @@ public void ResolveProgram(Program prog) {
             // Now we're ready to resolve the cloned module definition, using the compile signature
 
             ResolveModuleDefinition(nw, compileSig);
+
+            foreach (var rewriter in rewriters) {
+              rewriter.PostCompileCloneAndResolve(nw);
+            }
+
             prog.CompileModules.Add(nw);
             useCompileSignatures = false; // reset the flag
             Type.EnableScopes();
diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index f430e58654f..a9c24017459 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -9,7 +9,7 @@ namespace Microsoft.Dafny;
 
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
-  private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
+  private readonly Dictionary<string, (MemberDecl, MemberDecl)> wrappedDeclarations = new();
   private CallRedirector callRedirector;
 
   public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
@@ -112,7 +112,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     }
 
     if (newDecl is not null) {
-      wrappedDeclarations.Add(decl, newDecl);
+      wrappedDeclarations.Add(decl.Name, (decl, newDecl));
     }
   }
 
@@ -139,8 +139,8 @@ internal override void PreResolve(Program program) {
 
     // Add the generated wrappers to the module
     foreach (var (topLevelDecl, decl) in membersToWrap) {
-      if (wrappedDeclarations.ContainsKey(decl)) {
-        topLevelDecl.Members.Add(wrappedDeclarations[decl]);
+      if (wrappedDeclarations.ContainsKey(decl.Name)) {
+        topLevelDecl.Members.Add(wrappedDeclarations[decl.Name].Item2);
       }
     }
 
@@ -148,9 +148,9 @@ internal override void PreResolve(Program program) {
   }
 
   class CallRedirector : TopDownVisitor<MemberDecl> {
-    private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations;
+    private readonly Dictionary<string, (MemberDecl, MemberDecl)> wrappedDeclarations;
 
-    public CallRedirector(Dictionary<MemberDecl, MemberDecl> wrappedDeclarations) {
+    public CallRedirector(Dictionary<string, (MemberDecl, MemberDecl)> wrappedDeclarations) {
       this.wrappedDeclarations = wrappedDeclarations;
     }
 
@@ -162,20 +162,26 @@ private bool HasExternAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "extern");
     }
 
-    private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
+    private bool ShouldCallWrapper(MemberDecl caller, string calleeName) {
+      if (!wrappedDeclarations.ContainsKey(calleeName)) {
+        return false;
+      }
+
+      var callee = wrappedDeclarations[calleeName].Item2;
       // TODO: make this configurable
       return (HasTestAttribute(caller) || HasExternAttribute(callee)) &&
-             wrappedDeclarations.ContainsKey(callee) &&
-             !wrappedDeclarations.ContainsValue(caller);
+             // TODO: check this in a better way
+             !caller.Name.EndsWith("_checked");
     }
 
     protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
+      // TODO: this pulls targets from the original module. Fix that.
       if (expr is FunctionCallExpr fce) {
-        if (ShouldCallWrapper(decl, fce.Function)) {
-          var target = fce.Function;
-          var newTarget = wrappedDeclarations[target];
-          Console.WriteLine($"Call (expression) to {target.Name} redirecting to {newTarget.Name}");
-          // TODO: apparently the following isn't enough
+        Console.WriteLine($"Function call to {fce.Function.Name}");
+        if (ShouldCallWrapper(decl, fce.Function.Name)) {
+          var targetName = fce.Function.Name;
+          var newTarget = wrappedDeclarations[targetName].Item2;
+          Console.WriteLine($"Call (expression) to {targetName} redirecting to {newTarget.Name}");
           fce.Function = (Function)newTarget;
           fce.Name = newTarget.Name;
           var resolved = (FunctionCallExpr)fce.Resolved;
@@ -188,12 +194,13 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
     }
 
     protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
+      // TODO: this pulls targets from the original module. Fix that.
       if (stmt is CallStmt cs) {
-        if (ShouldCallWrapper(decl, cs.Method)) {
-          var target = cs.MethodSelect.Member;
-          var newTarget = wrappedDeclarations[target];
-          Console.WriteLine($"Call (statement) to {target.Name} redirecting to {newTarget.Name}");
-          // TODO: apparently the following isn't enough
+        Console.WriteLine($"Method call to {cs.Method.Name}");
+        if (ShouldCallWrapper(decl, cs.Method.Name)) {
+          var targetName = cs.Method.Name;
+          var newTarget = wrappedDeclarations[targetName].Item2;
+          Console.WriteLine($"Call (statement) to {targetName} redirecting to {newTarget.Name}");
           cs.MethodSelect.Member = newTarget;
           cs.MethodSelect.MemberName = newTarget.Name;
           var resolved = (MemberSelectExpr)cs.MethodSelect.Resolved;
@@ -206,14 +213,17 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
     }
   }
 
-  internal override void PostResolve(Program program) {
-    foreach (var moduleDefinition in program.Modules()) {
-      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-        foreach (var decl in topLevelDecl.Members) {
-          if (decl is ICallable callable) {
-            Console.WriteLine($"Visiting {decl.Name}");
-            callRedirector.Visit(callable, decl);
-          }
+  internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinition) {
+    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      // TODO: keep track of names
+      foreach (var decl in topLevelDecl.Members) { }
+    }
+
+    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      foreach (var decl in topLevelDecl.Members) {
+        if (decl is ICallable callable) {
+          Console.WriteLine($"Visiting {decl.Name}");
+          callRedirector.Visit(callable, decl);
         }
       }
     }
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index ec8cefff370..06ebb240eef 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -39,7 +39,7 @@ internal IRewriter(ErrorReporter reporter) {
     }
 
     /// <summary>
-    /// Phase 1/7
+    /// Phase 1/8
     /// Override this method to obtain the initial program after parsing and built-in pre-resolvers.
     /// You can then report errors using reporter.Error (see above)
     /// </summary>
@@ -49,7 +49,7 @@ internal virtual void PreResolve(Program program) {
     }
 
     /// <summary>
-    /// Phase 2/7
+    /// Phase 2/8
     /// Override this method to obtain a module definition after parsing and built-in pre-resolvers.
     /// You can then report errors using reporter.Error(MessageSource.Resolver, token, "message") (see above)
     /// This is a good place to perform AST rewritings, if necessary
@@ -60,7 +60,7 @@ internal virtual void PreResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 3/7
+    /// Phase 3/8
     /// Override this method to obtain a module definition after bare resolution, if no error were thrown.
     /// You can then report errors using reporter.Error (see above)
     /// We heavily discourage AST rewriting after this stage, as automatic type checking will not take place anymore.
@@ -71,7 +71,7 @@ internal virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition)
     }
 
     /// <summary>
-    /// Phase 4/7
+    /// Phase 4/8
     /// Override this method to obtain the module definition after resolution and
     /// SCC/Cyclicity/Recursivity analysis.
     /// You can then report errors using reporter.Error (see above)
@@ -83,7 +83,7 @@ internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 5/7
+    /// Phase 5/8
     /// Override this method to obtain the module definition after the phase decreasesResolve
     /// You can then report errors using reporter.Error (see above)
     /// </summary>
@@ -94,7 +94,7 @@ internal virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 6/7
+    /// Phase 6/8
     /// Override this method to obtain a module definition after the entire resolution pipeline
     /// You can then report errors using reporter.Error (see above)
     /// </summary>
@@ -105,7 +105,7 @@ internal virtual void PostResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 7/7
+    /// Phase 7/8
     /// Override this method to obtain the final program after the entire resolution pipeline
     /// after the individual PostResolve on every module
     /// You can then report errors using reporter.Error (see above)
@@ -114,6 +114,18 @@ internal virtual void PostResolve(ModuleDefinition moduleDefinition) {
     internal virtual void PostResolve(Program program) {
       Contract.Requires(program != null);
     }
+
+    /// <summary>
+    /// Phase 8/8
+    /// Override this method to obtain a module definition after the entire resolution pipeline
+    /// has finished and the module has been cloned and resolved prior to compilation.
+    /// You can then report errors using reporter.Error (see above)
+    /// </summary>
+    /// <param name="moduleDefinition">A module definition after it
+    /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed</param>
+    internal virtual void PostCompileCloneAndResolve(ModuleDefinition moduleDefinition) {
+      Contract.Requires(moduleDefinition != null);
+    }
   }
 
   public class AutoGeneratedToken : TokenWrapper {

From c10d268ea11bf64d23fc0ef50df88a8110d22075 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 1 Sep 2022 16:48:34 -0700
Subject: [PATCH 08/31] Clean up wrapper call redirection

---
 Source/Dafny/Resolver/ExpectContracts.cs | 87 +++++++++++++-----------
 1 file changed, 48 insertions(+), 39 deletions(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index a9c24017459..8897ca87b33 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Data;
 using System.Linq;
+using System.Runtime.CompilerServices;
 using Microsoft.Boogie;
 using Microsoft.CodeAnalysis.CSharp.Syntax;
 
@@ -9,8 +10,8 @@ namespace Microsoft.Dafny;
 
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
-  private readonly Dictionary<string, (MemberDecl, MemberDecl)> wrappedDeclarations = new();
-  private CallRedirector callRedirector;
+  private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
+  private CallRedirector callRedirector = new();
 
   public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
 
@@ -57,11 +58,17 @@ private static Expression MakeApplySuffix(IToken tok, string name, List<Expressi
   }
 
   private bool ShouldGenerateWrapper(MemberDecl decl) {
-    // TODO: make this more discriminating
-    // TODO: could work for ghost statements eventually
     return !decl.IsGhost && decl is not Constructor;
   }
 
+  /// <summary>
+  /// Create a wrapper for the given function or method declaration that
+  /// dynamically checks all of its preconditions, calls it, and checks
+  /// all of its postconditions before returning. The new wrapper will
+  /// later be added as a sibling of the original declaration.
+  /// </summary>
+  /// <param name="parent">The declaration containing the on to be wrapped.</param>
+  /// <param name="decl">The declaration to be wrapped.</param>
   private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     var tok = decl.tok; // TODO: do better
 
@@ -112,7 +119,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     }
 
     if (newDecl is not null) {
-      wrappedDeclarations.Add(decl.Name, (decl, newDecl));
+      wrappedDeclarations.Add(decl, newDecl);
     }
   }
 
@@ -121,7 +128,7 @@ internal override void PreResolve(Program program) {
     // Keep a list of members to wrap so that we don't modify the collection we're iterating over.
     List<(TopLevelDeclWithMembers, MemberDecl)> membersToWrap = new();
 
-    // Find module members to wrap
+    // Find module members to wrap.
     foreach (var moduleDefinition in program.RawModules()) {
       foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
         foreach (var decl in topLevelDecl.Members) {
@@ -132,27 +139,21 @@ internal override void PreResolve(Program program) {
       }
     }
 
-    // Generate a wrapper for each of the members identified above
+    // Generate a wrapper for each of the members identified above.
     foreach (var (topLevelDecl, decl) in membersToWrap) {
       GenerateWrapper(topLevelDecl, decl);
     }
 
-    // Add the generated wrappers to the module
+    // Add the generated wrappers to the module.
     foreach (var (topLevelDecl, decl) in membersToWrap) {
-      if (wrappedDeclarations.ContainsKey(decl.Name)) {
-        topLevelDecl.Members.Add(wrappedDeclarations[decl.Name].Item2);
+      if (wrappedDeclarations.ContainsKey(decl)) {
+        topLevelDecl.Members.Add(wrappedDeclarations[decl]);
       }
     }
-
-    callRedirector = new CallRedirector(wrappedDeclarations);
   }
 
   class CallRedirector : TopDownVisitor<MemberDecl> {
-    private readonly Dictionary<string, (MemberDecl, MemberDecl)> wrappedDeclarations;
-
-    public CallRedirector(Dictionary<string, (MemberDecl, MemberDecl)> wrappedDeclarations) {
-      this.wrappedDeclarations = wrappedDeclarations;
-    }
+    internal readonly Dictionary<MemberDecl, MemberDecl> newRedirections = new();
 
     private bool HasTestAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "test");
@@ -162,12 +163,12 @@ private bool HasExternAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "extern");
     }
 
-    private bool ShouldCallWrapper(MemberDecl caller, string calleeName) {
-      if (!wrappedDeclarations.ContainsKey(calleeName)) {
+    private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
+      // If there's no wrapper for the callee, don't try to call it.
+      if (!newRedirections.ContainsKey(callee)) {
         return false;
       }
 
-      var callee = wrappedDeclarations[calleeName].Item2;
       // TODO: make this configurable
       return (HasTestAttribute(caller) || HasExternAttribute(callee)) &&
              // TODO: check this in a better way
@@ -175,15 +176,13 @@ private bool ShouldCallWrapper(MemberDecl caller, string calleeName) {
     }
 
     protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
-      // TODO: this pulls targets from the original module. Fix that.
       if (expr is FunctionCallExpr fce) {
-        Console.WriteLine($"Function call to {fce.Function.Name}");
-        if (ShouldCallWrapper(decl, fce.Function.Name)) {
-          var targetName = fce.Function.Name;
-          var newTarget = wrappedDeclarations[targetName].Item2;
-          Console.WriteLine($"Call (expression) to {targetName} redirecting to {newTarget.Name}");
-          fce.Function = (Function)newTarget;
-          fce.Name = newTarget.Name;
+        var f = fce.Function;
+        var targetName = f.Name;
+        //Console.WriteLine($"Function call to {targetName}");
+        if (ShouldCallWrapper(decl, f)) {
+          var newTarget = newRedirections[f];
+          Console.WriteLine($"Call (expression) to {f.FullName} redirecting to {newTarget.FullName}");
           var resolved = (FunctionCallExpr)fce.Resolved;
           resolved.Function = (Function)newTarget;
           resolved.Name = newTarget.Name;
@@ -194,15 +193,13 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
     }
 
     protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
-      // TODO: this pulls targets from the original module. Fix that.
       if (stmt is CallStmt cs) {
-        Console.WriteLine($"Method call to {cs.Method.Name}");
-        if (ShouldCallWrapper(decl, cs.Method.Name)) {
-          var targetName = cs.Method.Name;
-          var newTarget = wrappedDeclarations[targetName].Item2;
-          Console.WriteLine($"Call (statement) to {targetName} redirecting to {newTarget.Name}");
-          cs.MethodSelect.Member = newTarget;
-          cs.MethodSelect.MemberName = newTarget.Name;
+        var m = cs.Method;
+        var targetName = m.Name;
+        //Console.WriteLine($"Method call to {m.FullName}");
+        if (ShouldCallWrapper(decl, m)) {
+          var newTarget = newRedirections[m];
+          Console.WriteLine($"Call (statement) to {m.FullName} redirecting to {newTarget.FullName}");
           var resolved = (MemberSelectExpr)cs.MethodSelect.Resolved;
           resolved.Member = newTarget;
           resolved.MemberName = newTarget.Name;
@@ -214,15 +211,27 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
   }
 
   internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinition) {
+    Dictionary<string, MemberDecl> newDeclarationsByName = new();
     foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-      // TODO: keep track of names
-      foreach (var decl in topLevelDecl.Members) { }
+      // Keep track of current declarations by name to avoid redirecting
+      // calls to functions or methods from obsolete modules (those that
+      // existed prior to processing by CompilationCloner).
+      foreach (var decl in topLevelDecl.Members) {
+        //Console.WriteLine(($"Adding {decl.FullName}"));
+        newDeclarationsByName.Add(decl.FullName, decl);
+      }
+    }
+
+    foreach (var (caller, callee) in wrappedDeclarations) {
+      callRedirector.newRedirections.Add(
+        newDeclarationsByName[caller.FullName],
+        newDeclarationsByName[callee.FullName]);
     }
 
     foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
       foreach (var decl in topLevelDecl.Members) {
         if (decl is ICallable callable) {
-          Console.WriteLine($"Visiting {decl.Name}");
+          //Console.WriteLine($"Visiting {decl.FullName}");
           callRedirector.Visit(callable, decl);
         }
       }

From 7ce51973131bf80d5a430e11b9fabfdbdef3e6f6 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 1 Sep 2022 16:49:02 -0700
Subject: [PATCH 09/31] Add /testContracts command-line option

---
 Source/Dafny/DafnyOptions.cs             | 30 ++++++++++++++++++++++++
 Source/Dafny/Resolver.cs                 |  5 ++--
 Source/Dafny/Resolver/ExpectContracts.cs |  9 +++----
 3 files changed, 38 insertions(+), 6 deletions(-)

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 508ef65c831..6855191e569 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -81,6 +81,12 @@ public enum PrintModes {
       NoGhost
     }
 
+    public enum ContractTestingMode {
+      None,
+      TestAttribute,
+      ExternAttribute
+    }
+
     public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
     public bool DafnyVerify = true;
     public string DafnyPrintResolvedFile = null;
@@ -117,6 +123,7 @@ public enum PrintModes {
     public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version3;
     public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version3;
     public HashSet<string> LibraryFiles { get; } = new();
+    public ContractTestingMode TestContracts = ContractTestingMode.None;
 
     public enum FunctionSyntaxOptions {
       Version3,
@@ -636,6 +643,19 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) {
           }
           return true;
 
+        case "testContracts":
+          // TODO: support more than one argument
+          if (ps.ConfirmArgumentCount(1)) {
+            if (args[ps.i].Equals("Tests")) {
+              TestContracts = ContractTestingMode.TestAttribute;
+            } else if (args[ps.i].Equals("Externs")) {
+              TestContracts = ContractTestingMode.ExternAttribute;
+            } else {
+              InvalidArgumentError(name, ps);
+            }
+          }
+          return true;
+
       }
 
       // Unless this is an option for test generation, defer to superclass
@@ -1320,6 +1340,16 @@ than including DafnyRuntime.cs verbatim.
     This option is useful in a diamond dependency situation, 
     to prevent code from the bottom dependency from being generated more than once.
 
+/testContracts:<Tests|Externs>
+    Enable run-time testing of compiled function or method contracts in
+    certain situations.
+
+    Tests - Check contracts on functions and methods when calling them
+        directly from methods marked with the :test attribute.
+    Externs - Check contracts when calling functions or methods marked
+        with the :extern attribute.
+
+
 ----------------------------------------------------------------------------
 
 Dafny generally accepts Boogie options and passes these on to Boogie. However,
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 33da1633b4c..5ac31ac4b47 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -430,8 +430,9 @@ public void ResolveProgram(Program prog) {
         rewriters.Add(new TriggerGeneratingRewriter(reporter));
       }
 
-      // TODO: check option
-      rewriters.Add(new ExpectContracts(reporter));
+      if (DafnyOptions.O.TestContracts != DafnyOptions.ContractTestingMode.None) {
+        rewriters.Add(new ExpectContracts(reporter));
+      }
 
       if (DafnyOptions.O.RunAllTests) {
         rewriters.Add(new RunAllTestsMainMethod(reporter));
diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 8897ca87b33..8b9ff7b3319 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -169,10 +169,11 @@ private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
         return false;
       }
 
-      // TODO: make this configurable
-      return (HasTestAttribute(caller) || HasExternAttribute(callee)) &&
-             // TODO: check this in a better way
-             !caller.Name.EndsWith("_checked");
+      var opts = DafnyOptions.O.TestContracts;
+      return ((HasTestAttribute(caller) && opts == DafnyOptions.ContractTestingMode.TestAttribute) ||
+              (HasExternAttribute(callee) && opts == DafnyOptions.ContractTestingMode.ExternAttribute)) &&
+             // Skip if the caller is a wrapper, otherwise it'd just call itself recursively.
+             !newRedirections.ContainsValue(caller);
     }
 
     protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {

From 1dbf4e98f4041cdf9cd68c22e956a4ad54651aaa Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 8 Sep 2022 15:49:41 -0700
Subject: [PATCH 10/31] Move wrapper generation to a later phase

Now it runs during `PostResolveIntermediate` so that it has easier
access to attributes.
---
 Source/Dafny/Resolver/ExpectContracts.cs | 42 ++++++++++++++++--------
 1 file changed, 29 insertions(+), 13 deletions(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 8b9ff7b3319..948478791be 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -11,6 +11,7 @@ namespace Microsoft.Dafny;
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
   private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
+  private readonly Dictionary<MemberDecl, string> fullNames = new();
   private CallRedirector callRedirector = new();
 
   public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
@@ -58,7 +59,10 @@ private static Expression MakeApplySuffix(IToken tok, string name, List<Expressi
   }
 
   private bool ShouldGenerateWrapper(MemberDecl decl) {
-    return !decl.IsGhost && decl is not Constructor;
+    return !decl.IsGhost &&
+           decl is not Constructor &&
+           (callRedirector.HasExternAttribute(decl) /*||
+            CalledFromTestMethod(decl)*/);
   }
 
   /// <summary>
@@ -120,21 +124,27 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
 
     if (newDecl is not null) {
       wrappedDeclarations.Add(decl, newDecl);
+      callRedirector.AddFullName(newDecl, decl.FullName + "_checked");
     }
   }
 
-  internal override void PreResolve(Program program) {
+  /// <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
+  /// attributes and call targets, but it generates pre-resolution syntax.
+  /// This is okay because the program gets resolved again during compilation.
+  /// </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();
 
     // Find module members to wrap.
-    foreach (var moduleDefinition in program.RawModules()) {
-      foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
-        foreach (var decl in topLevelDecl.Members) {
-          if (ShouldGenerateWrapper(decl)) {
-            membersToWrap.Add((topLevelDecl, decl));
-          }
+    foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+      foreach (var decl in topLevelDecl.Members) {
+        if (ShouldGenerateWrapper(decl)) {
+          membersToWrap.Add((topLevelDecl, decl));
         }
       }
     }
@@ -154,12 +164,17 @@ internal override void PreResolve(Program program) {
 
   class CallRedirector : TopDownVisitor<MemberDecl> {
     internal readonly Dictionary<MemberDecl, MemberDecl> newRedirections = new();
+    internal readonly Dictionary<MemberDecl, string> newFullNames = new();
+
+    internal void AddFullName(MemberDecl decl, string fullName) {
+      newFullNames.Add(decl, fullName);
+    }
 
-    private bool HasTestAttribute(MemberDecl decl) {
+    internal bool HasTestAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "test");
     }
 
-    private bool HasExternAttribute(MemberDecl decl) {
+    internal bool HasExternAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "extern");
     }
 
@@ -183,7 +198,7 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
         //Console.WriteLine($"Function call to {targetName}");
         if (ShouldCallWrapper(decl, f)) {
           var newTarget = newRedirections[f];
-          Console.WriteLine($"Call (expression) to {f.FullName} redirecting to {newTarget.FullName}");
+          //Console.WriteLine($"Call (expression) to {f.FullName} redirecting to {newTarget.FullName}");
           var resolved = (FunctionCallExpr)fce.Resolved;
           resolved.Function = (Function)newTarget;
           resolved.Name = newTarget.Name;
@@ -200,7 +215,7 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
         //Console.WriteLine($"Method call to {m.FullName}");
         if (ShouldCallWrapper(decl, m)) {
           var newTarget = newRedirections[m];
-          Console.WriteLine($"Call (statement) to {m.FullName} redirecting to {newTarget.FullName}");
+          //Console.WriteLine($"Call (statement) to {m.FullName} redirecting to {newTarget.FullName}");
           var resolved = (MemberSelectExpr)cs.MethodSelect.Resolved;
           resolved.Member = newTarget;
           resolved.MemberName = newTarget.Name;
@@ -224,9 +239,10 @@ internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinit
     }
 
     foreach (var (caller, callee) in wrappedDeclarations) {
+      var calleeFullName = callRedirector.newFullNames[callee];
       callRedirector.newRedirections.Add(
         newDeclarationsByName[caller.FullName],
-        newDeclarationsByName[callee.FullName]);
+        newDeclarationsByName[calleeFullName]);
     }
 
     foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {

From dc8169287acef1a83c20c6e7da377d8fdbdf426a Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 8 Sep 2022 15:50:37 -0700
Subject: [PATCH 11/31] Update Options.txt

---
 docs/DafnyRef/Options.txt | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index 90b20e90e01..04cdcb85ee3 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -479,6 +479,16 @@ Usage: Dafny [ option ... ] [ filename ... ]
       option is useful in a diamond dependency situation, to prevent code
       from the bottom dependency from being generated more than once.
   
+  /testContracts:<Tests|Externs>
+      Enable run-time testing of compiled function or method contracts in
+      certain situations.
+  
+      Tests - Check contracts on functions and methods when calling them
+          directly from methods marked with the :test attribute.
+      Externs - Check contracts when calling functions or methods marked
+          with the :extern attribute.
+  
+  
   ----------------------------------------------------------------------------
   
   Dafny generally accepts Boogie options and passes these on to Boogie.

From 2c9a9a238819530cee89778428793e2cf86a6beb Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 8 Sep 2022 16:41:28 -0700
Subject: [PATCH 12/31] Test on real-world example

---
 Source/Dafny/Resolver/ExpectContracts.cs | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/Source/Dafny/Resolver/ExpectContracts.cs b/Source/Dafny/Resolver/ExpectContracts.cs
index 948478791be..f1f80e5df78 100644
--- a/Source/Dafny/Resolver/ExpectContracts.cs
+++ b/Source/Dafny/Resolver/ExpectContracts.cs
@@ -12,6 +12,7 @@ public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
   private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
   private readonly Dictionary<MemberDecl, string> fullNames = new();
+  private readonly Dictionary<string, MemberDecl> newDeclarationsByName = new();
   private CallRedirector callRedirector = new();
 
   public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
@@ -123,6 +124,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     }
 
     if (newDecl is not null) {
+      newDecl.Attributes = null;
       wrappedDeclarations.Add(decl, newDecl);
       callRedirector.AddFullName(newDecl, decl.FullName + "_checked");
     }
@@ -227,22 +229,29 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
   }
 
   internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinition) {
-    Dictionary<string, MemberDecl> newDeclarationsByName = new();
     foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
       // Keep track of current declarations by name to avoid redirecting
       // calls to functions or methods from obsolete modules (those that
       // existed prior to processing by CompilationCloner).
       foreach (var decl in topLevelDecl.Members) {
-        //Console.WriteLine(($"Adding {decl.FullName}"));
-        newDeclarationsByName.Add(decl.FullName, decl);
+        var noCompileName = decl.FullName.Replace("_Compile", "");
+        //Console.WriteLine(($"Adding {noCompileName}"));
+        newDeclarationsByName.Add(noCompileName, decl);
       }
     }
 
     foreach (var (caller, callee) in wrappedDeclarations) {
+      var callerFullName = caller.FullName;
       var calleeFullName = callRedirector.newFullNames[callee];
-      callRedirector.newRedirections.Add(
-        newDeclarationsByName[caller.FullName],
-        newDeclarationsByName[calleeFullName]);
+      //Console.WriteLine($"Looking up {caller.FullName} -> {calleeFullName}");
+      if (newDeclarationsByName.ContainsKey(callerFullName) &&
+          newDeclarationsByName.ContainsKey(calleeFullName)) {
+        var callerDecl = newDeclarationsByName[caller.FullName];
+        var calleeDecl = newDeclarationsByName[calleeFullName];
+        if (!callRedirector.newRedirections.ContainsKey(callerDecl)) {
+          callRedirector.newRedirections.Add(callerDecl, calleeDecl);
+        }
+      }
     }
 
     foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {

From 759c745ba59657d3d913eeddef43c80d49a628ae Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Fri, 16 Sep 2022 16:08:14 -0700
Subject: [PATCH 13/31] Improve warnings about testing ghost expressions

---
 Source/DafnyCore/Resolver/ExpectContracts.cs | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index f1f80e5df78..80078c1bd91 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -21,16 +21,26 @@ public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
   /// Create an expect statement that checks the given contract clause
   /// expression and fails with a message that points to the original
   /// location of the contract clause if it is not true at runtime.
+  ///
+  /// If the given clause is not compilable, emit a warning and construct
+  /// an `expect true` statement with a message explaining the situation.
   /// </summary>
   /// <param name="expr">The contract clause expression to evaluate.</param>
   /// <param name="exprType">Either "requires" or "ensures", to use in the
   /// failure message.</param>
   /// <returns>The newly-created expect statement.</returns>
-  private static Statement CreateContractExpectStatement(AttributedExpression expr, string exprType) {
+  private Statement CreateContractExpectStatement(AttributedExpression expr, string exprType) {
     var tok = expr.E.tok;
     var msg = $"Runtime failure of {exprType} clause from {tok.filename}:{tok.line}:{tok.col}";
+    var exprToCheck = expr.E;
+    if (ExpressionTester.UsesSpecFeatures(exprToCheck)) {
+      Reporter.Warning(MessageSource.Rewriter, tok,
+        $"The {exprType} clause at this location cannot be compiled to be tested at runtime, because it references ghost state.");
+      exprToCheck = new LiteralExpr(tok, true);
+      msg += " (not checked because it references ghost state)";
+    }
     var msgExpr = Expression.CreateStringLiteral(tok, msg);
-    return new ExpectStmt(tok, expr.E.EndToken, expr.E, msgExpr, null);
+    return new ExpectStmt(tok, expr.E.EndToken, exprToCheck, msgExpr, null);
   }
 
   /// <summary>
@@ -42,7 +52,7 @@ private static Statement CreateContractExpectStatement(AttributedExpression expr
   /// <param name="ensures">The list of ensures clause expressions.</param>
   /// <param name="callStmt">The call statement to include.</param>
   /// <returns>The newly-created block statement.</returns>
-  private static BlockStmt MakeContractCheckingBody(List<AttributedExpression> requires,
+  private BlockStmt MakeContractCheckingBody(List<AttributedExpression> requires,
     List<AttributedExpression> ensures, Statement callStmt) {
     var expectRequiresStmts = requires.Select(req =>
       CreateContractExpectStatement(req, "requires"));

From aa0d31a945bfeb1f0a2dc04953a2714d9957f3bb Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 09:55:04 -0700
Subject: [PATCH 14/31] Update options and logic for which calls to wrap

---
 Source/DafnyCore/DafnyOptions.cs             | 26 +++++++++-----------
 Source/DafnyCore/Resolver/ExpectContracts.cs | 26 ++++++++++++++------
 2 files changed, 30 insertions(+), 22 deletions(-)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 81a4f013fd6..b2cfe4f8dd0 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -98,8 +98,8 @@ public enum PrintModes {
 
     public enum ContractTestingMode {
       None,
-      TestAttribute,
-      ExternAttribute
+      AllExterns,
+      ExternsInTests,
     }
 
     public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
@@ -658,12 +658,11 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) {
           return true;
 
         case "testContracts":
-          // TODO: support more than one argument
           if (ps.ConfirmArgumentCount(1)) {
-            if (args[ps.i].Equals("Tests")) {
-              TestContracts = ContractTestingMode.TestAttribute;
-            } else if (args[ps.i].Equals("Externs")) {
-              TestContracts = ContractTestingMode.ExternAttribute;
+            if (args[ps.i].Equals("AllExterns")) {
+              TestContracts = ContractTestingMode.AllExterns;
+            } else if (args[ps.i].Equals("ExternsInTests")) {
+              TestContracts = ContractTestingMode.ExternsInTests;
             } else {
               InvalidArgumentError(name, ps);
             }
@@ -1445,15 +1444,14 @@ contents are skipped during code generation and verification. This
     option is useful in a diamond dependency situation, to prevent code
     from the bottom dependency from being generated more than once.
 
-/testContracts:<Tests|Externs>
+/testContracts:<AllExterns|ExternsInTests>
     Enable run-time testing of compiled function or method contracts in
-    certain situations.
-
-    Tests - Check contracts on functions and methods when calling them
-        directly from methods marked with the :test attribute.
-    Externs - Check contracts when calling functions or methods marked
-        with the :extern attribute.
+    certain situations, currently focused on :extern code.
 
+    AllExterns - Check contracts on every call to a function or
+        method marked :extern, regardless of where it occurs.
+    Externs - Check contracts on every call to a function or method
+        marked :extern when it occurs in one marked :test.
 
 ----------------------------------------------------------------------------
 
diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index 80078c1bd91..86f009d4928 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -13,9 +13,11 @@ public class ExpectContracts : IRewriter {
   private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
   private readonly Dictionary<MemberDecl, string> fullNames = new();
   private readonly Dictionary<string, MemberDecl> newDeclarationsByName = new();
-  private CallRedirector callRedirector = new();
+  private CallRedirector callRedirector;
 
-  public ExpectContracts(ErrorReporter reporter) : base(reporter) { }
+  public ExpectContracts(ErrorReporter reporter) : base(reporter) {
+    callRedirector = new(reporter);
+  }
 
   /// <summary>
   /// Create an expect statement that checks the given contract clause
@@ -72,8 +74,7 @@ private static Expression MakeApplySuffix(IToken tok, string name, List<Expressi
   private bool ShouldGenerateWrapper(MemberDecl decl) {
     return !decl.IsGhost &&
            decl is not Constructor &&
-           (callRedirector.HasExternAttribute(decl) /*||
-            CalledFromTestMethod(decl)*/);
+           callRedirector.HasExternAttribute(decl);
   }
 
   /// <summary>
@@ -177,6 +178,11 @@ internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition
   class CallRedirector : TopDownVisitor<MemberDecl> {
     internal readonly Dictionary<MemberDecl, MemberDecl> newRedirections = new();
     internal readonly Dictionary<MemberDecl, string> newFullNames = new();
+    private readonly ErrorReporter reporter;
+
+    public CallRedirector(ErrorReporter reporter) {
+      this.reporter = reporter;
+    }
 
     internal void AddFullName(MemberDecl decl, string fullName) {
       newFullNames.Add(decl, fullName);
@@ -191,14 +197,18 @@ internal bool HasExternAttribute(MemberDecl decl) {
     }
 
     private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
-      // If there's no wrapper for the callee, don't try to call it.
+      if (!HasExternAttribute(callee)) {
+        return false;
+      }
+      // If there's no wrapper for the callee, don't try to call it, but warn.
       if (!newRedirections.ContainsKey(callee)) {
+        reporter.Warning(MessageSource.Rewriter, caller.tok, $"Internal: no wrapper for {callee.FullDafnyName}");
         return false;
       }
 
-      var opts = DafnyOptions.O.TestContracts;
-      return ((HasTestAttribute(caller) && opts == DafnyOptions.ContractTestingMode.TestAttribute) ||
-              (HasExternAttribute(callee) && opts == DafnyOptions.ContractTestingMode.ExternAttribute)) &&
+      var opt = DafnyOptions.O.TestContracts;
+      return ((HasTestAttribute(caller) && opt == DafnyOptions.ContractTestingMode.ExternsInTests) ||
+              (opt == DafnyOptions.ContractTestingMode.AllExterns)) &&
              // Skip if the caller is a wrapper, otherwise it'd just call itself recursively.
              !newRedirections.ContainsValue(caller);
     }

From a478eceae296ab14c5a7704a8ecb4e9d15035d81 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 10:24:40 -0700
Subject: [PATCH 15/31] Minor code cleanups

---
 Source/DafnyCore/Resolver/ExpectContracts.cs | 33 +++++++++-----------
 1 file changed, 14 insertions(+), 19 deletions(-)

diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index 86f009d4928..b2cb92175c0 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -37,9 +37,9 @@ private Statement CreateContractExpectStatement(AttributedExpression expr, strin
     var exprToCheck = expr.E;
     if (ExpressionTester.UsesSpecFeatures(exprToCheck)) {
       Reporter.Warning(MessageSource.Rewriter, tok,
-        $"The {exprType} clause at this location cannot be compiled to be tested at runtime, because it references ghost state.");
+        $"The {exprType} clause at this location cannot be compiled to be tested at runtime because it references ghost state.");
       exprToCheck = new LiteralExpr(tok, true);
-      msg += " (not checked because it references ghost state)";
+      msg += " (not compiled because it references ghost state)";
     }
     var msgExpr = Expression.CreateStringLiteral(tok, msg);
     return new ExpectStmt(tok, expr.E.EndToken, exprToCheck, msgExpr, null);
@@ -54,8 +54,8 @@ private Statement CreateContractExpectStatement(AttributedExpression expr, strin
   /// <param name="ensures">The list of ensures clause expressions.</param>
   /// <param name="callStmt">The call statement to include.</param>
   /// <returns>The newly-created block statement.</returns>
-  private BlockStmt MakeContractCheckingBody(List<AttributedExpression> requires,
-    List<AttributedExpression> ensures, Statement callStmt) {
+  private BlockStmt MakeContractCheckingBody(IEnumerable<AttributedExpression> requires,
+    IEnumerable<AttributedExpression> ensures, Statement callStmt) {
     var expectRequiresStmts = requires.Select(req =>
       CreateContractExpectStatement(req, "requires"));
     var expectEnsuresStmts = ensures.Select(ens =>
@@ -74,19 +74,19 @@ private static Expression MakeApplySuffix(IToken tok, string name, List<Expressi
   private bool ShouldGenerateWrapper(MemberDecl decl) {
     return !decl.IsGhost &&
            decl is not Constructor &&
-           callRedirector.HasExternAttribute(decl);
+           CallRedirector.HasExternAttribute(decl);
   }
 
   /// <summary>
   /// Create a wrapper for the given function or method declaration that
   /// dynamically checks all of its preconditions, calls it, and checks
-  /// all of its postconditions before returning. The new wrapper will
-  /// later be added as a sibling of the original declaration.
+  /// all of its postconditions before returning. Then add the new wrapper
+  /// as a sibling of the original declaration.
   /// </summary>
   /// <param name="parent">The declaration containing the on to be wrapped.</param>
   /// <param name="decl">The declaration to be wrapped.</param>
   private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
-    var tok = decl.tok; // TODO: do better
+    var tok = decl.tok; // TODO: would this be less confusing as an internal token?
 
     var newName = decl.Name + "_checked";
     MemberDecl newDecl = null;
@@ -135,8 +135,11 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
     }
 
     if (newDecl is not null) {
+      // We especially want to remove {:extern} from the wrapper, but also any other attributes.
       newDecl.Attributes = null;
+
       wrappedDeclarations.Add(decl, newDecl);
+      parent.Members.Add(newDecl);
       callRedirector.AddFullName(newDecl, decl.FullName + "_checked");
     }
   }
@@ -149,7 +152,6 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
   /// </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();
 
@@ -166,16 +168,9 @@ internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition
     foreach (var (topLevelDecl, decl) in membersToWrap) {
       GenerateWrapper(topLevelDecl, decl);
     }
-
-    // Add the generated wrappers to the module.
-    foreach (var (topLevelDecl, decl) in membersToWrap) {
-      if (wrappedDeclarations.ContainsKey(decl)) {
-        topLevelDecl.Members.Add(wrappedDeclarations[decl]);
-      }
-    }
   }
 
-  class CallRedirector : TopDownVisitor<MemberDecl> {
+  private class CallRedirector : TopDownVisitor<MemberDecl> {
     internal readonly Dictionary<MemberDecl, MemberDecl> newRedirections = new();
     internal readonly Dictionary<MemberDecl, string> newFullNames = new();
     private readonly ErrorReporter reporter;
@@ -188,11 +183,11 @@ internal void AddFullName(MemberDecl decl, string fullName) {
       newFullNames.Add(decl, fullName);
     }
 
-    internal bool HasTestAttribute(MemberDecl decl) {
+    internal static bool HasTestAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "test");
     }
 
-    internal bool HasExternAttribute(MemberDecl decl) {
+    internal static bool HasExternAttribute(MemberDecl decl) {
       return decl.Attributes is not null && Attributes.Contains(decl.Attributes, "extern");
     }
 

From 90660fcd582e82457accbafd882aa26cf2ccdb97 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 10:45:12 -0700
Subject: [PATCH 16/31] Update Options.txt

---
 docs/DafnyRef/Options.txt | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index 04cdcb85ee3..3452d5a291b 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -479,15 +479,14 @@ Usage: Dafny [ option ... ] [ filename ... ]
       option is useful in a diamond dependency situation, to prevent code
       from the bottom dependency from being generated more than once.
   
-  /testContracts:<Tests|Externs>
+  /testContracts:<AllExterns|ExternsInTests>
       Enable run-time testing of compiled function or method contracts in
-      certain situations.
-  
-      Tests - Check contracts on functions and methods when calling them
-          directly from methods marked with the :test attribute.
-      Externs - Check contracts when calling functions or methods marked
-          with the :extern attribute.
+      certain situations, currently focused on :extern code.
   
+      AllExterns - Check contracts on every call to a function or
+          method marked :extern, regardless of where it occurs.
+      Externs - Check contracts on every call to a function or method
+          marked :extern when it occurs in one marked :test.
   
   ----------------------------------------------------------------------------
   

From e141a1209e44d34c949a6797d357ca2943e25e78 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 13:36:24 -0700
Subject: [PATCH 17/31] Add tests for contract-checking wrappers

---
 Test/contract-wrappers/AllExterns.dfy         |  8 +++++
 Test/contract-wrappers/AllExterns.dfy.expect  |  9 +++++
 Test/contract-wrappers/CheckExtern.dfy        | 35 +++++++++++++++++++
 Test/contract-wrappers/ExternsInTests.dfy     |  8 +++++
 .../ExternsInTests.dfy.expect                 |  9 +++++
 5 files changed, 69 insertions(+)
 create mode 100644 Test/contract-wrappers/AllExterns.dfy
 create mode 100644 Test/contract-wrappers/AllExterns.dfy.expect
 create mode 100644 Test/contract-wrappers/CheckExtern.dfy
 create mode 100644 Test/contract-wrappers/ExternsInTests.dfy
 create mode 100644 Test/contract-wrappers/ExternsInTests.dfy.expect

diff --git a/Test/contract-wrappers/AllExterns.dfy b/Test/contract-wrappers/AllExterns.dfy
new file mode 100644
index 00000000000..3043a3838f6
--- /dev/null
+++ b/Test/contract-wrappers/AllExterns.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:AllExterns %s %s.externs.cs > %t
+// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s"
+// CHECK: .*Foo__checked\(x\).*
+// CHECK: .*Foo__checked\(new BigInteger\(3\)\).*
+// CHECK: .*Bar__checked\(x\).*
+// CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
+include "CheckExtern.dfy"
diff --git a/Test/contract-wrappers/AllExterns.dfy.expect b/Test/contract-wrappers/AllExterns.dfy.expect
new file mode 100644
index 00000000000..5235e29fa4c
--- /dev/null
+++ b/Test/contract-wrappers/AllExterns.dfy.expect
@@ -0,0 +1,9 @@
+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:13
+BarTest: FAILED
+	CheckExtern.dfy(21,12): Runtime failure of ensures clause from CheckExtern.dfy:21:13
+Test failures occurred: see above.
diff --git a/Test/contract-wrappers/CheckExtern.dfy b/Test/contract-wrappers/CheckExtern.dfy
new file mode 100644
index 00000000000..9009e58eb53
--- /dev/null
+++ b/Test/contract-wrappers/CheckExtern.dfy
@@ -0,0 +1,35 @@
+method {:extern} Foo(x: int) returns (y: int)
+  requires 1 < x < 10
+  ensures y >= 10
+
+method FooCaller(x: int) returns (y: int)
+  requires 1 < x < 10
+  ensures y >= 10
+{
+  y := Foo(x);
+}
+
+method {:test} FooTest()
+{
+  var y := Foo(3);
+  expect y == 30;
+}
+
+function method {:extern} Bar(x: int, ghost z: int): (y: int)
+  requires 1 < x < 10
+  requires z > x
+  ensures y >= 10
+  ensures y > z
+
+function method BarCaller(x: int): (y: int)
+  requires 1 < x < 10;
+  ensures y >= 10;
+{
+  Bar(x, 20)
+}
+
+method {:test} BarTest()
+{
+  var y := Bar(3, 20);
+  expect y == 30;
+}
diff --git a/Test/contract-wrappers/ExternsInTests.dfy b/Test/contract-wrappers/ExternsInTests.dfy
new file mode 100644
index 00000000000..633a9d38f95
--- /dev/null
+++ b/Test/contract-wrappers/ExternsInTests.dfy
@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:ExternsInTests %s %s.externs.cs > %t
+// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "%S/ExternsInTests.cs" "%s"
+// CHECK-NOT: .*Foo__checked\(x\).*
+// CHECK: .*Foo__checked\(new BigInteger\(3\)\).*
+// CHECK-NOT: .*Bar__checked\(x\).*
+// CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
+include "CheckExtern.dfy"
diff --git a/Test/contract-wrappers/ExternsInTests.dfy.expect b/Test/contract-wrappers/ExternsInTests.dfy.expect
new file mode 100644
index 00000000000..5235e29fa4c
--- /dev/null
+++ b/Test/contract-wrappers/ExternsInTests.dfy.expect
@@ -0,0 +1,9 @@
+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:13
+BarTest: FAILED
+	CheckExtern.dfy(21,12): Runtime failure of ensures clause from CheckExtern.dfy:21:13
+Test failures occurred: see above.

From 4e2e6bd75897668b08acb915765a4d54c5117d68 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 14:43:03 -0700
Subject: [PATCH 18/31] Add previously-omitted C# files for contract-wrappers
 tests

---
 Test/contract-wrappers/AllExterns.dfy.externs.cs    |  1 +
 Test/contract-wrappers/CheckExtern.dfy.externs.cs   | 13 +++++++++++++
 .../contract-wrappers/ExternsInTests.dfy.externs.cs |  1 +
 3 files changed, 15 insertions(+)
 create mode 120000 Test/contract-wrappers/AllExterns.dfy.externs.cs
 create mode 100644 Test/contract-wrappers/CheckExtern.dfy.externs.cs
 create mode 120000 Test/contract-wrappers/ExternsInTests.dfy.externs.cs

diff --git a/Test/contract-wrappers/AllExterns.dfy.externs.cs b/Test/contract-wrappers/AllExterns.dfy.externs.cs
new file mode 120000
index 00000000000..e107dafc664
--- /dev/null
+++ b/Test/contract-wrappers/AllExterns.dfy.externs.cs
@@ -0,0 +1 @@
+CheckExtern.dfy.externs.cs
\ No newline at end of file
diff --git a/Test/contract-wrappers/CheckExtern.dfy.externs.cs b/Test/contract-wrappers/CheckExtern.dfy.externs.cs
new file mode 100644
index 00000000000..03eba8578b6
--- /dev/null
+++ b/Test/contract-wrappers/CheckExtern.dfy.externs.cs
@@ -0,0 +1,13 @@
+using System.Numerics;
+
+namespace _module {
+
+  public partial class __default {
+    public static BigInteger Foo(BigInteger x) {
+      return BigInteger.Zero;
+    }
+    public static BigInteger Bar(BigInteger x) {
+      return BigInteger.Zero;
+    }
+  }
+}
diff --git a/Test/contract-wrappers/ExternsInTests.dfy.externs.cs b/Test/contract-wrappers/ExternsInTests.dfy.externs.cs
new file mode 120000
index 00000000000..e107dafc664
--- /dev/null
+++ b/Test/contract-wrappers/ExternsInTests.dfy.externs.cs
@@ -0,0 +1 @@
+CheckExtern.dfy.externs.cs
\ No newline at end of file

From 10f227482743183fb984d7ea48bc7ee79f536e9f Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 15:12:32 -0700
Subject: [PATCH 19/31] Add successful runtime contract checking test

---
 Test/contract-wrappers/AllExterns.dfy.expect      |  1 +
 Test/contract-wrappers/CheckExtern.dfy            | 11 +++++++++++
 Test/contract-wrappers/CheckExtern.dfy.externs.cs |  3 +++
 Test/contract-wrappers/ExternsInTests.dfy.expect  |  1 +
 4 files changed, 16 insertions(+)

diff --git a/Test/contract-wrappers/AllExterns.dfy.expect b/Test/contract-wrappers/AllExterns.dfy.expect
index 5235e29fa4c..ed50f210a44 100644
--- a/Test/contract-wrappers/AllExterns.dfy.expect
+++ b/Test/contract-wrappers/AllExterns.dfy.expect
@@ -6,4 +6,5 @@ FooTest: FAILED
 	CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy:3:13
 BarTest: FAILED
 	CheckExtern.dfy(21,12): Runtime failure of ensures clause from CheckExtern.dfy:21:13
+BazTest: PASSED
 Test failures occurred: see above.
diff --git a/Test/contract-wrappers/CheckExtern.dfy b/Test/contract-wrappers/CheckExtern.dfy
index 9009e58eb53..2ed2bee4f55 100644
--- a/Test/contract-wrappers/CheckExtern.dfy
+++ b/Test/contract-wrappers/CheckExtern.dfy
@@ -33,3 +33,14 @@ method {:test} BarTest()
   var y := Bar(3, 20);
   expect y == 30;
 }
+
+function method {:extern} Baz(x: int): (y: int)
+  ensures y == x
+
+method {:test} BazTest()
+{
+  var y := Baz(3);
+  // An extra check just for fun. The auto-generated wrapper should
+  // already ensure that y == 3.
+  expect y != 7;
+}
diff --git a/Test/contract-wrappers/CheckExtern.dfy.externs.cs b/Test/contract-wrappers/CheckExtern.dfy.externs.cs
index 03eba8578b6..946f4bc3c39 100644
--- a/Test/contract-wrappers/CheckExtern.dfy.externs.cs
+++ b/Test/contract-wrappers/CheckExtern.dfy.externs.cs
@@ -9,5 +9,8 @@ public static BigInteger Foo(BigInteger x) {
     public static BigInteger Bar(BigInteger x) {
       return BigInteger.Zero;
     }
+    public static BigInteger Baz(BigInteger x) {
+      return x;
+    }
   }
 }
diff --git a/Test/contract-wrappers/ExternsInTests.dfy.expect b/Test/contract-wrappers/ExternsInTests.dfy.expect
index 5235e29fa4c..ed50f210a44 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy.expect
+++ b/Test/contract-wrappers/ExternsInTests.dfy.expect
@@ -6,4 +6,5 @@ FooTest: FAILED
 	CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy:3:13
 BarTest: FAILED
 	CheckExtern.dfy(21,12): Runtime failure of ensures clause from CheckExtern.dfy:21:13
+BazTest: PASSED
 Test failures occurred: see above.

From d58329bd4b050db89cb757d4a94b9131a39f52da Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 19 Sep 2022 15:19:59 -0700
Subject: [PATCH 20/31] Rearrange files to get tests to pass

---
 Test/contract-wrappers/AllExterns.dfy               | 2 +-
 Test/contract-wrappers/ExternsInTests.dfy           | 2 +-
 Test/contract-wrappers/{ => Inputs}/CheckExtern.dfy | 0
 3 files changed, 2 insertions(+), 2 deletions(-)
 rename Test/contract-wrappers/{ => Inputs}/CheckExtern.dfy (100%)

diff --git a/Test/contract-wrappers/AllExterns.dfy b/Test/contract-wrappers/AllExterns.dfy
index 3043a3838f6..174882a3744 100644
--- a/Test/contract-wrappers/AllExterns.dfy
+++ b/Test/contract-wrappers/AllExterns.dfy
@@ -5,4 +5,4 @@
 // CHECK: .*Foo__checked\(new BigInteger\(3\)\).*
 // CHECK: .*Bar__checked\(x\).*
 // CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
-include "CheckExtern.dfy"
+include "Inputs/CheckExtern.dfy"
diff --git a/Test/contract-wrappers/ExternsInTests.dfy b/Test/contract-wrappers/ExternsInTests.dfy
index 633a9d38f95..e7fef485214 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy
+++ b/Test/contract-wrappers/ExternsInTests.dfy
@@ -5,4 +5,4 @@
 // CHECK: .*Foo__checked\(new BigInteger\(3\)\).*
 // CHECK-NOT: .*Bar__checked\(x\).*
 // CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
-include "CheckExtern.dfy"
+include "Inputs/CheckExtern.dfy"
diff --git a/Test/contract-wrappers/CheckExtern.dfy b/Test/contract-wrappers/Inputs/CheckExtern.dfy
similarity index 100%
rename from Test/contract-wrappers/CheckExtern.dfy
rename to Test/contract-wrappers/Inputs/CheckExtern.dfy

From 853a77800b79b71dc2cba570a105bafcc4a147cb Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 21 Sep 2022 09:17:04 -0700
Subject: [PATCH 21/31] Warn if :extern not tested with ExternsInTests

---
 Source/DafnyCore/DafnyOptions.cs              |  5 ++--
 Source/DafnyCore/Resolver/ExpectContracts.cs  | 17 +++++++++++
 Source/DafnyCore/Rewriter.cs                  | 30 +++++++++----------
 .../CheckExtern.dfy.externs.cs                |  3 ++
 Test/contract-wrappers/ExternsInTests.dfy     |  3 ++
 .../ExternsInTests.dfy.expect                 |  1 +
 docs/DafnyRef/Options.txt                     |  5 ++--
 7 files changed, 45 insertions(+), 19 deletions(-)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index b2cfe4f8dd0..3cc679cf88d 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -1450,8 +1450,9 @@ Enable run-time testing of compiled function or method contracts in
 
     AllExterns - Check contracts on every call to a function or
         method marked :extern, regardless of where it occurs.
-    Externs - Check contracts on every call to a function or method
-        marked :extern when it occurs in one marked :test.
+    ExternsInTests - Check contracts on every call to a function or
+        method marked :extern when it occurs in one marked :test, and
+        warn if no corresponding :test exists for a given :extern.
 
 ----------------------------------------------------------------------------
 
diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index b2cb92175c0..fa3f1b5b31e 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -174,6 +174,7 @@ private class CallRedirector : TopDownVisitor<MemberDecl> {
     internal readonly Dictionary<MemberDecl, MemberDecl> newRedirections = new();
     internal readonly Dictionary<MemberDecl, string> newFullNames = new();
     private readonly ErrorReporter reporter;
+    internal readonly HashSet<MemberDecl> calledWrappers = new();
 
     public CallRedirector(ErrorReporter reporter) {
       this.reporter = reporter;
@@ -219,6 +220,7 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
           var resolved = (FunctionCallExpr)fce.Resolved;
           resolved.Function = (Function)newTarget;
           resolved.Name = newTarget.Name;
+          calledWrappers.Add(newTarget);
         }
       }
 
@@ -236,6 +238,7 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
           var resolved = (MemberSelectExpr)cs.MethodSelect.Resolved;
           resolved.Member = newTarget;
           resolved.MemberName = newTarget.Name;
+          calledWrappers.Add(newTarget);
         }
       }
 
@@ -278,4 +281,18 @@ internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinit
       }
     }
   }
+
+  internal override void PostResolve(Program program) {
+    if (DafnyOptions.O.TestContracts != DafnyOptions.ContractTestingMode.ExternsInTests) {
+      return;
+    }
+
+    // If running in ExternsInTests mode, warn if any :extern has no corresponding :test.
+    var uncalledRedirections =
+      callRedirector.newRedirections.ExceptBy(callRedirector.calledWrappers, x => x.Value);
+    foreach (var uncalledRedirection in uncalledRedirections) {
+      var uncalledOriginal = uncalledRedirection.Key;
+      Reporter.Warning(MessageSource.Rewriter, uncalledOriginal.tok, $"No :test code calls {uncalledOriginal.FullDafnyName}");
+    }
+  }
 }
diff --git a/Source/DafnyCore/Rewriter.cs b/Source/DafnyCore/Rewriter.cs
index 0aff8f4dedb..eb32f2f1fad 100644
--- a/Source/DafnyCore/Rewriter.cs
+++ b/Source/DafnyCore/Rewriter.cs
@@ -73,6 +73,18 @@ internal virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition)
 
     /// <summary>
     /// Phase 4/8
+    /// Override this method to obtain a module definition after the module
+    /// has been cloned and re-resolved prior to compilation.
+    /// You can then report errors using reporter.Error (see above)
+    /// </summary>
+    /// <param name="moduleDefinition">A module definition after it
+    /// is cloned and re-resolved for compilation.</param>
+    internal virtual void PostCompileCloneAndResolve(ModuleDefinition moduleDefinition) {
+      Contract.Requires(moduleDefinition != null);
+    }
+
+    /// <summary>
+    /// Phase 5/8
     /// Override this method to obtain the module definition after resolution and
     /// SCC/Cyclicity/Recursivity analysis.
     /// You can then report errors using reporter.Error (see above)
@@ -84,7 +96,7 @@ internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 5/8
+    /// Phase 6/8
     /// Override this method to obtain the module definition after the phase decreasesResolve
     /// You can then report errors using reporter.Error (see above)
     /// </summary>
@@ -95,7 +107,7 @@ internal virtual void PostDecreasesResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 6/8
+    /// Phase 7/8
     /// Override this method to obtain a module definition after the entire resolution pipeline
     /// You can then report errors using reporter.Error (see above)
     /// </summary>
@@ -106,7 +118,7 @@ internal virtual void PostResolve(ModuleDefinition moduleDefinition) {
     }
 
     /// <summary>
-    /// Phase 7/8
+    /// Phase 8/8
     /// Override this method to obtain the final program after the entire resolution pipeline
     /// after the individual PostResolve on every module
     /// You can then report errors using reporter.Error (see above)
@@ -115,18 +127,6 @@ internal virtual void PostResolve(ModuleDefinition moduleDefinition) {
     internal virtual void PostResolve(Program program) {
       Contract.Requires(program != null);
     }
-
-    /// <summary>
-    /// Phase 8/8
-    /// Override this method to obtain a module definition after the entire resolution pipeline
-    /// has finished and the module has been cloned and resolved prior to compilation.
-    /// You can then report errors using reporter.Error (see above)
-    /// </summary>
-    /// <param name="moduleDefinition">A module definition after it
-    /// is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed</param>
-    internal virtual void PostCompileCloneAndResolve(ModuleDefinition moduleDefinition) {
-      Contract.Requires(moduleDefinition != null);
-    }
   }
 
   public class AutoGeneratedToken : TokenWrapper {
diff --git a/Test/contract-wrappers/CheckExtern.dfy.externs.cs b/Test/contract-wrappers/CheckExtern.dfy.externs.cs
index 946f4bc3c39..7d6382d9794 100644
--- a/Test/contract-wrappers/CheckExtern.dfy.externs.cs
+++ b/Test/contract-wrappers/CheckExtern.dfy.externs.cs
@@ -12,5 +12,8 @@ public static BigInteger Bar(BigInteger x) {
     public static BigInteger Baz(BigInteger x) {
       return x;
     }
+    public static BigInteger NotCalled(BigInteger x) {
+      return BigInteger.One;
+    }
   }
 }
diff --git a/Test/contract-wrappers/ExternsInTests.dfy b/Test/contract-wrappers/ExternsInTests.dfy
index e7fef485214..bd3e1023aac 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy
+++ b/Test/contract-wrappers/ExternsInTests.dfy
@@ -6,3 +6,6 @@
 // CHECK-NOT: .*Bar__checked\(x\).*
 // CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
 include "Inputs/CheckExtern.dfy"
+
+method {:extern} NotCalled(x: int) returns (y: int)
+  ensures y != x
diff --git a/Test/contract-wrappers/ExternsInTests.dfy.expect b/Test/contract-wrappers/ExternsInTests.dfy.expect
index ed50f210a44..1716d8898cd 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy.expect
+++ b/Test/contract-wrappers/ExternsInTests.dfy.expect
@@ -1,5 +1,6 @@
 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.
+ExternsInTests.dfy(10,17): Warning: No :test code calls NotCalled
 
 Dafny program verifier did not attempt verification
 FooTest: FAILED
diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index 3452d5a291b..ac5e17a5274 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -485,8 +485,9 @@ Usage: Dafny [ option ... ] [ filename ... ]
   
       AllExterns - Check contracts on every call to a function or
           method marked :extern, regardless of where it occurs.
-      Externs - Check contracts on every call to a function or method
-          marked :extern when it occurs in one marked :test.
+      ExternsInTests - Check contracts on every call to a function or
+          method marked :extern when it occurs in one marked :test, and
+          warn if no corresponding :test exists for a given :extern.
   
   ----------------------------------------------------------------------------
   

From 18ff18868284b8128e66af88e6b4edf60cb8448f Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 22 Sep 2022 12:03:50 -0700
Subject: [PATCH 22/31] Small cleanups

---
 Source/DafnyCore/Resolver/ExpectContracts.cs | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index fa3f1b5b31e..f3a8ba20493 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -86,9 +86,9 @@ decl is not Constructor &&
   /// <param name="parent">The declaration containing the on to be wrapped.</param>
   /// <param name="decl">The declaration to be wrapped.</param>
   private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
-    var tok = decl.tok; // TODO: would this be less confusing as an internal token?
+    var tok = decl.tok;
 
-    var newName = decl.Name + "_checked";
+    var newName = decl.Name + "__dafny_checked";
     MemberDecl newDecl = null;
 
     if (decl is Method origMethod) {
@@ -140,7 +140,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
 
       wrappedDeclarations.Add(decl, newDecl);
       parent.Members.Add(newDecl);
-      callRedirector.AddFullName(newDecl, decl.FullName + "_checked");
+      callRedirector.AddFullName(newDecl, decl.FullName + "__dafny_checked");
     }
   }
 
@@ -213,10 +213,8 @@ protected override bool VisitOneExpr(Expression expr, ref MemberDecl decl) {
       if (expr is FunctionCallExpr fce) {
         var f = fce.Function;
         var targetName = f.Name;
-        //Console.WriteLine($"Function call to {targetName}");
         if (ShouldCallWrapper(decl, f)) {
           var newTarget = newRedirections[f];
-          //Console.WriteLine($"Call (expression) to {f.FullName} redirecting to {newTarget.FullName}");
           var resolved = (FunctionCallExpr)fce.Resolved;
           resolved.Function = (Function)newTarget;
           resolved.Name = newTarget.Name;
@@ -231,10 +229,8 @@ protected override bool VisitOneStmt(Statement stmt, ref MemberDecl decl) {
       if (stmt is CallStmt cs) {
         var m = cs.Method;
         var targetName = m.Name;
-        //Console.WriteLine($"Method call to {m.FullName}");
         if (ShouldCallWrapper(decl, m)) {
           var newTarget = newRedirections[m];
-          //Console.WriteLine($"Call (statement) to {m.FullName} redirecting to {newTarget.FullName}");
           var resolved = (MemberSelectExpr)cs.MethodSelect.Resolved;
           resolved.Member = newTarget;
           resolved.MemberName = newTarget.Name;
@@ -253,7 +249,6 @@ internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinit
       // existed prior to processing by CompilationCloner).
       foreach (var decl in topLevelDecl.Members) {
         var noCompileName = decl.FullName.Replace("_Compile", "");
-        //Console.WriteLine(($"Adding {noCompileName}"));
         newDeclarationsByName.Add(noCompileName, decl);
       }
     }
@@ -261,7 +256,6 @@ internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinit
     foreach (var (caller, callee) in wrappedDeclarations) {
       var callerFullName = caller.FullName;
       var calleeFullName = callRedirector.newFullNames[callee];
-      //Console.WriteLine($"Looking up {caller.FullName} -> {calleeFullName}");
       if (newDeclarationsByName.ContainsKey(callerFullName) &&
           newDeclarationsByName.ContainsKey(calleeFullName)) {
         var callerDecl = newDeclarationsByName[caller.FullName];
@@ -275,7 +269,6 @@ internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinit
     foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
       foreach (var decl in topLevelDecl.Members) {
         if (decl is ICallable callable) {
-          //Console.WriteLine($"Visiting {decl.FullName}");
           callRedirector.Visit(callable, decl);
         }
       }

From 3635bbc3402d12c1190ca55a65798f889959e3f7 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 22 Sep 2022 14:19:07 -0700
Subject: [PATCH 23/31] Update tests to match wrapper name change

---
 Test/contract-wrappers/AllExterns.dfy     | 8 ++++----
 Test/contract-wrappers/ExternsInTests.dfy | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Test/contract-wrappers/AllExterns.dfy b/Test/contract-wrappers/AllExterns.dfy
index 174882a3744..ff9862b82b0 100644
--- a/Test/contract-wrappers/AllExterns.dfy
+++ b/Test/contract-wrappers/AllExterns.dfy
@@ -1,8 +1,8 @@
 // RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:AllExterns %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/AllExterns.cs" "%s"
-// CHECK: .*Foo__checked\(x\).*
-// CHECK: .*Foo__checked\(new BigInteger\(3\)\).*
-// CHECK: .*Bar__checked\(x\).*
-// CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
+// CHECK: .*Foo____dafny__checked\(x\).*
+// CHECK: .*Foo____dafny__checked\(new BigInteger\(3\)\).*
+// CHECK: .*Bar____dafny__checked\(x\).*
+// CHECK: .*Bar____dafny__checked\(new BigInteger\(3\)\).*
 include "Inputs/CheckExtern.dfy"
diff --git a/Test/contract-wrappers/ExternsInTests.dfy b/Test/contract-wrappers/ExternsInTests.dfy
index bd3e1023aac..7999098e028 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy
+++ b/Test/contract-wrappers/ExternsInTests.dfy
@@ -1,10 +1,10 @@
 // RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:ExternsInTests %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
 // RUN: %OutputCheck --file-to-check "%S/ExternsInTests.cs" "%s"
-// CHECK-NOT: .*Foo__checked\(x\).*
-// CHECK: .*Foo__checked\(new BigInteger\(3\)\).*
-// CHECK-NOT: .*Bar__checked\(x\).*
-// CHECK: .*Bar__checked\(new BigInteger\(3\)\).*
+// CHECK-NOT: .*Foo____dafny__checked\(x\).*
+// CHECK: .*Foo____dafny__checked\(new BigInteger\(3\)\).*
+// CHECK-NOT: .*Bar____dafny__checked\(x\).*
+// CHECK: .*Bar____dafny__checked\(new BigInteger\(3\)\).*
 include "Inputs/CheckExtern.dfy"
 
 method {:extern} NotCalled(x: int) returns (y: int)

From 8247175599af4f3a566757ac120bd8282fcf58d4 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Thu, 22 Sep 2022 14:19:19 -0700
Subject: [PATCH 24/31] Add a release notes entry

---
 RELEASE_NOTES.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 38e7c6883dd..90daa4e3191 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -1,5 +1,6 @@
 # Upcoming
 
+- feat: Support for testing certain contracts at runtime with a new `/testContracts` flag (https://github.com/dafny-lang/dafny/pull/2712)
 - feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (https://github.com/dafny-lang/dafny/pull/2717)
 - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
 - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)

From f7d9a1dfff1638abb1fa85211e4eeaed83de83eb Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 09:06:42 -0700
Subject: [PATCH 25/31] Change `/testContracts` arguments, update docs

---
 Source/DafnyCore/DafnyOptions.cs              | 25 ++++++++++---------
 Source/DafnyCore/Resolver/ExpectContracts.cs  |  6 ++---
 Test/contract-wrappers/AllExterns.dfy         |  2 +-
 .../{ExternsInTests.dfy => TestedExterns.dfy} |  4 +--
 ...ts.dfy.expect => TestedExterns.dfy.expect} |  2 +-
 ...xterns.cs => TestedExterns.dfy.externs.cs} |  0
 docs/DafnyRef/Options.txt                     | 17 +++++++------
 7 files changed, 29 insertions(+), 27 deletions(-)
 rename Test/contract-wrappers/{ExternsInTests.dfy => TestedExterns.dfy} (79%)
 rename Test/contract-wrappers/{ExternsInTests.dfy.expect => TestedExterns.dfy.expect} (90%)
 rename Test/contract-wrappers/{ExternsInTests.dfy.externs.cs => TestedExterns.dfy.externs.cs} (100%)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 3cc679cf88d..3931a56cd83 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -99,7 +99,7 @@ public enum PrintModes {
     public enum ContractTestingMode {
       None,
       AllExterns,
-      ExternsInTests,
+      TestedExterns,
     }
 
     public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
@@ -659,10 +659,10 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) {
 
         case "testContracts":
           if (ps.ConfirmArgumentCount(1)) {
-            if (args[ps.i].Equals("AllExterns")) {
+            if (args[ps.i].Equals("Externs")) {
               TestContracts = ContractTestingMode.AllExterns;
-            } else if (args[ps.i].Equals("ExternsInTests")) {
-              TestContracts = ContractTestingMode.ExternsInTests;
+            } else if (args[ps.i].Equals("TestedExterns")) {
+              TestContracts = ContractTestingMode.TestedExterns;
             } else {
               InvalidArgumentError(name, ps);
             }
@@ -1444,15 +1444,16 @@ contents are skipped during code generation and verification. This
     option is useful in a diamond dependency situation, to prevent code
     from the bottom dependency from being generated more than once.
 
-/testContracts:<AllExterns|ExternsInTests>
+/testContracts:<Externs|TestedExterns>
     Enable run-time testing of compiled function or method contracts in
-    certain situations, currently focused on :extern code.
-
-    AllExterns - Check contracts on every call to a function or
-        method marked :extern, regardless of where it occurs.
-    ExternsInTests - Check contracts on every call to a function or
-        method marked :extern when it occurs in one marked :test, and
-        warn if no corresponding :test exists for a given :extern.
+    certain situations, currently focused on {{:extern}} code.
+
+    Externs - Check contracts on every call to a function or method marked
+        with the {{:extern}} attribute, regardless of where it occurs.
+    TestedExterns - Check contracts on every call to a function or method
+        marked with the {{:extern}} attribute when it occurs in a method
+        with the {{:test}} attribute, and warn if no corresponding test
+        exists for a given external declaration.
 
 ----------------------------------------------------------------------------
 
diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index f3a8ba20493..ff4a209ff65 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -203,7 +203,7 @@ private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
       }
 
       var opt = DafnyOptions.O.TestContracts;
-      return ((HasTestAttribute(caller) && opt == DafnyOptions.ContractTestingMode.ExternsInTests) ||
+      return ((HasTestAttribute(caller) && opt == DafnyOptions.ContractTestingMode.TestedExterns) ||
               (opt == DafnyOptions.ContractTestingMode.AllExterns)) &&
              // Skip if the caller is a wrapper, otherwise it'd just call itself recursively.
              !newRedirections.ContainsValue(caller);
@@ -276,11 +276,11 @@ internal override void PostCompileCloneAndResolve(ModuleDefinition moduleDefinit
   }
 
   internal override void PostResolve(Program program) {
-    if (DafnyOptions.O.TestContracts != DafnyOptions.ContractTestingMode.ExternsInTests) {
+    if (DafnyOptions.O.TestContracts != DafnyOptions.ContractTestingMode.TestedExterns) {
       return;
     }
 
-    // If running in ExternsInTests mode, warn if any :extern has no corresponding :test.
+    // If running in TestedExterns, warn if any extern has no corresponding test.
     var uncalledRedirections =
       callRedirector.newRedirections.ExceptBy(callRedirector.calledWrappers, x => x.Value);
     foreach (var uncalledRedirection in uncalledRedirections) {
diff --git a/Test/contract-wrappers/AllExterns.dfy b/Test/contract-wrappers/AllExterns.dfy
index ff9862b82b0..ce6ec2a62f4 100644
--- a/Test/contract-wrappers/AllExterns.dfy
+++ b/Test/contract-wrappers/AllExterns.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:AllExterns %s %s.externs.cs > %t
+// RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts: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\).*
diff --git a/Test/contract-wrappers/ExternsInTests.dfy b/Test/contract-wrappers/TestedExterns.dfy
similarity index 79%
rename from Test/contract-wrappers/ExternsInTests.dfy
rename to Test/contract-wrappers/TestedExterns.dfy
index 7999098e028..531cccc1297 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy
+++ b/Test/contract-wrappers/TestedExterns.dfy
@@ -1,6 +1,6 @@
-// RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:ExternsInTests %s %s.externs.cs > %t
+// RUN: %dafny /compile:4 /noVerify /runAllTests:1 /testContracts:TestedExterns %s %s.externs.cs > %t
 // RUN: %diff "%s.expect" "%t"
-// RUN: %OutputCheck --file-to-check "%S/ExternsInTests.cs" "%s"
+// RUN: %OutputCheck --file-to-check "%S/TestedExterns.cs" "%s"
 // CHECK-NOT: .*Foo____dafny__checked\(x\).*
 // CHECK: .*Foo____dafny__checked\(new BigInteger\(3\)\).*
 // CHECK-NOT: .*Bar____dafny__checked\(x\).*
diff --git a/Test/contract-wrappers/ExternsInTests.dfy.expect b/Test/contract-wrappers/TestedExterns.dfy.expect
similarity index 90%
rename from Test/contract-wrappers/ExternsInTests.dfy.expect
rename to Test/contract-wrappers/TestedExterns.dfy.expect
index 1716d8898cd..2548db5d01e 100644
--- a/Test/contract-wrappers/ExternsInTests.dfy.expect
+++ b/Test/contract-wrappers/TestedExterns.dfy.expect
@@ -1,6 +1,6 @@
 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.
-ExternsInTests.dfy(10,17): Warning: No :test code calls NotCalled
+TestedExterns.dfy(10,17): Warning: No :test code calls NotCalled
 
 Dafny program verifier did not attempt verification
 FooTest: FAILED
diff --git a/Test/contract-wrappers/ExternsInTests.dfy.externs.cs b/Test/contract-wrappers/TestedExterns.dfy.externs.cs
similarity index 100%
rename from Test/contract-wrappers/ExternsInTests.dfy.externs.cs
rename to Test/contract-wrappers/TestedExterns.dfy.externs.cs
diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index ac5e17a5274..aa124511e5f 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -479,15 +479,16 @@ Usage: Dafny [ option ... ] [ filename ... ]
       option is useful in a diamond dependency situation, to prevent code
       from the bottom dependency from being generated more than once.
   
-  /testContracts:<AllExterns|ExternsInTests>
+  /testContracts:<Externs|TestedExterns>
       Enable run-time testing of compiled function or method contracts in
-      certain situations, currently focused on :extern code.
-  
-      AllExterns - Check contracts on every call to a function or
-          method marked :extern, regardless of where it occurs.
-      ExternsInTests - Check contracts on every call to a function or
-          method marked :extern when it occurs in one marked :test, and
-          warn if no corresponding :test exists for a given :extern.
+      certain situations, currently focused on {:extern} code.
+  
+      Externs - Check contracts on every call to a function or method marked
+          with the {:extern} attribute, regardless of where it occurs.
+      TestedExterns - Check contracts on every call to a function or method
+          marked with the {:extern} attribute when it occurs in a method
+          with the {:test} attribute, and warn if no corresponding test
+          exists for a given external declaration.
   
   ----------------------------------------------------------------------------
   

From 84947a1f6370be9b84cbfe4b78f79cdf79475fb1 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 09:56:29 -0700
Subject: [PATCH 26/31] Add class-level documentation comments

---
 Source/DafnyCore/Resolver/ExpectContracts.cs | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index ff4a209ff65..f99e07e05b4 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -8,6 +8,16 @@
 
 namespace Microsoft.Dafny;
 
+/// <summary>
+/// This class implements a rewriter that will insert dynamic checks of
+/// the contracts on certain functions and methods. It proceeds by
+///
+/// 1. identifying each declaration that should have its contract checked,
+/// 2. creating a new wrapper definition that uses expect statements to
+///    check all contract clauses for that declarations, and
+/// 3. replacing calls to the original definition with calls to the new
+///    wrapper definition.
+/// </summary>
 public class ExpectContracts : IRewriter {
   private readonly ClonerButDropMethodBodies cloner = new();
   private readonly Dictionary<MemberDecl, MemberDecl> wrappedDeclarations = new();
@@ -170,6 +180,11 @@ internal override void PostResolveIntermediate(ModuleDefinition moduleDefinition
     }
   }
 
+  /// <summary>
+  /// This class implements a top-down AST traversal to replace certain
+  /// function and method calls with calls to wrappers that dynamically
+  /// check contracts using expect statements.
+  /// </summary>
   private class CallRedirector : TopDownVisitor<MemberDecl> {
     internal readonly Dictionary<MemberDecl, MemberDecl> newRedirections = new();
     internal readonly Dictionary<MemberDecl, string> newFullNames = new();

From 8f7496a4cc81d02e7bc14bace3bd54a37cf8e555 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 10:06:26 -0700
Subject: [PATCH 27/31] Add RM entry for `/testContracts`

---
 docs/DafnyRef/UserGuide.md | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index e0625ac048a..5916e2a7aee 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -1652,3 +1652,27 @@ periods.
   compiled assembly rather than including `DafnyRuntime.cs` in the build
   process.
 
+
+* `-testContracts:<mode>` - test certain function and method contracts
+  at runtime. This works by generating a wrapper for each function or
+  method to be tested that includes a sequence of `expect` statements
+  for each requires clause, a call to the original, and sequence of
+  `expect` statements for each `ensures` clause. This is particularly
+  useful for code marked with the `{:extern}` attribute and implemented
+  in the target language instead of Dafny. Having runtime checks of the
+  contracts on such code makes it possible to gather evidence that the
+  target-language code satisfies the assumptions made of it during Dafny
+  verification through mechanisms ranging from manual tests through
+  fuzzing to full verification. For the latter two use cases, having
+  checks for `requires` clauses can be helpful, even if the Dafny
+  calling code will never violate them.
+
+  The `<mode>` parameter can currently be one of the following.
+
+  * `Externs` - insert dynamic checks when calling any function or
+    method marked with the `{:extern}` attribute, wherever the call
+    occurs.
+
+  * `TestedExterns` - insert dynamic checks when calling any function or
+    method marked with the `{:extern}` attribute directly from a
+    function or method marked with the `{:test}` attribute.

From ca6eb3bc3f7fd0dab6053d92072218fcd19c097a Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 10:16:40 -0700
Subject: [PATCH 28/31] Move `MakeApplySuffix` to Expressions.cs

---
 Source/DafnyCore/AST/Expressions.cs          | 13 +++++++++++++
 Source/DafnyCore/Resolver/ExpectContracts.cs | 10 ++--------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/Source/DafnyCore/AST/Expressions.cs b/Source/DafnyCore/AST/Expressions.cs
index eacfbad8378..b13d07d1da6 100644
--- a/Source/DafnyCore/AST/Expressions.cs
+++ b/Source/DafnyCore/AST/Expressions.cs
@@ -4286,4 +4286,17 @@ public ApplySuffix(IToken tok, IToken/*?*/ atLabel, Expression lhs, List<ActualB
       FormatTokens = new[] { closeParen };
     }
   }
+
+  /// <summary>
+  /// Create an ApplySuffix expression using the most basic pieces: a target name and a list of expressions.
+  /// </summary>
+  /// <param name="tok">The location to associate with the new ApplySuffix expression.</param>
+  /// <param name="name">The name of the target function or method.</param>
+  /// <param name="args">The arguments to apply the function or method to.</param>
+  /// <returns></returns>
+  public static Expression MakeRawApplySuffix(IToken tok, string name, List<Expression> args) {
+    var nameExpr = new NameSegment(tok, name, null);
+    var argBindings = args.ConvertAll(arg => new ActualBinding(null, arg));
+    return new ApplySuffix(tok, null, nameExpr, argBindings, tok);
+  }
 }
diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index f99e07e05b4..2b9031abc26 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -75,12 +75,6 @@ private BlockStmt MakeContractCheckingBody(IEnumerable<AttributedExpression> req
     return new BlockStmt(callStmt.Tok, callStmt.EndTok, bodyStatements.ToList());
   }
 
-  private static Expression MakeApplySuffix(IToken tok, string name, List<Expression> args) {
-    var nameExpr = new NameSegment(tok, name, null);
-    var argBindings = args.ConvertAll(arg => new ActualBinding(null, arg));
-    return new ApplySuffix(tok, null, nameExpr, argBindings, tok);
-  }
-
   private bool ShouldGenerateWrapper(MemberDecl decl) {
     return !decl.IsGhost &&
            decl is not Constructor &&
@@ -107,7 +101,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
 
       var args = newMethod.Ins.Select(Expression.CreateIdentExpr).ToList();
       var outs = newMethod.Outs.Select(Expression.CreateIdentExpr).ToList();
-      var applyExpr = MakeApplySuffix(tok, origMethod.Name, args);
+      var applyExpr = ApplySuffix.MakeRawApplySuffix(tok, origMethod.Name, args);
       var applyRhs = new ExprRhs(applyExpr);
       var callStmt = new UpdateStmt(tok, tok, outs, new List<AssignmentRhs>() { applyRhs });
 
@@ -119,7 +113,7 @@ private void GenerateWrapper(TopLevelDeclWithMembers parent, MemberDecl decl) {
       newFunc.Name = newName;
 
       var args = origFunc.Formals.Select(Expression.CreateIdentExpr).ToList();
-      var callExpr = MakeApplySuffix(tok, origFunc.Name, args);
+      var callExpr = ApplySuffix.MakeRawApplySuffix(tok, origFunc.Name, args);
       newFunc.Body = callExpr;
 
       var localName = origFunc.Result?.Name ?? "__result";

From 252dc6ef329252887669b687d35fa6bfb01e4a0c Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 15:11:35 -0700
Subject: [PATCH 29/31] Rename the internal constructor for the Externs mode

---
 Source/DafnyCore/DafnyOptions.cs             | 4 ++--
 Source/DafnyCore/Resolver/ExpectContracts.cs | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 3931a56cd83..70b36639dc1 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -98,7 +98,7 @@ public enum PrintModes {
 
     public enum ContractTestingMode {
       None,
-      AllExterns,
+      Externs,
       TestedExterns,
     }
 
@@ -660,7 +660,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) {
         case "testContracts":
           if (ps.ConfirmArgumentCount(1)) {
             if (args[ps.i].Equals("Externs")) {
-              TestContracts = ContractTestingMode.AllExterns;
+              TestContracts = ContractTestingMode.Externs;
             } else if (args[ps.i].Equals("TestedExterns")) {
               TestContracts = ContractTestingMode.TestedExterns;
             } else {
diff --git a/Source/DafnyCore/Resolver/ExpectContracts.cs b/Source/DafnyCore/Resolver/ExpectContracts.cs
index 2b9031abc26..bad39fb694c 100644
--- a/Source/DafnyCore/Resolver/ExpectContracts.cs
+++ b/Source/DafnyCore/Resolver/ExpectContracts.cs
@@ -213,7 +213,7 @@ private bool ShouldCallWrapper(MemberDecl caller, MemberDecl callee) {
 
       var opt = DafnyOptions.O.TestContracts;
       return ((HasTestAttribute(caller) && opt == DafnyOptions.ContractTestingMode.TestedExterns) ||
-              (opt == DafnyOptions.ContractTestingMode.AllExterns)) &&
+              (opt == DafnyOptions.ContractTestingMode.Externs)) &&
              // Skip if the caller is a wrapper, otherwise it'd just call itself recursively.
              !newRedirections.ContainsValue(caller);
     }

From 49f68baba2149642ef24ec3216846e782b13b054 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 15:11:51 -0700
Subject: [PATCH 30/31] Finesse the help text for /testContracts

---
 Source/DafnyCore/DafnyOptions.cs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 70b36639dc1..56fb339a973 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -1445,8 +1445,9 @@ contents are skipped during code generation and verification. This
     from the bottom dependency from being generated more than once.
 
 /testContracts:<Externs|TestedExterns>
-    Enable run-time testing of compiled function or method contracts in
-    certain situations, currently focused on {{:extern}} code.
+    Enable run-time testing of the compilable portions of certain function
+    or method contracts, at their call sites. The current implementation
+    focuses on {{:extern}} code but may support other code in the future.
 
     Externs - Check contracts on every call to a function or method marked
         with the {{:extern}} attribute, regardless of where it occurs.

From d69a1b37fad305b72889f06f4bbd6e73a8335124 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Mon, 26 Sep 2022 15:28:09 -0700
Subject: [PATCH 31/31] Update Options.txt

---
 docs/DafnyRef/Options.txt | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt
index aa124511e5f..b112e326757 100644
--- a/docs/DafnyRef/Options.txt
+++ b/docs/DafnyRef/Options.txt
@@ -480,8 +480,9 @@ Usage: Dafny [ option ... ] [ filename ... ]
       from the bottom dependency from being generated more than once.
   
   /testContracts:<Externs|TestedExterns>
-      Enable run-time testing of compiled function or method contracts in
-      certain situations, currently focused on {:extern} code.
+      Enable run-time testing of the compilable portions of certain function
+      or method contracts, at their call sites. The current implementation
+      focuses on {:extern} code but may support other code in the future.
   
       Externs - Check contracts on every call to a function or method marked
           with the {:extern} attribute, regardless of where it occurs.