Add script to run Boogie with the args Dafny uses

.github/workflows/msbuild.yml

@@ -42,6 +42,9 @@ jobs:
         sudo apt-get update
         sudo apt-get install -qq libxml2-utils
         echo "boogieVersion=`xmllint --xpath "//PackageReference[@Include='Boogie.ExecutionEngine']/@Version" dafny/Source/DafnyCore/DafnyCore.csproj | grep -Po 'Version="\K.*?(?=")'`" >> $GITHUB_ENV
+    - name: Compare Boogie versions
+      working-directory: dafny
+      run: ./Scripts/compare_boogie_versions.sh
     - name: Attempt custom Boogie patch
       working-directory: dafny
       run: git apply customBoogie.patch

Scripts/compare_boogie_versions.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+LIB_VERSION=$(grep Boogie.ExecutionEngine Source/DafnyCore/DafnyCore.csproj | cut -d "\"" -f 4)
+TOOL_VERSION=$(./Scripts/dafny_boogie.sh -version | cut -d ' ' -f 5 | cut -d . -f 1-3)
+if [ "$LIB_VERSION" != "$TOOL_VERSION" ] ; then
+  echo "Mismatched Boogie versions."
+  echo "Library version is ${LIB_VERSION}"
+  echo "dotnet tool version is ${TOOL_VERSION}"
+  exit 1
+else
+  echo "Boogie versions match (${LIB_VERSION})"
+fi

Scripts/dafny_boogie.sh

@@ -0,0 +1,4 @@
+#!/bin/bash
+ROOT=$(dirname $(dirname "${BASH_SOURCE[0]}"))
+BOOGIE_ARGS=$(sed -e 's|^|-|' "${ROOT}"/Source/boogie-args.cfg | sed -e "s|{ROOT}|$ROOT|")
+dotnet tool run boogie $BOOGIE_ARGS "$@"

Source/IntegrationTests/LitTests.cs

@@ -27,17 +27,6 @@ public class LitTests {
 
     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 + $"../unzippedRelease/dafny/z3/bin/z3-{DafnyOptions.DefaultZ3Version}"
-    };
-
     private static readonly LitTestConfiguration Config;
 
     static LitTests() {
@@ -74,6 +63,12 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         { "%repositoryRoot", RepositoryRoot.Replace(@"\", "/") },
       };
 
+      var defaultBoogieArguments =
+        File.ReadAllLines(RepositoryRoot + "Source/boogie-args.cfg")
+          .Select(arg => "-" + arg)
+          .Append("-proverOpt:PROVER_PATH:" + RepositoryRoot + $"../unzippedRelease/dafny/z3/bin/z3-{DafnyOptions.DefaultZ3Version}")
+          .ToArray();
+
       var commands = new Dictionary<string, Func<IEnumerable<string>, LitTestConfiguration, ILitCommand>> {
         {
           "%baredafny", (args, config) =>
@@ -117,7 +112,7 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         }, {
           "%boogie", (args, config) => // TODO
             new DotnetToolCommand("boogie",
-              args.Concat(DefaultBoogieArguments),
+              args.Concat(defaultBoogieArguments),
               config.PassthroughEnvironmentVariables)
         }, {
           "%diff", (args, config) => DiffCommand.Parse(args.ToArray())
@@ -171,7 +166,7 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
           new ShellLitCommand(Path.Join(dafnyReleaseDir, "DafnyServer"), args, config.PassthroughEnvironmentVariables);
         commands["%boogie"] = (args, config) =>
           new DotnetToolCommand("boogie",
-            args.Concat(DefaultBoogieArguments),
+            args.Concat(defaultBoogieArguments),
             config.PassthroughEnvironmentVariables);
         substitutions["%z3"] = Path.Join(dafnyReleaseDir, "z3", "bin", $"z3-{DafnyOptions.DefaultZ3Version}");
       }

Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg

@@ -110,6 +110,21 @@ boogieExecutable = 'dotnet tool run boogie'
 
 config.suffixes.append('.transcript')
 
+def find(name, rooot):
+    for root, dirs, files in os.walk(rooot):
+        for file in files:
+            if file.endswith(name):
+                return name
+    return ""
+
+solverPath = \
+    find("z3-4.12.1", binaryDir) or \
+    find("cvc4", binaryDir)
+
+if not solverPath:
+    lit_config.fatal('Could not find solver')
+config.substitutions.append( ('%z3', solverPath ) )
+
 dafnyArgs = [
     # We do not want absolute or relative paths in error messages, just the basename of the file
     'useBaseNameForFileName',
@@ -131,15 +146,9 @@ dafnyArgs = [
     'standardLibraries:0'
 ]
 
-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'
-]
+boogieArgs = ""
+with open(repositoryRoot + '/Source/boogie-args.cfg', 'r') as boogieArgFile:
+    boogieArgs = boogieArgFile.read().splitlines() + ["proverOpt:PROVER_PATH=" + solverPath]
 
 # Add standard parameters
 def addParams(cmd):
@@ -203,21 +212,6 @@ elif "18.04" in ver and "Ubuntu" in ver:
 else:
     config.available_features = [ 'ubuntu', 'posix' ]
 
-def find(name, rooot):
-    for root, dirs, files in os.walk(rooot):
-        for file in files:
-            if file.endswith(name):
-                return name
-    return ""
-
-solverPath = \
-    find("z3-4.12.1", binaryDir) or \
-    find("cvc4", binaryDir)
-
-if not solverPath:
-    lit_config.fatal('Could not find solver')
-config.substitutions.append( ('%z3', solverPath ) )
-
 # Add diff tool substitution
 commonDiffFlags=' --unified=3 --strip-trailing-cr'
 diffExecutable = None

Source/boogie-args.cfg

@@ -0,0 +1,11 @@
+infer:j
+normalizeDeclarationOrder:1
+normalizeNames:1
+typeEncoding:a
+prune
+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