doc

README.md

@@ -1,2 +0,0 @@
-# SQA-Homework
-

dse/.idea/.gitignore

@@ -0,0 +1,8 @@
+# Default ignored files
+/shelf/
+/workspace.xml
+# Editor-based HTTP Client requests
+/httpRequests/
+# Datasource local storage ignored files
+/dataSources/
+/dataSources.local.xml

dse/.idea/dse.iml

@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module classpath="CMake" type="CPP_MODULE" version="4" />

dse/.idea/misc.xml

@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="CMakeWorkspace" PROJECT_DIR="$PROJECT_DIR$" />
+</project>

dse/.idea/modules.xml

@@ -0,0 +1,8 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project version="4">
+  <component name="ProjectModuleManager">
+    <modules>
+      <module fileurl="file://$PROJECT_DIR$/.idea/dse.iml" filepath="$PROJECT_DIR$/.idea/dse.iml" />
+    </modules>
+  </component>
+</project>

dse/CMakeLists.txt

@@ -0,0 +1,39 @@
+cmake_minimum_required(VERSION 3.10)
+
+find_package(LLVM 14 REQUIRED CONFIG)
+list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
+include(HandleLLVMOptions)
+include(AddLLVM)
+
+message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}")
+
+set(Z3_DIR $ENV{Z3_DIR})
+get_filename_component(Z3_DIR ${Z3_DIR} ABSOLUTE)
+set(Z3_CXX_INCLUDE_DIRS ${Z3_DIR}/include)
+set(Z3_LIBRARIES ${Z3_DIR}/lib/libz3.so)
+message(STATUS "Z3_DIR: ${Z3_DIR}")
+
+add_definitions(${LLVM_DEFINITIONS})
+include_directories(${LLVM_INCLUDE_DIRS} include)
+include_directories(${Z3_CXX_INCLUDE_DIRS})
+link_directories(${LLVM_LIBRARY_DIRS} ${CMAKE_CURRENT_BINARY_DIR} ${Z3_LIBRARIES})
+
+add_executable(dse
+  src/DSE.cpp
+  src/Strategy.cpp
+  )
+
+add_llvm_library(InstrumentPass MODULE
+  src/Instrument.cpp
+  )
+
+llvm_map_components_to_libnames(llvm_libs support core irreader)
+
+target_link_libraries(dse ${llvm_libs} ${Z3_LIBRARIES})
+
+add_library(runtime MODULE
+  src/SymbolicInterpreter.cpp
+  src/Runtime.cpp
+  )
+
+target_link_libraries(runtime ${llvm_libs} ${Z3_LIBRARIES})

dse/include/Instrument.h

@@ -0,0 +1,73 @@
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Function.h"
+#include "llvm/IR/IRBuilder.h"
+#include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Module.h"
+#include "llvm/Pass.h"
+#include <map>
+
+using namespace llvm;
+
+namespace instrument {
+#define RET         1
+#define BR          2
+#define ADD         13      ///    +
+#define SUB         15      ///    -
+#define MUL         17      ///    *
+#define SDIV        20      ///    /
+#define SREM        23      ///    %
+#define ALLOCA      31
+#define LOAD        32
+#define STORE       33
+#define ICMP        53
+#define CALL        56
+
+#define DSE_Init        "__DSE_Init__"
+#define DSE_Alloca      "__DSE_Alloca__"
+#define DSE_Store       "__DSE_Store__"
+#define DSE_Load        "__DSE_Load__"
+#define DSE_ICmp        "__DSE_ICmp__"
+#define DSE_Label       "__DSE_Label__"
+#define DSE_Loop        "__DSE_Loop__"
+#define DSE_BinOP       "__DSE_BinOp__"
+#define DSE_Branch      "__DSE_Branch__"
+#define DSE_Const       "__DSE_Const__"
+#define DSE_Register    "__DSE_Register__"
+
+
+int RegisterID = 0;
+std::map<Value *, int> RegisterMap;
+int BranchID = 0;
+std::map<Value *, int> BranchMap;
+
+int getRegisterID(Value *I) {
+  /// 找当前地址的ID，没有则分配一个
+  if (RegisterMap.find(I) == RegisterMap.end()) {
+    /// 为地址 *I 分配一个 ID
+    RegisterMap[I] = RegisterID;
+    return RegisterID++;
+  } else {
+    return RegisterMap[I];
+  }
+}
+
+int getBranchID(Value *I) {
+  if (BranchMap.find(I) == BranchMap.end()) {
+    BranchMap[I] = BranchID;
+    return BranchID++;
+  } else {
+    return BranchMap[I];
+  }
+}
+
+/// 插桩，详细可以看官网文档
+/// https://releases.llvm.org/14.0.0/docs/WritingAnLLVMPass.html
+struct Instrument : public FunctionPass {
+  static char ID;
+  static const char *checkFunctionName;
+
+  Instrument() : FunctionPass(ID) {}
+
+  bool runOnFunction(Function &F) override;
+};
+} // namespace instrument

dse/include/Runtime.h

@@ -0,0 +1,3 @@
+void __DSE_Input__(int *x, int ID);
+
+#define DSE_Input(x) __DSE_Input__(&x, __COUNTER__)

dse/include/Strategy.h

@@ -0,0 +1,4 @@
+#include "z3++.h"
+
+void recordBranches(z3::expr_vector &OldVec);
+void searchStrategy(z3::expr_vector &OldVec);

dse/include/SymbolicInterpreter.h

@@ -0,0 +1,62 @@
+#ifndef SYMBOLIC_INTERPRETER_H
+#define SYMBOLIC_INTERPRETER_H
+
+#include <cstdlib>
+#include <map>
+#include <stack>
+#include <vector>
+
+#include "z3++.h"
+
+/// 结果输出目录
+static const char *FormulaFile = "formula.smt2";
+/// 输入读取目录
+static const char *InputFile = "input.txt";
+/// 日志：记录 Path Condition
+static const char *LogFile = "log.txt";
+/// 目前不清楚
+static const char *BranchFile = "branch.txt";
+
+class Address {
+public:
+  enum Ty { Memory, Register };
+  Address(int *Ptr) : Type(Memory), Addr((uintptr_t)Ptr) {}
+  Address(int ID) : Type(Register), Addr(ID) {}
+  Address(z3::expr &R)
+      : Type(Register), Addr(std::stoi(R.to_string().substr(1))) {}
+
+  bool operator<(const Address &RHS) const {
+    return (Type < RHS.Type) || (Type == RHS.Type && Addr < RHS.Addr);
+  }
+  friend std::ostream &operator<<(std::ostream &OS, const Address &SE);
+
+private:
+  Ty Type;
+  uintptr_t Addr;
+};
+
+using MemoryTy = std::map<Address, z3::expr>;
+
+class SymbolicInterpreter {
+public:
+  int NewInput(int *Ptr, int ID);
+  MemoryTy &getMemory() { return Mem; }
+  std::map<int, int> &getInputs() { return Inputs; }
+  z3::context &getContext() { return Ctx; }
+  std::stack<z3::expr> &getStack() { return Stack; }
+  std::vector<std::pair<int, z3::expr>> &getPathCondition() {
+    return PathCondition;
+  }
+
+private:
+  MemoryTy Mem;
+  /// Inputs: <RegisteredId, Value>
+  std::map<int, int> Inputs;
+  int NumOfInputs = 0;
+  std::stack<z3::expr> Stack;
+  std::vector<std::pair<int, z3::expr>> PathCondition;
+
+  z3::context Ctx;
+};
+
+#endif // SYMBOLIC_INTERPRETER_H

dse/src/DSE.cpp

@@ -0,0 +1,112 @@
+#include <fstream>
+#include <iostream>
+#include <sys/stat.h>
+#include <unistd.h>
+#include <vector>
+#include "z3++.h"
+
+#include "Strategy.h"
+#include "SymbolicInterpreter.h"
+
+z3::context Ctx;
+z3::solver Solver(Ctx);
+
+void storeInput() {
+  /// sat 结果写入到 "input.txt" 作为下一次输入
+  std::ofstream OS(InputFile);
+  z3::model Model = Solver.get_model();
+  for (int I = 0; I < Model.size(); I++) {
+    const z3::func_decl E = Model[I];
+    z3::expr Input = Model.get_const_interp(E);
+    if (Input.kind() == Z3_NUMERAL_AST) {
+      int res = Input.get_numeral_int();
+      OS << E.name() << "," << res << std::endl;
+    }
+  }
+}
+
+void printNewPathCondition(z3::expr_vector &Vec) {
+  std::ofstream Log;
+  /// 将路径条件写入到 “log.txt”
+  Log.open(LogFile, std::ofstream::out | std::ofstream::app);
+  Log << std::endl;
+  Log << "=== New Path Condition ===" << std::endl;
+  for (auto E : Vec) {
+    Log << E << std::endl;
+  }
+}
+
+/// 产生输入
+void generateInput() {
+  /// 获取 formula.smt2 中的内容
+  z3::expr_vector Vec = Ctx.parse_file(FormulaFile);
+    recordBranches(Vec);
+    //std::cout<<"Vec: "<<Vec.size()<<std::endl;
+  while (true) {
+    /// 搜索策略（需要自己编写）
+    searchStrategy(Vec);
+    Solver.reset();
+    /// Vec 格式:
+    for (const auto &E : Vec) {
+      Solver.add(E);
+    }
+    /// z3 求解器求解结果
+    z3::check_result Result = Solver.check();
+    /// 如果 sat
+    if (Result == z3::sat) {
+      /// 保存结果
+      storeInput();
+      /// 打印新的表达式，也就是这一次求解的表达式
+      printNewPathCondition(Vec);
+      break;
+    }
+  }
+}
+
+int main(int argc, char **argv) {
+  if (argc < 2) {
+    std::cerr << "Expected an argument - executable file name" << std::endl;
+    return 1;
+  }
+
+  struct stat Buffer;
+  if (stat(argv[1], &Buffer)) {
+    std::cerr << argv[1] << " not found\n" << std::endl;
+    return 1;
+  }
+
+  int MaxIter = INT_MAX;
+  if (argc == 3) {
+    /// 执行次数 argv[2]:
+    /// ../build/dse ./simple0 1 -> MaxIter = 1
+    MaxIter = atoi(argv[2]);
+  }
+
+  int Iter = 0;
+  while (Iter < MaxIter) {
+    /**
+     * 执行命令  argv[1]
+     * ../build/dse ./simple0 1 -> ./simple0
+     * 如果程序中没有 DSE_Input，那么后续的 generateInput() 将不会产生 Vec
+     * 也就是 z3::expr_vector Vec = Ctx.parse_file(FormulaFile) 为空
+     * 如果有 DSE_Input，就会产生一些列反应
+     */
+    int Ret = std::system(argv[1]);
+    /// 程序运行没有发生错误 -> Ret = 0
+    /// 程序运行发生错误，如除 0 错： -> Ret = 35584 != 0
+    if (Ret) {
+      std::cout << "Crashing input found (" << Iter << " iters)" << std::endl;
+      break;
+    }
+    /// stat: 获取文件信息，文件属性存放在结构体 stat 里
+    if (stat(FormulaFile, &Buffer)) {
+        /// 没有创建 formula.smt2
+      std::cerr << FormulaFile << " not found" << std::endl;
+      return 1;
+    }
+    /// 产生输入
+    generateInput();
+    /// 下次迭代
+    Iter++;
+  }
+}

dse/src/Instrument.cpp

@@ -0,0 +1,231 @@
+#include "Instrument.h"
+
+using namespace llvm;
+
+namespace instrument {
+
+
+
+/**
+ * Implement your instrumentation for dynamic symbolic execution engine
+ */
+bool Instrument::runOnFunction(Function &F) {
+    if(F.getName()!="main"){
+        return false;
+    }
+    LLVMContext &context = F.getParent()->getContext();
+    /// __DSE_Init__
+    auto *FuncInitType = FunctionType::get(Type::getVoidTy(context),
+                                           {},
+                                           false);
+    auto FuncInit = F.getParent()->getOrInsertFunction(DSE_Init, FuncInitType);
+
+    /// __DSE_Alloca__
+    auto *FuncAllocaType = FunctionType::get(Type::getVoidTy(context),
+                                             {Type::getInt32Ty(context),Type::getInt32PtrTy(context)},
+                                             false);
+    auto FuncAlloca = F.getParent()->getOrInsertFunction(DSE_Alloca, FuncAllocaType);
+
+    /// __DSE_Store__
+    auto *FuncStoreType= FunctionType::get(Type::getVoidTy(context),
+                                          {Type::getInt32PtrTy(context)},
+                                          false);
+    auto FuncStore = F.getParent()->getOrInsertFunction(DSE_Store, FuncStoreType);
+
+    /// __DSE_Load__
+    auto *FuncLoadType = FunctionType::get(Type::getVoidTy(context),
+                                           {Type::getInt32Ty(context),Type::getInt32PtrTy(context)},
+                                           false);
+    auto FuncLoad = F.getParent()->getOrInsertFunction(DSE_Load, FuncLoadType);
+
+    /// __DSE_ICmp__
+    auto *FuncICmpType = FunctionType::get(Type::getVoidTy(context),
+                                           {Type::getInt32Ty(context),Type::getInt32Ty(context)},
+                                           false);
+    auto FuncICmp = F.getParent()->getOrInsertFunction(DSE_ICmp, FuncICmpType);
+
+    /// __DSE_Label__
+    auto *FuncLabelType = FunctionType::get(Type::getVoidTy(context),
+                                            {Type::getInt32Ty(context),
+                                             Type::getInt32Ty(context),Type::getInt32Ty(context)},
+                                            false);
+    auto FuncLabel = F.getParent()->getOrInsertFunction(DSE_Label, FuncLabelType);
+
+    /// __DSE_Loop__
+    auto *FuncLoopType = FunctionType::get(Type::getVoidTy(context),
+                                           {Type::getInt32Ty(context)},
+                                           false);
+    auto FuncLoop = F.getParent()->getOrInsertFunction(DSE_Loop, FuncLoopType);
+
+    /// __DSE_Branch__
+    auto *FuncBranchType = FunctionType::get(Type::getVoidTy(context),
+                                             {Type::getInt32Ty(context),Type::getInt32Ty(context)},
+                                             false);
+    auto FuncBranch = F.getParent()->getOrInsertFunction(DSE_Branch, FuncBranchType);
+
+    /// __DSE_BinOp__
+    auto *FuncBinOpType = FunctionType::get(Type::getVoidTy(context),
+                                            {Type::getInt32Ty(context),Type::getInt32Ty(context)},
+                                            false);
+    auto FuncBinOp = F.getParent()->getOrInsertFunction(DSE_BinOP, FuncBinOpType);
+
+    /// __DSE_Const__
+    auto *FuncConstType = FunctionType::get(Type::getVoidTy(context),
+                                            {Type::getInt32Ty(context)},
+                                            false);
+    auto FuncConst = F.getParent()->getOrInsertFunction(DSE_Const,FuncConstType);
+
+    /// __DSE_Register__
+    auto *FuncRegisterType = FunctionType::get(Type::getVoidTy(context),
+                                               {Type::getInt32Ty(context)},
+                                               false);
+    auto FuncRegister = F.getParent()->getOrInsertFunction(DSE_Register, FuncRegisterType);
+
+     for(auto & B : F){
+         if(B.getName().startswith("if") || B.getName().startswith("land.lhs") || B.getName().startswith("for")){
+             CallInst::Create(FuncBranch,
+                              {ConstantInt::get(Type::getInt32Ty(context), getRegisterID(&B)),
+                               ConstantInt::get(Type::getInt32Ty(context), BranchID++)})
+                              ->insertBefore(&B.front());
+         }
+         //errs() << "hello" <<  B.getName() << " " <<getRegisterID(&B) << '\n';
+         for(auto &bb : B){
+             auto bbName = bb.getName();
+             //errs() << bbName << ":"<< getRegisterID(&bb) << '\n';
+             if(bbName == "retval"){
+                 CallInst::Create(FuncInit)
+                                  ->insertBefore(&bb);
+                 continue;
+             }
+             //errs() << bb.getOpcodeName() << ":"<< bb.getOpcode()<< '\n';
+             switch (bb.getOpcode()) {
+                 case RET:
+                     break;
+                 case BR:
+                     if(dyn_cast<BranchInst>(&bb)->isConditional()){
+                         //errs() << getRegisterID(bb.getOperand(2)) <<" "<< getBranchID(bb.getOperand(1))<<'\n';
+                         CallInst::Create(FuncLabel,
+                                          {ConstantInt::get(Type::getInt32Ty(context),
+                                                            getRegisterID(bb.getOperand(0))),
+                                                ConstantInt::get(Type::getInt32Ty(context),
+                                                            getRegisterID(bb.getOperand(2))),
+                                                ConstantInt::get(Type::getInt32Ty(context),1)})
+                                                ->insertBefore(&bb);
+                         CallInst::Create(FuncLabel,
+                                          {ConstantInt::get(Type::getInt32Ty(context),
+                                                            getRegisterID(bb.getOperand(0))),
+                                                ConstantInt::get(Type::getInt32Ty(context),
+                                                            getRegisterID(bb.getOperand(1))),
+                                                ConstantInt::get(Type::getInt32Ty(context),0)})
+                                                ->insertBefore(&bb);
+                         CallInst::Create(FuncLoop,
+                                          {ConstantInt::get(Type::getInt32Ty(context), 1)})
+                                          ->insertBefore(&bb);
+                     } else{
+                         CallInst::Create(FuncLoop,
+                                          {ConstantInt::get(Type::getInt32Ty(context), 0)})
+                                          ->insertBefore(&bb);
+                     }
+                     break;
+                 case ADD:
+                 case SUB:
+                 case MUL:
+                 case SDIV:
+                 case SREM:
+                     CallInst::Create(FuncBinOp,
+                                      {ConstantInt::get(Type::getInt32Ty(context), getRegisterID(&bb)),
+                                       ConstantInt::get(Type::getInt32Ty(context),bb.getOpcode())})
+                                       ->insertAfter(&bb);
+                     for(unsigned i = 0; i < bb.getNumOperands(); i++){
+                         if(dyn_cast<ConstantInt>(bb.getOperand(i))){
+                             CallInst::Create(FuncConst,{ConstantInt::get(
+                                     Type::getInt32Ty(context),
+                                     dyn_cast<ConstantInt>(bb.getOperand(i))->getSExtValue())})
+                                     ->insertAfter(&bb);
+                         } else{
+                             CallInst::Create(FuncRegister,{ConstantInt::get(Type::getInt32Ty(context),
+                                                                             getRegisterID(bb.getOperand(i)))})
+                                                                             ->insertAfter(&bb);
+                         }
+                     }
+                     break;
+                 case ALLOCA:
+                     CallInst::Create(FuncAlloca,
+                                      {ConstantInt::get(Type::getInt32Ty(context),getRegisterID(&bb)),
+                                       &bb})
+                                       ->insertAfter(&bb);
+
+                     break;
+                 case LOAD:
+                     CallInst::Create(FuncLoad,
+                                      {ConstantInt::get(Type::getInt32Ty(context),getRegisterID(&bb)),
+                                       bb.getOperand(0)})
+                                       ->insertAfter(&bb);
+                     break;
+                 case STORE:
+                     if(dyn_cast<ConstantInt>(bb.getOperand(0))){
+                         CallInst::Create(FuncStore,
+                                          {bb.getOperand(1)})
+                                 ->insertAfter(&bb);
+                         CallInst::Create(FuncConst,
+                                          {ConstantInt::get(
+                                                  Type::getInt32Ty(context),
+                                                  dyn_cast<ConstantInt>(bb.getOperand(0))->getSExtValue())})
+                                                  ->insertAfter(&bb);
+                     }
+                     else{
+                         CallInst::Create(FuncStore,
+                                          {bb.getOperand(1)})
+                                 ->insertAfter(&bb);
+                         CallInst::Create(FuncRegister,
+                                          {ConstantInt::get(Type::getInt32Ty(context),getRegisterID(bb.getOperand(0)))})
+                                 ->insertAfter(&bb);
+
+                     }
+                     break;
+                 case ICMP:
+                     CallInst::Create(FuncICmp,
+                                      {ConstantInt::get(Type::getInt32Ty(context),getRegisterID(&bb)),
+                                       ConstantInt::get(Type::getInt32Ty(context),
+                                                        dyn_cast<ICmpInst>(&bb)->getPredicate())})
+                                                        ->insertAfter(&bb);
+                     for(unsigned i = 0; i < bb.getNumOperands(); i++)
+                     {
+                         if(dyn_cast<ConstantInt>(bb.getOperand(i))){
+                             CallInst::Create(FuncConst,
+                                              {ConstantInt::get(
+                                                      Type::getInt32Ty(context),
+                                                      dyn_cast<ConstantInt>(bb.getOperand(i))->getSExtValue())})
+                                     ->insertAfter(&bb);
+                             //errs() << dyn_cast<ConstantInt>(bb.getOperand(i))->getSExtValue() <<'\n';
+                         } else{
+                             CallInst::Create(FuncRegister,
+                                              {ConstantInt::get(Type::getInt32Ty(context),
+                                                                getRegisterID(bb.getOperand(i)))})
+                                     ->insertAfter(&bb);
+                         }
+                     }
+                     break;
+                 case CALL:
+                 default:
+                     break;
+             }
+         }
+     }
+    return false;
+}
+
+
+
+/// We initialize pass ID here. LLVM uses ID’s address to
+/// identify a pass, so initialization value is not important.
+char Instrument::ID = 1;
+static RegisterPass<Instrument>
+    /// Lastly, we register our class Instrument,giving it
+    /// a command line argument “Instrument”, and a name
+    /// “Instrumentation for Dynamic Symbolic Execution”.
+    X("Instrument", "Instrumentation for Dynamic Symbolic Execution",
+      false /* Only looks at CFG */,
+      false /* Analysis Pass */);
+
+} // namespace instrument

dse/src/Runtime.cpp

@@ -0,0 +1,149 @@
+#include <iostream>
+
+#include "llvm/IR/InstrTypes.h"
+#include "llvm/IR/Instruction.h"
+
+#include "SymbolicInterpreter.h"
+
+#define ADD         13      ///    +
+#define SUB         15      ///    -
+#define MUL         17      ///    *
+#define SDIV        20      ///    /
+#define SREM        23      ///    %
+
+#define ICMP_EQ     32  ///< equal
+#define ICMP_NE     33  ///< not equal
+#define ICMP_SGT    38  ///< signed greater than
+#define ICMP_SGE    39  ///< signed greater or equal
+#define ICMP_SLT    40  ///< signed less than
+#define ICMP_SLE    41  ///< signed less or equal
+#define ICMP_UGT    34  ///< unsigned greater than
+#define ICMP_UGE    35  ///< unsigned greater or equal
+#define ICMP_ULT    36  ///< unsigned less than
+#define ICMP_ULE    37  ///< unsigned less or equal
+
+extern SymbolicInterpreter SI;
+using namespace z3;
+using namespace std;
+/**
+ * Implement your transfer functions.
+ */
+
+/// DSE_Alloca(getRegisterId(%x),%x)
+/// Reg(%x) => 0x1000
+extern "C" void __DSE_Alloca__(int R, int *Ptr) {
+    expr e = SI.getContext().int_val(*Ptr);
+    auto address = Address(R);
+    SI.getMemory().insert(make_pair(address, e));
+}
+
+extern "C" void __DSE_Store__(int *X) {
+    expr e = SI.getStack().top();
+    SI.getStack().pop();
+    if(e.to_string().at(0) == 'R'){
+        e = SI.getMemory().at(e);
+    }
+    auto address = Address(X);
+    SI.getMemory().insert(make_pair(address, e));
+    SI.getMemory().at(address) = e;
+}
+
+extern "C" void __DSE_Load__(int Y, int *X) {
+    expr e = SI.getMemory().at(Address(X));
+    auto address = Address(Y);
+    SI.getMemory().insert(make_pair(address, e));
+    SI.getMemory().at(address) = e;
+}
+
+extern "C" void __DSE_Label__(int RID, int BID, int label){
+    expr el = SI.getMemory().at(Address(RID));
+    auto address = Address(BID);
+    expr t = SI.getContext().bool_val(true);
+    expr f = SI.getContext().bool_val(false);
+    if(label){
+        SI.getMemory().insert(make_pair(address, el == t));
+        SI.getMemory().at(address) = (el == t);
+    } else{
+        SI.getMemory().insert(make_pair(address, el == f));
+        SI.getMemory().at(address) = (el == f);
+    }
+}
+
+extern "C" void __DSE_Loop__(int Type){
+    expr type = SI.getContext().int_val(Type);
+    SI.getStack().push(type);
+}
+
+extern "C" void __DSE_ICmp__(int R, int Op) {
+    expr el = SI.getStack().top();
+    SI.getStack().pop();
+    expr er = SI.getStack().top();
+    SI.getStack().pop();
+    if(el.to_string().at(0) == 'R'){
+        el = SI.getMemory().at(el);
+    }
+    if(er.to_string().at(0) == 'R'){
+        er = SI.getMemory().at(er);
+    }
+    expr res = el == er;
+    switch (Op) {
+        case ICMP_EQ:
+            res = el == er;
+            break;
+        case ICMP_NE:
+            res = el != er;
+            break;
+        case ICMP_SLT:
+            res = el < er;
+            break;
+        case ICMP_SLE:
+            res = el <= er;
+            break;
+        case ICMP_SGT:
+            res = el > er;
+            break;
+        case ICMP_SGE:
+            res = el >= er;
+        default:
+            break;
+    }
+    auto address = Address(R);
+    SI.getMemory().insert(make_pair(address, res));
+    SI.getMemory().at(address) = res;
+}
+
+extern "C" void __DSE_BinOp__(int R, int Op) {
+    expr el = SI.getStack().top();
+    SI.getStack().pop();
+    expr er = SI.getStack().top();
+    SI.getStack().pop();
+    if(el.to_string().at(0) == 'R'){
+        el = SI.getMemory().at(el);
+    }
+    if(er.to_string().at(0) == 'R'){
+        er = SI.getMemory().at(er);
+    }
+    expr res = el + er;
+    switch (Op) {
+        case ADD:
+            res = el + er;
+            break;
+        case SUB:
+            res = el - er;
+            break;
+        case MUL:
+            res = el * er;
+            break;
+        case SDIV:
+            res = el / er;
+            break;
+        case SREM:
+            res = el % er;
+            break;
+        default:
+            break;
+    }
+    auto address = Address(R);
+    SI.getMemory().insert(make_pair(address, res));
+    SI.getMemory().at(address) = res;
+}

dse/src/Strategy.cpp

@@ -0,0 +1,51 @@
+#include "Strategy.h"
+#include <iostream>
+
+static const char *NOT = "not";
+std::vector<std::string> Branches;
+/**
+ * Implement your search strategy.
+ */
+
+void recordBranches(z3::expr_vector &OldVec){
+    for (auto && E : OldVec) {
+        if(E.to_string().find('X') == std::string::npos){
+            continue;
+        }
+        if(std::find(Branches.begin(), Branches.end(),E.to_string()) == Branches.end()){
+            Branches.push_back(E.to_string().c_str());
+        }
+    }
+}
+
+void searchStrategy(z3::expr_vector &OldVec) {
+    int i = OldVec.size()-1;
+    if(i<0){
+        return;
+    }
+    auto e = OldVec[i];
+    if(e.to_string().find('X') == std::string::npos){
+        OldVec.pop_back();
+        searchStrategy(OldVec);
+        return;
+    }
+    if(e.to_string().substr(1, 3) != NOT){
+        std::string newExpr = e.to_string();
+        if(newExpr.find("false") != std::string::npos){
+            newExpr = newExpr.replace(newExpr.end()-6, newExpr.end()-1,"true");
+        } else{
+            newExpr = newExpr.replace(newExpr.end()-5, newExpr.end()-1,"false");
+        }
+        if(std::find(Branches.begin(), Branches.end(), newExpr) == Branches.end()){
+            OldVec.pop_back();
+            OldVec.push_back(not e);
+        } else{
+            OldVec.pop_back();
+            searchStrategy(OldVec);
+        }
+    }
+    else {
+        OldVec.pop_back();
+        searchStrategy(OldVec);
+    }
+}

dse/src/SymbolicInterpreter.cpp

@@ -0,0 +1,110 @@
+#include "SymbolicInterpreter.h"
+
+#include <ctime>
+#include <fstream>
+
+std::ostream &operator<<(std::ostream &OS, const Address &A) {
+  if (A.Type == A.Memory) {
+    OS << A.Addr;
+  } else {
+    OS << "R" << A.Addr;
+  }
+  return OS;
+}
+
+int SymbolicInterpreter::NewInput(int *Ptr, int ID) {
+  int Ret = 0;
+  if (Inputs.find(ID) != Inputs.end()) {
+    Ret = Inputs[ID];
+  } else {
+    Ret = std::rand();
+    Inputs[ID] = Ret;
+  }
+  Address X(Ptr);
+  std::string InputName = "X" + std::to_string(NumOfInputs);
+  z3::expr SE = Ctx.int_const(InputName.c_str());
+  /// Type(Mem) : MemoryTy = std::map<Address, z3::expr>
+  Mem.insert(std::make_pair(X, SE));
+  NumOfInputs++;
+  return Ret;
+}
+
+SymbolicInterpreter SI;
+
+void print(std::ostream &OS) {
+  OS << "=== Inputs ===" << std::endl;
+  int Idx = 0;
+  for (auto &E : SI.getInputs()) {
+    OS << "X" << E.first << " : " << E.second << std::endl;
+  }
+  OS << std::endl;
+  OS << "=== Symbolic Memory ===" << std::endl;
+  for (auto &E : SI.getMemory()) {
+    OS << E.first << " : " << E.second << std::endl;
+  }
+  OS << std::endl;
+
+  OS << "=== Path Condition ===" << std::endl;
+  for (auto &E : SI.getPathCondition()) {
+    std::string BID = "B" + std::to_string(E.first);
+    OS << BID << " : " << E.second << std::endl;
+  }
+}
+
+extern "C" void __DSE_Exit__() {
+  z3::solver Solver(SI.getContext());
+  std::ofstream Branch(BranchFile);
+  for (auto &E : SI.getPathCondition()) {
+    std::string BID = "B" + std::to_string(E.first);
+    Solver.add(E.second);
+    Branch << E.second << "\n";
+  }
+  std::ofstream Smt2(FormulaFile);
+  Smt2 << Solver.to_smt2();
+  std::ofstream Log(LogFile);
+  print(Log);
+}
+
+extern "C" void __DSE_Init__() {
+  std::srand(std::time(nullptr));
+  std::string Line;
+  std::ifstream Input(InputFile);
+  if (Input.is_open()) {
+    while (getline(Input, Line)) {
+      int ID = std::stoi(Line.substr(1, Line.find(",")));
+      int Val = std::stoi(Line.substr(Line.find(",") + 1));
+      SI.getInputs()[ID] = Val;
+    }
+  }
+  std::atexit(__DSE_Exit__);
+}
+
+extern "C" void __DSE_Input__(int *X, int ID) {
+    /// 地址 *X 的值变为 (int)SI.NewInput(X, ID)
+    /// Inputs<0, V0> => %x = V0
+    *X = (int)SI.NewInput(X, ID);
+}
+
+/// 这里我按照自己的逻辑改了框架
+extern "C" void __DSE_Branch__(int RID, int BID) {
+  if(SI.getStack().top().to_string() == "0"){
+      SI.getStack().pop();
+      return;
+  }
+  MemoryTy &Mem = SI.getMemory();
+  Address Addr(RID);
+  /// (Addr(RID), SE)
+  z3::expr SE = Mem.at(Addr);
+  SI.getPathCondition().push_back(std::make_pair(BID, SE));
+}
+
+extern "C" void __DSE_Const__(int X) {
+  z3::expr SE = SI.getContext().int_val(X);
+  SI.getStack().push(SE);
+}
+
+extern "C" void __DSE_Register__(int X) {
+  std::string Name = "R" + std::to_string(X);
+  z3::expr SE = SI.getContext().int_const(Name.c_str());
+  SI.getStack().push(SE);
+}

dse/test/Makefile

@@ -0,0 +1,13 @@
+.PRECIOUS: %.ll %.instrumented.ll
+#-Instrument
+TARGETS=simple0 simple1 simple2 branch0 branch1 branch2 infeasable
+
+all: ${TARGETS}
+
+%: %.c
+	clang -emit-llvm -S -fno-discard-value-names -c -o $@.ll $<
+	opt -enable-new-pm=0 -load ../build/InstrumentPass.so -Instrument -S $*.ll -o $*.instrumented.ll
+	clang -o $@ -L${PWD}/../build -lruntime $*.instrumented.ll
+
+clean:
+	rm -f *.ll *.out *.err *.smt2 input.txt branch.txt ${TARGETS}

dse/test/branch0.c

@@ -0,0 +1,26 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x;
+  DSE_Input(x);
+  int y;
+  DSE_Input(y);
+  int z;
+  DSE_Input(z);
+
+  if (x == 1) {
+	 if (y == z) {
+		x = x / (y-z);
+	 }
+  } else {
+  	if(x == 0){
+  		x = 1;
+  	}
+  }
+
+  return 0;
+}
+
+

dse/test/branch1.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x;
+  DSE_Input(x);
+  int y;
+  DSE_Input(y);
+  int z;
+  DSE_Input(z);
+
+  if (x == y && y == z) {
+	x = x / (y-z);
+  }
+  else{
+  	x = 1;
+  }
+
+  return 0;
+}
+
+

dse/test/branch2.c

@@ -0,0 +1,21 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x;
+  DSE_Input(x);
+  int y;
+  DSE_Input(y);
+  int z;
+  DSE_Input(z);
+
+
+  if (x > y && y > z && z == 0) {
+	x = x / z;
+  }
+  
+  return 0;
+}
+
+

dse/test/infeasable.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x;
+  DSE_Input(x);
+
+  //c is a product of two primes 
+  int c = 1022;
+
+  int y = 1;
+
+  for(int i=0; i<x; i++){
+	y *= 2;
+  }
+
+  if (y % c == 2) {
+  	x = x / (c-c);
+  }
+  return 0;
+}

dse/test/simple0.c

@@ -0,0 +1,10 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x = 1;
+  int y = x;
+  int z = 9;
+  return 0;
+}

dse/test/simple1.c

@@ -0,0 +1,13 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x; 
+  DSE_Input(x);
+  int y;
+  DSE_Input(y);
+  int z = (x*y) + (y/x) - (x+y);
+  x = z;
+  return 0;
+}

dse/test/simple2.c

@@ -0,0 +1,10 @@
+#include <stdio.h>
+
+#include "../include/Runtime.h"
+
+int main() {
+  int x; DSE_Input(x);
+  int y = x + 1;
+  x = y;
+  return 0;
+}