1module Compiler.MachineX86NativeAssembly
2
3import Compiler.MachineX86Native
4import Compiler.MachineX86NativeOffset
5
6family X86NativeAssembly : Type 0
7constructor X86NativeAssemblyEnd
8constructor X86NativeAssemblyEmit
9field unrestricted x86NativeAssemblyInstruction : (family X86NativeInstruction)
10recursive unrestricted x86NativeAssemblyAfterInstruction
11constructor X86NativeAssemblyLabel
12field unrestricted x86NativeAssemblyLabelName : Bytes
13recursive unrestricted x86NativeAssemblyAfterLabel
14constructor X86NativeAssemblyJump
15field unrestricted x86NativeAssemblyJumpTarget : Bytes
16recursive unrestricted x86NativeAssemblyAfterJump
17constructor X86NativeAssemblyJumpCondition
18field unrestricted x86NativeAssemblyJumpConditionValue : (family X86NativeCondition)
19field unrestricted x86NativeAssemblyJumpConditionTarget : Bytes
20recursive unrestricted x86NativeAssemblyAfterJumpCondition
21constructor X86NativeAssemblyLoadEffectiveAddressRIPLabel
22field unrestricted x86NativeAssemblyLEADestination : (family X86NativeRegister64)
23field unrestricted x86NativeAssemblyLEATarget : Bytes
24recursive unrestricted x86NativeAssemblyAfterLEA
25
26end-family
27
28family X86NativeLabelTable : Type 0
29constructor X86NativeLabelTableEmpty
30constructor X86NativeLabelTableEntry
31field unrestricted x86NativeLabelName : Bytes
32field unrestricted x86NativeLabelOffset : (family X86NativeUnsigned32)
33recursive unrestricted x86NativeRemainingLabels
34
35end-family
36
37family X86NativeLabelLookupResult : Type 0
38constructor X86NativeLabelFound
39field unrestricted x86NativeFoundLabelOffset : (family X86NativeUnsigned32)
40constructor X86NativeLabelMissing
41
42end-family
43
44family X86NativeAssemblyLayoutResult : Type 0
45constructor X86NativeAssemblyLayoutSuccess
46field unrestricted x86NativeAssemblyLabels : (family X86NativeLabelTable)
47field unrestricted x86NativeAssemblySize : (family X86NativeUnsigned32)
48constructor X86NativeAssemblyDuplicateLabel
49field unrestricted x86NativeDuplicateLabelName : Bytes
50constructor X86NativeAssemblyOffsetOverflow
51
52end-family
53
54family X86NativeAssemblyResult : Type 0
55constructor X86NativeAssemblyEncoded
56field unrestricted x86NativeAssemblyEncodedBytes : Bytes
57constructor X86NativeAssemblyEncodeDuplicateLabel
58field unrestricted x86NativeAssemblyEncodeDuplicateName : Bytes
59constructor X86NativeAssemblyEncodeOffsetOverflow
60constructor X86NativeAssemblyMissingLabel
61field unrestricted x86NativeAssemblyMissingLabelName : Bytes
62constructor X86NativeAssemblyDisplacementOutOfRange
63field unrestricted x86NativeAssemblyDistantLabelName : Bytes
64
65end-family
66
67def x86NativeLookupLabel :
68 (pi unrestricted name : Bytes .
69 (pi unrestricted table : (family X86NativeLabelTable) . (family X86NativeLabelLookupResult))) =
70 (lambda unrestricted name : Bytes .
71 (lambda unrestricted table : (family X86NativeLabelTable) .
72 (eliminate
73 X86NativeLabelTable
74 (lambda unrestricted value : (family X86NativeLabelTable) .
75 (family X86NativeLabelLookupResult))
76 table
77 (branch
78 X86NativeLabelTableEmpty
79 .
80 (constructor X86NativeLabelLookupResult X86NativeLabelMissing))
81 (branch
82 X86NativeLabelTableEntry
83 existingName
84 offset
85 remaining
86 induction
87 .
88 (nat-eliminate
89 (lambda unrestricted equal : Nat . (family X86NativeLabelLookupResult))
90 induction
91 (lambda unrestricted predecessor : Nat .
92 (lambda unrestricted equalInduction : (family X86NativeLabelLookupResult) .
93 (constructor X86NativeLabelLookupResult X86NativeLabelFound offset)))
94 (bytes-equal name existingName))))))
95
96def x86NativeAdvanceLayout :
97 (pi unrestricted encoded : Bytes .
98 (pi unrestricted offset : (family X86NativeUnsigned32) .
99 (pi unrestricted continuation : (pi unrestricted nextOffset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult)) .
100 (family X86NativeAssemblyLayoutResult)))) =
101 (lambda unrestricted encoded : Bytes .
102 (lambda unrestricted offset : (family X86NativeUnsigned32) .
103 (lambda unrestricted continuation : (pi unrestricted nextOffset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult)) .
104 (eliminate
105 X86NativeUnsigned32Result
106 (lambda unrestricted result : (family X86NativeUnsigned32Result) .
107 (family X86NativeAssemblyLayoutResult))
108 (x86NativeAdvanceUnsigned32ByBytes offset encoded)
109 (branch X86NativeUnsigned32Success nextOffset . (continuation nextOffset))
110 (branch
111 X86NativeUnsigned32Overflow
112 .
113 (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyOffsetOverflow))))))
114
115def x86NativeLayoutAssemblyFrom :
116 (pi unrestricted assembly : (family X86NativeAssembly) .
117 (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyLayoutResult))) =
118 (lambda unrestricted assembly : (family X86NativeAssembly) .
119 (eliminate
120 X86NativeAssembly
121 (lambda unrestricted value : (family X86NativeAssembly) .
122 (pi unrestricted offset : (family X86NativeUnsigned32) .
123 (family X86NativeAssemblyLayoutResult)))
124 assembly
125 (branch
126 X86NativeAssemblyEnd
127 .
128 (lambda unrestricted offset : (family X86NativeUnsigned32) .
129 (constructor
130 X86NativeAssemblyLayoutResult
131 X86NativeAssemblyLayoutSuccess
132 (constructor X86NativeLabelTable X86NativeLabelTableEmpty)
133 offset)))
134 (branch
135 X86NativeAssemblyEmit
136 instruction
137 tail
138 layoutTail
139 .
140 (lambda unrestricted offset : (family X86NativeUnsigned32) .
141 (x86NativeAdvanceLayout (x86EncodeNativeInstruction instruction) offset layoutTail)))
142 (branch
143 X86NativeAssemblyLabel
144 name
145 tail
146 layoutTail
147 .
148 (lambda unrestricted offset : (family X86NativeUnsigned32) .
149 (eliminate
150 X86NativeAssemblyLayoutResult
151 (lambda unrestricted result : (family X86NativeAssemblyLayoutResult) .
152 (family X86NativeAssemblyLayoutResult))
153 (layoutTail offset)
154 (branch
155 X86NativeAssemblyLayoutSuccess
156 labels
157 finalSize
158 .
159 (eliminate
160 X86NativeLabelLookupResult
161 (lambda unrestricted lookup : (family X86NativeLabelLookupResult) .
162 (family X86NativeAssemblyLayoutResult))
163 (x86NativeLookupLabel name labels)
164 (branch
165 X86NativeLabelFound
166 existingOffset
167 .
168 (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyDuplicateLabel name))
169 (branch
170 X86NativeLabelMissing
171 .
172 (constructor
173 X86NativeAssemblyLayoutResult
174 X86NativeAssemblyLayoutSuccess
175 (constructor X86NativeLabelTable X86NativeLabelTableEntry name offset labels)
176 finalSize))))
177 (branch
178 X86NativeAssemblyDuplicateLabel
179 duplicateName
180 .
181 (constructor
182 X86NativeAssemblyLayoutResult
183 X86NativeAssemblyDuplicateLabel
184 duplicateName))
185 (branch
186 X86NativeAssemblyOffsetOverflow
187 .
188 (constructor X86NativeAssemblyLayoutResult X86NativeAssemblyOffsetOverflow)))))
189 (branch
190 X86NativeAssemblyJump
191 target
192 tail
193 layoutTail
194 .
195 (lambda unrestricted offset : (family X86NativeUnsigned32) .
196 (x86NativeAdvanceLayout (bytes 0 0 0 0 0) offset layoutTail)))
197 (branch
198 X86NativeAssemblyJumpCondition
199 condition
200 target
201 tail
202 layoutTail
203 .
204 (lambda unrestricted offset : (family X86NativeUnsigned32) .
205 (x86NativeAdvanceLayout (bytes 0 0 0 0 0 0) offset layoutTail)))
206 (branch
207 X86NativeAssemblyLoadEffectiveAddressRIPLabel
208 destination
209 target
210 tail
211 layoutTail
212 .
213 (lambda unrestricted offset : (family X86NativeUnsigned32) .
214 (x86NativeAdvanceLayout (bytes 0 0 0 0 0 0 0) offset layoutTail)))))
215
216def x86NativeLayoutAssembly :
217 (pi unrestricted assembly : (family X86NativeAssembly) . (family X86NativeAssemblyLayoutResult)) =
218 (lambda unrestricted assembly : (family X86NativeAssembly) .
219 (x86NativeLayoutAssemblyFrom assembly x86NativeUnsigned32Zero))
220
221def x86NativeUnsigned32Displacement :
222 (pi unrestricted value : (family X86NativeUnsigned32) . (family X86NativeDisplacement32)) =
223 (lambda unrestricted value : (family X86NativeUnsigned32) .
224 (eliminate
225 X86NativeUnsigned32
226 (lambda unrestricted current : (family X86NativeUnsigned32) .
227 (family X86NativeDisplacement32))
228 value
229 (branch
230 X86NativeUnsigned32Value
231 byte0
232 byte1
233 byte2
234 byte3
235 .
236 (constructor X86NativeDisplacement32 X86NativeDisplacement32Value byte0 byte1 byte2 byte3))))
237
238def x86NativePrependAssemblyBytes :
239 (pi unrestricted prefix : Bytes .
240 (pi unrestricted result : (family X86NativeAssemblyResult) . (family X86NativeAssemblyResult))) =
241 (lambda unrestricted prefix : Bytes .
242 (lambda unrestricted result : (family X86NativeAssemblyResult) .
243 (eliminate
244 X86NativeAssemblyResult
245 (lambda unrestricted value : (family X86NativeAssemblyResult) .
246 (family X86NativeAssemblyResult))
247 result
248 (branch
249 X86NativeAssemblyEncoded
250 encoded
251 .
252 (constructor
253 X86NativeAssemblyResult
254 X86NativeAssemblyEncoded
255 (bytes-append prefix encoded)))
256 (branch
257 X86NativeAssemblyEncodeDuplicateLabel
258 duplicateName
259 .
260 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeDuplicateLabel duplicateName))
261 (branch
262 X86NativeAssemblyEncodeOffsetOverflow
263 .
264 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))
265 (branch
266 X86NativeAssemblyMissingLabel
267 missingName
268 .
269 (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel missingName))
270 (branch
271 X86NativeAssemblyDisplacementOutOfRange
272 distantName
273 .
274 (constructor X86NativeAssemblyResult X86NativeAssemblyDisplacementOutOfRange distantName)))))
275
276def x86NativeEncodeJumpToLabel :
277 (pi unrestricted conditionFlag : Nat .
278 (pi unrestricted condition : (family X86NativeCondition) .
279 (pi unrestricted targetName : Bytes .
280 (pi unrestricted labels : (family X86NativeLabelTable) .
281 (pi unrestricted sourceEnd : (family X86NativeUnsigned32) .
282 (pi unrestricted tailResult : (family X86NativeAssemblyResult) .
283 (family X86NativeAssemblyResult))))))) =
284 (lambda unrestricted conditionFlag : Nat .
285 (lambda unrestricted condition : (family X86NativeCondition) .
286 (lambda unrestricted targetName : Bytes .
287 (lambda unrestricted labels : (family X86NativeLabelTable) .
288 (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) .
289 (lambda unrestricted tailResult : (family X86NativeAssemblyResult) .
290 (eliminate
291 X86NativeLabelLookupResult
292 (lambda unrestricted lookup : (family X86NativeLabelLookupResult) .
293 (family X86NativeAssemblyResult))
294 (x86NativeLookupLabel targetName labels)
295 (branch
296 X86NativeLabelFound
297 targetOffset
298 .
299 (eliminate
300 X86NativeRelativeDisplacementResult
301 (lambda unrestricted displacementResult : (family X86NativeRelativeDisplacementResult) .
302 (family X86NativeAssemblyResult))
303 (x86NativeRelativeDisplacement targetOffset sourceEnd)
304 (branch
305 X86NativeRelativeDisplacementSuccess
306 displacement
307 .
308 (nat-eliminate
309 (lambda unrestricted conditional : Nat . (family X86NativeAssemblyResult))
310 (x86NativePrependAssemblyBytes
311 (x86EncodeNativeInstruction
312 (constructor
313 X86NativeInstruction
314 X86NativeJumpRelative32
315 (x86NativeUnsigned32Displacement displacement)))
316 tailResult)
317 (lambda unrestricted predecessor : Nat .
318 (lambda unrestricted induction : (family X86NativeAssemblyResult) .
319 (x86NativePrependAssemblyBytes
320 (x86EncodeNativeInstruction
321 (constructor
322 X86NativeInstruction
323 X86NativeJumpConditionRelative32
324 condition
325 (x86NativeUnsigned32Displacement displacement)))
326 tailResult)))
327 conditionFlag))
328 (branch
329 X86NativeRelativeDisplacementOutOfRange
330 .
331 (constructor
332 X86NativeAssemblyResult
333 X86NativeAssemblyDisplacementOutOfRange
334 targetName))))
335 (branch
336 X86NativeLabelMissing
337 .
338 (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel targetName)))))))))
339
340def x86NativeEncodeLEAToLabel :
341 (pi unrestricted destination : (family X86NativeRegister64) .
342 (pi unrestricted targetName : Bytes .
343 (pi unrestricted labels : (family X86NativeLabelTable) .
344 (pi unrestricted sourceEnd : (family X86NativeUnsigned32) .
345 (pi unrestricted tailResult : (family X86NativeAssemblyResult) .
346 (family X86NativeAssemblyResult)))))) =
347 (lambda unrestricted destination : (family X86NativeRegister64) .
348 (lambda unrestricted targetName : Bytes .
349 (lambda unrestricted labels : (family X86NativeLabelTable) .
350 (lambda unrestricted sourceEnd : (family X86NativeUnsigned32) .
351 (lambda unrestricted tailResult : (family X86NativeAssemblyResult) .
352 (eliminate
353 X86NativeLabelLookupResult
354 (lambda unrestricted lookup : (family X86NativeLabelLookupResult) .
355 (family X86NativeAssemblyResult))
356 (x86NativeLookupLabel targetName labels)
357 (branch
358 X86NativeLabelFound
359 targetOffset
360 .
361 (eliminate
362 X86NativeRelativeDisplacementResult
363 (lambda unrestricted displacementResult : (family X86NativeRelativeDisplacementResult) .
364 (family X86NativeAssemblyResult))
365 (x86NativeRelativeDisplacement targetOffset sourceEnd)
366 (branch
367 X86NativeRelativeDisplacementSuccess
368 displacement
369 .
370 (x86NativePrependAssemblyBytes
371 (x86EncodeNativeInstruction
372 (constructor
373 X86NativeInstruction
374 X86NativeLoadEffectiveAddressRIP
375 destination
376 (x86NativeUnsigned32Displacement displacement)))
377 tailResult))
378 (branch
379 X86NativeRelativeDisplacementOutOfRange
380 .
381 (constructor
382 X86NativeAssemblyResult
383 X86NativeAssemblyDisplacementOutOfRange
384 targetName))))
385 (branch
386 X86NativeLabelMissing
387 .
388 (constructor X86NativeAssemblyResult X86NativeAssemblyMissingLabel targetName))))))))
389
390def x86NativeEncodeAssemblyFrom :
391 (pi unrestricted assembly : (family X86NativeAssembly) .
392 (pi unrestricted labels : (family X86NativeLabelTable) .
393 (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyResult)))) =
394 (lambda unrestricted assembly : (family X86NativeAssembly) .
395 (eliminate
396 X86NativeAssembly
397 (lambda unrestricted value : (family X86NativeAssembly) .
398 (pi unrestricted labels : (family X86NativeLabelTable) .
399 (pi unrestricted offset : (family X86NativeUnsigned32) . (family X86NativeAssemblyResult))))
400 assembly
401 (branch
402 X86NativeAssemblyEnd
403 .
404 (lambda unrestricted labels : (family X86NativeLabelTable) .
405 (lambda unrestricted offset : (family X86NativeUnsigned32) .
406 (constructor X86NativeAssemblyResult X86NativeAssemblyEncoded b""))))
407 (branch
408 X86NativeAssemblyEmit
409 instruction
410 tail
411 encodeTail
412 .
413 (lambda unrestricted labels : (family X86NativeLabelTable) .
414 (lambda unrestricted offset : (family X86NativeUnsigned32) .
415 (let unrestricted encoded =
416 (x86EncodeNativeInstruction instruction)
417 in
418 (eliminate
419 X86NativeUnsigned32Result
420 (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) .
421 (family X86NativeAssemblyResult))
422 (x86NativeAdvanceUnsigned32ByBytes offset encoded)
423 (branch
424 X86NativeUnsigned32Success
425 nextOffset
426 .
427 (x86NativePrependAssemblyBytes encoded (encodeTail labels nextOffset)))
428 (branch
429 X86NativeUnsigned32Overflow
430 .
431 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow)))))))
432 (branch
433 X86NativeAssemblyLabel
434 name
435 tail
436 encodeTail
437 .
438 (lambda unrestricted labels : (family X86NativeLabelTable) .
439 (lambda unrestricted offset : (family X86NativeUnsigned32) . (encodeTail labels offset))))
440 (branch
441 X86NativeAssemblyJump
442 target
443 tail
444 encodeTail
445 .
446 (lambda unrestricted labels : (family X86NativeLabelTable) .
447 (lambda unrestricted offset : (family X86NativeUnsigned32) .
448 (eliminate
449 X86NativeUnsigned32Result
450 (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) .
451 (family X86NativeAssemblyResult))
452 (x86NativeAdvanceUnsigned32ByBytes offset (bytes 0 0 0 0 0))
453 (branch
454 X86NativeUnsigned32Success
455 nextOffset
456 .
457 (x86NativeEncodeJumpToLabel
458 zero
459 (constructor X86NativeCondition X86NativeConditionZero)
460 target
461 labels
462 nextOffset
463 (encodeTail labels nextOffset)))
464 (branch
465 X86NativeUnsigned32Overflow
466 .
467 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))))))
468 (branch
469 X86NativeAssemblyJumpCondition
470 condition
471 target
472 tail
473 encodeTail
474 .
475 (lambda unrestricted labels : (family X86NativeLabelTable) .
476 (lambda unrestricted offset : (family X86NativeUnsigned32) .
477 (eliminate
478 X86NativeUnsigned32Result
479 (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) .
480 (family X86NativeAssemblyResult))
481 (x86NativeAdvanceUnsigned32ByBytes offset (bytes 0 0 0 0 0 0))
482 (branch
483 X86NativeUnsigned32Success
484 nextOffset
485 .
486 (x86NativeEncodeJumpToLabel
487 (succ zero)
488 condition
489 target
490 labels
491 nextOffset
492 (encodeTail labels nextOffset)))
493 (branch
494 X86NativeUnsigned32Overflow
495 .
496 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))))))
497 (branch
498 X86NativeAssemblyLoadEffectiveAddressRIPLabel
499 destination
500 target
501 tail
502 encodeTail
503 .
504 (lambda unrestricted labels : (family X86NativeLabelTable) .
505 (lambda unrestricted offset : (family X86NativeUnsigned32) .
506 (eliminate
507 X86NativeUnsigned32Result
508 (lambda unrestricted advanceResult : (family X86NativeUnsigned32Result) .
509 (family X86NativeAssemblyResult))
510 (x86NativeAdvanceUnsigned32ByBytes offset (bytes 0 0 0 0 0 0 0))
511 (branch
512 X86NativeUnsigned32Success
513 nextOffset
514 .
515 (x86NativeEncodeLEAToLabel
516 destination
517 target
518 labels
519 nextOffset
520 (encodeTail labels nextOffset)))
521 (branch
522 X86NativeUnsigned32Overflow
523 .
524 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))))))))
525
526def x86NativeAssemble :
527 (pi unrestricted assembly : (family X86NativeAssembly) . (family X86NativeAssemblyResult)) =
528 (lambda unrestricted assembly : (family X86NativeAssembly) .
529 (eliminate
530 X86NativeAssemblyLayoutResult
531 (lambda unrestricted layout : (family X86NativeAssemblyLayoutResult) .
532 (family X86NativeAssemblyResult))
533 (x86NativeLayoutAssembly assembly)
534 (branch
535 X86NativeAssemblyLayoutSuccess
536 labels
537 size
538 .
539 (x86NativeEncodeAssemblyFrom assembly labels x86NativeUnsigned32Zero))
540 (branch
541 X86NativeAssemblyDuplicateLabel
542 duplicateName
543 .
544 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeDuplicateLabel duplicateName))
545 (branch
546 X86NativeAssemblyOffsetOverflow
547 .
548 (constructor X86NativeAssemblyResult X86NativeAssemblyEncodeOffsetOverflow))))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.