Skip to content

Commit df5dd7a

Browse files
peterschrammelpeterschrammel
committed
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.
1 parent 58d440a commit df5dd7a

22 files changed

+84
-42
lines changed

‎CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ set_target_properties(
5858
goto-analyzer-lib
5959
goto-cc
6060
goto-cc-lib
61+
goto-checker
6162
goto-diff
6263
goto-diff-lib
6364
goto-instrument

‎jbmc/src/jbmc/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ target_link_libraries(jbmc-lib
1212
ansi-c
1313
big-int
1414
cbmc-lib
15+
goto-checker
1516
goto-instrument-lib
1617
goto-programs
1718
goto-symex

‎jbmc/src/jbmc/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
66
../java_bytecode/java_bytecode$(LIBEXT) \
77
../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
88
../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
9+
../$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
910
../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
1011
../$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
1112
../$(CPROVER_DIR)/src/pointer-analysis/value_set$(OBJEXT) \
@@ -40,7 +41,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
4041
../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
4142
../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
4243
../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
43-
../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
4444
../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
4545
../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
4646
../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \

‎jbmc/src/jbmc/module_dependencies.txt

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
analyses
22
ansi-c # should go away
3-
cbmc # bmc.h
3+
cbmc # bmc.h - will go away
4+
goto-checker
45
goto-instrument
56
goto-programs
67
goto-symex

‎jbmc/unit/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,9 @@ target_link_libraries(java-unit
2323
testing-utils
2424
ansi-c
2525
solvers
26+
goto-checker
2627
goto-programs
28+
goto-symex
2729
goto-instrument-lib
2830
cbmc-lib
2931
json-symtab-language

‎jbmc/unit/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,6 @@ BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
8686
$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
8787
$(CPROVER_DIR)/src/cbmc/cbmc_languages$(OBJEXT) \
8888
$(CPROVER_DIR)/src/cbmc/cbmc_parse_options$(OBJEXT) \
89-
$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
9089
$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
9190
$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
9291
$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
@@ -114,6 +113,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
114113
$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
115114
$(CPROVER_DIR)/src/util/util$(LIBEXT) \
116115
$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
116+
$(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \
117117
$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
118118
$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
119119
$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \

‎src/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ add_subdirectory(ansi-c)
8585
add_subdirectory(assembler)
8686
add_subdirectory(big-int)
8787
add_subdirectory(cpp)
88+
add_subdirectory(goto-checker)
8889
add_subdirectory(goto-programs)
8990
add_subdirectory(goto-symex)
9091
add_subdirectory(jsil)

‎src/Makefile

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ DIRS = analyses \
66
cpp \
77
goto-analyzer \
88
goto-cc \
9+
goto-checker \
910
goto-diff \
1011
goto-instrument \
1112
goto-programs \
@@ -49,9 +50,11 @@ solvers.dir: util.dir langapi.dir
4950
goto-instrument.dir: languages goto-programs.dir pointer-analysis.dir \
5051
goto-symex.dir linking.dir analyses.dir solvers.dir
5152

53+
goto-checker.dir: solvers.dir goto-symex.dir goto-programs.dir
54+
5255
cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
5356
pointer-analysis.dir goto-programs.dir linking.dir \
54-
goto-instrument.dir
57+
goto-instrument.dir goto-checker.dir
5558

5659
goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
5760
goto-instrument.dir

‎src/cbmc/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ target_link_libraries(cbmc-lib
1313
assembler
1414
big-int
1515
cpp
16+
goto-checker
1617
goto-instrument-lib
1718
goto-programs
1819
goto-symex

‎src/cbmc/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ SRC = all_properties.cpp \
44
cbmc_languages.cpp \
55
cbmc_main.cpp \
66
cbmc_parse_options.cpp \
7-
cbmc_solvers.cpp \
87
counterexample_beautification.cpp \
98
fault_localization.cpp \
109
symex_bmc.cpp \
@@ -18,6 +17,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
1817
../json-symtab-language/json-symtab-language$(LIBEXT) \
1918
../linking/linking$(LIBEXT) \
2019
../big-int/big-int$(LIBEXT) \
20+
../goto-checker/goto-checker$(LIBEXT) \
2121
../goto-programs/goto-programs$(LIBEXT) \
2222
../goto-symex/goto-symex$(LIBEXT) \
2323
../pointer-analysis/value_set$(OBJEXT) \

‎src/cbmc/bmc.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,8 @@ Author: Daniel Kroening, [email protected]
3232

3333
#include <linking/static_lifetime_init.h>
3434

35-
#include "cbmc_solvers.h"
35+
#include <goto-checker/solver_factory.h>
36+
3637
#include "counterexample_beautification.h"
3738
#include "fault_localization.h"
3839

@@ -519,12 +520,12 @@ int bmct::do_language_agnostic_bmc(
519520
try
520521
{
521522
{
522-
cbmc_solverst solvers(
523+
solver_factoryt solvers(
523524
opts,
524525
symbol_table,
525526
ui,
526527
ui.get_ui() == ui_message_handlert::uit::XML_UI);
527-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
528+
std::unique_ptr<solver_factoryt::solvert> cbmc_solver;
528529
cbmc_solver = solvers.get_solver();
529530
prop_convt &pc = cbmc_solver->prop_conv();
530531
bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex);
@@ -566,13 +567,13 @@ int bmct::do_language_agnostic_bmc(
566567

567568
while(!worklist->empty())
568569
{
569-
cbmc_solverst solvers(
570+
solver_factoryt solvers(
570571
opts,
571572
symbol_table,
572573
ui,
573574
ui.get_ui() == ui_message_handlert::uit::XML_UI);
574-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solver;
575-
cbmc_solver = solvers.get_solver();
575+
std::unique_ptr<solver_factoryt::solvert> cbmc_solver =
576+
solvers.get_solver();
576577
prop_convt &pc = cbmc_solver->prop_conv();
577578
path_storaget::patht &resume = worklist->peek();
578579
path_explorert pe(

‎src/cbmc/cbmc_parse_options.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,14 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <analyses/goto_check.h>
2626

27+
#include <goto-checker/solver_factory.h>
28+
2729
#include <goto-programs/goto_trace.h>
2830

2931
#include <solvers/refinement/string_refinement.h>
3032

3133
#include "bmc.h"
3234
#include "xml_interface.h"
33-
#include "cbmc_solvers.h"
3435

3536
class bmct;
3637
class goto_functionst;

‎src/cbmc/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
analyses
22
ansi-c
33
cpp
4+
goto-checker
45
goto-instrument
56
goto-programs
67
goto-symex

‎src/goto-checker/CMakeLists.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
file(GLOB_RECURSE sources "*.cpp" "*.h")
2+
add_library(goto-checker ${sources})
3+
4+
generic_includes(goto-checker)
5+
6+
target_link_libraries(goto-checker goto-programs goto-symex solvers util)

‎src/goto-checker/Makefile

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
SRC = solver_factory.cpp \
2+
# Empty last line
3+
4+
INCLUDES= -I ..
5+
6+
include ../config.inc
7+
include ../common
8+
9+
CLEANFILES = goto-checker$(LIBEXT)
10+
11+
all: goto-checker$(LIBEXT)
12+
13+
###############################################################################
14+
15+
goto-checker$(LIBEXT): $(OBJ)
16+
$(LINKLIB)

‎src/goto-checker/module_dependencies.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
goto-checker
2+
goto-programs
3+
goto-symex
4+
solvers
5+
util

‎src/cbmc/cbmc_solvers.cpp renamed to ‎src/goto-checker/solver_factory.cpp

Lines changed: 14 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
/*******************************************************************\
22
3-
Module: Solvers for VCs Generated by Symbolic Execution of ANSI-C
3+
Module: Solver Factory
44
5-
Author: Daniel Kroening, [email protected]
5+
Author: Daniel Kroening, Peter Schrammel
66
77
\*******************************************************************/
88

99
/// \file
10-
/// Solvers for VCs Generated by Symbolic Execution of ANSI-C
10+
/// Solver Factory
1111

12-
#include "cbmc_solvers.h"
12+
#include "solver_factory.h"
1313

1414
#include <fstream>
1515
#include <iostream>
@@ -28,11 +28,9 @@ Author: Daniel Kroening, [email protected]
2828
#include <solvers/sat/satcheck.h>
2929
#include <solvers/smt2/smt2_dec.h>
3030

31-
#include "counterexample_beautification.h"
32-
3331
/// Uses the options to pick an SMT 2.0 solver
3432
/// \return An smt2_dect::solvert giving the solver to use.
35-
smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
33+
smt2_dect::solvert solver_factoryt::get_smt2_solver_type() const
3634
{
3735
// we shouldn't get here if this option isn't set
3836
PRECONDITION(options.get_bool_option("smt2"));
@@ -59,7 +57,7 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
5957
return s;
6058
}
6159

62-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
60+
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
6361
{
6462
auto solver=util_make_unique<solvert>();
6563

@@ -88,7 +86,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
8886
return solver;
8987
}
9088

91-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
89+
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_dimacs()
9290
{
9391
no_beautification();
9492
no_incremental_check();
@@ -102,7 +100,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
102100
return util_make_unique<solvert>(std::move(bv_dimacs), std::move(prop));
103101
}
104102

105-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
103+
std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_bv_refinement()
106104
{
107105
std::unique_ptr<propt> prop=[this]() -> std::unique_ptr<propt>
108106
{
@@ -138,7 +136,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
138136
/// the string refinement adds to the bit vector refinement specifications for
139137
/// functions from the Java string library
140138
/// \return a solver for cbmc
141-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
139+
std::unique_ptr<solver_factoryt::solvert>
140+
solver_factoryt::get_string_refinement()
142141
{
143142
string_refinementt::infot info;
144143
info.ns=&ns;
@@ -157,8 +156,8 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
157156
util_make_unique<string_refinementt>(info), std::move(prop));
158157
}
159158

160-
std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
161-
smt2_dect::solvert solver)
159+
std::unique_ptr<solver_factoryt::solvert>
160+
solver_factoryt::get_smt2(smt2_dect::solvert solver)
162161
{
163162
no_beautification();
164163

@@ -234,7 +233,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
234233
}
235234
}
236235

237-
void cbmc_solverst::no_beautification()
236+
void solver_factoryt::no_beautification()
238237
{
239238
if(options.get_bool_option("beautify"))
240239
{
@@ -243,7 +242,7 @@ void cbmc_solverst::no_beautification()
243242
}
244243
}
245244

246-
void cbmc_solverst::no_incremental_check()
245+
void solver_factoryt::no_incremental_check()
247246
{
248247
const bool all_properties = options.get_bool_option("all-properties");
249248
const bool cover = options.is_set("cover");

‎src/cbmc/cbmc_solvers.h renamed to ‎src/goto-checker/solver_factory.h

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
/*******************************************************************\
22
3-
Module: Bounded Model Checking for ANSI-C + HDL
3+
Module: Solver Factory
44
5-
Author: Daniel Kroening, [email protected]
5+
Author: Daniel Kroening, Peter Schrammel
66
77
\*******************************************************************/
88

99
/// \file
10-
/// Bounded Model Checking for ANSI-C + HDL
10+
/// Solver Factory
1111

12-
#ifndef CPROVER_CBMC_CBMC_SOLVERS_H
13-
#define CPROVER_CBMC_CBMC_SOLVERS_H
12+
#ifndef CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
13+
#define CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H
1414

1515
#include <list>
1616
#include <map>
@@ -25,10 +25,10 @@ Author: Daniel Kroening, [email protected]
2525
#include <solvers/smt2/smt2_dec.h>
2626
#include <goto-symex/symex_target_equation.h>
2727

28-
class cbmc_solverst
28+
class solver_factoryt
2929
{
3030
public:
31-
cbmc_solverst(
31+
solver_factoryt(
3232
const optionst &_options,
3333
const symbol_tablet &_symbol_table,
3434
message_handlert &_message_handler,
@@ -113,7 +113,7 @@ class cbmc_solverst
113113
return get_default();
114114
}
115115

116-
virtual ~cbmc_solverst()
116+
virtual ~solver_factoryt()
117117
{
118118
}
119119

@@ -137,4 +137,4 @@ class cbmc_solverst
137137
void no_incremental_check();
138138
};
139139

140-
#endif // CPROVER_CBMC_CBMC_SOLVERS_H
140+
#endif // CPROVER_GOTO_CHECKER_SOLVER_FACTORY_H

‎unit/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,10 @@ target_link_libraries(
3434
testing-utils
3535
ansi-c
3636
solvers
37+
goto-checker
3738
goto-programs
3839
goto-instrument-lib
40+
goto-symex
3941
cbmc-lib
4042
json-symtab-language
4143
)

‎unit/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,6 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \
8686
../src/cbmc/bmc_cover$(OBJEXT) \
8787
../src/cbmc/cbmc_languages$(OBJEXT) \
8888
../src/cbmc/cbmc_parse_options$(OBJEXT) \
89-
../src/cbmc/cbmc_solvers$(OBJEXT) \
9089
../src/cbmc/counterexample_beautification$(OBJEXT) \
9190
../src/cbmc/fault_localization$(OBJEXT) \
9291
../src/cbmc/symex_bmc$(OBJEXT) \
@@ -119,6 +118,7 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \
119118
../src/linking/linking$(LIBEXT) \
120119
../src/util/util$(LIBEXT) \
121120
../src/big-int/big-int$(LIBEXT) \
121+
../src/goto-checker/goto-checker$(LIBEXT) \
122122
../src/goto-programs/goto-programs$(LIBEXT) \
123123
../src/pointer-analysis/pointer-analysis$(LIBEXT) \
124124
../src/langapi/langapi$(LIBEXT) \

‎unit/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
ansi-c
22
cbmc
33
cpp
4+
goto-checker
45
goto-instrument
56
goto-programs
67
goto-symex

0 commit comments

Comments
 (0)