From 6ff76eab216127b10dede8e5767e31c54312b912 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 18 Oct 2023 05:58:26 -0700
Subject: [PATCH 1/2] ebmc: re-enable --cegar

This resurrects the defunct CEGAR implementation in ebmc.
---
 src/ebmc/cegar/abstract.cpp     |   8 +-
 src/ebmc/cegar/bmc_cegar.cpp    | 128 ++++++++------------------------
 src/ebmc/cegar/bmc_cegar.h      |  64 +++++++++-------
 src/ebmc/cegar/simulate.cpp     |   5 +-
 src/ebmc/cegar/verify.cpp       |   4 +-
 src/ebmc/ebmc_base.h            |   3 +-
 src/ebmc/ebmc_parse_options.cpp |  34 ++++-----
 7 files changed, 89 insertions(+), 157 deletions(-)

diff --git a/src/ebmc/cegar/abstract.cpp b/src/ebmc/cegar/abstract.cpp
index 455e83f4d..48037bf7e 100644
--- a/src/ebmc/cegar/abstract.cpp
+++ b/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;
   }
 }
diff --git a/src/ebmc/cegar/bmc_cegar.cpp b/src/ebmc/cegar/bmc_cegar.cpp
index 28d7d3244..dfd8db4e1 100644
--- a/src/ebmc/cegar/bmc_cegar.cpp
+++ b/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;
 }
diff --git a/src/ebmc/cegar/bmc_cegar.h b/src/ebmc/cegar/bmc_cegar.h
index 50cd2dafd..a3071fbfc 100644
--- a/src/ebmc/cegar/bmc_cegar.h
+++ b/src/ebmc/cegar/bmc_cegar.h
@@ -6,59 +6,69 @@ 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 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
diff --git a/src/ebmc/cegar/simulate.cpp b/src/ebmc/cegar/simulate.cpp
index 5a791ab5f..166006d9a 100644
--- a/src/ebmc/cegar/simulate.cpp
+++ b/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:
diff --git a/src/ebmc/cegar/verify.cpp b/src/ebmc/cegar/verify.cpp
index ba5e64c0b..77a8580d9 100644
--- a/src/ebmc/cegar/verify.cpp
+++ b/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;
diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h
index 9d6ab6c5e..8ce407b2f 100644
--- a/src/ebmc/ebmc_base.h
+++ b/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();
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index 0997641e4..c453bd812 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ebmc_version.h"
 #include "ic3_engine.h"
 #include "liveness_to_safety.h"
+#include "netlist.h"
 #include "neural_liveness.h"
 #include "output_file.h"
 #include "property_checker.h"
@@ -28,6 +29,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"
@@ -114,26 +117,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";
@@ -299,6 +282,17 @@ int ebmc_parse_optionst::doit()
         return 0;
       }
 
+      if(cmdline.isset("cegar"))
+      {
+        auto netlist = make_netlist(
+          ebmc_base.transition_system,
+          ebmc_base.properties,
+          ui_message_handler);
+        const namespacet ns(ebmc_base.transition_system.symbol_table);
+        return do_bmc_cegar(
+          netlist, ebmc_base.properties, ns, ui_message_handler);
+      }
+
       if(cmdline.isset("compute-ct"))
         return ebmc_base.do_compute_ct();
 

From 1fd30cd790a584d3c484de0425eb0bdc2bd7c7ee Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 18 Oct 2023 06:05:08 -0700
Subject: [PATCH 2/2] ebmc: add two basic tests for CEGAR

---
 regression/ebmc/cegar/basic1.desc |  6 ++++++
 regression/ebmc/cegar/basic1.sv   | 12 ++++++++++++
 regression/ebmc/cegar/basic2.desc |  6 ++++++
 regression/ebmc/cegar/basic2.sv   | 13 +++++++++++++
 4 files changed, 37 insertions(+)
 create mode 100644 regression/ebmc/cegar/basic1.desc
 create mode 100644 regression/ebmc/cegar/basic1.sv
 create mode 100644 regression/ebmc/cegar/basic2.desc
 create mode 100644 regression/ebmc/cegar/basic2.sv

diff --git a/regression/ebmc/cegar/basic1.desc b/regression/ebmc/cegar/basic1.desc
new file mode 100644
index 000000000..60fd10d0d
--- /dev/null
+++ b/regression/ebmc/cegar/basic1.desc
@@ -0,0 +1,6 @@
+CORE
+basic1.sv
+--cegar
+^VERIFICATION SUCCESSFUL -- PROPERTY HOLDS$
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/ebmc/cegar/basic1.sv b/regression/ebmc/cegar/basic1.sv
new file mode 100644
index 000000000..105aa9418
--- /dev/null
+++ b/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
diff --git a/regression/ebmc/cegar/basic2.desc b/regression/ebmc/cegar/basic2.desc
new file mode 100644
index 000000000..cb7e55d35
--- /dev/null
+++ b/regression/ebmc/cegar/basic2.desc
@@ -0,0 +1,6 @@
+KNOWNBUG
+basic2.sv
+--cegar
+^VERIFICATION FAILED -- PROPERTY REFUTED$
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/ebmc/cegar/basic2.sv b/regression/ebmc/cegar/basic2.sv
new file mode 100644
index 000000000..6d961c548
--- /dev/null
+++ b/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