From a35ad1d9e19ba4048f7d45fe0df3dc1ecafac0a4 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 12 Nov 2023 15:26:51 +0400 Subject: [PATCH 01/11] [fix] `MemoryTriggerCoverOnTheFly` --- lib/Core/Executor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c5dc81f2f5..f0a919e514 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4142,7 +4142,7 @@ bool Executor::checkMemoryUsage() { const auto mmapUsage = memory->getUsedDeterministicSize() >> 20U; const auto totalUsage = mallocUsage + mmapUsage; - if (MemoryTriggerCoverOnTheFly && 3 * totalUsage <= 2 * MaxMemory) { + if (MemoryTriggerCoverOnTheFly && totalUsage > MaxMemory * 0.75) { klee_warning_once(0, "enabling cover-on-the-fly (close to memory cap: %luMB)", totalUsage); From 4eb4514c7ad98fafcc9cbf7b4bd4a8855fe16359 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 12 Nov 2023 17:11:37 +0400 Subject: [PATCH 02/11] [chore] Update `kleef` --- scripts/kleef | 21 +++++++++++++++++-- .../CoverageErrorCall/btor2c-lazyMod.mul6.c | 6 +++--- 2 files changed, 22 insertions(+), 5 deletions(-) diff --git a/scripts/kleef b/scripts/kleef index c98a94114a..3994601fe9 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -19,6 +19,7 @@ def klee_options( is32, f_err, f_cov, + write_ktests, ): if max_time and int(max_time) > 30: MAX_SOLVER_TIME = 10 @@ -29,6 +30,7 @@ def klee_options( "--delete-dead-loops=false", # without this optimizer removes some code, which decreases coverage "--emit-all-errors", # without this we generate only one test for assertion failures, which decreases coverage "--mock-all-externals", # this helps for some linux benchmarks, which have unused extern globals. without this flag we will not even start on them. + "--external-calls=all", "--use-forked-solver=false", # "--solver-backend=stp", "--solver-backend=z3-tree", @@ -42,6 +44,7 @@ def klee_options( "--output-istats=false", # "--istats-write-interval=90s", # Istats file can be large as well "--write-xml-tests", # Write tests in XML format + f"--write-ktests={write_ktests}", # Write tests in KTest format f"--xml-metadata-programfile={source.name}", # Provide the name of the original source file f"--xml-metadata-programhash={hexhash}", # Provide sha256 hash of source file # "--use-guided-search=none", @@ -101,8 +104,12 @@ def klee_options( ] if max_time: max_time = float(max_time) - late_time = int(max_time * 0.9) - last_time = int(max_time * 0.97) + if max_time and int(max_time) > 30: + late_time = int(max_time * 0.9) + last_time = int(max_time * 0.97) + else: + late_time = int(max_time * 0.8) + last_time = int(max_time * 0.9) cmd += [ "--cover-on-the-fly=true", f"--delay-cover-on-the-fly={late_time}", @@ -167,6 +174,7 @@ class KLEEF(object): max_time=0, use_perf=False, use_valgrind=False, + write_ktests=False, ): self.source = Path(source) if source else None self.is32 = is32 @@ -178,6 +186,10 @@ class KLEEF(object): self.max_time = max_time self.use_perf = use_perf self.use_valgrind = use_valgrind + if write_ktests: + self.write_ktests = "true" + else: + self.write_ktests = "false" # This file is inside the bin directory - use the root as base self.bin_directory = Path(__file__).parent @@ -280,6 +292,7 @@ class KLEEF(object): self.is32, self.f_err, self.f_cov, + self.write_ktests, ) if self.isModifyingUlimitPermitted(): cmd = ["ulimit -s unlimited", "&&"] + cmd @@ -378,6 +391,7 @@ def run(args): max_time=time, use_perf=args.perf, use_valgrind=args.valgrind, + write_ktests=args.write_ktests, ) wrapper.compile() return wrapper.run() @@ -426,6 +440,9 @@ def main(): type=str, default=None, ) + parser.add_argument( + "--write-ktests", help="Write tests in KTest format", action="store_true" + ) args = parser.parse_args() run(args) diff --git a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c index 0a1b1dcd5e..f11474a141 100644 --- a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c +++ b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c @@ -1,7 +1,7 @@ // It requires Z3 because the script currently runs with Z3 solver backend -//REQUIRES: z3 -//RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 %s 2>&1 | FileCheck %s -//CHECK: KLEE: WARNING: 100.00% Reachable Reachable +// REQUIRES: z3 +// RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --write-ktests %s 2>&1 | FileCheck %s +// CHECK: KLEE: WARNING: 100.00% Reachable Reachable // This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks From 67bcaa222a7fceb520cdc4d61d899ea1a117f36c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 14 Nov 2023 02:03:06 +0400 Subject: [PATCH 03/11] [fix] Optimized free-standing functions are broken --- lib/Core/Executor.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index f0a919e514..e97704699f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -575,7 +575,7 @@ llvm::Module *Executor::setModule( kmodule = std::make_unique(); // 1.) Link the modules together && 2.) Apply different instrumentation - kmodule->link(userModules, 0); + kmodule->link(userModules, 1); kmodule->instrument(opts); kmodule->link(libsModules, 2); @@ -603,8 +603,6 @@ llvm::Module *Executor::setModule( specialFunctionHandler = new SpecialFunctionHandler(*this); specialFunctionHandler->prepare(preservedFunctions); - preservedFunctions.push_back(opts.EntryPoint.c_str()); - // Preserve the free-standing library calls preservedFunctions.push_back("memset"); preservedFunctions.push_back("memcpy"); @@ -612,12 +610,21 @@ llvm::Module *Executor::setModule( preservedFunctions.push_back("memmove"); if (FunctionCallReproduce != "") { - // prevent elimination of the function - auto f = kmodule->module->getFunction(FunctionCallReproduce); - if (f) + preservedFunctions.push_back(FunctionCallReproduce.c_str()); + } + + // prevent elimination of the preservedFunctions functions + for (auto pf : preservedFunctions) { + auto f = kmodule->module->getFunction(pf); + if (f) { f->addFnAttr(Attribute::OptimizeNone); + f->addFnAttr(Attribute::NoInline); + } } + // except the entry point + preservedFunctions.push_back(opts.EntryPoint.c_str()); + kmodule->optimiseAndPrepare(opts, preservedFunctions); kmodule->checkModule(); From 420bd7c95acfb922299c28e5260c9525a5439600 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 10 Nov 2023 04:33:01 +0400 Subject: [PATCH 04/11] [chore] Update `kleef` script --- scripts/kleef | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/kleef b/scripts/kleef index 3994601fe9..35f0e4ac65 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -53,9 +53,10 @@ def klee_options( # "--libc=uclibc", # "--posix-runtime", "--fp-runtime", - "--x86FP-as-x87FP80", + "--x86FP-as-x87FP80=false", # "--max-sym-array-size=4096", "--symbolic-allocation-threshold=8192", + "--uninit-memory-test-multiplier=10", # "--dump-all-states=false", # "--search=nurs:covnew", # "--search=nurs:md2u", "--search=random-path", From b74bfa6127fae5d01ec3d148c060c4cb124004c3 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 15 Nov 2023 00:57:59 +0400 Subject: [PATCH 05/11] [fix] Address may be symbolic but unique, try resolve firstly --- lib/Core/Executor.cpp | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e97704699f..48a2b4ae09 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2949,18 +2949,19 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } else { ref v = eval(ki, 0, state).value; - if (!isa(v) && MockExternalCalls) { - if (ki->inst->getType()->isSized()) { - prepareMockValue(state, "mockExternResult", ki); - } - } else { - ExecutionState *free = &state; - bool hasInvalid = false, first = true; - - /* XXX This is wasteful, no need to do a full evaluate since we - have already got a value. But in the end the caches should - handle it for us, albeit with some overhead. */ - do { + ExecutionState *free = &state; + bool hasInvalid = false, first = true; + + /* XXX This is wasteful, no need to do a full evaluate since we + have already got a value. But in the end the caches should + handle it for us, albeit with some overhead. */ + do { + if (!first && MockExternalCalls) { + free = nullptr; + if (ki->inst->getType()->isSized()) { + prepareMockValue(state, "mockExternResult", ki); + } + } else { v = optimizer.optimizeExpr(v, true); ref value; bool success = solver->getValue(free->constraints.cs(), v, value, @@ -2993,8 +2994,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { first = false; free = res.second; timers.invoke(); - } while (free && !haltExecution); - } + } + } while (free && !haltExecution); } break; } From 52efb479295db2b0de569462b2e90378b1c7ad8f Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 15 Nov 2023 01:00:34 +0400 Subject: [PATCH 06/11] [fix] Put in order `fp-runtime` functions --- include/klee/Support/ModuleUtil.h | 35 ++++--------------- lib/Module/KModule.cpp | 19 ++-------- lib/Module/ModuleUtil.cpp | 16 +++++++++ runtime/klee-fp/CMakeLists.txt | 12 +++---- runtime/klee-fp/ceil.c | 16 ++++----- .../klee-fp/{klee_copysign.c => copysign.c} | 4 +-- .../klee-fp/{klee_copysign.h => copysign.h} | 2 +- runtime/klee-fp/fabs.c | 8 ++--- runtime/klee-fp/{klee_fenv.c => fenv.c} | 8 ++--- runtime/klee-fp/{klee_fenv.h => fenv.h} | 4 +-- runtime/klee-fp/{klee_floor.c => floor.c} | 11 +++--- runtime/klee-fp/{klee_floor.h => floor.h} | 8 ++--- runtime/klee-fp/fpclassify.c | 27 +++++++++----- .../{klee_internal_isinf.ll => isinf.ll} | 28 +++++++++++---- runtime/klee-fp/log.c | 3 +- runtime/klee-fp/{klee_rint.c => rint.c} | 10 +++--- runtime/klee-fp/{klee_rint.h => rint.h} | 8 ++--- runtime/klee-fp/round.c | 6 ++++ .../klee-fp/{klee_signbit.ll => signbit.ll} | 6 ++-- runtime/klee-fp/sqrt.c | 8 ++--- tools/klee/main.cpp | 16 --------- 21 files changed, 124 insertions(+), 131 deletions(-) rename runtime/klee-fp/{klee_copysign.c => copysign.c} (97%) rename runtime/klee-fp/{klee_copysign.h => copysign.h} (88%) rename runtime/klee-fp/{klee_fenv.c => fenv.c} (92%) rename runtime/klee-fp/{klee_fenv.h => fenv.h} (85%) rename runtime/klee-fp/{klee_floor.c => floor.c} (79%) rename runtime/klee-fp/{klee_floor.h => floor.h} (68%) rename runtime/klee-fp/{klee_internal_isinf.ll => isinf.ll} (78%) rename runtime/klee-fp/{klee_rint.c => rint.c} (62%) rename runtime/klee-fp/{klee_rint.h => rint.h} (69%) rename runtime/klee-fp/{klee_signbit.ll => signbit.ll} (89%) diff --git a/include/klee/Support/ModuleUtil.h b/include/klee/Support/ModuleUtil.h index 4d385c4c42..7ff0e36bd2 100644 --- a/include/klee/Support/ModuleUtil.h +++ b/include/klee/Support/ModuleUtil.h @@ -39,19 +39,16 @@ bool linkModules(llvm::Module *composite, std::vector> &modules, const unsigned Flags, std::string &errorMsg); -#if defined(__x86_64__) || defined(__i386__) -#define addFunctionReplacement(from, to) \ - {#from "f", #to "f"}, {#from "", #to ""}, { "" #from "l", #to "l" } +void replaceOrRenameFunction(llvm::Module *module, const char *old_name, + const char *new_name); +#if defined(__x86_64__) || defined(__i386__) #define addIntrinsicReplacement(from, to) \ {"llvm." #from ".f32", #to "f"}, {"llvm." #from ".f64", #to}, { \ "llvm." #from ".f80", #to "l" \ } #else -#define addFunctionReplacement(from, to) \ - {#from "f", #to "f"}, { "" #from, "" #to } - #define addIntrinsicReplacement(from, to) \ {"llvm." #from ".f32", #to "f"}, { "llvm." #from ".f64", #to } @@ -62,33 +59,15 @@ bool linkModules(llvm::Module *composite, /// implementations in runtime/klee-fp, but not explicitly replaced here. Should /// we rename them and complete the list? const std::vector> floatReplacements = { - addFunctionReplacement(__isnan, klee_internal_isnan), - addFunctionReplacement(isnan, klee_internal_isnan), - addFunctionReplacement(__isinf, klee_internal_isinf), - addFunctionReplacement(isinf, klee_internal_isinf), - addFunctionReplacement(__fpclassify, klee_internal_fpclassify), - addFunctionReplacement(fpclassify, klee_internal_fpclassify), - addFunctionReplacement(__finite, klee_internal_finite), - addFunctionReplacement(finite, klee_internal_finite), - addFunctionReplacement(sqrt, klee_internal_sqrt), - addFunctionReplacement(fabs, klee_internal_fabs), - addFunctionReplacement(rint, klee_internal_rint), - addFunctionReplacement(round, klee_internal_rint), - addFunctionReplacement(__signbit, klee_internal_signbit), - addIntrinsicReplacement(sqrt, klee_internal_sqrt), - addIntrinsicReplacement(rint, klee_internal_rint), - addIntrinsicReplacement(round, klee_internal_rint), + addIntrinsicReplacement(sqrt, sqrt), + addIntrinsicReplacement(rint, rint), + addIntrinsicReplacement(round, rint), addIntrinsicReplacement(nearbyint, nearbyint), addIntrinsicReplacement(copysign, copysign), - addIntrinsicReplacement(floor, klee_floor), + addIntrinsicReplacement(floor, floor), addIntrinsicReplacement(ceil, ceil)}; -#undef addFunctionReplacement #undef addIntrinsicReplacement -const std::vector> feRoundReplacements{ - {"fegetround", "klee_internal_fegetround"}, - {"fesetround", "klee_internal_fesetround"}}; - /// Return the Function* target of a Call or Invoke instruction, or /// null if it cannot be determined (should be only for indirect /// calls, although complicated constant expressions might be diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index ce09edfcc2..64e1d3037c 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -235,19 +235,6 @@ bool KModule::link(std::vector> &modules, return true; } -void KModule::replaceFunction(const std::unique_ptr &m, - const char *original, const char *replacement) { - llvm::Function *originalFunc = m->getFunction(original); - llvm::Function *replacementFunc = m->getFunction(replacement); - if (!originalFunc) - return; - klee_message("Replacing function \"%s\" with \"%s\"", original, replacement); - assert(replacementFunc && "Replacement function not found"); - assert(!(replacementFunc->isDeclaration()) && "replacement must have body"); - originalFunc->replaceAllUsesWith(replacementFunc); - originalFunc->eraseFromParent(); -} - void KModule::instrument(const Interpreter::ModuleOptions &opts) { // Inject checks prior to optimization... we also perform the // invariant transformations that we will end up doing later so that @@ -301,12 +288,10 @@ void KModule::optimiseAndPrepare( if (opts.WithFPRuntime) { if (UseKleeFloatInternals) { for (const auto &p : klee::floatReplacements) { - replaceFunction(module, p.first.c_str(), p.second.c_str()); + replaceOrRenameFunction(module.get(), p.first.c_str(), + p.second.c_str()); } } - for (const auto &p : klee::feRoundReplacements) { - replaceFunction(module, p.first.c_str(), p.second.c_str()); - } } // Needs to happen after linking (since ctors/dtors can be modified) diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp index e64d628e71..d23e41a607 100644 --- a/lib/Module/ModuleUtil.cpp +++ b/lib/Module/ModuleUtil.cpp @@ -367,3 +367,19 @@ bool klee::loadFileAsOneModule( } return res; } + +void klee::replaceOrRenameFunction(llvm::Module *module, const char *old_name, + const char *new_name) { + Function *new_function, *old_function; + new_function = module->getFunction(new_name); + old_function = module->getFunction(old_name); + if (old_function) { + if (new_function) { + old_function->replaceAllUsesWith(new_function); + old_function->eraseFromParent(); + } else { + old_function->setName(new_name); + assert(old_function->getName() == new_name); + } + } +} \ No newline at end of file diff --git a/runtime/klee-fp/CMakeLists.txt b/runtime/klee-fp/CMakeLists.txt index 0314ca9c50..42b2829004 100644 --- a/runtime/klee-fp/CMakeLists.txt +++ b/runtime/klee-fp/CMakeLists.txt @@ -10,18 +10,18 @@ set(LIB_PREFIX "RuntimeFp") set(SRC_FILES ceil.c - klee_copysign.c + copysign.c exp.c fabs.c - klee_fenv.c - klee_floor.c + fenv.c + floor.c fpclassify.c - klee_internal_isinf.ll - klee_rint.c + isinf.ll klee_set_rounding_mode.c - klee_signbit.ll log.c + rint.c round.c + signbit.ll sqrt.c trigonometry.c ) diff --git a/runtime/klee-fp/ceil.c b/runtime/klee-fp/ceil.c index 9d112a16a3..d185cb7cb1 100644 --- a/runtime/klee-fp/ceil.c +++ b/runtime/klee-fp/ceil.c @@ -8,26 +8,26 @@ //===----------------------------------------------------------------------===*/ #include "float.h" -#include "klee_floor.h" -#include "klee_rint.h" +#include "floor.h" +#include "rint.h" float ceilf(float f) { - if (f == klee_internal_rintf(f)) { + if (f == rintf(f)) { return f; } - return ((f < 0.0f) ? -1 : 1) + klee_floorf(f); + return ((f < 0.0f) ? -1 : 1) + floorf(f); } double ceil(double f) { - if (f == klee_internal_rint(f)) { + if (f == rint(f)) { return f; } - return ((f < 0.0f) ? -1 : 1) + klee_floor(f); + return ((f < 0.0f) ? -1 : 1) + floor(f); } long double ceill(long double f) { - if (f == klee_internal_rintl(f)) { + if (f == rintl(f)) { return f; } - return ((f < 0.0f) ? -1 : 1) + klee_floorl(f); + return ((f < 0.0f) ? -1 : 1) + floorl(f); } diff --git a/runtime/klee-fp/klee_copysign.c b/runtime/klee-fp/copysign.c similarity index 97% rename from runtime/klee-fp/klee_copysign.c rename to runtime/klee-fp/copysign.c index ddd72fdc53..7505b51ffb 100644 --- a/runtime/klee-fp/klee_copysign.c +++ b/runtime/klee-fp/copysign.c @@ -1,4 +1,4 @@ -/*===-- klee_copysign.c ---------------------------------------------------===// +/*===-- copysign.c --------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===*/ -#include "klee_copysign.h" +#include "copysign.h" #include "ansidecl.h" #include "klee/klee.h" diff --git a/runtime/klee-fp/klee_copysign.h b/runtime/klee-fp/copysign.h similarity index 88% rename from runtime/klee-fp/klee_copysign.h rename to runtime/klee-fp/copysign.h index 444e0ab264..4384a216cb 100644 --- a/runtime/klee-fp/klee_copysign.h +++ b/runtime/klee-fp/copysign.h @@ -1,4 +1,4 @@ -/*===-- klee_copysign.h ---------------------------------------------------===// +/*===-- copysign.h --------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // diff --git a/runtime/klee-fp/fabs.c b/runtime/klee-fp/fabs.c index c3c4c88a6a..236cc38658 100644 --- a/runtime/klee-fp/fabs.c +++ b/runtime/klee-fp/fabs.c @@ -8,12 +8,10 @@ //===----------------------------------------------------------------------===*/ #include "klee/klee.h" -double klee_internal_fabs(double d) { return klee_abs_double(d); } +double fabs(double d) { return klee_abs_double(d); } -float klee_internal_fabsf(float f) { return klee_abs_float(f); } +float fabsf(float f) { return klee_abs_float(f); } #if defined(__x86_64__) || defined(__i386__) -long double klee_internal_fabsl(long double f) { - return klee_abs_long_double(f); -} +long double fabsl(long double f) { return klee_abs_long_double(f); } #endif diff --git a/runtime/klee-fp/klee_fenv.c b/runtime/klee-fp/fenv.c similarity index 92% rename from runtime/klee-fp/klee_fenv.c rename to runtime/klee-fp/fenv.c index d6b52e3820..0a70f90f34 100644 --- a/runtime/klee-fp/klee_fenv.c +++ b/runtime/klee-fp/fenv.c @@ -1,4 +1,4 @@ -/*===-- klee_fenv.c -------------------------------------------------------===// +/*===-- fenv.c ------------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -6,7 +6,7 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===*/ -#include "klee_fenv.h" +#include "fenv.h" #include "klee/klee.h" // Define the constants. Don't include `fenv.h` here to avoid @@ -28,7 +28,7 @@ enum { #error Architecture not supported #endif -int klee_internal_fegetround(void) { +int fegetround(void) { enum KleeRoundingMode rm = klee_get_rounding_mode(); switch (rm) { case KLEE_FP_RNE: @@ -52,7 +52,7 @@ int klee_internal_fegetround(void) { } } -int klee_internal_fesetround(int rm) { +int fesetround(int rm) { switch (rm) { case FE_TONEAREST: klee_set_rounding_mode(KLEE_FP_RNE); diff --git a/runtime/klee-fp/klee_fenv.h b/runtime/klee-fp/fenv.h similarity index 85% rename from runtime/klee-fp/klee_fenv.h rename to runtime/klee-fp/fenv.h index af75c5591b..3cb7728f20 100644 --- a/runtime/klee-fp/klee_fenv.h +++ b/runtime/klee-fp/fenv.h @@ -11,7 +11,7 @@ #define KLEE_FENV_H #include "klee/klee.h" -int klee_internal_fegetround(void); -int klee_internal_fesetround(int rm); +int fegetround(void); +int fesetround(int rm); #endif // KLEE_FENV_H diff --git a/runtime/klee-fp/klee_floor.c b/runtime/klee-fp/floor.c similarity index 79% rename from runtime/klee-fp/klee_floor.c rename to runtime/klee-fp/floor.c index 51a3785fe7..3b79738fe2 100644 --- a/runtime/klee-fp/klee_floor.c +++ b/runtime/klee-fp/floor.c @@ -1,4 +1,5 @@ -/*===-- klee_floor.c ------------------------------------------------------===// +/*===-- floor.c +------------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,11 +8,11 @@ // //===----------------------------------------------------------------------===*/ -#include "klee_floor.h" +#include "floor.h" #include "klee/klee.h" #include "math.h" -float klee_floorf(float x) { +float floorf(float x) { int sign = signbit(x); x = klee_abs_float(x); if (klee_rintf(x) > x) { @@ -21,7 +22,7 @@ float klee_floorf(float x) { } } -double klee_floor(double x) { +double floor(double x) { int sign = signbit(x); x = klee_abs_double(x); if (klee_rint(x) > x) { @@ -31,7 +32,7 @@ double klee_floor(double x) { } } -long double klee_floorl(long double x) { +long double floorl(long double x) { int sign = signbit(x); x = klee_abs_long_double(x); if (klee_rintl(x) > x) { diff --git a/runtime/klee-fp/klee_floor.h b/runtime/klee-fp/floor.h similarity index 68% rename from runtime/klee-fp/klee_floor.h rename to runtime/klee-fp/floor.h index 03e1c1c8da..4cdbc93981 100644 --- a/runtime/klee-fp/klee_floor.h +++ b/runtime/klee-fp/floor.h @@ -1,4 +1,4 @@ -/*===-- klee_floor.h ------------------------------------------------------===// +/*===-- floor.h -----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -10,8 +10,8 @@ #ifndef KLEE_FLOOR_H #define KLEE_FLOOR_H -float klee_floorf(float x); -double klee_floor(double x); -long double klee_floorl(long double x); +float floorf(float x); +double floor(double x); +long double floorl(long double x); #endif // KLEE_FLOOR_H diff --git a/runtime/klee-fp/fpclassify.c b/runtime/klee-fp/fpclassify.c index 06f9d001f9..0e0b1b179d 100644 --- a/runtime/klee-fp/fpclassify.c +++ b/runtime/klee-fp/fpclassify.c @@ -13,16 +13,19 @@ // during linking. // __isnanf -int klee_internal_isnanf(float f) { return klee_is_nan_float(f); } +int __isnanf(float f) { return klee_is_nan_float(f); } +int isnanf(float f) { return __isnanf(f); } // __isnan -int klee_internal_isnan(double d) { return klee_is_nan_double(d); } +int __isnan(double d) { return klee_is_nan_double(d); } +int isnan(double d) { return __isnan(d); } // __isnanl -int klee_internal_isnanl(long double d) { return klee_is_nan_long_double(d); } +int __isnanl(long double d) { return klee_is_nan_long_double(d); } +int isnanl(long double d) { return __isnanl(d); } // __fpclassifyf -int klee_internal_fpclassifyf(float f) { +int __fpclassifyf(float f) { /* * This version acts like a switch case which returns correct * float type from the enum, but itself does not fork @@ -33,38 +36,44 @@ int klee_internal_fpclassifyf(float f) { int x = klee_is_normal_float(f); return ((x << 2) | ((c | d) << 1) | (b | d)); } +int fpclassifyf(float f) { return __fpclassifyf(f); } // __fpclassify -int klee_internal_fpclassify(double f) { +int __fpclassify(double f) { int b = klee_is_infinite_double(f); int c = (f == 0.0f); int d = klee_is_subnormal_double(f); int x = klee_is_normal_double(f); return ((x << 2) | ((c | d) << 1) | (b | d)); } +int fpclassify(double f) { return __fpclassify(f); } // __fpclassifyl #if defined(__x86_64__) || defined(__i386__) -int klee_internal_fpclassifyl(long double f) { +int __fpclassifyl(long double f) { int b = klee_is_infinite_long_double(f); int c = (f == 0.0f); int d = klee_is_subnormal_long_double(f); int x = klee_is_normal_long_double(f); return ((x << 2) | ((c | d) << 1) | (b | d)); } +int fpclassifyl(long double f) { return __fpclassifyl(f); } #endif // __finitef -int klee_internal_finitef(float f) { +int __finitef(float f) { return (!klee_is_nan_float(f)) & (!klee_is_infinite_float(f)); } +int finitef(float f) { return __finitef(f); } // __finite -int klee_internal_finite(double f) { +int __finite(double f) { return (!klee_is_nan_double(f)) & (!klee_is_infinite_double(f)); } +int finite(double f) { return __finite(f); } // __finitel -int klee_internal_finitel(long double f) { +int __finitel(long double f) { return (!klee_is_nan_long_double(f)) & (!klee_is_infinite_long_double(f)); } +int finitel(long double f) { return finitel(f); } diff --git a/runtime/klee-fp/klee_internal_isinf.ll b/runtime/klee-fp/isinf.ll similarity index 78% rename from runtime/klee-fp/klee_internal_isinf.ll rename to runtime/klee-fp/isinf.ll index 8a50b15134..f22bee07ce 100644 --- a/runtime/klee-fp/klee_internal_isinf.ll +++ b/runtime/klee-fp/isinf.ll @@ -1,4 +1,4 @@ -;;===-- klee_internal_isinff.ll --------------------------------------------===;; +;;===-- isinff.ll ---------------------------------------------------------===;; ;; ;; The KLEE Symbolic Virtual Machine ;; @@ -6,8 +6,6 @@ ;; License. See LICENSE.TXT for details. ;; ;;===----------------------------------------------------------------------===;; -;target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128" -;target triple = "x86_64-unknown-linux-gnu" ;; These are implementations of internal functions found in libm for classifying ;; floating point numbers. They have different names to avoid name collisions @@ -19,7 +17,7 @@ declare zeroext i1 @klee_is_infinite_float(float) #2 declare zeroext i1 @klee_is_infinite_double(double) #2 declare zeroext i1 @klee_is_infinite_long_double(x86_fp80) #2 -define i32 @klee_internal_isinff(float %f) #1 #0 { +define i32 @__isinff(float %f) #1 #0 { entry: %isinf = tail call zeroext i1 @klee_is_infinite_float(float %f) #3 %cmp = fcmp ogt float %f, 0.000000e+00 @@ -28,7 +26,13 @@ entry: ret i32 %result } -define i32 @klee_internal_isinf(double %d) #1 #0 { +define i32 @isinff(float %f) #1 #0 { +entry: + %result = tail call zeroext i32 @__isinff(float %f) #3 + ret i32 %result +} + +define i32 @__isinf(double %d) #1 #0 { entry: %isinf = tail call zeroext i1 @klee_is_infinite_double(double %d) #3 %cmp = fcmp ogt double %d, 0.000000e+00 @@ -37,7 +41,13 @@ entry: ret i32 %result } -define i32 @klee_internal_isinfl(x86_fp80 %d) #0 { +define i32 @isinf(double %d) #1 #0 { +entry: + %result = tail call zeroext i32 @__isinf(double %d) #3 + ret i32 %result +} + +define i32 @__isinfl(x86_fp80 %d) #0 { entry: %isinf = tail call zeroext i1 @klee_is_infinite_long_double(x86_fp80 %d) #3 %cmp = fcmp ogt x86_fp80 %d, 0xK00000000000000000000 @@ -46,6 +56,12 @@ entry: ret i32 %result } +define i32 @isinfl(x86_fp80 %d) #0 { +entry: + %result = tail call zeroext i32 @__isinfl(x86_fp80 %d) #3 + ret i32 %result +} + ; NOTE: Use of optnone and noinline here are important so that the KLEE diff --git a/runtime/klee-fp/log.c b/runtime/klee-fp/log.c index 25b797ace4..77f3d3a12f 100644 --- a/runtime/klee-fp/log.c +++ b/runtime/klee-fp/log.c @@ -8,9 +8,10 @@ //===----------------------------------------------------------------------===*/ #include "fenv.h" -#include "klee_fenv.h" #include "math.h" +#include + #define LOG_CORNER_CASE(suffix, type, isnan_function) \ int log_corner_case_##suffix(type *x) { \ if (isinf(*x) || isnan_function(*x)) { \ diff --git a/runtime/klee-fp/klee_rint.c b/runtime/klee-fp/rint.c similarity index 62% rename from runtime/klee-fp/klee_rint.c rename to runtime/klee-fp/rint.c index 9dc7701991..a15096a01c 100644 --- a/runtime/klee-fp/klee_rint.c +++ b/runtime/klee-fp/rint.c @@ -1,4 +1,4 @@ -/*===-- klee_rint.c -------------------------------------------------------===// +/*===-- rint.c ------------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,14 +7,14 @@ // //===----------------------------------------------------------------------===*/ -#include "klee_rint.h" +#include "rint.h" #include "klee/klee.h" -float klee_internal_rintf(float arg) { return klee_rintf(arg); } +float rintf(float arg) { return klee_rintf(arg); } -double klee_internal_rint(double arg) { return klee_rint(arg); } +double rint(double arg) { return klee_rint(arg); } -long double klee_internal_rintl(long double arg) { return klee_rintl(arg); } +long double rintl(long double arg) { return klee_rintl(arg); } float nearbyintf(float arg) { return klee_rintf(arg); } diff --git a/runtime/klee-fp/klee_rint.h b/runtime/klee-fp/rint.h similarity index 69% rename from runtime/klee-fp/klee_rint.h rename to runtime/klee-fp/rint.h index b1be763080..4fb35f4382 100644 --- a/runtime/klee-fp/klee_rint.h +++ b/runtime/klee-fp/rint.h @@ -1,4 +1,4 @@ -/*===-- klee_rint.h -------------------------------------------------------===// +/*===-- rint.h ------------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -10,9 +10,9 @@ #ifndef KLEE_RINT_H #define KLEE_RINT_H -float klee_internal_rintf(float arg); -double klee_internal_rint(double arg); -long double klee_internal_rintl(long double arg); +float rintf(float arg); +double rint(double arg); +long double rintl(long double arg); float nearbyintf(float arg); double nearbyint(double arg); long double nearbyintl(long double arg); diff --git a/runtime/klee-fp/round.c b/runtime/klee-fp/round.c index 490cc4849e..d5a6ad9f51 100644 --- a/runtime/klee-fp/round.c +++ b/runtime/klee-fp/round.c @@ -9,6 +9,12 @@ #include "klee/klee.h" +float roundf(float x) { return klee_rintf(x); } + +double round(double x) { return klee_rint(x); } + +long double roundl(long double x) { return klee_rintl(x); } + long lroundf(float x) { return klee_rintf(x); } long lround(double x) { return klee_rint(x); } diff --git a/runtime/klee-fp/klee_signbit.ll b/runtime/klee-fp/signbit.ll similarity index 89% rename from runtime/klee-fp/klee_signbit.ll rename to runtime/klee-fp/signbit.ll index a7c504f856..8ee4768ed9 100644 --- a/runtime/klee-fp/klee_signbit.ll +++ b/runtime/klee-fp/signbit.ll @@ -9,7 +9,7 @@ ;target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128" ;target triple = "x86_64-unknown-linux-gnu" -define i32 @klee_internal_signbitf(float %f) #1 #0 { +define i32 @__signbitf(float %f) #1 #0 { entry: %0 = bitcast float %f to i32 %1 = icmp slt i32 %0, 0 @@ -17,7 +17,7 @@ entry: ret i32 %2 } -define i32 @klee_internal_signbit(double %d) #1 #0 { +define i32 @__signbit(double %d) #1 #0 { entry: %0 = bitcast double %d to i64 %1 = icmp slt i64 %0, 0 @@ -25,7 +25,7 @@ entry: ret i32 %2 } -define i32 @klee_internal_signbitl(x86_fp80 %d) #0 { +define i32 @__signbitl(x86_fp80 %d) #0 { entry: %0 = bitcast x86_fp80 %d to i80 %1 = icmp slt i80 %0, 0 diff --git a/runtime/klee-fp/sqrt.c b/runtime/klee-fp/sqrt.c index ba1b928340..26fbe2cc9f 100644 --- a/runtime/klee-fp/sqrt.c +++ b/runtime/klee-fp/sqrt.c @@ -8,12 +8,10 @@ //===----------------------------------------------------------------------===*/ #include "klee/klee.h" -double klee_internal_sqrt(double d) { return klee_sqrt_double(d); } +double sqrt(double d) { return klee_sqrt_double(d); } -float klee_internal_sqrtf(float f) { return klee_sqrt_float(f); } +float sqrtf(float f) { return klee_sqrt_float(f); } #if defined(__x86_64__) || defined(__i386__) -long double klee_internal_sqrtl(long double f) { - return klee_sqrt_long_double(f); -} +long double sqrtl(long double f) { return klee_sqrt_long_double(f); } #endif diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 71e7f8623a..766013544b 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -1222,22 +1222,6 @@ static void halt_via_gdb(int pid) { perror("system"); } -static void replaceOrRenameFunction(llvm::Module *module, const char *old_name, - const char *new_name) { - Function *new_function, *old_function; - new_function = module->getFunction(new_name); - old_function = module->getFunction(old_name); - if (old_function) { - if (new_function) { - old_function->replaceAllUsesWith(new_function); - old_function->eraseFromParent(); - } else { - old_function->setName(new_name); - assert(old_function->getName() == new_name); - } - } -} - static void createLibCWrapper(std::vector> &userModules, std::vector> &libsModules, From 62aa5ed6078b2874f77ac9b79069d79856569bad Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 15 Nov 2023 06:08:44 +0400 Subject: [PATCH 07/11] [fix] Bring calls to `SparseStorage` constructor up to date --- lib/Solver/CexCachingSolver.cpp | 5 +++-- lib/Solver/ConcretizingSolver.cpp | 2 +- lib/Solver/IndependentSolver.cpp | 2 +- unittests/Assignment/AssignmentTest.cpp | 2 +- 4 files changed, 6 insertions(+), 5 deletions(-) diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 2c4b83d4c8..3cd4947c9f 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -382,10 +382,11 @@ bool CexCachingSolver::computeInitialValues( // FIXME: We should use smarter assignment for result so we don't // need redundant copy. values = std::vector>(objects.size()); + Assignment::bindings_ty aBindings; + a->tryGetInitialValues(aBindings); + for (unsigned i = 0; i < objects.size(); ++i) { const Array *os = objects[i]; - Assignment::bindings_ty aBindings; - a->tryGetInitialValues(aBindings); Assignment::bindings_ty::iterator it = aBindings.find(os); if (it == aBindings.end()) { diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index c2d717ceed..6f0327a226 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -378,7 +378,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, sizeSymcrete->addressSymcrete.symcretized, newSize); unsigned char *charAddressIterator = reinterpret_cast(&address); - SparseStorage storage(sizeof(address)); + SparseStorage storage(0); storage.store(0, charAddressIterator, charAddressIterator + sizeof(address)); diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 67c0309335..56cf4d043c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -225,7 +225,7 @@ bool IndependentSolver::computeInitialValues( dyn_cast(retMap.evaluate(arr->size)); assert(arrayConstantSize && "Array of symbolic size had not receive value for size!"); - SparseStorage ret(arrayConstantSize->getZExtValue()); + SparseStorage ret(0); values.push_back(ret); } else { values.push_back(retMap.bindings.at(arr)); diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp index 410a4ce357..419a4d0956 100644 --- a/unittests/Assignment/AssignmentTest.cpp +++ b/unittests/Assignment/AssignmentTest.cpp @@ -19,7 +19,7 @@ TEST(AssignmentTest, FoldNotOptimized) { SourceBuilder::makeSymbolic("simple_array", 0)); // Create a simple assignment std::vector objects; - SparseStorage value(1); + SparseStorage value(0); std::vector> values; objects.push_back(array); From c5839a462259ee85399022dde47b7209fcf36946 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 7 Sep 2023 01:01:56 +0400 Subject: [PATCH 08/11] [feat] Add `BlockLevelSearcher` --- include/klee/Module/KModule.h | 9 ++ lib/Core/ExecutionState.cpp | 3 + lib/Core/ExecutionState.h | 2 + lib/Core/Executor.cpp | 2 +- lib/Core/Searcher.cpp | 130 +++++++++++++++++- lib/Core/Searcher.h | 64 +++++++++ lib/Core/TargetedExecutionManager.cpp | 5 +- lib/Core/TargetedExecutionManager.h | 8 +- lib/Core/UserSearcher.cpp | 8 +- test/Feature/BlockPath.ll | 2 +- test/Feature/OvershiftCheck.c | 4 +- test/Feature/consecutive_divide_by_zero.c | 4 +- test/Feature/srem.c | 4 +- .../DefaultPointerAlignment.c | 4 +- test/Solver/CexCacheValidityCoresCheck.c | 4 +- 15 files changed, 225 insertions(+), 28 deletions(-) diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index 83cef2cce5..025b4ddc0f 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -187,6 +187,9 @@ struct KFunction : public KCallable { /// Unique index for KFunction and KInstruction inside KModule /// from 0 to [KFunction + KInstruction] [[nodiscard]] inline unsigned getGlobalIndex() const { return globalIndex; } + + bool operator<(const KFunction &rhs) const { return id < rhs.id; } + bool operator<(const KFunction *rhs) const { return id < rhs->id; } }; struct KBlockCompare { @@ -197,6 +200,12 @@ struct KBlockCompare { } }; +struct KFunctionCompare { + bool operator()(const KFunction *a, const KFunction *b) const { + return a->id < b->id; + } +}; + class KConstant { public: /// Actual LLVM constant this represents. diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 31d60372dd..471e58f101 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -446,7 +446,10 @@ void ExecutionState::increaseLevel() { if (prevPC->inst->isTerminator() && kmodule->inMainModule(*kf->function)) { auto srcLevel = stack.infoStack().back().multilevel[srcbb].second; stack.infoStack().back().multilevel.replace({srcbb, srcLevel + 1}); + stack.infoStack().back().maxMultilevel = + std::max(stack.infoStack().back().maxMultilevel, srcLevel + 1); level.insert(prevPC->parent); + stack.infoStack().back().level.insert(prevPC->parent); } } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 9e74c4ef37..c15cebe282 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -96,6 +96,8 @@ struct InfoStackFrame { KFunction *kf; CallPathNode *callPathNode = nullptr; PersistentMap multilevel; + unsigned long long maxMultilevel = 0; + std::set level; /// Minimum distance to an uncovered instruction once the function /// returns. This is not a good place for this but is used to diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 48a2b4ae09..397c68572a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -6763,7 +6763,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, if (guidanceKind == GuidanceKind::ErrorGuidance) { std::map, - klee::TargetedExecutionManager::KFunctionLess> + klee::KFunctionCompare> prepTargets; if (FunctionCallReproduce == "") { auto &paths = interpreterOpts.Paths.value(); diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index f2d91cfd79..e3535af48e 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -181,8 +181,7 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) { return weight; } auto distRes = distanceCalculator.getDistance(*es, target->getBlock()); - weight = klee::util::ulog2(distRes.weight + es->steppedMemoryInstructions + - 1); // [0, 32) + weight = klee::util::ulog2(distRes.weight + 1); // [0, 32) if (!distRes.isInsideFunction) { weight += 32; // [32, 64) } @@ -193,12 +192,12 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) { ExecutionState &GuidedSearcher::selectState() { unsigned size = historiesAndTargets.size(); - index = theRNG.getInt32() % (size + 1); + interleave ^= 1; ExecutionState *state = nullptr; - if (index == size) { + if (interleave || !size) { state = &baseSearcher->selectState(); } else { - index = index % size; + index = theRNG.getInt32() % size; auto &historyTargetPair = historiesAndTargets[index]; ref history = historyTargetPair.first; ref target = historyTargetPair.second; @@ -763,3 +762,124 @@ void InterleavedSearcher::printName(llvm::raw_ostream &os) { searcher->printName(os); os << "\n"; } + +/// + +BlockLevelSearcher::BlockLevelSearcher(RNG &rng) : theRNG{rng} {} + +ExecutionState &BlockLevelSearcher::selectState() { + unsigned rnd = 0; + unsigned index = 0; + unsigned mod = 10; + unsigned border = 9; + + auto kfi = data.begin(); + index = theRNG.getInt32() % data.size(); + std::advance(kfi, index); + auto &sizesTo = kfi->second; + + for (auto &sizesSize : sizesTo) { + rnd = theRNG.getInt32(); + if (rnd % mod < border) { + for (auto &size : sizesSize.second) { + rnd = theRNG.getInt32(); + if (rnd % mod < border) { + auto lbi = size.second.begin(); + index = theRNG.getInt32() % size.second.size(); + std::advance(lbi, index); + auto &level = *lbi; + auto si = level.second.begin(); + index = theRNG.getInt32() % level.second.size(); + std::advance(si, index); + auto &state = *si; + return *state; + } + } + } + } + + return **(sizesTo.begin()->second.begin()->second.begin()->second.begin()); +} + +void BlockLevelSearcher::clear(ExecutionState &state) { + KFunction *kf = state.initPC->parent->parent; + BlockLevel &bl = stateToBlockLevel[&state]; + auto &sizeTo = data[kf]; + auto &sizesTo = sizeTo[bl.sizeOfLevel]; + auto &levelTo = sizesTo[bl.sizesOfFrameLevels]; + auto &states = levelTo[bl.maxMultilevel]; + + states.erase(&state); + if (states.size() == 0) { + levelTo.erase(bl.maxMultilevel); + } + if (levelTo.size() == 0) { + sizesTo.erase(bl.sizesOfFrameLevels); + } + if (sizesTo.size() == 0) { + sizeTo.erase(bl.sizeOfLevel); + } + if (sizeTo.size() == 0) { + data.erase(kf); + } +} + +void BlockLevelSearcher::update(ExecutionState *current, + const StateIterable &addedStates, + const StateIterable &removedStates) { + if (current && std::find(removedStates.begin(), removedStates.end(), + current) == removedStates.end()) { + KFunction *kf = current->initPC->parent->parent; + BlockLevel &bl = stateToBlockLevel[current]; + sizes.clear(); + unsigned long long maxMultilevel = 0u; + for (auto &infoFrame : current->stack.infoStack()) { + sizes.push_back(infoFrame.level.size()); + maxMultilevel = std::max(maxMultilevel, infoFrame.maxMultilevel); + } + for (auto &kfLevel : current->stack.multilevel) { + maxMultilevel = std::max(maxMultilevel, kfLevel.second); + } + if (sizes != bl.sizesOfFrameLevels || + current->level.size() != bl.sizeOfLevel || + maxMultilevel != bl.maxMultilevel) { + clear(*current); + + data[kf][current->level.size()][sizes][maxMultilevel].insert(current); + + stateToBlockLevel[current] = + BlockLevel(kf, current->level.size(), sizes, maxMultilevel); + } + } + + for (const auto state : addedStates) { + KFunction *kf = state->initPC->parent->parent; + + sizes.clear(); + unsigned long long maxMultilevel = 0u; + for (auto &infoFrame : state->stack.infoStack()) { + sizes.push_back(infoFrame.level.size()); + maxMultilevel = std::max(maxMultilevel, infoFrame.maxMultilevel); + } + for (auto &kfLevel : state->stack.multilevel) { + maxMultilevel = std::max(maxMultilevel, kfLevel.second); + } + + data[kf][state->level.size()][sizes][maxMultilevel].insert(state); + + stateToBlockLevel[state] = + BlockLevel(kf, state->level.size(), sizes, maxMultilevel); + } + + // remove states + for (const auto state : removedStates) { + clear(*state); + stateToBlockLevel.erase(state); + } +} + +bool BlockLevelSearcher::empty() { return stateToBlockLevel.empty(); } + +void BlockLevelSearcher::printName(llvm::raw_ostream &os) { + os << "BlockLevelSearcher\n"; +} diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 8b8224f85c..2be9b1bf53 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -76,6 +76,7 @@ class Searcher { enum CoreSearchType : std::uint8_t { DFS, BFS, + BlockLevelSearch, RandomState, RandomPath, NURS_CovNew, @@ -169,6 +170,7 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { DistanceCalculator &distanceCalculator; RNG &theRNG; unsigned index{1}; + bool interleave = true; TargetForestHistoryTargetSet localHistoryTargets; std::vector baseAddedStates; @@ -363,6 +365,68 @@ class InterleavedSearcher final : public Searcher { void printName(llvm::raw_ostream &os) override; }; +class BlockLevelSearcher final : public Searcher { +private: + struct KBlockSetsCompare { + bool operator()(const std::set &a, + const std::set &b) const { + return a.size() > b.size() || (a.size() == b.size() && a > b); + } + }; + + struct VectorsCompare { + bool operator()(const std::vector &a, + const std::vector &b) const { + auto ai = a.begin(), ae = a.end(), bi = b.begin(), be = b.end(); + for (; ai != ae && bi != be; ++ai, ++bi) { + if (*ai != *bi) { + return *ai > *bi; + } + } + return bi != be; + } + }; + + struct BlockLevel { + KFunction *kf; + unsigned sizeOfLevel; + std::vector sizesOfFrameLevels; + unsigned long long maxMultilevel; + BlockLevel(KFunction *kf, unsigned sizeOfLevel, + const std::vector &sizesOfFrameLevels, + unsigned long long maxMultilevel) + : kf(kf), sizeOfLevel(sizeOfLevel), + sizesOfFrameLevels(sizesOfFrameLevels), maxMultilevel(maxMultilevel) { + } + BlockLevel() : kf(nullptr), sizeOfLevel(0), maxMultilevel(0){}; + }; + + using states_ty = std::set; + using kblocks_ty = std::set; + + using ThirdLayer = + std::map>; + using SecondLayer = + std::map, ThirdLayer, VectorsCompare>; + using FirstLayer = std::map>; + using Data = std::map; + + Data data; + std::unordered_map stateToBlockLevel; + std::vector sizes; + RNG &theRNG; + + void clear(ExecutionState &state); + +public: + explicit BlockLevelSearcher(RNG &rng); + ExecutionState &selectState() override; + void update(ExecutionState *current, const StateIterable &addedStates, + const StateIterable &removedStates) override; + bool empty() override; + void printName(llvm::raw_ostream &os) override; +}; + } // namespace klee #endif /* KLEE_SEARCHER_H */ diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index d323180908..ab4b67f3df 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -493,13 +493,12 @@ KFunction *TargetedExecutionManager::tryResolveEntryFunction( return resKf; } -std::map, - TargetedExecutionManager::KFunctionLess> +std::map, KFunctionCompare> TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) { Locations locations = collectAllLocations(paths); LocationToBlocks locToBlocks = prepareAllLocations(kmodule, locations); - std::map, KFunctionLess> whitelists; + std::map, KFunctionCompare> whitelists; for (auto &result : paths.results) { bool isFullyResolved = tryResolveLocations(result, locToBlocks); diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 93ea108a07..e5f72e935b 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -115,17 +115,11 @@ class TargetedExecutionManager { StatesSet localStates; public: - struct KFunctionLess { - bool operator()(const KFunction *a, const KFunction *b) const { - return a->id < b->id; - } - }; - explicit TargetedExecutionManager(CodeGraphInfo &codeGraphInfo_, TargetManager &targetManager_) : codeGraphInfo(codeGraphInfo_), targetManager(targetManager_) {} ~TargetedExecutionManager() = default; - std::map, KFunctionLess> + std::map, KFunctionCompare> prepareTargets(KModule *kmodule, SarifReport paths); void reportFalseNegative(ExecutionState &state, ReachWithError error); diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 59674a84f7..a6cc1fc5da 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -38,6 +38,9 @@ cl::list CoreSearch( clEnumValN(Searcher::BFS, "bfs", "use Breadth First Search (BFS), where scheduling decisions " "are taken at the level of (2-way) forks"), + clEnumValN(Searcher::BlockLevelSearch, "bls", + "use Block Level Search (BLS), where selection " + "between states with same level is is carried out randomly"), clEnumValN(Searcher::RandomState, "random-state", "randomly select a state to explore"), clEnumValN(Searcher::RandomPath, "random-path", @@ -92,7 +95,7 @@ void klee::initializeSearchOptions() { // default values if (CoreSearch.empty()) { CoreSearch.push_back(Searcher::RandomPath); - CoreSearch.push_back(Searcher::NURS_CovNew); + CoreSearch.push_back(Searcher::BlockLevelSearch); } } @@ -119,6 +122,9 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, case Searcher::BFS: searcher = new BFSSearcher(); break; + case Searcher::BlockLevelSearch: + searcher = new BlockLevelSearcher(rng); + break; case Searcher::RandomState: searcher = new RandomSearcher(rng); break; diff --git a/test/Feature/BlockPath.ll b/test/Feature/BlockPath.ll index b46b04e96f..685e942022 100644 --- a/test/Feature/BlockPath.ll +++ b/test/Feature/BlockPath.ll @@ -1,7 +1,7 @@ ; REQUIRES: geq-llvm-12.0 ; RUN: %llvmas %s -o %t1.bc ; RUN: rm -rf %t.klee-out -; RUN: %klee --output-dir=%t.klee-out --libc=klee --write-kpaths %t1.bc +; RUN: %klee --output-dir=%t.klee-out --libc=klee --search=dfs --write-kpaths %t1.bc ; RUN: grep "(path: 0 (main: %0 %5 %6 %8 (abs: %1 %8 %11 %13) %8 %10 %16 %17 %19" %t.klee-out/test000001.kpath ; RUN: grep "(path: 0 (main: %0 %5 %6 %8 (abs: %1 %6 %11 %13) %8 %10 %16 %17 %19" %t.klee-out/test000002.kpath diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c index cd2295c5c6..5fdcfee387 100644 --- a/test/Feature/OvershiftCheck.c +++ b/test/Feature/OvershiftCheck.c @@ -15,12 +15,12 @@ int main() { /* Overshift if y>= sizeof(x) */ klee_make_symbolic(&y, sizeof(y), "shift_amount1"); - // CHECK: OvershiftCheck.c:[[@LINE+1]]: overshift error + // CHECK-DAG: OvershiftCheck.c:[[@LINE+1]]: overshift error result = x << y; /* Overshift is z>= sizeof(x) */ klee_make_symbolic(&z, sizeof(z), "shift_amount2"); - // CHECK: OvershiftCheck.c:[[@LINE+1]]: overshift error + // CHECK-DAG: OvershiftCheck.c:[[@LINE+1]]: overshift error result = x >> z; return 0; diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c index 535efd4f87..5fd47acac5 100644 --- a/test/Feature/consecutive_divide_by_zero.c +++ b/test/Feature/consecutive_divide_by_zero.c @@ -18,11 +18,11 @@ int main() { klee_make_symbolic(&d2, sizeof(d2), "divisor2"); // deliberate division by zero possible - // CHECK: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero + // CHECK-DAG: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero unsigned int result1 = a / d1; // another deliberate division by zero possible - // CHECK: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero + // CHECK-DAG: consecutive_divide_by_zero.c:[[@LINE+1]]: divide by zero unsigned int result2 = b / d2; // CHECK: completed paths = 1 diff --git a/test/Feature/srem.c b/test/Feature/srem.c index a4fec8ca9a..15c4a67efe 100644 --- a/test/Feature/srem.c +++ b/test/Feature/srem.c @@ -16,7 +16,7 @@ int main(int argc, char **argv) { if (y >= 0) { if (y < 2) { // Two test cases generated taking this path, one for y == 0 and y == 1 - // CHECK: srem.c:[[@LINE+1]]: divide by zero + // CHECK-DAG: srem.c:[[@LINE+1]]: divide by zero assert(1 % y == 0); } else { assert(1 % y == 1); @@ -35,7 +35,7 @@ int main(int argc, char **argv) { // should fail for y == 0 and y == +/-1, but succeed for all others // generates one testcase for either y == 1 or y == -1 - // CHECK: srem.c:[[@LINE+1]]: ASSERTION FAIL + // CHECK-DAG: srem.c:[[@LINE+1]]: ASSERTION FAIL assert(-1 % y == -1); // CHECK: KLEE: done: completed paths = 2 diff --git a/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c b/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c index 3a21e7e1ea..536cc816c1 100644 --- a/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c +++ b/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c @@ -11,13 +11,13 @@ int main() { float *ptr; klee_make_symbolic(&ptr, sizeof(ptr), "ptr"); - // CHECK: KLEE: ERROR: {{.*}}runtime/Sanitizer/ubsan/ubsan_handlers.cpp:{{[0-9]+}}: null-pointer-use + // CHECK-DAG: KLEE: ERROR: {{.*}}runtime/Sanitizer/ubsan/ubsan_handlers.cpp:{{[0-9]+}}: null-pointer-use *ptr = 10; int n = klee_range(1, 4, "n"); ptr = (float *)(((char *)ptr) + n); - // CHECK: KLEE: ERROR: {{.*}}runtime/Sanitizer/ubsan/ubsan_handlers.cpp:{{[0-9]+}}: misaligned-pointer-use + // CHECK-DAG: KLEE: ERROR: {{.*}}runtime/Sanitizer/ubsan/ubsan_handlers.cpp:{{[0-9]+}}: misaligned-pointer-use *ptr = 20; return 0; diff --git a/test/Solver/CexCacheValidityCoresCheck.c b/test/Solver/CexCacheValidityCoresCheck.c index 0e48f6f24f..f903e2652c 100644 --- a/test/Solver/CexCacheValidityCoresCheck.c +++ b/test/Solver/CexCacheValidityCoresCheck.c @@ -2,8 +2,8 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t1.klee-out // RUN: rm -rf %t2.klee-out -// RUN: %klee --output-dir=%t1.klee-out --use-guided-search=none --cex-cache-validity-cores=false --solver-backend=z3 %t1.bc -// RUN: %klee --output-dir=%t2.klee-out --use-guided-search=none --cex-cache-validity-cores=true --solver-backend=z3 %t1.bc +// RUN: %klee --output-dir=%t1.klee-out --search=bfs --use-guided-search=none --cex-cache-validity-cores=false --solver-backend=z3 %t1.bc +// RUN: %klee --output-dir=%t2.klee-out --search=bfs --use-guided-search=none --cex-cache-validity-cores=true --solver-backend=z3 %t1.bc // RUN: %klee-stats --print-columns 'QCexCacheHits,SolverQueries' --table-format=csv %t1.klee-out > %t1.stats // RUN: %klee-stats --print-columns 'QCexCacheHits,SolverQueries' --table-format=csv %t2.klee-out > %t2.stats // RUN: FileCheck -check-prefix=CHECK-CACHE-OFF -input-file=%t1.stats %s From de6c1d3bf19ea3d9562935b6fb75e86313bbba9f Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 11 Nov 2023 17:07:27 +0400 Subject: [PATCH 09/11] [chore] Update `kleef` --- scripts/kleef | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/kleef b/scripts/kleef index 35f0e4ac65..5056eba954 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -29,6 +29,7 @@ def klee_options( "--strip-unwanted-calls", # removes llvm.dbg.* instructions, exponentially reduces time on some benchmarks "--delete-dead-loops=false", # without this optimizer removes some code, which decreases coverage "--emit-all-errors", # without this we generate only one test for assertion failures, which decreases coverage + "--external-calls=all", "--mock-all-externals", # this helps for some linux benchmarks, which have unused extern globals. without this flag we will not even start on them. "--external-calls=all", "--use-forked-solver=false", @@ -100,8 +101,9 @@ def klee_options( # "--tc-type=cov", "--only-output-states-covering-new", # Don't generate all test cases "--dump-states-on-halt=true", # Check in case we missed some oncovered instructions - "--search=dfs", + # "--search=dfs", "--search=random-state", + "--search=bls", ] if max_time: max_time = float(max_time) From 83e43d59b90715ae960df3064e923f2186c3de4c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 15 Nov 2023 04:20:28 +0400 Subject: [PATCH 10/11] [fix] Improve BLS --- lib/Core/Searcher.cpp | 2 +- lib/Core/Searcher.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index e3535af48e..b5f9480c06 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -656,7 +656,7 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric { return state.isCycled(maxCycles); } void increaseLimit() final { - maxCycles *= 2ULL; + maxCycles *= 4ULL; klee_message("increased max-cycles to %llu", maxCycles); } }; diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 2be9b1bf53..b7b2d40c2e 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -405,7 +405,7 @@ class BlockLevelSearcher final : public Searcher { using kblocks_ty = std::set; using ThirdLayer = - std::map>; + std::map>; using SecondLayer = std::map, ThirdLayer, VectorsCompare>; using FirstLayer = std::map>; From 9da90e2a571e8cb88d54264023d35fc116048346 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 15 Nov 2023 04:20:47 +0400 Subject: [PATCH 11/11] [chore] Update `kleef` script --- scripts/kleef | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/kleef b/scripts/kleef index 5056eba954..7551985f6f 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -29,7 +29,6 @@ def klee_options( "--strip-unwanted-calls", # removes llvm.dbg.* instructions, exponentially reduces time on some benchmarks "--delete-dead-loops=false", # without this optimizer removes some code, which decreases coverage "--emit-all-errors", # without this we generate only one test for assertion failures, which decreases coverage - "--external-calls=all", "--mock-all-externals", # this helps for some linux benchmarks, which have unused extern globals. without this flag we will not even start on them. "--external-calls=all", "--use-forked-solver=false", @@ -80,6 +79,7 @@ def klee_options( "--dump-states-on-halt=false", # Explicitly do not dump states "--exit-on-error-type=Assert", # Only generate test cases of type assert # "--dump-test-case-type=Assert", # Only dump test cases of type assert + "--search=bls", "--search=dfs", # "--search=nurs:covnew", "--search=random-path","--search=dfs", "--use-batching-search", # "--search=distance","--search=random-path","--use-batching-search",