From 0dee67bf09a16c51f951bb6d659eb0baaae94126 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Thu, 5 Sep 2019 17:01:47 +0100
Subject: 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.
---
 runtime/POSIX/fd.c | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'runtime')

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;
     }
   }
-- 
cgit 1.4.1