diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2009-05-23 02:42:09 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2009-05-23 02:42:09 +0000 |
commit | 266cc79f26aa8df4718f2309808f77a5426f266c (patch) | |
tree | 640584c9eec64bb834a5452ff908145e4c5c8362 | |
parent | ac6570f762e6520a4458d53963beb5bd4578a2f0 (diff) | |
download | klee-266cc79f26aa8df4718f2309808f77a5426f266c.tar.gz |
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
-rw-r--r-- | include/klee/Internal/ADT/KTest.h (renamed from include/klee/Internal/ADT/BOut.h) | 32 | ||||
-rw-r--r-- | include/klee/Interpreter.h | 6 | ||||
-rw-r--r-- | lib/Basic/KTest.cpp (renamed from lib/Basic/BOut.cpp) | 54 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 8 | ||||
-rw-r--r-- | lib/Core/Executor.h | 10 | ||||
-rw-r--r-- | lib/Core/SeedInfo.cpp | 8 | ||||
-rw-r--r-- | lib/Core/SeedInfo.h | 12 | ||||
-rw-r--r-- | runtime/Runtest/intrinsics.c | 16 | ||||
-rw-r--r-- | test/Feature/DumpStatesOnHalt.c | 2 | ||||
-rw-r--r-- | test/Feature/InAndOutOfBounds.c | 2 | ||||
-rw-r--r-- | test/Feature/LowerSwitch.c | 4 | ||||
-rw-r--r-- | test/Feature/MultipleFreeResolution.c | 2 | ||||
-rw-r--r-- | test/Feature/NamedSeedMatching.c | 6 | ||||
-rw-r--r-- | test/Feature/OverlappedError.c | 2 | ||||
-rw-r--r-- | test/Feature/PreferCex.c | 2 | ||||
-rw-r--r-- | test/regression/2007-10-12-failed-make-symbolic-after-copy.c | 2 | ||||
-rw-r--r-- | tools/gen-random-bout/gen-random-bout.cpp | 16 | ||||
-rw-r--r-- | tools/klee/main.cpp | 38 | ||||
-rw-r--r-- | www/tutorial-1.html | 36 |
19 files changed, 130 insertions, 128 deletions
diff --git a/include/klee/Internal/ADT/BOut.h b/include/klee/Internal/ADT/KTest.h index 14aeb714..c6586f9e 100644 --- a/include/klee/Internal/ADT/BOut.h +++ b/include/klee/Internal/ADT/KTest.h @@ -1,4 +1,4 @@ -//===-- BOut.h --------------------------------------------------*- C++ -*-===// +//===-- KTest.h --------------------------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // @@ -7,23 +7,23 @@ // //===----------------------------------------------------------------------===// -#ifndef __COMMON_BOUT_H__ -#define __COMMON_BOUT_H__ +#ifndef __COMMON_KTEST_H__ +#define __COMMON_KTEST_H__ #ifdef __cplusplus extern "C" { #endif - typedef struct BOutObject BOutObject; - struct BOutObject { + typedef struct KTestObject KTestObject; + struct KTestObject { char *name; unsigned numBytes; unsigned char *bytes; }; - typedef struct BOut BOut; - struct BOut { + typedef struct KTest KTest; + struct KTest { /* file format version */ unsigned version; @@ -34,26 +34,26 @@ extern "C" { unsigned symArgvLen; unsigned numObjects; - BOutObject *objects; + KTestObject *objects; }; - /* returns the current .bout file format version */ - unsigned bOut_getCurrentVersion(); + /* returns the current .ktest file format version */ + unsigned kTest_getCurrentVersion(); - /* return true iff file at path matches BOut header */ - int bOut_isBOutFile(const char *path); + /* return true iff file at path matches KTest header */ + int kTest_isKTestFile(const char *path); /* returns NULL on (unspecified) error */ - BOut* bOut_fromFile(const char *path); + KTest* kTest_fromFile(const char *path); /* returns 1 on success, 0 on (unspecified) error */ - int bOut_toFile(BOut *, const char *path); + int kTest_toFile(KTest *, const char *path); /* returns total number of object bytes */ - unsigned bOut_numBytes(BOut *); + unsigned kTest_numBytes(KTest *); - void bOut_free(BOut *); + void kTest_free(KTest *); #ifdef __cplusplus } 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 <map> #include <set> -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<struct BOut *> *seeds) = 0; + virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0; virtual void runFunctionAsMain(llvm::Function *f, int argc, diff --git a/lib/Basic/BOut.cpp b/lib/Basic/KTest.cpp index 42d17e27..d17916f5 100644 --- a/lib/Basic/BOut.cpp +++ b/lib/Basic/KTest.cpp @@ -1,4 +1,4 @@ -//===-- BOut.c ------------------------------------------------------------===// +//===-- KTest.cpp ---------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,15 +7,15 @@ // //===----------------------------------------------------------------------===// -#include "klee/Internal/ADT/BOut.h" +#include "klee/Internal/ADT/KTest.h" #include <stdlib.h> #include <string.h> #include <stdio.h> -#define BOUT_MAGIC "BOUT\n" -#define BOUT_MAGIC_SIZE 5 -#define BOUT_VERSION 2 +#define KTEST_MAGIC "BOUT\n" +#define KTEST_MAGIC_SIZE 5 +#define KTEST_VERSION 2 /***/ @@ -61,50 +61,50 @@ static int write_string(FILE *f, const char *value) { /***/ -unsigned bOut_getCurrentVersion() { - return BOUT_VERSION; +unsigned kTest_getCurrentVersion() { + return KTEST_VERSION; } -static int bOut_checkHeader(FILE *f) { - char header[BOUT_MAGIC_SIZE]; - if (fread(header, BOUT_MAGIC_SIZE, 1, f)!=1) +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, BOUT_MAGIC, BOUT_MAGIC_SIZE)) + if (memcmp(header, KTEST_MAGIC, KTEST_MAGIC_SIZE)) return 0; return 1; } -int bOut_isBOutFile(const char *path) { +int kTest_isKTestFile(const char *path) { FILE *f = fopen(path, "rb"); int res; if (!f) return 0; - res = bOut_checkHeader(f); + res = kTest_checkHeader(f); fclose(f); return res; } -BOut *bOut_fromFile(const char *path) { +KTest *kTest_fromFile(const char *path) { FILE *f = fopen(path, "rb"); - BOut *res = 0; + KTest *res = 0; unsigned i, version; if (!f) goto error; - if (!bOut_checkHeader(f)) + if (!kTest_checkHeader(f)) goto error; - res = (BOut*) calloc(1, sizeof(*res)); + res = (KTest*) calloc(1, sizeof(*res)); if (!res) goto error; if (!read_uint32(f, &version)) goto error; - if (version > bOut_getCurrentVersion()) + if (version > kTest_getCurrentVersion()) goto error; res->version = version; @@ -128,11 +128,11 @@ BOut *bOut_fromFile(const char *path) { if (!read_uint32(f, &res->numObjects)) goto error; - res->objects = (BOutObject*) calloc(res->numObjects, sizeof(*res->objects)); + res->objects = (KTestObject*) calloc(res->numObjects, sizeof(*res->objects)); if (!res->objects) goto error; for (i=0; i<res->numObjects; i++) { - BOutObject *o = &res->objects[i]; + KTestObject *o = &res->objects[i]; if (!read_string(f, &o->name)) goto error; if (!read_uint32(f, &o->numBytes)) @@ -155,7 +155,7 @@ BOut *bOut_fromFile(const char *path) { } if (res->objects) { for (i=0; i<res->numObjects; i++) { - BOutObject *bo = &res->objects[i]; + KTestObject *bo = &res->objects[i]; if (bo->name) free(bo->name); if (bo->bytes) @@ -171,15 +171,15 @@ BOut *bOut_fromFile(const char *path) { return 0; } -int bOut_toFile(BOut *bo, const char *path) { +int kTest_toFile(KTest *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) + if (fwrite(KTEST_MAGIC, strlen(KTEST_MAGIC), 1, f)!=1) goto error; - if (!write_uint32(f, BOUT_VERSION)) + if (!write_uint32(f, KTEST_VERSION)) goto error; if (!write_uint32(f, bo->numArgs)) @@ -197,7 +197,7 @@ int bOut_toFile(BOut *bo, const char *path) { if (!write_uint32(f, bo->numObjects)) goto error; for (i=0; i<bo->numObjects; i++) { - BOutObject *o = &bo->objects[i]; + KTestObject *o = &bo->objects[i]; if (!write_string(f, o->name)) goto error; if (!write_uint32(f, o->numBytes)) @@ -215,14 +215,14 @@ int bOut_toFile(BOut *bo, const char *path) { return 0; } -unsigned bOut_numBytes(BOut *bo) { +unsigned kTest_numBytes(KTest *bo) { unsigned i, res = 0; for (i=0; i<bo->numObjects; i++) res += bo->objects[i].numBytes; return res; } -void bOut_free(BOut *bo) { +void kTest_free(KTest *bo) { unsigned i; for (i=0; i<bo->numArgs; i++) free(bo->args[i]); 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<SeedInfo> &v = seedMap[&initialState]; - for (std::vector<BOut*>::const_iterator it = usingSeeds->begin(), + for (std::vector<KTest*>::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<SeedInfo>::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 <map> #include <set> -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<bool> *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<struct BOut *> *usingSeeds; + const std::vector<struct KTest *> *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<struct BOut *> *seeds) { + virtual void useSeeds(const std::vector<struct KTest *> *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; i<input->numObjects; ++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 (i<input->numObjects) { - 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<struct BOutObject*> used; + std::set<struct KTestObject*> 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, nbytes<o->numBytes ? 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 <stdio.h> 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 <stdlib.h> 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 <stdlib.h> 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 <assert.h> #include <stdlib.h> 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 <time.h> #include <unistd.h> -#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; i<b.numObjects; i++) { - BOutObject *o = &b.objects[i]; + KTestObject *o = &b.objects[i]; o->name = const_cast<char*>(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<BOut*> bOuts; + std::vector<KTest*> kTests; for (std::vector<std::string>::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<BOut*>::iterator - it = bOuts.begin(), ie = bOuts.end(); + for (std::vector<KTest*>::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<BOut *> seeds; + std::vector<KTest *> seeds; for (std::vector<std::string>::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<std::string>::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 @@ <pre class="output"> $ ls klee-last/ - assembly.ll messages.txt run.stats test000002.bout warnings.txt - info run.istats test000001.bout test000003.bout </pre> + assembly.ll run.istats test000002.ktest + info run.stats test000003.ktest + messages.txt test000001.ktest warnings.txt </pre> Please click <a href="klee-files.html">here</a> 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. <h2>KLEE-generated test cases</h2> The test cases generated by KLEE - are written in files with extension <tt>.bout</tt>. These are - binary files, which can be read with the <tt>klee-bout-tool</tt> + are written in files with extension <tt>.ktest</tt>. These are + binary files, which can be read with the <tt>ktest-tool</tt> utility. So let's examine each file: <pre class="output"> - $ 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' </pre> 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 <i>replay library</i>, which simply replaces the call to <tt>klee_make_symbolic</tt> 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 <tt>.ktest</tt> + file. To use it, simply link your program with the <tt>libkleeRuntest</tt> - library and set the <tt>KLEE_RUNTEST</tt> environment variable to + library and set the <tt>KTEST_FILE</tt> environment variable to point to the name of the desired test case: <pre class="output"> - $ 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 </pre> |