1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
#include "AST.h"
using namespace BEEV;
int main()
{
const int size = 32;
BeevMgr *bm = new BeevMgr();
ASTNode s1 = bm->CreateSymbol("x");
s1.SetValueWidth(size);
cout << "s1" << s1 << endl;
ASTNode s2 = bm->CreateSymbol("y");
s2.SetValueWidth(size);
cout << "s2" << s2 << endl;
ASTNode s3 = bm->CreateSymbol("z");
s3.SetValueWidth(size);
cout << "s3" << s3 << endl;
ASTNode c1 = bm->CreateBVConst(size,0);
cout << "c1" << c1 << endl;
ASTVec bbc1 = bm->BBTerm(c1);
cout << "bitblasted c1 " << endl;
LispPrintVec(cout, bbc1, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
ASTNode c2 = bm->CreateBVConst(size,1);
c2.SetValueWidth(size);
cout << "c2" << c2 << endl;
ASTVec bbc2 = bm->BBTerm(c2);
cout << "bitblasted c2 " << endl;
LispPrintVec(cout, bbc2, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
ASTNode c3 = bm->CreateBVConst(size, 0xFFFFFFFF);
c3.SetValueWidth(size);
cout << "c3" << c3 << endl;
ASTVec bbc3 = bm->BBTerm(c3);
cout << "bitblasted c3 " << endl;
LispPrintVec(cout, bbc3, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
ASTNode c4 = bm->CreateBVConst(size, 0xAAAAAAAA);
c4.SetValueWidth(size);
cout << "c4" << c4 << endl;
ASTVec bbc4 = bm->BBTerm(c4);
cout << "bitblasted c4 " << endl;
LispPrintVec(cout, bbc4, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
// ASTNode b1 = bm->CreateBVConst(12);
// ASTNode b2 = bm->CreateBVConst(36);
// cout << "b1: " << b1 << endl;
// cout << "b2: " << b2 << endl;
ASTNode a1 = bm->CreateNode(BVPLUS, s1, s2);
a1.SetValueWidth(size);
ASTVec& bba1 = bm->BBTerm(a1);
cout << "bitblasted a1 " << endl;
LispPrintVec(cout, bba1, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
ASTNode a2 = bm->CreateNode(BVPLUS, s1, s2, s3);
a1.SetValueWidth(2);
ASTVec& bba2 = bm->BBTerm(a2);
cout << "bitblasted a2 " << endl;
LispPrintVec(cout, bba2, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
ASTNode a3 = bm->CreateNode(BVXOR, s1, s2);
a3.SetValueWidth(2);
ASTVec& bba3 = bm->BBTerm(a3);
cout << "bitblasted a3 " << endl;
LispPrintVec(cout, bba3, 0);
cout << endl;
bm->AlreadyPrintedSet.clear();
ASTNode a4 = bm->CreateNode(EQ, s1, s2);
ASTNode bba4 = bm->BBForm(a4);
cout << "bitblasted a4 " << endl << bba4 << endl;
ASTNode a5 = bm->CreateNode(BVLE, s1, s2);
ASTNode bba5 = bm->BBForm(a5);
cout << "bitblasted a5 " << endl << bba5 << endl;
return 0;
}
|