From f992f74ff55edfbe8134eee4c5494803da8fdabc Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Mon, 8 Jun 2009 07:41:41 +0000
Subject: FastCexSolver: Start implementing exact value propogation.  - So far
 this just propogates obvious equalities and reads. For example,   
 FastCexSolver can now prove that: -- array arr219[3] : w32 -> w8 = symbolic
 (query [(Eq 235 N0:(Read w8 0 arr219))]        (Eq 235 N0)) --    is valid.

Even though this is very basic, it is good enough to solve ~50% of the valid
queries on pcresymtest-[34].pc (total reduction in # of queries is ~25%).
Unfortunately, this only gives a 1-2% speedup, which is disappointing, but there
is a lot more we can do.

I'm a little surprised the speedup is so low, this may be an indicator that
there are some other things going on, for example perhaps the STP expr
construction cost for arrays is very high, and we inevitably will end up paying
this unless we solve so many queries that some arrays never ever make it to STP.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73058 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/Solver/FastCexSolver.cpp | 66 ++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 60 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 6882682a..ea5427e3 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -732,6 +732,8 @@ 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.
@@ -743,6 +745,37 @@ public:
     case Expr::NotOptimized: break;
 
     case Expr::Read: {
+      ReadExpr *re = cast<ReadExpr>(e);
+      const Array *array = re->updates.root;
+      CexObjectData &cod = getObjectData(array);
+      CexValueData index = evalRangeForExpr(re->index);
+        
+      for (const UpdateNode *un = re->updates.head; un; un = un->next) {
+        CexValueData ui = evalRangeForExpr(un->index);
+
+        // If these indices can't alias, continue propogation
+        if (!ui.mayEqual(index))
+          continue;
+
+        // Otherwise if we know they alias, propogate into the write value.
+        if (ui.mustEqual(index) || re->index == un->index)
+          propogateExactValues(un->value, range);
+        return;
+      }
+
+      // We reached the initial array write, update the exact range if possible.
+      if (index.isFixed()) {
+        CexValueData cvd = cod.getExactValues(index.min());
+        if (range.min() > cvd.min()) {
+          assert(range.min() <= cvd.max());
+          cvd = CexValueData(range.min(), cvd.max());
+        }
+        if (range.max() < cvd.max()) {
+          assert(range.max() >= cvd.min());
+          cvd = CexValueData(cvd.min(), range.max());
+        }
+        cod.setExactValues(index.min(), cvd);
+      }
       break;
     }
 
@@ -785,6 +818,22 @@ public:
       // Comparison
 
     case Expr::Eq: {
+      BinaryExpr *be = cast<BinaryExpr>(e);
+      if (range.isFixed()) {
+        if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
+          uint64_t value = CE->getConstantValue();
+          if (range.min()) {
+            // If the equality is true, then propogate the value.
+            propogateExactValue(be->right, value);
+          } else {
+            // If the equality is false and the comparison is of booleans, then
+            // we can infer the value to propogate.
+            if (be->right->getWidth() == Expr::Bool) {
+              propogateExactValue(be->right, !value);
+            }
+          }
+        }
+      }
       break;
     }
 
@@ -808,7 +857,7 @@ public:
     }
   }
 
-  ValueRange evalRangeForExpr(ref<Expr> &e) {
+  ValueRange evalRangeForExpr(const ref<Expr> &e) {
     CexRangeEvaluator ce(objects);
     return ce.evaluate(e);
   }
@@ -871,9 +920,10 @@ static bool propogateValues(const Query& query, CexData &cd,
   }
 
   // Check the result.
+  bool hasSatisfyingAssignment = true;
   if (checkExpr) {
     if (!cd.evaluatePossible(query.expr)->isFalse())
-      return false;
+      hasSatisfyingAssignment = false;
 
     // If the query is known to be true, then we have proved validity.
     if (cd.evaluateExact(query.expr)->isTrue()) {
@@ -884,8 +934,8 @@ static bool propogateValues(const Query& query, CexData &cd,
 
   for (ConstraintManager::const_iterator it = query.constraints.begin(), 
          ie = query.constraints.end(); it != ie; ++it) {
-    if (!cd.evaluatePossible(*it)->isTrue())
-      return false;
+    if (hasSatisfyingAssignment && !cd.evaluatePossible(*it)->isTrue())
+      hasSatisfyingAssignment = false;
 
     // If this constraint is known to be false, then we can prove anything, so
     // the query is valid.
@@ -895,8 +945,12 @@ static bool propogateValues(const Query& query, CexData &cd,
     }
   }
 
-  isValid = false;
-  return true;
+  if (hasSatisfyingAssignment) {
+    isValid = false;
+    return true;
+  }
+
+  return false;
 }
 
 IncompleteSolver::PartialValidity 
-- 
cgit 1.4.1