From 3a69ec398f9567edb4594ba2ae5da65c37fbf464 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Tue, 24 Oct 2023 11:19:41 +0300 Subject: [PATCH 1/5] [chore] Deal with compiler warnings --- include/klee/Expr/AlphaBuilder.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h index f00b324ae7..b56e9563cf 100644 --- a/include/klee/Expr/AlphaBuilder.h +++ b/include/klee/Expr/AlphaBuilder.h @@ -16,7 +16,7 @@ namespace klee { -class AlphaBuilder : public ExprVisitor { +class AlphaBuilder final : public ExprVisitor { public: ExprHashMap> reverseExprMap; ArrayCache::ArrayHashMap reverseAlphaArrayMap; @@ -28,7 +28,8 @@ class AlphaBuilder : public ExprVisitor { const Array *visitArray(const Array *arr); UpdateList visitUpdateList(UpdateList u); - Action visitRead(const ReadExpr &re); + Action visitRead(const ReadExpr &re) override; + using ExprVisitor::visitExpr; public: AlphaBuilder(ArrayCache &_arrayCache); From 89b55688d6378f4a73528edcec06f463277af1d8 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Tue, 24 Oct 2023 13:27:04 +0300 Subject: [PATCH 2/5] [feat] Cover on the fly based on time --- lib/Core/Executor.cpp | 24 ++++++++++++++++-------- lib/Core/Executor.h | 3 +++ test/Feature/CoverOnTheFly.c | 6 ++---- 3 files changed, 21 insertions(+), 12 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index cda2c31aaf..300c71400c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -249,10 +249,10 @@ cl::opt CoverOnTheFly( "(default=false, i.e. one per (error,instruction) pair)"), cl::cat(TestGenCat)); -cl::opt DelayCoverOnTheFly( - "delay-cover-on-the-fly", cl::init(10000), - cl::desc("Start on the fly tests generation after this many instructions " - "(default=10000)"), +cl::opt DelayCoverOnTheFly( + "delay-cover-on-the-fly", cl::init("0s"), + cl::desc("Start on the fly tests generation after the specified duration. " + "Set to 0s to disable (default=0s)"), cl::cat(TestGenCat)); cl::opt UninitMemoryTestMultiplier( @@ -487,8 +487,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, targetedExecutionManager( new TargetedExecutionManager(*codeGraphInfo, *targetManager)), replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), - inhibitForking(false), haltExecution(HaltExecution::NotHalt), - ivcEnabled(false), debugLogBuffer(debugBufferString) { + inhibitForking(false), coverOnTheFly(false), + haltExecution(HaltExecution::NotHalt), ivcEnabled(false), + debugLogBuffer(debugBufferString) { const time::Span maxTime{MaxTime}; if (maxTime) timers.add(std::make_unique(maxTime, [&] { @@ -496,6 +497,13 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, setHaltExecution(HaltExecution::MaxTime); })); + if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance) { + const time::Span delayTime{DelayCoverOnTheFly}; + if (delayTime) + timers.add( + std::make_unique(delayTime, [&] { coverOnTheFly = true; })); + } + coreSolverTimeout = time::Span{MaxCoreSolverTime}; if (coreSolverTimeout) UseForkedCoreSolver = true; @@ -4381,8 +4389,8 @@ static std::string terminationTypeFileExtension(StateTerminationType type) { void Executor::executeStep(ExecutionState &state) { KFunction *initKF = state.initPC->parent->parent; - if (CoverOnTheFly && guidanceKind != GuidanceKind::ErrorGuidance && - stats::instructions > DelayCoverOnTheFly && shouldWriteTest(state)) { + + if (coverOnTheFly && shouldWriteTest(state)) { state.clearCoveredNew(); interpreterHandler->processTestCase( state, nullptr, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 5a4f8bc554..a1a1e3c380 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -208,6 +208,9 @@ class Executor : public Interpreter { /// Disables forking, set by client. \see setInhibitForking() bool inhibitForking; + /// Should it generate test cases for each new covered block or branch + bool coverOnTheFly; + /// Signals the executor to halt execution at the next instruction /// step. HaltExecution::Reason haltExecution = HaltExecution::NotHalt; diff --git a/test/Feature/CoverOnTheFly.c b/test/Feature/CoverOnTheFly.c index 85c0ead78c..37e4381614 100644 --- a/test/Feature/CoverOnTheFly.c +++ b/test/Feature/CoverOnTheFly.c @@ -2,11 +2,10 @@ // REQUIRES: not-asan // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --delay-cover-on-the-fly=500 --dump-states-on-halt=false --cover-on-the-fly --search=bfs --use-guided-search=none --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s +// RUN: %klee --only-output-states-covering-new --max-instructions=2000 --timer-interval=1ms --delay-cover-on-the-fly=1ms --dump-states-on-halt=false --cover-on-the-fly --search=bfs --use-guided-search=none --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s #include "klee/klee.h" -#define a (2) int main() { int res = 0; for (;;) { @@ -31,5 +30,4 @@ int main() { } } -// CHECK: KLEE: done: completed paths = 0 -// CHECK: KLEE: done: generated tests = 5 +// CHECK-NOT: KLEE: done: generated tests = 0 From 042a4b64b98b54b5340d97796075d9c8462a14f7 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Tue, 24 Oct 2023 13:28:09 +0300 Subject: [PATCH 3/5] [fix] rewriting ordering for terms with equal height --- include/klee/Expr/Expr.h | 4 ++-- lib/Expr/Constraints.cpp | 32 ++++++++++++++------------------ lib/Expr/Expr.cpp | 10 ++++++---- 3 files changed, 22 insertions(+), 24 deletions(-) diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index df98d892f9..4646b1a3c8 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -304,8 +304,8 @@ class Expr { std::string toString() const; /// Returns the pre-computed hash of the current expression - virtual unsigned hash() const { return hashValue; } - virtual unsigned height() const { return heightValue; } + unsigned hash() const { return hashValue; } + unsigned height() const { return heightValue; } /// (Re)computes the hash of the current expression. /// Returns the hash value. diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 241c1a329b..ae00a3303c 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -423,27 +423,23 @@ Simplificator::simplifyExpr(const constraints_ty &constraints, for (auto &constraint : constraints) { if (const EqExpr *ee = dyn_cast(constraint)) { - ref left = ee->left; - ref right = ee->right; - if (right->height() < left->height()) { - left = ee->right; - right = ee->left; - } - if (isa(ee->left)) { - equalities.insert(std::make_pair(ee->right, ee->left)); - equalitiesParents.insert({ee->right, constraint}); - } else { - equalities.insert(std::make_pair(constraint, Expr::createTrue())); - equalities.insert(std::make_pair(right, left)); - equalitiesParents.insert({constraint, constraint}); - equalitiesParents.insert({right, constraint}); + ref small = ee->left; + ref big = ee->right; + if (!isa(small)) { + auto hr = big->height(), hl = small->height(); + if (hr < hl || (hr == hl && big < small)) + std::swap(small, big); + equalities.emplace(constraint, Expr::createTrue()); + equalitiesParents.emplace(constraint, constraint); } + equalities.emplace(big, small); + equalitiesParents.emplace(big, constraint); } else { - equalities.insert(std::make_pair(constraint, Expr::createTrue())); - equalitiesParents.insert({constraint, constraint}); + equalities.emplace(constraint, Expr::createTrue()); + equalitiesParents.emplace(constraint, constraint); if (const NotExpr *ne = dyn_cast(constraint)) { - equalities.insert(std::make_pair(ne->expr, Expr::createFalse())); - equalitiesParents.insert({ne->expr, constraint}); + equalities.emplace(ne->expr, Expr::createFalse()); + equalitiesParents.emplace(ne->expr, constraint); } } } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index c889af5ed4..4f26cb1aaa 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -153,11 +153,13 @@ int Expr::compare(const Expr &b, ExprEquivSet &equivs) const { return 0; Kind ak = getKind(), bk = b.getKind(); - if (ak != bk) - return (ak < bk) ? -1 : 1; + int kc = (ak > bk) - (ak < bk); + if (kc) + return kc; - if (hashValue != b.hashValue) - return (hashValue < b.hashValue) ? -1 : 1; + int hc = (hashValue > b.hashValue) - (hashValue < b.hashValue); + if (hc) + return hc; if (int res = compareContents(b)) return res; From 4f15289be704dd616c4921bca1b6debded91e367 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 25 Oct 2023 02:03:49 +0400 Subject: [PATCH 4/5] [fix] Update test --- test/Feature/SymbolicSizes/IntArray.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/Feature/SymbolicSizes/IntArray.c b/test/Feature/SymbolicSizes/IntArray.c index 46edaeb836..48ea30e48e 100644 --- a/test/Feature/SymbolicSizes/IntArray.c +++ b/test/Feature/SymbolicSizes/IntArray.c @@ -1,5 +1,5 @@ -// REQUIRES: not-darwin -// Disabling darwin because it overflows stack on CI +// REQUIRES: not-darwin, not-metasmt +// Disabling darwin and metasmt because test has flaky behaviour on CI // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --use-sym-size-alloc --use-sym-size-li --min-number-elements-li=1 --skip-not-lazy-initialized %t1.bc 2>&1 | FileCheck %s From fef825f0a65741d372876b482165c5af6eb5ec99 Mon Sep 17 00:00:00 2001 From: Yurii Kostyukov Date: Wed, 25 Oct 2023 11:10:49 +0300 Subject: [PATCH 5/5] [feat] Removed unwanted calls pass --- lib/Module/CMakeLists.txt | 1 + lib/Module/CallRemover.cpp | 36 ++++++++++++++++++++++++++++++++++++ lib/Module/CallSplitter.cpp | 8 ++++---- lib/Module/KModule.cpp | 7 +++++++ lib/Module/Optimize.cpp | 7 ------- lib/Module/Passes.h | 8 ++++++++ 6 files changed, 56 insertions(+), 11 deletions(-) create mode 100644 lib/Module/CallRemover.cpp diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt index 42ef35556b..bca27a10ea 100644 --- a/lib/Module/CMakeLists.txt +++ b/lib/Module/CMakeLists.txt @@ -8,6 +8,7 @@ #===------------------------------------------------------------------------===# set(KLEE_MODULE_COMPONENT_SRCS CallSplitter.cpp + CallRemover.cpp Checks.cpp CodeGraphInfo.cpp FunctionAlias.cpp diff --git a/lib/Module/CallRemover.cpp b/lib/Module/CallRemover.cpp new file mode 100644 index 0000000000..d2854ebd47 --- /dev/null +++ b/lib/Module/CallRemover.cpp @@ -0,0 +1,36 @@ +//===-- CallRemover.cpp----------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "Passes.h" +#include + +namespace klee { + +using namespace llvm; + +char CallRemover::ID; + +bool CallRemover::runOnModule(llvm::Module &M) { + std::vector badFuncs = {"llvm.dbg.declare", "llvm.dbg.label"}; + + for (const auto &f : badFuncs) { + auto Declare = M.getFunction(f); + if (!Declare) + continue; + while (!Declare->use_empty()) { + auto CI = cast(Declare->user_back()); + assert(CI->use_empty() && "deleted function must have void result"); + CI->eraseFromParent(); + } + Declare->eraseFromParent(); + } + + return true; +} +} // namespace klee diff --git a/lib/Module/CallSplitter.cpp b/lib/Module/CallSplitter.cpp index 4c4a71c4f3..a90e17516d 100644 --- a/lib/Module/CallSplitter.cpp +++ b/lib/Module/CallSplitter.cpp @@ -1,5 +1,4 @@ -//===-- CallSplitter.cpp -//-------------------------------------------------------===// +//===-- CallSplitter.cpp --------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -46,8 +45,9 @@ bool CallSplitter::runOnFunction(Function &F) { if (callInst != firstInst) { fbb = fbb->splitBasicBlock(callInst); } - if (isa(afterCallInst) && - cast(afterCallInst)->isUnconditional()) { + if ((isa(afterCallInst) && + cast(afterCallInst)->isUnconditional()) || + isa(afterCallInst)) { break; } fbb = fbb->splitBasicBlock(afterCallInst); diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 343974b472..ce09edfcc2 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -117,6 +117,11 @@ cl::opt cl::desc("Split each call in own basic block (default=true)"), cl::init(true), cl::cat(klee::ModuleCat)); +static cl::opt + StripUnwantedCalls("strip-unwanted-calls", + cl::desc("Strip all unwanted calls (llvm.dbg.* stuff)"), + cl::init(false), cl::cat(klee::ModuleCat)); + cl::opt SplitReturns( "split-returns", cl::desc("Split each return in own basic block (default=true)"), @@ -332,6 +337,8 @@ void KModule::optimiseAndPrepare( pm3.add(createScalarizerPass()); pm3.add(new PhiCleanerPass()); pm3.add(new FunctionAliasPass()); + if (StripUnwantedCalls) + pm3.add(new CallRemover()); if (SplitCalls) { pm3.add(new CallSplitter()); } diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index 77e11b2e2d..cda430bd96 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -72,11 +72,6 @@ static cl::opt cl::desc("Strip debugger symbol info from executable"), cl::init(false), cl::cat(klee::ModuleCat)); -static cl::opt - StripDebugDeclare("strip-debug-declare", - cl::desc("Strip all llvm.dbg.declare intrinsics"), - cl::init(true), cl::cat(klee::ModuleCat)); - static cl::alias A1("S", cl::desc("Alias for --strip-debug"), cl::aliasopt(StripDebug)); @@ -103,8 +98,6 @@ static void AddStandardCompilePasses(legacy::PassManager &PM) { // If the -strip-debug command line option was specified, do it. if (StripDebug) addPass(PM, createStripSymbolsPass(true)); - if (StripDebugDeclare) - addPass(PM, createStripDebugDeclarePass()); addPass(PM, createCFGSimplificationPass()); // Clean up disgusting code addPass(PM, createPromoteMemoryToRegisterPass()); // Kill useless allocas diff --git a/lib/Module/Passes.h b/lib/Module/Passes.h index 76499428df..01983e0b85 100644 --- a/lib/Module/Passes.h +++ b/lib/Module/Passes.h @@ -206,6 +206,14 @@ class CallSplitter : public llvm::FunctionPass { bool runOnFunction(llvm::Function &F) override; }; +/// Remove unwanted calls +class CallRemover : public llvm::ModulePass { +public: + static char ID; + CallRemover() : llvm::ModulePass(ID) {} + bool runOnModule(llvm::Module &M) override; +}; + class ReturnSplitter : public llvm::FunctionPass { public: static char ID;