Merge pull request #566 from delcypher/fix_libkleeruntest

Fixes and testing for libkleeRuntest

1 files changed, 51 insertions, 18 deletions

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;
 }