diff options
| -rw-r--r-- | lib/Solver/FastCexSolver.cpp | 66 | ||||
| -rw-r--r-- | test/Solver/FastCexSolver.pc | 12 | ||||
| -rw-r--r-- | test/Solver/dg.exp | 3 |
3 files changed, 76 insertions, 5 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index e9f40a49..5a2db747 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -401,6 +401,10 @@ public: : objects(_objects) {} }; +#if 0 +#define DEBUG +#endif + class CexData { public: std::map<const Array*, CexObjectData*> objects; @@ -434,12 +438,15 @@ public: } void propogatePossibleValues(ref<Expr> e, CexValueData range) { + #ifdef DEBUG + llvm::cerr << "propogate: " << range << " for\n" << e << "\n"; + #endif + switch (e->getKind()) { - case Expr::Constant: { + case Expr::Constant: // rather a pity if the constant isn't in the range, but how can // we use this? break; - } // Special @@ -525,7 +532,8 @@ public: ConcatExpr *ce = cast<ConcatExpr>(e); Expr::Width LSBWidth = ce->getKid(1)->getWidth(); Expr::Width MSBWidth = ce->getKid(1)->getWidth(); - propogatePossibleValues(ce->getKid(0), range.extract(LSBWidth, MSBWidth)); + propogatePossibleValues(ce->getKid(0), + range.extract(LSBWidth, LSBWidth + MSBWidth)); propogatePossibleValues(ce->getKid(1), range.extract(0, LSBWidth)); break; } @@ -568,6 +576,27 @@ public: // Binary + case Expr::Add: { + BinaryExpr *be = cast<BinaryExpr>(e); + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) { + // FIXME: Don't depend on width. + if (CE->getWidth() <= 64) { + // FIXME: Why do we ever propogate empty ranges? It doesn't make + // sense. + if (range.isEmpty()) + break; + + // C_0 + X \in [MIN, MAX) ==> X \in [MIN - C_0, MAX - C_0) + Expr::Width W = CE->getWidth(); + CexValueData nrange(ConstantExpr::alloc(range.min(), W)->Sub(CE)->getZExtValue(), + ConstantExpr::alloc(range.max(), W)->Sub(CE)->getZExtValue()); + if (!nrange.isEmpty()) + propogatePossibleValues(be->right, nrange); + } + } + break; + } + case Expr::And: { BinaryExpr *be = cast<BinaryExpr>(e); if (be->getWidth()==Expr::Bool) { @@ -743,8 +772,6 @@ public: } void propogateExactValues(ref<Expr> e, CexValueData range) { - //llvm::cout << e << " \\in " << range << "\n"; - switch (e->getKind()) { case Expr::Constant: { // FIXME: Assert that range contains this constant. @@ -890,6 +917,31 @@ public: ref<Expr> evaluateExact(ref<Expr> e) { return CexExactEvaluator(objects).visit(e); } + + void dump() { + llvm::cerr << "-- propogated values --\n"; + for (std::map<const Array*, CexObjectData*>::iterator + it = objects.begin(), ie = objects.end(); it != ie; ++it) { + const Array *A = it->first; + CexObjectData *COD = it->second; + + llvm::cerr << A->name << "\n"; + llvm::cerr << "possible: ["; + for (unsigned i = 0; i < A->size; ++i) { + if (i) + llvm::cerr << ", "; + llvm::cerr << COD->getPossibleValues(i); + } + llvm::cerr << "]\n"; + llvm::cerr << "exact : ["; + for (unsigned i = 0; i < A->size; ++i) { + if (i) + llvm::cerr << ", "; + llvm::cerr << COD->getExactValues(i); + } + llvm::cerr << "]\n"; + } + } }; /* *** */ @@ -938,6 +990,10 @@ static bool propogateValues(const Query& query, CexData &cd, cd.propogateExactValue(query.expr, 0); } +#ifdef DEBUG + cd.dump(); +#endif + // Check the result. bool hasSatisfyingAssignment = true; if (checkExpr) { diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.pc new file mode 100644 index 00000000..10cdce48 --- /dev/null +++ b/test/Solver/FastCexSolver.pc @@ -0,0 +1,12 @@ +# RUN: %kleaver --use-fast-cex-solver --use-dummy-solver %s > %t +# RUN: not grep FAIL %t + +array arr1[4] : w32 -> w8 = symbolic +(query [] (Not (Eq 4096 (ReadLSB w32 0 arr1)))) + +array arr2[2] : w32 -> w8 = symbolic +(query [(Ule (Add w8 208 N0:(Read w8 0 arr2)) + 9)] + (Eq 52 N0)) + + diff --git a/test/Solver/dg.exp b/test/Solver/dg.exp new file mode 100644 index 00000000..94fc4df8 --- /dev/null +++ b/test/Solver/dg.exp @@ -0,0 +1,3 @@ +load_lib llvm.exp + +RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]] |