In-process Z3 interface

CMakeLists.txt

@@ -218,6 +218,12 @@ set(SOUPER_INFER_FILES
   include/souper/Infer/Interpreter.h
   lib/Infer/Preconditions.cpp
   include/souper/Infer/Preconditions.h
+  lib/Infer/Z3Expr.cpp
+  include/souper/Infer/Z3Expr.h
+  lib/Infer/Z3Driver.cpp
+  include/souper/Infer/Z3Driver.h
+  lib/Infer/Verification.cpp
+  include/souper/Infer/Verification.h
 )
 
 add_library(souperInfer STATIC

include/souper/Extractor/ExprBuilder.h

@@ -58,7 +58,13 @@ class ExprBuilder {
 
   Inst *getDataflowConditions(Inst *I);
   Inst *getUBInstCondition(Inst *Root);
-
+  Inst *GetCandidateExprForReplacement(
+         const BlockPCs &BPCs, const std::vector<InstMapping> &PCs,
+         InstMapping Mapping, Inst *Precondition, bool Negate, bool DropUB);
+  void setBlockPCMap(const BlockPCs &BPCs);
+  Inst *getBlockPCs(Inst *Root);
+  std::vector<Inst *> getVarInsts(const std::vector<Inst *> Insts);
+  Inst *getImpliesInst(Inst *Ante, Inst *I);
 protected:
   InstContext *LIC;
 
@@ -77,14 +83,10 @@ class ExprBuilder {
                               std::map<Inst *, bool> *SelectBranches,
                               UBPathInstMap &CachedUBPathInsts);
 
-  void setBlockPCMap(const BlockPCs &BPCs);
-
-  Inst *getBlockPCs(Inst *Root);
   std::map<Inst *, Inst *> getUBInstConstraints(Inst *Root);
   std::vector<Inst *> getUBPathInsts(Inst *Root);
-  std::vector<Inst *> getVarInsts(const std::vector<Inst *> Insts);
+
   Inst *getExtractInst(Inst *I, unsigned Offset, unsigned W);
-  Inst *getImpliesInst(Inst *Ante, Inst *I);
 
   Inst *addnswUB(Inst *I);
   Inst *addnuwUB(Inst *I);
@@ -102,9 +104,7 @@ class ExprBuilder {
   Inst *lshrExactUB(Inst *I);
   Inst *ashrExactUB(Inst *I);
 
-  Inst *GetCandidateExprForReplacement(
-         const BlockPCs &BPCs, const std::vector<InstMapping> &PCs,
-         InstMapping Mapping, Inst *Precondition, bool Negate, bool DropUB);
+
 };
 
 std::string BuildQuery(InstContext &IC, const BlockPCs &BPCs,

include/souper/Infer/ConstantSynthesis.h

@@ -32,17 +32,32 @@ class ConstantSynthesis {
   ConstantSynthesis(PruningManager *P = nullptr) : Pruner(P) {}
 
   // Synthesize a set of constants from the specification in LHS
-  std::error_code synthesize(SMTLIBSolver *SMTSolver,
+  virtual std::error_code synthesize(SMTLIBSolver *SMTSolver,
                              const BlockPCs &BPCs,
                              const std::vector<InstMapping> &PCs,
                              InstMapping Mapping, std::set <Inst *> &ConstSet,
                              std::map <Inst *, llvm::APInt> &ResultMap,
                              InstContext &IC, unsigned MaxTries, unsigned Timeout,
                              bool AvoidNops);
 
-private:
+protected:
   PruningManager *Pruner = nullptr;
 };
+
+class ConstantSynthesisZ3 : public ConstantSynthesis {
+public:
+  ConstantSynthesisZ3(PruningManager *P = nullptr) : ConstantSynthesis(P) {}
+
+  std::error_code synthesize(SMTLIBSolver *SMTSolver,
+                             const BlockPCs &BPCs,
+                             const std::vector<InstMapping> &PCs,
+                             InstMapping Mapping, std::set <Inst *> &ConstSet,
+                             std::map <Inst *, llvm::APInt> &ResultMap,
+                             InstContext &IC, unsigned MaxTries, unsigned Timeout,
+                             bool AvoidNops) override;
+
+};
+
 }
 
 #endif  // SOUPER_CONSTANT_SYNTHESIS_H

include/souper/Infer/Verification.h

@@ -0,0 +1,52 @@
+#ifndef SOUPER_INFER_VERIFICATION_H
+#define SOUPER_INFER_VERIFICATION_H
+#include "souper/Inst/Inst.h"
+
+namespace souper {
+
+struct RefinementProblem {
+  souper::Inst *LHS;
+  souper::Inst *RHS;
+  souper::Inst *Pre;
+  BlockPCs BPCs;
+
+  RefinementProblem ReplacePhi(souper::InstContext &IC, std::map<Block *, size_t> &Change);
+
+  bool operator == (const RefinementProblem &P) const {
+    if (LHS == P.LHS && RHS == P.RHS &&
+        Pre == P.Pre && BPCs.size() == P.BPCs.size()) {
+      for (size_t i = 0; i < BPCs.size(); ++i) {
+        if (BPCs[i].B != P.BPCs[i].B ||
+            BPCs[i].PC.LHS != P.BPCs[i].PC.LHS ||
+            BPCs[i].PC.RHS != P.BPCs[i].PC.RHS) {
+          return false;
+        }
+      }
+      return true;
+    } else {
+      return false;
+    }
+  }
+  struct Hash
+  {
+    std::size_t operator()(const RefinementProblem &P) const
+    {
+      return std::hash<Inst *>()(P.LHS)
+             ^ std::hash<Inst *>()(P.RHS) << 1
+             ^ std::hash<Inst *>()(P.Pre) << 2
+             ^ std::hash<size_t>()(P.BPCs.size());
+    }
+  };
+
+};
+
+void collectPhis(souper::Inst *I,
+                 std::map<souper::Block *, std::set<souper::Inst *>> &Phis);
+
+std::unordered_set<RefinementProblem, RefinementProblem::Hash>
+  explodePhis(InstContext &IC, RefinementProblem P);
+
+Inst *getDataflowConditions(const Inst *I, InstContext &IC);
+
+}
+#endif