fix: Fix naming of formals in Translator (dafny-lang#2266)

Fixes dafny-lang#2263, which is due to inconsistent naming of formal parameters in
automatically generated function handles.

Explanation: The syntax of `MkTyParamFormals` was changed with commit
dafny-lang@81cf582
from

```cs
List<Bpl.Variable> MkTyParamFormals(List<TypeParameter> args, bool named = true)
```
 to

```cs
List<Variable> MkTyParamFormals(List<TypeParameter> args, bool includeWhereClause, bool named = true)
```

But the call to the method [on this
line](https://github.com/dafny-lang/dafny/blob/fcc912f9b117115cbc8b2273800397e88d3c1e53/Source/Dafny/Verifier/Translator.cs#L6855)
was left unchanged, so the method is now being called with `named` field
set to the default `true`.
[Elsewhere](https://github.com/dafny-lang/dafny/blob/fcc912f9b117115cbc8b2273800397e88d3c1e53/Source/Dafny/Verifier/Translator.cs#L6882)
the formal parameters of the a function handle don't get a name. The
result is a mix-match of named and unnamed formals that causes the bug
reported in the linked issue.

I don't completely understand the meaning of `includeWhereClause` in
this context but I think `false` is the correct value for this call?

---------

Co-authored-by: Sasha Fedchin <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>

Source/DafnyCore/Verifier/Translator.cs

@@ -5656,7 +5656,7 @@ public string FunctionHandle(Function f) {
         functionHandles[f] = name;
         var args = new List<Bpl.Expr>();
         var vars = MkTyParamBinders(GetTypeParams(f), out args);
-        var formals = MkTyParamFormals(GetTypeParams(f), false);
+        var formals = MkTyParamFormals(GetTypeParams(f), false, false);
         var tyargs = new List<Bpl.Expr>();
         foreach (var fm in f.Formals) {
           tyargs.Add(TypeToTy(fm.Type));

Source/IntegrationTests/LitTests.cs

@@ -24,6 +24,18 @@ public class LitTests {
     private static readonly Assembly TestDafnyAssembly = typeof(TestDafny.TestDafny).Assembly;
     private static readonly Assembly DafnyServerAssembly = typeof(Server).Assembly;
 
+    private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net6.0/
+    private static readonly string[] DefaultBoogieArguments = new[] {
+      "/infer:j",
+      "/proverOpt:O:auto_config=false",
+      "/proverOpt:O:type_check=true",
+      "/proverOpt:O:smt.case_split=3",
+      "/proverOpt:O:smt.qi.eager_threshold=100",
+      "/proverOpt:O:smt.delay_units=true",
+      "/proverOpt:O:smt.arith.solver=2",
+      "/proverOpt:PROVER_PATH:" + RepositoryRoot + "Binaries/z3/bin/z3"
+    };
+
     private static readonly LitTestConfiguration Config;
 
     static LitTests() {
@@ -36,14 +48,12 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         return (extraDafnyArguments is null ? args : args.Append(extraDafnyArguments)).Concat(local);
       }
 
-      var repositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net6.0/
-
       var substitutions = new Dictionary<string, object> {
         { "%diff", "diff" },
         { "%resolveargs", "--useBaseNameForFileName" },
         { "%binaryDir", "." },
         { "%z3", Path.Join("z3", "bin", "z3") },
-        { "%repositoryRoot", repositoryRoot.Replace(@"\", "/") },
+        { "%repositoryRoot", RepositoryRoot.Replace(@"\", "/") },
       };
 
       var commands = new Dictionary<string, Func<IEnumerable<string>, LitTestConfiguration, ILitCommand>> {
@@ -61,6 +71,11 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         }, {
           "%server", (args, config) =>
             MainMethodLitCommand.Parse(DafnyServerAssembly, args, config, InvokeMainMethodsDirectly)
+        }, {
+          "%boogie", (args, config) =>
+            new DotnetToolCommand("boogie",
+              args.Concat(DefaultBoogieArguments),
+              config.PassthroughEnvironmentVariables)
         }, {
           "%diff", (args, config) => DiffCommand.Parse(args.ToArray())
         }, {
@@ -110,6 +125,10 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
             InvokeMainMethodsDirectly);
         commands["%server"] = (args, config) =>
           new ShellLitCommand(Path.Join(dafnyReleaseDir, "DafnyServer"), args, config.PassthroughEnvironmentVariables);
+        commands["%boogie"] = (args, config) =>
+          new DotnetToolCommand("boogie",
+            args.Concat(DefaultBoogieArguments),
+            config.PassthroughEnvironmentVariables);
         substitutions["%z3"] = Path.Join(dafnyReleaseDir, "z3", "bin", "z3");
       }
 

Source/XUnitExtensions/Lit/DotnetToolCommand.cs

@@ -0,0 +1,13 @@
+using System.Collections.Generic;
+using System.Linq;
+
+namespace XUnitExtensions.Lit {
+
+  public class DotnetToolCommand : ShellLitCommand {
+
+    private static readonly string[] DotnetToolArgs = { "tool", "run" };
+
+    public DotnetToolCommand(string dotnetToolName, IEnumerable<string> arguments, IEnumerable<string> passthroughEnvironmentVariables) :
+      base("dotnet", DotnetToolArgs.Append(dotnetToolName).Concat(arguments), passthroughEnvironmentVariables) { }
+  }
+}

Test/git-issues/git-issue-2266.dfy

@@ -0,0 +1,5 @@
+// RUN: %dafny /compile:0 /noVerify /print:%t.bpl "%s"
+// RUN: %boogie "%t.bpl" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function Test(f: (int ~> bool)): (b:bool) reads f.reads { true }

Test/git-issues/git-issue-2266.dfy.expect

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

Test/lit.site.cfg

@@ -107,6 +107,8 @@ testDafnyExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.joi
 defaultServerExecutable = 'dotnet run --no-build --project ' + quotePath(os.path.join(sourceDirectory, 'DafnyServer', 'DafnyServer.csproj'))
 serverExecutable = lit_config.params.get('serverExecutable', defaultServerExecutable)
 
+boogieExecutable = 'dotnet tool run boogie'
+
 config.suffixes.append('.transcript')
 
 dafnyArgs = [
@@ -123,7 +125,18 @@ dafnyArgs = [
     # Set a default time limit, to catch cases where verification time runs off the rails
     'timeLimit:300'
 ]
+
+boogieArgs = [
+    'infer:j',
+    'proverOpt:O:auto_config=false',
+    'proverOpt:O:type_check=true',
+    'proverOpt:O:smt.case_split=3',
+    'proverOpt:O:smt.qi.eager_threshold=100',
+    'proverOpt:O:smt.delay_units=true',
+    'proverOpt:O:smt.arith.solver=2'
+]
 
+# Add standart parameters
 newDafnyArgs = [
 # We do not want absolute or relative paths in error messages, just the basename of the file
 '--use-basename-for-filename',
@@ -144,20 +157,22 @@ def addParams(cmd):
         return cmd
 
 # Add run specific parameters
-def buildCmd(args):
+def buildCmd(cmd, args):
     if len(args) > 0:
         argStr = ' /'.join(args)
-        return f'{dafnyExecutable} /{argStr}'
+        return f'{cmd} /{argStr}'
     else:
         return args
-
-dafny = addParams(buildCmd(dafnyArgs))
+
+dafny = addParams(buildCmd(dafnyExecutable, dafnyArgs))
+boogie = buildCmd(boogieExecutable, boogieArgs)
 
 standardArguments = addParams(' '.join(newDafnyArgs))
 
 # Inform user what executable is being used
 lit_config.note(f'Using Dafny (%dafny): {dafny}\n')
 lit_config.note(f'%baredafny will expand to {dafnyExecutable}\n')
+lit_config.note(f'%boogie will expand to {boogie}\n')
 
 ver = "0"
 if os.name != "nt":
@@ -167,6 +182,7 @@ config.substitutions.append( ('%resolveargs', "--useBaseNameForFileName" ) )
 config.substitutions.append( ('%repositoryRoot', repositoryRoot) )
 config.substitutions.append( ('%binaryDir', binaryDir) )
 config.substitutions.append( ('%dafny', dafny) )
+config.substitutions.append( ('%boogie', boogie) )
 config.substitutions.append( ('%args', standardArguments) )
 config.substitutions.append( ('%testDafnyForEachCompiler', testDafnyExecutable) )
 config.substitutions.append( ('%baredafny', dafnyExecutable) )
@@ -221,4 +237,4 @@ if outputCheckPath == None:
 
 config.substitutions.append( ('%OutputCheck', outputCheckPath + ' --dump-file-to-check  --comment=//') )
 
-config.substitutions.append( ('%{dirsep}', os.sep) )
+config.substitutions.append( ('%{dirsep}', os.sep) )

docs/dev/news/2266.fix

@@ -0,0 +1 @@
+Fix Dafny to Boogie translation of FunctionHandles

dotnet-tools.json

@@ -13,6 +13,12 @@
       "commands": [
         "dotnet-format"
       ]
+    },
+    "boogie": {
+      "version": "2.15.9",
+      "commands": [
+        "boogie"
+      ]
     }
   }
 }