about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/klee.h30
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp7
-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
-rw-r--r--test/Feature/GetValue.c6
-rw-r--r--tools/klee-replay/klee-replay.c11
8 files changed, 62 insertions, 32 deletions
diff --git a/include/klee/klee.h b/include/klee/klee.h
index aa47ce22..ce92ba37 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -10,6 +10,9 @@
 #ifndef __KLEE_H__
 #define __KLEE_H__
 
+#include "stdint.h"
+#include "stddef.h"
+
 #ifdef __cplusplus
 extern "C" {
 #endif
@@ -19,7 +22,7 @@ extern "C" {
      objects do not overlap. These memory objects will also
      (obviously) not correctly interact with external function
      calls. */
-  void klee_define_fixed_object(void *addr, unsigned nbytes);
+  void klee_define_fixed_object(void *addr, size_t nbytes);
 
   /// klee_make_symbolic - Make the contents of the object pointer to by \arg
   /// addr symbolic. 
@@ -29,7 +32,7 @@ extern "C" {
   /// be the entire contents of the object.
   /// \arg name - An optional name, used for identifying the object in messages,
   /// output files, etc.
-  void klee_make_symbolic(void *addr, unsigned nbytes, const char *name);
+  void klee_make_symbolic(void *addr, size_t nbytes, const char *name);
 
   /// klee_range - Construct a symbolic value in the signed interval
   /// [begin,end).
@@ -67,7 +70,7 @@ extern "C" {
 			 const char *suffix);
   
   /* called by checking code to get size of memory. */
-  unsigned klee_get_obj_size(void *ptr);
+  size_t klee_get_obj_size(void *ptr);
   
   /* print the tree associated w/ a given expression. */
   void klee_print_expr(const char *msg, ...);
@@ -75,7 +78,7 @@ extern "C" {
   /* NB: this *does not* fork n times and return [0,n) in children.
    * It makes n be symbolic and returns: caller must compare N times.
    */
-  unsigned klee_choose(unsigned n);
+  uintptr_t klee_choose(uintptr_t n);
   
   /* special klee assert macro. this assert should be used when path consistency
    * across platforms is desired (e.g., in tests).
@@ -91,21 +94,30 @@ extern "C" {
    * and writing tests but can also be used to enable prints in replay
    * mode.
    */
-  unsigned klee_is_symbolic(unsigned n);
+  unsigned klee_is_symbolic(uintptr_t n);
 
 
   /* The following intrinsics are primarily intended for internal use
      and may have peculiar semantics. */
 
-  void klee_assume(unsigned condition);
+  void klee_assume(uintptr_t condition);
   void klee_warning(const char *message);
   void klee_warning_once(const char *message);
-  void klee_prefer_cex(void *object, unsigned condition);
+  void klee_prefer_cex(void *object, uintptr_t condition);
   void klee_mark_global(void *object);
 
   /* Return a possible constant value for the input expression. This
      allows programs to forcibly concretize values on their own. */
-  unsigned klee_get_value(unsigned expr);
+#define KLEE_GET_VALUE_PROTO(suffix, type)	type klee_get_value##suffix(type expr)
+
+  KLEE_GET_VALUE_PROTO(f, float);
+  KLEE_GET_VALUE_PROTO(d, double);
+  KLEE_GET_VALUE_PROTO(l, long);
+  KLEE_GET_VALUE_PROTO(ll, long long);
+  KLEE_GET_VALUE_PROTO(_i32, int32_t);
+  KLEE_GET_VALUE_PROTO(_i64, int64_t);
+
+#undef KLEE_GET_VALUE_PROTO
 
   /* Ensure that memory in the range [address, address+size) is
      accessible to the program. If some byte in the range is not
@@ -114,7 +126,7 @@ extern "C" {
   
      The current implementation requires both address and size to be
      constants and that the range lie within a single object. */
-  void klee_check_memory_access(const void *address, unsigned size);
+  void klee_check_memory_access(const void *address, size_t size);
 
   /* Enable/disable forking. */
   void klee_set_forking(unsigned enable);
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index d3a86aac..2ef80acc 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -68,7 +68,12 @@ HandlerInfo handlerInfo[] = {
   add("free", handleFree, false),
   add("klee_assume", handleAssume, false),
   add("klee_check_memory_access", handleCheckMemoryAccess, false),
-  add("klee_get_value", handleGetValue, true),
+  add("klee_get_valuef", handleGetValue, true),
+  add("klee_get_valued", handleGetValue, true),
+  add("klee_get_valuel", handleGetValue, true),
+  add("klee_get_valuell", handleGetValue, true),
+  add("klee_get_value_i32", handleGetValue, true),
+  add("klee_get_value_i64", handleGetValue, true),
   add("klee_define_fixed_object", handleDefineFixedObject, false),
   add("klee_get_obj_size", handleGetObjSize, true),
   add("klee_get_errno", handleGetErrno, true),
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.
diff --git a/test/Feature/GetValue.c b/test/Feature/GetValue.c
index 391b68e3..dfd40d69 100644
--- a/test/Feature/GetValue.c
+++ b/test/Feature/GetValue.c
@@ -9,9 +9,9 @@ int main() {
   klee_assume(x > 10);
   klee_assume(x < 20);
 
-  assert(!klee_is_symbolic(klee_get_value(x)));
-  assert(klee_get_value(x) > 10);
-  assert(klee_get_value(x) < 20);
+  assert(!klee_is_symbolic(klee_get_value_i32(x)));
+  assert(klee_get_value_i32(x) > 10);
+  assert(klee_get_value_i32(x) < 20);
 
   return 0;
 }
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 1cbbf6d8..7c605a53 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -15,6 +15,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
+#include <stdint.h>
 
 #include <errno.h>
 #include <time.h>
@@ -327,22 +328,22 @@ void klee_warning_once(char *name) {
   fprintf(stderr, "WARNING: %s\n", name);
 }
 
-int klee_assume(int x) {
+unsigned klee_assume(uintptr_t x) {
   if (!x) {
     fprintf(stderr, "WARNING: klee_assume(0)!\n");
   }
   return 0;
 }
 
-int klee_is_symbolic(int x) {
+unsigned klee_is_symbolic(uintptr_t x) {
   return 0;
 }
 
-void klee_prefer_cex(void *buffer, unsigned condition) {
+void klee_prefer_cex(void *buffer, uintptr_t condition) {
   ;
 }
 
-void klee_make_symbolic(void *addr, unsigned nbytes, const char *name) {
+void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
   /* XXX remove model version code once new tests gen'd */
   if (obj_index >= input->numObjects) {
     if (strcmp("model_version", name) == 0) {
@@ -361,7 +362,7 @@ void klee_make_symbolic(void *addr, unsigned nbytes, const char *name) {
     } else {
       if (boo->numBytes != nbytes) {
 	fprintf(stderr, "make_symbolic mismatch, different sizes: "
-		"%d in input file, %d in code\n", boo->numBytes, nbytes);
+		"%d in input file, %ld in code\n", boo->numBytes, nbytes);
 	exit(1);
       } else {
         memcpy(addr, boo->bytes, nbytes);
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 06:02:56 +0000