ebmc CEGAR

regression/ebmc/cegar/basic1.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+basic1.sv
+--cegar
+SUCCESS$
+^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

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;
@@ -213,7 +211,7 @@ void bmc_cegart::cegar_loop()
 
 /*******************************************************************\
 
-Function: bmc_cegart::make_netlist
+Function: do_bmc_cegar
 
   Inputs:
 
@@ -223,25 +221,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
-  {
-    convert_trans_to_netlist(
-      symbol_table, main_module,
-      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,47 +6,46 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#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 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();
@@ -62,3 +61,15 @@ class bmc_cegart:public messaget
 
   std::list<bvt> prop_bv;
 };
+
+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

@@ -41,8 +41,19 @@ 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);
+    {
+      std::list<exprt> property_expr_list;
+      for(auto &p : properties.properties)
+        property_expr_list.push_back(p.expr);
+
+      show_counterexample(
+        property_expr_list,
+        prop_bv,
+        get_message_handler(),
+        solver,
+        bmc_map,
+        ns);
+    }
     return true;
 
   case propt::resultt::P_UNSATISFIABLE:

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:
@@ -58,7 +60,6 @@ class ebmc_baset
   bool typecheck();
 
   std::size_t bound;
-  using propertyt = ebmc_propertiest::propertyt;
 
 public:
   int do_compute_ct();

src/ebmc/ebmc_parse_options.cpp

@@ -28,6 +28,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <iostream>
 
+#include "cegar/bmc_cegar.h"
+
 #ifdef HAVE_INTERPOLATION
 #include "interpolation/interpolation_expr.h"
 #include "interpolation/interpolation_netlist.h"
@@ -112,26 +114,6 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("show-symbol-table"))
       return show_symbol_table(cmdline, ui_message_handler);
 
-    if(cmdline.isset("cegar"))
-    {
-      throw ebmc_errort() << "This option is currently disabled";
-
-#if 0
-      namespacet ns(symbol_table);
-      var_mapt var_map(symbol_table, main_symbol->name);
-
-      bmc_cegart bmc_cegar(
-        var_map,
-        *trans_expr,
-        ns,
-        *this,
-        prop_expr_list);
-
-      bmc_cegar.bmc_cegar();
-      return 0;
-#endif
-    }
-
     if(cmdline.isset("coverage"))
     {
       throw ebmc_errort() << "This option is currently disabled";
@@ -292,7 +274,15 @@ int ebmc_parse_optionst::doit()
       if(result != -1)
         return result;
 
-      if(cmdline.isset("compute-ct"))
+      if(cmdline.isset("cegar"))
+      {
+        netlistt netlist;
+        ebmc_base.make_netlist(netlist);
+        const namespacet ns(ebmc_base.transition_system.symbol_table);
+        return do_bmc_cegar(
+          netlist, ebmc_base.properties, ns, ui_message_handler);
+      }
+      else if(cmdline.isset("compute-ct"))
         return ebmc_base.do_compute_ct();
 
       // possibly apply liveness-to-safety