Merge pull request #347 from diffblue/live-signal

nuterm: add 'live' signal

regression/ebmc/neural-liveness/live_signal1.desc

@@ -0,0 +1,17 @@
+CORE
+counter1.sv
+--number-of-traces 1 --neural-liveness --show-traces
+^nuterm::live@0 = 0$
+^nuterm::live@1 = 0$
+^nuterm::live@2 = 0$
+^nuterm::live@3 = 0$
+^nuterm::live@4 = 0$
+^nuterm::live@5 = 0$
+^nuterm::live@6 = 0$
+^nuterm::live@7 = 0$
+^nuterm::live@8 = 0$
+^nuterm::live@9 = 0$
+^nuterm::live@10 = 1$
+^EXIT=0$
+^SIGNAL=0$
+--

src/ebmc/Makefile

@@ -17,6 +17,7 @@ SRC = \
       ebmc_solver_factory.cpp \
       k_induction.cpp \
       liveness_to_safety.cpp \
+      live_signal.cpp \
       main.cpp \
       negate_property.cpp \
       neural_liveness.cpp \

src/ebmc/ebmc_parse_options.h

@@ -27,6 +27,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(show-parse)(show-varmap)(show-symbol-table)(show-netlist)"
         "(show-ldg)(show-modules)(show-module-hierarchy)"
         "(show-trans)(show-bdds)(show-formula)"
+        "(show-traces)"
         "(modules-xml):"
         "(show-properties)(property):p:(trace)(waveform)(numbered-trace)"
         "(dimacs)(module):(top):"

src/ebmc/live_signal.cpp

@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module: Live Signal
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "live_signal.h"
+
+#include <smvlang/temporal_expr.h>
+#include <verilog/sva_expr.h>
+
+#include "transition_system.h"
+
+void set_live_signal(transition_systemt &transition_system, exprt property)
+{
+  static const irep_idt identifier = "nuterm::live";
+
+  // add symbol if needed
+  if(!transition_system.symbol_table.has_symbol(identifier))
+  {
+    symbolt live_symbol{
+      identifier, bool_typet(), transition_system.main_symbol->mode};
+
+    live_symbol.module = transition_system.main_symbol->module;
+    live_symbol.base_name = "live";
+
+    const auto symbol_expr = live_symbol.symbol_expr();
+
+    auto result = transition_system.symbol_table.insert(std::move(live_symbol));
+    CHECK_RETURN(result.second);
+  }
+
+  const auto p = [](const exprt &expr) -> exprt {
+    if(expr.id() == ID_AF)
+      return to_AF_expr(expr).op();
+    else if(
+      expr.id() == ID_sva_always &&
+      to_sva_always_expr(expr).op().id() == ID_sva_eventually)
+    {
+      return to_sva_eventually_expr(to_sva_always_expr(expr).op()).op();
+    }
+    else
+      PRECONDITION(false);
+  }(property);
+
+  const auto live_symbol_expr = symbol_exprt(identifier, bool_typet());
+
+  auto &trans_expr = transition_system.trans_expr;
+
+  trans_expr.invar() =
+    conjunction({trans_expr.invar(), equal_exprt(live_symbol_expr, p)});
+}

src/ebmc/live_signal.h

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: Live Signal
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef EBMC_LIVE_SIGNAL_H
+#define EBMC_LIVE_SIGNAL_H
+
+#include <util/expr.h>
+
+class transition_systemt;
+
+void set_live_signal(transition_systemt &, exprt property);
+
+#endif // EBMC_LIVE_SIGNAL_H

src/ebmc/neural_liveness.cpp

@@ -13,16 +13,21 @@ Author: Daniel Kroening, [email protected]
 #include <util/string2int.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
+#include <util/unicode.h>
 
+#include <smvlang/temporal_expr.h>
 #include <verilog/sva_expr.h>
 
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
+#include "live_signal.h"
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "report_results.h"
+#include "waveform.h"
 
 #include <fstream>
+#include <iostream>
 
 /*******************************************************************\
 
@@ -51,14 +56,20 @@ class neural_livenesst
   transition_systemt transition_system;
   ebmc_propertiest properties;
 
+  int show_traces();
   void validate_properties();
-  void sample(temp_dirt &);
+  void set_live_signal(const ebmc_propertiest::propertyt &, const exprt &);
+  void sample(std::function<void(trans_tracet)>);
+  std::function<void(trans_tracet)> dump_vcd_files(temp_dirt &);
   exprt guess(ebmc_propertiest::propertyt &, const temp_dirt &);
   tvt verify(ebmc_propertiest::propertyt &, const exprt &candidate);
 };
 
 int neural_livenesst::operator()()
 {
+  if(cmdline.isset("show-traces"))
+    return show_traces();
+
   if(!cmdline.isset("neural-engine"))
     throw ebmc_errort() << "give a neural engine";
 
@@ -73,19 +84,29 @@ int neural_livenesst::operator()()
   // neural liveness.
   validate_properties();
 
-  // Now sample some traces.  These get stored in a set of files, one per
-  // trace, and are then read by the neural fitting procedure.
-  temp_dirt temp_dir("ebmc-neural.XXXXXXXX");
-  sample(temp_dir);
-
   auto solver_factory = ebmc_solver_factory(cmdline);
 
-  // We now do a guess-verify loop, per property.
+  // Save the transition system expression,
+  // to add the constraint for the 'live' signal.
+  const auto original_trans_expr = transition_system.main_symbol->value;
+
+  // We do everything per property.
   for(auto &property : properties.properties)
   {
     if(property.is_disabled())
       continue;
 
+    // Set the liveness signal for the property.
+    set_live_signal(property, original_trans_expr);
+
+    // Now sample some traces.
+    // Store the traces in a set of files, one per
+    // trace, which are then read by the neural fitting procedure.
+    temp_dirt temp_dir("ebmc-neural.XXXXXXXX");
+    const auto trace_files_prefix = temp_dir("trace.");
+    sample(dump_vcd_files(temp_dir));
+
+    // Now do a guess-and-verify loop.
     while(true)
     {
       const auto candidate = guess(property, temp_dir);
@@ -102,6 +123,34 @@ int neural_livenesst::operator()()
   return 0;
 }
 
+int neural_livenesst::show_traces()
+{
+  transition_system =
+    get_transition_system(cmdline, message.get_message_handler());
+
+  properties = ebmc_propertiest::from_command_line(
+    cmdline, transition_system, message.get_message_handler());
+
+  validate_properties();
+
+  const auto original_trans_expr = transition_system.main_symbol->value;
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled())
+      continue;
+
+    set_live_signal(property, original_trans_expr);
+
+    sample([&](trans_tracet trace) {
+      namespacet ns(transition_system.symbol_table);
+      show_trans_trace_numbered(trace, message, ns, std::cout);
+    });
+  }
+
+  return 0;
+}
+
 void neural_livenesst::validate_properties()
 {
   if(properties.properties.empty())
@@ -131,10 +180,37 @@ void neural_livenesst::validate_properties()
   }
 }
 
-void neural_livenesst::sample(temp_dirt &temp_dir)
+void neural_livenesst::set_live_signal(
+  const ebmc_propertiest::propertyt &property,
+  const exprt &original_trans_expr)
 {
-  const auto trace_files_prefix = temp_dir("trace.");
+  // restore the original transition system
+  auto main_symbol_writeable = transition_system.symbol_table.get_writeable(
+    transition_system.main_symbol->name);
+  main_symbol_writeable->value = original_trans_expr; // copy
+  ::set_live_signal(transition_system, property.expr);
+}
 
+std::function<void(trans_tracet)>
+neural_livenesst::dump_vcd_files(temp_dirt &temp_dir)
+{
+  const auto outfile_prefix = temp_dir("trace.");
+  return
+    [&, trace_nr = 0ull, outfile_prefix](trans_tracet trace) mutable -> void {
+      namespacet ns(transition_system.symbol_table);
+      auto filename = outfile_prefix + std::to_string(trace_nr + 1);
+      std::ofstream out(widen_if_needed(filename));
+
+      if(!out)
+        throw ebmc_errort() << "failed to write trace to " << filename;
+
+      message.progress() << "*** Writing " << filename << messaget::eom;
+      show_trans_trace_vcd(trace, message, ns, out);
+    };
+}
+
+void neural_livenesst::sample(std::function<void(trans_tracet)> trace_consumer)
+{
   const auto number_of_traces = [this]() -> std::size_t
   {
     if(cmdline.isset("number-of-traces"))
@@ -172,7 +248,7 @@ void neural_livenesst::sample(temp_dirt &temp_dir)
 
   random_traces(
     transition_system,
-    trace_files_prefix,
+    trace_consumer,
     number_of_traces,
     number_of_trace_steps,
     message.get_message_handler());

src/ebmc/random_traces.cpp

@@ -320,6 +320,31 @@ void random_traces(
 
 /*******************************************************************\
 
+Function: random_traces
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void random_traces(
+  const transition_systemt &transition_system,
+  std::function<void(trans_tracet)> consumer,
+  std::size_t number_of_traces,
+  std::size_t number_of_trace_steps,
+  message_handlert &message_handler)
+{
+  std::size_t random_seed = 0;
+
+  random_tracest(transition_system, message_handler)(
+    consumer, random_seed, number_of_traces, number_of_trace_steps);
+}
+
+/*******************************************************************\
+
 Function: random_tracest::random_bit
 
   Inputs: