39 using namespace SVFUtil;
44 "symbolic abstraction test",
50 "abstract execution basic function test",
68 outs() <<
"hello print\n";
74 auto start_time = std::chrono::high_resolution_clock::now();
76 auto end_time = std::chrono::high_resolution_clock::now();
77 auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
78 end_time - start_time);
79 outs() <<
"running time of RSY : " << duration.count()
86 auto start_time = std::chrono::high_resolution_clock::now();
88 auto end_time = std::chrono::high_resolution_clock::now();
89 auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
90 end_time - start_time);
91 outs() <<
"running time of Bilateral: " << duration.count()
98 auto start_time = std::chrono::high_resolution_clock::now();
100 auto end_time = std::chrono::high_resolution_clock::now();
101 auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
102 end_time - start_time);
103 outs() <<
"running time of BS : " << duration.count()
104 <<
" microseconds\n";
110 outs() <<
sucMsg(
"\t SUCCESS :") <<
"test1_1 start\n";
115 relation[0] = getContext().int_const(
"0");
118 getContext().int_const(
"1") == getContext().int_const(
"0") + 1;
123 assert(res ==
Set<u32_t>({0, 1}) &&
"inconsistency occurs");
126 const Z3Expr& relExpr = relation[1];
128 const Z3Expr& phi = (relExpr && initExpr).simplify();
133 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
136 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
144 outs() <<
"test1_2 start\n";
148 relation[0] = getContext().int_const(
"0");
152 getContext().int_const(
"1") == getContext().int_const(
"0") * 2;
158 assert(res ==
Set<u32_t>({0, 1}) &&
"inconsistency occurs");
161 const Z3Expr& relExpr = relation[1];
163 const Z3Expr& phi = (relExpr && initExpr).simplify();
168 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
171 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
179 outs() <<
"test2_1 start\n";
183 relation[0] = getContext().int_const(
"0");
187 getContext().int_const(
"1") == getContext().int_const(
"0");
190 relation[2] = getContext().int_const(
"2") ==
191 getContext().int_const(
"1") - getContext().int_const(
"0");
192 itv[2] = itv[1].getInterval() - itv[0].getInterval();
196 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
199 const Z3Expr& relExpr = relation[2] && relation[1];
201 const Z3Expr& phi = (relExpr && initExpr).simplify();
206 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
209 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
221 outs() <<
"test2_2 start\n";
225 relation[0] = getContext().int_const(
"0");
229 getContext().int_const(
"1") == getContext().int_const(
"0");
232 relation[2] = getContext().int_const(
"2") ==
233 getContext().int_const(
"1") - getContext().int_const(
"0");
234 itv[2] = itv[1].getInterval() - itv[0].getInterval();
239 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
242 const Z3Expr& relExpr = relation[2] && relation[1];
244 const Z3Expr& phi = (relExpr && initExpr).simplify();
249 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
252 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
264 outs() <<
"test2_3 start\n";
268 relation[0] = getContext().int_const(
"0");
272 getContext().int_const(
"1") == getContext().int_const(
"0");
275 relation[2] = getContext().int_const(
"2") ==
276 getContext().int_const(
"1") - getContext().int_const(
"0");
277 itv[2] = itv[1].getInterval() - itv[0].getInterval();
282 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
285 const Z3Expr& relExpr = relation[2] && relation[1];
287 const Z3Expr& phi = (relExpr && initExpr).simplify();
292 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
295 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
307 outs() <<
"test2_4 start\n";
311 relation[0] = getContext().int_const(
"0");
315 getContext().int_const(
"1") == getContext().int_const(
"0");
318 relation[2] = getContext().int_const(
"2") ==
319 getContext().int_const(
"1") - getContext().int_const(
"0");
320 itv[2] = itv[1].getInterval() - itv[0].getInterval();
325 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
328 const Z3Expr& relExpr = relation[2] && relation[1];
330 const Z3Expr& phi = (relExpr && initExpr).simplify();
335 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
338 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
350 outs() <<
"test2_5 start\n";
354 relation[0] = getContext().int_const(
"0");
358 getContext().int_const(
"1") == getContext().int_const(
"0");
361 relation[2] = getContext().int_const(
"2") ==
362 getContext().int_const(
"1") - getContext().int_const(
"0");
363 itv[2] = itv[1].getInterval() - itv[0].getInterval();
368 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
371 const Z3Expr& relExpr = relation[2] && relation[1];
373 const Z3Expr& phi = (relExpr && initExpr).simplify();
378 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
381 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
393 outs() <<
"test3_1 start\n";
397 relation[0] = getContext().int_const(
"0");
401 getContext().int_const(
"1") == getContext().int_const(
"0");
404 relation[2] = getContext().int_const(
"2") ==
405 getContext().int_const(
"1") / getContext().int_const(
"0");
406 itv[2] = itv[1].getInterval() / itv[0].getInterval();
410 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
413 const Z3Expr& relExpr = relation[2] && relation[1];
415 const Z3Expr& phi = (relExpr && initExpr).simplify();
420 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
423 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
435 outs() <<
"test3_2 start\n";
439 relation[0] = getContext().int_const(
"0");
443 getContext().int_const(
"1") == getContext().int_const(
"0");
446 relation[2] = getContext().int_const(
"2") ==
447 getContext().int_const(
"1") / getContext().int_const(
"0");
448 itv[2] = itv[1].getInterval() / itv[0].getInterval();
452 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
455 const Z3Expr& relExpr = relation[2] && relation[1];
457 const Z3Expr& phi = (relExpr && initExpr).simplify();
462 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
465 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
477 outs() <<
"test3_3 start\n";
481 relation[0] = getContext().int_const(
"0");
485 getContext().int_const(
"1") == getContext().int_const(
"0");
488 relation[2] = getContext().int_const(
"2") ==
489 getContext().int_const(
"1") / getContext().int_const(
"0");
490 itv[2] = itv[1].getInterval() / itv[0].getInterval();
494 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
497 const Z3Expr& relExpr = relation[2] && relation[1];
499 const Z3Expr& phi = (relExpr && initExpr).simplify();
504 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
507 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
518 outs() <<
"test3_4 start\n";
522 relation[0] = getContext().int_const(
"0");
526 getContext().int_const(
"1") == getContext().int_const(
"0");
529 relation[2] = getContext().int_const(
"2") ==
530 getContext().int_const(
"1") / getContext().int_const(
"0");
531 itv[2] = itv[1].getInterval() / itv[0].getInterval();
535 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
538 const Z3Expr& relExpr = relation[2] && relation[1];
540 const Z3Expr& phi = (relExpr && initExpr).simplify();
545 assert(resRSY == resBS && resBS == resBilateral &&
"inconsistency occurs");
548 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
560 outs() <<
"test4_1 start\n";
564 relation[0] = getContext().int_const(
"0");
568 getContext().int_const(
"1") == getContext().int_const(
"0");
571 relation[2] = getContext().int_const(
"2") ==
572 getContext().int_const(
"1") / getContext().int_const(
"0");
573 itv[2] = itv[1].getInterval() / itv[0].getInterval();
577 assert(res ==
Set<u32_t>({0, 1, 2}) &&
"inconsistency occurs");
580 const Z3Expr& relExpr = relation[2] && relation[1];
582 const Z3Expr& phi = (relExpr && initExpr).simplify();
584 outs() <<
"rsy done\n";
586 outs() <<
"bilateral done\n";
588 outs() <<
"bs done\n";
593 outs() << r.first <<
" " << r.second.getInterval() <<
"\n";
620 outs() <<
"start top\n";
843 int main(
int argc,
char** argv)
847 char **arg_value =
new char *[argc + extraArgc];
848 for (; arg_num < argc; ++arg_num)
850 arg_value[arg_num] = argv[arg_num];
853 arg_value[arg_num++] = (
char*)
"-model-consts=true";
854 arg_value[arg_num++] = (
char*)
"-model-arrays=true";
855 arg_value[arg_num++] = (
char*)
"-pre-field-sensitive=false";
856 assert(arg_num == (argc + extraArgc) &&
"more extra arguments? Change the value of extraArgc");
858 std::vector<std::string> moduleNameVec;
860 arg_num, arg_value,
"Static Symbolic Execution",
"[options] <input-bitcode...>"
887 ae.
addDetector(std::make_unique<BufOverflowDetector>());
int main(int argc, char **argv)
static Option< bool > AETEST("aetest", "abstract execution basic function test", false)
static Option< bool > SYMABS("symabs", "symbolic abstraction test", false)
static std::vector< std::string > parseOptions(int argc, char *argv[], std::string description, std::string callFormat)
AbstractInterpretation is same as Abstract Execution.
void addDetector(std::unique_ptr< AEDetector > detector)
virtual void runOnModule(ICFG *icfg)
static AbstractInterpretation & getAEInstance()
void printAbstractState() const
const VarToAbsValMap & getVarToVal() const
get var2val map
AbstractValue loadValue(NodeID varId)
Map< u32_t, AbstractValue > VarToAbsValMap
void storeValue(NodeID varId, AbstractValue val)
static bool eqVarToValMap(const VarToAbsValMap &lhs, const VarToAbsValMap &rhs)
AbstractState sliceState(Set< u32_t > &sl)
Copy some values and return a new IntervalExeState.
bool equals(const AbstractValue &rhs) const
static AndersenWaveDiff * createAndersenWaveDiff(SVFIR *_pag)
Create an singleton instance directly instead of invoking llvm pass manager.
void updateCallGraph(PTACallGraph *callgraph)
update ICFG for indirect calls
static BoundedInt minus_infinity()
Get minus infinity -inf.
static IntervalValue bottom()
Create the bottom IntervalValue [+inf, -inf].
static BoundedInt plus_infinity()
Get plus infinity +inf.
static IntervalValue top()
Create the IntervalValue [-inf, +inf].
static void releaseLLVMModuleSet()
static LLVMModuleSet * getLLVMModuleSet()
static SVFModule * buildSVFModule(Module &mod)
static const Option< bool > BufferOverflowCheck
buffer overflow checker, Default: false
PTACallGraph * getCallGraph() const
Return call graph.
void extractSubVars(const Z3Expr &expr, Set< u32_t > &res)
Extract sub SVFVar IDs of a Z3Expr.
Z3Expr gamma_hat(const AbstractState &exeState) const
Return Z3Expr according to valToValMap.
AbstractState RSY(const AbstractState &domain, const Z3Expr &phi)
AbstractState bilateral(const AbstractState &domain, const Z3Expr &phi, u32_t descend_check=0)
AbstractState BS(const AbstractState &domain, const Z3Expr &phi)
void updateCallGraph(PTACallGraph *callgraph)
connect PAG edges based on callgraph
virtual SVFIR * build()
Start building SVFIR here.
static z3::context & getContext()
Get z3 context, singleton design here to make sure we only have one context.
AbstractState BS_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
void testRelExeState1_2()
SymblicAbstractionTest()=default
void testRelExeState2_4()
void testRelExeState2_1()
void testRelExeState2_2()
void testRelExeState3_2()
~SymblicAbstractionTest()=default
void testRelExeState2_3()
void testRelExeState3_3()
AbstractState RSY_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
void testRelExeState4_1()
void testRelExeState2_5()
static z3::context & getContext()
void testRelExeState3_1()
void testRelExeState1_1()
AbstractState Bilateral_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
void testRelExeState3_4()
std::string sucMsg(const std::string &msg)
Returns successful message by converting a string into green string output.
std::ostream & outs()
Overwrite llvm::outs()
std::unordered_set< Key, Hash, KeyEqual, Allocator > Set