From 6f290d8f9e9d7faac295cb51fc96884a18f4ded4 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 21 May 2009 04:36:41 +0000 Subject: Initial KLEE checkin. - Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Support/Makefile | 16 ++++ lib/Support/README.txt | 2 + lib/Support/RNG.cpp | 146 ++++++++++++++++++++++++++++++++ lib/Support/Time.cpp | 27 ++++++ lib/Support/Timer.cpp | 27 ++++++ lib/Support/TreeStream.cpp | 201 +++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 419 insertions(+) create mode 100644 lib/Support/Makefile create mode 100644 lib/Support/README.txt create mode 100644 lib/Support/RNG.cpp create mode 100644 lib/Support/Time.cpp create mode 100644 lib/Support/Timer.cpp create mode 100644 lib/Support/TreeStream.cpp (limited to 'lib/Support') diff --git a/lib/Support/Makefile b/lib/Support/Makefile new file mode 100644 index 00000000..a1b46f3c --- /dev/null +++ b/lib/Support/Makefile @@ -0,0 +1,16 @@ +#===-- lib/Support/Makefile --------------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +LEVEL=../.. + +LIBRARYNAME=kleeSupport +DONT_BUILD_RELINKED=1 +BUILD_ARCHIVE=1 + +include $(LEVEL)/Makefile.common diff --git a/lib/Support/README.txt b/lib/Support/README.txt new file mode 100644 index 00000000..1ed6fcb4 --- /dev/null +++ b/lib/Support/README.txt @@ -0,0 +1,2 @@ +This directory holds basic support facilities (data structures, +utilities, etc.) used by klee. diff --git a/lib/Support/RNG.cpp b/lib/Support/RNG.cpp new file mode 100644 index 00000000..fef7e489 --- /dev/null +++ b/lib/Support/RNG.cpp @@ -0,0 +1,146 @@ +/* + A C-program for MT19937, with initialization improved 2002/1/26. + Coded by Takuji Nishimura and Makoto Matsumoto. + Modified to be a C++ class by Daniel Dunbar. + + Before using, initialize the state by using init_genrand(seed) + or init_by_array(init_key, key_length). + + Copyright (C) 1997 - 2002, Makoto Matsumoto and Takuji Nishimura, + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + 3. The names of its contributors may not be used to endorse or promote + products derived from this software without specific prior written + permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR + A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR + CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + + + Any feedback is very welcome. + http://www.math.sci.hiroshima-u.ac.jp/~m-mat/MT/emt.html + email: m-mat @ math.sci.hiroshima-u.ac.jp (remove space) +*/ + +#include "klee/Internal/ADT/RNG.h" + +using namespace klee; + +/* initializes mt[N] with a seed */ +RNG::RNG(unsigned int s) { + seed(s); +} + +void RNG::seed(unsigned int s) { + mt[0]= s & 0xffffffffUL; + for (mti=1; mti> 30)) + mti); + /* See Knuth TAOCP Vol2. 3rd Ed. P.106 for multiplier. */ + /* In the previous versions, MSBs of the seed affect */ + /* only MSBs of the array mt[]. */ + /* 2002/01/09 modified by Makoto Matsumoto */ + mt[mti] &= 0xffffffffUL; + /* for >32 bit machines */ + } +} + +/* generates a random number on [0,0xffffffff]-interval */ +unsigned int RNG::getInt32() { + unsigned int y; + static unsigned int mag01[2]={0x0UL, MATRIX_A}; + /* mag01[x] = x * MATRIX_A for x=0,1 */ + + if (mti >= N) { /* generate N words at one time */ + int kk; + + for (kk=0;kk> 1) ^ mag01[y & 0x1UL]; + } + for (;kk> 1) ^ mag01[y & 0x1UL]; + } + y = (mt[N-1]&UPPER_MASK)|(mt[0]&LOWER_MASK); + mt[N-1] = mt[M-1] ^ (y >> 1) ^ mag01[y & 0x1UL]; + + mti = 0; + } + + y = mt[mti++]; + + /* Tempering */ + y ^= (y >> 11); + y ^= (y << 7) & 0x9d2c5680UL; + y ^= (y << 15) & 0xefc60000UL; + y ^= (y >> 18); + + return y; +} + +/* generates a random number on [0,0x7fffffff]-interval */ +int RNG::getInt31() { + return (int)(getInt32()>>1); +} + +/* generates a random number on [0,1]-real-interval */ +double RNG::getDoubleLR() { + return getInt32()*(1.0/4294967295.0); + /* divided by 2^32-1 */ +} + +/* generates a random number on [0,1)-real-interval */ +double RNG::getDoubleL() { + return getInt32()*(1.0/4294967296.0); + /* divided by 2^32 */ +} + +/* generates a random number on (0,1)-real-interval */ +double RNG::getDouble() { + return (((double)getInt32()) + 0.5)*(1.0/4294967296.0); + /* divided by 2^32 */ +} + +float RNG::getFloatLR() { + return getInt32()*(1.0f/4294967295.0f); + /* divided by 2^32-1 */ +} +float RNG::getFloatL() { + return getInt32()*(1.0f/4294967296.0f); + /* divided by 2^32 */ +} +float RNG::getFloat() { + return (getInt32() + 0.5f)*(1.0f/4294967296.0f); + /* divided by 2^32 */ +} + +bool RNG::getBool() { + unsigned bits = getInt32(); + bits ^= bits >> 16; + bits ^= bits >> 8; + bits ^= bits >> 4; + bits ^= bits >> 2; + bits ^= bits >> 1; + return bits&1; +} diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp new file mode 100644 index 00000000..0ec8d9d7 --- /dev/null +++ b/lib/Support/Time.cpp @@ -0,0 +1,27 @@ +//===-- Time.cpp ----------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Internal/System/Time.h" + +#include "llvm/System/Process.h" + +using namespace llvm; +using namespace klee; + +double util::getUserTime() { + sys::TimeValue now(0,0),user(0,0),sys(0,0); + sys::Process::GetTimeUsage(now,user,sys); + return (user.seconds() + (double) user.nanoseconds() * 1e-9); +} + +double util::getWallTime() { + sys::TimeValue now(0,0),user(0,0),sys(0,0); + sys::Process::GetTimeUsage(now,user,sys); + return (now.seconds() + (double) now.nanoseconds() * 1e-9); +} diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp new file mode 100644 index 00000000..cddb0707 --- /dev/null +++ b/lib/Support/Timer.cpp @@ -0,0 +1,27 @@ +//===-- Timer.cpp ---------------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Internal/Support/Timer.h" + +#include "llvm/System/Process.h" + +using namespace klee; +using namespace llvm; + +WallTimer::WallTimer() { + sys::TimeValue now(0,0),user(0,0),sys(0,0); + sys::Process::GetTimeUsage(now,user,sys); + startMicroseconds = now.usec(); +} + +uint64_t WallTimer::check() { + sys::TimeValue now(0,0),user(0,0),sys(0,0); + sys::Process::GetTimeUsage(now,user,sys); + return now.usec() - startMicroseconds; +} diff --git a/lib/Support/TreeStream.cpp b/lib/Support/TreeStream.cpp new file mode 100644 index 00000000..0e8b86dd --- /dev/null +++ b/lib/Support/TreeStream.cpp @@ -0,0 +1,201 @@ +//===-- TreeStream.cpp ----------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Internal/ADT/TreeStream.h" + +#include +#include +#include +#include +#include +#include + +#include + +using namespace klee; + +/// + +TreeStreamWriter::TreeStreamWriter(const std::string &_path) + : lastID(0), + bufferCount(0), + path(_path), + output(new std::ofstream(path.c_str(), + std::ios::out | std::ios::binary)), + ids(1) { + if (!output->good()) { + delete output; + output = 0; + } +} + +TreeStreamWriter::~TreeStreamWriter() { + flush(); + if (output) + delete output; +} + +bool TreeStreamWriter::good() { + return !!output; +} + +TreeOStream TreeStreamWriter::open() { + return open(TreeOStream(*this, 0)); +} + +TreeOStream TreeStreamWriter::open(const TreeOStream &os) { + assert(output && os.writer==this); + flushBuffer(); + unsigned id = ids++; + output->write(reinterpret_cast(&os.id), 4); + unsigned tag = id | (1<<31); + output->write(reinterpret_cast(&tag), 4); + return TreeOStream(*this, id); +} + +void TreeStreamWriter::write(TreeOStream &os, const char *s, unsigned size) { +#if 1 + if (bufferCount && + (os.id!=lastID || size+bufferCount>bufferSize)) + flushBuffer(); + if (bufferCount) { // (os.id==lastID && size+bufferCount<=bufferSize) + memcpy(&buffer[bufferCount], s, size); + bufferCount += size; + } else if (sizewrite(reinterpret_cast(&os.id), 4); + output->write(reinterpret_cast(&size), 4); + output->write(buffer, size); + } +#else + output->write(reinterpret_cast(&os.id), 4); + output->write(reinterpret_cast(&size), 4); + output->write(s, size); +#endif +} + +void TreeStreamWriter::flushBuffer() { + if (bufferCount) { + output->write(reinterpret_cast(&lastID), 4); + output->write(reinterpret_cast(&bufferCount), 4); + output->write(buffer, bufferCount); + bufferCount = 0; + } +} + +void TreeStreamWriter::flush() { + flushBuffer(); + output->flush(); +} + +void TreeStreamWriter::readStream(TreeStreamID streamID, + std::vector &out) { + assert(streamID>0 && streamID parents; + std::vector roots; + for (;;) { + assert(is.good()); + unsigned id; + unsigned tag; + is.read(reinterpret_cast(&id), 4); + is.read(reinterpret_cast(&tag), 4); + if (tag&(1<<31)) { // fork + unsigned child = tag ^ (1<<31); + + if (child==streamID) { + roots.push_back(child); + while (id) { + roots.push_back(id); + std::map::iterator it = parents.find(id); + assert(it!=parents.end()); + id = it->second; + } + break; + } else { + parents.insert(std::make_pair(child,id)); + } + } else { + unsigned size = tag; + while (size--) is.get(); + } + } +#if 0 + std::cout << "roots: "; + std::copy(roots.begin(), roots.end(), std::ostream_iterator(std::cout, " ")); + std::cout << "\n"; +#endif + is.seekg(0, std::ios::beg); + for (;;) { + unsigned id; + unsigned tag; + is.read(reinterpret_cast(&id), 4); + is.read(reinterpret_cast(&tag), 4); + if (!is.good()) break; + if (tag&(1<<31)) { // fork + unsigned child = tag ^ (1<<31); + if (id==roots.back() && roots.size()>1 && child==roots[roots.size()-2]) + roots.pop_back(); + } else { + unsigned size = tag; + if (id==roots.back()) { + while (size--) out.push_back(is.get()); + } else { + while (size--) is.get(); + } + } + } +} + +/// + +TreeOStream::TreeOStream() + : writer(0), + id(0) { +} + +TreeOStream::TreeOStream(TreeStreamWriter &_writer, unsigned _id) + : writer(&_writer), + id(_id) { +} + +TreeOStream::~TreeOStream() { +} + +unsigned TreeOStream::getID() const { + assert(writer); + return id; +} + +void TreeOStream::write(const char *buffer, unsigned size) { + assert(writer); + writer->write(*this, buffer, size); +} + +TreeOStream &TreeOStream::operator<<(const std::string &s) { + assert(writer); + write(s.c_str(), s.size()); + return *this; +} + +void TreeOStream::flush() { + assert(writer); + writer->flush(); +} -- cgit 1.4.1