diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-08 06:49:10 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-08 06:49:10 +0000 |
commit | 62cbc80b703edf16c2d0dc7d0bb4fada78257bc8 (patch) | |
tree | a143cca9434c9980d255f79f4d14bb59e69c693a /lib/Solver | |
parent | 807b4e140d8afb55b3651fdcaf9ebe733afeb67e (diff) | |
download | klee-62cbc80b703edf16c2d0dc7d0bb4fada78257bc8.tar.gz |
FastCexSolver: Stub out infrastructure for propogating exact values & proving
validity. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73055 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 166 |
1 files changed, 148 insertions, 18 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 516df85d..6882682a 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -346,15 +346,14 @@ public: } }; -class CexEvaluator : public ExprEvaluator { +class CexPossibleEvaluator : public ExprEvaluator { protected: ref<Expr> getInitialValue(const Array& array, unsigned index) { // If the index is out of range, we cannot assign it a value, since that // value cannot be part of the assignment. - if (index >= array.size) { + if (index >= array.size) return ReadExpr::create(UpdateList(&array, true, 0), ConstantExpr::alloc(index, Expr::Int32)); - } std::map<unsigned, CexObjectData*>::iterator it = objects.find(array.id); return ConstantExpr::alloc((it == objects.end() ? 127 : @@ -364,7 +363,35 @@ protected: public: std::map<unsigned, CexObjectData*> &objects; - CexEvaluator(std::map<unsigned, CexObjectData*> &_objects) + CexPossibleEvaluator(std::map<unsigned, CexObjectData*> &_objects) + : objects(_objects) {} +}; + +class CexExactEvaluator : public ExprEvaluator { +protected: + ref<Expr> getInitialValue(const Array& array, unsigned index) { + // If the index is out of range, we cannot assign it a value, since that + // value cannot be part of the assignment. + if (index >= array.size) + return ReadExpr::create(UpdateList(&array, true, 0), + ConstantExpr::alloc(index, Expr::Int32)); + + std::map<unsigned, CexObjectData*>::iterator it = objects.find(array.id); + if (it == objects.end()) + return ReadExpr::create(UpdateList(&array, true, 0), + ConstantExpr::alloc(index, Expr::Int32)); + + CexValueData cvd = it->second->getExactValues(index); + if (!cvd.isFixed()) + return ReadExpr::create(UpdateList(&array, true, 0), + ConstantExpr::alloc(index, Expr::Int32)); + + return ConstantExpr::alloc(cvd.min(), Expr::Int8); + } + +public: + std::map<unsigned, CexObjectData*> &objects; + CexExactEvaluator(std::map<unsigned, CexObjectData*> &_objects) : objects(_objects) {} }; @@ -396,6 +423,10 @@ public: propogatePossibleValues(e, CexValueData(value,value)); } + void propogateExactValue(ref<Expr> e, uint64_t value) { + propogateExactValues(e, CexValueData(value,value)); + } + void propogatePossibleValues(ref<Expr> e, CexValueData range) { switch (e->getKind()) { case Expr::Constant: { @@ -700,6 +731,83 @@ public: } } + void propogateExactValues(ref<Expr> e, CexValueData range) { + switch (e->getKind()) { + case Expr::Constant: { + // FIXME: Assert that range contains this constant. + break; + } + + // Special + + case Expr::NotOptimized: break; + + case Expr::Read: { + break; + } + + case Expr::Select: { + break; + } + + case Expr::Concat: { + break; + } + + case Expr::Extract: { + break; + } + + // Casting + + case Expr::ZExt: { + break; + } + + case Expr::SExt: { + break; + } + + // Binary + + case Expr::And: { + break; + } + + case Expr::Or: { + break; + } + + case Expr::Xor: { + break; + } + + // Comparison + + case Expr::Eq: { + break; + } + + case Expr::Ult: { + break; + } + + case Expr::Ule: { + break; + } + + case Expr::Ne: + case Expr::Ugt: + case Expr::Uge: + case Expr::Sgt: + case Expr::Sge: + assert(0 && "invalid expressions (uncanonicalized"); + + default: + break; + } + } + ValueRange evalRangeForExpr(ref<Expr> &e) { CexRangeEvaluator ce(objects); return ce.evaluate(e); @@ -707,8 +815,12 @@ public: /// evaluate - Try to evaluate the given expression using a consistent fixed /// value for the current set of possible ranges. - ref<Expr> evaluate(ref<Expr> e) { - return CexEvaluator(objects).visit(e); + ref<Expr> evaluatePossible(ref<Expr> e) { + return CexPossibleEvaluator(objects).visit(e); + } + + ref<Expr> evaluateExact(ref<Expr> e) { + return CexExactEvaluator(objects).visit(e); } }; @@ -749,22 +861,40 @@ FastCexSolver::~FastCexSolver() { } static bool propogateValues(const Query& query, CexData &cd, bool checkExpr, bool &isValid) { for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) + ie = query.constraints.end(); it != ie; ++it) { cd.propogatePossibleValue(*it, 1); - if (checkExpr) + cd.propogateExactValue(*it, 1); + } + if (checkExpr) { cd.propogatePossibleValue(query.expr, 0); + cd.propogateExactValue(query.expr, 0); + } // Check the result. - if (checkExpr) - if (!cd.evaluate(query.expr)->isFalse()) + if (checkExpr) { + if (!cd.evaluatePossible(query.expr)->isFalse()) return false; + // If the query is known to be true, then we have proved validity. + if (cd.evaluateExact(query.expr)->isTrue()) { + isValid = true; + return true; + } + } + for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) - if (!cd.evaluate(*it)->isTrue()) + ie = query.constraints.end(); it != ie; ++it) { + if (!cd.evaluatePossible(*it)->isTrue()) return false; - // Currently we can only prove invalidity. + // If this constraint is known to be false, then we can prove anything, so + // the query is valid. + if (cd.evaluateExact(*it)->isFalse()) { + isValid = true; + return true; + } + } + isValid = false; return true; } @@ -797,7 +927,7 @@ bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) { return false; // Propogation found a satisfying assignment, evaluate the expression. - ref<Expr> value = cd.evaluate(query.expr); + ref<Expr> value = cd.evaluatePossible(query.expr); if (isa<ConstantExpr>(value)) { // FIXME: We should be able to make sure this never fails? @@ -835,10 +965,10 @@ FastCexSolver::computeInitialValues(const Query& query, data.reserve(array->size); for (unsigned i=0; i < array->size; i++) { - ref<Expr> value = - cd.evaluate(ReadExpr::create(UpdateList(array, true, 0), - ConstantExpr::create(i, - kMachinePointerType))); + ref<Expr> read = + ReadExpr::create(UpdateList(array, true, 0), + ConstantExpr::create(i, kMachinePointerType)); + ref<Expr> value = cd.evaluatePossible(read); if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) { data.push_back((unsigned char) CE->getConstantValue()); |