Merge pull request #3342 from tautschnig/show_program

Refactor show_program [blocks: #2310]

Author: tautschnig

src/goto-symex/show_program.cpp

@@ -17,87 +17,64 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/language_util.h>
 
+/// Output a single SSA step
+/// \param ns: Namespace
+/// \param step: SSA step
+/// \param annotation: Additonal information to include in step output
+/// \param count: Step number, incremented after output
+static void show_step(
+  const namespacet &ns,
+  const symex_target_equationt::SSA_stept &step,
+  const std::string &annotation,
+  std::size_t &count)
+{
+  const irep_idt &function = step.source.function;
+
+  std::string string_value = (step.is_shared_read() || step.is_shared_write())
+                               ? from_expr(ns, function, step.ssa_lhs)
+                               : from_expr(ns, function, step.cond_expr);
+  std::cout << '(' << count << ") ";
+  if(annotation.empty())
+    std::cout << string_value;
+  else
+    std::cout << annotation << '(' << string_value << ')';
+  std::cout << '\n';
+
+  if(!step.guard.is_true())
+  {
+    const std::string guard_string = from_expr(ns, function, step.guard);
+    std::cout << std::string(std::to_string(count).size() + 3, ' ');
+    std::cout << "guard: " << guard_string << '\n';
+  }
+
+  ++count;
+}
+
 void show_program(const namespacet &ns, const symex_target_equationt &equation)
 {
-  unsigned count = 1;
+  std::size_t count = 1;
 
-  std::cout << "\n"
-            << "Program constraints:"
-            << "\n";
+  std::cout << '\n' << "Program constraints:" << '\n';
 
   for(const auto &step : equation.SSA_steps)
   {
     std::cout << "// " << step.source.pc->location_number << " ";
     std::cout << step.source.pc->source_location.as_string() << "\n";
-    const irep_idt &function = step.source.function;
 
     if(step.is_assignment())
-    {
-      std::string string_value = from_expr(ns, function, step.cond_expr);
-      std::cout << "(" << count << ") " << string_value << "\n";
-
-      if(!step.guard.is_true())
-      {
-        std::string string_value = from_expr(ns, function, step.guard);
-        std::cout << std::string(std::to_string(count).size() + 3, ' ');
-        std::cout << "guard: " << string_value << "\n";
-      }
-
-      count++;
-    }
+      show_step(ns, step, "", count);
     else if(step.is_assert())
-    {
-      std::string string_value = from_expr(ns, function, step.cond_expr);
-      std::cout << "(" << count << ") ASSERT(" << string_value << ") "
-                << "\n";
-
-      if(!step.guard.is_true())
-      {
-        std::string string_value = from_expr(ns, function, step.guard);
-        std::cout << std::string(std::to_string(count).size() + 3, ' ');
-        std::cout << "guard: " << string_value << "\n";
-      }
-
-      count++;
-    }
+      show_step(ns, step, "ASSERT", count);
     else if(step.is_assume())
-    {
-      std::string string_value = from_expr(ns, function, step.cond_expr);
-      std::cout << "(" << count << ") ASSUME(" << string_value << ") "
-                << "\n";
-
-      if(!step.guard.is_true())
-      {
-        std::string string_value = from_expr(ns, function, step.guard);
-        std::cout << std::string(std::to_string(count).size() + 3, ' ');
-        std::cout << "guard: " << string_value << "\n";
-      }
-
-      count++;
-    }
+      show_step(ns, step, "ASSUME", count);
     else if(step.is_constraint())
     {
-      std::string string_value = from_expr(ns, function, step.cond_expr);
-      std::cout << "(" << count << ") CONSTRAINT(" << string_value << ") "
-                << "\n";
-
-      count++;
-    }
-    else if(step.is_shared_read() || step.is_shared_write())
-    {
-      std::string string_value = from_expr(ns, function, step.ssa_lhs);
-      std::cout << "(" << count << ") SHARED_"
-                << (step.is_shared_write() ? "WRITE" : "READ") << "("
-                << string_value << ")\n";
-
-      if(!step.guard.is_true())
-      {
-        std::string string_value = from_expr(ns, function, step.guard);
-        std::cout << std::string(std::to_string(count).size() + 3, ' ');
-        std::cout << "guard: " << string_value << "\n";
-      }
-
-      count++;
+      PRECONDITION(step.guard.is_true());
+      show_step(ns, step, "CONSTRAINT", count);
     }
+    else if(step.is_shared_read())
+      show_step(ns, step, "SHARED_READ", count);
+    else if(step.is_shared_write())
+      show_step(ns, step, "SHARED_WRITE", count);
   }
 }