Static Value-Flow Analysis
Loading...
Searching...
No Matches
ae.cpp
Go to the documentation of this file.
1//===- ae.cpp -- Abstract Execution -------------------------------------//
2//
3// SVF: Static Value-Flow Analysis
4//
5// Copyright (C) <2013-2017> <Yulei Sui>
6//
7
8// This program is free software: you can redistribute it and/or modify
9// it under the terms of the GNU Affero General Public License as published by
10// the Free Software Foundation, either version 3 of the License, or
11// (at your option) any later version.
12
13// This program is distributed in the hope that it will be useful,
14// but WITHOUT ANY WARRANTY; without even the implied warranty of
15// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16// GNU Affero General Public License for more details.
17
18// You should have received a copy of the GNU Affero General Public License
19// along with this program. If not, see <http://www.gnu.org/licenses/>.
20//
21//===-----------------------------------------------------------------------===//
22
23/*
24 // Abstract Execution
25 //
26 // Author: Jiawei Wang, Xiao Cheng, Jiawei Yang, Jiawei Ren, Yulei Sui
27 */
28#include "SVF-LLVM/SVFIRBuilder.h"
29#include "WPA/WPAPass.h"
30#include "Util/CommandLine.h"
31#include "Util/Options.h"
32#include "WPA/Andersen.h"
33
34#include "AE/Core/RelExeState.h"
35#include "AE/Core/RelationSolver.h"
36#include "AE/Svfexe/AbstractInterpretation.h"
37
38using namespace SVF;
39using namespace SVFUtil;
40
41
42static Option<bool> SYMABS(
43 "symabs",
44 "symbolic abstraction test",
45 false
46);
47
48static Option<bool> AETEST(
49 "aetest",
50 "abstract execution basic function test",
51 false
52);
53
54class SymblicAbstractionTest
55{
56public:
57 SymblicAbstractionTest() = default;
58
59 ~SymblicAbstractionTest() = default;
60
61 static z3::context& getContext()
62 {
63 return Z3Expr::getContext();
64 }
65
66 void test_print()
67 {
68 outs() << "hello print\n";
69 }
70
71 AbstractState RSY_time(AbstractState& inv, const Z3Expr& phi,
72 RelationSolver& rs)
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 }
83 AbstractState Bilateral_time(AbstractState& inv, const Z3Expr& phi,
84 RelationSolver& rs)
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 }
95 AbstractState BS_time(AbstractState& inv, const Z3Expr& phi,
96 RelationSolver& rs)
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 }
107
108 void testRelExeState1_1()
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 }
141
142 void testRelExeState1_2()
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 }
176
177 void testRelExeState2_1()
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 }
218
219 void testRelExeState2_2()
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 }
261
262 void testRelExeState2_3()
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 }
304
305 void testRelExeState2_4()
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 }
347
348 void testRelExeState2_5()
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 }
390
391 void testRelExeState3_1()
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 }
432
433 void testRelExeState3_2()
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 }
474
475 void testRelExeState3_3()
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 }
515
516 void testRelExeState3_4()
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 }
557
558 void testRelExeState4_1()
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 }
602
603 void testsValidation()
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 }
623};
624
625class AETest
626{
627public:
628 AETest() = default;
629
630 ~AETest() = default;
631
632 void testBinaryOpStmt()
633 {
634 // test division /
635 assert((IntervalValue(4) / IntervalValue::bottom()).equals(IntervalValue::bottom()));
636 assert((IntervalValue::bottom() / IntervalValue(2)).equals(IntervalValue::bottom()));
637 assert((IntervalValue::top() / IntervalValue(0)).equals(IntervalValue::bottom()));
638 assert((IntervalValue(4) / IntervalValue(2)).equals(IntervalValue(2)));
639 assert((IntervalValue(3) / IntervalValue(2)).equals(IntervalValue(1))); //
640 assert((IntervalValue(-3) / IntervalValue(2)).equals(IntervalValue(-1))); //
641 assert((IntervalValue(1, 3) / IntervalValue(2)).equals(IntervalValue(0, 1))); //
642 assert((IntervalValue(2, 7) / IntervalValue(2)).equals(IntervalValue(1, 3))); //
643 assert((IntervalValue(-3, 3) / IntervalValue(2)).equals(IntervalValue(-1, 1)));
644 assert((IntervalValue(-3, IntervalValue::plus_infinity()) / IntervalValue(2)).equals(IntervalValue(-1, IntervalValue::plus_infinity())));
645 assert((IntervalValue(IntervalValue::minus_infinity(), 3) / IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity(), 1)));
646 assert((IntervalValue(1, 3) / IntervalValue(1, 2)).equals(IntervalValue(0, 3)));//
647 assert((IntervalValue(-3, 3) / IntervalValue(1, 2)).equals(IntervalValue(-3, 3)));
648 assert((IntervalValue(2, 7) / IntervalValue(-2, 3)).equals(IntervalValue(-7, 7))); //
649 assert((IntervalValue(-2, 7) / IntervalValue(-2, 3)).equals(IntervalValue(-7, 7))); //
650 assert((IntervalValue(IntervalValue::minus_infinity(), 7) / IntervalValue(-2, 3)).equals(IntervalValue::top()));
651 assert((IntervalValue(-2, IntervalValue::plus_infinity()) / IntervalValue(-2, 3)).equals(IntervalValue::top()));
652
653 assert((IntervalValue(-2, 7) / IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue(-7, 7)));
654 assert((IntervalValue(-2, 7) / IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue(-7, 7)));
655 assert((IntervalValue(-6, -3) / IntervalValue(3, 9)).equals(IntervalValue(-2, 0)));
656 assert((IntervalValue(-6, 6) / IntervalValue(3, 9)).equals(IntervalValue(-2, 2)));
657
658 // test remainder %
659 assert((IntervalValue(4) % IntervalValue::bottom()).equals(IntervalValue::bottom()));
660 assert((IntervalValue::bottom() % IntervalValue(2)).equals(IntervalValue::bottom()));
661 assert((IntervalValue::top() % IntervalValue(0)).equals(IntervalValue::top()));
662 assert((IntervalValue(4) % IntervalValue(2)).equals(IntervalValue(0)));
663 assert((IntervalValue(3) % IntervalValue(2)).equals(IntervalValue(1)));
664 assert((IntervalValue(-3) % IntervalValue(2)).equals(IntervalValue(-1)));
665 assert((IntervalValue(1, 3) % IntervalValue(2)).equals(IntervalValue(0, 1)));
666 assert((IntervalValue(2, 7) % IntervalValue(2)).equals(IntervalValue(0, 1)));
667 assert((IntervalValue(-3, 3) % IntervalValue(2)).equals(IntervalValue(-1, 1)));
668 assert((IntervalValue(-3, IntervalValue::plus_infinity()) % IntervalValue(2)).equals(IntervalValue(-1, 1)));
669 assert((IntervalValue(IntervalValue::minus_infinity(), 3) % IntervalValue(2)).equals(IntervalValue(-1, 1)));
670 assert((IntervalValue(1, 3) % IntervalValue(1, 2)).equals(IntervalValue(0, 1)));
671 assert((IntervalValue(-3, 3) % IntervalValue(1, 2)).equals(IntervalValue(-1, 1)));
672 assert((IntervalValue(2, 7) % IntervalValue(-2, 3)).equals(IntervalValue::top())); //
673 assert((IntervalValue(-2, 7) % IntervalValue(-2, 3)).equals(IntervalValue::top())); //
674 assert((IntervalValue(IntervalValue::minus_infinity(), 7) % IntervalValue(-2, 3)).equals(IntervalValue::top()));
675 assert((IntervalValue(-2, IntervalValue::plus_infinity()) % IntervalValue(-2, 3)).equals(IntervalValue::top()));
676 assert((IntervalValue(-2, 7) % IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
677 assert((IntervalValue(-2, 7) % IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
678 assert((IntervalValue(-6, -3) % IntervalValue(3, 9)).equals(IntervalValue(-6, 0)));
679 assert((IntervalValue(-6, 6) % IntervalValue(3, 9)).equals(IntervalValue(-6, 6)));
680
681 // shl <<
682 assert((IntervalValue(IntervalValue::plus_infinity()) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
683 assert((IntervalValue(IntervalValue::plus_infinity()) << IntervalValue(2, 2)).equals(IntervalValue(IntervalValue::plus_infinity())));
684 assert((IntervalValue(IntervalValue::minus_infinity()) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
685 assert((IntervalValue(IntervalValue::minus_infinity()) << IntervalValue(2, 2)).equals(IntervalValue(IntervalValue::minus_infinity())));
686 assert((IntervalValue(2, 2) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
687 assert((IntervalValue(0, 0) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(0, 0)));
688 assert((IntervalValue(-2, -2) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
689 assert((IntervalValue(0, 0) << IntervalValue(2, 2)).equals(IntervalValue(0, 0)));
690 assert((IntervalValue(2, 2) << IntervalValue(3, 3)).equals(IntervalValue(16, 16)));
691 assert((IntervalValue(-2, -2) << IntervalValue(3, 3)).equals(IntervalValue(-16, -16)));
692
693 assert((IntervalValue(4) << IntervalValue::bottom()).equals(IntervalValue::bottom()));
694 assert((IntervalValue::bottom() << IntervalValue(2)).equals(IntervalValue::bottom()));
695 assert((IntervalValue::top() << IntervalValue(0)).equals(IntervalValue::top()));
696 assert((IntervalValue(4) << IntervalValue(2)).equals(IntervalValue(16)));
697 assert((IntervalValue(3) << IntervalValue(2)).equals(IntervalValue(12)));
698 assert((IntervalValue(-3) << IntervalValue(2)).equals(IntervalValue(-12)));
699 assert((IntervalValue(4) << IntervalValue(-2)).equals(IntervalValue::bottom()));
700 assert((IntervalValue(1, 3) << IntervalValue(2)).equals(IntervalValue(4, 12)));
701 assert((IntervalValue(2, 7) << IntervalValue(2)).equals(IntervalValue(8, 28)));
702 assert((IntervalValue(-3, 3) << IntervalValue(2)).equals(IntervalValue(-12, 12)));
703 assert((IntervalValue(-3, IntervalValue::plus_infinity()) << IntervalValue(2)).equals(IntervalValue(-12, IntervalValue::plus_infinity())));
704 assert((IntervalValue(IntervalValue::minus_infinity(), 3) << IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity(), 12)));
705 assert((IntervalValue(1, 3) << IntervalValue(1, 2)).equals(IntervalValue(2, 12)));
706 assert((IntervalValue(-3, 3) << IntervalValue(1, 2)).equals(IntervalValue(-12, 12)));
707 assert((IntervalValue(2, 7) << IntervalValue(-2, 3)).equals(IntervalValue(2, 56)));
708 assert((IntervalValue(-2, 7) << IntervalValue(-2, 3)).equals(IntervalValue(-16, 56)));
709 assert((IntervalValue(IntervalValue::minus_infinity(), 7) << IntervalValue(-2, 3)).equals(IntervalValue(IntervalValue::minus_infinity(), 56)));
710 assert((IntervalValue(-2, IntervalValue::plus_infinity()) << IntervalValue(-2, 3)).equals(IntervalValue(-16, IntervalValue::plus_infinity())));
711 assert((IntervalValue(-2, 7) << IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue(-16, 56)));
712 assert((IntervalValue(-2, 7) << IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
713 assert((IntervalValue(-6, -3) << IntervalValue(3, 9)).equals(IntervalValue(-3072, -24)));
714 assert((IntervalValue(-6, 6) << IntervalValue(3, 9)).equals(IntervalValue(-3072, 3072)));
715 assert((IntervalValue(-2, 7) << IntervalValue(IntervalValue::minus_infinity(), -1)).equals(IntervalValue::bottom()));
716 assert((IntervalValue(0) << IntervalValue::top()).equals(IntervalValue(0)));
717
718
719 // shr >>
720 assert((IntervalValue(IntervalValue::plus_infinity()) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::plus_infinity())));
721 assert((IntervalValue(IntervalValue::plus_infinity()) >> IntervalValue(2)).equals(IntervalValue(IntervalValue::plus_infinity())));
722 assert((IntervalValue(IntervalValue::minus_infinity()) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::minus_infinity())));
723 assert((IntervalValue(IntervalValue::minus_infinity()) >> IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity())));
724 assert((IntervalValue(2) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(0)));
725 assert((IntervalValue(0) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(0)));
726 assert((IntervalValue(-2) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(-1)));
727 assert((IntervalValue(0) >> IntervalValue(2)).equals(IntervalValue(0)));
728 assert((IntervalValue(15) >> IntervalValue(2)).equals(IntervalValue(3)));
729 assert((IntervalValue(-15) >> IntervalValue(2)).equals(IntervalValue(-4)));
730
731 assert((IntervalValue(4) >> IntervalValue::bottom()).equals(IntervalValue::bottom()));
732 assert((IntervalValue::bottom() >> IntervalValue(2)).equals(IntervalValue::bottom()));
733 assert((IntervalValue::top() >> IntervalValue(0)).equals(IntervalValue::top()));
734 assert((IntervalValue(15) >> IntervalValue(2)).equals(IntervalValue(3)));
735 assert((IntervalValue(1) >> IntervalValue(2)).equals(IntervalValue(0)));
736 assert((IntervalValue(-15) >> IntervalValue(2)).equals(IntervalValue(-4)));
737 assert((IntervalValue(4) >> IntervalValue(-2)).equals(IntervalValue::bottom()));
738 assert((IntervalValue(1, 3) >> IntervalValue(2)).equals(IntervalValue(0)));
739 assert((IntervalValue(2, 7) >> IntervalValue(2)).equals(IntervalValue(0, 1)));
740 assert((IntervalValue(-15, 15) >> IntervalValue(2)).equals(IntervalValue(-4, 3)));
741 assert((IntervalValue(-15, IntervalValue::plus_infinity()) >> IntervalValue(2)).equals(IntervalValue(-4, IntervalValue::plus_infinity())));
742 assert((IntervalValue(IntervalValue::minus_infinity(), 15) >> IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity(), 3)));
743 assert((IntervalValue(0, 15) >> IntervalValue(1, 2)).equals(IntervalValue(0, 7)));
744 assert((IntervalValue(-17, 15) >> IntervalValue(1, 2)).equals(IntervalValue(-9, 7)));
745 assert((IntervalValue(2, 7) >> IntervalValue(-2, 3)).equals(IntervalValue(0, 7)));
746 assert((IntervalValue(-2, 7) >> IntervalValue(-2, 3)).equals(IntervalValue(-2, 7)));
747 assert((IntervalValue(IntervalValue::minus_infinity(), 7) >> IntervalValue(-2, 3)).equals(IntervalValue(IntervalValue::minus_infinity(), 7)));
748 assert((IntervalValue(-2, IntervalValue::plus_infinity()) >> IntervalValue(-2, 3)).equals(IntervalValue(-2, IntervalValue::plus_infinity())));
749 assert((IntervalValue(-2, 7) >> IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue(-2, 7)));
750 assert((IntervalValue(-2, 7) >> IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue(-2, 7)));
751 assert((IntervalValue(-6, -3) >> IntervalValue(2, 3)).equals(IntervalValue(-2, -1)));
752 assert((IntervalValue(-6, 6) >> IntervalValue(2, 3)).equals(IntervalValue(-2, 1)));
753 assert((IntervalValue(-2, 7) >> IntervalValue(IntervalValue::minus_infinity(), -1)).equals(IntervalValue::bottom()));
754 assert((IntervalValue(0) >> IntervalValue::top()).equals(IntervalValue(0)));
755
756 // and &
757 assert((IntervalValue(4) & IntervalValue::bottom()).equals(IntervalValue::bottom()));
758 assert((IntervalValue::bottom() & IntervalValue(2)).equals(IntervalValue::bottom()));
759 assert((IntervalValue::top() & IntervalValue(0)).equals(IntervalValue(0)));
760 assert((IntervalValue(4) & IntervalValue(2)).equals(IntervalValue(0)));
761 assert((IntervalValue(3) & IntervalValue(2)).equals(IntervalValue(2)));
762 assert((IntervalValue(-3) & IntervalValue(2)).equals(IntervalValue(0)));
763 assert((IntervalValue(1, 3) & IntervalValue(2)).equals(IntervalValue(0, 2)));
764 assert((IntervalValue(2, 7) & IntervalValue(2)).equals(IntervalValue(0, 2)));
765 assert((IntervalValue(-3, 3) & IntervalValue(2)).equals(IntervalValue(0, 2)));
766 assert((IntervalValue(-3, IntervalValue::plus_infinity()) & IntervalValue(2)).equals(IntervalValue(0, 2)));
767 assert((IntervalValue(IntervalValue::minus_infinity(), 3) & IntervalValue(2)).equals(IntervalValue(0, 2)));
768 assert((IntervalValue(1, 3) & IntervalValue(1, 2)).equals(IntervalValue(0, 2)));
769 assert((IntervalValue(-3, 3) & IntervalValue(1, 2)).equals(IntervalValue(0, 2)));
770 assert((IntervalValue(2, 7) & IntervalValue(-2, 3)).equals(IntervalValue(0, 7)));
771 assert((IntervalValue(-2, 7) & IntervalValue(-2, 3)).equals(IntervalValue::top()));
772 assert((IntervalValue(IntervalValue::minus_infinity(), 7) & IntervalValue(-2, 3)).equals(IntervalValue::top()));
773 assert((IntervalValue(-2, IntervalValue::plus_infinity()) & IntervalValue(-2, 3)).equals(IntervalValue::top()));
774 assert((IntervalValue(-2, 7) & IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
775 assert((IntervalValue(-2, 7) & IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
776 assert((IntervalValue(-6, -3) & IntervalValue(3, 9)).equals(IntervalValue(0, 9)));
777 assert((IntervalValue(-6, 6) & IntervalValue(3, 9)).equals(IntervalValue(0, 9)));
778
779 // Or |
780 assert((IntervalValue(4) | IntervalValue::bottom()).equals(IntervalValue::bottom()));
781 assert((IntervalValue::bottom() | IntervalValue(2)).equals(IntervalValue::bottom()));
782 assert((IntervalValue::top() | IntervalValue(-1)).equals(IntervalValue::top()));//
783 assert((IntervalValue(-1) | IntervalValue::top()).equals(IntervalValue::top()));//
784 assert((IntervalValue(4) | IntervalValue(2)).equals(IntervalValue(6)));
785 assert((IntervalValue(3) | IntervalValue(2)).equals(IntervalValue(3)));
786 assert((IntervalValue(-3) | IntervalValue(2)).equals(IntervalValue(-1)));
787 assert((IntervalValue(1, 3) | IntervalValue(2)).equals(IntervalValue(0, 3)));
788 assert((IntervalValue(2, 7) | IntervalValue(2)).equals(IntervalValue(0, 7)));
789 assert((IntervalValue(-3, 3) | IntervalValue(2)).equals(IntervalValue::top()));
790 assert((IntervalValue(-3, IntervalValue::plus_infinity()) | IntervalValue(2)).equals(IntervalValue::top()));
791 assert((IntervalValue(IntervalValue::minus_infinity(), 3) | IntervalValue(2)).equals(IntervalValue::top()));
792 assert((IntervalValue(1, 3) | IntervalValue(1, 2)).equals(IntervalValue(0, 3)));
793 assert((IntervalValue(-3, 3) | IntervalValue(1, 2)).equals(IntervalValue::top()));
794 assert((IntervalValue(2, 7) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
795 assert((IntervalValue(-2, 7) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
796 assert((IntervalValue(IntervalValue::minus_infinity(), 7) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
797 assert((IntervalValue(-2, IntervalValue::plus_infinity()) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
798 assert((IntervalValue(-2, 7) | IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
799 assert((IntervalValue(-2, 7) | IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
800 assert((IntervalValue(-6, -3) | IntervalValue(3, 9)).equals(IntervalValue::top()));
801 assert((IntervalValue(-6, 6) | IntervalValue(3, 9)).equals(IntervalValue::top()));
802
803 // Xor ^
804 assert((IntervalValue(4) ^ IntervalValue::bottom()).equals(IntervalValue::bottom()));
805 assert((IntervalValue::bottom() ^ IntervalValue(2)).equals(IntervalValue::bottom()));
806 assert((IntervalValue::top() ^ IntervalValue(-1)).equals(IntervalValue::top()));
807 assert((IntervalValue(-1) ^ IntervalValue::top()).equals(IntervalValue::top()));
808 assert((IntervalValue(4) ^ IntervalValue(2)).equals(IntervalValue(6)));
809 assert((IntervalValue(3) ^ IntervalValue(2)).equals(IntervalValue(1)));
810 assert((IntervalValue(-3) ^ IntervalValue(2)).equals(IntervalValue(-1)));
811 assert((IntervalValue(1, 3) ^ IntervalValue(2)).equals(IntervalValue(0, 3)));
812 assert((IntervalValue(2, 7) ^ IntervalValue(2)).equals(IntervalValue(0, 7)));
813 assert((IntervalValue(-3, 3) ^ IntervalValue(2)).equals(IntervalValue::top()));
814 assert((IntervalValue(-3, IntervalValue::plus_infinity()) ^ IntervalValue(2)).equals(IntervalValue::top()));
815 assert((IntervalValue(IntervalValue::minus_infinity(), 3) ^ IntervalValue(2)).equals(IntervalValue::top()));
816 assert((IntervalValue(1, 3) ^ IntervalValue(1, 2)).equals(IntervalValue(0, 3)));
817 assert((IntervalValue(-3, 3) ^ IntervalValue(1, 2)).equals(IntervalValue::top()));
818 assert((IntervalValue(2, 7) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
819 assert((IntervalValue(-2, 7) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
820 assert((IntervalValue(IntervalValue::minus_infinity(), 7) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
821 assert((IntervalValue(-2, IntervalValue::plus_infinity()) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
822 assert((IntervalValue(-2, 7) ^ IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
823 assert((IntervalValue(-2, 7) ^ IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
824 assert((IntervalValue(-6, -3) ^ IntervalValue(3, 9)).equals(IntervalValue::top()));
825 assert((IntervalValue(-6, 6) ^ IntervalValue(3, 9)).equals(IntervalValue::top()));
826 }
827
828 void testAbsState()
829 {
830 AbstractState as;
831 as[1] = IntervalValue(1, 3);
832 as[2] = IntervalValue(2, 7);
833 as[3] = AddressValue(0x7f000007);
834 as[4] = AddressValue(0x7f000008);
835 as.storeValue(3, as[1]);
836 as.storeValue(4, as[2]);
837 as.printAbstractState();
838 assert(as.loadValue(3).equals(as[1]) && as.loadValue(4).equals(as[2]));
839 }
840};
841
842
843int main(int argc, char** argv)
844{
845 int arg_num = 0;
846 int extraArgc = 3;
847 char **arg_value = new char *[argc + extraArgc];
848 for (; arg_num < argc; ++arg_num)
849 {
850 arg_value[arg_num] = argv[arg_num];
851 }
852 // add extra options
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");
857
858 std::vector<std::string> moduleNameVec;
859 moduleNameVec = OptionBase::parseOptions(
860 arg_num, arg_value, "Static Symbolic Execution", "[options] <input-bitcode...>"
861 );
862 delete[] arg_value;
863 if (SYMABS())
864 {
865 SymblicAbstractionTest saTest;
866 saTest.testsValidation();
867 return 0;
868 }
869
870 if (AETEST())
871 {
872 AETest aeTest;
873 aeTest.testBinaryOpStmt();
874 aeTest.testAbsState();
875 return 0;
876 }
877
878 SVFModule *svfModule = LLVMModuleSet::getLLVMModuleSet()->buildSVFModule(moduleNameVec);
879 SVFIRBuilder builder(svfModule);
880 SVFIR* pag = builder.build();
881 AndersenWaveDiff* ander = AndersenWaveDiff::createAndersenWaveDiff(pag);
882 PTACallGraph* callgraph = ander->getCallGraph();
883 builder.updateCallGraph(callgraph);
884 pag->getICFG()->updateCallGraph(callgraph);
885 AbstractInterpretation& ae = AbstractInterpretation::getAEInstance();
886 if (Options::BufferOverflowCheck())
887 ae.addDetector(std::make_unique<BufOverflowDetector>());
888 ae.runOnModule(pag->getICFG());
889
890 LLVMModuleSet::releaseLLVMModuleSet();
891
892 return 0;
893}
main
int main(int argc, char **argv)
Definition ae.cpp:843
SYMABS
static Option< bool > SYMABS("symabs", "symbolic abstraction test", false)
AETEST
static Option< bool > AETEST("aetest", "abstract execution basic function test", false)
AETest
Definition ae.cpp:626
AETest::~AETest
~AETest()=default
AETest::AETest
AETest()=default
AETest::testBinaryOpStmt
void testBinaryOpStmt()
Definition ae.cpp:632
AETest::testAbsState
void testAbsState()
Definition ae.cpp:828
OptionBase::parseOptions
static std::vector< std::string > parseOptions(int argc, char *argv[], std::string description, std::string callFormat)
Definition CommandLine.h:75
SVF::AbstractInterpretation
AbstractInterpretation is same as Abstract Execution.
Definition AbstractInterpretation.h:103
SVF::AbstractInterpretation::getAEInstance
static AbstractInterpretation & getAEInstance()
Definition AbstractInterpretation.h:121
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
SVF::AndersenWaveDiff::createAndersenWaveDiff
static AndersenWaveDiff * createAndersenWaveDiff(SVFIR *_pag)
Create an singleton instance directly instead of invoking llvm pass manager.
Definition Andersen.h:408
SVF::ICFG::updateCallGraph
void updateCallGraph(PTACallGraph *callgraph)
update ICFG for indirect calls
Definition ICFG.cpp:419
SVF::IntervalValue::minus_infinity
static BoundedInt minus_infinity()
Get minus infinity -inf.
Definition IntervalValue.h:77
SVF::IntervalValue::bottom
static IntervalValue bottom()
Create the bottom IntervalValue [+inf, -inf].
Definition IntervalValue.h:100
SVF::IntervalValue::plus_infinity
static BoundedInt plus_infinity()
Get plus infinity +inf.
Definition IntervalValue.h:83
SVF::IntervalValue::top
static IntervalValue top()
Create the IntervalValue [-inf, +inf].
Definition IntervalValue.h:94
SVF::LLVMModuleSet::getLLVMModuleSet
static LLVMModuleSet * getLLVMModuleSet()
Definition LLVMModule.h:122
SVF::LLVMModuleSet::releaseLLVMModuleSet
static void releaseLLVMModuleSet()
Definition LLVMModule.h:129
SVF::LLVMModuleSet::buildSVFModule
static SVFModule * buildSVFModule(Module &mod)
Definition LLVMModule.cpp:111
SVF::Options::BufferOverflowCheck
static const Option< bool > BufferOverflowCheck
buffer overflow checker, Default: false
Definition Options.h:252
SVF::PointerAnalysis::getCallGraph
PTACallGraph * getCallGraph() const
Return call graph.
Definition PointerAnalysis.h:171
SVF::SVFIR::getICFG
ICFG * getICFG() const
Definition SVFIR.h:172
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
SymblicAbstractionTest::BS_time
AbstractState BS_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:95
SymblicAbstractionTest::testRelExeState1_2
void testRelExeState1_2()
Definition ae.cpp:142
SymblicAbstractionTest::SymblicAbstractionTest
SymblicAbstractionTest()=default
SymblicAbstractionTest::testRelExeState2_4
void testRelExeState2_4()
Definition ae.cpp:305
SymblicAbstractionTest::testRelExeState2_1
void testRelExeState2_1()
Definition ae.cpp:177
SymblicAbstractionTest::testRelExeState2_2
void testRelExeState2_2()
Definition ae.cpp:219
SymblicAbstractionTest::testRelExeState3_2
void testRelExeState3_2()
Definition ae.cpp:433
SymblicAbstractionTest::~SymblicAbstractionTest
~SymblicAbstractionTest()=default
SymblicAbstractionTest::testsValidation
void testsValidation()
Definition ae.cpp:603
SymblicAbstractionTest::testRelExeState2_3
void testRelExeState2_3()
Definition ae.cpp:262
SymblicAbstractionTest::testRelExeState3_3
void testRelExeState3_3()
Definition ae.cpp:475
SymblicAbstractionTest::RSY_time
AbstractState RSY_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:71
SymblicAbstractionTest::testRelExeState4_1
void testRelExeState4_1()
Definition ae.cpp:558
SymblicAbstractionTest::testRelExeState2_5
void testRelExeState2_5()
Definition ae.cpp:348
SymblicAbstractionTest::testRelExeState3_1
void testRelExeState3_1()
Definition ae.cpp:391
SymblicAbstractionTest::testRelExeState1_1
void testRelExeState1_1()
Definition ae.cpp:108
SymblicAbstractionTest::Bilateral_time
AbstractState Bilateral_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:83
SymblicAbstractionTest::getContext
static z3::context & getContext()
Definition ae.cpp:61
SymblicAbstractionTest::testRelExeState3_4
void testRelExeState3_4()
Definition ae.cpp:516
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
SVF::SVFUtil::outs
std::ostream & outs()
Overwrite llvm::outs()
Definition SVFUtil.h:50
SVF
for isBitcode
Definition BasicTypes.h:68
SVF::IRBuilder
llvm::IRBuilder IRBuilder
Definition BasicTypes.h:74
Generated by doxygen 1.9.8