aboutsummaryrefslogtreecommitdiffhomepage
path: root/runtime
diff options
context:
space:
mode:
authorAndrea Mattavelli <andreamattavelli@users.noreply.github.com>2017-01-16 16:36:42 +0000
committerGitHub <noreply@github.com>2017-01-16 16:36:42 +0000
commitaedbca881945da47005835a405188041b40ae7cc (patch)
tree84c553f78bc9e8bdcdd5b7aa2e2c9c78d84494dc /runtime
parent23e656156e4790a06a295d48932db53f2a582227 (diff)
parentdcc709dd23fc8a50d5dc087d4d5961dea041bf01 (diff)
downloadklee-aedbca881945da47005835a405188041b40ae7cc.tar.gz
Merge pull request #566 from delcypher/fix_libkleeruntest
Fixes and testing for libkleeRuntest
Diffstat (limited to 'runtime')
-rw-r--r--runtime/Runtest/Makefile11
-rw-r--r--runtime/Runtest/intrinsics.c69
2 files changed, 62 insertions, 18 deletions
diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile
index 666fe06d..82e21345 100644
--- a/runtime/Runtest/Makefile
+++ b/runtime/Runtest/Makefile
@@ -59,3 +59,14 @@ ifeq ($(HOST_OS), $(filter $(HOST_OS), Linux GNU GNU/kFreeBSD))
# Don't allow unresolved symbols.
LLVMLibsOptions += -Wl,--no-undefined
endif
+
+ifeq ($(HOST_OS), Linux)
+ # HACK: Setup symlinks that `ldconfig` would set up
+ # so that libkleeRuntest can be used from the build directory.
+ # This is needed to run tests.
+ sym_link_name := $(SharedLibDir)/$(SharedPrefix)$(LIBRARYNAME)$(SHLIBEXT).$(SHARED_VERSION)
+
+all:: $(LibName.SO)
+ $(Verb) [ ! -e "$(sym_link_name)" ] && ln -s $(LibName.SO) "$(sym_link_name)" || echo ""
+
+endif
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 2302e278..4d785ee2 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -10,8 +10,9 @@
/* Straight C for linking simplicity */
#include <assert.h>
-#include <stdlib.h>
+#include <stdarg.h>
#include <stdio.h>
+#include <stdlib.h>
#include <string.h>
#include <sys/mman.h>
#include <sys/time.h>
@@ -31,6 +32,23 @@ static unsigned char rand_byte(void) {
return x & 0xFF;
}
+static void report_internal_error(const char *msg, ...)
+ __attribute__((format(printf, 1, 2)));
+static void report_internal_error(const char *msg, ...) {
+ fprintf(stderr, "KLEE_RUN_TEST_ERROR: ");
+ va_list ap;
+ va_start(ap, msg);
+ vfprintf(stderr, msg, ap);
+ va_end(ap);
+ fprintf(stderr, "\n");
+ char *testErrorsNonFatal = getenv("KLEE_RUN_TEST_ERRORS_NON_FATAL");
+ if (testErrorsNonFatal) {
+ fprintf(stderr, "KLEE_RUN_TEST_ERROR: Forcing execution to continue\n");
+ } else {
+ exit(1);
+ }
+}
+
void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
static int rand_init = -1;
@@ -80,16 +98,34 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
}
}
- if (testPosition >= testData->numObjects) {
- fprintf(stderr, "ERROR: out of inputs, using zero\n");
- memset(array, 0, nbytes);
- } else {
- 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");
- if (o->numBytes < nbytes)
- memset((char*) array + o->numBytes, 0, nbytes - o->numBytes);
+ for (;; ++testPosition) {
+ if (testPosition >= testData->numObjects) {
+ report_internal_error("out of inputs. Will use zero if continuing.");
+ memset(array, 0, nbytes);
+ break;
+ } else {
+ KTestObject *o = &testData->objects[testPosition];
+ if (strcmp("model_version", o->name) == 0 &&
+ strcmp("model_version", name) != 0) {
+ // Skip over this KTestObject because we've hit
+ // `model_version` which is from the POSIX runtime
+ // and the caller didn't ask for it.
+ continue;
+ }
+ if (strcmp(name, o->name) != 0) {
+ report_internal_error(
+ "object name mismatch. Requesting \"%s\" but returning \"%s\"",
+ name, o->name);
+ }
+ memcpy(array, o->bytes, nbytes < o->numBytes ? nbytes : o->numBytes);
+ if (nbytes != o->numBytes) {
+ report_internal_error("object sizes differ. Expected %zu but got %u",
+ nbytes, o->numBytes);
+ if (o->numBytes < nbytes)
+ memset((char *)array + o->numBytes, 0, nbytes - o->numBytes);
+ }
+ ++testPosition;
+ break;
}
}
}
@@ -102,14 +138,13 @@ uintptr_t klee_choose(uintptr_t n) {
uintptr_t x;
klee_make_symbolic(&x, sizeof x, "klee_choose");
if(x >= n)
- fprintf(stderr, "ERROR: max = %ld, got = %ld\n", n, x);
- assert(x < n);
+ report_internal_error("klee_choose failure. max = %ld, got = %ld\n", n, x);
return x;
}
void klee_assume(uintptr_t x) {
if (!x) {
- fprintf(stderr, "ERROR: invalid klee_assume\n");
+ report_internal_error("invalid klee_assume");
}
}
@@ -131,10 +166,8 @@ int klee_range(int begin, int end, const char* name) {
int x;
klee_make_symbolic(&x, sizeof x, name);
if (x<begin || x>=end) {
- fprintf(stderr,
- "KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n",
- begin, end, name, x);
- abort();
+ report_internal_error("invalid klee_range(%u,%u,%s) value, got: %u\n",
+ begin, end, name, x);
}
return x;
}