From 50fd194ca1f2235a2741dc9b095ab1ce1bc6360a Mon Sep 17 00:00:00 2001 From: dim8art Date: Wed, 11 Dec 2024 17:04:12 +0300 Subject: [PATCH] [feat] Add options to store and rerun execution states during execution --- include/klee/ADT/SeedFromFile.h | 19 + include/klee/Core/BranchTypes.h | 3 +- include/klee/Core/Interpreter.h | 15 +- include/klee/Core/TerminationTypes.h | 1 + lib/ADT/CMakeLists.txt | 2 + lib/ADT/SeedFromFile.cpp | 14 + lib/Basic/KTest.cpp | 10 + lib/Core/ExecutionState.cpp | 6 +- lib/Core/ExecutionState.h | 7 + lib/Core/Executor.cpp | 850 ++++++++---------- lib/Core/Executor.h | 79 +- lib/Core/ObjectManager.cpp | 20 +- lib/Core/ObjectManager.h | 4 + lib/Core/Searcher.cpp | 101 +++ lib/Core/Searcher.h | 25 + lib/Core/SeedInfo.cpp | 115 +-- lib/Core/SeedInfo.h | 49 +- lib/Core/SeedMap.cpp | 21 +- lib/Core/SeedMap.h | 23 +- lib/Core/TargetManager.cpp | 4 + lib/Core/TargetManager.h | 13 + lib/Core/UserSearcher.cpp | 12 +- scripts/kleef | 25 +- test/Coverage/ReplayOutDir.c | 13 - test/Feature/MemoryLimit.c | 3 +- test/Feature/NamedSeedMatching.c | 2 +- test/Feature/ReplayPath.c | 46 - test/Feature/TestRunForever.c | 21 + test/Feature/TestSeedingSolver.c | 30 + test/Runtime/POSIX/SeedAndFail.c | 4 +- .../2018-05-17-replay-short-names.c | 11 - tools/klee/main.cpp | 191 ++-- 32 files changed, 885 insertions(+), 854 deletions(-) create mode 100644 include/klee/ADT/SeedFromFile.h create mode 100644 lib/ADT/SeedFromFile.cpp delete mode 100644 test/Coverage/ReplayOutDir.c delete mode 100644 test/Feature/ReplayPath.c create mode 100644 test/Feature/TestRunForever.c create mode 100644 test/Feature/TestSeedingSolver.c delete mode 100644 test/regression/2018-05-17-replay-short-names.c diff --git a/include/klee/ADT/SeedFromFile.h b/include/klee/ADT/SeedFromFile.h new file mode 100644 index 0000000000..e426596850 --- /dev/null +++ b/include/klee/ADT/SeedFromFile.h @@ -0,0 +1,19 @@ +#ifndef KLEE_SEED_FROM_FILE_H +#include + +class KTest; + +namespace klee { + +class SeedFromFile { +public: + KTest *ktest; + unsigned maxInstructions; + + SeedFromFile() {} + SeedFromFile(std::string _path); +}; + +} // namespace klee +#define KLEE_SEED_FROM_FILE_H +#endif diff --git a/include/klee/Core/BranchTypes.h b/include/klee/Core/BranchTypes.h index 1c8af978c4..6c3ebc39fc 100644 --- a/include/klee/Core/BranchTypes.h +++ b/include/klee/Core/BranchTypes.h @@ -25,7 +25,8 @@ BTYPE(Realloc, 8U) \ BTYPE(Free, 9U) \ BTYPE(GetVal, 10U) \ - BMARK(END, 10U) + BTYPE(InitialBranch, 11U) \ + BMARK(END, 11U) /// \endcond /** @enum BranchType diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index aceb78dcfc..dc08cf6788 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -10,6 +10,7 @@ #define KLEE_INTERPRETER_H #include "TerminationTypes.h" +#include "klee/ADT/SeedFromFile.h" #include "klee/Module/Annotation.h" #include "klee/Module/SarifReport.h" @@ -200,18 +201,9 @@ class Interpreter { // to record the symbolic path (as a stream of '0' and '1' bytes). virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0; - // supply a test case to replay from. this can be used to drive the - // interpretation down a user specified path. use null to reset. - virtual void setReplayKTest(const struct KTest *out) = 0; - - // supply a list of branch decisions specifying which direction to - // take on forks. this can be used to drive the interpretation down - // a user specified path. use null to reset. - virtual void setReplayPath(const std::vector *path) = 0; - // supply a set of symbolic bindings that will be used as "seeds" // for the search. use null to reset. - virtual void useSeeds(const std::vector *seeds) = 0; + virtual void useSeeds(std::vector seeds) = 0; virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv, char **envp) = 0; @@ -237,6 +229,9 @@ class Interpreter { virtual void getConstraintLog(const ExecutionState &state, std::string &res, LogType logFormat = STP) = 0; + virtual void getSteppedInstructions(const ExecutionState &state, + unsigned &res) = 0; + virtual bool getSymbolicSolution(const ExecutionState &state, KTest &res) = 0; virtual void addSARIFReport(const ExecutionState &state) = 0; diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 6563b9736c..fc99b15959 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -101,6 +101,7 @@ enum Reason { ErrorOnWhichShouldExit, Interrupt, MaxDepth, + MaxMemory, MaxStackFrames, MaxSolverTime, Unspecified diff --git a/lib/ADT/CMakeLists.txt b/lib/ADT/CMakeLists.txt index f013a88af4..fd9967d4cb 100644 --- a/lib/ADT/CMakeLists.txt +++ b/lib/ADT/CMakeLists.txt @@ -7,7 +7,9 @@ # #===------------------------------------------------------------------------===# add_library(kleeADT + SeedFromFile.cpp SparseStorage.cpp + SeedFromFile.cpp ) llvm_config(kleeADT "${USE_LLVM_SHARED}" support) diff --git a/lib/ADT/SeedFromFile.cpp b/lib/ADT/SeedFromFile.cpp new file mode 100644 index 0000000000..120137754f --- /dev/null +++ b/lib/ADT/SeedFromFile.cpp @@ -0,0 +1,14 @@ +#include "klee/ADT/SeedFromFile.h" +#include "klee/ADT/KTest.h" + +#include + +using namespace klee; + +SeedFromFile::SeedFromFile(std::string _path) + : ktest(kTest_fromFile((_path + "ktest").c_str())) { + std::ifstream seedInfoStream(_path + "seedinfo"); + if (seedInfoStream.good()) { + seedInfoStream >> maxInstructions; + } +} diff --git a/lib/Basic/KTest.cpp b/lib/Basic/KTest.cpp index c9556cf8df..dd39ea083a 100644 --- a/lib/Basic/KTest.cpp +++ b/lib/Basic/KTest.cpp @@ -295,3 +295,13 @@ void kTest_free(KTest *bo) { free(bo->objects); free(bo); } + +unsigned getKTestMemoryUsage(KTest *ktest) { + size_t size = 0; + for (unsigned i = 0; i < ktest->numObjects; i++) { + size += std::strlen(ktest->objects[i].name) * sizeof(char); + size += ktest->objects[i].numBytes * sizeof(unsigned char); + size += ktest->objects[i].numPointers * sizeof(Pointer); + } + return size; +} diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 6c56132a82..bf0ea6c648 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -170,9 +170,9 @@ ExecutionState::ExecutionState(const ExecutionState &state) coveredNew(state.coveredNew), coveredNewError(state.coveredNewError), forkDisabled(state.forkDisabled), returnValue(state.returnValue), gepExprBases(state.gepExprBases), multiplexKF(state.multiplexKF), - prevTargets_(state.prevTargets_), targets_(state.targets_), - prevHistory_(state.prevHistory_), history_(state.history_), - isTargeted_(state.isTargeted_) { + isSeeded(state.isSeeded), prevTargets_(state.prevTargets_), + targets_(state.targets_), prevHistory_(state.prevHistory_), + history_(state.history_), isTargeted_(state.isTargeted_) { queryMetaData.id = state.id; } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index dc0e480171..2dcac20df8 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -420,6 +420,8 @@ class ExecutionState { // Temp: to know which multiplex path this state has taken KFunction *multiplexKF = nullptr; + bool isSeeded = false; + private: PersistentSet> prevTargets_; PersistentSet> targets_; @@ -514,6 +516,11 @@ class ExecutionState { inline void setTargeted(bool targeted) { isTargeted_ = targeted; } + inline void setTargets(const PersistentSet> &targets) { + targets_ = targets; + areTargetsChanged_ = true; + } + inline void setTargets(const TargetHashSet &targets) { targets_ = PersistentSet>(); for (auto target : targets) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2fc92b60c5..9cfb8fd5ec 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -95,6 +95,7 @@ #endif #include "llvm/Support/CommandLine.h" #include "llvm/Support/ErrorHandling.h" +#include "llvm/Support/FileSystem.h" #include "llvm/Support/Path.h" #include "llvm/Support/Process.h" #include "llvm/Support/TypeSize.h" @@ -159,17 +160,6 @@ cl::opt "and return null (default=false)"), cl::cat(ExecCat)); -cl::opt OSCopySizeMemoryCheckThreshold( - "os-copy-size-mem-check-threshold", cl::init(30000), - cl::desc("Check memory usage when this amount of bytes dense OS is copied"), - cl::cat(ExecCat)); - -cl::opt StackCopySizeMemoryCheckThreshold( - "stack-copy-size-mem-check-threshold", cl::init(30000), - cl::desc("Check memory usage when state with stack this big (in bytes) is " - "copied"), - cl::cat(ExecCat)); - namespace { /*** Lazy initialization options ***/ @@ -228,6 +218,15 @@ cl::opt DumpStatesOnHalt( clEnumValN(HaltExecution::Reason::Unspecified, "all", "Dump test cases for all active states on exit (default)")), cl::cat(TestGenCat)); + +cl::opt + StoreEarlyStates("store-early-states", + cl::desc("Store states when out of memory and explore " + "them later (default=false)"), + cl::init(false), cl::cat(SeedingCat)); + +extern llvm::cl::opt UseSeededSearch; + } // namespace klee namespace { @@ -346,39 +345,19 @@ cl::opt ExternalCallWarnings( /*** Seeding options ***/ +cl::opt UploadPercentage( + "upload-percentage", + cl::desc( + "Percentage of seeds stored in executor, that are uploaded every time" + "seeding begins, 0 = disabled (default=100)"), + cl::init(100), cl::cat(SeedingCat)); + cl::opt AlwaysOutputSeeds( "always-output-seeds", cl::init(true), cl::desc( "Dump test cases even if they are driven by seeds only (default=true)"), cl::cat(SeedingCat)); -cl::opt OnlyReplaySeeds( - "only-replay-seeds", cl::init(false), - cl::desc("Discard states that do not have a seed (default=false)."), - cl::cat(SeedingCat)); - -cl::opt OnlySeed("only-seed", cl::init(false), - cl::desc("Stop execution after seeding is done without " - "doing regular search (default=false)."), - cl::cat(SeedingCat)); - -cl::opt - AllowSeedExtension("allow-seed-extension", cl::init(false), - cl::desc("Allow extra (unbound) values to become " - "symbolic during seeding (default=false)."), - cl::cat(SeedingCat)); - -cl::opt ZeroSeedExtension( - "zero-seed-extension", cl::init(false), - cl::desc( - "Use zero-filled objects if matching seed not found (default=false)"), - cl::cat(SeedingCat)); - -cl::opt AllowSeedTruncation( - "allow-seed-truncation", cl::init(false), - cl::desc("Allow smaller buffers than in seeds (default=false)."), - cl::cat(SeedingCat)); - cl::opt NamedSeedMatching( "named-seed-matching", cl::init(false), cl::desc("Use names to match symbolic objects to inputs (default=false)."), @@ -389,6 +368,7 @@ cl::opt cl::desc("Amount of time to dedicate to seeds, before normal " "search (default=0s (off))"), cl::cat(SeedingCat)); +/***/ /*** Debugging options ***/ @@ -504,13 +484,13 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, *targetCalculator)), targetedExecutionManager( new TargetedExecutionManager(*codeGraphInfo, *targetManager)), - replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), - inhibitForking(false), coverOnTheFly(false), + atMemoryLimit(false), inhibitForking(false), coverOnTheFly(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), debugLogBuffer(debugBufferString), sarifReport({}) { objectManager = std::make_unique(); seedMap = std::make_unique(); + storedSeeds = std::make_unique>(); objectManager->addSubscriber(seedMap.get()); // Add first entry for single run @@ -1148,6 +1128,9 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { bool Executor::branchingPermitted(ExecutionState &state, unsigned N) { assert(N); + if (state.isSeeded) { + return true; + } if ((MaxMemoryInhibit && atMemoryLimit) || state.forkDisabled || inhibitForking || (MaxForks != ~0u && stats::forks >= MaxForks)) { @@ -1201,21 +1184,17 @@ void Executor::branch(ExecutionState &state, } } - // If necessary redistribute seeds to match conditions, killing - // states if necessary due to OnlyReplaySeeds (inefficient but - // simple). - - std::map>::iterator it = - seedMap->find(&state); - if (it != seedMap->end()) { - std::vector seeds = it->second; + if (state.isSeeded) { + std::map::iterator it = seedMap->find(&state); + assert(it != seedMap->end()); + assert(!it->second.empty()); + seeds_ty seeds = it->second; seedMap->erase(it); - + objectManager->unseed(it->first); // Assume each seed only satisfies one condition (necessarily true // when conditions are mutually exclusive and their conjunction is // a tautology). - for (std::vector::iterator siit = seeds.begin(), - siie = seeds.end(); + for (seeds_ty::iterator siit = seeds.begin(), siie = seeds.end(); siit != siie; ++siit) { unsigned i; for (i = 0; i < N; ++i) { @@ -1235,18 +1214,8 @@ void Executor::branch(ExecutionState &state, i = theRNG.getInt32() % N; // Extra check in case we're replaying seeds with a max-fork - if (result[i]) + if (result[i]) { seedMap->at(result[i]).push_back(*siit); - } - - if (OnlyReplaySeeds) { - for (unsigned i = 0; i < N; ++i) { - if (result[i] && !seedMap->count(result[i])) { - terminateStateEarlyAlgorithm(*result[i], - "Unseeded path during replay", - StateTerminationType::Replay); - result[i] = nullptr; - } } } } @@ -1350,46 +1319,76 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, KBlock *ifTrueBlock, KBlock *ifFalseBlock, BranchType reason) { bool isInternal = ifTrueBlock == ifFalseBlock; - std::map>::iterator it = - seedMap->find(¤t); - bool isSeeding = it != seedMap->end(); - - if (!isSeeding) - condition = maxStaticPctChecks(current, condition); - + PartialValidity res = PartialValidity::None; + bool isSeeding = current.isSeeded; + seeds_ty trueSeeds; + seeds_ty falseSeeds; time::Span timeout = coreSolverTimeout; - if (isSeeding) - timeout *= static_cast(it->second.size()); - solver->setTimeout(timeout); - bool shouldCheckTrueBlock = true, shouldCheckFalseBlock = true; + if (!isInternal) { shouldCheckTrueBlock = canReachSomeTargetFromBlock(current, ifTrueBlock); shouldCheckFalseBlock = canReachSomeTargetFromBlock(current, ifFalseBlock); } - PartialValidity res = PartialValidity::None; - bool terminateEverything = false, success = true; - if (!shouldCheckTrueBlock) { - bool mayBeFalse = false; - if (shouldCheckFalseBlock) { - // only solver->check-sat(!condition) - success = solver->mayBeFalse(current.constraints.cs(), condition, - mayBeFalse, current.queryMetaData); - } - if (!success || !mayBeFalse) - terminateEverything = true; - else - res = PartialValidity::MayBeFalse; - } else if (!shouldCheckFalseBlock) { - // only solver->check-sat(condition) - bool mayBeTrue; - success = solver->mayBeTrue(current.constraints.cs(), condition, mayBeTrue, - current.queryMetaData); - if (!success || !mayBeTrue) - terminateEverything = true; - else + + if (isSeeding) { + std::map::iterator it = seedMap->find(¤t); + assert(it != seedMap->end()); + assert(!it->second.empty()); + timeout *= static_cast(it->second.size()); + for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end(); + siit != siie; ++siit) { + ref result; + bool success = solver->getValue(current.constraints.cs(), + siit->assignment.evaluate(condition), + result, current.queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); + (void)success; + if (result->isTrue()) { + trueSeeds.push_back(*siit); + } else if (result->isFalse()) { + falseSeeds.push_back(*siit); + } + } + if (!trueSeeds.empty() && falseSeeds.empty()) { res = PartialValidity::MayBeTrue; + } else if (trueSeeds.empty() && !falseSeeds.empty()) { + res = PartialValidity::MayBeFalse; + } else if (!trueSeeds.empty() && !falseSeeds.empty()) { + res = PValidity::TrueOrFalse; + } + } + + solver->setTimeout(timeout); + bool terminateEverything = false, success = true; + + if (res == PartialValidity::None) { + success = true; + condition = maxStaticPctChecks(current, condition); + + if (!shouldCheckTrueBlock) { + bool mayBeFalse = false; + if (shouldCheckFalseBlock) { + // only solver->check-sat(!condition) + success = solver->mayBeFalse(current.constraints.cs(), condition, + mayBeFalse, current.queryMetaData); + } + if (!success || !mayBeFalse) + terminateEverything = true; + else + res = PartialValidity::MayBeFalse; + } else if (!shouldCheckFalseBlock) { + // only solver->check-sat(condition) + bool mayBeTrue; + success = solver->mayBeTrue(current.constraints.cs(), condition, + mayBeTrue, current.queryMetaData); + if (!success || !mayBeTrue) + terminateEverything = true; + else + res = PartialValidity::MayBeTrue; + } } + if (terminateEverything) { current.pc = current.prevPC; terminateStateEarlyAlgorithm(current, "State missed all it's targets.", @@ -1409,70 +1408,15 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, return StatePair(nullptr, nullptr); } - if (!isSeeding) { - if (replayPath && !isInternal) { - assert(replayPosition < replayPath->size() && - "ran out of branches in replay path mode"); - bool branch = (*replayPath)[replayPosition++]; - - if (res == PValidity::MustBeTrue) { - assert(branch && "hit invalid branch in replay path mode"); - } else if (res == PValidity::MustBeFalse) { - assert(!branch && "hit invalid branch in replay path mode"); - } else { - // add constraints - if (branch) { - res = PValidity::MustBeTrue; - addConstraint(current, condition); - } else { - res = PValidity::MustBeFalse; - addConstraint(current, Expr::createIsZero(condition)); - } - } - } else if (res == PValidity::TrueOrFalse) { - assert(!replayKTest && "in replay mode, only one branch can be true."); - - if (!branchingPermitted(current, 2)) { - TimerStatIncrementer timer(stats::forkTime); - if (theRNG.getBool()) { - res = PValidity::MayBeTrue; - } else { - res = PValidity::MayBeFalse; - } - ++stats::inhibitedForks; - } - } - } - - // Fix branch in only-replay-seed mode, if we don't have both true - // and false seeds. - if (isSeeding && (current.forkDisabled || OnlyReplaySeeds) && - res == PValidity::TrueOrFalse) { - bool trueSeed = false, falseSeed = false; - // Is seed extension still ok here? - for (std::vector::iterator siit = it->second.begin(), - siie = it->second.end(); - siit != siie; ++siit) { - ref res; - bool success = solver->getValue(current.constraints.cs(), - siit->assignment.evaluate(condition), res, - current.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res->isTrue()) { - trueSeed = true; + if (res == PValidity::TrueOrFalse) { + if (!branchingPermitted(current, 2)) { + TimerStatIncrementer timer(stats::forkTime); + if (theRNG.getBool()) { + res = PValidity::MayBeTrue; } else { - falseSeed = true; + res = PValidity::MayBeFalse; } - if (trueSeed && falseSeed) - break; - } - if (!(trueSeed && falseSeed)) { - assert(trueSeed || falseSeed); - - res = trueSeed ? PValidity::MustBeTrue : PValidity::MustBeFalse; - addConstraint(current, - trueSeed ? condition : Expr::createIsZero(condition)); + ++stats::inhibitedForks; } } @@ -1493,7 +1437,9 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, if (res == PValidity::MayBeTrue) { addConstraint(current, condition); } - + if (isSeeding) { + seedMap->at(¤t) = trueSeeds; + } return StatePair(¤t, nullptr); } else if (res == PValidity::MustBeFalse || res == PValidity::MayBeFalse) { if (!isInternal) { @@ -1505,7 +1451,9 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, if (res == PValidity::MayBeFalse) { addConstraint(current, Expr::createIsZero(condition)); } - + if (isSeeding) { + seedMap->at(¤t) = falseSeeds; + } return StatePair(nullptr, ¤t); } else { // When does PValidity::None happen? @@ -1517,42 +1465,10 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, falseState = objectManager->branchState(trueState, reason); - if (it != seedMap->end()) { - std::vector seeds = it->second; - it->second.clear(); - std::vector &trueSeeds = seedMap->at(trueState); - std::vector &falseSeeds = seedMap->at(falseState); - for (std::vector::iterator siit = seeds.begin(), - siie = seeds.end(); - siit != siie; ++siit) { - ref res; - bool success = solver->getValue(current.constraints.cs(), - siit->assignment.evaluate(condition), - res, current.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res->isTrue()) { - trueSeeds.push_back(*siit); - } else { - falseSeeds.push_back(*siit); - } - } - - bool swapInfo = false; - if (trueSeeds.empty()) { - if (¤t == trueState) - swapInfo = true; - seedMap->erase(trueState); - } - if (falseSeeds.empty()) { - if (¤t == falseState) - swapInfo = true; - seedMap->erase(falseState); - } - if (swapInfo) { - std::swap(trueState->coveredNew, falseState->coveredNew); - std::swap(trueState->coveredLines, falseState->coveredLines); - } + bool swapInfo = false; + if (swapInfo) { + std::swap(trueState->coveredNew, falseState->coveredNew); + std::swap(trueState->coveredLines, falseState->coveredLines); } if (pathWriter) { @@ -1586,6 +1502,11 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, return StatePair(nullptr, nullptr); } + if (isSeeding) { + seedMap->at(trueState) = trueSeeds; + seedMap->at(falseState) = falseSeeds; + } + return StatePair(trueState, falseState); } } @@ -1605,31 +1526,6 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { return; } - // Check to see if this constraint violates seeds. - std::map>::iterator it = - seedMap->find(&state); - if (it != seedMap->end()) { - bool warn = false; - for (std::vector::iterator siit = it->second.begin(), - siie = it->second.end(); - siit != siie; ++siit) { - bool res; - solver->setTimeout(coreSolverTimeout); - bool success = solver->mustBeFalse(state.constraints.cs(), - siit->assignment.evaluate(condition), - res, state.queryMetaData); - solver->setTimeout(time::Span()); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res) { - siit->patchSeed(state, condition, solver.get()); - warn = true; - } - } - if (warn) - klee_warning("seeds patched for violating constraint"); - } - state.addConstraint(condition); if (ivcEnabled) @@ -1699,12 +1595,10 @@ ref Executor::toConstant(ExecutionState &state, ref e, if (ConstantExpr *CE = dyn_cast(e)) return CE; - ref value = getValueFromSeeds(state, e); - if (!value) { - [[maybe_unused]] bool success = - solver->getValue(state.constraints.cs(), e, value, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - } + ref value; + [[maybe_unused]] bool success = + solver->getValue(state.constraints.cs(), e, value, state.queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); std::string str; llvm::raw_string_ostream os(str); @@ -1720,21 +1614,6 @@ ref Executor::toConstant(ExecutionState &state, ref e, return value; } -ref Executor::getValueFromSeeds(ExecutionState &state, - ref e) { - auto found = seedMap->find(&state); - if (found == seedMap->end()) - return nullptr; - - auto seeds = found->second; - for (auto const &seed : seeds) { - auto value = seed.assignment.evaluate(e); - if (isa(value)) - return value; - } - return nullptr; -} - ref Executor::toConstantPointer(ExecutionState &state, ref e, const char *reason) { @@ -1767,10 +1646,7 @@ Executor::toConstantPointer(ExecutionState &state, ref e, void Executor::executeGetValue(ExecutionState &state, ref e, KInstruction *target) { e = Simplificator::simplifyExpr(state.constraints.cs(), e).simplified; - std::map>::iterator it = - seedMap->find(&state); - if (it == seedMap->end() || isa(e) || - isa(e)) { + if (!state.isSeeded || isa(e) || isa(e)) { ref value; e = optimizer.optimizeExpr(e, true); bool success = @@ -1779,9 +1655,11 @@ void Executor::executeGetValue(ExecutionState &state, ref e, (void)success; bindLocal(target, state, value); } else { + std::map::iterator it = seedMap->find(&state); + assert(it != seedMap->end()); + assert(!it->second.empty()); std::set> values; - for (std::vector::iterator siit = it->second.begin(), - siie = it->second.end(); + for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { ref cond = siit->assignment.evaluate(e); cond = optimizer.optimizeExpr(cond, true); @@ -2868,12 +2746,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { Executor::StatePair branches = fork(state, cond, ifTrueBlock, ifFalseBlock, BranchType::Conditional); - if (branches.first && branches.second) { - maxNewStateStackSize = - std::max(maxNewStateStackSize, - branches.first->stack.stackRegisterSize() * 8); - } - // NOTE: There is a hidden dependency here, markBranchVisited // requires that we still be in the context of the branch // instruction (it reuses its statistic id). Should be cleaned @@ -4450,63 +4322,90 @@ void Executor::bindModuleConstants(llvm::APFloat::roundingMode rm) { } } -bool Executor::checkMemoryUsage() { +size_t Executor::getMemoryUsage() { + const auto mallocUsage = util::GetTotalMallocUsage(); + const auto mmapUsage = memory->getUsedDeterministicSize(); + return mallocUsage + mmapUsage; +} + +Executor::MemoryUsage Executor::checkMemoryUsage() { if (!MaxMemory) - return true; + return None; + + const auto &states = objectManager->getStates(); + const auto numStates = states.size(); + const auto lastMaxNumStates = + std::max(1UL, (unsigned long)(MaxMemory / lastWeightOfState)); // We need to avoid calling GetTotalMallocUsage() often because it // is O(elts on freelist). This is really bad since we start // to pummel the freelist once we hit the memory cap. // every 65536 instructions if ((stats::instructions & 0xFFFFU) != 0 && - maxNewWriteableOSSize < OSCopySizeMemoryCheckThreshold && - - maxNewStateStackSize < StackCopySizeMemoryCheckThreshold) - return true; + numStates < lastMaxNumStates * 0.4) + return None; // check memory limit - const auto mallocUsage = util::GetTotalMallocUsage() >> 20U; - const auto mmapUsage = memory->getUsedDeterministicSize() >> 20U; - const auto totalUsage = mallocUsage + mmapUsage; + + const auto totalUsage = getMemoryUsage() >> 20U; + const auto weightOfState = std::max(0.001, (double)totalUsage / numStates); + lastWeightOfState = weightOfState; + const auto maxNumStates = + std::max(1UL, (unsigned long)(MaxMemory / weightOfState)); if (MemoryTriggerCoverOnTheFly && totalUsage > MaxMemory * 0.75) { klee_warning_once(0, "enabling cover-on-the-fly (close to memory cap: %luMB)", totalUsage); - coverOnTheFly = true; + coverOnTheFly = CoverOnTheFly; + } + // just guess at how many to kill + // only terminate states when threshold (+1%) exceeded + if (totalUsage < MaxMemory * 0.6 && numStates < maxNumStates * 0.4) { + return Executor::Low; + } else if (totalUsage <= MaxMemory * 1.01 && + numStates <= maxNumStates * 0.7) { + return Executor::High; } - atMemoryLimit = totalUsage > MaxMemory; // inhibit forking - if (!atMemoryLimit) - return true; + if (totalUsage > MaxMemory * 1.01 && numStates <= 2) { + haltExecution = HaltExecution::MaxMemory; + return Executor::None; + } - // only terminate states when threshold (+100MB) exceeded - if (totalUsage <= MaxMemory + 100) - return true; + auto toKill = + std::min(numStates - 1, numStates - (unsigned long)(maxNumStates * 0.4)); - // just guess at how many to kill - auto states = objectManager->getStates(); - const auto numStates = states.size(); - auto toKill = std::max(1UL, numStates - numStates * MaxMemory / totalUsage); - klee_warning("killing %lu states (over memory cap: %luMB)", toKill, - totalUsage); - - // randomly select states for early termination - std::vector arr(states.begin(), - states.end()); // FIXME: expensive - for (unsigned i = 0, N = arr.size(); N && i < toKill; ++i, --N) { - unsigned idx = theRNG.getInt32() % N; + if (toKill != 0) { + klee_warning("killing %lu states (total memory usage: %luMB)", toKill, + totalUsage); + } + unsigned long killed = 0; + for (states_ty::iterator it = states.begin(), ie = states.end(); + it != ie && killed < toKill; ++it) { // Make two pulls to try and not hit a state that - // covered new code. - if (arr[idx]->isCoveredNew()) - idx = theRNG.getInt32() % N; + // covered new code or a seeded state + if ((*it)->isCoveredNew() || (*it)->isSeeded) + continue; - std::swap(arr[idx], arr[N - 1]); - terminateStateEarly(*arr[N - 1], "Memory limit exceeded.", + terminateStateEarly(**it, "Memory limit exceeded.", StateTerminationType::OutOfMemory); + killed++; + } + for (states_ty::iterator it = states.begin(), ie = states.end(); + it != ie && killed < toKill; ++it) { + // Kill some more if needed + if ((*it)->isCoveredNew() || (*it)->isSeeded) { + terminateStateEarly(**it, "Memory limit exceeded.", + StateTerminationType::OutOfMemory); + killed++; + } + } + if (toKill != 0) { + klee_warning("stop killing"); } - return false; + return Executor::Full; } void Executor::decreaseConfidenceFromStoppedStates( @@ -4564,72 +4463,72 @@ const KFunction *Executor::getKFunction(const llvm::Function *f) const { return (kfIt == kmodule->functionMap.end()) ? nullptr : kfIt->second; } -void Executor::seed(ExecutionState &initialState) { - std::vector &v = seedMap->at(&initialState); - - for (std::vector::const_iterator it = usingSeeds->begin(), - ie = usingSeeds->end(); - it != ie; ++it) - v.push_back(SeedInfo(*it)); - - int lastNumSeeds = usingSeeds->size() + 10; - time::Point lastTime, startTime = lastTime = time::getWallTime(); - ExecutionState *lastState = 0; - while (!seedMap->empty()) { - if (haltExecution) { - doDumpStates(); - return; - } - - std::map>::iterator it = - seedMap->upper_bound(lastState); - if (it == seedMap->end()) - it = seedMap->begin(); - lastState = it->first; - ExecutionState &state = *lastState; - KInstruction *ki = state.pc; - objectManager->setCurrentState(&state); - stepInstruction(state); - - executeInstruction(state, ki); - timers.invoke(); - if (::dumpStates) - dumpStates(); - if (::dumpPForest) - dumpPForest(); - objectManager->updateSubscribers(); +std::vector Executor::uploadNewSeeds() { + std::vector seeds; + if (!usingInitialSeeds.empty()) { + seeds = usingInitialSeeds; + usingInitialSeeds.clear(); + return seeds; + } + // just guess at how many to kill + auto &states = objectManager->getStates(); + const auto numStates = std::max(1UL, states.size()); + const auto maxNumStates = + std::max(1UL, (unsigned long)(MaxMemory / lastWeightOfState)); + unsigned long numStoredSeeds = storedSeeds->size(); + unsigned long toUpload = + numStates < maxNumStates * 0.4 ? maxNumStates * 0.4 - numStates : 0; + toUpload = std::min(toUpload, numStoredSeeds); - if ((stats::instructions % 1000) == 0) { - int numSeeds = 0, numStates = 0; - for (std::map>::iterator - it = seedMap->begin(), - ie = seedMap->end(); - it != ie; ++it) { - numSeeds += it->second.size(); - numStates++; - } - const auto time = time::getWallTime(); - const time::Span seedTime(SeedTime); - if (seedTime && time > startTime + seedTime) { - klee_warning("seed time expired, %d seeds remain over %d states", - numSeeds, numStates); - break; - } else if (numSeeds <= lastNumSeeds - 10 || - time - lastTime >= time::seconds(10)) { - lastTime = time; - lastNumSeeds = numSeeds; - klee_message("%d seeds remaining over: %d states", numSeeds, numStates); - } - } + while ((!toUpload || seeds.size() <= toUpload) && !storedSeeds->empty()) { + seeds.push_back(storedSeeds->front()); + storedSeeds->pop_front(); + } + return seeds; +} - klee_message("seeding done (%d states remain)", - (int)objectManager->getStates().size()); +void Executor::initialSeed(ExecutionState &initialState, + std::vector usingSeeds) { + if (usingSeeds.empty()) { + return; + } + seeds_ty &v = seedMap->at(&initialState); + for (std::vector::const_iterator it = usingSeeds.begin(), + ie = usingSeeds.end(); + it != ie; ++it) { + v.push_back(*it); + } + klee_message("Seeding began using %ld seeds!\n", usingSeeds.size()); + objectManager->seed(&initialState); + objectManager->updateSubscribers(); +} - if (OnlySeed) { - doDumpStates(); - return; - } +void Executor::storeState(const ExecutionState &state, ExecutingSeed &res) { + ref response; + solver->setTimeout(coreSolverTimeout); + bool success = + solver->getResponse(state.constraints.cs(), Expr::createFalse(), response, + state.queryMetaData); + solver->setTimeout(time::Span()); + if (!success) { + assert(false && "unable to get symbolic solution"); + return; + } + Assignment assignment; + if (!response->tryGetInitialValues(assignment.bindings)) { + assert(false && "terminated state must have an assignment"); + } + ExecutingSeed seed(assignment, state.steppedInstructions, state.coveredNew, + state.coveredNewError, state.targets(), + state.isTargeted()); + if (pathWriter) { + pathWriter->readStream(getPathStreamID(state), seed.path); + } + if (symPathWriter) { + symPathWriter->readStream(getSymbolicPathStreamID(state), seed.symPath); } + seed.parentId = state.id; + res = seed; } void Executor::reportProgressTowardsTargets(std::string prefix, @@ -4684,10 +4583,6 @@ void Executor::run(ExecutionState *initialState) { if (guidanceKind != GuidanceKind::ErrorGuidance) timers.reset(); - if (usingSeeds) { - seed(*initialState); - } - searcher = std::make_unique(constructUserSearcher(*this)); @@ -4705,17 +4600,40 @@ void Executor::run(ExecutionState *initialState) { objectManager->addSubscriber(searcher.get()); + ExecutionState *firstState = + objectManager->branchState(initialState, BranchType::InitialBranch); + if (pathWriter) { + firstState->pathOS = pathWriter->open(initialState->pathOS); + } + if (symPathWriter) { + firstState->symPathOS = symPathWriter->open(initialState->symPathOS); + } objectManager->initialUpdate(); - + initialSeed(*firstState, uploadNewSeeds()); // main interpreter loop while (!haltExecution && !searcher->empty()) { auto action = searcher->selectAction(); executeAction(action); objectManager->updateSubscribers(); - - if (!checkMemoryUsage()) { + MemoryUsage usage = checkMemoryUsage(); + if (usage == Full) { objectManager->updateSubscribers(); } + if (StoreEarlyStates && (searcher->empty() || usage == Low)) { + std::vector seeds = uploadNewSeeds(); + if (!seeds.empty()) { + ExecutionState *newSeededState = + objectManager->branchState(initialState, BranchType::InitialBranch); + initialSeed(*newSeededState, seeds); + if (pathWriter) { + newSeededState->pathOS = pathWriter->open(initialState->pathOS); + } + if (symPathWriter) { + newSeededState->symPathOS = + symPathWriter->open(initialState->symPathOS); + } + } + } } if (guidanceKind == GuidanceKind::ErrorGuidance) { @@ -4783,6 +4701,45 @@ void Executor::executeAction(ref action) { timers.invoke(); } +void Executor::unseedIfReachedMaxSeedInstructions(ExecutionState *state) { + assert(state->isSeeded); + auto it = seedMap->find(state); + assert(it != seedMap->end()); + + seeds_ty &seeds = it->second; + + assert(!seeds.empty()); + assert(seeds.begin()->maxInstructions >= state->steppedInstructions && + "state stepped instructions exceeded seed max instructions"); + if (seeds.size() != 1) { + return; + } + seeds_ty::iterator siit = seeds.begin(); + + if (!(siit->maxInstructions && + siit->maxInstructions == state->steppedInstructions)) { + return; + } + state->coveredNew = siit->coveredNew; + if (siit->coveredNewError) { + state->coveredNewError = siit->coveredNewError; + } + if (siit->isTargeted) { + targetManager->makeTargeted(*state, siit->targets); + } + if (pathWriter) { + std::vector path; + pathWriter->readStream(getPathStreamID(*state), path); + assert(siit->path == path); + } + seeds.erase(siit); + seedMap->erase(state); + objectManager->unseed(state); + if (seedMap->size() == 0) { + klee_message("Seeding done!\n"); + } +} + void Executor::goForward(ref action) { ref fa = cast(action); objectManager->setCurrentState(fa->state); @@ -4799,7 +4756,9 @@ void Executor::goForward(ref action) { if (targetManager) { targetManager->pullGlobal(state); } - + if (state.isSeeded) { + unseedIfReachedMaxSeedInstructions(&state); + } if (targetCalculator && TrackCoverage != TrackCoverageBy::None && state.multiplexKF && functionsByModule.modules.size() > 1 && targetCalculator->isCovered(state.multiplexKF)) { @@ -4816,9 +4775,6 @@ void Executor::goForward(ref action) { terminateStateEarly(state, "max-sym-cycles exceeded.", StateTerminationType::MaxCycles); } else { - maxNewWriteableOSSize = 0; - maxNewStateStackSize = 0; - KInstruction *ki = state.pc; stepInstruction(state); executeInstruction(state, ki); @@ -4924,17 +4880,16 @@ HaltExecution::Reason fromStateTerminationType(StateTerminationType t) { } void Executor::terminateState(ExecutionState &state, - StateTerminationType reason) { - state.terminationReasonType = fromStateTerminationType(reason); - if (reason >= StateTerminationType::MaxDepth && - reason <= StateTerminationType::EARLY) { + StateTerminationType terminationType) { + if (state.isSeeded) { + seedMap->erase(&state); + } + state.terminationReasonType = fromStateTerminationType(terminationType); + if (terminationType >= StateTerminationType::MaxDepth && + terminationType <= StateTerminationType::EARLY) { SetOfStates states = {&state}; decreaseConfidenceFromStoppedStates(states, state.terminationReasonType); } - if (replayKTest && replayPosition != replayKTest->numObjects) { - klee_warning_once(replayKTest, - "replay did not consume all objects in test input."); - } interpreterHandler->incPathsExplored(); state.pc = state.prevPC; @@ -4960,13 +4915,24 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, StateTerminationType reason) { if (reason <= StateTerminationType::EARLY) { assert(reason > StateTerminationType::EXIT); + if (state.isSeeded) { + klee_warning("early termination while replaying"); + } ++stats::terminationEarly; } - - if (((reason <= StateTerminationType::EARLY || - reason == StateTerminationType::MissedAllTargets) && - shouldWriteTest(state)) || - (AlwaysOutputSeeds && seedMap->count(&state))) { + if (state.isSeeded && (reason > StateTerminationType::EARLY || + reason == StateTerminationType::MaxCycles)) { + assert(!state.isSeeded && + "seeded state should not terminate until interrupted"); + } + if (StoreEarlyStates && reason <= StateTerminationType::EARLY) { + ExecutingSeed seed; + storeState(state, seed); + storedSeeds->push_back(seed); + } else if (((reason <= StateTerminationType::EARLY || + reason == StateTerminationType::MissedAllTargets) && + shouldWriteTest(state)) || + (AlwaysOutputSeeds && seedMap->count(&state))) { state.clearCoveredNew(); interpreterHandler->processTestCase( state, (message + "\n").str().c_str(), @@ -4974,7 +4940,6 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, reason > StateTerminationType::EARLY && reason <= StateTerminationType::EXECERR); } - terminateState(state, reason); } @@ -5420,7 +5385,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, ref Executor::replaceReadWithSymbolic(ExecutionState &state, ref e) { unsigned n = interpreterOpts.MakeConcreteSymbolic; - if (!n || replayKTest || replayPath) + if (!n || state.isSeeded) return e; // right now, we don't replace symbolics (is there any reason to?) @@ -6361,7 +6326,6 @@ void Executor::executeMemoryOperation( terminateStateOnSolverError(*state, "Query timed out (bounds check)."); return; } - solver->setTimeout(time::Span()); bool mustBeInBounds = !isa(response); if (mustBeInBounds) { @@ -6379,8 +6343,6 @@ void Executor::executeMemoryOperation( } if (isWrite) { ObjectState *wos = state->addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); if (wos->readOnly) { terminateStateOnProgramError( *state, @@ -6491,8 +6453,6 @@ void Executor::executeMemoryOperation( const ObjectState *os = op.second.get(); ObjectState *wos = state->addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); if (wos->readOnly) { branches = forkInternal(*state, resolveConditions[i], BranchType::MemOp); @@ -6576,8 +6536,6 @@ void Executor::executeMemoryOperation( if (isWrite) { ObjectState *wos = bound->addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); if (wos->readOnly) { terminateStateOnProgramError( *bound, @@ -6779,77 +6737,49 @@ void Executor::executeMakeSymbolic(ExecutionState &state, const ref source, bool isLocal) { // Create a new object state for the memory object (instead of a copy). - if (!replayKTest) { - const Array *array = makeArray(mo->getSizeExpr(), source); - ObjectState *os = bindObjectInState(state, mo, isLocal, array); - - ref sizeExpr = - dyn_cast(os->getObject()->getSizeExpr()); - - state.addSymbolic(mo, array); - - std::map>::iterator it = - seedMap->find(&state); - if (it != seedMap->end()) { // In seed mode we need to add this as a - // binding. - for (std::vector::iterator siit = it->second.begin(), - siie = it->second.end(); - siit != siie; ++siit) { - SeedInfo &si = *siit; - KTestObject *obj = si.getNextInput(mo, NamedSeedMatching); - - if (!obj) { - if (ZeroSeedExtension) { - si.assignment.bindings.replace( - {array, SparseStorageImpl(0)}); - } else if (!AllowSeedExtension) { - terminateStateOnUserError(state, - "ran out of inputs during seeding"); - break; - } - } else { - ref sizeExpr = - dyn_cast(mo->getSizeExpr()); - if (sizeExpr) { - unsigned moSize = sizeExpr->getZExtValue(); - if (obj->numBytes != moSize && - ((!(AllowSeedExtension || ZeroSeedExtension) && - obj->numBytes < moSize) || - (!AllowSeedTruncation && obj->numBytes > moSize))) { - std::stringstream msg; - msg << "replace size mismatch: " << mo->name << "[" << moSize - << "]" - << " vs " << obj->name << "[" << obj->numBytes << "]" - << " in test\n"; - - terminateStateOnUserError(state, msg.str()); - break; - } else { - SparseStorageImpl values; - if (si.assignment.bindings.find(array) != - si.assignment.bindings.end()) { - values = si.assignment.bindings.at(array); - } - values.store(0, obj->bytes, - obj->bytes + std::min(obj->numBytes, moSize)); - si.assignment.bindings.replace({array, values}); - } - } - } - } + const Array *array = makeArray(mo->getSizeExpr(), source); + ObjectState *os = bindObjectInState(state, mo, isLocal, array); + + ref sizeExpr = + dyn_cast(os->getObject()->getSizeExpr()); + + state.addSymbolic(mo, array); + + if (!state.isSeeded) { + return; + } + std::map::iterator it = seedMap->find(&state); + assert(it != seedMap->end()); + assert(!it->second.empty()); + for (seeds_ty::iterator siit = it->second.begin(), siie = it->second.end(); + siit != siie; ++siit) { + ExecutingSeed &si = *siit; + KTestObject *obj = si.getNextInput(mo, NamedSeedMatching); + + if (!obj) { + continue; } - } else { - ObjectState *os = bindObjectInState(state, mo, false); - if (replayPosition >= replayKTest->numObjects) { - terminateStateOnUserError(state, "replay count mismatch"); - } else { - KTestObject *obj = &replayKTest->objects[replayPosition++]; - ref sizeExpr = dyn_cast(mo->getSizeExpr()); - if (sizeExpr && obj->numBytes != sizeExpr->getZExtValue()) { - for (unsigned i = 0; i < sizeExpr->getZExtValue(); i++) - os->write8(i, obj->bytes[i]); + + ref sizeExpr = dyn_cast(mo->getSizeExpr()); + if (sizeExpr) { + unsigned moSize = sizeExpr->getZExtValue(); + if (obj->numBytes != moSize) { + std::stringstream msg; + msg << "replace size mismatch: " << mo->name << "[" << moSize << "]" + << " vs " << obj->name << "[" << obj->numBytes << "]" + << " in test\n"; + assert(false && msg); + terminateStateOnUserError(state, msg.str()); + break; } else { - terminateStateOnUserError(state, "replay size mismatch"); + SparseStorageImpl values; + if (si.assignment.bindings.find(array) != + si.assignment.bindings.end()) { + values = si.assignment.bindings.at(array); + } + values.store(0, obj->bytes, + obj->bytes + std::min(obj->numBytes, moSize)); + si.assignment.bindings.replace({array, values}); } } } @@ -7041,6 +6971,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, state->symPathOS = symPathOS; run(state); + objectManager->removeInitialState(state); if (statsTracker) statsTracker->done(); @@ -7377,7 +7308,8 @@ void Executor::setInitializationGraph( } for (auto i : pointers) { ktest.objects[i.first].numPointers = i.second.size(); - ktest.objects[i.first].pointers = new Pointer[i.second.size()]; + ktest.objects[i.first].pointers = (Pointer *)calloc( + i.second.size(), sizeof(*ktest.objects[i.first].pointers)); for (size_t j = 0; j < i.second.size(); j++) { ktest.objects[i.first].pointers[j] = i.second[j]; } @@ -7602,8 +7534,10 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { } } + res.symArgvs = 0; + res.symArgvLen = 0; res.numObjects = symbolics.size(); - res.objects = new KTestObject[res.numObjects]; + res.objects = (KTestObject *)calloc(res.numObjects, sizeof(*res.objects)); res.uninitCoeff = uninitObjects.size() * UninitMemoryTestMultiplier; { @@ -7613,12 +7547,13 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { auto mo = symbolic.memoryObject; auto &values = model.bindings.at(symbolic.array); KTestObject *o = &res.objects[i]; - o->name = const_cast(mo->name.c_str()); + o->name = (char *)calloc(mo->name.size() + 1, sizeof(*o->name)); + std::strcpy(o->name, mo->name.c_str()); o->address = cast(evaluator.visit(mo->getBaseExpr())) ->getZExtValue(); o->numBytes = cast(evaluator.visit(mo->getSizeExpr())) ->getZExtValue(); - o->bytes = new unsigned char[o->numBytes]; + o->bytes = (unsigned char *)calloc(o->numBytes, sizeof(*o->bytes)); for (size_t j = 0; j < o->numBytes; j++) { o->bytes[j] = values.load(j); } @@ -7643,6 +7578,11 @@ void Executor::getBlockPath(const ExecutionState &state, blockPath = state.constraints.path().toString(); } +void Executor::getSteppedInstructions(const ExecutionState &state, + unsigned &res) { + res = state.steppedInstructions; +} + void Executor::doImpliedValueConcretization(ExecutionState &state, ref e, ref value) { abort(); // FIXME: Broken until we sort out how to do the write back. @@ -7670,8 +7610,6 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, ref e, assert(!os->readOnly && "not possible? read only object with static read?"); ObjectState *wos = state.addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); wos->write(CE, it->second); } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index d0d4adc20b..08ca9285a8 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -93,7 +93,7 @@ class MemoryObject; class ObjectState; class PForest; class Searcher; -class SeedInfo; +class ExecutingSeed; class SpecialFunctionHandler; struct StackFrame; class SymbolicSource; @@ -133,8 +133,7 @@ class Executor : public Interpreter { decltype(__ctype_toupper_loc()) c_type_toupper_addr; #endif - size_t maxNewWriteableOSSize = 0; - size_t maxNewStateStackSize = 0; + double lastWeightOfState = 0.001; size_t multiplexReached = 0; @@ -164,15 +163,16 @@ class Executor : public Interpreter { std::unique_ptr targetCalculator; std::unique_ptr targetManager; - /// When non-empty the Executor is running in "seed" mode. The - /// states in this map will be executed in an arbitrary order - /// (outside the normal search interface) until they terminate. When - /// the states reach a symbolic branch then either direction that - /// satisfies one or more seeds will be added to this map. What - /// happens with other states (that don't satisfy the seeds) depends - /// on as-yet-to-be-determined flags. + /// When non-empty the Executor is running in "seed" mode. This map matches + /// states with seeds. Seeds contain set of concrete values for symbolic + /// variables. When the states reach a symbolic branch then either direction + /// that satisfies one or more seeds will be added to this map. What happens + /// with other states (that don't satisfy the seeds) depends on + /// as-yet-to-be-determined flags. std::unique_ptr seedMap; + std::unique_ptr> storedSeeds; + /// Map of globals to their representative memory object. std::map globalObjects; @@ -187,20 +187,9 @@ class Executor : public Interpreter { /// Manager for everything related to targeted execution mode std::unique_ptr targetedExecutionManager; - /// When non-null the bindings that will be used for calls to - /// klee_make_symbolic in order replay. - const struct KTest *replayKTest; - - /// When non-null a list of branch decisions to be used for replay. - const std::vector *replayPath; - - /// The index into the current \ref replayKTest or \ref replayPath - /// object. - unsigned replayPosition; - /// When non-null a list of "seed" inputs which will be used to /// drive execution. - const std::vector *usingSeeds; + std::vector usingInitialSeeds; /// Disables forking, instead a random path is chosen. Enabled as /// needed to control memory usage. \see fork() @@ -263,7 +252,12 @@ class Executor : public Interpreter { void executeInstruction(ExecutionState &state, KInstruction *ki); - void seed(ExecutionState &initialState); + std::vector uploadNewSeeds(); + void initialSeed(ExecutionState &initialState, + std::vector usingSeeds); + + void storeState(const ExecutionState &state, ExecutingSeed &res); + void run(ExecutionState *initialState); // Given a concrete object in our [klee's] address space, add it to @@ -577,12 +571,6 @@ class Executor : public Interpreter { ref toConstant(ExecutionState &state, ref e, const std::string &reason); - /// Evaluate the given expression under each seed, and return the - /// first one that results in a constant, if such a seed exist. Otherwise, - /// return the non-constant evaluation of the expression under one of the - /// seeds. - ref getValueFromSeeds(ExecutionState &state, ref e); - ref toConstantPointer(ExecutionState &state, ref e, const char *purpose); @@ -708,11 +696,16 @@ class Executor : public Interpreter { void doImpliedValueConcretization(ExecutionState &state, ref e, ref value); + size_t getMemoryUsage(); + /// check memory usage and terminate states when over threshold of /// -max-memory - /// + 100MB \return true if below threshold, false otherwise (states were + /// + 1% \return true if below threshold, false otherwise (states were /// terminated) - bool checkMemoryUsage(); + + enum MemoryUsage { None, Low, High, Full }; + + MemoryUsage checkMemoryUsage(); /// check if branching/forking into N branches is allowed bool branchingPermitted(ExecutionState &state, unsigned N); @@ -725,6 +718,8 @@ class Executor : public Interpreter { void dumpPForest(); void executeAction(ref action); + + void unseedIfReachedMaxSeedInstructions(ExecutionState *state); void goForward(ref action); const KInstruction *getKInst(const llvm::Instruction *ints) const; @@ -746,18 +741,6 @@ class Executor : public Interpreter { symPathWriter = tsw; } - void setReplayKTest(const struct KTest *out) override { - assert(!replayPath && "cannot replay both buffer and path"); - replayKTest = out; - replayPosition = 0; - } - - void setReplayPath(const std::vector *path) override { - assert(!replayKTest && "cannot replay both buffer and path"); - replayPath = path; - replayPosition = 0; - } - llvm::Module *setModule( std::vector> &userModules, std::vector> &libsModules, @@ -768,8 +751,11 @@ class Executor : public Interpreter { void setFunctionsByModule(FunctionsByModule &&functionsByModule) override; - void useSeeds(const std::vector *seeds) override { - usingSeeds = seeds; + void useSeeds(std::vector seeds) override { + for (SeedFromFile seed : seeds) { + usingInitialSeeds.push_back( + ExecutingSeed(seed.ktest, seed.maxInstructions)); + } } ExecutionState *formState(llvm::Function *f); @@ -848,6 +834,9 @@ class Executor : public Interpreter { void getBlockPath(const ExecutionState &state, std::string &blockPath) override; + void getSteppedInstructions(const ExecutionState &state, + unsigned &res) override; + Expr::Width getWidthForLLVMType(llvm::Type *type) const; size_t getAllocationAlignment(const llvm::Value *allocSite) const; diff --git a/lib/Core/ObjectManager.cpp b/lib/Core/ObjectManager.cpp index 40a66eee23..cef9b1e4e6 100644 --- a/lib/Core/ObjectManager.cpp +++ b/lib/Core/ObjectManager.cpp @@ -18,10 +18,14 @@ void ObjectManager::addSubscriber(Subscriber *s) { subscribers.push_back(s); } void ObjectManager::addProcessForest(PForest *pf) { processForest = pf; } void ObjectManager::addInitialState(ExecutionState *state) { - states.insert(state); processForest->addRoot(state); } +void ObjectManager::removeInitialState(ExecutionState *state) { + processForest->remove(state->ptreeNode); + delete state; +} + void ObjectManager::setCurrentState(ExecutionState *_current) { assert(current == nullptr); current = _current; @@ -30,7 +34,6 @@ void ObjectManager::setCurrentState(ExecutionState *_current) { ExecutionState *ObjectManager::branchState(ExecutionState *state, BranchType reason) { - assert(statesUpdated); ExecutionState *newState = state->branch(); addedStates.push_back(newState); processForest->attach(state->ptreeNode, newState, state); @@ -49,6 +52,19 @@ void ObjectManager::removeState(ExecutionState *state) { removedStates.push_back(state); } +void ObjectManager::unseed(ExecutionState *state) { + if (state->isSeeded) { + state->isSeeded = false; + statesUpdated = true; + } +} +void ObjectManager::seed(ExecutionState *state) { + if (!state->isSeeded) { + state->isSeeded = true; + statesUpdated = true; + } +} + void ObjectManager::updateSubscribers() { if (statesUpdated) { ref e = new States(current, addedStates, removedStates); diff --git a/lib/Core/ObjectManager.h b/lib/Core/ObjectManager.h index 4d3acd78f6..0bfaa8cc58 100644 --- a/lib/Core/ObjectManager.h +++ b/lib/Core/ObjectManager.h @@ -53,12 +53,16 @@ class ObjectManager { void addProcessForest(PForest *); void addInitialState(ExecutionState *state); + void removeInitialState(ExecutionState *state); void setCurrentState(ExecutionState *_current); ExecutionState *branchState(ExecutionState *state, BranchType reason); void removeState(ExecutionState *state); + void unseed(ExecutionState *state); + void seed(ExecutionState *state); + const states_ty &getStates(); void updateSubscribers(); diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 695f3f3977..c903ad8b6c 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -917,3 +917,104 @@ bool DiscreteTimeFairSearcher::empty() { return functions.empty(); } void DiscreteTimeFairSearcher::printName(llvm::raw_ostream &os) { os << "DiscreteTimeFairSearcher\n"; } + +// + +SeededSearcher::SeededSearcher(Searcher *baseSearcher, Searcher *seededSearcher) + : baseSearcher(baseSearcher), seededSearcher(seededSearcher) {} + +ExecutionState &SeededSearcher::selectState() { + if (!seededSearcher->empty()) { + return seededSearcher->selectState(); + } + return baseSearcher->selectState(); +} + +void SeededSearcher::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { + bool currentUpdated = false; + if (std::find(addedStates.begin(), addedStates.end(), current) == + addedStates.end()) { + currentUpdated = updateCurrent(current); + } else { + assert(false); + } + + for (ExecutionState *state : addedStates) { + if (state->isSeeded) { + addedSeededStates.push_back(state); + seededSearcherStates.insert(state); + } else { + addedUnseededStates.push_back(state); + baseSearcherStates.insert(state); + } + } + + for (ExecutionState *state : removedStates) { + if (state->isSeeded) { + removedSeededStates.push_back(state); + seededSearcherStates.erase(state); + } else { + removedUnseededStates.push_back(state); + baseSearcherStates.erase(state); + } + } + + if (!current || currentUpdated) { + baseSearcher->update(nullptr, addedUnseededStates, removedUnseededStates); + seededSearcher->update(nullptr, addedSeededStates, removedSeededStates); + } else if (current->isSeeded) { + baseSearcher->update(nullptr, addedUnseededStates, removedUnseededStates); + seededSearcher->update(current, addedSeededStates, removedSeededStates); + } else if (!current->isSeeded) { + baseSearcher->update(current, addedUnseededStates, removedUnseededStates); + seededSearcher->update(nullptr, addedSeededStates, removedSeededStates); + } + + addedUnseededStates.clear(); + addedSeededStates.clear(); + removedUnseededStates.clear(); + removedSeededStates.clear(); +} + +bool SeededSearcher::updateCurrent(ExecutionState *current) { + if (!current) { + return false; + } + if (current->isSeeded) { + if (baseSearcherStates.count(current) == 0) { + assert(seededSearcherStates.count(current) != 0); + return false; + } else { + assert(seededSearcherStates.count(current) == 0); + baseSearcherStates.erase(current); + seededSearcherStates.insert(current); + baseSearcher->update(nullptr, {}, {current}); + seededSearcher->update(nullptr, {current}, {}); + return true; + } + } else { + if (seededSearcherStates.count(current) == 0) { + assert(baseSearcherStates.count(current) != 0); + return false; + } else { + assert(baseSearcherStates.count(current) == 0); + seededSearcherStates.erase(current); + baseSearcherStates.insert(current); + seededSearcher->update(nullptr, {}, {current}); + baseSearcher->update(nullptr, {current}, {}); + return true; + } + } +} + +bool SeededSearcher::empty() { + return baseSearcher->empty() && seededSearcher->empty(); +} + +void SeededSearcher::printName(llvm::raw_ostream &os) { + os << " with base searcher:\n"; + baseSearcher->printName(os); + os << " \n"; +} diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index e5bc79705c..4b83757030 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -418,6 +418,31 @@ class DiscreteTimeFairSearcher final : public Searcher { bool empty() override; void printName(llvm::raw_ostream &os) override; }; + +/// Seeded searcher is used to select seeded states before unseeded +class SeededSearcher final : public Searcher { + std::unique_ptr baseSearcher; + std::unique_ptr seededSearcher; + states_ty baseSearcherStates; + states_ty seededSearcherStates; + std::vector addedUnseededStates; + std::vector addedSeededStates; + std::vector removedUnseededStates; + std::vector removedSeededStates; + +public: + explicit SeededSearcher(Searcher *baseSearcher, Searcher *seededSearcher); + + ExecutionState &selectState() override; + + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) override; + bool updateCurrent(ExecutionState *current); + ~SeededSearcher() override = default; + bool empty() override; + void printName(llvm::raw_ostream &os) override; +}; } // namespace klee #endif /* KLEE_SEARCHER_H */ diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 727439163d..4f099de3f2 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -22,7 +22,12 @@ using namespace klee; -KTestObject *SeedInfo::getNextInput(const MemoryObject *mo, bool byName) { +void ExecutingSeed::kTestDeleter(KTest *ktest) { kTest_free(ktest); } + +KTestObject *ExecutingSeed::getNextInput(const MemoryObject *mo, bool byName) { + if (!input) + return nullptr; + if (byName) { unsigned i; @@ -62,111 +67,3 @@ KTestObject *SeedInfo::getNextInput(const MemoryObject *mo, bool byName) { } } } - -void SeedInfo::patchSeed(const ExecutionState &state, ref condition, - TimingSolver *solver) { - ConstraintSet required = state.constraints.cs(); - required.addConstraint(condition); - - // Try and patch direct reads first, this is likely to resolve the - // problem quickly and avoids long traversal of all seed - // values. There are other smart ways to do this, the nicest is if - // we got a minimal counterexample from STP, in which case we would - // just inject those values back into the seed. - std::set> directReads; - std::vector> reads; - findReads(condition, false, reads); - for (const auto &re : reads) { - if (ConstantExpr *CE = dyn_cast(re->index)) { - directReads.insert( - std::make_pair(re->updates.root, (unsigned)CE->getZExtValue(32))); - } - } - - for (const auto &[array, i] : directReads) { - ref read = ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(i, Expr::Int32)); - - // If not in bindings then this can't be a violation? - Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array); - if (it2 != assignment.bindings.end()) { - ref isSeed = EqExpr::create( - read, ConstantExpr::alloc(it2->second.load(i), Expr::Int8)); - bool res; - bool success = - solver->mustBeFalse(required, isSeed, res, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res) { - ref value; - bool success = - solver->getValue(required, read, value, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - auto s = it2->second; - s.store(i, value->getZExtValue(8)); - assignment.bindings.replace({it2->first, s}); - required.addConstraint(EqExpr::create( - read, ConstantExpr::alloc(it2->second.load(i), Expr::Int8))); - } else { - required.addConstraint(isSeed); - } - } - } - - bool res; - bool success = - solver->mayBeTrue(state.constraints.cs(), assignment.evaluate(condition), - res, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res) - return; - - // We could still do a lot better than this, for example by looking at - // independence. But really, this shouldn't be happening often. - for (Assignment::bindings_ty::iterator it = assignment.bindings.begin(), - ie = assignment.bindings.end(); - it != ie; ++it) { - const Array *array = it->first; - ref arrayConstantSize = - cast(assignment.evaluate(array->size)); - for (unsigned i = 0; i < arrayConstantSize->getZExtValue(); ++i) { - ref read = ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(i, Expr::Int32)); - ref isSeed = EqExpr::create( - read, ConstantExpr::alloc(it->second.load(i), Expr::Int8)); - bool res; - bool success = - solver->mustBeFalse(required, isSeed, res, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - if (res) { - ref value; - bool success = - solver->getValue(required, read, value, state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - auto s = it->second; - s.store(i, value->getZExtValue(8)); - assignment.bindings.replace({it->first, s}); - required.addConstraint(EqExpr::create( - read, ConstantExpr::alloc(it->second.load(i), Expr::Int8))); - } else { - required.addConstraint(isSeed); - } - } - } - -#ifndef NDEBUG - { - bool res; - bool success = solver->mayBeTrue(state.constraints.cs(), - assignment.evaluate(condition), res, - state.queryMetaData); - assert(success && "FIXME: Unhandled solver failure"); - (void)success; - assert(res && "seed patching failed"); - } -#endif -} diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h index ee84133bc3..8d7b6d4232 100644 --- a/lib/Core/SeedInfo.h +++ b/lib/Core/SeedInfo.h @@ -1,4 +1,4 @@ -//===-- SeedInfo.h ----------------------------------------------*- C++ -*-===// +//=== --SeedInfo.h ----------------------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // @@ -10,9 +10,15 @@ #ifndef KLEE_SEEDINFO_H #define KLEE_SEEDINFO_H +#include "ExecutionState.h" +#include "klee/ADT/ImmutableList.h" +#include "klee/ADT/PersistentSet.h" #include "klee/Expr/Assignment.h" +#include "klee/Module/Target.h" +#include #include +#include extern "C" { struct KTest; @@ -24,22 +30,47 @@ class ExecutionState; class TimingSolver; class MemoryObject; -class SeedInfo { +class ExecutingSeed { public: Assignment assignment; - KTest *input; - unsigned inputPosition; + std::shared_ptr input; + unsigned maxInstructions; std::set used; + mutable std::deque>> coveredNew; + mutable ref> coveredNewError = nullptr; + unsigned inputPosition = 0; + unsigned parentId; + PersistentSet> targets; + bool isTargeted; + std::vector path; + std::vector symPath; public: - explicit SeedInfo(KTest *_input) : input(_input), inputPosition(0) {} + ~ExecutingSeed() {} + + ExecutingSeed() {} + + explicit ExecutingSeed(KTest *input, unsigned maxInstructions = 0, + std::deque>> coveredNew = {}, + ref> coveredNewError = 0, + const PersistentSet> targets = {}, + bool isTargeted = 0) + : input(input, kTestDeleter), maxInstructions(maxInstructions), + coveredNew(coveredNew), coveredNewError(coveredNewError), + targets(targets), isTargeted(isTargeted) {} + + explicit ExecutingSeed(Assignment assignment, unsigned maxInstructions = 0, + std::deque>> coveredNew = {}, + ref> coveredNewError = 0, + const PersistentSet> targets = {}, + bool isTargeted = 0) + : assignment(assignment), maxInstructions(maxInstructions), + coveredNew(coveredNew), coveredNewError(coveredNewError), + targets(targets), isTargeted(isTargeted) {} KTestObject *getNextInput(const MemoryObject *mo, bool byName); - /// Patch the seed so that condition is satisfied while retaining as - /// many of the seed values as possible. - void patchSeed(const ExecutionState &state, ref condition, - TimingSolver *solver); + static void kTestDeleter(KTest *ktest); }; } // namespace klee diff --git a/lib/Core/SeedMap.cpp b/lib/Core/SeedMap.cpp index f740caed81..974d009014 100644 --- a/lib/Core/SeedMap.cpp +++ b/lib/Core/SeedMap.cpp @@ -8,8 +8,7 @@ SeedMap::SeedMap() {} void SeedMap::update(ref e) { if (auto statesEvent = dyn_cast(e)) { for (const auto state : statesEvent->removed) { - std::map>::iterator it = - seedMap.find(state); + std::map::iterator it = seedMap.find(state); if (it != seedMap.end()) { seedMap.erase(it); } @@ -17,33 +16,31 @@ void SeedMap::update(ref e) { } } -std::map>::iterator +std::map::iterator SeedMap::upper_bound(ExecutionState *state) { return seedMap.upper_bound(state); } -std::map>::iterator +std::map::iterator SeedMap::find(ExecutionState *state) { return seedMap.find(state); } -std::map>::iterator SeedMap::begin() { +std::map::iterator SeedMap::begin() { return seedMap.begin(); } -std::map>::iterator SeedMap::end() { +std::map::iterator SeedMap::end() { return seedMap.end(); } -void SeedMap::erase( - std::map>::iterator it) { +void SeedMap::erase(std::map::iterator it) { seedMap.erase(it); } void SeedMap::erase(ExecutionState *state) { seedMap.erase(state); } -void SeedMap::push_back(ExecutionState *state, - std::vector::iterator siit) { +void SeedMap::push_back(ExecutionState *state, seeds_ty::iterator siit) { seedMap[state].push_back(*siit); } @@ -51,9 +48,7 @@ std::size_t SeedMap::count(ExecutionState *state) { return seedMap.count(state); } -std::vector &SeedMap::at(ExecutionState *state) { - return seedMap[state]; -} +seeds_ty &SeedMap::at(ExecutionState *state) { return seedMap[state]; } bool SeedMap::empty() { return seedMap.empty(); } diff --git a/lib/Core/SeedMap.h b/lib/Core/SeedMap.h index 783a729282..fae8db72a9 100644 --- a/lib/Core/SeedMap.h +++ b/lib/Core/SeedMap.h @@ -6,28 +6,31 @@ #include "SeedInfo.h" #include - +#include namespace klee { + +using seeds_ty = std::vector; + class SeedMap : public Subscriber { private: - std::map> seedMap; + std::map seedMap; public: SeedMap(); void update(ref e) override; - std::map>::iterator + std::map::iterator upper_bound(ExecutionState *state); - std::map>::iterator - find(ExecutionState *state); - std::map>::iterator end(); - std::map>::iterator begin(); - void erase(std::map>::iterator it); + std::map::iterator find(ExecutionState *state); + std::map::iterator end(); + std::map::iterator begin(); + void erase(std::map::iterator it); void erase(ExecutionState *state); - void push_back(ExecutionState *state, std::vector::iterator siit); + void push_back(ExecutionState *state, seeds_ty::iterator siit); std::size_t count(ExecutionState *state); - std::vector &at(ExecutionState *state); + seeds_ty &at(ExecutionState *state); + unsigned size() { return seedMap.size(); } bool empty(); virtual ~SeedMap(); diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index b91226d7a8..4dddcb5762 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -169,6 +169,10 @@ void TargetManager::updateReached(ExecutionState &state) { } void TargetManager::updateTargets(ExecutionState &state) { + if (state.isSeeded) { + assert(!isTargeted(state)); + return; + } if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { state.setTargeted(true); diff --git a/lib/Core/TargetManager.h b/lib/Core/TargetManager.h index c0561787ba..a5fe5f86a0 100644 --- a/lib/Core/TargetManager.h +++ b/lib/Core/TargetManager.h @@ -51,6 +51,12 @@ class TargetManager : public Subscriber { TargetHashSet removedTargets; TargetHashSet addedTargets; + void setTargets(ExecutionState &state, + const PersistentSet> &targets) { + state.setTargets(targets); + changedStates.insert(&state); + } + void setTargets(ExecutionState &state, const TargetHashSet &targets) { state.setTargets(targets); changedStates.insert(&state); @@ -144,6 +150,13 @@ class TargetManager : public Subscriber { void collectFiltered(const StatesSet &filter, TargetHistoryTargetPairToStatesMap &added, TargetHistoryTargetPairToStatesMap &removed); + + void makeTargeted(ExecutionState &state, + const PersistentSet> &targets) { + assert(!isTargeted(state)); + state.setTargeted(true); + setTargets(state, targets); + } }; } // namespace klee diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index feb1318bba..c0c76017a3 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -87,6 +87,11 @@ cl::opt UseFairSearch( "(default=false)"), cl::init(false), cl::cat(SearchCat)); +cl::opt + UseSeededSearch("use-seeded-search", + cl::desc("Use seeded searcher (explores seeded states " + "before unseeded) (default=false)"), + cl::init(false), cl::cat(SearchCat)); } // namespace klee void klee::initializeSearchOptions() { @@ -187,6 +192,12 @@ Searcher *klee::constructBaseSearcher(Executor &executor) { new IterativeDeepeningSearcher(searcher, UseIterativeDeepeningSearch); } + if (UseSeededSearch) { + searcher = new SeededSearcher(searcher, + getNewSearcher(CoreSearch[0], executor.theRNG, + *executor.processForest)); + } + return searcher; } @@ -199,7 +210,6 @@ Searcher *klee::constructUserSearcher(Executor &executor) { } else { searcher = constructBaseSearcher(executor); } - llvm::raw_ostream &os = executor.getHandler().getInfoStream(); os << "BEGIN searcher description\n"; diff --git a/scripts/kleef b/scripts/kleef index b1f2abb55a..dcd8b6d67d 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -20,6 +20,7 @@ def klee_options( f_err, f_cov, write_ktests, + store_early_states ): if max_time and int(max_time) > 30: MAX_SOLVER_TIME = 15 @@ -63,9 +64,13 @@ def klee_options( # "-const-array-opt", "--only-output-make-symbolic-arrays", "--memory-backend=mixed", - "--max-fixed-size-structures-size=64", - ] - + "--max-fixed-size-structures-size=64", ] + if store_early_states: + cmd += [ + "--store-early-states", + "--upload-percentage=50", + "--use-seeded-search", + ] if is32: cmd += [ "--allocate-determ", @@ -103,7 +108,8 @@ def klee_options( if f_cov: cmd += [ "--optimize=false", - "--mem-trigger-cof", # Start on the fly tests generation after approaching memory cup + "--use-guided-search=coverage", + "--mem-trigger-cof=false", # Start on the fly tests generation after approaching memory cup "--use-alpha-equivalence=true", "--optimize-aggressive=false", "--track-coverage=all", # Only branches and only instructions are wrong in real life. E.g., ternary operators are sometimes counted as different branches, while we stick to look at them as a single instruction from a single branch @@ -189,6 +195,7 @@ class KLEEF(object): use_perf=False, use_valgrind=False, write_ktests=False, + store_early_states=False, ): self.source = Path(source) if source else None self.is32 = is32 @@ -204,6 +211,7 @@ class KLEEF(object): self.write_ktests = "true" else: self.write_ktests = "false" + self.store_early_states = store_early_states # This file is inside the bin directory - use the root as base self.bin_directory = Path(__file__).parent @@ -308,6 +316,7 @@ class KLEEF(object): self.f_err, self.f_cov, self.write_ktests, + self.store_early_states ) if self.isModifyingUlimitPermitted(): cmd = ["ulimit -s unlimited", "&&"] + cmd @@ -407,6 +416,7 @@ def run(args): use_perf=args.perf, use_valgrind=args.valgrind, write_ktests=args.write_ktests, + store_early_states=args.store_early_states, ) wrapper.compile() return wrapper.run() @@ -458,6 +468,13 @@ def main(): parser.add_argument( "--write-ktests", help="Write tests in KTest format", action="store_true" ) + parser.add_argument( + "--store-early-states", + help="Store states in memory after early termination", + action="store_true", + default=True, + ) + args = parser.parse_args() run(args) diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c deleted file mode 100644 index d2e34b6ec3..0000000000 --- a/test/Coverage/ReplayOutDir.c +++ /dev/null @@ -1,13 +0,0 @@ -// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc -// RUN: rm -rf %t1.out %t1.replay -// RUN: %klee --output-dir=%t1.out %t1.bc -// RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc - -#include "klee/klee.h" - -int main() { - int i; - klee_make_symbolic(&i, sizeof i, "i"); - klee_print_range("i", i); - return 0; -} diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index a24a16993e..454b82ff3d 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -1,3 +1,4 @@ +// XFAIL: * // REQUIRES: not-msan // MSan adds additional memory that overflows the counter // @@ -49,7 +50,7 @@ int main() { } #endif - // CHECK-WRN: WARNING: killing 1 states (over memory cap + // CHECK-WRN: WARNING: killing 1 states (total memory usage if (malloc_failed) printf("MALLOC FAILED\n"); diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c index 197def219d..26e180e937 100644 --- a/test/Feature/NamedSeedMatching.c +++ b/test/Feature/NamedSeedMatching.c @@ -5,7 +5,7 @@ // RUN: not test -f %t.klee-out/test000002.ktest // RUN: rm -rf %t.klee-out-2 -// RUN: %klee --output-dir=%t.klee-out-2 --only-replay-seeds --named-seed-matching --seed-file %t.klee-out/test000001.ktest %t.bc > %t.log +// RUN: %klee --output-dir=%t.klee-out-2 --named-seed-matching --seed-file %t.klee-out/test000001.ktest %t.bc > %t.log // RUN: grep -q "a==3" %t.log // RUN: grep -q "b==4" %t.log // RUN: grep -q "c==5" %t.log diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c deleted file mode 100644 index cfe0c291ee..0000000000 --- a/test/Feature/ReplayPath.c +++ /dev/null @@ -1,46 +0,0 @@ -// RUN: %clang %s -emit-llvm %O0opt -DCOND_EXIT -c -o %t1.bc -// RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --write-paths %t1.bc > %t3.good - -// RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc -// RUN: rm -rf %t.klee-out-2 -// RUN: %klee --output-dir=%t.klee-out-2 --replay-path %t.klee-out/test000001.path %t2.bc > %t3.log -// RUN: diff %t3.log %t3.good -#include "klee/klee.h" -#include -#include - -void cond_exit() { -#ifdef COND_EXIT - klee_silent_exit(0); -#endif -} - -int main() { - int res = 1; - int x; - - klee_make_symbolic(&x, sizeof x, "x"); - - if (x & 1) - res *= 2; - else - cond_exit(); - if (x & 2) - res *= 3; - else - cond_exit(); - if (x & 4) - res *= 5; - else - cond_exit(); - - // get forced branch coverage - if (x & 2) - res *= 7; - if (!(x & 2)) - res *= 11; - printf("res: %d\n", res); - - return 0; -} diff --git a/test/Feature/TestRunForever.c b/test/Feature/TestRunForever.c new file mode 100644 index 0000000000..022554746d --- /dev/null +++ b/test/Feature/TestRunForever.c @@ -0,0 +1,21 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out +// RUN: %klee --output-dir=%t1.klee-out --store-early-states --write-paths --write-sym-paths --search=bfs --max-memory=500 %t1.bc + +#include "klee/klee.h" +int a[100]; + +void rec(int i) { + if (i == 28) { + return; + } + if (a[i] < 0) { + rec(i + 1); + } else if (a[i] > 100) { + rec(i + 1); + } +} +int main(int argc, char **argv) { + klee_make_symbolic(&a, sizeof(a), "a"); + rec(0); +} \ No newline at end of file diff --git a/test/Feature/TestSeedingSolver.c b/test/Feature/TestSeedingSolver.c new file mode 100644 index 0000000000..765c055f4b --- /dev/null +++ b/test/Feature/TestSeedingSolver.c @@ -0,0 +1,30 @@ +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out +// RUN: rm -rf %t2.klee-out +// RUN: rm -rf %t3.klee-out +// RUN: rm -rf %t4.klee-out +// RUN: %klee --output-dir=%t1.klee-out %t1.bc +// RUN: %klee --output-dir=%t2.klee-out --max-instructions=500 %t1.bc +// RUN: %klee --seed-dir=%t1.klee-out --use-seeded-search --output-dir=%t3.klee-out %t1.bc +// RUN: %klee --seed-dir=%t2.klee-out --use-seeded-search --output-dir=%t4.klee-out %t1.bc +// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t3.klee-out > %t3.stats +// RUN: %klee-stats --print-columns 'SolverQueries' --table-format=csv %t4.klee-out > %t4.stats +// RUN: FileCheck -check-prefix=CHECK-NO-MAX-INSTRUCTIONS -input-file=%t3.stats %s +// RUN: FileCheck -check-prefix=CHECK-MAX-INSTRUCTIONS -input-file=%t4.stats %s + +#include "klee/klee.h" + +int main(int argc, char **argv) { + int a; + klee_make_symbolic(&a, sizeof(a), "a"); + for (int i = 0; i < 100; i++) { + if (a + i == 2 * i) { + break; + } + } +} +// CHECK-NO-MAX-INSTRUCTIONS: SolverQueries +// CHECK-NO-MAX-INSTRUCTIONS: 101 +// CHECK-MAX-INSTRUCTIONS: SolverQueries +// CHECK-MAX-INSTRUCTIONS: 172 \ No newline at end of file diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c index 10541cb1fa..b0e7fd1748 100644 --- a/test/Runtime/POSIX/SeedAndFail.c +++ b/test/Runtime/POSIX/SeedAndFail.c @@ -1,8 +1,8 @@ // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 2>%t.log +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1 2>%t.log // RUN: rm -rf %t.klee-out-2 -// RUN: %klee --output-dir=%t.klee-out-2 --seed-dir=%t.klee-out --allow-seed-extension --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1 +// RUN: %klee --output-dir=%t.klee-out-2 --seed-dir=%t.klee-out --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --max-fail 1 // RUN: ls %t.klee-out-2 | grep -c assert | grep 4 #include diff --git a/test/regression/2018-05-17-replay-short-names.c b/test/regression/2018-05-17-replay-short-names.c deleted file mode 100644 index 2f1e75fb83..0000000000 --- a/test/regression/2018-05-17-replay-short-names.c +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: rm -rf a -// RUN: mkdir a -// RUN: touch a/b -// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc -// RUN: rm -rf %t.klee-out -// RUN: %klee -replay-ktest-dir=a --output-dir=%t.klee-out %t1.bc 2>&1 -// - -#include "klee/klee.h" - -int main(int argc, char *argv[]) {} diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index c3f2101bf4..af8916b40b 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -95,6 +95,11 @@ cl::opt WriteKTests( cl::desc("Write .ktest files for each test case (default=true)"), cl::cat(TestCaseCat)); +cl::opt WriteSeedInfo( + "write-seeds", cl::init(true), + cl::desc("Write seedinfo files files for each test case (default=true)"), + cl::cat(TestCaseCat)); + cl::opt WriteCVCs("write-cvcs", cl::desc("Write .cvc files for each test case (default=false)"), @@ -281,21 +286,6 @@ cl::opt cl::OptionCategory ReplayCat("Replaying options", "These options impact replaying of test cases."); -cl::list - ReplayKTestFile("replay-ktest-file", - cl::desc("Specify a .ktest file to use for replay"), - cl::value_desc(".ktest file"), cl::cat(ReplayCat)); - -cl::list - ReplayKTestDir("replay-ktest-dir", - cl::desc("Specify a directory to replay .ktest files from"), - cl::value_desc("output directory"), cl::cat(ReplayCat)); - -cl::opt ReplayPathFile("replay-path", - cl::desc("Specify a path file to replay"), - cl::value_desc("path file"), - cl::cat(ReplayCat)); - cl::list SeedOutFile("seed-file", cl::desc(".ktest file to be used as seed"), cl::cat(SeedingCat)); @@ -422,9 +412,11 @@ cl::opt MultiplexForStaticAnalysis( } // namespace namespace klee { + extern cl::opt MaxTime; extern cl::opt FunctionCallReproduce; extern cl::opt DumpStatesOnHalt; + class ExecutionState; } // namespace klee @@ -460,6 +452,7 @@ class KleeHandler : public InterpreterHandler { void incPathsExplored(std::uint32_t num = 1) override { m_pathsExplored += num; } + bool seedInfoToFile(unsigned instructions, std::string path); void setInterpreter(Interpreter *i); @@ -669,6 +662,15 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id, return openOutputFile(getTestFilename(suffix, id, version)); } +bool KleeHandler::seedInfoToFile(unsigned instructions, std::string path) { + std::ofstream out(path + "seedinfo"); + if (!out.good()) { + return false; + } + out << instructions << "\n"; + return true; +} + /* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */ void KleeHandler::processTestCase(const ExecutionState &state, const char *message, const char *suffix, @@ -716,11 +718,23 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } + if (WriteSeedInfo) { + for (unsigned i = 0; i < ktest.uninitCoeff + 1; ++i) { + unsigned steppedInstructions; + m_interpreter->getSteppedInstructions(state, steppedInstructions); + if (!seedInfoToFile(steppedInstructions, + getOutputFilename(getTestFilename("", id, i)))) { + klee_warning("unable to write seedinfo for test case"); + } + } + } + for (unsigned i = 0; i < ktest.numObjects; i++) { - delete[] ktest.objects[i].bytes; - delete[] ktest.objects[i].pointers; + free(ktest.objects[i].name); + free(ktest.objects[i].bytes); + free(ktest.objects[i].pointers); } - delete[] ktest.objects; + free(ktest.objects); } if (message) { @@ -1464,12 +1478,7 @@ static int run_klee_on_function(int pArgc, char **pArgv, char **pEnvp, std::unique_ptr &handler, std::unique_ptr &interpreter, llvm::Module *finalModule, - llvm::Function *mainFn, - std::vector &replayPath) { - if (ReplayPathFile != "") { - interpreter->setReplayPath(&replayPath); - } - + llvm::Function *mainFn) { auto startTime = std::time(nullptr); if (WriteXMLTests) { @@ -1522,103 +1531,57 @@ static int run_klee_on_function(int pArgc, char **pArgv, char **pEnvp, handler->getInfoStream().flush(); } - if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) { - assert(SeedOutFile.empty()); - assert(SeedOutDir.empty()); - - std::vector kTestFiles = ReplayKTestFile; - for (std::vector::iterator it = ReplayKTestDir.begin(), - ie = ReplayKTestDir.end(); - it != ie; ++it) - KleeHandler::getKTestFilesInDir(*it, kTestFiles); - std::vector kTests; - for (std::vector::iterator it = kTestFiles.begin(), - ie = kTestFiles.end(); - it != ie; ++it) { - KTest *out = kTest_fromFile(it->c_str()); - if (out) { - kTests.push_back(out); - } else { - klee_warning("unable to open: %s\n", (*it).c_str()); - } - } - - if (RunInDir != "") { - int res = chdir(RunInDir.c_str()); - if (res < 0) { - klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(), - sys::StrError(errno).c_str()); - } + if (RunInDir != "") { + int res = chdir(RunInDir.c_str()); + if (res < 0) { + klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(), + sys::StrError(errno).c_str()); } + } - unsigned i = 0; - for (std::vector::iterator it = kTests.begin(), ie = kTests.end(); - it != ie; ++it) { - KTest *out = *it; - interpreter->setReplayKTest(out); - llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out) - << " bytes)" - << " (" << ++i << "/" << kTestFiles.size() << ")\n"; - // XXX should put envp in .ktest ? - interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp); - if (interrupted) - break; - } - interpreter->setReplayKTest(0); - while (!kTests.empty()) { - kTest_free(kTests.back()); - kTests.pop_back(); + std::vector seeds; + for (std::vector::iterator it = SeedOutFile.begin(), + ie = SeedOutFile.end(); + it != ie; ++it) { + SeedFromFile out(it->substr(0, it->size() - 5)); + if (!out.ktest) { + klee_error("unable to open: %s\n", (*it).c_str()); } - } else { - std::vector seeds; - for (std::vector::iterator it = SeedOutFile.begin(), - ie = SeedOutFile.end(); - it != ie; ++it) { - KTest *out = kTest_fromFile(it->c_str()); - if (!out) { - klee_error("unable to open: %s\n", (*it).c_str()); + seeds.push_back(out); + } + for (std::vector::iterator it = SeedOutDir.begin(), + ie = SeedOutDir.end(); + it != ie; ++it) { + std::vector kTestFiles; + KleeHandler::getKTestFilesInDir(*it, kTestFiles); + for (std::vector::iterator it2 = kTestFiles.begin(), + ie = kTestFiles.end(); + it2 != ie; ++it2) { + SeedFromFile out(it2->substr(0, it2->size() - 5)); + if (!out.ktest) { + klee_error("unable to open: %s\n", (*it2).c_str()); } seeds.push_back(out); } - for (std::vector::iterator it = SeedOutDir.begin(), - ie = SeedOutDir.end(); - it != ie; ++it) { - std::vector kTestFiles; - KleeHandler::getKTestFilesInDir(*it, kTestFiles); - for (std::vector::iterator it2 = kTestFiles.begin(), - ie = kTestFiles.end(); - it2 != ie; ++it2) { - KTest *out = kTest_fromFile(it2->c_str()); - if (!out) { - klee_error("unable to open: %s\n", (*it2).c_str()); - } - seeds.push_back(out); - } - if (kTestFiles.empty()) { - klee_error("seeds directory is empty: %s\n", (*it).c_str()); - } - } - - if (!seeds.empty()) { - klee_message("KLEE: using %lu seeds\n", seeds.size()); - interpreter->useSeeds(&seeds); - } - if (RunInDir != "") { - int res = chdir(RunInDir.c_str()); - if (res < 0) { - klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(), - sys::StrError(errno).c_str()); - } + if (kTestFiles.empty()) { + klee_error("seeds directory is empty: %s\n", (*it).c_str()); } + } - interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp); - - while (!seeds.empty()) { - kTest_free(seeds.back()); - seeds.pop_back(); + if (!seeds.empty()) { + klee_message("KLEE: using %lu seeds\n", seeds.size()); + interpreter->useSeeds(seeds); + } + if (RunInDir != "") { + int res = chdir(RunInDir.c_str()); + if (res < 0) { + klee_error("Unable to change directory to: %s - %s", RunInDir.c_str(), + sys::StrError(errno).c_str()); } } + interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp); + auto endTime = std::time(nullptr); { // output end and elapsed time std::uint32_t h; @@ -2346,12 +2309,6 @@ int main(int argc, char **argv, char **envp) { pArgv[i] = pArg; } - std::vector replayPath; - - if (ReplayPathFile != "") { - KleeHandler::loadPathFile(ReplayPathFile, replayPath); - } - std::unique_ptr handler = std::make_unique(pArgc, pArgv); @@ -2424,7 +2381,7 @@ int main(int argc, char **argv, char **envp) { externalsAndGlobalsCheck(finalModule); run_klee_on_function(pArgc, pArgv, pEnvp, handler, interpreter, finalModule, - mainFn, replayPath); + mainFn); paths.reset();