Merge pull request #227 from diffblue/waveform

ebmc: add waveform output

regression/ebmc/traces/waveform1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+waveform1.smv
+--bound 20 --waveform
+^EXIT=10$
+^SIGNAL=0$
+^\[smv::main::spec1\] .* FAILURE$
+^Counterexample:$
+^                   0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20$
+^smv::main::var::x  0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20$
+^smv::main::var::y  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0$
+--
+^warning: ignoring

regression/ebmc/traces/waveform1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR x: 0..20;
+VAR y: 0..20;
+
+INIT x=0
+INIT y=0
+
+ASSIGN next(x):=x + 1;
+ASSIGN next(y):=y;
+
+SPEC AG x!=20

src/ebmc/Makefile

@@ -25,6 +25,7 @@ SRC = \
       show_properties.cpp \
       show_trans.cpp \
       transition_system.cpp \
+      waveform.cpp \
       #empty line
 
 OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \

src/ebmc/ebmc_parse_options.cpp

@@ -345,6 +345,7 @@ void ebmc_parse_optionst::help()
     " {y--json-result} {ufile name}  \t use JSON for property status and traces\n"
     " {y--trace}                     \t generate a trace for failing properties\n"
     " {y--vcd} {ufile name}          \t generate traces in VCD format\n"
+    " {y--waveform}                  \t show a waveform for failing properties\n"
     " {y--show-properties}           \t list the properties in the model\n"
     " {y--property} {uid}            \t check the property with given ID\n"
     " {y-I} {upath}                  \t set include path\n"

src/ebmc/ebmc_parse_options.h

@@ -28,7 +28,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(show-ldg)(show-modules)(show-module-hierarchy)"
         "(show-trans)(show-bdds)(show-formula)"
         "(modules-xml):"
-        "(show-properties)(property):p:(trace)"
+        "(show-properties)(property):p:(trace)(waveform)"
         "(dimacs)(module):(top):"
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)(json-result):"

src/ebmc/report_results.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/xml.h>
 
 #include "ebmc_error.h"
+#include "waveform.h"
 
 #include <fstream>
 #include <iostream>
@@ -148,10 +149,18 @@ void report_results(
 
       message.status() << messaget::eom;
 
-      if(property.is_failure() && cmdline.isset("trace"))
+      if(property.is_failure())
       {
-        message.status() << "Counterexample:\n" << messaget::eom;
-        show_trans_trace(property.counterexample, message, ns, std::cout);
+        if(cmdline.isset("trace"))
+        {
+          message.status() << "Counterexample:\n" << messaget::eom;
+          show_trans_trace(property.counterexample, message, ns, std::cout);
+        }
+        else if(cmdline.isset("waveform"))
+        {
+          message.status() << "Counterexample:" << messaget::eom;
+          show_waveform(property.counterexample, ns);
+        }
       }
     }
   }

src/ebmc/waveform.cpp

@@ -0,0 +1,151 @@
+/*******************************************************************\
+
+Module: Waveform Trace Output
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "waveform.h"
+
+#include <util/console.h>
+#include <util/std_expr.h>
+#include <util/symbol.h>
+
+#include <langapi/language_util.h>
+
+#include <algorithm>
+#include <map>
+#include <unordered_set>
+
+std::vector<irep_idt>
+lhs_symbols(const trans_tracet &trace, const namespacet &ns)
+{
+  std::unordered_set<irep_idt, irep_id_hash> identifier_set;
+
+  for(auto &state : trace.states)
+    for(auto &assignment : state.assignments)
+    {
+      auto &lhs = assignment.lhs;
+      if(lhs.id() == ID_symbol)
+      {
+        auto identifier = to_symbol_expr(lhs).get_identifier();
+        auto &symbol = ns.lookup(identifier);
+        if(!symbol.is_auxiliary)
+          identifier_set.insert(identifier);
+      }
+    }
+
+  std::vector<irep_idt> result;
+
+  for(auto identifier : identifier_set)
+    result.push_back(identifier);
+
+  return result;
+}
+
+std::size_t
+max_name_width(const std::vector<irep_idt> &identifiers, const namespacet &ns)
+{
+  std::size_t width = 0;
+
+  for(auto identifier : identifiers)
+  {
+    auto &symbol = ns.lookup(identifier);
+    width = std::max(symbol.display_name().size(), width);
+  }
+
+  return width;
+}
+
+std::vector<std::string> values(const trans_tracet &trace)
+{
+  return {};
+}
+
+void show_waveform(const trans_tracet &trace, const namespacet &ns)
+{
+  auto y_identifiers = lhs_symbols(trace, ns);
+
+  // sort by display_name
+  std::sort(
+    y_identifiers.begin(),
+    y_identifiers.end(),
+    [&ns](const irep_idt &a, const irep_idt &b) {
+      auto &a_symbol = ns.lookup(a);
+      auto &b_symbol = ns.lookup(b);
+      auto &a_name = a_symbol.display_name();
+      auto &b_name = b_symbol.display_name();
+      return a_name.compare(b_name) < 0;
+    });
+
+  std::map<std::pair<irep_idt, std::size_t>, std::string> value_map;
+  std::map<std::size_t, std::size_t> column_width;
+
+  for(std::size_t timeframe = 0; timeframe < trace.states.size(); timeframe++)
+  {
+    auto &state = trace.states[timeframe];
+    for(auto &assignment : state.assignments)
+    {
+      auto &lhs = assignment.lhs;
+      if(lhs.id() == ID_symbol)
+      {
+        auto identifier = to_symbol_expr(lhs).get_identifier();
+        if(assignment.rhs.is_not_nil())
+        {
+          auto as_string = from_expr(ns, identifier, assignment.rhs);
+          value_map[std::make_pair(identifier, timeframe)] = as_string;
+          auto &width = column_width[timeframe];
+          width = std::max(width, as_string.size());
+          if(width < 2)
+            width = 2;
+        }
+      }
+    }
+  }
+
+  auto y_label_width = max_name_width(y_identifiers, ns);
+
+  {
+    consolet::out() << consolet::underline;
+    consolet::out().width(y_label_width);
+    consolet::out() << "";
+
+    for(std::size_t x = 0; x < trace.states.size(); x++)
+    {
+      consolet::out() << ' ';
+      if(consolet::is_terminal() && consolet::use_SGR())
+        consolet::out() << ((x % 2) ? "\x1b[47m" : "");
+      consolet::out().width(column_width[x]);
+      consolet::out() << x % 100;
+      if(consolet::is_terminal() && consolet::use_SGR())
+        consolet::out() << "\x1b[49m";
+    }
+
+    consolet::out() << consolet::reset;
+    consolet::out() << '\n';
+  }
+
+  for(auto y : y_identifiers)
+  {
+    auto &symbol = ns.lookup(y);
+
+    if(consolet::is_terminal() && consolet::use_SGR())
+      consolet::out() << "\x1b[97m\x1b[100m";
+    consolet::out().width(y_label_width);
+    consolet::out() << symbol.display_name();
+    consolet::out() << consolet::reset;
+
+    for(std::size_t x = 0; x < trace.states.size(); x++)
+    {
+      consolet::out() << ' ';
+      if(consolet::is_terminal() && consolet::use_SGR())
+        consolet::out() << ((x % 2) ? "\x1b[47m" : "");
+      consolet::out().width(std::min(std::size_t(2), column_width[x]));
+      consolet::out() << value_map[std::make_pair(y, x)];
+      consolet::out() << consolet::reset;
+    }
+
+    consolet::out() << '\n';
+  }
+}

src/ebmc/waveform.h

@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module: Waveform Trace Output
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_WAVEFORM_H
+#define CPROVER_EBMC_WAVEFORM_H
+
+#include <trans-netlist/trans_trace.h>
+
+void show_waveform(const trans_tracet &, const namespacet &);
+
+#endif