From a35ad1d9e19ba4048f7d45fe0df3dc1ecafac0a4 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sun, 12 Nov 2023 15:26:51 +0400 Subject: [PATCH 1/7] [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 2/7] [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 3/7] [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 4/7] [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 5/7] [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 6/7] [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 7/7] [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);