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#include <chrono>
38
39using namespace SVF;
40using namespace SVFUtil;
41
42
43static Option<bool> SYMABS(
44 "symabs",
45 "symbolic abstraction test",
46 false
47);
48
49static Option<bool> AETEST(
50 "aetest",
51 "abstract execution basic function test",
52 false
53);
54
55class SymblicAbstractionTest
56{
57public:
58 SymblicAbstractionTest() = default;
59
60 ~SymblicAbstractionTest() = default;
61
62 static z3::context& getContext()
63 {
64 return Z3Expr::getContext();
65 }
66
67 void test_print()
68 {
69 outs() << "hello print\n";
70 }
71
72 AbstractState RSY_time(AbstractState& inv, const Z3Expr& phi,
73 RelationSolver& rs)
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 }
84 AbstractState Bilateral_time(AbstractState& inv, const Z3Expr& phi,
85 RelationSolver& rs)
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 }
96 AbstractState BS_time(AbstractState& inv, const Z3Expr& phi,
97 RelationSolver& rs)
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 }
108
109 void testRelExeState1_1()
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 }
142
143 void testRelExeState1_2()
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 }
177
178 void testRelExeState2_1()
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 }
219
220 void testRelExeState2_2()
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 }
262
263 void testRelExeState2_3()
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 }
305
306 void testRelExeState2_4()
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 }
348
349 void testRelExeState2_5()
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 }
391
392 void testRelExeState3_1()
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 }
433
434 void testRelExeState3_2()
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 }
475
476 void testRelExeState3_3()
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 }
516
517 void testRelExeState3_4()
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 }
558
559 void testRelExeState4_1()
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 }
603
604 void testsValidation()
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 }
624};
625
626class AETest
627{
628public:
629 AETest() = default;
630
631 ~AETest() = default;
632
633 void testBinaryOpStmt()
634 {
635 // test division /
636 assert((IntervalValue(4) / IntervalValue::bottom()).equals(IntervalValue::bottom()));
637 assert((IntervalValue::bottom() / IntervalValue(2)).equals(IntervalValue::bottom()));
638 assert((IntervalValue::top() / IntervalValue(0)).equals(IntervalValue::bottom()));
639 assert((IntervalValue(4) / IntervalValue(2)).equals(IntervalValue(2)));
640 assert((IntervalValue(3) / IntervalValue(2)).equals(IntervalValue(1))); //
641 assert((IntervalValue(-3) / IntervalValue(2)).equals(IntervalValue(-1))); //
642 assert((IntervalValue(1, 3) / IntervalValue(2)).equals(IntervalValue(0, 1))); //
643 assert((IntervalValue(2, 7) / IntervalValue(2)).equals(IntervalValue(1, 3))); //
644 assert((IntervalValue(-3, 3) / IntervalValue(2)).equals(IntervalValue(-1, 1)));
645 assert((IntervalValue(-3, IntervalValue::plus_infinity()) / IntervalValue(2)).equals(IntervalValue(-1, IntervalValue::plus_infinity())));
646 assert((IntervalValue(IntervalValue::minus_infinity(), 3) / IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity(), 1)));
647 assert((IntervalValue(1, 3) / IntervalValue(1, 2)).equals(IntervalValue(0, 3)));//
648 assert((IntervalValue(-3, 3) / IntervalValue(1, 2)).equals(IntervalValue(-3, 3)));
649 assert((IntervalValue(2, 7) / IntervalValue(-2, 3)).equals(IntervalValue(-7, 7))); //
650 assert((IntervalValue(-2, 7) / IntervalValue(-2, 3)).equals(IntervalValue(-7, 7))); //
651 assert((IntervalValue(IntervalValue::minus_infinity(), 7) / IntervalValue(-2, 3)).equals(IntervalValue::top()));
652 assert((IntervalValue(-2, IntervalValue::plus_infinity()) / IntervalValue(-2, 3)).equals(IntervalValue::top()));
653
654 assert((IntervalValue(-2, 7) / IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue(-7, 7)));
655 assert((IntervalValue(-2, 7) / IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue(-7, 7)));
656 assert((IntervalValue(-6, -3) / IntervalValue(3, 9)).equals(IntervalValue(-2, 0)));
657 assert((IntervalValue(-6, 6) / IntervalValue(3, 9)).equals(IntervalValue(-2, 2)));
658
659 // test remainder %
660 assert((IntervalValue(4) % IntervalValue::bottom()).equals(IntervalValue::bottom()));
661 assert((IntervalValue::bottom() % IntervalValue(2)).equals(IntervalValue::bottom()));
662 assert((IntervalValue::top() % IntervalValue(0)).equals(IntervalValue::top()));
663 assert((IntervalValue(4) % IntervalValue(2)).equals(IntervalValue(0)));
664 assert((IntervalValue(3) % IntervalValue(2)).equals(IntervalValue(1)));
665 assert((IntervalValue(-3) % IntervalValue(2)).equals(IntervalValue(-1)));
666 assert((IntervalValue(1, 3) % IntervalValue(2)).equals(IntervalValue(0, 1)));
667 assert((IntervalValue(2, 7) % IntervalValue(2)).equals(IntervalValue(0, 1)));
668 assert((IntervalValue(-3, 3) % IntervalValue(2)).equals(IntervalValue(-1, 1)));
669 assert((IntervalValue(-3, IntervalValue::plus_infinity()) % IntervalValue(2)).equals(IntervalValue(-1, 1)));
670 assert((IntervalValue(IntervalValue::minus_infinity(), 3) % IntervalValue(2)).equals(IntervalValue(-1, 1)));
671 assert((IntervalValue(1, 3) % IntervalValue(1, 2)).equals(IntervalValue(0, 1)));
672 assert((IntervalValue(-3, 3) % IntervalValue(1, 2)).equals(IntervalValue(-1, 1)));
673 assert((IntervalValue(2, 7) % IntervalValue(-2, 3)).equals(IntervalValue::top())); //
674 assert((IntervalValue(-2, 7) % IntervalValue(-2, 3)).equals(IntervalValue::top())); //
675 assert((IntervalValue(IntervalValue::minus_infinity(), 7) % IntervalValue(-2, 3)).equals(IntervalValue::top()));
676 assert((IntervalValue(-2, IntervalValue::plus_infinity()) % IntervalValue(-2, 3)).equals(IntervalValue::top()));
677 assert((IntervalValue(-2, 7) % IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
678 assert((IntervalValue(-2, 7) % IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
679 assert((IntervalValue(-6, -3) % IntervalValue(3, 9)).equals(IntervalValue(-6, 0)));
680 assert((IntervalValue(-6, 6) % IntervalValue(3, 9)).equals(IntervalValue(-6, 6)));
681
682 // shl <<
683 assert((IntervalValue(IntervalValue::plus_infinity()) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
684 assert((IntervalValue(IntervalValue::plus_infinity()) << IntervalValue(2, 2)).equals(IntervalValue(IntervalValue::plus_infinity())));
685 assert((IntervalValue(IntervalValue::minus_infinity()) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
686 assert((IntervalValue(IntervalValue::minus_infinity()) << IntervalValue(2, 2)).equals(IntervalValue(IntervalValue::minus_infinity())));
687 assert((IntervalValue(2, 2) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
688 assert((IntervalValue(0, 0) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(0, 0)));
689 assert((IntervalValue(0) << IntervalValue(31)).equals(IntervalValue(0)));
690 assert((IntervalValue(0) << IntervalValue(31, 32)).equals(IntervalValue(0)));
691 assert((IntervalValue(0) << IntervalValue(-1)).equals(IntervalValue::bottom()));
692 assert((IntervalValue(0) << IntervalValue::bottom()).equals(IntervalValue::bottom()));
693 assert((IntervalValue(1) << IntervalValue(31)).equals(IntervalValue::top()));
694 assert((IntervalValue(-2, -2) << IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::top())));
695 assert((IntervalValue(0, 0) << IntervalValue(2, 2)).equals(IntervalValue(0, 0)));
696 assert((IntervalValue(2, 2) << IntervalValue(3, 3)).equals(IntervalValue(16, 16)));
697 assert((IntervalValue(-2, -2) << IntervalValue(3, 3)).equals(IntervalValue(-16, -16)));
698
699 assert((IntervalValue(4) << IntervalValue::bottom()).equals(IntervalValue::bottom()));
700 assert((IntervalValue::bottom() << IntervalValue(2)).equals(IntervalValue::bottom()));
701 assert((IntervalValue::top() << IntervalValue(0)).equals(IntervalValue::top()));
702 assert((IntervalValue(4) << IntervalValue(2)).equals(IntervalValue(16)));
703 assert((IntervalValue(3) << IntervalValue(2)).equals(IntervalValue(12)));
704 assert((IntervalValue(-3) << IntervalValue(2)).equals(IntervalValue(-12)));
705 assert((IntervalValue(4) << IntervalValue(-2)).equals(IntervalValue::bottom()));
706 assert((IntervalValue(1, 3) << IntervalValue(2)).equals(IntervalValue(4, 12)));
707 assert((IntervalValue(2, 7) << IntervalValue(2)).equals(IntervalValue(8, 28)));
708 assert((IntervalValue(-3, 3) << IntervalValue(2)).equals(IntervalValue(-12, 12)));
709 assert((IntervalValue(-3, IntervalValue::plus_infinity()) << IntervalValue(2)).equals(IntervalValue(-12, IntervalValue::plus_infinity())));
710 assert((IntervalValue(IntervalValue::minus_infinity(), 3) << IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity(), 12)));
711 assert((IntervalValue(1, 3) << IntervalValue(1, 2)).equals(IntervalValue(2, 12)));
712 assert((IntervalValue(-3, 3) << IntervalValue(1, 2)).equals(IntervalValue(-12, 12)));
713 assert((IntervalValue(2, 7) << IntervalValue(-2, 3)).equals(IntervalValue(2, 56)));
714 assert((IntervalValue(-2, 7) << IntervalValue(-2, 3)).equals(IntervalValue(-16, 56)));
715 assert((IntervalValue(IntervalValue::minus_infinity(), 7) << IntervalValue(-2, 3)).equals(IntervalValue(IntervalValue::minus_infinity(), 56)));
716 assert((IntervalValue(-2, IntervalValue::plus_infinity()) << IntervalValue(-2, 3)).equals(IntervalValue(-16, IntervalValue::plus_infinity())));
717 assert((IntervalValue(-2, 7) << IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue(-16, 56)));
718 assert((IntervalValue(-2, 7) << IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
719 assert((IntervalValue(-6, -3) << IntervalValue(3, 9)).equals(IntervalValue(-3072, -24)));
720 assert((IntervalValue(-6, 6) << IntervalValue(3, 9)).equals(IntervalValue(-3072, 3072)));
721 assert((IntervalValue(-2, 7) << IntervalValue(IntervalValue::minus_infinity(), -1)).equals(IntervalValue::bottom()));
722 assert((IntervalValue(0) << IntervalValue::top()).equals(IntervalValue(0)));
723
724
725 // shr >>
726 assert((IntervalValue(IntervalValue::plus_infinity()) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::plus_infinity())));
727 assert((IntervalValue(IntervalValue::plus_infinity()) >> IntervalValue(2)).equals(IntervalValue(IntervalValue::plus_infinity())));
728 assert((IntervalValue(IntervalValue::minus_infinity()) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(IntervalValue::minus_infinity())));
729 assert((IntervalValue(IntervalValue::minus_infinity()) >> IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity())));
730 assert((IntervalValue(2) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(0)));
731 assert((IntervalValue(0) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(0)));
732 assert((IntervalValue(-2) >> IntervalValue(IntervalValue::plus_infinity())).equals(IntervalValue(-1)));
733 assert((IntervalValue(0) >> IntervalValue(2)).equals(IntervalValue(0)));
734 assert((IntervalValue(15) >> IntervalValue(2)).equals(IntervalValue(3)));
735 assert((IntervalValue(-15) >> IntervalValue(2)).equals(IntervalValue(-4)));
736
737 assert((IntervalValue(4) >> IntervalValue::bottom()).equals(IntervalValue::bottom()));
738 assert((IntervalValue::bottom() >> IntervalValue(2)).equals(IntervalValue::bottom()));
739 assert((IntervalValue::top() >> IntervalValue(0)).equals(IntervalValue::top()));
740 assert((IntervalValue(15) >> IntervalValue(2)).equals(IntervalValue(3)));
741 assert((IntervalValue(1) >> IntervalValue(2)).equals(IntervalValue(0)));
742 assert((IntervalValue(-15) >> IntervalValue(2)).equals(IntervalValue(-4)));
743 assert((IntervalValue(4) >> IntervalValue(-2)).equals(IntervalValue::bottom()));
744 assert((IntervalValue(1, 3) >> IntervalValue(2)).equals(IntervalValue(0)));
745 assert((IntervalValue(2, 7) >> IntervalValue(2)).equals(IntervalValue(0, 1)));
746 assert((IntervalValue(-15, 15) >> IntervalValue(2)).equals(IntervalValue(-4, 3)));
747 assert((IntervalValue(-15, IntervalValue::plus_infinity()) >> IntervalValue(2)).equals(IntervalValue(-4, IntervalValue::plus_infinity())));
748 assert((IntervalValue(IntervalValue::minus_infinity(), 15) >> IntervalValue(2)).equals(IntervalValue(IntervalValue::minus_infinity(), 3)));
749 assert((IntervalValue(0, 15) >> IntervalValue(1, 2)).equals(IntervalValue(0, 7)));
750 assert((IntervalValue(-17, 15) >> IntervalValue(1, 2)).equals(IntervalValue(-9, 7)));
751 assert((IntervalValue(2, 7) >> IntervalValue(-2, 3)).equals(IntervalValue(0, 7)));
752 assert((IntervalValue(-2, 7) >> IntervalValue(-2, 3)).equals(IntervalValue(-2, 7)));
753 assert((IntervalValue(IntervalValue::minus_infinity(), 7) >> IntervalValue(-2, 3)).equals(IntervalValue(IntervalValue::minus_infinity(), 7)));
754 assert((IntervalValue(-2, IntervalValue::plus_infinity()) >> IntervalValue(-2, 3)).equals(IntervalValue(-2, IntervalValue::plus_infinity())));
755 assert((IntervalValue(-2, 7) >> IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue(-2, 7)));
756 assert((IntervalValue(-2, 7) >> IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue(-2, 7)));
757 assert((IntervalValue(-6, -3) >> IntervalValue(2, 3)).equals(IntervalValue(-2, -1)));
758 assert((IntervalValue(-6, 6) >> IntervalValue(2, 3)).equals(IntervalValue(-2, 1)));
759 assert((IntervalValue(-2, 7) >> IntervalValue(IntervalValue::minus_infinity(), -1)).equals(IntervalValue::bottom()));
760 assert((IntervalValue(0) >> IntervalValue::top()).equals(IntervalValue(0)));
761
762 // and &
763 assert((IntervalValue(4) & IntervalValue::bottom()).equals(IntervalValue::bottom()));
764 assert((IntervalValue::bottom() & IntervalValue(2)).equals(IntervalValue::bottom()));
765 assert((IntervalValue::top() & IntervalValue(0)).equals(IntervalValue(0)));
766 assert((IntervalValue(4) & IntervalValue(2)).equals(IntervalValue(0)));
767 assert((IntervalValue(3) & IntervalValue(2)).equals(IntervalValue(2)));
768 assert((IntervalValue(-3) & IntervalValue(2)).equals(IntervalValue(0)));
769 assert((IntervalValue(1, 3) & IntervalValue(2)).equals(IntervalValue(0, 2)));
770 assert((IntervalValue(2, 7) & IntervalValue(2)).equals(IntervalValue(0, 2)));
771 assert((IntervalValue(-3, 3) & IntervalValue(2)).equals(IntervalValue(0, 2)));
772 assert((IntervalValue(-3, IntervalValue::plus_infinity()) & IntervalValue(2)).equals(IntervalValue(0, 2)));
773 assert((IntervalValue(IntervalValue::minus_infinity(), 3) & IntervalValue(2)).equals(IntervalValue(0, 2)));
774 assert((IntervalValue(1, 3) & IntervalValue(1, 2)).equals(IntervalValue(0, 2)));
775 assert((IntervalValue(-3, 3) & IntervalValue(1, 2)).equals(IntervalValue(0, 2)));
776 assert((IntervalValue(2, 7) & IntervalValue(-2, 3)).equals(IntervalValue(0, 7)));
777 assert((IntervalValue(-2, 7) & IntervalValue(-2, 3)).equals(IntervalValue::top()));
778 assert((IntervalValue(IntervalValue::minus_infinity(), 7) & IntervalValue(-2, 3)).equals(IntervalValue::top()));
779 assert((IntervalValue(-2, IntervalValue::plus_infinity()) & IntervalValue(-2, 3)).equals(IntervalValue::top()));
780 assert((IntervalValue(-2, 7) & IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
781 assert((IntervalValue(-2, 7) & IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
782 assert((IntervalValue(-6, -3) & IntervalValue(3, 9)).equals(IntervalValue(0, 9)));
783 assert((IntervalValue(-6, 6) & IntervalValue(3, 9)).equals(IntervalValue(0, 9)));
784
785 // Or |
786 assert((IntervalValue(4) | IntervalValue::bottom()).equals(IntervalValue::bottom()));
787 assert((IntervalValue::bottom() | IntervalValue(2)).equals(IntervalValue::bottom()));
788 assert((IntervalValue::top() | IntervalValue(-1)).equals(IntervalValue::top()));//
789 assert((IntervalValue(-1) | IntervalValue::top()).equals(IntervalValue::top()));//
790 assert((IntervalValue(4) | IntervalValue(2)).equals(IntervalValue(6)));
791 assert((IntervalValue(3) | IntervalValue(2)).equals(IntervalValue(3)));
792 assert((IntervalValue(-3) | IntervalValue(2)).equals(IntervalValue(-1)));
793 assert((IntervalValue(1, 3) | IntervalValue(2)).equals(IntervalValue(0, 3)));
794 assert((IntervalValue(2, 7) | IntervalValue(2)).equals(IntervalValue(0, 7)));
795 assert((IntervalValue(-3, 3) | IntervalValue(2)).equals(IntervalValue::top()));
796 assert((IntervalValue(-3, IntervalValue::plus_infinity()) | IntervalValue(2)).equals(IntervalValue::top()));
797 assert((IntervalValue(IntervalValue::minus_infinity(), 3) | IntervalValue(2)).equals(IntervalValue::top()));
798 assert((IntervalValue(1, 3) | IntervalValue(1, 2)).equals(IntervalValue(0, 3)));
799 assert((IntervalValue(-3, 3) | IntervalValue(1, 2)).equals(IntervalValue::top()));
800 assert((IntervalValue(2, 7) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
801 assert((IntervalValue(-2, 7) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
802 assert((IntervalValue(IntervalValue::minus_infinity(), 7) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
803 assert((IntervalValue(-2, IntervalValue::plus_infinity()) | IntervalValue(-2, 3)).equals(IntervalValue::top()));
804 assert((IntervalValue(-2, 7) | IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
805 assert((IntervalValue(-2, 7) | IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
806 assert((IntervalValue(-6, -3) | IntervalValue(3, 9)).equals(IntervalValue::top()));
807 assert((IntervalValue(-6, 6) | IntervalValue(3, 9)).equals(IntervalValue::top()));
808
809 // Xor ^
810 assert((IntervalValue(4) ^ IntervalValue::bottom()).equals(IntervalValue::bottom()));
811 assert((IntervalValue::bottom() ^ IntervalValue(2)).equals(IntervalValue::bottom()));
812 assert((IntervalValue::top() ^ IntervalValue(-1)).equals(IntervalValue::top()));
813 assert((IntervalValue(-1) ^ IntervalValue::top()).equals(IntervalValue::top()));
814 assert((IntervalValue(4) ^ IntervalValue(2)).equals(IntervalValue(6)));
815 assert((IntervalValue(3) ^ IntervalValue(2)).equals(IntervalValue(1)));
816 assert((IntervalValue(-3) ^ IntervalValue(2)).equals(IntervalValue(-1)));
817 assert((IntervalValue(1, 3) ^ IntervalValue(2)).equals(IntervalValue(0, 3)));
818 assert((IntervalValue(2, 7) ^ IntervalValue(2)).equals(IntervalValue(0, 7)));
819 assert((IntervalValue(-3, 3) ^ IntervalValue(2)).equals(IntervalValue::top()));
820 assert((IntervalValue(-3, IntervalValue::plus_infinity()) ^ IntervalValue(2)).equals(IntervalValue::top()));
821 assert((IntervalValue(IntervalValue::minus_infinity(), 3) ^ IntervalValue(2)).equals(IntervalValue::top()));
822 assert((IntervalValue(1, 3) ^ IntervalValue(1, 2)).equals(IntervalValue(0, 3)));
823 assert((IntervalValue(-3, 3) ^ IntervalValue(1, 2)).equals(IntervalValue::top()));
824 assert((IntervalValue(2, 7) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
825 assert((IntervalValue(-2, 7) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
826 assert((IntervalValue(IntervalValue::minus_infinity(), 7) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
827 assert((IntervalValue(-2, IntervalValue::plus_infinity()) ^ IntervalValue(-2, 3)).equals(IntervalValue::top()));
828 assert((IntervalValue(-2, 7) ^ IntervalValue(IntervalValue::minus_infinity(), 3)).equals(IntervalValue::top()));
829 assert((IntervalValue(-2, 7) ^ IntervalValue(-2, IntervalValue::plus_infinity())).equals(IntervalValue::top()));
830 assert((IntervalValue(-6, -3) ^ IntervalValue(3, 9)).equals(IntervalValue::top()));
831 assert((IntervalValue(-6, 6) ^ IntervalValue(3, 9)).equals(IntervalValue::top()));
832 }
833
834 void testAbsState()
835 {
836 AbstractState as;
837 as[1] = IntervalValue(1, 3);
838 as[2] = IntervalValue(2, 7);
839 as[3] = AddressValue(0x7f000007);
840 as[4] = AddressValue(0x7f000008);
841 // store: *as[3] = as[1], *as[4] = as[2]
842 for (auto addr : as[3].getAddrs()) as.store(addr, as[1]);
843 for (auto addr : as[4].getAddrs()) as.store(addr, as[2]);
844 as.printAbstractState();
845 // load: verify *as[3] == as[1] && *as[4] == as[2]
846 AbstractValue v3, v4;
847 for (auto addr : as[3].getAddrs()) v3.join_with(as.load(addr));
848 for (auto addr : as[4].getAddrs()) v4.join_with(as.load(addr));
849 assert(v3.equals(as[1]) && v4.equals(as[2]));
850 }
851};
852
853
854int main(int argc, char** argv)
855{
856 int arg_num = 0;
857 int extraArgc = 3;
858 char **arg_value = new char *[argc + extraArgc];
859 for (; arg_num < argc; ++arg_num)
860 {
861 arg_value[arg_num] = argv[arg_num];
862 }
863 // add extra options
864 arg_value[arg_num++] = (char*) "-model-consts=true";
865 arg_value[arg_num++] = (char*) "-model-arrays=true";
866 arg_value[arg_num++] = (char*) "-pre-field-sensitive=false";
867 assert(arg_num == (argc + extraArgc) && "more extra arguments? Change the value of extraArgc");
868
869 std::vector<std::string> moduleNameVec;
870 moduleNameVec = OptionBase::parseOptions(
871 arg_num, arg_value, "Static Symbolic Execution", "[options] <input-bitcode...>"
872 );
873 delete[] arg_value;
874 if (SYMABS())
875 {
876 SymblicAbstractionTest saTest;
877 saTest.testsValidation();
878 return 0;
879 }
880
881 if (AETEST())
882 {
883 AETest aeTest;
884 aeTest.testBinaryOpStmt();
885 aeTest.testAbsState();
886 return 0;
887 }
888
889 LLVMModuleSet::getLLVMModuleSet()->buildSVFModule(moduleNameVec);
890 SVFIRBuilder builder;
891 SVFIR* pag = builder.build();
892 // Run Andersen's to resolve indirect calls, then update SVFIR with resolved targets.
893 // The Andersen singleton will be reused inside AbstractInterpretation::runOnModule().
894 AndersenWaveDiff* ander = AndersenWaveDiff::createAndersenWaveDiff(pag);
895 builder.updateCallGraph(ander->getCallGraph());
896 AbstractInterpretation& ae = AbstractInterpretation::getAEInstance();
897 if (Options::BufferOverflowCheck())
898 ae.addDetector(std::make_unique<BufOverflowDetector>());
899 if (Options::NullDerefCheck())
900 ae.addDetector(std::make_unique<NullptrDerefDetector>());
901 ae.runOnModule();
902
903 AndersenWaveDiff::releaseAndersenWaveDiff();
904 LLVMModuleSet::releaseLLVMModuleSet();
905
906 return 0;
907}
main
int main(int argc, char **argv)
Definition ae.cpp:854
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:627
AETest::~AETest
~AETest()=default
AETest::AETest
AETest()=default
AETest::testBinaryOpStmt
void testBinaryOpStmt()
Definition ae.cpp:633
AETest::testAbsState
void testAbsState()
Definition ae.cpp:834
OptionBase::parseOptions
static std::vector< std::string > parseOptions(int argc, char *argv[], std::string description, std::string callFormat)
Definition CommandLine.h:75
SVF::AbstractInterpretation::addDetector
void addDetector(std::unique_ptr< AEDetector > detector)
Definition AbstractInterpretation.h:124
SVF::AbstractInterpretation::getAEInstance
static AbstractInterpretation & getAEInstance()
Definition AbstractInterpretation.cpp:76
SVF::AbstractState::getVarToVal
const VarToAbsValMap & getVarToVal() const
get var2val map
Definition AbstractState.h:252
SVF::AbstractState::store
void store(u32_t addr, const AbstractValue &val)
Definition AbstractState.h:196
SVF::AbstractState::printAbstractState
void printAbstractState() const
Definition AbstractState.cpp:209
SVF::AbstractState::eqVarToValMap
bool eqVarToValMap(const VarToAbsValMap &lhs, const VarToAbsValMap &rhs) const
Definition AbstractState.cpp:319
SVF::AbstractState::load
virtual AbstractValue & load(u32_t addr)
Definition AbstractState.h:182
SVF::AbstractState::VarToAbsValMap
Map< u32_t, AbstractValue > VarToAbsValMap
Definition AbstractState.h:61
SVF::AbstractState::sliceState
AbstractState sliceState(Set< u32_t > &sl)
Copy some values and return a new IntervalExeState.
Definition AbstractState.h:133
SVF::AbstractValue::join_with
void join_with(const AbstractValue &other)
Definition AbstractValue.h:128
SVF::AbstractValue::equals
bool equals(const AbstractValue &rhs) const
Definition AbstractValue.h:123
SVF::AndersenWaveDiff::createAndersenWaveDiff
static AndersenWaveDiff * createAndersenWaveDiff(SVFIR *_pag)
Create an singleton instance directly instead of invoking llvm pass manager.
Definition Andersen.h:430
SVF::AndersenWaveDiff::releaseAndersenWaveDiff
static void releaseAndersenWaveDiff()
Definition Andersen.h:440
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:137
SVF::LLVMModuleSet::releaseLLVMModuleSet
static void releaseLLVMModuleSet()
Definition LLVMModule.h:144
SVF::LLVMModuleSet::buildSVFModule
static void buildSVFModule(Module &mod)
Definition LLVMModule.cpp:110
SVF::Options::NullDerefCheck
static const Option< bool > NullDerefCheck
nullptr dereference checker, Default: false
Definition Options.h:250
SVF::Options::BufferOverflowCheck
static const Option< bool > BufferOverflowCheck
buffer overflow checker, Default: false
Definition Options.h:248
SVF::PointerAnalysis::getCallGraph
CallGraph * getCallGraph() const
Return call graph.
Definition PointerAnalysis.h:122
SVF::RelExeState::extractSubVars
void extractSubVars(const Z3Expr &expr, Set< u32_t > &res)
Extract sub SVFVar IDs of a Z3Expr.
Definition RelExeState.cpp:45
SVF::RelationSolver::gamma_hat
Z3Expr gamma_hat(const AbstractState &exeState) const
Return Z3Expr according to valToValMap.
Definition RelationSolver.cpp:205
SVF::RelationSolver::RSY
AbstractState RSY(const AbstractState &domain, const Z3Expr &phi)
Definition RelationSolver.cpp:120
SVF::RelationSolver::bilateral
AbstractState bilateral(const AbstractState &domain, const Z3Expr &phi, u32_t descend_check=0)
Definition RelationSolver.cpp:42
SVF::RelationSolver::BS
AbstractState BS(const AbstractState &domain, const Z3Expr &phi)
Definition RelationSolver.cpp:276
SVF::SVFIRBuilder::updateCallGraph
void updateCallGraph(CallGraph *callgraph)
connect PAG edges based on callgraph
Definition SVFIRBuilder.cpp:2228
SVF::SVFIRBuilder::build
virtual SVFIR * build()
Start building SVFIR here.
Definition SVFIRBuilder.cpp:55
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:96
SymblicAbstractionTest::testRelExeState1_2
void testRelExeState1_2()
Definition ae.cpp:143
SymblicAbstractionTest::SymblicAbstractionTest
SymblicAbstractionTest()=default
SymblicAbstractionTest::testRelExeState2_4
void testRelExeState2_4()
Definition ae.cpp:306
SymblicAbstractionTest::testRelExeState2_1
void testRelExeState2_1()
Definition ae.cpp:178
SymblicAbstractionTest::testRelExeState2_2
void testRelExeState2_2()
Definition ae.cpp:220
SymblicAbstractionTest::testRelExeState3_2
void testRelExeState3_2()
Definition ae.cpp:434
SymblicAbstractionTest::~SymblicAbstractionTest
~SymblicAbstractionTest()=default
SymblicAbstractionTest::testsValidation
void testsValidation()
Definition ae.cpp:604
SymblicAbstractionTest::testRelExeState2_3
void testRelExeState2_3()
Definition ae.cpp:263
SymblicAbstractionTest::testRelExeState3_3
void testRelExeState3_3()
Definition ae.cpp:476
SymblicAbstractionTest::RSY_time
AbstractState RSY_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:72
SymblicAbstractionTest::testRelExeState4_1
void testRelExeState4_1()
Definition ae.cpp:559
SymblicAbstractionTest::testRelExeState2_5
void testRelExeState2_5()
Definition ae.cpp:349
SymblicAbstractionTest::testRelExeState3_1
void testRelExeState3_1()
Definition ae.cpp:392
SymblicAbstractionTest::testRelExeState1_1
void testRelExeState1_1()
Definition ae.cpp:109
SymblicAbstractionTest::Bilateral_time
AbstractState Bilateral_time(AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
Definition ae.cpp:84
SymblicAbstractionTest::getContext
static z3::context & getContext()
Definition ae.cpp:62
SymblicAbstractionTest::testRelExeState3_4
void testRelExeState3_4()
Definition ae.cpp:517
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
SVF::SVFUtil::outs
std::ostream & outs()
Overwrite llvm::outs().
Definition SVFUtil.h:58
SVF
for isBitcode
Definition BasicTypes.h:70
SVF::Set
std::unordered_set< Key, Hash, KeyEqual, Allocator > Set
Definition GeneralType.h:51
Generated by doxygen 1.15.0