Retrace improve logging

Author: lks9

src/goto-symex/symex_goto.cpp

@@ -647,68 +647,78 @@ void goto_symext::symex_goto_retrace(statet &state)
 
   // goto or next depends on input trace from user
   bool choose_goto;
-  bool default_choice;
-  static int retrace_index = 0;
-  if (retrace_index < static_cast<int>(symex_config.retrace_input.size()))
+  static size_t retrace_index = 0;
+  if (retrace_index < symex_config.retrace_input.size())
   {
     choose_goto = symex_config.retrace_input[retrace_index] == '1';
-    default_choice = false;
-    retrace_index++;
   }
   else
   {
     choose_goto = false;
-    default_choice = true;
   }
+  retrace_index++;
 
   // print goto choice
-  if(true){
-    source_locationt cur = state.source.pc->source_location();
-    source_locationt goto_dest = goto_target->source_location();
-    source_locationt next_dest = next_instruction->source_location();
-    source_locationt t_dest  = choose_goto ? goto_dest : next_dest;
-    source_locationt nt_dest = choose_goto ? next_dest : goto_dest;
-
-    auto cur_file = cur.get_file();
-    if(cur_file.empty()) cur_file = "<unknown>";
-    auto t_file = t_dest.get_file();
-    if(t_file.empty()) t_file = "<unknown>";
-    auto nt_file = nt_dest.get_file();
-    if(nt_file.empty()) nt_file = "<unknown>";
-
-    // print nothing when files are the same
-    if(cur_file == t_file) t_file = "";
-    if(cur_file == nt_file) nt_file = "";
-
-    auto cur_line = cur.get_line();
-    if(cur_line.empty()) cur_line = "?";
-    auto t_line = t_dest.get_line();
-    if(t_line.empty()) t_line = "?";
-    auto nt_line = nt_dest.get_line();
-    if(nt_line.empty()) nt_line = "?";
-
-    std::string mode = default_choice ? "Retrace* " : "Retrace ";
-    std::string desc = choose_goto ? "1/GOTO" : "0/NEXT";
-
-    std::string padding_1 = std::string(abs(3-cur_line.size()), ' ');
-    std::string padding_2 = std::string(abs(3-t_line.size()), ' ');
-
-    log.status() << mode << desc
-                 << " at " << cur_file << ":" << cur_line << padding_1
-                 << " to " << t_file << ":" << t_line << padding_2
-                 << " (not " << nt_file << ":" << nt_line << ")"
-                 << log.eom;
-  }
+  log.conditional_output(
+    log.status(),
+    [this, &state, &goto_target, &next_instruction, choose_goto](messaget::mstreamt &mstream) {
+      source_locationt cur = state.source.pc->source_location();
+      source_locationt goto_dest = goto_target->source_location();
+      source_locationt next_dest = next_instruction->source_location();
+      source_locationt t_dest  = choose_goto ? goto_dest : next_dest;
+      source_locationt nt_dest = choose_goto ? next_dest : goto_dest;
+
+      auto cur_file = cur.get_file();
+      if(cur_file.empty()) cur_file = "<unknown>";
+      auto t_file = t_dest.get_file();
+      if(t_file.empty()) t_file = "<unknown>";
+      auto nt_file = nt_dest.get_file();
+      if(nt_file.empty()) nt_file = "<unknown>";
+
+      // print nothing when files are the same
+      if(cur_file == t_file) t_file = "";
+      if(cur_file == nt_file) nt_file = "";
+
+      auto cur_line = cur.get_line();
+      if(cur_line.empty()) cur_line = "?";
+      auto t_line = t_dest.get_line();
+      if(t_line.empty()) t_line = "?";
+      auto nt_line = nt_dest.get_line();
+      if(nt_line.empty()) nt_line = "?";
+
+      std::string head = symex_config.retrace_input;
+      // add 0s in case input trace was shorter
+      head.resize(retrace_index-1, '0');
+      std::string decision = choose_goto ? "1" : "0";
+
+      std::string step = choose_goto ? " goto " : " next ";
+
+      std::string padding_1 = cur_line.size() < 3
+                            ? std::string(3-cur_line.size(), ' ')
+                            : "";
+      std::string padding_2 = t_line.size() < 3
+                            ? std::string(3-t_line.size(), ' ')
+                            : "";
+
+      mstream << "Retrace " << head << messaget::bold << decision << messaget::reset
+              << " at " << cur_file << ":" << cur_line << padding_1
+              << step << t_file << ":" << t_line << padding_2
+              << " (not " << nt_file << ":" << nt_line << ")"
+              << messaget::eom;
+    });
 
   // warn when not following unconditional goto
   if(new_guard.is_true() && !choose_goto)
   {
-    log.warning() << "Retrace input \033[31minconsistent\033[0m: 0/NEXT although guard is true!"
-                  << log.eom;
+    log.result() << "Retrace input " << messaget::red << "inconsistent" << messaget::reset
+                 << ": 0/next although guard is true!"
+                 << log.eom;
   }
   else if(new_guard.is_false() && choose_goto)
   {
-    log.warning() << "Retrace input inconsistent: 1/GOTO although guard is false!" << log.eom;
+    log.result() << "Retrace input " << messaget::red << "inconsistent" << messaget::reset
+                 << ": 1/goto although guard is false!"
+                 << log.eom;
   }
 
   symex_targett::sourcet original_source=state.source;
@@ -773,15 +783,11 @@ void goto_symext::symex_goto_retrace(statet &state)
   {
     symex_assume_l2(state, guard_expr);
     state.guard.add(guard_expr);
-    log.debug() << "Following jump target"
-                << log.eom;
   }
   else
   {
     symex_assume_l2(state, boolean_negate(guard_expr));
     state.guard.add(boolean_negate(guard_expr));
-    log.debug() << "Following next instruction"
-                << log.eom;
   }
   return;
 }