From b8a74d8593e063ac9168ce273cbf1691aaa360cd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 18 Dec 2015 13:16:56 +0000 Subject: Move lib/Solver/SolverStats.h -> include/klee/SolverStats.h so that it is possible to ``#include "klee/util/ArrayExprHash.h"`` --- include/klee/SolverStats.h | 38 ++++++++++++++++++++++++++++++++++++++ include/klee/util/ArrayExprHash.h | 2 +- lib/Core/Executor.cpp | 2 +- lib/Core/StatsTracker.cpp | 2 +- lib/Solver/CachingSolver.cpp | 2 +- lib/Solver/CexCachingSolver.cpp | 2 +- lib/Solver/STPBuilder.cpp | 2 +- lib/Solver/Solver.cpp | 2 +- lib/Solver/SolverStats.cpp | 2 +- lib/Solver/SolverStats.h | 38 -------------------------------------- 10 files changed, 46 insertions(+), 46 deletions(-) create mode 100644 include/klee/SolverStats.h delete mode 100644 lib/Solver/SolverStats.h diff --git a/include/klee/SolverStats.h b/include/klee/SolverStats.h new file mode 100644 index 00000000..a38c9826 --- /dev/null +++ b/include/klee/SolverStats.h @@ -0,0 +1,38 @@ +//===-- SolverStats.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_SOLVERSTATS_H +#define KLEE_SOLVERSTATS_H + +#include "klee/Statistic.h" + +namespace klee { +namespace stats { + + extern Statistic cexCacheTime; + extern Statistic queries; + extern Statistic queriesInvalid; + extern Statistic queriesValid; + extern Statistic queryCacheHits; + extern Statistic queryCacheMisses; + extern Statistic queryCexCacheHits; + extern Statistic queryCexCacheMisses; + extern Statistic queryConstructTime; + extern Statistic queryConstructs; + extern Statistic queryCounterexamples; + extern Statistic queryTime; + +#ifdef DEBUG + extern Statistic arrayHashTime; +#endif + +} +} + +#endif diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h index da3b1d2b..23211a70 100644 --- a/include/klee/util/ArrayExprHash.h +++ b/include/klee/util/ArrayExprHash.h @@ -12,7 +12,7 @@ #include "klee/Expr.h" #include "klee/TimerStatIncrementer.h" -#include "SolverStats.h" +#include "klee/SolverStats.h" #include diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4a21be3e..9211f485 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -23,7 +23,6 @@ #include "UserSearcher.h" #include "ExecutorTimerInfo.h" -#include "../Solver/SolverStats.h" #include "klee/ExecutionState.h" #include "klee/Expr.h" @@ -47,6 +46,7 @@ #include "klee/Internal/Support/FloatEvaluation.h" #include "klee/Internal/System/Time.h" #include "klee/Internal/System/MemoryUsage.h" +#include "klee/SolverStats.h" #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Function.h" diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 4633a5c5..2e107fb3 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -18,13 +18,13 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/SolverStats.h" #include "CallPathManager.h" #include "CoreStats.h" #include "Executor.h" #include "MemoryManager.h" #include "UserSearcher.h" -#include "../Solver/SolverStats.h" #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2) #include "llvm/IR/BasicBlock.h" diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index cfe08a96..1a6dce52 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -15,7 +15,7 @@ #include "klee/IncompleteSolver.h" #include "klee/SolverImpl.h" -#include "SolverStats.h" +#include "klee/SolverStats.h" #include #ifdef _LIBCPP_VERSION diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index fb07a6ec..8627b2ac 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -18,7 +18,7 @@ #include "klee/util/ExprVisitor.h" #include "klee/Internal/ADT/MapOfSets.h" -#include "SolverStats.h" +#include "klee/SolverStats.h" #include "klee/Internal/Support/ErrorHandling.h" diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 4bd0145f..2f51c2b9 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -12,9 +12,9 @@ #include "klee/Expr.h" #include "klee/Solver.h" #include "klee/util/Bits.h" +#include "klee/SolverStats.h" #include "ConstantDivision.h" -#include "SolverStats.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 341ca17c..6f4bbc5b 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -10,7 +10,6 @@ #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "SolverStats.h" #include "STPBuilder.h" #include "MetaSMTBuilder.h" @@ -23,6 +22,7 @@ #include "klee/Internal/Support/Timer.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/CommandLine.h" +#include "klee/SolverStats.h" #define vc_bvBoolExtract IAMTHESPAWNOFSATAN diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index 9d6963cf..4b9c69c8 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "SolverStats.h" +#include "klee/SolverStats.h" using namespace klee; diff --git a/lib/Solver/SolverStats.h b/lib/Solver/SolverStats.h deleted file mode 100644 index a38c9826..00000000 --- a/lib/Solver/SolverStats.h +++ /dev/null @@ -1,38 +0,0 @@ -//===-- SolverStats.h -------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_SOLVERSTATS_H -#define KLEE_SOLVERSTATS_H - -#include "klee/Statistic.h" - -namespace klee { -namespace stats { - - extern Statistic cexCacheTime; - extern Statistic queries; - extern Statistic queriesInvalid; - extern Statistic queriesValid; - extern Statistic queryCacheHits; - extern Statistic queryCacheMisses; - extern Statistic queryCexCacheHits; - extern Statistic queryCexCacheMisses; - extern Statistic queryConstructTime; - extern Statistic queryConstructs; - extern Statistic queryCounterexamples; - extern Statistic queryTime; - -#ifdef DEBUG - extern Statistic arrayHashTime; -#endif - -} -} - -#endif -- cgit 1.4.1 From 0dbb147725e61ccb491039100d170357567c2b46 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 18 Dec 2015 13:24:18 +0000 Subject: Fix duplication of ``klee::ArrayHashFn`` in ``include/klee/util/ArrayCache.h``. --- include/klee/util/ArrayCache.h | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/include/klee/util/ArrayCache.h b/include/klee/util/ArrayCache.h index 3dd88a11..56d69df6 100644 --- a/include/klee/util/ArrayCache.h +++ b/include/klee/util/ArrayCache.h @@ -11,6 +11,7 @@ #define KLEE_ARRAY_CACHE_H #include "klee/Expr.h" +#include "klee/util/ArrayExprHash.h" // For klee::ArrayHashFn // FIXME: Remove this hack when we switch to C++11 #ifdef _LIBCPP_VERSION @@ -26,15 +27,6 @@ namespace klee { -// FIXME: This is copied from ``klee/util/ArrayExprHash.h``. -// We can't include it here becaues the includes are messed up -// in that file. -struct EquivArrayHashFn { - unsigned operator()(const Array *array) const { - return (array ? array->hash() : 0); - } -}; - struct EquivArrayCmpFn { bool operator()(const Array *array1, const Array *array2) const { if (array1 == NULL || array2 == NULL) @@ -76,7 +68,7 @@ public: Expr::Width _range = Expr::Int8); private: - typedef unordered_set ArrayHashMap; ArrayHashMap cachedSymbolicArrays; typedef std::vector ArrayPtrVec; -- cgit 1.4.1