about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-06-07 17:48:17 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-06-07 17:48:17 +0000
commit08e5f32e11923cdaa46f68c8cc5de1ff9e5036d0 (patch)
tree0213c1918e962ce2a81853204b6adc0c3f3485a5
parent1391a42343d7a597b9ee413551ba013218d21b8c (diff)
downloadklee-08e5f32e11923cdaa46f68c8cc5de1ff9e5036d0.tar.gz
Make sure that ExprEvaluator will fold constant expressions (klee never creates
these, but the parser can).


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73033 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--include/klee/util/ExprEvaluator.h1
-rw-r--r--lib/Expr/ExprEvaluator.cpp21
2 files changed, 22 insertions, 0 deletions
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
index be98942d..739e51e6 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/util/ExprEvaluator.h
@@ -18,6 +18,7 @@ namespace klee {
   protected:
     Action evalRead(const UpdateList &ul, unsigned index);
     Action visitRead(const ReadExpr &re);
+    Action visitExpr(const Expr &e);
       
     Action protectedDivOperation(const BinaryExpr &e);
     Action visitUDiv(const UDivExpr &e);
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index ca8f1611..eced0e87 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -33,6 +33,27 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
   return Action::changeTo(getInitialValue(*ul.root, index));
 }
 
+ExprVisitor::Action ExprEvaluator::visitExpr(const Expr &e) {
+  // Evaluate all constant expressions here, in case they weren't folded in
+  // construction. Don't do this for reads though, because we want them to go to
+  // the normal rewrite path.
+  unsigned N = e.getNumKids();
+  if (!N || isa<ReadExpr>(e))
+    return Action::doChildren();
+
+  for (unsigned i = 0; i != N; ++i)
+    if (!isa<ConstantExpr>(e.getKid(i)))
+      return Action::doChildren();
+
+  ref<Expr> Kids[3];
+  for (unsigned i = 0; i != N; ++i) {
+    assert(i < 3);
+    Kids[i] = e.getKid(i);
+  }
+
+  return Action::changeTo(e.rebuild(Kids));
+}
+
 ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
   ref<Expr> v = visit(re.index);