Remove model_version from the POSIX runtime, as we have never used it.

8 files changed, 9 insertions, 43 deletions

diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h
index 5fa42874..87d967ee 100644
--- a/runtime/POSIX/fd.h
+++ b/runtime/POSIX/fd.h
@@ -93,7 +93,6 @@ typedef struct {
 typedef struct {
   exe_file_t fds[MAX_FDS];
   mode_t umask; /* process umask */
-  unsigned version;
   /* If set, writes execute as expected.  Otherwise, writes extending
      the file size only change the contents up to the initial
      size. The file offset is always incremented correctly. */
diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c
index a8d557e7..a064e42b 100644
--- a/runtime/POSIX/fd_init.c
+++ b/runtime/POSIX/fd_init.c
@@ -36,7 +36,6 @@ exe_sym_env_t __exe_env = {
    { 1, eOpen | eWriteable, 0, 0}, 
    { 2, eOpen | eWriteable, 0, 0}},
   022,
-  0,
   0
 };
 
@@ -96,12 +95,6 @@ static void __create_new_dfile(exe_disk_file_t *dfile, unsigned size,
   dfile->stat = s;
 }
 
-static unsigned __sym_uint32(const char *name) {
-  unsigned x;
-  klee_make_symbolic(&x, sizeof x, name);
-  return x;
-}
-
 /* n_files: number of symbolic input files, excluding stdin
    file_length: size in bytes of each symbolic file, including stdin
    sym_stdout_flag: 1 if stdout should be symbolic, 0 otherwise
@@ -168,6 +161,4 @@ void klee_init_fds(unsigned n_files, unsigned file_length,
   else __exe_fs.sym_stdout = NULL;
   
   __exe_env.save_all_writes = save_all_writes_flag;
-  __exe_env.version = __sym_uint32("model_version");
-  klee_assume(__exe_env.version == 1);
 }
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
index 2442db0c..18eb3cff 100644
--- a/runtime/Runtest/intrinsics.c
+++ b/runtime/Runtest/intrinsics.c
@@ -109,13 +109,6 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) {
       break;
     } else {
       KTestObject *o = &testData->objects[testPosition];
-      if (strcmp("model_version", o->name) == 0 &&
-          strcmp("model_version", name) != 0) {
-        // Skip over this KTestObject because we've hit
-        // `model_version` which is from the POSIX runtime
-        // and the caller didn't ask for it.
-        continue;
-      }
       if (strcmp(name, o->name) != 0) {
         report_internal_error(
             "object name mismatch. Requesting \"%s\" but returning \"%s\"",
diff --git a/test/Replay/libkleeruntest/replay_posix_runtime.c b/test/Replay/libkleeruntest/replay_posix_runtime.c
index 57046257..39b8d18f 100644
--- a/test/Replay/libkleeruntest/replay_posix_runtime.c
+++ b/test/Replay/libkleeruntest/replay_posix_runtime.c
@@ -27,9 +27,8 @@ int main(int argc, char** argv) {
   return 0;
 }
 
-// CHECKMODEL: num objects: 2
-// CHECKMODEL: object 0: name: {{b*}}'model_version'
-// CHECKMODEL: object 1: name: {{b*}}'x'
+// CHECKMODEL: num objects: 1
+// CHECKMODEL: object 0: name: {{b*}}'x'
 
 // TESTONE: x is not 0
 // TESTTWO: x is 0
diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c
index a1685a02..5e848964 100644
--- a/tools/klee-replay/file-creator.c
+++ b/tools/klee-replay/file-creator.c
@@ -301,7 +301,7 @@ static int create_reg_file(const char *fname, exe_disk_file_t *dfile,
   fprintf(stderr, "KLEE-REPLAY: NOTE: Creating file %s of length %d\n", fname, flen);
 
   // Open in RDWR just in case we have to end up using this fd.
-  if (__exe_env.version == 0 && mode == 0)
+  if (mode == 0)
     mode = 0644;
 
   int fd = open(fname, O_CREAT | O_RDWR, mode);
diff --git a/tools/klee-replay/klee-replay.c b/tools/klee-replay/klee-replay.c
index 72eeb17e..82c638c2 100644
--- a/tools/klee-replay/klee-replay.c
+++ b/tools/klee-replay/klee-replay.c
@@ -466,30 +466,17 @@ void klee_posix_prefer_cex(void *buffer, uintptr_t condition) {
 }
 
 void klee_make_symbolic(void *addr, size_t nbytes, const char *name) {
-  /* XXX remove model version code once new tests gen'd */
   if (obj_index >= input->numObjects) {
-    if (strcmp("model_version", name) == 0) {
-      assert(nbytes == 4);
-      *((int*) addr) = 0;
-    } else {
       __emit_error("ran out of appropriate inputs");
-    }
   } else {
     KTestObject *boo = &input->objects[obj_index];
-
-    if (strcmp("model_version", name) == 0 &&
-        strcmp("model_version", boo->name) != 0) {
-      assert(nbytes == 4);
-      *((int*) addr) = 0;
+    if (boo->numBytes != nbytes) {
+      fprintf(stderr, "KLEE-REPLAY: ERROR: make_symbolic mismatch, different sizes: "
+              "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes);
+      exit(1);
     } else {
-      if (boo->numBytes != nbytes) {
-        fprintf(stderr, "KLEE-REPLAY: ERROR: make_symbolic mismatch, different sizes: "
-           "%d in input file, %lu in code\n", boo->numBytes, (unsigned long)nbytes);
-        exit(1);
-      } else {
-        memcpy(addr, boo->bytes, nbytes);
-        obj_index++;
-      }
+      memcpy(addr, boo->bytes, nbytes);
+      obj_index++;
     }
   }
 }
diff --git a/tools/ktest-gen/ktest-gen.cpp b/tools/ktest-gen/ktest-gen.cpp
index 331ff7b1..d127c0e5 100644
--- a/tools/ktest-gen/ktest-gen.cpp
+++ b/tools/ktest-gen/ktest-gen.cpp
@@ -303,8 +303,6 @@ int main(int argc, char *argv[]) {
   b.numArgs = argv_copy_idx;
   b.args = argv_copy;
 
-  push_range(&b, "model_version", 1);
-
   if (!kTest_toFile(&b, bout_file ? bout_file : "file.bout"))
     assert(0);
 
diff --git a/tools/ktest-randgen/ktest-randgen.cpp b/tools/ktest-randgen/ktest-randgen.cpp
index 9b7260eb..6146d35d 100644
--- a/tools/ktest-randgen/ktest-randgen.cpp
+++ b/tools/ktest-randgen/ktest-randgen.cpp
@@ -281,7 +281,6 @@ int main(int argc, char *argv[]) {
     push_random_obj(&b, "stdout", 1024, 1024);
     push_obj(&b, "stdout-stat", sizeof(struct stat), (unsigned char *)&s);
   }
-  push_range(&b, "model_version", 1);
 
   if (!kTest_toFile(&b, bout_file ? bout_file : "random.bout")) {
     error_exit("Error in storing data into random.bout\n");