-
Notifications
You must be signed in to change notification settings - Fork 1
/
bitwise_expr_lookup_tbl.cpp
168 lines (161 loc) · 11.6 KB
/
bitwise_expr_lookup_tbl.cpp
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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
/*
* Copyright (c) 2023 by Hex-Rays, [email protected]
* ALL RIGHTS RESERVED.
*
* gooMBA plugin for Hex-Rays Decompiler.
*
*/
#include "z3++_no_warn.h"
#include "bitwise_expr_lookup_tbl.hpp"
bw_expr_tbl_t bw_expr_tbl_t::instance;
bw_expr_tbl_t::bw_expr_tbl_t()
{
minsn_templates_t X;
X.push_back(std::make_shared<mt_varref_t>(0));
X.push_back(std::make_shared<mt_varref_t>(1));
X.push_back(std::make_shared<mt_varref_t>(2));
minsn_template_ptr_t zero = std::make_shared<mt_constant_t>(0ull);
// note that all expressions are ordered by the numeric value of the instruction trace
// see lin_conj_exprs.hpp for more info on ordering.
auto &onevar = tbl.push_back();
onevar.push_back(zero); // [0 0]
onevar.push_back(X[0]); // [0 1]
auto &twovar = tbl.push_back();
twovar.push_back(zero); // [0 0 0 0]
twovar.push_back(X[0]&~X[1]); // [0 1 0 0]
twovar.push_back(~(X[0]|~X[1])); // [0 0 1 0]
twovar.push_back(X[0]^X[1]); // [0 1 1 0]
twovar.push_back(X[0]&X[1]); // [0 0 0 1]
twovar.push_back(X[0]); // [0 1 0 1]
twovar.push_back(X[1]); // [0 0 1 1]
twovar.push_back(X[0]|X[1]); // [0 1 1 1]
auto &threevar = tbl.push_back();
threevar.push_back(zero); // [0 0 0 0 0 0 0 0]
threevar.push_back(~(~X[0]|(X[1]|X[2]))); // [0 1 0 0 0 0 0 0]
threevar.push_back(~(X[0]|(~X[1]|X[2]))); // [0 0 1 0 0 0 0 0]
threevar.push_back(~X[2]&(X[0]^X[1])); // [0 1 1 0 0 0 0 0]
threevar.push_back(~(~X[0]|(~X[1]|X[2]))); // [0 0 0 1 0 0 0 0]
threevar.push_back(X[0]&~X[2]); // [0 1 0 1 0 0 0 0]
threevar.push_back(X[1]&~X[2]); // [0 0 1 1 0 0 0 0]
threevar.push_back(X[2]^(X[0]|(X[1]|X[2]))); // [0 1 1 1 0 0 0 0]
threevar.push_back(~X[0]&(~X[1]&X[2])); // [0 0 0 0 1 0 0 0]
threevar.push_back(~X[1]&(X[0]^X[2])); // [0 1 0 0 1 0 0 0]
threevar.push_back(~X[0]&(X[1]^X[2])); // [0 0 1 0 1 0 0 0]
threevar.push_back(~(X[0]&X[1])&(X[0]^(X[1]^X[2]))); // [0 1 1 0 1 0 0 0]
threevar.push_back(~(X[0]^X[1])&(X[0]^X[2])); // [0 0 0 1 1 0 0 0]
threevar.push_back(X[2]^(X[0]|(X[1]&X[2]))); // [0 1 0 1 1 0 0 0]
threevar.push_back(~(X[0]&~X[1])&(X[1]^X[2])); // [0 0 1 1 1 0 0 0]
threevar.push_back(X[2]^(X[0]|X[1])); // [0 1 1 1 1 0 0 0]
threevar.push_back(X[0]&(~X[1]&X[2])); // [0 0 0 0 0 1 0 0]
threevar.push_back(X[0]&~X[1]); // [0 1 0 0 0 1 0 0]
threevar.push_back((X[0]^X[1])&~(X[0]^X[2])); // [0 0 1 0 0 1 0 0]
threevar.push_back(X[1]^(X[0]|(X[1]&X[2]))); // [0 1 1 0 0 1 0 0]
threevar.push_back(X[0]&(X[1]^X[2])); // [0 0 0 1 0 1 0 0]
threevar.push_back(~(~X[0]|(X[1]&X[2]))); // [0 1 0 1 0 1 0 0]
threevar.push_back((X[0]|X[1])&(X[1]^X[2])); // [0 0 1 1 0 1 0 0]
threevar.push_back((X[0]&X[1])^~(X[0]^(~X[1]|X[2]))); // [0 1 1 1 0 1 0 0]
threevar.push_back(~(X[1]|~X[2])); // [0 0 0 0 1 1 0 0]
threevar.push_back(X[1]^(X[0]|(X[1]|X[2]))); // [0 1 0 0 1 1 0 0]
threevar.push_back(~(X[0]&X[1])&(X[1]^X[2])); // [0 0 1 0 1 1 0 0]
threevar.push_back(X[1]^(X[0]|X[2])); // [0 1 1 0 1 1 0 0]
threevar.push_back((X[0]|~X[1])&(X[1]^X[2])); // [0 0 0 1 1 1 0 0]
threevar.push_back((X[0]&X[2])^(X[0]^(~X[1]&X[2]))); // [0 1 0 1 1 1 0 0]
threevar.push_back(X[1]^X[2]); // [0 0 1 1 1 1 0 0]
threevar.push_back((X[0]&~X[1])|(X[1]^X[2])); // [0 1 1 1 1 1 0 0]
threevar.push_back(~X[0]&(X[1]&X[2])); // [0 0 0 0 0 0 1 0]
threevar.push_back((X[0]^X[1])&(X[0]^X[2])); // [0 1 0 0 0 0 1 0]
threevar.push_back(~(X[0]|~X[1])); // [0 0 1 0 0 0 1 0]
threevar.push_back(X[1]^~(~X[0]|(~X[1]&X[2]))); // [0 1 1 0 0 0 1 0]
threevar.push_back(X[1]&(X[0]^X[2])); // [0 0 0 1 0 0 1 0]
threevar.push_back(X[2]^(X[0]|(~X[1]&X[2]))); // [0 1 0 1 0 0 1 0]
threevar.push_back(X[1]&~(X[0]&X[2])); // [0 0 1 1 0 0 1 0]
threevar.push_back(X[1]^~(~X[0]|(X[1]^X[2]))); // [0 1 1 1 0 0 1 0]
threevar.push_back(~(X[0]|~X[2])); // [0 0 0 0 1 0 1 0]
threevar.push_back(X[2]^(X[0]&(~X[1]|X[2]))); // [0 1 0 0 1 0 1 0]
threevar.push_back(~X[0]&(X[1]|X[2])); // [0 0 1 0 1 0 1 0]
threevar.push_back(X[0]^(X[1]|X[2])); // [0 1 1 0 1 0 1 0]
threevar.push_back(X[2]^(X[0]&(X[1]|X[2]))); // [0 0 0 1 1 0 1 0]
threevar.push_back(X[0]^X[2]); // [0 1 0 1 1 0 1 0]
threevar.push_back((X[0]&X[2])^(X[1]|X[2])); // [0 0 1 1 1 0 1 0]
threevar.push_back(X[2]^~(~X[0]&(~X[1]|X[2]))); // [0 1 1 1 1 0 1 0]
threevar.push_back(X[2]&(X[0]^X[1])); // [0 0 0 0 0 1 1 0]
threevar.push_back(X[1]^~(~X[0]&(~X[1]|X[2]))); // [0 1 0 0 0 1 1 0]
threevar.push_back(X[1]^(X[0]&(X[1]|X[2]))); // [0 0 1 0 0 1 1 0]
threevar.push_back(X[0]^X[1]); // [0 1 1 0 0 1 1 0]
threevar.push_back((X[0]|X[1])&~(X[0]^(X[1]^X[2]))); // [0 0 0 1 0 1 1 0]
threevar.push_back(X[0]^(X[1]&X[2])); // [0 1 0 1 0 1 1 0]
threevar.push_back(X[1]^(X[0]&X[2])); // [0 0 1 1 0 1 1 0]
threevar.push_back(X[1]^(X[0]&(~X[1]|X[2]))); // [0 1 1 1 0 1 1 0]
threevar.push_back(X[2]&~(X[0]&X[1])); // [0 0 0 0 1 1 1 0]
threevar.push_back(X[1]^(X[0]|(X[1]^X[2]))); // [0 1 0 0 1 1 1 0]
threevar.push_back((X[0]&X[1])^(X[1]|X[2])); // [0 0 1 0 1 1 1 0]
threevar.push_back(X[1]^(X[0]|(~X[1]&X[2]))); // [0 1 1 0 1 1 1 0]
threevar.push_back(X[2]^(X[0]&X[1])); // [0 0 0 1 1 1 1 0]
threevar.push_back(X[2]^~(~X[0]|(~X[1]&X[2]))); // [0 1 0 1 1 1 1 0]
threevar.push_back(~(X[0]|~X[1])|(X[1]^X[2])); // [0 0 1 1 1 1 1 0]
threevar.push_back((X[0]^X[1])|(X[0]^X[2])); // [0 1 1 1 1 1 1 0]
threevar.push_back(X[0]&(X[1]&X[2])); // [0 0 0 0 0 0 0 1]
threevar.push_back(~(~X[0]|(X[1]^X[2]))); // [0 1 0 0 0 0 0 1]
threevar.push_back(X[1]&~(X[0]^X[2])); // [0 0 1 0 0 0 0 1]
threevar.push_back((X[0]|X[1])&(X[0]^(X[1]^X[2]))); // [0 1 1 0 0 0 0 1]
threevar.push_back(X[0]&X[1]); // [0 0 0 1 0 0 0 1]
threevar.push_back(~(~X[0]|(~X[1]&X[2]))); // [0 1 0 1 0 0 0 1]
threevar.push_back(X[1]&(X[0]|~X[2])); // [0 0 1 1 0 0 0 1]
threevar.push_back((X[1]&~X[2])|~(~X[0]|(~X[1]&X[2]))); // [0 1 1 1 0 0 0 1]
threevar.push_back(X[2]&~(X[0]^X[1])); // [0 0 0 0 1 0 0 1]
threevar.push_back((X[0]|~X[1])&(X[0]^(X[1]^X[2]))); // [0 1 0 0 1 0 0 1]
threevar.push_back(~(X[0]&~X[1])&(X[0]^(X[1]^X[2]))); // [0 0 1 0 1 0 0 1]
threevar.push_back(X[0]^(X[1]^X[2])); // [0 1 1 0 1 0 0 1]
threevar.push_back(X[1]^(~X[0]&(X[1]|X[2]))); // [0 0 0 1 1 0 0 1]
threevar.push_back(X[0]^(~X[1]&X[2])); // [0 1 0 1 1 0 0 1]
threevar.push_back(X[1]^~(X[0]|~X[2])); // [0 0 1 1 1 0 0 1]
threevar.push_back((X[0]&X[1])|(X[0]^(X[1]^X[2]))); // [0 1 1 1 1 0 0 1]
threevar.push_back(X[0]&X[2]); // [0 0 0 0 0 1 0 1]
threevar.push_back(X[0]&(~X[1]|X[2])); // [0 1 0 0 0 1 0 1]
threevar.push_back(X[2]^(~X[0]&(X[1]|X[2]))); // [0 0 1 0 0 1 0 1]
threevar.push_back(~(X[0]^(~X[1]|X[2]))); // [0 1 1 0 0 1 0 1]
threevar.push_back(X[0]&(X[1]|X[2])); // [0 0 0 1 0 1 0 1]
threevar.push_back(X[0]); // [0 1 0 1 0 1 0 1]
threevar.push_back((X[0]&X[2])|(X[1]&~X[2])); // [0 0 1 1 0 1 0 1]
threevar.push_back(~(~X[0]&(~X[1]|X[2]))); // [0 1 1 1 0 1 0 1]
threevar.push_back(X[2]&(X[0]|~X[1])); // [0 0 0 0 1 1 0 1]
threevar.push_back((X[1]&~X[2])^(X[0]|(X[1]^X[2]))); // [0 1 0 0 1 1 0 1]
threevar.push_back(X[2]^~(X[0]|~X[1])); // [0 0 1 0 1 1 0 1]
threevar.push_back((X[0]&~X[1])|(X[0]^(X[1]^X[2]))); // [0 1 1 0 1 1 0 1]
threevar.push_back((X[0]&X[1])|~(X[1]|~X[2])); // [0 0 0 1 1 1 0 1]
threevar.push_back(X[0]|(~X[1]&X[2])); // [0 1 0 1 1 1 0 1]
threevar.push_back((X[0]&X[1])|(X[1]^X[2])); // [0 0 1 1 1 1 0 1]
threevar.push_back(X[0]|(X[1]^X[2])); // [0 1 1 1 1 1 0 1]
threevar.push_back(X[1]&X[2]); // [0 0 0 0 0 0 1 1]
threevar.push_back((X[0]|X[1])&~(X[1]^X[2])); // [0 1 0 0 0 0 1 1]
threevar.push_back(X[1]&~(X[0]&~X[2])); // [0 0 1 0 0 0 1 1]
threevar.push_back(X[1]^(X[0]&~X[2])); // [0 1 1 0 0 0 1 1]
threevar.push_back(X[1]&(X[0]|X[2])); // [0 0 0 1 0 0 1 1]
threevar.push_back((X[0]&X[2])^(X[0]^(X[1]&X[2]))); // [0 1 0 1 0 0 1 1]
threevar.push_back(X[1]); // [0 0 1 1 0 0 1 1]
threevar.push_back(X[1]|(X[0]&~X[2])); // [0 1 1 1 0 0 1 1]
threevar.push_back(X[2]&~(X[0]&~X[1])); // [0 0 0 0 1 0 1 1]
threevar.push_back(X[2]^(X[0]&~X[1])); // [0 1 0 0 1 0 1 1]
threevar.push_back((X[1]&X[2])|(~X[0]&(X[1]|X[2]))); // [0 0 1 0 1 0 1 1]
threevar.push_back(~(X[0]|~X[1])|(X[0]^(X[1]^X[2]))); // [0 1 1 0 1 0 1 1]
threevar.push_back(X[1]^(~X[0]&(X[1]^X[2]))); // [0 0 0 1 1 0 1 1]
threevar.push_back(X[2]^~(~X[0]|(X[1]&X[2]))); // [0 1 0 1 1 0 1 1]
threevar.push_back(X[1]|~(X[0]|~X[2])); // [0 0 1 1 1 0 1 1]
threevar.push_back(X[1]|(X[0]^X[2])); // [0 1 1 1 1 0 1 1]
threevar.push_back(X[2]&(X[0]|X[1])); // [0 0 0 0 0 1 1 1]
threevar.push_back((X[0]&X[1])^(X[0]^(X[1]&X[2]))); // [0 1 0 0 0 1 1 1]
threevar.push_back(X[1]^(X[0]&(X[1]^X[2]))); // [0 0 1 0 0 1 1 1]
threevar.push_back(X[1]^~(~X[0]|(X[1]&X[2]))); // [0 1 1 0 0 1 1 1]
threevar.push_back((X[1]&X[2])|(X[0]&(X[1]|X[2]))); // [0 0 0 1 0 1 1 1]
threevar.push_back(X[0]|(X[1]&X[2])); // [0 1 0 1 0 1 1 1]
threevar.push_back(X[1]|(X[0]&X[2])); // [0 0 1 1 0 1 1 1]
threevar.push_back(X[0]|X[1]); // [0 1 1 1 0 1 1 1]
threevar.push_back(X[2]); // [0 0 0 0 1 1 1 1]
threevar.push_back(X[2]|(X[0]&~X[1])); // [0 1 0 0 1 1 1 1]
threevar.push_back(X[2]|~(X[0]|~X[1])); // [0 0 1 0 1 1 1 1]
threevar.push_back(X[2]|(X[0]^X[1])); // [0 1 1 0 1 1 1 1]
threevar.push_back(X[2]|(X[0]&X[1])); // [0 0 0 1 1 1 1 1]
threevar.push_back(X[0]|X[2]); // [0 1 0 1 1 1 1 1]
threevar.push_back(X[1]|X[2]); // [0 0 1 1 1 1 1 1]
threevar.push_back(X[0]|(X[1]|X[2])); // [0 1 1 1 1 1 1 1]
}