Static Value-Flow Analysis
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | List of all members
SymblicAbstractionTest Class Reference

Public Member Functions

 SymblicAbstractionTest ()=default
 
 ~SymblicAbstractionTest ()=default
 
void test_print ()
 
AbstractState RSY_time (AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
 
AbstractState Bilateral_time (AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
 
AbstractState BS_time (AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
 
void testRelExeState1_1 ()
 
void testRelExeState1_2 ()
 
void testRelExeState2_1 ()
 
void testRelExeState2_2 ()
 
void testRelExeState2_3 ()
 
void testRelExeState2_4 ()
 
void testRelExeState2_5 ()
 
void testRelExeState3_1 ()
 
void testRelExeState3_2 ()
 
void testRelExeState3_3 ()
 
void testRelExeState3_4 ()
 
void testRelExeState4_1 ()
 
void testsValidation ()
 

Static Public Member Functions

static z3::context & getContext ()
 

Detailed Description

Definition at line 54 of file ae.cpp.

Constructor & Destructor Documentation

◆ SymblicAbstractionTest()

SymblicAbstractionTest::SymblicAbstractionTest ( )
default

◆ ~SymblicAbstractionTest()

SymblicAbstractionTest::~SymblicAbstractionTest ( )
default

Member Function Documentation

◆ Bilateral_time()

AbstractState SymblicAbstractionTest::Bilateral_time ( AbstractState &  inv,
const Z3Expr &  phi,
RelationSolver &  rs 
)
inline

Definition at line 83 of file ae.cpp.

85 {
86 auto start_time = std::chrono::high_resolution_clock::now();
87 AbstractState resBilateral = rs.bilateral(inv, phi);
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()
92 << " microseconds\n";
93 return resBilateral;
94 }
SVF::SVFUtil::outs
std::ostream & outs()
Overwrite llvm::outs()
Definition SVFUtil.h:50
SVF::IRBuilder
llvm::IRBuilder IRBuilder
Definition BasicTypes.h:74

◆ BS_time()

AbstractState SymblicAbstractionTest::BS_time ( AbstractState &  inv,
const Z3Expr &  phi,
RelationSolver &  rs 
)
inline

Definition at line 95 of file ae.cpp.

97 {
98 auto start_time = std::chrono::high_resolution_clock::now();
99 AbstractState resBS = rs.BS(inv, phi);
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";
105 return resBS;
106 }

◆ getContext()

static z3::context & SymblicAbstractionTest::getContext ( )
inlinestatic

Definition at line 61 of file ae.cpp.

62 {
63 return Z3Expr::getContext();
64 }
SVF::Z3Expr::getContext
static z3::context & getContext()
Get z3 context, singleton design here to make sure we only have one context.
Definition Z3Expr.cpp:66

◆ RSY_time()

AbstractState SymblicAbstractionTest::RSY_time ( AbstractState &  inv,
const Z3Expr &  phi,
RelationSolver &  rs 
)
inline

Definition at line 71 of file ae.cpp.

73 {
74 auto start_time = std::chrono::high_resolution_clock::now();
75 AbstractState resRSY = rs.RSY(inv, phi);
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()
80 << " microseconds\n";
81 return resRSY;
82 }

◆ test_print()

void SymblicAbstractionTest::test_print ( )
inline

Definition at line 66 of file ae.cpp.

67 {
68 outs() << "hello print\n";
69 }

◆ testRelExeState1_1()

void SymblicAbstractionTest::testRelExeState1_1 ( )
inline

Definition at line 108 of file ae.cpp.

109 {
110 outs() << sucMsg("\t SUCCESS :") << "test1_1 start\n";
111 AbstractState itv;
112 RelExeState relation;
113 // var0 := [0, 1];
114 itv[0] = IntervalValue(0, 1);
115 relation[0] = getContext().int_const("0");
116 // var1 := var0 + 1;
117 relation[1] =
118 getContext().int_const("1") == getContext().int_const("0") + 1;
119 itv[1] = itv[0].getInterval() + IntervalValue(1);
120 // Test extract sub vars
121 Set<u32_t> res;
122 relation.extractSubVars(relation[1], res);
123 assert(res == Set<u32_t>({0, 1}) && "inconsistency occurs");
124 AbstractState inv = itv.sliceState(res);
125 RelationSolver rs;
126 const Z3Expr& relExpr = relation[1];
127 const Z3Expr& initExpr = rs.gamma_hat(inv);
128 const Z3Expr& phi = (relExpr && initExpr).simplify();
129 AbstractState resRSY = rs.RSY(inv, phi);
130 AbstractState resBilateral = rs.bilateral(inv, phi);
131 AbstractState resBS = rs.BS(inv, phi);
132 // 0:[0,1] 1:[1,2]
133 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
134 for (auto r : resRSY.getVarToVal())
135 {
136 outs() << r.first << " " << r.second.getInterval() << "\n";
137 }
138 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 1)}, {1, IntervalValue(1, 2)}};
139 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
140 }
SVF::AbstractState::VarToAbsValMap
Map< u32_t, AbstractValue > VarToAbsValMap
Definition AbstractState.h:63
SVF::AbstractState::eqVarToValMap
static bool eqVarToValMap(const VarToAbsValMap &lhs, const VarToAbsValMap &rhs)
Definition AbstractState.h:326
SVF::AbstractState::sliceState
AbstractState sliceState(Set< u32_t > &sl)
Copy some values and return a new IntervalExeState.
Definition AbstractState.h:177
SymblicAbstractionTest::getContext
static z3::context & getContext()
Definition ae.cpp:61
SVF::SVFUtil::sucMsg
std::string sucMsg(const std::string &msg)
Returns successful message by converting a string into green string output.
Definition SVFUtil.cpp:54

◆ testRelExeState1_2()

void SymblicAbstractionTest::testRelExeState1_2 ( )
inline

Definition at line 142 of file ae.cpp.

143 {
144 outs() << "test1_2 start\n";
145 AbstractState itv;
146 RelExeState relation;
147 // var0 := [0, 1];
148 relation[0] = getContext().int_const("0");
149 itv[0] = IntervalValue(0, 1);
150 // var1 := var0 + 1;
151 relation[1] =
152 getContext().int_const("1") == getContext().int_const("0") * 2;
153 itv[1] = itv[0].getInterval() * IntervalValue(2);
154
155 // Test extract sub vars
156 Set<u32_t> res;
157 relation.extractSubVars(relation[1], res);
158 assert(res == Set<u32_t>({0, 1}) && "inconsistency occurs");
159 AbstractState inv = itv.sliceState(res);
160 RelationSolver rs;
161 const Z3Expr& relExpr = relation[1];
162 const Z3Expr& initExpr = rs.gamma_hat(inv);
163 const Z3Expr& phi = (relExpr && initExpr).simplify();
164 AbstractState resRSY = rs.RSY(inv, phi);
165 AbstractState resBilateral = rs.bilateral(inv, phi);
166 AbstractState resBS = rs.BS(inv, phi);
167 // 0:[0,1] 1:[0,2]
168 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
169 for (auto r : resRSY.getVarToVal())
170 {
171 outs() << r.first << " " << r.second.getInterval() << "\n";
172 }
173 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 1)}, {1, IntervalValue(0, 2)}};
174 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
175 }

◆ testRelExeState2_1()

void SymblicAbstractionTest::testRelExeState2_1 ( )
inline

Definition at line 177 of file ae.cpp.

178 {
179 outs() << "test2_1 start\n";
180 AbstractState itv;
181 RelExeState relation;
182 // var0 := [0, 10];
183 relation[0] = getContext().int_const("0");
184 itv[0] = IntervalValue(0, 10);
185 // var1 := var0;
186 relation[1] =
187 getContext().int_const("1") == getContext().int_const("0");
188 itv[1] = itv[0];
189 // var2 := var1 - var0;
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();
193 // Test extract sub vars
194 Set<u32_t> res;
195 relation.extractSubVars(relation[2], res);
196 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
197 AbstractState inv = itv.sliceState(res);
198 RelationSolver rs;
199 const Z3Expr& relExpr = relation[2] && relation[1];
200 const Z3Expr& initExpr = rs.gamma_hat(inv);
201 const Z3Expr& phi = (relExpr && initExpr).simplify();
202 AbstractState resRSY = rs.RSY(inv, phi);
203 AbstractState resBilateral = rs.bilateral(inv, phi);
204 AbstractState resBS = rs.BS(inv, phi);
205 // 0:[0,10] 1:[0,10] 2:[0,0]
206 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
207 for (auto r : resRSY.getVarToVal())
208 {
209 outs() << r.first << " " << r.second.getInterval() << "\n";
210 }
211 // ground truth
212 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 10)},
213 {1, IntervalValue(0, 10)},
214 {2, IntervalValue(0, 0)}
215 };
216 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
217 }

◆ testRelExeState2_2()

void SymblicAbstractionTest::testRelExeState2_2 ( )
inline

Definition at line 219 of file ae.cpp.

220 {
221 outs() << "test2_2 start\n";
222 AbstractState itv;
223 RelExeState relation;
224 // var0 := [0, 100];
225 relation[0] = getContext().int_const("0");
226 itv[0] = IntervalValue(0, 100);
227 // var1 := var0;
228 relation[1] =
229 getContext().int_const("1") == getContext().int_const("0");
230 itv[1] = itv[0];
231 // var2 := var1 - var0;
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();
235
236 // Test extract sub vars
237 Set<u32_t> res;
238 relation.extractSubVars(relation[2], res);
239 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
240 AbstractState inv = itv.sliceState(res);
241 RelationSolver rs;
242 const Z3Expr& relExpr = relation[2] && relation[1];
243 const Z3Expr& initExpr = rs.gamma_hat(inv);
244 const Z3Expr& phi = (relExpr && initExpr).simplify();
245 AbstractState resRSY = rs.RSY(inv, phi);
246 AbstractState resBilateral = rs.bilateral(inv, phi);
247 AbstractState resBS = rs.BS(inv, phi);
248 // 0:[0,100] 1:[0,100] 2:[0,0]
249 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
250 for (auto r : resRSY.getVarToVal())
251 {
252 outs() << r.first << " " << r.second.getInterval() << "\n";
253 }
254 // ground truth
255 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 100)},
256 {1, IntervalValue(0, 100)},
257 {2, IntervalValue(0, 0)}
258 };
259 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
260 }

◆ testRelExeState2_3()

void SymblicAbstractionTest::testRelExeState2_3 ( )
inline

Definition at line 262 of file ae.cpp.

263 {
264 outs() << "test2_3 start\n";
265 AbstractState itv;
266 RelExeState relation;
267 // var0 := [0, 1000];
268 relation[0] = getContext().int_const("0");
269 itv[0] = IntervalValue(0, 1000);
270 // var1 := var0;
271 relation[1] =
272 getContext().int_const("1") == getContext().int_const("0");
273 itv[1] = itv[0];
274 // var2 := var1 - var0;
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();
278
279 // Test extract sub vars
280 Set<u32_t> res;
281 relation.extractSubVars(relation[2], res);
282 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
283 AbstractState inv = itv.sliceState(res);
284 RelationSolver rs;
285 const Z3Expr& relExpr = relation[2] && relation[1];
286 const Z3Expr& initExpr = rs.gamma_hat(inv);
287 const Z3Expr& phi = (relExpr && initExpr).simplify();
288 AbstractState resRSY = rs.RSY(inv, phi);
289 AbstractState resBilateral = rs.bilateral(inv, phi);
290 AbstractState resBS = rs.BS(inv, phi);
291 // 0:[0,1000] 1:[0,1000] 2:[0,0]
292 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
293 for (auto r : resRSY.getVarToVal())
294 {
295 outs() << r.first << " " << r.second.getInterval() << "\n";
296 }
297 // ground truth
298 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 1000)},
299 {1, IntervalValue(0, 1000)},
300 {2, IntervalValue(0, 0)}
301 };
302 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
303 }

◆ testRelExeState2_4()

void SymblicAbstractionTest::testRelExeState2_4 ( )
inline

Definition at line 305 of file ae.cpp.

306 {
307 outs() << "test2_4 start\n";
308 AbstractState itv;
309 RelExeState relation;
310 // var0 := [0, 10000];
311 relation[0] = getContext().int_const("0");
312 itv[0] = IntervalValue(0, 10000);
313 // var1 := var0;
314 relation[1] =
315 getContext().int_const("1") == getContext().int_const("0");
316 itv[1] = itv[0];
317 // var2 := var1 - var0;
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();
321
322 // Test extract sub vars
323 Set<u32_t> res;
324 relation.extractSubVars(relation[2], res);
325 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
326 AbstractState inv = itv.sliceState(res);
327 RelationSolver rs;
328 const Z3Expr& relExpr = relation[2] && relation[1];
329 const Z3Expr& initExpr = rs.gamma_hat(inv);
330 const Z3Expr& phi = (relExpr && initExpr).simplify();
331 AbstractState resRSY = RSY_time(inv, phi, rs);
332 AbstractState resBilateral = Bilateral_time(inv, phi, rs);
333 AbstractState resBS = BS_time(inv, phi, rs);
334 // 0:[0,10000] 1:[0,10000] 2:[0,0]
335 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
336 for (auto r : resRSY.getVarToVal())
337 {
338 outs() << r.first << " " << r.second.getInterval() << "\n";
339 }
340 // ground truth
341 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 10000)},
342 {1, IntervalValue(0, 10000)},
343 {2, IntervalValue(0, 0)}
344 };
345 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
346 }
SymblicAbstractionTest::BS_time
AbstractState BS_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:95
SymblicAbstractionTest::RSY_time
AbstractState RSY_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:71
SymblicAbstractionTest::Bilateral_time
AbstractState Bilateral_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:83

◆ testRelExeState2_5()

void SymblicAbstractionTest::testRelExeState2_5 ( )
inline

Definition at line 348 of file ae.cpp.

349 {
350 outs() << "test2_5 start\n";
351 AbstractState itv;
352 RelExeState relation;
353 // var0 := [0, 100000];
354 relation[0] = getContext().int_const("0");
355 itv[0] = IntervalValue(0, 100000);
356 // var1 := var0;
357 relation[1] =
358 getContext().int_const("1") == getContext().int_const("0");
359 itv[1] = itv[0];
360 // var2 := var1 - var0;
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();
364
365 // Test extract sub vars
366 Set<u32_t> res;
367 relation.extractSubVars(relation[2], res);
368 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
369 AbstractState inv = itv.sliceState(res);
370 RelationSolver rs;
371 const Z3Expr& relExpr = relation[2] && relation[1];
372 const Z3Expr& initExpr = rs.gamma_hat(inv);
373 const Z3Expr& phi = (relExpr && initExpr).simplify();
374 AbstractState resRSY = RSY_time(inv, phi, rs);
375 AbstractState resBilateral = Bilateral_time(inv, phi, rs);
376 AbstractState resBS = BS_time(inv, phi, rs);
377 // 0:[0,100000] 1:[0,100000] 2:[0,0]
378 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
379 for (auto r : resRSY.getVarToVal())
380 {
381 outs() << r.first << " " << r.second.getInterval() << "\n";
382 }
383 // ground truth
384 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 100000)},
385 {1, IntervalValue(0, 100000)},
386 {2, IntervalValue(0, 0)}
387 };
388 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
389 }

◆ testRelExeState3_1()

void SymblicAbstractionTest::testRelExeState3_1 ( )
inline

Definition at line 391 of file ae.cpp.

392 {
393 outs() << "test3_1 start\n";
394 AbstractState itv;
395 RelExeState relation;
396 // var0 := [1, 10];
397 relation[0] = getContext().int_const("0");
398 itv[0] = IntervalValue(1, 10);
399 // var1 := var0;
400 relation[1] =
401 getContext().int_const("1") == getContext().int_const("0");
402 itv[1] = itv[0];
403 // var2 := var1 / var0;
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();
407 // Test extract sub vars
408 Set<u32_t> res;
409 relation.extractSubVars(relation[2], res);
410 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
411 AbstractState inv = itv.sliceState(res);
412 RelationSolver rs;
413 const Z3Expr& relExpr = relation[2] && relation[1];
414 const Z3Expr& initExpr = rs.gamma_hat(inv);
415 const Z3Expr& phi = (relExpr && initExpr).simplify();
416 AbstractState resRSY = rs.RSY(inv, phi);
417 AbstractState resBilateral = rs.bilateral(inv, phi);
418 AbstractState resBS = rs.BS(inv, phi);
419 // 0:[1,10] 1:[1,10] 2:[1,1]
420 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
421 for (auto r : resRSY.getVarToVal())
422 {
423 outs() << r.first << " " << r.second.getInterval() << "\n";
424 }
425 // ground truth
426 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 10)},
427 {1, IntervalValue(1, 10)},
428 {2, IntervalValue(1, 1)}
429 };
430 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
431 }

◆ testRelExeState3_2()

void SymblicAbstractionTest::testRelExeState3_2 ( )
inline

Definition at line 433 of file ae.cpp.

434 {
435 outs() << "test3_2 start\n";
436 AbstractState itv;
437 RelExeState relation;
438 // var0 := [1, 1000];
439 relation[0] = getContext().int_const("0");
440 itv[0] = IntervalValue(1, 1000);
441 // var1 := var0;
442 relation[1] =
443 getContext().int_const("1") == getContext().int_const("0");
444 itv[1] = itv[0];
445 // var2 := var1 / var0;
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();
449 // Test extract sub vars
450 Set<u32_t> res;
451 relation.extractSubVars(relation[2], res);
452 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
453 AbstractState inv = itv.sliceState(res);
454 RelationSolver rs;
455 const Z3Expr& relExpr = relation[2] && relation[1];
456 const Z3Expr& initExpr = rs.gamma_hat(inv);
457 const Z3Expr& phi = (relExpr && initExpr).simplify();
458 AbstractState resRSY = rs.RSY(inv, phi);
459 AbstractState resBilateral = rs.bilateral(inv, phi);
460 AbstractState resBS = rs.BS(inv, phi);
461 // 0:[1,1000] 1:[1,1000] 2:[1,1]
462 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
463 for (auto r : resRSY.getVarToVal())
464 {
465 outs() << r.first << " " << r.second.getInterval() << "\n";
466 }
467 // ground truth
468 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 1000)},
469 {1, IntervalValue(1, 1000)},
470 {2, IntervalValue(1, 1)}
471 };
472 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
473 }

◆ testRelExeState3_3()

void SymblicAbstractionTest::testRelExeState3_3 ( )
inline

Definition at line 475 of file ae.cpp.

476 {
477 outs() << "test3_3 start\n";
478 AbstractState itv;
479 RelExeState relation;
480 // var0 := [1, 10000];
481 relation[0] = getContext().int_const("0");
482 itv[0] = IntervalValue(1, 10000);
483 // var1 := var0;
484 relation[1] =
485 getContext().int_const("1") == getContext().int_const("0");
486 itv[1] = itv[0];
487 // var2 := var1 / var0;
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();
491 // Test extract sub vars
492 Set<u32_t> res;
493 relation.extractSubVars(relation[2], res);
494 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
495 AbstractState inv = itv.sliceState(res);
496 RelationSolver rs;
497 const Z3Expr& relExpr = relation[2] && relation[1];
498 const Z3Expr& initExpr = rs.gamma_hat(inv);
499 const Z3Expr& phi = (relExpr && initExpr).simplify();
500 AbstractState resRSY = RSY_time(inv, phi, rs);
501 AbstractState resBilateral = Bilateral_time(inv, phi, rs);
502 AbstractState resBS = BS_time(inv, phi, rs);
503 // 0:[1,10000] 1:[1,10000] 2:[1,1]
504 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
505 for (auto r : resRSY.getVarToVal())
506 {
507 outs() << r.first << " " << r.second.getInterval() << "\n";
508 }
509 // ground truth
510 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 10000)},
511 {1, IntervalValue(1, 10000)},
512 {2, IntervalValue(1, 1)}
513 };
514 }

◆ testRelExeState3_4()

void SymblicAbstractionTest::testRelExeState3_4 ( )
inline

Definition at line 516 of file ae.cpp.

517 {
518 outs() << "test3_4 start\n";
519 AbstractState itv;
520 RelExeState relation;
521 // var0 := [1, 100000];
522 relation[0] = getContext().int_const("0");
523 itv[0] = IntervalValue(1, 100000);
524 // var1 := var0;
525 relation[1] =
526 getContext().int_const("1") == getContext().int_const("0");
527 itv[1] = itv[0];
528 // var2 := var1 / var0;
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();
532 // Test extract sub vars
533 Set<u32_t> res;
534 relation.extractSubVars(relation[2], res);
535 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
536 AbstractState inv = itv.sliceState(res);
537 RelationSolver rs;
538 const Z3Expr& relExpr = relation[2] && relation[1];
539 const Z3Expr& initExpr = rs.gamma_hat(inv);
540 const Z3Expr& phi = (relExpr && initExpr).simplify();
541 AbstractState resRSY = RSY_time(inv, phi, rs);
542 AbstractState resBilateral = Bilateral_time(inv, phi, rs);
543 AbstractState resBS = BS_time(inv, phi, rs);
544 // 0:[1,100000] 1:[1,100000] 2:[1,1]
545 assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
546 for (auto r : resRSY.getVarToVal())
547 {
548 outs() << r.first << " " << r.second.getInterval() << "\n";
549 }
550 // ground truth
551 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 100000)},
552 {1, IntervalValue(1, 100000)},
553 {2, IntervalValue(1, 1)}
554 };
555 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
556 }

◆ testRelExeState4_1()

void SymblicAbstractionTest::testRelExeState4_1 ( )
inline

Definition at line 558 of file ae.cpp.

559 {
560 outs() << "test4_1 start\n";
561 AbstractState itv;
562 RelExeState relation;
563 // var0 := [0, 10];
564 relation[0] = getContext().int_const("0");
565 itv[0] = IntervalValue(0, 10);
566 // var1 := var0;
567 relation[1] =
568 getContext().int_const("1") == getContext().int_const("0");
569 itv[1] = itv[0];
570 // var2 := var1 / var0;
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();
574 // Test extract sub vars
575 Set<u32_t> res;
576 relation.extractSubVars(relation[2], res);
577 assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
578 AbstractState inv = itv.sliceState(res);
579 RelationSolver rs;
580 const Z3Expr& relExpr = relation[2] && relation[1];
581 const Z3Expr& initExpr = rs.gamma_hat(inv);
582 const Z3Expr& phi = (relExpr && initExpr).simplify();
583 // IntervalExeState resRSY = rs.RSY(inv, phi);
584 outs() << "rsy done\n";
585 // IntervalExeState resBilateral = rs.bilateral(inv, phi);
586 outs() << "bilateral done\n";
587 AbstractState resBS = rs.BS(inv, phi);
588 outs() << "bs done\n";
589 // 0:[0,10] 1:[0,10] 2:[-00,+00]
590 // assert(resRSY == resBS && resBS == resBilateral);
591 for (auto r : resBS.getVarToVal())
592 {
593 outs() << r.first << " " << r.second.getInterval() << "\n";
594 }
595 // ground truth
596 AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 10)},
597 {1, IntervalValue(0, 10)},
598 {2, IntervalValue(0, 10)}
599 };
600 assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
601 }

◆ testsValidation()

void SymblicAbstractionTest::testsValidation ( )
inline

top

Definition at line 603 of file ae.cpp.

604 {
605 SymblicAbstractionTest saTest;
606 saTest.testRelExeState1_1();
607 saTest.testRelExeState1_2();
608
609 saTest.testRelExeState2_1();
610 saTest.testRelExeState2_2();
611 saTest.testRelExeState2_3();
612 // saTest.testRelExeState2_4(); /// 10000
613 // saTest.testRelExeState2_5(); /// 100000
614
615 saTest.testRelExeState3_1();
616 saTest.testRelExeState3_2();
617 // saTest.testRelExeState3_3(); /// 10000
618 // saTest.testRelExeState3_4(); /// 100000
619
620 outs() << "start top\n";
621 saTest.testRelExeState4_1();
622 }
SymblicAbstractionTest::testRelExeState1_1
void testRelExeState1_1()
Definition ae.cpp:108
The documentation for this class was generated from the following file:
Generated by doxygen 1.9.8