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..06d1522923 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -39,7 +39,8 @@ 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") \ + TTMARK(EARLY, 14U) \ TTYPE(Solver, 20U, "solver.err") \ TTMARK(SOLVERERR, 20U) \ TTYPE(Abort, 30U, "abort.err") \ @@ -68,7 +69,7 @@ enum class StateTerminationClass : std::uint8_t { TTYPE(External, 61U, "external.err") \ TTMARK(EXECERR, 61U) \ TTYPE(Replay, 70U, "") \ - TTYPE(MissedAllTargets, 71U, "") \ + TTYPE(MissedAllTargets, 71U, "miss_all_targets.early") \ TTMARK(EARLYALGORITHM, 71U) \ TTYPE(SilentExit, 80U, "") \ TTMARK(EARLYUSER, 80U) \ 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/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/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/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..80bf7e0c1d 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 { @@ -45,35 +43,63 @@ struct ErrorLocation { optional endColumn; }; -struct Target { +class ReproduceErrorTarget; + +class Target { private: - typedef std::unordered_set - EquivTargetHashSet; - typedef std::unordered_set TargetHashSet; - static EquivTargetHashSet cachedTargets; - static TargetHashSet targets; +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); + } + }; + + 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()); + } + } + }; + KBlock *block; - std::set - 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 + static TargetCacheSet cachedTargets; + bool isCached = false; + bool toBeCleared = false; + + /// @brief Required by klee::ref-managed objects + mutable class ReferenceCounter _refCount; - explicit Target(const std::set &_errors, - const std::string &_id, optional _loc, - KBlock *_block) - : block(_block), errors(_errors), id(_id), loc(_loc) {} + explicit Target(KBlock *_block) : block(_block) {} - static ref getFromCacheOrReturn(Target *target); + static ref createCachedTarget(ref target); public: - bool isReported = false; - /// @brief Required by klee::ref-managed objects - class ReferenceCounter _refCount; + static const unsigned MAGIC_HASH_CONSTANT = 39; - static ref create(const std::set &_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; @@ -83,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; } @@ -93,23 +117,99 @@ struct Target { unsigned hash() const { return reinterpret_cast(block); } - const std::set &getErrors() const { return errors; } - bool isThatError(ReachWithError err) const; bool shouldFailOnThisTarget() const { - return errors.count(ReachWithError::None) == 0; + return isa(this); + } +}; + +class ReachBlockTarget : public Target { +protected: + bool atEnd; + + explicit ReachBlockTarget(KBlock *_block, bool _atEnd) + : Target(_block), atEnd(_atEnd) {} + +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()); } - bool isTheSameAsIn(KInstruction *instr) const; +public: + static ref create(const std::vector &_errors, + const std::string &_id, ErrorLocation _loc, + KBlock *_block); + + Kind getKind() const override { return Kind::ReproduceError; } - /// returns true if we cannot use CFG reachability checks - /// from instr children to this target - /// to avoid solver calls - bool mustVisitForkBranches(KInstruction *instr) const; + 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/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..2c2c2f81bd 100644 --- a/include/klee/Module/TargetHash.h +++ b/include/klee/Module/TargetHash.h @@ -21,46 +21,37 @@ class BasicBlock; } namespace klee { -struct Target; +class 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; }; typedef std::pair Transition; +typedef std::pair Branch; struct TransitionHash { std::size_t operator()(const Transition &p) const; }; -struct RefTargetLess { +struct BranchHash { + std::size_t operator()(const Branch &p) const; +}; + +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/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/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..15cf13be42 100644 --- a/lib/Core/DistanceCalculator.cpp +++ b/lib/Core/DistanceCalculator.cpp @@ -40,44 +40,70 @@ std::string DistanceResult::toString() const { return out.str(); } -DistanceResult DistanceCalculator::getDistance(ExecutionState &es, - ref target) { - return getDistance(es.pc, es.prevPC, es.initPC, es.stack, es.error, target); +unsigned DistanceCalculator::SpeculativeState::computeHash() { + unsigned res = + (reinterpret_cast(kb) * SymbolicSource::MAGIC_HASH_CONSTANT) + + kind; + hashValue = res; + return hashValue; } -DistanceResult -DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, - KInstruction *initPC, - const ExecutionState::stack_ty &stack, - ReachWithError error, ref target) { +DistanceResult DistanceCalculator::getDistance(const ExecutionState &state, + KBlock *target) { + return getDistance(state.prevPC, state.pc, state.stack.callStack(), target); +} + +DistanceResult DistanceCalculator::getDistance(KBlock *kb, TargetKind kind, + KBlock *target) { + SpeculativeState specState(kb, kind); + if (distanceResultCache.count(target) == 0 || + distanceResultCache.at(target).count(specState) == 0) { + auto result = computeDistance(kb, kind, target); + distanceResultCache[target][specState] = result; + } + return distanceResultCache.at(target).at(specState); +} + +DistanceResult DistanceCalculator::computeDistance(KBlock *kb, TargetKind kind, + KBlock *target) const { + const auto &distanceToTargetFunction = + codeGraphDistance.getBackwardDistance(target->parent); weight_type weight = 0; + WeightResult res = Miss; + bool isInsideFunction = true; + switch (kind) { + case LocalTarget: + res = tryGetTargetWeight(kb, weight, target); + break; - BasicBlock *pcBlock = pc->inst->getParent(); - BasicBlock *prevPCBlock = prevPC->inst->getParent(); + case PreTarget: + res = tryGetPreTargetWeight(kb, weight, distanceToTargetFunction, target); + isInsideFunction = false; + break; - 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); - } - } + case PostTarget: + res = tryGetPostTargetWeight(kb, weight, target); + isInsideFunction = false; + break; - if (target->shouldFailOnThisTarget() && target->isTheSameAsIn(prevPC) && - target->isThatError(error)) { - return DistanceResult(Done); + case NoneTarget: + break; } + return DistanceResult(res, weight, isInsideFunction); +} + +DistanceResult DistanceCalculator::getDistance( + const KInstruction *prevPC, const KInstruction *pc, + const ExecutionStack::call_stack_ty &frames, KBlock *target) { + weight_type weight = 0; - BasicBlock *bb = pcBlock; - KBlock *kb = pc->parent->parent->blockMap[bb]; + 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 = 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)); + sfi != sfe && sfi->kf->parent->inMainModule(*sfi->kf->function); for (; sfi != sfe; sfi++) { unsigned callWeight; if (distanceInCallGraph(sfi->kf, kb, callWeight, distanceToTargetFunction, @@ -85,7 +111,7 @@ DistanceCalculator::getDistance(KInstruction *pc, KInstruction *prevPC, callWeight *= 2; callWeight += sfNum; - if (callWeight < minCallWeight) { + if (callWeight < UINT_MAX) { minCallWeight = callWeight; minSfNum = sfNum; } @@ -93,44 +119,34 @@ 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, target); } bool DistanceCalculator::distanceInCallGraph( KFunction *kf, KBlock *origKB, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target, bool strictlyAfterKB) { + 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) { @@ -157,7 +173,7 @@ bool DistanceCalculator::distanceInCallGraph( KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target) { + KBlock *target) const { distance = UINT_MAX; const std::unordered_map &dist = codeGraphDistance.getDistance(kb); @@ -176,14 +192,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, + KBlock *target) const { + KFunction *currentKF = kb->parent; + KBlock *currentKB = kb; const std::unordered_map &dist = codeGraphDistance.getDistance(currentKB); weight = UINT_MAX; @@ -196,8 +210,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 +218,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; + KBlock *target) const { + KFunction *currentKF = kb->parent; std::vector localTargets; for (auto &kCallBlock : currentKF->kCallBlocks) { for (auto &calledFunction : kCallBlock->calledFunctions) { @@ -225,30 +237,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, + KBlock *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) { - std::vector localTargets = {target->getBlock()}; - WeightResult res = tryGetLocalWeight(pc, initPC, pcBlock, prevPCBlock, weight, - localTargets, target); +WeightResult DistanceCalculator::tryGetTargetWeight(KBlock *kb, + weight_type &weight, + 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 8d8ae38add..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,44 +48,85 @@ 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, - ReachWithError error, ref target); + DistanceResult getDistance(const ExecutionState &es, KBlock *target); + + DistanceResult getDistance(const KInstruction *prevPC, const KInstruction *pc, + const ExecutionStack::call_stack_ty &frames, + KBlock *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; + SpeculativeState(KBlock *kb_, TargetKind kind_) : kb(kb_), kind(kind_) { + 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.kind == b.kind; + } + }; + + using SpeculativeStateToDistanceResultMap = + std::unordered_map; + using TargetToSpeculativeStateToDistanceResultMap = + std::unordered_map; + + using StatesSet = std::unordered_set; + CodeGraphDistance &codeGraphDistance; + TargetToSpeculativeStateToDistanceResultMap distanceResultCache; + StatesSet localStates; + + DistanceResult getDistance(KBlock *kb, TargetKind kind, KBlock *target); + + DistanceResult computeDistance(KBlock *kb, TargetKind kind, + KBlock *target) const; bool distanceInCallGraph(KFunction *kf, KBlock *kb, unsigned int &distance, const std::unordered_map &distanceToTargetFunction, - ref target); + KBlock *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, + KBlock *target, bool strictlyAfterKB) const; + + WeightResult tryGetLocalWeight(KBlock *kb, weight_type &weight, const std::vector &localTargets, - ref target); + KBlock *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); + KBlock *target) const; + WeightResult tryGetTargetWeight(KBlock *kb, weight_type &weight, + KBlock *target) const; + WeightResult tryGetPostTargetWeight(KBlock *kb, weight_type &weight, + KBlock *target) const; }; } // namespace klee diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9288283849..90a2c9ac45 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,37 +63,80 @@ std::uint32_t ExecutionState::nextID = 1; /***/ -StackFrame::StackFrame(KInstIterator _caller, KFunction *_kf) - : caller(_caller), kf(_kf), callPathNode(0), minDistToUncoveredOnReturn(0), - varargs(0) { +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)); + } + 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(); + } + --stackBalance; + assert(valueStack_.size() == callStack_.size()); + assert(valueStack_.size() == infoStack_.size()); +} + +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), 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 +146,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(); } @@ -123,7 +176,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++; @@ -182,20 +238,18 @@ ExecutionState *ExecutionState::copy() const { } void ExecutionState::pushFrame(KInstIterator caller, KFunction *kf) { - stack.emplace_back(StackFrame(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(); - --stackBalance; + stack.popFrame(); } void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array, @@ -346,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') @@ -372,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 { @@ -383,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; } } @@ -411,8 +465,8 @@ void ExecutionState::increaseLevel() { KFunction *kf = prevPC->parent->parent; KModule *kmodule = kf->parent; - if (prevPC->inst->isTerminator() && kmodule->inMainModule(kf->function)) { - multilevel[srcbb]++; + if (prevPC->inst->isTerminator() && kmodule->inMainModule(*kf->function)) { + ++multilevel[srcbb]; level.insert(srcbb); } if (srcbb != dstbb) { @@ -420,8 +474,6 @@ void ExecutionState::increaseLevel() { } } -bool ExecutionState::isTransfered() { return getPrevPCBlock() != getPCBlock(); } - bool ExecutionState::isGEPExpr(ref expr) const { return UseGEPOptimization && gepExprBases.find(expr) != gepExprBases.end(); } @@ -430,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 3e4c9d3c2a..e0d432239b 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" @@ -51,26 +52,32 @@ 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); -struct StackFrame { +extern llvm::cl::opt MaxCyclesBeforeStuck; + +struct CallStackFrame { KInstIterator caller; KFunction *kf; - CallPathNode *callPathNode; + CallStackFrame(KInstIterator caller_, KFunction *kf_) + : caller(caller_), kf(kf_) {} + ~CallStackFrame() = default; + CallStackFrame(const CallStackFrame &s); + + bool equals(const CallStackFrame &other) const; + + bool operator==(const CallStackFrame &other) const { return equals(other); } +}; + +struct StackFrame { + KFunction *kf; 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 @@ -78,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: @@ -207,9 +256,7 @@ class ExecutionState { ExecutionState(const ExecutionState &state); public: - using stack_ty = std::vector; - using TargetHashSet = - std::unordered_set, RefTargetHash, RefTargetCmp>; + using stack_ty = ExecutionStack; // Execution - Control Flow specific @@ -223,7 +270,7 @@ 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; int stackBalance = 0; @@ -333,6 +380,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 +443,49 @@ class ExecutionState { llvm::BasicBlock *getPrevPCBlock() const; llvm::BasicBlock *getPCBlock() const; void increaseLevel(); - bool isTransfered(); + + inline bool isTransfered() const { return getPrevPCBlock() != getPCBlock(); } + bool isGEPExpr(ref expr) const; - bool reachedTarget(Target target) 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(ref 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..cde0b6d77d 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" @@ -56,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" @@ -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)}, - concretizationManager(new ConcretizationManager(EqualitySubstitution)), - codeGraphDistance(new CodeGraphDistance()), + guidanceKind(opts.Guidance), 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) { - - guidanceKind = opts.Guidance; - + 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) { const time::Span maxTime{MaxTime}; if (maxTime) timers.add(std::make_unique(maxTime, [&] { @@ -491,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); @@ -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,9 +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())); - return kmodule->module.get(); } @@ -1045,7 +1042,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. && @@ -1086,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.getTargets()) { + 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(nextInstr, es.prevPC, es.initPC, - es.stack, es.error, target); + auto dist = distanceCalculator->getDistance( + es.prevPC, nextInstr, es.stack.callStack(), target->getBlock()); if (dist.result != WeightResult::Miss) return true; } @@ -1387,28 +1400,14 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { klee_warning("seeds patched for violating constraint"); } - std::pair symcretization = - concretizationManager->get(state.constraints.cs(), condition); + Assignment concretization = computeConcretization( + state.constraints.cs(), condition, state.queryMetaData); - if (!symcretization.second && - Query(state.constraints.cs(), condition).containsSymcretes()) { - bool mayBeInBounds; - solver->setTimeout(coreSolverTimeout); - bool success = solver->mayBeTrue(state.constraints.cs(), condition, - mayBeInBounds, state.queryMetaData); - solver->setTimeout(time::Span()); - assert(success); - assert(mayBeInBounds); - symcretization = - concretizationManager->get(state.constraints.cs(), condition); - assert(symcretization.second); - } - - 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, {}); @@ -1444,7 +1443,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, @@ -1578,7 +1577,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); @@ -1747,7 +1752,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 { @@ -1755,7 +1760,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; @@ -1809,8 +1814,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 @@ -2101,7 +2106,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) @@ -2187,7 +2192,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 @@ -2265,7 +2271,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)); @@ -2359,7 +2365,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); } @@ -2396,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; } @@ -2408,7 +2416,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); @@ -2522,7 +2530,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 = @@ -2532,7 +2540,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) @@ -2571,7 +2579,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 @@ -2666,7 +2674,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 @@ -3907,6 +3915,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 +4064,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 +4080,6 @@ bool Executor::decreaseConfidenceFromStoppedStates( .subtractConfidencesFrom(state->targetForest, realReason); } } - return hasStateWhichCanReachSomeTarget; } void Executor::doDumpStates() { @@ -4178,9 +4192,9 @@ 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 distance = targetManager->distance(*state, target); auto it = distancesTowardsTargets.find(target); if (it == distancesTowardsTargets.end()) distancesTowardsTargets.insert(it, std::make_pair(target, distance)); @@ -4196,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(); @@ -4235,6 +4251,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 @@ -4244,7 +4263,8 @@ 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); } @@ -4256,30 +4276,24 @@ 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()) haltExecution = HaltExecution::NoMoreStates; } + doDumpStates(); + delete searcher; searcher = nullptr; + targetManager = nullptr; - doDumpStates(); haltExecution = HaltExecution::NotHalt; } @@ -4312,10 +4326,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()) { + 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.", + StateTerminationType::MaxCycles); + } else { + KInstruction *ki = state.pc; + stepInstruction(state); + executeInstruction(state, ki); + } - executeInstruction(state, ki); timers.invoke(); if (::dumpStates) dumpStates(); @@ -4340,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()); @@ -4445,6 +4469,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 +4481,11 @@ HaltExecution::Reason fromStateTerminationType(StateTerminationType t) { void Executor::terminateState(ExecutionState &state, StateTerminationType terminationType) { state.terminationReasonType = fromStateTerminationType(terminationType); + if (terminationType >= StateTerminationType::MaxDepth && + terminationType <= StateTerminationType::EARLY) { + SetOfStates states = {&state}; + decreaseConfidenceFromStoppedStates(states, state.terminationReasonType); + } if (replayKTest && replayPosition != replayKTest->numObjects) { klee_warning_once(replayKTest, "replay did not consume all objects in test input."); @@ -4467,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); } @@ -4508,11 +4541,15 @@ 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(), - terminationTypeFileExtension(reason).c_str()); + terminationTypeFileExtension(reason).c_str(), + reason > StateTerminationType::EARLY && + reason <= StateTerminationType::EXECERR); } terminateState(state, reason); } @@ -4537,8 +4574,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--; @@ -4586,9 +4624,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); } } } @@ -4658,7 +4696,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(); @@ -4668,10 +4706,10 @@ 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); terminateState(state, terminationType); if (shouldExitOn(terminationType)) @@ -4702,8 +4740,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, @@ -4976,7 +5012,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; } @@ -5773,15 +5809,11 @@ 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 concretization = computeConcretization( + state.constraints.cs(), resolveConditions.at(i), state.queryMetaData); + resolveConcretizations.push_back(concretization); } + return true; } @@ -6293,7 +6325,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, @@ -6565,7 +6598,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 +6626,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,11 +6690,13 @@ 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(ReachBlockTarget::create(target)); + prepareTargetedExecution(*state, targets); 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; @@ -6678,9 +6713,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, @@ -6730,12 +6768,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, @@ -6765,7 +6803,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) { @@ -6892,14 +6930,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 +6970,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); @@ -6951,6 +6989,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); @@ -6976,10 +7032,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) { - auto symcretization = - concretizationManager->get(extendedConstraints.cs(), pi); - if (symcretization.second) { - extendedConstraints.addConstraint(pi, symcretization.first); + Assignment concretization = computeConcretization( + extendedConstraints.cs(), pi, state.queryMetaData); + + if (!concretization.isEmpty()) { + extendedConstraints.addConstraint(pi, concretization); } else { extendedConstraints.addConstraint(pi, {}); } @@ -7179,12 +7236,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 << "), "; @@ -7193,7 +7251,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 582c22f0f0..d66ff5986f 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" @@ -95,6 +94,7 @@ class SpecialFunctionHandler; struct StackFrame; class SymbolicSource; class TargetCalculator; +class TargetManager; class StatsTracker; class TimingSolver; class TreeStreamWriter; @@ -144,11 +144,12 @@ class Executor : public Interpreter { TreeStreamWriter *pathWriter, *symPathWriter; SpecialFunctionHandler *specialFunctionHandler; TimerGroup timers; - std::unique_ptr concretizationManager; std::unique_ptr processForest; + GuidanceKind guidanceKind; 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 +183,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. @@ -241,7 +242,7 @@ 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` ref getEhTypeidFor(ref type_info); @@ -447,6 +448,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, @@ -497,11 +502,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, @@ -645,13 +650,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..5522316555 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->getBlock()); + 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(); +bool GuidedSearcher::isThereTarget(ref history, + ref target) { + return targetedSearchers.count({history, target}) != 0; } -void GuidedSearcher::printName(llvm::raw_ostream &os) { - os << "GuidedSearcher\n"; -} - -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"; } /// @@ -753,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; @@ -765,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/Searcher.h b/lib/Core/Searcher.h index 0469a00724..0a6c734f73 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,65 @@ 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::unordered_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/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 ba91e239ce..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); } } @@ -863,11 +866,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(); @@ -1130,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..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,57 +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.rbegin(), sfe = state.stack.rend(); sfi != sfe; - sfi++, sfNum++) { + for (auto sfi = state.stack.callStack().rbegin(), + sfe = state.stack.callStack().rend(); + 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) { @@ -143,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 new file mode 100644 index 0000000000..bfb3be2931 --- /dev/null +++ b/lib/Core/TargetManager.cpp @@ -0,0 +1,285 @@ +//===-- 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) { + if (targets(state).size() == 0) { + 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) { + 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; + } + + 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::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()) { + TargetHashSet targets(targetCalculator.calculate(state)); + if (!targets.empty()) { + for (auto target : targets) { + 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) { + updateReached(*state); + 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); + distances.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(); +} + +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 new file mode 100644 index 0000000000..11cba8bfc9 --- /dev/null +++ b/lib/Core/TargetManager.h @@ -0,0 +1,161 @@ +//===-- 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 StateToDistanceMap = + std::unordered_map>; + using TargetHistoryTargetPair = + std::pair, ref>; + using StatesVector = std::vector; + using TargetHistoryTargetPairToStatesMap = + std::unordered_map; + 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; + 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 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, + 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) { + + 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) { + 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(); } + + bool isReachedTarget(const ExecutionState &state, ref target); + + 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..25357773ae 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) { @@ -272,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; } @@ -286,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); @@ -296,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; } } @@ -478,23 +490,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 +530,13 @@ 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->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 @@ -529,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 @@ -537,7 +553,7 @@ bool TargetedExecutionManager::reportTruePositive(ExecutionState &state, found = false; break; } - possibleInstruction = state.stack[i].caller; + possibleInstruction = state.stack.callStack().at(i).caller; i--; } if (!found) @@ -545,16 +561,57 @@ 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; - reported_traces.insert(target->getId()); + errorTarget->isReported = true; + reportedTraces.insert(errorTarget->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 = targetManager.distance(*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(); +} diff --git a/lib/Core/TargetedExecutionManager.h b/lib/Core/TargetedExecutionManager.h index 079b230754..7d5b285d41 100644 --- a/lib/Core/TargetedExecutionManager.h +++ b/lib/Core/TargetedExecutionManager.h @@ -22,6 +22,8 @@ #include namespace klee { +class TargetManager; + extern llvm::cl::OptionCategory TerminationCat; /*** Termination criteria options ***/ @@ -56,6 +58,8 @@ extern llvm::cl::opt MaxStaticPctCheckDelay; extern llvm::cl::opt TimerInterval; +extern llvm::cl::opt MaxCycles; + class CodeGraphDistance; class TargetedHaltsOnTraces { @@ -64,8 +68,8 @@ class TargetedHaltsOnTraces { using TraceToHaltTypeToConfidence = std::unordered_map, HaltTypeToConfidence, - TargetForest::RefUnorderedTargetsSetHash, - TargetForest::RefUnorderedTargetsSetCmp>; + TargetForest::UnorderedTargetsSetHash, + TargetForest::UnorderedTargetsSetCmp>; TraceToHaltTypeToConfidence traceToHaltTypeToConfidence; static void totalConfidenceAndTopContributor( @@ -89,14 +93,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 +117,31 @@ class TargetedExecutionManager { LocationToBlocks &locToBlocks) const; CodeGraphDistance &codeGraphDistance; + TargetManager &targetManager; + 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_, + TargetManager &targetManager_) + : codeGraphDistance(codeGraphDistance_), targetManager(targetManager_) {} + ~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/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/SarifReport.cpp b/lib/Module/SarifReport.cpp index 0d51bb6078..075ce32417 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::MustBeNullPointerException}; } 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::MustBeNullPointerException}; // 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::MustBeNullPointerException}; // 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::MustBeNullPointerException}; } 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..5e63ce51c5 100644 --- a/lib/Module/Target.cpp +++ b/lib/Module/Target.cpp @@ -26,52 +26,73 @@ 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(); - if (atReturn()) { + return repr.str(); +} + +std::string ReachBlockTarget::toString() const { + std::ostringstream repr; + repr << "Target: "; + repr << block->toString(); + if (atEnd) { repr << " (at the end)"; } return repr.str(); } -Target::EquivTargetHashSet Target::cachedTargets; -Target::TargetHashSet Target::targets; +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) { + 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, - const std::string &_id, optional _loc, - KBlock *_block) { - Target *target = new Target(_errors, _id, _loc, _block); - return getFromCacheOrReturn(target); +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(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() || @@ -79,19 +100,61 @@ bool Target::isTheSameAsIn(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 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 Target::compare(const Target &other) const { - if (errors != other.errors) { - return errors < other.errors ? -1 : 1; +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; } @@ -101,26 +164,29 @@ 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::operator<(const Target &other) const { return compare(other) == -1; } 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..07fed82b1d 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,16 +113,17 @@ 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) { - 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); } @@ -205,8 +227,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 +239,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 +365,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 +392,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 +407,62 @@ 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 (target && h.target) { - if (target != h.target) - return (target < h.target) ? -1 : 1; - } else { - return h.target ? -1 : (target ? 1 : 0); + if (size() != h.size()) { + return (size() < h.size()) ? -1 : 1; } - if (visitedTargets && h.visitedTargets) { - if (h.visitedTargets != h.visitedTargets) - return (visitedTargets < h.visitedTargets) ? -1 : 1; - } else { - return h.visitedTargets ? -1 : (visitedTargets ? 1 : 0); + if (size() == 0) { + return 0; + } + + assert(target && h.target); + if (target != h.target) { + return (target < h.target) ? -1 : 1; + } + + assert(visitedTargets && h.visitedTargets); + if (visitedTargets != h.visitedTargets) { + return (visitedTargets < h.visitedTargets) ? -1 : 1; } 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 +474,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); } } @@ -484,10 +493,9 @@ 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 = History::create(); + history = TargetsHistory::create(); } } @@ -521,16 +529,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 +611,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..7f5b9be2eb 100644 --- a/lib/Module/TargetHash.cpp +++ b/lib/Module/TargetHash.cpp @@ -14,34 +14,19 @@ 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 { 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; +} 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 6fbbce8855..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,14 +27,11 @@ namespace klee { class ConcretizingSolver : public SolverImpl { private: std::unique_ptr solver; - ConcretizationManager *concretizationManager; 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; @@ -403,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; @@ -458,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; } @@ -475,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; @@ -515,10 +478,6 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) { } } - if (!isValid) { - concretizationManager->add(query.negateExpr(), assign); - } - return true; } @@ -565,7 +524,6 @@ bool ConcretizingSolver::computeValidityCore(const Query &query, if (!isValid) { validityCore = ValidityCore(); - concretizationManager->add(query.negateExpr(), assign); } return true; @@ -619,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; @@ -643,9 +598,8 @@ 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), concretizationManager, addressGenerator)); + return std::make_unique( + std::make_unique(std::move(s), addressGenerator)); } } // namespace klee 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/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..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 --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/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 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(); 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); } }