From 7d85ee81dcf23e841ef794fa6ba08a076dcdebf0 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 3 Apr 2020 13:16:22 +0100 Subject: Removed the Internal directory from include/klee --- include/klee/ADT/DiscretePDF.h | 52 ++ include/klee/ADT/DiscretePDF.inc | 347 ++++++++++++ include/klee/ADT/ImmutableMap.h | 104 ++++ include/klee/ADT/ImmutableSet.h | 101 ++++ include/klee/ADT/ImmutableTree.h | 620 +++++++++++++++++++++ include/klee/ADT/KTest.h | 61 ++ include/klee/ADT/MapOfSets.h | 384 +++++++++++++ include/klee/ADT/RNG.h | 50 ++ include/klee/ADT/TreeStream.h | 76 +++ include/klee/ExecutionState.h | 6 +- include/klee/Internal/ADT/DiscretePDF.h | 52 -- include/klee/Internal/ADT/DiscretePDF.inc | 347 ------------ include/klee/Internal/ADT/ImmutableMap.h | 104 ---- include/klee/Internal/ADT/ImmutableSet.h | 101 ---- include/klee/Internal/ADT/ImmutableTree.h | 620 --------------------- include/klee/Internal/ADT/KTest.h | 61 -- include/klee/Internal/ADT/MapOfSets.h | 384 ------------- include/klee/Internal/ADT/RNG.h | 50 -- include/klee/Internal/ADT/TreeStream.h | 76 --- include/klee/Internal/Module/Cell.h | 23 - .../klee/Internal/Module/InstructionInfoTable.h | 77 --- include/klee/Internal/Module/KInstIterator.h | 42 -- include/klee/Internal/Module/KInstruction.h | 64 --- include/klee/Internal/Module/KModule.h | 153 ----- include/klee/Internal/README.txt | 3 - include/klee/Internal/Support/CompressionStream.h | 46 -- include/klee/Internal/Support/Debug.h | 27 - include/klee/Internal/Support/ErrorHandling.h | 51 -- include/klee/Internal/Support/FileHandling.h | 27 - include/klee/Internal/Support/FloatEvaluation.h | 263 --------- include/klee/Internal/Support/IntEvaluation.h | 164 ------ include/klee/Internal/Support/ModuleUtil.h | 70 --- include/klee/Internal/Support/PrintVersion.h | 25 - include/klee/Internal/Support/Timer.h | 96 ---- include/klee/Internal/System/MemoryUsage.h | 21 - include/klee/Internal/System/Time.h | 120 ---- include/klee/Module/Cell.h | 23 + include/klee/Module/InstructionInfoTable.h | 77 +++ include/klee/Module/KInstIterator.h | 42 ++ include/klee/Module/KInstruction.h | 64 +++ include/klee/Module/KModule.h | 153 +++++ include/klee/Solver/Solver.h | 2 +- include/klee/Solver/SolverImpl.h | 2 +- include/klee/Support/CompressionStream.h | 46 ++ include/klee/Support/Debug.h | 27 + include/klee/Support/ErrorHandling.h | 51 ++ include/klee/Support/FileHandling.h | 27 + include/klee/Support/FloatEvaluation.h | 263 +++++++++ include/klee/Support/IntEvaluation.h | 164 ++++++ include/klee/Support/ModuleUtil.h | 70 +++ include/klee/Support/PrintVersion.h | 25 + include/klee/Support/Timer.h | 96 ++++ include/klee/System/MemoryUsage.h | 21 + include/klee/System/Time.h | 120 ++++ include/klee/TimerStatIncrementer.h | 2 +- 55 files changed, 3070 insertions(+), 3073 deletions(-) create mode 100644 include/klee/ADT/DiscretePDF.h create mode 100644 include/klee/ADT/DiscretePDF.inc create mode 100644 include/klee/ADT/ImmutableMap.h create mode 100644 include/klee/ADT/ImmutableSet.h create mode 100644 include/klee/ADT/ImmutableTree.h create mode 100644 include/klee/ADT/KTest.h create mode 100644 include/klee/ADT/MapOfSets.h create mode 100644 include/klee/ADT/RNG.h create mode 100644 include/klee/ADT/TreeStream.h delete mode 100644 include/klee/Internal/ADT/DiscretePDF.h delete mode 100644 include/klee/Internal/ADT/DiscretePDF.inc delete mode 100644 include/klee/Internal/ADT/ImmutableMap.h delete mode 100644 include/klee/Internal/ADT/ImmutableSet.h delete mode 100644 include/klee/Internal/ADT/ImmutableTree.h delete mode 100644 include/klee/Internal/ADT/KTest.h delete mode 100644 include/klee/Internal/ADT/MapOfSets.h delete mode 100644 include/klee/Internal/ADT/RNG.h delete mode 100644 include/klee/Internal/ADT/TreeStream.h delete mode 100644 include/klee/Internal/Module/Cell.h delete mode 100644 include/klee/Internal/Module/InstructionInfoTable.h delete mode 100644 include/klee/Internal/Module/KInstIterator.h delete mode 100644 include/klee/Internal/Module/KInstruction.h delete mode 100644 include/klee/Internal/Module/KModule.h delete mode 100644 include/klee/Internal/README.txt delete mode 100644 include/klee/Internal/Support/CompressionStream.h delete mode 100644 include/klee/Internal/Support/Debug.h delete mode 100644 include/klee/Internal/Support/ErrorHandling.h delete mode 100644 include/klee/Internal/Support/FileHandling.h delete mode 100644 include/klee/Internal/Support/FloatEvaluation.h delete mode 100644 include/klee/Internal/Support/IntEvaluation.h delete mode 100644 include/klee/Internal/Support/ModuleUtil.h delete mode 100644 include/klee/Internal/Support/PrintVersion.h delete mode 100644 include/klee/Internal/Support/Timer.h delete mode 100644 include/klee/Internal/System/MemoryUsage.h delete mode 100644 include/klee/Internal/System/Time.h create mode 100644 include/klee/Module/Cell.h create mode 100644 include/klee/Module/InstructionInfoTable.h create mode 100644 include/klee/Module/KInstIterator.h create mode 100644 include/klee/Module/KInstruction.h create mode 100644 include/klee/Module/KModule.h create mode 100644 include/klee/Support/CompressionStream.h create mode 100644 include/klee/Support/Debug.h create mode 100644 include/klee/Support/ErrorHandling.h create mode 100644 include/klee/Support/FileHandling.h create mode 100644 include/klee/Support/FloatEvaluation.h create mode 100644 include/klee/Support/IntEvaluation.h create mode 100644 include/klee/Support/ModuleUtil.h create mode 100644 include/klee/Support/PrintVersion.h create mode 100644 include/klee/Support/Timer.h create mode 100644 include/klee/System/MemoryUsage.h create mode 100644 include/klee/System/Time.h (limited to 'include') diff --git a/include/klee/ADT/DiscretePDF.h b/include/klee/ADT/DiscretePDF.h new file mode 100644 index 00000000..74a1ce9e --- /dev/null +++ b/include/klee/ADT/DiscretePDF.h @@ -0,0 +1,52 @@ +//===-- DiscretePDF.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_DISCRETEPDF_H +#define KLEE_DISCRETEPDF_H + +namespace klee { + template + class DiscretePDF { + // not perfectly parameterized, but float/double/int should work ok, + // although it would be better to have choose argument range from 0 + // to queryable max. + typedef double weight_type; + + public: + DiscretePDF(); + ~DiscretePDF(); + + bool empty() const; + void insert(T item, weight_type weight); + void update(T item, weight_type newWeight); + void remove(T item); + bool inTree(T item); + weight_type getWeight(T item); + + /* pick a tree element according to its + * weight. p should be in [0,1). + */ + T choose(double p); + + private: + class Node; + Node *m_root; + + Node **lookup(T item, Node **parent_out); + void split(Node *node); + void rotate(Node *node); + void lengthen(Node *node); + void propogateSumsUp(Node *n); + }; + +} + +#include "DiscretePDF.inc" + +#endif /* KLEE_DISCRETEPDF_H */ diff --git a/include/klee/ADT/DiscretePDF.inc b/include/klee/ADT/DiscretePDF.inc new file mode 100644 index 00000000..743a69b5 --- /dev/null +++ b/include/klee/ADT/DiscretePDF.inc @@ -0,0 +1,347 @@ +//===- DiscretePDF.inc - --*- C++ -*---------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include +namespace klee { + +template +class DiscretePDF::Node +{ +private: + bool m_mark; + +public: + Node *parent, *left, *right; + T key; + weight_type weight, sumWeights; + +public: + Node(T key_, weight_type weight_, Node *parent_); + ~Node(); + + Node *sibling() { return this==parent->left?parent->right:parent->left; } + + void markRed() { m_mark = true; } + void markBlack() { m_mark = false; } + bool isBlack() { return !m_mark; } + bool leftIsBlack() { return !left || left->isBlack(); } + bool rightIsBlack() { return !right || right->isBlack(); } + void setSum() { + sumWeights = weight; + if (left) sumWeights += left->sumWeights; + if (right) sumWeights += right->sumWeights; + } +}; + + /// + +template +DiscretePDF::Node::Node(T key_, weight_type weight_, Node *parent_) { + m_mark = false; + + key = key_; + weight = weight_; + sumWeights = 0; + left = right = 0; + parent = parent_; +} + +template +DiscretePDF::Node::~Node() { + delete left; + delete right; +} + +// + +template +DiscretePDF::DiscretePDF() { + m_root = 0; +} + +template +DiscretePDF::~DiscretePDF() { + delete m_root; +} + +template +bool DiscretePDF::empty() const { + return m_root == 0; +} + +template +void DiscretePDF::insert(T item, weight_type weight) { + Node *p=0, *n=m_root; + + while (n) { + if (!n->leftIsBlack() && !n->rightIsBlack()) + split(n); + + p = n; + if (n->key==item) { + assert(0 && "insert: argument(item) already in tree"); + } else { + n = (itemkey)?n->left:n->right; + } + } + + n = new Node(item, weight, p); + + if (!p) { + m_root = n; + } else { + if (itemkey) { + p->left = n; + } else { + p->right = n; + } + + split(n); + } + + propogateSumsUp(n); +} + +template +void DiscretePDF::remove(T item) { + Node **np = lookup(item, 0); + Node *child, *n = *np; + + if (!n) { + assert(0 && "remove: argument(item) not in tree"); + } else { + if (n->left) { + Node **leftMaxp = &n->left; + + while ((*leftMaxp)->right) + leftMaxp = &(*leftMaxp)->right; + + n->key = (*leftMaxp)->key; + n->weight = (*leftMaxp)->weight; + + np = leftMaxp; + n = *np; + } + + // node now has at most one child + + child = n->left?n->left:n->right; + *np = child; + + if (child) { + child->parent = n->parent; + + if (n->isBlack()) { + lengthen(child); + } + } + + propogateSumsUp(n->parent); + + n->left = n->right = 0; + delete n; + } +} + +template +void DiscretePDF::update(T item, weight_type weight) { + Node *n = *lookup(item, 0); + + if (!n) { + assert(0 && "update: argument(item) not in tree"); + } else { + n->weight = weight; + propogateSumsUp(n); + } +} + +template +T DiscretePDF::choose(double p) { + assert (!((p < 0.0) || (p >= 1.0)) && "choose: argument(p) outside valid range"); + + if (!m_root) + assert(0 && "choose: choose() called on empty tree"); + + weight_type w = (weight_type) (m_root->sumWeights * p); + Node *n = m_root; + + while (1) { + if (n->left) { + if (wleft->sumWeights) { + n = n->left; + continue; + } else { + w -= n->left->sumWeights; + } + } + if (wweight || !n->right) { + break; // !n->right condition shouldn't be necessary, just sanity check + } + w -= n->weight; + n = n->right; + } + + return n->key; +} + +template +bool DiscretePDF::inTree(T item) { + Node *n = *lookup(item, 0); + + return !!n; +} + +template +typename DiscretePDF::weight_type DiscretePDF::getWeight(T item) { + Node *n = *lookup(item, 0); + assert(n); + return n->weight; +} + +// + +template +typename DiscretePDF::Node ** +DiscretePDF::lookup(T item, Node **parent_out) { + Node *n, *p=0, **np=&m_root; + + while ((n = *np)) { + if (n->key==item) { + break; + } else { + p = n; + if (itemkey) { + np = &n->left; + } else { + np = &n->right; + } + } + } + + if (parent_out) + *parent_out = p; + return np; +} + +template +void DiscretePDF::split(Node *n) { + if (n->left) n->left->markBlack(); + if (n->right) n->right->markBlack(); + + if (n->parent) { + Node *p = n->parent; + + n->markRed(); + + if (!p->isBlack()) { + p->parent->markRed(); + + // not same direction + if (!((n==p->left && p==p->parent->left) || + (n==p->right && p==p->parent->right))) { + rotate(n); + p = n; + } + + rotate(p); + p->markBlack(); + } + } +} + +template +void DiscretePDF::rotate(Node *n) { + Node *p=n->parent, *pp=p->parent; + + n->parent = pp; + p->parent = n; + + if (n==p->left) { + p->left = n->right; + n->right = p; + if (p->left) p->left->parent = p; + } else { + p->right = n->left; + n->left = p; + if (p->right) p->right->parent = p; + } + + n->setSum(); + p->setSum(); + + if (!pp) { + m_root = n; + } else { + if (p==pp->left) { + pp->left = n; + } else { + pp->right = n; + } + } +} + +template +void DiscretePDF::lengthen(Node *n) { + if (!n->isBlack()) { + n->markBlack(); + } else if (n->parent) { + Node *sibling = n->sibling(); + + if (sibling && !sibling->isBlack()) { + n->parent->markRed(); + sibling->markBlack(); + + rotate(sibling); // node sibling is now old sibling child, must be black + sibling = n->sibling(); + } + + // sibling is black + + if (!sibling) { + lengthen(n->parent); + } else if (sibling->leftIsBlack() && sibling->rightIsBlack()) { + if (n->parent->isBlack()) { + sibling->markRed(); + lengthen(n->parent); + } else { + sibling->markRed(); + n->parent->markBlack(); + } + } else { + if (n==n->parent->left && sibling->rightIsBlack()) { + rotate(sibling->left); // sibling->left must be red + sibling->markRed(); + sibling->parent->markBlack(); + sibling = sibling->parent; + } else if (n==n->parent->right && sibling->leftIsBlack()) { + rotate(sibling->right); // sibling->right must be red + sibling->markRed(); + sibling->parent->markBlack(); + sibling = sibling->parent; + } + + // sibling is black, and sibling's far child is red + + rotate(sibling); + if (!n->parent->isBlack()) + sibling->markRed(); + sibling->left->markBlack(); + sibling->right->markBlack(); + } + } +} + +template +void DiscretePDF::propogateSumsUp(Node *n) { + for (; n; n=n->parent) + n->setSum(); +} + +} + diff --git a/include/klee/ADT/ImmutableMap.h b/include/klee/ADT/ImmutableMap.h new file mode 100644 index 00000000..a7a18a89 --- /dev/null +++ b/include/klee/ADT/ImmutableMap.h @@ -0,0 +1,104 @@ +//===-- ImmutableMap.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_IMMUTABLEMAP_H +#define KLEE_IMMUTABLEMAP_H + +#include + +#include "ImmutableTree.h" + +namespace klee { + template + struct _Select1st { + D &operator()(V &a) const { return a.first; } + const D &operator()(const V &a) const { return a.first; } + }; + + template > + class ImmutableMap { + public: + typedef K key_type; + typedef std::pair value_type; + + typedef ImmutableTree, CMP> Tree; + typedef typename Tree::iterator iterator; + + private: + Tree elts; + + ImmutableMap(const Tree &b): elts(b) {} + + public: + ImmutableMap() {} + ImmutableMap(const ImmutableMap &b) : elts(b.elts) {} + ~ImmutableMap() {} + + ImmutableMap &operator=(const ImmutableMap &b) { elts = b.elts; return *this; } + + bool empty() const { + return elts.empty(); + } + size_t count(const key_type &key) const { + return elts.count(key); + } + const value_type *lookup(const key_type &key) const { + return elts.lookup(key); + } + const value_type *lookup_previous(const key_type &key) const { + return elts.lookup_previous(key); + } + const value_type &min() const { + return elts.min(); + } + const value_type &max() const { + return elts.max(); + } + size_t size() const { + return elts.size(); + } + + ImmutableMap insert(const value_type &value) const { + return elts.insert(value); + } + ImmutableMap replace(const value_type &value) const { + return elts.replace(value); + } + ImmutableMap remove(const key_type &key) const { + return elts.remove(key); + } + ImmutableMap popMin(const value_type &valueOut) const { + return elts.popMin(valueOut); + } + ImmutableMap popMax(const value_type &valueOut) const { + return elts.popMax(valueOut); + } + + iterator begin() const { + return elts.begin(); + } + iterator end() const { + return elts.end(); + } + iterator find(const key_type &key) const { + return elts.find(key); + } + iterator lower_bound(const key_type &key) const { + return elts.lower_bound(key); + } + iterator upper_bound(const key_type &key) const { + return elts.upper_bound(key); + } + + static size_t getAllocated() { return Tree::allocated; } + }; + +} + +#endif /* KLEE_IMMUTABLEMAP_H */ diff --git a/include/klee/ADT/ImmutableSet.h b/include/klee/ADT/ImmutableSet.h new file mode 100644 index 00000000..1618e559 --- /dev/null +++ b/include/klee/ADT/ImmutableSet.h @@ -0,0 +1,101 @@ +//===-- ImmutableSet.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_IMMUTABLESET_H +#define KLEE_IMMUTABLESET_H + +#include + +#include "ImmutableTree.h" + +namespace klee { + template + struct _Identity { + T &operator()(T &a) const { return a; } + const T &operator()(const T &a) const { return a; } + }; + + template > + class ImmutableSet { + public: + typedef T key_type; + typedef T value_type; + + typedef ImmutableTree, CMP> Tree; + typedef typename Tree::iterator iterator; + + private: + Tree elts; + + ImmutableSet(const Tree &b): elts(b) {} + + public: + ImmutableSet() {} + ImmutableSet(const ImmutableSet &b) : elts(b.elts) {} + ~ImmutableSet() {} + + ImmutableSet &operator=(const ImmutableSet &b) { elts = b.elts; return *this; } + + bool empty() const { + return elts.empty(); + } + size_t count(const key_type &key) const { + return elts.count(key); + } + const value_type *lookup(const key_type &key) const { + return elts.lookup(key); + } + const value_type &min() const { + return elts.min(); + } + const value_type &max() const { + return elts.max(); + } + size_t size() { + return elts.size(); + } + + ImmutableSet insert(const value_type &value) const { + return elts.insert(value); + } + ImmutableSet replace(const value_type &value) const { + return elts.replace(value); + } + ImmutableSet remove(const key_type &key) const { + return elts.remove(key); + } + ImmutableSet popMin(const value_type &valueOut) const { + return elts.popMin(valueOut); + } + ImmutableSet popMax(const value_type &valueOut) const { + return elts.popMax(valueOut); + } + + iterator begin() const { + return elts.begin(); + } + iterator end() const { + return elts.end(); + } + iterator find(const key_type &key) const { + return elts.find(key); + } + iterator lower_bound(const key_type &key) const { + return elts.lower_bound(key); + } + iterator upper_bound(const key_type &key) const { + return elts.upper_bound(key); + } + + static size_t getAllocated() { return Tree::allocated; } + }; + +} + +#endif /* KLEE_IMMUTABLESET_H */ diff --git a/include/klee/ADT/ImmutableTree.h b/include/klee/ADT/ImmutableTree.h new file mode 100644 index 00000000..ada3c211 --- /dev/null +++ b/include/klee/ADT/ImmutableTree.h @@ -0,0 +1,620 @@ +//===-- ImmutableTree.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_IMMUTABLETREE_H +#define KLEE_IMMUTABLETREE_H + +#include +#include + +namespace klee { + template + class ImmutableTree { + public: + static size_t allocated; + class iterator; + + typedef K key_type; + typedef V value_type; + typedef KOV key_of_value; + typedef CMP key_compare; + + public: + ImmutableTree(); + ImmutableTree(const ImmutableTree &s); + ~ImmutableTree(); + + ImmutableTree &operator=(const ImmutableTree &s); + + bool empty() const; + + size_t count(const key_type &key) const; // always 0 or 1 + const value_type *lookup(const key_type &key) const; + + // find the last value less than or equal to key, or null if + // no such value exists + const value_type *lookup_previous(const key_type &key) const; + + const value_type &min() const; + const value_type &max() const; + size_t size() const; + + ImmutableTree insert(const value_type &value) const; + ImmutableTree replace(const value_type &value) const; + ImmutableTree remove(const key_type &key) const; + ImmutableTree popMin(value_type &valueOut) const; + ImmutableTree popMax(value_type &valueOut) const; + + iterator begin() const; + iterator end() const; + iterator find(const key_type &key) const; + iterator lower_bound(const key_type &key) const; + iterator upper_bound(const key_type &key) const; + + static size_t getAllocated() { return allocated; } + + private: + class Node; + + Node *node; + ImmutableTree(Node *_node); + }; + + /***/ + + template + class ImmutableTree::Node { + public: + static Node terminator; + Node *left, *right; + value_type value; + unsigned height, references; + + protected: + Node(); // solely for creating the terminator node + static Node *balance(Node *left, const value_type &value, Node *right); + + public: + + Node(Node *_left, Node *_right, const value_type &_value); + ~Node(); + + void decref(); + Node *incref(); + + bool isTerminator(); + + size_t size(); + Node *popMin(value_type &valueOut); + Node *popMax(value_type &valueOut); + Node *insert(const value_type &v); + Node *replace(const value_type &v); + Node *remove(const key_type &k); + }; + + // Should live somewhere else, this is a simple stack with maximum (dynamic) + // size. + template + class FixedStack { + unsigned pos, max; + T *elts; + + public: + FixedStack(unsigned _max) : pos(0), + max(_max), + elts(new T[max]) {} + FixedStack(const FixedStack &b) : pos(b.pos), + max(b.max), + elts(new T[b.max]) { + std::copy(b.elts, b.elts+pos, elts); + } + ~FixedStack() { delete[] elts; } + + void push_back(const T &elt) { elts[pos++] = elt; } + void pop_back() { --pos; } + bool empty() { return pos==0; } + T &back() { return elts[pos-1]; } + + + FixedStack &operator=(const FixedStack &b) { + assert(max == b.max); + pos = b.pos; + std::copy(b.elts, b.elts+pos, elts); + return *this; + } + + bool operator==(const FixedStack &b) { + return (pos == b.pos && + std::equal(elts, elts+pos, b.elts)); + } + bool operator!=(const FixedStack &b) { return !(*this==b); } + }; + + template + class ImmutableTree::iterator { + friend class ImmutableTree; + private: + Node *root; // so can back up from end + FixedStack stack; + + public: + iterator(Node *_root, bool atBeginning) : root(_root->incref()), + stack(root->height) { + if (atBeginning) { + for (Node *n=root; !n->isTerminator(); n=n->left) + stack.push_back(n); + } + } + iterator(const iterator &i) : root(i.root->incref()), + stack(i.stack) { + } + ~iterator() { + root->decref(); + } + + iterator &operator=(const iterator &b) { + b.root->incref(); + root->decref(); + root = b.root; + stack = b.stack; + return *this; + } + + const value_type &operator*() { + Node *n = stack.back(); + return n->value; + } + + const value_type *operator->() { + Node *n = stack.back(); + return &n->value; + } + + bool operator==(const iterator &b) { + return stack==b.stack; + } + bool operator!=(const iterator &b) { + return stack!=b.stack; + } + + iterator &operator--() { + if (stack.empty()) { + for (Node *n=root; !n->isTerminator(); n=n->right) + stack.push_back(n); + } else { + Node *n = stack.back(); + if (n->left->isTerminator()) { + for (;;) { + Node *prev = n; + stack.pop_back(); + if (stack.empty()) { + break; + } else { + n = stack.back(); + if (prev==n->right) + break; + } + } + } else { + stack.push_back(n->left); + for (n=n->left->right; !n->isTerminator(); n=n->right) + stack.push_back(n); + } + } + return *this; + } + + iterator &operator++() { + assert(!stack.empty()); + Node *n = stack.back(); + if (n->right->isTerminator()) { + for (;;) { + Node *prev = n; + stack.pop_back(); + if (stack.empty()) { + break; + } else { + n = stack.back(); + if (prev==n->left) + break; + } + } + } else { + stack.push_back(n->right); + for (n=n->right->left; !n->isTerminator(); n=n->left) + stack.push_back(n); + } + return *this; + } + }; + + /***/ + + template + typename ImmutableTree::Node + ImmutableTree::Node::terminator; + + template + size_t ImmutableTree::allocated = 0; + + template + ImmutableTree::Node::Node() + : left(&terminator), + right(&terminator), + height(0), + references(3) { + assert(this==&terminator); + } + + template + ImmutableTree::Node::Node(Node *_left, Node *_right, const value_type &_value) + : left(_left), + right(_right), + value(_value), + height(std::max(left->height, right->height) + 1), + references(1) + { + ++allocated; + } + + template + ImmutableTree::Node::~Node() { + left->decref(); + right->decref(); + --allocated; + } + + template + inline void ImmutableTree::Node::decref() { + --references; + if (references==0) delete this; + } + + template + inline typename ImmutableTree::Node *ImmutableTree::Node::incref() { + ++references; + return this; + } + + template + inline bool ImmutableTree::Node::isTerminator() { + return this==&terminator; + } + + /***/ + + template + typename ImmutableTree::Node * + ImmutableTree::Node::balance(Node *left, const value_type &value, Node *right) { + if (left->height > right->height + 2) { + Node *ll = left->left; + Node *lr = left->right; + if (ll->height >= lr->height) { + Node *nlr = new Node(lr->incref(), right, value); + Node *res = new Node(ll->incref(), nlr, left->value); + left->decref(); + return res; + } else { + Node *lrl = lr->left; + Node *lrr = lr->right; + Node *nll = new Node(ll->incref(), lrl->incref(), left->value); + Node *nlr = new Node(lrr->incref(), right, value); + Node *res = new Node(nll, nlr, lr->value); + left->decref(); + return res; + } + } else if (right->height > left->height + 2) { + Node *rl = right->left; + Node *rr = right->right; + if (rr->height >= rl->height) { + Node *nrl = new Node(left, rl->incref(), value); + Node *res = new Node(nrl, rr->incref(), right->value); + right->decref(); + return res; + } else { + Node *rll = rl->left; + Node *rlr = rl->right; + Node *nrl = new Node(left, rll->incref(), value); + Node *nrr = new Node(rlr->incref(), rr->incref(), right->value); + Node *res = new Node(nrl, nrr, rl->value); + right->decref(); + return res; + } + } else { + return new Node(left, right, value); + } + } + + template + size_t ImmutableTree::Node::size() { + if (isTerminator()) { + return 0; + } else { + return left->size() + 1 + right->size(); + } + } + + template + typename ImmutableTree::Node * + ImmutableTree::Node::popMin(value_type &valueOut) { + if (left->isTerminator()) { + valueOut = value; + return right->incref(); + } else { + return balance(left->popMin(valueOut), value, right->incref()); + } + } + + template + typename ImmutableTree::Node * + ImmutableTree::Node::popMax(value_type &valueOut) { + if (right->isTerminator()) { + valueOut = value; + return left->incref(); + } else { + return balance(left->incref(), value, right->popMax(valueOut)); + } + } + + template + typename ImmutableTree::Node * + ImmutableTree::Node::insert(const value_type &v) { + if (isTerminator()) { + return new Node(terminator.incref(), terminator.incref(), v); + } else { + if (key_compare()(key_of_value()(v), key_of_value()(value))) { + return balance(left->insert(v), value, right->incref()); + } else if (key_compare()(key_of_value()(value), key_of_value()(v))) { + return balance(left->incref(), value, right->insert(v)); + } else { + return incref(); + } + } + } + + template + typename ImmutableTree::Node * + ImmutableTree::Node::replace(const value_type &v) { + if (isTerminator()) { + return new Node(terminator.incref(), terminator.incref(), v); + } else { + if (key_compare()(key_of_value()(v), key_of_value()(value))) { + return balance(left->replace(v), value, right->incref()); + } else if (key_compare()(key_of_value()(value), key_of_value()(v))) { + return balance(left->incref(), value, right->replace(v)); + } else { + return new Node(left->incref(), right->incref(), v); + } + } + } + + template + typename ImmutableTree::Node * + ImmutableTree::Node::remove(const key_type &k) { + if (isTerminator()) { + return incref(); + } else { + if (key_compare()(k, key_of_value()(value))) { + return balance(left->remove(k), value, right->incref()); + } else if (key_compare()(key_of_value()(value), k)) { + return balance(left->incref(), value, right->remove(k)); + } else { + if (left->isTerminator()) { + return right->incref(); + } else if (right->isTerminator()) { + return left->incref(); + } else { + value_type min; + Node *nr = right->popMin(min); + return balance(left->incref(), min, nr); + } + } + } + } + + /***/ + + template + ImmutableTree::ImmutableTree() + : node(Node::terminator.incref()) { + } + + template + ImmutableTree::ImmutableTree(Node *_node) + : node(_node) { + } + + template + ImmutableTree::ImmutableTree(const ImmutableTree &s) + : node(s.node->incref()) { + } + + template + ImmutableTree::~ImmutableTree() { + node->decref(); + } + + template + ImmutableTree &ImmutableTree::operator=(const ImmutableTree &s) { + Node *n = s.node->incref(); + node->decref(); + node = n; + return *this; + } + + template + bool ImmutableTree::empty() const { + return node->isTerminator(); + } + + template + size_t ImmutableTree::count(const key_type &k) const { + Node *n = node; + while (!n->isTerminator()) { + key_type key = key_of_value()(n->value); + if (key_compare()(k, key)) { + n = n->left; + } else if (key_compare()(key, k)) { + n = n->right; + } else { + return 1; + } + } + return 0; + } + + template + const typename ImmutableTree::value_type * + ImmutableTree::lookup(const key_type &k) const { + Node *n = node; + while (!n->isTerminator()) { + key_type key = key_of_value()(n->value); + if (key_compare()(k, key)) { + n = n->left; + } else if (key_compare()(key, k)) { + n = n->right; + } else { + return &n->value; + } + } + return 0; + } + + template + const typename ImmutableTree::value_type * + ImmutableTree::lookup_previous(const key_type &k) const { + Node *n = node; + Node *result = 0; + while (!n->isTerminator()) { + key_type key = key_of_value()(n->value); + if (key_compare()(k, key)) { + n = n->left; + } else if (key_compare()(key, k)) { + result = n; + n = n->right; + } else { + return &n->value; + } + } + return result ? &result->value : 0; + } + + template + const typename ImmutableTree::value_type & + ImmutableTree::min() const { + Node *n = node; + assert(!n->isTerminator()); + while (!n->left->isTerminator()) n = n->left; + return n->value; + } + + template + const typename ImmutableTree::value_type & + ImmutableTree::max() const { + Node *n = node; + assert(!n->isTerminator()); + while (!n->right->isTerminator()) n = n->right; + return n->value; + } + + template + size_t ImmutableTree::size() const { + return node->size(); + } + + template + ImmutableTree + ImmutableTree::insert(const value_type &value) const { + return ImmutableTree(node->insert(value)); + } + + template + ImmutableTree + ImmutableTree::replace(const value_type &value) const { + return ImmutableTree(node->replace(value)); + } + + template + ImmutableTree + ImmutableTree::remove(const key_type &key) const { + return ImmutableTree(node->remove(key)); + } + + template + ImmutableTree + ImmutableTree::popMin(value_type &valueOut) const { + return ImmutableTree(node->popMin(valueOut)); + } + + template + ImmutableTree + ImmutableTree::popMax(value_type &valueOut) const { + return ImmutableTree(node->popMax(valueOut)); + } + + template + inline typename ImmutableTree::iterator + ImmutableTree::begin() const { + return iterator(node, true); + } + + template + inline typename ImmutableTree::iterator + ImmutableTree::end() const { + return iterator(node, false); + } + + template + inline typename ImmutableTree::iterator + ImmutableTree::find(const key_type &key) const { + iterator end(node,false), it = lower_bound(key); + if (it==end || key_compare()(key,key_of_value()(*it))) { + return end; + } else { + return it; + } + } + + template + inline typename ImmutableTree::iterator + ImmutableTree::lower_bound(const key_type &k) const { + // XXX ugh this doesn't have to be so ugly does it? + iterator it(node,false); + for (Node *root=node; !root->isTerminator();) { + it.stack.push_back(root); + if (key_compare()(k, key_of_value()(root->value))) { + root = root->left; + } else if (key_compare()(key_of_value()(root->value), k)) { + root = root->right; + } else { + return it; + } + } + // it is now beginning or first element < k + if (!it.stack.empty()) { + Node *last = it.stack.back(); + if (key_compare()(key_of_value()(last->value), k)) + ++it; + } + return it; + } + + template + typename ImmutableTree::iterator + ImmutableTree::upper_bound(const key_type &key) const { + iterator end(node,false),it = lower_bound(key); + if (it!=end && + !key_compare()(key,key_of_value()(*it))) // no need to loop, no duplicates + ++it; + return it; + } + +} + +#endif /* KLEE_IMMUTABLETREE_H */ diff --git a/include/klee/ADT/KTest.h b/include/klee/ADT/KTest.h new file mode 100644 index 00000000..5b5c45ef --- /dev/null +++ b/include/klee/ADT/KTest.h @@ -0,0 +1,61 @@ +//===-- KTest.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_KTEST_H +#define KLEE_KTEST_H + +#ifdef __cplusplus +extern "C" { +#endif + + typedef struct KTestObject KTestObject; + struct KTestObject { + char *name; + unsigned numBytes; + unsigned char *bytes; + }; + + typedef struct KTest KTest; + struct KTest { + /* file format version */ + unsigned version; + + unsigned numArgs; + char **args; + + unsigned symArgvs; + unsigned symArgvLen; + + unsigned numObjects; + KTestObject *objects; + }; + + + /* returns the current .ktest file format version */ + unsigned kTest_getCurrentVersion(); + + /* return true iff file at path matches KTest header */ + int kTest_isKTestFile(const char *path); + + /* returns NULL on (unspecified) error */ + KTest* kTest_fromFile(const char *path); + + /* returns 1 on success, 0 on (unspecified) error */ + int kTest_toFile(KTest *, const char *path); + + /* returns total number of object bytes */ + unsigned kTest_numBytes(KTest *); + + void kTest_free(KTest *); + +#ifdef __cplusplus +} +#endif + +#endif /* KLEE_KTEST_H */ diff --git a/include/klee/ADT/MapOfSets.h b/include/klee/ADT/MapOfSets.h new file mode 100644 index 00000000..b30934d8 --- /dev/null +++ b/include/klee/ADT/MapOfSets.h @@ -0,0 +1,384 @@ +//===-- MapOfSets.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_MAPOFSETS_H +#define KLEE_MAPOFSETS_H + +#include +#include +#include +#include + +// This should really be broken down into TreeOfSets on top of which +// SetOfSets and MapOfSets are easily implemeted. It should also be +// parameterized on the underlying set type. Neither are hard to do, +// just not worth it at the moment. +// +// I also broke some STLish conventions because I was bored. + +namespace klee { + + /** This implements the UBTree data structure (see Hoffmann and + Koehler, "A New Method to Index and Query Sets", IJCAI 1999) */ + template + class MapOfSets { + public: + class iterator; + + public: + MapOfSets(); + + void clear(); + + void insert(const std::set &set, const V &value); + + V *lookup(const std::set &set); + + iterator begin(); + iterator end(); + + void subsets(const std::set &set, + std::vector< std::pair, V> > &resultOut); + void supersets(const std::set &set, + std::vector< std::pair, V> > &resultOut); + + template + V *findSuperset(const std::set &set, const Predicate &p); + template + V *findSubset(const std::set &set, const Predicate &p); + + private: + class Node; + + Node root; + + template + void findSubsets(Node *n, + const std::set &accum, + Iterator begin, + Iterator end, + Vector &resultsOut); + template + void findSupersets(Node *n, + const std::set &accum, + Iterator begin, + Iterator end, + Vector &resultsOut); + template + V *findSuperset(Node *n, + typename std::set::iterator begin, + typename std::set::iterator end, + const Predicate &p); + template + V *findSubset(Node *n, + typename std::set::iterator begin, + typename std::set::iterator end, + const Predicate &p); + }; + + /***/ + + template + class MapOfSets::Node { + friend class MapOfSets; + friend class MapOfSets::iterator; + + public: + typedef std::map children_ty; + + V value; + + private: + bool isEndOfSet; + std::map children; + + public: + Node() : value(), isEndOfSet(false) {} + }; + + template + class MapOfSets::iterator { + typedef std::vector< typename std::map::iterator > stack_ty; + friend class MapOfSets; + private: + Node *root; + bool onEntry; + stack_ty stack; + + void step() { + if (onEntry) { + onEntry = false; + Node *n = stack.empty() ? root : &stack.back()->second; + while (!n->children.empty()) { + stack.push_back(n->children.begin()); + n = &stack.back()->second; + if (n->isEndOfSet) { + onEntry = true; + return; + } + } + } + + while (!stack.empty()) { + unsigned size = stack.size(); + Node *at = size==1 ? root : &stack[size-2]->second; + typename std::map::iterator &cur = stack.back(); + ++cur; + if (cur==at->children.end()) { + stack.pop_back(); + } else { + Node *n = &cur->second; + + while (!n->isEndOfSet) { + assert(!n->children.empty()); + stack.push_back(n->children.begin()); + n = &stack.back()->second; + } + + onEntry = true; + break; + } + } + } + + public: + // end() + iterator() : onEntry(false) {} + // begin() + iterator(Node *_n) : root(_n), onEntry(true) { + if (!root->isEndOfSet) + step(); + } + + const std::pair, const V> operator*() { + assert(onEntry || !stack.empty()); + std::set s; + for (typename stack_ty::iterator it = stack.begin(), ie = stack.end(); + it != ie; ++it) + s.insert((*it)->first); + Node *n = stack.empty() ? root : &stack.back()->second; + return std::make_pair(s, n->value); + } + + bool operator==(const iterator &b) { + return onEntry==b.onEntry && stack==b.stack; + } + bool operator!=(const iterator &b) { + return !(*this==b); + } + + iterator &operator++() { + step(); + return *this; + } + }; + + /***/ + + template + MapOfSets::MapOfSets() {} + + template + void MapOfSets::insert(const std::set &set, const V &value) { + Node *n = &root; + for (auto const& element : set) { + n = &n->children.insert(std::make_pair(element, Node())).first->second; + } + n->isEndOfSet = true; + n->value = value; + } + + template + V *MapOfSets::lookup(const std::set &set) { + Node *n = &root; + for (typename std::set::const_iterator it = set.begin(), ie = set.end(); + it != ie; ++it) { + typename Node::children_ty::iterator kit = n->children.find(*it); + if (kit==n->children.end()) { + return 0; + } else { + n = &kit->second; + } + } + if (n->isEndOfSet) { + return &n->value; + } else { + return 0; + } + } + + template + typename MapOfSets::iterator + MapOfSets::begin() { return iterator(&root); } + + template + typename MapOfSets::iterator + MapOfSets::end() { return iterator(); } + + template + template + void MapOfSets::findSubsets(Node *n, + const std::set &accum, + Iterator begin, + Iterator end, + Vector &resultsOut) { + if (n->isEndOfSet) { + resultsOut.push_back(std::make_pair(accum, n->value)); + } + + for (Iterator it=begin; it!=end;) { + K elt = *it; + typename Node::children_ty::iterator kit = n->children.find(elt); + it++; + if (kit!=n->children.end()) { + std::set nacc = accum; + nacc.insert(elt); + findSubsets(&kit->second, nacc, it, end, resultsOut); + } + } + } + + template + void MapOfSets::subsets(const std::set &set, + std::vector< std::pair, + V> > &resultOut) { + findSubsets(&root, std::set(), set.begin(), set.end(), resultOut); + } + + template + template + void MapOfSets::findSupersets(Node *n, + const std::set &accum, + Iterator begin, + Iterator end, + Vector &resultsOut) { + if (begin==end) { + if (n->isEndOfSet) + resultsOut.push_back(std::make_pair(accum, n->value)); + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + std::set nacc = accum; + nacc.insert(it->first); + findSupersets(&it->second, nacc, begin, end, resultsOut); + } + } else { + K elt = *begin; + Iterator next = begin; + ++next; + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + std::set nacc = accum; + nacc.insert(it->first); + if (elt==it->first) { + findSupersets(&it->second, nacc, next, end, resultsOut); + } else if (it->firstsecond, nacc, begin, end, resultsOut); + } else { + break; + } + } + } + } + + template + void MapOfSets::supersets(const std::set &set, + std::vector< std::pair, V> > &resultOut) { + findSupersets(&root, std::set(), set.begin(), set.end(), resultOut); + } + + template + template + V *MapOfSets::findSubset(Node *n, + typename std::set::iterator begin, + typename std::set::iterator end, + const Predicate &p) { + if (n->isEndOfSet && p(n->value)) { + return &n->value; + } else if (begin==end) { + return 0; + } else { + typename Node::children_ty::iterator kend = n->children.end(); + typename Node::children_ty::iterator + kbegin = n->children.lower_bound(*begin); + typename std::set::iterator it = begin; + if (kbegin==kend) + return 0; + for (;;) { // kbegin!=kend && *it <= kbegin->first + while (*it < kbegin->first) { + ++it; + if (it==end) + return 0; + } + if (*it == kbegin->first) { + ++it; + V *res = findSubset(&kbegin->second, it, end, p); + if (res || it==end) + return res; + } + while (kbegin->first < *it) { + ++kbegin; + if (kbegin==kend) + return 0; + } + } + } + } + + template + template + V *MapOfSets::findSuperset(Node *n, + typename std::set::iterator begin, + typename std::set::iterator end, + const Predicate &p) { + if (begin==end) { + if (n->isEndOfSet && p(n->value)) + return &n->value; + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + V *res = findSuperset(&it->second, begin, end, p); + if (res) return res; + } + } else { + typename Node::children_ty::iterator kmid = + n->children.lower_bound(*begin); + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + V *res = findSuperset(&it->second, begin, end, p); + if (res) return res; + } + if (kmid!=n->children.end() && *begin==kmid->first) { + V *res = findSuperset(&kmid->second, ++begin, end, p); + if (res) return res; + } + } + return 0; + } + + template + template + V *MapOfSets::findSuperset(const std::set &set, const Predicate &p) { + return findSuperset(&root, set.begin(), set.end(), p); + } + + template + template + V *MapOfSets::findSubset(const std::set &set, const Predicate &p) { + return findSubset(&root, set.begin(), set.end(), p); + } + + template + void MapOfSets::clear() { + root.isEndOfSet = false; + root.value = V(); + root.children.clear(); + } + +} + +#endif /* KLEE_MAPOFSETS_H */ diff --git a/include/klee/ADT/RNG.h b/include/klee/ADT/RNG.h new file mode 100644 index 00000000..5ea375b5 --- /dev/null +++ b/include/klee/ADT/RNG.h @@ -0,0 +1,50 @@ +//===-- RNG.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_RNG_H +#define KLEE_RNG_H + +namespace klee { + class RNG { + private: + /* Period parameters */ + static const int N = 624; + static const int M = 397; + static const unsigned int MATRIX_A = 0x9908b0dfUL; /* constant vector a */ + static const unsigned int UPPER_MASK = 0x80000000UL; /* most significant w-r bits */ + static const unsigned int LOWER_MASK = 0x7fffffffUL; /* least significant r bits */ + + private: + unsigned int mt[N]; /* the array for the state vector */ + int mti; + + public: + RNG(unsigned int seed=5489UL); + + void seed(unsigned int seed); + + /* generates a random number on [0,0xffffffff]-interval */ + unsigned int getInt32(); + /* generates a random number on [0,0x7fffffff]-interval */ + int getInt31(); + /* generates a random number on [0,1]-real-interval */ + double getDoubleLR(); + float getFloatLR(); + /* generates a random number on [0,1)-real-interval */ + double getDoubleL(); + float getFloatL(); + /* generates a random number on (0,1)-real-interval */ + double getDouble(); + float getFloat(); + /* generators a random flop */ + bool getBool(); + }; +} + +#endif /* KLEE_RNG_H */ diff --git a/include/klee/ADT/TreeStream.h b/include/klee/ADT/TreeStream.h new file mode 100644 index 00000000..32c856c9 --- /dev/null +++ b/include/klee/ADT/TreeStream.h @@ -0,0 +1,76 @@ +//===-- TreeStream.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_TREESTREAM_H +#define KLEE_TREESTREAM_H + +#include +#include + +namespace klee { + + typedef unsigned TreeStreamID; + class TreeOStream; + + class TreeStreamWriter { + static const unsigned bufferSize = 4*4096; + + friend class TreeOStream; + + private: + char buffer[bufferSize]; + unsigned lastID, bufferCount; + + std::string path; + std::ofstream *output; + unsigned ids; + + void write(TreeOStream &os, const char *s, unsigned size); + void flushBuffer(); + + public: + TreeStreamWriter(const std::string &_path); + ~TreeStreamWriter(); + + bool good(); + + TreeOStream open(); + TreeOStream open(const TreeOStream &node); + + void flush(); + + // hack, to be replace by proper stream capabilities + void readStream(TreeStreamID id, + std::vector &out); + }; + + class TreeOStream { + friend class TreeStreamWriter; + + private: + TreeStreamWriter *writer; + unsigned id; + + TreeOStream(TreeStreamWriter &_writer, unsigned _id); + + public: + TreeOStream(); + ~TreeOStream(); + + unsigned getID() const; + + void write(const char *buffer, unsigned size); + + TreeOStream &operator<<(const std::string &s); + + void flush(); + }; +} + +#endif /* KLEE_TREESTREAM_H */ diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index e647d0ab..b5625a00 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -12,13 +12,13 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" -#include "klee/Internal/ADT/TreeStream.h" -#include "klee/Internal/System/Time.h" +#include "klee/ADT/TreeStream.h" +#include "klee/System/Time.h" #include "klee/MergeHandler.h" // FIXME: We do not want to be exposing these? :( #include "../../lib/Core/AddressSpace.h" -#include "klee/Internal/Module/KInstIterator.h" +#include "klee/Module/KInstIterator.h" #include #include diff --git a/include/klee/Internal/ADT/DiscretePDF.h b/include/klee/Internal/ADT/DiscretePDF.h deleted file mode 100644 index 74a1ce9e..00000000 --- a/include/klee/Internal/ADT/DiscretePDF.h +++ /dev/null @@ -1,52 +0,0 @@ -//===-- DiscretePDF.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_DISCRETEPDF_H -#define KLEE_DISCRETEPDF_H - -namespace klee { - template - class DiscretePDF { - // not perfectly parameterized, but float/double/int should work ok, - // although it would be better to have choose argument range from 0 - // to queryable max. - typedef double weight_type; - - public: - DiscretePDF(); - ~DiscretePDF(); - - bool empty() const; - void insert(T item, weight_type weight); - void update(T item, weight_type newWeight); - void remove(T item); - bool inTree(T item); - weight_type getWeight(T item); - - /* pick a tree element according to its - * weight. p should be in [0,1). - */ - T choose(double p); - - private: - class Node; - Node *m_root; - - Node **lookup(T item, Node **parent_out); - void split(Node *node); - void rotate(Node *node); - void lengthen(Node *node); - void propogateSumsUp(Node *n); - }; - -} - -#include "DiscretePDF.inc" - -#endif /* KLEE_DISCRETEPDF_H */ diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc deleted file mode 100644 index 743a69b5..00000000 --- a/include/klee/Internal/ADT/DiscretePDF.inc +++ /dev/null @@ -1,347 +0,0 @@ -//===- DiscretePDF.inc - --*- C++ -*---------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include -namespace klee { - -template -class DiscretePDF::Node -{ -private: - bool m_mark; - -public: - Node *parent, *left, *right; - T key; - weight_type weight, sumWeights; - -public: - Node(T key_, weight_type weight_, Node *parent_); - ~Node(); - - Node *sibling() { return this==parent->left?parent->right:parent->left; } - - void markRed() { m_mark = true; } - void markBlack() { m_mark = false; } - bool isBlack() { return !m_mark; } - bool leftIsBlack() { return !left || left->isBlack(); } - bool rightIsBlack() { return !right || right->isBlack(); } - void setSum() { - sumWeights = weight; - if (left) sumWeights += left->sumWeights; - if (right) sumWeights += right->sumWeights; - } -}; - - /// - -template -DiscretePDF::Node::Node(T key_, weight_type weight_, Node *parent_) { - m_mark = false; - - key = key_; - weight = weight_; - sumWeights = 0; - left = right = 0; - parent = parent_; -} - -template -DiscretePDF::Node::~Node() { - delete left; - delete right; -} - -// - -template -DiscretePDF::DiscretePDF() { - m_root = 0; -} - -template -DiscretePDF::~DiscretePDF() { - delete m_root; -} - -template -bool DiscretePDF::empty() const { - return m_root == 0; -} - -template -void DiscretePDF::insert(T item, weight_type weight) { - Node *p=0, *n=m_root; - - while (n) { - if (!n->leftIsBlack() && !n->rightIsBlack()) - split(n); - - p = n; - if (n->key==item) { - assert(0 && "insert: argument(item) already in tree"); - } else { - n = (itemkey)?n->left:n->right; - } - } - - n = new Node(item, weight, p); - - if (!p) { - m_root = n; - } else { - if (itemkey) { - p->left = n; - } else { - p->right = n; - } - - split(n); - } - - propogateSumsUp(n); -} - -template -void DiscretePDF::remove(T item) { - Node **np = lookup(item, 0); - Node *child, *n = *np; - - if (!n) { - assert(0 && "remove: argument(item) not in tree"); - } else { - if (n->left) { - Node **leftMaxp = &n->left; - - while ((*leftMaxp)->right) - leftMaxp = &(*leftMaxp)->right; - - n->key = (*leftMaxp)->key; - n->weight = (*leftMaxp)->weight; - - np = leftMaxp; - n = *np; - } - - // node now has at most one child - - child = n->left?n->left:n->right; - *np = child; - - if (child) { - child->parent = n->parent; - - if (n->isBlack()) { - lengthen(child); - } - } - - propogateSumsUp(n->parent); - - n->left = n->right = 0; - delete n; - } -} - -template -void DiscretePDF::update(T item, weight_type weight) { - Node *n = *lookup(item, 0); - - if (!n) { - assert(0 && "update: argument(item) not in tree"); - } else { - n->weight = weight; - propogateSumsUp(n); - } -} - -template -T DiscretePDF::choose(double p) { - assert (!((p < 0.0) || (p >= 1.0)) && "choose: argument(p) outside valid range"); - - if (!m_root) - assert(0 && "choose: choose() called on empty tree"); - - weight_type w = (weight_type) (m_root->sumWeights * p); - Node *n = m_root; - - while (1) { - if (n->left) { - if (wleft->sumWeights) { - n = n->left; - continue; - } else { - w -= n->left->sumWeights; - } - } - if (wweight || !n->right) { - break; // !n->right condition shouldn't be necessary, just sanity check - } - w -= n->weight; - n = n->right; - } - - return n->key; -} - -template -bool DiscretePDF::inTree(T item) { - Node *n = *lookup(item, 0); - - return !!n; -} - -template -typename DiscretePDF::weight_type DiscretePDF::getWeight(T item) { - Node *n = *lookup(item, 0); - assert(n); - return n->weight; -} - -// - -template -typename DiscretePDF::Node ** -DiscretePDF::lookup(T item, Node **parent_out) { - Node *n, *p=0, **np=&m_root; - - while ((n = *np)) { - if (n->key==item) { - break; - } else { - p = n; - if (itemkey) { - np = &n->left; - } else { - np = &n->right; - } - } - } - - if (parent_out) - *parent_out = p; - return np; -} - -template -void DiscretePDF::split(Node *n) { - if (n->left) n->left->markBlack(); - if (n->right) n->right->markBlack(); - - if (n->parent) { - Node *p = n->parent; - - n->markRed(); - - if (!p->isBlack()) { - p->parent->markRed(); - - // not same direction - if (!((n==p->left && p==p->parent->left) || - (n==p->right && p==p->parent->right))) { - rotate(n); - p = n; - } - - rotate(p); - p->markBlack(); - } - } -} - -template -void DiscretePDF::rotate(Node *n) { - Node *p=n->parent, *pp=p->parent; - - n->parent = pp; - p->parent = n; - - if (n==p->left) { - p->left = n->right; - n->right = p; - if (p->left) p->left->parent = p; - } else { - p->right = n->left; - n->left = p; - if (p->right) p->right->parent = p; - } - - n->setSum(); - p->setSum(); - - if (!pp) { - m_root = n; - } else { - if (p==pp->left) { - pp->left = n; - } else { - pp->right = n; - } - } -} - -template -void DiscretePDF::lengthen(Node *n) { - if (!n->isBlack()) { - n->markBlack(); - } else if (n->parent) { - Node *sibling = n->sibling(); - - if (sibling && !sibling->isBlack()) { - n->parent->markRed(); - sibling->markBlack(); - - rotate(sibling); // node sibling is now old sibling child, must be black - sibling = n->sibling(); - } - - // sibling is black - - if (!sibling) { - lengthen(n->parent); - } else if (sibling->leftIsBlack() && sibling->rightIsBlack()) { - if (n->parent->isBlack()) { - sibling->markRed(); - lengthen(n->parent); - } else { - sibling->markRed(); - n->parent->markBlack(); - } - } else { - if (n==n->parent->left && sibling->rightIsBlack()) { - rotate(sibling->left); // sibling->left must be red - sibling->markRed(); - sibling->parent->markBlack(); - sibling = sibling->parent; - } else if (n==n->parent->right && sibling->leftIsBlack()) { - rotate(sibling->right); // sibling->right must be red - sibling->markRed(); - sibling->parent->markBlack(); - sibling = sibling->parent; - } - - // sibling is black, and sibling's far child is red - - rotate(sibling); - if (!n->parent->isBlack()) - sibling->markRed(); - sibling->left->markBlack(); - sibling->right->markBlack(); - } - } -} - -template -void DiscretePDF::propogateSumsUp(Node *n) { - for (; n; n=n->parent) - n->setSum(); -} - -} - diff --git a/include/klee/Internal/ADT/ImmutableMap.h b/include/klee/Internal/ADT/ImmutableMap.h deleted file mode 100644 index a7a18a89..00000000 --- a/include/klee/Internal/ADT/ImmutableMap.h +++ /dev/null @@ -1,104 +0,0 @@ -//===-- ImmutableMap.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_IMMUTABLEMAP_H -#define KLEE_IMMUTABLEMAP_H - -#include - -#include "ImmutableTree.h" - -namespace klee { - template - struct _Select1st { - D &operator()(V &a) const { return a.first; } - const D &operator()(const V &a) const { return a.first; } - }; - - template > - class ImmutableMap { - public: - typedef K key_type; - typedef std::pair value_type; - - typedef ImmutableTree, CMP> Tree; - typedef typename Tree::iterator iterator; - - private: - Tree elts; - - ImmutableMap(const Tree &b): elts(b) {} - - public: - ImmutableMap() {} - ImmutableMap(const ImmutableMap &b) : elts(b.elts) {} - ~ImmutableMap() {} - - ImmutableMap &operator=(const ImmutableMap &b) { elts = b.elts; return *this; } - - bool empty() const { - return elts.empty(); - } - size_t count(const key_type &key) const { - return elts.count(key); - } - const value_type *lookup(const key_type &key) const { - return elts.lookup(key); - } - const value_type *lookup_previous(const key_type &key) const { - return elts.lookup_previous(key); - } - const value_type &min() const { - return elts.min(); - } - const value_type &max() const { - return elts.max(); - } - size_t size() const { - return elts.size(); - } - - ImmutableMap insert(const value_type &value) const { - return elts.insert(value); - } - ImmutableMap replace(const value_type &value) const { - return elts.replace(value); - } - ImmutableMap remove(const key_type &key) const { - return elts.remove(key); - } - ImmutableMap popMin(const value_type &valueOut) const { - return elts.popMin(valueOut); - } - ImmutableMap popMax(const value_type &valueOut) const { - return elts.popMax(valueOut); - } - - iterator begin() const { - return elts.begin(); - } - iterator end() const { - return elts.end(); - } - iterator find(const key_type &key) const { - return elts.find(key); - } - iterator lower_bound(const key_type &key) const { - return elts.lower_bound(key); - } - iterator upper_bound(const key_type &key) const { - return elts.upper_bound(key); - } - - static size_t getAllocated() { return Tree::allocated; } - }; - -} - -#endif /* KLEE_IMMUTABLEMAP_H */ diff --git a/include/klee/Internal/ADT/ImmutableSet.h b/include/klee/Internal/ADT/ImmutableSet.h deleted file mode 100644 index 1618e559..00000000 --- a/include/klee/Internal/ADT/ImmutableSet.h +++ /dev/null @@ -1,101 +0,0 @@ -//===-- ImmutableSet.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_IMMUTABLESET_H -#define KLEE_IMMUTABLESET_H - -#include - -#include "ImmutableTree.h" - -namespace klee { - template - struct _Identity { - T &operator()(T &a) const { return a; } - const T &operator()(const T &a) const { return a; } - }; - - template > - class ImmutableSet { - public: - typedef T key_type; - typedef T value_type; - - typedef ImmutableTree, CMP> Tree; - typedef typename Tree::iterator iterator; - - private: - Tree elts; - - ImmutableSet(const Tree &b): elts(b) {} - - public: - ImmutableSet() {} - ImmutableSet(const ImmutableSet &b) : elts(b.elts) {} - ~ImmutableSet() {} - - ImmutableSet &operator=(const ImmutableSet &b) { elts = b.elts; return *this; } - - bool empty() const { - return elts.empty(); - } - size_t count(const key_type &key) const { - return elts.count(key); - } - const value_type *lookup(const key_type &key) const { - return elts.lookup(key); - } - const value_type &min() const { - return elts.min(); - } - const value_type &max() const { - return elts.max(); - } - size_t size() { - return elts.size(); - } - - ImmutableSet insert(const value_type &value) const { - return elts.insert(value); - } - ImmutableSet replace(const value_type &value) const { - return elts.replace(value); - } - ImmutableSet remove(const key_type &key) const { - return elts.remove(key); - } - ImmutableSet popMin(const value_type &valueOut) const { - return elts.popMin(valueOut); - } - ImmutableSet popMax(const value_type &valueOut) const { - return elts.popMax(valueOut); - } - - iterator begin() const { - return elts.begin(); - } - iterator end() const { - return elts.end(); - } - iterator find(const key_type &key) const { - return elts.find(key); - } - iterator lower_bound(const key_type &key) const { - return elts.lower_bound(key); - } - iterator upper_bound(const key_type &key) const { - return elts.upper_bound(key); - } - - static size_t getAllocated() { return Tree::allocated; } - }; - -} - -#endif /* KLEE_IMMUTABLESET_H */ diff --git a/include/klee/Internal/ADT/ImmutableTree.h b/include/klee/Internal/ADT/ImmutableTree.h deleted file mode 100644 index ada3c211..00000000 --- a/include/klee/Internal/ADT/ImmutableTree.h +++ /dev/null @@ -1,620 +0,0 @@ -//===-- ImmutableTree.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_IMMUTABLETREE_H -#define KLEE_IMMUTABLETREE_H - -#include -#include - -namespace klee { - template - class ImmutableTree { - public: - static size_t allocated; - class iterator; - - typedef K key_type; - typedef V value_type; - typedef KOV key_of_value; - typedef CMP key_compare; - - public: - ImmutableTree(); - ImmutableTree(const ImmutableTree &s); - ~ImmutableTree(); - - ImmutableTree &operator=(const ImmutableTree &s); - - bool empty() const; - - size_t count(const key_type &key) const; // always 0 or 1 - const value_type *lookup(const key_type &key) const; - - // find the last value less than or equal to key, or null if - // no such value exists - const value_type *lookup_previous(const key_type &key) const; - - const value_type &min() const; - const value_type &max() const; - size_t size() const; - - ImmutableTree insert(const value_type &value) const; - ImmutableTree replace(const value_type &value) const; - ImmutableTree remove(const key_type &key) const; - ImmutableTree popMin(value_type &valueOut) const; - ImmutableTree popMax(value_type &valueOut) const; - - iterator begin() const; - iterator end() const; - iterator find(const key_type &key) const; - iterator lower_bound(const key_type &key) const; - iterator upper_bound(const key_type &key) const; - - static size_t getAllocated() { return allocated; } - - private: - class Node; - - Node *node; - ImmutableTree(Node *_node); - }; - - /***/ - - template - class ImmutableTree::Node { - public: - static Node terminator; - Node *left, *right; - value_type value; - unsigned height, references; - - protected: - Node(); // solely for creating the terminator node - static Node *balance(Node *left, const value_type &value, Node *right); - - public: - - Node(Node *_left, Node *_right, const value_type &_value); - ~Node(); - - void decref(); - Node *incref(); - - bool isTerminator(); - - size_t size(); - Node *popMin(value_type &valueOut); - Node *popMax(value_type &valueOut); - Node *insert(const value_type &v); - Node *replace(const value_type &v); - Node *remove(const key_type &k); - }; - - // Should live somewhere else, this is a simple stack with maximum (dynamic) - // size. - template - class FixedStack { - unsigned pos, max; - T *elts; - - public: - FixedStack(unsigned _max) : pos(0), - max(_max), - elts(new T[max]) {} - FixedStack(const FixedStack &b) : pos(b.pos), - max(b.max), - elts(new T[b.max]) { - std::copy(b.elts, b.elts+pos, elts); - } - ~FixedStack() { delete[] elts; } - - void push_back(const T &elt) { elts[pos++] = elt; } - void pop_back() { --pos; } - bool empty() { return pos==0; } - T &back() { return elts[pos-1]; } - - - FixedStack &operator=(const FixedStack &b) { - assert(max == b.max); - pos = b.pos; - std::copy(b.elts, b.elts+pos, elts); - return *this; - } - - bool operator==(const FixedStack &b) { - return (pos == b.pos && - std::equal(elts, elts+pos, b.elts)); - } - bool operator!=(const FixedStack &b) { return !(*this==b); } - }; - - template - class ImmutableTree::iterator { - friend class ImmutableTree; - private: - Node *root; // so can back up from end - FixedStack stack; - - public: - iterator(Node *_root, bool atBeginning) : root(_root->incref()), - stack(root->height) { - if (atBeginning) { - for (Node *n=root; !n->isTerminator(); n=n->left) - stack.push_back(n); - } - } - iterator(const iterator &i) : root(i.root->incref()), - stack(i.stack) { - } - ~iterator() { - root->decref(); - } - - iterator &operator=(const iterator &b) { - b.root->incref(); - root->decref(); - root = b.root; - stack = b.stack; - return *this; - } - - const value_type &operator*() { - Node *n = stack.back(); - return n->value; - } - - const value_type *operator->() { - Node *n = stack.back(); - return &n->value; - } - - bool operator==(const iterator &b) { - return stack==b.stack; - } - bool operator!=(const iterator &b) { - return stack!=b.stack; - } - - iterator &operator--() { - if (stack.empty()) { - for (Node *n=root; !n->isTerminator(); n=n->right) - stack.push_back(n); - } else { - Node *n = stack.back(); - if (n->left->isTerminator()) { - for (;;) { - Node *prev = n; - stack.pop_back(); - if (stack.empty()) { - break; - } else { - n = stack.back(); - if (prev==n->right) - break; - } - } - } else { - stack.push_back(n->left); - for (n=n->left->right; !n->isTerminator(); n=n->right) - stack.push_back(n); - } - } - return *this; - } - - iterator &operator++() { - assert(!stack.empty()); - Node *n = stack.back(); - if (n->right->isTerminator()) { - for (;;) { - Node *prev = n; - stack.pop_back(); - if (stack.empty()) { - break; - } else { - n = stack.back(); - if (prev==n->left) - break; - } - } - } else { - stack.push_back(n->right); - for (n=n->right->left; !n->isTerminator(); n=n->left) - stack.push_back(n); - } - return *this; - } - }; - - /***/ - - template - typename ImmutableTree::Node - ImmutableTree::Node::terminator; - - template - size_t ImmutableTree::allocated = 0; - - template - ImmutableTree::Node::Node() - : left(&terminator), - right(&terminator), - height(0), - references(3) { - assert(this==&terminator); - } - - template - ImmutableTree::Node::Node(Node *_left, Node *_right, const value_type &_value) - : left(_left), - right(_right), - value(_value), - height(std::max(left->height, right->height) + 1), - references(1) - { - ++allocated; - } - - template - ImmutableTree::Node::~Node() { - left->decref(); - right->decref(); - --allocated; - } - - template - inline void ImmutableTree::Node::decref() { - --references; - if (references==0) delete this; - } - - template - inline typename ImmutableTree::Node *ImmutableTree::Node::incref() { - ++references; - return this; - } - - template - inline bool ImmutableTree::Node::isTerminator() { - return this==&terminator; - } - - /***/ - - template - typename ImmutableTree::Node * - ImmutableTree::Node::balance(Node *left, const value_type &value, Node *right) { - if (left->height > right->height + 2) { - Node *ll = left->left; - Node *lr = left->right; - if (ll->height >= lr->height) { - Node *nlr = new Node(lr->incref(), right, value); - Node *res = new Node(ll->incref(), nlr, left->value); - left->decref(); - return res; - } else { - Node *lrl = lr->left; - Node *lrr = lr->right; - Node *nll = new Node(ll->incref(), lrl->incref(), left->value); - Node *nlr = new Node(lrr->incref(), right, value); - Node *res = new Node(nll, nlr, lr->value); - left->decref(); - return res; - } - } else if (right->height > left->height + 2) { - Node *rl = right->left; - Node *rr = right->right; - if (rr->height >= rl->height) { - Node *nrl = new Node(left, rl->incref(), value); - Node *res = new Node(nrl, rr->incref(), right->value); - right->decref(); - return res; - } else { - Node *rll = rl->left; - Node *rlr = rl->right; - Node *nrl = new Node(left, rll->incref(), value); - Node *nrr = new Node(rlr->incref(), rr->incref(), right->value); - Node *res = new Node(nrl, nrr, rl->value); - right->decref(); - return res; - } - } else { - return new Node(left, right, value); - } - } - - template - size_t ImmutableTree::Node::size() { - if (isTerminator()) { - return 0; - } else { - return left->size() + 1 + right->size(); - } - } - - template - typename ImmutableTree::Node * - ImmutableTree::Node::popMin(value_type &valueOut) { - if (left->isTerminator()) { - valueOut = value; - return right->incref(); - } else { - return balance(left->popMin(valueOut), value, right->incref()); - } - } - - template - typename ImmutableTree::Node * - ImmutableTree::Node::popMax(value_type &valueOut) { - if (right->isTerminator()) { - valueOut = value; - return left->incref(); - } else { - return balance(left->incref(), value, right->popMax(valueOut)); - } - } - - template - typename ImmutableTree::Node * - ImmutableTree::Node::insert(const value_type &v) { - if (isTerminator()) { - return new Node(terminator.incref(), terminator.incref(), v); - } else { - if (key_compare()(key_of_value()(v), key_of_value()(value))) { - return balance(left->insert(v), value, right->incref()); - } else if (key_compare()(key_of_value()(value), key_of_value()(v))) { - return balance(left->incref(), value, right->insert(v)); - } else { - return incref(); - } - } - } - - template - typename ImmutableTree::Node * - ImmutableTree::Node::replace(const value_type &v) { - if (isTerminator()) { - return new Node(terminator.incref(), terminator.incref(), v); - } else { - if (key_compare()(key_of_value()(v), key_of_value()(value))) { - return balance(left->replace(v), value, right->incref()); - } else if (key_compare()(key_of_value()(value), key_of_value()(v))) { - return balance(left->incref(), value, right->replace(v)); - } else { - return new Node(left->incref(), right->incref(), v); - } - } - } - - template - typename ImmutableTree::Node * - ImmutableTree::Node::remove(const key_type &k) { - if (isTerminator()) { - return incref(); - } else { - if (key_compare()(k, key_of_value()(value))) { - return balance(left->remove(k), value, right->incref()); - } else if (key_compare()(key_of_value()(value), k)) { - return balance(left->incref(), value, right->remove(k)); - } else { - if (left->isTerminator()) { - return right->incref(); - } else if (right->isTerminator()) { - return left->incref(); - } else { - value_type min; - Node *nr = right->popMin(min); - return balance(left->incref(), min, nr); - } - } - } - } - - /***/ - - template - ImmutableTree::ImmutableTree() - : node(Node::terminator.incref()) { - } - - template - ImmutableTree::ImmutableTree(Node *_node) - : node(_node) { - } - - template - ImmutableTree::ImmutableTree(const ImmutableTree &s) - : node(s.node->incref()) { - } - - template - ImmutableTree::~ImmutableTree() { - node->decref(); - } - - template - ImmutableTree &ImmutableTree::operator=(const ImmutableTree &s) { - Node *n = s.node->incref(); - node->decref(); - node = n; - return *this; - } - - template - bool ImmutableTree::empty() const { - return node->isTerminator(); - } - - template - size_t ImmutableTree::count(const key_type &k) const { - Node *n = node; - while (!n->isTerminator()) { - key_type key = key_of_value()(n->value); - if (key_compare()(k, key)) { - n = n->left; - } else if (key_compare()(key, k)) { - n = n->right; - } else { - return 1; - } - } - return 0; - } - - template - const typename ImmutableTree::value_type * - ImmutableTree::lookup(const key_type &k) const { - Node *n = node; - while (!n->isTerminator()) { - key_type key = key_of_value()(n->value); - if (key_compare()(k, key)) { - n = n->left; - } else if (key_compare()(key, k)) { - n = n->right; - } else { - return &n->value; - } - } - return 0; - } - - template - const typename ImmutableTree::value_type * - ImmutableTree::lookup_previous(const key_type &k) const { - Node *n = node; - Node *result = 0; - while (!n->isTerminator()) { - key_type key = key_of_value()(n->value); - if (key_compare()(k, key)) { - n = n->left; - } else if (key_compare()(key, k)) { - result = n; - n = n->right; - } else { - return &n->value; - } - } - return result ? &result->value : 0; - } - - template - const typename ImmutableTree::value_type & - ImmutableTree::min() const { - Node *n = node; - assert(!n->isTerminator()); - while (!n->left->isTerminator()) n = n->left; - return n->value; - } - - template - const typename ImmutableTree::value_type & - ImmutableTree::max() const { - Node *n = node; - assert(!n->isTerminator()); - while (!n->right->isTerminator()) n = n->right; - return n->value; - } - - template - size_t ImmutableTree::size() const { - return node->size(); - } - - template - ImmutableTree - ImmutableTree::insert(const value_type &value) const { - return ImmutableTree(node->insert(value)); - } - - template - ImmutableTree - ImmutableTree::replace(const value_type &value) const { - return ImmutableTree(node->replace(value)); - } - - template - ImmutableTree - ImmutableTree::remove(const key_type &key) const { - return ImmutableTree(node->remove(key)); - } - - template - ImmutableTree - ImmutableTree::popMin(value_type &valueOut) const { - return ImmutableTree(node->popMin(valueOut)); - } - - template - ImmutableTree - ImmutableTree::popMax(value_type &valueOut) const { - return ImmutableTree(node->popMax(valueOut)); - } - - template - inline typename ImmutableTree::iterator - ImmutableTree::begin() const { - return iterator(node, true); - } - - template - inline typename ImmutableTree::iterator - ImmutableTree::end() const { - return iterator(node, false); - } - - template - inline typename ImmutableTree::iterator - ImmutableTree::find(const key_type &key) const { - iterator end(node,false), it = lower_bound(key); - if (it==end || key_compare()(key,key_of_value()(*it))) { - return end; - } else { - return it; - } - } - - template - inline typename ImmutableTree::iterator - ImmutableTree::lower_bound(const key_type &k) const { - // XXX ugh this doesn't have to be so ugly does it? - iterator it(node,false); - for (Node *root=node; !root->isTerminator();) { - it.stack.push_back(root); - if (key_compare()(k, key_of_value()(root->value))) { - root = root->left; - } else if (key_compare()(key_of_value()(root->value), k)) { - root = root->right; - } else { - return it; - } - } - // it is now beginning or first element < k - if (!it.stack.empty()) { - Node *last = it.stack.back(); - if (key_compare()(key_of_value()(last->value), k)) - ++it; - } - return it; - } - - template - typename ImmutableTree::iterator - ImmutableTree::upper_bound(const key_type &key) const { - iterator end(node,false),it = lower_bound(key); - if (it!=end && - !key_compare()(key,key_of_value()(*it))) // no need to loop, no duplicates - ++it; - return it; - } - -} - -#endif /* KLEE_IMMUTABLETREE_H */ diff --git a/include/klee/Internal/ADT/KTest.h b/include/klee/Internal/ADT/KTest.h deleted file mode 100644 index 5b5c45ef..00000000 --- a/include/klee/Internal/ADT/KTest.h +++ /dev/null @@ -1,61 +0,0 @@ -//===-- KTest.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_KTEST_H -#define KLEE_KTEST_H - -#ifdef __cplusplus -extern "C" { -#endif - - typedef struct KTestObject KTestObject; - struct KTestObject { - char *name; - unsigned numBytes; - unsigned char *bytes; - }; - - typedef struct KTest KTest; - struct KTest { - /* file format version */ - unsigned version; - - unsigned numArgs; - char **args; - - unsigned symArgvs; - unsigned symArgvLen; - - unsigned numObjects; - KTestObject *objects; - }; - - - /* returns the current .ktest file format version */ - unsigned kTest_getCurrentVersion(); - - /* return true iff file at path matches KTest header */ - int kTest_isKTestFile(const char *path); - - /* returns NULL on (unspecified) error */ - KTest* kTest_fromFile(const char *path); - - /* returns 1 on success, 0 on (unspecified) error */ - int kTest_toFile(KTest *, const char *path); - - /* returns total number of object bytes */ - unsigned kTest_numBytes(KTest *); - - void kTest_free(KTest *); - -#ifdef __cplusplus -} -#endif - -#endif /* KLEE_KTEST_H */ diff --git a/include/klee/Internal/ADT/MapOfSets.h b/include/klee/Internal/ADT/MapOfSets.h deleted file mode 100644 index b30934d8..00000000 --- a/include/klee/Internal/ADT/MapOfSets.h +++ /dev/null @@ -1,384 +0,0 @@ -//===-- MapOfSets.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_MAPOFSETS_H -#define KLEE_MAPOFSETS_H - -#include -#include -#include -#include - -// This should really be broken down into TreeOfSets on top of which -// SetOfSets and MapOfSets are easily implemeted. It should also be -// parameterized on the underlying set type. Neither are hard to do, -// just not worth it at the moment. -// -// I also broke some STLish conventions because I was bored. - -namespace klee { - - /** This implements the UBTree data structure (see Hoffmann and - Koehler, "A New Method to Index and Query Sets", IJCAI 1999) */ - template - class MapOfSets { - public: - class iterator; - - public: - MapOfSets(); - - void clear(); - - void insert(const std::set &set, const V &value); - - V *lookup(const std::set &set); - - iterator begin(); - iterator end(); - - void subsets(const std::set &set, - std::vector< std::pair, V> > &resultOut); - void supersets(const std::set &set, - std::vector< std::pair, V> > &resultOut); - - template - V *findSuperset(const std::set &set, const Predicate &p); - template - V *findSubset(const std::set &set, const Predicate &p); - - private: - class Node; - - Node root; - - template - void findSubsets(Node *n, - const std::set &accum, - Iterator begin, - Iterator end, - Vector &resultsOut); - template - void findSupersets(Node *n, - const std::set &accum, - Iterator begin, - Iterator end, - Vector &resultsOut); - template - V *findSuperset(Node *n, - typename std::set::iterator begin, - typename std::set::iterator end, - const Predicate &p); - template - V *findSubset(Node *n, - typename std::set::iterator begin, - typename std::set::iterator end, - const Predicate &p); - }; - - /***/ - - template - class MapOfSets::Node { - friend class MapOfSets; - friend class MapOfSets::iterator; - - public: - typedef std::map children_ty; - - V value; - - private: - bool isEndOfSet; - std::map children; - - public: - Node() : value(), isEndOfSet(false) {} - }; - - template - class MapOfSets::iterator { - typedef std::vector< typename std::map::iterator > stack_ty; - friend class MapOfSets; - private: - Node *root; - bool onEntry; - stack_ty stack; - - void step() { - if (onEntry) { - onEntry = false; - Node *n = stack.empty() ? root : &stack.back()->second; - while (!n->children.empty()) { - stack.push_back(n->children.begin()); - n = &stack.back()->second; - if (n->isEndOfSet) { - onEntry = true; - return; - } - } - } - - while (!stack.empty()) { - unsigned size = stack.size(); - Node *at = size==1 ? root : &stack[size-2]->second; - typename std::map::iterator &cur = stack.back(); - ++cur; - if (cur==at->children.end()) { - stack.pop_back(); - } else { - Node *n = &cur->second; - - while (!n->isEndOfSet) { - assert(!n->children.empty()); - stack.push_back(n->children.begin()); - n = &stack.back()->second; - } - - onEntry = true; - break; - } - } - } - - public: - // end() - iterator() : onEntry(false) {} - // begin() - iterator(Node *_n) : root(_n), onEntry(true) { - if (!root->isEndOfSet) - step(); - } - - const std::pair, const V> operator*() { - assert(onEntry || !stack.empty()); - std::set s; - for (typename stack_ty::iterator it = stack.begin(), ie = stack.end(); - it != ie; ++it) - s.insert((*it)->first); - Node *n = stack.empty() ? root : &stack.back()->second; - return std::make_pair(s, n->value); - } - - bool operator==(const iterator &b) { - return onEntry==b.onEntry && stack==b.stack; - } - bool operator!=(const iterator &b) { - return !(*this==b); - } - - iterator &operator++() { - step(); - return *this; - } - }; - - /***/ - - template - MapOfSets::MapOfSets() {} - - template - void MapOfSets::insert(const std::set &set, const V &value) { - Node *n = &root; - for (auto const& element : set) { - n = &n->children.insert(std::make_pair(element, Node())).first->second; - } - n->isEndOfSet = true; - n->value = value; - } - - template - V *MapOfSets::lookup(const std::set &set) { - Node *n = &root; - for (typename std::set::const_iterator it = set.begin(), ie = set.end(); - it != ie; ++it) { - typename Node::children_ty::iterator kit = n->children.find(*it); - if (kit==n->children.end()) { - return 0; - } else { - n = &kit->second; - } - } - if (n->isEndOfSet) { - return &n->value; - } else { - return 0; - } - } - - template - typename MapOfSets::iterator - MapOfSets::begin() { return iterator(&root); } - - template - typename MapOfSets::iterator - MapOfSets::end() { return iterator(); } - - template - template - void MapOfSets::findSubsets(Node *n, - const std::set &accum, - Iterator begin, - Iterator end, - Vector &resultsOut) { - if (n->isEndOfSet) { - resultsOut.push_back(std::make_pair(accum, n->value)); - } - - for (Iterator it=begin; it!=end;) { - K elt = *it; - typename Node::children_ty::iterator kit = n->children.find(elt); - it++; - if (kit!=n->children.end()) { - std::set nacc = accum; - nacc.insert(elt); - findSubsets(&kit->second, nacc, it, end, resultsOut); - } - } - } - - template - void MapOfSets::subsets(const std::set &set, - std::vector< std::pair, - V> > &resultOut) { - findSubsets(&root, std::set(), set.begin(), set.end(), resultOut); - } - - template - template - void MapOfSets::findSupersets(Node *n, - const std::set &accum, - Iterator begin, - Iterator end, - Vector &resultsOut) { - if (begin==end) { - if (n->isEndOfSet) - resultsOut.push_back(std::make_pair(accum, n->value)); - for (typename Node::children_ty::iterator it = n->children.begin(), - ie = n->children.end(); it != ie; ++it) { - std::set nacc = accum; - nacc.insert(it->first); - findSupersets(&it->second, nacc, begin, end, resultsOut); - } - } else { - K elt = *begin; - Iterator next = begin; - ++next; - for (typename Node::children_ty::iterator it = n->children.begin(), - ie = n->children.end(); it != ie; ++it) { - std::set nacc = accum; - nacc.insert(it->first); - if (elt==it->first) { - findSupersets(&it->second, nacc, next, end, resultsOut); - } else if (it->firstsecond, nacc, begin, end, resultsOut); - } else { - break; - } - } - } - } - - template - void MapOfSets::supersets(const std::set &set, - std::vector< std::pair, V> > &resultOut) { - findSupersets(&root, std::set(), set.begin(), set.end(), resultOut); - } - - template - template - V *MapOfSets::findSubset(Node *n, - typename std::set::iterator begin, - typename std::set::iterator end, - const Predicate &p) { - if (n->isEndOfSet && p(n->value)) { - return &n->value; - } else if (begin==end) { - return 0; - } else { - typename Node::children_ty::iterator kend = n->children.end(); - typename Node::children_ty::iterator - kbegin = n->children.lower_bound(*begin); - typename std::set::iterator it = begin; - if (kbegin==kend) - return 0; - for (;;) { // kbegin!=kend && *it <= kbegin->first - while (*it < kbegin->first) { - ++it; - if (it==end) - return 0; - } - if (*it == kbegin->first) { - ++it; - V *res = findSubset(&kbegin->second, it, end, p); - if (res || it==end) - return res; - } - while (kbegin->first < *it) { - ++kbegin; - if (kbegin==kend) - return 0; - } - } - } - } - - template - template - V *MapOfSets::findSuperset(Node *n, - typename std::set::iterator begin, - typename std::set::iterator end, - const Predicate &p) { - if (begin==end) { - if (n->isEndOfSet && p(n->value)) - return &n->value; - for (typename Node::children_ty::iterator it = n->children.begin(), - ie = n->children.end(); it != ie; ++it) { - V *res = findSuperset(&it->second, begin, end, p); - if (res) return res; - } - } else { - typename Node::children_ty::iterator kmid = - n->children.lower_bound(*begin); - for (typename Node::children_ty::iterator it = n->children.begin(), - ie = n->children.end(); it != ie; ++it) { - V *res = findSuperset(&it->second, begin, end, p); - if (res) return res; - } - if (kmid!=n->children.end() && *begin==kmid->first) { - V *res = findSuperset(&kmid->second, ++begin, end, p); - if (res) return res; - } - } - return 0; - } - - template - template - V *MapOfSets::findSuperset(const std::set &set, const Predicate &p) { - return findSuperset(&root, set.begin(), set.end(), p); - } - - template - template - V *MapOfSets::findSubset(const std::set &set, const Predicate &p) { - return findSubset(&root, set.begin(), set.end(), p); - } - - template - void MapOfSets::clear() { - root.isEndOfSet = false; - root.value = V(); - root.children.clear(); - } - -} - -#endif /* KLEE_MAPOFSETS_H */ diff --git a/include/klee/Internal/ADT/RNG.h b/include/klee/Internal/ADT/RNG.h deleted file mode 100644 index 5ea375b5..00000000 --- a/include/klee/Internal/ADT/RNG.h +++ /dev/null @@ -1,50 +0,0 @@ -//===-- RNG.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_RNG_H -#define KLEE_RNG_H - -namespace klee { - class RNG { - private: - /* Period parameters */ - static const int N = 624; - static const int M = 397; - static const unsigned int MATRIX_A = 0x9908b0dfUL; /* constant vector a */ - static const unsigned int UPPER_MASK = 0x80000000UL; /* most significant w-r bits */ - static const unsigned int LOWER_MASK = 0x7fffffffUL; /* least significant r bits */ - - private: - unsigned int mt[N]; /* the array for the state vector */ - int mti; - - public: - RNG(unsigned int seed=5489UL); - - void seed(unsigned int seed); - - /* generates a random number on [0,0xffffffff]-interval */ - unsigned int getInt32(); - /* generates a random number on [0,0x7fffffff]-interval */ - int getInt31(); - /* generates a random number on [0,1]-real-interval */ - double getDoubleLR(); - float getFloatLR(); - /* generates a random number on [0,1)-real-interval */ - double getDoubleL(); - float getFloatL(); - /* generates a random number on (0,1)-real-interval */ - double getDouble(); - float getFloat(); - /* generators a random flop */ - bool getBool(); - }; -} - -#endif /* KLEE_RNG_H */ diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h deleted file mode 100644 index 32c856c9..00000000 --- a/include/klee/Internal/ADT/TreeStream.h +++ /dev/null @@ -1,76 +0,0 @@ -//===-- TreeStream.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_TREESTREAM_H -#define KLEE_TREESTREAM_H - -#include -#include - -namespace klee { - - typedef unsigned TreeStreamID; - class TreeOStream; - - class TreeStreamWriter { - static const unsigned bufferSize = 4*4096; - - friend class TreeOStream; - - private: - char buffer[bufferSize]; - unsigned lastID, bufferCount; - - std::string path; - std::ofstream *output; - unsigned ids; - - void write(TreeOStream &os, const char *s, unsigned size); - void flushBuffer(); - - public: - TreeStreamWriter(const std::string &_path); - ~TreeStreamWriter(); - - bool good(); - - TreeOStream open(); - TreeOStream open(const TreeOStream &node); - - void flush(); - - // hack, to be replace by proper stream capabilities - void readStream(TreeStreamID id, - std::vector &out); - }; - - class TreeOStream { - friend class TreeStreamWriter; - - private: - TreeStreamWriter *writer; - unsigned id; - - TreeOStream(TreeStreamWriter &_writer, unsigned _id); - - public: - TreeOStream(); - ~TreeOStream(); - - unsigned getID() const; - - void write(const char *buffer, unsigned size); - - TreeOStream &operator<<(const std::string &s); - - void flush(); - }; -} - -#endif /* KLEE_TREESTREAM_H */ diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h deleted file mode 100644 index c7d9ae18..00000000 --- a/include/klee/Internal/Module/Cell.h +++ /dev/null @@ -1,23 +0,0 @@ -//===-- Cell.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_CELL_H -#define KLEE_CELL_H - -#include "klee/Expr/Expr.h" - -namespace klee { - class MemoryObject; - - struct Cell { - ref value; - }; -} - -#endif /* KLEE_CELL_H */ diff --git a/include/klee/Internal/Module/InstructionInfoTable.h b/include/klee/Internal/Module/InstructionInfoTable.h deleted file mode 100644 index e3684802..00000000 --- a/include/klee/Internal/Module/InstructionInfoTable.h +++ /dev/null @@ -1,77 +0,0 @@ -//===-- InstructionInfoTable.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_INSTRUCTIONINFOTABLE_H -#define KLEE_INSTRUCTIONINFOTABLE_H - -#include -#include -#include -#include - -namespace llvm { - class Function; - class Instruction; - class Module; -} - -namespace klee { - - /* Stores debug information for a KInstruction */ - struct InstructionInfo { - unsigned id; - const std::string &file; - unsigned line; - unsigned column; - unsigned assemblyLine; - - public: - InstructionInfo(unsigned _id, const std::string &_file, unsigned _line, - unsigned _column, unsigned _assemblyLine) - : id(_id), file(_file), line(_line), column(_column), - assemblyLine(_assemblyLine) {} - }; - - /* Stores debug information for a KInstruction */ - struct FunctionInfo { - unsigned id; - const std::string &file; - unsigned line; - uint64_t assemblyLine; - - public: - FunctionInfo(unsigned _id, const std::string &_file, unsigned _line, - uint64_t _assemblyLine) - : id(_id), file(_file), line(_line), assemblyLine(_assemblyLine) {} - - FunctionInfo(const FunctionInfo &) = delete; - FunctionInfo &operator=(FunctionInfo const &) = delete; - - FunctionInfo(FunctionInfo &&) = default; - }; - - class InstructionInfoTable { - std::unordered_map> - infos; - std::unordered_map> - functionInfos; - std::vector> internedStrings; - - public: - InstructionInfoTable(const llvm::Module &m); - - unsigned getMaxID() const; - const InstructionInfo &getInfo(const llvm::Instruction &) const; - const FunctionInfo &getFunctionInfo(const llvm::Function &) const; - }; - -} - -#endif /* KLEE_INSTRUCTIONINFOTABLE_H */ diff --git a/include/klee/Internal/Module/KInstIterator.h b/include/klee/Internal/Module/KInstIterator.h deleted file mode 100644 index e5bd37f8..00000000 --- a/include/klee/Internal/Module/KInstIterator.h +++ /dev/null @@ -1,42 +0,0 @@ -//===-- KInstIterator.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_KINSTITERATOR_H -#define KLEE_KINSTITERATOR_H - -namespace klee { - struct KInstruction; - - class KInstIterator { - KInstruction **it; - - public: - KInstIterator() : it(0) {} - KInstIterator(KInstruction **_it) : it(_it) {} - - bool operator==(const KInstIterator &b) const { - return it==b.it; - } - bool operator!=(const KInstIterator &b) const { - return !(*this == b); - } - - KInstIterator &operator++() { - ++it; - return *this; - } - - operator KInstruction*() const { return it ? *it : 0;} - operator bool() const { return it != 0; } - - KInstruction *operator ->() const { return *it; } - }; -} // End klee namespace - -#endif /* KLEE_KINSTITERATOR_H */ diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h deleted file mode 100644 index d641b4e3..00000000 --- a/include/klee/Internal/Module/KInstruction.h +++ /dev/null @@ -1,64 +0,0 @@ -//===-- KInstruction.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_KINSTRUCTION_H -#define KLEE_KINSTRUCTION_H - -#include "klee/Config/Version.h" -#include "klee/Internal/Module/InstructionInfoTable.h" - -#include "llvm/Support/DataTypes.h" -#include "llvm/Support/raw_ostream.h" - -#include - -namespace llvm { - class Instruction; -} - -namespace klee { - class Executor; - struct InstructionInfo; - class KModule; - - - /// KInstruction - Intermediate instruction representation used - /// during execution. - struct KInstruction { - llvm::Instruction *inst; - const InstructionInfo *info; - - /// Value numbers for each operand. -1 is an invalid value, - /// otherwise negative numbers are indices (negated and offset by - /// 2) into the module constant table and positive numbers are - /// register indices. - int *operands; - /// Destination register index. - unsigned dest; - - public: - virtual ~KInstruction(); - std::string getSourceLocation() const; - - }; - - struct KGEPInstruction : KInstruction { - /// indices - The list of variable sized adjustments to add to the pointer - /// operand to execute the instruction. The first element is the operand - /// index into the GetElementPtr instruction, and the second element is the - /// element size to multiple that index by. - std::vector< std::pair > indices; - - /// offset - A constant offset to add to the pointer operand to execute the - /// instruction. - uint64_t offset; - }; -} - -#endif /* KLEE_KINSTRUCTION_H */ diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h deleted file mode 100644 index 89606e2e..00000000 --- a/include/klee/Internal/Module/KModule.h +++ /dev/null @@ -1,153 +0,0 @@ -//===-- KModule.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_KMODULE_H -#define KLEE_KMODULE_H - -#include "klee/Config/Version.h" -#include "klee/Interpreter.h" - -#include "llvm/ADT/ArrayRef.h" - -#include -#include -#include -#include - -namespace llvm { - class BasicBlock; - class Constant; - class Function; - class Instruction; - class Module; - class DataLayout; -} - -namespace klee { - struct Cell; - class Executor; - class Expr; - class InterpreterHandler; - class InstructionInfoTable; - struct KInstruction; - class KModule; - template class ref; - - struct KFunction { - llvm::Function *function; - - unsigned numArgs, numRegisters; - - unsigned numInstructions; - KInstruction **instructions; - - std::map basicBlockEntry; - - /// Whether instructions in this function should count as - /// "coverable" for statistics and search heuristics. - bool trackCoverage; - - public: - explicit KFunction(llvm::Function*, KModule *); - KFunction(const KFunction &) = delete; - KFunction &operator=(const KFunction &) = delete; - - ~KFunction(); - - unsigned getArgRegister(unsigned index) { return index; } - }; - - - class KConstant { - public: - /// Actual LLVM constant this represents. - llvm::Constant* ct; - - /// The constant ID. - unsigned id; - - /// First instruction where this constant was encountered, or NULL - /// if not applicable/unavailable. - KInstruction *ki; - - KConstant(llvm::Constant*, unsigned, KInstruction*); - }; - - - class KModule { - public: - std::unique_ptr module; - std::unique_ptr targetData; - - // Our shadow versions of LLVM structures. - std::vector> functions; - std::map functionMap; - - // Functions which escape (may be called indirectly) - // XXX change to KFunction - std::set escapingFunctions; - - std::unique_ptr infos; - - std::vector constants; - std::map> constantMap; - KConstant* getKConstant(const llvm::Constant *c); - - std::unique_ptr constantTable; - - // Functions which are part of KLEE runtime - std::set internalFunctions; - - private: - // Mark function with functionName as part of the KLEE runtime - void addInternalFunction(const char* functionName); - - public: - KModule() = default; - - /// Optimise and prepare module such that KLEE can execute it - // - void optimiseAndPrepare(const Interpreter::ModuleOptions &opts, - llvm::ArrayRef); - - /// Manifest the generated module (e.g. assembly.ll, output.bc) and - /// prepares KModule - /// - /// @param ih - /// @param forceSourceOutput true if assembly.ll should be created - /// - // FIXME: ihandler should not be here - void manifest(InterpreterHandler *ih, bool forceSourceOutput); - - /// Link the provided modules together as one KLEE module. - /// - /// If the entry point is empty, all modules are linked together. - /// If the entry point is not empty, all modules are linked which resolve - /// the dependencies of the module containing entryPoint - /// - /// @param modules list of modules to be linked together - /// @param entryPoint name of the function which acts as the program's entry - /// point - /// @return true if at least one module has been linked in, false if nothing - /// changed - bool link(std::vector> &modules, - const std::string &entryPoint); - - void instrument(const Interpreter::ModuleOptions &opts); - - /// Return an id for the given constant, creating a new one if necessary. - unsigned getConstantID(llvm::Constant *c, KInstruction* ki); - - /// Run passes that check if module is valid LLVM IR and if invariants - /// expected by KLEE's Executor hold. - void checkModule(); - }; -} // End klee namespace - -#endif /* KLEE_KMODULE_H */ diff --git a/include/klee/Internal/README.txt b/include/klee/Internal/README.txt deleted file mode 100644 index 9cedb653..00000000 --- a/include/klee/Internal/README.txt +++ /dev/null @@ -1,3 +0,0 @@ -This directory holds header files for things which are exposed as part -of the internal API of a library, but shouldn't be exposed to -externally. diff --git a/include/klee/Internal/Support/CompressionStream.h b/include/klee/Internal/Support/CompressionStream.h deleted file mode 100644 index bc9119dd..00000000 --- a/include/klee/Internal/Support/CompressionStream.h +++ /dev/null @@ -1,46 +0,0 @@ -//===-- CompressionStream.h --------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_COMPRESSIONSTREAM_H -#define KLEE_COMPRESSIONSTREAM_H - -#include "llvm/Support/raw_ostream.h" -#include "zlib.h" - -namespace klee { -const size_t BUFSIZE = 128 * 1024; - -class compressed_fd_ostream : public llvm::raw_ostream { - int FD; - uint8_t buffer[BUFSIZE]; - z_stream strm; - uint64_t pos; - - /// write_impl - See raw_ostream::write_impl. - virtual void write_impl(const char *Ptr, size_t Size); - void write_file(const char *Ptr, size_t Size); - - virtual uint64_t current_pos() const { return pos; } - - void flush_compressed_data(); - void writeFullCompressedData(); - -public: - /// compressed_fd_ostream - Open the specified file for writing. If an error - /// occurs, information about the error is put into ErrorInfo, and the stream - /// should be immediately destroyed; the string will be empty if no error - /// occurred. This allows optional flags to control how the file will be - /// opened. - compressed_fd_ostream(const std::string &Filename, std::string &ErrorInfo); - - ~compressed_fd_ostream(); -}; -} - -#endif /* KLEE_COMPRESSIONSTREAM_H */ diff --git a/include/klee/Internal/Support/Debug.h b/include/klee/Internal/Support/Debug.h deleted file mode 100644 index 0fe7906a..00000000 --- a/include/klee/Internal/Support/Debug.h +++ /dev/null @@ -1,27 +0,0 @@ -//===-- Debug.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_DEBUG_H -#define KLEE_DEBUG_H - -#include "klee/Config/config.h" -#include "llvm/Support/Debug.h" - -// We define wrappers around the LLVM DEBUG macros that are conditionalized on -// whether the LLVM we are building against has the symbols needed by these -// checks. - -#ifdef ENABLE_KLEE_DEBUG -#define KLEE_DEBUG_WITH_TYPE(TYPE, X) DEBUG_WITH_TYPE(TYPE, X) -#else -#define KLEE_DEBUG_WITH_TYPE(TYPE, X) do { } while (0) -#endif -#define KLEE_DEBUG(X) KLEE_DEBUG_WITH_TYPE(DEBUG_TYPE, X) - -#endif /* KLEE_DEBUG_H */ diff --git a/include/klee/Internal/Support/ErrorHandling.h b/include/klee/Internal/Support/ErrorHandling.h deleted file mode 100644 index 92762c03..00000000 --- a/include/klee/Internal/Support/ErrorHandling.h +++ /dev/null @@ -1,51 +0,0 @@ -//===-- ErrorHandling.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_ERRORHANDLING_H -#define KLEE_ERRORHANDLING_H - -#ifdef __CYGWIN__ -#ifndef WINDOWS -#define WINDOWS -#endif -#endif - -#include - -namespace klee { - -extern FILE *klee_warning_file; -extern FILE *klee_message_file; - -/// Print "KLEE: ERROR: " followed by the msg in printf format and a -/// newline on stderr and to warnings.txt, then exit with an error. -void klee_error(const char *msg, ...) - __attribute__((format(printf, 1, 2), noreturn)); - -/// Print "KLEE: " followed by the msg in printf format and a -/// newline on stderr and to messages.txt. -void klee_message(const char *msg, ...) __attribute__((format(printf, 1, 2))); - -/// Print "KLEE: " followed by the msg in printf format and a -/// newline to messages.txt. -void klee_message_to_file(const char *msg, ...) - __attribute__((format(printf, 1, 2))); - -/// Print "KLEE: WARNING: " followed by the msg in printf format and a -/// newline on stderr and to warnings.txt. -void klee_warning(const char *msg, ...) __attribute__((format(printf, 1, 2))); - -/// Print "KLEE: WARNING: " followed by the msg in printf format and a -/// newline on stderr and to warnings.txt. However, the warning is only -/// printed once for each unique (id, msg) pair (as pointers). -void klee_warning_once(const void *id, const char *msg, ...) - __attribute__((format(printf, 2, 3))); -} - -#endif /* KLEE_ERRORHANDLING_H */ diff --git a/include/klee/Internal/Support/FileHandling.h b/include/klee/Internal/Support/FileHandling.h deleted file mode 100644 index 90ce20b3..00000000 --- a/include/klee/Internal/Support/FileHandling.h +++ /dev/null @@ -1,27 +0,0 @@ -//===-- FileHandling.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_FILEHANDLING_H -#define KLEE_FILEHANDLING_H - -#include "llvm/Support/raw_ostream.h" -#include -#include - -namespace klee { -std::unique_ptr -klee_open_output_file(const std::string &path, std::string &error); - -#ifdef HAVE_ZLIB_H -std::unique_ptr -klee_open_compressed_output_file(const std::string &path, std::string &error); -#endif -} // namespace klee - -#endif /* KLEE_FILEHANDLING_H */ diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h deleted file mode 100644 index 37392576..00000000 --- a/include/klee/Internal/Support/FloatEvaluation.h +++ /dev/null @@ -1,263 +0,0 @@ -//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -// FIXME: Ditch this and use APFloat. - -#ifndef KLEE_FLOATEVALUATION_H -#define KLEE_FLOATEVALUATION_H - -#include "klee/util/Bits.h" //bits64::truncateToNBits -#include "IntEvaluation.h" //ints::sext - -#include "llvm/Support/ErrorHandling.h" -#include "llvm/Support/MathExtras.h" - -#include - -namespace klee { -namespace floats { - -// ********************************** // -// *** Pack uint64_t into FP types ** // -// ********************************** // - -// interpret the 64 bits as a double instead of a uint64_t -inline double UInt64AsDouble( uint64_t bits ) { - double ret; - assert( sizeof(bits) == sizeof(ret) ); - memcpy( &ret, &bits, sizeof bits ); - return ret; -} - -// interpret the first 32 bits as a float instead of a uint64_t -inline float UInt64AsFloat( uint64_t bits ) { - uint32_t tmp = bits; // ensure that we read correct bytes - float ret; - assert( sizeof(tmp) == sizeof(ret) ); - memcpy( &ret, &tmp, sizeof tmp ); - return ret; -} - - -// ********************************** // -// *** Pack FP types into uint64_t ** // -// ********************************** // - -// interpret the 64 bits as a uint64_t instead of a double -inline uint64_t DoubleAsUInt64( double d ) { - uint64_t ret; - assert( sizeof(d) == sizeof(ret) ); - memcpy( &ret, &d, sizeof d ); - return ret; -} - -// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s) -inline uint64_t FloatAsUInt64( float f ) { - uint32_t tmp; - assert( sizeof(tmp) == sizeof(f) ); - memcpy( &tmp, &f, sizeof f ); - return (uint64_t)tmp; -} - - -// ********************************** // -// ************ Constants *********** // -// ********************************** // - -const unsigned FLT_BITS = 32; -const unsigned DBL_BITS = 64; - - - -// ********************************** // -// ***** LLVM Binary Operations ***** // -// ********************************** // - -// add of l and r -inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) + UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// difference of l and r -inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) - UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// product of l and r -inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) * UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// signed divide of l by r -inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) / UInt64AsFloat(r)), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// signed modulo of l by r -inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l), UInt64AsFloat(r)) ), FLT_BITS); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - - -// ********************************** // -// *** LLVM Comparison Operations *** // -// ********************************** // - -// determine if l represents NaN -inline bool isNaN(uint64_t l, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: - return std::isnan(UInt64AsFloat(l)); - case DBL_BITS: - return std::isnan(UInt64AsDouble(l)); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) == UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) != UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) < UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) <= UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) > UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) { - switch( inWidth ) { - case FLT_BITS: return UInt64AsFloat(l) >= UInt64AsFloat(r); - case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - - -// ********************************** // -// *** LLVM Conversion Operations *** // -// ********************************** // - -// truncation of l (which must be a double) to float (casts a double to a float) -inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { - // FIXME: Investigate this, should this not happen? Was a quick - // patch for busybox. - if (inWidth==64 && outWidth==64) { - return l; - } else { - assert(inWidth==64 && "can only truncate from a 64-bit double"); - assert(outWidth==32 && "can only truncate to a 32-bit float"); - float trunc = (float)UInt64AsDouble(l); - return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth); - } -} - -// extension of l (which must be a float) to double (casts a float to a double) -inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) { - // FIXME: Investigate this, should this not happen? Was a quick - // patch for busybox. - if (inWidth==64 && outWidth==64) { - return l; - } else { - assert(inWidth==32 && "can only extend from a 32-bit float"); - assert(outWidth==64 && "can only extend to a 64-bit double"); - double ext = (double)UInt64AsFloat(l); - return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth); - } -} - -// conversion of l to an unsigned integer, rounding towards zero -inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l), outWidth ); - case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth ); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// conversion of l to a signed integer, rounding towards zero -inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { - switch( inWidth ) { - case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l), outWidth); - case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// conversion of l, interpreted as an unsigned int, to a floating point number -inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) { - switch( outWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l), outWidth); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -// conversion of l, interpreted as a signed int, to a floating point number -inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) { - switch( outWidth ) { - case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth); - case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth); - default: llvm::report_fatal_error("unsupported floating point width"); - } -} - -} // end namespace ints -} // end namespace klee - -#endif /* KLEE_FLOATEVALUATION_H */ diff --git a/include/klee/Internal/Support/IntEvaluation.h b/include/klee/Internal/Support/IntEvaluation.h deleted file mode 100644 index 27a8daf0..00000000 --- a/include/klee/Internal/Support/IntEvaluation.h +++ /dev/null @@ -1,164 +0,0 @@ -//===-- IntEvaluation.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_INTEVALUATION_H -#define KLEE_INTEVALUATION_H - -#include "klee/util/Bits.h" - -#define MAX_BITS (sizeof(uint64_t) * 8) - -// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is -// between making trunc/zext/sext fast and making operations that depend -// on the invalid bits being 0 fast. - -namespace klee { -namespace ints { - -// add of l and r -inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l + r, inWidth); -} - -// difference of l and r -inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l - r, inWidth); -} - -// product of l and r -inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l * r, inWidth); -} - -// truncation of l to outWidth bits -inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { - return bits64::truncateToNBits(l, outWidth); -} - -// zero-extension of l from inWidth to outWidth bits -inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) { - return l; -} - -// sign-extension of l from inWidth to outWidth bits -inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) { - uint32_t numInvalidBits = MAX_BITS - inWidth; - return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth); -} - -// unsigned divide of l by r -inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l / r, inWidth); -} - -// unsigned mod of l by r -inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) { - return bits64::truncateToNBits(l % r, inWidth); -} - -// signed divide of l by r -inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) { - // sign extend operands so that signed operation on 64-bits works correctly - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return bits64::truncateToNBits(sl / sr, inWidth); -} - -// signed mod of l by r -inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) { - // sign extend operands so that signed operation on 64-bits works correctly - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return bits64::truncateToNBits(sl % sr, inWidth); -} - -// arithmetic shift right of l by r bits -inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - return bits64::truncateToNBits(sl >> shift, inWidth); -} - -// logical shift right of l by r bits -inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) { - return l >> shift; -} - -// shift left of l by r bits -inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) { - return bits64::truncateToNBits(l << shift, inWidth); -} - -// logical AND of l and r -inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) { - return l & r; -} - -// logical OR of l and r -inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) { - return l | r; -} - -// logical XOR of l and r -inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) { - return l ^ r; -} - -// comparison operations -inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { - return l == r; -} - -inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { - return l != r; -} - -inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) { - return l < r; -} - -inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) { - return l <= r; -} - -inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) { - return l > r; -} - -inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) { - return l >= r; -} - -inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl < sr; -} - -inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl <= sr; -} - -inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl > sr; -} - -inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) { - int64_t sl = sext(l, MAX_BITS, inWidth); - int64_t sr = sext(r, MAX_BITS, inWidth); - return sl >= sr; -} - -} // end namespace ints -} // end namespace klee - -#endif /* KLEE_INTEVALUATION_H */ diff --git a/include/klee/Internal/Support/ModuleUtil.h b/include/klee/Internal/Support/ModuleUtil.h deleted file mode 100644 index e80fc673..00000000 --- a/include/klee/Internal/Support/ModuleUtil.h +++ /dev/null @@ -1,70 +0,0 @@ -//===-- ModuleUtil.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_MODULEUTIL_H -#define KLEE_MODULEUTIL_H - -#include "klee/Config/Version.h" - -#include "llvm/IR/CallSite.h" -#include "llvm/IR/Module.h" - -#include -#include -#include - -namespace klee { - -/// Links all the modules together into one and returns it. -/// -/// All the modules which are used for resolving entities are freed, -/// all the remaining ones are preserved. -/// -/// @param modules List of modules to link together: if resolveOnly true, -/// everything is linked against the first entry. -/// @param entryFunction if set, missing functions of the module containing the -/// entry function will be solved. -/// @return final module or null in this case errorMsg is set -std::unique_ptr -linkModules(std::vector> &modules, - llvm::StringRef entryFunction, std::string &errorMsg); - -/// Return the Function* target of a Call or Invoke instruction, or -/// null if it cannot be determined (should be only for indirect -/// calls, although complicated constant expressions might be -/// another possibility). -/// -/// If `moduleIsFullyLinked` is set to true it will be assumed that the -/// module containing the `llvm::CallSite` is fully linked. This assumption -/// allows resolution of functions that are marked as overridable. -llvm::Function *getDirectCallTarget(llvm::CallSite, bool moduleIsFullyLinked); - -/// Return true iff the given Function value is used in something -/// other than a direct call (or a constant expression that -/// terminates in a direct call). -bool functionEscapes(const llvm::Function *f); - -/// Loads the file libraryName and reads all possible modules out of it. -/// -/// Different file types are possible: -/// * .bc binary file -/// * .ll IR file -/// * .a archive containing .bc and .ll files -/// -/// @param libraryName library to read -/// @param modules contains extracted modules -/// @param errorMsg contains the error description in case the file could not be -/// loaded -/// @return true if successful otherwise false -bool loadFile(const std::string &libraryName, llvm::LLVMContext &context, - std::vector> &modules, - std::string &errorMsg); -} - -#endif /* KLEE_MODULEUTIL_H */ diff --git a/include/klee/Internal/Support/PrintVersion.h b/include/klee/Internal/Support/PrintVersion.h deleted file mode 100644 index fbd20e39..00000000 --- a/include/klee/Internal/Support/PrintVersion.h +++ /dev/null @@ -1,25 +0,0 @@ -//===-- PrintVersion.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_PRINTVERSION_H -#define KLEE_PRINTVERSION_H - -#include "llvm/Support/raw_ostream.h" - -#include "klee/Config/Version.h" - -namespace klee { -#if LLVM_VERSION_CODE >= LLVM_VERSION(6, 0) - void printVersion(llvm::raw_ostream &OS); -#else - void printVersion(); -#endif -} - -#endif /* KLEE_PRINTVERSION_H */ diff --git a/include/klee/Internal/Support/Timer.h b/include/klee/Internal/Support/Timer.h deleted file mode 100644 index 30b1b758..00000000 --- a/include/klee/Internal/Support/Timer.h +++ /dev/null @@ -1,96 +0,0 @@ -//===-- Timer.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_TIMER_H -#define KLEE_TIMER_H - -#include "klee/Internal/System/Time.h" - -#include "llvm/ADT/SmallVector.h" - -#include -#include - -namespace klee { - - /** - * A WallTimer stores its creation time. - */ - class WallTimer { - const time::Point start; - public: - WallTimer(); - - /// Return the delta since the timer was created - time::Span delta() const; - }; - - - /** - * A Timer repeatedly executes a `callback` after a specified `interval`. - * An object of this class is _passive_ and only keeps track of the next invocation time. - * _Passive_ means, that it has to be `invoke`d by an external caller with the current time. - * Only when the time span between the current time and the last invocation exceeds the - * specified `interval`, the `callback` will be executed. - * Multiple timers are typically managed by a TimerGroup. - */ - class Timer { - /// Approximate interval between callback invocations. - time::Span interval; - /// Wall time for next invocation. - time::Point nextInvocationTime; - /// The event callback. - std::function run; - public: - /// \param interval The time span between callback invocations. - /// \param callback The event callback. - Timer(const time::Span &interval, std::function &&callback); - - /// Return specified `interval` between invocations. - time::Span getInterval() const; - /// Execute `callback` if invocation time exceeded. - void invoke(const time::Point ¤tTime); - /// Set new invocation time to `currentTime + interval`. - void reset(const time::Point ¤tTime); - }; - - - /** - * A TimerGroup manages multiple timers. - * - * TimerGroup simplifies the handling of multiple Timer objects by offering a unifying - * Timer-like interface. Additionally, it serves as a barrier and prevents timers from - * being invoked too often by defining a minimum invocation interval (MI). - * All registered timer intervals should be larger than MI and also be multiples of MI. - * Similar to Timer, a TimerGroup is _passive_ and needs to be `invoke`d by an external - * caller. - */ - class TimerGroup { - /// Registered timers. - llvm::SmallVector, 4> timers; - /// Timer that invokes all registered timers after minimum interval. - Timer invocationTimer; - /// Time of last `invoke` call. - time::Point currentTime; - public: - /// \param minInterval The minimum interval between invocations of registered timers. - explicit TimerGroup(const time::Span &minInterval); - - /// Add a timer to be executed periodically. - /// - /// \param timer The timer object to register. - void add(std::unique_ptr timer); - /// Invoke registered timers with current time only if minimum interval exceeded. - void invoke(); - /// Reset all timers. - void reset(); - }; - -} // klee -#endif /* KLEE_TIMER_H */ diff --git a/include/klee/Internal/System/MemoryUsage.h b/include/klee/Internal/System/MemoryUsage.h deleted file mode 100644 index c3cf3c74..00000000 --- a/include/klee/Internal/System/MemoryUsage.h +++ /dev/null @@ -1,21 +0,0 @@ -//===-- MemoryUsage.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_MEMORYUSAGE_H -#define KLEE_MEMORYUSAGE_H - -#include - -namespace klee { - namespace util { - size_t GetTotalMallocUsage(); - } -} - -#endif /* KLEE_MEMORYUSAGE_H */ diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h deleted file mode 100644 index 2ebebdfd..00000000 --- a/include/klee/Internal/System/Time.h +++ /dev/null @@ -1,120 +0,0 @@ -//===-- Time.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_TIME_H -#define KLEE_TIME_H - -#include "llvm/Support/raw_ostream.h" - -#include -#include -#include - -namespace klee { - namespace time { - - /// The klee::time namespace offers various functions to measure the time (`getWallTime`) - /// and to get timing information for the current KLEE process (`getUserTime`). - /// This implementation is based on `std::chrono` and uses time points and time spans. - /// For KLEE statistics, spans are converted to µs and stored in `uint64_t`. - - struct Point; - struct Span; - - /// Returns information about clock - std::string getClockInfo(); - - /// Returns time spent by this process in user mode - Span getUserTime(); - - /// Returns point in time using a monotonic steady clock - Point getWallTime(); - - struct Point { - using SteadyTimePoint = std::chrono::steady_clock::time_point; - - SteadyTimePoint point; - - // ctors - Point() = default; - explicit Point(SteadyTimePoint p): point(p) {}; - - // operators - Point& operator+=(const Span&); - Point& operator-=(const Span&); - }; - - // operators - Point operator+(const Point&, const Span&); - Point operator+(const Span&, const Point&); - Point operator-(const Point&, const Span&); - Span operator-(const Point&, const Point&); - bool operator==(const Point&, const Point&); - bool operator!=(const Point&, const Point&); - bool operator<(const Point&, const Point&); - bool operator<=(const Point&, const Point&); - bool operator>(const Point&, const Point&); - bool operator>=(const Point&, const Point&); - - namespace { using Duration = std::chrono::steady_clock::duration; } - - struct Span { - Duration duration = Duration::zero(); - - // ctors - Span() = default; - explicit Span(const Duration &d): duration(d) {} - explicit Span(const std::string &s); - - // operators - Span& operator=(const Duration&); - Span& operator+=(const Span&); - Span& operator-=(const Span&); - Span& operator*=(unsigned); - Span& operator*=(double); - - // conversions - explicit operator Duration() const; - explicit operator bool() const; - explicit operator timeval() const; - - std::uint64_t toMicroseconds() const; - double toSeconds() const; - std::tuple toHMS() const; // hours, minutes, seconds - }; - - Span operator+(const Span&, const Span&); - Span operator-(const Span&, const Span&); - Span operator*(const Span&, double); - Span operator*(double, const Span&); - Span operator*(const Span&, unsigned); - Span operator*(unsigned, const Span&); - Span operator/(const Span&, unsigned); - bool operator==(const Span&, const Span&); - bool operator<=(const Span&, const Span&); - bool operator>=(const Span&, const Span&); - bool operator<(const Span&, const Span&); - bool operator>(const Span&, const Span&); - - /// Span -> "X.Ys" - std::ostream& operator<<(std::ostream&, Span); - llvm::raw_ostream& operator<<(llvm::raw_ostream&, Span); - - /// time spans - Span hours(std::uint16_t); - Span minutes(std::uint16_t); - Span seconds(std::uint64_t); - Span milliseconds(std::uint64_t); - Span microseconds(std::uint64_t); - Span nanoseconds(std::uint64_t); - - } // time -} // klee - -#endif /* KLEE_TIME_H */ diff --git a/include/klee/Module/Cell.h b/include/klee/Module/Cell.h new file mode 100644 index 00000000..c7d9ae18 --- /dev/null +++ b/include/klee/Module/Cell.h @@ -0,0 +1,23 @@ +//===-- Cell.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_CELL_H +#define KLEE_CELL_H + +#include "klee/Expr/Expr.h" + +namespace klee { + class MemoryObject; + + struct Cell { + ref value; + }; +} + +#endif /* KLEE_CELL_H */ diff --git a/include/klee/Module/InstructionInfoTable.h b/include/klee/Module/InstructionInfoTable.h new file mode 100644 index 00000000..e3684802 --- /dev/null +++ b/include/klee/Module/InstructionInfoTable.h @@ -0,0 +1,77 @@ +//===-- InstructionInfoTable.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_INSTRUCTIONINFOTABLE_H +#define KLEE_INSTRUCTIONINFOTABLE_H + +#include +#include +#include +#include + +namespace llvm { + class Function; + class Instruction; + class Module; +} + +namespace klee { + + /* Stores debug information for a KInstruction */ + struct InstructionInfo { + unsigned id; + const std::string &file; + unsigned line; + unsigned column; + unsigned assemblyLine; + + public: + InstructionInfo(unsigned _id, const std::string &_file, unsigned _line, + unsigned _column, unsigned _assemblyLine) + : id(_id), file(_file), line(_line), column(_column), + assemblyLine(_assemblyLine) {} + }; + + /* Stores debug information for a KInstruction */ + struct FunctionInfo { + unsigned id; + const std::string &file; + unsigned line; + uint64_t assemblyLine; + + public: + FunctionInfo(unsigned _id, const std::string &_file, unsigned _line, + uint64_t _assemblyLine) + : id(_id), file(_file), line(_line), assemblyLine(_assemblyLine) {} + + FunctionInfo(const FunctionInfo &) = delete; + FunctionInfo &operator=(FunctionInfo const &) = delete; + + FunctionInfo(FunctionInfo &&) = default; + }; + + class InstructionInfoTable { + std::unordered_map> + infos; + std::unordered_map> + functionInfos; + std::vector> internedStrings; + + public: + InstructionInfoTable(const llvm::Module &m); + + unsigned getMaxID() const; + const InstructionInfo &getInfo(const llvm::Instruction &) const; + const FunctionInfo &getFunctionInfo(const llvm::Function &) const; + }; + +} + +#endif /* KLEE_INSTRUCTIONINFOTABLE_H */ diff --git a/include/klee/Module/KInstIterator.h b/include/klee/Module/KInstIterator.h new file mode 100644 index 00000000..e5bd37f8 --- /dev/null +++ b/include/klee/Module/KInstIterator.h @@ -0,0 +1,42 @@ +//===-- KInstIterator.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_KINSTITERATOR_H +#define KLEE_KINSTITERATOR_H + +namespace klee { + struct KInstruction; + + class KInstIterator { + KInstruction **it; + + public: + KInstIterator() : it(0) {} + KInstIterator(KInstruction **_it) : it(_it) {} + + bool operator==(const KInstIterator &b) const { + return it==b.it; + } + bool operator!=(const KInstIterator &b) const { + return !(*this == b); + } + + KInstIterator &operator++() { + ++it; + return *this; + } + + operator KInstruction*() const { return it ? *it : 0;} + operator bool() const { return it != 0; } + + KInstruction *operator ->() const { return *it; } + }; +} // End klee namespace + +#endif /* KLEE_KINSTITERATOR_H */ diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h new file mode 100644 index 00000000..2873db45 --- /dev/null +++ b/include/klee/Module/KInstruction.h @@ -0,0 +1,64 @@ +//===-- KInstruction.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_KINSTRUCTION_H +#define KLEE_KINSTRUCTION_H + +#include "klee/Config/Version.h" +#include "klee/Module/InstructionInfoTable.h" + +#include "llvm/Support/DataTypes.h" +#include "llvm/Support/raw_ostream.h" + +#include + +namespace llvm { + class Instruction; +} + +namespace klee { + class Executor; + struct InstructionInfo; + class KModule; + + + /// KInstruction - Intermediate instruction representation used + /// during execution. + struct KInstruction { + llvm::Instruction *inst; + const InstructionInfo *info; + + /// Value numbers for each operand. -1 is an invalid value, + /// otherwise negative numbers are indices (negated and offset by + /// 2) into the module constant table and positive numbers are + /// register indices. + int *operands; + /// Destination register index. + unsigned dest; + + public: + virtual ~KInstruction(); + std::string getSourceLocation() const; + + }; + + struct KGEPInstruction : KInstruction { + /// indices - The list of variable sized adjustments to add to the pointer + /// operand to execute the instruction. The first element is the operand + /// index into the GetElementPtr instruction, and the second element is the + /// element size to multiple that index by. + std::vector< std::pair > indices; + + /// offset - A constant offset to add to the pointer operand to execute the + /// instruction. + uint64_t offset; + }; +} + +#endif /* KLEE_KINSTRUCTION_H */ diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h new file mode 100644 index 00000000..89606e2e --- /dev/null +++ b/include/klee/Module/KModule.h @@ -0,0 +1,153 @@ +//===-- KModule.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_KMODULE_H +#define KLEE_KMODULE_H + +#include "klee/Config/Version.h" +#include "klee/Interpreter.h" + +#include "llvm/ADT/ArrayRef.h" + +#include +#include +#include +#include + +namespace llvm { + class BasicBlock; + class Constant; + class Function; + class Instruction; + class Module; + class DataLayout; +} + +namespace klee { + struct Cell; + class Executor; + class Expr; + class InterpreterHandler; + class InstructionInfoTable; + struct KInstruction; + class KModule; + template class ref; + + struct KFunction { + llvm::Function *function; + + unsigned numArgs, numRegisters; + + unsigned numInstructions; + KInstruction **instructions; + + std::map basicBlockEntry; + + /// Whether instructions in this function should count as + /// "coverable" for statistics and search heuristics. + bool trackCoverage; + + public: + explicit KFunction(llvm::Function*, KModule *); + KFunction(const KFunction &) = delete; + KFunction &operator=(const KFunction &) = delete; + + ~KFunction(); + + unsigned getArgRegister(unsigned index) { return index; } + }; + + + class KConstant { + public: + /// Actual LLVM constant this represents. + llvm::Constant* ct; + + /// The constant ID. + unsigned id; + + /// First instruction where this constant was encountered, or NULL + /// if not applicable/unavailable. + KInstruction *ki; + + KConstant(llvm::Constant*, unsigned, KInstruction*); + }; + + + class KModule { + public: + std::unique_ptr module; + std::unique_ptr targetData; + + // Our shadow versions of LLVM structures. + std::vector> functions; + std::map functionMap; + + // Functions which escape (may be called indirectly) + // XXX change to KFunction + std::set escapingFunctions; + + std::unique_ptr infos; + + std::vector constants; + std::map> constantMap; + KConstant* getKConstant(const llvm::Constant *c); + + std::unique_ptr constantTable; + + // Functions which are part of KLEE runtime + std::set internalFunctions; + + private: + // Mark function with functionName as part of the KLEE runtime + void addInternalFunction(const char* functionName); + + public: + KModule() = default; + + /// Optimise and prepare module such that KLEE can execute it + // + void optimiseAndPrepare(const Interpreter::ModuleOptions &opts, + llvm::ArrayRef); + + /// Manifest the generated module (e.g. assembly.ll, output.bc) and + /// prepares KModule + /// + /// @param ih + /// @param forceSourceOutput true if assembly.ll should be created + /// + // FIXME: ihandler should not be here + void manifest(InterpreterHandler *ih, bool forceSourceOutput); + + /// Link the provided modules together as one KLEE module. + /// + /// If the entry point is empty, all modules are linked together. + /// If the entry point is not empty, all modules are linked which resolve + /// the dependencies of the module containing entryPoint + /// + /// @param modules list of modules to be linked together + /// @param entryPoint name of the function which acts as the program's entry + /// point + /// @return true if at least one module has been linked in, false if nothing + /// changed + bool link(std::vector> &modules, + const std::string &entryPoint); + + void instrument(const Interpreter::ModuleOptions &opts); + + /// Return an id for the given constant, creating a new one if necessary. + unsigned getConstantID(llvm::Constant *c, KInstruction* ki); + + /// Run passes that check if module is valid LLVM IR and if invariants + /// expected by KLEE's Executor hold. + void checkModule(); + }; +} // End klee namespace + +#endif /* KLEE_KMODULE_H */ diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index fe4d7e88..ec107c20 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -11,7 +11,7 @@ #define KLEE_SOLVER_H #include "klee/Expr/Expr.h" -#include "klee/Internal/System/Time.h" +#include "klee/System/Time.h" #include "klee/Solver/SolverCmdLine.h" #include diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h index 90d5af24..f03db964 100644 --- a/include/klee/Solver/SolverImpl.h +++ b/include/klee/Solver/SolverImpl.h @@ -10,7 +10,7 @@ #ifndef KLEE_SOLVERIMPL_H #define KLEE_SOLVERIMPL_H -#include "klee/Internal/System/Time.h" +#include "klee/System/Time.h" #include "Solver.h" #include diff --git a/include/klee/Support/CompressionStream.h b/include/klee/Support/CompressionStream.h new file mode 100644 index 00000000..bc9119dd --- /dev/null +++ b/include/klee/Support/CompressionStream.h @@ -0,0 +1,46 @@ +//===-- CompressionStream.h --------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_COMPRESSIONSTREAM_H +#define KLEE_COMPRESSIONSTREAM_H + +#include "llvm/Support/raw_ostream.h" +#include "zlib.h" + +namespace klee { +const size_t BUFSIZE = 128 * 1024; + +class compressed_fd_ostream : public llvm::raw_ostream { + int FD; + uint8_t buffer[BUFSIZE]; + z_stream strm; + uint64_t pos; + + /// write_impl - See raw_ostream::write_impl. + virtual void write_impl(const char *Ptr, size_t Size); + void write_file(const char *Ptr, size_t Size); + + virtual uint64_t current_pos() const { return pos; } + + void flush_compressed_data(); + void writeFullCompressedData(); + +public: + /// compressed_fd_ostream - Open the specified file for writing. If an error + /// occurs, information about the error is put into ErrorInfo, and the stream + /// should be immediately destroyed; the string will be empty if no error + /// occurred. This allows optional flags to control how the file will be + /// opened. + compressed_fd_ostream(const std::string &Filename, std::string &ErrorInfo); + + ~compressed_fd_ostream(); +}; +} + +#endif /* KLEE_COMPRESSIONSTREAM_H */ diff --git a/include/klee/Support/Debug.h b/include/klee/Support/Debug.h new file mode 100644 index 00000000..0fe7906a --- /dev/null +++ b/include/klee/Support/Debug.h @@ -0,0 +1,27 @@ +//===-- Debug.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_DEBUG_H +#define KLEE_DEBUG_H + +#include "klee/Config/config.h" +#include "llvm/Support/Debug.h" + +// We define wrappers around the LLVM DEBUG macros that are conditionalized on +// whether the LLVM we are building against has the symbols needed by these +// checks. + +#ifdef ENABLE_KLEE_DEBUG +#define KLEE_DEBUG_WITH_TYPE(TYPE, X) DEBUG_WITH_TYPE(TYPE, X) +#else +#define KLEE_DEBUG_WITH_TYPE(TYPE, X) do { } while (0) +#endif +#define KLEE_DEBUG(X) KLEE_DEBUG_WITH_TYPE(DEBUG_TYPE, X) + +#endif /* KLEE_DEBUG_H */ diff --git a/include/klee/Support/ErrorHandling.h b/include/klee/Support/ErrorHandling.h new file mode 100644 index 00000000..92762c03 --- /dev/null +++ b/include/klee/Support/ErrorHandling.h @@ -0,0 +1,51 @@ +//===-- ErrorHandling.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_ERRORHANDLING_H +#define KLEE_ERRORHANDLING_H + +#ifdef __CYGWIN__ +#ifndef WINDOWS +#define WINDOWS +#endif +#endif + +#include + +namespace klee { + +extern FILE *klee_warning_file; +extern FILE *klee_message_file; + +/// Print "KLEE: ERROR: " followed by the msg in printf format and a +/// newline on stderr and to warnings.txt, then exit with an error. +void klee_error(const char *msg, ...) + __attribute__((format(printf, 1, 2), noreturn)); + +/// Print "KLEE: " followed by the msg in printf format and a +/// newline on stderr and to messages.txt. +void klee_message(const char *msg, ...) __attribute__((format(printf, 1, 2))); + +/// Print "KLEE: " followed by the msg in printf format and a +/// newline to messages.txt. +void klee_message_to_file(const char *msg, ...) + __attribute__((format(printf, 1, 2))); + +/// Print "KLEE: WARNING: " followed by the msg in printf format and a +/// newline on stderr and to warnings.txt. +void klee_warning(const char *msg, ...) __attribute__((format(printf, 1, 2))); + +/// Print "KLEE: WARNING: " followed by the msg in printf format and a +/// newline on stderr and to warnings.txt. However, the warning is only +/// printed once for each unique (id, msg) pair (as pointers). +void klee_warning_once(const void *id, const char *msg, ...) + __attribute__((format(printf, 2, 3))); +} + +#endif /* KLEE_ERRORHANDLING_H */ diff --git a/include/klee/Support/FileHandling.h b/include/klee/Support/FileHandling.h new file mode 100644 index 00000000..90ce20b3 --- /dev/null +++ b/include/klee/Support/FileHandling.h @@ -0,0 +1,27 @@ +//===-- FileHandling.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_FILEHANDLING_H +#define KLEE_FILEHANDLING_H + +#include "llvm/Support/raw_ostream.h" +#include +#include + +namespace klee { +std::unique_ptr +klee_open_output_file(const std::string &path, std::string &error); + +#ifdef HAVE_ZLIB_H +std::unique_ptr +klee_open_compressed_output_file(const std::string &path, std::string &error); +#endif +} // namespace klee + +#endif /* KLEE_FILEHANDLING_H */ diff --git a/include/klee/Support/FloatEvaluation.h b/include/klee/Support/FloatEvaluation.h new file mode 100644 index 00000000..37392576 --- /dev/null +++ b/include/klee/Support/FloatEvaluation.h @@ -0,0 +1,263 @@ +//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +// FIXME: Ditch this and use APFloat. + +#ifndef KLEE_FLOATEVALUATION_H +#define KLEE_FLOATEVALUATION_H + +#include "klee/util/Bits.h" //bits64::truncateToNBits +#include "IntEvaluation.h" //ints::sext + +#include "llvm/Support/ErrorHandling.h" +#include "llvm/Support/MathExtras.h" + +#include + +namespace klee { +namespace floats { + +// ********************************** // +// *** Pack uint64_t into FP types ** // +// ********************************** // + +// interpret the 64 bits as a double instead of a uint64_t +inline double UInt64AsDouble( uint64_t bits ) { + double ret; + assert( sizeof(bits) == sizeof(ret) ); + memcpy( &ret, &bits, sizeof bits ); + return ret; +} + +// interpret the first 32 bits as a float instead of a uint64_t +inline float UInt64AsFloat( uint64_t bits ) { + uint32_t tmp = bits; // ensure that we read correct bytes + float ret; + assert( sizeof(tmp) == sizeof(ret) ); + memcpy( &ret, &tmp, sizeof tmp ); + return ret; +} + + +// ********************************** // +// *** Pack FP types into uint64_t ** // +// ********************************** // + +// interpret the 64 bits as a uint64_t instead of a double +inline uint64_t DoubleAsUInt64( double d ) { + uint64_t ret; + assert( sizeof(d) == sizeof(ret) ); + memcpy( &ret, &d, sizeof d ); + return ret; +} + +// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s) +inline uint64_t FloatAsUInt64( float f ) { + uint32_t tmp; + assert( sizeof(tmp) == sizeof(f) ); + memcpy( &tmp, &f, sizeof f ); + return (uint64_t)tmp; +} + + +// ********************************** // +// ************ Constants *********** // +// ********************************** // + +const unsigned FLT_BITS = 32; +const unsigned DBL_BITS = 64; + + + +// ********************************** // +// ***** LLVM Binary Operations ***** // +// ********************************** // + +// add of l and r +inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) + UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// difference of l and r +inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) - UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// product of l and r +inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) * UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// signed divide of l by r +inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) / UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// signed modulo of l by r +inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l), UInt64AsFloat(r)) ), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + + +// ********************************** // +// *** LLVM Comparison Operations *** // +// ********************************** // + +// determine if l represents NaN +inline bool isNaN(uint64_t l, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: + return std::isnan(UInt64AsFloat(l)); + case DBL_BITS: + return std::isnan(UInt64AsDouble(l)); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) == UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) != UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) < UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) <= UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) > UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) >= UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + + +// ********************************** // +// *** LLVM Conversion Operations *** // +// ********************************** // + +// truncation of l (which must be a double) to float (casts a double to a float) +inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { + // FIXME: Investigate this, should this not happen? Was a quick + // patch for busybox. + if (inWidth==64 && outWidth==64) { + return l; + } else { + assert(inWidth==64 && "can only truncate from a 64-bit double"); + assert(outWidth==32 && "can only truncate to a 32-bit float"); + float trunc = (float)UInt64AsDouble(l); + return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth); + } +} + +// extension of l (which must be a float) to double (casts a float to a double) +inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) { + // FIXME: Investigate this, should this not happen? Was a quick + // patch for busybox. + if (inWidth==64 && outWidth==64) { + return l; + } else { + assert(inWidth==32 && "can only extend from a 32-bit float"); + assert(outWidth==64 && "can only extend to a 64-bit double"); + double ext = (double)UInt64AsFloat(l); + return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth); + } +} + +// conversion of l to an unsigned integer, rounding towards zero +inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l), outWidth ); + case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth ); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// conversion of l to a signed integer, rounding towards zero +inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l), outWidth); + case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// conversion of l, interpreted as an unsigned int, to a floating point number +inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) { + switch( outWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l), outWidth); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +// conversion of l, interpreted as a signed int, to a floating point number +inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) { + switch( outWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth); + default: llvm::report_fatal_error("unsupported floating point width"); + } +} + +} // end namespace ints +} // end namespace klee + +#endif /* KLEE_FLOATEVALUATION_H */ diff --git a/include/klee/Support/IntEvaluation.h b/include/klee/Support/IntEvaluation.h new file mode 100644 index 00000000..27a8daf0 --- /dev/null +++ b/include/klee/Support/IntEvaluation.h @@ -0,0 +1,164 @@ +//===-- IntEvaluation.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_INTEVALUATION_H +#define KLEE_INTEVALUATION_H + +#include "klee/util/Bits.h" + +#define MAX_BITS (sizeof(uint64_t) * 8) + +// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is +// between making trunc/zext/sext fast and making operations that depend +// on the invalid bits being 0 fast. + +namespace klee { +namespace ints { + +// add of l and r +inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l + r, inWidth); +} + +// difference of l and r +inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l - r, inWidth); +} + +// product of l and r +inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l * r, inWidth); +} + +// truncation of l to outWidth bits +inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { + return bits64::truncateToNBits(l, outWidth); +} + +// zero-extension of l from inWidth to outWidth bits +inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) { + return l; +} + +// sign-extension of l from inWidth to outWidth bits +inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) { + uint32_t numInvalidBits = MAX_BITS - inWidth; + return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth); +} + +// unsigned divide of l by r +inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l / r, inWidth); +} + +// unsigned mod of l by r +inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l % r, inWidth); +} + +// signed divide of l by r +inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) { + // sign extend operands so that signed operation on 64-bits works correctly + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return bits64::truncateToNBits(sl / sr, inWidth); +} + +// signed mod of l by r +inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) { + // sign extend operands so that signed operation on 64-bits works correctly + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return bits64::truncateToNBits(sl % sr, inWidth); +} + +// arithmetic shift right of l by r bits +inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + return bits64::truncateToNBits(sl >> shift, inWidth); +} + +// logical shift right of l by r bits +inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) { + return l >> shift; +} + +// shift left of l by r bits +inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) { + return bits64::truncateToNBits(l << shift, inWidth); +} + +// logical AND of l and r +inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) { + return l & r; +} + +// logical OR of l and r +inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) { + return l | r; +} + +// logical XOR of l and r +inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) { + return l ^ r; +} + +// comparison operations +inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { + return l == r; +} + +inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { + return l != r; +} + +inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) { + return l < r; +} + +inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) { + return l <= r; +} + +inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) { + return l > r; +} + +inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) { + return l >= r; +} + +inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl < sr; +} + +inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl <= sr; +} + +inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl > sr; +} + +inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl >= sr; +} + +} // end namespace ints +} // end namespace klee + +#endif /* KLEE_INTEVALUATION_H */ diff --git a/include/klee/Support/ModuleUtil.h b/include/klee/Support/ModuleUtil.h new file mode 100644 index 00000000..e80fc673 --- /dev/null +++ b/include/klee/Support/ModuleUtil.h @@ -0,0 +1,70 @@ +//===-- ModuleUtil.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_MODULEUTIL_H +#define KLEE_MODULEUTIL_H + +#include "klee/Config/Version.h" + +#include "llvm/IR/CallSite.h" +#include "llvm/IR/Module.h" + +#include +#include +#include + +namespace klee { + +/// Links all the modules together into one and returns it. +/// +/// All the modules which are used for resolving entities are freed, +/// all the remaining ones are preserved. +/// +/// @param modules List of modules to link together: if resolveOnly true, +/// everything is linked against the first entry. +/// @param entryFunction if set, missing functions of the module containing the +/// entry function will be solved. +/// @return final module or null in this case errorMsg is set +std::unique_ptr +linkModules(std::vector> &modules, + llvm::StringRef entryFunction, std::string &errorMsg); + +/// Return the Function* target of a Call or Invoke instruction, or +/// null if it cannot be determined (should be only for indirect +/// calls, although complicated constant expressions might be +/// another possibility). +/// +/// If `moduleIsFullyLinked` is set to true it will be assumed that the +/// module containing the `llvm::CallSite` is fully linked. This assumption +/// allows resolution of functions that are marked as overridable. +llvm::Function *getDirectCallTarget(llvm::CallSite, bool moduleIsFullyLinked); + +/// Return true iff the given Function value is used in something +/// other than a direct call (or a constant expression that +/// terminates in a direct call). +bool functionEscapes(const llvm::Function *f); + +/// Loads the file libraryName and reads all possible modules out of it. +/// +/// Different file types are possible: +/// * .bc binary file +/// * .ll IR file +/// * .a archive containing .bc and .ll files +/// +/// @param libraryName library to read +/// @param modules contains extracted modules +/// @param errorMsg contains the error description in case the file could not be +/// loaded +/// @return true if successful otherwise false +bool loadFile(const std::string &libraryName, llvm::LLVMContext &context, + std::vector> &modules, + std::string &errorMsg); +} + +#endif /* KLEE_MODULEUTIL_H */ diff --git a/include/klee/Support/PrintVersion.h b/include/klee/Support/PrintVersion.h new file mode 100644 index 00000000..fbd20e39 --- /dev/null +++ b/include/klee/Support/PrintVersion.h @@ -0,0 +1,25 @@ +//===-- PrintVersion.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_PRINTVERSION_H +#define KLEE_PRINTVERSION_H + +#include "llvm/Support/raw_ostream.h" + +#include "klee/Config/Version.h" + +namespace klee { +#if LLVM_VERSION_CODE >= LLVM_VERSION(6, 0) + void printVersion(llvm::raw_ostream &OS); +#else + void printVersion(); +#endif +} + +#endif /* KLEE_PRINTVERSION_H */ diff --git a/include/klee/Support/Timer.h b/include/klee/Support/Timer.h new file mode 100644 index 00000000..48cbbdea --- /dev/null +++ b/include/klee/Support/Timer.h @@ -0,0 +1,96 @@ +//===-- Timer.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_TIMER_H +#define KLEE_TIMER_H + +#include "klee/System/Time.h" + +#include "llvm/ADT/SmallVector.h" + +#include +#include + +namespace klee { + + /** + * A WallTimer stores its creation time. + */ + class WallTimer { + const time::Point start; + public: + WallTimer(); + + /// Return the delta since the timer was created + time::Span delta() const; + }; + + + /** + * A Timer repeatedly executes a `callback` after a specified `interval`. + * An object of this class is _passive_ and only keeps track of the next invocation time. + * _Passive_ means, that it has to be `invoke`d by an external caller with the current time. + * Only when the time span between the current time and the last invocation exceeds the + * specified `interval`, the `callback` will be executed. + * Multiple timers are typically managed by a TimerGroup. + */ + class Timer { + /// Approximate interval between callback invocations. + time::Span interval; + /// Wall time for next invocation. + time::Point nextInvocationTime; + /// The event callback. + std::function run; + public: + /// \param interval The time span between callback invocations. + /// \param callback The event callback. + Timer(const time::Span &interval, std::function &&callback); + + /// Return specified `interval` between invocations. + time::Span getInterval() const; + /// Execute `callback` if invocation time exceeded. + void invoke(const time::Point ¤tTime); + /// Set new invocation time to `currentTime + interval`. + void reset(const time::Point ¤tTime); + }; + + + /** + * A TimerGroup manages multiple timers. + * + * TimerGroup simplifies the handling of multiple Timer objects by offering a unifying + * Timer-like interface. Additionally, it serves as a barrier and prevents timers from + * being invoked too often by defining a minimum invocation interval (MI). + * All registered timer intervals should be larger than MI and also be multiples of MI. + * Similar to Timer, a TimerGroup is _passive_ and needs to be `invoke`d by an external + * caller. + */ + class TimerGroup { + /// Registered timers. + llvm::SmallVector, 4> timers; + /// Timer that invokes all registered timers after minimum interval. + Timer invocationTimer; + /// Time of last `invoke` call. + time::Point currentTime; + public: + /// \param minInterval The minimum interval between invocations of registered timers. + explicit TimerGroup(const time::Span &minInterval); + + /// Add a timer to be executed periodically. + /// + /// \param timer The timer object to register. + void add(std::unique_ptr timer); + /// Invoke registered timers with current time only if minimum interval exceeded. + void invoke(); + /// Reset all timers. + void reset(); + }; + +} // klee +#endif /* KLEE_TIMER_H */ diff --git a/include/klee/System/MemoryUsage.h b/include/klee/System/MemoryUsage.h new file mode 100644 index 00000000..c3cf3c74 --- /dev/null +++ b/include/klee/System/MemoryUsage.h @@ -0,0 +1,21 @@ +//===-- MemoryUsage.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_MEMORYUSAGE_H +#define KLEE_MEMORYUSAGE_H + +#include + +namespace klee { + namespace util { + size_t GetTotalMallocUsage(); + } +} + +#endif /* KLEE_MEMORYUSAGE_H */ diff --git a/include/klee/System/Time.h b/include/klee/System/Time.h new file mode 100644 index 00000000..2ebebdfd --- /dev/null +++ b/include/klee/System/Time.h @@ -0,0 +1,120 @@ +//===-- Time.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_TIME_H +#define KLEE_TIME_H + +#include "llvm/Support/raw_ostream.h" + +#include +#include +#include + +namespace klee { + namespace time { + + /// The klee::time namespace offers various functions to measure the time (`getWallTime`) + /// and to get timing information for the current KLEE process (`getUserTime`). + /// This implementation is based on `std::chrono` and uses time points and time spans. + /// For KLEE statistics, spans are converted to µs and stored in `uint64_t`. + + struct Point; + struct Span; + + /// Returns information about clock + std::string getClockInfo(); + + /// Returns time spent by this process in user mode + Span getUserTime(); + + /// Returns point in time using a monotonic steady clock + Point getWallTime(); + + struct Point { + using SteadyTimePoint = std::chrono::steady_clock::time_point; + + SteadyTimePoint point; + + // ctors + Point() = default; + explicit Point(SteadyTimePoint p): point(p) {}; + + // operators + Point& operator+=(const Span&); + Point& operator-=(const Span&); + }; + + // operators + Point operator+(const Point&, const Span&); + Point operator+(const Span&, const Point&); + Point operator-(const Point&, const Span&); + Span operator-(const Point&, const Point&); + bool operator==(const Point&, const Point&); + bool operator!=(const Point&, const Point&); + bool operator<(const Point&, const Point&); + bool operator<=(const Point&, const Point&); + bool operator>(const Point&, const Point&); + bool operator>=(const Point&, const Point&); + + namespace { using Duration = std::chrono::steady_clock::duration; } + + struct Span { + Duration duration = Duration::zero(); + + // ctors + Span() = default; + explicit Span(const Duration &d): duration(d) {} + explicit Span(const std::string &s); + + // operators + Span& operator=(const Duration&); + Span& operator+=(const Span&); + Span& operator-=(const Span&); + Span& operator*=(unsigned); + Span& operator*=(double); + + // conversions + explicit operator Duration() const; + explicit operator bool() const; + explicit operator timeval() const; + + std::uint64_t toMicroseconds() const; + double toSeconds() const; + std::tuple toHMS() const; // hours, minutes, seconds + }; + + Span operator+(const Span&, const Span&); + Span operator-(const Span&, const Span&); + Span operator*(const Span&, double); + Span operator*(double, const Span&); + Span operator*(const Span&, unsigned); + Span operator*(unsigned, const Span&); + Span operator/(const Span&, unsigned); + bool operator==(const Span&, const Span&); + bool operator<=(const Span&, const Span&); + bool operator>=(const Span&, const Span&); + bool operator<(const Span&, const Span&); + bool operator>(const Span&, const Span&); + + /// Span -> "X.Ys" + std::ostream& operator<<(std::ostream&, Span); + llvm::raw_ostream& operator<<(llvm::raw_ostream&, Span); + + /// time spans + Span hours(std::uint16_t); + Span minutes(std::uint16_t); + Span seconds(std::uint64_t); + Span milliseconds(std::uint64_t); + Span microseconds(std::uint64_t); + Span nanoseconds(std::uint64_t); + + } // time +} // klee + +#endif /* KLEE_TIME_H */ diff --git a/include/klee/TimerStatIncrementer.h b/include/klee/TimerStatIncrementer.h index c467c82b..26ead0e6 100644 --- a/include/klee/TimerStatIncrementer.h +++ b/include/klee/TimerStatIncrementer.h @@ -11,7 +11,7 @@ #define KLEE_TIMERSTATINCREMENTER_H #include "klee/Statistics.h" -#include "klee/Internal/Support/Timer.h" +#include "klee/Support/Timer.h" namespace klee { -- cgit 1.4.1