[llvm-commits] [klee] r72312 - in /klee/trunk: include/klee/ include/klee/Internal/ADT/ lib/Basic/ lib/Core/ runtime/Runtest/ test/Feature/ test/regression/ tools/gen-random-bout/ tools/klee/ www/
Cristian Cadar
cristic at cs.stanford.edu
Fri May 22 19:42:09 PDT 2009
Author: cristic
Date: Fri May 22 21:42:09 2009
New Revision: 72312
URL: http://llvm.org/viewvc/llvm-project?rev=72312&view=rev
Log:
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.
Added:
klee/trunk/include/klee/Internal/ADT/KTest.h
- copied, changed from r72305, klee/trunk/include/klee/Internal/ADT/BOut.h
klee/trunk/lib/Basic/KTest.cpp
- copied, changed from r72305, klee/trunk/lib/Basic/BOut.cpp
Removed:
klee/trunk/include/klee/Internal/ADT/BOut.h
klee/trunk/lib/Basic/BOut.cpp
Modified:
klee/trunk/include/klee/Interpreter.h
klee/trunk/lib/Core/Executor.cpp
klee/trunk/lib/Core/Executor.h
klee/trunk/lib/Core/SeedInfo.cpp
klee/trunk/lib/Core/SeedInfo.h
klee/trunk/runtime/Runtest/intrinsics.c
klee/trunk/test/Feature/DumpStatesOnHalt.c
klee/trunk/test/Feature/InAndOutOfBounds.c
klee/trunk/test/Feature/LowerSwitch.c
klee/trunk/test/Feature/MultipleFreeResolution.c
klee/trunk/test/Feature/NamedSeedMatching.c
klee/trunk/test/Feature/OverlappedError.c
klee/trunk/test/Feature/PreferCex.c
klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
klee/trunk/tools/gen-random-bout/gen-random-bout.cpp
klee/trunk/tools/klee/main.cpp
klee/trunk/www/tutorial-1.html
Removed: klee/trunk/include/klee/Internal/ADT/BOut.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/Internal/ADT/BOut.h?rev=72311&view=auto
==============================================================================
--- klee/trunk/include/klee/Internal/ADT/BOut.h (original)
+++ klee/trunk/include/klee/Internal/ADT/BOut.h (removed)
@@ -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
Copied: klee/trunk/include/klee/Internal/ADT/KTest.h (from r72305, klee/trunk/include/klee/Internal/ADT/BOut.h)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/Internal/ADT/KTest.h?p2=klee/trunk/include/klee/Internal/ADT/KTest.h&p1=klee/trunk/include/klee/Internal/ADT/BOut.h&r1=72305&r2=72312&rev=72312&view=diff
==============================================================================
--- klee/trunk/include/klee/Internal/ADT/BOut.h (original)
+++ klee/trunk/include/klee/Internal/ADT/KTest.h Fri May 22 21:42:09 2009
@@ -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 @@
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
}
Modified: klee/trunk/include/klee/Interpreter.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/Interpreter.h?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/include/klee/Interpreter.h (original)
+++ klee/trunk/include/klee/Interpreter.h Fri May 22 21:42:09 2009
@@ -14,7 +14,7 @@
#include <map>
#include <set>
-struct BOut;
+struct KTest;
namespace llvm {
class Function;
@@ -102,7 +102,7 @@
// 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 @@
// 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,
Removed: klee/trunk/lib/Basic/BOut.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Basic/BOut.cpp?rev=72311&view=auto
==============================================================================
--- klee/trunk/lib/Basic/BOut.cpp (original)
+++ klee/trunk/lib/Basic/BOut.cpp (removed)
@@ -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 <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);
-}
Copied: klee/trunk/lib/Basic/KTest.cpp (from r72305, klee/trunk/lib/Basic/BOut.cpp)
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Basic/KTest.cpp?p2=klee/trunk/lib/Basic/KTest.cpp&p1=klee/trunk/lib/Basic/BOut.cpp&r1=72305&r2=72312&rev=72312&view=diff
==============================================================================
--- klee/trunk/lib/Basic/BOut.cpp (original)
+++ klee/trunk/lib/Basic/KTest.cpp Fri May 22 21:42:09 2009
@@ -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 @@
/***/
-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 @@
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 @@
}
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 @@
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 @@
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 @@
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]);
Modified: klee/trunk/lib/Core/Executor.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Executor.cpp?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/lib/Core/Executor.cpp (original)
+++ klee/trunk/lib/Core/Executor.cpp Fri May 22 21:42:09 2009
@@ -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 @@
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 @@
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 @@
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 {
Modified: klee/trunk/lib/Core/Executor.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Executor.h?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/lib/Core/Executor.h (original)
+++ klee/trunk/lib/Core/Executor.h Fri May 22 21:42:09 2009
@@ -22,7 +22,7 @@
#include <map>
#include <set>
-struct BOut;
+struct KTest;
namespace llvm {
class BasicBlock;
@@ -134,7 +134,7 @@
/// 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 @@
/// 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 @@
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 @@
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;
}
Modified: klee/trunk/lib/Core/SeedInfo.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/SeedInfo.cpp?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/lib/Core/SeedInfo.cpp (original)
+++ klee/trunk/lib/Core/SeedInfo.cpp Fri May 22 21:42:09 2009
@@ -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 @@
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)",
Modified: klee/trunk/lib/Core/SeedInfo.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/SeedInfo.h?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/lib/Core/SeedInfo.h (original)
+++ klee/trunk/lib/Core/SeedInfo.h Fri May 22 21:42:09 2009
@@ -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 @@
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
Modified: klee/trunk/runtime/Runtest/intrinsics.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/runtime/Runtest/intrinsics.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/runtime/Runtest/intrinsics.c (original)
+++ klee/trunk/runtime/Runtest/intrinsics.c Fri May 22 21:42:09 2009
@@ -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 @@
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 @@
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");
Modified: klee/trunk/test/Feature/DumpStatesOnHalt.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/DumpStatesOnHalt.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/DumpStatesOnHalt.c (original)
+++ klee/trunk/test/Feature/DumpStatesOnHalt.c Fri May 22 21:42:09 2009
@@ -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;
Modified: klee/trunk/test/Feature/InAndOutOfBounds.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/InAndOutOfBounds.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/InAndOutOfBounds.c (original)
+++ klee/trunk/test/Feature/InAndOutOfBounds.c Fri May 22 21:42:09 2009
@@ -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;
Modified: klee/trunk/test/Feature/LowerSwitch.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/LowerSwitch.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/LowerSwitch.c (original)
+++ klee/trunk/test/Feature/LowerSwitch.c Fri May 22 21:42:09 2009
@@ -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>
Modified: klee/trunk/test/Feature/MultipleFreeResolution.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/MultipleFreeResolution.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/MultipleFreeResolution.c (original)
+++ klee/trunk/test/Feature/MultipleFreeResolution.c Fri May 22 21:42:09 2009
@@ -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>
Modified: klee/trunk/test/Feature/NamedSeedMatching.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/NamedSeedMatching.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/NamedSeedMatching.c (original)
+++ klee/trunk/test/Feature/NamedSeedMatching.c Fri May 22 21:42:09 2009
@@ -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
Modified: klee/trunk/test/Feature/OverlappedError.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/OverlappedError.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/OverlappedError.c (original)
+++ klee/trunk/test/Feature/OverlappedError.c Fri May 22 21:42:09 2009
@@ -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>
Modified: klee/trunk/test/Feature/PreferCex.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/Feature/PreferCex.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/Feature/PreferCex.c (original)
+++ klee/trunk/test/Feature/PreferCex.c Fri May 22 21:42:09 2009
@@ -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>
Modified: klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c (original)
+++ klee/trunk/test/regression/2007-10-12-failed-make-symbolic-after-copy.c Fri May 22 21:42:09 2009
@@ -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];
Modified: klee/trunk/tools/gen-random-bout/gen-random-bout.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/tools/gen-random-bout/gen-random-bout.cpp?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/tools/gen-random-bout/gen-random-bout.cpp (original)
+++ klee/trunk/tools/gen-random-bout/gen-random-bout.cpp Fri May 22 21:42:09 2009
@@ -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 @@
}
#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_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 @@
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 @@
}
}
- if (!bOut_toFile(&b, "file.bout"))
+ if (!kTest_toFile(&b, "file.bout"))
assert(0);
return 0;
}
Modified: klee/trunk/tools/klee/main.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/tools/klee/main.cpp?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/tools/klee/main.cpp (original)
+++ klee/trunk/tools/klee/main.cpp Fri May 22 21:42:09 2009
@@ -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 @@
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 @@
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 @@
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 @@
}
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 @@
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 @@
interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
while (!seeds.empty()) {
- bOut_free(seeds.back());
+ kTest_free(seeds.back());
seeds.pop_back();
}
}
Modified: klee/trunk/www/tutorial-1.html
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/www/tutorial-1.html?rev=72312&r1=72311&r2=72312&view=diff
==============================================================================
--- klee/trunk/www/tutorial-1.html (original)
+++ klee/trunk/www/tutorial-1.html Fri May 22 21:42:09 2009
@@ -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>
More information about the llvm-commits
mailing list