first commit

.gitignore

@@ -0,0 +1,3 @@
+build/
+test/*.ll
+submission.zip

.vscode/settings.json

@@ -0,0 +1,64 @@
+{
+    "files.associations": {
+        "array": "cpp",
+        "atomic": "cpp",
+        "bit": "cpp",
+        "*.tcc": "cpp",
+        "bitset": "cpp",
+        "cctype": "cpp",
+        "chrono": "cpp",
+        "clocale": "cpp",
+        "cmath": "cpp",
+        "compare": "cpp",
+        "concepts": "cpp",
+        "condition_variable": "cpp",
+        "cstdarg": "cpp",
+        "cstddef": "cpp",
+        "cstdint": "cpp",
+        "cstdio": "cpp",
+        "cstdlib": "cpp",
+        "cstring": "cpp",
+        "ctime": "cpp",
+        "cwchar": "cpp",
+        "cwctype": "cpp",
+        "deque": "cpp",
+        "map": "cpp",
+        "string": "cpp",
+        "unordered_map": "cpp",
+        "vector": "cpp",
+        "exception": "cpp",
+        "algorithm": "cpp",
+        "functional": "cpp",
+        "iterator": "cpp",
+        "memory": "cpp",
+        "memory_resource": "cpp",
+        "numeric": "cpp",
+        "optional": "cpp",
+        "random": "cpp",
+        "ratio": "cpp",
+        "string_view": "cpp",
+        "system_error": "cpp",
+        "tuple": "cpp",
+        "type_traits": "cpp",
+        "utility": "cpp",
+        "fstream": "cpp",
+        "initializer_list": "cpp",
+        "iosfwd": "cpp",
+        "iostream": "cpp",
+        "istream": "cpp",
+        "limits": "cpp",
+        "mutex": "cpp",
+        "new": "cpp",
+        "numbers": "cpp",
+        "ostream": "cpp",
+        "semaphore": "cpp",
+        "shared_mutex": "cpp",
+        "sstream": "cpp",
+        "stdexcept": "cpp",
+        "stop_token": "cpp",
+        "streambuf": "cpp",
+        "thread": "cpp",
+        "cinttypes": "cpp",
+        "typeinfo": "cpp"
+    }
+}

CMakeLists.txt

@@ -0,0 +1,39 @@
+cmake_minimum_required(VERSION 3.10)
+
+find_package(LLVM 10 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/DSEInstrument.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})

Makefile

@@ -0,0 +1,17 @@
+MAKEFLAGS += --no-builtin-rules
+
+SRC:=$(shell find ./src -type f -name "*.cpp")
+
+all: submit
+
+submit: ${SRC} clean
+	chown -R --reference=CMakeLists.txt .
+	zip -r /tmp/submission.zip * 2> /dev/null
+	mv /tmp/submission.zip ./submission.zip
+	chown --reference=CMakeLists.txt submission.zip
+	echo "submission.zip created successfully."
+
+clean:
+	rm -rf build
+	(cd test; make clean) > /dev/null
+	rm -f submission.zip

include/DSEInstrument.h

@@ -0,0 +1,39 @@
+#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"
+
+using namespace llvm;
+
+namespace dse {
+
+int RegisterID = 0;
+std::map<Value *, int> RegisterMap;
+int BranchID = 0;
+std::map<Instruction *, int> BranchMap;
+
+int getRegisterID(Value *I) {
+  if (RegisterMap.find(I) == RegisterMap.end()) {
+    RegisterMap[I] = RegisterMap.size();
+  }
+  return RegisterMap[I];
+}
+
+int getBranchID(Instruction *I) {
+  if (BranchMap.find(I) == BranchMap.end()) {
+    BranchMap[I] = BranchMap.size();
+  }
+  return BranchMap[I];
+}
+
+struct DSEInstrument : public FunctionPass {
+  static char ID;
+  static const char *checkFunctionName;
+
+  DSEInstrument() : FunctionPass(ID) {}
+
+  bool runOnFunction(Function &F) override;
+};
+} // namespace dse

include/Runtime.h

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

include/Strategy.h

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

include/SymbolicInterpreter.h

@@ -0,0 +1,57 @@
+#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";
+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;
+  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

src/DSE.cpp

@@ -0,0 +1,97 @@
+#include <fstream>
+#include <iostream>
+#include <sys/stat.h>
+#include <unistd.h>
+
+#include "z3++.h"
+
+#include "Strategy.h"
+#include "SymbolicInterpreter.h"
+
+#define ARG_EXIST_CHECK(Name, Arg)                                             \
+  {                                                                            \
+    struct stat Buffer;                                                        \
+    if (stat(Arg, &Buffer)) {                                                  \
+      fprintf(stderr, "%s not found\n", Arg);                                  \
+      return 1;                                                                \
+    }                                                                          \
+  }                                                                            \
+  std::string Name(Arg);
+
+z3::context Ctx;
+z3::solver Solver(Ctx);
+
+void storeInput() {
+  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 I = Input.get_numeral_int();
+      OS << E.name() << "," << I << std::endl;
+    }
+  }
+}
+
+void printNewPathCondition(z3::expr_vector &Vec) {
+  std::ofstream Log;
+  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() {
+  z3::expr_vector Vec = Ctx.parse_file(FormulaFile);
+
+  while (true) {
+    searchStrategy(Vec);
+
+    for (const auto &E : Vec) {
+      Solver.add(E);
+    }
+    z3::check_result Result = Solver.check();
+    if (Result == z3::sat) {
+      storeInput();
+      printNewPathCondition(Vec);
+      break;
+    }
+  }
+}
+
+/**
+ * Usage:
+ * ./dse [target] (iterations)
+ */
+int main(int argc, char **argv) {
+  if (argc < 2) {
+    std::cerr << "usage: " << argv[0] << " [target] (iterations)" << std::endl;
+    return 1;
+  }
+
+  ARG_EXIST_CHECK(Target, argv[1]);
+
+  int MaxIter = INT_MAX;
+  if (argc == 3) {
+    MaxIter = atoi(argv[2]);
+  }
+
+  struct stat Buffer;
+  int Iter = 0;
+  while (Iter < MaxIter) {
+    int Ret = std::system(Target.c_str());
+    if (Ret) {
+      std::cout << "Crashing input found " << std::endl;
+      break;
+    }
+    if (stat(FormulaFile, &Buffer)) {
+      std::cerr << FormulaFile << " not found" << std::endl;
+      return 1;
+    }
+    generateInput();
+    Iter++;
+  }
+}

src/DSEInstrument.cpp

@@ -0,0 +1,210 @@
+#include "DSEInstrument.h"
+
+using namespace llvm;
+
+namespace dse {
+
+static const char *DSE_INIT_FUNCTION_NAME = "__DSE_Init__";
+static const char *DSE_ALLOCA_FUNCTION_NAME = "__DSE_Alloca__";
+static const char *DSE_STORE_FUNCTION_NAME = "__DSE_Store__";
+static const char *DSE_LOAD_FUNCTION_NAME = "__DSE_Load__";
+static const char *DSE_CONST_FUNCTION_NAME = "__DSE_Const__";
+static const char *DSE_REGISTER_FUNCTION_NAME = "__DSE_Register__";
+static const char *DSE_ICMP_FUNCTION_NAME = "__DSE_ICmp__";
+static const char *DSE_BRANCH_FUNCTION_NAME = "__DSE_Branch__";
+static const char *DSE_BINOP_FUNCTION_NAME = "__DSE_BinOp__";
+
+
+/**
+ * @brief Instrument to initialize the Z3 solver.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param F Function to Instrument
+ * @param I Instrumentation location
+ */
+void instrumentDSEInit(Module *Mod, Function &F, Instruction &I) {
+}
+
+/**
+ * @brief Instrument to Alloca Instructions.
+ *
+ * @param Mod Current Module
+ * @param AI Instrumentation location
+ */
+void instrumentAlloca(Module *Mod, AllocaInst *AI) {
+  auto &Context = Mod->getContext();
+  auto *Int32Type = Type::getInt32Ty(Context);
+
+  Value *VarID = ConstantInt::get(Int32Type, getRegisterID(AI));
+  std::vector<Value *> Args = {VarID, AI};
+
+  auto Fun = Mod->getFunction(DSE_ALLOCA_FUNCTION_NAME);
+  CallInst::Create(Fun, Args, "", AI->getNextNonDebugInstruction());
+}
+
+/**
+ * @brief Instrument to Store Instructions.
+ *
+ * @param Mod Current Module
+ * @param SI Instrumentation location
+ */
+void instrumentStore(Module *Mod, StoreInst *SI) {
+  std::vector<Value *> Args = {SI->getPointerOperand()};
+
+  auto Fun = Mod->getFunction(DSE_STORE_FUNCTION_NAME);
+  CallInst::Create(Fun, Args, "", SI);
+}
+
+/**
+ * @brief Instrument to Load Instructions.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param LI Instrumentation location
+ */
+void instrumentLoad(Module *Mod, LoadInst *LI) {
+}
+
+/**
+ * @brief Instrument Constant values.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param ConstInt Constant
+ * @param I Instrumentation location.
+ */
+void instrumentConstantValue(Module *Mod, ConstantInt *ConstInt, Instruction *I) {
+}
+
+/**
+ * @brief Instrument Registers.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param Var Variable
+ * @param I Instrumentation location
+ */
+void instrumentRegister(Module *Mod, Value *Var, Instruction *I) {
+}
+
+/**
+ * @brief Instrument a Value
+ *
+ * TODO: Implement this.
+ *
+ * Hint: Values are a stored in registers;
+ *       some values may also be a constant.
+ *       Use the function you just defined above.
+ *
+ * @param Mod Current Module
+ * @param Val Value
+ * @param I Instrumentation location
+ */
+void instrumentValue(Module *Mod, Value *Val, Instruction *I) {
+}
+
+/**
+ * @brief Instrument Comparision Instructions.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param CI Instrumentation location
+ */
+void instrumentICmp(Module *Mod, ICmpInst *CI) {
+}
+
+/**
+ * @brief Instrument Branch Instructions.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param BI Instrumentation location
+ */
+void instrumentBranch(Module *Mod, BranchInst *BI) {
+}
+
+/**
+ * @brief Instrument BinaryOperator.
+ *
+ * TODO: Implement this.
+ *
+ * @param Mod Current Module
+ * @param BO Instrumentation location
+ */
+void instrumentBinOp(Module *Mod, BinaryOperator *BO) {
+}
+
+/**
+ * @brief Instrument Instructions.
+ *
+ * TODO: Implement this.
+ *
+ * Hint: Make sure to instrument all the Values
+ *       used by an instruction so that they are available
+ *       to the DSE Engine.
+ *
+ * @param Mod Current Module
+ * @param I Instruction to Instrument
+ */
+void instrument(Module *Mod, Instruction *I) {
+  if (AllocaInst *AI = dyn_cast<AllocaInst>(I)) {
+    // TODO: Implement.
+  } else if (StoreInst *SI = dyn_cast<StoreInst>(I)) {
+    // TODO: Implement.
+  } else if (LoadInst *LI = dyn_cast<LoadInst>(I)) {
+    // TODO: Implement.
+  } else if (ICmpInst *CI = dyn_cast<ICmpInst>(I)) {
+    // TODO: Implement.
+  } else if (BranchInst *BI = dyn_cast<BranchInst>(I)) {
+    if (BI->isUnconditional())
+      return;
+    // TODO: Implement.
+  } else if (BinaryOperator *BO = dyn_cast<BinaryOperator>(I)) {
+    // TODO: Implement.
+  }
+}
+
+bool DSEInstrument::runOnFunction(Function &F) {
+  LLVMContext &Context = F.getContext();
+  Module *Mod = F.getParent();
+
+  Type *VoidType = Type::getVoidTy(Context);
+  Type *Int1Type = Type::getInt1Ty(Context);
+  auto *Int32Type = Type::getInt32Ty(Context);
+  Type *Int32PtrType = Type::getInt32PtrTy(Context);
+
+  // Insert all the DSE function declarations into Module.
+  Mod->getOrInsertFunction(DSE_INIT_FUNCTION_NAME, VoidType);
+  Mod->getOrInsertFunction(DSE_ALLOCA_FUNCTION_NAME, VoidType, Int32Type, Int32PtrType);
+  Mod->getOrInsertFunction(DSE_STORE_FUNCTION_NAME, VoidType, Int32PtrType);
+  Mod->getOrInsertFunction(DSE_LOAD_FUNCTION_NAME, VoidType, Int32Type, Int32PtrType);
+  Mod->getOrInsertFunction(DSE_CONST_FUNCTION_NAME, VoidType, Int32Type);
+  Mod->getOrInsertFunction(DSE_REGISTER_FUNCTION_NAME, VoidType, Int32Type);
+  Mod->getOrInsertFunction(DSE_ICMP_FUNCTION_NAME, VoidType, Int32Type, Int32Type);
+  Mod->getOrInsertFunction(DSE_BRANCH_FUNCTION_NAME, VoidType, Int32Type, Int32Type, Int1Type);
+  Mod->getOrInsertFunction(DSE_BINOP_FUNCTION_NAME, VoidType, Int32Type, Int32Type);
+
+  if (F.getName().equals("main")) {
+    // TODO: Initilize the DSE Engine
+  }
+
+  // Instrument each instruction
+  for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) {
+    instrument(Mod, &*I);
+  }
+  return true;
+}
+
+char DSEInstrument::ID = 1;
+static RegisterPass<DSEInstrument>
+    X("DSEInstrument", "Instrumentations for Dynamic Symbolic Execution", false,
+      false);
+
+} // namespace dse

src/Runtime.cpp

@@ -0,0 +1,84 @@
+#include <iostream>
+
+#include "llvm/IR/InstrTypes.h"
+#include "llvm/IR/Instruction.h"
+
+#include "SymbolicInterpreter.h"
+
+extern SymbolicInterpreter SI;
+
+z3::expr eval(z3::expr &E) {
+  if (E.kind() == Z3_NUMERAL_AST) {
+    return E;
+  } else {
+    MemoryTy Mem = SI.getMemory();
+    Address Register(E);
+    if (Mem.find(Register) != Mem.end()) {
+      return Mem.at(Register);
+    } else {
+      std::cout << "Warning: Cannot find register " << Register << " in memory "
+                << std::endl;
+      return E;
+    }
+  }
+}
+
+/**
+ * @brief Symbolically evaluate Alloca
+ *
+ * @param R RegisterID
+ * @param Ptr Address
+ */
+extern "C" void __DSE_Alloca__(int R, int *Ptr) {
+  MemoryTy &Mem = SI.getMemory();
+  Address Register(R);
+  z3::expr SE = SI.getContext().int_val((uintptr_t)Ptr);
+  Mem.insert(std::make_pair(Register, SE));
+}
+
+/**
+ * @brief Symbolically evaluate Store
+ *
+ * @param X Address
+ */
+extern "C" void __DSE_Store__(int *X) {
+  MemoryTy &Mem = SI.getMemory();
+  Address Addr(X);
+  z3::expr SE = eval(SI.getStack().top());
+  SI.getStack().pop();
+  Mem.erase(Addr);
+  Mem.insert(std::make_pair(Addr, SE));
+}
+
+/**
+ * @brief Symbolically evaluate Load
+ *
+ * TODO: Implement this.
+ *
+ * @param Y Address of destination
+ * @param X Address of Load source
+ */
+extern "C" void __DSE_Load__(int Y, int *X) {
+}
+
+/**
+ * @brief Symbolically evaluate Comparisions
+ *
+ * TODO: Implement this.
+ *
+ * @param R Address of Comparision result
+ * @param Op Operator Kind
+ */
+extern "C" void __DSE_ICmp__(int R, int Op) {
+}
+
+/**
+ * @brief Symbolically evaluate Binary Operation.
+ *
+ * TODO: Implement this.
+ *
+ * @param R Address of Binary Operation result.
+ * @param Op Operator Kind
+ */
+extern "C" void __DSE_BinOp__(int R, int Op) {
+}

src/Strategy.cpp

@@ -0,0 +1,15 @@
+#include "Strategy.h"
+
+/*******************************************************
+ * NOTE: You are free to edit this file as you see fit *
+ *******************************************************/
+
+/**
+ * Strategy to explore various paths of execution.
+ *
+ * TODO: Implement your search strategy.
+ *
+ * @param OldVec Vector of Z3 expressions.
+ */
+void searchStrategy(z3::expr_vector &OldVec) {
+}

src/SymbolicInterpreter.cpp

@@ -0,0 +1,101 @@
+#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());
+  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 << BID << "\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); }
+
+extern "C" void __DSE_Branch__(int BID, int RID, int B) {
+  MemoryTy &Mem = SI.getMemory();
+  Address Addr(RID);
+  z3::expr SE = Mem.at(Addr);
+  z3::expr Cond =
+      B ? SI.getContext().bool_val(true) : SI.getContext().bool_val(false);
+  SI.getPathCondition().push_back(std::make_pair(BID, SE == Cond));
+}
+
+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);
+}

test/Makefile

@@ -0,0 +1,20 @@
+.PRECIOUS: %.ll %.instrumented.ll
+
+SRC:=$(wildcard *.c)
+TARGETS:=$(patsubst %.c, %, $(SRC))
+
+build-all: ${TARGETS}
+
+all: $(patsubst %, dse-%, $(TARGETS))
+
+
+%: %.c
+	clang -emit-llvm -S -fno-discard-value-names -c -o $@.ll $<
+	opt -load ../build/InstrumentPass.so -DSEInstrument -S $*.ll -o $*.instrumented.ll
+	clang -o $@ -L${PWD}/../build -lruntime $*.instrumented.ll
+
+dse-%: %
+	./test $<
+
+clean:
+	rm -f *.ll *.out *.err *.smt2 input.txt branch.txt ${TARGETS}

test/branch0.c

@@ -0,0 +1,20 @@
+#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 == 0) {
+	 if (y == z) {
+		x = x / (y-z);
+	 }
+  }
+
+  return 0;
+}

test/branch1.c

@@ -0,0 +1,18 @@
+#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);
+  }
+
+  return 0;
+}

test/branch2.c

@@ -0,0 +1,18 @@
+#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;
+}

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 = 181 * 191;
+
+  int y = 1;
+
+  for(int i=0; i<x; i++){
+	y *= 2;
+  }
+
+  if (y % c == 17) {
+    x = x / (c-c);
+  }
+  return 0;
+}

test/simple0.c

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

test/simple1.c

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

test/test

@@ -0,0 +1,9 @@
+#!/bin/sh
+
+USAGE="Usage ./test [target] [timeout]"
+[ -z "$1" ] && echo "$USAGE" && exit 1
+TARGET="./$1"
+[ ! -f "$TARGET" ] && echo "$TARGET not found" && exit 1
+TIME="${2:-10s}"
+
+timeout "$TIME" ../build/dse "$TARGET" || echo "Exiting test for $TARGET with E${?}"