From 266cc79f26aa8df4718f2309808f77a5426f266c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 23 May 2009 02:42:09 +0000 Subject: Changed bout to ktest. Kept "BOUT\n" as the header of test files, for backward compatibility. Also changed KLEE_RUNTEST to KTEST_FILE. Updated tutorial-1. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72312 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/Internal/ADT/BOut.h | 62 ------ include/klee/Internal/ADT/KTest.h | 62 ++++++ include/klee/Interpreter.h | 6 +- lib/Basic/BOut.cpp | 236 --------------------- lib/Basic/KTest.cpp | 236 +++++++++++++++++++++ lib/Core/Executor.cpp | 8 +- lib/Core/Executor.h | 10 +- lib/Core/SeedInfo.cpp | 8 +- lib/Core/SeedInfo.h | 12 +- runtime/Runtest/intrinsics.c | 16 +- test/Feature/DumpStatesOnHalt.c | 2 +- test/Feature/InAndOutOfBounds.c | 2 +- test/Feature/LowerSwitch.c | 4 +- test/Feature/MultipleFreeResolution.c | 2 +- test/Feature/NamedSeedMatching.c | 6 +- test/Feature/OverlappedError.c | 2 +- test/Feature/PreferCex.c | 2 +- .../2007-10-12-failed-make-symbolic-after-copy.c | 2 +- tools/gen-random-bout/gen-random-bout.cpp | 16 +- tools/klee/main.cpp | 38 ++-- www/tutorial-1.html | 36 ++-- 21 files changed, 385 insertions(+), 383 deletions(-) delete mode 100644 include/klee/Internal/ADT/BOut.h create mode 100644 include/klee/Internal/ADT/KTest.h delete mode 100644 lib/Basic/BOut.cpp create mode 100644 lib/Basic/KTest.cpp diff --git a/include/klee/Internal/ADT/BOut.h b/include/klee/Internal/ADT/BOut.h deleted file mode 100644 index 14aeb714..00000000 --- a/include/klee/Internal/ADT/BOut.h +++ /dev/null @@ -1,62 +0,0 @@ -//===-- BOut.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 __COMMON_BOUT_H__ -#define __COMMON_BOUT_H__ - - -#ifdef __cplusplus -extern "C" { -#endif - - typedef struct BOutObject BOutObject; - struct BOutObject { - char *name; - unsigned numBytes; - unsigned char *bytes; - }; - - typedef struct BOut BOut; - struct BOut { - /* file format version */ - unsigned version; - - unsigned numArgs; - char **args; - - unsigned symArgvs; - unsigned symArgvLen; - - unsigned numObjects; - BOutObject *objects; - }; - - - /* returns the current .bout file format version */ - unsigned bOut_getCurrentVersion(); - - /* return true iff file at path matches BOut header */ - int bOut_isBOutFile(const char *path); - - /* returns NULL on (unspecified) error */ - BOut* bOut_fromFile(const char *path); - - /* returns 1 on success, 0 on (unspecified) error */ - int bOut_toFile(BOut *, const char *path); - - /* returns total number of object bytes */ - unsigned bOut_numBytes(BOut *); - - void bOut_free(BOut *); - -#ifdef __cplusplus -} -#endif - -#endif diff --git a/include/klee/Internal/ADT/KTest.h b/include/klee/Internal/ADT/KTest.h new file mode 100644 index 00000000..c6586f9e --- /dev/null +++ b/include/klee/Internal/ADT/KTest.h @@ -0,0 +1,62 @@ +//===-- 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 __COMMON_KTEST_H__ +#define __COMMON_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 diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index eca6e59e..14e653c1 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -14,7 +14,7 @@ #include #include -struct BOut; +struct KTest; namespace llvm { class Function; @@ -102,7 +102,7 @@ public: // supply a test case to replay from. this can be used to drive the // interpretation down a user specified path. use null to reset. - virtual void setReplayOut(const struct BOut *out) = 0; + virtual void setReplayOut(const struct KTest *out) = 0; // supply a list of branch decisions specifying which direction to // take on forks. this can be used to drive the interpretation down @@ -111,7 +111,7 @@ public: // supply a set of symbolic bindings that will be used as "seeds" // for the search. use null to reset. - virtual void useSeeds(const std::vector *seeds) = 0; + virtual void useSeeds(const std::vector *seeds) = 0; virtual void runFunctionAsMain(llvm::Function *f, int argc, diff --git a/lib/Basic/BOut.cpp b/lib/Basic/BOut.cpp deleted file mode 100644 index 42d17e27..00000000 --- a/lib/Basic/BOut.cpp +++ /dev/null @@ -1,236 +0,0 @@ -//===-- 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 -#include -#include - -#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; inumArgs; 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; inumObjects; 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; inumArgs; i++) - if (res->args[i]) - free(res->args[i]); - free(res->args); - } - if (res->objects) { - for (i=0; inumObjects; 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; inumArgs; 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; inumObjects; 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; inumObjects; i++) - res += bo->objects[i].numBytes; - return res; -} - -void bOut_free(BOut *bo) { - unsigned i; - for (i=0; inumArgs; i++) - free(bo->args[i]); - free(bo->args); - for (i=0; inumObjects; i++) { - free(bo->objects[i].name); - free(bo->objects[i].bytes); - } - free(bo->objects); - free(bo); -} diff --git a/lib/Basic/KTest.cpp b/lib/Basic/KTest.cpp new file mode 100644 index 00000000..d17916f5 --- /dev/null +++ b/lib/Basic/KTest.cpp @@ -0,0 +1,236 @@ +//===-- KTest.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/KTest.h" + +#include +#include +#include + +#define KTEST_MAGIC "BOUT\n" +#define KTEST_MAGIC_SIZE 5 +#define KTEST_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 kTest_getCurrentVersion() { + return KTEST_VERSION; +} + + +static int kTest_checkHeader(FILE *f) { + char header[KTEST_MAGIC_SIZE]; + if (fread(header, KTEST_MAGIC_SIZE, 1, f)!=1) + return 0; + if (memcmp(header, KTEST_MAGIC, KTEST_MAGIC_SIZE)) + return 0; + return 1; +} + +int kTest_isKTestFile(const char *path) { + FILE *f = fopen(path, "rb"); + int res; + + if (!f) + return 0; + res = kTest_checkHeader(f); + fclose(f); + + return res; +} + +KTest *kTest_fromFile(const char *path) { + FILE *f = fopen(path, "rb"); + KTest *res = 0; + unsigned i, version; + + if (!f) + goto error; + if (!kTest_checkHeader(f)) + goto error; + + res = (KTest*) calloc(1, sizeof(*res)); + if (!res) + goto error; + + if (!read_uint32(f, &version)) + goto error; + + if (version > kTest_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; inumArgs; 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 = (KTestObject*) calloc(res->numObjects, sizeof(*res->objects)); + if (!res->objects) + goto error; + for (i=0; inumObjects; i++) { + KTestObject *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; inumArgs; i++) + if (res->args[i]) + free(res->args[i]); + free(res->args); + } + if (res->objects) { + for (i=0; inumObjects; i++) { + KTestObject *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 kTest_toFile(KTest *bo, const char *path) { + FILE *f = fopen(path, "wb"); + unsigned i; + + if (!f) + goto error; + if (fwrite(KTEST_MAGIC, strlen(KTEST_MAGIC), 1, f)!=1) + goto error; + if (!write_uint32(f, KTEST_VERSION)) + goto error; + + if (!write_uint32(f, bo->numArgs)) + goto error; + for (i=0; inumArgs; 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; inumObjects; i++) { + KTestObject *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 kTest_numBytes(KTest *bo) { + unsigned i, res = 0; + for (i=0; inumObjects; i++) + res += bo->objects[i].numBytes; + return res; +} + +void kTest_free(KTest *bo) { + unsigned i; + for (i=0; inumArgs; i++) + free(bo->args[i]); + free(bo->args); + for (i=0; inumObjects; i++) { + free(bo->objects[i].name); + free(bo->objects[i].bytes); + } + free(bo->objects); + free(bo); +} diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d3409908..df8fdba8 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -34,7 +34,7 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/Config/config.h" -#include "klee/Internal/ADT/BOut.h" +#include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/RNG.h" #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/InstructionInfoTable.h" @@ -2227,7 +2227,7 @@ void Executor::run(ExecutionState &initialState) { if (usingSeeds) { std::vector &v = seedMap[&initialState]; - for (std::vector::const_iterator it = usingSeeds->begin(), + for (std::vector::const_iterator it = usingSeeds->begin(), ie = usingSeeds->end(); it != ie; ++it) v.push_back(SeedInfo(*it)); @@ -2973,7 +2973,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, for (std::vector::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { SeedInfo &si = *siit; - BOutObject *obj = si.getNextInput(mo, + KTestObject *obj = si.getNextInput(mo, NamedSeedMatching); if (!obj) { @@ -3019,7 +3019,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, if (replayPosition >= replayOut->numObjects) { terminateStateOnError(state, "replay count mismatch", "user.err"); } else { - BOutObject *obj = &replayOut->objects[replayPosition++]; + KTestObject *obj = &replayOut->objects[replayPosition++]; if (obj->numBytes != mo->size) { terminateStateOnError(state, "replay size mismatch", "user.err"); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 76868291..9fa63a04 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -22,7 +22,7 @@ #include #include -struct BOut; +struct KTest; namespace llvm { class BasicBlock; @@ -134,7 +134,7 @@ private: /// When non-null the bindings that will be used for calls to /// klee_make_symbolic in order replay. - const struct BOut *replayOut; + const struct KTest *replayOut; /// When non-null a list of branch decisions to be used for replay. const std::vector *replayPath; /// The index into the current \ref replayOut or \ref replayPath @@ -143,7 +143,7 @@ private: /// When non-null a list of "seed" inputs which will be used to /// drive execution. - const std::vector *usingSeeds; + const std::vector *usingSeeds; /// Disables forking, instead a random path is chosen. Enabled as /// needed to control memory usage. \see fork() @@ -386,7 +386,7 @@ public: symPathWriter = tsw; } - virtual void setReplayOut(const struct BOut *out) { + virtual void setReplayOut(const struct KTest *out) { assert(!replayPath && "cannot replay both buffer and path"); replayOut = out; replayPosition = 0; @@ -401,7 +401,7 @@ public: virtual const llvm::Module * setModule(llvm::Module *module, const ModuleOptions &opts); - virtual void useSeeds(const std::vector *seeds) { + virtual void useSeeds(const std::vector *seeds) { usingSeeds = seeds; } diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index d76d75dc..e6d88bac 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -16,17 +16,17 @@ #include "klee/ExecutionState.h" #include "klee/Expr.h" #include "klee/util/ExprUtil.h" -#include "klee/Internal/ADT/BOut.h" +#include "klee/Internal/ADT/KTest.h" using namespace klee; -BOutObject *SeedInfo::getNextInput(const MemoryObject *mo, +KTestObject *SeedInfo::getNextInput(const MemoryObject *mo, bool byName) { if (byName) { unsigned i; for (i=0; inumObjects; ++i) { - BOutObject *obj = &input->objects[i]; + KTestObject *obj = &input->objects[i]; if (std::string(obj->name) == mo->name) if (used.insert(obj).second) return obj; @@ -38,7 +38,7 @@ BOutObject *SeedInfo::getNextInput(const MemoryObject *mo, if (!used.count(&input->objects[i])) break; if (inumObjects) { - BOutObject *obj = &input->objects[i]; + KTestObject *obj = &input->objects[i]; if (obj->numBytes == mo->size) { used.insert(obj); klee_warning_once(mo, "using seed input %s[%d] for: %s (no name match)", diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h index dd151ed0..0acb130b 100644 --- a/lib/Core/SeedInfo.h +++ b/lib/Core/SeedInfo.h @@ -13,8 +13,8 @@ #include "klee/util/Assignment.h" extern "C" { - struct BOut; - struct BOutObject; + struct KTest; + struct KTestObject; } namespace klee { @@ -24,17 +24,17 @@ namespace klee { class SeedInfo { public: Assignment assignment; - BOut *input; + KTest *input; unsigned inputPosition; - std::set used; + std::set used; public: explicit - SeedInfo(BOut *_input) : assignment(true), + SeedInfo(KTest *_input) : assignment(true), input(_input), inputPosition(0) {} - BOutObject *getNextInput(const MemoryObject *mo, + KTestObject *getNextInput(const MemoryObject *mo, bool byName); /// Patch the seed so that condition is satisfied while retaining as diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index 36efb5c2..bcd072ac 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -19,9 +19,9 @@ #include "klee/klee.h" -#include "klee/Internal/ADT/BOut.h" +#include "klee/Internal/ADT/KTest.h" -static BOut *testData = 0; +static KTest *testData = 0; static unsigned testPosition = 0; static unsigned char rand_byte(void) { @@ -61,21 +61,21 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) { if (!testData) { char tmp[256]; - char *name = getenv("KLEE_RUNTEST"); + char *name = getenv("KTEST_FILE"); if (!name) { - fprintf(stdout, "KLEE-RUNTIME: KLEE_RUNTEST not set, please enter .bout path: "); + fprintf(stdout, "KLEE-RUNTIME: KTEST_FILE not set, please enter .ktest path: "); fflush(stdout); name = tmp; if (!fgets(tmp, sizeof tmp, stdin) || !strlen(tmp)) { - fprintf(stderr, "KLEE-RUNTIME: cannot replay, no KLEE_RUNTEST or user input\n"); + fprintf(stderr, "KLEE-RUNTIME: cannot replay, no KTEST_FILE or user input\n"); exit(1); } tmp[strlen(tmp)-1] = '\0'; /* kill newline */ } - testData = bOut_fromFile(name); + testData = kTest_fromFile(name); if (!testData) { - fprintf(stderr, "KLEE-RUNTIME: unable to open .bout file\n"); + fprintf(stderr, "KLEE-RUNTIME: unable to open .ktest file\n"); exit(1); } } @@ -84,7 +84,7 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) { fprintf(stderr, "ERROR: out of inputs, using zero\n"); memset(array, 0, nbytes); } else { - BOutObject *o = &testData->objects[testPosition++]; + KTestObject *o = &testData->objects[testPosition++]; memcpy(array, o->bytes, nbytesnumBytes ? nbytes : o->numBytes); if (nbytes != o->numBytes) { fprintf(stderr, "ERROR: object sizes differ\n"); diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c index 7e9cf46a..d86b786b 100644 --- a/test/Feature/DumpStatesOnHalt.c +++ b/test/Feature/DumpStatesOnHalt.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc // RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc -// RUN: test -f klee-last/test000001.bout +// RUN: test -f klee-last/test000001.ktest int main() { int x = 10; diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c index 18e5d2b2..ba655b83 100644 --- a/test/Feature/InAndOutOfBounds.c +++ b/test/Feature/InAndOutOfBounds.c @@ -2,7 +2,7 @@ // RUN: %klee %t1.bc // RUN: test -f klee-last/test000001.ptr.err -o -f klee-last/test000002.ptr.err // RUN: test ! -f klee-last/test000001.ptr.err -o ! -f klee-last/test000002.ptr.err -// RUN: test ! -f klee-last/test000003.bout +// RUN: test ! -f klee-last/test000003.ktest unsigned klee_urange(unsigned start, unsigned end) { unsigned x; diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c index c4d9644a..1b92e398 100644 --- a/test/Feature/LowerSwitch.c +++ b/test/Feature/LowerSwitch.c @@ -1,8 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc -// RUN: not test -f klee-last/test000010.bout +// RUN: not test -f klee-last/test000010.ktest // RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc -// RUN: test -f klee-last/test000010.bout +// RUN: test -f klee-last/test000010.ktest #include diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c index 872d6856..8a36f459 100644 --- a/test/Feature/MultipleFreeResolution.c +++ b/test/Feature/MultipleFreeResolution.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: %klee --emit-all-errors %t1.bc -// RUN: ls klee-last/ | grep .out | wc -l | grep 4 +// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4 // RUN: ls klee-last/ | grep .err | wc -l | grep 3 #include diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c index cff34282..bb7f6097 100644 --- a/test/Feature/NamedSeedMatching.c +++ b/test/Feature/NamedSeedMatching.c @@ -1,9 +1,9 @@ // RUN: %llvmgcc -c -g %s -o %t.bc // RUN: rm -rf %t.out // RUN: %klee --output-dir=%t.out %t.bc "initial" -// RUN: test -f %t.out/test000001.bout -// RUN: not test -f %t.out/test000002.bout -// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.bout %t.bc > %t.log +// RUN: test -f %t.out/test000001.ktest +// RUN: not test -f %t.out/test000002.ktest +// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.ktest %t.bc > %t.log // RUN: grep -q "a==3" %t.log // RUN: grep -q "b==4" %t.log // RUN: grep -q "c==5" %t.log diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c index 3c79380c..aa220ed9 100644 --- a/test/Feature/OverlappedError.c +++ b/test/Feature/OverlappedError.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc // RUN: %klee %t1.bc -// RUN: ls klee-last/ | grep .out | wc -l | grep 4 +// RUN: ls klee-last/ | grep .ktest | wc -l | grep 4 // RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2 #include diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c index d73b6076..97ce5101 100644 --- a/test/Feature/PreferCex.c +++ b/test/Feature/PreferCex.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: %klee --exit-on-error %t1.bc -// RUN: klee-bout-tool klee-last/test000001.bout | grep -F 'Hi\x00\x00' +// RUN: ktest-tool klee-last/test000001.ktest | grep -F 'Hi\x00\x00' #include #include diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c index 9d81fad0..e9a280c3 100644 --- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c +++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: %klee %t1.bc -// RUN: test -f klee-last/test000001.bout +// RUN: test -f klee-last/test000001.ktest int main() { unsigned x, y[4]; diff --git a/tools/gen-random-bout/gen-random-bout.cpp b/tools/gen-random-bout/gen-random-bout.cpp index 044c3d24..0a65bda2 100644 --- a/tools/gen-random-bout/gen-random-bout.cpp +++ b/tools/gen-random-bout/gen-random-bout.cpp @@ -7,7 +7,7 @@ #include #include -#include "klee/Internal/ADT/BOut.h" +#include "klee/Internal/ADT/KTest.h" // --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout static int getint(char *i) { @@ -19,9 +19,9 @@ static int getint(char *i) { } #define MAX 64 -static void push_obj(BOut *b, const char *name, unsigned non_zero_bytes, +static void push_obj(KTest *b, const char *name, unsigned non_zero_bytes, unsigned total_bytes) { - BOutObject *o = &b->objects[b->numObjects++]; + KTestObject *o = &b->objects[b->numObjects++]; assert(b->numObjects < MAX); o->name = strdup(name); @@ -37,8 +37,8 @@ static void push_obj(BOut *b, const char *name, unsigned non_zero_bytes, } -static void push_range(BOut *b, const char *name, unsigned value) { - BOutObject *o = &b->objects[b->numObjects++]; +static void push_range(KTest *b, const char *name, unsigned value) { + KTestObject *o = &b->objects[b->numObjects++]; assert(b->numObjects < MAX); o->name = strdup(name); @@ -65,14 +65,14 @@ int main(int argc, char *argv[]) { srandom(seed); else srandom(time(NULL) * getpid()); - BOut b; + KTest b; b.numArgs = argc; b.args = argv; b.symArgvs = 0; b.symArgvLen = 0; b.numObjects = 0; - b.objects = (BOutObject *)malloc(MAX * sizeof *b.objects); + b.objects = (KTestObject *)malloc(MAX * sizeof *b.objects); for(i = 2; i < (unsigned)argc; i++) { if(strcmp(argv[i], "--sym-args") == 0) { @@ -118,7 +118,7 @@ int main(int argc, char *argv[]) { } } - if (!bOut_toFile(&b, "file.bout")) + if (!kTest_toFile(&b, "file.bout")) assert(0); return 0; } diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 0a070452..97911759 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -8,7 +8,7 @@ #include "klee/Interpreter.h" #include "klee/Statistics.h" #include "klee/Config/config.h" -#include "klee/Internal/ADT/BOut.h" +#include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/TreeStream.h" #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/Time.h" @@ -385,16 +385,16 @@ void KleeHandler::processTestCase(const ExecutionState &state, unsigned id = ++m_testIndex; if (success) { - BOut b; + KTest b; b.numArgs = m_argc; b.args = m_argv; b.symArgvs = 0; b.symArgvLen = 0; b.numObjects = out.size(); - b.objects = new BOutObject[b.numObjects]; + b.objects = new KTestObject[b.numObjects]; assert(b.objects); for (unsigned i=0; iname = const_cast(out[i].first.c_str()); o->numBytes = out[i].second.size(); o->bytes = new unsigned char[o->numBytes]; @@ -402,7 +402,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, std::copy(out[i].second.begin(), out[i].second.end(), o->bytes); } - if (!bOut_toFile(&b, getTestFilename("bout", id).c_str())) { + if (!kTest_toFile(&b, getTestFilename("ktest", id).c_str())) { klee_warning("unable to write output test case, losing it"); } @@ -1274,13 +1274,13 @@ int main(int argc, char **argv, char **envp) { it = ReplayOutDir.begin(), ie = ReplayOutDir.end(); it != ie; ++it) KleeHandler::getOutFiles(*it, outFiles); - std::vector bOuts; + std::vector kTests; for (std::vector::iterator it = outFiles.begin(), ie = outFiles.end(); it != ie; ++it) { - BOut *out = bOut_fromFile(it->c_str()); + KTest *out = kTest_fromFile(it->c_str()); if (out) { - bOuts.push_back(out); + kTests.push_back(out); } else { llvm::cerr << "KLEE: unable to open: " << *it << "\n"; } @@ -1294,28 +1294,28 @@ int main(int argc, char **argv, char **envp) { } unsigned i=0; - for (std::vector::iterator - it = bOuts.begin(), ie = bOuts.end(); + for (std::vector::iterator + it = kTests.begin(), ie = kTests.end(); it != ie; ++it) { - BOut *out = *it; + KTest *out = *it; interpreter->setReplayOut(out); - llvm::cerr << "KLEE: replaying: " << *it << " (" << bOut_numBytes(out) << " bytes)" + llvm::cerr << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) << " bytes)" << " (" << ++i << "/" << outFiles.size() << ")\n"; // XXX should put envp in .bout ? interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp); if (interrupted) break; } interpreter->setReplayOut(0); - while (!bOuts.empty()) { - bOut_free(bOuts.back()); - bOuts.pop_back(); + while (!kTests.empty()) { + kTest_free(kTests.back()); + kTests.pop_back(); } } else { - std::vector seeds; + std::vector seeds; for (std::vector::iterator it = SeedOutFile.begin(), ie = SeedOutFile.end(); it != ie; ++it) { - BOut *out = bOut_fromFile(it->c_str()); + KTest *out = kTest_fromFile(it->c_str()); if (!out) { llvm::cerr << "KLEE: unable to open: " << *it << "\n"; exit(1); @@ -1330,7 +1330,7 @@ int main(int argc, char **argv, char **envp) { for (std::vector::iterator it2 = outFiles.begin(), ie = outFiles.end(); it2 != ie; ++it2) { - BOut *out = bOut_fromFile(it2->c_str()); + KTest *out = kTest_fromFile(it2->c_str()); if (!out) { llvm::cerr << "KLEE: unable to open: " << *it2 << "\n"; exit(1); @@ -1356,7 +1356,7 @@ int main(int argc, char **argv, char **envp) { interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp); while (!seeds.empty()) { - bOut_free(seeds.back()); + kTest_free(seeds.back()); seeds.pop_back(); } } diff --git a/www/tutorial-1.html b/www/tutorial-1.html index 389359b2..9f458237 100644 --- a/www/tutorial-1.html +++ b/www/tutorial-1.html @@ -101,33 +101,34 @@ 
   $ ls klee-last/
-  assembly.ll  messages.txt  run.stats        test000002.bout  warnings.txt 
-  info         run.istats    test000001.bout  test000003.bout
+ assembly.ll run.istats test000002.ktest + info run.stats test000003.ktest + messages.txt test000001.ktest warnings.txt Please click here if you would like an overview of the files generated by KLEE. In this tutorial, we only focus on the actual test files generated by KLEE.

KLEE-generated test cases

The test cases generated by KLEE - are written in files with extension .bout. These are - binary files, which can be read with the klee-bout-tool + are written in files with extension .ktest. These are + binary files, which can be read with the ktest-tool utility. So let's examine each file: 
-  $ klee-bout-tool klee-last/test000001.bout 
-  bout file  : 'klee-last/test000001.bout'
+  $ ktest-tool klee-last/test000001.ktest 
+  bout file  : 'klee-last/test000001.ktest'
   args       : ['demo.o']
   num objects: 1
   object    0: name: 'input'
   object    0: size: 1
-  object    0: data: 'b' 
+  object    0: data: 'b'
 
-  $ klee-bout-tool klee-last/test000002.bout 
+  $ ktest-tool klee-last/test000002.ktest 
   ...
   object    0: data: '~'
- 
-  $ klee-bout-tool klee-last/test000003.bout 
-  ...
+
+  $ ktest-tool klee-last/test000003.ktest 
+  ..
   object    0: data: '\x00'
In each test file, KLEE reports the arguments with which the program @@ -150,21 +151,22 @@ hand, (or with the help of an existing test infrastructure), KLEE provides a convenient replay library, which simply replaces the call to klee_make_symbolic with a call to a function - that assigns to our input the value stored in the .bout file. + that assigns to our input the value stored in the .ktest + file. To use it, simply link your program with the libkleeRuntest - library and set the KLEE_RUNTEST environment variable to + library and set the KTEST_FILE environment variable to point to the name of the desired test case: 
-  $ gcc path/to/klee/Release/lib/libkleeRuntest.dylib demo.c
-  $ KLEE_RUNTEST=klee-last/test000001.bout ./a.out 
+  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
+  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
   $ echo $?
   1
-  $ KLEE_RUNTEST=klee-last/test000002.bout ./a.out 
+  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
   $ echo $?
   0
-  $ KLEE_RUNTEST=klee-last/test000003.bout ./a.out
+  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
   $ echo $?
   0
-- cgit 1.4.1