From 513de049a419f550198da0d96e9442579c09239c Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 8 Nov 2023 18:18:47 +0000 Subject: 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. --- lib/Core/Executor.cpp | 27 ++++++++------------------- test/Feature/SeedConcretizeExtendFP.c | 33 +++++++++++++++++++++++++++++++++ test/Feature/SeedConcretizePatchedFP.c | 33 --------------------------------- test/Runtime/POSIX/SeedAndFail.c | 2 +- 4 files changed, 42 insertions(+), 53 deletions(-) create mode 100644 test/Feature/SeedConcretizeExtendFP.c delete mode 100644 test/Feature/SeedConcretizePatchedFP.c 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 OnlySeed("only-seed", "doing regular search (default=false)."), cl::cat(SeedingCat)); -cl::opt - 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 ZeroSeedExtension( - "zero-seed-extension", - cl::init(false), - cl::desc( - "Use zero-filled objects if matching seed not found (default=false)"), +cl::opt 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 AllowSeedTruncation( @@ -4576,17 +4568,17 @@ void Executor::executeMakeSymbolic(ExecutionState &state, KTestObject *obj = si.getNextInput(mo, NamedSeedMatching); if (!obj) { - if (ZeroSeedExtension) { + if (AllowSeedExtension) { std::vector &values = si.assignment.bindings[array]; values = std::vector(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 &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; isize; ++i) + for (unsigned i = obj->numBytes; i < mo->size; ++i) values.push_back('\0'); - } } } } diff --git a/test/Feature/SeedConcretizeExtendFP.c b/test/Feature/SeedConcretizeExtendFP.c new file mode 100644 index 00000000..6a8de589 --- /dev/null +++ b/test/Feature/SeedConcretizeExtendFP.c @@ -0,0 +1,33 @@ +/* This test checks the case where the seed needs to be patched on re-run */ + +// RUN: %clang -emit-llvm -c %O0opt -g %s -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --entry-point=TestGen %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// 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 %t.bc 2>&1 | FileCheck %s + +#include "klee/klee.h" + +#include +#include +#include + +void TestGen() { + uint16_t x; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x == 1234); +} + +int main() { + uint32_t i; + klee_make_symbolic(&i, sizeof(i), "i"); + + if (i < 5000) { + double d = i; + // CHECK: concretizing (reason: floating point) + assert((unsigned) d < 5001); + } +} diff --git a/test/Feature/SeedConcretizePatchedFP.c b/test/Feature/SeedConcretizePatchedFP.c deleted file mode 100644 index b8b758b5..00000000 --- a/test/Feature/SeedConcretizePatchedFP.c +++ /dev/null @@ -1,33 +0,0 @@ -/* This test checks the case where the seed needs to be patched on re-run */ - -// RUN: %clang -emit-llvm -c %O0opt -g %s -o %t.bc -// RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --entry-point=TestGen %t.bc -// RUN: test -f %t.klee-out/test000001.ktest -// 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 - -#include "klee/klee.h" - -#include -#include -#include - -void TestGen() { - uint16_t x; - klee_make_symbolic(&x, sizeof(x), "x"); - klee_assume(x == 1234); -} - -int main() { - uint32_t i; - klee_make_symbolic(&i, sizeof(i), "i"); - - if (i < 5000) { - double d = i; - // CHECK: concretizing (reason: floating point) - assert((unsigned) d < 5001); - } -} 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 -- cgit 1.4.1