Add option to print passive version of program (#805)

The `/printPassive` option now instructs `/print` to print the fully
passified version of the program. At the moment, this happens after
verification, as we can be sure the program has been fully processed by
then. Arguably it should happen earlier. Enabling `/printPassive`
automatically enables `/printUnstructured`.

Source/Core/PrintOptions.cs

@@ -13,11 +13,13 @@ public interface PrintOptions {
   bool PrintInlined { get; }
   int StratifiedInlining { get; }
   bool PrintDesugarings { get; set; }
+  bool PrintPassive { get; set; }
   int PrintUnstructured { get; set; }
   bool ReflectAdd { get; }
 }
 
 record PrintOptionsRec(bool PrintWithUniqueASTIds, bool PrintInstrumented, bool PrintInlined, int StratifiedInlining, bool ReflectAdd) : PrintOptions {
   public bool PrintDesugarings { get; set; }
+  public bool PrintPassive { get; set; }
   public int PrintUnstructured { get; set; }
 }

Source/ExecutionEngine/CommandLineOptions.cs

@@ -88,6 +88,11 @@ public bool PrintDesugarings {
       set => printDesugarings = value;
     }
 
+    public bool PrintPassive {
+      get => printPassive;
+      set => printPassive = value;
+    }
+
     public bool PrintLambdaLifting { get; set; }
     public bool FreeVarLambdaLifting { get; set; }
     public string ProverLogFilePath { get; set; }
@@ -559,6 +564,7 @@ void ObjectInvariant5()
     private bool printWithUniqueAstIds = false;
     private int printUnstructured = 0;
     private bool printDesugarings = false;
+    private bool printPassive = false;
     private bool emitDebugInformation = true;
     private bool normalizeNames;
     private bool normalizeDeclarationOrder = true;
@@ -1262,6 +1268,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("printWithUniqueIds", x => printWithUniqueAstIds = x) ||
               ps.CheckBooleanFlag("wait", x => Wait = x) ||
               ps.CheckBooleanFlag("trace", x => Verbosity = CoreOptions.VerbosityLevel.Trace) ||
@@ -1705,6 +1712,7 @@ The pattern <p> matches the whole procedure name and may
   /printWithUniqueIds : print augmented information that uniquely
                    identifies variables
   /printUnstructured : with /print option, desugars all structured statements
+  /printPassive :  with /print option, prints passive version of program
   /printDesugared : with /print option, desugars calls
   /printLambdaLifting : with /print option, desugars lambda lifting
 

Source/ExecutionEngine/ExecutionEngine.cs

@@ -145,7 +145,8 @@ public async Task<bool> ProcessProgram(TextWriter output, Program program, strin
         programId = "main_program_id";
       }
 
-      if (Options.PrintFile != null) {
+      if (Options.PrintFile != null && !Options.PrintPassive) {
+        // Printing passive programs happens later
         PrintBplFile(Options.PrintFile, program, false, true, Options.PrettyPrint);
       }
 
@@ -571,6 +572,10 @@ public async Task<PipelineOutcome> InferAndVerify(
       }
 
       var outcome = await VerifyEachImplementation(output, processedProgram, stats, programId, er, requestId, stablePrioritizedImpls);
+      if (Options.PrintPassive) {
+        Options.PrintUnstructured = 1;
+        PrintBplFile(Options.PrintFile, processedProgram.Program, true, true, Options.PrettyPrint);
+      }
 
       if (1 < Options.VerifySnapshots && programId != null)
       {