From 8228c8d39b868381e45808e6effe1e63072f36d9 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 14 Jul 2023 12:50:30 +0400 Subject: [PATCH 1/6] [feat] Add `TargetManager` [feat] Rework `TargetedSearcher` and `GuidedSearcher` [refactor] Refine the target's system --- configs/options.json | 2 +- include/klee/Core/Interpreter.h | 4 +- include/klee/Core/TargetedExecutionReporter.h | 2 +- include/klee/Core/TerminationTypes.h | 7 +- include/klee/Expr/Expr.h | 2 +- include/klee/Module/SarifReport.h | 4 +- include/klee/Module/Target.h | 70 ++- include/klee/Module/TargetForest.h | 333 +++++----- include/klee/Module/TargetHash.h | 24 +- lib/Core/CMakeLists.txt | 1 + lib/Core/DistanceCalculator.cpp | 150 +++-- lib/Core/DistanceCalculator.h | 92 ++- lib/Core/ExecutionState.cpp | 62 +- lib/Core/ExecutionState.h | 76 ++- lib/Core/Executor.cpp | 140 +++-- lib/Core/Executor.h | 12 +- lib/Core/Searcher.cpp | 592 ++++-------------- lib/Core/Searcher.h | 116 ++-- lib/Core/StatsTracker.cpp | 8 +- lib/Core/TargetManager.cpp | 191 ++++++ lib/Core/TargetManager.h | 134 ++++ lib/Core/TargetedExecutionManager.cpp | 69 +- lib/Core/TargetedExecutionManager.h | 37 +- lib/Core/TargetedExecutionReporter.cpp | 5 +- lib/Core/UserSearcher.cpp | 15 +- lib/Expr/Expr.cpp | 2 +- lib/Module/SarifReport.cpp | 18 +- lib/Module/Target.cpp | 54 +- lib/Module/TargetForest.cpp | 193 +++--- lib/Module/TargetHash.cpp | 25 +- lib/Solver/ConcretizingSolver.cpp | 10 +- test/Feature/MemoryLimit.c | 4 +- test/Feature/MultipleReallocResolution.c | 2 +- test/Feature/RecursionPruning/sum.c | 4 +- ...Var_Alloc_in_Loop_Exit_in_Loop_BadCase01.c | 2 +- test/Industry/NullReturn_Scene_BadCase06.c | 4 +- test/Industry/fp_forward_null_address.c | 2 +- test/Industry/if2.c | 2 +- test/Industry/while_true.c | 4 +- tools/klee/main.cpp | 18 +- 40 files changed, 1369 insertions(+), 1123 deletions(-) create mode 100644 lib/Core/TargetManager.cpp create mode 100644 lib/Core/TargetManager.h diff --git a/configs/options.json b/configs/options.json index 03a3849384..32f20ebbf7 100644 --- a/configs/options.json +++ b/configs/options.json @@ -41,7 +41,7 @@ "--use-lazy-initialization=only", "--min-number-elements-li=${minNumberElements}", "--use-sym-size-li=${useSymbolicSizeLI}", - "--max-cycles=${maxCycles}", + "--max-cycles-before-stuck=${maxCycles}", "--rewrite-equalities=simple", "--symbolic-allocation-threshold=${SymbolicAllocationThreshold}", "--analysis-reproduce=${sarifTracesFilePath}", diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 5cd177ca00..6c7ff2f878 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -57,8 +57,8 @@ class InterpreterHandler { virtual void incPathsCompleted() = 0; virtual void incPathsExplored(std::uint32_t num = 1) = 0; - virtual void processTestCase(const ExecutionState &state, const char *err, - const char *suffix) = 0; + virtual void processTestCase(const ExecutionState &state, const char *message, + const char *suffix, bool isError = false) = 0; }; class Interpreter { diff --git a/include/klee/Core/TargetedExecutionReporter.h b/include/klee/Core/TargetedExecutionReporter.h index e26c88ea72..01b87b4e80 100644 --- a/include/klee/Core/TargetedExecutionReporter.h +++ b/include/klee/Core/TargetedExecutionReporter.h @@ -30,7 +30,7 @@ ty min(ty left, ty right); }; // namespace confidence void reportFalsePositive(confidence::ty confidence, - const std::set &errors, + const std::vector &errors, const std::string &id, std::string whatToIncrease); } // namespace klee diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 787c6de2d1..16f665cfa8 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -39,7 +39,9 @@ enum class StateTerminationClass : std::uint8_t { TTYPE(MaxDepth, 11U, "early") \ TTYPE(OutOfMemory, 12U, "early") \ TTYPE(OutOfStackMemory, 13U, "early") \ - TTMARK(EARLY, 13U) \ + TTYPE(MaxCycles, 14U, "early") \ + TTYPE(MissedAllTargets, 15U, "miss_all_targets.early") \ + TTMARK(EARLY, 15U) \ TTYPE(Solver, 20U, "solver.err") \ TTMARK(SOLVERERR, 20U) \ TTYPE(Abort, 30U, "abort.err") \ @@ -68,8 +70,7 @@ enum class StateTerminationClass : std::uint8_t { TTYPE(External, 61U, "external.err") \ TTMARK(EXECERR, 61U) \ TTYPE(Replay, 70U, "") \ - TTYPE(MissedAllTargets, 71U, "") \ - TTMARK(EARLYALGORITHM, 71U) \ + TTMARK(EARLYALGORITHM, 70U) \ TTYPE(SilentExit, 80U, "") \ TTMARK(EARLYUSER, 80U) \ TTMARK(END, 80U) diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index 1def248760..8e258b8f56 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -127,7 +127,7 @@ class Expr { }; static ExprCacheSet cachedExpressions; - static ref createCachedExpr(const ref &e); + static ref createCachedExpr(ref e); bool isCached = false; bool toBeCleared = false; diff --git a/include/klee/Module/SarifReport.h b/include/klee/Module/SarifReport.h index 2d4ab20f7c..09a59d4d25 100644 --- a/include/klee/Module/SarifReport.h +++ b/include/klee/Module/SarifReport.h @@ -54,7 +54,7 @@ enum ReachWithError { }; const char *getErrorString(ReachWithError error); -std::string getErrorsString(const std::set &errors); +std::string getErrorsString(const std::vector &errors); struct FunctionInfo; struct KBlock; @@ -264,7 +264,7 @@ struct Result { std::vector> locations; std::vector> metadatas; std::string id; - std::set errors; + std::vector errors; }; struct SarifReport { diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h index b43726ab94..f075cafe99 100644 --- a/include/klee/Module/Target.h +++ b/include/klee/Module/Target.h @@ -10,6 +10,8 @@ #ifndef KLEE_TARGET_H #define KLEE_TARGET_H +#include "klee/Module/TargetHash.h" + #include "klee/ADT/RNG.h" #include "klee/ADT/Ref.h" #include "klee/Module/KModule.h" @@ -32,10 +34,6 @@ DISABLE_WARNING_POP #include namespace klee { -struct EquivTargetCmp; -struct TargetHash; -struct TargetCmp; - using nonstd::optional; struct ErrorLocation { @@ -47,30 +45,59 @@ struct ErrorLocation { struct Target { private: - typedef std::unordered_set - EquivTargetHashSet; - typedef std::unordered_set TargetHashSet; - static EquivTargetHashSet cachedTargets; - static TargetHashSet targets; KBlock *block; - std::set + std::vector errors; // None - if it is not terminated in error trace std::string id; // "" - if it is not terminated in error trace optional loc; // TODO(): only for check in reportTruePositive - explicit Target(const std::set &_errors, + explicit Target(const std::vector &_errors, const std::string &_id, optional _loc, KBlock *_block) - : block(_block), errors(_errors), id(_id), loc(_loc) {} + : block(_block), errors(_errors), id(_id), loc(_loc) { + std::sort(errors.begin(), errors.end()); + } + + static ref createCachedTarget(ref target); + +protected: + friend class ref; + friend class ref; + + struct TargetHash { + unsigned operator()(Target *const t) const { return t->hash(); } + }; + + struct TargetCmp { + bool operator()(Target *const a, Target *const b) const { + return a->equals(*b); + } + }; - static ref getFromCacheOrReturn(Target *target); + typedef std::unordered_set CacheType; + + struct TargetCacheSet { + CacheType cache; + ~TargetCacheSet() { + while (cache.size() != 0) { + ref tmp = *cache.begin(); + tmp->isCached = false; + cache.erase(cache.begin()); + } + } + }; + + static TargetCacheSet cachedTargets; + bool isCached = false; + bool toBeCleared = false; + + /// @brief Required by klee::ref-managed objects + mutable class ReferenceCounter _refCount; public: bool isReported = false; - /// @brief Required by klee::ref-managed objects - class ReferenceCounter _refCount; - static ref create(const std::set &_errors, + static ref create(const std::vector &_errors, const std::string &_id, optional _loc, KBlock *_block); static ref create(KBlock *_block); @@ -93,13 +120,16 @@ struct Target { unsigned hash() const { return reinterpret_cast(block); } - const std::set &getErrors() const { return errors; } - bool isThatError(ReachWithError err) const; + const std::vector &getErrors() const { return errors; } + bool isThatError(ReachWithError err) const { + return std::find(errors.begin(), errors.end(), err) != errors.end(); + } bool shouldFailOnThisTarget() const { - return errors.count(ReachWithError::None) == 0; + return std::find(errors.begin(), errors.end(), ReachWithError::None) == + errors.end(); } - bool isTheSameAsIn(KInstruction *instr) const; + bool isTheSameAsIn(const KInstruction *instr) const; /// returns true if we cannot use CFG reachability checks /// from instr children to this target diff --git a/include/klee/Module/TargetForest.h b/include/klee/Module/TargetForest.h index e6ff066430..3a03b7cb84 100644 --- a/include/klee/Module/TargetForest.h +++ b/include/klee/Module/TargetForest.h @@ -26,32 +26,120 @@ #include namespace klee { -struct RefTargetHash; -struct RefTargetCmp; -struct TargetsHistoryHash; -struct EquivTargetsHistoryCmp; -struct TargetsHistoryCmp; -struct UnorderedTargetsSetHash; -struct UnorderedTargetsSetCmp; -struct EquivUnorderedTargetsSetCmp; -struct RefUnorderedTargetsSetHash; -struct RefUnorderedTargetsSetCmp; +struct TargetHash; +struct TargetCmp; + +class TargetsHistory { +private: + unsigned hashValue; + unsigned sizeValue; + + explicit TargetsHistory(ref _target, + ref _visitedTargets) + : target(_target), visitedTargets(_visitedTargets) { + computeHash(); + computeSize(); + } + + void computeHash() { + unsigned res = 0; + if (target) { + res = target->hash() * Expr::MAGIC_HASH_CONSTANT; + } + if (visitedTargets) { + res ^= visitedTargets->hash() * Expr::MAGIC_HASH_CONSTANT; + } + hashValue = res; + } + + void computeSize() { + unsigned res = 0; + if (target) { + ++res; + } + if (visitedTargets) { + res += visitedTargets->size(); + } + sizeValue = res; + } + +protected: + friend class ref; + friend class ref; + + struct TargetsHistoryHash { + unsigned operator()(TargetsHistory *const t) const { return t->hash(); } + }; + + struct TargetsHistoryCmp { + bool operator()(TargetsHistory *const a, TargetsHistory *const b) const { + return a->equals(*b); + } + }; + + typedef std::unordered_set + CacheType; + + struct TargetHistoryCacheSet { + CacheType cache; + ~TargetHistoryCacheSet() { + while (cache.size() != 0) { + ref tmp = *cache.begin(); + tmp->isCached = false; + cache.erase(cache.begin()); + } + } + }; + + static TargetHistoryCacheSet cachedHistories; + bool isCached = false; + bool toBeCleared = false; + + /// @brief Required by klee::ref-managed objects + mutable class ReferenceCounter _refCount; -class TargetForest { public: - using TargetsSet = - std::unordered_set, RefTargetHash, RefTargetCmp>; + const ref target; + const ref visitedTargets; + + static ref create(ref _target, + ref _visitedTargets); + static ref create(ref _target); + static ref create(); + + ref add(ref _target) { + return TargetsHistory::create(_target, this); + } + + unsigned hash() const { return hashValue; } + unsigned size() const { return sizeValue; } + + int compare(const TargetsHistory &h) const; + bool equals(const TargetsHistory &h) const; + void dump() const; + + ~TargetsHistory(); +}; + +using TargetHistoryTargetPair = + std::pair, ref>; + +class TargetForest { +public: class UnorderedTargetsSet { public: static ref create(const ref &target); - static ref create(const TargetsSet &targets); + static ref create(const TargetHashSet &targets); ~UnorderedTargetsSet(); - std::size_t hash() const { return hashValue; } - bool operator==(const UnorderedTargetsSet &other) const { - return targetsVec == other.targetsVec; - } + unsigned hash() const { return hashValue; } + bool operator==(const UnorderedTargetsSet &other) const; + bool operator<(const UnorderedTargetsSet &other) const; + + int compare(const UnorderedTargetsSet &h) const; + bool equals(const UnorderedTargetsSet &h) const; const std::vector> &getTargets() const { return targetsVec; } @@ -66,54 +154,77 @@ class TargetForest { /// @brief Required by klee::ref-managed objects class ReferenceCounter _refCount; - private: - explicit UnorderedTargetsSet(const ref &target); - explicit UnorderedTargetsSet(const TargetsSet &targets); - static ref create(UnorderedTargetsSet *vec); + protected: + struct UnorderedTargetsSetHash { + unsigned operator()(UnorderedTargetsSet *const t) const { + return t->hash(); + } + }; + + struct UnorderedTargetsSetCmp { + bool operator()(UnorderedTargetsSet *const a, + UnorderedTargetsSet *const b) const { + return a->equals(*b); + } + }; - typedef std::unordered_set - EquivUnorderedTargetsSetHashSet; typedef std::unordered_set - UnorderedTargetsSetHashSet; + CacheType; + + struct UnorderedTargetsSetCacheSet { + CacheType cache; + ~UnorderedTargetsSetCacheSet() { + while (cache.size() != 0) { + ref tmp = *cache.begin(); + tmp->isCached = false; + cache.erase(cache.begin()); + } + } + }; + + static UnorderedTargetsSetCacheSet cachedVectors; + bool isCached = false; + bool toBeCleared = false; + + private: + explicit UnorderedTargetsSet(const ref &target); + explicit UnorderedTargetsSet(const TargetHashSet &targets); + static ref create(ref vec); - static EquivUnorderedTargetsSetHashSet cachedVectors; - static UnorderedTargetsSetHashSet vectors; std::vector> targetsVec; - std::size_t hashValue; + unsigned hashValue; - void sortAndComputeHash(); + unsigned sortAndComputeHash(); }; - struct RefUnorderedTargetsSetHash { + struct UnorderedTargetsSetHash { unsigned operator()(const ref &t) const { return t->hash(); } }; - struct RefUnorderedTargetsSetCmp { + struct UnorderedTargetsSetCmp { bool operator()(const ref &a, const ref &b) const { - return a.get() == b.get(); + return a == b; } }; private: using TargetToStateSetMap = std::unordered_map, std::unordered_set, - RefTargetHash, RefTargetCmp>; + TargetHash, TargetCmp>; class Layer { using InternalLayer = std::unordered_map, ref, - RefUnorderedTargetsSetHash, - RefUnorderedTargetsSetCmp>; + UnorderedTargetsSetHash, UnorderedTargetsSetCmp>; InternalLayer forest; using TargetsToVector = std::unordered_map< ref, - std::unordered_set, RefUnorderedTargetsSetHash, - RefUnorderedTargetsSetCmp>, - RefTargetHash, RefTargetCmp>; + std::unordered_set, UnorderedTargetsSetHash, + UnorderedTargetsSetCmp>, + TargetHash, TargetCmp>; TargetsToVector targetsToVector; /// @brief Confidence in % that this layer (i.e., parent target node) can be @@ -124,6 +235,7 @@ class TargetForest { confidence::ty confidence) : forest(forest), targetsToVector(targetsToVector), confidence(confidence) {} + explicit Layer(const Layer *layer) : Layer(layer->forest, layer->targetsToVector, layer->confidence) {} explicit Layer(const ref layer) : Layer(layer.get()) {} @@ -136,11 +248,6 @@ class TargetForest { return confidence::min(parentConfidence, confidence); } - void collectHowManyEventsInTracesWereReached( - std::unordered_map> - &traceToEventCount, - unsigned reached, unsigned total) const; - public: using iterator = TargetsToVector::const_iterator; @@ -166,8 +273,8 @@ class TargetForest { Layer *replaceChildWith( ref child, const std::unordered_set, - RefUnorderedTargetsSetHash, - RefUnorderedTargetsSetCmp> &other) const; + UnorderedTargetsSetHash, + UnorderedTargetsSetCmp> &other) const; Layer *replaceChildWith(ref child, Layer *other) const; Layer *removeChild(ref child) const; Layer *addChild(ref child) const; @@ -175,13 +282,19 @@ class TargetForest { ref leaf) const; Layer *blockLeafInChild(ref child, ref leaf) const; Layer *blockLeaf(ref leaf) const; - bool allNodesRefCountOne() const; + TargetHashSet getTargets() const { + TargetHashSet targets; + for (auto &targetVect : targetsToVector) { + targets.insert(targetVect.first); + } + return targets; + } + void dump(unsigned n) const; void addLeafs( std::vector, confidence::ty>> &leafs, confidence::ty parentConfidence) const; void propagateConfidenceToChildren(); - void addTargetWithConfidence(ref target, confidence::ty confidence); ref deepCopy(); Layer *copy(); void divideConfidenceBy(unsigned factor); @@ -190,11 +303,6 @@ class TargetForest { confidence::ty getConfidence() const { return getConfidence(confidence::MaxConfidence); } - void collectHowManyEventsInTracesWereReached( - std::unordered_map> - &traceToEventCount) const { - collectHowManyEventsInTracesWereReached(traceToEventCount, 0, 0); - } void addTrace( const Result &result, @@ -204,84 +312,13 @@ class TargetForest { ref forest; - bool allNodesRefCountOne() const; - -public: - class History { - private: - typedef std::unordered_set - EquivTargetsHistoryHashSet; - typedef std::unordered_set - TargetsHistoryHashSet; - - static EquivTargetsHistoryHashSet cachedHistories; - static TargetsHistoryHashSet histories; - unsigned hashValue; - unsigned sizeValue; - - explicit History(ref _target, ref _visitedTargets) - : target(_target), visitedTargets(_visitedTargets) { - computeHash(); - } - - void computeHash() { - unsigned res = 0; - if (target) { - res = target->hash() * Expr::MAGIC_HASH_CONSTANT; - } - if (visitedTargets) { - res ^= visitedTargets->hash() * Expr::MAGIC_HASH_CONSTANT; - } - hashValue = res; - } - - void computeSize() { - unsigned res = 0; - if (target) { - ++res; - } - if (visitedTargets) { - res += visitedTargets->size(); - } - sizeValue = res; - } - - public: - const ref target; - const ref visitedTargets; - - static ref create(ref _target, - ref _visitedTargets); - static ref create(ref _target); - static ref create(); - - ref add(ref _target) { - return History::create(_target, this); - } - - unsigned hash() const { return hashValue; } - unsigned size() const { return sizeValue; } - - int compare(const History &h) const; - bool equals(const History &h) const; - - void dump() const; - - ~History(); - - /// @brief Required by klee::ref-managed objects - class ReferenceCounter _refCount; - }; - private: - ref history; + ref history; KFunction *entryFunction; public: /// @brief Required by klee::ref-managed objects class ReferenceCounter _refCount; - unsigned getDebugReferenceCount() { return forest->_refCount.getCount(); } KFunction *getEntryFunction() { return entryFunction; } void addTrace( @@ -292,7 +329,7 @@ class TargetForest { } TargetForest(ref layer, KFunction *entryFunction) - : forest(layer), history(History::create()), + : forest(layer), history(TargetsHistory::create()), entryFunction(entryFunction) {} TargetForest() : TargetForest(new Layer(), nullptr) {} TargetForest(KFunction *entryFunction) @@ -312,14 +349,12 @@ class TargetForest { void remove(ref); void blockIn(ref, ref); void block(const ref &); - const ref getHistory() { return history; }; - const ref getTargets() { return forest; }; + const ref getHistory() { return history; }; + const ref getTopLayer() { return forest; }; + const TargetHashSet getTargets() const { return forest->getTargets(); } void dump() const; std::vector, confidence::ty>> leafs() const; - void addTargetWithConfidence(ref target, confidence::ty confidence) { - forest->addTargetWithConfidence(target, confidence); - } ref deepCopy(); void divideConfidenceBy(unsigned factor) { forest->divideConfidenceBy(factor); @@ -327,45 +362,29 @@ class TargetForest { void divideConfidenceBy(const TargetToStateSetMap &reachableStatesOfTarget) { forest = forest->divideConfidenceBy(reachableStatesOfTarget); } - void collectHowManyEventsInTracesWereReached( - std::unordered_map> - &traceToEventCount) const { - forest->collectHowManyEventsInTracesWereReached(traceToEventCount); - } }; struct TargetsHistoryHash { - unsigned operator()(const TargetForest::History *t) const { - return t ? t->hash() : 0; - } + unsigned operator()(const ref &t) const { return t->hash(); } }; struct TargetsHistoryCmp { - bool operator()(const TargetForest::History *a, - const TargetForest::History *b) const { + bool operator()(const ref &a, + const ref &b) const { return a == b; } }; -struct EquivTargetsHistoryCmp { - bool operator()(const TargetForest::History *a, - const TargetForest::History *b) const { - if (a == NULL || b == NULL) - return false; - return a->compare(*b) == 0; - } -}; - -struct RefTargetsHistoryHash { - unsigned operator()(const ref &t) const { - return t->hash(); +struct TargetHistoryTargetHash { + unsigned operator()(const TargetHistoryTargetPair &t) const { + return t.first->hash() * Expr::MAGIC_HASH_CONSTANT + t.second->hash(); } }; -struct RefTargetsHistoryCmp { - bool operator()(const ref &a, - const ref &b) const { - return a.get() == b.get(); +struct TargetHistoryTargetCmp { + bool operator()(const TargetHistoryTargetPair &a, + const TargetHistoryTargetPair &b) const { + return a.first == b.first && a.second == b.second; } }; diff --git a/include/klee/Module/TargetHash.h b/include/klee/Module/TargetHash.h index a484b521a7..2ceb35c747 100644 --- a/include/klee/Module/TargetHash.h +++ b/include/klee/Module/TargetHash.h @@ -24,22 +24,10 @@ namespace klee { struct Target; struct TargetHash { - unsigned operator()(const Target *t) const; -}; - -struct TargetCmp { - bool operator()(const Target *a, const Target *b) const; -}; - -struct EquivTargetCmp { - bool operator()(const Target *a, const Target *b) const; -}; - -struct RefTargetHash { unsigned operator()(const ref &t) const; }; -struct RefTargetCmp { +struct TargetCmp { bool operator()(const ref &a, const ref &b) const; }; @@ -49,18 +37,16 @@ struct TransitionHash { std::size_t operator()(const Transition &p) const; }; -struct RefTargetLess { +struct TargetLess { bool operator()(const ref &a, const ref &b) const { - return a.get() < b.get(); + return a < b; } }; template -class TargetHashMap - : public std::unordered_map, T, RefTargetHash, RefTargetCmp> {}; +using TargetHashMap = std::unordered_map, T, TargetHash, TargetCmp>; -class TargetHashSet - : public std::unordered_set, RefTargetHash, RefTargetCmp> {}; +using TargetHashSet = std::unordered_set, TargetHash, TargetCmp>; } // namespace klee #endif /* KLEE_TARGETHASH_H */ diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index edcd9eeb5b..9d94da9169 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -30,6 +30,7 @@ add_library(kleeCore TargetCalculator.cpp TargetedExecutionReporter.cpp TargetedExecutionManager.cpp + TargetManager.cpp TimingSolver.cpp TypeManager.cpp UserSearcher.cpp diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index 08c8caf64e..98433ff0c6 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -40,21 +40,73 @@ std::string DistanceResult::toString() const { return out.str(); } -DistanceResult DistanceCalculator::getDistance(ExecutionState &es, +unsigned DistanceCalculator::SpeculativeState::computeHash() { + unsigned res = + (reinterpret_cast(kb) * SymbolicSource::MAGIC_HASH_CONSTANT) + + kind; + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + error; + hashValue = res; + return hashValue; +} + +DistanceResult DistanceCalculator::getDistance(const ExecutionState &state, + ref target) { + return getDistance(state.prevPC, state.pc, state.frames, state.error, target); +} + +DistanceResult DistanceCalculator::getDistance(KBlock *kb, TargetKind kind, + ReachWithError error, ref target) { - return getDistance(es.pc, es.prevPC, es.initPC, es.stack, es.error, target); + SpeculativeState specState(kb, kind, error); + if (distanceResultCache.count(target) == 0 || + distanceResultCache.at(target).count(specState) == 0) { + auto result = computeDistance(kb, kind, error, target); + distanceResultCache[target][specState] = result; + } + return distanceResultCache.at(target).at(specState); +} + +DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind, + ReachWithError error, + ref target) const { + const auto &distanceToTargetFunction = + codeGraphDistance.getBackwardDistance(target->getBlock()->parent); + weight_type weight = 0; + WeightResult res = Miss; + bool isInsideFunction = true; + switch (kind) { + case LocalTarget: + res = tryGetTargetWeight(kb, weight, target); + break; + + case PreTarget: + res = tryGetPreTargetWeight(kb, weight, distanceToTargetFunction, target); + isInsideFunction = false; + break; + + case PostTarget: + res = tryGetPostTargetWeight(kb, weight, target); + isInsideFunction = false; + break; + + case NoneTarget: + break; + } + if (Done == res && target->shouldFailOnThisTarget()) { + if (!target->isThatError(error)) { + res = Continue; + } + } + return DistanceResult(res, weight, isInsideFunction); } DistanceResult -DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, - KInstruction *initPC, - const ExecutionState::stack_ty &stack, +DistanceCalculator::getDistance(const KInstruction *prevPC, + const KInstruction *pc, + const ExecutionState::frames_ty &frames, ReachWithError error, ref target) { weight_type weight = 0; - BasicBlock *pcBlock = pc->inst->getParent(); - BasicBlock *prevPCBlock = prevPC->inst->getParent(); - if (!target->shouldFailOnThisTarget() && target->atReturn()) { if (prevPC->parent == target->getBlock() && prevPC == target->getBlock()->getLastInstruction()) { @@ -69,12 +121,11 @@ DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, return DistanceResult(Done); } - BasicBlock *bb = pcBlock; - KBlock *kb = pc->parent->parent->blockMap[bb]; + KBlock *kb = pc->parent; const auto &distanceToTargetFunction = codeGraphDistance.getBackwardDistance(target->getBlock()->parent); unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0; - auto sfi = stack.rbegin(), sfe = stack.rend(); + auto sfi = frames.rbegin(), sfe = frames.rend(); bool strictlyAfterKB = sfi != sfe && (!target->shouldFailOnThisTarget() || sfi->kf->parent->inMainModule(sfi->kf->function)); @@ -85,7 +136,7 @@ DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, callWeight *= 2; callWeight += sfNum; - if (callWeight < minCallWeight) { + if (callWeight < UINT_MAX) { minCallWeight = callWeight; minSfNum = sfNum; } @@ -93,41 +144,31 @@ DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, if (sfi->caller) { kb = sfi->caller->parent; - bb = kb->basicBlock; } sfNum++; - if (minCallWeight < sfNum) + if (minCallWeight < UINT_MAX) break; } - WeightResult res = Miss; - bool isInsideFunction = true; + TargetKind kind = NoneTarget; if (minCallWeight == 0) { - res = tryGetTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, target); + kind = LocalTarget; } else if (minSfNum == 0) { - res = tryGetPreTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, - distanceToTargetFunction, target); - isInsideFunction = false; + kind = PreTarget; } else if (minSfNum != UINT_MAX) { - res = tryGetPostTargetWeight(pc, initPC, pcBlock, prevPCBlock, weight, - target); - isInsideFunction = false; - } - if (Done == res && target->shouldFailOnThisTarget()) { - if (!target->isThatError(error)) { - res = Continue; - } + kind = PostTarget; } - return DistanceResult(res, weight, isInsideFunction); + return getDistance(pc->parent, kind, error, target); } bool DistanceCalculator::distanceInCallGraph( KFunction *kf, KBlock *origKB, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target, bool strictlyAfterKB) { + ref target, bool strictlyAfterKB) const { + distance = UINT_MAX; const std::unordered_map &dist = codeGraphDistance.getDistance(origKB); KBlock *targetBB = target->getBlock(); @@ -157,7 +198,7 @@ bool DistanceCalculator::distanceInCallGraph( KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target) { + ref target) const { distance = UINT_MAX; const std::unordered_map &dist = codeGraphDistance.getDistance(kb); @@ -176,14 +217,12 @@ bool DistanceCalculator::distanceInCallGraph( return distance != UINT_MAX; } -WeightResult DistanceCalculator::tryGetLocalWeight( - KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, - BasicBlock *prevPCBlock, weight_type &weight, - const std::vector &localTargets, ref target) { - KFunction *currentKF = pc->parent->parent; - KBlock *initKB = initPC->parent; - KBlock *currentKB = currentKF->blockMap[pcBlock]; - KBlock *prevKB = currentKF->blockMap[prevPCBlock]; +WeightResult +DistanceCalculator::tryGetLocalWeight(KBlock *kb, weight_type &weight, + const std::vector &localTargets, + ref target) const { + KFunction *currentKF = kb->parent; + KBlock *currentKB = kb; const std::unordered_map &dist = codeGraphDistance.getDistance(currentKB); weight = UINT_MAX; @@ -196,8 +235,7 @@ WeightResult DistanceCalculator::tryGetLocalWeight( if (weight == UINT_MAX) return Miss; - if (weight == 0 && (initKB == currentKB || prevKB != currentKB || - target->shouldFailOnThisTarget())) { + if (weight == 0) { return Done; } @@ -205,12 +243,11 @@ WeightResult DistanceCalculator::tryGetLocalWeight( } WeightResult DistanceCalculator::tryGetPreTargetWeight( - KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, - BasicBlock *prevPCBlock, weight_type &weight, + KBlock *kb, weight_type &weight, const std::unordered_map &distanceToTargetFunction, - ref target) { - KFunction *currentKF = pc->parent->parent; + ref target) const { + KFunction *currentKF = kb->parent; std::vector localTargets; for (auto &kCallBlock : currentKF->kCallBlocks) { for (auto &calledFunction : kCallBlock->calledFunctions) { @@ -225,30 +262,27 @@ WeightResult DistanceCalculator::tryGetPreTargetWeight( if (localTargets.empty()) return Miss; - WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, - localTargets, target); + WeightResult res = tryGetLocalWeight(kb, weight, localTargets, target); return res == Done ? Continue : res; } -WeightResult DistanceCalculator::tryGetPostTargetWeight( - KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, - BasicBlock *prevPCBlock, weight_type &weight, ref target) { - KFunction *currentKF = pc->parent->parent; +WeightResult +DistanceCalculator::tryGetPostTargetWeight(KBlock *kb, weight_type &weight, + ref target) const { + KFunction *currentKF = kb->parent; std::vector &localTargets = currentKF->returnKBlocks; if (localTargets.empty()) return Miss; - WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, - localTargets, target); + WeightResult res = tryGetLocalWeight(kb, weight, localTargets, target); return res == Done ? Continue : res; } -WeightResult DistanceCalculator::tryGetTargetWeight( - KInstruction *pc, KInstruction *initPC, BasicBlock *pcBlock, - BasicBlock *prevPCBlock, weight_type &weight, ref target) { +WeightResult DistanceCalculator::tryGetTargetWeight(KBlock *kb, + weight_type &weight, + ref target) const { std::vector localTargets = {target->getBlock()}; - WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, - localTargets, target); + WeightResult res = tryGetLocalWeight(kb, weight, localTargets, target); return res; } diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h index 8d8ae38add..d791680f1f 100644 --- a/lib/Core/DistanceCalculator.h +++ b/lib/Core/DistanceCalculator.h @@ -48,44 +48,90 @@ class DistanceCalculator { explicit DistanceCalculator(CodeGraphDistance &codeGraphDistance_) : codeGraphDistance(codeGraphDistance_) {} - DistanceResult getDistance(ExecutionState &es, ref target); - DistanceResult getDistance(KInstruction *pc, KInstruction *prevPC, - KInstruction *initPC, - const ExecutionState::stack_ty &stack, + DistanceResult getDistance(const ExecutionState &es, ref target); + + DistanceResult getDistance(const KInstruction *prevPC, const KInstruction *pc, + const ExecutionState::frames_ty &frames, ReachWithError error, ref target); private: + enum TargetKind : std::uint8_t { + LocalTarget = 0U, + PreTarget = 1U, + PostTarget = 2U, + NoneTarget = 3U, + }; + + struct SpeculativeState { + private: + unsigned hashValue; + + unsigned computeHash(); + + public: + KBlock *kb; + TargetKind kind; + ReachWithError error; + SpeculativeState(KBlock *kb_, TargetKind kind_, ReachWithError error_) + : kb(kb_), kind(kind_), error(error_) { + computeHash(); + } + ~SpeculativeState() = default; + unsigned hash() const { return hashValue; } + }; + + struct SpeculativeStateHash { + bool operator()(const SpeculativeState &a) const { return a.hash(); } + }; + + struct SpeculativeStateCompare { + bool operator()(const SpeculativeState &a, + const SpeculativeState &b) const { + return a.kb == b.kb && a.error == b.error && a.kind == b.kind; + } + }; + + using SpeculativeStateToDistanceResultMap = + std::unordered_map; + using TargetToSpeculativeStateToDistanceResultMap = + std::unordered_map, SpeculativeStateToDistanceResultMap, + TargetHash, TargetCmp>; + + using StatesSet = std::unordered_set; + CodeGraphDistance &codeGraphDistance; + TargetToSpeculativeStateToDistanceResultMap distanceResultCache; + StatesSet localStates; + + DistanceResult getDistance(KBlock *kb, TargetKind kind, ReachWithError error, + ref target); + + DistanceResult computeDistance(KBlock *kb, TargetKind kind, + ReachWithError error, + ref target) const; bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target); + ref target) const; bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target, bool strictlyAfterKB); - WeightResult tryGetLocalWeight(KInstruction *pc, KInstruction *initPC, - llvm::BasicBlock *pcBlock, - llvm::BasicBlock *prevPCBlock, - weight_type &weight, + ref target, bool strictlyAfterKB) const; + + WeightResult tryGetLocalWeight(KBlock *kb, weight_type &weight, const std::vector &localTargets, - ref target); + ref target) const; WeightResult - tryGetPreTargetWeight(KInstruction *pc, KInstruction *initPC, - llvm::BasicBlock *pcBlock, - llvm::BasicBlock *prevPCBlock, weight_type &weight, + tryGetPreTargetWeight(KBlock *kb, weight_type &weight, const std::unordered_map &distanceToTargetFunction, - ref target); - WeightResult tryGetTargetWeight(KInstruction *pc, KInstruction *initPC, - llvm::BasicBlock *pcBlock, - llvm::BasicBlock *prevPCBlock, - weight_type &weight, ref target); - WeightResult tryGetPostTargetWeight(KInstruction *pc, KInstruction *initPC, - llvm::BasicBlock *pcBlock, - llvm::BasicBlock *prevPCBlock, - weight_type &weight, ref target); + ref target) const; + WeightResult tryGetTargetWeight(KBlock *kb, weight_type &weight, + ref target) const; + WeightResult tryGetPostTargetWeight(KBlock *kb, weight_type &weight, + ref target) const; }; } // namespace klee diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9288283849..b9806c8212 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -40,12 +40,21 @@ DISABLE_WARNING_POP using namespace llvm; using namespace klee; +namespace klee { +cl::opt MaxCyclesBeforeStuck( + "max-cycles-before-stuck", + cl::desc("Set target after after state visiting some basic block this " + "amount of times (default=1)."), + cl::init(1), cl::cat(TerminationCat)); +} + namespace { cl::opt UseGEPOptimization( "use-gep-opt", cl::init(true), cl::desc("Lazily initialize whole objects referenced by gep expressions " "instead of only the referenced parts (default=true)"), cl::cat(ExecCat)); + } // namespace /***/ @@ -54,6 +63,19 @@ std::uint32_t ExecutionState::nextID = 1; /***/ +int CallStackFrame::compare(const CallStackFrame &other) const { + if (kf != other.kf) { + return kf < other.kf ? -1 : 1; + } + if (!caller || !other.caller) { + return !caller ? !other.caller ? 0 : -1 : 1; + } + if (caller != other.caller) { + return caller < other.caller ? -1 : 1; + } + return 0; +} + StackFrame::StackFrame(KInstIterator _caller, KFunction *_kf) : caller(_caller), kf(_kf), callPathNode(0), minDistToUncoveredOnReturn(0), varargs(0) { @@ -78,13 +100,18 @@ ExecutionState::ExecutionState() depth(0), ptreeNode(nullptr), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false), - forkDisabled(false) { + forkDisabled(false), prevHistory_(TargetsHistory::create()), + history_(TargetsHistory::create()) { setID(); } ExecutionState::ExecutionState(KFunction *kf) - : initPC(kf->instructions), pc(initPC), prevPC(pc), - roundingMode(llvm::APFloat::rmNearestTiesToEven) { + : initPC(kf->instructions), pc(initPC), prevPC(pc), incomingBBIndex(-1), + depth(0), ptreeNode(nullptr), steppedInstructions(0), + steppedMemoryInstructions(0), instsSinceCovNew(0), + roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false), + forkDisabled(false), prevHistory_(TargetsHistory::create()), + history_(TargetsHistory::create()) { pushFrame(nullptr, kf); setID(); } @@ -94,7 +121,8 @@ ExecutionState::ExecutionState(KFunction *kf, KBlock *kb) depth(0), ptreeNode(nullptr), steppedInstructions(0), steppedMemoryInstructions(0), instsSinceCovNew(0), roundingMode(llvm::APFloat::rmNearestTiesToEven), coveredNew(false), - forkDisabled(false) { + forkDisabled(false), prevHistory_(TargetsHistory::create()), + history_(TargetsHistory::create()) { pushFrame(nullptr, kf); setID(); } @@ -106,9 +134,9 @@ ExecutionState::~ExecutionState() { ExecutionState::ExecutionState(const ExecutionState &state) : initPC(state.initPC), pc(state.pc), prevPC(state.prevPC), - stack(state.stack), stackBalance(state.stackBalance), - incomingBBIndex(state.incomingBBIndex), depth(state.depth), - multilevel(state.multilevel), level(state.level), + stack(state.stack), callStack(state.callStack), frames(state.frames), + stackBalance(state.stackBalance), incomingBBIndex(state.incomingBBIndex), + depth(state.depth), multilevel(state.multilevel), level(state.level), transitionLevel(state.transitionLevel), addressSpace(state.addressSpace), constraints(state.constraints), targetForest(state.targetForest), pathOS(state.pathOS), symPathOS(state.symPathOS), @@ -123,7 +151,10 @@ ExecutionState::ExecutionState(const ExecutionState &state) ? state.unwindingInformation->clone() : nullptr), coveredNew(state.coveredNew), forkDisabled(state.forkDisabled), - returnValue(state.returnValue), gepExprBases(state.gepExprBases) {} + returnValue(state.returnValue), gepExprBases(state.gepExprBases), + prevTargets_(state.prevTargets_), targets_(state.targets_), + prevHistory_(state.prevHistory_), history_(state.history_), + isTargeted_(state.isTargeted_) {} ExecutionState *ExecutionState::branch() { depth++; @@ -183,6 +214,11 @@ ExecutionState *ExecutionState::copy() const { void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) { stack.emplace_back(StackFrame(caller, kf)); + if (std::find(callStack.begin(), callStack.end(), + CallStackFrame(caller, kf)) == callStack.end()) { + frames.emplace_back(CallStackFrame(caller, kf)); + } + callStack.emplace_back(CallStackFrame(caller, kf)); ++stackBalance; } @@ -195,6 +231,12 @@ void ExecutionState::popFrame() { addressSpace.unbindObject(memoryObject); } stack.pop_back(); + callStack.pop_back(); + auto it = std::find(callStack.begin(), callStack.end(), + CallStackFrame(sf.caller, sf.kf)); + if (it == callStack.end()) { + frames.pop_back(); + } --stackBalance; } @@ -412,7 +454,7 @@ void ExecutionState::increaseLevel() { KModule *kmodule = kf->parent; if (prevPC->inst->isTerminator() && kmodule->inMainModule(kf->function)) { - multilevel[srcbb]++; + ++multilevel[srcbb]; level.insert(srcbb); } if (srcbb != dstbb) { @@ -420,8 +462,6 @@ void ExecutionState::increaseLevel() { } } -bool ExecutionState::isTransfered() { return getPrevPCBlock() != getPCBlock(); } - bool ExecutionState::isGEPExpr(ref expr) const { return UseGEPOptimization && gepExprBases.find(expr) != gepExprBases.end(); } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 3e4c9d3c2a..7c9ad8fd80 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -20,6 +20,7 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Module/KInstIterator.h" +#include "klee/Module/KInstruction.h" #include "klee/Module/Target.h" #include "klee/Module/TargetForest.h" #include "klee/Module/TargetHash.h" @@ -56,6 +57,27 @@ struct TranstionHash; llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); +extern llvm::cl::opt MaxCyclesBeforeStuck; + +struct CallStackFrame { + KInstruction *caller; + KFunction *kf; + + CallStackFrame(KInstruction *caller_, KFunction *kf_) + : caller(caller_), kf(kf_) {} + ~CallStackFrame() = default; + + int compare(const CallStackFrame &other) const; + + bool operator<(const CallStackFrame &other) const { + return compare(other) == -1; + } + + bool operator==(const CallStackFrame &other) const { + return compare(other) == 0; + } +}; + struct StackFrame { KInstIterator caller; KFunction *kf; @@ -208,8 +230,8 @@ class ExecutionState { public: using stack_ty = std::vector; - using TargetHashSet = - std::unordered_set, RefTargetHash, RefTargetCmp>; + using call_stack_ty = std::vector; + using frames_ty = std::vector; // Execution - Control Flow specific @@ -225,6 +247,8 @@ class ExecutionState { /// @brief Stack representing the current instruction stream stack_ty stack; + call_stack_ty callStack; + frames_ty frames; int stackBalance = 0; @@ -333,6 +357,14 @@ class ExecutionState { std::atomic terminationReasonType{ HaltExecution::NotHalt}; +private: + TargetHashSet prevTargets_; + TargetHashSet targets_; + ref prevHistory_; + ref history_; + bool isTargeted_ = false; + bool areTargetsChanged_ = false; + public: // only to create the initial state explicit ExecutionState(); @@ -388,11 +420,49 @@ class ExecutionState { llvm::BasicBlock *getPrevPCBlock() const; llvm::BasicBlock *getPCBlock() const; void increaseLevel(); - bool isTransfered(); + + inline bool isTransfered() { return getPrevPCBlock() != getPCBlock(); } + bool isGEPExpr(ref expr) const; + inline const TargetHashSet &prevTargets() const { return prevTargets_; } + + inline const TargetHashSet &targets() const { return targets_; } + + inline ref prevHistory() const { return prevHistory_; } + + inline ref history() const { return history_; } + + inline bool isTargeted() const { return isTargeted_; } + + inline bool areTargetsChanged() const { return areTargetsChanged_; } + + void stepTargetsAndHistory() { + prevHistory_ = history_; + prevTargets_ = targets_; + areTargetsChanged_ = false; + } + + inline void setTargeted(bool targeted) { isTargeted_ = targeted; } + + inline void setTargets(const TargetHashSet &targets) { + targets_ = targets; + areTargetsChanged_ = true; + } + + inline void setHistory(ref history) { + history_ = history; + areTargetsChanged_ = true; + } + bool reachedTarget(Target target) const; static std::uint32_t getLastID() { return nextID - 1; }; + + inline bool isStuck(unsigned long long bound) { + KInstruction *prevKI = prevPC; + return (prevKI->inst->isTerminator() && + multilevel[getPCBlock()] > bound - 1); + } }; struct ExecutionStateIDCompare { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d219f82761..03117c9c31 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -27,6 +27,7 @@ #include "SpecialFunctionHandler.h" #include "StatsTracker.h" #include "TargetCalculator.h" +#include "TargetManager.h" #include "TargetedExecutionManager.h" #include "TimingSolver.h" #include "TypeManager.h" @@ -458,10 +459,11 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, concretizationManager(new ConcretizationManager(EqualitySubstitution)), codeGraphDistance(new CodeGraphDistance()), distanceCalculator(new DistanceCalculator(*codeGraphDistance)), - targetedExecutionManager(*codeGraphDistance), replayKTest(0), - replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false), - haltExecution(HaltExecution::NotHalt), ivcEnabled(false), - debugLogBuffer(debugBufferString) { + targetedExecutionManager(new TargetedExecutionManager( + *codeGraphDistance, *distanceCalculator)), + replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), + inhibitForking(false), haltExecution(HaltExecution::NotHalt), + ivcEnabled(false), debugLogBuffer(debugBufferString) { guidanceKind = opts.Guidance; @@ -606,6 +608,12 @@ Executor::setModule(std::vector> &userModules, targetCalculator = std::unique_ptr( new TargetCalculator(*kmodule.get(), *codeGraphDistance.get())); + targetManager = std::unique_ptr(new TargetManager( + guidanceKind, *distanceCalculator.get(), *targetCalculator.get())); + + targetedExecutionManager = std::unique_ptr( + new TargetedExecutionManager(*codeGraphDistance, *distanceCalculator)); + return kmodule->module.get(); } @@ -1090,12 +1098,12 @@ bool Executor::canReachSomeTargetFromBlock(ExecutionState &es, KBlock *block) { if (interpreterOpts.Guidance != GuidanceKind::ErrorGuidance) return true; auto nextInstr = block->getFirstInstruction(); - for (const auto &p : *es.targetForest.getTargets()) { + for (const auto &p : *es.targetForest.getTopLayer()) { auto target = p.first; if (target->mustVisitForkBranches(es.prevPC)) return true; - auto dist = distanceCalculator->getDistance(nextInstr, es.prevPC, es.initPC, - es.stack, es.error, target); + auto dist = distanceCalculator->getDistance(es.prevPC, nextInstr, es.frames, + es.error, target); if (dist.result != WeightResult::Miss) return true; } @@ -1578,7 +1586,13 @@ void Executor::printDebugInstructions(ExecutionState &state) { if (state.pc->info->assemblyLine.hasValue()) { (*stream) << state.pc->info->assemblyLine.getValue() << ':'; } - (*stream) << state.getID(); + (*stream) << state.getID() << ":"; + (*stream) << "["; + for (auto target : state.targets()) { + (*stream) << target->toString() << ","; + } + (*stream) << "]"; + if (DebugPrintInstructions.isSet(STDERR_ALL) || DebugPrintInstructions.isSet(FILE_ALL)) (*stream) << ':' << *(state.pc->inst); @@ -3907,6 +3921,13 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } void Executor::updateStates(ExecutionState *current) { + if (targetManager) { + targetManager->update(current, addedStates, removedStates); + } + if (guidanceKind == GuidanceKind::ErrorGuidance && targetedExecutionManager) { + targetedExecutionManager->update(current, addedStates, removedStates); + } + if (searcher) { searcher->update(current, addedStates, removedStates); } @@ -4049,12 +4070,12 @@ bool Executor::checkMemoryUsage() { return false; } -bool Executor::decreaseConfidenceFromStoppedStates( - SetOfStates &left_states, HaltExecution::Reason reason) { - bool hasStateWhichCanReachSomeTarget = false; - if (targets.empty()) - return hasStateWhichCanReachSomeTarget; - for (auto state : left_states) { +void Executor::decreaseConfidenceFromStoppedStates( + SetOfStates &leftStates, HaltExecution::Reason reason) { + if (targets.size() == 0) { + return; + } + for (auto state : leftStates) { if (state->targetForest.empty()) continue; hasStateWhichCanReachSomeTarget = true; @@ -4065,7 +4086,6 @@ bool Executor::decreaseConfidenceFromStoppedStates( .subtractConfidencesFrom(state->targetForest, realReason); } } - return hasStateWhichCanReachSomeTarget; } void Executor::doDumpStates() { @@ -4178,7 +4198,7 @@ void Executor::reportProgressTowardsTargets(std::string prefix, klee_message("%zu %sstates remaining", states.size(), prefix.c_str()); TargetHashMap distancesTowardsTargets; for (auto &state : states) { - for (auto &p : *state->targetForest.getTargets()) { + for (auto &p : *state->targetForest.getTopLayer()) { auto target = p.first; auto distance = distanceCalculator->getDistance(*state, target); auto it = distancesTowardsTargets.find(target); @@ -4235,6 +4255,9 @@ void Executor::run(std::vector initialStates) { searcher = constructUserSearcher(*this); std::vector newStates(states.begin(), states.end()); + targetManager->update(0, newStates, std::vector()); + targetedExecutionManager->update(0, newStates, + std::vector()); searcher->update(0, newStates, std::vector()); // main interpreter loop @@ -4246,6 +4269,13 @@ void Executor::run(std::vector initialStates) { if (prevKI->inst->isTerminator() && kmodule->inMainModule(kf->function)) { targetCalculator->update(state); + auto target = Target::create(state.prevPC->parent); + if (guidanceKind == GuidanceKind::CoverageGuidance) { + if (!target->atReturn() || + state.prevPC == target->getBlock()->getLastInstruction()) { + targetManager->setReached(target); + } + } } executeStep(state); @@ -4256,20 +4286,12 @@ void Executor::run(std::vector initialStates) { } if (guidanceKind == GuidanceKind::ErrorGuidance) { - SetOfStates leftState = states; - for (auto state : pausedStates) { - leftState.erase(state); - } - reportProgressTowardsTargets(); - bool canReachNew1 = decreaseConfidenceFromStoppedStates( - pausedStates, HaltExecution::MaxCycles); - bool canReachNew2 = - decreaseConfidenceFromStoppedStates(leftState, haltExecution); + decreaseConfidenceFromStoppedStates(states, haltExecution); for (auto &startBlockAndWhiteList : targets) { - startBlockAndWhiteList.second.reportFalsePositives(canReachNew1 || - canReachNew2); + startBlockAndWhiteList.second.reportFalsePositives( + hasStateWhichCanReachSomeTarget); } if (searcher->empty()) @@ -4278,6 +4300,7 @@ void Executor::run(std::vector initialStates) { delete searcher; searcher = nullptr; + targetManager = nullptr; doDumpStates(); haltExecution = HaltExecution::NotHalt; @@ -4312,10 +4335,20 @@ void Executor::initializeTypeManager() { } void Executor::executeStep(ExecutionState &state) { - KInstruction *ki = state.pc; - stepInstruction(state); + KInstruction *prevKI = state.prevPC; + if (targetManager->isTargeted(state) && state.targets().empty()) { + terminateStateEarly(state, "State missed all it's targets.", + StateTerminationType::MissedAllTargets); + } else if (prevKI->inst->isTerminator() && + state.multilevel[state.getPCBlock()] > MaxCycles - 1) { + terminateStateEarly(state, "max-cycles exceeded.", + StateTerminationType::MaxCycles); + } else { + KInstruction *ki = state.pc; + stepInstruction(state); + executeInstruction(state, ki); + } - executeInstruction(state, ki); timers.invoke(); if (::dumpStates) dumpStates(); @@ -4445,6 +4478,10 @@ HaltExecution::Reason fromStateTerminationType(StateTerminationType t) { return HaltExecution::MaxStackFrames; case StateTerminationType::Solver: return HaltExecution::MaxSolverTime; + case StateTerminationType::MaxCycles: + return HaltExecution::MaxCycles; + case StateTerminationType::Interrupted: + return HaltExecution::Interrupt; default: return HaltExecution::Unspecified; } @@ -4453,6 +4490,11 @@ HaltExecution::Reason fromStateTerminationType(StateTerminationType t) { void Executor::terminateState(ExecutionState &state, StateTerminationType terminationType) { state.terminationReasonType = fromStateTerminationType(terminationType); + if (terminationType >= StateTerminationType::MaxDepth && + terminationType < StateTerminationType::MissedAllTargets) { + 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."); @@ -4512,7 +4554,9 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, (AlwaysOutputSeeds && seedMap.count(&state))) { interpreterHandler->processTestCase( state, (message + "\n").str().c_str(), - terminationTypeFileExtension(reason).c_str()); + terminationTypeFileExtension(reason).c_str(), + reason > StateTerminationType::EARLY && + reason <= StateTerminationType::EXECERR); } terminateState(state, reason); } @@ -4586,9 +4630,9 @@ void Executor::reportStateOnTargetError(ExecutionState &state, ReachWithError error) { if (guidanceKind == GuidanceKind::ErrorGuidance) { bool reportedTruePositive = - targetedExecutionManager.reportTruePositive(state, error); + targetedExecutionManager->reportTruePositive(state, error); if (!reportedTruePositive) { - targetedExecutionManager.reportFalseNegative(state, error); + targetedExecutionManager->reportFalseNegative(state, error); } } } @@ -4668,7 +4712,8 @@ void Executor::terminateStateOnError(ExecutionState &state, const std::string ext = terminationTypeFileExtension(terminationType); // use user provided suffix from klee_report_error() const char *file_suffix = suffix ? suffix : ext.c_str(); - interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix); + interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix, + true); } targetCalculator->update(state); @@ -4702,8 +4747,6 @@ void Executor::terminateStateOnSolverError(ExecutionState &state, const llvm::Twine &message) { ++stats::terminationSolverError; terminateStateOnError(state, message, StateTerminationType::Solver, ""); - SetOfStates states = {&state}; - decreaseConfidenceFromStoppedStates(states, HaltExecution::MaxSolverTime); } void Executor::terminateStateOnUserError(ExecutionState &state, @@ -6565,7 +6608,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, if (guidanceKind == GuidanceKind::ErrorGuidance) { auto &paths = interpreterOpts.Paths.value(); - auto prepTargets = targetedExecutionManager.prepareTargets( + auto prepTargets = targetedExecutionManager->prepareTargets( kmodule.get(), std::move(paths)); if (prepTargets.empty()) { klee_warning( @@ -6593,7 +6636,7 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv, targets.emplace(kf, TargetedHaltsOnTraces(whitelist)); ExecutionState *initialState = state->withStackFrame(caller, kf); prepareSymbolicArgs(*initialState); - prepareTargetedExecution(initialState, whitelist); + prepareTargetedExecution(*initialState, whitelist); states.push_back(initialState); } delete state; @@ -6657,7 +6700,9 @@ ExecutionState *Executor::prepareStateForPOSIX(KInstIterator &caller, processForest->addRoot(state); ExecutionState *original = state->copy(); ExecutionState *initialState = nullptr; - state->targetForest.add(Target::create(target)); + ref targets(new TargetForest()); + targets->add(Target::create(target)); + prepareTargetedExecution(*state, targets); targetedRun(*state, target, &initialState); state = initialState; if (state) { @@ -6678,9 +6723,12 @@ ExecutionState *Executor::prepareStateForPOSIX(KInstIterator &caller, return state; } -void Executor::prepareTargetedExecution(ExecutionState *initialState, +void Executor::prepareTargetedExecution(ExecutionState &initialState, ref whitelist) { - initialState->targetForest = *whitelist->deepCopy(); + initialState.targetForest = *whitelist->deepCopy(); + initialState.setTargeted(true); + initialState.setHistory(initialState.targetForest.getHistory()); + initialState.setTargets(initialState.targetForest.getTargets()); } bool isReturnValueFromInitBlock(const ExecutionState &state, @@ -6892,14 +6940,14 @@ void Executor::setInitializationGraph(const ExecutionState &state, continue; } - ref update_check; + ref updateCheck; if (auto e = dyn_cast(pointer.first)) { - update_check = e->getLeft(); + updateCheck = e->getLeft(); } else { - update_check = e; + updateCheck = e; } - if (auto e = dyn_cast(update_check)) { + if (auto e = dyn_cast(updateCheck)) { if (e->updates.getSize() != 0) { continue; } @@ -6932,7 +6980,7 @@ void Executor::setInitializationGraph(const ExecutionState &state, if (s[pointerIndex].count(o.offset) && s[pointerIndex][o.offset] != std::make_pair(o.index, o.indexOffset)) { - assert(0 && "wft"); + assert(0 && "unreachable"); } if (!s[pointerIndex].count(o.offset)) { pointers[pointerIndex].push_back(o); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 582c22f0f0..1f3298e5ea 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -95,6 +95,7 @@ class SpecialFunctionHandler; struct StackFrame; class SymbolicSource; class TargetCalculator; +class TargetManager; class StatsTracker; class TimingSolver; class TreeStreamWriter; @@ -149,6 +150,7 @@ class Executor : public Interpreter { std::unique_ptr codeGraphDistance; std::unique_ptr distanceCalculator; std::unique_ptr targetCalculator; + std::unique_ptr targetManager; /// Used to track states that have been added during the current /// instructions step. @@ -182,7 +184,7 @@ class Executor : public Interpreter { std::unordered_map legalFunctions; /// Manager for everything related to targeted execution mode - TargetedExecutionManager targetedExecutionManager; + std::unique_ptr targetedExecutionManager; /// When non-null the bindings that will be used for calls to /// klee_make_symbolic in order replay. @@ -243,6 +245,8 @@ class Executor : public Interpreter { GuidanceKind guidanceKind; + bool hasStateWhichCanReachSomeTarget = false; + /// Return the typeid corresponding to a certain `type_info` ref getEhTypeidFor(ref type_info); @@ -645,13 +649,13 @@ class Executor : public Interpreter { ExecutionState *prepareStateForPOSIX(KInstIterator &caller, ExecutionState *state); - void prepareTargetedExecution(ExecutionState *initialState, + void prepareTargetedExecution(ExecutionState &initialState, ref whitelist); void increaseProgressVelocity(ExecutionState &state, KBlock *block); - bool decreaseConfidenceFromStoppedStates( - SetOfStates &left_states, + void decreaseConfidenceFromStoppedStates( + SetOfStates &leftStates, HaltExecution::Reason reason = HaltExecution::NotHalt); void checkNullCheckAfterDeref(ref cond, ExecutionState &state, diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 7b164f7e2f..a89396b2ea 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -152,6 +152,14 @@ static unsigned int ulog2(unsigned int val) { /// +TargetedSearcher::~TargetedSearcher() {} + +bool TargetedSearcher::empty() { return states->empty(); } + +void TargetedSearcher::printName(llvm::raw_ostream &os) { + os << "TargetedSearcher"; +} + TargetedSearcher::TargetedSearcher(ref target, DistanceCalculator &_distanceCalculator) : states(std::make_unique< @@ -160,555 +168,189 @@ TargetedSearcher::TargetedSearcher(ref target, ExecutionState &TargetedSearcher::selectState() { return *states->choose(0); } -WeightResult TargetedSearcher::tryGetWeight(ExecutionState *es, - weight_type &weight) { - BasicBlock *bb = es->getPCBlock(); - KBlock *kb = es->pc->parent->parent->blockMap[bb]; - KInstruction *ki = es->pc; - if (!target->shouldFailOnThisTarget() && kb->numInstructions && - !isa(kb) && kb->getFirstInstruction() != ki && - states->tryGetWeight(es, weight)) { - return Continue; - } - - auto distRes = distanceCalculator.getDistance(*es, target); - weight = ulog2(distRes.weight + es->steppedMemoryInstructions); // [0, 32] - if (!distRes.isInsideFunction) { - weight += 32; // [32, 64] - } - - return distRes.result; -} - void TargetedSearcher::update( ExecutionState *current, const std::vector &addedStates, const std::vector &removedStates) { - updateCheckCanReach(current, addedStates, removedStates); -} - -bool TargetedSearcher::updateCheckCanReach( - ExecutionState *current, const std::vector &addedStates, - const std::vector &removedStates) { - weight_type weight = 0; - bool canReach = false; // update current if (current && std::find(removedStates.begin(), removedStates.end(), - current) == removedStates.end()) { - switch (tryGetWeight(current, weight)) { - case Continue: - states->update(current, weight); - canReach = true; - break; - case Done: - reachedOnLastUpdate.insert(current); - canReach = true; - break; - case Miss: - current->targetForest.remove(target); - states->remove(current); - break; - } - } + current) == removedStates.end()) + states->update(current, getWeight(current)); // insert states - for (const auto state : addedStates) { - switch (tryGetWeight(state, weight)) { - case Continue: - states->insert(state, weight); - canReach = true; - break; - case Done: - states->insert(state, weight); - reachedOnLastUpdate.insert(state); - canReach = true; - break; - case Miss: - state->targetForest.remove(target); - break; - } - } + for (const auto state : addedStates) + states->insert(state, getWeight(state)); // remove states - for (const auto state : removedStates) { - if (target->atReturn() && !target->shouldFailOnThisTarget() && - state->prevPC == target->getBlock()->getLastInstruction()) { - canReach = true; - reachedOnLastUpdate.insert(state); - } else { - switch (tryGetWeight(state, weight)) { - case Done: - reachedOnLastUpdate.insert(state); - canReach = true; - break; - case Miss: - state->targetForest.remove(target); - states->remove(state); - break; - case Continue: - states->remove(state); - canReach = true; - break; - } - } - } - return canReach; -} - -bool TargetedSearcher::empty() { return states->empty(); } - -void TargetedSearcher::printName(llvm::raw_ostream &os) { - os << "TargetedSearcher"; + for (const auto state : removedStates) + states->remove(state); } -TargetedSearcher::~TargetedSearcher() { - while (!states->empty()) { - auto &state = selectState(); - state.targetForest.remove(target); - states->remove(&state); +weight_type TargetedSearcher::getWeight(ExecutionState *es) { + KBlock *kb = es->pc->parent; + KInstruction *ki = es->pc; + weight_type weight; + if (!target->shouldFailOnThisTarget() && kb->numInstructions && + !isa(kb) && kb->getFirstInstruction() != ki && + states->tryGetWeight(es, weight)) { + return weight; } -} - -std::set TargetedSearcher::reached() { - return reachedOnLastUpdate; -} - -void TargetedSearcher::removeReached() { - for (auto state : reachedOnLastUpdate) { - states->remove(state); - state->targetForest.stepTo(target); + auto distRes = distanceCalculator.getDistance(*es, target); + weight = ulog2(distRes.weight + es->steppedMemoryInstructions + 1); // [0, 32) + if (!distRes.isInsideFunction) { + weight += 32; // [32, 64) } - reachedOnLastUpdate.clear(); + return weight; } /// -GuidedSearcher::GuidedSearcher( - DistanceCalculator &distanceCalculator, TargetCalculator &stateHistory, - std::set &pausedStates, - unsigned long long bound, RNG &rng, Searcher *baseSearcher) - : baseSearcher(baseSearcher), distanceCalculator(distanceCalculator), - stateHistory(stateHistory), pausedStates(pausedStates), bound(bound), - theRNG(rng) { - guidance = baseSearcher ? CoverageGuidance : ErrorGuidance; -} - ExecutionState &GuidedSearcher::selectState() { unsigned size = historiesAndTargets.size(); index = theRNG.getInt32() % (size + 1); ExecutionState *state = nullptr; - if (CoverageGuidance == guidance && index == size) { + if (index == size) { state = &baseSearcher->selectState(); } else { index = index % size; auto &historyTargetPair = historiesAndTargets[index]; - ref history = historyTargetPair.first; + ref history = historyTargetPair.first; ref target = historyTargetPair.second; - assert(targetedSearchers.find(history) != targetedSearchers.end() && - targetedSearchers.at(history).find(target) != - targetedSearchers.at(history).end() && - !targetedSearchers.at(history)[target]->empty()); - state = &targetedSearchers.at(history).at(target)->selectState(); + assert(targetedSearchers.find({history, target}) != + targetedSearchers.end() && + targetedSearchers.at({history, target}) && + !targetedSearchers.at({history, target})->empty()); + state = &targetedSearchers.at({history, target})->selectState(); } return *state; } -bool GuidedSearcher::isStuck(ExecutionState &state) { - KInstruction *prevKI = state.prevPC; - return (prevKI->inst->isTerminator() && - state.multilevel[state.getPCBlock()] > bound); -} - -bool GuidedSearcher::updateTargetedSearcher( - ref history, ref target, - ExecutionState *current, std::vector &addedStates, - std::vector &removedStates) { - bool canReach = false; - auto &historiedTargetedSearchers = targetedSearchers[history]; - - if (historiedTargetedSearchers.count(target) != 0 || - tryAddTarget(history, target)) { - - if (current) { - assert(current->targetForest.contains(target)); - for (auto &reached : reachedTargets) { - current->targetForest.blockIn(target, reached); - } - if (!current->targetForest.contains(target)) { - removedStates.push_back(current); - } - } - for (std::vector::iterator is = addedStates.begin(), - ie = addedStates.end(); - is != ie;) { - ExecutionState *state = *is; - assert(state->targetForest.contains(target)); - for (auto &reached : reachedTargets) { - state->targetForest.blockIn(target, reached); - } - if (!state->targetForest.contains(target)) { - is = addedStates.erase(is); - ie = addedStates.end(); - } else { - ++is; - } - } - - canReach = historiedTargetedSearchers[target]->updateCheckCanReach( - current, addedStates, removedStates); - if (historiedTargetedSearchers[target]->empty()) { - removeTarget(history, target); - } - } else if (isReached(history, target)) { - canReach = true; - if (current) { - current->targetForest.remove(target); - } - assert(removedStates.empty()); - for (auto &state : addedStates) { - state->targetForest.remove(target); - } - } - if (targetedSearchers[history].empty()) - targetedSearchers.erase(history); - return canReach; -} - -static void updateConfidences(ExecutionState *current, - const GuidedSearcher::TargetToStateUnorderedSetMap - &reachableStatesOfTarget) { - if (current) - current->targetForest.divideConfidenceBy(reachableStatesOfTarget); -} - -void GuidedSearcher::updateTargetedSearcherForStates( - std::vector &states, - std::vector &tmpAddedStates, - std::vector &tmpRemovedStates, - TargetToStateUnorderedSetMap &reachableStatesOfTarget, bool areStatesStuck, - bool areStatesRemoved) { - for (const auto state : states) { - auto history = state->targetForest.getHistory(); - auto targets = state->targetForest.getTargets(); - TargetForest::TargetsSet stateTargets; - for (auto &targetF : *targets) { - stateTargets.insert(targetF.first); - } - - for (auto &target : stateTargets) { - if (areStatesRemoved || state->targetForest.contains(target)) { - if (areStatesRemoved) - tmpRemovedStates.push_back(state); - else - tmpAddedStates.push_back(state); - assert(!state->targetForest.empty()); - - bool canReach = areStatesStuck; // overapproximation: assume that stuck - // state can reach any target - if (!areStatesStuck) - canReach = updateTargetedSearcher(history, target, nullptr, - tmpAddedStates, tmpRemovedStates); - if (canReach) - reachableStatesOfTarget[target].insert(state); - } - tmpAddedStates.clear(); - tmpRemovedStates.clear(); - } - } -} - -void GuidedSearcher::innerUpdate( +void GuidedSearcher::update( ExecutionState *current, const std::vector &addedStates, const std::vector &removedStates) { - baseAddedStates.insert(baseAddedStates.end(), addedStates.begin(), - addedStates.end()); - baseRemovedStates.insert(baseRemovedStates.end(), removedStates.begin(), - removedStates.end()); - - std::vector addedStuckStates; - if (ErrorGuidance == guidance) { - if (current && - (std::find(baseRemovedStates.begin(), baseRemovedStates.end(), - current) == baseRemovedStates.end()) && - isStuck(*current)) { - pausedStates.insert(current); - baseRemovedStates.push_back(current); - } - for (const auto state : addedStates) { - if (isStuck(*state)) { - pausedStates.insert(state); - addedStuckStates.push_back(state); - auto is = - std::find(baseAddedStates.begin(), baseAddedStates.end(), state); - assert(is != baseAddedStates.end()); - baseAddedStates.erase(is); - } + + if (current) { + ref history = current->history(); + const TargetHashSet &targets = current->targets(); + for (auto target : targets) { + localHistoryTargets.insert({history, target}); + currTargets.insert({history, target}); } } - for (const auto state : baseAddedStates) { - if (!state->targetForest.empty()) { - targetedAddedStates.push_back(state); - } else { - targetlessStates.push_back(state); + for (const auto state : addedStates) { + ref history = state->history(); + const TargetHashSet &targets = state->targets(); + for (auto target : targets) { + localHistoryTargets.insert({history, target}); + addedTStates[{history, target}].push_back(state); } } - TargetForest::TargetsSet currTargets; - if (current) { - auto targets = current->targetForest.getTargets(); - for (auto &targetF : *targets) { - auto target = targetF.first; - assert(target && "Target should be not null!"); - currTargets.insert(target); + for (const auto state : removedStates) { + ref history = state->history(); + const TargetHashSet &targets = state->targets(); + for (auto target : targets) { + localHistoryTargets.insert({history, target}); + removedTStates[{history, target}].push_back(state); } } - if (current && currTargets.empty() && - std::find(baseRemovedStates.begin(), baseRemovedStates.end(), current) == - baseRemovedStates.end()) { - targetlessStates.push_back(current); - } + for (auto historyTarget : localHistoryTargets) { + ref history = historyTarget.first; + ref target = historyTarget.second; - if (ErrorGuidance == guidance) { - if (!removedStates.empty()) { - std::vector alt = removedStates; - for (const auto state : alt) { - auto it = pausedStates.find(state); - if (it != pausedStates.end()) { - pausedStates.erase(it); - baseRemovedStates.erase(std::remove(baseRemovedStates.begin(), - baseRemovedStates.end(), state), - baseRemovedStates.end()); - } - } - } - } + ExecutionState *currTState = + currTargets.count({history, target}) != 0 ? current : nullptr; - std::vector tmpAddedStates; - std::vector tmpRemovedStates; - - if (CoverageGuidance == guidance) { - for (const auto state : targetlessStates) { - if (isStuck(*state)) { - ref target(stateHistory.calculate(*state)); - if (target) { - state->targetForest.add(target); - auto history = state->targetForest.getHistory(); - tmpAddedStates.push_back(state); - updateTargetedSearcher(history, target, nullptr, tmpAddedStates, - tmpRemovedStates); - auto is = std::find(targetedAddedStates.begin(), - targetedAddedStates.end(), state); - if (is != targetedAddedStates.end()) { - targetedAddedStates.erase(is); - } - tmpAddedStates.clear(); - tmpRemovedStates.clear(); - } else { - pausedStates.insert(state); - if (std::find(baseAddedStates.begin(), baseAddedStates.end(), - state) != baseAddedStates.end()) { - auto is = std::find(baseAddedStates.begin(), baseAddedStates.end(), - state); - baseAddedStates.erase(is); - } else { - baseRemovedStates.push_back(state); - } - } - } - } - } - targetlessStates.clear(); - - TargetToStateUnorderedSetMap reachableStatesOfTarget; - - if (current && !currTargets.empty()) { - auto history = current->targetForest.getHistory(); - for (auto &target : currTargets) { - bool canReach = false; - if (current->targetForest.contains(target)) { - canReach = updateTargetedSearcher(history, target, current, - tmpAddedStates, tmpRemovedStates); - } else { - tmpRemovedStates.push_back(current); - canReach = updateTargetedSearcher(history, target, nullptr, - tmpAddedStates, tmpRemovedStates); - } - if (canReach) - reachableStatesOfTarget[target].insert(current); - tmpAddedStates.clear(); - tmpRemovedStates.clear(); + if (!isThereTarget(history, target)) { + addTarget(history, target); } - } - updateTargetedSearcherForStates(targetedAddedStates, tmpAddedStates, - tmpRemovedStates, reachableStatesOfTarget, - false, false); - targetedAddedStates.clear(); - updateTargetedSearcherForStates(addedStuckStates, tmpAddedStates, - tmpRemovedStates, reachableStatesOfTarget, - true, false); - updateTargetedSearcherForStates(baseRemovedStates, tmpAddedStates, - tmpRemovedStates, reachableStatesOfTarget, - false, true); - - if (CoverageGuidance == guidance) { - assert(baseSearcher); - baseSearcher->update(current, baseAddedStates, baseRemovedStates); + targetedSearchers.at({history, target}) + ->update(currTState, addedTStates[{history, target}], + removedTStates[{history, target}]); + addedTStates.at({history, target}).clear(); + removedTStates.at({history, target}).clear(); + if (targetedSearchers.at({history, target})->empty()) { + removeTarget(history, target); + } } + localHistoryTargets.clear(); + currTargets.clear(); - if (ErrorGuidance == guidance) { - updateConfidences(current, reachableStatesOfTarget); - for (auto state : baseAddedStates) - updateConfidences(state, reachableStatesOfTarget); - for (auto state : addedStuckStates) - updateConfidences(state, reachableStatesOfTarget); + if (baseSearcher) { + baseSearcher->update(current, addedStates, removedStates); } - baseAddedStates.clear(); - baseRemovedStates.clear(); -} - -void GuidedSearcher::update( - ExecutionState *current, const std::vector &addedStates, - const std::vector &removedStates) { - innerUpdate(current, addedStates, removedStates); - clearReached(removedStates); } -void GuidedSearcher::collectReached(TargetToStateSetMap &reachedStates) { - for (auto &historyTarget : historiesAndTargets) { - auto &history = historyTarget.first; - auto &target = historyTarget.second; - auto reached = targetedSearchers.at(history).at(target)->reached(); - if (!reached.empty()) { - for (auto state : reached) - reachedStates[target].insert(state); - } +void GuidedSearcher::update(const TargetHistoryTargetPairToStatesMap &added, + const TargetHistoryTargetPairToStatesMap &removed) { + for (const auto &pair : added) { + if (!pair.second.empty()) + localHistoryTargets.insert(pair.first); } -} - -void GuidedSearcher::clearReached( - const std::vector &removedStates) { - std::vector addedStates; - std::vector tmpAddedStates; - std::vector tmpRemovedStates; - TargetToStateSetMap reachedStates; - collectReached(reachedStates); - - for (auto &targetState : reachedStates) { - auto target = targetState.first; - auto states = targetState.second; - for (auto &state : states) { - auto history = state->targetForest.getHistory(); - auto targets = state->targetForest.getTargets(); - if (std::find(removedStates.begin(), removedStates.end(), state) == - removedStates.end()) { - TargetForest::TargetsSet stateTargets; - for (auto &targetF : *targets) { - stateTargets.insert(targetF.first); - } - tmpRemovedStates.push_back(state); - for (auto &anotherTarget : stateTargets) { - if (target != anotherTarget) { - updateTargetedSearcher(history, anotherTarget, nullptr, - tmpAddedStates, tmpRemovedStates); - } - } - tmpRemovedStates.clear(); - addedStates.push_back(state); - } - } + for (const auto &pair : removed) { + if (!pair.second.empty()) + localHistoryTargets.insert(pair.first); } - if (!reachedStates.empty()) { - for (auto &targetState : reachedStates) { - auto target = targetState.first; - auto states = targetState.second; - for (auto &state : states) { - auto history = state->targetForest.getHistory(); - if (target->shouldFailOnThisTarget()) { - reachedTargets.insert(target); - } - targetedSearchers.at(history).at(target)->removeReached(); - if (CoverageGuidance == guidance || - (ErrorGuidance == guidance && target->shouldFailOnThisTarget()) || - targetedSearchers.at(history).at(target)->empty()) { - removeTarget(history, target); - } - if (targetedSearchers.at(history).empty()) - targetedSearchers.erase(history); - } - } - } + for (auto historyTarget : localHistoryTargets) { + ref history = historyTarget.first; + ref target = historyTarget.second; - for (const auto state : addedStates) { - auto history = state->targetForest.getHistory(); - auto targets = state->targetForest.getTargets(); - TargetForest::TargetsSet stateTargets; - for (auto &targetF : *targets) { - stateTargets.insert(targetF.first); + if (!isThereTarget(history, target)) { + addTarget(history, target); } - for (auto &target : stateTargets) { - if (state->targetForest.contains(target)) { - tmpAddedStates.push_back(state); - updateTargetedSearcher(history, target, nullptr, tmpAddedStates, - tmpRemovedStates); - } - tmpAddedStates.clear(); - tmpRemovedStates.clear(); + + targetedSearchers.at({history, target}) + ->update(nullptr, added.at({history, target}), + removed.at({history, target})); + if (targetedSearchers.at({history, target})->empty()) { + removeTarget(history, target); } } + localHistoryTargets.clear(); } -bool GuidedSearcher::empty() { - return CoverageGuidance == guidance ? baseSearcher->empty() - : targetedSearchers.empty(); -} - -void GuidedSearcher::printName(llvm::raw_ostream &os) { - os << "GuidedSearcher\n"; +bool GuidedSearcher::isThereTarget(ref history, + ref target) { + return targetedSearchers.count({history, target}) != 0; } -bool GuidedSearcher::isReached(ref history, +void GuidedSearcher::addTarget(ref history, ref target) { - return reachedTargets.count(target) != 0; -} - -bool GuidedSearcher::tryAddTarget(ref history, - ref target) { - if (isReached(history, target)) { - return false; - } - assert(targetedSearchers.count(history) == 0 || - targetedSearchers.at(history).count(target) == 0); - targetedSearchers[history][target] = + assert(targetedSearchers.count({history, target}) == 0); + targetedSearchers[{history, target}] = std::make_unique(target, distanceCalculator); - auto it = std::find_if( - historiesAndTargets.begin(), historiesAndTargets.end(), - [&history, &target]( - const std::pair, ref> &element) { - return element.first.get() == history.get() && - element.second.get() == target.get(); - }); - assert(it == historiesAndTargets.end()); + assert(std::find_if( + historiesAndTargets.begin(), historiesAndTargets.end(), + [&history, &target](const std::pair, + ref> &element) { + return element.first.get() == history.get() && + element.second.get() == target.get(); + }) == historiesAndTargets.end()); historiesAndTargets.push_back({history, target}); - return true; } -GuidedSearcher::TargetForestHisoryTargetVector::iterator -GuidedSearcher::removeTarget(ref history, - ref target) { - targetedSearchers.at(history).erase(target); +void GuidedSearcher::removeTarget(ref history, + ref target) { + targetedSearchers.erase({history, target}); auto it = std::find_if( historiesAndTargets.begin(), historiesAndTargets.end(), [&history, &target]( - const std::pair, ref> &element) { + const std::pair, ref> &element) { return element.first.get() == history.get() && element.second.get() == target.get(); }); assert(it != historiesAndTargets.end()); - return historiesAndTargets.erase(it); + historiesAndTargets.erase(it); +} + +bool GuidedSearcher::empty() { return baseSearcher->empty(); } + +void GuidedSearcher::printName(llvm::raw_ostream &os) { + os << "GuidedSearcher\n"; } /// diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 0469a00724..5fe557ca6f 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -14,6 +14,8 @@ #include "ExecutionState.h" #include "PForest.h" #include "PTree.h" +#include "TargetManager.h" + #include "klee/ADT/RNG.h" #include "klee/Module/KModule.h" #include "klee/System/Time.h" @@ -45,7 +47,7 @@ template class WeightedQueue; class ExecutionState; class TargetCalculator; class TargetForest; -class TargetReachability; +class TargetManagerSubscriber; /// A Searcher implements an exploration strategy for the Executor by selecting /// states for further exploration using different strategies or heuristics. @@ -132,16 +134,14 @@ class RandomSearcher final : public Searcher { void printName(llvm::raw_ostream &os) override; }; -/// TargetedSearcher picks a state /*COMMENT*/. class TargetedSearcher final : public Searcher { private: std::unique_ptr> states; ref target; DistanceCalculator &distanceCalculator; - std::set reachedOnLastUpdate; - WeightResult tryGetWeight(ExecutionState *es, weight_type &weight); + weight_type getWeight(ExecutionState *es); public: TargetedSearcher(ref target, DistanceCalculator &distanceCalculator); @@ -151,99 +151,63 @@ class TargetedSearcher final : public Searcher { void update(ExecutionState *current, const std::vector &addedStates, const std::vector &removedStates) override; - bool updateCheckCanReach(ExecutionState *current, - const std::vector &addedStates, - const std::vector &removedStates); bool empty() override; void printName(llvm::raw_ostream &os) override; - std::set reached(); - void removeReached(); }; -class GuidedSearcher final : public Searcher { -public: - using TargetToStateUnorderedSetMap = - TargetHashMap>; - - using TargetToSearcherMap = TargetHashMap>; - using TargetToStateSetMap = - TargetHashMap>; - using TargetToStateVectorMap = TargetHashMap>; - - template - class TargetForestHistoryHashMap - : public std::unordered_map, T, - RefTargetsHistoryHash, RefTargetsHistoryCmp> { - }; +class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { template - class TargetForestHistoryTargetsHashMap - : public TargetForestHistoryHashMap> {}; - - using TargetForestHistoryToSearcherMap = - TargetForestHistoryTargetsHashMap>; - using TargetForestHistoryToStateSetMap = - TargetForestHistoryTargetsHashMap>; - using TargetForestHisoryToStateVectorMap = - TargetForestHistoryTargetsHashMap>; - using TargetForestHisoryToTargetSet = TargetForestHistoryHashMap< - std::unordered_set, RefTargetHash, RefTargetCmp>>; - using TargetForestHisoryToTargetVector = - TargetForestHistoryHashMap>>; - using TargetForestHisoryTargetVector = - std::vector, ref>>; + using TargetHistoryTargetPairHashMap = + std::unordered_map; + + using TargetHistoryTargetPair = + std::pair, ref>; + using TargetHistoryTargetPairToSearcherMap = + std::unordered_map, + TargetHistoryTargetHash, TargetHistoryTargetCmp>; + using StatesVector = std::vector; + using TargetHistoryTargetPairToStatesMap = + std::unordered_map; + using TargetForestHisoryTargetVector = std::vector; + using TargetForestHistoryTargetSet = std::set; -private: - enum Guidance { CoverageGuidance, ErrorGuidance }; - - Guidance guidance; std::unique_ptr baseSearcher; - TargetForestHistoryToSearcherMap targetedSearchers; + TargetHistoryTargetPairToSearcherMap targetedSearchers; DistanceCalculator &distanceCalculator; - TargetCalculator &stateHistory; - TargetHashSet reachedTargets; - std::set &pausedStates; - unsigned long long bound; RNG &theRNG; unsigned index{1}; + TargetForestHistoryTargetSet localHistoryTargets; std::vector baseAddedStates; std::vector baseRemovedStates; - std::vector targetedAddedStates; - std::vector targetlessStates; - TargetForestHisoryTargetVector historiesAndTargets; + TargetHistoryTargetPairToStatesMap addedTStates; + TargetHistoryTargetPairToStatesMap removedTStates; - bool tryAddTarget(ref history, ref target); - TargetForestHisoryTargetVector::iterator - removeTarget(ref history, ref target); - bool isStuck(ExecutionState &state); - void innerUpdate(ExecutionState *current, - const std::vector &addedStates, - const std::vector &removedStates); - bool updateTargetedSearcher(ref history, - ref target, ExecutionState *current, - std::vector &addedStates, - std::vector &removedStates); - void updateTargetedSearcherForStates( - std::vector &states, - std::vector &tmpAddedStates, - std::vector &tmpRemovedStates, - TargetToStateUnorderedSetMap &reachableStatesOfTarget, - bool areStatesStuck, bool areStatesRemoved); - - void clearReached(const std::vector &removedStates); - void collectReached(TargetToStateSetMap &reachedStates); - bool isReached(ref history, ref target); + TargetHashSet removedTargets; + TargetHashSet addedTargets; + TargetForestHistoryTargetSet currTargets; + + TargetForestHisoryTargetVector historiesAndTargets; + bool isThereTarget(ref history, ref target); + void addTarget(ref history, ref target); + void removeTarget(ref history, ref target); public: - GuidedSearcher( - DistanceCalculator &distanceCalculator, TargetCalculator &stateHistory, - std::set &pausedStates, - unsigned long long bound, RNG &rng, Searcher *baseSearcher = nullptr); + GuidedSearcher(Searcher *baseSearcher, DistanceCalculator &distanceCalculator, + RNG &rng) + : baseSearcher(baseSearcher), distanceCalculator(distanceCalculator), + theRNG(rng) {} ~GuidedSearcher() override = default; ExecutionState &selectState() override; void update(ExecutionState *current, const std::vector &addedStates, const std::vector &removedStates) override; + void update(const TargetHistoryTargetPairToStatesMap &added, + const TargetHistoryTargetPairToStatesMap &removed) override; + void updateTargets(ExecutionState *current); bool empty() override; void printName(llvm::raw_ostream &os) override; diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index ba91e239ce..1ccc43d5ce 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -863,11 +863,13 @@ void StatsTracker::writeIStats() { /// -typedef std::map> calltargets_ty; +typedef std::unordered_map> + calltargets_ty; static calltargets_ty callTargets; -static std::map> functionCallers; -static std::map functionShortestPath; +static std::unordered_map> + functionCallers; +static std::unordered_map functionShortestPath; static std::vector getSuccs(Instruction *i) { BasicBlock *bb = i->getParent(); diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp new file mode 100644 index 0000000000..9321b4c829 --- /dev/null +++ b/lib/Core/TargetManager.cpp @@ -0,0 +1,191 @@ +//===-- TargetedManager.cpp -----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "TargetManager.h" + +#include "TargetCalculator.h" + +#include "klee/Module/KInstruction.h" + +#include + +using namespace llvm; +using namespace klee; + +namespace klee {} // namespace klee + +void TargetManager::updateMiss(ExecutionState &state, ref target) { + auto &stateTargetForest = targetForest(state); + stateTargetForest.remove(target); + setTargets(state, stateTargetForest.getTargets()); + if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { + state.setTargeted(false); + } +} + +void TargetManager::updateContinue(ExecutionState &state, ref target) {} + +void TargetManager::updateDone(ExecutionState &state, ref target) { + auto &stateTargetForest = targetForest(state); + + stateTargetForest.stepTo(target); + setTargets(state, stateTargetForest.getTargets()); + setHistory(state, stateTargetForest.getHistory()); + if (guidance == Interpreter::GuidanceKind::CoverageGuidance || + target->shouldFailOnThisTarget()) { + reachedTargets.insert(target); + for (auto es : states) { + if (isTargeted(*es)) { + auto &esTargetForest = targetForest(*es); + esTargetForest.block(target); + setTargets(*es, esTargetForest.getTargets()); + if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { + if (targets(*es).size() == 0) { + es->setTargeted(false); + } + } + } + } + } + if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { + state.setTargeted(false); + } +} + +void TargetManager::collect(ExecutionState &state) { + if (!state.areTargetsChanged()) { + return; + } + + ref prevHistory = state.prevHistory(); + ref history = state.history(); + const TargetHashSet &prevTargets = state.prevTargets(); + const TargetHashSet &targets = state.targets(); + if (prevHistory != history) { + for (auto target : prevTargets) { + removedTStates[{prevHistory, target}].push_back(&state); + addedTStates[{prevHistory, target}]; + } + for (auto target : targets) { + addedTStates[{history, target}].push_back(&state); + removedTStates[{history, target}]; + } + } else { + addedTargets = targets; + for (auto target : prevTargets) { + if (addedTargets.erase(target) == 0) { + removedTargets.insert(target); + } + } + for (auto target : removedTargets) { + removedTStates[{history, target}].push_back(&state); + addedTStates[{history, target}]; + } + for (auto target : addedTargets) { + addedTStates[{history, target}].push_back(&state); + removedTStates[{history, target}]; + } + removedTargets.clear(); + addedTargets.clear(); + } +} + +void TargetManager::updateTargets(ExecutionState &state) { + if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { + if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { + state.setTargeted(true); + } + if (isTargeted(state) && !targets(state).empty()) { + ref target(targetCalculator.calculate(state)); + if (target) { + state.targetForest.add(target); + setTargets(state, state.targetForest.getTargets()); + } + } + } + + if (!isTargeted(state)) { + return; + } + + auto stateTargets = targets(state); + auto &stateTargetForest = targetForest(state); + + for (auto target : stateTargets) { + if (!stateTargetForest.contains(target)) { + continue; + } + + DistanceResult stateDistance = distance(state, target); + switch (stateDistance.result) { + case WeightResult::Continue: + updateContinue(state, target); + break; + case WeightResult::Miss: + updateMiss(state, target); + break; + case WeightResult::Done: + updateDone(state, target); + break; + default: + assert(0 && "unreachable"); + } + } +} + +void TargetManager::update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates) { + + states.insert(addedStates.begin(), addedStates.end()); + + if (current && (std::find(removedStates.begin(), removedStates.end(), + current) == removedStates.end())) { + localStates.insert(current); + } + for (const auto state : addedStates) { + localStates.insert(state); + } + for (const auto state : removedStates) { + localStates.insert(state); + } + + for (auto state : localStates) { + updateTargets(*state); + if (state->areTargetsChanged()) { + changedStates.insert(state); + } + } + + for (auto state : changedStates) { + if (std::find(addedStates.begin(), addedStates.end(), state) == + addedStates.end()) { + collect(*state); + } + state->stepTargetsAndHistory(); + } + + for (const auto state : removedStates) { + states.erase(state); + } + + for (auto subscriber : subscribers) { + subscriber->update(addedTStates, removedTStates); + } + + for (auto &pair : addedTStates) { + pair.second.clear(); + } + for (auto &pair : removedTStates) { + pair.second.clear(); + } + + changedStates.clear(); + localStates.clear(); +} diff --git a/lib/Core/TargetManager.h b/lib/Core/TargetManager.h new file mode 100644 index 0000000000..3d81049443 --- /dev/null +++ b/lib/Core/TargetManager.h @@ -0,0 +1,134 @@ +//===-- TargetedManager.h --------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +// +// Class to manage everything about targets +// +//===----------------------------------------------------------------------===// + +#include "DistanceCalculator.h" + +#include "klee/Core/Interpreter.h" +#include "klee/Module/TargetHash.h" + +#include +#include + +#ifndef KLEE_TARGETMANAGER_H +#define KLEE_TARGETMANAGER_H + +namespace klee { +class TargetCalculator; + +class TargetManagerSubscriber { +public: + using TargetHistoryTargetPair = + std::pair, ref>; + using StatesVector = std::vector; + using TargetHistoryTargetPairToStatesMap = + std::unordered_map; + + virtual ~TargetManagerSubscriber() = default; + + /// Selects a state for further exploration. + /// \return The selected state. + virtual void update(const TargetHistoryTargetPairToStatesMap &added, + const TargetHistoryTargetPairToStatesMap &removed) = 0; +}; + +class TargetManager { +private: + using StatesSet = std::unordered_set; + using TargetHistoryTargetPair = + std::pair, ref>; + using StatesVector = std::vector; + using TargetHistoryTargetPairToStatesMap = + std::unordered_map; + using TargetForestHistoryTargetSet = std::set; + + Interpreter::GuidanceKind guidance; + DistanceCalculator &distanceCalculator; + TargetCalculator &targetCalculator; + TargetHashSet reachedTargets; + StatesSet states; + StatesSet localStates; + StatesSet changedStates; + std::vector subscribers; + TargetHistoryTargetPairToStatesMap addedTStates; + TargetHistoryTargetPairToStatesMap removedTStates; + TargetHashSet removedTargets; + TargetHashSet addedTargets; + + void setTargets(ExecutionState &state, const TargetHashSet &targets) { + state.setTargets(targets); + changedStates.insert(&state); + } + + void setHistory(ExecutionState &state, ref history) { + state.setHistory(history); + changedStates.insert(&state); + } + + void updateMiss(ExecutionState &state, ref target); + + void updateContinue(ExecutionState &state, ref target); + + void updateDone(ExecutionState &state, ref target); + + void updateTargets(ExecutionState &state); + void collect(ExecutionState &state); + +public: + TargetManager(Interpreter::GuidanceKind _guidance, + DistanceCalculator &_distanceCalculator, + TargetCalculator &_targetCalculator) + : guidance(_guidance), distanceCalculator(_distanceCalculator), + targetCalculator(_targetCalculator){}; + + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates); + + DistanceResult distance(const ExecutionState &state, ref target) { + return distanceCalculator.getDistance(state, target); + } + + const TargetHashSet &targets(const ExecutionState &state) { + return state.targets(); + } + + ref history(const ExecutionState &state) { + return state.history(); + } + + ref prevHistory(const ExecutionState &state) { + return state.prevHistory(); + } + + const TargetHashSet &prevTargets(const ExecutionState &state) { + return state.prevTargets(); + } + + TargetForest &targetForest(ExecutionState &state) { + return state.targetForest; + } + + void subscribe(TargetManagerSubscriber &subscriber) { + subscribers.push_back(&subscriber); + } + + bool isTargeted(const ExecutionState &state) { return state.isTargeted(); } + + void setReached(ref target) { reachedTargets.insert(target); } +}; + +} // namespace klee + +#endif /* KLEE_TARGETMANAGER_H */ diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index 5c975421d6..cfbad46826 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -9,6 +9,9 @@ #include "TargetedExecutionManager.h" +#include "DistanceCalculator.h" +#include "TargetManager.h" + #include "ExecutionState.h" #include "klee/Core/TerminationTypes.h" #include "klee/Module/CodeGraphDistance.h" @@ -173,6 +176,12 @@ llvm::cl::opt SmartResolveEntryFunction( "smart-resolve-entry-function", cl::init(false), cl::desc("Resolve entry function using code flow graph instead of taking " "function of first location (default=false)")); + +cl::opt + MaxCycles("max-cycles", + cl::desc("stop execution after visiting some basic block this " + "amount of times (default=0)."), + cl::init(0), cl::cat(TerminationCat)); } // namespace klee TargetedHaltsOnTraces::TargetedHaltsOnTraces(ref &forest) { @@ -478,23 +487,24 @@ KFunction *TargetedExecutionManager::tryResolveEntryFunction( return resKf; } -std::unordered_map> +std::map, + TargetedExecutionManager::KFunctionLess> TargetedExecutionManager::prepareTargets(KModule *kmodule, SarifReport paths) { Locations locations = collectAllLocations(paths); LocationToBlocks locToBlocks = prepareAllLocations(kmodule, locations); - std::unordered_map> whitelists; + std::map, KFunctionLess> whitelists; for (auto &result : paths.results) { bool isFullyResolved = tryResolveLocations(result, locToBlocks); if (!isFullyResolved) { - broken_traces.insert(result.id); + brokenTraces.insert(result.id); continue; } auto kf = tryResolveEntryFunction(result, locToBlocks); if (!kf) { - broken_traces.insert(result.id); + brokenTraces.insert(result.id); continue; } @@ -517,10 +527,9 @@ void TargetedExecutionManager::reportFalseNegative(ExecutionState &state, bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, ReachWithError error) { bool atLeastOneReported = false; - for (auto kvp : state.targetForest) { - auto target = kvp.first; - if (!target->isThatError(error) || broken_traces.count(target->getId()) || - reported_traces.count(target->getId())) + for (auto target : state.targetForest.getTargets()) { + if (!target->isThatError(error) || brokenTraces.count(target->getId()) || + reportedTraces.count(target->getId())) continue; /// The following code checks if target is a `call ...` instruction and we @@ -554,7 +563,49 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, getErrorString(error), target->getId().c_str()); } target->isReported = true; - reported_traces.insert(target->getId()); + reportedTraces.insert(target->getId()); } return atLeastOneReported; } + +void TargetedExecutionManager::update( + ExecutionState *current, const std::vector &addedStates, + const std::vector &removedStates) { + if (current && (std::find(removedStates.begin(), removedStates.end(), + current) == removedStates.end())) { + localStates.insert(current); + } + for (const auto state : addedStates) { + localStates.insert(state); + } + for (const auto state : removedStates) { + localStates.insert(state); + } + + TargetToStateUnorderedSetMap reachableStatesOfTarget; + + for (auto state : localStates) { + auto &stateTargets = state->targets(); + + for (auto target : stateTargets) { + DistanceResult stateDistance = + distanceCalculator.getDistance(*state, target); + switch (stateDistance.result) { + case WeightResult::Miss: + break; + case WeightResult::Continue: + case WeightResult::Done: + reachableStatesOfTarget[target].insert(state); + break; + default: + assert(0 && "unreachable"); + } + } + } + + for (auto state : localStates) { + state->targetForest.divideConfidenceBy(reachableStatesOfTarget); + } + + localStates.clear(); +} \ No newline at end of file diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 079b230754..6171d80d69 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -22,6 +22,9 @@ #include namespace klee { +class DistanceCalculator; +class TargetManager; + extern llvm::cl::OptionCategory TerminationCat; /*** Termination criteria options ***/ @@ -56,6 +59,8 @@ extern llvm::cl::opt MaxStaticPctCheckDelay; extern llvm::cl::opt TimerInterval; +extern llvm::cl::opt MaxCycles; + class CodeGraphDistance; class TargetedHaltsOnTraces { @@ -64,8 +69,8 @@ class TargetedHaltsOnTraces { using TraceToHaltTypeToConfidence = std::unordered_map, HaltTypeToConfidence, - TargetForest::RefUnorderedTargetsSetHash, - TargetForest::RefUnorderedTargetsSetCmp>; + TargetForest::UnorderedTargetsSetHash, + TargetForest::UnorderedTargetsSetCmp>; TraceToHaltTypeToConfidence traceToHaltTypeToConfidence; static void totalConfidenceAndTopContributor( @@ -89,14 +94,17 @@ class TargetedExecutionManager { RefLocationHash, RefLocationCmp>; using Locations = std::unordered_set, RefLocationHash, RefLocationCmp>; + using StatesSet = std::unordered_set; + using TargetToStateUnorderedSetMap = TargetHashMap; using Instructions = std::unordered_map< std::string, std::unordered_map< unsigned int, std::unordered_map>>>; - std::unordered_set broken_traces; - std::unordered_set reported_traces; + + std::unordered_set brokenTraces; + std::unordered_set reportedTraces; bool tryResolveLocations(Result &result, LocationToBlocks &locToBlocks) const; LocationToBlocks prepareAllLocations(KModule *kmodule, @@ -110,17 +118,32 @@ class TargetedExecutionManager { LocationToBlocks &locToBlocks) const; CodeGraphDistance &codeGraphDistance; + DistanceCalculator &distanceCalculator; + StatesSet localStates; public: - explicit TargetedExecutionManager(CodeGraphDistance &codeGraphDistance_) - : codeGraphDistance(codeGraphDistance_) {} - std::unordered_map> + struct KFunctionLess { + bool operator()(const KFunction *a, const KFunction *b) const { + return a->id < b->id; + } + }; + + explicit TargetedExecutionManager(CodeGraphDistance &codeGraphDistance_, + DistanceCalculator &distanceCalculator_) + : codeGraphDistance(codeGraphDistance_), + distanceCalculator(distanceCalculator_) {} + ~TargetedExecutionManager() = default; + std::map, KFunctionLess> prepareTargets(KModule *kmodule, SarifReport paths); void reportFalseNegative(ExecutionState &state, ReachWithError error); // Return true if report is successful bool reportTruePositive(ExecutionState &state, ReachWithError error); + + void update(ExecutionState *current, + const std::vector &addedStates, + const std::vector &removedStates); }; } // namespace klee diff --git a/lib/Core/TargetedExecutionReporter.cpp b/lib/Core/TargetedExecutionReporter.cpp index 41043ad9c6..b45569336f 100644 --- a/lib/Core/TargetedExecutionReporter.cpp +++ b/lib/Core/TargetedExecutionReporter.cpp @@ -15,11 +15,12 @@ using namespace klee; void klee::reportFalsePositive(confidence::ty confidence, - const std::set &errors, + const std::vector &errors, const std::string &id, std::string whatToIncrease) { std::ostringstream out; - out << getErrorsString(errors) << " False Positive at trace " << id; + std::vector errorsSet(errors.begin(), errors.end()); + out << getErrorsString(errorsSet) << " False Positive at trace " << id; if (!confidence::isConfident(confidence)) { out << ". Advice: " << "increase --" << whatToIncrease << " command line parameter value"; diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index ab86548677..8de5273052 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -80,11 +80,6 @@ cl::opt BatchTime( "--use-batching-search. Set to 0s to disable (default=5s)"), cl::init("5s"), cl::cat(SearchCat)); -cl::opt - MaxCycles("max-cycles", - cl::desc("stop execution after visiting some basic block this " - "amount of times (default=1)."), - cl::init(1), cl::cat(TerminationCat)); } // namespace void klee::initializeSearchOptions() { @@ -182,13 +177,9 @@ Searcher *klee::constructUserSearcher(Executor &executor, } if (executor.guidanceKind != Interpreter::GuidanceKind::NoGuidance) { - if (executor.guidanceKind == Interpreter::GuidanceKind::ErrorGuidance) { - delete searcher; - searcher = nullptr; - } - searcher = new GuidedSearcher( - *executor.distanceCalculator, *executor.targetCalculator, - executor.pausedStates, MaxCycles - 1, executor.theRNG, searcher); + searcher = new GuidedSearcher(searcher, *executor.distanceCalculator, + executor.theRNG); + executor.targetManager->subscribe(*static_cast(searcher)); } llvm::raw_ostream &os = executor.getHandler().getInfoStream(); diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 5df6320731..c816d5cdf4 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -536,7 +536,7 @@ Expr::~Expr() { } } -ref Expr::createCachedExpr(const ref &e) { +ref Expr::createCachedExpr(ref e) { std::pair success = cachedExpressions.cache.insert(e.get()); diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp index 0d51bb6078..6af80b66b0 100644 --- a/lib/Module/SarifReport.cpp +++ b/lib/Module/SarifReport.cpp @@ -49,7 +49,7 @@ tryConvertLocationJson(const LocationJson &locationJson) { region->endColumn); } -std::set +std::vector tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, const optional &errorMessage) { if (toolName == "SecB") { @@ -68,7 +68,8 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } } else if (toolName == "clang") { if ("core.NullDereference" == ruleId) { - return {ReachWithError::MayBeNullPointerException}; + return {ReachWithError::MayBeNullPointerException, + ReachWithError::MayBeNullPointerException}; } else if ("unix.Malloc" == ruleId) { if (errorMessage.has_value()) { if (errorMessage->text == "Attempt to free released memory") { @@ -88,7 +89,8 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } } else if (toolName == "CppCheck") { if ("nullPointer" == ruleId || "ctunullpointer" == ruleId) { - return {ReachWithError::MayBeNullPointerException}; // TODO: check it out + return {ReachWithError::MayBeNullPointerException, + ReachWithError::MayBeNullPointerException}; // TODO: check it out } else if ("doubleFree" == ruleId) { return {ReachWithError::DoubleFree}; } else { @@ -96,7 +98,8 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } } else if (toolName == "Infer") { if ("NULL_DEREFERENCE" == ruleId || "NULLPTR_DEREFERENCE" == ruleId) { - return {ReachWithError::MayBeNullPointerException}; // TODO: check it out + return {ReachWithError::MayBeNullPointerException, + ReachWithError::MayBeNullPointerException}; // TODO: check it out } else if ("USE_AFTER_DELETE" == ruleId || "USE_AFTER_FREE" == ruleId) { return {ReachWithError::UseAfterFree, ReachWithError::DoubleFree}; } else { @@ -104,7 +107,8 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } } else if (toolName == "Cooddy") { if ("NULL.DEREF" == ruleId || "NULL.UNTRUSTED.DEREF" == ruleId) { - return {ReachWithError::MayBeNullPointerException}; + return {ReachWithError::MayBeNullPointerException, + ReachWithError::MayBeNullPointerException}; } else if ("MEM.DOUBLE.FREE" == ruleId) { return {ReachWithError::DoubleFree}; } else if ("MEM.USE.FREE" == ruleId) { @@ -120,7 +124,7 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, optional tryConvertResultJson(const ResultJson &resultJson, const std::string &toolName, const std::string &id) { - std::set errors = {ReachWithError::None}; + std::vector errors = {}; if (!resultJson.ruleId.has_value()) { errors = {ReachWithError::Reachable}; } else { @@ -183,7 +187,7 @@ const char *getErrorString(ReachWithError error) { return ReachWithErrorNames[error]; } -std::string getErrorsString(const std::set &errors) { +std::string getErrorsString(const std::vector &errors) { if (errors.size() == 1) { return getErrorString(*errors.begin()); } diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp index 98929f2288..c6d102375b 100644 --- a/lib/Module/Target.cpp +++ b/lib/Module/Target.cpp @@ -39,35 +39,33 @@ std::string Target::toString() const { return repr.str(); } -Target::EquivTargetHashSet Target::cachedTargets; -Target::TargetHashSet Target::targets; +Target::TargetCacheSet Target::cachedTargets; + +ref Target::createCachedTarget(ref target) { + std::pair success = + cachedTargets.cache.insert(target.get()); -ref Target::getFromCacheOrReturn(Target *target) { - std::pair success = - cachedTargets.insert(target); if (success.second) { // Cache miss - targets.insert(target); + target->isCached = true; return target; } // Cache hit - delete target; - target = *(success.first); - return target; + return (ref)*(success.first); } -ref Target::create(const std::set &_errors, +ref Target::create(const std::vector &_errors, const std::string &_id, optional _loc, KBlock *_block) { Target *target = new Target(_errors, _id, _loc, _block); - return getFromCacheOrReturn(target); + return createCachedTarget(target); } ref Target::create(KBlock *_block) { return create({ReachWithError::None}, "", nonstd::nullopt, _block); } -bool Target::isTheSameAsIn(KInstruction *instr) const { +bool Target::isTheSameAsIn(const KInstruction *instr) const { if (!loc.has_value()) { return false; } @@ -89,9 +87,6 @@ bool Target::mustVisitForkBranches(KInstruction *instr) const { } int Target::compare(const Target &other) const { - if (errors != other.errors) { - return errors < other.errors ? -1 : 1; - } if (id != other.id) { return id < other.id ? -1 : 1; } @@ -101,10 +96,25 @@ int Target::compare(const Target &other) const { if (block->id != other.block->id) { return block->id < other.block->id ? -1 : 1; } + + if (errors.size() != other.errors.size()) { + return errors.size() < other.errors.size() ? -1 : 1; + } + + for (unsigned i = 0; i < errors.size(); ++i) { + if (errors.at(i) != other.errors.at(i)) { + return errors.at(i) < other.errors.at(i) ? -1 : 1; + } + } + return 0; } -bool Target::equals(const Target &other) const { return compare(other) == 0; } +bool Target::equals(const Target &b) const { + return (toBeCleared || b.toBeCleared) || (isCached && b.isCached) + ? this == &b + : compare(b) == 0; +} bool Target::operator<(const Target &other) const { return compare(other) == -1; @@ -112,15 +122,9 @@ bool Target::operator<(const Target &other) const { bool Target::operator==(const Target &other) const { return equals(other); } -bool Target::isThatError(ReachWithError err) const { - return errors.count(err) != 0 || - (err == ReachWithError::MustBeNullPointerException && - errors.count(ReachWithError::MayBeNullPointerException) != 0); -} - Target::~Target() { - if (targets.find(this) != targets.end()) { - cachedTargets.erase(this); - targets.erase(this); + if (isCached) { + toBeCleared = true; + cachedTargets.cache.erase(this); } } diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp index ee9cd949ab..f512bf7cc5 100644 --- a/lib/Module/TargetForest.cpp +++ b/lib/Module/TargetForest.cpp @@ -20,10 +20,8 @@ using namespace klee; using namespace llvm; -TargetForest::UnorderedTargetsSet::EquivUnorderedTargetsSetHashSet +TargetForest::UnorderedTargetsSet::UnorderedTargetsSetCacheSet TargetForest::UnorderedTargetsSet::cachedVectors; -TargetForest::UnorderedTargetsSet::UnorderedTargetsSetHashSet - TargetForest::UnorderedTargetsSet::vectors; TargetForest::UnorderedTargetsSet::UnorderedTargetsSet( const ref &target) { @@ -32,21 +30,46 @@ TargetForest::UnorderedTargetsSet::UnorderedTargetsSet( } TargetForest::UnorderedTargetsSet::UnorderedTargetsSet( - const TargetsSet &targets) { + const TargetHashSet &targets) { for (const auto &p : targets) { targetsVec.push_back(p); } sortAndComputeHash(); } -void TargetForest::UnorderedTargetsSet::sortAndComputeHash() { - std::sort(targetsVec.begin(), targetsVec.end(), RefTargetLess{}); - RefTargetHash hasher; - std::size_t seed = targetsVec.size(); - for (const auto &r : targetsVec) { - seed ^= hasher(r) + 0x9e3779b9 + (seed << 6) + (seed >> 2); +unsigned TargetForest::UnorderedTargetsSet::sortAndComputeHash() { + std::sort(targetsVec.begin(), targetsVec.end(), TargetLess{}); + unsigned res = targetsVec.size(); + for (auto r : targetsVec) { + res = (res * Expr::MAGIC_HASH_CONSTANT) + r->hash(); } - hashValue = seed; + hashValue = res; + return res; +} + +int TargetForest::UnorderedTargetsSet::compare( + const TargetForest::UnorderedTargetsSet &other) const { + if (targetsVec != other.targetsVec) { + return targetsVec < other.targetsVec ? -1 : 1; + } + return 0; +} + +bool TargetForest::UnorderedTargetsSet::equals( + const TargetForest::UnorderedTargetsSet &b) const { + return (toBeCleared || b.toBeCleared) || (isCached && b.isCached) + ? this == &b + : compare(b) == 0; +} + +bool TargetForest::UnorderedTargetsSet::operator<( + const TargetForest::UnorderedTargetsSet &other) const { + return compare(other) == -1; +} + +bool TargetForest::UnorderedTargetsSet::operator==( + const TargetForest::UnorderedTargetsSet &other) const { + return equals(other); } ref @@ -56,30 +79,28 @@ TargetForest::UnorderedTargetsSet::create(const ref &target) { } ref -TargetForest::UnorderedTargetsSet::create(const TargetsSet &targets) { +TargetForest::UnorderedTargetsSet::create(const TargetHashSet &targets) { UnorderedTargetsSet *vec = new UnorderedTargetsSet(targets); return create(vec); } ref -TargetForest::UnorderedTargetsSet::create(UnorderedTargetsSet *vec) { - std::pair success = - cachedVectors.insert(vec); +TargetForest::UnorderedTargetsSet::create(ref vec) { + std::pair success = + cachedVectors.cache.insert(vec.get()); if (success.second) { // Cache miss - vectors.insert(vec); + vec->isCached = true; return vec; } // Cache hit - delete vec; - vec = *(success.first); - return vec; + return (ref)*(success.first); } TargetForest::UnorderedTargetsSet::~UnorderedTargetsSet() { - if (vectors.find(this) != vectors.end()) { - vectors.erase(this); - cachedVectors.erase(this); + if (isCached) { + toBeCleared = true; + cachedVectors.cache.erase(this); } } @@ -92,7 +113,7 @@ void TargetForest::Layer::addTrace( const auto &loc = result.locations[i]; auto it = locToBlocks.find(loc); assert(it != locToBlocks.end()); - TargetsSet targets; + TargetHashSet targets; for (auto block : it->second) { ref target = nullptr; if (i == result.locations.size() - 1) { @@ -205,8 +226,7 @@ void TargetForest::Layer::removeTarget(ref target) { bool TargetForest::Layer::deepFind(ref target) const { if (empty()) return false; - auto res = targetsToVector.find(target); - if (res != targetsToVector.end()) { + if (targetsToVector.count(target) != 0) { return true; } for (auto &f : forest) { @@ -218,18 +238,17 @@ bool TargetForest::Layer::deepFind(ref target) const { bool TargetForest::Layer::deepFindIn(ref child, ref target) const { - auto res = targetsToVector.find(child); - if (res == targetsToVector.end()) { + if (targetsToVector.count(child) == 0) { return false; } + auto &res = targetsToVector.at(child); if (child == target) { return true; } - for (auto &targetsVec : res->second) { - auto it = forest.find(targetsVec); - assert(it != forest.end()); - if (it->second->deepFind(target)) { + for (auto &targetsVec : res) { + auto &it = forest.at(targetsVec); + if (it->deepFind(target)) { return true; } } @@ -345,9 +364,8 @@ TargetForest::Layer *TargetForest::Layer::replaceChildWith( TargetForest::Layer *TargetForest::Layer::replaceChildWith( ref child, - const std::unordered_set, - RefUnorderedTargetsSetHash, - RefUnorderedTargetsSetCmp> &other) const { + const std::unordered_set, UnorderedTargetsSetHash, + UnorderedTargetsSetCmp> &other) const { std::vector layers; for (auto &targetsVec : other) { auto it = forest.find(targetsVec); @@ -373,16 +391,6 @@ TargetForest::Layer *TargetForest::Layer::replaceChildWith( return result; } -bool TargetForest::Layer::allNodesRefCountOne() const { - bool all = true; - for (const auto &it : forest) { - all &= it.second->_refCount.getCount() == 1; - assert(all); - all &= it.second->allNodesRefCountOne(); - } - return all; -} - void TargetForest::Layer::dump(unsigned n) const { llvm::errs() << "THE " << n << " LAYER:\n"; llvm::errs() << "Confidence: " << confidence << "\n"; @@ -398,62 +406,64 @@ void TargetForest::Layer::dump(unsigned n) const { } } -TargetForest::History::EquivTargetsHistoryHashSet - TargetForest::History::cachedHistories; -TargetForest::History::TargetsHistoryHashSet TargetForest::History::histories; +TargetsHistory::TargetHistoryCacheSet TargetsHistory::cachedHistories; -ref -TargetForest::History::create(ref _target, - ref _visitedTargets) { - History *history = new History(_target, _visitedTargets); +ref +TargetsHistory::create(ref _target, + ref _visitedTargets) { + ref history = new TargetsHistory(_target, _visitedTargets); - std::pair success = - cachedHistories.insert(history); + std::pair success = + cachedHistories.cache.insert(history.get()); if (success.second) { // Cache miss - histories.insert(history); + history->isCached = true; return history; } // Cache hit - delete history; - history = *(success.first); - return history; + return (ref)*(success.first); } -ref TargetForest::History::create(ref _target) { +ref TargetsHistory::create(ref _target) { return create(_target, nullptr); } -ref TargetForest::History::create() { - return create(nullptr); -} +ref TargetsHistory::create() { return create(nullptr); } -int TargetForest::History::compare(const History &h) const { +int TargetsHistory::compare(const TargetsHistory &h) const { if (this == &h) return 0; + if (size() != h.size()) { + return (size() < h.size()) ? -1 : 1; + } + + if (size() == 0) { + return 0; + } + if (target && h.target) { - if (target != h.target) + if (target != h.target) { return (target < h.target) ? -1 : 1; - } else { - return h.target ? -1 : (target ? 1 : 0); + } } if (visitedTargets && h.visitedTargets) { - if (h.visitedTargets != h.visitedTargets) + if (h.visitedTargets != h.visitedTargets) { return (visitedTargets < h.visitedTargets) ? -1 : 1; - } else { - return h.visitedTargets ? -1 : (visitedTargets ? 1 : 0); + } } return 0; } -bool TargetForest::History::equals(const History &h) const { - return compare(h) == 0; +bool TargetsHistory::equals(const TargetsHistory &b) const { + return (toBeCleared || b.toBeCleared) || (isCached && b.isCached) + ? this == &b + : compare(b) == 0; } -void TargetForest::History::dump() const { +void TargetsHistory::dump() const { if (target) { llvm::errs() << target->toString() << "\n"; } else { @@ -465,10 +475,10 @@ void TargetForest::History::dump() const { visitedTargets->dump(); } -TargetForest::History::~History() { - if (histories.find(this) != histories.end()) { - histories.erase(this); - cachedHistories.erase(this); +TargetsHistory::~TargetsHistory() { + if (isCached) { + toBeCleared = true; + cachedHistories.cache.erase(this); } } @@ -487,7 +497,7 @@ void TargetForest::stepTo(ref loc) { loc->isReported = true; } if (forest->empty() && !loc->shouldFailOnThisTarget()) { - history = History::create(); + history = TargetsHistory::create(); } } @@ -521,16 +531,12 @@ void TargetForest::block(const ref &target) { } void TargetForest::dump() const { - llvm::errs() << "History:\n"; + llvm::errs() << "TargetHistory:\n"; history->dump(); llvm::errs() << "Forest:\n"; forest->dump(1); } -bool TargetForest::allNodesRefCountOne() const { - return forest->allNodesRefCountOne(); -} - void TargetForest::Layer::addLeafs( std::vector, confidence::ty>> &leafs, confidence::ty parentConfidence) const { @@ -607,28 +613,3 @@ TargetForest::Layer *TargetForest::Layer::divideConfidenceBy( } return result; } - -void TargetForest::Layer::collectHowManyEventsInTracesWereReached( - std::unordered_map> - &traceToEventCount, - unsigned reached, unsigned total) const { - total++; - for (const auto &p : forest) { - auto targetsVec = p.first; - auto child = p.second; - bool isReported = false; - for (auto &target : targetsVec->getTargets()) { - if (target->isReported) { - isReported = true; - } - } - auto reachedCurrent = isReported ? reached + 1 : reached; - auto target = *targetsVec->getTargets().begin(); - if (target->shouldFailOnThisTarget()) { - traceToEventCount[target->getId()] = - std::make_pair(reachedCurrent, total); - } - child->collectHowManyEventsInTracesWereReached(traceToEventCount, - reachedCurrent, total); - } -} diff --git a/lib/Module/TargetHash.cpp b/lib/Module/TargetHash.cpp index b187311b83..05f703ed10 100644 --- a/lib/Module/TargetHash.cpp +++ b/lib/Module/TargetHash.cpp @@ -14,31 +14,12 @@ using namespace llvm; using namespace klee; -unsigned TargetHash::operator()(const Target *t) const { - if (t) { - return t->hash(); - } else { - return 0; - } -} - -bool TargetCmp::operator()(const Target *a, const Target *b) const { - return a == b; -} - -bool EquivTargetCmp::operator()(const Target *a, const Target *b) const { - if (a == NULL || b == NULL) - return false; - return a->compare(*b) == 0; -} - -unsigned RefTargetHash::operator()(const ref &t) const { +unsigned TargetHash::operator()(const ref &t) const { return t->hash(); } -bool RefTargetCmp::operator()(const ref &a, - const ref &b) const { - return a.get() == b.get(); +bool TargetCmp::operator()(const ref &a, const ref &b) const { + return a == b; } std::size_t TransitionHash::operator()(const Transition &p) const { diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index 6fbbce8855..bf0f02f08d 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -32,10 +32,8 @@ class ConcretizingSolver : public SolverImpl { AddressGenerator *addressGenerator; public: - ConcretizingSolver(std::unique_ptr _solver, - ConcretizationManager *_cm, AddressGenerator *_ag) - : solver(std::move(_solver)), concretizationManager(_cm), - addressGenerator(_ag) {} + ConcretizingSolver(std::unique_ptr _solver, AddressGenerator *_ag) + : solver(std::move(_solver)), addressGenerator(_ag) {} ~ConcretizingSolver() = default; @@ -645,7 +643,7 @@ std::unique_ptr createConcretizingSolver(std::unique_ptr s, ConcretizationManager *concretizationManager, AddressGenerator *addressGenerator) { - return std::make_unique(std::make_unique( - std::move(s), concretizationManager, addressGenerator)); + return std::make_unique( + std::make_unique(std::move(s), addressGenerator)); } } // namespace klee diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index f0522c4da8..330b2547ea 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -7,13 +7,13 @@ // RUN: %clang -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-memory=20 --max-cycles=0 %t.little.bc > %t.little.log +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 --max-cycles-before-stuck=0 %t.little.bc > %t.little.log // RUN: FileCheck -check-prefix=CHECK-LITTLE -input-file=%t.little.log %s // RUN: FileCheck -check-prefix=CHECK-WRN -input-file=%t.klee-out/warnings.txt %s // RUN: %clang -emit-llvm -g -c %s -o %t.big.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-memory=20 --max-cycles=0 %t.big.bc > %t.big.log 2> %t.big.err +// RUN: %klee --output-dir=%t.klee-out --max-memory=20 --max-cycles-before-stuck=0 %t.big.bc > %t.big.log 2> %t.big.err // RUN: FileCheck -check-prefix=CHECK-BIG -input-file=%t.big.log %s // RUN: FileCheck -check-prefix=CHECK-WRN -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c index bc531555a8..feb01bce62 100644 --- a/test/Feature/MultipleReallocResolution.c +++ b/test/Feature/MultipleReallocResolution.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out %t1.bc +// RUN: %klee --use-guided-search=none--output-dir=%t.klee-out %t1.bc // RUN: ls %t.klee-out/ | grep .err | wc -l | grep 2 // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2 diff --git a/test/Feature/RecursionPruning/sum.c b/test/Feature/RecursionPruning/sum.c index d4a917398c..bc74f0e85f 100644 --- a/test/Feature/RecursionPruning/sum.c +++ b/test/Feature/RecursionPruning/sum.c @@ -13,9 +13,9 @@ int main() { sn = sn + a; } if (sn > 10) { - printf("sn > 10"); + printf("sn > 10\n"); } else { - printf("sn <= 10"); + printf("sn <= 10\n"); } } diff --git a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c index 405d751b7f..4b77bd1b66 100644 --- a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c +++ b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c @@ -56,7 +56,7 @@ void call_func(int num) // REQUIRES: z3 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles=0 --use-guided-search=error --check-out-of-memory --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles-before-stuck=0 --use-guided-search=error --check-out-of-memory --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable at trace 1 diff --git a/test/Industry/NullReturn_Scene_BadCase06.c b/test/Industry/NullReturn_Scene_BadCase06.c index 0710dc14b5..8ad07ac540 100644 --- a/test/Industry/NullReturn_Scene_BadCase06.c +++ b/test/Industry/NullReturn_Scene_BadCase06.c @@ -58,5 +58,5 @@ void TestBad6(unsigned int count) // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -// CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1 -// CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 2 +// CHECK-DAG: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1 +// CHECK-DAG: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 2 diff --git a/test/Industry/fp_forward_null_address.c b/test/Industry/fp_forward_null_address.c index 7f6d612f6d..f39297d2a4 100644 --- a/test/Industry/fp_forward_null_address.c +++ b/test/Industry/fp_forward_null_address.c @@ -25,5 +25,5 @@ void foo() // REQUIRES: z3 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-cycles=150 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --max-cycles-before-stuck=150 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/if2.c b/test/Industry/if2.c index 38eabcc472..27f414ed01 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -11,7 +11,7 @@ int main(int x) { // REQUIRES: z3 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=19 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=19 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE diff --git a/test/Industry/while_true.c b/test/Industry/while_true.c index 4a75fdfd86..a2eebdcc0a 100644 --- a/test/Industry/while_true.c +++ b/test/Industry/while_true.c @@ -11,14 +11,14 @@ int main() { // REQUIRES: z3 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out-1 -// RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=10 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=10 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out-1/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 0.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out-1/messages.txt %s -check-prefix=CHECK-REACH-1 // CHECK-REACH-1: (0, 1, 4) for Target 1: error in function main (lines 8 to 8) // RUN: rm -rf %t.klee-out-2 -// RUN: %klee --output-dir=%t.klee-out-2 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=50000 --max-cycles=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out-2 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=50000 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out-2/warnings.txt %s -check-prefix=CHECK-ALL // CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out-2/messages.txt %s -check-prefix=CHECK-REACH-2 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 68525c7f52..1099b9da14 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -381,8 +381,8 @@ class KleeHandler : public InterpreterHandler { void setInterpreter(Interpreter *i); - void processTestCase(const ExecutionState &state, const char *errorMessage, - const char *errorSuffix); + void processTestCase(const ExecutionState &state, const char *message, + const char *suffix, bool isError = false); std::string getOutputFilename(const std::string &filename); std::unique_ptr @@ -549,8 +549,8 @@ KleeHandler::openTestFile(const std::string &suffix, unsigned id) { /* Outputs all files (.ktest, .kquery, .cov etc.) describing a test case */ void KleeHandler::processTestCase(const ExecutionState &state, - const char *errorMessage, - const char *errorSuffix) { + const char *message, const char *suffix, + bool isError) { unsigned id = ++m_numTotalTests; if (!WriteNone) { KTest ktest; @@ -587,10 +587,10 @@ void KleeHandler::processTestCase(const ExecutionState &state, } delete[] ktest.objects; - if (errorMessage) { - auto f = openTestFile(errorSuffix, id); + if (message) { + auto f = openTestFile(suffix, id); if (f) - *f << errorMessage; + *f << message; } if (m_pathWriter) { @@ -675,9 +675,9 @@ void KleeHandler::processTestCase(const ExecutionState &state, } } - if (errorMessage && OptExitOnError) { + if (isError && OptExitOnError) { m_interpreter->prepareForEarlyExit(); - klee_error("EXITING ON ERROR:\n%s\n", errorMessage); + klee_error("EXITING ON ERROR:\n%s\n", message); } } From 0ead216e885bd8b8040967511dc5eea9f24585c7 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 14 Jul 2023 12:56:05 +0400 Subject: [PATCH 2/6] [clean] Remove `ConcretizationManager` as unnecessary --- include/klee/Expr/Assignment.h | 1 + include/klee/Solver/Common.h | 2 - include/klee/Solver/ConcretizationManager.h | 74 --------------------- include/klee/Solver/Solver.h | 2 - lib/Core/Executor.cpp | 72 ++++++++++++-------- lib/Core/Executor.h | 2 - lib/Core/TargetManager.cpp | 2 +- lib/Solver/CMakeLists.txt | 1 - lib/Solver/ConcretizationManager.cpp | 44 ------------ lib/Solver/ConcretizingSolver.cpp | 44 ------------ lib/Solver/ConstructSolverChain.cpp | 7 +- tools/kleaver/main.cpp | 2 +- 12 files changed, 48 insertions(+), 205 deletions(-) delete mode 100644 include/klee/Solver/ConcretizationManager.h delete mode 100644 lib/Solver/ConcretizationManager.cpp diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h index a31ed3c22b..ad48af0baa 100644 --- a/include/klee/Expr/Assignment.h +++ b/include/klee/Expr/Assignment.h @@ -66,6 +66,7 @@ class Assignment { bindings_ty::const_iterator begin() const { return bindings.begin(); } bindings_ty::const_iterator end() const { return bindings.end(); } + bool isEmpty() { return begin() == end(); } std::vector keys() const; std::vector> values() const; diff --git a/include/klee/Solver/Common.h b/include/klee/Solver/Common.h index 54911b1209..57ebad547d 100644 --- a/include/klee/Solver/Common.h +++ b/include/klee/Solver/Common.h @@ -15,7 +15,6 @@ #define KLEE_COMMON_H #include "klee/Solver/AddressGenerator.h" -#include "klee/Solver/ConcretizationManager.h" #include "klee/Solver/Solver.h" #include @@ -30,7 +29,6 @@ std::unique_ptr constructSolverChain( std::unique_ptr coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath, std::string baseSolverQueryKQueryLogPath, - ConcretizationManager *concretizationManager, AddressGenerator *addressGenerator); } // namespace klee diff --git a/include/klee/Solver/ConcretizationManager.h b/include/klee/Solver/ConcretizationManager.h deleted file mode 100644 index 47c99d28f0..0000000000 --- a/include/klee/Solver/ConcretizationManager.h +++ /dev/null @@ -1,74 +0,0 @@ -#ifndef KLEE_CONCRETIZATIONMANAGER_H -#define KLEE_CONCRETIZATIONMANAGER_H - -#include "klee/ADT/MapOfSets.h" -#include "klee/Expr/Assignment.h" -#include "klee/Expr/Constraints.h" -#include - -namespace klee { -struct CacheEntry; -struct CacheEntryHash; -struct Query; - -class ConcretizationManager { - using cs_entry = constraints_ty; - using sm_entry = symcretes_ty; - -private: - struct CacheEntry { - public: - CacheEntry(const cs_entry &c, const sm_entry &s, ref q) - : constraints(c), symcretes(s), query(q) {} - - CacheEntry(const CacheEntry &ce) - : constraints(ce.constraints), symcretes(ce.symcretes), - query(ce.query) {} - - cs_entry constraints; - sm_entry symcretes; - ref query; - - bool operator==(const CacheEntry &b) const { - return constraints == b.constraints && symcretes == b.symcretes && - query == b.query; - } - }; - - struct CacheEntryHash { - public: - unsigned operator()(const CacheEntry &ce) const { - unsigned result = ce.query->hash(); - - for (auto const &constraint : ce.constraints) { - result ^= constraint->hash(); - } - - return result; - } - }; - - struct CacheEntryCmp { - public: - bool operator()(const CacheEntry &ce1, const CacheEntry &ce2) const { - return ce1 == ce2; - } - }; - - typedef std::unordered_map - concretizations_map; - concretizations_map concretizations; - bool simplifyExprs; - -public: - ConcretizationManager(bool simplifyExprs) : simplifyExprs(simplifyExprs) {} - - std::pair get(const ConstraintSet &set, ref query); - bool contains(const ConstraintSet &set, ref query); - void add(const Query &q, const Assignment &assign); -}; - -}; // namespace klee - -#endif /* KLEE_CONCRETIZATIONMANAGER_H */ diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index 7e8d3dafb0..30b344efec 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -12,7 +12,6 @@ #include "klee/ADT/SparseStorage.h" #include "klee/Expr/Expr.h" -#include "klee/Solver/ConcretizationManager.h" #include "klee/Solver/SolverCmdLine.h" #include "klee/Solver/SolverUtil.h" #include "klee/System/Time.h" @@ -264,7 +263,6 @@ std::unique_ptr createCoreSolver(CoreSolverType cst); std::unique_ptr createConcretizingSolver(std::unique_ptr s, - ConcretizationManager *concretizationManager, AddressGenerator *addressGenerator); } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 03117c9c31..3962fa7e60 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -57,7 +57,6 @@ #include "klee/Module/KModule.h" #include "klee/Module/KType.h" #include "klee/Solver/Common.h" -#include "klee/Solver/ConcretizationManager.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverCmdLine.h" #include "klee/Statistics/TimerStatIncrementer.h" @@ -456,7 +455,6 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0), pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)}, - concretizationManager(new ConcretizationManager(EqualitySubstitution)), codeGraphDistance(new CodeGraphDistance()), distanceCalculator(new DistanceCalculator(*codeGraphDistance)), targetedExecutionManager(new TargetedExecutionManager( @@ -493,7 +491,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME), - concretizationManager.get(), addressManager.get()); + addressManager.get()); this->solver = std::make_unique(std::move(solver), optimizer, EqualitySubstitution); @@ -1395,28 +1393,25 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { klee_warning("seeds patched for violating constraint"); } - std::pair symcretization = - concretizationManager->get(state.constraints.cs(), condition); - - if (!symcretization.second && - Query(state.constraints.cs(), condition).containsSymcretes()) { - bool mayBeInBounds; + Assignment concretization; + if (Query(state.constraints.cs(), condition).containsSymcretes()) { + ref response; solver->setTimeout(coreSolverTimeout); - bool success = solver->mayBeTrue(state.constraints.cs(), condition, - mayBeInBounds, state.queryMetaData); + bool success = solver->getResponse(state.constraints.cs(), + Expr::createIsZero(condition), response, + state.queryMetaData); solver->setTimeout(time::Span()); assert(success); - assert(mayBeInBounds); - symcretization = - concretizationManager->get(state.constraints.cs(), condition); - assert(symcretization.second); + assert(isa(response)); + concretization = cast(response)->initialValuesFor( + state.constraints.cs().gatherSymcretizedArrays()); } - if (symcretization.second) { + if (!concretization.isEmpty()) { // Update memory objects if arrays have affected them. Assignment delta = - state.constraints.cs().concretization().diffWith(symcretization.first); - updateStateWithSymcretes(state, symcretization.first); + state.constraints.cs().concretization().diffWith(concretization); + updateStateWithSymcretes(state, delta); state.addConstraint(condition, delta); } else { state.addConstraint(condition, {}); @@ -5816,14 +5811,21 @@ bool Executor::collectConcretizations( } for (unsigned int i = 0; i < resolvedMemoryObjects.size(); ++i) { - auto symcretization = concretizationManager->get(state.constraints.cs(), - resolveConditions.at(i)); - if (symcretization.second) { - Assignment assigment = symcretization.first; - resolveConcretizations.push_back(assigment); - } else { - resolveConcretizations.push_back(state.constraints.cs().concretization()); + Assignment symcretization; + if (Query(state.constraints.cs(), resolveConditions.at(i)) + .containsSymcretes()) { + ref response; + solver->setTimeout(coreSolverTimeout); + bool success = solver->getResponse( + state.constraints.cs(), Expr::createIsZero(resolveConditions.at(i)), + response, state.queryMetaData); + solver->setTimeout(time::Span()); + assert(success); + assert(isa(response)); + symcretization = cast(response)->initialValuesFor( + state.constraints.cs().gatherSymcretizedArrays()); } + resolveConcretizations.push_back(symcretization); } return true; } @@ -7024,10 +7026,22 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { // If the particular constraint operated on in this iteration through // the loop isn't implied then add it to the list of constraints. if (!mustBeTrue) { - auto symcretization = - concretizationManager->get(extendedConstraints.cs(), pi); - if (symcretization.second) { - extendedConstraints.addConstraint(pi, symcretization.first); + Assignment symcretization; + if (Query(extendedConstraints.cs(), pi).containsSymcretes()) { + ref response; + solver->setTimeout(coreSolverTimeout); + bool success = solver->getResponse(extendedConstraints.cs(), + Expr::createIsZero(pi), response, + state.queryMetaData); + solver->setTimeout(time::Span()); + assert(success); + assert(isa(response)); + symcretization = cast(response)->initialValuesFor( + state.constraints.cs().gatherSymcretizedArrays()); + } + + if (!symcretization.isEmpty()) { + extendedConstraints.addConstraint(pi, symcretization); } else { extendedConstraints.addConstraint(pi, {}); } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 1f3298e5ea..ddce6e6632 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -31,7 +31,6 @@ #include "klee/Module/Cell.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" -#include "klee/Solver/ConcretizationManager.h" #include "klee/System/Time.h" #include "klee/Support/CompilerWarning.h" @@ -145,7 +144,6 @@ class Executor : public Interpreter { TreeStreamWriter *pathWriter, *symPathWriter; SpecialFunctionHandler *specialFunctionHandler; TimerGroup timers; - std::unique_ptr concretizationManager; std::unique_ptr processForest; std::unique_ptr codeGraphDistance; std::unique_ptr distanceCalculator; diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index 9321b4c829..840f347147 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -101,7 +101,7 @@ void TargetManager::updateTargets(ExecutionState &state) { if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { state.setTargeted(true); } - if (isTargeted(state) && !targets(state).empty()) { + if (isTargeted(state) && targets(state).empty()) { ref target(targetCalculator.calculate(state)); if (target) { state.targetForest.add(target); diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 2fbd797f6f..a1b15052bc 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -12,7 +12,6 @@ add_library(kleaverSolver CexCachingSolver.cpp ConstantDivision.cpp ConstructSolverChain.cpp - ConcretizationManager.cpp ConcretizingSolver.cpp CoreSolver.cpp DummySolver.cpp diff --git a/lib/Solver/ConcretizationManager.cpp b/lib/Solver/ConcretizationManager.cpp deleted file mode 100644 index 2c4a4a7a60..0000000000 --- a/lib/Solver/ConcretizationManager.cpp +++ /dev/null @@ -1,44 +0,0 @@ -#include "klee/Solver/ConcretizationManager.h" -#include "klee/Expr/Assignment.h" -#include "klee/Expr/Constraints.h" -#include "klee/Expr/IndependentSet.h" -#include "klee/Solver/Solver.h" -#include -#include - -using namespace klee; - -std::pair ConcretizationManager::get(const ConstraintSet &set, - ref query) { - if (simplifyExprs) { - query = Simplificator::simplifyExpr(set, query).simplified; - } - CacheEntry ce(set.cs(), set.symcretes(), query); - concretizations_map::iterator it = concretizations.find(ce); - if (it != concretizations.end()) { - return {it->second, true}; - } else { - return {Assignment(true), false}; - } -} - -bool ConcretizationManager::contains(const ConstraintSet &set, - ref query) { - if (simplifyExprs) { - query = Simplificator::simplifyExpr(set, query).simplified; - } - CacheEntry ce(set.cs(), set.symcretes(), query); - concretizations_map::iterator it = concretizations.find(ce); - return it != concretizations.end(); -} - -void ConcretizationManager::add(const Query &query, const Assignment &assign) { - ref expr = query.expr; - if (simplifyExprs) { - expr = Simplificator::simplifyExpr(query.constraints, expr).simplified; - } - CacheEntry ce(query.constraints.cs(), query.constraints.symcretes(), expr); - concretizations.insert(std::make_pair(ce, assign)); - assert(concretizations.find(ce) != concretizations.end()); - assert(contains(query.constraints, expr)); -} diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index bf0f02f08d..36f5a81191 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -8,7 +8,6 @@ #include "klee/Expr/Symcrete.h" #include "klee/Solver/AddressGenerator.h" -#include "klee/Solver/ConcretizationManager.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverImpl.h" #include "klee/Solver/SolverUtil.h" @@ -28,7 +27,6 @@ namespace klee { class ConcretizingSolver : public SolverImpl { private: std::unique_ptr solver; - ConcretizationManager *concretizationManager; AddressGenerator *addressGenerator; public: @@ -401,36 +399,14 @@ bool ConcretizingSolver::computeValidity( // appropriate for the remain branch. if (isa(queryResult)) { - concretizationManager->add( - query, - cast(negatedQueryResult)->initialValuesFor(objects)); if (!relaxSymcreteConstraints(query, queryResult)) { return false; } - if (ref queryInvalidResponse = - dyn_cast(queryResult)) { - concretizationManager->add( - query.negateExpr(), queryInvalidResponse->initialValuesFor(objects)); - } } else if (isa(negatedQueryResult)) { - concretizationManager->add( - query.negateExpr(), - cast(queryResult)->initialValuesFor(objects)); if (!relaxSymcreteConstraints(query.negateExpr(), negatedQueryResult)) { return false; } - if (ref negatedQueryInvalidResponse = - dyn_cast(negatedQueryResult)) { - concretizationManager->add( - query, negatedQueryInvalidResponse->initialValuesFor(objects)); - } } else { - concretizationManager->add( - query.negateExpr(), - cast(queryResult)->initialValuesFor(objects)); - concretizationManager->add( - query, - cast(negatedQueryResult)->initialValuesFor(objects)); } return true; @@ -456,13 +432,6 @@ bool ConcretizingSolver::check(const Query &query, } } - if (ref resultInvalidResponse = - dyn_cast(result)) { - concretizationManager->add( - query.negateExpr(), - resultInvalidResponse->initialValuesFor(assign.keys())); - } - return true; } @@ -473,10 +442,6 @@ char *ConcretizingSolver::getConstraintLog(const Query &query) { bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) { if (!query.containsSymcretes()) { if (solver->impl->computeTruth(query, isValid)) { - if (!isValid) { - concretizationManager->add(query.negateExpr(), - query.constraints.concretization()); - } return true; } return false; @@ -513,10 +478,6 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) { } } - if (!isValid) { - concretizationManager->add(query.negateExpr(), assign); - } - return true; } @@ -563,7 +524,6 @@ bool ConcretizingSolver::computeValidityCore(const Query &query, if (!isValid) { validityCore = ValidityCore(); - concretizationManager->add(query.negateExpr(), assign); } return true; @@ -617,14 +577,11 @@ bool ConcretizingSolver::computeInitialValues( dyn_cast(result)) { hasSolution = true; assign = resultInvalidResponse->initialValuesFor(assign.keys()); - concretizationManager->add(query.negateExpr(), assign); values = std::vector>(); return solver->impl->computeInitialValues( constructConcretizedQuery(query, assign), objects, values, hasSolution); } - } else { - concretizationManager->add(query.negateExpr(), assign); } return true; @@ -641,7 +598,6 @@ void ConcretizingSolver::setCoreSolverTimeout(time::Span timeout) { std::unique_ptr createConcretizingSolver(std::unique_ptr s, - ConcretizationManager *concretizationManager, AddressGenerator *addressGenerator) { return std::make_unique( std::make_unique(std::move(s), addressGenerator)); diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index 6877337983..a8eb1e2fe7 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -28,14 +28,12 @@ DISABLE_WARNING_POP #include namespace klee { -class ConcretizationManager; class AddressGenerator; std::unique_ptr constructSolverChain( std::unique_ptr coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath, std::string baseSolverQueryKQueryLogPath, - ConcretizationManager *concretizationManager, AddressGenerator *addressGenerator) { Solver *rawCoreSolver = coreSolver.get(); std::unique_ptr solver = std::move(coreSolver); @@ -72,9 +70,8 @@ std::unique_ptr constructSolverChain( if (UseIndependentSolver) solver = createIndependentSolver(std::move(solver)); - if (UseConcretizingSolver && concretizationManager) - solver = createConcretizingSolver(std::move(solver), concretizationManager, - addressGenerator); + if (UseConcretizingSolver) + solver = createConcretizingSolver(std::move(solver), addressGenerator); if (DebugValidateSolver) solver = createValidatingSolver(std::move(solver), rawCoreSolver, false); diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 5d20590afe..441e7ffacf 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -212,7 +212,7 @@ static bool EvaluateInputAST(const char *Filename, const llvm::MemoryBuffer *MB, std::move(coreSolver), getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME), nullptr, nullptr); + getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME), nullptr); unsigned Index = 0; for (std::vector::iterator it = Decls.begin(), ie = Decls.end(); From 3d60a8e5668ff9d8a0be871e88317d7f3dc5aff1 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 14 Jul 2023 12:56:20 +0400 Subject: [PATCH 3/6] [fix] Update tests and add a few fixes --- include/klee/Core/TerminationTypes.h | 6 +++--- lib/Core/Executor.cpp | 6 +++--- lib/Module/SarifReport.cpp | 8 ++++---- test/Feature/MultipleReallocResolution.c | 2 +- test/Solver/CexCacheValidityCoresCheck.c | 8 ++++---- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 16f665cfa8..06d1522923 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -40,8 +40,7 @@ enum class StateTerminationClass : std::uint8_t { TTYPE(OutOfMemory, 12U, "early") \ TTYPE(OutOfStackMemory, 13U, "early") \ TTYPE(MaxCycles, 14U, "early") \ - TTYPE(MissedAllTargets, 15U, "miss_all_targets.early") \ - TTMARK(EARLY, 15U) \ + TTMARK(EARLY, 14U) \ TTYPE(Solver, 20U, "solver.err") \ TTMARK(SOLVERERR, 20U) \ TTYPE(Abort, 30U, "abort.err") \ @@ -70,7 +69,8 @@ enum class StateTerminationClass : std::uint8_t { TTYPE(External, 61U, "external.err") \ TTMARK(EXECERR, 61U) \ TTYPE(Replay, 70U, "") \ - TTMARK(EARLYALGORITHM, 70U) \ + TTYPE(MissedAllTargets, 71U, "miss_all_targets.early") \ + TTMARK(EARLYALGORITHM, 71U) \ TTYPE(SilentExit, 80U, "") \ TTMARK(EARLYUSER, 80U) \ TTMARK(END, 80U) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3962fa7e60..3d96310b7a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4332,8 +4332,8 @@ void Executor::initializeTypeManager() { void Executor::executeStep(ExecutionState &state) { KInstruction *prevKI = state.prevPC; if (targetManager->isTargeted(state) && state.targets().empty()) { - terminateStateEarly(state, "State missed all it's targets.", - StateTerminationType::MissedAllTargets); + terminateStateEarlyAlgorithm(state, "State missed all it's targets.", + StateTerminationType::MissedAllTargets); } else if (prevKI->inst->isTerminator() && state.multilevel[state.getPCBlock()] > MaxCycles - 1) { terminateStateEarly(state, "max-cycles exceeded.", @@ -4486,7 +4486,7 @@ void Executor::terminateState(ExecutionState &state, StateTerminationType terminationType) { state.terminationReasonType = fromStateTerminationType(terminationType); if (terminationType >= StateTerminationType::MaxDepth && - terminationType < StateTerminationType::MissedAllTargets) { + terminationType <= StateTerminationType::EARLY) { SetOfStates states = {&state}; decreaseConfidenceFromStoppedStates(states, state.terminationReasonType); } diff --git a/lib/Module/SarifReport.cpp b/lib/Module/SarifReport.cpp index 6af80b66b0..075ce32417 100644 --- a/lib/Module/SarifReport.cpp +++ b/lib/Module/SarifReport.cpp @@ -69,7 +69,7 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } else if (toolName == "clang") { if ("core.NullDereference" == ruleId) { return {ReachWithError::MayBeNullPointerException, - ReachWithError::MayBeNullPointerException}; + ReachWithError::MustBeNullPointerException}; } else if ("unix.Malloc" == ruleId) { if (errorMessage.has_value()) { if (errorMessage->text == "Attempt to free released memory") { @@ -90,7 +90,7 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } else if (toolName == "CppCheck") { if ("nullPointer" == ruleId || "ctunullpointer" == ruleId) { return {ReachWithError::MayBeNullPointerException, - ReachWithError::MayBeNullPointerException}; // TODO: check it out + ReachWithError::MustBeNullPointerException}; // TODO: check it out } else if ("doubleFree" == ruleId) { return {ReachWithError::DoubleFree}; } else { @@ -99,7 +99,7 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } else if (toolName == "Infer") { if ("NULL_DEREFERENCE" == ruleId || "NULLPTR_DEREFERENCE" == ruleId) { return {ReachWithError::MayBeNullPointerException, - ReachWithError::MayBeNullPointerException}; // TODO: check it out + ReachWithError::MustBeNullPointerException}; // TODO: check it out } else if ("USE_AFTER_DELETE" == ruleId || "USE_AFTER_FREE" == ruleId) { return {ReachWithError::UseAfterFree, ReachWithError::DoubleFree}; } else { @@ -108,7 +108,7 @@ tryConvertRuleJson(const std::string &ruleId, const std::string &toolName, } else if (toolName == "Cooddy") { if ("NULL.DEREF" == ruleId || "NULL.UNTRUSTED.DEREF" == ruleId) { return {ReachWithError::MayBeNullPointerException, - ReachWithError::MayBeNullPointerException}; + ReachWithError::MustBeNullPointerException}; } else if ("MEM.DOUBLE.FREE" == ruleId) { return {ReachWithError::DoubleFree}; } else if ("MEM.USE.FREE" == ruleId) { diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c index feb01bce62..d7a182ab11 100644 --- a/test/Feature/MultipleReallocResolution.c +++ b/test/Feature/MultipleReallocResolution.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --use-guided-search=none--output-dir=%t.klee-out %t1.bc +// RUN: %klee --use-guided-search=none --output-dir=%t.klee-out %t1.bc // RUN: ls %t.klee-out/ | grep .err | wc -l | grep 2 // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2 diff --git a/test/Solver/CexCacheValidityCoresCheck.c b/test/Solver/CexCacheValidityCoresCheck.c index f471847121..26ba133d63 100644 --- a/test/Solver/CexCacheValidityCoresCheck.c +++ b/test/Solver/CexCacheValidityCoresCheck.c @@ -2,8 +2,8 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t1.klee-out // RUN: rm -rf %t2.klee-out -// RUN: %klee --output-dir=%t1.klee-out --cex-cache-validity-cores=false --solver-backend=z3 %t1.bc -// RUN: %klee --output-dir=%t2.klee-out --cex-cache-validity-cores=true --solver-backend=z3 %t1.bc +// RUN: %klee --output-dir=%t1.klee-out --use-guided-search=none --cex-cache-validity-cores=false --solver-backend=z3 %t1.bc +// RUN: %klee --output-dir=%t2.klee-out --use-guided-search=none --cex-cache-validity-cores=true --solver-backend=z3 %t1.bc // RUN: %klee-stats --print-columns 'QCexCacheHits,SolverQueries' --table-format=csv %t1.klee-out > %t1.stats // RUN: %klee-stats --print-columns 'QCexCacheHits,SolverQueries' --table-format=csv %t2.klee-out > %t2.stats // RUN: FileCheck -check-prefix=CHECK-CACHE-OFF -input-file=%t1.stats %s @@ -30,6 +30,6 @@ int main(int argc, char **argv) { } } // CHECK-CACHE-ON: QCexCacheHits,SolverQueries -// CHECK-CACHE-ON: 277,124 +// CHECK-CACHE-ON: 1461,202 // CHECK-CACHE-OFF: QCexCacheHits,SolverQueries -// CHECK-CACHE-OFF: 226,175 +// CHECK-CACHE-OFF: 1011,652 From 7253073da665c7212b715453b421cbc175f1ad68 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 15 Jul 2023 02:26:12 +0400 Subject: [PATCH 4/6] [refactor] Replace `stack_ty` --- lib/Core/DistanceCalculator.cpp | 5 +- lib/Core/DistanceCalculator.h | 2 +- lib/Core/ExecutionState.cpp | 104 ++++++++++++++------------ lib/Core/ExecutionState.h | 77 ++++++++++++------- lib/Core/Executor.cpp | 68 +++++++++-------- lib/Core/Executor.h | 4 +- lib/Core/Searcher.cpp | 4 +- lib/Core/SpecialFunctionHandler.cpp | 10 ++- lib/Core/StatsTracker.cpp | 40 ++++++---- lib/Core/StatsTracker.h | 4 +- lib/Core/TargetCalculator.cpp | 5 +- lib/Core/TargetedExecutionManager.cpp | 2 +- 12 files changed, 189 insertions(+), 136 deletions(-) diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index 98433ff0c6..774303a28b 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -51,7 +51,8 @@ unsigned DistanceCalculator::SpeculativeState::computeHash() { DistanceResult DistanceCalculator::getDistance(const ExecutionState &state, ref target) { - return getDistance(state.prevPC, state.pc, state.frames, state.error, target); + return getDistance(state.prevPC, state.pc, state.stack.uniqueFrames(), + state.error, target); } DistanceResult DistanceCalculator::getDistance(KBlock *kb, TargetKind kind, @@ -103,7 +104,7 @@ DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind, DistanceResult DistanceCalculator::getDistance(const KInstruction *prevPC, const KInstruction *pc, - const ExecutionState::frames_ty &frames, + const ExecutionStack::call_stack_ty &frames, ReachWithError error, ref target) { weight_type weight = 0; diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h index d791680f1f..3f24018586 100644 --- a/lib/Core/DistanceCalculator.h +++ b/lib/Core/DistanceCalculator.h @@ -51,7 +51,7 @@ class DistanceCalculator { DistanceResult getDistance(const ExecutionState &es, ref target); DistanceResult getDistance(const KInstruction *prevPC, const KInstruction *pc, - const ExecutionState::frames_ty &frames, + const ExecutionStack::call_stack_ty &frames, ReachWithError error, ref target); private: diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index b9806c8212..17a55162e7 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -63,37 +63,62 @@ std::uint32_t ExecutionState::nextID = 1; /***/ -int CallStackFrame::compare(const CallStackFrame &other) const { - if (kf != other.kf) { - return kf < other.kf ? -1 : 1; +void ExecutionStack::pushFrame(KInstIterator caller, KFunction *kf) { + valueStack_.emplace_back(StackFrame(kf)); + if (std::find(callStack_.begin(), callStack_.end(), + CallStackFrame(caller, kf)) == callStack_.end()) { + uniqueFrames_.emplace_back(CallStackFrame(caller, kf)); } - if (!caller || !other.caller) { - return !caller ? !other.caller ? 0 : -1 : 1; - } - if (caller != other.caller) { - return caller < other.caller ? -1 : 1; + callStack_.emplace_back(CallStackFrame(caller, kf)); + infoStack_.emplace_back(InfoStackFrame(kf)); + ++stackBalance; + assert(valueStack_.size() == callStack_.size()); + assert(valueStack_.size() == infoStack_.size()); +} + +void ExecutionStack::popFrame() { + assert(callStack_.size() > 0); + KInstIterator caller = callStack_.back().caller; + KFunction *kf = callStack_.back().kf; + valueStack_.pop_back(); + callStack_.pop_back(); + infoStack_.pop_back(); + auto it = std::find(callStack_.begin(), callStack_.end(), + CallStackFrame(caller, kf)); + if (it == callStack_.end()) { + uniqueFrames_.pop_back(); } - return 0; + --stackBalance; + assert(valueStack_.size() == callStack_.size()); + assert(valueStack_.size() == infoStack_.size()); } -StackFrame::StackFrame(KInstIterator _caller, KFunction *_kf) - : caller(_caller), kf(_kf), callPathNode(0), minDistToUncoveredOnReturn(0), - varargs(0) { +bool CallStackFrame::equals(const CallStackFrame &other) const { + return kf == other.kf && caller == other.caller; +} + +StackFrame::StackFrame(KFunction *kf) : kf(kf), varargs(0) { locals = new Cell[kf->numRegisters]; } StackFrame::StackFrame(const StackFrame &s) - : caller(s.caller), kf(s.kf), callPathNode(s.callPathNode), - allocas(s.allocas), - minDistToUncoveredOnReturn(s.minDistToUncoveredOnReturn), - varargs(s.varargs) { - locals = new Cell[s.kf->numRegisters]; - for (unsigned i = 0; i < s.kf->numRegisters; i++) + : kf(s.kf), allocas(s.allocas), varargs(s.varargs) { + locals = new Cell[kf->numRegisters]; + for (unsigned i = 0; i < kf->numRegisters; i++) locals[i] = s.locals[i]; } StackFrame::~StackFrame() { delete[] locals; } +CallStackFrame::CallStackFrame(const CallStackFrame &s) + : caller(s.caller), kf(s.kf) {} + +InfoStackFrame::InfoStackFrame(KFunction *kf) : kf(kf) {} + +InfoStackFrame::InfoStackFrame(const InfoStackFrame &s) + : kf(s.kf), callPathNode(s.callPathNode), + minDistToUncoveredOnReturn(s.minDistToUncoveredOnReturn) {} + /***/ ExecutionState::ExecutionState() : initPC(nullptr), pc(nullptr), prevPC(nullptr), incomingBBIndex(-1), @@ -134,9 +159,9 @@ ExecutionState::~ExecutionState() { ExecutionState::ExecutionState(const ExecutionState &state) : initPC(state.initPC), pc(state.pc), prevPC(state.prevPC), - stack(state.stack), callStack(state.callStack), frames(state.frames), - stackBalance(state.stackBalance), incomingBBIndex(state.incomingBBIndex), - depth(state.depth), multilevel(state.multilevel), level(state.level), + stack(state.stack), stackBalance(state.stackBalance), + incomingBBIndex(state.incomingBBIndex), depth(state.depth), + multilevel(state.multilevel), level(state.level), transitionLevel(state.transitionLevel), addressSpace(state.addressSpace), constraints(state.constraints), targetForest(state.targetForest), pathOS(state.pathOS), symPathOS(state.symPathOS), @@ -213,31 +238,18 @@ ExecutionState *ExecutionState::copy() const { } void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) { - stack.emplace_back(StackFrame(caller, kf)); - if (std::find(callStack.begin(), callStack.end(), - CallStackFrame(caller, kf)) == callStack.end()) { - frames.emplace_back(CallStackFrame(caller, kf)); - } - callStack.emplace_back(CallStackFrame(caller, kf)); - ++stackBalance; + stack.pushFrame(caller, kf); } void ExecutionState::popFrame() { - const StackFrame &sf = stack.back(); + const StackFrame &sf = stack.valueStack().back(); for (const auto id : sf.allocas) { const MemoryObject *memoryObject = addressSpace.findObject(id).first; assert(memoryObject); removePointerResolutions(memoryObject); addressSpace.unbindObject(memoryObject); } - stack.pop_back(); - callStack.pop_back(); - auto it = std::find(callStack.begin(), callStack.end(), - CallStackFrame(sf.caller, sf.kf)); - if (it == callStack.end()) { - frames.pop_back(); - } - --stackBalance; + stack.popFrame(); } void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array, @@ -388,15 +400,15 @@ llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, } void ExecutionState::dumpStack(llvm::raw_ostream &out) const { - unsigned idx = 0; const KInstruction *target = prevPC; - for (ExecutionState::stack_ty::const_reverse_iterator it = stack.rbegin(), - ie = stack.rend(); - it != ie; ++it) { - const StackFrame &sf = *it; - Function *f = sf.kf->function; + for (unsigned i = 0; i < stack.size(); ++i) { + unsigned ri = stack.size() - 1 - i; + const CallStackFrame &csf = stack.callStack().at(ri); + const StackFrame &sf = stack.valueStack().at(ri); + + Function *f = csf.kf->function; const InstructionInfo &ii = *target->info; - out << "\t#" << idx++; + out << "\t#" << i; if (ii.assemblyLine.hasValue()) { std::stringstream AssStream; AssStream << std::setw(8) << std::setfill('0') @@ -414,7 +426,7 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const { if (ai->hasName()) out << ai->getName().str() << "="; - ref value = sf.locals[sf.kf->getArgRegister(index++)].value; + ref value = sf.locals[csf.kf->getArgRegister(index++)].value; if (isa_and_nonnull(value)) { out << value; } else { @@ -425,7 +437,7 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const { if (ii.file != "") out << " at " << ii.file << ":" << ii.line; out << "\n"; - target = sf.caller; + target = csf.caller; } } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 7c9ad8fd80..1a2751a054 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -60,39 +60,24 @@ llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); extern llvm::cl::opt MaxCyclesBeforeStuck; struct CallStackFrame { - KInstruction *caller; + KInstIterator caller; KFunction *kf; - CallStackFrame(KInstruction *caller_, KFunction *kf_) + CallStackFrame(KInstIterator caller_, KFunction *kf_) : caller(caller_), kf(kf_) {} ~CallStackFrame() = default; + CallStackFrame(const CallStackFrame &s); - int compare(const CallStackFrame &other) const; - - bool operator<(const CallStackFrame &other) const { - return compare(other) == -1; - } + bool equals(const CallStackFrame &other) const; - bool operator==(const CallStackFrame &other) const { - return compare(other) == 0; - } + bool operator==(const CallStackFrame &other) const { return equals(other); } }; struct StackFrame { - KInstIterator caller; KFunction *kf; - CallPathNode *callPathNode; - std::vector allocas; Cell *locals; - /// Minimum distance to an uncovered instruction once the function - /// returns. This is not a good place for this but is used to - /// quickly compute the context sensitive minimum distance to an - /// uncovered instruction. This value is updated by the StatsTracker - /// periodically. - unsigned minDistToUncoveredOnReturn; - // For vararg functions: arguments not passed via parameter are // stored (packed tightly) in a local (alloca) memory object. This // is set up to match the way the front-end generates vaarg code (it @@ -100,11 +85,53 @@ struct StackFrame { // of intrinsic lowering. MemoryObject *varargs; - StackFrame(KInstIterator caller, KFunction *kf); + StackFrame(KFunction *kf); StackFrame(const StackFrame &s); ~StackFrame(); }; +struct InfoStackFrame { + KFunction *kf; + CallPathNode *callPathNode = nullptr; + + /// Minimum distance to an uncovered instruction once the function + /// returns. This is not a good place for this but is used to + /// quickly compute the context sensitive minimum distance to an + /// uncovered instruction. This value is updated by the StatsTracker + /// periodically. + unsigned minDistToUncoveredOnReturn = 0; + + InfoStackFrame(KFunction *kf); + InfoStackFrame(const InfoStackFrame &s); + ~InfoStackFrame() = default; +}; + +struct ExecutionStack { +public: + using value_stack_ty = std::vector; + using call_stack_ty = std::vector; + using info_stack_ty = std::vector; + +private: + value_stack_ty valueStack_; + call_stack_ty callStack_; + info_stack_ty infoStack_; + call_stack_ty uniqueFrames_; + unsigned stackBalance = 0; + +public: + void pushFrame(KInstIterator caller, KFunction *kf); + void popFrame(); + inline value_stack_ty &valueStack() { return valueStack_; } + inline const value_stack_ty &valueStack() const { return valueStack_; } + inline const call_stack_ty &callStack() const { return callStack_; } + inline info_stack_ty &infoStack() { return infoStack_; } + inline const call_stack_ty &uniqueFrames() const { return uniqueFrames_; } + + inline unsigned size() const { return callStack_.size(); } + inline bool empty() const { return callStack_.empty(); } +}; + /// Contains information related to unwinding (Itanium ABI/2-Phase unwinding) class UnwindingInformation { public: @@ -229,9 +256,7 @@ class ExecutionState { ExecutionState(const ExecutionState &state); public: - using stack_ty = std::vector; - using call_stack_ty = std::vector; - using frames_ty = std::vector; + using stack_ty = ExecutionStack; // Execution - Control Flow specific @@ -245,10 +270,8 @@ class ExecutionState { /// @brief Pointer to instruction which is currently executed KInstIterator prevPC; - /// @brief Stack representing the current instruction stream + /// @brief Execution stack representing the current instruction stream stack_ty stack; - call_stack_ty callStack; - frames_ty frames; int stackBalance = 0; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3d96310b7a..ce6d27aee6 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1051,7 +1051,7 @@ ref Executor::maxStaticPctChecks(ExecutionState ¤t, return condition; StatisticManager &sm = *theStatisticManager; - CallPathNode *cpn = current.stack.back().callPathNode; + CallPathNode *cpn = current.stack.infoStack().back().callPathNode; bool reached_max_fork_limit = (MaxStaticForkPct < 1. && @@ -1100,8 +1100,8 @@ bool Executor::canReachSomeTargetFromBlock(ExecutionState &es, KBlock *block) { auto target = p.first; if (target->mustVisitForkBranches(es.prevPC)) return true; - auto dist = distanceCalculator->getDistance(es.prevPC, nextInstr, es.frames, - es.error, target); + auto dist = distanceCalculator->getDistance( + es.prevPC, nextInstr, es.stack.callStack(), es.error, target); if (dist.result != WeightResult::Miss) return true; } @@ -1447,7 +1447,7 @@ const Cell &Executor::eval(const KInstruction *ki, unsigned index, const Cell &Executor::eval(const KInstruction *ki, unsigned index, ExecutionState &state, bool isSymbolic) { - return eval(ki, index, state, state.stack.back(), isSymbolic); + return eval(ki, index, state, state.stack.valueStack().back(), isSymbolic); } void Executor::bindLocal(const KInstruction *target, StackFrame &frame, @@ -1756,7 +1756,7 @@ void Executor::unwindToNextLandingpad(ExecutionState &state) { lowestStackIndex = 0; popFrames = false; } else if (auto *cui = dyn_cast(ui)) { - startIndex = state.stack.size() - 1; + startIndex = state.stack.callStack().size() - 1; lowestStackIndex = cui->catchingStackIndex; popFrames = true; } else { @@ -1764,7 +1764,7 @@ void Executor::unwindToNextLandingpad(ExecutionState &state) { } for (std::size_t i = startIndex; i > lowestStackIndex; i--) { - auto const &sf = state.stack.at(i); + auto const &sf = state.stack.callStack().at(i); Instruction *inst = sf.caller ? sf.caller->inst : nullptr; @@ -1818,8 +1818,8 @@ void Executor::unwindToNextLandingpad(ExecutionState &state) { bindArgument(kf, 2, state, clauses_mo->getBaseExpr()); if (statsTracker) { - statsTracker->framePushed(state, - &state.stack[state.stack.size() - 2]); + statsTracker->framePushed( + state, &state.stack.infoStack()[state.stack.size() - 2]); } // make sure we remember our search progress afterwards @@ -2110,7 +2110,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, // va_arg is handled by caller and intrinsic lowering, see comment for // ExecutionState::varargs case Intrinsic::vastart: { - StackFrame &sf = state.stack.back(); + StackFrame &sf = state.stack.valueStack().back(); // varargs can be zero if no varargs were provided if (!sf.varargs) @@ -2196,7 +2196,8 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, state); if (statsTracker) - statsTracker->framePushed(state, &state.stack[state.stack.size() - 2]); + statsTracker->framePushed( + state, &state.stack.infoStack()[state.stack.size() - 2]); // TODO: support zeroext, signext, sret attributes @@ -2274,7 +2275,7 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, } } - StackFrame &sf = state.stack.back(); + StackFrame &sf = state.stack.valueStack().back(); MemoryObject *mo = sf.varargs = memory->allocate(size, true, false, false, state.prevPC->inst, (requires16ByteAlignment ? 16 : 8)); @@ -2368,7 +2369,7 @@ void Executor::transferToBasicBlock(KBlock *kdst, BasicBlock *src, void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src, ExecutionState &state) { - KFunction *kf = state.stack.back().kf; + KFunction *kf = state.stack.callStack().back().kf; auto kdst = kf->blockMap[dst]; transferToBasicBlock(kdst, src, state); } @@ -2417,7 +2418,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Control flow case Instruction::Ret: { ReturnInst *ri = cast(i); - KInstIterator kcaller = state.stack.back().caller; + KInstIterator kcaller = state.stack.callStack().back().caller; Instruction *caller = kcaller ? kcaller->inst : nullptr; bool isVoidReturn = (ri->getNumOperands() == 0); ref result = ConstantExpr::alloc(0, Expr::Bool); @@ -2531,7 +2532,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { cond = optimizer.optimizeExpr(cond, false); - KFunction *kf = state.stack.back().kf; + KFunction *kf = state.stack.callStack().back().kf; auto ifTrueBlock = kf->blockMap[bi->getSuccessor(0)]; auto ifFalseBlock = kf->blockMap[bi->getSuccessor(1)]; Executor::StatePair branches = @@ -2541,7 +2542,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // requires that we still be in the context of the branch // instruction (it reuses its statistic id). Should be cleaned // up with convenient instruction specific data. - if (statsTracker && state.stack.back().kf->trackCoverage) + if (statsTracker && state.stack.callStack().back().kf->trackCoverage) statsTracker->markBranchVisited(branches.first, branches.second); if (branches.first) @@ -2580,7 +2581,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { ref errorCase = ConstantExpr::alloc(1, Expr::Bool); SmallPtrSet destinations; - KFunction *kf = state.stack.back().kf; + KFunction *kf = state.stack.callStack().back().kf; // collect and check destinations from label list for (unsigned k = 0; k < numDestinations; ++k) { // filter duplicates @@ -2675,7 +2676,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Track default branch values ref defaultValue = ConstantExpr::alloc(1, Expr::Bool); - KFunction *kf = state.stack.back().kf; + KFunction *kf = state.stack.callStack().back().kf; // iterate through all non-default cases but in order of the expressions for (std::map, BasicBlock *>::iterator @@ -4545,7 +4546,9 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message, ++stats::terminationEarly; } - if ((reason <= StateTerminationType::EARLY && shouldWriteTest(state)) || + if (((reason <= StateTerminationType::EARLY || + reason == StateTerminationType::MissedAllTargets) && + shouldWriteTest(state)) || (AlwaysOutputSeeds && seedMap.count(&state))) { interpreterHandler->processTestCase( state, (message + "\n").str().c_str(), @@ -4576,8 +4579,9 @@ Executor::getLastNonKleeInternalInstruction(const ExecutionState &state, Instruction **lastInstruction) { // unroll the stack of the applications state and find // the last instruction which is not inside a KLEE internal function - ExecutionState::stack_ty::const_reverse_iterator it = state.stack.rbegin(), - itE = state.stack.rend(); + ExecutionStack::call_stack_ty::const_reverse_iterator + it = state.stack.callStack().rbegin(), + itE = state.stack.callStack().rend(); // don't check beyond the outermost function (i.e. main()) itE--; @@ -4697,7 +4701,7 @@ void Executor::terminateStateOnError(ExecutionState &state, } msg << "State: " << state.getID() << '\n'; } - msg << "Stack: \n"; + msg << "ExecutionStack: \n"; state.dumpStack(msg); std::string info_str = info.str(); @@ -5014,7 +5018,7 @@ ObjectState *Executor::bindObjectInState(ExecutionState &state, // matter because all we use this list for is to unbind the object // on function return. if (isLocal && state.stack.size() > 0) { - state.stack.back().allocas.push_back(mo->id); + state.stack.valueStack().back().allocas.push_back(mo->id); } return os; } @@ -6338,7 +6342,8 @@ IDType Executor::lazyInitializeLocalObject(ExecutionState &state, IDType Executor::lazyInitializeLocalObject(ExecutionState &state, ref address, const KInstruction *target) { - return lazyInitializeLocalObject(state, state.stack.back(), address, target); + return lazyInitializeLocalObject(state, state.stack.valueStack().back(), + address, target); } void Executor::updateStateWithSymcretes(ExecutionState &state, @@ -6708,7 +6713,7 @@ ExecutionState *Executor::prepareStateForPOSIX(KInstIterator &caller, targetedRun(*state, target, &initialState); state = initialState; if (state) { - auto frame = state->stack.back(); + auto frame = state->stack.callStack().back(); caller = frame.caller; state->popFrame(); delete original; @@ -6780,12 +6785,12 @@ void Executor::prepareMockValue(ExecutionState &state, const std::string &name, KInstruction *target) { Expr::Width width = kmodule->targetData->getTypeSizeInBits(target->inst->getType()); - prepareMockValue(state, state.stack.back(), name, width, target); + prepareMockValue(state, state.stack.valueStack().back(), name, width, target); } void Executor::prepareSymbolicValue(ExecutionState &state, KInstruction *target) { - prepareSymbolicValue(state, state.stack.back(), target); + prepareSymbolicValue(state, state.stack.valueStack().back(), target); } void Executor::prepareSymbolicRegister(ExecutionState &state, StackFrame &sf, @@ -6815,7 +6820,7 @@ void Executor::prepareSymbolicArgs(ExecutionState &state, StackFrame &frame) { } void Executor::prepareSymbolicArgs(ExecutionState &state) { - prepareSymbolicArgs(state, state.stack.back()); + prepareSymbolicArgs(state, state.stack.valueStack().back()); } unsigned Executor::getPathStreamID(const ExecutionState &state) { @@ -7241,12 +7246,13 @@ void Executor::dumpStates() { for (ExecutionState *es : states) { *os << "(" << es << ","; *os << "["; - auto next = es->stack.begin(); + auto next = es->stack.callStack().begin(); ++next; - for (auto sfIt = es->stack.begin(), sf_ie = es->stack.end(); + for (auto sfIt = es->stack.callStack().begin(), + sf_ie = es->stack.callStack().end(); sfIt != sf_ie; ++sfIt) { *os << "('" << sfIt->kf->function->getName().str() << "',"; - if (next == es->stack.end()) { + if (next == es->stack.callStack().end()) { *os << es->prevPC->info->line << "), "; } else { *os << next->caller->info->line << "), "; @@ -7255,7 +7261,7 @@ void Executor::dumpStates() { } *os << "], "; - StackFrame &sf = es->stack.back(); + InfoStackFrame &sf = es->stack.infoStack().back(); uint64_t md2u = computeMinDistToUncovered(es->pc, sf.minDistToUncoveredOnReturn); uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index ddce6e6632..28f26f99cc 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -499,11 +499,11 @@ class Executor : public Interpreter { Cell &getArgumentCell(const ExecutionState &state, const KFunction *kf, unsigned index) { - return getArgumentCell(state.stack.back(), kf, index); + return getArgumentCell(state.stack.valueStack().back(), kf, index); } Cell &getDestCell(const ExecutionState &state, const KInstruction *target) { - return getDestCell(state.stack.back(), target); + return getDestCell(state.stack.valueStack().back(), target); } void bindLocal(const KInstruction *target, StackFrame &frame, diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index a89396b2ea..1be798e88c 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -395,7 +395,7 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { return inv * inv; } case CPInstCount: { - StackFrame &sf = es->stack.back(); + const InfoStackFrame &sf = es->stack.infoStack().back(); uint64_t count = sf.callPathNode->statistics.getValue(stats::instructions); double inv = 1. / std::max((uint64_t)1, count); return inv; @@ -407,7 +407,7 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) { case CoveringNew: case MinDistToUncovered: { uint64_t md2u = computeMinDistToUncovered( - es->pc, es->stack.back().minDistToUncoveredOnReturn); + es->pc, es->stack.infoStack().back().minDistToUncoveredOnReturn); double invMD2U = 1. / (md2u ? md2u : 10000); if (type == CoveringNew) { diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 60c65f14ba..1d3e07b85f 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -625,7 +625,8 @@ void SpecialFunctionHandler::handleWarning(ExecutionState &state, "invalid number of arguments to klee_warning"); std::string msg_str = readStringAtAddress(state, arguments[0]); - klee_warning("%s: %s", state.stack.back().kf->function->getName().data(), + klee_warning("%s: %s", + state.stack.callStack().back().kf->function->getName().data(), msg_str.c_str()); } @@ -636,9 +637,10 @@ void SpecialFunctionHandler::handleWarningOnce( "invalid number of arguments to klee_warning_once"); std::string msg_str = readStringAtAddress(state, arguments[0]); - klee_warning_once(0, "%s: %s", - state.stack.back().kf->function->getName().data(), - msg_str.c_str()); + klee_warning_once( + 0, "%s: %s", + state.stack.callStack().back().kf->function->getName().data(), + msg_str.c_str()); } void SpecialFunctionHandler::handlePrintRange( diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 1ccc43d5ce..372c6fc61b 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -394,7 +394,7 @@ void StatsTracker::stepInstruction(ExecutionState &es) { Instruction *inst = es.pc->inst; const InstructionInfo &ii = *es.pc->info; - StackFrame &sf = es.stack.back(); + InfoStackFrame &sf = es.stack.infoStack().back(); theStatisticManager->setIndex(ii.id); if (UseCallPaths) theStatisticManager->setContext(&sf.callPathNode->statistics); @@ -438,28 +438,31 @@ void StatsTracker::stepInstruction(ExecutionState &es) { /// /* Should be called _after_ the es->pushFrame() */ -void StatsTracker::framePushed(ExecutionState &es, StackFrame *parentFrame) { +void StatsTracker::framePushed(ExecutionState &es, + InfoStackFrame *parentFrame) { if (OutputIStats) { - StackFrame &sf = es.stack.back(); + const CallStackFrame &csf = es.stack.callStack().back(); + InfoStackFrame &isf = es.stack.infoStack().back(); if (UseCallPaths) { CallPathNode *parent = parentFrame ? parentFrame->callPathNode : 0; CallPathNode *cp = callPathManager.getCallPath( - parent, sf.caller ? sf.caller->inst : 0, sf.kf->function); - sf.callPathNode = cp; + parent, csf.caller ? csf.caller->inst : 0, csf.kf->function); + isf.callPathNode = cp; cp->count++; } } if (updateMinDistToUncovered) { - StackFrame &sf = es.stack.back(); + const CallStackFrame &csf = es.stack.callStack().back(); + InfoStackFrame &isf = es.stack.infoStack().back(); uint64_t minDistAtRA = 0; if (parentFrame) minDistAtRA = parentFrame->minDistToUncoveredOnReturn; - sf.minDistToUncoveredOnReturn = - sf.caller ? computeMinDistToUncovered(sf.caller, minDistAtRA) : 0; + isf.minDistToUncoveredOnReturn = + csf.caller ? computeMinDistToUncovered(csf.caller, minDistAtRA) : 0; } } @@ -698,8 +701,8 @@ void StatsTracker::updateStateStatistics(uint64_t addend) { const InstructionInfo &ii = *state.pc->info; theStatisticManager->incrementIndexedValue(stats::states, ii.id, addend); if (UseCallPaths) - state.stack.back().callPathNode->statistics.incrementValue(stats::states, - addend); + state.stack.infoStack().back().callPathNode->statistics.incrementValue( + stats::states, addend); } } @@ -1132,20 +1135,25 @@ void StatsTracker::computeReachableUncovered() { it != ie; ++it) { ExecutionState *es = *it; uint64_t currentFrameMinDist = 0; - for (ExecutionState::stack_ty::iterator sfIt = es->stack.begin(), - sf_ie = es->stack.end(); - sfIt != sf_ie; ++sfIt) { - ExecutionState::stack_ty::iterator next = sfIt + 1; + ExecutionStack::call_stack_ty::const_iterator + sfIt = es->stack.callStack().begin(), + sf_ie = es->stack.callStack().end(); + ExecutionStack::info_stack_ty::iterator isfIt = + es->stack.infoStack().begin(), + isf_ie = + es->stack.infoStack().end(); + for (; sfIt != sf_ie && isfIt != isf_ie; ++sfIt, ++isfIt) { + ExecutionStack::call_stack_ty::const_iterator next = sfIt + 1; KInstIterator kii; - if (next == es->stack.end()) { + if (next == sf_ie) { kii = es->pc; } else { kii = next->caller; ++kii; } - sfIt->minDistToUncoveredOnReturn = currentFrameMinDist; + isfIt->minDistToUncoveredOnReturn = currentFrameMinDist; currentFrameMinDist = computeMinDistToUncovered(kii, currentFrameMinDist); } diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index cd479dc529..be0f39ae5b 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -30,7 +30,7 @@ class Executor; class InstructionInfoTable; class InterpreterHandler; struct KInstruction; -struct StackFrame; +struct InfoStackFrame; class StatsTracker { friend class WriteStatsTimer; @@ -79,7 +79,7 @@ class StatsTracker { StatsTracker &operator=(StatsTracker &&other) noexcept = delete; // called after a new StackFrame has been pushed (for callpath tracing) - void framePushed(ExecutionState &es, StackFrame *parentFrame); + void framePushed(ExecutionState &es, InfoStackFrame *parentFrame); // called after a StackFrame has been popped void framePopped(ExecutionState &es); diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index 8975b32e21..c56417d5a2 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -98,8 +98,9 @@ ref TargetCalculator::calculate(ExecutionState &state) { unsigned int minDistance = UINT_MAX; unsigned int sfNum = 0; bool newCov = false; - for (auto sfi = state.stack.rbegin(), sfe = state.stack.rend(); sfi != sfe; - sfi++, sfNum++) { + for (auto sfi = state.stack.callStack().rbegin(), + sfe = state.stack.callStack().rend(); + sfi != sfe; sfi++, sfNum++) { kf = sfi->kf; for (const auto &kbd : codeGraphDistance.getSortedDistance(kb)) { diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index cfbad46826..20cb63683f 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -546,7 +546,7 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, found = false; break; } - possibleInstruction = state.stack[i].caller; + possibleInstruction = state.stack.callStack().at(i).caller; i--; } if (!found) From add7dc104a8299e8045f8a82ba66579e9271183c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 17 Jul 2023 23:13:15 +0400 Subject: [PATCH 5/6] [refactor] Add `computeConcretization` --- lib/Core/Executor.cpp | 71 +++++++++++++++++-------------------------- lib/Core/Executor.h | 4 +++ 2 files changed, 32 insertions(+), 43 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ce6d27aee6..8488d3a884 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1393,19 +1393,8 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { klee_warning("seeds patched for violating constraint"); } - Assignment concretization; - if (Query(state.constraints.cs(), condition).containsSymcretes()) { - ref response; - solver->setTimeout(coreSolverTimeout); - bool success = solver->getResponse(state.constraints.cs(), - Expr::createIsZero(condition), response, - state.queryMetaData); - solver->setTimeout(time::Span()); - assert(success); - assert(isa(response)); - concretization = cast(response)->initialValuesFor( - state.constraints.cs().gatherSymcretizedArrays()); - } + Assignment concretization = computeConcretization( + state.constraints.cs(), condition, state.queryMetaData); if (!concretization.isEmpty()) { // Update memory objects if arrays have affected them. @@ -5815,22 +5804,11 @@ bool Executor::collectConcretizations( } for (unsigned int i = 0; i < resolvedMemoryObjects.size(); ++i) { - Assignment symcretization; - if (Query(state.constraints.cs(), resolveConditions.at(i)) - .containsSymcretes()) { - ref response; - solver->setTimeout(coreSolverTimeout); - bool success = solver->getResponse( - state.constraints.cs(), Expr::createIsZero(resolveConditions.at(i)), - response, state.queryMetaData); - solver->setTimeout(time::Span()); - assert(success); - assert(isa(response)); - symcretization = cast(response)->initialValuesFor( - state.constraints.cs().gatherSymcretizedArrays()); - } - resolveConcretizations.push_back(symcretization); + Assignment concretization = computeConcretization( + state.constraints.cs(), resolveConditions.at(i), state.queryMetaData); + resolveConcretizations.push_back(concretization); } + return true; } @@ -7006,6 +6984,24 @@ void Executor::setInitializationGraph(const ExecutionState &state, return; } +Assignment Executor::computeConcretization(const ConstraintSet &constraints, + ref condition, + SolverQueryMetaData &queryMetaData) { + Assignment concretization; + if (Query(constraints, condition).containsSymcretes()) { + ref response; + solver->setTimeout(coreSolverTimeout); + bool success = solver->getResponse( + constraints, Expr::createIsZero(condition), response, queryMetaData); + solver->setTimeout(time::Span()); + assert(success); + assert(isa(response)); + concretization = cast(response)->initialValuesFor( + constraints.gatherSymcretizedArrays()); + } + return concretization; +} + bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { solver->setTimeout(coreSolverTimeout); @@ -7031,22 +7027,11 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { // If the particular constraint operated on in this iteration through // the loop isn't implied then add it to the list of constraints. if (!mustBeTrue) { - Assignment symcretization; - if (Query(extendedConstraints.cs(), pi).containsSymcretes()) { - ref response; - solver->setTimeout(coreSolverTimeout); - bool success = solver->getResponse(extendedConstraints.cs(), - Expr::createIsZero(pi), response, - state.queryMetaData); - solver->setTimeout(time::Span()); - assert(success); - assert(isa(response)); - symcretization = cast(response)->initialValuesFor( - state.constraints.cs().gatherSymcretizedArrays()); - } + Assignment concretization = computeConcretization( + extendedConstraints.cs(), pi, state.queryMetaData); - if (!symcretization.isEmpty()) { - extendedConstraints.addConstraint(pi, symcretization); + if (!concretization.isEmpty()) { + extendedConstraints.addConstraint(pi, concretization); } else { extendedConstraints.addConstraint(pi, {}); } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 28f26f99cc..aab82e0072 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -449,6 +449,10 @@ class Executor : public Interpreter { // return it. Otherwise, return the unmodified condition. ref maxStaticPctChecks(ExecutionState ¤t, ref condition); + Assignment computeConcretization(const ConstraintSet &constraints, + ref condition, + SolverQueryMetaData &queryMetaData); + /// Add the given (boolean) condition as a constraint on state. This /// function is a wrapper around the state's addConstraint function /// which also manages propagation of implied values, From 400a06707fe8581bac003bf7a21e72e09d7d4cc9 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 25 Jul 2023 15:25:59 +0400 Subject: [PATCH 6/6] [feat] Classify `Target` into `ReachBlockTarget`, `ReproduceErrorTarget` and `CoverBranchTarget` [refactor] `TargetCalculator::calculate` --- include/klee/Module/CodeGraphDistance.h | 3 + include/klee/Module/KModule.h | 4 +- include/klee/Module/Target.h | 142 ++++++++++++++++++------ include/klee/Module/TargetHash.h | 7 +- lib/Core/DistanceCalculator.cpp | 72 ++++-------- lib/Core/DistanceCalculator.h | 33 +++--- lib/Core/ExecutionState.cpp | 10 +- lib/Core/ExecutionState.h | 6 +- lib/Core/Executor.cpp | 81 +++++++------- lib/Core/Executor.h | 3 +- lib/Core/Searcher.cpp | 2 +- lib/Core/Searcher.h | 4 +- lib/Core/TargetCalculator.cpp | 128 +++++++++++++-------- lib/Core/TargetCalculator.h | 24 +++- lib/Core/TargetManager.cpp | 104 ++++++++++++++++- lib/Core/TargetManager.h | 31 +++++- lib/Core/TargetedExecutionManager.cpp | 42 ++++--- lib/Core/TargetedExecutionManager.h | 8 +- lib/Module/CodeGraphDistance.cpp | 25 +++++ lib/Module/KModule.cpp | 7 +- lib/Module/Target.cpp | 122 +++++++++++++++----- lib/Module/TargetForest.cpp | 26 ++--- lib/Module/TargetHash.cpp | 4 + 23 files changed, 604 insertions(+), 284 deletions(-) diff --git a/include/klee/Module/CodeGraphDistance.h b/include/klee/Module/CodeGraphDistance.h index 014ed02e34..3192344ec4 100644 --- a/include/klee/Module/CodeGraphDistance.h +++ b/include/klee/Module/CodeGraphDistance.h @@ -65,6 +65,9 @@ class CodeGraphDistance { getSortedDistance(KFunction *kf); const std::vector> & getSortedBackwardDistance(KFunction *kf); + + void getNearestPredicateSatisfying(KBlock *from, KBlockPredicate predicate, + std::set &result); }; } // namespace klee diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index f7499f6c25..bfd30c019b 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -94,6 +94,8 @@ struct KBlock { std::string toString() const; }; +typedef std::function KBlockPredicate; + struct KCallBlock : KBlock { KInstruction *kcallInstruction; std::set calledFunctions; @@ -287,7 +289,7 @@ class KModule { KBlock *getKBlock(llvm::BasicBlock *bb); - bool inMainModule(llvm::Function *f); + bool inMainModule(const llvm::Function &f); bool inMainModule(const llvm::GlobalVariable &v); diff --git a/include/klee/Module/Target.h b/include/klee/Module/Target.h index f075cafe99..80bf7e0c1d 100644 --- a/include/klee/Module/Target.h +++ b/include/klee/Module/Target.h @@ -43,23 +43,10 @@ struct ErrorLocation { optional endColumn; }; -struct Target { -private: - KBlock *block; - std::vector - errors; // None - if it is not terminated in error trace - std::string id; // "" - if it is not terminated in error trace - optional loc; // TODO(): only for check in reportTruePositive - - explicit Target(const std::vector &_errors, - const std::string &_id, optional _loc, - KBlock *_block) - : block(_block), errors(_errors), id(_id), loc(_loc) { - std::sort(errors.begin(), errors.end()); - } - - static ref createCachedTarget(ref target); +class ReproduceErrorTarget; +class Target { +private: protected: friend class ref; friend class ref; @@ -87,6 +74,7 @@ struct Target { } }; + KBlock *block; static TargetCacheSet cachedTargets; bool isCached = false; bool toBeCleared = false; @@ -94,13 +82,24 @@ struct Target { /// @brief Required by klee::ref-managed objects mutable class ReferenceCounter _refCount; + explicit Target(KBlock *_block) : block(_block) {} + + static ref createCachedTarget(ref target); + public: - bool isReported = false; + static const unsigned MAGIC_HASH_CONSTANT = 39; - static ref create(const std::vector &_errors, - const std::string &_id, - optional _loc, KBlock *_block); - static ref create(KBlock *_block); + enum Kind { + CoverBranch = 3, + ReproduceError, + ReachBlock, + }; + + virtual ~Target(); + virtual Kind getKind() const = 0; + virtual int internalCompare(const Target &b) const = 0; + static bool classof(const Target *) { return true; } + virtual std::string toString() const = 0; int compare(const Target &other) const; @@ -110,8 +109,6 @@ struct Target { bool operator==(const Target &other) const; - bool atReturn() const { return isa(block); } - KBlock *getBlock() const { return block; } bool isNull() const { return block == nullptr; } @@ -120,26 +117,99 @@ struct Target { unsigned hash() const { return reinterpret_cast(block); } - const std::vector &getErrors() const { return errors; } - bool isThatError(ReachWithError err) const { - return std::find(errors.begin(), errors.end(), err) != errors.end(); - } bool shouldFailOnThisTarget() const { - return std::find(errors.begin(), errors.end(), ReachWithError::None) == - errors.end(); + return isa(this); } +}; - bool isTheSameAsIn(const KInstruction *instr) const; +class ReachBlockTarget : public Target { +protected: + bool atEnd; + + explicit ReachBlockTarget(KBlock *_block, bool _atEnd) + : Target(_block), atEnd(_atEnd) {} - /// returns true if we cannot use CFG reachability checks - /// from instr children to this target - /// to avoid solver calls - bool mustVisitForkBranches(KInstruction *instr) const; +public: + static ref create(KBlock *_block, bool _atEnd); + static ref create(KBlock *_block); + + Kind getKind() const override { return Kind::ReachBlock; } + + static bool classof(const Target *S) { + return S->getKind() == Kind::ReachBlock; + } + static bool classof(const ReachBlockTarget *) { return true; } + + bool isAtEnd() const { return atEnd; } + + virtual int internalCompare(const Target &other) const override; + virtual std::string toString() const override; +}; + +class CoverBranchTarget : public Target { +protected: + unsigned branchCase; + + explicit CoverBranchTarget(KBlock *_block, unsigned _branchCase) + : Target(_block), branchCase(_branchCase) {} + +public: + static ref create(KBlock *_block, unsigned _branchCase); + + Kind getKind() const override { return Kind::CoverBranch; } + + static bool classof(const Target *S) { + return S->getKind() == Kind::CoverBranch; + } + static bool classof(const CoverBranchTarget *) { return true; } + + virtual int internalCompare(const Target &other) const override; + virtual std::string toString() const override; + + unsigned getBranchCase() const { return branchCase; } +}; + +class ReproduceErrorTarget : public Target { +private: + std::vector + errors; // None - if it is not terminated in error trace + std::string id; // "" - if it is not terminated in error trace + ErrorLocation loc; // TODO(): only for check in reportTruePositive + +protected: + explicit ReproduceErrorTarget(const std::vector &_errors, + const std::string &_id, ErrorLocation _loc, + KBlock *_block) + : Target(_block), errors(_errors), id(_id), loc(_loc) { + assert(errors.size() > 0); + std::sort(errors.begin(), errors.end()); + } + +public: + static ref create(const std::vector &_errors, + const std::string &_id, ErrorLocation _loc, + KBlock *_block); + + Kind getKind() const override { return Kind::ReproduceError; } + + static bool classof(const Target *S) { + return S->getKind() == Kind::ReproduceError; + } + static bool classof(const ReproduceErrorTarget *) { return true; } + + virtual int internalCompare(const Target &other) const override; + virtual std::string toString() const override; std::string getId() const { return id; } - std::string toString() const; - ~Target(); + bool isReported = false; + + const std::vector &getErrors() const { return errors; } + bool isThatError(ReachWithError err) const { + return std::find(errors.begin(), errors.end(), err) != errors.end(); + } + + bool isTheSameAsIn(const KInstruction *instr) const; }; } // namespace klee diff --git a/include/klee/Module/TargetHash.h b/include/klee/Module/TargetHash.h index 2ceb35c747..2c2c2f81bd 100644 --- a/include/klee/Module/TargetHash.h +++ b/include/klee/Module/TargetHash.h @@ -21,7 +21,7 @@ class BasicBlock; } namespace klee { -struct Target; +class Target; struct TargetHash { unsigned operator()(const ref &t) const; @@ -32,11 +32,16 @@ struct TargetCmp { }; typedef std::pair Transition; +typedef std::pair Branch; struct TransitionHash { std::size_t operator()(const Transition &p) const; }; +struct BranchHash { + std::size_t operator()(const Branch &p) const; +}; + struct TargetLess { bool operator()(const ref &a, const ref &b) const { return a < b; diff --git a/lib/Core/DistanceCalculator.cpp b/lib/Core/DistanceCalculator.cpp index 774303a28b..15cf13be42 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -44,34 +44,30 @@ unsigned DistanceCalculator::SpeculativeState::computeHash() { unsigned res = (reinterpret_cast(kb) * SymbolicSource::MAGIC_HASH_CONSTANT) + kind; - res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + error; hashValue = res; return hashValue; } DistanceResult DistanceCalculator::getDistance(const ExecutionState &state, - ref target) { - return getDistance(state.prevPC, state.pc, state.stack.uniqueFrames(), - state.error, target); + KBlock *target) { + return getDistance(state.prevPC, state.pc, state.stack.callStack(), target); } DistanceResult DistanceCalculator::getDistance(KBlock *kb, TargetKind kind, - ReachWithError error, - ref target) { - SpeculativeState specState(kb, kind, error); + KBlock *target) { + SpeculativeState specState(kb, kind); if (distanceResultCache.count(target) == 0 || distanceResultCache.at(target).count(specState) == 0) { - auto result = computeDistance(kb, kind, error, target); + auto result = computeDistance(kb, kind, target); distanceResultCache[target][specState] = result; } return distanceResultCache.at(target).at(specState); } DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind, - ReachWithError error, - ref target) const { + KBlock *target) const { const auto &distanceToTargetFunction = - codeGraphDistance.getBackwardDistance(target->getBlock()->parent); + codeGraphDistance.getBackwardDistance(target->parent); weight_type weight = 0; WeightResult res = Miss; bool isInsideFunction = true; @@ -93,43 +89,21 @@ DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind, case NoneTarget: break; } - if (Done == res && target->shouldFailOnThisTarget()) { - if (!target->isThatError(error)) { - res = Continue; - } - } return DistanceResult(res, weight, isInsideFunction); } -DistanceResult -DistanceCalculator::getDistance(const KInstruction *prevPC, - const KInstruction *pc, - const ExecutionStack::call_stack_ty &frames, - ReachWithError error, ref target) { +DistanceResult DistanceCalculator::getDistance( + const KInstruction *prevPC, const KInstruction *pc, + const ExecutionStack::call_stack_ty &frames, KBlock *target) { weight_type weight = 0; - if (!target->shouldFailOnThisTarget() && target->atReturn()) { - if (prevPC->parent == target->getBlock() && - prevPC == target->getBlock()->getLastInstruction()) { - return DistanceResult(Done); - } else if (pc->parent == target->getBlock()) { - return DistanceResult(Continue); - } - } - - if (target->shouldFailOnThisTarget() && target->isTheSameAsIn(prevPC) && - target->isThatError(error)) { - return DistanceResult(Done); - } - KBlock *kb = pc->parent; const auto &distanceToTargetFunction = - codeGraphDistance.getBackwardDistance(target->getBlock()->parent); + codeGraphDistance.getBackwardDistance(target->parent); unsigned int minCallWeight = UINT_MAX, minSfNum = UINT_MAX, sfNum = 0; auto sfi = frames.rbegin(), sfe = frames.rend(); bool strictlyAfterKB = - sfi != sfe && (!target->shouldFailOnThisTarget() || - sfi->kf->parent->inMainModule(sfi->kf->function)); + sfi != sfe && sfi->kf->parent->inMainModule(*sfi->kf->function); for (; sfi != sfe; sfi++) { unsigned callWeight; if (distanceInCallGraph(sfi->kf, kb, callWeight, distanceToTargetFunction, @@ -161,18 +135,18 @@ DistanceCalculator::getDistance(const KInstruction *prevPC, kind = PostTarget; } - return getDistance(pc->parent, kind, error, target); + return getDistance(pc->parent, kind, target); } bool DistanceCalculator::distanceInCallGraph( KFunction *kf, KBlock *origKB, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target, bool strictlyAfterKB) const { + KBlock *target, bool strictlyAfterKB) const { distance = UINT_MAX; const std::unordered_map &dist = codeGraphDistance.getDistance(origKB); - KBlock *targetBB = target->getBlock(); + KBlock *targetBB = target; KFunction *targetF = targetBB->parent; if (kf == targetF && dist.count(targetBB) != 0) { @@ -199,7 +173,7 @@ bool DistanceCalculator::distanceInCallGraph( KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target) const { + KBlock *target) const { distance = UINT_MAX; const std::unordered_map &dist = codeGraphDistance.getDistance(kb); @@ -221,7 +195,7 @@ bool DistanceCalculator::distanceInCallGraph( WeightResult DistanceCalculator::tryGetLocalWeight(KBlock *kb, weight_type &weight, const std::vector &localTargets, - ref target) const { + KBlock *target) const { KFunction *currentKF = kb->parent; KBlock *currentKB = kb; const std::unordered_map &dist = @@ -247,7 +221,7 @@ WeightResult DistanceCalculator::tryGetPreTargetWeight( KBlock *kb, weight_type &weight, const std::unordered_map &distanceToTargetFunction, - ref target) const { + KBlock *target) const { KFunction *currentKF = kb->parent; std::vector localTargets; for (auto &kCallBlock : currentKF->kCallBlocks) { @@ -267,9 +241,9 @@ WeightResult DistanceCalculator::tryGetPreTargetWeight( return res == Done ? Continue : res; } -WeightResult -DistanceCalculator::tryGetPostTargetWeight(KBlock *kb, weight_type &weight, - ref target) const { +WeightResult DistanceCalculator::tryGetPostTargetWeight(KBlock *kb, + weight_type &weight, + KBlock *target) const { KFunction *currentKF = kb->parent; std::vector &localTargets = currentKF->returnKBlocks; @@ -282,8 +256,8 @@ DistanceCalculator::tryGetPostTargetWeight(KBlock *kb, weight_type &weight, WeightResult DistanceCalculator::tryGetTargetWeight(KBlock *kb, weight_type &weight, - ref target) const { - std::vector localTargets = {target->getBlock()}; + KBlock *target) const { + std::vector localTargets = {target}; WeightResult res = tryGetLocalWeight(kb, weight, localTargets, target); return res; } diff --git a/lib/Core/DistanceCalculator.h b/lib/Core/DistanceCalculator.h index 3f24018586..f0fdd15655 100644 --- a/lib/Core/DistanceCalculator.h +++ b/lib/Core/DistanceCalculator.h @@ -18,7 +18,7 @@ class BasicBlock; namespace klee { class CodeGraphDistance; -struct Target; +class Target; enum WeightResult : std::uint8_t { Done = 0U, @@ -48,11 +48,11 @@ class DistanceCalculator { explicit DistanceCalculator(CodeGraphDistance &codeGraphDistance_) : codeGraphDistance(codeGraphDistance_) {} - DistanceResult getDistance(const ExecutionState &es, ref target); + DistanceResult getDistance(const ExecutionState &es, KBlock *target); DistanceResult getDistance(const KInstruction *prevPC, const KInstruction *pc, const ExecutionStack::call_stack_ty &frames, - ReachWithError error, ref target); + KBlock *target); private: enum TargetKind : std::uint8_t { @@ -71,9 +71,7 @@ class DistanceCalculator { public: KBlock *kb; TargetKind kind; - ReachWithError error; - SpeculativeState(KBlock *kb_, TargetKind kind_, ReachWithError error_) - : kb(kb_), kind(kind_), error(error_) { + SpeculativeState(KBlock *kb_, TargetKind kind_) : kb(kb_), kind(kind_) { computeHash(); } ~SpeculativeState() = default; @@ -87,7 +85,7 @@ class DistanceCalculator { struct SpeculativeStateCompare { bool operator()(const SpeculativeState &a, const SpeculativeState &b) const { - return a.kb == b.kb && a.error == b.error && a.kind == b.kind; + return a.kb == b.kb && a.kind == b.kind; } }; @@ -95,8 +93,7 @@ class DistanceCalculator { std::unordered_map; using TargetToSpeculativeStateToDistanceResultMap = - std::unordered_map, SpeculativeStateToDistanceResultMap, - TargetHash, TargetCmp>; + std::unordered_map; using StatesSet = std::unordered_set; @@ -104,34 +101,32 @@ class DistanceCalculator { TargetToSpeculativeStateToDistanceResultMap distanceResultCache; StatesSet localStates; - DistanceResult getDistance(KBlock *kb, TargetKind kind, ReachWithError error, - ref target); + DistanceResult getDistance(KBlock *kb, TargetKind kind, KBlock *target); DistanceResult computeDistance(KBlock *kb, TargetKind kind, - ReachWithError error, - ref target) const; + KBlock *target) const; bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target) const; + KBlock *target) const; bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target, bool strictlyAfterKB) const; + KBlock *target, bool strictlyAfterKB) const; WeightResult tryGetLocalWeight(KBlock *kb, weight_type &weight, const std::vector &localTargets, - ref target) const; + KBlock *target) const; WeightResult tryGetPreTargetWeight(KBlock *kb, weight_type &weight, const std::unordered_map &distanceToTargetFunction, - ref target) const; + KBlock *target) const; WeightResult tryGetTargetWeight(KBlock *kb, weight_type &weight, - ref target) const; + KBlock *target) const; WeightResult tryGetPostTargetWeight(KBlock *kb, weight_type &weight, - ref target) const; + KBlock *target) const; }; } // namespace klee diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 17a55162e7..90a2c9ac45 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -465,7 +465,7 @@ void ExecutionState::increaseLevel() { KFunction *kf = prevPC->parent->parent; KModule *kmodule = kf->parent; - if (prevPC->inst->isTerminator() && kmodule->inMainModule(kf->function)) { + if (prevPC->inst->isTerminator() && kmodule->inMainModule(*kf->function)) { ++multilevel[srcbb]; level.insert(srcbb); } @@ -482,13 +482,13 @@ bool ExecutionState::visited(KBlock *block) const { return level.count(block->basicBlock) != 0; } -bool ExecutionState::reachedTarget(Target target) const { +bool ExecutionState::reachedTarget(ref target) const { if (constraints.path().KBlockSize() == 0) { return false; } - if (target.atReturn()) { - return prevPC == target.getBlock()->getLastInstruction(); + if (target->isAtEnd()) { + return prevPC == target->getBlock()->getLastInstruction(); } else { - return pc == target.getBlock()->getFirstInstruction(); + return pc == target->getBlock()->getFirstInstruction(); } } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 1a2751a054..e0d432239b 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -52,7 +52,7 @@ struct KInstruction; class MemoryObject; class PTreeNode; struct InstructionInfo; -struct Target; +class Target; struct TranstionHash; llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); @@ -444,7 +444,7 @@ class ExecutionState { llvm::BasicBlock *getPCBlock() const; void increaseLevel(); - inline bool isTransfered() { return getPrevPCBlock() != getPCBlock(); } + inline bool isTransfered() const { return getPrevPCBlock() != getPCBlock(); } bool isGEPExpr(ref expr) const; @@ -478,7 +478,7 @@ class ExecutionState { areTargetsChanged_ = true; } - bool reachedTarget(Target target) const; + bool reachedTarget(ref target) const; static std::uint32_t getLastID() { return nextID - 1; }; inline bool isStuck(unsigned long long bound) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 8488d3a884..cde0b6d77d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -455,16 +455,16 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0), pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)}, - codeGraphDistance(new CodeGraphDistance()), + guidanceKind(opts.Guidance), codeGraphDistance(new CodeGraphDistance()), distanceCalculator(new DistanceCalculator(*codeGraphDistance)), - targetedExecutionManager(new TargetedExecutionManager( - *codeGraphDistance, *distanceCalculator)), + targetCalculator(new TargetCalculator(*codeGraphDistance)), + targetManager(new TargetManager(guidanceKind, *distanceCalculator, + *targetCalculator)), + targetedExecutionManager( + new TargetedExecutionManager(*codeGraphDistance, *targetManager)), replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), debugLogBuffer(debugBufferString) { - - guidanceKind = opts.Guidance; - const time::Span maxTime{MaxTime}; if (maxTime) timers.add(std::make_unique(maxTime, [&] { @@ -577,12 +577,12 @@ Executor::setModule(std::vector> &userModules, kmodule->checkModule(); // 4.) Manifest the module - kmodule->manifest(interpreterHandler, interpreterOpts.Guidance, - StatsTracker::useStatistics()); kmodule->mainModuleFunctions.insert(mainModuleFunctions.begin(), mainModuleFunctions.end()); kmodule->mainModuleGlobals.insert(mainModuleGlobals.begin(), mainModuleGlobals.end()); + kmodule->manifest(interpreterHandler, interpreterOpts.Guidance, + StatsTracker::useStatistics()); if (origInfos) { kmodule->origInfos = origInfos->getInstructions(); @@ -603,15 +603,6 @@ Executor::setModule(std::vector> &userModules, Context::initialize(TD->isLittleEndian(), (Expr::Width)TD->getPointerSizeInBits()); - targetCalculator = std::unique_ptr( - new TargetCalculator(*kmodule.get(), *codeGraphDistance.get())); - - targetManager = std::unique_ptr(new TargetManager( - guidanceKind, *distanceCalculator.get(), *targetCalculator.get())); - - targetedExecutionManager = std::unique_ptr( - new TargetedExecutionManager(*codeGraphDistance, *distanceCalculator)); - return kmodule->module.get(); } @@ -1092,16 +1083,32 @@ ref Executor::maxStaticPctChecks(ExecutionState ¤t, return condition; } +/// returns true if we cannot use CFG reachability checks +/// from instr children to this target +/// to avoid solver calls +bool mustVisitForkBranches(ref target, KInstruction *instr) { + // null check after deref error is checked after fork + // but reachability of this target from instr children + // will always give false, so we need to force visiting + // fork branches here + if (auto reprErrorTarget = dyn_cast(target)) { + return reprErrorTarget->isTheSameAsIn(instr) && + reprErrorTarget->isThatError( + ReachWithError::NullCheckAfterDerefException); + } + return false; +} + bool Executor::canReachSomeTargetFromBlock(ExecutionState &es, KBlock *block) { if (interpreterOpts.Guidance != GuidanceKind::ErrorGuidance) return true; auto nextInstr = block->getFirstInstruction(); for (const auto &p : *es.targetForest.getTopLayer()) { auto target = p.first; - if (target->mustVisitForkBranches(es.prevPC)) + if (mustVisitForkBranches(target, es.prevPC)) return true; auto dist = distanceCalculator->getDistance( - es.prevPC, nextInstr, es.stack.callStack(), es.error, target); + es.prevPC, nextInstr, es.stack.callStack(), target->getBlock()); if (dist.result != WeightResult::Miss) return true; } @@ -2395,8 +2402,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { if (guidanceKind == GuidanceKind::ErrorGuidance) { for (auto kvp : state.targetForest) { auto target = kvp.first; - if (target->isThatError(ReachWithError::Reachable) && - target->isTheSameAsIn(ki)) { + if (target->shouldFailOnThisTarget() && + cast(target)->isThatError( + ReachWithError::Reachable) && + cast(target)->isTheSameAsIn(ki)) { terminateStateOnTargetError(state, ReachWithError::Reachable); return; } @@ -4185,7 +4194,7 @@ void Executor::reportProgressTowardsTargets(std::string prefix, for (auto &state : states) { for (auto &p : *state->targetForest.getTopLayer()) { auto target = p.first; - auto distance = distanceCalculator->getDistance(*state, target); + auto distance = targetManager->distance(*state, target); auto it = distancesTowardsTargets.find(target); if (it == distancesTowardsTargets.end()) distancesTowardsTargets.insert(it, std::make_pair(target, distance)); @@ -4201,9 +4210,11 @@ void Executor::reportProgressTowardsTargets(std::string prefix, auto target = p.first; auto distance = p.second; std::ostringstream repr; - repr << "Target " << target->getId() << ": "; + repr << "Target "; if (target->shouldFailOnThisTarget()) { - repr << "error "; + repr << cast(target)->getId() << ": error "; + } else { + repr << ": "; } repr << "in function " + target->getBlock()->parent->function->getName().str(); @@ -4252,15 +4263,9 @@ void Executor::run(std::vector initialStates) { KInstruction *prevKI = state.prevPC; KFunction *kf = prevKI->parent->parent; - if (prevKI->inst->isTerminator() && kmodule->inMainModule(kf->function)) { + if (prevKI->inst->isTerminator() && + kmodule->inMainModule(*kf->function)) { targetCalculator->update(state); - auto target = Target::create(state.prevPC->parent); - if (guidanceKind == GuidanceKind::CoverageGuidance) { - if (!target->atReturn() || - state.prevPC == target->getBlock()->getLastInstruction()) { - targetManager->setReached(target); - } - } } executeStep(state); @@ -4283,11 +4288,12 @@ void Executor::run(std::vector initialStates) { haltExecution = HaltExecution::NoMoreStates; } + doDumpStates(); + delete searcher; searcher = nullptr; targetManager = nullptr; - doDumpStates(); haltExecution = HaltExecution::NotHalt; } @@ -4358,8 +4364,8 @@ void Executor::targetedRun(ExecutionState &initialState, KBlock *target, states.insert(&initialState); - TargetedSearcher *targetedSearcher = - new TargetedSearcher(Target::create(target), *distanceCalculator); + TargetedSearcher *targetedSearcher = new TargetedSearcher( + ReachBlockTarget::create(target), *distanceCalculator); searcher = targetedSearcher; std::vector newStates(states.begin(), states.end()); @@ -4494,9 +4500,9 @@ void Executor::terminateState(ExecutionState &state, } interpreterHandler->incPathsExplored(); + state.pc = state.prevPC; targetCalculator->update(state); - state.pc = state.prevPC; removedStates.push_back(&state); } @@ -4704,7 +4710,6 @@ void Executor::terminateStateOnError(ExecutionState &state, true); } - targetCalculator->update(state); terminateState(state, terminationType); if (shouldExitOn(terminationType)) @@ -6686,7 +6691,7 @@ ExecutionState *Executor::prepareStateForPOSIX(KInstIterator &caller, ExecutionState *original = state->copy(); ExecutionState *initialState = nullptr; ref targets(new TargetForest()); - targets->add(Target::create(target)); + targets->add(ReachBlockTarget::create(target)); prepareTargetedExecution(*state, targets); targetedRun(*state, target, &initialState); state = initialState; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index aab82e0072..d66ff5986f 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -145,6 +145,7 @@ class Executor : public Interpreter { SpecialFunctionHandler *specialFunctionHandler; TimerGroup timers; std::unique_ptr processForest; + GuidanceKind guidanceKind; std::unique_ptr codeGraphDistance; std::unique_ptr distanceCalculator; std::unique_ptr targetCalculator; @@ -241,8 +242,6 @@ class Executor : public Interpreter { /// Typeids used during exception handling std::vector> eh_typeids; - GuidanceKind guidanceKind; - bool hasStateWhichCanReachSomeTarget = false; /// Return the typeid corresponding to a certain `type_info` diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 1be798e88c..5522316555 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -195,7 +195,7 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) { states->tryGetWeight(es, weight)) { return weight; } - auto distRes = distanceCalculator.getDistance(*es, target); + auto distRes = distanceCalculator.getDistance(*es, target->getBlock()); weight = ulog2(distRes.weight + es->steppedMemoryInstructions + 1); // [0, 32) if (!distRes.isInsideFunction) { weight += 32; // [32, 64) diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 5fe557ca6f..0a6c734f73 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -172,7 +172,9 @@ class GuidedSearcher final : public Searcher, public TargetManagerSubscriber { std::unordered_map; using TargetForestHisoryTargetVector = std::vector; - using TargetForestHistoryTargetSet = std::set; + using TargetForestHistoryTargetSet = + std::unordered_set; std::unique_ptr baseSearcher; TargetHistoryTargetPairToSearcherMap targetedSearchers; diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index c56417d5a2..c2340e4af2 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -38,21 +38,40 @@ llvm::cl::opt TargetCalculatorMode( } // namespace klee void TargetCalculator::update(const ExecutionState &state) { + Function *initialFunction = state.getInitPCBlock()->getParent(); switch (TargetCalculatorMode) { case TargetCalculateBy::Default: - blocksHistory[state.getInitPCBlock()][state.getPrevPCBlock()].insert( + blocksHistory[initialFunction][state.getPrevPCBlock()].insert( state.getInitPCBlock()); + if (state.prevPC == state.prevPC->parent->getLastInstruction()) { + coveredBlocks[state.getPrevPCBlock()->getParent()].insert( + state.getPrevPCBlock()); + } + if (state.prevPC == state.prevPC->parent->getLastInstruction()) { + unsigned index = 0; + coveredBranches[state.getPrevPCBlock()->getParent()] + [state.getPrevPCBlock()]; + for (auto succ : successors(state.getPrevPCBlock())) { + if (succ == state.getPCBlock()) { + coveredBranches[state.getPrevPCBlock()->getParent()] + [state.getPrevPCBlock()] + .insert(index); + break; + } + ++index; + } + } break; case TargetCalculateBy::Blocks: - blocksHistory[state.getInitPCBlock()][state.getPrevPCBlock()].insert( + blocksHistory[initialFunction][state.getPrevPCBlock()].insert( state.level.begin(), state.level.end()); break; case TargetCalculateBy::Transitions: - blocksHistory[state.getInitPCBlock()][state.getPrevPCBlock()].insert( + blocksHistory[initialFunction][state.getPrevPCBlock()].insert( state.level.begin(), state.level.end()); - transitionsHistory[state.getInitPCBlock()][state.getPrevPCBlock()].insert( + transitionsHistory[initialFunction][state.getPrevPCBlock()].insert( state.transitionLevel.begin(), state.transitionLevel.end()); break; } @@ -85,58 +104,77 @@ bool TargetCalculator::differenceIsEmpty( return diff.empty(); } -ref TargetCalculator::calculate(ExecutionState &state) { - BasicBlock *initialBlock = state.getInitPCBlock(); +bool TargetCalculator::uncoveredBlockPredicate(ExecutionState *state, + KBlock *kblock) { + Function *initialFunction = state->getInitPCBlock()->getParent(); std::unordered_map &history = - blocksHistory[initialBlock]; + blocksHistory[initialFunction]; std::unordered_map - &transitionHistory = transitionsHistory[initialBlock]; + &transitionHistory = transitionsHistory[initialFunction]; + bool result = false; + switch (TargetCalculatorMode) { + case TargetCalculateBy::Default: { + if (coveredBranches[kblock->parent->function].count(kblock->basicBlock) == + 0) { + result = true; + } else { + auto &cb = coveredBranches[kblock->parent->function][kblock->basicBlock]; + result = + kblock->basicBlock->getTerminator()->getNumSuccessors() > cb.size(); + } + break; + } + case TargetCalculateBy::Blocks: { + if (history[kblock->basicBlock].size() != 0) { + result = !differenceIsEmpty(*state, history, kblock); + } + break; + } + case TargetCalculateBy::Transitions: { + if (history[kblock->basicBlock].size() != 0) { + result = !differenceIsEmpty(*state, transitionHistory, kblock); + } + break; + } + } + + return result; +} + +TargetHashSet TargetCalculator::calculate(ExecutionState &state) { BasicBlock *bb = state.getPCBlock(); + const KModule &module = *state.pc->parent->parent->parent; KFunction *kf = module.functionMap.at(bb->getParent()); KBlock *kb = kf->blockMap[bb]; - ref nearestBlock; - unsigned int minDistance = UINT_MAX; - unsigned int sfNum = 0; - bool newCov = false; for (auto sfi = state.stack.callStack().rbegin(), sfe = state.stack.callStack().rend(); - sfi != sfe; sfi++, sfNum++) { + sfi != sfe; sfi++) { kf = sfi->kf; - for (const auto &kbd : codeGraphDistance.getSortedDistance(kb)) { - KBlock *target = kbd.first; - unsigned distance = kbd.second; - if ((sfNum > 0 || distance > 0)) { - if (distance >= minDistance) - break; - if (history[target->basicBlock].size() != 0) { - bool diffIsEmpty = true; - if (!newCov) { - switch (TargetCalculatorMode) { - case TargetCalculateBy::Blocks: - diffIsEmpty = differenceIsEmpty(state, history, target); - break; - case TargetCalculateBy::Transitions: - diffIsEmpty = differenceIsEmpty(state, transitionHistory, target); - break; - case TargetCalculateBy::Default: - break; - } - } - - if (diffIsEmpty) { - continue; - } + std::set blocks; + using std::placeholders::_1; + KBlockPredicate func = + std::bind(&TargetCalculator::uncoveredBlockPredicate, this, &state, _1); + codeGraphDistance.getNearestPredicateSatisfying(kb, func, blocks); + + if (!blocks.empty()) { + TargetHashSet targets; + for (auto block : blocks) { + if (coveredBranches[block->parent->function].count(block->basicBlock) == + 0) { + targets.insert(ReachBlockTarget::create(block, true)); } else { - newCov = true; + auto &cb = + coveredBranches[block->parent->function][block->basicBlock]; + for (unsigned index = 0; + index < block->basicBlock->getTerminator()->getNumSuccessors(); + ++index) { + if (!cb.count(index)) + targets.insert(CoverBranchTarget::create(block, index)); + } } - nearestBlock = Target::create(target); - minDistance = distance; } - } - - if (nearestBlock) { - return nearestBlock; + return targets; } if (sfi->caller) { @@ -144,5 +182,5 @@ ref TargetCalculator::calculate(ExecutionState &state) { } } - return nearestBlock; + return {}; } diff --git a/lib/Core/TargetCalculator.h b/lib/Core/TargetCalculator.h index 3b99fb1913..7369519afd 100644 --- a/lib/Core/TargetCalculator.h +++ b/lib/Core/TargetCalculator.h @@ -39,34 +39,44 @@ struct TransitionHash; enum TargetCalculateBy { Default, Blocks, Transitions }; typedef std::pair Transition; +typedef std::pair Branch; class TargetCalculator { typedef std::unordered_set VisitedBlocks; typedef std::unordered_set VisitedTransitions; + typedef std::unordered_set VisitedBranches; enum HistoryKind { Blocks, Transitions }; typedef std::unordered_map< - llvm::BasicBlock *, std::unordered_map> + llvm::Function *, std::unordered_map> BlocksHistory; typedef std::unordered_map< - llvm::BasicBlock *, + llvm::Function *, std::unordered_map> TransitionsHistory; + typedef std::unordered_map< + llvm::Function *, + std::unordered_map>> + CoveredBranches; + + typedef std::unordered_map CoveredBlocks; + public: - TargetCalculator(const KModule &module, CodeGraphDistance &codeGraphDistance) - : module(module), codeGraphDistance(codeGraphDistance) {} + TargetCalculator(CodeGraphDistance &codeGraphDistance) + : codeGraphDistance(codeGraphDistance) {} void update(const ExecutionState &state); - ref calculate(ExecutionState &state); + TargetHashSet calculate(ExecutionState &state); private: - const KModule &module; CodeGraphDistance &codeGraphDistance; BlocksHistory blocksHistory; TransitionsHistory transitionsHistory; + CoveredBranches coveredBranches; + CoveredBlocks coveredBlocks; bool differenceIsEmpty( const ExecutionState &state, @@ -76,6 +86,8 @@ class TargetCalculator { const ExecutionState &state, const std::unordered_map &history, KBlock *target); + + bool uncoveredBlockPredicate(ExecutionState *state, KBlock *kblock); }; } // namespace klee diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index 840f347147..bfb3be2931 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -25,7 +25,9 @@ void TargetManager::updateMiss(ExecutionState &state, ref target) { stateTargetForest.remove(target); setTargets(state, stateTargetForest.getTargets()); if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { - state.setTargeted(false); + if (targets(state).size() == 0) { + state.setTargeted(false); + } } } @@ -54,12 +56,16 @@ void TargetManager::updateDone(ExecutionState &state, ref target) { } } if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { - state.setTargeted(false); + if (targets(state).size() == 0) { + state.setTargeted(false); + } } } void TargetManager::collect(ExecutionState &state) { if (!state.areTargetsChanged()) { + assert(state.targets() == state.prevTargets()); + assert(state.history() == state.prevHistory()); return; } @@ -96,15 +102,44 @@ void TargetManager::collect(ExecutionState &state) { } } +void TargetManager::updateReached(ExecutionState &state) { + auto prevKI = state.prevPC; + auto kf = prevKI->parent->parent; + auto kmodule = kf->parent; + + if (prevKI->inst->isTerminator() && kmodule->inMainModule(*kf->function)) { + ref target; + + if (state.getPrevPCBlock()->getTerminator()->getNumSuccessors() == 0) { + target = ReachBlockTarget::create(state.prevPC->parent, true); + } else { + unsigned index = 0; + for (auto succ : successors(state.getPrevPCBlock())) { + if (succ == state.getPCBlock()) { + target = CoverBranchTarget::create(state.prevPC->parent, index); + break; + } + ++index; + } + } + + if (target && guidance == Interpreter::GuidanceKind::CoverageGuidance) { + setReached(target); + } + } +} + void TargetManager::updateTargets(ExecutionState &state) { if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { state.setTargeted(true); } if (isTargeted(state) && targets(state).empty()) { - ref target(targetCalculator.calculate(state)); - if (target) { - state.targetForest.add(target); + TargetHashSet targets(targetCalculator.calculate(state)); + if (!targets.empty()) { + for (auto target : targets) { + state.targetForest.add(target); + } setTargets(state, state.targetForest.getTargets()); } } @@ -157,6 +192,7 @@ void TargetManager::update(ExecutionState *current, } for (auto state : localStates) { + updateReached(*state); updateTargets(*state); if (state->areTargetsChanged()) { changedStates.insert(state); @@ -173,6 +209,7 @@ void TargetManager::update(ExecutionState *current, for (const auto state : removedStates) { states.erase(state); + distances.erase(state); } for (auto subscriber : subscribers) { @@ -189,3 +226,60 @@ void TargetManager::update(ExecutionState *current, changedStates.clear(); localStates.clear(); } + +bool TargetManager::isReachedTarget(const ExecutionState &state, + ref target) { + WeightResult result; + if (isReachedTarget(state, target, result)) { + return result == Done; + } + return false; +} + +bool TargetManager::isReachedTarget(const ExecutionState &state, + ref target, WeightResult &result) { + if (state.constraints.path().KBlockSize() == 0) { + return false; + } + + if (isa(target)) { + if (cast(target)->isAtEnd()) { + if (state.prevPC->parent == target->getBlock() || + state.pc->parent == target->getBlock()) { + if (state.prevPC == target->getBlock()->getLastInstruction()) { + result = Done; + } else { + result = Continue; + } + return true; + } + } + } + + if (isa(target)) { + if (state.prevPC->parent == target->getBlock()) { + if (state.prevPC == target->getBlock()->getLastInstruction() && + state.prevPC->inst->getSuccessor( + cast(target)->getBranchCase()) == + state.pc->parent->basicBlock) { + result = Done; + } else { + result = Continue; + } + return true; + } + } + + if (target->shouldFailOnThisTarget()) { + if (state.pc->parent == target->getBlock()) { + if (cast(target)->isTheSameAsIn(state.prevPC) && + cast(target)->isThatError(state.error)) { + result = Done; + } else { + result = Continue; + } + return true; + } + } + return false; +} diff --git a/lib/Core/TargetManager.h b/lib/Core/TargetManager.h index 3d81049443..11cba8bfc9 100644 --- a/lib/Core/TargetManager.h +++ b/lib/Core/TargetManager.h @@ -45,19 +45,24 @@ class TargetManagerSubscriber { class TargetManager { private: using StatesSet = std::unordered_set; + using StateToDistanceMap = + std::unordered_map>; using TargetHistoryTargetPair = std::pair, ref>; using StatesVector = std::vector; using TargetHistoryTargetPairToStatesMap = std::unordered_map; - using TargetForestHistoryTargetSet = std::set; + using TargetForestHistoryTargetSet = + std::unordered_set; Interpreter::GuidanceKind guidance; DistanceCalculator &distanceCalculator; TargetCalculator &targetCalculator; TargetHashSet reachedTargets; StatesSet states; + StateToDistanceMap distances; StatesSet localStates; StatesSet changedStates; std::vector subscribers; @@ -82,9 +87,15 @@ class TargetManager { void updateDone(ExecutionState &state, ref target); + void updateReached(ExecutionState &state); + void updateTargets(ExecutionState &state); + void collect(ExecutionState &state); + bool isReachedTarget(const ExecutionState &state, ref target, + WeightResult &result); + public: TargetManager(Interpreter::GuidanceKind _guidance, DistanceCalculator &_distanceCalculator, @@ -97,7 +108,21 @@ class TargetManager { const std::vector &removedStates); DistanceResult distance(const ExecutionState &state, ref target) { - return distanceCalculator.getDistance(state, target); + + WeightResult wresult; + if (isReachedTarget(state, target, wresult)) { + return DistanceResult(wresult); + } + + if (!state.isTransfered() && distances[&state].count(target)) { + return distances[&state][target]; + } + + DistanceResult result = + distanceCalculator.getDistance(state, target->getBlock()); + distances[&state][target] = result; + + return result; } const TargetHashSet &targets(const ExecutionState &state) { @@ -126,6 +151,8 @@ class TargetManager { bool isTargeted(const ExecutionState &state) { return state.isTargeted(); } + bool isReachedTarget(const ExecutionState &state, ref target); + void setReached(ref target) { reachedTargets.insert(target); } }; diff --git a/lib/Core/TargetedExecutionManager.cpp b/lib/Core/TargetedExecutionManager.cpp index 20cb63683f..25357773ae 100644 --- a/lib/Core/TargetedExecutionManager.cpp +++ b/lib/Core/TargetedExecutionManager.cpp @@ -281,12 +281,11 @@ void TargetedHaltsOnTraces::reportFalsePositives(bool canReachSomeTarget) { confidence::ty confidence; HaltExecution::Reason reason; for (const auto &targetSetWithConfidences : traceToHaltTypeToConfidence) { - const auto &target = targetSetWithConfidences.first->getTargets().front(); - if (!target->shouldFailOnThisTarget()) - continue; bool atLeastOneReported = false; for (const auto &target : targetSetWithConfidences.first->getTargets()) { - if (target->isReported) { + if (!target->shouldFailOnThisTarget()) + continue; + if (cast(target)->isReported) { atLeastOneReported = true; break; } @@ -295,6 +294,9 @@ void TargetedHaltsOnTraces::reportFalsePositives(bool canReachSomeTarget) { if (atLeastOneReported) { continue; } + const auto &target = targetSetWithConfidences.first->getTargets().front(); + assert(target->shouldFailOnThisTarget()); + auto errorTarget = cast(target); totalConfidenceAndTopContributor(targetSetWithConfidences.second, &confidence, &reason); @@ -305,9 +307,10 @@ void TargetedHaltsOnTraces::reportFalsePositives(bool canReachSomeTarget) { confidence = confidence::VeryConfident; reason = HaltExecution::MaxTime; } - reportFalsePositive(confidence, target->getErrors(), target->getId(), + reportFalsePositive(confidence, errorTarget->getErrors(), + errorTarget->getId(), getAdviseWhatToIncreaseConfidenceRate(reason)); - target->isReported = true; + errorTarget->isReported = true; } } @@ -528,8 +531,12 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, ReachWithError error) { bool atLeastOneReported = false; for (auto target : state.targetForest.getTargets()) { - if (!target->isThatError(error) || brokenTraces.count(target->getId()) || - reportedTraces.count(target->getId())) + if (!target->shouldFailOnThisTarget()) + continue; + auto errorTarget = cast(target); + if (!errorTarget->isThatError(error) || + brokenTraces.count(errorTarget->getId()) || + reportedTraces.count(errorTarget->getId())) continue; /// The following code checks if target is a `call ...` instruction and we @@ -538,7 +545,7 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, int i = state.stack.size() - 1; bool found = true; - while (!target->isTheSameAsIn( + while (!errorTarget->isTheSameAsIn( possibleInstruction)) { // TODO: target->getBlock() == // possibleInstruction should also be checked, // but more smartly @@ -554,16 +561,16 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, state.error = error; atLeastOneReported = true; - assert(!target->isReported); - if (target->isThatError(ReachWithError::Reachable)) { + assert(!errorTarget->isReported); + if (errorTarget->isThatError(ReachWithError::Reachable)) { klee_warning("100.00%% %s Reachable at trace %s", getErrorString(error), - target->getId().c_str()); + errorTarget->getId().c_str()); } else { klee_warning("100.00%% %s True Positive at trace %s", - getErrorString(error), target->getId().c_str()); + getErrorString(error), errorTarget->getId().c_str()); } - target->isReported = true; - reportedTraces.insert(target->getId()); + errorTarget->isReported = true; + reportedTraces.insert(errorTarget->getId()); } return atLeastOneReported; } @@ -588,8 +595,7 @@ void TargetedExecutionManager::update( auto &stateTargets = state->targets(); for (auto target : stateTargets) { - DistanceResult stateDistance = - distanceCalculator.getDistance(*state, target); + DistanceResult stateDistance = targetManager.distance(*state, target); switch (stateDistance.result) { case WeightResult::Miss: break; @@ -608,4 +614,4 @@ void TargetedExecutionManager::update( } localStates.clear(); -} \ No newline at end of file +} diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 6171d80d69..7d5b285d41 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -22,7 +22,6 @@ #include namespace klee { -class DistanceCalculator; class TargetManager; extern llvm::cl::OptionCategory TerminationCat; @@ -118,7 +117,7 @@ class TargetedExecutionManager { LocationToBlocks &locToBlocks) const; CodeGraphDistance &codeGraphDistance; - DistanceCalculator &distanceCalculator; + TargetManager &targetManager; StatesSet localStates; public: @@ -129,9 +128,8 @@ class TargetedExecutionManager { }; explicit TargetedExecutionManager(CodeGraphDistance &codeGraphDistance_, - DistanceCalculator &distanceCalculator_) - : codeGraphDistance(codeGraphDistance_), - distanceCalculator(distanceCalculator_) {} + TargetManager &targetManager_) + : codeGraphDistance(codeGraphDistance_), targetManager(targetManager_) {} ~TargetedExecutionManager() = default; std::map, KFunctionLess> prepareTargets(KModule *kmodule, SarifReport paths); diff --git a/lib/Module/CodeGraphDistance.cpp b/lib/Module/CodeGraphDistance.cpp index 5bcae51d26..54839c6cd3 100644 --- a/lib/Module/CodeGraphDistance.cpp +++ b/lib/Module/CodeGraphDistance.cpp @@ -175,3 +175,28 @@ CodeGraphDistance::getSortedBackwardDistance(KFunction *kf) { calculateBackwardDistance(kf); return functionSortedBackwardDistance.at(kf); } + +void CodeGraphDistance::getNearestPredicateSatisfying( + KBlock *from, KBlockPredicate predicate, std::set &result) { + std::set visited; + + auto blockMap = from->parent->blockMap; + std::deque nodes; + nodes.push_back(from); + + while (!nodes.empty()) { + KBlock *currBB = nodes.front(); + visited.insert(currBB); + + if (predicate(currBB) && currBB != from) { + result.insert(currBB); + } else { + for (auto const &succ : successors(currBB->basicBlock)) { + if (visited.count(blockMap[succ]) == 0) { + nodes.push_back(blockMap[succ]); + } + } + } + nodes.pop_front(); + } +} diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 74f58f01b5..2ab1059a8f 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -404,7 +404,8 @@ void KModule::manifest(InterpreterHandler *ih, isInlineAsm = true; } if (kcb->calledFunctions.empty() && !isInlineAsm && - guidance != Interpreter::GuidanceKind::ErrorGuidance) { + (guidance != Interpreter::GuidanceKind::ErrorGuidance || + !inMainModule(*kfp.get()->function))) { kcb->calledFunctions.insert(escapingFunctions.begin(), escapingFunctions.end()); } @@ -447,8 +448,8 @@ KBlock *KModule::getKBlock(llvm::BasicBlock *bb) { return functionMap[bb->getParent()]->blockMap[bb]; } -bool KModule::inMainModule(llvm::Function *f) { - return mainModuleFunctions.count(f->getName().str()) != 0; +bool KModule::inMainModule(const llvm::Function &f) { + return mainModuleFunctions.count(f.getName().str()) != 0; } bool KModule::inMainModule(const GlobalVariable &v) { diff --git a/lib/Module/Target.cpp b/lib/Module/Target.cpp index c6d102375b..5e63ce51c5 100644 --- a/lib/Module/Target.cpp +++ b/lib/Module/Target.cpp @@ -26,19 +26,31 @@ llvm::cl::opt LocationAccuracy( cl::desc("Check location with line and column accuracy (default=false)")); } -std::string Target::toString() const { +std::string ReproduceErrorTarget::toString() const { std::ostringstream repr; repr << "Target " << getId() << ": "; - if (shouldFailOnThisTarget()) { - repr << "error in "; - } + repr << "error in "; + repr << block->toString(); + return repr.str(); +} + +std::string ReachBlockTarget::toString() const { + std::ostringstream repr; + repr << "Target: "; repr << block->toString(); - if (atReturn()) { + if (atEnd) { repr << " (at the end)"; } return repr.str(); } +std::string CoverBranchTarget::toString() const { + std::ostringstream repr; + repr << "Target: "; + repr << "cover " << branchCase << "branch at " << block->toString(); + return repr.str(); +} + Target::TargetCacheSet Target::cachedTargets; ref Target::createCachedTarget(ref target) { @@ -54,22 +66,33 @@ ref Target::createCachedTarget(ref target) { return (ref)*(success.first); } -ref Target::create(const std::vector &_errors, - const std::string &_id, optional _loc, - KBlock *_block) { - Target *target = new Target(_errors, _id, _loc, _block); +ref +ReproduceErrorTarget::create(const std::vector &_errors, + const std::string &_id, ErrorLocation _loc, + KBlock *_block) { + ReproduceErrorTarget *target = + new ReproduceErrorTarget(_errors, _id, _loc, _block); return createCachedTarget(target); } -ref Target::create(KBlock *_block) { - return create({ReachWithError::None}, "", nonstd::nullopt, _block); +ref ReachBlockTarget::create(KBlock *_block, bool _atEnd) { + ReachBlockTarget *target = new ReachBlockTarget(_block, _atEnd); + return createCachedTarget(target); } -bool Target::isTheSameAsIn(const KInstruction *instr) const { - if (!loc.has_value()) { - return false; - } - const auto &errLoc = *loc; +ref ReachBlockTarget::create(KBlock *_block) { + ReachBlockTarget *target = + new ReachBlockTarget(_block, isa(_block)); + return createCachedTarget(target); +} + +ref CoverBranchTarget::create(KBlock *_block, unsigned _branchCase) { + CoverBranchTarget *target = new CoverBranchTarget(_block, _branchCase); + return createCachedTarget(target); +} + +bool ReproduceErrorTarget::isTheSameAsIn(const KInstruction *instr) const { + const auto &errLoc = loc; return instr->info->line >= errLoc.startLine && instr->info->line <= errLoc.endLine && (!LocationAccuracy || !errLoc.startColumn.has_value() || @@ -77,16 +100,61 @@ bool Target::isTheSameAsIn(const KInstruction *instr) const { instr->info->column <= *errLoc.endColumn)); } -bool Target::mustVisitForkBranches(KInstruction *instr) const { - // null check after deref error is checked after fork - // but reachability of this target from instr children - // will always give false, so we need to force visiting - // fork branches here - return isTheSameAsIn(instr) && - isThatError(ReachWithError::NullCheckAfterDerefException); +int Target::compare(const Target &b) const { return internalCompare(b); } + +bool Target::equals(const Target &b) const { + return (toBeCleared || b.toBeCleared) || (isCached && b.isCached) + ? this == &b + : compare(b) == 0; } -int Target::compare(const Target &other) const { +int ReachBlockTarget::internalCompare(const Target &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const ReachBlockTarget &other = static_cast(b); + + if (block->parent->id != other.block->parent->id) { + return block->parent->id < other.block->parent->id ? -1 : 1; + } + if (block->id != other.block->id) { + return block->id < other.block->id ? -1 : 1; + } + + if (atEnd != other.atEnd) { + return !atEnd ? -1 : 1; + } + + return 0; +} + +int CoverBranchTarget::internalCompare(const Target &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const CoverBranchTarget &other = static_cast(b); + + if (block->parent->id != other.block->parent->id) { + return block->parent->id < other.block->parent->id ? -1 : 1; + } + if (block->id != other.block->id) { + return block->id < other.block->id ? -1 : 1; + } + + if (branchCase != other.branchCase) { + return branchCase < other.branchCase ? -1 : 1; + } + + return 0; +} + +int ReproduceErrorTarget::internalCompare(const Target &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const ReproduceErrorTarget &other = + static_cast(b); + if (id != other.id) { return id < other.id ? -1 : 1; } @@ -110,12 +178,6 @@ int Target::compare(const Target &other) const { return 0; } -bool Target::equals(const Target &b) const { - return (toBeCleared || b.toBeCleared) || (isCached && b.isCached) - ? this == &b - : compare(b) == 0; -} - bool Target::operator<(const Target &other) const { return compare(other) == -1; } diff --git a/lib/Module/TargetForest.cpp b/lib/Module/TargetForest.cpp index f512bf7cc5..07fed82b1d 100644 --- a/lib/Module/TargetForest.cpp +++ b/lib/Module/TargetForest.cpp @@ -117,12 +117,13 @@ void TargetForest::Layer::addTrace( for (auto block : it->second) { ref target = nullptr; if (i == result.locations.size() - 1) { - target = Target::create(result.errors, result.id, - ErrorLocation{loc->startLine, loc->endLine, - loc->startColumn, loc->endColumn}, - block); + target = ReproduceErrorTarget::create( + result.errors, result.id, + ErrorLocation{loc->startLine, loc->endLine, loc->startColumn, + loc->endColumn}, + block); } else { - target = Target::create(block); + target = ReachBlockTarget::create(block); } targets.insert(target); } @@ -442,16 +443,14 @@ int TargetsHistory::compare(const TargetsHistory &h) const { return 0; } - if (target && h.target) { - if (target != h.target) { - return (target < h.target) ? -1 : 1; - } + assert(target && h.target); + if (target != h.target) { + return (target < h.target) ? -1 : 1; } - if (visitedTargets && h.visitedTargets) { - if (h.visitedTargets != h.visitedTargets) { - return (visitedTargets < h.visitedTargets) ? -1 : 1; - } + assert(visitedTargets && h.visitedTargets); + if (visitedTargets != h.visitedTargets) { + return (visitedTargets < h.visitedTargets) ? -1 : 1; } return 0; @@ -494,7 +493,6 @@ void TargetForest::stepTo(ref loc) { } else { history = history->add(loc); forest = forest->replaceChildWith(loc, res->second); - loc->isReported = true; } if (forest->empty() && !loc->shouldFailOnThisTarget()) { history = TargetsHistory::create(); diff --git a/lib/Module/TargetHash.cpp b/lib/Module/TargetHash.cpp index 05f703ed10..7f5b9be2eb 100644 --- a/lib/Module/TargetHash.cpp +++ b/lib/Module/TargetHash.cpp @@ -26,3 +26,7 @@ std::size_t TransitionHash::operator()(const Transition &p) const { return reinterpret_cast(p.first) * 31 + reinterpret_cast(p.second); } + +std::size_t BranchHash::operator()(const Branch &p) const { + return reinterpret_cast(p.first) * 31 + p.second; +}