about summary refs log tree commit diff homepage
path: root/runtime
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2017-01-14 19:44:08 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2017-01-14 23:03:06 +0000
commitdcc709dd23fc8a50d5dc087d4d5961dea041bf01 (patch)
tree84c553f78bc9e8bdcdd5b7aa2e2c9c78d84494dc /runtime
parent6137888c07ab45bee354ff7b66f6f313ea158da8 (diff)
downloadklee-dcc709dd23fc8a50d5dc087d4d5961dea041bf01.tar.gz
Change how error handling is done in libkleeRuntest.
Previously error messages would be emitted but execution would continue
which might not be desirable.

Now a wrapper function (for fprintf) `report_internal_error()` is used
which will cause the program to exit. The older behaviour of continuing
to execute after an error can be achieved by setting a new environment
variable `KLEE_RUN_TEST_ERRORS_NON_FATAL`.

This commit also adds a test for each error case.
Diffstat (limited to 'runtime')
-rw-r--r--runtime/Runtest/intrinsics.c42
1 files changed, 29 insertions, 13 deletions
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index d67f093e..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;
 
@@ -82,7 +100,7 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
 
   for (;; ++testPosition) {
     if (testPosition >= testData->numObjects) {
-      fprintf(stderr, "ERROR: out of inputs, using zero\n");
+      report_internal_error("out of inputs. Will use zero if continuing.");
       memset(array, 0, nbytes);
       break;
     } else {
@@ -95,13 +113,14 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
         continue;
       }
       if (strcmp(name, o->name) != 0) {
-        fprintf(stderr, "ERROR: object name mismatch. Requesting \"%s\" but "
-                        "returning \"%s\"",
-                name, o->name);
+        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) {
-        fprintf(stderr, "ERROR: object sizes differ\n");
+        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);
       }
@@ -119,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");
   }
 }
 
@@ -148,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;
 }