about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/regexp/Regexp.c2
-rw-r--r--examples/sort/sort.c2
-rw-r--r--include/klee/klee.h46
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp17
-rw-r--r--runtime/Intrinsic/klee_int.c2
-rw-r--r--runtime/Intrinsic/klee_make_symbolic.c14
-rw-r--r--runtime/Intrinsic/klee_range.c5
-rw-r--r--runtime/POSIX/fd_init.c16
-rw-r--r--runtime/POSIX/klee_init_env.c2
-rw-r--r--runtime/POSIX/misc.c2
-rw-r--r--runtime/Runtest/intrinsics.c12
-rw-r--r--runtime/klee-libc/klee-choose.c2
-rw-r--r--test/Coverage/ReplayOutDir.c2
-rw-r--r--test/Feature/AliasFunction.c2
-rw-r--r--test/Feature/AliasFunctionExit.c2
-rw-r--r--test/Feature/MakeSymbolicName.c2
-rw-r--r--test/Feature/NamedSeedMatching.c16
-rw-r--r--test/Feature/const_array_opt1.c2
-rw-r--r--test/Makefile4
-rw-r--r--test/regression/2007-10-12-failed-make-symbolic-after-copy.c4
-rw-r--r--test/regression/2008-04-10-bad-alloca-free.c2
-rw-r--r--tools/klee/main.cpp2
-rw-r--r--www/code-examples/demo.c2
23 files changed, 84 insertions, 78 deletions
diff --git a/examples/regexp/Regexp.c b/examples/regexp/Regexp.c
index f3e751f9..a48ea928 100644
--- a/examples/regexp/Regexp.c
+++ b/examples/regexp/Regexp.c
@@ -53,7 +53,7 @@ int main() {
   char re[SIZE];
   
   // Make the input symbolic. 
-  klee_make_symbolic_name(re, sizeof re, "re");
+  klee_make_symbolic(re, sizeof re, "re");
 
   // Try to match against a constant string "hello".
   match(re, "hello");
diff --git a/examples/sort/sort.c b/examples/sort/sort.c
index a1629c6b..62e4124e 100644
--- a/examples/sort/sort.c
+++ b/examples/sort/sort.c
@@ -71,7 +71,7 @@ void test(int *array, unsigned nelem) {
 int main() {
   int input[4] = { 4, 3, 2, 1};
 
-  klee_make_symbolic(&input, sizeof(input));
+  klee_make_symbolic(&input, sizeof(input), "input");
   test(input, 4);
 
   return 0;
diff --git a/include/klee/klee.h b/include/klee/klee.h
index 698a61c4..3d2d1782 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -21,31 +21,45 @@ extern "C" {
      calls. */
   void klee_define_fixed_object(void *addr, unsigned nbytes);
 
-  /* make the contents of the object pointed to by addr symbolic. addr
-   * should always be the start of the object and nbytes must be its
-   * entire size. name is an optional name (can be the empty string)
-   */
-  void klee_make_symbolic_name(void *addr, unsigned nbytes, 
-			       const char *name);
-
-  void klee_make_symbolic(void *addr, unsigned nbytes);  
-  
-  /* Return symbolic value in the (signed) interval [begin,end) */
+  /// klee_make_symbolic - Make the contents of the object pointer to by \arg
+  /// addr symbolic. 
+  ///
+  /// \arg addr - The start of the object.
+  /// \arg nbytes - The number of bytes to make symbolic; currently this *must*
+  /// 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);
+
+  /// klee_range - Construct a symbolic value in the signed interval
+  /// [begin,end).
+  ///
+  /// \arg name - An optional name, used for identifying the object in messages,
+  /// output files, etc.
   int klee_range(int begin, int end, const char *name);
 
-  /* Return a symbolic integer */
+  /// klee_int - Construct an unconstrained symbolic integer.
+  ///
+  /// \arg name - An optional name, used for identifying the object in messages,
+  /// output files, etc.
   int klee_int(const char *name);
 
-  void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment);
-
-  /* terminate the state without generating a test file */
+  /// klee_silent_exit - Terminate the current KLEE process without generating a
+  /// test file.
   __attribute__((noreturn))
   void klee_silent_exit(int status);
-  
+
+  /// klee_abort - Abort the current KLEE process.
   __attribute__((noreturn))
   void klee_abort(void);  
 
-  /** Report an error and terminate the state. */
+  /// klee_report_error - Report a user defined error and terminate the current
+  /// KLEE process.
+  ///
+  /// \arg file - The filename to report in the error message.
+  /// \arg line - The line number to report in the error message.
+  /// \arg message - A string to include in the error message.
+  /// \arg suffix - The suffix to use for error files.
   __attribute__((noreturn))
   void klee_report_error(const char *file, 
 			 int line, 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index da2a4a49..2e423785 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -72,7 +72,7 @@ HandlerInfo handlerInfo[] = {
   add("klee_get_obj_size", handleGetObjSize, true),
   add("klee_get_errno", handleGetErrno, true),
   add("klee_is_symbolic", handleIsSymbolic, true),
-  add("klee_make_symbolic_name", handleMakeSymbolic, false),
+  add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
   add("klee_malloc_n", handleMallocN, true),
   add("klee_merge", handleMerge, false),
@@ -670,8 +670,18 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
 void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
                                                 KInstruction *target,
                                                 std::vector<ref<Expr> > &arguments) {
-  assert(arguments.size()==3 &&
-         "invalid number of arguments to klee_make_symbolic[_name]");  
+  std::string name;
+
+  // FIXME: For backwards compatibility, we should eventually enforce the
+  // correct arguments.
+  if (arguments.size() == 2) {
+    name = "unnamed";
+  } else {
+    // FIXME: Should be a user.err, not an assert.
+    assert(arguments.size()==3 &&
+           "invalid number of arguments to klee_make_symbolic");  
+    name = readStringAtAddress(state, arguments[2]);
+  }
 
   Executor::ExactResolutionList rl;
   executor.resolveExact(state, arguments[0], rl, "make_symbolic");
@@ -679,7 +689,6 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
   for (Executor::ExactResolutionList::iterator it = rl.begin(), 
          ie = rl.end(); it != ie; ++it) {
     MemoryObject *mo = (MemoryObject*) it->first.first;
-    std::string name = readStringAtAddress(state, arguments[2]);
     mo->setName(name);
     
     const ObjectState *old = it->first.second;
diff --git a/runtime/Intrinsic/klee_int.c b/runtime/Intrinsic/klee_int.c
index 88ec5026..56f0f9dc 100644
--- a/runtime/Intrinsic/klee_int.c
+++ b/runtime/Intrinsic/klee_int.c
@@ -12,6 +12,6 @@
 
 int klee_int(const char *name) {
   int x;
-  klee_make_symbolic_name(&x, sizeof x, name);
+  klee_make_symbolic(&x, sizeof x, name);
   return x;
 }
diff --git a/runtime/Intrinsic/klee_make_symbolic.c b/runtime/Intrinsic/klee_make_symbolic.c
deleted file mode 100644
index b9dec2a7..00000000
--- a/runtime/Intrinsic/klee_make_symbolic.c
+++ /dev/null
@@ -1,14 +0,0 @@
-//===-- klee_make_symbolic.c ----------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include <klee/klee.h>
-
-void klee_make_symbolic(void *addr, unsigned nbytes) {
-  klee_make_symbolic_name(addr, nbytes, "unnamed");
-}
diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c
index 59d1a05e..5da6a7a5 100644
--- a/runtime/Intrinsic/klee_range.c
+++ b/runtime/Intrinsic/klee_range.c
@@ -13,12 +13,13 @@
 int klee_range(int start, int end, const char* name) {
   int x;
 
-  assert(start < end);
+  if (start >= end)
+    klee_report_error(__FILE__, __LINE__, "invalid range", "user");
 
   if (start+1==end) {
     return start;
   } else {
-    klee_make_symbolic_name(&x, sizeof x, name); 
+    klee_make_symbolic(&x, sizeof x, name); 
 
     /* Make nicer constraint when simple... */
     if (start==0) {
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index 61e49893..d976b0b4 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -56,9 +56,9 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
 
   dfile->size = size;
   dfile->contents = malloc(dfile->size);
-  klee_make_symbolic_name(dfile->contents, dfile->size, name);
+  klee_make_symbolic(dfile->contents, dfile->size, name);
   
-  klee_make_symbolic_name(s, sizeof(*s), sname);
+  klee_make_symbolic(s, sizeof(*s), sname);
 
   /* For broken tests */
   if (!klee_is_symbolic(s->st_ino) && 
@@ -96,7 +96,7 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
 
 static unsigned __sym_uint32(const char *name) {
   unsigned x;
-  klee_make_symbolic_name(&x, sizeof x, name);
+  klee_make_symbolic(&x, sizeof x, name);
   return x;
 }
 
@@ -139,11 +139,11 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
     __exe_fs.ftruncate_fail = malloc(sizeof(*__exe_fs.ftruncate_fail));
     __exe_fs.getcwd_fail = malloc(sizeof(*__exe_fs.getcwd_fail));
 
-    klee_make_symbolic_name(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
-    klee_make_symbolic_name(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
-    klee_make_symbolic_name(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
-    klee_make_symbolic_name(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
-    klee_make_symbolic_name(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
+    klee_make_symbolic(__exe_fs.read_fail, sizeof(*__exe_fs.read_fail), "read_fail");
+    klee_make_symbolic(__exe_fs.write_fail, sizeof(*__exe_fs.write_fail), "write_fail");
+    klee_make_symbolic(__exe_fs.close_fail, sizeof(*__exe_fs.close_fail), "close_fail");
+    klee_make_symbolic(__exe_fs.ftruncate_fail, sizeof(*__exe_fs.ftruncate_fail), "ftruncate_fail");
+    klee_make_symbolic(__exe_fs.getcwd_fail, sizeof(*__exe_fs.getcwd_fail), "getcwd_fail");
   }
 
   /* setting symbolic stdout */
diff --git a/runtime/POSIX/klee_init_env.c b/runtime/POSIX/klee_init_env.c
index 83e9fde6..f5609973 100644
--- a/runtime/POSIX/klee_init_env.c
+++ b/runtime/POSIX/klee_init_env.c
@@ -62,7 +62,7 @@ static char *__get_sym_str(int numChars, char *name) {
   int i;
   char *s = malloc(numChars+1);
   klee_mark_global(s);
-  klee_make_symbolic_name(s, numChars+1, name);
+  klee_make_symbolic(s, numChars+1, name);
 
   for (i=0; i<numChars; i++)
     klee_prefer_cex(s, __isprint(s[i]));
diff --git a/runtime/POSIX/misc.c b/runtime/POSIX/misc.c
index 12ff2f58..d0e88290 100644
--- a/runtime/POSIX/misc.c
+++ b/runtime/POSIX/misc.c
@@ -69,7 +69,7 @@ char *getenv(const char *name) {
       if (__klee_sym_env_count < __klee_sym_env_nvars) {
         if (klee_range(0, 2, name)) {
           char *s = malloc(__klee_sym_env_var_size+1);
-          klee_make_symbolic(s, __klee_sym_env_var_size+1);
+          klee_make_symbolic(s, __klee_sym_env_var_size+1. "env");
           s[__klee_sym_env_var_size] = '\0';
           
           memcpy(__klee_sym_env[__klee_sym_env_count].name, name, len+1);
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 1a2fd030..36efb5c2 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_name(void *array, unsigned nbytes, const char *name) {
+void klee_make_symbolic(void *array, unsigned nbytes, const char *name) {
   static int rand_init = -1;
 
   if (rand_init == -1) {
@@ -94,10 +94,6 @@ void klee_make_symbolic_name(void *array, unsigned nbytes, const char *name) {
   }
 }
 
-void klee_make_symbolic(void *array, unsigned nbytes) {
-  klee_make_symbolic_name(array, nbytes, "unnamed");
-}
-
 void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment) {
 #if 1
   return mmap((void*) 0x90000000, nelems*size, PROT_READ|PROT_WRITE, 
@@ -119,7 +115,7 @@ void klee_silent_exit(int x) {
 
 unsigned klee_choose(unsigned n) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "klee_choose");
   if(x >= n)
     fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x);
   assert(x < n);
@@ -136,9 +132,9 @@ unsigned klee_get_value(unsigned x) {
   return x;
 }
 
-int klee_range_name(int begin, int end, const char* name) {
+int klee_range(int begin, int end, const char* name) {
   int x;
-  klee_make_symbolic_name(&x, sizeof x, name);
+  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", 
diff --git a/runtime/klee-libc/klee-choose.c b/runtime/klee-libc/klee-choose.c
index 106b4f89..347933df 100644
--- a/runtime/klee-libc/klee-choose.c
+++ b/runtime/klee-libc/klee-choose.c
@@ -11,7 +11,7 @@
 
 unsigned klee_choose(unsigned n) {
   unsigned x;
-  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&x, sizeof x, "klee_choose");
 
   // NB: this will *not* work if they don't compare to n values.
   if(x >= n)
diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c
index 3ca6fb80..ca7e590a 100644
--- a/test/Coverage/ReplayOutDir.c
+++ b/test/Coverage/ReplayOutDir.c
@@ -5,7 +5,7 @@
 
 int main() {
   int i;
-  klee_make_symbolic(&i, sizeof i);
+  klee_make_symbolic(&i, sizeof i, "i");
   klee_print_range("i", i);
   return 0;
 }
diff --git a/test/Feature/AliasFunction.c b/test/Feature/AliasFunction.c
index e7acfc19..16d89ef6 100644
--- a/test/Feature/AliasFunction.c
+++ b/test/Feature/AliasFunction.c
@@ -11,7 +11,7 @@ void bar() { printf("  bar()\n"); }
 
 int main() {
   int x;
-  klee_make_symbolic_name(&x, sizeof(x), "x");
+  klee_make_symbolic(&x, sizeof(x), "x");
 
   // no aliases
   foo();
diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c
index fcaf7e6c..4bda950a 100644
--- a/test/Feature/AliasFunctionExit.c
+++ b/test/Feature/AliasFunctionExit.c
@@ -22,7 +22,7 @@ void end(int status) {
 
 int main() {
   int x;
-  klee_make_symbolic_name(&x, sizeof(x), "x");
+  klee_make_symbolic(&x, sizeof(x), "x");
 
   klee_alias_function("exit", "end");
   start(x);
diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c
index c1f11424..a4d4e2a6 100644
--- a/test/Feature/MakeSymbolicName.c
+++ b/test/Feature/MakeSymbolicName.c
@@ -7,7 +7,7 @@ int main() {
   int a[4] = {1, 2, 3, 4};
   unsigned i;
 
-  klee_make_symbolic_name(&i, sizeof(i), "index");  
+  klee_make_symbolic(&i, sizeof(i), "index");  
   if (i > 3)
     klee_silent_exit(0);
 
diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c
index 6d52e7a4..cff34282 100644
--- a/test/Feature/NamedSeedMatching.c
+++ b/test/Feature/NamedSeedMatching.c
@@ -16,20 +16,20 @@ int main(int argc, char **argv) {
   int a, b, c, x;
 
   if (argc==2 && strcmp(argv[1], "initial") == 0) {
-    klee_make_symbolic_name(&a, sizeof a, "a");
-    klee_make_symbolic_name(&b, sizeof b, "b");
-    klee_make_symbolic_name(&c, sizeof c, "c");
-    klee_make_symbolic_name(&x, sizeof x, "a");
+    klee_make_symbolic(&a, sizeof a, "a");
+    klee_make_symbolic(&b, sizeof b, "b");
+    klee_make_symbolic(&c, sizeof c, "c");
+    klee_make_symbolic(&x, sizeof x, "a");
 
     klee_assume(a == 3);
     klee_assume(b == 4);
     klee_assume(c == 5);
     klee_assume(x == 6);
   } else {
-    klee_make_symbolic_name(&a, sizeof a, "a");
-    klee_make_symbolic_name(&c, sizeof c, "c");
-    klee_make_symbolic_name(&b, sizeof b, "b");
-    klee_make_symbolic_name(&x, sizeof x, "a");
+    klee_make_symbolic(&a, sizeof a, "a");
+    klee_make_symbolic(&c, sizeof c, "c");
+    klee_make_symbolic(&b, sizeof b, "b");
+    klee_make_symbolic(&x, sizeof x, "a");
   }
 
   if (a==3) printf("a==3\n");
diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c
index 96c46fb9..09ed07fd 100644
--- a/test/Feature/const_array_opt1.c
+++ b/test/Feature/const_array_opt1.c
@@ -20,7 +20,7 @@ int main() {
   for (i=0; i<N; i++)
     a[i] = i % 256;
   
-  klee_make_symbolic_name(k, sizeof(k), "k");
+  klee_make_symbolic(k, sizeof(k), "k");
   
   for (i=0; i<N_IDX; i++) {
     if (k[i] >= N)
diff --git a/test/Makefile b/test/Makefile
index 0c42a6f6..8cd8688a 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -89,8 +89,8 @@ site.exp: Makefile $(LEVEL)/Makefile.config
 	@echo 'set compile_c "$(CC) $(CPP.Flags) $(C.Flags) $(CompileCommonOpts) -c "' >>site.tmp
 	@echo 'set compile_cxx "$(CXX) $(CPP.Flags) $(CXX.Flags) $(CompileCommonOpts) - c"' >> site.tmp
 	@echo 'set link "$(CXX) $(CPP.Flags) $(CXX.Flags) $(CompileCommonOpts) $(LD.Flags)"' >>site.tmp
-	@echo 'set llvmgcc "$(LLVMGCC)"' >> site.tmp
-	@echo 'set llvmgxx "$(LLVMGCC)"' >> site.tmp
+	@echo 'set llvmgcc "$(LLVMGCC) -m32"' >> site.tmp
+	@echo 'set llvmgxx "$(LLVMGCC) -m32"' >> site.tmp
 	@echo 'set llvmgccmajvers "$(LLVMGCC_MAJVERS)"' >> site.tmp
 	@echo 'set shlibext "$(SHLIBEXT)"' >> site.tmp
 	@echo '## All variables above are generated by configure. Do Not Edit ## ' >>site.tmp
diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
index 144281fa..9d81fad0 100644
--- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
+++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c
@@ -5,13 +5,13 @@
 int main() {
   unsigned x, y[4];
 
-  klee_make_symbolic(&x,sizeof x);
+  klee_make_symbolic(&x, sizeof x, "x");
   if (x>=4) klee_silent_exit(0);
   
   y[x] = 0;
 
   if (x) { // force branch so y is copied
-    klee_make_symbolic(&y, sizeof y);
+    klee_make_symbolic(&y, sizeof y, "y");
     if (y[x]==0) klee_silent_exit(0);
     return 0; // should be reachable
   } else {
diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c
index 46e2b0cf..a6215f64 100644
--- a/test/regression/2008-04-10-bad-alloca-free.c
+++ b/test/regression/2008-04-10-bad-alloca-free.c
@@ -2,7 +2,7 @@
 // RUN: %klee --exit-on-error %t1.bc
 
 void f(int *addr) {
-  klee_make_symbolic_name(addr, sizeof *addr, "moo");
+  klee_make_symbolic(addr, sizeof *addr, "moo");
 }
 
 int main() {
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 39b208ec..0a070452 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -661,7 +661,7 @@ static const char *modelledExternals[] = {
   "klee_get_value",
   "klee_get_obj_size", 
   "klee_is_symbolic", 
-  "klee_make_symbolic_name", 
+  "klee_make_symbolic", 
   "klee_mark_global", 
   "klee_malloc_n", 
   "klee_merge", 
diff --git a/www/code-examples/demo.c b/www/code-examples/demo.c
index 69e0715a..2bf1c00d 100644
--- a/www/code-examples/demo.c
+++ b/www/code-examples/demo.c
@@ -6,6 +6,6 @@ int my_islower(int x) {
 
 int main() {
   char c;
-  klee_make_symbolic_name(&c, sizeof(c), "input");
+  klee_make_symbolic(&c, sizeof(c), "input");
   return my_islower(c);
 }
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-06-03 00:25:17 +0000