WP propagate to support bb-unmerge

lib/Core/Executor.cpp

@@ -1477,8 +1477,9 @@ Executor::StatePair Executor::branchFork(ExecutionState &current,
     }
 
     if (INTERPOLATION_ENABLED) {
-      if(BBUnmerge)
-        current.txTreeNode = txTree->splitSingle(current.txTreeNode, &current);
+      if(BBUnmerge) {
+        current.txTreeNode = txTree->splitSingle(current.txTreeNode, &current, true);
+      }
       // Validity proof succeeded of a query: antecedent -> consequent.
       // We then extract the unsatisfiability core of antecedent and not
       // consequent as the Craig interpolant.
@@ -1593,8 +1594,9 @@ Executor::StatePair Executor::branchFork(ExecutionState &current,
     }
 
     if (INTERPOLATION_ENABLED) {
-      if(BBUnmerge)
-        current.txTreeNode = txTree->splitSingle(current.txTreeNode, &current);
+      if(BBUnmerge) {
+        current.txTreeNode = txTree->splitSingle(current.txTreeNode, &current, false);
+      }
       // Falsity proof succeeded of a query: antecedent -> consequent,
       // which means that antecedent -> not(consequent) is valid. In this
       // case also we extract the unsat core of the proof
@@ -3046,8 +3048,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       txTree->setPhiValuesFlag(0);
     if (bi->isUnconditional()) {
       if(INTERPOLATION_ENABLED) {
-        if(BBUnmerge)
-          state.txTreeNode = txTree->splitSingle(state.txTreeNode, &state);
+        if(BBUnmerge) {
+          state.txTreeNode = txTree->splitSingle(state.txTreeNode, &state, false);
+        }
       }
       transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
       if (INTERPOLATION_ENABLED)

lib/Core/TxTree.cpp

@@ -2473,8 +2473,11 @@ void TxTree::remove(ExecutionState *state, TimingSolver *solver, bool dumping) {
 #endif
 }
 
-TxTreeNode * TxTree::splitSingle(TxTreeNode *parent, ExecutionState *newState) {
+TxTreeNode * TxTree::splitSingle(TxTreeNode *parent, ExecutionState *newState, const bool splitCond) {
   TimerStatIncrementer t(splitTime);
+  if(WPInterpolant) {
+    parent->singleSplitWPCond = splitCond ? parent->wp->True() : parent->wp->False();
+  }
   TxTreeNode *const ret = parent->createChild<&TxTreeNode::left>();
   newState->txTreeNode = ret;
   TxTreeGraph::addChildren(parent, parent->left, parent->left);
@@ -2793,8 +2796,12 @@ ref<Expr> TxTreeNode::generateWPInterpolant() {
     llvm::Instruction *i = reverseInstructionList.back().first->inst;
     if (i->getOpcode() == llvm::Instruction::Br) {
       llvm::BranchInst *br = dyn_cast<llvm::BranchInst>(i);
-      if (br->isConditional()) {
+      if (br->isConditional() && singleSplitWPCond.isNull()) {
         branchCondition = wp->getBrCondition(i);
+      } else {
+        // Branch is unconditional
+        assert(!singleSplitWPCond.isNull());
+        branchCondition = singleSplitWPCond;
       }
     }
     if (!branchCondition.isNull()) {

lib/Core/TxTree.h

@@ -455,6 +455,7 @@ class TxTreeNode {
   // \brief Set if the speculation has failed and the node should be removed
   bool speculationFailed;
 
+  ref<Expr> singleSplitWPCond;
   // \brief Instance of weakest precondition class used to generate WP
   // interpolant
   TxWeakestPreCondition *wp;
@@ -1004,7 +1005,7 @@ class TxTree {
   void markPathConditionWithBrInst(llvm::BranchInst *binst,
                                    std::vector<ref<Expr> > &unsatCore);
 
-  TxTreeNode * splitSingle(TxTreeNode *parent, ExecutionState *newState);
+  TxTreeNode * splitSingle(TxTreeNode *parent, ExecutionState *newState, bool splitCond);
 
   /// \brief Creates fresh interpolation data holder for the two given KLEE
   /// execution states.

lib/Core/TxWP.cpp

@@ -400,7 +400,9 @@ ref<Expr> TxWeakestPreCondition::PushUp(
     if (flag == 1) {
       // 1- call getCondition on the cond argument of the branch instruction
       // 2- create and expression from the condition and this->WPExpr
-      ref<Expr> result = getBrCondition(i);
+      const auto br = dyn_cast<llvm::BranchInst>(i);
+      assert(br);
+      ref<Expr> result = br->isConditional() ? getBrCondition(i) : True();
       if (result.isNull()) {
         WPExpr = result;
         return WPExpr;
@@ -428,7 +430,9 @@ ref<Expr> TxWeakestPreCondition::PushUp(
       // 1- call getCondition on the cond argument of the branch instruction
       // 2- generate not(condition): expr::not(condition)
       // 3- create and expression from the condition and this->WPExpr
-      ref<Expr> result = getBrCondition(i);
+      const auto br = dyn_cast<llvm::BranchInst>(i);
+      assert(br);
+      ref<Expr> result = br->isConditional() ? getBrCondition(i) : False();
       // llvm::outs()<<"\nThe result from the flag
       // 2::::::::::::::::::::::::::::\n"<<result;
       // llvm::outs()<<"\n\n";