Static Value-Flow Analysis
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 
38 using namespace SVF;
39 using namespace SVFUtil;
40 
41 
42 static Option<bool> SYMABS(
43  "symabs",
44  "symbolic abstraction test",
45  false
46 );
47 
48 static Option<bool> AETEST(
49  "aetest",
50  "abstract execution basic function test",
51  false
52 );
53 
54 class SymblicAbstractionTest
55 {
56 public:
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 
625 class AETest
626 {
627 public:
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 
843 int 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
AETEST
static Option< bool > AETEST("aetest", "abstract execution basic function test", false)
SYMABS
static Option< bool > SYMABS("symabs", "symbolic abstraction 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::addDetector
void addDetector(std::unique_ptr< AEDetector > detector)
Definition: AbstractInterpretation.h:127
SVF::AbstractInterpretation::runOnModule
virtual void runOnModule(ICFG *icfg)
Definition: AbstractInterpretation.cpp:40
SVF::AbstractInterpretation::getAEInstance
static AbstractInterpretation & getAEInstance()
Definition: AbstractInterpretation.h:121
SVF::AbstractState::printAbstractState
void printAbstractState() const
Definition: AbstractState.cpp:391
SVF::AbstractState::getVarToVal
const VarToAbsValMap & getVarToVal() const
get var2val map
Definition: AbstractState.h:260
SVF::AbstractState::loadValue
AbstractValue loadValue(NodeID varId)
Definition: AbstractState.cpp:373
SVF::AbstractState::VarToAbsValMap
Map< u32_t, AbstractValue > VarToAbsValMap
Definition: AbstractState.h:63
SVF::AbstractState::storeValue
void storeValue(NodeID varId, AbstractValue val)
Definition: AbstractState.cpp:383
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::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: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::releaseLLVMModuleSet
static void releaseLLVMModuleSet()
Definition: LLVMModule.h:125
SVF::LLVMModuleSet::getLLVMModuleSet
static LLVMModuleSet * getLLVMModuleSet()
Definition: LLVMModule.h:118
SVF::LLVMModuleSet::buildSVFModule
static SVFModule * buildSVFModule(Module &mod)
Definition: LLVMModule.cpp:102
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::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:199
SVF::RelationSolver::RSY
AbstractState RSY(const AbstractState &domain, const Z3Expr &phi)
Definition: RelationSolver.cpp:114
SVF::RelationSolver::bilateral
AbstractState bilateral(const AbstractState &domain, const Z3Expr &phi, u32_t descend_check=0)
Definition: RelationSolver.cpp:36
SVF::RelationSolver::BS
AbstractState BS(const AbstractState &domain, const Z3Expr &phi)
Definition: RelationSolver.cpp:270
SVF::SVFIRBuilder::updateCallGraph
void updateCallGraph(PTACallGraph *callgraph)
connect PAG edges based on callgraph
Definition: SVFIRBuilder.cpp:1192
SVF::SVFIRBuilder::build
virtual SVFIR * build()
Start building SVFIR here.
Definition: SVFIRBuilder.cpp:54
SVF::SVFIR::getICFG
ICFG * getICFG() const
Definition: SVFIR.h:171
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::test_print
void test_print()
Definition: ae.cpp:66
SymblicAbstractionTest::testRelExeState2_5
void testRelExeState2_5()
Definition: ae.cpp:348
SymblicAbstractionTest::getContext
static z3::context & getContext()
Definition: ae.cpp:61
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::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:53
SVF::SVFUtil::outs
std::ostream & outs()
Overwrite llvm::outs()
Definition: SVFUtil.h:50
SVF
for isBitcode
Definition: BasicTypes.h:68
SVF::Set
std::unordered_set< Key, Hash, KeyEqual, Allocator > Set
Definition: GeneralType.h:96
Generated by doxygen 1.9.1