1 files changed, 155 insertions, 0 deletions
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
new file mode 100644
index 00000000..e9c376f4
--- /dev/null
+++ b/lib/Expr/Constraints.cpp
@@ -0,0 +1,155 @@
+//===-- Constraints.cpp ---------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Constraints.h"
+
+#include "klee/util/ExprPPrinter.h"
+#include "klee/util/ExprVisitor.h"
+
+#include <iostream>
+#include <map>
+
+using namespace klee;
+
+class ExprReplaceVisitor : public ExprVisitor {
+private:
+  ref<Expr> src, dst;
+
+public:
+  ExprReplaceVisitor(ref<Expr> _src, ref<Expr> _dst) : src(_src), dst(_dst) {}
+
+  Action visitExpr(const Expr &e) {
+    if (e == *src.get()) {
+      return Action::changeTo(dst);
+    } else {
+      return Action::doChildren();
+    }
+  }
+
+  Action visitExprPost(const Expr &e) {
+    if (e == *src.get()) {
+      return Action::changeTo(dst);
+    } else {
+      return Action::doChildren();
+    }
+  }
+};
+
+class ExprReplaceVisitor2 : public ExprVisitor {
+private:
+  const std::map< ref<Expr>, ref<Expr> > &replacements;
+
+public:
+  ExprReplaceVisitor2(const std::map< ref<Expr>, ref<Expr> > &_replacements) 
+    : ExprVisitor(true),
+      replacements(_replacements) {}
+
+  Action visitExprPost(const Expr &e) {
+    std::map< ref<Expr>, ref<Expr> >::const_iterator it =
+      replacements.find(ref<Expr>((Expr*) &e));
+    if (it!=replacements.end()) {
+      return Action::changeTo(it->second);
+    } else {
+      return Action::doChildren();
+    }
+  }
+};
+
+bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
+  ConstraintManager::constraints_ty old;
+  bool changed = false;
+
+  constraints.swap(old);
+  for (ConstraintManager::constraints_ty::iterator 
+         it = old.begin(), ie = old.end(); it != ie; ++it) {
+    ref<Expr> &ce = *it;
+    ref<Expr> e = visitor.visit(ce);
+
+    if (e!=ce) {
+      addConstraintInternal(e); // enable further reductions
+      changed = true;
+    } else {
+      constraints.push_back(ce);
+    }
+  }
+
+  return changed;
+}
+
+void ConstraintManager::simplifyForValidConstraint(ref<Expr> e) {
+  // XXX 
+}
+
+ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
+  if (e.isConstant())
+    return e;
+
+  std::map< ref<Expr>, ref<Expr> > equalities;
+  
+  for (ConstraintManager::constraints_ty::const_iterator 
+         it = constraints.begin(), ie = constraints.end(); it != ie; ++it) {
+    if (const EqExpr *ee = dyn_ref_cast<EqExpr>(*it)) {
+      if (ee->left.isConstant()) {
+        equalities.insert(std::make_pair(ee->right,
+                                         ee->left));
+      } else {
+        equalities.insert(std::make_pair(*it,
+                                         ref<Expr>(1,Expr::Bool)));
+      }
+    } else {
+      equalities.insert(std::make_pair(*it,
+                                       ref<Expr>(1,Expr::Bool)));
+    }
+  }
+
+  return ExprReplaceVisitor2(equalities).visit(e);
+}
+
+void ConstraintManager::addConstraintInternal(ref<Expr> e) {
+  // rewrite any known equalities 
+
+  // XXX should profile the effects of this and the overhead.
+  // traversing the constraints looking for equalities is hardly the
+  // slowest thing we do, but it is probably nicer to have a
+  // ConstraintSet ADT which efficiently remembers obvious patterns
+  // (byte-constant comparison).
+
+  switch (e.getKind()) {
+  case Expr::Constant:
+    assert(e.getConstantValue() && "attempt to add invalid (false) constraint");
+    break;
+    
+    // split to enable finer grained independence and other optimizations
+  case Expr::And: {
+    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    addConstraintInternal(be->left);
+    addConstraintInternal(be->right);
+    break;
+  }
+
+  case Expr::Eq: {
+    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    if (be->left.isConstant()) {
+      ExprReplaceVisitor visitor(be->right, be->left);
+      rewriteConstraints(visitor);
+    }
+    constraints.push_back(e);
+    break;
+  }
+    
+  default:
+    constraints.push_back(e);
+    break;
+  }
+}
+
+void ConstraintManager::addConstraint(ref<Expr> e) {
+  e = simplifyExpr(e);
+  addConstraintInternal(e);
+}