Add option to print passive version of program

boogie-org · Nov 10, 2023 · 0f6a09d · 0f6a09d
1 parent aa56ffb
commit 0f6a09d
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 1 deletion.
diff --git a/Source/Core/PrintOptions.cs b/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; }
 }
diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/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) ||
@@ -1700,6 +1707,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
 

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/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)
       {