about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-09-05 17:01:47 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2019-11-05 14:51:18 +0000
commit0dee67bf09a16c51f951bb6d659eb0baaae94126 (patch)
treebed4c55d7a6fe789843810d2cdbc7eacdcd3f56b
parent7fa96f70cf52b0f3112046962487e95eab0d88fe (diff)
downloadklee-0dee67bf09a16c51f951bb6d659eb0baaae94126.tar.gz
Do not modify strings if they are read-only.
Hoist increment of `sc` into the loop header.

Memory locations can only be written to if they are writeable.
Avoid concretising a value by writing it. If the location is not symbolic in the first place.
This avoids writing read-only memory locations.
-rw-r--r--runtime/POSIX/fd.c14
1 files changed, 10 insertions, 4 deletions
diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index a2cbe0ab..ae08183f 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -1352,19 +1352,25 @@ static const char *__concretize_string(const char *s) {
   char *sc = __concretize_ptr(s);
   unsigned i;
 
-  for (i=0; ; ++i) {
+  for (i = 0;; ++i, ++sc) {
     char c = *sc;
+    // Avoid writing read-only memory locations
+    if (!klee_is_symbolic(c)) {
+      if (!c)
+        break;
+      continue;
+    }
     if (!(i&(i-1))) {
       if (!c) {
-        *sc++ = 0;
+        *sc = 0;
         break;
       } else if (c=='/') {
-        *sc++ = '/';
+        *sc = '/';
       } 
     } else {
       char cc = (char) klee_get_valuel((long)c);
       klee_assume(cc == c);
-      *sc++ = cc;
+      *sc = cc;
       if (!cc) break;
     }
   }