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 55 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 84 of file ae.cpp.

86 {
87 auto start_time = std::chrono::high_resolution_clock::now();
88 AbstractState resBilateral = rs.bilateral(inv, phi);
89 auto end_time = std::chrono::high_resolution_clock::now();
90 auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
91 end_time - start_time);
92 outs() << "running time of Bilateral: " << duration.count()
93 << " microseconds\n";
94 return resBilateral;
95 }
SVF::SVFUtil::outs
std::ostream & outs()
Overwrite llvm::outs()
Definition SVFUtil.h:58
SVF::IRBuilder
llvm::IRBuilder IRBuilder
Definition BasicTypes.h:76

◆ BS_time()

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

Definition at line 96 of file ae.cpp.

98 {
99 auto start_time = std::chrono::high_resolution_clock::now();
100 AbstractState resBS = rs.BS(inv, phi);
101 auto end_time = std::chrono::high_resolution_clock::now();
102 auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
103 end_time - start_time);
104 outs() << "running time of BS : " << duration.count()
105 << " microseconds\n";
106 return resBS;
107 }

◆ getContext()

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

Definition at line 62 of file ae.cpp.

63 {
64 return Z3Expr::getContext();
65 }
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 72 of file ae.cpp.

74 {
75 auto start_time = std::chrono::high_resolution_clock::now();
76 AbstractState resRSY = rs.RSY(inv, phi);
77 auto end_time = std::chrono::high_resolution_clock::now();
78 auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
79 end_time - start_time);
80 outs() << "running time of RSY : " << duration.count()
81 << " microseconds\n";
82 return resRSY;
83 }

◆ test_print()

void SymblicAbstractionTest::test_print ( )
inline

Definition at line 67 of file ae.cpp.

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

◆ testRelExeState1_1()

void SymblicAbstractionTest::testRelExeState1_1 ( )
inline

Definition at line 109 of file ae.cpp.

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

◆ testRelExeState1_2()

void SymblicAbstractionTest::testRelExeState1_2 ( )
inline

Definition at line 143 of file ae.cpp.

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

◆ testRelExeState2_1()

void SymblicAbstractionTest::testRelExeState2_1 ( )
inline

Definition at line 178 of file ae.cpp.

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

◆ testRelExeState2_2()

void SymblicAbstractionTest::testRelExeState2_2 ( )
inline

Definition at line 220 of file ae.cpp.

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

◆ testRelExeState2_3()

void SymblicAbstractionTest::testRelExeState2_3 ( )
inline

Definition at line 263 of file ae.cpp.

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

◆ testRelExeState2_4()

void SymblicAbstractionTest::testRelExeState2_4 ( )
inline

Definition at line 306 of file ae.cpp.

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

◆ testRelExeState2_5()

void SymblicAbstractionTest::testRelExeState2_5 ( )
inline

Definition at line 349 of file ae.cpp.

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

◆ testRelExeState3_1()

void SymblicAbstractionTest::testRelExeState3_1 ( )
inline

Definition at line 392 of file ae.cpp.

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

◆ testRelExeState3_2()

void SymblicAbstractionTest::testRelExeState3_2 ( )
inline

Definition at line 434 of file ae.cpp.

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

◆ testRelExeState3_3()

void SymblicAbstractionTest::testRelExeState3_3 ( )
inline

Definition at line 476 of file ae.cpp.

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

◆ testRelExeState3_4()

void SymblicAbstractionTest::testRelExeState3_4 ( )
inline

Definition at line 517 of file ae.cpp.

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

◆ testRelExeState4_1()

void SymblicAbstractionTest::testRelExeState4_1 ( )
inline

Definition at line 559 of file ae.cpp.

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

◆ testsValidation()

void SymblicAbstractionTest::testsValidation ( )
inline

top

Definition at line 604 of file ae.cpp.

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