From e1f055b1785fd7f23fc4d30eeb0276278892ed20 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 15 Aug 2019 22:32:39 +0100 Subject: Moved ConstructSolverChain.cpp to the Solver library. --- lib/Basic/CMakeLists.txt | 10 ----- lib/Basic/ConstructSolverChain.cpp | 77 ------------------------------------- lib/Solver/CMakeLists.txt | 1 + lib/Solver/ConstructSolverChain.cpp | 77 +++++++++++++++++++++++++++++++++++++ 4 files changed, 78 insertions(+), 87 deletions(-) delete mode 100644 lib/Basic/ConstructSolverChain.cpp create mode 100644 lib/Solver/ConstructSolverChain.cpp (limited to 'lib') diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt index 78890ea6..d156116f 100644 --- a/lib/Basic/CMakeLists.txt +++ b/lib/Basic/CMakeLists.txt @@ -7,7 +7,6 @@ # #===------------------------------------------------------------------------===# klee_add_component(kleeBasic - ConstructSolverChain.cpp KTest.cpp Statistics.cpp ) @@ -17,12 +16,3 @@ set(LLVM_COMPONENTS klee_get_llvm_libs(LLVM_LIBS ${LLVM_COMPONENTS}) target_link_libraries(kleeBasic PUBLIC ${LLVM_LIBS}) - -target_link_libraries(kleeBasic PRIVATE - # FIXME: THIS IS STUPID. - # `ConstructSolverChain.cpp` should be in - # `kleaverSolver` not in in `kleeBasic`. - # We are creating a circular dependency because - # of this because `kleaverSolver` depends on `kleeBasic`. - kleaverSolver -) diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp deleted file mode 100644 index 39e0e824..00000000 --- a/lib/Basic/ConstructSolverChain.cpp +++ /dev/null @@ -1,77 +0,0 @@ -//===-- ConstructSolverChain.cpp ------------------------------------++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -/* - * This file groups declarations that are common to both KLEE and Kleaver. - */ -#include "klee/Common.h" -#include "klee/SolverCmdLine.h" -#include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Internal/System/Time.h" -#include "llvm/Support/raw_ostream.h" - - -namespace klee { -Solver *constructSolverChain(Solver *coreSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryKQueryLogPath, - std::string baseSolverQueryKQueryLogPath) { - Solver *solver = coreSolver; - const time::Span minQueryTimeToLog(MinQueryTimeToLog); - - if (QueryLoggingOptions.isSet(SOLVER_KQUERY)) { - solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); - klee_message("Logging queries that reach solver in .kquery format to %s\n", - baseSolverQueryKQueryLogPath.c_str()); - } - - if (QueryLoggingOptions.isSet(SOLVER_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); - klee_message("Logging queries that reach solver in .smt2 format to %s\n", - baseSolverQuerySMT2LogPath.c_str()); - } - - if (UseAssignmentValidatingSolver) - solver = createAssignmentValidatingSolver(solver); - - if (UseFastCexSolver) - solver = createFastCexSolver(solver); - - if (UseCexCache) - solver = createCexCachingSolver(solver); - - if (UseBranchCache) - solver = createCachingSolver(solver); - - if (UseIndependentSolver) - solver = createIndependentSolver(solver); - - if (DebugValidateSolver) - solver = createValidatingSolver(solver, coreSolver); - - if (QueryLoggingOptions.isSet(ALL_KQUERY)) { - solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); - klee_message("Logging all queries in .kquery format to %s\n", - queryKQueryLogPath.c_str()); - } - - if (QueryLoggingOptions.isSet(ALL_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); - klee_message("Logging all queries in .smt2 format to %s\n", - querySMT2LogPath.c_str()); - } - if (DebugCrossCheckCoreSolverWith != NO_SOLVER) { - Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith); - solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver); - } - - return solver; -} -} diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index f4cfa738..31c8302a 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -11,6 +11,7 @@ klee_add_component(kleaverSolver CachingSolver.cpp CexCachingSolver.cpp ConstantDivision.cpp + ConstructSolverChain.cpp CoreSolver.cpp DummySolver.cpp FastCexSolver.cpp diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp new file mode 100644 index 00000000..39e0e824 --- /dev/null +++ b/lib/Solver/ConstructSolverChain.cpp @@ -0,0 +1,77 @@ +//===-- ConstructSolverChain.cpp ------------------------------------++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +/* + * This file groups declarations that are common to both KLEE and Kleaver. + */ +#include "klee/Common.h" +#include "klee/SolverCmdLine.h" +#include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/System/Time.h" +#include "llvm/Support/raw_ostream.h" + + +namespace klee { +Solver *constructSolverChain(Solver *coreSolver, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, + std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath) { + Solver *solver = coreSolver; + const time::Span minQueryTimeToLog(MinQueryTimeToLog); + + if (QueryLoggingOptions.isSet(SOLVER_KQUERY)) { + solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); + klee_message("Logging queries that reach solver in .kquery format to %s\n", + baseSolverQueryKQueryLogPath.c_str()); + } + + if (QueryLoggingOptions.isSet(SOLVER_SMTLIB)) { + solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); + klee_message("Logging queries that reach solver in .smt2 format to %s\n", + baseSolverQuerySMT2LogPath.c_str()); + } + + if (UseAssignmentValidatingSolver) + solver = createAssignmentValidatingSolver(solver); + + if (UseFastCexSolver) + solver = createFastCexSolver(solver); + + if (UseCexCache) + solver = createCexCachingSolver(solver); + + if (UseBranchCache) + solver = createCachingSolver(solver); + + if (UseIndependentSolver) + solver = createIndependentSolver(solver); + + if (DebugValidateSolver) + solver = createValidatingSolver(solver, coreSolver); + + if (QueryLoggingOptions.isSet(ALL_KQUERY)) { + solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); + klee_message("Logging all queries in .kquery format to %s\n", + queryKQueryLogPath.c_str()); + } + + if (QueryLoggingOptions.isSet(ALL_SMTLIB)) { + solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); + klee_message("Logging all queries in .smt2 format to %s\n", + querySMT2LogPath.c_str()); + } + if (DebugCrossCheckCoreSolverWith != NO_SOLVER) { + Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith); + solver = createValidatingSolver(/*s=*/solver, /*oracle=*/oracleSolver); + } + + return solver; +} +} -- cgit 1.4.1