1module Compiler.MachineX86Native
2
3import Std.Natural
4
5family X86NativeRegister64 : Type 0
6constructor X86NativeRAX
7constructor X86NativeRCX
8constructor X86NativeRDX
9constructor X86NativeRBX
10constructor X86NativeRSP
11constructor X86NativeRBP
12constructor X86NativeRSI
13constructor X86NativeRDI
14constructor X86NativeR8
15constructor X86NativeR9
16constructor X86NativeR10
17constructor X86NativeR11
18constructor X86NativeR12
19constructor X86NativeR13
20constructor X86NativeR14
21constructor X86NativeR15
22
23end-family
24
25family X86NativeImmediate32 : Type 0
26constructor X86NativeImmediate32Value
27field unrestricted x86NativeImmediate32Byte0 : Byte
28field unrestricted x86NativeImmediate32Byte1 : Byte
29field unrestricted x86NativeImmediate32Byte2 : Byte
30field unrestricted x86NativeImmediate32Byte3 : Byte
31
32end-family
33
34family X86NativeImmediate8 : Type 0
35constructor X86NativeImmediate8Value
36field unrestricted x86NativeImmediate8Byte0 : Byte
37
38end-family
39
40family X86NativeImmediate64 : Type 0
41constructor X86NativeImmediate64Value
42field unrestricted x86NativeImmediate64Byte0 : Byte
43field unrestricted x86NativeImmediate64Byte1 : Byte
44field unrestricted x86NativeImmediate64Byte2 : Byte
45field unrestricted x86NativeImmediate64Byte3 : Byte
46field unrestricted x86NativeImmediate64Byte4 : Byte
47field unrestricted x86NativeImmediate64Byte5 : Byte
48field unrestricted x86NativeImmediate64Byte6 : Byte
49field unrestricted x86NativeImmediate64Byte7 : Byte
50
51end-family
52
53family X86NativeDisplacement32 : Type 0
54constructor X86NativeDisplacement32Value
55field unrestricted x86NativeDisplacement32Byte0 : Byte
56field unrestricted x86NativeDisplacement32Byte1 : Byte
57field unrestricted x86NativeDisplacement32Byte2 : Byte
58field unrestricted x86NativeDisplacement32Byte3 : Byte
59
60end-family
61
62family X86NativeRegisterLow3 : Type 0
63constructor X86NativeLow0
64constructor X86NativeLow1
65constructor X86NativeLow2
66constructor X86NativeLow3
67constructor X86NativeLow4
68constructor X86NativeLow5
69constructor X86NativeLow6
70constructor X86NativeLow7
71
72end-family
73
74family X86NativeRegisterBank : Type 0
75constructor X86NativeLowBank
76constructor X86NativeHighBank
77
78end-family
79
80-- the SSE registers the encoder names (xmm0 .. xmm7: no REX bit)
81family X86NativeRegisterXMM : Type 0
82constructor X86NativeXMM0
83constructor X86NativeXMM1
84constructor X86NativeXMM2
85constructor X86NativeXMM3
86constructor X86NativeXMM4
87constructor X86NativeXMM5
88constructor X86NativeXMM6
89constructor X86NativeXMM7
90
91end-family
92
93-- the SSE2 scalar-double operations on two XMM registers (F2 0F op):
94-- destination op= source, the square root of the source, and the source
95-- rounded to binary32 (CVTSD2SS) -- in the MXCSR rounding mode
96family X86NativeScalarDoubleOperation : Type 0
97constructor X86NativeScalarDoubleAdd
98constructor X86NativeScalarDoubleSubtract
99constructor X86NativeScalarDoubleMultiply
100constructor X86NativeScalarDoubleDivide
101constructor X86NativeScalarDoubleSquareRoot
102constructor X86NativeScalarDoubleToSingle
103
104end-family
105
106family X86NativeCondition : Type 0
107constructor X86NativeConditionZero
108constructor X86NativeConditionNotZero
109constructor X86NativeConditionBelow
110constructor X86NativeConditionAbove
111constructor X86NativeConditionSign
112
113end-family
114
115family X86NativeInstruction : Type 0
116constructor X86NativeMoveImmediate32
117field unrestricted x86NativeMoveImmediate32Destination : (family X86NativeRegister64)
118field unrestricted x86NativeMoveImmediate32Value : (family X86NativeImmediate32)
119constructor X86NativeMoveImmediate64
120field unrestricted x86NativeMoveImmediate64Destination : (family X86NativeRegister64)
121field unrestricted x86NativeMoveImmediate64Value : (family X86NativeImmediate64)
122constructor X86NativeClear32
123field unrestricted x86NativeClear32Destination : (family X86NativeRegister64)
124constructor X86NativeMoveRegister64
125field unrestricted x86NativeMoveRegister64Source : (family X86NativeRegister64)
126field unrestricted x86NativeMoveRegister64Destination : (family X86NativeRegister64)
127constructor X86NativeAddRegister64
128field unrestricted x86NativeAddRegister64Source : (family X86NativeRegister64)
129field unrestricted x86NativeAddRegister64Destination : (family X86NativeRegister64)
130constructor X86NativeSubtractRegister64
131field unrestricted x86NativeSubtractRegister64Source : (family X86NativeRegister64)
132field unrestricted x86NativeSubtractRegister64Destination : (family X86NativeRegister64)
133constructor X86NativeAndRegister64
134field unrestricted x86NativeAndRegister64Source : (family X86NativeRegister64)
135field unrestricted x86NativeAndRegister64Destination : (family X86NativeRegister64)
136constructor X86NativeOrRegister64
137field unrestricted x86NativeOrRegister64Source : (family X86NativeRegister64)
138field unrestricted x86NativeOrRegister64Destination : (family X86NativeRegister64)
139constructor X86NativeXorRegister64
140field unrestricted x86NativeXorRegister64Source : (family X86NativeRegister64)
141field unrestricted x86NativeXorRegister64Destination : (family X86NativeRegister64)
142constructor X86NativeCompareRegister64
143field unrestricted x86NativeCompareRegister64Source : (family X86NativeRegister64)
144field unrestricted x86NativeCompareRegister64Destination : (family X86NativeRegister64)
145constructor X86NativeTestRegister64
146field unrestricted x86NativeTestRegister64Source : (family X86NativeRegister64)
147field unrestricted x86NativeTestRegister64Destination : (family X86NativeRegister64)
148constructor X86NativeAddImmediate64
149field unrestricted x86NativeAddImmediate64Destination : (family X86NativeRegister64)
150field unrestricted x86NativeAddImmediate64Value : (family X86NativeImmediate32)
151constructor X86NativeAndImmediate64
152field unrestricted x86NativeAndImmediate64Destination : (family X86NativeRegister64)
153field unrestricted x86NativeAndImmediate64Value : (family X86NativeImmediate32)
154constructor X86NativeCompareImmediate64
155field unrestricted x86NativeCompareImmediate64Destination : (family X86NativeRegister64)
156field unrestricted x86NativeCompareImmediate64Value : (family X86NativeImmediate32)
157constructor X86NativeMultiplyImmediate64
158field unrestricted x86NativeMultiplyImmediate64Destination : (family X86NativeRegister64)
159field unrestricted x86NativeMultiplyImmediate64Value : (family X86NativeImmediate32)
160-- Unsigned implicit-accumulator forms: multiply writes RDX:RAX; divide
161-- consumes RDX:RAX and writes quotient RAX and remainder RDX. The caller
162-- must establish a nonzero divisor and a quotient that fits in 64 bits.
163constructor X86NativeMultiplyRegister64Unsigned
164field unrestricted x86NativeMultiplyRegister64UnsignedSource : (family X86NativeRegister64)
165constructor X86NativeDivideRegister64Unsigned
166field unrestricted x86NativeDivideRegister64UnsignedDivisor : (family X86NativeRegister64)
167constructor X86NativeShiftLeftImmediate64
168field unrestricted x86NativeShiftLeftImmediate64Destination : (family X86NativeRegister64)
169field unrestricted x86NativeShiftLeftImmediate64Value : (family X86NativeImmediate8)
170constructor X86NativeShiftRightImmediate64
171field unrestricted x86NativeShiftRightImmediate64Destination : (family X86NativeRegister64)
172field unrestricted x86NativeShiftRightImmediate64Value : (family X86NativeImmediate8)
173constructor X86NativeLoadMemory64
174field unrestricted x86NativeLoadMemory64Destination : (family X86NativeRegister64)
175field unrestricted x86NativeLoadMemory64Base : (family X86NativeRegister64)
176field unrestricted x86NativeLoadMemory64Displacement : (family X86NativeDisplacement32)
177constructor X86NativeLoadMemory8ZeroExtend64
178field unrestricted x86NativeLoadMemory8Destination : (family X86NativeRegister64)
179field unrestricted x86NativeLoadMemory8Base : (family X86NativeRegister64)
180field unrestricted x86NativeLoadMemory8Displacement : (family X86NativeDisplacement32)
181constructor X86NativeLoadMemory32ZeroExtend64
182field unrestricted x86NativeLoadMemory32Destination : (family X86NativeRegister64)
183field unrestricted x86NativeLoadMemory32Base : (family X86NativeRegister64)
184field unrestricted x86NativeLoadMemory32Displacement : (family X86NativeDisplacement32)
185constructor X86NativeStoreMemory32
186field unrestricted x86NativeStoreMemory32Base : (family X86NativeRegister64)
187field unrestricted x86NativeStoreMemory32Displacement : (family X86NativeDisplacement32)
188field unrestricted x86NativeStoreMemory32Source : (family X86NativeRegister64)
189constructor X86NativeStoreMemory64
190field unrestricted x86NativeStoreMemory64Base : (family X86NativeRegister64)
191field unrestricted x86NativeStoreMemory64Displacement : (family X86NativeDisplacement32)
192field unrestricted x86NativeStoreMemory64Source : (family X86NativeRegister64)
193constructor X86NativeStoreMemory8
194field unrestricted x86NativeStoreMemory8Base : (family X86NativeRegister64)
195field unrestricted x86NativeStoreMemory8Displacement : (family X86NativeDisplacement32)
196field unrestricted x86NativeStoreMemory8Source : (family X86NativeRegister64)
197constructor X86NativeStoreFence
198constructor X86NativeLoadEffectiveAddressRIP
199field unrestricted x86NativeLEADestination : (family X86NativeRegister64)
200field unrestricted x86NativeLEADisplacement : (family X86NativeDisplacement32)
201constructor X86NativeJumpRelative32
202field unrestricted x86NativeJumpDisplacement : (family X86NativeDisplacement32)
203constructor X86NativeJumpConditionRelative32
204field unrestricted x86NativeJumpCondition : (family X86NativeCondition)
205field unrestricted x86NativeJumpConditionDisplacement : (family X86NativeDisplacement32)
206constructor X86NativeCallRegister64
207field unrestricted x86NativeCallRegister64Target : (family X86NativeRegister64)
208constructor X86NativeReturn
209constructor X86NativeSystemCall
210-- MOVQ xmm, r64
211constructor X86NativeMoveToXMM64
212field unrestricted x86NativeMoveToXMM64Destination : (family X86NativeRegisterXMM)
213field unrestricted x86NativeMoveToXMM64Source : (family X86NativeRegister64)
214-- MOVQ r64, xmm
215constructor X86NativeMoveFromXMM64
216field unrestricted x86NativeMoveFromXMM64Destination : (family X86NativeRegister64)
217field unrestricted x86NativeMoveFromXMM64Source : (family X86NativeRegisterXMM)
218-- MOVD r32, xmm (zero-extended into the 64-bit register)
219constructor X86NativeMoveFromXMM32
220field unrestricted x86NativeMoveFromXMM32Destination : (family X86NativeRegister64)
221field unrestricted x86NativeMoveFromXMM32Source : (family X86NativeRegisterXMM)
222constructor X86NativeScalarDouble
223field unrestricted x86NativeScalarDoubleOperation : (family X86NativeScalarDoubleOperation)
224field unrestricted x86NativeScalarDoubleDestination : (family X86NativeRegisterXMM)
225field unrestricted x86NativeScalarDoubleSource : (family X86NativeRegisterXMM)
226-- CVTSS2SD xmm, xmm: the source's binary32 as a binary64
227constructor X86NativeScalarSingleToDouble
228field unrestricted x86NativeScalarSingleToDoubleDestination : (family X86NativeRegisterXMM)
229field unrestricted x86NativeScalarSingleToDoubleSource : (family X86NativeRegisterXMM)
230-- CVTSI2SD xmm, r64: the signed 64-bit integer as the nearest binary64
231constructor X86NativeScalarDoubleFromInteger64
232field unrestricted x86NativeScalarDoubleFromIntegerDestination : (family X86NativeRegisterXMM)
233field unrestricted x86NativeScalarDoubleFromIntegerSource : (family X86NativeRegister64)
234
235end-family
236
237family X86NativeProgram : Type 0
238constructor X86NativeProgramEnd
239constructor X86NativeProgramNext
240field unrestricted x86NativeProgramInstruction : (family X86NativeInstruction)
241recursive unrestricted x86NativeProgramTail
242
243end-family
244
245def x86NativeImmediate32Bytes :
246 (pi unrestricted immediate : (family X86NativeImmediate32) . Bytes) =
247 (lambda unrestricted immediate : (family X86NativeImmediate32) .
248 (eliminate
249 X86NativeImmediate32
250 (lambda unrestricted value : (family X86NativeImmediate32) . Bytes)
251 immediate
252 (branch X86NativeImmediate32Value byte0 byte1 byte2 byte3 . (bytes byte0 byte1 byte2 byte3))))
253
254def x86NativeImmediate8Bytes : (pi unrestricted immediate : (family X86NativeImmediate8) . Bytes) =
255 (lambda unrestricted immediate : (family X86NativeImmediate8) .
256 (eliminate
257 X86NativeImmediate8
258 (lambda unrestricted value : (family X86NativeImmediate8) . Bytes)
259 immediate
260 (branch X86NativeImmediate8Value byte0 . (bytes byte0))))
261
262def x86NativeImmediate64Bytes :
263 (pi unrestricted immediate : (family X86NativeImmediate64) . Bytes) =
264 (lambda unrestricted immediate : (family X86NativeImmediate64) .
265 (eliminate
266 X86NativeImmediate64
267 (lambda unrestricted value : (family X86NativeImmediate64) . Bytes)
268 immediate
269 (branch
270 X86NativeImmediate64Value
271 byte0
272 byte1
273 byte2
274 byte3
275 byte4
276 byte5
277 byte6
278 byte7
279 .
280 (bytes byte0 byte1 byte2 byte3 byte4 byte5 byte6 byte7))))
281
282def x86NativeDisplacement32Bytes :
283 (pi unrestricted displacement : (family X86NativeDisplacement32) . Bytes) =
284 (lambda unrestricted displacement : (family X86NativeDisplacement32) .
285 (eliminate
286 X86NativeDisplacement32
287 (lambda unrestricted value : (family X86NativeDisplacement32) . Bytes)
288 displacement
289 (branch
290 X86NativeDisplacement32Value
291 byte0
292 byte1
293 byte2
294 byte3
295 .
296 (bytes byte0 byte1 byte2 byte3))))
297
298def x86NativeMoveImmediate32Head :
299 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
300 (lambda unrestricted destination : (family X86NativeRegister64) .
301 (eliminate
302 X86NativeRegister64
303 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
304 destination
305 (branch X86NativeRAX . (bytes 184))
306 (branch X86NativeRCX . (bytes 185))
307 (branch X86NativeRDX . (bytes 186))
308 (branch X86NativeRBX . (bytes 187))
309 (branch X86NativeRSP . (bytes 188))
310 (branch X86NativeRBP . (bytes 189))
311 (branch X86NativeRSI . (bytes 190))
312 (branch X86NativeRDI . (bytes 191))
313 (branch X86NativeR8 . (bytes 65 184))
314 (branch X86NativeR9 . (bytes 65 185))
315 (branch X86NativeR10 . (bytes 65 186))
316 (branch X86NativeR11 . (bytes 65 187))
317 (branch X86NativeR12 . (bytes 65 188))
318 (branch X86NativeR13 . (bytes 65 189))
319 (branch X86NativeR14 . (bytes 65 190))
320 (branch X86NativeR15 . (bytes 65 191))))
321
322def x86NativeMoveImmediate64Head :
323 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
324 (lambda unrestricted destination : (family X86NativeRegister64) .
325 (eliminate
326 X86NativeRegister64
327 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
328 destination
329 (branch X86NativeRAX . (bytes 72 184))
330 (branch X86NativeRCX . (bytes 72 185))
331 (branch X86NativeRDX . (bytes 72 186))
332 (branch X86NativeRBX . (bytes 72 187))
333 (branch X86NativeRSP . (bytes 72 188))
334 (branch X86NativeRBP . (bytes 72 189))
335 (branch X86NativeRSI . (bytes 72 190))
336 (branch X86NativeRDI . (bytes 72 191))
337 (branch X86NativeR8 . (bytes 73 184))
338 (branch X86NativeR9 . (bytes 73 185))
339 (branch X86NativeR10 . (bytes 73 186))
340 (branch X86NativeR11 . (bytes 73 187))
341 (branch X86NativeR12 . (bytes 73 188))
342 (branch X86NativeR13 . (bytes 73 189))
343 (branch X86NativeR14 . (bytes 73 190))
344 (branch X86NativeR15 . (bytes 73 191))))
345
346def x86NativeClear32Bytes : (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
347 (lambda unrestricted destination : (family X86NativeRegister64) .
348 (eliminate
349 X86NativeRegister64
350 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
351 destination
352 (branch X86NativeRAX . (bytes 49 192))
353 (branch X86NativeRCX . (bytes 49 201))
354 (branch X86NativeRDX . (bytes 49 210))
355 (branch X86NativeRBX . (bytes 49 219))
356 (branch X86NativeRSP . (bytes 49 228))
357 (branch X86NativeRBP . (bytes 49 237))
358 (branch X86NativeRSI . (bytes 49 246))
359 (branch X86NativeRDI . (bytes 49 255))
360 (branch X86NativeR8 . (bytes 69 49 192))
361 (branch X86NativeR9 . (bytes 69 49 201))
362 (branch X86NativeR10 . (bytes 69 49 210))
363 (branch X86NativeR11 . (bytes 69 49 219))
364 (branch X86NativeR12 . (bytes 69 49 228))
365 (branch X86NativeR13 . (bytes 69 49 237))
366 (branch X86NativeR14 . (bytes 69 49 246))
367 (branch X86NativeR15 . (bytes 69 49 255))))
368
369def x86NativeRegisterLow3 :
370 (pi unrestricted register : (family X86NativeRegister64) . (family X86NativeRegisterLow3)) =
371 (lambda unrestricted register : (family X86NativeRegister64) .
372 (eliminate
373 X86NativeRegister64
374 (lambda unrestricted value : (family X86NativeRegister64) . (family X86NativeRegisterLow3))
375 register
376 (branch X86NativeRAX . (constructor X86NativeRegisterLow3 X86NativeLow0))
377 (branch X86NativeRCX . (constructor X86NativeRegisterLow3 X86NativeLow1))
378 (branch X86NativeRDX . (constructor X86NativeRegisterLow3 X86NativeLow2))
379 (branch X86NativeRBX . (constructor X86NativeRegisterLow3 X86NativeLow3))
380 (branch X86NativeRSP . (constructor X86NativeRegisterLow3 X86NativeLow4))
381 (branch X86NativeRBP . (constructor X86NativeRegisterLow3 X86NativeLow5))
382 (branch X86NativeRSI . (constructor X86NativeRegisterLow3 X86NativeLow6))
383 (branch X86NativeRDI . (constructor X86NativeRegisterLow3 X86NativeLow7))
384 (branch X86NativeR8 . (constructor X86NativeRegisterLow3 X86NativeLow0))
385 (branch X86NativeR9 . (constructor X86NativeRegisterLow3 X86NativeLow1))
386 (branch X86NativeR10 . (constructor X86NativeRegisterLow3 X86NativeLow2))
387 (branch X86NativeR11 . (constructor X86NativeRegisterLow3 X86NativeLow3))
388 (branch X86NativeR12 . (constructor X86NativeRegisterLow3 X86NativeLow4))
389 (branch X86NativeR13 . (constructor X86NativeRegisterLow3 X86NativeLow5))
390 (branch X86NativeR14 . (constructor X86NativeRegisterLow3 X86NativeLow6))
391 (branch X86NativeR15 . (constructor X86NativeRegisterLow3 X86NativeLow7))))
392
393def x86NativeRegisterBank :
394 (pi unrestricted register : (family X86NativeRegister64) . (family X86NativeRegisterBank)) =
395 (lambda unrestricted register : (family X86NativeRegister64) .
396 (eliminate
397 X86NativeRegister64
398 (lambda unrestricted value : (family X86NativeRegister64) . (family X86NativeRegisterBank))
399 register
400 (branch X86NativeRAX . (constructor X86NativeRegisterBank X86NativeLowBank))
401 (branch X86NativeRCX . (constructor X86NativeRegisterBank X86NativeLowBank))
402 (branch X86NativeRDX . (constructor X86NativeRegisterBank X86NativeLowBank))
403 (branch X86NativeRBX . (constructor X86NativeRegisterBank X86NativeLowBank))
404 (branch X86NativeRSP . (constructor X86NativeRegisterBank X86NativeLowBank))
405 (branch X86NativeRBP . (constructor X86NativeRegisterBank X86NativeLowBank))
406 (branch X86NativeRSI . (constructor X86NativeRegisterBank X86NativeLowBank))
407 (branch X86NativeRDI . (constructor X86NativeRegisterBank X86NativeLowBank))
408 (branch X86NativeR8 . (constructor X86NativeRegisterBank X86NativeHighBank))
409 (branch X86NativeR9 . (constructor X86NativeRegisterBank X86NativeHighBank))
410 (branch X86NativeR10 . (constructor X86NativeRegisterBank X86NativeHighBank))
411 (branch X86NativeR11 . (constructor X86NativeRegisterBank X86NativeHighBank))
412 (branch X86NativeR12 . (constructor X86NativeRegisterBank X86NativeHighBank))
413 (branch X86NativeR13 . (constructor X86NativeRegisterBank X86NativeHighBank))
414 (branch X86NativeR14 . (constructor X86NativeRegisterBank X86NativeHighBank))
415 (branch X86NativeR15 . (constructor X86NativeRegisterBank X86NativeHighBank))))
416
417def x86NativeRexWRegisterPair :
418 (pi unrestricted source : (family X86NativeRegister64) .
419 (pi unrestricted destination : (family X86NativeRegister64) . Bytes)) =
420 (lambda unrestricted source : (family X86NativeRegister64) .
421 (lambda unrestricted destination : (family X86NativeRegister64) .
422 (eliminate
423 X86NativeRegisterBank
424 (lambda unrestricted sourceBank : (family X86NativeRegisterBank) . Bytes)
425 (x86NativeRegisterBank source)
426 (branch
427 X86NativeLowBank
428 .
429 (eliminate
430 X86NativeRegisterBank
431 (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes)
432 (x86NativeRegisterBank destination)
433 (branch X86NativeLowBank . b"H")
434 (branch X86NativeHighBank . b"I")))
435 (branch
436 X86NativeHighBank
437 .
438 (eliminate
439 X86NativeRegisterBank
440 (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes)
441 (x86NativeRegisterBank destination)
442 (branch X86NativeLowBank . b"L")
443 (branch X86NativeHighBank . b"M"))))))
444
445def x86NativeRexRegisterPair :
446 (pi unrestricted source : (family X86NativeRegister64) .
447 (pi unrestricted destination : (family X86NativeRegister64) . Bytes)) =
448 (lambda unrestricted source : (family X86NativeRegister64) .
449 (lambda unrestricted destination : (family X86NativeRegister64) .
450 (eliminate
451 X86NativeRegisterBank
452 (lambda unrestricted sourceBank : (family X86NativeRegisterBank) . Bytes)
453 (x86NativeRegisterBank source)
454 (branch
455 X86NativeLowBank
456 .
457 (eliminate
458 X86NativeRegisterBank
459 (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes)
460 (x86NativeRegisterBank destination)
461 (branch X86NativeLowBank . b"")
462 (branch X86NativeHighBank . b"A")))
463 (branch
464 X86NativeHighBank
465 .
466 (eliminate
467 X86NativeRegisterBank
468 (lambda unrestricted destinationBank : (family X86NativeRegisterBank) . Bytes)
469 (x86NativeRegisterBank destination)
470 (branch X86NativeLowBank . b"D")
471 (branch X86NativeHighBank . b"E"))))))
472
473def x86NativeModRMRegisterRow0 :
474 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
475 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
476 (eliminate
477 X86NativeRegisterLow3
478 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
479 destination
480 (branch X86NativeLow0 . (bytes 192))
481 (branch X86NativeLow1 . (bytes 193))
482 (branch X86NativeLow2 . (bytes 194))
483 (branch X86NativeLow3 . (bytes 195))
484 (branch X86NativeLow4 . (bytes 196))
485 (branch X86NativeLow5 . (bytes 197))
486 (branch X86NativeLow6 . (bytes 198))
487 (branch X86NativeLow7 . (bytes 199))))
488
489def x86NativeModRMRegisterRow1 :
490 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
491 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
492 (eliminate
493 X86NativeRegisterLow3
494 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
495 destination
496 (branch X86NativeLow0 . (bytes 200))
497 (branch X86NativeLow1 . (bytes 201))
498 (branch X86NativeLow2 . (bytes 202))
499 (branch X86NativeLow3 . (bytes 203))
500 (branch X86NativeLow4 . (bytes 204))
501 (branch X86NativeLow5 . (bytes 205))
502 (branch X86NativeLow6 . (bytes 206))
503 (branch X86NativeLow7 . (bytes 207))))
504
505def x86NativeModRMRegisterRow2 :
506 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
507 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
508 (eliminate
509 X86NativeRegisterLow3
510 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
511 destination
512 (branch X86NativeLow0 . (bytes 208))
513 (branch X86NativeLow1 . (bytes 209))
514 (branch X86NativeLow2 . (bytes 210))
515 (branch X86NativeLow3 . (bytes 211))
516 (branch X86NativeLow4 . (bytes 212))
517 (branch X86NativeLow5 . (bytes 213))
518 (branch X86NativeLow6 . (bytes 214))
519 (branch X86NativeLow7 . (bytes 215))))
520
521def x86NativeModRMRegisterRow3 :
522 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
523 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
524 (eliminate
525 X86NativeRegisterLow3
526 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
527 destination
528 (branch X86NativeLow0 . (bytes 216))
529 (branch X86NativeLow1 . (bytes 217))
530 (branch X86NativeLow2 . (bytes 218))
531 (branch X86NativeLow3 . (bytes 219))
532 (branch X86NativeLow4 . (bytes 220))
533 (branch X86NativeLow5 . (bytes 221))
534 (branch X86NativeLow6 . (bytes 222))
535 (branch X86NativeLow7 . (bytes 223))))
536
537def x86NativeModRMRegisterRow4 :
538 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
539 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
540 (eliminate
541 X86NativeRegisterLow3
542 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
543 destination
544 (branch X86NativeLow0 . (bytes 224))
545 (branch X86NativeLow1 . (bytes 225))
546 (branch X86NativeLow2 . (bytes 226))
547 (branch X86NativeLow3 . (bytes 227))
548 (branch X86NativeLow4 . (bytes 228))
549 (branch X86NativeLow5 . (bytes 229))
550 (branch X86NativeLow6 . (bytes 230))
551 (branch X86NativeLow7 . (bytes 231))))
552
553def x86NativeModRMRegisterRow5 :
554 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
555 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
556 (eliminate
557 X86NativeRegisterLow3
558 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
559 destination
560 (branch X86NativeLow0 . (bytes 232))
561 (branch X86NativeLow1 . (bytes 233))
562 (branch X86NativeLow2 . (bytes 234))
563 (branch X86NativeLow3 . (bytes 235))
564 (branch X86NativeLow4 . (bytes 236))
565 (branch X86NativeLow5 . (bytes 237))
566 (branch X86NativeLow6 . (bytes 238))
567 (branch X86NativeLow7 . (bytes 239))))
568
569def x86NativeModRMRegisterRow6 :
570 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
571 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
572 (eliminate
573 X86NativeRegisterLow3
574 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
575 destination
576 (branch X86NativeLow0 . (bytes 240))
577 (branch X86NativeLow1 . (bytes 241))
578 (branch X86NativeLow2 . (bytes 242))
579 (branch X86NativeLow3 . (bytes 243))
580 (branch X86NativeLow4 . (bytes 244))
581 (branch X86NativeLow5 . (bytes 245))
582 (branch X86NativeLow6 . (bytes 246))
583 (branch X86NativeLow7 . (bytes 247))))
584
585def x86NativeModRMRegisterRow7 :
586 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes) =
587 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
588 (eliminate
589 X86NativeRegisterLow3
590 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
591 destination
592 (branch X86NativeLow0 . (bytes 248))
593 (branch X86NativeLow1 . (bytes 249))
594 (branch X86NativeLow2 . (bytes 250))
595 (branch X86NativeLow3 . (bytes 251))
596 (branch X86NativeLow4 . (bytes 252))
597 (branch X86NativeLow5 . (bytes 253))
598 (branch X86NativeLow6 . (bytes 254))
599 (branch X86NativeLow7 . (bytes 255))))
600
601def x86NativeModRMRegister :
602 (pi unrestricted source : (family X86NativeRegisterLow3) .
603 (pi unrestricted destination : (family X86NativeRegisterLow3) . Bytes)) =
604 (lambda unrestricted source : (family X86NativeRegisterLow3) .
605 (lambda unrestricted destination : (family X86NativeRegisterLow3) .
606 (eliminate
607 X86NativeRegisterLow3
608 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
609 source
610 (branch X86NativeLow0 . (x86NativeModRMRegisterRow0 destination))
611 (branch X86NativeLow1 . (x86NativeModRMRegisterRow1 destination))
612 (branch X86NativeLow2 . (x86NativeModRMRegisterRow2 destination))
613 (branch X86NativeLow3 . (x86NativeModRMRegisterRow3 destination))
614 (branch X86NativeLow4 . (x86NativeModRMRegisterRow4 destination))
615 (branch X86NativeLow5 . (x86NativeModRMRegisterRow5 destination))
616 (branch X86NativeLow6 . (x86NativeModRMRegisterRow6 destination))
617 (branch X86NativeLow7 . (x86NativeModRMRegisterRow7 destination)))))
618
619def x86NativeModRMMemoryRow0 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
620 (lambda unrestricted base : (family X86NativeRegisterLow3) .
621 (eliminate
622 X86NativeRegisterLow3
623 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
624 base
625 (branch X86NativeLow0 . (bytes 128))
626 (branch X86NativeLow1 . (bytes 129))
627 (branch X86NativeLow2 . (bytes 130))
628 (branch X86NativeLow3 . (bytes 131))
629 (branch X86NativeLow4 . (bytes 132))
630 (branch X86NativeLow5 . (bytes 133))
631 (branch X86NativeLow6 . (bytes 134))
632 (branch X86NativeLow7 . (bytes 135))))
633
634def x86NativeModRMMemoryRow1 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
635 (lambda unrestricted base : (family X86NativeRegisterLow3) .
636 (eliminate
637 X86NativeRegisterLow3
638 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
639 base
640 (branch X86NativeLow0 . (bytes 136))
641 (branch X86NativeLow1 . (bytes 137))
642 (branch X86NativeLow2 . (bytes 138))
643 (branch X86NativeLow3 . (bytes 139))
644 (branch X86NativeLow4 . (bytes 140))
645 (branch X86NativeLow5 . (bytes 141))
646 (branch X86NativeLow6 . (bytes 142))
647 (branch X86NativeLow7 . (bytes 143))))
648
649def x86NativeModRMMemoryRow2 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
650 (lambda unrestricted base : (family X86NativeRegisterLow3) .
651 (eliminate
652 X86NativeRegisterLow3
653 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
654 base
655 (branch X86NativeLow0 . (bytes 144))
656 (branch X86NativeLow1 . (bytes 145))
657 (branch X86NativeLow2 . (bytes 146))
658 (branch X86NativeLow3 . (bytes 147))
659 (branch X86NativeLow4 . (bytes 148))
660 (branch X86NativeLow5 . (bytes 149))
661 (branch X86NativeLow6 . (bytes 150))
662 (branch X86NativeLow7 . (bytes 151))))
663
664def x86NativeModRMMemoryRow3 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
665 (lambda unrestricted base : (family X86NativeRegisterLow3) .
666 (eliminate
667 X86NativeRegisterLow3
668 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
669 base
670 (branch X86NativeLow0 . (bytes 152))
671 (branch X86NativeLow1 . (bytes 153))
672 (branch X86NativeLow2 . (bytes 154))
673 (branch X86NativeLow3 . (bytes 155))
674 (branch X86NativeLow4 . (bytes 156))
675 (branch X86NativeLow5 . (bytes 157))
676 (branch X86NativeLow6 . (bytes 158))
677 (branch X86NativeLow7 . (bytes 159))))
678
679def x86NativeModRMMemoryRow4 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
680 (lambda unrestricted base : (family X86NativeRegisterLow3) .
681 (eliminate
682 X86NativeRegisterLow3
683 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
684 base
685 (branch X86NativeLow0 . (bytes 160))
686 (branch X86NativeLow1 . (bytes 161))
687 (branch X86NativeLow2 . (bytes 162))
688 (branch X86NativeLow3 . (bytes 163))
689 (branch X86NativeLow4 . (bytes 164))
690 (branch X86NativeLow5 . (bytes 165))
691 (branch X86NativeLow6 . (bytes 166))
692 (branch X86NativeLow7 . (bytes 167))))
693
694def x86NativeModRMMemoryRow5 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
695 (lambda unrestricted base : (family X86NativeRegisterLow3) .
696 (eliminate
697 X86NativeRegisterLow3
698 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
699 base
700 (branch X86NativeLow0 . (bytes 168))
701 (branch X86NativeLow1 . (bytes 169))
702 (branch X86NativeLow2 . (bytes 170))
703 (branch X86NativeLow3 . (bytes 171))
704 (branch X86NativeLow4 . (bytes 172))
705 (branch X86NativeLow5 . (bytes 173))
706 (branch X86NativeLow6 . (bytes 174))
707 (branch X86NativeLow7 . (bytes 175))))
708
709def x86NativeModRMMemoryRow6 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
710 (lambda unrestricted base : (family X86NativeRegisterLow3) .
711 (eliminate
712 X86NativeRegisterLow3
713 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
714 base
715 (branch X86NativeLow0 . (bytes 176))
716 (branch X86NativeLow1 . (bytes 177))
717 (branch X86NativeLow2 . (bytes 178))
718 (branch X86NativeLow3 . (bytes 179))
719 (branch X86NativeLow4 . (bytes 180))
720 (branch X86NativeLow5 . (bytes 181))
721 (branch X86NativeLow6 . (bytes 182))
722 (branch X86NativeLow7 . (bytes 183))))
723
724def x86NativeModRMMemoryRow7 : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
725 (lambda unrestricted base : (family X86NativeRegisterLow3) .
726 (eliminate
727 X86NativeRegisterLow3
728 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
729 base
730 (branch X86NativeLow0 . (bytes 184))
731 (branch X86NativeLow1 . (bytes 185))
732 (branch X86NativeLow2 . (bytes 186))
733 (branch X86NativeLow3 . (bytes 187))
734 (branch X86NativeLow4 . (bytes 188))
735 (branch X86NativeLow5 . (bytes 189))
736 (branch X86NativeLow6 . (bytes 190))
737 (branch X86NativeLow7 . (bytes 191))))
738
739def x86NativeModRMMemory :
740 (pi unrestricted register : (family X86NativeRegisterLow3) .
741 (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes)) =
742 (lambda unrestricted register : (family X86NativeRegisterLow3) .
743 (lambda unrestricted base : (family X86NativeRegisterLow3) .
744 (eliminate
745 X86NativeRegisterLow3
746 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
747 register
748 (branch X86NativeLow0 . (x86NativeModRMMemoryRow0 base))
749 (branch X86NativeLow1 . (x86NativeModRMMemoryRow1 base))
750 (branch X86NativeLow2 . (x86NativeModRMMemoryRow2 base))
751 (branch X86NativeLow3 . (x86NativeModRMMemoryRow3 base))
752 (branch X86NativeLow4 . (x86NativeModRMMemoryRow4 base))
753 (branch X86NativeLow5 . (x86NativeModRMMemoryRow5 base))
754 (branch X86NativeLow6 . (x86NativeModRMMemoryRow6 base))
755 (branch X86NativeLow7 . (x86NativeModRMMemoryRow7 base)))))
756
757def x86NativeMemorySIB : (pi unrestricted base : (family X86NativeRegisterLow3) . Bytes) =
758 (lambda unrestricted base : (family X86NativeRegisterLow3) .
759 (eliminate
760 X86NativeRegisterLow3
761 (lambda unrestricted value : (family X86NativeRegisterLow3) . Bytes)
762 base
763 (branch X86NativeLow0 . b"")
764 (branch X86NativeLow1 . b"")
765 (branch X86NativeLow2 . b"")
766 (branch X86NativeLow3 . b"")
767 (branch X86NativeLow4 . b"$")
768 (branch X86NativeLow5 . b"")
769 (branch X86NativeLow6 . b"")
770 (branch X86NativeLow7 . b"")))
771
772def x86NativeMemoryInstructionBytes :
773 (pi unrestricted opcode : Bytes .
774 (pi unrestricted register : (family X86NativeRegister64) .
775 (pi unrestricted base : (family X86NativeRegister64) .
776 (pi unrestricted displacement : (family X86NativeDisplacement32) . Bytes)))) =
777 (lambda unrestricted opcode : Bytes .
778 (lambda unrestricted register : (family X86NativeRegister64) .
779 (lambda unrestricted base : (family X86NativeRegister64) .
780 (lambda unrestricted displacement : (family X86NativeDisplacement32) .
781 (bytes-builder-build
782 (bytes-builder-append
783 (bytes-builder-chunk (x86NativeRexWRegisterPair register base))
784 (bytes-builder-append
785 (bytes-builder-chunk opcode)
786 (bytes-builder-append
787 (bytes-builder-chunk
788 (x86NativeModRMMemory
789 (x86NativeRegisterLow3 register)
790 (x86NativeRegisterLow3 base)))
791 (bytes-builder-append
792 (bytes-builder-chunk (x86NativeMemorySIB (x86NativeRegisterLow3 base)))
793 (bytes-builder-chunk (x86NativeDisplacement32Bytes displacement)))))))))))
794
795def x86NativeMemoryInstruction32Bytes :
796 (pi unrestricted opcode : Bytes .
797 (pi unrestricted register : (family X86NativeRegister64) .
798 (pi unrestricted base : (family X86NativeRegister64) .
799 (pi unrestricted displacement : (family X86NativeDisplacement32) . Bytes)))) =
800 (lambda unrestricted opcode : Bytes .
801 (lambda unrestricted register : (family X86NativeRegister64) .
802 (lambda unrestricted base : (family X86NativeRegister64) .
803 (lambda unrestricted displacement : (family X86NativeDisplacement32) .
804 (bytes-builder-build
805 (bytes-builder-append
806 (bytes-builder-chunk (x86NativeRexRegisterPair register base))
807 (bytes-builder-append
808 (bytes-builder-chunk opcode)
809 (bytes-builder-append
810 (bytes-builder-chunk
811 (x86NativeModRMMemory
812 (x86NativeRegisterLow3 register)
813 (x86NativeRegisterLow3 base)))
814 (bytes-builder-append
815 (bytes-builder-chunk (x86NativeMemorySIB (x86NativeRegisterLow3 base)))
816 (bytes-builder-chunk (x86NativeDisplacement32Bytes displacement)))))))))))
817
818def x86NativeLoadEffectiveAddressRIPHead :
819 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
820 (lambda unrestricted destination : (family X86NativeRegister64) .
821 (eliminate
822 X86NativeRegister64
823 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
824 destination
825 (branch X86NativeRAX . (bytes 72 141 5))
826 (branch X86NativeRCX . (bytes 72 141 13))
827 (branch X86NativeRDX . (bytes 72 141 21))
828 (branch X86NativeRBX . (bytes 72 141 29))
829 (branch X86NativeRSP . (bytes 72 141 37))
830 (branch X86NativeRBP . (bytes 72 141 45))
831 (branch X86NativeRSI . (bytes 72 141 53))
832 (branch X86NativeRDI . (bytes 72 141 61))
833 (branch X86NativeR8 . (bytes 76 141 5))
834 (branch X86NativeR9 . (bytes 76 141 13))
835 (branch X86NativeR10 . (bytes 76 141 21))
836 (branch X86NativeR11 . (bytes 76 141 29))
837 (branch X86NativeR12 . (bytes 76 141 37))
838 (branch X86NativeR13 . (bytes 76 141 45))
839 (branch X86NativeR14 . (bytes 76 141 53))
840 (branch X86NativeR15 . (bytes 76 141 61))))
841
842def x86NativeConditionOpcode : (pi unrestricted condition : (family X86NativeCondition) . Byte) =
843 (lambda unrestricted condition : (family X86NativeCondition) .
844 (eliminate
845 X86NativeCondition
846 (lambda unrestricted value : (family X86NativeCondition) . Byte)
847 condition
848 (branch X86NativeConditionZero . (byte 132))
849 (branch X86NativeConditionNotZero . (byte 133))
850 (branch X86NativeConditionBelow . (byte 130))
851 (branch X86NativeConditionAbove . (byte 135))
852 (branch X86NativeConditionSign . (byte 136))))
853
854def x86NativeRegisterInstructionBytes :
855 (pi unrestricted opcode : Byte .
856 (pi unrestricted source : (family X86NativeRegister64) .
857 (pi unrestricted destination : (family X86NativeRegister64) . Bytes))) =
858 (lambda unrestricted opcode : Byte .
859 (lambda unrestricted source : (family X86NativeRegister64) .
860 (lambda unrestricted destination : (family X86NativeRegister64) .
861 (bytes-append
862 (x86NativeRexWRegisterPair source destination)
863 (bytes-append
864 (bytes opcode)
865 (x86NativeModRMRegister
866 (x86NativeRegisterLow3 source)
867 (x86NativeRegisterLow3 destination)))))))
868
869def x86NativeAddImmediate64Head :
870 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
871 (lambda unrestricted destination : (family X86NativeRegister64) .
872 (eliminate
873 X86NativeRegister64
874 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
875 destination
876 (branch X86NativeRAX . (bytes 72 129 192))
877 (branch X86NativeRCX . (bytes 72 129 193))
878 (branch X86NativeRDX . (bytes 72 129 194))
879 (branch X86NativeRBX . (bytes 72 129 195))
880 (branch X86NativeRSP . (bytes 72 129 196))
881 (branch X86NativeRBP . (bytes 72 129 197))
882 (branch X86NativeRSI . (bytes 72 129 198))
883 (branch X86NativeRDI . (bytes 72 129 199))
884 (branch X86NativeR8 . (bytes 73 129 192))
885 (branch X86NativeR9 . (bytes 73 129 193))
886 (branch X86NativeR10 . (bytes 73 129 194))
887 (branch X86NativeR11 . (bytes 73 129 195))
888 (branch X86NativeR12 . (bytes 73 129 196))
889 (branch X86NativeR13 . (bytes 73 129 197))
890 (branch X86NativeR14 . (bytes 73 129 198))
891 (branch X86NativeR15 . (bytes 73 129 199))))
892
893def x86NativeAndImmediate64Head :
894 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
895 (lambda unrestricted destination : (family X86NativeRegister64) .
896 (eliminate
897 X86NativeRegister64
898 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
899 destination
900 (branch X86NativeRAX . (bytes 72 129 224))
901 (branch X86NativeRCX . (bytes 72 129 225))
902 (branch X86NativeRDX . (bytes 72 129 226))
903 (branch X86NativeRBX . (bytes 72 129 227))
904 (branch X86NativeRSP . (bytes 72 129 228))
905 (branch X86NativeRBP . (bytes 72 129 229))
906 (branch X86NativeRSI . (bytes 72 129 230))
907 (branch X86NativeRDI . (bytes 72 129 231))
908 (branch X86NativeR8 . (bytes 73 129 224))
909 (branch X86NativeR9 . (bytes 73 129 225))
910 (branch X86NativeR10 . (bytes 73 129 226))
911 (branch X86NativeR11 . (bytes 73 129 227))
912 (branch X86NativeR12 . (bytes 73 129 228))
913 (branch X86NativeR13 . (bytes 73 129 229))
914 (branch X86NativeR14 . (bytes 73 129 230))
915 (branch X86NativeR15 . (bytes 73 129 231))))
916
917def x86NativeCompareImmediate64Head :
918 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
919 (lambda unrestricted destination : (family X86NativeRegister64) .
920 (eliminate
921 X86NativeRegister64
922 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
923 destination
924 (branch X86NativeRAX . (bytes 72 129 248))
925 (branch X86NativeRCX . (bytes 72 129 249))
926 (branch X86NativeRDX . (bytes 72 129 250))
927 (branch X86NativeRBX . (bytes 72 129 251))
928 (branch X86NativeRSP . (bytes 72 129 252))
929 (branch X86NativeRBP . (bytes 72 129 253))
930 (branch X86NativeRSI . (bytes 72 129 254))
931 (branch X86NativeRDI . (bytes 72 129 255))
932 (branch X86NativeR8 . (bytes 73 129 248))
933 (branch X86NativeR9 . (bytes 73 129 249))
934 (branch X86NativeR10 . (bytes 73 129 250))
935 (branch X86NativeR11 . (bytes 73 129 251))
936 (branch X86NativeR12 . (bytes 73 129 252))
937 (branch X86NativeR13 . (bytes 73 129 253))
938 (branch X86NativeR14 . (bytes 73 129 254))
939 (branch X86NativeR15 . (bytes 73 129 255))))
940
941def x86NativeMultiplyImmediate64Head :
942 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
943 (lambda unrestricted destination : (family X86NativeRegister64) .
944 (x86NativeRegisterInstructionBytes (byte 105) destination destination))
945
946def x86NativeShiftLeftImmediate64Head :
947 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
948 (lambda unrestricted destination : (family X86NativeRegister64) .
949 (eliminate
950 X86NativeRegister64
951 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
952 destination
953 (branch X86NativeRAX . (bytes 72 193 224))
954 (branch X86NativeRCX . (bytes 72 193 225))
955 (branch X86NativeRDX . (bytes 72 193 226))
956 (branch X86NativeRBX . (bytes 72 193 227))
957 (branch X86NativeRSP . (bytes 72 193 228))
958 (branch X86NativeRBP . (bytes 72 193 229))
959 (branch X86NativeRSI . (bytes 72 193 230))
960 (branch X86NativeRDI . (bytes 72 193 231))
961 (branch X86NativeR8 . (bytes 73 193 224))
962 (branch X86NativeR9 . (bytes 73 193 225))
963 (branch X86NativeR10 . (bytes 73 193 226))
964 (branch X86NativeR11 . (bytes 73 193 227))
965 (branch X86NativeR12 . (bytes 73 193 228))
966 (branch X86NativeR13 . (bytes 73 193 229))
967 (branch X86NativeR14 . (bytes 73 193 230))
968 (branch X86NativeR15 . (bytes 73 193 231))))
969
970def x86NativeShiftRightImmediate64Head :
971 (pi unrestricted destination : (family X86NativeRegister64) . Bytes) =
972 (lambda unrestricted destination : (family X86NativeRegister64) .
973 (eliminate
974 X86NativeRegister64
975 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
976 destination
977 (branch X86NativeRAX . (bytes 72 193 232))
978 (branch X86NativeRCX . (bytes 72 193 233))
979 (branch X86NativeRDX . (bytes 72 193 234))
980 (branch X86NativeRBX . (bytes 72 193 235))
981 (branch X86NativeRSP . (bytes 72 193 236))
982 (branch X86NativeRBP . (bytes 72 193 237))
983 (branch X86NativeRSI . (bytes 72 193 238))
984 (branch X86NativeRDI . (bytes 72 193 239))
985 (branch X86NativeR8 . (bytes 73 193 232))
986 (branch X86NativeR9 . (bytes 73 193 233))
987 (branch X86NativeR10 . (bytes 73 193 234))
988 (branch X86NativeR11 . (bytes 73 193 235))
989 (branch X86NativeR12 . (bytes 73 193 236))
990 (branch X86NativeR13 . (bytes 73 193 237))
991 (branch X86NativeR14 . (bytes 73 193 238))
992 (branch X86NativeR15 . (bytes 73 193 239))))
993
994def x86NativeCallRegister64Bytes : (pi unrestricted target : (family X86NativeRegister64) . Bytes) =
995 (lambda unrestricted target : (family X86NativeRegister64) .
996 (eliminate
997 X86NativeRegister64
998 (lambda unrestricted value : (family X86NativeRegister64) . Bytes)
999 target
1000 (branch X86NativeRAX . (bytes 255 208))
1001 (branch X86NativeRCX . (bytes 255 209))
1002 (branch X86NativeRDX . (bytes 255 210))
1003 (branch X86NativeRBX . (bytes 255 211))
1004 (branch X86NativeRSP . (bytes 255 212))
1005 (branch X86NativeRBP . (bytes 255 213))
1006 (branch X86NativeRSI . (bytes 255 214))
1007 (branch X86NativeRDI . (bytes 255 215))
1008 (branch X86NativeR8 . (bytes 65 255 208))
1009 (branch X86NativeR9 . (bytes 65 255 209))
1010 (branch X86NativeR10 . (bytes 65 255 210))
1011 (branch X86NativeR11 . (bytes 65 255 211))
1012 (branch X86NativeR12 . (bytes 65 255 212))
1013 (branch X86NativeR13 . (bytes 65 255 213))
1014 (branch X86NativeR14 . (bytes 65 255 214))
1015 (branch X86NativeR15 . (bytes 65 255 215))))
1016
1017def x86NativeRegisterXMMLow3 :
1018 (pi unrestricted register : (family X86NativeRegisterXMM) . (family X86NativeRegisterLow3)) =
1019 (lambda unrestricted register : (family X86NativeRegisterXMM) .
1020 (eliminate
1021 X86NativeRegisterXMM
1022 (lambda unrestricted value : (family X86NativeRegisterXMM) . (family X86NativeRegisterLow3))
1023 register
1024 (branch X86NativeXMM0 . (constructor X86NativeRegisterLow3 X86NativeLow0))
1025 (branch X86NativeXMM1 . (constructor X86NativeRegisterLow3 X86NativeLow1))
1026 (branch X86NativeXMM2 . (constructor X86NativeRegisterLow3 X86NativeLow2))
1027 (branch X86NativeXMM3 . (constructor X86NativeRegisterLow3 X86NativeLow3))
1028 (branch X86NativeXMM4 . (constructor X86NativeRegisterLow3 X86NativeLow4))
1029 (branch X86NativeXMM5 . (constructor X86NativeRegisterLow3 X86NativeLow5))
1030 (branch X86NativeXMM6 . (constructor X86NativeRegisterLow3 X86NativeLow6))
1031 (branch X86NativeXMM7 . (constructor X86NativeRegisterLow3 X86NativeLow7))))
1032
1033def x86NativeScalarDoubleOpcode :
1034 (pi unrestricted operation : (family X86NativeScalarDoubleOperation) . Byte) =
1035 (lambda unrestricted operation : (family X86NativeScalarDoubleOperation) .
1036 (eliminate
1037 X86NativeScalarDoubleOperation
1038 (lambda unrestricted value : (family X86NativeScalarDoubleOperation) . Byte)
1039 operation
1040 (branch X86NativeScalarDoubleAdd . (byte 88))
1041 (branch X86NativeScalarDoubleSubtract . (byte 92))
1042 (branch X86NativeScalarDoubleMultiply . (byte 89))
1043 (branch X86NativeScalarDoubleDivide . (byte 94))
1044 (branch X86NativeScalarDoubleSquareRoot . (byte 81))
1045 (branch X86NativeScalarDoubleToSingle . (byte 90))))
1046
1047-- an SSE instruction with an XMM register in ModRM.reg and a general
1048-- register in ModRM.rm: the mandatory prefix, REX (W when `wide`; B for
1049-- r8 .. r15; none when neither), 0F, the opcode
1050def x86NativeXMMGeneralBytes :
1051 (pi unrestricted prefix : Byte .
1052 (pi unrestricted wide : Nat .
1053 (pi unrestricted opcode : Byte .
1054 (pi unrestricted xmm : (family X86NativeRegisterXMM) .
1055 (pi unrestricted general : (family X86NativeRegister64) . Bytes))))) =
1056 (lambda unrestricted prefix : Byte .
1057 (lambda unrestricted wide : Nat .
1058 (lambda unrestricted opcode : Byte .
1059 (lambda unrestricted xmm : (family X86NativeRegisterXMM) .
1060 (lambda unrestricted general : (family X86NativeRegister64) .
1061 (bytes-append
1062 (bytes prefix)
1063 (bytes-append
1064 (eliminate
1065 X86NativeRegisterBank
1066 (lambda unrestricted bank : (family X86NativeRegisterBank) . Bytes)
1067 (x86NativeRegisterBank general)
1068 (branch X86NativeLowBank . (nat-eliminate (lambda unrestricted w : Nat . Bytes) b"" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"H")) wide))
1069 (branch X86NativeHighBank . (nat-eliminate (lambda unrestricted w : Nat . Bytes) b"A" (lambda unrestricted p : Nat . (lambda unrestricted ignored : Bytes . b"I")) wide)))
1070 (bytes-append
1071 (bytes 15 opcode)
1072 (x86NativeModRMRegister (x86NativeRegisterXMMLow3 xmm) (x86NativeRegisterLow3 general))))))))))
1073
1074def x86EncodeNativeInstruction :
1075 (pi unrestricted instruction : (family X86NativeInstruction) . Bytes) =
1076 (lambda unrestricted instruction : (family X86NativeInstruction) .
1077 (eliminate
1078 X86NativeInstruction
1079 (lambda unrestricted value : (family X86NativeInstruction) . Bytes)
1080 instruction
1081 (branch
1082 X86NativeMoveImmediate32
1083 destination
1084 immediate
1085 .
1086 (bytes-append
1087 (x86NativeMoveImmediate32Head destination)
1088 (x86NativeImmediate32Bytes immediate)))
1089 (branch
1090 X86NativeMoveImmediate64
1091 destination
1092 immediate
1093 .
1094 (bytes-append
1095 (x86NativeMoveImmediate64Head destination)
1096 (x86NativeImmediate64Bytes immediate)))
1097 (branch X86NativeClear32 destination . (x86NativeClear32Bytes destination))
1098 (branch
1099 X86NativeMoveRegister64
1100 source
1101 destination
1102 .
1103 (x86NativeRegisterInstructionBytes (byte 137) source destination))
1104 (branch
1105 X86NativeAddRegister64
1106 source
1107 destination
1108 .
1109 (x86NativeRegisterInstructionBytes (byte 1) source destination))
1110 (branch
1111 X86NativeSubtractRegister64
1112 source
1113 destination
1114 .
1115 (x86NativeRegisterInstructionBytes (byte 41) source destination))
1116 (branch
1117 X86NativeAndRegister64
1118 source
1119 destination
1120 .
1121 (x86NativeRegisterInstructionBytes (byte 33) source destination))
1122 (branch
1123 X86NativeOrRegister64
1124 source
1125 destination
1126 .
1127 (x86NativeRegisterInstructionBytes (byte 9) source destination))
1128 (branch
1129 X86NativeXorRegister64
1130 source
1131 destination
1132 .
1133 (x86NativeRegisterInstructionBytes (byte 49) source destination))
1134 (branch
1135 X86NativeCompareRegister64
1136 source
1137 destination
1138 .
1139 (x86NativeRegisterInstructionBytes (byte 57) source destination))
1140 (branch
1141 X86NativeTestRegister64
1142 source
1143 destination
1144 .
1145 (x86NativeRegisterInstructionBytes (byte 133) source destination))
1146 (branch
1147 X86NativeAddImmediate64
1148 destination
1149 immediate
1150 .
1151 (bytes-append
1152 (x86NativeAddImmediate64Head destination)
1153 (x86NativeImmediate32Bytes immediate)))
1154 (branch
1155 X86NativeAndImmediate64
1156 destination
1157 immediate
1158 .
1159 (bytes-append
1160 (x86NativeAndImmediate64Head destination)
1161 (x86NativeImmediate32Bytes immediate)))
1162 (branch
1163 X86NativeCompareImmediate64
1164 destination
1165 immediate
1166 .
1167 (bytes-append
1168 (x86NativeCompareImmediate64Head destination)
1169 (x86NativeImmediate32Bytes immediate)))
1170 (branch
1171 X86NativeMultiplyImmediate64
1172 destination
1173 immediate
1174 .
1175 (bytes-append
1176 (x86NativeMultiplyImmediate64Head destination)
1177 (x86NativeImmediate32Bytes immediate)))
1178 (branch X86NativeMultiplyRegister64Unsigned source .
1179 (x86NativeRegisterInstructionBytes (byte 247) (constructor X86NativeRegister64 X86NativeRSP) source))
1180 (branch X86NativeDivideRegister64Unsigned divisor .
1181 (x86NativeRegisterInstructionBytes (byte 247) (constructor X86NativeRegister64 X86NativeRSI) divisor))
1182 (branch
1183 X86NativeShiftLeftImmediate64
1184 destination
1185 immediate
1186 .
1187 (bytes-append
1188 (x86NativeShiftLeftImmediate64Head destination)
1189 (x86NativeImmediate8Bytes immediate)))
1190 (branch
1191 X86NativeShiftRightImmediate64
1192 destination
1193 immediate
1194 .
1195 (bytes-append
1196 (x86NativeShiftRightImmediate64Head destination)
1197 (x86NativeImmediate8Bytes immediate)))
1198 (branch
1199 X86NativeLoadMemory64
1200 destination
1201 base
1202 displacement
1203 .
1204 (x86NativeMemoryInstructionBytes (bytes 139) destination base displacement))
1205 (branch
1206 X86NativeLoadMemory8ZeroExtend64
1207 destination
1208 base
1209 displacement
1210 .
1211 (x86NativeMemoryInstructionBytes (bytes 15 182) destination base displacement))
1212 (branch
1213 X86NativeLoadMemory32ZeroExtend64
1214 destination
1215 base
1216 displacement
1217 .
1218 (x86NativeMemoryInstruction32Bytes (bytes 139) destination base displacement))
1219 (branch
1220 X86NativeStoreMemory32
1221 base
1222 displacement
1223 source
1224 .
1225 (x86NativeMemoryInstruction32Bytes (bytes 137) source base displacement))
1226 (branch
1227 X86NativeStoreMemory64
1228 base
1229 displacement
1230 source
1231 .
1232 (x86NativeMemoryInstructionBytes (bytes 137) source base displacement))
1233 (branch
1234 X86NativeStoreMemory8
1235 base
1236 displacement
1237 source
1238 .
1239 (x86NativeMemoryInstructionBytes (bytes 136) source base displacement))
1240 (branch X86NativeStoreFence . (bytes 15 174 248))
1241 (branch
1242 X86NativeLoadEffectiveAddressRIP
1243 destination
1244 displacement
1245 .
1246 (bytes-append
1247 (x86NativeLoadEffectiveAddressRIPHead destination)
1248 (x86NativeDisplacement32Bytes displacement)))
1249 (branch
1250 X86NativeJumpRelative32
1251 displacement
1252 .
1253 (bytes-append (bytes 233) (x86NativeDisplacement32Bytes displacement)))
1254 (branch
1255 X86NativeJumpConditionRelative32
1256 condition
1257 displacement
1258 .
1259 (bytes-append
1260 (bytes 15 (x86NativeConditionOpcode condition))
1261 (x86NativeDisplacement32Bytes displacement)))
1262 (branch X86NativeCallRegister64 target . (x86NativeCallRegister64Bytes target))
1263 (branch X86NativeReturn . (bytes 195))
1264 (branch X86NativeSystemCall . (bytes 15 5))
1265 (branch X86NativeMoveToXMM64 destination source . (x86NativeXMMGeneralBytes (byte 102) 1 (byte 110) destination source))
1266 (branch X86NativeMoveFromXMM64 destination source . (x86NativeXMMGeneralBytes (byte 102) 1 (byte 126) source destination))
1267 (branch X86NativeMoveFromXMM32 destination source . (x86NativeXMMGeneralBytes (byte 102) 0 (byte 126) source destination))
1268 (branch
1269 X86NativeScalarDouble
1270 operation
1271 destination
1272 source
1273 .
1274 (bytes-append
1275 (bytes 242 15 (x86NativeScalarDoubleOpcode operation))
1276 (x86NativeModRMRegister (x86NativeRegisterXMMLow3 destination) (x86NativeRegisterXMMLow3 source))))
1277 (branch
1278 X86NativeScalarSingleToDouble
1279 destination
1280 source
1281 .
1282 (bytes-append
1283 (bytes 243 15 90)
1284 (x86NativeModRMRegister (x86NativeRegisterXMMLow3 destination) (x86NativeRegisterXMMLow3 source))))
1285 (branch X86NativeScalarDoubleFromInteger64 destination source . (x86NativeXMMGeneralBytes (byte 242) 1 (byte 42) destination source))))
1286
1287def x86EncodeNativeProgram : (pi unrestricted program : (family X86NativeProgram) . Bytes) =
1288 (lambda unrestricted program : (family X86NativeProgram) .
1289 (eliminate
1290 X86NativeProgram
1291 (lambda unrestricted value : (family X86NativeProgram) . Bytes)
1292 program
1293 (branch X86NativeProgramEnd . b"")
1294 (branch
1295 X86NativeProgramNext
1296 instruction
1297 tail
1298 encodedTail
1299 .
1300 (bytes-append (x86EncodeNativeInstruction instruction) encodedTail))))
1301
1302-- Truncating low-word constructors; sign interpretation is the instruction's
1303-- contract. This keeps signed offsets and unsigned constants out of handwritten
1304-- per-routine byte decompositions.
1305def x86NativeByteOfNatural = (lambda unrestricted value : Nat . (lambda unrestricted scale : Nat .
1306 (nat-to-byte (naturalModuloUnchecked (naturalDivideUnchecked value scale) 256))))
1307def x86NativeImmediate32FromNatural = (lambda unrestricted value : Nat .
1308 (constructor X86NativeImmediate32 X86NativeImmediate32Value
1309 (x86NativeByteOfNatural value 1) (x86NativeByteOfNatural value 256)
1310 (x86NativeByteOfNatural value 65536) (x86NativeByteOfNatural value 16777216)))
1311def x86NativeDisplacement32FromNatural = (lambda unrestricted value : Nat .
1312 (constructor X86NativeDisplacement32 X86NativeDisplacement32Value
1313 (x86NativeByteOfNatural value 1) (x86NativeByteOfNatural value 256)
1314 (x86NativeByteOfNatural value 65536) (x86NativeByteOfNatural value 16777216)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.