Removed --zero-seed-extension, and merge it with --allow-seed-extension. This reworked logic also fixes a buffer overflow which could be triggered during seed extension.

3 files changed, 10 insertions, 21 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 89072490..c07fa18e 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -259,18 +259,10 @@ cl::opt<bool> OnlySeed("only-seed",
                                 "doing regular search (default=false)."),
                        cl::cat(SeedingCat));
 
-cl::opt<bool>
-    AllowSeedExtension("allow-seed-extension",
-                       cl::init(false),
-                       cl::desc("Allow extra (unbound) values to become "
-                                "symbolic during seeding (default=false)."),
-                       cl::cat(SeedingCat));
-
-cl::opt<bool> ZeroSeedExtension(
-    "zero-seed-extension",
-    cl::init(false),
-    cl::desc(
-        "Use zero-filled objects if matching seed not found (default=false)"),
+cl::opt<bool> AllowSeedExtension(
+    "allow-seed-extension", cl::init(false),
+    cl::desc("Allow extra values to become symbolic during seeding; "
+             "the seed is extended with zeros (default=false)."),
     cl::cat(SeedingCat));
 
 cl::opt<bool> AllowSeedTruncation(
@@ -4576,17 +4568,17 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
         KTestObject *obj = si.getNextInput(mo, NamedSeedMatching);
 
         if (!obj) {
-          if (ZeroSeedExtension) {
+          if (AllowSeedExtension) {
             std::vector<unsigned char> &values = si.assignment.bindings[array];
             values = std::vector<unsigned char>(mo->size, '\0');
-          } else if (!AllowSeedExtension) {
+          } else /*if (!AllowSeedExtension)*/ {
             terminateStateOnUserError(state,
                                       "ran out of inputs during seeding");
             break;
           }
         } else {
           /* The condition below implies obj->numBytes != mo->size */
-          if ((obj->numBytes < mo->size && !(AllowSeedExtension || ZeroSeedExtension)) ||
+          if ((obj->numBytes < mo->size && !AllowSeedExtension) ||
               (obj->numBytes > mo->size && !AllowSeedTruncation)) {
             std::stringstream msg;
 	    msg << "replace size mismatch: "
@@ -4600,11 +4592,8 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
             std::vector<unsigned char> &values = si.assignment.bindings[array];
             values.insert(values.begin(), obj->bytes,
                           obj->bytes + std::min(obj->numBytes, mo->size));
-
-            if (ZeroSeedExtension) {
-              for (unsigned i=obj->numBytes; i<mo->size; ++i)
+              for (unsigned i = obj->numBytes; i < mo->size; ++i)
                 values.push_back('\0');
-            }
           }
         }
       }
diff --git a/test/Feature/SeedConcretizePatchedFP.c b/test/Feature/SeedConcretizeExtendFP.c
index b8b758b5..6a8de589 100644
--- a/test/Feature/SeedConcretizePatchedFP.c
+++ b/test/Feature/SeedConcretizeExtendFP.c
@@ -7,7 +7,7 @@
 // RUN: not test -f %t.klee-out/test000002.ktest
 
 // RUN: rm -rf %t.klee-out-2
-// RUN: %klee --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest --allow-seed-extension --zero-seed-extension %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --exit-on-error --output-dir=%t.klee-out-2 --seed-file %t.klee-out/test000001.ktest --allow-seed-extension %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 
diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c
index c9ef0168..b39a8bd5 100644
--- a/test/Runtime/POSIX/SeedAndFail.c
+++ b/test/Runtime/POSIX/SeedAndFail.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 1 10  2>%t.log
 // RUN: rm -rf %t.klee-out-2
-// RUN: %klee --output-dir=%t.klee-out-2 --seed-dir=%t.klee-out --zero-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
+// RUN: %klee --output-dir=%t.klee-out-2 --seed-dir=%t.klee-out --allow-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1
 // RUN: ls %t.klee-out-2 | grep -c assert | grep 4
 
 #include <string.h>