Enable InferAndVerify to schedule tasks on the scheduler of the caller, enabling verifying different Boogie programs in parallel using one ThreadPool

.github/workflows/test.yml

@@ -12,6 +12,7 @@ on:
 env:
   SOLUTION: Source/Boogie.sln
   Z3URL: https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-ubuntu-16.04.zip
+  CVC5URL: https://github.com/cvc5/cvc5/releases/latest/download/cvc5-Linux
 
 jobs:
   job0:
@@ -20,6 +21,7 @@ jobs:
     strategy:
       matrix:
         configuration: [Debug, Release]
+        lit_param: ["batch_mode=True", "batch_mode=False"]
     steps:
       - name: Setup dotnet
         uses: actions/setup-dotnet@v1
@@ -35,6 +37,10 @@ jobs:
           wget ${Z3URL}
           unzip z3*.zip
           export PATH="$(find $PWD/z3* -name bin -type d):$PATH"
+          # Download a CVC5 release
+          mkdir -p bin
+          (cd bin && wget ${CVC5URL} && mv cvc5-Linux cvc5 && chmod +x cvc5)
+          export PATH="$PWD/bin:$PATH"
           # Install python tools
           sudo pip3 install setuptools
           sudo pip3 install lit OutputCheck pyyaml psutil
@@ -53,7 +59,7 @@ jobs:
           # Run unit tests
           dotnet test --no-build -c ${{ matrix.configuration }} ${SOLUTION}
           # Run lit test suite
-          lit -v --timeout=120 -D configuration=${{ matrix.configuration }} Test
+          lit --param ${{ matrix.lit_param }} -v --timeout=120 -D configuration=${{ matrix.configuration }} Test
       - name: Deploy to nuget
         if: matrix.configuration == 'Release' && startsWith(github.ref, 'refs/tags/v')
         run: dotnet nuget push "Source/**/bin/${{ matrix.configuration }}/Boogie*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json

Source/AbsInt/IntervalDomain.cs

@@ -14,7 +14,7 @@ abstract class E_Common : NativeLattice.Element
 
     class E_Bottom : E_Common
     {
-      public override Expr ToExpr()
+      public override Expr ToExpr(CoreOptions options)
       {
         return Expr.False;
       }
@@ -33,12 +33,12 @@ public E(Node n)
         N = n;
       }
 
-      public override Expr ToExpr()
+      public override Expr ToExpr(CoreOptions options)
       {
         Expr expr = Expr.True;
         for (var n = N; n != null; n = n.Next)
         {
-          expr = BplAnd(expr, n.ToExpr());
+          expr = BplAnd(expr, n.ToExpr(options));
         }
 
         return expr;
@@ -212,10 +212,10 @@ public static IEnumerable<Tuple<Node, Node>> Merge(Node a, Node b)
         }
       }
 
-      public Expr ToExpr()
+      public Expr ToExpr(CoreOptions options)
       {
-        if (!V.IsMutable && CommandLineOptions.Clo.InstrumentInfer !=
-          CommandLineOptions.InstrumentationPlaces.Everywhere)
+        if (!V.IsMutable && options.InstrumentInfer !=
+          CoreOptions.InstrumentationPlaces.Everywhere)
         {
           // omit invariants about readonly variables
           return Expr.True;

Source/AbsInt/NativeLattice.cs

@@ -17,7 +17,7 @@ public abstract class NativeLattice
     /// </summary>
     public abstract class Element
     {
-      public abstract Expr ToExpr();
+      public abstract Expr ToExpr(CoreOptions options);
     }
 
     public abstract Element Top { get; }
@@ -70,14 +70,21 @@ public virtual void Validate()
 
   public class NativeAbstractInterpretation
   {
-    public static void RunAbstractInterpretation(Program program)
+    private CoreOptions options;
+
+    public NativeAbstractInterpretation(CoreOptions options)
+    {
+      this.options = options;
+    }
+
+    public void RunAbstractInterpretation(Program program)
     {
       Contract.Requires(program != null);
 
-      Helpers.ExtraTraceInformation("Starting abstract interpretation");
+      Helpers.ExtraTraceInformation(options, "Starting abstract interpretation");
 
       DateTime start = new DateTime(); // to please compiler's definite assignment rules
-      if (CommandLineOptions.Clo.Trace)
+      if (options.Trace)
       {
         Console.WriteLine();
         Console.WriteLine("Running abstract interpretation...");
@@ -87,11 +94,11 @@ public static void RunAbstractInterpretation(Program program)
       WidenPoints.Compute(program);
 
       NativeLattice lattice = null;
-      if (CommandLineOptions.Clo.Ai.J_Trivial)
+      if (options.Ai.J_Trivial)
       {
         lattice = new TrivialDomain();
       }
-      else if (CommandLineOptions.Clo.Ai.J_Intervals)
+      else if (options.Ai.J_Intervals)
       {
         lattice = new NativeIntervalDomain();
       }
@@ -100,13 +107,13 @@ public static void RunAbstractInterpretation(Program program)
       {
         Dictionary<Procedure, Implementation[]> procedureImplementations = ComputeProcImplMap(program);
         ComputeProgramInvariants(program, procedureImplementations, lattice);
-        if (CommandLineOptions.Clo.Ai.DebugStatistics)
+        if (options.Ai.DebugStatistics)
         {
           Console.Error.WriteLine(lattice.DebugStatistics);
         }
       }
 
-      if (CommandLineOptions.Clo.Trace)
+      if (options.Trace)
       {
         DateTime end = DateTime.UtcNow;
         TimeSpan elapsed = end - start;
@@ -132,7 +139,7 @@ private static Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Progra
     /// <summary>
     /// Compute and apply the invariants for the program using the underlying abstract domain.
     /// </summary>
-    public static void ComputeProgramInvariants(Program program,
+    public void ComputeProgramInvariants(Program program,
       Dictionary<Procedure, Implementation[]> procedureImplementations, NativeLattice lattice)
     {
       Contract.Requires(program != null);
@@ -157,7 +164,7 @@ public static void ComputeProgramInvariants(Program program,
           foreach (var impl in procedureImplementations[proc])
           {
             // add the precondition to the axioms
-            Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap());
+            Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options));
             var start = initialElement;
             foreach (Requires pre in proc.Requires)
             {
@@ -173,14 +180,14 @@ public static void ComputeProgramInvariants(Program program,
       }
     }
 
-    public static void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.Element start)
+    public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.Element start)
     {
       // We need to keep track of some information for each(some) block(s).  To do that efficiently,
       // we number the implementation's blocks sequentially, and then we can use arrays to store
       // the additional information.
       var pre = new NativeLattice.Element[impl.Blocks
         .Count]; // set to null if we never compute a join/widen at this block
-      var post = CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere
+      var post = options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere
         ? new NativeLattice.Element[impl.Blocks.Count]
         : null;
       var iterations = new int[impl.Blocks.Count];
@@ -223,7 +230,7 @@ public static void Analyze(Implementation impl, NativeLattice lattice, NativeLat
           // no change
           continue;
         }
-        else if (b.widenBlock && CommandLineOptions.Clo.Ai.StepsBeforeWidening <= iterations[id])
+        else if (b.widenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
         {
           e = lattice.Widen(pre[id], e);
           pre[id] = e;
@@ -261,22 +268,22 @@ public static void Analyze(Implementation impl, NativeLattice lattice, NativeLat
       Instrument(impl, pre, post);
     }
 
-    static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.Element[] post)
+    void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.Element[] post)
     {
       Contract.Requires(impl != null);
       Contract.Requires(pre != null);
 
       foreach (var b in impl.Blocks)
       {
         var element = pre[b.aiId];
-        if (element != null && (b.widenBlock || CommandLineOptions.Clo.InstrumentInfer ==
-          CommandLineOptions.InstrumentationPlaces.Everywhere))
+        if (element != null && (b.widenBlock || options.InstrumentInfer ==
+          CoreOptions.InstrumentationPlaces.Everywhere))
         {
           List<Cmd> newCommands = new List<Cmd>();
-          Expr inv = element.ToExpr();
+          Expr inv = element.ToExpr(options);
           PredicateCmd cmd;
           var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
-          if (CommandLineOptions.Clo.InstrumentWithAsserts)
+          if (options.InstrumentWithAsserts)
           {
             cmd = new AssertCmd(Token.NoToken, inv, kv);
           }
@@ -289,9 +296,9 @@ static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeL
           newCommands.AddRange(b.Cmds);
           if (post != null && post[b.aiId] != null)
           {
-            inv = post[b.aiId].ToExpr();
+            inv = post[b.aiId].ToExpr(options);
             kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
-            if (CommandLineOptions.Clo.InstrumentWithAsserts)
+            if (options.InstrumentWithAsserts)
             {
               cmd = new AssertCmd(Token.NoToken, inv, kv);
             }
@@ -312,7 +319,7 @@ static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeL
     /// The abstract transition relation.
     /// 'cmd' is allowed to be a StateCmd.
     /// </summary>
-    static NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element elmt)
+    NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element elmt)
     {
       Contract.Requires(lattice != null);
       Contract.Requires(cmd != null);
@@ -364,7 +371,7 @@ static NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.
       else if (cmd is SugaredCmd)
       {
         var c = (SugaredCmd) cmd;
-        elmt = Step(lattice, c.Desugaring, elmt);
+        elmt = Step(lattice, c.GetDesugaring(options), elmt);
       }
       else if (cmd is CommentCmd)
       {

Source/AbsInt/TrivialDomain.cs

@@ -11,7 +11,7 @@ public E(bool isTop)
         IsTop = isTop;
       }
 
-      public override Expr ToExpr()
+      public override Expr ToExpr(CoreOptions options)
       {
         return Expr.Literal(IsTop);
       }

Source/BoogieDriver/BoogieDriver.cs

@@ -11,18 +11,16 @@ public static int Main(string[] args)
     {
       Contract.Requires(cce.NonNullElements(args));
 
-
-      var options = new CommandLineOptionsImpl
+      var options = new CommandLineOptions(new ConsolePrinter())
       {
         RunningBoogieFromCommandLine = true
       };
-      ExecutionEngine.printer = new ConsolePrinter(options);
-      CommandLineOptionsImpl.Install(options);
 
       if (!options.Parse(args))
       {
         return 1;
       }
+      using var executionEngine = ExecutionEngine.CreateWithoutSharedCache(options);
 
       if (options.ProcessInfoFlags())
       {
@@ -31,7 +29,7 @@ public static int Main(string[] args)
 
       if (options.Files.Count == 0)
       {
-        ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");
+        options.Printer.ErrorWriteLine(Console.Out, "*** Error: No input files were specified.");
         return 1;
       }
 
@@ -46,7 +44,7 @@ public static int Main(string[] args)
         string errMsg = options.XmlSink.Open();
         if (errMsg != null)
         {
-          ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg);
+          options.Printer.ErrorWriteLine(Console.Out, "*** Error: " + errMsg);
           return 1;
         }
       }
@@ -63,13 +61,13 @@ public static int Main(string[] args)
         Console.WriteLine("--------------------");
       }
 
-      Helpers.ExtraTraceInformation("Becoming sentient");
+      Helpers.ExtraTraceInformation(options, "Becoming sentient");
 
-      var success = ExecutionEngine.ProcessFiles(options, fileList);
+      var success = executionEngine.ProcessFiles(Console.Out, fileList);
 
-      if (CommandLineOptions.Clo.XmlSink != null)
+      if (options.XmlSink != null)
       {
-        CommandLineOptions.Clo.XmlSink.Close();
+        options.XmlSink.Close();
       }
 
       if (options.Wait)
@@ -81,7 +79,7 @@ public static int Main(string[] args)
       return success ? 0 : 1;
     }
 
-    private static List<string> GetFileList(CommandLineOptionsImpl options)
+    private static List<string> GetFileList(CommandLineOptions options)
     {
       List<string> fileList = new List<string>();
       foreach (string file in options.Files)
@@ -115,7 +113,7 @@ private static List<string> GetFileList(CommandLineOptionsImpl options)
 
         if (extension != ".bpl")
         {
-          ExecutionEngine.printer.ErrorWriteLine(
+          options.Printer.ErrorWriteLine(
             Console.Out,
             "*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).",
             file,