aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Basic
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-05-21 04:36:41 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-05-21 04:36:41 +0000
commit6f290d8f9e9d7faac295cb51fc96884a18f4ded4 (patch)
tree46e7d426abc0c9f06ac472ac6f7f9e661b5d78cb /lib/Basic
parenta55960edd4dcd7535526de8d2277642522aa0209 (diff)
downloadklee-6f290d8f9e9d7faac295cb51fc96884a18f4ded4.tar.gz
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
Diffstat (limited to 'lib/Basic')
-rw-r--r--lib/Basic/BOut.cpp236
-rw-r--r--lib/Basic/Makefile16
-rw-r--r--lib/Basic/README.txt3
-rw-r--r--lib/Basic/Statistics.cpp84
4 files changed, 339 insertions, 0 deletions
diff --git a/lib/Basic/BOut.cpp b/lib/Basic/BOut.cpp
new file mode 100644
index 00000000..42d17e27
--- /dev/null
+++ b/lib/Basic/BOut.cpp
@@ -0,0 +1,236 @@
+//===-- BOut.c ------------------------------------------------------------===//
+//
+// 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/BOut.h"
+
+#include <stdlib.h>
+#include <string.h>
+#include <stdio.h>
+
+#define BOUT_MAGIC "BOUT\n"
+#define BOUT_MAGIC_SIZE 5
+#define BOUT_VERSION 2
+
+/***/
+
+static int read_uint32(FILE *f, unsigned *value_out) {
+ unsigned char data[4];
+ if (fread(data, 4, 1, f)!=1)
+ return 0;
+ *value_out = (((((data[0]<<8) + data[1])<<8) + data[2])<<8) + data[3];
+ return 1;
+}
+
+static int write_uint32(FILE *f, unsigned value) {
+ unsigned char data[4];
+ data[0] = value>>24;
+ data[1] = value>>16;
+ data[2] = value>> 8;
+ data[3] = value>> 0;
+ return fwrite(data, 1, 4, f)==4;
+}
+
+static int read_string(FILE *f, char **value_out) {
+ unsigned len;
+ if (!read_uint32(f, &len))
+ return 0;
+ *value_out = (char*) malloc(len+1);
+ if (!*value_out)
+ return 0;
+ if (fread(*value_out, len, 1, f)!=1)
+ return 0;
+ (*value_out)[len] = 0;
+ return 1;
+}
+
+static int write_string(FILE *f, const char *value) {
+ unsigned len = strlen(value);
+ if (!write_uint32(f, len))
+ return 0;
+ if (fwrite(value, len, 1, f)!=1)
+ return 0;
+ return 1;
+}
+
+/***/
+
+
+unsigned bOut_getCurrentVersion() {
+ return BOUT_VERSION;
+}
+
+
+static int bOut_checkHeader(FILE *f) {
+ char header[BOUT_MAGIC_SIZE];
+ if (fread(header, BOUT_MAGIC_SIZE, 1, f)!=1)
+ return 0;
+ if (memcmp(header, BOUT_MAGIC, BOUT_MAGIC_SIZE))
+ return 0;
+ return 1;
+}
+
+int bOut_isBOutFile(const char *path) {
+ FILE *f = fopen(path, "rb");
+ int res;
+
+ if (!f)
+ return 0;
+ res = bOut_checkHeader(f);
+ fclose(f);
+
+ return res;
+}
+
+BOut *bOut_fromFile(const char *path) {
+ FILE *f = fopen(path, "rb");
+ BOut *res = 0;
+ unsigned i, version;
+
+ if (!f)
+ goto error;
+ if (!bOut_checkHeader(f))
+ goto error;
+
+ res = (BOut*) calloc(1, sizeof(*res));
+ if (!res)
+ goto error;
+
+ if (!read_uint32(f, &version))
+ goto error;
+
+ if (version > bOut_getCurrentVersion())
+ goto error;
+
+ res->version = version;
+
+ if (!read_uint32(f, &res->numArgs))
+ goto error;
+ res->args = (char**) calloc(res->numArgs, sizeof(*res->args));
+ if (!res->args)
+ goto error;
+
+ for (i=0; i<res->numArgs; i++)
+ if (!read_string(f, &res->args[i]))
+ goto error;
+
+ if (version >= 2) {
+ if (!read_uint32(f, &res->symArgvs))
+ goto error;
+ if (!read_uint32(f, &res->symArgvLen))
+ goto error;
+ }
+
+ if (!read_uint32(f, &res->numObjects))
+ goto error;
+ res->objects = (BOutObject*) calloc(res->numObjects, sizeof(*res->objects));
+ if (!res->objects)
+ goto error;
+ for (i=0; i<res->numObjects; i++) {
+ BOutObject *o = &res->objects[i];
+ if (!read_string(f, &o->name))
+ goto error;
+ if (!read_uint32(f, &o->numBytes))
+ goto error;
+ o->bytes = (unsigned char*) malloc(o->numBytes);
+ if (fread(o->bytes, o->numBytes, 1, f)!=1)
+ goto error;
+ }
+
+ fclose(f);
+
+ return res;
+ error:
+ if (res) {
+ if (res->args) {
+ for (i=0; i<res->numArgs; i++)
+ if (res->args[i])
+ free(res->args[i]);
+ free(res->args);
+ }
+ if (res->objects) {
+ for (i=0; i<res->numObjects; i++) {
+ BOutObject *bo = &res->objects[i];
+ if (bo->name)
+ free(bo->name);
+ if (bo->bytes)
+ free(bo->bytes);
+ }
+ free(res->objects);
+ }
+ free(res);
+ }
+
+ if (f) fclose(f);
+
+ return 0;
+}
+
+int bOut_toFile(BOut *bo, const char *path) {
+ FILE *f = fopen(path, "wb");
+ unsigned i;
+
+ if (!f)
+ goto error;
+ if (fwrite(BOUT_MAGIC, strlen(BOUT_MAGIC), 1, f)!=1)
+ goto error;
+ if (!write_uint32(f, BOUT_VERSION))
+ goto error;
+
+ if (!write_uint32(f, bo->numArgs))
+ goto error;
+ for (i=0; i<bo->numArgs; i++) {
+ if (!write_string(f, bo->args[i]))
+ goto error;
+ }
+
+ if (!write_uint32(f, bo->symArgvs))
+ goto error;
+ if (!write_uint32(f, bo->symArgvLen))
+ goto error;
+
+ if (!write_uint32(f, bo->numObjects))
+ goto error;
+ for (i=0; i<bo->numObjects; i++) {
+ BOutObject *o = &bo->objects[i];
+ if (!write_string(f, o->name))
+ goto error;
+ if (!write_uint32(f, o->numBytes))
+ goto error;
+ if (fwrite(o->bytes, o->numBytes, 1, f)!=1)
+ goto error;
+ }
+
+ fclose(f);
+
+ return 1;
+ error:
+ if (f) fclose(f);
+
+ return 0;
+}
+
+unsigned bOut_numBytes(BOut *bo) {
+ unsigned i, res = 0;
+ for (i=0; i<bo->numObjects; i++)
+ res += bo->objects[i].numBytes;
+ return res;
+}
+
+void bOut_free(BOut *bo) {
+ unsigned i;
+ for (i=0; i<bo->numArgs; i++)
+ free(bo->args[i]);
+ free(bo->args);
+ for (i=0; i<bo->numObjects; i++) {
+ free(bo->objects[i].name);
+ free(bo->objects[i].bytes);
+ }
+ free(bo->objects);
+ free(bo);
+}
diff --git a/lib/Basic/Makefile b/lib/Basic/Makefile
new file mode 100644
index 00000000..d4481e7f
--- /dev/null
+++ b/lib/Basic/Makefile
@@ -0,0 +1,16 @@
+#===-- lib/Basic/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=kleeBasic
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
+
+include $(LEVEL)/Makefile.common
diff --git a/lib/Basic/README.txt b/lib/Basic/README.txt
new file mode 100644
index 00000000..b13df6bd
--- /dev/null
+++ b/lib/Basic/README.txt
@@ -0,0 +1,3 @@
+This directory holds the most basic support facilities provided for
+both the klee and kleaver libraries. The code in this directory should
+have no dependencies on LLVM or any other klee libraries.
diff --git a/lib/Basic/Statistics.cpp b/lib/Basic/Statistics.cpp
new file mode 100644
index 00000000..9c95a891
--- /dev/null
+++ b/lib/Basic/Statistics.cpp
@@ -0,0 +1,84 @@
+//===-- Statistics.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/Statistics.h"
+
+#include <vector>
+
+using namespace klee;
+
+StatisticManager::StatisticManager()
+ : enabled(true),
+ globalStats(0),
+ indexedStats(0),
+ contextStats(0),
+ index(0) {
+}
+
+StatisticManager::~StatisticManager() {
+ if (globalStats) delete[] globalStats;
+ if (indexedStats) delete[] indexedStats;
+}
+
+void StatisticManager::useIndexedStats(unsigned totalIndices) {
+ if (indexedStats) delete[] indexedStats;
+ indexedStats = new uint64_t[totalIndices * stats.size()];
+ memset(indexedStats, 0, sizeof(*indexedStats) * totalIndices * stats.size());
+}
+
+void StatisticManager::registerStatistic(Statistic &s) {
+ if (globalStats) delete[] globalStats;
+ s.id = stats.size();
+ stats.push_back(&s);
+ globalStats = new uint64_t[stats.size()];
+ memset(globalStats, 0, sizeof(*globalStats)*stats.size());
+}
+
+int StatisticManager::getStatisticID(const std::string &name) const {
+ for (unsigned i=0; i<stats.size(); i++)
+ if (stats[i]->getName() == name)
+ return i;
+ return -1;
+}
+
+Statistic *StatisticManager::getStatisticByName(const std::string &name) const {
+ for (unsigned i=0; i<stats.size(); i++)
+ if (stats[i]->getName() == name)
+ return stats[i];
+ return 0;
+}
+
+StatisticManager *klee::theStatisticManager = 0;
+
+static StatisticManager &getStatisticManager() {
+ static StatisticManager sm;
+ theStatisticManager = &sm;
+ return sm;
+}
+
+/* *** */
+
+Statistic::Statistic(const std::string &_name,
+ const std::string &_shortName)
+ : name(_name),
+ shortName(_shortName) {
+ getStatisticManager().registerStatistic(*this);
+}
+
+Statistic::~Statistic() {
+}
+
+Statistic &Statistic::operator +=(const uint64_t addend) {
+ theStatisticManager->incrementStatistic(*this, addend);
+ return *this;
+}
+
+uint64_t Statistic::getValue() const {
+ return theStatisticManager->getValue(*this);
+}