diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-01-29 16:50:52 +0000 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2014-02-06 23:55:29 +0100 |
commit | ebaad172d4aab5fbaeca8c2658aaa94fc2e9b08e (patch) | |
tree | b4f81977ede05119b41881787e5b0476dae04cb9 | |
parent | d3202c9705ebd840051574956c04d12322c8afe6 (diff) | |
download | klee-ebaad172d4aab5fbaeca8c2658aaa94fc2e9b08e.tar.gz |
Implement const_iterator interface for SpecialFunctionHandler so
that clients can access HandlerInfo nicely.
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 39 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 33 |
2 files changed, 63 insertions, 9 deletions
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 04f32780..ca9f7b63 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -38,20 +38,14 @@ using namespace klee; /// -struct HandlerInfo { - const char *name; - SpecialFunctionHandler::Handler handler; - bool doesNotReturn; /// Intrinsic terminates the process - bool hasReturnValue; /// Intrinsic has a return value - bool doNotOverride; /// Intrinsic should not be used if already defined -}; + // FIXME: We are more or less committed to requiring an intrinsic // library these days. We can move some of this stuff there, // especially things like realloc which have complicated semantics // w.r.t. forking. Among other things this makes delayed query // dispatch easier to implement. -HandlerInfo handlerInfo[] = { +static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { #define add(name, handler, ret) { name, \ &SpecialFunctionHandler::handler, \ false, ret, false } @@ -117,12 +111,37 @@ HandlerInfo handlerInfo[] = { #undef add }; +SpecialFunctionHandler::const_iterator SpecialFunctionHandler::begin() { + return SpecialFunctionHandler::const_iterator(handlerInfo); +} + +SpecialFunctionHandler::const_iterator SpecialFunctionHandler::end() { + // NULL pointer is sentinel + return SpecialFunctionHandler::const_iterator(0); +} + +SpecialFunctionHandler::const_iterator& SpecialFunctionHandler::const_iterator::operator++() { + ++index; + if ( index >= SpecialFunctionHandler::size()) + { + // Out of range, return .end() + base=0; // Sentinel + index=0; + } + + return *this; +} + +int SpecialFunctionHandler::size() { + return sizeof(handlerInfo)/sizeof(handlerInfo[0]); +} + SpecialFunctionHandler::SpecialFunctionHandler(Executor &_executor) : executor(_executor) {} void SpecialFunctionHandler::prepare() { - unsigned N = sizeof(handlerInfo)/sizeof(handlerInfo[0]); + unsigned N = size(); for (unsigned i=0; i<N; ++i) { HandlerInfo &hi = handlerInfo[i]; @@ -715,3 +734,5 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, mo->isGlobal = true; } } + + diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 02e70ed4..f68c6edb 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -10,6 +10,7 @@ #ifndef KLEE_SPECIALFUNCTIONHANDLER_H #define KLEE_SPECIALFUNCTIONHANDLER_H +#include <iterator> #include <map> #include <vector> #include <string> @@ -37,6 +38,38 @@ namespace klee { handlers_ty handlers; class Executor &executor; + struct HandlerInfo { + const char *name; + SpecialFunctionHandler::Handler handler; + bool doesNotReturn; /// Intrinsic terminates the process + bool hasReturnValue; /// Intrinsic has a return value + bool doNotOverride; /// Intrinsic should not be used if already defined + }; + + // const_iterator to iterate over stored HandlerInfo + // FIXME: Implement >, >=, <=, < operators + class const_iterator : public std::iterator<std::random_access_iterator_tag, HandlerInfo> + { + private: + value_type* base; + int index; + public: + const_iterator(value_type* hi) : base(hi), index(0) {}; + const_iterator& operator++(); // pre-fix + const_iterator operator++(int); // post-fix + const value_type& operator*() { return base[index];} + const value_type* operator->() { return &(base[index]);} + const value_type& operator[](int i) { return base[i];} + bool operator==(const_iterator& rhs) { return (rhs.base + rhs.index) == (this->base + this->index);} + bool operator!=(const_iterator& rhs) { return !(*this == rhs);} + }; + + static const_iterator begin(); + static const_iterator end(); + static int size(); + + + public: SpecialFunctionHandler(Executor &_executor); |