diff options
| -rw-r--r-- | include/klee/Constraints.h | 57 | ||||
| -rw-r--r-- | lib/Solver/CachingSolver.cpp | 12 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 26 |
3 files changed, 45 insertions, 50 deletions
diff --git a/include/klee/Constraints.h b/include/klee/Constraints.h index 87069f89..08077293 100644 --- a/include/klee/Constraints.h +++ b/include/klee/Constraints.h @@ -19,54 +19,47 @@ namespace klee { class ExprVisitor; - + class ConstraintManager { public: - typedef std::vector< ref<Expr> > constraints_ty; - typedef constraints_ty::iterator iterator; - typedef constraints_ty::const_iterator const_iterator; + using constraints_ty = std::vector<ref<Expr>>; + using iterator = constraints_ty::iterator; + using const_iterator = constraints_ty::const_iterator; - ConstraintManager() {} + ConstraintManager() = default; + ConstraintManager(const ConstraintManager &cs) = default; + ConstraintManager &operator=(const ConstraintManager &cs) = default; + ConstraintManager(ConstraintManager &&cs) = default; + ConstraintManager &operator=(ConstraintManager &&cs) = default; // create from constraints with no optimization - explicit - ConstraintManager(const std::vector< ref<Expr> > &_constraints) : - constraints(_constraints) {} - - ConstraintManager(const ConstraintManager &cs) : constraints(cs.constraints) {} - - typedef std::vector< ref<Expr> >::const_iterator constraint_iterator; + explicit ConstraintManager(const std::vector<ref<Expr>> &_constraints) + : constraints(_constraints) {} - // given a constraint which is known to be valid, attempt to + // given a constraint which is known to be valid, attempt to // simplify the existing constraint set void simplifyForValidConstraint(ref<Expr> e); ref<Expr> simplifyExpr(ref<Expr> e) const; void addConstraint(ref<Expr> e); - - bool empty() const { - return constraints.empty(); - } - ref<Expr> back() const { - return constraints.back(); - } - constraint_iterator begin() const { - return constraints.begin(); - } - constraint_iterator end() const { - return constraints.end(); - } - size_t size() const { - return constraints.size(); - } + + bool empty() const noexcept { return constraints.empty(); } + ref<Expr> back() const { return constraints.back(); } + const_iterator begin() const { return constraints.cbegin(); } + const_iterator end() const { return constraints.cend(); } + std::size_t size() const noexcept { return constraints.size(); } bool operator==(const ConstraintManager &other) const { return constraints == other.constraints; } - + + bool operator!=(const ConstraintManager &other) const { + return constraints != other.constraints; + } + private: - std::vector< ref<Expr> > constraints; + std::vector<ref<Expr>> constraints; // returns true iff the constraints were modified bool rewriteConstraints(ExprVisitor &visitor); @@ -74,6 +67,6 @@ private: void addConstraintInternal(ref<Expr> e); }; -} +} // namespace klee #endif /* KLEE_CONSTRAINTS_H */ diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index be46621b..a6ca93ac 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -53,15 +53,15 @@ private: return constraints==b.constraints && *query.get()==*b.query.get(); } }; - + struct CacheEntryHash { unsigned operator()(const CacheEntry &ce) const { unsigned result = ce.query->hash(); - - for (ConstraintManager::constraint_iterator it = ce.constraints.begin(); - it != ce.constraints.end(); ++it) - result ^= (*it)->hash(); - + + for (auto const &constraint : ce.constraints) { + result ^= constraint->hash(); + } + return result; } }; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 19a0d745..447e5575 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -441,12 +441,13 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) { // Helper function used only for assertions to make sure point created // during computeInitialValues is in fact correct. The ``retMap`` is used // in the case ``objects`` doesn't contain all the assignments needed. -bool assertCreatedPointEvaluatesToTrue(const Query &query, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - std::map<const Array*, std::vector<unsigned char> > &retMap){ - // _allowFreeValues is set to true so that if there are missing bytes in the assigment - // we will end up with a non ConstantExpr after evaluating the assignment and fail +bool assertCreatedPointEvaluatesToTrue( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char>> &values, + std::map<const Array *, std::vector<unsigned char>> &retMap) { + // _allowFreeValues is set to true so that if there are missing bytes in the + // assigment we will end up with a non ConstantExpr after evaluating the + // assignment and fail Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); // Add any additional bindings. @@ -456,19 +457,20 @@ bool assertCreatedPointEvaluatesToTrue(const Query &query, if (retMap.size() > 0) assign.bindings.insert(retMap.begin(), retMap.end()); - for(ConstraintManager::constraint_iterator it = query.constraints.begin(); - it != query.constraints.end(); ++it){ - ref<Expr> ret = assign.evaluate(*it); + for (auto const &constraint : query.constraints) { + ref<Expr> ret = assign.evaluate(constraint); - assert(isa<ConstantExpr>(ret) && "assignment evaluation did not result in constant"); + assert(isa<ConstantExpr>(ret) && + "assignment evaluation did not result in constant"); ref<ConstantExpr> evaluatedConstraint = dyn_cast<ConstantExpr>(ret); - if(evaluatedConstraint->isFalse()){ + if (evaluatedConstraint->isFalse()) { return false; } } ref<Expr> neg = Expr::createIsZero(query.expr); ref<Expr> q = assign.evaluate(neg); - assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); + assert(isa<ConstantExpr>(q) && + "assignment evaluation did not result in constant"); return cast<ConstantExpr>(q)->isTrue(); } |