From 9b3c98850572f0729afe97ffde16d05a7e6e691b Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 25 Jul 2019 22:22:55 +0100 Subject: Consolidated Expr-related include files into a single include/klee/Expr directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE. --- lib/Solver/AssignmentValidatingSolver.cpp | 6 ++++-- lib/Solver/CachingSolver.cpp | 4 ++-- lib/Solver/CexCachingSolver.cpp | 10 +++++----- lib/Solver/FastCexSolver.cpp | 20 +++++++++----------- lib/Solver/IncompleteSolver.cpp | 2 +- lib/Solver/IndependentSolver.cpp | 16 ++++++++-------- lib/Solver/KQueryLoggingSolver.cpp | 6 ++---- lib/Solver/MetaSMTBuilder.h | 18 ++++++------------ lib/Solver/MetaSMTSolver.cpp | 13 +++++++------ lib/Solver/SMTLIBLoggingSolver.cpp | 3 ++- lib/Solver/STPBuilder.cpp | 4 ++-- lib/Solver/STPBuilder.h | 4 ++-- lib/Solver/STPSolver.cpp | 12 +++++++----- lib/Solver/Solver.cpp | 3 ++- lib/Solver/ValidatingSolver.cpp | 4 +++- lib/Solver/Z3Builder.cpp | 2 +- lib/Solver/Z3Builder.h | 5 +++-- lib/Solver/Z3Solver.cpp | 9 ++++++--- 18 files changed, 72 insertions(+), 69 deletions(-) (limited to 'lib/Solver') diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index 82702dbf..b75f982a 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -6,10 +6,12 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/util/Assignment.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Assignment.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" + #include namespace klee { diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index a6ca93ac..2eedc616 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -10,8 +10,8 @@ #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" #include "klee/IncompleteSolver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index d2e080d9..5c181dc3 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -9,17 +9,17 @@ #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/Internal/ADT/MapOfSets.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/SolverImpl.h" #include "klee/SolverStats.h" #include "klee/TimerStatIncrementer.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" -#include "klee/util/ExprVisitor.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 5ea6c1d4..9f493cd1 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -10,27 +10,25 @@ #define DEBUG_TYPE "cex-solver" #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprEvaluator.h" +#include "klee/Expr/ExprRangeEvaluator.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/IncompleteSolver.h" -#include "klee/util/ExprEvaluator.h" -#include "klee/util/ExprRangeEvaluator.h" -#include "klee/util/ExprVisitor.h" -// FIXME: Use APInt. #include "klee/Internal/Support/Debug.h" -#include "klee/Internal/Support/IntEvaluation.h" +#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt #include "llvm/Support/raw_ostream.h" -#include + #include #include +#include #include using namespace klee; -/***/ - - // Hacker's Delight, pgs 58-63 +// Hacker's Delight, pgs 58-63 static uint64_t minOR(uint64_t a, uint64_t b, uint64_t c, uint64_t d) { uint64_t temp, m = ((uint64_t) 1)<<63; diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index 72fe2a95..e19a71e1 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -9,7 +9,7 @@ #include "klee/IncompleteSolver.h" -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" using namespace klee; using namespace llvm; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 447e5575..12017e5c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -10,19 +10,19 @@ #define DEBUG_TYPE "independent-solver" #include "klee/Solver.h" -#include "klee/Expr.h" -#include "klee/Constraints.h" -#include "klee/SolverImpl.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/Debug.h" - -#include "klee/util/ExprUtil.h" -#include "klee/util/Assignment.h" +#include "klee/SolverImpl.h" #include "llvm/Support/raw_ostream.h" + +#include #include -#include #include -#include +#include using namespace klee; using namespace llvm; diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp index 0c2ac6dd..27e8ad0b 100644 --- a/lib/Solver/KQueryLoggingSolver.cpp +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -9,14 +9,12 @@ #include "QueryLoggingSolver.h" -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprPPrinter.h" #include "klee/Internal/System/Time.h" using namespace klee; -/// - class KQueryLoggingSolver : public QueryLoggingSolver { private : diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index ffe4608d..3112495d 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -7,23 +7,17 @@ // //===----------------------------------------------------------------------===// -/* - * MetaSMTBuilder.h - * - * Created on: 8 Aug 2012 - * Author: hpalikar - */ - #ifndef KLEE_METASMTBUILDER_H #define KLEE_METASMTBUILDER_H -#include "klee/Config/config.h" -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ArrayExprHash.h" -#include "klee/util/ExprHashMap.h" #include "ConstantDivision.h" +#include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/ExprPPrinter.h" + #ifdef ENABLE_METASMT #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index dfa78e42..c4ff1f13 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -7,16 +7,17 @@ // //===----------------------------------------------------------------------===// #include "klee/Config/config.h" -#ifdef ENABLE_METASMT +#ifdef ENABLE_METASMT #include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/ErrorHandling.h" @@ -51,11 +52,11 @@ #endif #include -#include #include -#include #include #include +#include +#include static unsigned char *shared_memory_ptr; static int shared_memory_id = 0; diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index f734ac38..bfea5c1b 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -8,7 +8,8 @@ //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" -#include "klee/util/ExprSMTLIBPrinter.h" + +#include "klee/Expr/ExprSMTLIBPrinter.h" using namespace klee; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 0bd5084a..645c8989 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -10,10 +10,10 @@ #ifdef ENABLE_STP #include "STPBuilder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Solver.h" -#include "klee/util/Bits.h" #include "klee/SolverStats.h" +#include "klee/util/Bits.h" #include "ConstantDivision.h" diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index cb163384..814046fa 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -10,9 +10,9 @@ #ifndef KLEE_STPBUILDER_H #define KLEE_STPBUILDER_H -#include "klee/util/ExprHashMap.h" -#include "klee/util/ArrayExprHash.h" #include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" #include diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index e8b9222f..eb46b6db 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -9,23 +9,25 @@ #include "klee/Config/config.h" #ifdef ENABLE_STP + #include "STPBuilder.h" #include "STPSolver.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/SolverImpl.h" -#include "klee/Internal/Support/ErrorHandling.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" #include -#include #include #include #include +#include namespace { diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 4f7458c5..6c7361dc 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -8,8 +8,9 @@ //===----------------------------------------------------------------------===// #include "klee/Solver.h" + +#include "klee/Expr/Constraints.h" #include "klee/SolverImpl.h" -#include "klee/Constraints.h" using namespace klee; diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 40a7c9e0..71e6834e 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -6,9 +6,11 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" + #include namespace klee { diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 06b995ae..07a7b681 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -10,7 +10,7 @@ #ifdef ENABLE_Z3 #include "Z3Builder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverStats.h" diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index efbf4f9a..4501ecbd 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -11,8 +11,9 @@ #define KLEE_Z3BUILDER_H #include "klee/Config/config.h" -#include "klee/util/ArrayExprHash.h" -#include "klee/util/ExprHashMap.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" + #include #include diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 74fee290..cfcb77e7 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -6,19 +6,22 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// + #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/FileHandling.h" #include "klee/OptionCategories.h" #ifdef ENABLE_Z3 + #include "Z3Solver.h" #include "Z3Builder.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -- cgit 1.4.1