diff --git a/dse/build/CMakeFiles/InstrumentPass.dir/src/Instrument.cpp.o b/dse/build/CMakeFiles/InstrumentPass.dir/src/Instrument.cpp.o index e83ab9c..e773503 100644 Binary files a/dse/build/CMakeFiles/InstrumentPass.dir/src/Instrument.cpp.o and b/dse/build/CMakeFiles/InstrumentPass.dir/src/Instrument.cpp.o differ diff --git a/dse/build/CMakeFiles/dse.dir/compiler_depend.internal b/dse/build/CMakeFiles/dse.dir/compiler_depend.internal index fe73bd2..23e2afe 100644 --- a/dse/build/CMakeFiles/dse.dir/compiler_depend.internal +++ b/dse/build/CMakeFiles/dse.dir/compiler_depend.internal @@ -214,13 +214,17 @@ CMakeFiles/dse.dir/src/DSE.cpp.o /usr/include/x86_64-linux-gnu/bits/getopt_core.h /usr/include/x86_64-linux-gnu/bits/unistd_ext.h /usr/include/linux/close_range.h + /usr/include/c++/11/vector + /usr/include/c++/11/bits/stl_uninitialized.h + /usr/include/c++/11/bits/stl_vector.h + /usr/include/c++/11/bits/stl_bvector.h + /usr/include/c++/11/bits/vector.tcc /usr/local/include/z3++.h /usr/include/c++/11/cassert /usr/include/assert.h /usr/include/c++/11/sstream /usr/include/c++/11/bits/sstream.tcc /usr/include/c++/11/memory - /usr/include/c++/11/bits/stl_uninitialized.h /usr/include/c++/11/bits/stl_tempbuf.h /usr/include/c++/11/bits/stl_raw_storage_iter.h /usr/include/c++/11/bits/align.h @@ -244,10 +248,6 @@ CMakeFiles/dse.dir/src/DSE.cpp.o /usr/include/c++/11/backward/auto_ptr.h /usr/include/c++/11/pstl/glue_memory_defs.h /usr/include/c++/11/pstl/execution_defs.h - /usr/include/c++/11/vector - /usr/include/c++/11/bits/stl_vector.h - /usr/include/c++/11/bits/stl_bvector.h - /usr/include/c++/11/bits/vector.tcc /usr/local/include/z3.h /usr/lib/gcc/x86_64-linux-gnu/11/include/stdbool.h /usr/local/include/z3_macros.h @@ -543,4 +543,5 @@ CMakeFiles/dse.dir/src/Strategy.cpp.o /usr/include/c++/11/bits/algorithmfwd.h /usr/include/c++/11/bits/stl_heap.h /usr/include/c++/11/bits/uniform_int_dist.h + /usr/include/c++/11/iostream diff --git a/dse/build/CMakeFiles/dse.dir/compiler_depend.make b/dse/build/CMakeFiles/dse.dir/compiler_depend.make index 70fe232..4c437e7 100644 --- a/dse/build/CMakeFiles/dse.dir/compiler_depend.make +++ b/dse/build/CMakeFiles/dse.dir/compiler_depend.make @@ -213,13 +213,17 @@ CMakeFiles/dse.dir/src/DSE.cpp.o: ../src/DSE.cpp \ /usr/include/x86_64-linux-gnu/bits/getopt_core.h \ /usr/include/x86_64-linux-gnu/bits/unistd_ext.h \ /usr/include/linux/close_range.h \ + /usr/include/c++/11/vector \ + /usr/include/c++/11/bits/stl_uninitialized.h \ + /usr/include/c++/11/bits/stl_vector.h \ + /usr/include/c++/11/bits/stl_bvector.h \ + /usr/include/c++/11/bits/vector.tcc \ /usr/local/include/z3++.h \ /usr/include/c++/11/cassert \ /usr/include/assert.h \ /usr/include/c++/11/sstream \ /usr/include/c++/11/bits/sstream.tcc \ /usr/include/c++/11/memory \ - /usr/include/c++/11/bits/stl_uninitialized.h \ /usr/include/c++/11/bits/stl_tempbuf.h \ /usr/include/c++/11/bits/stl_raw_storage_iter.h \ /usr/include/c++/11/bits/align.h \ @@ -243,10 +247,6 @@ CMakeFiles/dse.dir/src/DSE.cpp.o: ../src/DSE.cpp \ /usr/include/c++/11/backward/auto_ptr.h \ /usr/include/c++/11/pstl/glue_memory_defs.h \ /usr/include/c++/11/pstl/execution_defs.h \ - /usr/include/c++/11/vector \ - /usr/include/c++/11/bits/stl_vector.h \ - /usr/include/c++/11/bits/stl_bvector.h \ - /usr/include/c++/11/bits/vector.tcc \ /usr/local/include/z3.h \ /usr/lib/gcc/x86_64-linux-gnu/11/include/stdbool.h \ /usr/local/include/z3_macros.h \ @@ -540,7 +540,8 @@ CMakeFiles/dse.dir/src/Strategy.cpp.o: ../src/Strategy.cpp \ /usr/include/c++/11/bits/stl_algo.h \ /usr/include/c++/11/bits/algorithmfwd.h \ /usr/include/c++/11/bits/stl_heap.h \ - /usr/include/c++/11/bits/uniform_int_dist.h + /usr/include/c++/11/bits/uniform_int_dist.h \ + /usr/include/c++/11/iostream ../src/Strategy.cpp: @@ -1077,22 +1078,30 @@ CMakeFiles/dse.dir/src/Strategy.cpp.o: ../src/Strategy.cpp \ /usr/include/x86_64-linux-gnu/bits/getopt_core.h: -/usr/include/c++/11/bits/align.h: - /usr/include/c++/11/vector: +/usr/include/c++/11/bits/align.h: + /usr/include/x86_64-linux-gnu/bits/unistd_ext.h: +/usr/include/c++/11/bits/stl_uninitialized.h: + +/usr/include/c++/11/backward/auto_ptr.h: + +/usr/include/x86_64-linux-gnu/bits/types/struct___jmp_buf_tag.h: + +/usr/include/x86_64-linux-gnu/bits/types/clockid_t.h: + +/usr/include/c++/11/bits/stl_bvector.h: + +/usr/include/c++/11/bits/vector.tcc: + /usr/include/c++/11/cassert: /usr/include/c++/11/sstream: /usr/include/c++/11/memory: -/usr/include/c++/11/bits/stl_uninitialized.h: - -/usr/include/c++/11/backward/auto_ptr.h: - /usr/include/c++/11/bits/stl_raw_storage_iter.h: /usr/include/c++/11/bits/uses_allocator.h: @@ -1109,14 +1118,6 @@ CMakeFiles/dse.dir/src/Strategy.cpp.o: ../src/Strategy.cpp \ /usr/include/c++/11/bits/shared_ptr_atomic.h: -/usr/include/x86_64-linux-gnu/bits/types/struct___jmp_buf_tag.h: - -/usr/include/x86_64-linux-gnu/bits/types/clockid_t.h: - -/usr/include/c++/11/bits/stl_bvector.h: - -/usr/include/c++/11/bits/vector.tcc: - /usr/include/x86_64-linux-gnu/bits/local_lim.h: /usr/lib/gcc/x86_64-linux-gnu/11/include/stdbool.h: diff --git a/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o b/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o index afc8419..80f28bb 100644 Binary files a/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o and b/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o differ diff --git a/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o.d b/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o.d index 4b5d52f..617a632 100644 --- a/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o.d +++ b/dse/build/CMakeFiles/dse.dir/src/DSE.cpp.o.d @@ -169,11 +169,14 @@ CMakeFiles/dse.dir/src/DSE.cpp.o: \ /usr/include/x86_64-linux-gnu/bits/getopt_posix.h \ /usr/include/x86_64-linux-gnu/bits/getopt_core.h \ /usr/include/x86_64-linux-gnu/bits/unistd_ext.h \ - /usr/include/linux/close_range.h /usr/local/include/z3++.h \ + /usr/include/linux/close_range.h /usr/include/c++/11/vector \ + /usr/include/c++/11/bits/stl_uninitialized.h \ + /usr/include/c++/11/bits/stl_vector.h \ + /usr/include/c++/11/bits/stl_bvector.h \ + /usr/include/c++/11/bits/vector.tcc /usr/local/include/z3++.h \ /usr/include/c++/11/cassert /usr/include/assert.h \ /usr/include/c++/11/sstream /usr/include/c++/11/bits/sstream.tcc \ - /usr/include/c++/11/memory /usr/include/c++/11/bits/stl_uninitialized.h \ - /usr/include/c++/11/bits/stl_tempbuf.h \ + /usr/include/c++/11/memory /usr/include/c++/11/bits/stl_tempbuf.h \ /usr/include/c++/11/bits/stl_raw_storage_iter.h \ /usr/include/c++/11/bits/align.h /usr/include/c++/11/bit \ /usr/include/c++/11/bits/uses_allocator.h \ @@ -191,10 +194,7 @@ CMakeFiles/dse.dir/src/DSE.cpp.o: \ /usr/include/c++/11/bits/atomic_lockfree_defines.h \ /usr/include/c++/11/backward/auto_ptr.h \ /usr/include/c++/11/pstl/glue_memory_defs.h \ - /usr/include/c++/11/pstl/execution_defs.h /usr/include/c++/11/vector \ - /usr/include/c++/11/bits/stl_vector.h \ - /usr/include/c++/11/bits/stl_bvector.h \ - /usr/include/c++/11/bits/vector.tcc /usr/local/include/z3.h \ + /usr/include/c++/11/pstl/execution_defs.h /usr/local/include/z3.h \ /usr/lib/gcc/x86_64-linux-gnu/11/include/stdbool.h \ /usr/local/include/z3_macros.h /usr/local/include/z3_api.h \ /usr/local/include/z3_ast_containers.h /usr/local/include/z3_algebraic.h \ diff --git a/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o b/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o index ae53282..b725694 100644 Binary files a/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o and b/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o differ diff --git a/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o.d b/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o.d index bd1fcf9..92bbcd8 100644 --- a/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o.d +++ b/dse/build/CMakeFiles/dse.dir/src/Strategy.cpp.o.d @@ -194,4 +194,4 @@ CMakeFiles/dse.dir/src/Strategy.cpp.o: \ /usr/include/c++/11/bits/erase_if.h /usr/include/c++/11/bits/stl_algo.h \ /usr/include/c++/11/bits/algorithmfwd.h \ /usr/include/c++/11/bits/stl_heap.h \ - /usr/include/c++/11/bits/uniform_int_dist.h + /usr/include/c++/11/bits/uniform_int_dist.h /usr/include/c++/11/iostream diff --git a/dse/build/CMakeFiles/runtime.dir/src/Runtime.cpp.o b/dse/build/CMakeFiles/runtime.dir/src/Runtime.cpp.o index 83969bf..f78f4b9 100644 Binary files a/dse/build/CMakeFiles/runtime.dir/src/Runtime.cpp.o and b/dse/build/CMakeFiles/runtime.dir/src/Runtime.cpp.o differ diff --git a/dse/build/CMakeFiles/runtime.dir/src/SymbolicInterpreter.cpp.o b/dse/build/CMakeFiles/runtime.dir/src/SymbolicInterpreter.cpp.o index b6824c8..a66297a 100644 Binary files a/dse/build/CMakeFiles/runtime.dir/src/SymbolicInterpreter.cpp.o and b/dse/build/CMakeFiles/runtime.dir/src/SymbolicInterpreter.cpp.o differ diff --git a/dse/build/InstrumentPass.so b/dse/build/InstrumentPass.so index 35b9f19..51b9c7f 100755 Binary files a/dse/build/InstrumentPass.so and b/dse/build/InstrumentPass.so differ diff --git a/dse/build/Testing/Temporary/LastTest.log b/dse/build/Testing/Temporary/LastTest.log index b6c83c4..e41d5a1 100644 --- a/dse/build/Testing/Temporary/LastTest.log +++ b/dse/build/Testing/Temporary/LastTest.log @@ -1,3 +1,3 @@ -Start testing: Jun 25 08:28 CST +Start testing: Jun 26 13:14 CST ---------------------------------------------------------- -End testing: Jun 25 08:28 CST +End testing: Jun 26 13:14 CST diff --git a/dse/build/dse b/dse/build/dse index b24a101..78d19b3 100755 Binary files a/dse/build/dse and b/dse/build/dse differ diff --git a/dse/build/libruntime.so b/dse/build/libruntime.so index 2fa1b8d..89e8972 100755 Binary files a/dse/build/libruntime.so and b/dse/build/libruntime.so differ diff --git a/dse/include/Instrument.h b/dse/include/Instrument.h index 93dcb38..f1170ae 100644 --- a/dse/include/Instrument.h +++ b/dse/include/Instrument.h @@ -15,7 +15,7 @@ namespace instrument { #define SUB 15 /// - #define MUL 17 /// * #define SDIV 20 /// / -#define SREM 23 +#define SREM 23 /// % #define ALLOCA 31 #define LOAD 32 #define STORE 33 @@ -28,6 +28,7 @@ namespace instrument { #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__" diff --git a/dse/include/Strategy.h b/dse/include/Strategy.h index 5193d8f..6afc3d2 100644 --- a/dse/include/Strategy.h +++ b/dse/include/Strategy.h @@ -1,3 +1,4 @@ #include "z3++.h" +void recordBranches(z3::expr_vector &OldVec); void searchStrategy(z3::expr_vector &OldVec); diff --git a/dse/src/DSE.cpp b/dse/src/DSE.cpp index 9eb29d2..3d63869 100644 --- a/dse/src/DSE.cpp +++ b/dse/src/DSE.cpp @@ -2,7 +2,7 @@ #include #include #include - +#include #include "z3++.h" #include "Strategy.h" @@ -19,8 +19,8 @@ void storeInput() { const z3::func_decl E = Model[I]; z3::expr Input = Model.get_const_interp(E); if (Input.kind() == Z3_NUMERAL_AST) { - I = Input.get_numeral_int(); - OS << E.name() << "," << I << std::endl; + int res = Input.get_numeral_int(); + OS << E.name() << "," << res << std::endl; } } } @@ -40,10 +40,12 @@ void printNewPathCondition(z3::expr_vector &Vec) { void generateInput() { /// 获取 formula.smt2 中的内容 z3::expr_vector Vec = Ctx.parse_file(FormulaFile); - std::cout<<"Vec: "<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)}, @@ -76,7 +82,7 @@ bool Instrument::runOnFunction(Function &F) { auto FuncRegister = F.getParent()->getOrInsertFunction(DSE_Register, FuncRegisterType); for(auto & B : F){ - if(B.getName().startswith("if")){ + 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++)}) @@ -97,8 +103,7 @@ bool Instrument::runOnFunction(Function &F) { break; case BR: if(dyn_cast(&bb)->isConditional()){ - errs() << getRegisterID(bb.getOperand(2)) <<" "<< getBranchID(bb.getOperand(1))<<'\n'; - + //errs() << getRegisterID(bb.getOperand(2)) <<" "<< getBranchID(bb.getOperand(1))<<'\n'; CallInst::Create(FuncLabel, {ConstantInt::get(Type::getInt32Ty(context), getRegisterID(bb.getOperand(0))), @@ -113,13 +118,20 @@ bool Instrument::runOnFunction(Function &F) { 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())}) @@ -200,8 +212,6 @@ bool Instrument::runOnFunction(Function &F) { } } } - - return false; } diff --git a/dse/src/Runtime.cpp b/dse/src/Runtime.cpp index 93b43c5..1114c6a 100644 --- a/dse/src/Runtime.cpp +++ b/dse/src/Runtime.cpp @@ -9,6 +9,7 @@ #define SUB 15 /// - #define MUL 17 /// * #define SDIV 20 /// / +#define SREM 23 /// % #define ICMP_EQ 32 ///< equal #define ICMP_NE 33 ///< not equal @@ -41,7 +42,6 @@ extern "C" void __DSE_Store__(int *X) { SI.getStack().pop(); if(e.to_string().at(0) == 'R'){ e = SI.getMemory().at(e); - cout << e << endl; } auto address = Address(X); SI.getMemory().insert(make_pair(address, e)); @@ -52,6 +52,7 @@ 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){ @@ -59,10 +60,18 @@ extern "C" void __DSE_Label__(int RID, int BID, int label){ auto address = Address(BID); expr t = SI.getContext().bool_val(true); expr f = SI.getContext().bool_val(false); - if(label) + if(label){ SI.getMemory().insert(make_pair(address, el == t)); - else + 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) { @@ -100,6 +109,7 @@ extern "C" void __DSE_ICmp__(int R, int Op) { } 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) { @@ -127,9 +137,13 @@ extern "C" void __DSE_BinOp__(int R, int Op) { 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; } diff --git a/dse/src/Strategy.cpp b/dse/src/Strategy.cpp index 4470dea..fa05f19 100644 --- a/dse/src/Strategy.cpp +++ b/dse/src/Strategy.cpp @@ -1,6 +1,68 @@ #include "Strategy.h" +#include -/* +static const char *NOT = "not"; +std::vector Branches; +/** * Implement your search strategy. */ -void searchStrategy(z3::expr_vector &OldVec) { /* Add your code here */ } + +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()); + } + } + /* + for(const auto &E : Branches){ + printf("%s\n", E.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; + } + //printf("e%d:%s\n\n",i, e.to_string().c_str()); + if(e.to_string().substr(1, 3) != NOT){ + std::string newExpr = e.to_string(); + //printf("expr0:%s\n", newExpr.c_str()); + 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"); + } + //printf("expr1:%s\n", newExpr.c_str()); + if(std::find(Branches.begin(), Branches.end(), newExpr) == Branches.end()){ + //printf("newpath\n"); + OldVec.pop_back(); + OldVec.push_back(not e); + //printf("new\n"); + /* + for(auto EX : OldVec){ + printf("%s\n", EX.to_string().c_str()); + } + */ + } else{ + //printf("back\n"); + OldVec.pop_back(); + searchStrategy(OldVec); + } + } + else { + //printf("unsat\n"); + OldVec.pop_back(); + searchStrategy(OldVec); + } +} diff --git a/dse/src/SymbolicInterpreter.cpp b/dse/src/SymbolicInterpreter.cpp index 12b8fe9..601d43f 100644 --- a/dse/src/SymbolicInterpreter.cpp +++ b/dse/src/SymbolicInterpreter.cpp @@ -57,7 +57,7 @@ extern "C" void __DSE_Exit__() { for (auto &E : SI.getPathCondition()) { std::string BID = "B" + std::to_string(E.first); Solver.add(E.second); - Branch << BID << "\n"; + Branch << E.second << "\n"; } std::ofstream Smt2(FormulaFile); Smt2 << Solver.to_smt2(); @@ -87,6 +87,10 @@ extern "C" void __DSE_Input__(int *X, int 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) diff --git a/dse/test/branch.txt b/dse/test/branch.txt index 65923b9..343556a 100644 --- a/dse/test/branch.txt +++ b/dse/test/branch.txt @@ -1 +1,11 @@ -B5 +(= (< 0 X0) true) +(= (< (+ 0 1) X0) true) +(= (< (+ 0 1 1) X0) true) +(= (< (+ 0 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false) +(= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) false) diff --git a/dse/test/branch0 b/dse/test/branch0 index 3395a58..56d3f14 100755 Binary files a/dse/test/branch0 and b/dse/test/branch0 differ diff --git a/dse/test/branch0.c b/dse/test/branch0.c index b71bff3..646e6db 100644 --- a/dse/test/branch0.c +++ b/dse/test/branch0.c @@ -16,6 +16,11 @@ int main() { x = x / (y-z); } } + else { + if(x == 0){ + x = 0; + } + } return 0; } diff --git a/dse/test/branch0.instrumented.ll b/dse/test/branch0.instrumented.ll index cb4ce12..4f2cd72 100644 --- a/dse/test/branch0.instrumented.ll +++ b/dse/test/branch0.instrumented.ll @@ -28,10 +28,11 @@ entry: call void @__DSE_ICmp__(i32 4, i32 32) call void @__DSE_Label__(i32 4, i32 5, i32 1) call void @__DSE_Label__(i32 4, i32 6, i32 0) - br i1 %cmp, label %if.then, label %if.end3 + call void @__DSE_Loop__(i32 1) + br i1 %cmp, label %if.then, label %if.else if.then: ; preds = %entry - call void @__DSE_Branch__(i32 5, i32 1) + call void @__DSE_Branch__(i32 5, i32 0) %1 = load i32, i32* %y, align 4 call void @__DSE_Load__(i32 7, i32* %y) %2 = load i32, i32* %z, align 4 @@ -42,10 +43,11 @@ if.then: ; preds = %entry call void @__DSE_ICmp__(i32 9, i32 32) call void @__DSE_Label__(i32 9, i32 10, i32 1) call void @__DSE_Label__(i32 9, i32 11, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp1, label %if.then2, label %if.end if.then2: ; preds = %if.then - call void @__DSE_Branch__(i32 10, i32 3) + call void @__DSE_Branch__(i32 10, i32 1) %3 = load i32, i32* %x, align 4 call void @__DSE_Load__(i32 12, i32* %x) %4 = load i32, i32* %y, align 4 @@ -63,14 +65,42 @@ if.then2: ; preds = %if.then store i32 %div, i32* %x, align 4 call void @__DSE_Register__(i32 16) call void @__DSE_Store__(i32* %x) + call void @__DSE_Loop__(i32 0) br label %if.end if.end: ; preds = %if.then2, %if.then - call void @__DSE_Branch__(i32 11, i32 4) - br label %if.end3 + call void @__DSE_Branch__(i32 11, i32 2) + call void @__DSE_Loop__(i32 0) + br label %if.end6 + +if.else: ; preds = %entry + call void @__DSE_Branch__(i32 6, i32 3) + %6 = load i32, i32* %x, align 4 + call void @__DSE_Load__(i32 17, i32* %x) + %cmp3 = icmp eq i32 %6, 0 + call void @__DSE_Const__(i32 0) + call void @__DSE_Register__(i32 17) + call void @__DSE_ICmp__(i32 18, i32 32) + call void @__DSE_Label__(i32 18, i32 19, i32 1) + call void @__DSE_Label__(i32 18, i32 20, i32 0) + call void @__DSE_Loop__(i32 1) + br i1 %cmp3, label %if.then4, label %if.end5 + +if.then4: ; preds = %if.else + call void @__DSE_Branch__(i32 19, i32 4) + store i32 0, i32* %x, align 4 + call void @__DSE_Const__(i32 0) + call void @__DSE_Store__(i32* %x) + call void @__DSE_Loop__(i32 0) + br label %if.end5 -if.end3: ; preds = %if.end, %entry - call void @__DSE_Branch__(i32 6, i32 5) +if.end5: ; preds = %if.then4, %if.else + call void @__DSE_Branch__(i32 20, i32 5) + call void @__DSE_Loop__(i32 0) + br label %if.end6 + +if.end6: ; preds = %if.end5, %if.end + call void @__DSE_Branch__(i32 21, i32 6) ret i32 0 } @@ -88,6 +118,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32) diff --git a/dse/test/branch0.ll b/dse/test/branch0.ll index 96172b2..8e68374 100644 --- a/dse/test/branch0.ll +++ b/dse/test/branch0.ll @@ -16,7 +16,7 @@ entry: call void @__DSE_Input__(i32* noundef %z, i32 noundef 2) %0 = load i32, i32* %x, align 4 %cmp = icmp eq i32 %0, 1 - br i1 %cmp, label %if.then, label %if.end3 + br i1 %cmp, label %if.then, label %if.else if.then: ; preds = %entry %1 = load i32, i32* %y, align 4 @@ -34,9 +34,21 @@ if.then2: ; preds = %if.then br label %if.end if.end: ; preds = %if.then2, %if.then - br label %if.end3 + br label %if.end6 -if.end3: ; preds = %if.end, %entry +if.else: ; preds = %entry + %6 = load i32, i32* %x, align 4 + %cmp3 = icmp eq i32 %6, 0 + br i1 %cmp3, label %if.then4, label %if.end5 + +if.then4: ; preds = %if.else + store i32 0, i32* %x, align 4 + br label %if.end5 + +if.end5: ; preds = %if.then4, %if.else + br label %if.end6 + +if.end6: ; preds = %if.end5, %if.end ret i32 0 } diff --git a/dse/test/branch1 b/dse/test/branch1 index c671558..7740e9a 100755 Binary files a/dse/test/branch1 and b/dse/test/branch1 differ diff --git a/dse/test/branch1.instrumented.ll b/dse/test/branch1.instrumented.ll index 8c11ed0..4cba781 100644 --- a/dse/test/branch1.instrumented.ll +++ b/dse/test/branch1.instrumented.ll @@ -30,9 +30,11 @@ entry: call void @__DSE_ICmp__(i32 5, i32 32) call void @__DSE_Label__(i32 5, i32 6, i32 1) call void @__DSE_Label__(i32 5, i32 7, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp, label %land.lhs.true, label %if.else land.lhs.true: ; preds = %entry + call void @__DSE_Branch__(i32 6, i32 0) %2 = load i32, i32* %y, align 4 call void @__DSE_Load__(i32 8, i32* %y) %3 = load i32, i32* %z, align 4 @@ -43,6 +45,7 @@ land.lhs.true: ; preds = %entry call void @__DSE_ICmp__(i32 10, i32 32) call void @__DSE_Label__(i32 10, i32 11, i32 1) call void @__DSE_Label__(i32 10, i32 7, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp1, label %if.then, label %if.else if.then: ; preds = %land.lhs.true @@ -64,6 +67,7 @@ if.then: ; preds = %land.lhs.true store i32 %div, i32* %x, align 4 call void @__DSE_Register__(i32 16) call void @__DSE_Store__(i32* %x) + call void @__DSE_Loop__(i32 0) br label %if.end if.else: ; preds = %land.lhs.true, %entry @@ -71,6 +75,7 @@ if.else: ; preds = %land.lhs.true, %ent store i32 1, i32* %x, align 4 call void @__DSE_Const__(i32 1) call void @__DSE_Store__(i32* %x) + call void @__DSE_Loop__(i32 0) br label %if.end if.end: ; preds = %if.else, %if.then @@ -92,6 +97,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32) diff --git a/dse/test/branch2 b/dse/test/branch2 index 06eb2c5..9a4ca30 100755 Binary files a/dse/test/branch2 and b/dse/test/branch2 differ diff --git a/dse/test/branch2.c b/dse/test/branch2.c index fe0003d..5e911de 100644 --- a/dse/test/branch2.c +++ b/dse/test/branch2.c @@ -10,9 +10,19 @@ int main() { int z; DSE_Input(z); + if (x > y && y > z && z == 0) { x = x / z; } - + + /* + if(x>y){ + if(y>z){ + if(z==0){ + x = x/z; + } + } + } + */ return 0; } diff --git a/dse/test/branch2.instrumented.ll b/dse/test/branch2.instrumented.ll index 79cb000..1915dc1 100644 --- a/dse/test/branch2.instrumented.ll +++ b/dse/test/branch2.instrumented.ll @@ -30,9 +30,11 @@ entry: call void @__DSE_ICmp__(i32 5, i32 38) call void @__DSE_Label__(i32 5, i32 6, i32 1) call void @__DSE_Label__(i32 5, i32 7, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp, label %land.lhs.true, label %if.end land.lhs.true: ; preds = %entry + call void @__DSE_Branch__(i32 6, i32 0) %2 = load i32, i32* %y, align 4 call void @__DSE_Load__(i32 8, i32* %y) %3 = load i32, i32* %z, align 4 @@ -43,9 +45,11 @@ land.lhs.true: ; preds = %entry call void @__DSE_ICmp__(i32 10, i32 38) call void @__DSE_Label__(i32 10, i32 11, i32 1) call void @__DSE_Label__(i32 10, i32 7, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp1, label %land.lhs.true2, label %if.end land.lhs.true2: ; preds = %land.lhs.true + call void @__DSE_Branch__(i32 11, i32 1) %4 = load i32, i32* %z, align 4 call void @__DSE_Load__(i32 12, i32* %z) %cmp3 = icmp eq i32 %4, 0 @@ -54,10 +58,11 @@ land.lhs.true2: ; preds = %land.lhs.true call void @__DSE_ICmp__(i32 13, i32 32) call void @__DSE_Label__(i32 13, i32 14, i32 1) call void @__DSE_Label__(i32 13, i32 7, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp3, label %if.then, label %if.end if.then: ; preds = %land.lhs.true2 - call void @__DSE_Branch__(i32 14, i32 1) + call void @__DSE_Branch__(i32 14, i32 2) %5 = load i32, i32* %x, align 4 call void @__DSE_Load__(i32 15, i32* %x) %6 = load i32, i32* %z, align 4 @@ -69,10 +74,11 @@ if.then: ; preds = %land.lhs.true2 store i32 %div, i32* %x, align 4 call void @__DSE_Register__(i32 17) call void @__DSE_Store__(i32* %x) + call void @__DSE_Loop__(i32 0) br label %if.end if.end: ; preds = %if.then, %land.lhs.true2, %land.lhs.true, %entry - call void @__DSE_Branch__(i32 7, i32 2) + call void @__DSE_Branch__(i32 7, i32 3) ret i32 0 } @@ -90,6 +96,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32) diff --git a/dse/test/formula.smt2 b/dse/test/formula.smt2 index a82e12c..6dd5917 100644 --- a/dse/test/formula.smt2 +++ b/dse/test/formula.smt2 @@ -2,6 +2,61 @@ (set-info :status unknown) (declare-fun X0 () Int) (assert - (let (($x14 (= X0 1))) - (= $x14 false))) + (= (< 0 X0) true)) +(assert + (= (< (+ 0 1) X0) true)) +(assert + (= (< (+ (+ 0 1) 1) X0) true)) +(assert + (= (< (+ (+ (+ 0 1) 1) 1) X0) true)) +(assert + (= (< (+ (+ (+ (+ 0 1) 1) 1) 1) X0) true)) +(assert + (= (< (+ (+ (+ (+ (+ 0 1) 1) 1) 1) 1) X0) true)) +(assert + (let ((?x18 (+ 0 1))) + (let ((?x22 (+ ?x18 1))) + (let ((?x26 (+ ?x22 1))) + (let ((?x30 (+ ?x26 1))) + (let ((?x34 (+ ?x30 1))) + (let ((?x38 (+ ?x34 1))) + (= (< ?x38 X0) true)))))))) +(assert + (let ((?x18 (+ 0 1))) + (let ((?x22 (+ ?x18 1))) + (let ((?x26 (+ ?x22 1))) + (let ((?x30 (+ ?x26 1))) + (let ((?x34 (+ ?x30 1))) + (let ((?x38 (+ ?x34 1))) + (let ((?x42 (+ ?x38 1))) + (= (< ?x42 X0) true))))))))) +(assert + (let ((?x18 (+ 0 1))) + (let ((?x22 (+ ?x18 1))) + (let ((?x26 (+ ?x22 1))) + (let ((?x30 (+ ?x26 1))) + (let ((?x34 (+ ?x30 1))) + (let ((?x38 (+ ?x34 1))) + (let ((?x42 (+ ?x38 1))) + (let ((?x46 (+ ?x42 1))) + (= (< ?x46 X0) true)))))))))) +(assert + (let ((?x18 (+ 0 1))) + (let ((?x22 (+ ?x18 1))) + (let ((?x26 (+ ?x22 1))) + (let ((?x30 (+ ?x26 1))) + (let ((?x34 (+ ?x30 1))) + (let ((?x38 (+ ?x34 1))) + (let ((?x42 (+ ?x38 1))) + (let ((?x46 (+ ?x42 1))) + (let ((?x50 (+ ?x46 1))) + (let (($x51 (< ?x50 X0))) + (= $x51 false)))))))))))) +(assert + (let ((?x36 (* (* (* (* (* (* (* 1 2) 2) 2) 2) 2) 2) 2))) + (let ((?x40 (* ?x36 2))) + (let ((?x44 (* ?x40 2))) + (let ((?x53 (mod ?x44 1022))) + (let (($x54 (= ?x53 2))) + (= $x54 false))))))) (check-sat) diff --git a/dse/test/infeasable b/dse/test/infeasable index 4c5647c..2c1fc96 100755 Binary files a/dse/test/infeasable and b/dse/test/infeasable differ diff --git a/dse/test/infeasable.c b/dse/test/infeasable.c index fe1f801..833a8df 100644 --- a/dse/test/infeasable.c +++ b/dse/test/infeasable.c @@ -7,7 +7,7 @@ int main() { DSE_Input(x); //c is a product of two primes - int c = 181 * 191; + int c = 1022; int y = 1; @@ -15,7 +15,7 @@ int main() { y *= 2; } - if (y % c == 17) { + if (y % c == 2) { x = x / (c-c); } return 0; diff --git a/dse/test/infeasable.instrumented.ll b/dse/test/infeasable.instrumented.ll index 598bc85..f9d8177 100644 --- a/dse/test/infeasable.instrumented.ll +++ b/dse/test/infeasable.instrumented.ll @@ -20,8 +20,8 @@ entry: call void @__DSE_Const__(i32 0) call void @__DSE_Store__(i32* %retval) call void @__DSE_Input__(i32* noundef %x, i32 noundef 0) - store i32 34571, i32* %c, align 4 - call void @__DSE_Const__(i32 34571) + store i32 1022, i32* %c, align 4 + call void @__DSE_Const__(i32 1022) call void @__DSE_Store__(i32* %c) store i32 1, i32* %y, align 4 call void @__DSE_Const__(i32 1) @@ -29,82 +29,95 @@ entry: store i32 0, i32* %i, align 4 call void @__DSE_Const__(i32 0) call void @__DSE_Store__(i32* %i) + call void @__DSE_Loop__(i32 0) br label %for.cond for.cond: ; preds = %for.inc, %entry + call void @__DSE_Branch__(i32 4, i32 0) %0 = load i32, i32* %i, align 4 - call void @__DSE_Load__(i32 4, i32* %i) + call void @__DSE_Load__(i32 5, i32* %i) %1 = load i32, i32* %x, align 4 - call void @__DSE_Load__(i32 5, i32* %x) + call void @__DSE_Load__(i32 6, i32* %x) %cmp = icmp slt i32 %0, %1 + call void @__DSE_Register__(i32 6) call void @__DSE_Register__(i32 5) - call void @__DSE_Register__(i32 4) - call void @__DSE_ICmp__(i32 6, i32 40) - call void @__DSE_Label__(i32 6, i32 7, i32 1) - call void @__DSE_Label__(i32 6, i32 8, i32 0) + call void @__DSE_ICmp__(i32 7, i32 40) + call void @__DSE_Label__(i32 7, i32 8, i32 1) + call void @__DSE_Label__(i32 7, i32 9, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp, label %for.body, label %for.end for.body: ; preds = %for.cond + call void @__DSE_Branch__(i32 8, i32 1) %2 = load i32, i32* %y, align 4 - call void @__DSE_Load__(i32 9, i32* %y) + call void @__DSE_Load__(i32 10, i32* %y) %mul = mul nsw i32 %2, 2 call void @__DSE_Const__(i32 2) - call void @__DSE_Register__(i32 9) - call void @__DSE_BinOp__(i32 10, i32 17) - store i32 %mul, i32* %y, align 4 call void @__DSE_Register__(i32 10) + call void @__DSE_BinOp__(i32 11, i32 17) + store i32 %mul, i32* %y, align 4 + call void @__DSE_Register__(i32 11) call void @__DSE_Store__(i32* %y) + call void @__DSE_Loop__(i32 0) br label %for.inc for.inc: ; preds = %for.body + call void @__DSE_Branch__(i32 12, i32 2) %3 = load i32, i32* %i, align 4 - call void @__DSE_Load__(i32 11, i32* %i) + call void @__DSE_Load__(i32 13, i32* %i) %inc = add nsw i32 %3, 1 call void @__DSE_Const__(i32 1) - call void @__DSE_Register__(i32 11) - call void @__DSE_BinOp__(i32 12, i32 13) + call void @__DSE_Register__(i32 13) + call void @__DSE_BinOp__(i32 14, i32 13) store i32 %inc, i32* %i, align 4 - call void @__DSE_Register__(i32 12) + call void @__DSE_Register__(i32 14) call void @__DSE_Store__(i32* %i) + call void @__DSE_Loop__(i32 0) br label %for.cond, !llvm.loop !4 for.end: ; preds = %for.cond + call void @__DSE_Branch__(i32 9, i32 3) %4 = load i32, i32* %y, align 4 - call void @__DSE_Load__(i32 13, i32* %y) + call void @__DSE_Load__(i32 15, i32* %y) %5 = load i32, i32* %c, align 4 - call void @__DSE_Load__(i32 14, i32* %c) + call void @__DSE_Load__(i32 16, i32* %c) %rem = srem i32 %4, %5 - %cmp1 = icmp eq i32 %rem, 17 - call void @__DSE_Const__(i32 17) call void @__DSE_Register__(i32 16) - call void @__DSE_ICmp__(i32 15, i32 32) - call void @__DSE_Label__(i32 15, i32 17, i32 1) - call void @__DSE_Label__(i32 15, i32 18, i32 0) + call void @__DSE_Register__(i32 15) + call void @__DSE_BinOp__(i32 17, i32 23) + %cmp1 = icmp eq i32 %rem, 2 + call void @__DSE_Const__(i32 2) + call void @__DSE_Register__(i32 17) + call void @__DSE_ICmp__(i32 18, i32 32) + call void @__DSE_Label__(i32 18, i32 19, i32 1) + call void @__DSE_Label__(i32 18, i32 20, i32 0) + call void @__DSE_Loop__(i32 1) br i1 %cmp1, label %if.then, label %if.end if.then: ; preds = %for.end - call void @__DSE_Branch__(i32 17, i32 2) + call void @__DSE_Branch__(i32 19, i32 4) %6 = load i32, i32* %x, align 4 - call void @__DSE_Load__(i32 19, i32* %x) + call void @__DSE_Load__(i32 21, i32* %x) %7 = load i32, i32* %c, align 4 - call void @__DSE_Load__(i32 20, i32* %c) + call void @__DSE_Load__(i32 22, i32* %c) %8 = load i32, i32* %c, align 4 - call void @__DSE_Load__(i32 21, i32* %c) + call void @__DSE_Load__(i32 23, i32* %c) %sub = sub nsw i32 %7, %8 - call void @__DSE_Register__(i32 21) - call void @__DSE_Register__(i32 20) - call void @__DSE_BinOp__(i32 22, i32 15) - %div = sdiv i32 %6, %sub + call void @__DSE_Register__(i32 23) call void @__DSE_Register__(i32 22) - call void @__DSE_Register__(i32 19) - call void @__DSE_BinOp__(i32 23, i32 20) + call void @__DSE_BinOp__(i32 24, i32 15) + %div = sdiv i32 %6, %sub + call void @__DSE_Register__(i32 24) + call void @__DSE_Register__(i32 21) + call void @__DSE_BinOp__(i32 25, i32 20) store i32 %div, i32* %x, align 4 - call void @__DSE_Register__(i32 23) + call void @__DSE_Register__(i32 25) call void @__DSE_Store__(i32* %x) + call void @__DSE_Loop__(i32 0) br label %if.end if.end: ; preds = %if.then, %for.end - call void @__DSE_Branch__(i32 18, i32 3) + call void @__DSE_Branch__(i32 20, i32 5) ret i32 0 } @@ -122,6 +135,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32) diff --git a/dse/test/infeasable.ll b/dse/test/infeasable.ll index a444d27..f338472 100644 --- a/dse/test/infeasable.ll +++ b/dse/test/infeasable.ll @@ -13,7 +13,7 @@ entry: %i = alloca i32, align 4 store i32 0, i32* %retval, align 4 call void @__DSE_Input__(i32* noundef %x, i32 noundef 0) - store i32 34571, i32* %c, align 4 + store i32 1022, i32* %c, align 4 store i32 1, i32* %y, align 4 store i32 0, i32* %i, align 4 br label %for.cond @@ -40,7 +40,7 @@ for.end: ; preds = %for.cond %4 = load i32, i32* %y, align 4 %5 = load i32, i32* %c, align 4 %rem = srem i32 %4, %5 - %cmp1 = icmp eq i32 %rem, 17 + %cmp1 = icmp eq i32 %rem, 2 br i1 %cmp1, label %if.then, label %if.end if.then: ; preds = %for.end diff --git a/dse/test/input.txt b/dse/test/input.txt index b91a16e..93e313e 100644 --- a/dse/test/input.txt +++ b/dse/test/input.txt @@ -1 +1 @@ -X0,2 +X0,10 diff --git a/dse/test/log.txt b/dse/test/log.txt index d596b89..f28af94 100644 --- a/dse/test/log.txt +++ b/dse/test/log.txt @@ -1,23 +1,53 @@ === Inputs === -X0 : 1850737439 -X1 : 1423391991 -X2 : 1736296805 +X0 : 9 === Symbolic Memory === -140723196736720 : X2 -140723196736724 : X1 -140723196736728 : X0 -140723196736732 : 0 -R0 : 1270725261 +140722793318076 : (+ 0 1 1 1 1 1 1 1 1 1) +140722793318080 : (* 1 2 2 2 2 2 2 2 2 2) +140722793318084 : 1022 +140722793318088 : X0 +140722793318092 : 0 +R0 : 2124147437 R1 : 32764 -R2 : (- 1406716656) -R3 : X0 -R4 : (= X0 1) -R5 : (= (= X0 1) true) -R6 : (= (= X0 1) false) +R2 : (- 1810135296) +R3 : 32764 +R5 : (+ 0 1 1 1 1 1 1 1 1 1) +R6 : X0 +R7 : (< (+ 0 1 1 1 1 1 1 1 1 1) X0) +R8 : (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) true) +R9 : (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false) +R10 : (* 1 2 2 2 2 2 2 2 2) +R11 : (* 1 2 2 2 2 2 2 2 2 2) +R13 : (+ 0 1 1 1 1 1 1 1 1) +R14 : (+ 0 1 1 1 1 1 1 1 1 1) +R15 : (* 1 2 2 2 2 2 2 2 2 2) +R16 : 1022 +R17 : (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) +R18 : (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) +R19 : (= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) true) +R20 : (= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) false) === Path Condition === -B5 : (= (= X0 1) false) +B1 : (= (< 0 X0) true) +B1 : (= (< (+ 0 1) X0) true) +B1 : (= (< (+ 0 1 1) X0) true) +B1 : (= (< (+ 0 1 1 1) X0) true) +B1 : (= (< (+ 0 1 1 1 1) X0) true) +B1 : (= (< (+ 0 1 1 1 1 1) X0) true) +B1 : (= (< (+ 0 1 1 1 1 1 1) X0) true) +B1 : (= (< (+ 0 1 1 1 1 1 1 1) X0) true) +B1 : (= (< (+ 0 1 1 1 1 1 1 1 1) X0) true) +B3 : (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false) +B5 : (= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) false) === New Path Condition === -(= (= X0 1) false) +(= (< 0 X0) true) +(= (< (+ 0 1) X0) true) +(= (< (+ 0 1 1) X0) true) +(= (< (+ 0 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1 1) X0) true) +(= (< (+ 0 1 1 1 1 1 1 1 1) X0) true) +(not (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false)) diff --git a/dse/test/simple0.instrumented.ll b/dse/test/simple0.instrumented.ll index 65a1fea..04d969d 100644 --- a/dse/test/simple0.instrumented.ll +++ b/dse/test/simple0.instrumented.ll @@ -43,6 +43,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32) diff --git a/dse/test/simple1.instrumented.ll b/dse/test/simple1.instrumented.ll index a1f3071..6a1141d 100644 --- a/dse/test/simple1.instrumented.ll +++ b/dse/test/simple1.instrumented.ll @@ -76,6 +76,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32) diff --git a/dse/test/simple2.instrumented.ll b/dse/test/simple2.instrumented.ll index 48ab1b1..02e924f 100644 --- a/dse/test/simple2.instrumented.ll +++ b/dse/test/simple2.instrumented.ll @@ -47,6 +47,8 @@ declare void @__DSE_ICmp__(i32, i32) declare void @__DSE_Label__(i32, i32, i32) +declare void @__DSE_Loop__(i32) + declare void @__DSE_Branch__(i32, i32) declare void @__DSE_BinOp__(i32, i32)