Merge pull request #5237 from thk123/refinement-iteration-printing

Refinement iteration printing

Author: Thomas Kiley

regression/cbmc-incr-oneloop/alarm2/test-json-output.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --json-ui
+^EXIT=10$
+^SIGNAL=0$
+"messageText": "VERIFICATION FAILED"
+"currentUnwinding": 1
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+<text>VERIFICATION FAILED</text>
+<current-unwinding>1</current-unwinding>
+<refinement-iteration>1</refinement-iteration>
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --incremental-loop main.0 --unwind-min 5 --unwind-max 10
+Current unwinding: 1
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -34,7 +34,8 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
       equation,
       options,
       path_storage,
-      guard_manager),
+      guard_manager,
+      ui_message_handler.get_ui()),
     property_decider(options, ui_message_handler, equation, ns)
 {
   setup_symex(symex, ns, options, ui_message_handler);

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -19,7 +19,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   symex_target_equationt &target,
   const optionst &options,
   path_storaget &path_storage,
-  guard_managert &guard_manager)
+  guard_managert &guard_manager,
+  ui_message_handlert::uit output_ui)
   : symex_bmct(
       message_handler,
       outer_symbol_table,
@@ -33,7 +34,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
                                    : std::numeric_limits<unsigned>::max()),
     incr_min_unwind(
       options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min")
-                                   : 0)
+                                   : 0),
+    output_ui(output_ui)
 {
   ignore_assertions =
     incr_min_unwind >= 1 &&
@@ -56,6 +58,7 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind(
     this_loop_limit = incr_max_unwind;
     if(unwind + 1 >= incr_min_unwind)
       ignore_assertions = false;
+
     abort_unwind_decision = tvt(unwind >= this_loop_limit);
   }
   else
@@ -85,6 +88,7 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind(
     abort_unwind_decision.is_known(), "unwind decision should be taken by now");
   bool abort = abort_unwind_decision.is_true();
 
+  log_unwinding(unwind);
   log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                    << " iteration " << unwind;
 
@@ -131,3 +135,29 @@ bool symex_bmc_incremental_one_loopt::resume(
 
   return should_pause_symex;
 }
+void symex_bmc_incremental_one_loopt::log_unwinding(unsigned unwind)
+{
+  const std::string unwind_num = std::to_string(unwind);
+  switch(output_ui)
+  {
+  case ui_message_handlert::uit::PLAIN:
+  {
+    log.statistics() << "Current unwinding: " << unwind_num << messaget::eom;
+    break;
+  }
+  case ui_message_handlert::uit::XML_UI:
+  {
+    xmlt xml("current-unwinding");
+    xml.data = unwind_num;
+    log.statistics() << xml << messaget::eom;
+    break;
+  }
+  case ui_message_handlert::uit::JSON_UI:
+  {
+    json_objectt json;
+    json["currentUnwinding"] = json_numbert(unwind_num);
+    log.statistics() << json << messaget::eom;
+    break;
+  }
+  }
+}

src/goto-checker/symex_bmc_incremental_one_loop.h

@@ -10,6 +10,7 @@
 #define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
 
 #include "symex_bmc.h"
+#include <util/ui_message.h>
 
 class symex_bmc_incremental_one_loopt : public symex_bmct
 {
@@ -20,7 +21,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     symex_target_equationt &,
     const optionst &,
     path_storaget &,
-    guard_managert &);
+    guard_managert &,
+    ui_message_handlert::uit output_ui);
 
   /// Return true if symex can be resumed
   bool from_entry_point_of(
@@ -44,6 +46,10 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     const symex_targett::sourcet &source,
     const call_stackt &context,
     unsigned unwind) override;
+
+  void log_unwinding(unsigned unwind);
+
+  ui_message_handlert::uit output_ui;
 };
 
 #endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H