From fc50ab32349a4cc61980ba5b97bfa7c3961ce964 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 3 Apr 2020 19:37:11 +0100 Subject: Moved header files that were placed directly in include/klee/ into appropriate existing directories and a new directory Statistics; a few missing renames. --- include/klee/Common.h | 36 ------ include/klee/Expr/ArrayExprHash.h | 2 +- include/klee/OptionCategories.h | 29 ----- include/klee/Solver/Common.h | 36 ++++++ include/klee/Solver/SolverStats.h | 2 +- include/klee/Statistic.h | 63 ---------- include/klee/Statistics.h | 154 ------------------------- include/klee/Statistics/Statistic.h | 63 ++++++++++ include/klee/Statistics/Statistics.h | 154 +++++++++++++++++++++++++ include/klee/Statistics/TimerStatIncrementer.h | 37 ++++++ include/klee/Support/OptionCategories.h | 29 +++++ include/klee/TimerStatIncrementer.h | 37 ------ 12 files changed, 321 insertions(+), 321 deletions(-) delete mode 100644 include/klee/Common.h delete mode 100644 include/klee/OptionCategories.h create mode 100644 include/klee/Solver/Common.h delete mode 100644 include/klee/Statistic.h delete mode 100644 include/klee/Statistics.h create mode 100644 include/klee/Statistics/Statistic.h create mode 100644 include/klee/Statistics/Statistics.h create mode 100644 include/klee/Statistics/TimerStatIncrementer.h create mode 100644 include/klee/Support/OptionCategories.h delete mode 100644 include/klee/TimerStatIncrementer.h (limited to 'include') diff --git a/include/klee/Common.h b/include/klee/Common.h deleted file mode 100644 index 7b244158..00000000 --- a/include/klee/Common.h +++ /dev/null @@ -1,36 +0,0 @@ -//===-- Common.h ------------------------------------------------*- C++ -*-===// -// -// 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. - */ - -#ifndef KLEE_COMMON_H -#define KLEE_COMMON_H - -#include "klee/Solver/Solver.h" - -#include - -namespace klee { - const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2"; - const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2"; - const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery"; - const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery"; - - Solver *constructSolverChain(Solver *coreSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryKQueryLogPath, - std::string baseSolverQueryKQueryLogPath); -} - - - -#endif /* KLEE_COMMON_H */ diff --git a/include/klee/Expr/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h index f8bef491..5e9ed62b 100644 --- a/include/klee/Expr/ArrayExprHash.h +++ b/include/klee/Expr/ArrayExprHash.h @@ -11,8 +11,8 @@ #define KLEE_ARRAYEXPRHASH_H #include "klee/Expr/Expr.h" +#include "klee/Statistics/TimerStatIncrementer.h" #include "klee/Solver/SolverStats.h" -#include "klee/TimerStatIncrementer.h" #include #include diff --git a/include/klee/OptionCategories.h b/include/klee/OptionCategories.h deleted file mode 100644 index 4fb7e5cb..00000000 --- a/include/klee/OptionCategories.h +++ /dev/null @@ -1,29 +0,0 @@ -//===-- OptionCategories.h --------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -/* - * This header defines the option categories used in KLEE. - */ - -#ifndef KLEE_OPTIONCATEGORIES_H -#define KLEE_OPTIONCATEGORIES_H - -#include "llvm/Support/CommandLine.h" - -namespace klee { - extern llvm::cl::OptionCategory DebugCat; - extern llvm::cl::OptionCategory MergeCat; - extern llvm::cl::OptionCategory ModuleCat; - extern llvm::cl::OptionCategory SeedingCat; - extern llvm::cl::OptionCategory SolvingCat; - extern llvm::cl::OptionCategory TerminationCat; - extern llvm::cl::OptionCategory TestGenCat; -} - -#endif /* KLEE_OPTIONCATEGORIES_H */ diff --git a/include/klee/Solver/Common.h b/include/klee/Solver/Common.h new file mode 100644 index 00000000..7b244158 --- /dev/null +++ b/include/klee/Solver/Common.h @@ -0,0 +1,36 @@ +//===-- Common.h ------------------------------------------------*- C++ -*-===// +// +// 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. + */ + +#ifndef KLEE_COMMON_H +#define KLEE_COMMON_H + +#include "klee/Solver/Solver.h" + +#include + +namespace klee { + const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2"; + const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2"; + const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery"; + const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery"; + + Solver *constructSolverChain(Solver *coreSolver, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, + std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath); +} + + + +#endif /* KLEE_COMMON_H */ diff --git a/include/klee/Solver/SolverStats.h b/include/klee/Solver/SolverStats.h index 308ea318..fe14d9e5 100644 --- a/include/klee/Solver/SolverStats.h +++ b/include/klee/Solver/SolverStats.h @@ -10,7 +10,7 @@ #ifndef KLEE_SOLVERSTATS_H #define KLEE_SOLVERSTATS_H -#include "klee/Statistic.h" +#include "klee/Statistics/Statistic.h" namespace klee { namespace stats { diff --git a/include/klee/Statistic.h b/include/klee/Statistic.h deleted file mode 100644 index bbb67116..00000000 --- a/include/klee/Statistic.h +++ /dev/null @@ -1,63 +0,0 @@ -//===-- Statistic.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_STATISTIC_H -#define KLEE_STATISTIC_H - -#include - -namespace klee { - class Statistic; - class StatisticManager; - class StatisticRecord; - - /// Statistic - A named statistic instance. - /// - /// The Statistic class holds information about the statistic, but - /// not the actual values. Values are managed by the global - /// StatisticManager to enable transparent support for instruction - /// level and call path level statistics. - class Statistic final { - friend class StatisticManager; - friend class StatisticRecord; - - private: - std::uint32_t id; - const std::string name; - const std::string shortName; - - public: - Statistic(const std::string &name, const std::string &shortName); - ~Statistic() = default; - - /// getID - Get the unique statistic ID. - std::uint32_t getID() const { return id; } - - /// getName - Get the statistic name. - const std::string &getName() const { return name; } - - /// getShortName - Get the "short" statistic name, used in - /// callgrind output for example. - const std::string &getShortName() const { return shortName; } - - /// getValue - Get the current primary statistic value. - std::uint64_t getValue() const; - - /// operator std::uint64_t - Get the current primary statistic value. - operator std::uint64_t() const { return getValue(); } - - /// operator++ - Increment the statistic by 1. - Statistic &operator++() { return (*this += 1); } - - /// operator+= - Increment the statistic by \arg addend. - Statistic &operator+=(std::uint64_t addend); - }; -} - -#endif /* KLEE_STATISTIC_H */ diff --git a/include/klee/Statistics.h b/include/klee/Statistics.h deleted file mode 100644 index 158459cc..00000000 --- a/include/klee/Statistics.h +++ /dev/null @@ -1,154 +0,0 @@ -//===-- Statistics.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_STATISTICS_H -#define KLEE_STATISTICS_H - -#include "Statistic.h" - -#include -#include -#include - -namespace klee { - class Statistic; - class StatisticRecord { - friend class StatisticManager; - - private: - uint64_t *data; - - public: - StatisticRecord(); - StatisticRecord(const StatisticRecord &s); - ~StatisticRecord() { delete[] data; } - - void zero(); - - uint64_t getValue(const Statistic &s) const; - void incrementValue(const Statistic &s, uint64_t addend) const; - StatisticRecord &operator =(const StatisticRecord &s); - StatisticRecord &operator +=(const StatisticRecord &sr); - }; - - class StatisticManager { - private: - bool enabled; - std::vector stats; - uint64_t *globalStats; - uint64_t *indexedStats; - StatisticRecord *contextStats; - unsigned index; - - public: - StatisticManager(); - ~StatisticManager(); - - void useIndexedStats(unsigned totalIndices); - - StatisticRecord *getContext(); - void setContext(StatisticRecord *sr); /* null to reset */ - - void setIndex(unsigned i) { index = i; } - unsigned getIndex() { return index; } - unsigned getNumStatistics() { return stats.size(); } - Statistic &getStatistic(unsigned i) { return *stats[i]; } - - void registerStatistic(Statistic &s); - void incrementStatistic(Statistic &s, uint64_t addend); - uint64_t getValue(const Statistic &s) const; - void incrementIndexedValue(const Statistic &s, unsigned index, - uint64_t addend) const; - uint64_t getIndexedValue(const Statistic &s, unsigned index) const; - void setIndexedValue(const Statistic &s, unsigned index, uint64_t value); - int getStatisticID(const std::string &name) const; - Statistic *getStatisticByName(const std::string &name) const; - }; - - extern StatisticManager *theStatisticManager; - - inline void StatisticManager::incrementStatistic(Statistic &s, - uint64_t addend) { - if (enabled) { - globalStats[s.id] += addend; - if (indexedStats) { - indexedStats[index*stats.size() + s.id] += addend; - if (contextStats) - contextStats->data[s.id] += addend; - } - } - } - - inline StatisticRecord *StatisticManager::getContext() { - return contextStats; - } - inline void StatisticManager::setContext(StatisticRecord *sr) { - contextStats = sr; - } - - inline void StatisticRecord::zero() { - ::memset(data, 0, sizeof(*data)*theStatisticManager->getNumStatistics()); - } - - inline StatisticRecord::StatisticRecord() - : data(new uint64_t[theStatisticManager->getNumStatistics()]) { - zero(); - } - - inline StatisticRecord::StatisticRecord(const StatisticRecord &s) - : data(new uint64_t[theStatisticManager->getNumStatistics()]) { - ::memcpy(data, s.data, - sizeof(*data)*theStatisticManager->getNumStatistics()); - } - - inline StatisticRecord &StatisticRecord::operator=(const StatisticRecord &s) { - ::memcpy(data, s.data, - sizeof(*data)*theStatisticManager->getNumStatistics()); - return *this; - } - - inline void StatisticRecord::incrementValue(const Statistic &s, - uint64_t addend) const { - data[s.id] += addend; - } - inline uint64_t StatisticRecord::getValue(const Statistic &s) const { - return data[s.id]; - } - - inline StatisticRecord & - StatisticRecord::operator +=(const StatisticRecord &sr) { - unsigned nStats = theStatisticManager->getNumStatistics(); - for (unsigned i=0; i + +namespace klee { + class Statistic; + class StatisticManager; + class StatisticRecord; + + /// Statistic - A named statistic instance. + /// + /// The Statistic class holds information about the statistic, but + /// not the actual values. Values are managed by the global + /// StatisticManager to enable transparent support for instruction + /// level and call path level statistics. + class Statistic final { + friend class StatisticManager; + friend class StatisticRecord; + + private: + std::uint32_t id; + const std::string name; + const std::string shortName; + + public: + Statistic(const std::string &name, const std::string &shortName); + ~Statistic() = default; + + /// getID - Get the unique statistic ID. + std::uint32_t getID() const { return id; } + + /// getName - Get the statistic name. + const std::string &getName() const { return name; } + + /// getShortName - Get the "short" statistic name, used in + /// callgrind output for example. + const std::string &getShortName() const { return shortName; } + + /// getValue - Get the current primary statistic value. + std::uint64_t getValue() const; + + /// operator std::uint64_t - Get the current primary statistic value. + operator std::uint64_t() const { return getValue(); } + + /// operator++ - Increment the statistic by 1. + Statistic &operator++() { return (*this += 1); } + + /// operator+= - Increment the statistic by \arg addend. + Statistic &operator+=(std::uint64_t addend); + }; +} + +#endif /* KLEE_STATISTIC_H */ diff --git a/include/klee/Statistics/Statistics.h b/include/klee/Statistics/Statistics.h new file mode 100644 index 00000000..158459cc --- /dev/null +++ b/include/klee/Statistics/Statistics.h @@ -0,0 +1,154 @@ +//===-- Statistics.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_STATISTICS_H +#define KLEE_STATISTICS_H + +#include "Statistic.h" + +#include +#include +#include + +namespace klee { + class Statistic; + class StatisticRecord { + friend class StatisticManager; + + private: + uint64_t *data; + + public: + StatisticRecord(); + StatisticRecord(const StatisticRecord &s); + ~StatisticRecord() { delete[] data; } + + void zero(); + + uint64_t getValue(const Statistic &s) const; + void incrementValue(const Statistic &s, uint64_t addend) const; + StatisticRecord &operator =(const StatisticRecord &s); + StatisticRecord &operator +=(const StatisticRecord &sr); + }; + + class StatisticManager { + private: + bool enabled; + std::vector stats; + uint64_t *globalStats; + uint64_t *indexedStats; + StatisticRecord *contextStats; + unsigned index; + + public: + StatisticManager(); + ~StatisticManager(); + + void useIndexedStats(unsigned totalIndices); + + StatisticRecord *getContext(); + void setContext(StatisticRecord *sr); /* null to reset */ + + void setIndex(unsigned i) { index = i; } + unsigned getIndex() { return index; } + unsigned getNumStatistics() { return stats.size(); } + Statistic &getStatistic(unsigned i) { return *stats[i]; } + + void registerStatistic(Statistic &s); + void incrementStatistic(Statistic &s, uint64_t addend); + uint64_t getValue(const Statistic &s) const; + void incrementIndexedValue(const Statistic &s, unsigned index, + uint64_t addend) const; + uint64_t getIndexedValue(const Statistic &s, unsigned index) const; + void setIndexedValue(const Statistic &s, unsigned index, uint64_t value); + int getStatisticID(const std::string &name) const; + Statistic *getStatisticByName(const std::string &name) const; + }; + + extern StatisticManager *theStatisticManager; + + inline void StatisticManager::incrementStatistic(Statistic &s, + uint64_t addend) { + if (enabled) { + globalStats[s.id] += addend; + if (indexedStats) { + indexedStats[index*stats.size() + s.id] += addend; + if (contextStats) + contextStats->data[s.id] += addend; + } + } + } + + inline StatisticRecord *StatisticManager::getContext() { + return contextStats; + } + inline void StatisticManager::setContext(StatisticRecord *sr) { + contextStats = sr; + } + + inline void StatisticRecord::zero() { + ::memset(data, 0, sizeof(*data)*theStatisticManager->getNumStatistics()); + } + + inline StatisticRecord::StatisticRecord() + : data(new uint64_t[theStatisticManager->getNumStatistics()]) { + zero(); + } + + inline StatisticRecord::StatisticRecord(const StatisticRecord &s) + : data(new uint64_t[theStatisticManager->getNumStatistics()]) { + ::memcpy(data, s.data, + sizeof(*data)*theStatisticManager->getNumStatistics()); + } + + inline StatisticRecord &StatisticRecord::operator=(const StatisticRecord &s) { + ::memcpy(data, s.data, + sizeof(*data)*theStatisticManager->getNumStatistics()); + return *this; + } + + inline void StatisticRecord::incrementValue(const Statistic &s, + uint64_t addend) const { + data[s.id] += addend; + } + inline uint64_t StatisticRecord::getValue(const Statistic &s) const { + return data[s.id]; + } + + inline StatisticRecord & + StatisticRecord::operator +=(const StatisticRecord &sr) { + unsigned nStats = theStatisticManager->getNumStatistics(); + for (unsigned i=0; i