Add an experimental backend that uses Lean to discharge goals

Source/ExecutionEngine/CommandLineOptions.cs

@@ -3,7 +3,9 @@
 using System.Collections.Specialized;
 using System.Diagnostics.Contracts;
 using System.IO;
+using Microsoft.Boogie.LeanAuto;
 using Microsoft.Boogie.SMTLib;
+using VC;
 
 namespace Microsoft.Boogie
 {
@@ -64,7 +66,6 @@ void ObjectInvariant2()
     public bool VerifySeparately { get; set; }
     public string PrintFile { get; set; }
     public string PrintPrunedFile { get; set; }
-    public string LeanFile { get; set; }
 
     /**
      * Whether to emit {:qid}, {:skolemid} and set-info :boogie-vc-id
@@ -92,6 +93,37 @@ public bool PrintPassive {
       set => printPassive = value;
     }
 
+    public List<Action<ExecutionEngineOptions, ProcessedProgram>> UseResolvedProgram { get; } = new();
+
+    static void PassifyAllImplementations(ExecutionEngineOptions options, ProcessedProgram processedProgram)
+    {
+      // All three of these objects can be new instances because they're essentially not used by PrepareImplementation.
+      var callback = new VerifierCallback(options.PrintProverWarnings);
+      var checkerPool = new CheckerPool(options);
+      var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, checkerPool);
+
+      foreach(var implementation in processedProgram.Program.Implementations) {
+        vcGenerator.PrepareImplementation(new ImplementationRun(implementation, options.OutputWriter),
+          callback, out _, out _, out _);
+      }
+    }
+
+    public static void PrintPassiveProgram(ExecutionEngineOptions options, ProcessedProgram processedProgram)
+    {
+      options.PrintUnstructured = 1;
+      PassifyAllImplementations(options, processedProgram);
+      ExecutionEngine.PrintBplFile(options, options.PrintFile, processedProgram.Program, true, true, options.PrettyPrint);
+    }
+
+    public static void PrintPassiveProgramAsLean(string fileName, ExecutionEngineOptions options, ProcessedProgram processedProgram)
+    {
+        var writer = new StreamWriter(fileName);
+        PassifyAllImplementations(options, processedProgram);
+        LeanAutoGenerator.EmitPassiveProgramAsLean(options, processedProgram.Program, writer);
+        writer.Close();
+
+    }
+
     public bool PrintLambdaLifting { get; set; }
     public bool FreeVarLambdaLifting { get; set; }
     public string ProverLogFilePath { get; set; }
@@ -406,7 +438,7 @@ public bool TrustRefinement {
       get => trustRefinement;
       set => trustRefinement = value;
     }
-    
+
     public int TrustLayersUpto { get; set; } = -1;
 
     public int TrustLayersDownto { get; set; } = int.MaxValue;
@@ -682,9 +714,10 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
           return true;
 
         case "printLean":
-          if (ps.ConfirmArgumentCount(1))
-          {
-            LeanFile = args[ps.i];
+          if (ps.ConfirmArgumentCount(1)) {
+            var fileName = args[ps.i];
+            UseResolvedProgram.Add((o, p) =>
+              PrintPassiveProgramAsLean(fileName, o, p));
           }
 
           return true;
@@ -1285,7 +1318,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
           if (ps.CheckBooleanFlag("printDesugared", x => printDesugarings = x) ||
               ps.CheckBooleanFlag("printLambdaLifting", x => PrintLambdaLifting = x) ||
               ps.CheckBooleanFlag("printInstrumented", x => printInstrumented = x) ||
-              ps.CheckBooleanFlag("printPassive", x => printPassive = x) ||
+              ps.CheckBooleanFlag("printPassive", x => UseResolvedProgram.Add(PrintPassiveProgram)) ||
               ps.CheckBooleanFlag("printWithUniqueIds", x => printWithUniqueAstIds = x) ||
               ps.CheckBooleanFlag("wait", x => Wait = x) ||
               ps.CheckBooleanFlag("trace", x => Verbosity = CoreOptions.VerbosityLevel.Trace) ||

Source/ExecutionEngine/ExecutionEngine.cs

@@ -553,6 +553,10 @@ public async Task<PipelineOutcome> InferAndVerify(
 
       var processedProgram = PreProcessProgramVerification(program);
 
+      if (Options.UseResolvedProgram.Any()) {
+        Options.UseResolvedProgram.ForEach(action => action(Options, processedProgram));
+      }
+
       if (!Options.Verify)
       {
         return PipelineOutcome.Done;
@@ -572,12 +576,6 @@ public async Task<PipelineOutcome> InferAndVerify(
 
       var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls);
 
-      // We unfortunately have to do any processing of the passive program
-      // after running VerifyEachImplementation, because it passifies the
-      // program in place. We should eventually refactor the code to
-      // passify the program as an independent step.
-      UsePassiveProgram(processedProgram.Program);
-
       if (1 < Options.VerifySnapshots && programId != null)
       {
         program.FreezeTopLevelDeclarations();
@@ -589,20 +587,6 @@ public async Task<PipelineOutcome> InferAndVerify(
       return outcome;
     }
 
-    private void UsePassiveProgram(Program passiveProgram)
-    {
-      if (Options.PrintPassive) {
-        Options.PrintUnstructured = 1;
-        PrintBplFile(Options.PrintFile, passiveProgram, true, true, Options.PrettyPrint);
-      }
-
-      if (Options.LeanFile is not null) {
-        var writer = new StreamWriter(Options.LeanFile);
-        LeanAutoGenerator.EmitPassiveProgramAsLean(Options, passiveProgram, writer);
-        writer.Close();
-      }
-    }
-
     private ProcessedProgram PreProcessProgramVerification(Program program)
     {
       // Doing lambda expansion before abstract interpretation means that the abstract interpreter

Source/ExecutionEngine/ExecutionEngineOptions.cs

@@ -14,7 +14,8 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions
   string DescriptiveToolName { get; }
   bool TraceProofObligations { get; }
   string PrintFile { get; }
-  string LeanFile { get; }
+  List<Action<ExecutionEngineOptions, ProcessedProgram>> UseResolvedProgram { get; }
+
   string PrintCFGPrefix { get; }
   string CivlDesugaredFile { get; }
   bool CoalesceBlocks { get; }

Source/Provers/LeanAuto/LeanAutoGenerator.cs

@@ -197,9 +197,13 @@ public override Cmd VisitAssumeCmd(AssumeCmd node)
 
   public override GotoCmd VisitGotoCmd(GotoCmd node)
   {
-    var gotoText = node.labelTargets.Select(l =>
-      $"goto {BlockName(l)}").Aggregate((a, b) => $"{a} {AndString} {b}");
-    Indent(2, gotoText);
+    string cmd = node.labelTargets.Any()
+      ? node
+        .labelTargets
+        .Select(l => $"goto {BlockName(l)}")
+        .Aggregate((a, b) => $"{a} {AndString} {b}")
+      : "ret";
+    Indent(2, cmd);
     return node;
   }