-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathscripts.js
386 lines (301 loc) · 17 KB
/
scripts.js
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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
str=
`
xR11[0,32] := { (xR8=69) /\ (xR13[0,32]) } \/
{ [xR8=194] /\ [(0 ≤ xR12[15,23] ≤ 2) /\ (xR12[28,32]) \/ (xR12[15,23]=59) /\ (xR12[32,40])] } \/
{ (xR8=192) /\ (xR12[15,23]=32) /\ (xR13[32,64]) } \/
{ (xR8=128) /\ (RCF[3,5]=0) /\ MEM[RIP] } \/
{ ¬(xR8=69) /\ (¬(xR8=192) \/ ¬(xR12[15,23]=32)) /\ (¬(xR8=194) \/ (¬(0 ≤ xR12[15,23] ≤ 2) /\ ¬(xR12[15,23]=59))) /\ (¬(xR8=128) \/ ¬(RCF[3,5]=0)) /\ (xR11[0,32]) }
xR11[32,64] := { (xR8=128) /\ (RCF[3,5]=0) /\ MEM[RIP] } \/
{ (¬(xR8=128) \/ ¬(RCF[3,5]=0)) /\ (xR11[32,64]) }
INSTRUCTION_FORMAT_CORRECT :=
[
[0 ≤ xR11[0,8] ≤ 2] /\ [(xR11[23,27]=1) \/ (xR11[23,27]=2) \/ (xR11[23,27]=4) \/ (xR11[23,27]=8)] /\ [xR11[59,64]=0] \/
[9 ≤ xR11[0,8] ≤ 10] /\ [xR11[50,64]=0] \/ [17 ≤ xR11[0,8] ≤ 33] /\ [xR11[18,64]=0] \/ [xR11[0,8]=44] /\ [xR11[45,64]=0] \/
[51 ≤ xR11[0,8] ≤ 53] /\ [xR11[13,64]=0] \/ [xR11[0,8]=59] /\ [xR11[16,64]=0] \/ [60 ≤ xR11[0,8] ≤ 67] /\ [xR11[40,64]=0] \/
[76 ≤ xR11[0,8] ≤ 78] /\ [xR11[8,64]=0]
]
xR12[0,1] := { [xR8=192] /\ [(xR12[15,23]=31) \/ (xR12[15,23]=33) \/ (xR12[15,23]=52) \/ (59 ≤ xR12[15,23] ≤ 60)] } \/
{ (xR8=68) } \/ { (xR8=69) } \/ { (xR8=72) } \/
{ (¬(xR8=192) \/ (¬(xR12[15,23]=31) /\ ¬(xR12[15,23]=33) /\ ¬(xR12[15,23]=52) /\ ¬(59 ≤ xR12[15,23] ≤ 60))) /\ ¬(xR8=68) /\ ¬(xR8=69) /\ ¬(xR8=72) /\ (xR12[0,1]) }
xR12[1,2] := { [2 ≤ xR8 ≤ 31] /\ [¬(xR13[0,32]=0) \/ (xR12[2,3])] /\ [xR12[2,3]] } \/
{ (xR8=65) /\ (xR12[0,1] \/ xR12[1,2]) } \/
{ (33 ≤ xR8 ≤ 63) /\ (xR12[2,3]) } \/
{ [(xR8=66) | (xR8=32)] /\ [xR12[1,2]] }
xR12[2,3] := { [xR8=32] /\ [(xR13[(xR8) /\ (31)]) /\ (xR14[(xR8) /\ (31)]) \/ (xR12[1,2]) /\ ((xR13[(xR8) /\ (31)]) \/ (xR14[(xR8) /\ (31)]))] } \/
{ [33 ≤ xR8 ≤ 63] /\ [(xR13[(xR8) /\ (31)]) /\ (xR14[(xR8) /\ (31)]) \/ (xR12[2,3]) /\ ((xR13[(xR8) /\ (31)]) \/ (xR14[(xR8) /\ (31)]))] } \/
{ [(xR8=64) | (2 ≤ xR8 ≤ 31) | (xR8=71)] /\ [xR12[2,3]] }
xR12[3,4] := { (xR8=66) /\ (xR13[31,32]) } \/
{ (32 ≤ xR8 ≤ 64) /\ (xR12[3,4]) }
xR12[4,5] := { (xR8=66) /\ (xR14[31,32]) } \/
(32 ≤ xR8 ≤ 64) /\ (xR12[4,5])
xR12[5,6] := { (xR8=67) /\ ¬(xR11[0,32]=0) /\ ¬(xR15[0,32]=0) /\ ¬(xR11[0,32]=1) /\ ¬(xR15[0,32]=1) /\ (xR11[31,32]) } \/
{ ¬(xR8=67) /\ (xR12[5,6]) }
xR12[6,7] := { (xR8=67) /\ ¬(xR11[0,32]=0) /\ ¬(xR15[0,32]=0) /\ ¬(xR11[0,32]=1) /\ ¬(xR15[0,32]=1) /\ (xR15[31,32]) } \/
{ ¬(xR8=67) /\ (xR12[6,7]) }
xR12[7,8] := { (xR8=193) /\ (xR12[63,64]) } \/
{ [xR8=67] /\ [¬(xR11[0,32]=0) /\ ¬(xR11[0,32]=1) /\ (xR15[0,32]=1) /\ (xR11[31,32]) \/ ¬(xR15[0,32]=0) /\ ¬(xR15[0,32]=1) /\ (xR11[0,32]=1) /\ (xR15[31,32])] } \/
{ (xR8=73) /\ (xR13[31,32]) } \/
{ [xR8=66] /\ ¬xR12[1,2] /\ [¬(xR13[0,32]=0) /\ (xR14[0,32]=0) /\ (xR13[31,32]) \/ (xR13[0,32]=0) /\ ¬(xR14[0,32]=0) /\ (xR14[31,32])] } \/
{ [xR8=64] /\ ¬[(xR13[31,32]) /\ ¬(xR12[3,4]) /\ ¬(xR12[4,5]) \/ ¬(xR13[31,32]) /\ (xR12[3,4]) /\ (xR12[4,5])] /\ [xR13[31,32]] } \/
{ ¬(xR8=64) /\ ¬(xR8=66) /\ ¬(xR8=67) /\ ¬(xR8=73) /\ ¬(xR8=193) /\ (xR12[7,8]) }
xR12[9,10] := { (xR8=193) /\ (xR12[32,64]=0) } \/
{ [xR8=67] /\ [(xR11[0,32]=0) \/ (xR15[0,32]=0)] } \/
{ (xR8=73) /\ (xR13[0,32]=0) } \/
{ (xR8=66) /\ (xR13[0,32]=0) /\ (xR14[0,32]=0) } \/
{ [xR8=64] /\ ¬[(xR13[31,32]) /\ ¬(xR12[3,4]) /\ ¬(xR12[4,5]) \/ ¬(xR13[31,32]) /\ (xR12[3,4]) /\ (xR12[4,5])] /\ [xR13[31,32]] /\ [xR13[0,32]=0] } \/
{ ¬(xR8=64) /\ ¬(xR8=66) /\ ¬(xR8=67) /\ ¬(xR8=73) /\ ¬(xR8=193) /\ (xR12[9,10]) }
xR12[15,23] := { (xR8=160) /\ (INSTRUCTION_FORMAT_CORRECT) /\ (xR11[0,8]) } \/
{ ¬(xR8=160) /\ (xR12[15,23]) }
xR12[23,28] := { (xR8=160) /\ (INSTRUCTION_FORMAT_CORRECT) /\ (xR11[8,13]) } \/
{ ¬(xR8=160) /\ (xR12[23,28]) }
xR12[28,32] := { (xR8=160) /\ (INSTRUCTION_FORMAT_CORRECT) /\ (xR11[23,27]) } \/
{ ¬(xR8=160) /\ (xR12[28,32]) }
xR12[32,64] := { [xR8=224] /\ [(xR12[15,23]=0) \/ (xR12[15,23]=9)] /\ [0 ≤ xR12[32,64] ≤ 0x2000000] /\ [(0 ≤ xR12[32,64] ≤ 0x2000000) /\ (xR12[32,64])]mem } \/
{ (xR8=225) /\ (xR12[15,23]=59) /\ [xR12[32,64] /\ (xR8=225) /\ (xR12[15,23]=59)]mem } \/
{ (xR8=160) /\ (INSTRUCTION_FORMAT_CORRECT) /\ (xR11[8,40]) } \/
{ [xR8=167] /\ [(xR11[0,8]=44) /\ (xR11[13,45]) \/ (9 ≤ xR11[0,8] < 10) /\ (xR11[18,50]) \/ (0 ≤ xR11[0,8] < 2) /\ (xR11[27,59]) ] } \/
{ (xR8=194) /\ ¬(xR12[15,23]=33) /\ ¬(xR12[15,23]=59) /\ ¬(xR12[15,23]=60) /\ (xR13[0,32]) } \/
{ [xR8=192] /\ [(xR12[15,23]=24) /\ (xR13[32,64]) /\ (xR14[32,64]) \/ (xR12[15,23]=25) /\ ((xR13[32,64]) \/ (xR14[32,64])) \/ (xR12[15,23]=26) /\ ((xR13[32,64]) /\ ¬(xR14[32,64]) \/ ¬(xR13[32,64]) /\ (xR14[32,64])) \/ (xR12[15,23]=27) /\ ((xR13[32,64]) << ((xR14[32,64]) /\ (31))) \/ (xR12[15,23]=28) /\ ((xR13[32,64]) >> ((xR14[32,64]) /\ (31))) \/ (xR12[15,23]=29) /\ ((xR13[32,64]) >>> ((xR14[32,64]) /\ (31))) \/ (xR12[15,23]=51) /\ ¬(xR13[32,64])] }
{ [(xR8=196) \/ (xR8=197)] /\ [xR13[0,32]] } \/
{ ¬(xR8=160) /\ ¬(xR8=167) /\ ¬(xR8=192) /\ ¬(xR8=194) /\ ¬(xR8=196) /\ ¬(xR8=197) /\ ¬(xR8=224) /\ ¬(xR8=225) /\ (xR12[32,64]) }
xR13[0,1] := { (xR8=256) \/ (xR8=257) } \/
(xR8=165) /\ 0
(xR8=163) /\ 0
(xR8=161) /\ 0
xR13[1,6] := { [(xR8=256) \/ (xR8=257)] /\ xR12[23,28] } \/
{ (xR8=165) /\ xR11[18,23] } \/
{ (xR8=163) /\ xR11[13,18] } \/
{ (xR8=161) /\ xR11[8,13] }
xR13[0,32] := { [(xR8=192) /\ ((xR12[15,23]=52) \/ (xR12[15,23]=53) \/ (xR12[15,23]=59) \/ (xR12[15,23]=60) \/ (xR12[15,23]=76))] /\ xR14[32,64] } \/
{ [(xR8=192) /\ ((xR12[15,23]=30) \/ (xR12[15,23]=31) \/ (xR12[15,23]=33))] /\ xR13[32,64] } \/
{ [(xR8=192) /\ ((xR12[15,23]=0) \/ (xR12[15,23]=1) \/ (xR12[15,23]=2) \/ (xR12[15,23]=9) \/ (xR12[15,23]=10))] /\ xR12[32,64] } \/
{ (xR8=128) /\ RIP} \/
{ (xR8=67) /\ (xR11[0,32]=1) /\ ¬(xR15[0,32]=0) /\ ¬(xR15[0,32]=1) /\ (xR15[0,32]) } \/
{ (xR8=67) /\ (xR15[0,32]=1) /\ ¬(xR11[0,32]=0) /\ ¬(xR11[0,32]=1) /\ (xR11[0,32]) } \/
{ (xR8=67) /\ [(xR11[0,32]=0) \/ (xR15[0,32]=0)] /\ 0 } \/
{ (xR8=68) /\ [(xR12[5,6]) \/ (¬xR12[5,6] /\ xR12[6,7])] /\ 0 } \/
{ (xR8=69) /\ xR12[6,7] /\ 0 } \/
{ (xR8=1) /\ xR15[0,1] /\ xR11[0,32] } \/
{ (xR8=1) /\ ¬xR15[0,1] /\ xR15[1,2] /\ (xR11[0,32]<<1) } \/
{ (xR8=1) /\ ¬xR15[0,1] /\ ¬xR15[1,2] /\ 0 } \/
{ (2 ≤ xR8 ≤ 31) /\ ¬xR15[xR8] /\ 0 } \/
{ (2 ≤ xR8 ≤ 31) /\ xR15[xR8] /\ (xR11[0,32]<< xR8) } \/
{ (xR8=72) /\ 0 } \/
{ (xR8=66) /\ (xR13[0,32]=0) /\ (xR14[0,32]=0) /\ xR12[1,2] } \/
{ (xR8=66) /\ (xR13[0,32]=0) /\ ¬(xR14[0,32]=0) /\ ¬xR12[1,2] /\ xR14[0,32] } \/
{ (xR8=97) /\ [
((xR13[1,6]=0) /\ RIP) \/
((xR13[1,6]=1) /\ RSP) \/
((xR13[1,6]=2) /\ RBP) \/
((xR13[1,6]=3) /\ RCF) \/
((xR13[1,6]=4) /\ R4) \/
((xR13[1,6]=5) /\ R5) \/
((xR13[1,6]=6) /\ R6) \/
((xR13[1,6]=7) /\ R7) \/
((xR13[1,6]=8) /\ R8) \/
((xR13[1,6]=9) /\ R9) \/
((xR13[1,6]=10) /\ R10) \/
((xR13[1,6]=11) /\ R11) \/
((xR13[1,6]=12) /\ R12) \/
((xR13[1,6]=13) /\ R13) \/
((xR13[1,6]=14) /\ R14) \/
((xR13[1,6]=15) /\ R15) \/
((xR13[1,6]=16) /\ R16) \/
((xR13[1,6]=17) /\ R17) \/
((xR13[1,6]=18) /\ R18) \/
((xR13[1,6]=19) /\ R19) \/
((xR13[1,6]=20) /\ R20) \/
((xR13[1,6]=21) /\ R21) \/
((xR13[1,6]=22) /\ R22) \/
((xR13[1,6]=23) /\ R23) \/
((xR13[1,6]=24) /\ R24) \/
((xR13[1,6]=25) /\ R25) \/
((xR13[1,6]=26) /\ R26) \/
((xR13[1,6]=27) /\ R27) \/
((xR13[1,6]=28) /\ R28) \/
((xR13[1,6]=29) /\ R29) \/
((xR13[1,6]=30) /\ R30) \/
((xR13[1,6]=31) /\ R31) ]}
xR13[0] := { (xR8=32) /\ [(¬xR12[1] /\ ¬xR13[0] /\ xR14[0]) \/ (¬xR12[1] /\ xR13[0] /\ ¬xR14[0]) \/
(xR12[1] /\ ¬xR13[0] /\ ¬xR14[0]) \/ (xR12[1] /\ xR13[0] /\ xR14[0])] }
xR13[xR8 /\ 31] := { (33 ≤ xR8 ≤ 63) /\ [(¬xR12[2] /\ ¬xR13[xR8 /\ 31] /\ xR14[xR8 /\ 31]) \/
(¬xR12[2] /\ xR13[xR8 /\ 31] /\ ¬xR14[xR8 /\ 31]) \/
(xR12[2] /\ ¬xR13[xR8 /\ 31] /\ ¬xR14[xR8 /\ 31]) \/
(xR12[2] /\ xR13[xR8 /\ 31] /\ xR14[xR8 /\ 31])] }
xR13[32,64] := { [(xR8=194) /\ ((xR12[15,23]=59) \/ (xR12[15,23]=60))] /\ xR13[0,32] }
{ (xR8=162) /\ xR13[0,32] }
xR14[0,32] := { (xR8=256) /\ [(xR12[15,23]=0) \/ (xR12[15,23]=2) \/ (xR12[15,23]=9) \/ (24 ≤ xR12[15,23] ≤ 32) \/ (xR12[15,23]=44) \/ (xR12[15,23]=51)] /\ xR12[32,64] } \/
{ (xR8=256) /\ (17 ≤ xR12[15,23] ≤ 23) /\ xR14[32,64] } \/
{ (xR8=257) /\ (xR12[15,23]=53) /\ xR15[32,64] } \/
{ (xR8=192) /\ [ (0 ≤ xR12[15,23] ≤ 2) \/ (xR12[15,23]=9) \/ (xR12[15,23]=10) \/ (xR12[15,23]=30) \/ (xR12[15,23]=31) \/ (xR12[15,23]=33) ] /\ xR14[32,64] } \/
{ (xR8=192) /\ [ (xR12[15,23]=52) \/ (xR12[15,23]=53) \/ (xR12[15,23]=59) \/ (xR12[15,23]=60) \/ (xR12[15,23]=76) ] /\ 4 } \/
{ (xR8=195) /\ (0 ≤ xR12[15,23] ≤ 2) /\ xR12[32,64] } \/
{ (xR8=195) /\ (xR12[15,23]=59) /\ INTERUPT_TABLE } \/
{ (xR8=128) /\ 8 } \/
{ (xR8=68) /\ ¬xR12[5,6] /\ xR12[6,7] /\ xR15[0,32] } \/
{ (xR8=68) /\ xR12[5,6] /\ xR11[0,32] } \/
{ (xR8=69) /\ xR12[6,7] /\ xR15[0,32] } \/
{ (xR8=1) /\ xR15[0] /\ xR15[1] /\ (xR11[0,32]<<1) } \/
{ (2 ≤ xR8 ≤ 31) /\ [ ¬(xR13[0,32]=0) \/ xR12[2] ] /\ xR15[xR8] /\ (xR11[0,32]<<xR8) } \/
{ (2 ≤ xR8 ≤ 31) /\ [ ¬(xR13[0,32]=0) \/ xR12[2] ] /\ ¬xR15[xR8] /\ 0 } \/
{ (xR8=71) /\ ¬xR12[2] /\ ¬xR13[31] /\ [ (xR12[5] /\ ¬xR12[6]) \/ (¬xR12[5] /\ xR12[6]) ] /\ xR13[0,32] } \/
{ (xR8=65) /\ [ (xR14[0,32] /\ ¬xR12[0]) \/ (¬xR14[0,32] /\ xR12[0]) ] }
xR14[32,64] := { (xR8=164) /\ xR13[0,32] } \/
{ (xR8=167) /\ [ (xR11[0,8]=52) \/ (xR11[0,8]=53) \/ (xR11[0,8]=59) \/
(xR11[0,8]=60) \/ (xR11[0,8]=76) ] /\ RSP } \/
xR15[0,32] := { (xR8=192) /\ (xR12[15,23]=32) /\ xR14[32,64] } \/
{ (xR8=194) /\ (xR12[15,23]=59) /\ 4 } \/
{ (xR8=194) /\ [ (0 ≤ xR12[15,23] ≤ 2) ] /\ xR15[32,64] } \/
{ (xR8=70) /\ xR13[0,32] } \/
xR15[32,64] := { (xR8=224) /\ [ (xR12[15,23]=53) \/ (xR12[15,23]=76) ] /\
(STACK_MIN ≤ xR12[32,64] ≤ STACK_MAX) /\ MEM[xR12[32,64]] } \/
{ (xR8=166) /\ xR13[0,32] } \/
{ (xR8=167) /\ [ (xR12[15,23]=52) \/ (xR12[15,23]=53) \/
(xR12[15,23]=59) \/ (xR12[15,23]=60) \/ (xR12[15,23]=76) ] /\ RIP }
RIP := { (xR8=256) /\ [ (xR12[15,23]=63) \/ (xR12[15,23]=65) \/ (xR12[15,23]=66) ] /\ RCF[2] /\ xR12[32,64] } \/
{ (xR8=256) /\ [ (xR12[15,23]=62) \/ (xR12[15,23]=63) \/ (xR12[15,23]=67) ] /\ RCF[0] /\ xR12[32,64] } \/
{ (xR8=256) /\ [ (xR12[15,23]=64) \/ (xR12[15,23]=65) \/ (xR12[15,23]=67) ] /\ ¬RCF[0] /\ ¬RCF[2] /\ xR12[32,64] } \/
{ (xR8=257) /\ (59 ≤ xR12[15,23] ≤ 61) /\ xR12[32,64] } \/
{ (xR8=257) /\ (xR12[15,23]=76) /\ xR15[32,64] } \/
{ (xR8=98) /\ [ [ (xR13[1,6]=0) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=0) /\ RIP ] ] } \/
{ (xR8=129) /\ xR13[0,32] }
RSP := { (xR8=256) /\ [ (xR12[15,23]=52) \/ (xR12[15,23]=53) \/ (xR12[15,23]=76) ] /\ xR12[32,64] } \/
{ (xR8=256) /\ [ (xR12[15,23]=59) \/ (xR12[15,23]=60) ] /\ xR13[32,64] } \/
{ (xR8=98) /\ [ [ (xR13[1,6]=1) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=1) /\ RSP ] ] }
RBP := { (xR8=98) /\ [ [ (xR13[1,6]=2) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=2) /\ RBP ] ] }
RCF := { (xR8=98) /\ [ [ (xR13[1,6]=3) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=3) /\ RCF ] ] }
RCF[3,5] := { (xR8=224) /\ [ (xR12[15,23]=0) \/ (xR12[15,23]=1) \/ (xR12[15,23]=9) \/
(xR12[15,23]=10) ] /\ ¬(MEM_MIN ≤ xR12[32,64] ≤ MEM_MAX) /\ 3 } \/
{ (xR8=224) /\ [ (xR12[15,23]=53) \/ (xR12[15,23]=76) ] /\ ¬(STACK_MIN ≤ xR12[32,64] ≤ STACK_MAX) /\ 3 } \/
{ (xR8=224) /\ [ (xR12[15,23]=52) \/ (xR12[15,23]=59) \/ (xR12[15,23]=60) ] /\ ¬(STACK_MIN ≤ xR14[32,64] ≤ STACK_MAX) /\ 3 } \/
{ (xR8=258) /\ 0 } \/
{ (xR8=64) /\ [ (xR13[31] /\ ¬xR12[3] /\ ¬xR12[4]) \/ (¬xR13[31] /\ xR12[3] /\ xR12[4]) ] /\ 1 } \/
{ (xR8=71) /\ (xR12[2] \/ xR13[31]) /\ 1 } \/
{ (xR8=160) /\ ¬INSTRUCTION_FORMAT_CORRECT /\ 2 } \/
{ (xR8=161) /\ (xR11[0,8]=77) /\ 0 }
RCF[0] := { (xR8=258) /\ [ (24 ≤ xR12[15,23] ≤ 33) \/ (xR12[15,23]=51) ] /\ xR12[7] } \/
{ (xR8=258) /\ [ ¬(24 ≤ xR12[15,23] ≤ 33) /\ ¬(xR12[15,23]=51) ] /\ 0 }
RCF[2] := { (xR8=258) /\ [ (24 ≤ xR12[15,23] ≤ 33) \/ (xR12[15,23]=51) ] /\ xR12[9] } \/
{ (xR8=258) /\ [ ¬(24 ≤ xR12[15,23] ≤ 33) /\ ¬(xR12[15,23]=51) ] /\ 0 }
R4 := { (xR8=98) /\ [ [ (xR13[1,6]=4) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=4) /\ R4 ] ] }
R5 := { (xR8=98) /\ [ [ (xR13[1,6]=5) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=5) /\ R5 ] ] }
R6 := { (xR8=98) /\ [ [ (xR13[1,6]=6) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=6) /\ R6 ] ] }
R7 := { (xR8=98) /\ [ [ (xR13[1,6]=7) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=7) /\ R7 ] ] }
R8 := { (xR8=98) /\ [ [ (xR13[1,6]=8) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=8) /\ R8 ] ] }
R9 := { (xR8=98) /\ [ [ (xR13[1,6]=9) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=9) /\ R9 ] ] }
R10 := { (xR8=98) /\ [ [ (xR13[1,6]=10) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=10) /\ R10 ] ] }
R11 := { (xR8=98) /\ [ [ (xR13[1,6]=11) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=11) /\ R11 ] ] }
R12 := { (xR8=98) /\ [ [ (xR13[1,6]=12) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=12) /\ R12 ] ] }
R13 := { (xR8=98) /\ [ [ (xR13[1,6]=13) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=13) /\ R13 ] ] }
R14 := { (xR8=98) /\ [ [ (xR13[1,6]=14) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=14) /\ R14 ] ] }
R15 := { (xR8=98) /\ [ [ (xR13[1,6]=15) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=15) /\ R15 ] ] }
R16 := { (xR8=98) /\ [ [ (xR13[1,6]=16) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=16) /\ R16 ] ] }
R17 := { (xR8=98) /\ [ [ (xR13[1,6]=17) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=17) /\ R17 ] ] }
R18 := { (xR8=98) /\ [ [ (xR13[1,6]=18) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=18) /\ R18 ] ] }
R19 := { (xR8=98) /\ [ [ (xR13[1,6]=19) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=19) /\ R19 ] ] }
R20 := { (xR8=98) /\ [ [ (xR13[1,6]=20) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=20) /\ R20 ] ] }
R21 := { (xR8=98) /\ [ [ (xR13[1,6]=21) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=21) /\ R21 ] ] }
R22 := { (xR8=98) /\ [ [ (xR13[1,6]=22) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=22) /\ R22 ] ] }
R23 := { (xR8=98) /\ [ [ (xR13[1,6]=23) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=23) /\ R23 ] ] }
R24 := { (xR8=98) /\ [ [ (xR13[1,6]=24) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=24) /\ R24 ] ] }
R25 := { (xR8=98) /\ [ [ (xR13[1,6]=25) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=25) /\ R25 ] ] }
R26 := { (xR8=98) /\ [ [ (xR13[1,6]=26) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=26) /\ R26 ] ] }
R27 := { (xR8=98) /\ [ [ (xR13[1,6]=27) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=27) /\ R27 ] ] }
R28 := { (xR8=98) /\ [ [ (xR13[1,6]=28) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=28) /\ R28 ] ] }
R29 := { (xR8=98) /\ [ [ (xR13[1,6]=29) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=29) /\ R29 ] ] }
R30 := { (xR8=98) /\ [ [ (xR13[1,6]=30) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=30) /\ R30 ] ] }
R31 := { (xR8=98) /\ [ [ (xR13[1,6]=31) /\ xR14[0,32] ] \/ [ ¬(xR13[1,6]=31) /\ R31 ] ] }
MEMORY[xR14[32,64]] := { (xR8=224) /\ [ (xR12[15,23]=59) \/ (xR12[15,23]=60) ] /\ (STACK_MIN ≤ xR14[32,64] ≤ STACK_MAX) /\ xR15[32,64] }
MEMORY[xR12[32,64]] := { (xR8=224) /\ [ (xR12[15,23]=1) \/ (xR12[15,23]=10) ] /\ (MEM_MIN ≤ xR12[32,64] ≤ MEM_MAX) /\ xR13[32,64] }
MEMORY[xR14[32,64]] := { (xR8=224) /\ (xR12[15,23]=52) /\ (STACK_MIN ≤ xR14[32,64] ≤ STACK_MAX) /\ xR13[32,64] }
`
xHashMap = []
for(i = 8; i <16; i++){
for(j=0; j <40; j++) {
xHashMap.push(
{
reg: `xR${i}`,
regNum: `${i}`,
from: "",
to:"",
bit:false,
fun:""
}
)
}
}
for(i=0,l=str.length; i < l; i++) {
if(str[i]!='x') continue;
num=""
j=0
if((str[i]=='x')&&(str[i+1]=='R')&&(str[i+2]>='0')&&(str[i+2]<='9')&&(str[i+3]>='0')&&(str[i+3]<='9')) {
num+= (str[i+2]+str[i+3])
j=i+4
}
else if((str[i]=='x')&&(str[i+1]=='R')&&(str[i+2]>='0')&&(str[i+2]<='9')) {
num+= (str[i+2])
j=i+3
}
if(str[j] !='[') {
console.log(`xR${num} is not partitioned`)
continue;
}
j++
nf=""
nt=""
while((str[j]>='0')&& (str[j]<='9')) {
nf+=str[j]
j++;
}
if(str[j] !=',') console.log("ERROR, NOT ,")
j++;
while((str[j]>='0')&& (str[j]<='9')) {
nt+=str[j]
j++;
}
if(str[j] !=']') console.log("ERROR, NOT ]")
for(k=(num-8)*40;k<((num-8)*40)+40;k++){
if((xHashMap[k].from==nf)&&(xHashMap[k].to==nt)){
break;
}
if(xHashMap[k].from=="") {
xHashMap[k].from=nf;
xHashMap[k].to=nt;
break;
}
if((k%40)==39){
console.log("ERROR")
}
}
}
for(i=0,l=xHashMap.length; i <l;i++){
if((xHashMap[i].from != "")&&(xHashMap[i].to != "")) {
diff=(xHashMap[i].to-xHashMap[i].from)
reg=xHashMap[i].reg
regNum=xHashMap[i].regNum
from=xHashMap[i].from
to=xHashMap[i].to - 1
if(diff==1){
xHashMap[i].fun += `${reg}_${from} == [i \\in 0..63 |-> `
}
else{
xHashMap[i].fun += `${reg}_${from}_${to} == [i \\in 0..63 |-> `
}
for(j=0;j<diff;j++){
if((from=='0')&&(diff!=1)){
xHashMap[i].fun += `(i>=${from}) /\\ (i<=${to}) /\\ ${reg}[i]]\n`
break;
}
else if(j==(diff-1)){
xHashMap[i].fun += `((i=${j}) /\\ ${reg}[${j+parseInt(from)}])]\n`
}
else {
xHashMap[i].fun += `((i=${j}) /\\ ${reg}[${j+parseInt(from)}]) \\/ `
}
}
}
}
for(i=0,l=xHashMap.length; i <l;i++){
if((xHashMap[i].from != "")&&(xHashMap[i].to != ""))
console.log(xHashMap[i].fun)
}