Bump to cbmc-develop and make compileable [WIP]

1: there is no `bmct` so hw-cbmc uses the verifier factory
2: smt2 support is dropped for now (smt decision procedure don't have access to
`propt`, have to find out how to convert properties at world-level)
3: `aigt` support now lives in trans-netlist (copied from 5.8)

(strange clang-formatting in ebmc-solvers)

Author: petr-bauch

lib/cbmc

@@ -1,9 +1,12 @@
 default: tests.log
 
+include ../../lib/cbmc/src/config.inc
+include ../../lib/cbmc/src/common
+
 test:
 	@../test.pl -c ../../../src/ebmc/ebmc
 
-tests.log: ../test.pl ../../../src/ebmc/ebmc
+tests.log: ../test.pl
 	@../test.pl
 
 show:

regression/ebmc/Makefile

@@ -1,7 +1,9 @@
 DIRS = ebmc hw-cbmc trans-word-level trans-netlist verilog vhdl smvlang ic3 aiger
 
-CPROVER_DIR = lib/cbmc/src
+EBMC_DIR:=$(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
+CPROVER_DIR = $(EBMC_DIR)/../lib/cbmc/src
 export CPROVER_DIR
+export EBMC_DIR
 
 all: hw-cbmc.dir ebmc.dir
 
@@ -22,8 +24,8 @@ hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
 # building cbmc proper
 .PHONY: cprover.dir
 cprover.dir:
-	$(MAKE) $(MAKEARGS) -C ../$(CPROVER_DIR) \
-	CXXFLAGS='-D"LOCAL_IREP_IDS=<../../../src/hw_cbmc_irep_ids.h>" -Wall -pedantic -Werror -Wno-deprecated-declarations'
+	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR) \
+	CXXFLAGS='-D"LOCAL_IREP_IDS=<$(EBMC_DIR)/hw_cbmc_irep_ids.h>" -Wall -pedantic -Werror -Wno-deprecated-declarations -g'
 
 clean: $(patsubst %, %_clean, $(SUBDIRS))
 

src/Makefile

@@ -1,8 +1,9 @@
 SRC = aiger_language.cpp
 
-include ../config.inc
+include $(CPROVER_DIR)/config.inc
+include $(CPROVER_DIR)/common
 
-INCLUDES= -I $(CBMC)/src
+INCLUDES= -I $(CPROVER_DIR)
 
 CLEANFILES = 
 

src/aiger/Makefile

@@ -19,16 +19,20 @@ SRC = \
       show_trans.cpp \
       #empty line
 
-OBJ+= $(CBMC)/src/util/util$(LIBEXT) \
-      $(CBMC)/src/langapi/langapi$(LIBEXT) \
-      $(CBMC)/src/goto-programs/system_library_symbols$(OBJEXT) \
-      $(CBMC)/src/solvers/solvers$(LIBEXT) \
-      $(CBMC)/src/big-int/big-int$(LIBEXT) \
+OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \
+      $(CPROVER_DIR)/langapi/langapi$(LIBEXT) \
+      $(CPROVER_DIR)/goto-programs/system_library_symbols$(OBJEXT) \
+      $(CPROVER_DIR)/solvers/solvers$(LIBEXT) \
+      $(CPROVER_DIR)/big-int/big-int$(LIBEXT) \
+      $(CPROVER_DIR)/util/c_types$(OBJEXT) \
+      $(CPROVER_DIR)/goto-programs/xml_expr$(OBJEXT) \
       ../trans-netlist/trans-netlist$(LIBEXT) \
       ../trans-word-level/trans-word-level$(LIBEXT) \
       ../smvlang/smvlang$(LIBEXT) \
       ../aiger/aiger$(LIBEXT) \
-      ../ic3/libic3$(LIBEXT)   
+      ../ic3/libic3$(LIBEXT) \
+      ../trans-netlist/aig$(OBJEXT) \
+      ../trans-netlist/aig_prop$(OBJEXT)
 
 ifdef MODULE_INTERPOLATION
   CXXFLAGS += -DHAVE_INTERPOLATION
@@ -53,9 +57,10 @@ ifneq ($(wildcard ../vhdl/Makefile),)
   CXXFLAGS += -DHAVE_VHDL
 endif
 
-include ../config.inc
+include $(CPROVER_DIR)/config.inc
+include $(CPROVER_DIR)/common
 
-INCLUDES= -I .. -I $(CBMC)/src
+INCLUDES= -I $(CPROVER_DIR) -I ..
 
 CXXFLAGS += -D'LOCAL_IREP_IDS=<hw_cbmc_irep_ids.h>'
 

src/ebmc/Makefile

@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <algorithm>
 
-#include <solvers/miniBDD/miniBDD.h>
+#include <solvers/bdd/miniBDD/miniBDD.h>
 #include <solvers/sat/satcheck.h>
 
 #include <trans-netlist/aig_prop.h>
@@ -349,7 +349,7 @@ void bdd_enginet::compute_counterexample(
 
   bmc_mapt bmc_map;
 
-  satcheckt solver;
+  satcheckt solver{*message_handler};
   bmc_map.map_timeframes(netlist, number_of_timeframes, solver);
 
   const namespacet ns(symbol_table);
@@ -372,7 +372,7 @@ void bdd_enginet::compute_counterexample(
 
   case propt::resultt::P_UNSATISFIABLE:
     throw "SAT solver says UNSAT!";
-    
+  case propt::resultt::P_ERROR:
   default:
     throw "unexpected result from SAT solver";
   }
@@ -717,9 +717,8 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr)
 
     assert(expr.type().id()==ID_bool);
 
-    aig_prop_constraintt aig_prop(netlist);
-    aig_prop.set_message_handler(get_message_handler());
-    
+    aig_prop_constraintt aig_prop(netlist, *message_handler);
+
     const namespacet ns(symbol_table);
 
     literalt l=instantiate_convert(

src/ebmc/bdd_engine.cpp

@@ -29,7 +29,7 @@ bool bmc_cegart::simulate(unsigned bound)
 {
   status() << "Simulating Counterexample" << eom;
 
-  satcheckt satcheck;
+  satcheckt satcheck{*message_handler};
   cnft &solver=satcheck;
 
   unwind(bound, concrete_netlist, solver);
@@ -41,9 +41,8 @@ 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, ui_message_handlert::uit::PLAIN);
+    show_counterexample(properties, prop_bv, get_message_handler(), solver,
+                        bmc_map, ns);
     return true;
 
   case propt::resultt::P_UNSATISFIABLE:

src/ebmc/cegar/simulate.cpp

@@ -26,7 +26,7 @@ bool bmc_cegart::verify(unsigned bound)
 {
   status() << "Checking Abstract Model (bound=" << bound << ")" << eom;
 
-  satcheckt satcheck;
+  satcheckt satcheck{*message_handler};
   cnft &solver=satcheck;
 
   unwind(bound, abstract_netlist, solver);

src/ebmc/cegar/verify.cpp

@@ -24,11 +24,11 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-void diatest(bool efficient, unsigned no_states, unsigned state_bits)
-{
+void diatest(bool efficient, unsigned no_states, unsigned state_bits,
+             message_handlert &message_handler) {
   std::cout << (efficient?"Efficient:":"Simple:") << '\n';
 
-  dimacs_cnft solver;
+  dimacs_cnft solver{message_handler};
 
   std::vector<bvt> states;
 
@@ -67,13 +67,13 @@ void diatest(bool efficient, unsigned no_states, unsigned state_bits)
 
 \*******************************************************************/
 
-void diatest(unsigned bound, unsigned state_bits)
-{
+void diatest(unsigned bound, unsigned state_bits,
+             message_handlert &message_handler) {
   unsigned no_states=bound+1;
 
   std::cout << "Testing recurrence diameter computation:" << '\n';
   std::cout << "States: " << no_states << '\n';
   std::cout << "State bits: " << state_bits << '\n';
-  diatest(0, no_states, state_bits);
-  diatest(1, no_states, state_bits);
+  diatest(0, no_states, state_bits, message_handler);
+  diatest(1, no_states, state_bits, message_handler);
 }