Merge pull request #3557 from peterschrammel/solver-factory

peterschrammel · web-flow · commit 8065b1075515 · 2018-12-17T18:34:48.000Z
Move cbmc_solvers as solver_factory to new goto-checker module [blocks: 3564, 3565]
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -58,6 +58,7 @@ set_target_properties(
     goto-analyzer-lib
     goto-cc
     goto-cc-lib
+    goto-checker
     goto-diff
     goto-diff-lib
     goto-instrument
diff --git a/jbmc/src/jbmc/CMakeLists.txt b/jbmc/src/jbmc/CMakeLists.txt
@@ -12,6 +12,7 @@ target_link_libraries(jbmc-lib
     ansi-c
     big-int
     cbmc-lib
+    goto-checker
     goto-instrument-lib
     goto-programs
     goto-symex
diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile
@@ -6,6 +6,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../java_bytecode/java_bytecode$(LIBEXT) \
       ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
       ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
       ../$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
       ../$(CPROVER_DIR)/src/pointer-analysis/value_set$(OBJEXT) \
@@ -40,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
-      ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
       ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt
@@ -1,6 +1,7 @@
 analyses
 ansi-c # should go away
-cbmc # bmc.h
+cbmc # bmc.h - will go away
+goto-checker
 goto-instrument
 goto-programs
 goto-symex
diff --git a/jbmc/unit/CMakeLists.txt b/jbmc/unit/CMakeLists.txt
@@ -23,7 +23,9 @@ target_link_libraries(java-unit
         testing-utils
         ansi-c
         solvers
+        goto-checker
         goto-programs
+        goto-symex
         goto-instrument-lib
         cbmc-lib
         json-symtab-language
diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
@@ -86,7 +86,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
-          $(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
           $(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
@@ -114,6 +113,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
               $(CPROVER_DIR)/src/util/util$(LIBEXT) \
               $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+              $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -85,6 +85,7 @@ add_subdirectory(ansi-c)
 add_subdirectory(assembler)
 add_subdirectory(big-int)
 add_subdirectory(cpp)
+add_subdirectory(goto-checker)
 add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
 add_subdirectory(jsil)
diff --git a/src/Makefile b/src/Makefile
@@ -6,6 +6,7 @@ DIRS = analyses \
        cpp \
        goto-analyzer \
        goto-cc \
+       goto-checker \
        goto-diff \
        goto-instrument \
        goto-programs \
@@ -49,9 +50,11 @@ solvers.dir: util.dir langapi.dir
 goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
                      goto-symex.dir linking.dir analyses.dir solvers.dir
 
+goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir
+
 cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
-          goto-instrument.dir
+          goto-instrument.dir goto-checker.dir
 
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    goto-instrument.dir
diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt
@@ -13,6 +13,7 @@ target_link_libraries(cbmc-lib
     assembler
     big-int
     cpp
+    goto-checker
     goto-instrument-lib
     goto-programs
     goto-symex
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
@@ -4,7 +4,6 @@ SRC = all_properties.cpp \
       cbmc_languages.cpp \
       cbmc_main.cpp \
       cbmc_parse_options.cpp \
-      cbmc_solvers.cpp \
       counterexample_beautification.cpp \
       fault_localization.cpp \
       symex_bmc.cpp \
@@ -18,6 +17,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../json-symtab-language/json-symtab-language$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
+      ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../goto-symex/goto-symex$(LIBEXT) \
       ../pointer-analysis/value_set$(OBJEXT) \
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -32,7 +32,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <linking/static_lifetime_init.h>
 
-#include "cbmc_solvers.h"
+#include <goto-checker/solver_factory.h>
+
 #include "counterexample_beautification.h"
 #include "fault_localization.h"
 
@@ -519,13 +520,13 @@ int bmct::do_language_agnostic_bmc(
   try
   {
     {
-      cbmc_solverst solvers(
+      solver_factoryt solvers(
         opts,
         symbol_table,
         ui,
         ui.get_ui() == ui_message_handlert::uit::XML_UI);
-      std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
-      cbmc_solver = solvers.get_solver();
+      std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
+        solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
       bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
       if(driver_configure_bmc)
@@ -566,13 +567,13 @@ int bmct::do_language_agnostic_bmc(
 
     while(!worklist->empty())
     {
-      cbmc_solverst solvers(
+      solver_factoryt solvers(
         opts,
         symbol_table,
         ui,
         ui.get_ui() == ui_message_handlert::uit::XML_UI);
-      std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
-      cbmc_solver = solvers.get_solver();
+      std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
+        solvers.get_solver();
       prop_convt &pc = cbmc_solver->prop_conv();
       path_storaget::patht &resume = worklist->peek();
       path_explorert pe(
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
@@ -24,13 +24,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <analyses/goto_check.h>
 
+#include <goto-checker/solver_factory.h>
+
 #include <goto-programs/goto_trace.h>
 
 #include <solvers/refinement/string_refinement.h>
 
 #include "bmc.h"
 #include "xml_interface.h"
-#include "cbmc_solvers.h"
 
 class bmct;
 class goto_functionst;
diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt
@@ -1,6 +1,7 @@
 analyses
 ansi-c
 cpp
+goto-checker
 goto-instrument
 goto-programs
 goto-symex
diff --git a/src/goto-checker/CMakeLists.txt b/src/goto-checker/CMakeLists.txt
@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(goto-checker ${sources})
+
+generic_includes(goto-checker)
+
+target_link_libraries(goto-checker goto-programs goto-symex solvers util)
diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile
@@ -0,0 +1,16 @@
+SRC = solver_factory.cpp \
+      # Empty last line
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = goto-checker$(LIBEXT)
+
+all: goto-checker$(LIBEXT)
+
+###############################################################################
+
+goto-checker$(LIBEXT): $(OBJ)
+	$(LINKLIB)
diff --git a/src/goto-checker/module_dependencies.txt b/src/goto-checker/module_dependencies.txt
@@ -0,0 +1,5 @@
+goto-checker
+goto-programs
+goto-symex
+solvers
+util
diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp
diff --git a/src/goto-checker/solver_factory.h b/src/goto-checker/solver_factory.h
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
diff --git a/unit/Makefile b/unit/Makefile
diff --git a/unit/module_dependencies.txt b/unit/module_dependencies.txt
diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp
