Move cbmc_solvers as solver_factory to goto-checker module
This is the first step of introducing the goto-checker module which will hold the language-agnostic BMC classes.
This commit is contained in:
parent
0a21a31fba
commit
bac549b50b
|
@ -58,6 +58,7 @@ set_target_properties(
|
|||
goto-analyzer-lib
|
||||
goto-cc
|
||||
goto-cc-lib
|
||||
goto-checker
|
||||
goto-diff
|
||||
goto-diff-lib
|
||||
goto-instrument
|
||||
|
|
|
@ -12,6 +12,7 @@ target_link_libraries(jbmc-lib
|
|||
ansi-c
|
||||
big-int
|
||||
cbmc-lib
|
||||
goto-checker
|
||||
goto-instrument-lib
|
||||
goto-programs
|
||||
goto-symex
|
||||
|
|
|
@ -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) \
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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) \
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -13,6 +13,7 @@ target_link_libraries(cbmc-lib
|
|||
assembler
|
||||
big-int
|
||||
cpp
|
||||
goto-checker
|
||||
goto-instrument-lib
|
||||
goto-programs
|
||||
goto-symex
|
||||
|
|
|
@ -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) \
|
||||
|
|
|
@ -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(
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
analyses
|
||||
ansi-c
|
||||
cpp
|
||||
goto-checker
|
||||
goto-instrument
|
||||
goto-programs
|
||||
goto-symex
|
||||
|
|
|
@ -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)
|
|
@ -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)
|
|
@ -0,0 +1,5 @@
|
|||
goto-checker
|
||||
goto-programs
|
||||
goto-symex
|
||||
solvers
|
||||
util
|
|
@ -1,15 +1,15 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Solvers for VCs Generated by Symbolic Execution of ANSI-C
|
||||
Module: Solver Factory
|
||||
|
||||
Author: Daniel Kroening, kroening@kroening.com
|
||||
Author: Daniel Kroening, Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Solvers for VCs Generated by Symbolic Execution of ANSI-C
|
||||
/// Solver Factory
|
||||
|
||||
#include "cbmc_solvers.h"
|
||||
#include "solver_factory.h"
|
||||
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
|
@ -28,11 +28,9 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <solvers/sat/satcheck.h>
|
||||
#include <solvers/smt2/smt2_dec.h>
|
||||
|
||||
#include "counterexample_beautification.h"
|
||||
|
||||
/// Uses the options to pick an SMT 2.0 solver
|
||||
/// \return An smt2_dect::solvert giving the solver to use.
|
||||
smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
|
||||
smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
|
||||
{
|
||||
// we shouldn't get here if this option isn't set
|
||||
PRECONDITION(options.get_bool_option("smt2"));
|
||||
|
@ -59,7 +57,7 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
|
|||
return s;
|
||||
}
|
||||
|
||||
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
|
||||
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
|
||||
{
|
||||
auto solver=util_make_unique<solvert>();
|
||||
|
||||
|
@ -88,7 +86,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
|
|||
return solver;
|
||||
}
|
||||
|
||||
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
|
||||
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
|
||||
{
|
||||
no_beautification();
|
||||
no_incremental_check();
|
||||
|
@ -102,7 +100,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
|
|||
return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
|
||||
}
|
||||
|
||||
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
|
||||
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
|
||||
{
|
||||
std::unique_ptr<propt> prop=[this]() -> std::unique_ptr<propt>
|
||||
{
|
||||
|
@ -138,7 +136,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
|
|||
/// the string refinement adds to the bit vector refinement specifications for
|
||||
/// functions from the Java string library
|
||||
/// \return a solver for cbmc
|
||||
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
|
||||
std::unique_ptr<solver_factoryt::solvert>
|
||||
solver_factoryt::get_string_refinement()
|
||||
{
|
||||
string_refinementt::infot info;
|
||||
info.ns=&ns;
|
||||
|
@ -157,8 +156,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
|
|||
util_make_unique<string_refinementt>(info), std::move(prop));
|
||||
}
|
||||
|
||||
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
|
||||
smt2_dect::solvert solver)
|
||||
std::unique_ptr<solver_factoryt::solvert>
|
||||
solver_factoryt::get_smt2(smt2_dect::solvert solver)
|
||||
{
|
||||
no_beautification();
|
||||
|
||||
|
@ -234,7 +233,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
|
|||
}
|
||||
}
|
||||
|
||||
void cbmc_solverst::no_beautification()
|
||||
void solver_factoryt::no_beautification()
|
||||
{
|
||||
if(options.get_bool_option("beautify"))
|
||||
{
|
||||
|
@ -243,7 +242,7 @@ void cbmc_solverst::no_beautification()
|
|||
}
|
||||
}
|
||||
|
||||
void cbmc_solverst::no_incremental_check()
|
||||
void solver_factoryt::no_incremental_check()
|
||||
{
|
||||
const bool all_properties = options.get_bool_option("all-properties");
|
||||
const bool cover = options.is_set("cover");
|
|
@ -1,16 +1,16 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Bounded Model Checking for ANSI-C + HDL
|
||||
Module: Solver Factory
|
||||
|
||||
Author: Daniel Kroening, kroening@kroening.com
|
||||
Author: Daniel Kroening, Peter Schrammel
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Bounded Model Checking for ANSI-C + HDL
|
||||
/// Solver Factory
|
||||
|
||||
#ifndef CPROVER_CBMC_CBMC_SOLVERS_H
|
||||
#define CPROVER_CBMC_CBMC_SOLVERS_H
|
||||
#ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
|
||||
#define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
|
||||
|
||||
#include <list>
|
||||
#include <map>
|
||||
|
@ -25,10 +25,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <solvers/smt2/smt2_dec.h>
|
||||
#include <goto-symex/symex_target_equation.h>
|
||||
|
||||
class cbmc_solverst
|
||||
class solver_factoryt
|
||||
{
|
||||
public:
|
||||
cbmc_solverst(
|
||||
solver_factoryt(
|
||||
const optionst &_options,
|
||||
const symbol_tablet &_symbol_table,
|
||||
message_handlert &_message_handler,
|
||||
|
@ -113,7 +113,7 @@ public:
|
|||
return get_default();
|
||||
}
|
||||
|
||||
virtual ~cbmc_solverst()
|
||||
virtual ~solver_factoryt()
|
||||
{
|
||||
}
|
||||
|
||||
|
@ -137,4 +137,4 @@ protected:
|
|||
void no_incremental_check();
|
||||
};
|
||||
|
||||
#endif // CPROVER_CBMC_CBMC_SOLVERS_H
|
||||
#endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
|
|
@ -34,8 +34,10 @@ target_link_libraries(
|
|||
testing-utils
|
||||
ansi-c
|
||||
solvers
|
||||
goto-checker
|
||||
goto-programs
|
||||
goto-instrument-lib
|
||||
goto-symex
|
||||
cbmc-lib
|
||||
json-symtab-language
|
||||
)
|
||||
|
|
|
@ -86,7 +86,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
|
|||
../src/cbmc/bmc_cover$(OBJEXT) \
|
||||
../src/cbmc/cbmc_languages$(OBJEXT) \
|
||||
../src/cbmc/cbmc_parse_options$(OBJEXT) \
|
||||
../src/cbmc/cbmc_solvers$(OBJEXT) \
|
||||
../src/cbmc/counterexample_beautification$(OBJEXT) \
|
||||
../src/cbmc/fault_localization$(OBJEXT) \
|
||||
../src/cbmc/symex_bmc$(OBJEXT) \
|
||||
|
@ -119,6 +118,7 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \
|
|||
../src/linking/linking$(LIBEXT) \
|
||||
../src/util/util$(LIBEXT) \
|
||||
../src/big-int/big-int$(LIBEXT) \
|
||||
../src/goto-checker/goto-checker$(LIBEXT) \
|
||||
../src/goto-programs/goto-programs$(LIBEXT) \
|
||||
../src/pointer-analysis/pointer-analysis$(LIBEXT) \
|
||||
../src/langapi/langapi$(LIBEXT) \
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
ansi-c
|
||||
cbmc
|
||||
cpp
|
||||
goto-checker
|
||||
goto-instrument
|
||||
goto-programs
|
||||
goto-symex
|
||||
|
|
|
@ -18,7 +18,8 @@ Author: Kareem Khazem <karkhaz@karkhaz.com>, 2018
|
|||
|
||||
#include <cbmc/bmc.h>
|
||||
#include <cbmc/cbmc_parse_options.h>
|
||||
#include <cbmc/cbmc_solvers.h>
|
||||
|
||||
#include <goto-checker/solver_factory.h>
|
||||
|
||||
#include <langapi/language_ui.h>
|
||||
#include <langapi/mode.h>
|
||||
|
@ -376,9 +377,8 @@ void _check_with_strategy(
|
|||
ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh);
|
||||
REQUIRE(ret == -1);
|
||||
|
||||
cbmc_solverst initial_solvers(opts, gm.get_symbol_table(), mh, false);
|
||||
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver =
|
||||
initial_solvers.get_solver();
|
||||
solver_factoryt solvers(opts, gm.get_symbol_table(), mh, false);
|
||||
std::unique_ptr<solver_factoryt::solvert> cbmc_solver = solvers.get_solver();
|
||||
prop_convt &initial_pc = cbmc_solver->prop_conv();
|
||||
std::function<bool(void)> callback = []() { return false; };
|
||||
|
||||
|
@ -403,7 +403,7 @@ void _check_with_strategy(
|
|||
|
||||
while(!worklist->empty())
|
||||
{
|
||||
cbmc_solverst solvers(opts, gm.get_symbol_table(), mh, false);
|
||||
solver_factoryt solvers(opts, gm.get_symbol_table(), mh, false);
|
||||
cbmc_solver = solvers.get_solver();
|
||||
prop_convt &pc = cbmc_solver->prop_conv();
|
||||
path_storaget::patht &resume = worklist->peek();
|
||||
|
|
Loading…
Reference in New Issue