Merge pull request #133 from diffblue/ebmc-cegar

ebmc CEGAR

regression/ebmc/cegar/basic1.desc

@@ -0,0 +1,6 @@
+CORE
+basic1.sv
+--cegar
+^VERIFICATION SUCCESSFUL -- PROPERTY HOLDS$
+^EXIT=0$
+^SIGNAL=0$

regression/ebmc/cegar/basic1.sv

@@ -0,0 +1,12 @@
+module top(input clk);
+
+  reg important;
+  reg not_important;
+
+  initial important = 1;
+  always @(posedge clk)
+    important = important;
+
+  assert property (important == 1);
+
+endmodule

regression/ebmc/cegar/basic2.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+basic2.sv
+--cegar
+^VERIFICATION FAILED -- PROPERTY REFUTED$
+^EXIT=0$
+^SIGNAL=0$

regression/ebmc/cegar/basic2.sv

@@ -0,0 +1,13 @@
+module top(input clk);
+
+  reg important;
+  reg not_important;
+
+  initial important = 1;
+  always @(posedge clk)
+    important = 0;
+
+  // should fail after one transition
+  assert property (important == 1);
+
+endmodule

src/ebmc/cegar/abstract.cpp

@@ -45,10 +45,8 @@ void bmc_cegart::abstract()
     latch_orderingt latch_ordering;
     latch_ordering.compute(ldg);
 
-    for(unsigned l=0; l<latch_ordering.node_ordering.size(); l++)
-      std::cout << "Latch " << l << ": "
-                << latch_ordering.node_ordering[l] << std::endl;
-
-    exit(0);
+    for(std::size_t l = 0; l < latch_ordering.node_ordering.size(); l++)
+      std::cout << "Latch " << l << ": " << latch_ordering.node_ordering[l]
+                << std::endl;
   }
 }

src/ebmc/cegar/bmc_cegar.cpp

@@ -31,9 +31,7 @@ Function: bmc_cegart::bmc_cegar
 
 void bmc_cegart::bmc_cegar()
 {
-  make_netlist();
-
-  if(properties.empty())
+  if(properties.properties.empty())
   {
     error() << "No properties given" << eom;
     return;
@@ -68,68 +66,24 @@ Function: bmc_cegart::unwind
 \*******************************************************************/
 
 void bmc_cegart::unwind(
-  unsigned bound,
+  std::size_t bound,
   const netlistt &netlist,
-  propt &prop)
+  cnft &solver)
 {
-  // allocate timeframes
-  const auto bmc_map = bmc_mapt{netlist, bound + 1, prop};
-
-#if 0
-  for(unsigned timeframe=0; timeframe<=bound; timeframe++)
-    bmc_map.timeframe_map[timeframe].resize(aig_map.no_vars);
+  ::unwind(netlist, bmc_map, *this, solver);
 
-  // do initial state
-  for(unsigned v=0; v<aig_map.no_vars; v++)
-    bmc_map.timeframe_map[0][v]=prop.new_variable();
+  // one of the properties needs to fail
+  bvt disjuncts;
 
-  // do transitions
-  for(unsigned timeframe=0; timeframe<bound; timeframe++)
+  for(auto &property_it : netlist.properties)
   {
-    status() << "Round " << timeframe << eom;
-
-    aig.clear_convert_cache();
-
-    // set current state bits
-    for(unsigned v=0; v<aig_map.no_vars; v++)
-    {
-      //std::cout << "SETTING "
-      //          << aig_map.timeframe_map[0][v] << std::endl;
-
-      aig.set_l(prop,
-                      aig_map.timeframe_map[0][v],
-                      bmc_map.timeframe_map[timeframe][v]);
-    }
+    auto &prop_bv = prop_bv_map[property_it.first];
+    unwind_property(property_it.second, bmc_map, prop_bv);
 
-    // convert next state bits
-    for(unsigned v=0; v<aig_map.no_vars; v++)
-    {
-      literalt a=aig_map.timeframe_map[1][v];
-
-      // std::cout << "CONVERTING " << a << std::endl;
-
-      literalt l;
-
-      if(latches.find(v)!=latches.end())
-      {
-        assert(aig.can_convert(a));
-
-        l=aig.convert_prop(prop, a);
-      }
-      else
-        l=prop.new_variable();
-
-      bmc_map.timeframe_map[timeframe+1][v]=l;
-    }
+    disjuncts.push_back(!solver.land(prop_bv));
   }
 
-  instantiate(prop, bmc_map, initial_state_predicate, 0, 1,
-              false, ns);
-
-  // do the property
-  property(properties, prop_bv, get_message_handler(), prop,
-           bmc_map, ns);
-#endif
+  solver.lcnf(disjuncts);
 }
 
 /*******************************************************************\
@@ -144,21 +98,19 @@ Function: bmc_cegart::compute_ct
 
 \*******************************************************************/
 
-unsigned bmc_cegart::compute_ct()
+std::size_t bmc_cegart::compute_ct()
 {
-  status() << "Computing CT" << eom;
-
   status() << "Computing abstract LDG" << eom;
 
   ldgt ldg;
- 
+
   ldg.compute(abstract_netlist);
-
-  status() << "Computing CT" << eom;
 
-  unsigned ct=::compute_ct(ldg);
+  status() << "Computing abstract CT" << eom;
 
-  result() << "CT=" << ct << eom;
+  auto ct = ::compute_ct(ldg);
+
+  result() << "Abstract CT=" << ct << eom;
 
   return ct;
 }
@@ -182,8 +134,8 @@ void bmc_cegart::cegar_loop()
   while(true)
   {
     abstract();
-    
-    unsigned ct=compute_ct();
+
+    auto ct = compute_ct();
 
     if(ct>=MAX_CT)
     {
@@ -192,8 +144,8 @@ void bmc_cegart::cegar_loop()
     }
 
     // this is enough
-    unsigned bound=ct;
-    
+    auto bound = ct;
+
     if(verify(bound))
     {
       status() << "VERIFICATION SUCCESSFUL -- PROPERTY HOLDS" << eom;
@@ -212,7 +164,7 @@ void bmc_cegart::cegar_loop()
 
 /*******************************************************************\
 
-Function: bmc_cegart::make_netlist
+Function: do_bmc_cegar
 
   Inputs:
 
@@ -222,34 +174,14 @@ Function: bmc_cegart::make_netlist
 
 \*******************************************************************/
 
-void bmc_cegart::make_netlist()
+int do_bmc_cegar(
+  const netlistt &netlist,
+  ebmc_propertiest &properties,
+  const namespacet &ns,
+  message_handlert &message_handler)
 {
-  // make net-list
-  status() << "Making Netlist" << eom;
-
-  try
-  {
-    const symbolt &module_symbol = ns.lookup(main_module);
-    const transt &trans = to_trans_expr(module_symbol.value);
-
-    std::map<irep_idt, exprt> property_map;
-
-    convert_trans_to_netlist(
-      symbol_table,
-      main_module,
-      trans,
-      property_map,
-      concrete_netlist,
-      get_message_handler());
-  }
-
-  catch(const std::string &error_msg)
-  {
-    error() << error_msg << eom;
-    return;
-  }
+  bmc_cegart bmc_cegar(netlist, properties, ns, message_handler);
 
-  statistics() 
-    << "Latches: " << concrete_netlist.var_map.latches.size()
-    << ", nodes: " << concrete_netlist.number_of_nodes() << eom;
+  bmc_cegar.bmc_cegar();
+  return 0;
 }

src/ebmc/cegar/bmc_cegar.h

@@ -6,59 +6,69 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/std_expr.h>
+#ifndef EBMC_CEGAR_BMC_CEGAR_H
+#define EBMC_CEGAR_BMC_CEGAR_H
+
 #include <util/message.h>
 #include <util/namespace.h>
+#include <util/std_expr.h>
 
+#include <ebmc/ebmc_properties.h>
+#include <ebmc/transition_system.h>
 #include <trans-netlist/bmc_map.h>
 #include <trans-netlist/netlist.h>
 
+class cnft;
+
 class bmc_cegart:public messaget
 {
 public:
   bmc_cegart(
-    symbol_table_baset &_symbol_table,
-    const irep_idt &_main_module,
-    message_handlert &_message_handler,
-    const std::list<exprt> &_properties)
+    const netlistt &_netlist,
+    ebmc_propertiest &_properties,
+    const namespacet &_ns,
+    message_handlert &_message_handler)
     : messaget(_message_handler),
-      symbol_table(_symbol_table),
-      ns(_symbol_table),
-      main_module(_main_module),
-      properties(_properties)
+      properties(_properties),
+      concrete_netlist(_netlist),
+      ns(_ns)
   {
   }
 
   void bmc_cegar();
 
 protected:
-  symbol_table_baset &symbol_table;
-  const namespacet ns;
-  const irep_idt &main_module;
-  const std::list<exprt> &properties;
-
+  ebmc_propertiest &properties;
   bmc_mapt bmc_map;
   netlistt concrete_netlist, abstract_netlist;
+  const namespacet &ns;
 
   bool initial_abstraction;
 
   typedef std::set<literalt> cut_pointst;
   cut_pointst cut_points;
-
-  void make_netlist();
-
+
   void cegar_loop();
 
   void abstract();
   void refine();
-  bool verify(unsigned bound);
-  bool simulate(unsigned bound);
-  unsigned compute_ct();
-
-  void unwind(
-    unsigned bound,
-    const netlistt &netlist,
-    propt &prop);
-
-  std::list<bvt> prop_bv;
+  bool verify(std::size_t bound);
+  bool simulate(std::size_t bound);
+  std::size_t compute_ct();
+
+  void unwind(std::size_t bound, const netlistt &netlist, cnft &solver);
+
+  std::map<irep_idt, bvt> prop_bv_map;
 };
+
+class ebmc_propertiest;
+class message_handlert;
+class netlistt;
+
+int do_bmc_cegar(
+  const netlistt &,
+  ebmc_propertiest &,
+  const namespacet &,
+  message_handlert &);
+
+#endif // EBMC_CEGAR_BMC_CEGAR_H

src/ebmc/cegar/simulate.cpp

@@ -25,7 +25,7 @@ Function: bmc_cegart::simulate
 
 \*******************************************************************/
 
-bool bmc_cegart::simulate(unsigned bound)
+bool bmc_cegart::simulate(std::size_t bound)
 {
   status() << "Simulating Counterexample" << eom;
 
@@ -40,9 +40,6 @@ bool bmc_cegart::simulate(unsigned bound)
   {
   case propt::resultt::P_SATISFIABLE:
     status() << "SAT: bug found within bound" << eom;
-
-    show_counterexample(properties, prop_bv, get_message_handler(), solver,
-                        bmc_map, ns);
     return true;
 
   case propt::resultt::P_UNSATISFIABLE:

src/ebmc/cegar/verify.cpp

@@ -22,9 +22,9 @@ Function: bmc_cegart::verify
 
 \*******************************************************************/
 
-bool bmc_cegart::verify(unsigned bound)
+bool bmc_cegart::verify(const std::size_t bound)
 {
-  status() << "Checking Abstract Model (bound=" << bound << ")" << eom;
+  status() << "Checking abstract model (bound=" << bound << ")" << eom;
 
   satcheckt satcheck{*message_handler};
   cnft &solver=satcheck;

src/ebmc/ebmc_base.h

@@ -37,6 +37,8 @@ class ebmc_baset
   bool make_netlist(netlistt &);
 
   transition_systemt transition_system;
+
+  using propertyt = ebmc_propertiest::propertyt;
   ebmc_propertiest properties;
 
 protected:
@@ -53,7 +55,6 @@ class ebmc_baset
   bool typecheck();
 
   std::size_t bound;
-  using propertyt = ebmc_propertiest::propertyt;
 
 public:
   int do_compute_ct();