about summary refs log tree commit diff homepage
path: root/runtime
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2010-06-28 15:07:59 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2010-06-28 15:07:59 +0000
commite3414c0e8cc91a35cdcae09c0af8162b8f7c2f94 (patch)
tree112586608310b81d1179c003fd8a73734e2577c9 /runtime
parentff0d675fc2861e34e1f0767af6b8b73e1a854889 (diff)
downloadklee-e3414c0e8cc91a35cdcae09c0af8162b8f7c2f94.tar.gz
Applied Stefan Bucur's patch from
http://llvm.org/bugs/show_bug.cgi?id=6690.  

The patch adds specialized versions of klee_get_value for different
types, fixing the previous klee_get_value function that sometimes
truncated 64bit parameters to 32bit.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107006 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'runtime')
-rw-r--r--runtime/POSIX/fd.c6
-rw-r--r--runtime/POSIX/klee_init_env.c2
-rw-r--r--runtime/Runtest/intrinsics.c28
-rw-r--r--runtime/klee-libc/klee-choose.c4
4 files changed, 26 insertions, 14 deletions
diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index d94604fa..b9a848d0 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -1251,13 +1251,13 @@ char *getcwd(char *buf, size_t size) {
 
 static void *__concretize_ptr(const void *p) {
   /* XXX 32-bit assumption */
-  char *pc = (char*) klee_get_value((unsigned) (long) p);
+  char *pc = (char*) klee_get_valuel((long) p);
   klee_assume(pc == p);
   return pc;
 }
 
 static size_t __concretize_size(size_t s) {
-  size_t sc = klee_get_value(s);
+  size_t sc = klee_get_valuel((long)s);
   klee_assume(sc == s);
   return sc;
 }
@@ -1276,7 +1276,7 @@ static const char *__concretize_string(const char *s) {
         *sc++ = '/';
       } 
     } else {
-      char cc = (char) klee_get_value(c);
+      char cc = (char) klee_get_valuel((long)c);
       klee_assume(cc == c);
       *sc++ = cc;
       if (!cc) break;
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 5c1cc4fb..2a6b6f68 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -8,7 +8,9 @@
 //===----------------------------------------------------------------------===//
 
 #include "klee/klee.h"
+#ifndef _LARGEFILE64_SOURCE
 #define _LARGEFILE64_SOURCE
+#endif
 #include "fd.h"
 
 #include <stdlib.h>
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 7ec21901..2302e278 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -31,7 +31,7 @@ static unsigned char rand_byte(void) {
   return x & 0xFF;
 }
 
-void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
+void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
   static int rand_init = -1;
 
   if (rand_init == -1) {
@@ -52,7 +52,7 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
       *v = rand() % 69;
     } else {
       char *c = array;
-      unsigned i;
+      size_t i;
       for (i=0; i<nbytes; i++)
         c[i] = rand_byte();
     }
@@ -98,24 +98,34 @@ void klee_silent_exit(int x) {
   exit(x);
 }
 
-unsigned klee_choose(unsigned n) {
-  unsigned x;
+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 = %d, got = %d\n", n, x);
+    fprintf(stderr, "ERROR: max = %ld, got = %ld\n", n, x);
   assert(x < n);
   return x;
 }
 
-void klee_assume(unsigned x) {
+void klee_assume(uintptr_t x) {
   if (!x) {
     fprintf(stderr, "ERROR: invalid klee_assume\n");
   }
 }
 
-unsigned klee_get_value(unsigned x) {
-  return x;
-}
+#define KLEE_GET_VALUE_STUB(suffix, type)	\
+	type klee_get_value##suffix(type x) { \
+		return x; \
+	}
+
+KLEE_GET_VALUE_STUB(f, float)
+KLEE_GET_VALUE_STUB(d, double)
+KLEE_GET_VALUE_STUB(l, long)
+KLEE_GET_VALUE_STUB(ll, long long)
+KLEE_GET_VALUE_STUB(_i32, int32_t)
+KLEE_GET_VALUE_STUB(_i64, int64_t)
+
+#undef KLEE_GET_VALUE_STUB
 
 int klee_range(int begin, int end, const char* name) {
   int x;
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
index 347933df..181aedaa 100644
--- a/runtime/klee-libc/klee-choose.c
+++ b/runtime/klee-libc/klee-choose.c
@@ -9,8 +9,8 @@
 
 #include "klee/klee.h"
 
-unsigned klee_choose(unsigned n) {
-  unsigned x;
+uintptr_t klee_choose(uintptr_t n) {
+  uintptr_t x;
   klee_make_symbolic(&x, sizeof x, "klee_choose");
 
   // NB: this will *not* work if they don't compare to n values.