From f388e7a6f7aeb3813745bd1dc83cc1bf791fb101 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 3 Nov 2023 02:11:13 +0400 Subject: [PATCH 1/4] [style] --- lib/Core/Executor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index f7b5fe697f..fd4d9333be 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -7167,7 +7167,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { // also make understanding individual test cases much easier. const size_t cexPreferencesBound = 16; if (state.cexPreferences.size() > cexPreferencesBound) { - klee_warning_once(0, "skipping cex preffering (size of restrictons > %d).", + klee_warning_once(0, "skipping cex preffering (size of restrictons > %zu).", cexPreferencesBound); } else { for (auto &pi : state.cexPreferences) { From 2b5072fa05a838628b8bc813047d8127ae423327 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 3 Nov 2023 15:37:56 +0400 Subject: [PATCH 2/4] [fix] Consider all not empty and not fully covered functions --- lib/Core/TargetCalculator.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/lib/Core/TargetCalculator.cpp b/lib/Core/TargetCalculator.cpp index 94953d51b8..36c23a9026 100644 --- a/lib/Core/TargetCalculator.cpp +++ b/lib/Core/TargetCalculator.cpp @@ -92,8 +92,7 @@ void TargetCalculator::update(const ExecutionState &state) { } if (!fnsTaken.count(calledKFunction) && fullyCoveredFunctions.count(calledKFunction) == 0 && - calledKFunction->numInstructions != 0 && - !getCoverageTargets(calledKFunction).empty()) { + calledKFunction->numInstructions != 0) { fns.push_back(calledKFunction); } } From d3f26ef6df450427cd31081c6360c42c4130d855 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 3 Nov 2023 15:38:17 +0400 Subject: [PATCH 3/4] [fix] Fix perfomance bug --- include/klee/Expr/Assignment.h | 39 ++++++++++++++++++++++++-------- include/klee/Solver/SolverUtil.h | 20 +++------------- lib/Solver/CexCachingSolver.cpp | 25 ++------------------ 3 files changed, 34 insertions(+), 50 deletions(-) diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h index f72bb581b7..bb86172a60 100644 --- a/include/klee/Expr/Assignment.h +++ b/include/klee/Expr/Assignment.h @@ -25,6 +25,7 @@ class ConstraintSet; typedef std::set, SymcreteLess> SymcreteOrderedSet; using symcretes_ty = SymcreteOrderedSet; +typedef std::function)> ExprPredicate; class Assignment { public: @@ -57,11 +58,14 @@ class Assignment { ref evaluate(ref e, bool allowFreeValues = true) const; constraints_ty createConstraintsFromAssignment() const; + template + bool satisfies(InputIterator begin, InputIterator end, + ExprPredicate predicate, bool allowFreeValues = true); template bool satisfies(InputIterator begin, InputIterator end, bool allowFreeValues = true); template - bool satisfiesNonBoolean(InputIterator begin, InputIterator end, + bool satisfiesOrConstant(InputIterator begin, InputIterator end, bool allowFreeValues = true); void dump() const; @@ -115,28 +119,43 @@ inline ref Assignment::evaluate(ref e, bool allowFreeValues) const { return v.visit(e); } +struct isTrueBoolean { + bool operator()(ref e) const { + return e->getWidth() == Expr::Bool && e->isTrue(); + } +}; + +struct isTrueBooleanOrConstantNotBoolean { + bool operator()(ref e) const { + return (e->getWidth() == Expr::Bool && e->isTrue()) || + ((isa(e) && e->getWidth() != Expr::Bool)); + } +}; + template inline bool Assignment::satisfies(InputIterator begin, InputIterator end, + ExprPredicate predicate, bool allowFreeValues) { AssignmentEvaluator v(*this, allowFreeValues); for (; begin != end; ++begin) { - assert((*begin)->getWidth() == Expr::Bool && "constraints must be boolean"); - if (!v.visit(*begin)->isTrue()) + if (!predicate(v.visit(*begin))) return false; } return true; } template -inline bool Assignment::satisfiesNonBoolean(InputIterator begin, +inline bool Assignment::satisfies(InputIterator begin, InputIterator end, + bool allowFreeValues) { + return satisfies(begin, end, isTrueBoolean(), allowFreeValues); +} + +template +inline bool Assignment::satisfiesOrConstant(InputIterator begin, InputIterator end, bool allowFreeValues) { - AssignmentEvaluator v(*this, allowFreeValues); - for (; begin != end; ++begin) { - if (!isa(v.visit(*begin))) - return false; - } - return true; + return satisfies(begin, end, isTrueBooleanOrConstantNotBoolean(), + allowFreeValues); } } // namespace klee diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h index ffd3849c62..9be7d0f2d2 100644 --- a/include/klee/Solver/SolverUtil.h +++ b/include/klee/Solver/SolverUtil.h @@ -299,26 +299,12 @@ class InvalidResponse : public SolverResponse { } bool satisfies(const std::set> &key, bool allowFreeValues = true) { - std::set> booleanKey; - std::set> nonBooleanKey; - - for (auto i : key) { - if (i->getWidth() == Expr::Bool) { - booleanKey.insert(i); - } else { - nonBooleanKey.insert(i); - } - } - - return result.satisfies(booleanKey.begin(), booleanKey.end(), - allowFreeValues) && - result.satisfiesNonBoolean(nonBooleanKey.begin(), - nonBooleanKey.end(), allowFreeValues); + return result.satisfies(key.begin(), key.end(), allowFreeValues); } - bool satisfiesNonBoolean(const std::set> &key, + bool satisfiesOrConstant(const std::set> &key, bool allowFreeValues = true) { - return result.satisfiesNonBoolean(key.begin(), key.end(), allowFreeValues); + return result.satisfiesOrConstant(key.begin(), key.end(), allowFreeValues); } void dump() { result.dump(); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index ddb5861c88..74144a0697 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -169,16 +169,6 @@ bool CexCachingSolver::searchForResponse(KeyType &key, return true; } - KeyType booleanKey; - KeyType nonBooleanKey; - for (auto i : key) { - if (i->getWidth() == Expr::Bool) { - booleanKey.insert(i); - } else { - nonBooleanKey.insert(i); - } - } - // Otherwise, iterate through the set of current solver responses to see if // one of them satisfies the query. for (responseTable_ty::iterator it = responseTable.begin(), @@ -186,8 +176,7 @@ bool CexCachingSolver::searchForResponse(KeyType &key, it != ie; ++it) { ref a = *it; if (isa(a) && - cast(a)->satisfies(booleanKey) && - cast(a)->satisfiesNonBoolean(nonBooleanKey)) { + cast(a)->satisfiesOrConstant(key)) { result = a; return true; } @@ -272,17 +261,7 @@ bool CexCachingSolver::getResponse(const Query &query, } if (DebugCexCacheCheckBinding) { - KeyType booleanKey; - KeyType nonBooleanKey; - for (auto i : key) { - if (i->getWidth() == Expr::Bool) { - booleanKey.insert(i); - } else { - nonBooleanKey.insert(i); - } - } - if (!cast(result)->satisfies(booleanKey) || - !cast(result)->satisfiesNonBoolean(nonBooleanKey)) { + if (!cast(result)->satisfiesOrConstant(key)) { query.dump(); result->dump(); klee_error("Generated assignment doesn't match query"); From facd5751fe67533c25ea88c72cd346763e04fc1a Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 3 Nov 2023 16:48:59 +0400 Subject: [PATCH 4/4] [fix] Fix `isStuck` --- lib/Core/ExecutionState.h | 4 ++-- lib/Core/Executor.cpp | 2 +- lib/Core/TargetManager.cpp | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 7ae7d692cb..9e74c4ef37 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -509,9 +509,9 @@ class ExecutionState { } inline bool isStuck(unsigned long long bound) const { - if (depth == 1) + if (depth == 0) return false; - return isCycled(bound) && depth > klee::util::ulog2(bound); + return isCycled(bound) && klee::util::ulog2(depth) > bound; } bool isCoveredNew() const { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fd4d9333be..b4e17bf9e6 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4415,7 +4415,7 @@ void Executor::executeStep(ExecutionState &state) { if (targetManager->isTargeted(state) && state.targets().empty()) { terminateStateEarlyAlgorithm(state, "State missed all it's targets.", StateTerminationType::MissedAllTargets); - } else if (state.isStuck(MaxCycles)) { + } else if (state.isCycled(MaxCycles)) { terminateStateEarly(state, "max-cycles exceeded.", StateTerminationType::MaxCycles); } else { diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index 23ad1347e8..9dcaedcd86 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -135,7 +135,7 @@ void TargetManager::updateReached(ExecutionState &state) { void TargetManager::updateTargets(ExecutionState &state) { if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { - if (targets(state).empty() && state.isCycled(MaxCyclesBeforeStuck)) { + if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { state.setTargeted(true); } if (isTargeted(state) && targets(state).empty()) {