DEP: Wp interpolant, fix function calls

include/klee/CommandLine.h

@@ -98,6 +98,8 @@ extern llvm::cl::opt<bool> TracerXPointerError;
 
 extern llvm::cl::opt<bool> EmitAllErrorsInSamePath;
 
+extern llvm::cl::opt<bool> WPInterpolant;
+
 #endif
 
 #ifdef ENABLE_METASMT

include/klee/Expr.h

@@ -19,6 +19,12 @@
 #include "llvm/ADT/SmallVector.h"
 #include "llvm/Support/raw_ostream.h"
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
+#include <llvm/IR/Value.h>
+#else
+#include <llvm/Value.h>
+#endif
+
 #include <sstream>
 #include <set>
 #include <vector>
@@ -161,6 +167,9 @@ class Expr {
     Sge, ///< Not used in canonical form
     Exists,
     LastKind = Exists,
+    WPVar, // Expressions for WP Interpolation
+    Upd,   // Array Update
+    Sel,   // Array Select
     CastKindFirst = ZExt,
     CastKindLast = SExt,
     BinaryKindFirst = Add,
@@ -413,6 +422,149 @@ class ExistsExpr : public NonConstantExpr {
       : variables(variables), body(body) {}
 };
 
+/// Class representing a WP variable
+class WPVarExpr : public NonConstantExpr {
+public:
+  llvm::Value *address;
+  std::string name;
+  ref<Expr> index;
+
+public:
+  static ref<Expr> alloc(llvm::Value *_address, std::string _name,
+                         const ref<Expr> &_index) {
+    ref<Expr> r(new WPVarExpr(_address, _name, _index));
+    r->computeHash();
+    return r;
+  }
+
+  static ref<Expr> create(llvm::Value *address, std::string name,
+                          ref<Expr> index);
+
+  Width getWidth() const { return index->getWidth(); }
+  Kind getKind() const { return WPVar; }
+
+  unsigned getNumKids() const { return 1; }
+  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }
+
+  std::string getName() const { return name; }
+
+  llvm::Value *getAddress() const { return address; }
+
+  int compareContents(const Expr &b) const;
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
+    return create(address, name, kids[0]);
+  }
+
+  void print(llvm::raw_ostream &os) const;
+
+  virtual unsigned computeHash();
+
+private:
+  WPVarExpr(llvm::Value *_address, std::string _name, const ref<Expr> &_index)
+      : address(_address), name(_name) {
+    index = _index;
+  }
+
+public:
+  static bool classof(const Expr *E) { return E->getKind() == Expr::WPVar; }
+  static bool classof(const WPVarExpr *) { return true; }
+};
+
+/// Class representing the update operation in array theory
+class UpdExpr : public NonConstantExpr {
+public:
+  ref<Expr> array;
+  ref<Expr> index;
+  ref<Expr> value;
+
+public:
+  static ref<Expr> alloc(const ref<Expr> &_array, const ref<Expr> &_index,
+                         const ref<Expr> &_value) {
+    ref<Expr> r(new UpdExpr(_array, _index, _value));
+    r->computeHash();
+    return r;
+  }
+
+  static ref<Expr> create(ref<Expr> array, ref<Expr> index, ref<Expr> update);
+
+  Width getWidth() const { return array->getWidth(); }
+  Kind getKind() const { return Upd; }
+
+  unsigned getNumKids() const { return 3; }
+  ref<Expr> getKid(unsigned i) const {
+    if (i == 2)
+      return value;
+    else if (i == 1)
+      return index;
+    else
+      return array;
+  }
+
+  int compareContents(const Expr &b) const;
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
+    return create(kids[0], kids[1], kids[2]);
+  }
+
+  void print(llvm::raw_ostream &os) const;
+
+  virtual unsigned computeHash();
+
+private:
+  UpdExpr(const ref<Expr> &_array, const ref<Expr> &_index,
+          const ref<Expr> &_value)
+      : array(_array) {
+    index = _index;
+    value = _value;
+  }
+
+public:
+  static bool classof(const Expr *E) { return E->getKind() == Expr::Upd; }
+  static bool classof(const UpdExpr *) { return true; }
+};
+
+/// Class representing the select operation in array theory
+class SelExpr : public NonConstantExpr {
+public:
+  ref<Expr> array;
+  ref<Expr> index;
+
+public:
+  static ref<Expr> alloc(const ref<Expr> &_array, const ref<Expr> &_index) {
+    ref<Expr> r(new SelExpr(_array, _index));
+    r->computeHash();
+    return r;
+  }
+
+  static ref<Expr> create(ref<Expr> array, ref<Expr> index);
+
+  Width getWidth() const { return array->getWidth(); }
+  Kind getKind() const { return Sel; }
+
+  unsigned getNumKids() const { return 2; }
+  ref<Expr> getKid(unsigned i) const { return i ? index : array; }
+
+  int compareContents(const Expr &b) const;
+
+  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
+    return create(kids[0], kids[1]);
+  }
+
+  void print(llvm::raw_ostream &os) const;
+
+  virtual unsigned computeHash();
+
+private:
+  SelExpr(const ref<Expr> &_array, const ref<Expr> &_index) : array(_array) {
+    index = _index;
+  }
+
+public:
+  static bool classof(const Expr *E) { return E->getKind() == Expr::Sel; }
+  static bool classof(const SelExpr *) { return true; }
+};
+
 // Special
 
 class NotOptimizedExpr : public NonConstantExpr {
@@ -588,7 +740,13 @@ class ReadExpr : public NonConstantExpr {
 
   unsigned getNumKids() const { return numKids; }
   ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }
-
+
+  std::string getName() const { return updates.root->name; }
+
+  const Array *getArray() const { return updates.root; }
+
+  void replaceArray(const Array *arr) { updates.root = arr; }
+
   int compareContents(const Expr &b) const;
 
   virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
@@ -608,7 +766,6 @@ class ReadExpr : public NonConstantExpr {
   static bool classof(const ReadExpr *) { return true; }
 };
 
-
 /// Class representing an if-then-else expression.
 class SelectExpr : public NonConstantExpr {
 public:

include/klee/util/ExprVisitor.h

@@ -80,6 +80,8 @@ namespace klee {
     virtual Action visitSgt(const SgtExpr&);
     virtual Action visitSge(const SgeExpr&);
     virtual Action visitExists(const ExistsExpr&);
+    virtual Action visitSel(const SelExpr &);
+    virtual Action visitUpd(const UpdExpr &);
 
   private:
     typedef ExprHashMap< ref<Expr> > visited_ty;

lib/Basic/CmdLineOptions.cpp

@@ -174,6 +174,11 @@ llvm::cl::opt<bool> TracerXPointerError(
     llvm::cl::desc("Enables detection of more memory errors by interpolation "
                    "shadow memory (may be false positives)."),
     llvm::cl::init(false));
+
+llvm::cl::opt<bool>
+    WPInterpolant("wp-interpolant",
+                  llvm::cl::desc("Perform weakest-precondition interpolation"),
+                  llvm::cl::init(false));
 #endif // ENABLE_Z3
 
 #ifdef ENABLE_METASMT

lib/Core/Executor.cpp

@@ -897,6 +897,8 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       // We then extract the unsatisfiability core of antecedent and not
       // consequent as the Craig interpolant.
       txTree->markPathCondition(current, unsatCore);
+      if (WPInterpolant)
+        txTree->markInstruction(current.prevPC, true);
     }
 
     return StatePair(&current, 0);
@@ -912,6 +914,8 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
       // which means that antecedent -> not(consequent) is valid. In this
       // case also we extract the unsat core of the proof
       txTree->markPathCondition(current, unsatCore);
+      if (WPInterpolant)
+        txTree->markInstruction(current.prevPC, false);
     }
 
     return StatePair(0, &current);
@@ -1509,7 +1513,6 @@ void Executor::processBBCoverage(int BBCoverage, llvm::BasicBlock *bb) {
                             << allBlockCount << "," << percent << "]\n";
       livePercentCovFileOut.close();
     }
-
     // print live BB
     if (BBCoverage >= 3 && isNew) {
       std::string liveBBFile =
@@ -1608,6 +1611,9 @@ static inline const llvm::fltSemantics *fpWidthToSemantics(unsigned width) {
 void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   Instruction *i = ki->inst;
 
+  if (INTERPOLATION_ENABLED && WPInterpolant)
+    txTree->storeInstruction(ki, state.incomingBBIndex);
+
   switch (i->getOpcode()) {
   // Control flow
   case Instruction::Ret: {
@@ -2909,7 +2915,7 @@ void Executor::updateStates(ExecutionState *current) {
       seedMap.erase(it3);
     processTree->remove(es->ptreeNode);
     if (INTERPOLATION_ENABLED)
-      txTree->remove(es->txTreeNode, (current == 0));
+      txTree->remove(es, solver, (current == 0));
     delete es;
   }
   removedStates.clear();
@@ -3027,7 +3033,6 @@ void Executor::doDumpStates() {
 }
 
 void Executor::run(ExecutionState &initialState) {
-
   startingBBPlottingTime = time(0);
   // get interested source code
   size_t lastindex = InputFile.find_last_of(".");
@@ -3068,6 +3073,7 @@ void Executor::run(ExecutionState &initialState) {
           fBBOrder[firstBB->getParent()].end()) {
     processBBCoverage(BBCoverage, ki->inst->getParent());
   }
+
   bindModuleConstants();
 
   // Delay init till now so that ticks don't accrue during
@@ -3293,7 +3299,7 @@ void Executor::terminateState(ExecutionState &state) {
     processTree->remove(state.ptreeNode);
 
     if (INTERPOLATION_ENABLED)
-      txTree->remove(state.txTreeNode, false);
+      txTree->remove(&state, solver, false);
     delete &state;
   }
 }
@@ -3430,6 +3436,8 @@ void Executor::terminateStateOnError(ExecutionState &state,
       state.txTreeNode->setGenericEarlyTermination();
       TxTreeGraph::setError(state, TxTreeGraph::GENERIC);
     }
+    if (WPInterpolant)
+      state.txTreeNode->setAssertionFail(EmitAllErrors);
   }
 
   std::string message = messaget.str();

lib/Core/Executor.h

@@ -22,6 +22,7 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/util/ArrayCache.h"
 #include "llvm/Support/raw_ostream.h"
+
 #include "llvm/IR/Function.h"
 #include "llvm/ADT/Twine.h"