about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-07-25 22:22:55 +0100
committerMartinNowack <martin.nowack@gmail.com>2019-07-30 21:40:30 +0100
commit9b3c98850572f0729afe97ffde16d05a7e6e691b (patch)
tree886a893600961d6d1287ea716f5c776597a65fc9 /lib/Solver
parentd1f714b72da1674f6f784a8a1b2a6179f103b723 (diff)
downloadklee-9b3c98850572f0729afe97ffde16d05a7e6e691b.tar.gz
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.
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/AssignmentValidatingSolver.cpp6


-rw-r--r--lib/Solver/CachingSolver.cpp4


-rw-r--r--lib/Solver/CexCachingSolver.cpp10


-rw-r--r--lib/Solver/FastCexSolver.cpp20


-rw-r--r--lib/Solver/IncompleteSolver.cpp2


-rw-r--r--lib/Solver/IndependentSolver.cpp16


-rw-r--r--lib/Solver/KQueryLoggingSolver.cpp6


-rw-r--r--lib/Solver/MetaSMTBuilder.h18


-rw-r--r--lib/Solver/MetaSMTSolver.cpp13


-rw-r--r--lib/Solver/SMTLIBLoggingSolver.cpp3


-rw-r--r--lib/Solver/STPBuilder.cpp4


-rw-r--r--lib/Solver/STPBuilder.h4


-rw-r--r--lib/Solver/STPSolver.cpp12


-rw-r--r--lib/Solver/Solver.cpp3


-rw-r--r--lib/Solver/ValidatingSolver.cpp4


-rw-r--r--lib/Solver/Z3Builder.cpp2


-rw-r--r--lib/Solver/Z3Builder.h5


-rw-r--r--lib/Solver/Z3Solver.cpp9


18 files changed, 72 insertions, 69 deletions
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 <vector>
 
 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 <sstream>
+
 #include <cassert>
 #include <map>
+#include <sstream>
 #include <vector>
 
 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 <list>
 #include <map>
-#include <vector>
 #include <ostream>
-#include <list>
+#include <vector>
 
 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 <errno.h>
-#include <unistd.h>
 #include <signal.h>
-#include <sys/wait.h>
 #include <sys/ipc.h>
 #include <sys/shm.h>
+#include <sys/wait.h>
+#include <unistd.h>
 
 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 <vector>
 
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 <csignal>
-#include <unistd.h>
 #include <sys/ipc.h>
 #include <sys/shm.h>
 #include <sys/wait.h>
+#include <unistd.h>
 
 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 <vector>
 
 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 <unordered_map>
 #include <z3.h>
 
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"
 

 

generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-21 18:12:58 +0000