Merge pull request #116 from diffblue/liveness-to-safety

ebmc: liveness to safety translation

Author: kroening

regression/ebmc/liveness-to-safety/failing1.desc

@@ -0,0 +1,7 @@
+CORE
+failing1.sv
+--bound 1 --liveness-to-safety
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.property\.p0\] always eventually main\.my_bit: REFUTED$
+--

regression/ebmc/liveness-to-safety/failing1.sv

@@ -0,0 +1,13 @@
+module main(input clk);
+
+  reg my_bit;
+
+  initial my_bit=0;
+
+  always @(posedge clk)
+    my_bit = 0;
+
+  // expected to fail
+  p0: assert property (eventually my_bit);
+
+endmodule

regression/ebmc/liveness-to-safety/failing2.desc

@@ -0,0 +1,8 @@
+CORE
+failing2.sv
+--bound 6 --liveness-to-safety
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.property\.p0\] always eventually main\.counter == 0: REFUTED$
+^\[main\.property\.p1\] always eventually main\.counter == 6: REFUTED$
+--

regression/ebmc/liveness-to-safety/failing2.sv

@@ -0,0 +1,17 @@
+module main(input clk);
+
+  reg [31:0] counter;
+
+  initial counter=0;
+
+  always @(posedge clk)
+    if(counter == 5)
+      counter = 5;
+    else
+      counter=counter+1;
+
+  // both expected to fail
+  p0: assert property (eventually counter==0);
+  p1: assert property (eventually counter==6);
+
+endmodule

regression/ebmc/liveness-to-safety/passing1.desc

@@ -0,0 +1,7 @@
+CORE
+passing1.sv
+--bound 10 --liveness-to-safety
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.property\.p0\] always eventually main\.my_bit: PROVED up to bound 10$
+--

regression/ebmc/liveness-to-safety/passing1.sv

@@ -0,0 +1,13 @@
+module main(input clk);
+
+  reg my_bit;
+
+  initial my_bit=0;
+
+  always @(posedge clk)
+    my_bit = !my_bit;
+
+  // expected to pass
+  p0: assert property (eventually my_bit);
+
+endmodule

regression/ebmc/liveness-to-safety/passing2.desc

@@ -0,0 +1,8 @@
+CORE
+passing2.sv
+--bound 10 --liveness-to-safety
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.property\.p0\] always eventually main\.counter == 0: PROVED up to bound 10$
+^\[main\.property\.p1\] always eventually main\.counter == 8: PROVED up to bound 10$
+--

regression/ebmc/liveness-to-safety/passing2.sv

@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [31:0] counter;
+
+  initial counter=0;
+
+  always @(posedge clk)
+    counter=counter+1;
+
+  // both expected to pass
+  p0: assert property (eventually counter==0);
+  p1: assert property (eventually counter==8);
+
+endmodule

src/ebmc/Makefile

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

src/ebmc/ebmc_base.cpp

@@ -56,27 +56,6 @@ ebmc_baset::ebmc_baset(
 
 /*******************************************************************\
 
-Function: ebmc_baset::property_requires_lasso_constraints
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bool ebmc_baset::property_requires_lasso_constraints() const
-{
-  for(const auto &p : properties.properties)
-    if(!p.is_disabled() && requires_lasso_constraints(p.expr))
-      return true;
-
-  return false;
-}
-
-/*******************************************************************\
-
 Function: ebmc_baset::finish_word_level_bmc
 
   Inputs:
@@ -108,7 +87,7 @@ void ebmc_baset::word_level_properties(decision_proceduret &solver)
   }
 
   // lasso constraints, if needed
-  if(property_requires_lasso_constraints())
+  if(properties.requires_lasso_constraints())
   {
     message.status() << "Adding lasso constraints" << messaget::eom;
     lasso_constraints(

src/ebmc/ebmc_base.h

@@ -37,6 +37,7 @@ class ebmc_baset
   bool make_netlist(netlistt &);
 
   transition_systemt transition_system;
+  ebmc_propertiest properties;
 
 protected:
   messaget message;
@@ -62,11 +63,7 @@ class ebmc_baset
   bool typecheck();
 
   std::size_t bound;
-
   using propertyt = ebmc_propertiest::propertyt;
-  ebmc_propertiest properties;
-
-  bool property_requires_lasso_constraints() const;
 
 public:
   int do_compute_ct();

src/ebmc/ebmc_error.h

@@ -36,9 +36,16 @@ class ebmc_errort
     return std::move(*this);
   }
 
+  ebmc_errort with_location(source_locationt _location) &&
+  {
+    __location = std::move(_location);
+    return std::move(*this);
+  }
+
 protected:
   std::ostringstream message;
   optionalt<int> __exit_code = {};
+  source_locationt __location = source_locationt::nil();
 };
 
 /// add to the diagnostic information in the given ebmc_error exception

src/ebmc/ebmc_parse_options.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_version.h"
 #include "ic3_engine.h"
 #include "k_induction.h"
+#include "liveness_to_safety.h"
 #include "neural_liveness.h"
 #include "random_traces.h"
 #include "ranking_function.h"
@@ -293,7 +294,12 @@ int ebmc_parse_optionst::doit()
 
       if(cmdline.isset("compute-ct"))
         return ebmc_base.do_compute_ct();
-      else if(cmdline.isset("aig") || cmdline.isset("dimacs"))
+
+      // possibly apply liveness-to-safety
+      if(cmdline.isset("liveness-to-safety"))
+        liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
+
+      if(cmdline.isset("aig") || cmdline.isset("dimacs"))
         return ebmc_base.do_bit_level_bmc();
       else
         return ebmc_base.do_word_level_bmc(); // default
@@ -354,6 +360,7 @@ void ebmc_parse_optionst::help()
     " {y--property} {uid}            \t check the property with given ID\n"
     " {y-I} {upath}                  \t set include path\n"
     " {y--reset} {uexpr}             \t set up module reset\n"
+    " {y--liveness-to-safety}        \t translate liveness properties to safety properties\n"
     "\n"
     "Methods:\n"
     " {y--k-induction}               \t do k-induction with k=bound\n"

src/ebmc/ebmc_parse_options.h

@@ -44,6 +44,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
         "(random-traces)(trace-steps):(random-seed):(number-of-traces):"
         "(random-trace)(random-waveform)"
+        "(liveness-to-safety)"
         "I:(preprocess)",
         argc,
         argv,

src/ebmc/ebmc_properties.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/prop/literal.h>
 #include <trans-netlist/trans_trace.h>
+#include <trans-word-level/property.h>
 
 #include "transition_system.h"
 
@@ -137,6 +138,11 @@ class ebmc_propertiest
     std::string status_as_string() const;
 
     propertyt() = default;
+
+    bool requires_lasso_constraints() const
+    {
+      return ::requires_lasso_constraints(expr);
+    }
   };
 
   typedef std::list<propertyt> propertiest;
@@ -151,6 +157,15 @@ class ebmc_propertiest
     return true;
   }
 
+  bool requires_lasso_constraints() const
+  {
+    for(const auto &p : properties)
+      if(!p.is_disabled() && p.requires_lasso_constraints())
+        return true;
+
+    return false;
+  }
+
   static ebmc_propertiest from_command_line(
     const cmdlinet &,
     const transition_systemt &,