Mark all constant global memory objects as constant

Fixes #264.

We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory.
After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic).

2 files changed, 30 insertions, 1 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index bc889f25..4ac848b0 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -788,6 +788,9 @@ void Executor::initializeGlobals(ExecutionState &state) {
   }
 
   // once all objects are allocated, do the actual initialization
+  // remember constant objects to initialise their counter part for external
+  // calls
+  std::vector<ObjectState *> constantObjects;
   for (Module::const_global_iterator i = m->global_begin(),
          e = m->global_end();
        i != e; ++i) {
@@ -799,9 +802,20 @@ void Executor::initializeGlobals(ExecutionState &state) {
       ObjectState *wos = state.addressSpace.getWriteable(mo, os);
       
       initializeGlobalObject(state, wos, i->getInitializer(), 0);
-      // if(i->isConstant()) os->setReadOnly(true);
+      if (i->isConstant())
+        constantObjects.emplace_back(wos);
     }
   }
+
+  // initialise constant memory that is potentially used with external calls
+  if (!constantObjects.empty()) {
+    // initialise the actual memory with constant values
+    state.addressSpace.copyOutConcretes();
+
+    // mark constant objects as read-only
+    for (auto obj : constantObjects)
+      obj->setReadOnly(true);
+  }
 }
 
 void Executor::branch(ExecutionState &state, 
diff --git a/test/regression/2019-09-06-make-const-symbolic.c b/test/regression/2019-09-06-make-const-symbolic.c
new file mode 100644
index 00000000..52d430a5
--- /dev/null
+++ b/test/regression/2019-09-06-make-const-symbolic.c
@@ -0,0 +1,15 @@
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+#include "klee/klee.h"
+
+const int c = 23;
+int main(int argc, char **argv) {
+  klee_make_symbolic(&c, sizeof(c), "c");
+  // CHECK: cannot make readonly object symbolic
+
+  if (c > 20)
+    return 0;
+  else
+    return 1;
+}
\ No newline at end of file