Improve error messages for ReadStringAtAddress

2 files changed, 26 insertions, 7 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index e927adf0..22c27432 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -236,9 +236,19 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
                                             ref<Expr> addressExpr) {
   ObjectPair op;
   addressExpr = executor.toUnique(state, addressExpr);
+  if (!isa<ConstantExpr>(addressExpr)) {
+    executor.terminateStateOnError(
+        state, "Symbolic string pointer passed to one of the klee_ functions",
+        Executor::TerminateReason::User);
+    return "";
+  }
   ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
-  if (!state.addressSpace.resolveOne(address, op))
-    assert(0 && "XXX out of bounds / multiple resolution unhandled");
+  if (!state.addressSpace.resolveOne(address, op)) {
+    executor.terminateStateOnError(
+        state, "Invalid string pointer passed to one of the klee_ functions",
+        Executor::TerminateReason::User);
+    return "";
+  }
   bool res __attribute__ ((unused));
   assert(executor.solver->mustBeTrue(state, 
                                      EqExpr::create(address, 
diff --git a/test/Feature/MakeSymbolicAPI.c b/test/Feature/MakeSymbolicAPI.c
index 0ff4b82f..6868edc7 100644
--- a/test/Feature/MakeSymbolicAPI.c
+++ b/test/Feature/MakeSymbolicAPI.c
@@ -5,15 +5,24 @@
 // RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log
 
 int main() {
-  unsigned a, b, c;
+  unsigned a, b, c, d, e;
+  const char *invalid_pointer = 0xf;
 
   klee_make_symbolic(&a, sizeof(a), "");
-// CHECK-WRN: KLEE: WARNING: klee_make_symbolic: renamed empty name to "unnamed"
+  //CHECK-WRN: KLEE: WARNING: klee_make_symbolic: renamed empty name to "unnamed"
+
 
   klee_make_symbolic(&b, sizeof(b));
-// CHECK-WRN: KLEE: WARNING: klee_make_symbolic: deprecated number of arguments (2 instead of 3)
-// CHECK-WRN: KLEE: WARNING: klee_make_symbolic: renamed empty name to "unnamed"
+  //CHECK-WRN: KLEE: WARNING: klee_make_symbolic: deprecated number of arguments (2 instead of 3)
+  //CHECK-WRN: KLEE: WARNING: klee_make_symbolic: renamed empty name to "unnamed"
+
+  if(a == 2)
+    klee_make_symbolic(&d, sizeof(e), invalid_pointer);
+    //CHECK-ERR-DAG: KLEE: ERROR: {{.*}} Invalid string pointer passed to one of the klee_ functions
+  if(a == 3)
+    klee_make_symbolic(&d, sizeof(e), (char *) b);
+    //CHECK-ERR-DAG: KLEE: ERROR: {{.*}} Symbolic string pointer passed to one of the klee_ functions
 
   klee_make_symbolic(&c);
-// CHECK-ERR: KLEE: ERROR: {{.*}} illegal number of arguments to klee_make_symbolic(void*, size_t, char*)
+  //CHECK-ERR-DAG: KLEE: ERROR: {{.*}} illegal number of arguments to klee_make_symbolic(void*, size_t, char*)
 }