diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..cc741fc --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +build/ +test/*.ll +submission.zip diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..3365a73 --- /dev/null +++ b/.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" + } +} \ No newline at end of file diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..f1cdefe --- /dev/null +++ b/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}) diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..d77f8c9 --- /dev/null +++ b/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 diff --git a/include/DSEInstrument.h b/include/DSEInstrument.h new file mode 100644 index 0000000..4537626 --- /dev/null +++ b/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 RegisterMap; +int BranchID = 0; +std::map 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 diff --git a/include/Runtime.h b/include/Runtime.h new file mode 100644 index 0000000..962b756 --- /dev/null +++ b/include/Runtime.h @@ -0,0 +1,3 @@ +void __DSE_Input__(int *x, int ID); + +#define DSE_Input(x) __DSE_Input__(&x, __COUNTER__) diff --git a/include/Strategy.h b/include/Strategy.h new file mode 100644 index 0000000..5193d8f --- /dev/null +++ b/include/Strategy.h @@ -0,0 +1,3 @@ +#include "z3++.h" + +void searchStrategy(z3::expr_vector &OldVec); diff --git a/include/SymbolicInterpreter.h b/include/SymbolicInterpreter.h new file mode 100644 index 0000000..7eff25f --- /dev/null +++ b/include/SymbolicInterpreter.h @@ -0,0 +1,57 @@ +#ifndef SYMBOLIC_INTERPRETER_H +#define SYMBOLIC_INTERPRETER_H + +#include +#include +#include +#include + +#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; + +class SymbolicInterpreter { +public: + int NewInput(int *Ptr, int ID); + MemoryTy &getMemory() { return Mem; } + std::map &getInputs() { return Inputs; } + z3::context &getContext() { return Ctx; } + std::stack &getStack() { return Stack; } + std::vector> &getPathCondition() { + return PathCondition; + } + +private: + MemoryTy Mem; + std::map Inputs; + int NumOfInputs = 0; + std::stack Stack; + std::vector> PathCondition; + + z3::context Ctx; +}; + +#endif // SYMBOLIC_INTERPRETER_H diff --git a/src/DSE.cpp b/src/DSE.cpp new file mode 100644 index 0000000..4a9b35e --- /dev/null +++ b/src/DSE.cpp @@ -0,0 +1,97 @@ +#include +#include +#include +#include + +#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++; + } +} diff --git a/src/DSEInstrument.cpp b/src/DSEInstrument.cpp new file mode 100644 index 0000000..468ec56 --- /dev/null +++ b/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 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 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(I)) { + // TODO: Implement. + } else if (StoreInst *SI = dyn_cast(I)) { + // TODO: Implement. + } else if (LoadInst *LI = dyn_cast(I)) { + // TODO: Implement. + } else if (ICmpInst *CI = dyn_cast(I)) { + // TODO: Implement. + } else if (BranchInst *BI = dyn_cast(I)) { + if (BI->isUnconditional()) + return; + // TODO: Implement. + } else if (BinaryOperator *BO = dyn_cast(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 + X("DSEInstrument", "Instrumentations for Dynamic Symbolic Execution", false, + false); + +} // namespace dse diff --git a/src/Runtime.cpp b/src/Runtime.cpp new file mode 100644 index 0000000..f85ebeb --- /dev/null +++ b/src/Runtime.cpp @@ -0,0 +1,84 @@ +#include + +#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) { +} diff --git a/src/Strategy.cpp b/src/Strategy.cpp new file mode 100644 index 0000000..ca978f4 --- /dev/null +++ b/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) { +} diff --git a/src/SymbolicInterpreter.cpp b/src/SymbolicInterpreter.cpp new file mode 100644 index 0000000..1d2b05f --- /dev/null +++ b/src/SymbolicInterpreter.cpp @@ -0,0 +1,101 @@ +#include "SymbolicInterpreter.h" + +#include +#include + +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); +} diff --git a/test/Makefile b/test/Makefile new file mode 100644 index 0000000..c100474 --- /dev/null +++ b/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} diff --git a/test/branch0.c b/test/branch0.c new file mode 100644 index 0000000..56e5100 --- /dev/null +++ b/test/branch0.c @@ -0,0 +1,20 @@ +#include + +#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; +} diff --git a/test/branch1.c b/test/branch1.c new file mode 100644 index 0000000..9ef71d2 --- /dev/null +++ b/test/branch1.c @@ -0,0 +1,18 @@ +#include + +#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; +} diff --git a/test/branch2.c b/test/branch2.c new file mode 100644 index 0000000..fe0003d --- /dev/null +++ b/test/branch2.c @@ -0,0 +1,18 @@ +#include + +#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; +} diff --git a/test/infeasable.c b/test/infeasable.c new file mode 100644 index 0000000..1fbf6f5 --- /dev/null +++ b/test/infeasable.c @@ -0,0 +1,22 @@ +#include + +#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 + +#include "../include/Runtime.h" + +int main() { + int x; + DSE_Input(x); + int y = x; + if (y == 1024) { + int z = 4 / (y - 1024); + } + return 0; +} diff --git a/test/simple1.c b/test/simple1.c new file mode 100644 index 0000000..2aedb79 --- /dev/null +++ b/test/simple1.c @@ -0,0 +1,16 @@ +#include + +#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; +} diff --git a/test/test b/test/test new file mode 100644 index 0000000..6accd3f --- /dev/null +++ b/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${?}" \ No newline at end of file