Conditions Dumped

include/klee/Expr/Constraints.h

@@ -40,6 +40,14 @@ class ConstraintSet {
     return constraints == b.constraints;
   }
 
+  // REVISIT
+  inline void printConstraintSetTY(std::stringstream &sso) {
+    sso << "Constraints Set :: " << "\n";
+    for (const auto &conds : constraints) {
+      sso << conds << "\n";
+    }
+  }
+
 private:
   constraints_ty constraints;
 };

lib/Core/Executor.cpp

@@ -882,6 +882,12 @@ void Executor::branch(ExecutionState &state,
   unsigned N = conditions.size();
   assert(N);
 
+  *conditionsDump << "Executor Branch ::"
+                  << "\n";
+  for (const auto &conds : conditions) {
+    *conditionsDump << conds << "\n";
+  }
+
   if (!branchingPermitted(state)) {
     unsigned next = theRNG.getInt32() % N;
     for (unsigned i = 0; i < N; ++i) {
@@ -965,6 +971,10 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       seedMap.find(&current);
   bool isSeeding = it != seedMap.end();
 
+  // REVISIT
+  *conditionsDump << "Fork :: " << current.getID() << "\n";
+  *conditionsDump << condition << "\n";
+
   if (!isSeeding && !isa<ConstantExpr>(condition) &&
       (MaxStaticForkPct != 1. || MaxStaticSolvePct != 1. ||
        MaxStaticCPForkPct != 1. || MaxStaticCPSolvePct != 1.) &&
@@ -1208,6 +1218,10 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
   }
 
   state.addConstraint(condition);
+  *conditionsDump << "Constraints :: "
+                  << "\n";
+  *conditionsDump << condition << "\n";
+
   if (ivcEnabled)
     doImpliedValueConcretization(state, condition,
                                  ConstantExpr::alloc(1, Expr::Bool));
@@ -2108,8 +2122,10 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     } else {
       // FIXME: Find a way that we don't have this hidden dependency.
       assert(bi->getCondition() == bi->getOperand(0) && "Wrong operand index!");
-      ref<Expr> cond = eval(ki, 0, state).value;
 
+      // REVISIT
+      ref<Expr> cond = eval(ki, 0, state).value;
+      *conditionsDump << ki->getSourceLocation() << "\n";
       cond = optimizer.optimizeExpr(cond, false);
       Executor::StatePair branches = fork(state, cond, false);
 
@@ -3331,9 +3347,9 @@ void Executor::computeOffsets(KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) {
     if (StructType *st = dyn_cast<StructType>(*ii)) {
       const StructLayout *sl = kmodule->targetData->getStructLayout(st);
       const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
-      uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue());
-      constantOffset = constantOffset->Add(ConstantExpr::alloc(addend,
-                                                               Context::get().getPointerWidth()));
+      uint64_t addend = sl->getElementOffset((unsigned)ci->getZExtValue());
+      constantOffset = constantOffset->Add(
+          ConstantExpr::alloc(addend, Context::get().getPointerWidth()));
 #if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
     } else if (isa<ArrayType>(*ii)) {
       computeOffsetsSeqTy<ArrayType>(kgepi, constantOffset, index, ii);
@@ -4430,8 +4446,9 @@ void Executor::runFunctionAsMain(Function *f, int argc, char **argv,
   executionTree = std::make_unique<ETree>(initState);
   processTree = std::make_unique<PTree>(state);
 
-  kqueryDumpFileptr = interpreterHandler->openOutputFile("kquey_dump.txt");
+  kqueryDumpFileptr = interpreterHandler->openOutputFile("kquery_dump.txt");
   smtlib2DumpFileptr = interpreterHandler->openOutputFile("smtlib2_dump.txt");
+  conditionsDump = interpreterHandler->openOutputFile("conds_dump.txt");
 
   run(*state);
   printETree();

lib/Core/Executor.h

@@ -99,10 +99,8 @@ class Executor : public Interpreter {
 public:
   typedef std::pair<ExecutionState *, ExecutionState *> StatePair;
 
-  /// KQuery Dump file pointer.
-  /// FIXME : Make Private
   std::unique_ptr<llvm::raw_fd_ostream> kqueryDumpFileptr, smtlib2DumpFileptr,
-      stackDump;
+      conditionsDump, stackDump;
 
   enum TerminateReason {
     Abort,

lib/Expr/Constraints.cpp

@@ -25,8 +25,7 @@ llvm::cl::opt<bool> RewriteEqualities(
     "rewrite-equalities",
     llvm::cl::desc("Rewrite existing constraints when an equality with a "
                    "constant is added (default=true)"),
-    llvm::cl::init(true),
-    llvm::cl::cat(SolvingCat));
+    llvm::cl::init(true), llvm::cl::cat(SolvingCat));
 } // namespace
 
 class ExprReplaceVisitor : public ExprVisitor {
@@ -54,7 +53,7 @@ class ExprReplaceVisitor : public ExprVisitor {
 
 class ExprReplaceVisitor2 : public ExprVisitor {
 private:
-  const std::map< ref<Expr>, ref<Expr> > &replacements;
+  const std::map<ref<Expr>, ref<Expr>> &replacements;
 
 public:
   explicit ExprReplaceVisitor2(
@@ -63,7 +62,7 @@ class ExprReplaceVisitor2 : public ExprVisitor {
 
   Action visitExprPost(const Expr &e) override {
     auto it = replacements.find(ref<Expr>(const_cast<Expr *>(&e)));
-    if (it!=replacements.end()) {
+    if (it != replacements.end()) {
       return Action::changeTo(it->second);
     }
     return Action::doChildren();
@@ -78,7 +77,7 @@ bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
   for (auto &ce : old) {
     ref<Expr> e = visitor.visit(ce);
 
-    if (e!=ce) {
+    if (e != ce) {
       addConstraintInternal(e); // enable further reductions
       changed = true;
     } else {
@@ -95,13 +94,12 @@ ref<Expr> ConstraintManager::simplifyExpr(const ConstraintSet &constraints,
   if (isa<ConstantExpr>(e))
     return e;
 
-  std::map< ref<Expr>, ref<Expr> > equalities;
+  std::map<ref<Expr>, ref<Expr>> equalities;
 
   for (auto &constraint : constraints) {
     if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
       if (isa<ConstantExpr>(ee->left)) {
-        equalities.insert(std::make_pair(ee->right,
-                                         ee->left));
+        equalities.insert(std::make_pair(ee->right, ee->left));
       } else {
         equalities.insert(
             std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool)));
@@ -141,8 +139,8 @@ void ConstraintManager::addConstraintInternal(const ref<Expr> &e) {
       // (byte-constant comparison).
       BinaryExpr *be = cast<BinaryExpr>(e);
       if (isa<ConstantExpr>(be->left)) {
-	ExprReplaceVisitor visitor(be->right, be->left);
-	rewriteConstraints(visitor);
+        ExprReplaceVisitor visitor(be->right, be->left);
+        rewriteConstraints(visitor);
       }
     }
     constraints.push_back(e);