cranelift-codegen 0.130.0

Low-level code generator library
Documentation
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
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
;;;; Instruction definition ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(type OperandSize extern (enum Size32 Size64))

(decl ty_to_operand_size (Type) OperandSize)
(rule (ty_to_operand_size $I32) (OperandSize.Size32))
(rule (ty_to_operand_size $I64) (OperandSize.Size64))

;; Note: in the instructions below, we order destination registers first and
;; then source registers afterwards.
(type MInst
  (enum
    ;;;; Pseudo-Instructions ;;;;

    ;; A pseudo-instruction that captures register arguments in vregs.
    (Args (args VecArgPair))

    ;; A pseudo-instruction that moves vregs to return registers.
    (Rets (rets VecRetPair))

    (DummyUse (reg Reg))

    ;; Implementation of `br_table`, uses `idx` to jump to one of `targets` or
    ;; jumps to `default` if it's out-of-bounds.
    (BrTable
      (idx XReg)
      (default MachLabel)
      (targets BoxVecMachLabel))

    ;;;; Actual Instructions ;;;;

    ;; Trap if `cond` is true.
    (TrapIf (cond Cond) (code TrapCode))

    ;; Nothing.
    (Nop)

    ;; Move a special register (e.g. sp, fp, lr, etc) in to a general-purpose
    ;; register.
    (GetSpecial
      (dst WritableXReg)
      (reg XReg))

    ;; Load an external symbol's address into a register.
    (LoadExtNameNear (dst WritableXReg) (name BoxExternalName) (offset i64))
    (LoadExtNameFar (dst WritableXReg) (name BoxExternalName) (offset i64))

    ;; A direct call to a known callee.
    (Call (info BoxCallInfo))

    ;; An indirect call to an unknown callee.
    (IndirectCall (info BoxCallIndInfo))

    ;; A direct return-call macro instruction.
    (ReturnCall (info BoxReturnCallInfo))

    ;; An indirect return-call macro instruction.
    (ReturnIndirectCall (info BoxReturnCallIndInfo))

    ;; An indirect call out to a host-defined function. The host function
    ;; pointer is the first "argument" of this function call.
    (IndirectCallHost (info BoxCallIndirectHostInfo))

    ;; Unconditional jumps.
    (Jump (label MachLabel))

    ;; Jump to `then` if `c` is true, otherwise to `else`.
    (BrIf (cond Cond) (taken MachLabel) (not_taken MachLabel))

    ;; Load the memory address referenced by `mem` into `dst`.
    (LoadAddr (dst WritableXReg) (mem Amode))

    ;; Load `ty` bytes from memory pointed to by `mem` and store in `dst`.
    ;;
    ;; How much is written to the register is defined by `ExtKind`. The `flags`
    ;; control behavior such as endianness.
    (XLoad (dst WritableXReg) (mem Amode) (ty Type) (flags MemFlags))
    (FLoad (dst WritableFReg) (mem Amode) (ty Type) (flags MemFlags))
    (VLoad (dst WritableVReg) (mem Amode) (ty Type) (flags MemFlags))

    ;; Stores.
    (XStore (mem Amode) (src XReg) (ty Type) (flags MemFlags))
    (FStore (mem Amode) (src FReg) (ty Type) (flags MemFlags))
    (VStore (mem Amode) (src VReg) (ty Type) (flags MemFlags))

    ;; A raw pulley instruction generated at compile-time via Pulley's
    ;; `for_each_op!` macro. This variant has `pulley_*` constructors to
    ;; emit this instruction and auto-generated methods for other various
    ;; bits and pieces of boilerplate in the backend.
    (Raw (raw RawInst))

    ;; Island generation prior to variable-length instructions.
    (EmitIsland (space_needed u32))

    ;; A pseudoinstruction that loads the address of a label.
    (LabelAddress (dst WritableXReg)
                  (label MachLabel))

    ;; A pseudoinstruction that serves as a sequence point.
    (SequencePoint)
  )
)

;; Helper type on conditional branches and traps to represent what the
;; condition that is being performed is.
;;
;; Used in `BrIf` and `TrapIf` above for example.
(type Cond
  (enum
    ;; True if `reg` contains a nonzero value in the low 32-bits.
    (If32 (reg XReg))
    ;; True if `reg` contains a zero in the low 32-bits.
    (IfNot32 (reg XReg))

    ;; Conditionals for comparing the low 32-bits of two registers.
    (IfXeq32 (src1 XReg) (src2 XReg))
    (IfXneq32 (src1 XReg) (src2 XReg))
    (IfXslt32 (src1 XReg) (src2 XReg))
    (IfXslteq32 (src1 XReg) (src2 XReg))
    (IfXult32 (src1 XReg) (src2 XReg))
    (IfXulteq32 (src1 XReg) (src2 XReg))

    (IfXeq32I32 (src1 XReg) (src2 i32))
    (IfXneq32I32 (src1 XReg) (src2 i32))
    (IfXslt32I32 (src1 XReg) (src2 i32))
    (IfXslteq32I32 (src1 XReg) (src2 i32))
    (IfXult32I32 (src1 XReg) (src2 u32))
    (IfXulteq32I32 (src1 XReg) (src2 u32))
    (IfXsgt32I32 (src1 XReg) (src2 i32))
    (IfXsgteq32I32 (src1 XReg) (src2 i32))
    (IfXugt32I32 (src1 XReg) (src2 u32))
    (IfXugteq32I32 (src1 XReg) (src2 u32))

    ;; Conditionals for comparing two 64-bit registers.
    (IfXeq64 (src1 XReg) (src2 XReg))
    (IfXneq64 (src1 XReg) (src2 XReg))
    (IfXslt64 (src1 XReg) (src2 XReg))
    (IfXslteq64 (src1 XReg) (src2 XReg))
    (IfXult64 (src1 XReg) (src2 XReg))
    (IfXulteq64 (src1 XReg) (src2 XReg))

    (IfXeq64I32 (src1 XReg) (src2 i32))
    (IfXneq64I32 (src1 XReg) (src2 i32))
    (IfXslt64I32 (src1 XReg) (src2 i32))
    (IfXslteq64I32 (src1 XReg) (src2 i32))
    (IfXult64I32 (src1 XReg) (src2 u32))
    (IfXulteq64I32 (src1 XReg) (src2 u32))
    (IfXsgt64I32 (src1 XReg) (src2 i32))
    (IfXsgteq64I32 (src1 XReg) (src2 i32))
    (IfXugt64I32 (src1 XReg) (src2 u32))
    (IfXugteq64I32 (src1 XReg) (src2 u32))
  )
)

(decl cond_invert (Cond) Cond)
(extern constructor cond_invert cond_invert)

(decl raw_inst_to_inst (RawInst) MInst)
(rule (raw_inst_to_inst inst) (MInst.Raw inst))
(convert RawInst MInst raw_inst_to_inst)

(type U6 (primitive U6))
(type PcRelOffset (primitive PcRelOffset))
(type BoxCallInfo (primitive BoxCallInfo))
(type BoxCallIndInfo (primitive BoxCallIndInfo))
(type BoxReturnCallInfo (primitive BoxReturnCallInfo))
(type BoxReturnCallIndInfo (primitive BoxReturnCallIndInfo))
(type UpperXRegSet (primitive UpperXRegSet))
(type BoxCallIndirectHostInfo (primitive BoxCallIndirectHostInfo))

;;;; Address Modes ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(type ExtKind (enum None Sign32 Sign64 Zero32 Zero64))
(type VExtKind (enum None S8x8 U8x8 S16x4 U16x4 S32x2 U32x2))

;; Helper to convert a `(Value Offset32)` to `(Value i32)` while peeling off
;; constant addition within the first `Value` into the static offset, if
;; possible.
;;
;; Note that ideally this wouldn't be necessary and we could rely on the egraph
;; pass to do this but that's not implemented at this time.
(type ValueOffset (enum (Both (value Value) (offset i32))))
(decl pure amode_base (Value Offset32) ValueOffset)
(rule (amode_base addr (offset32 offset)) (ValueOffset.Both addr offset))
(rule 1 (amode_base (iadd addr (i32_from_iconst b)) (offset32 offset))
  (if-let new_offset (i32_checked_add b offset))
  (ValueOffset.Both addr new_offset))

(type StackAMode extern (enum))

(type Amode
  (enum
    (SpOffset (offset i32))
    (RegOffset (base XReg) (offset i32))
    (Stack (amode StackAMode))
  )
)

(decl amode (Value Offset32) Amode)
(rule (amode addr offset)
  (if-let (ValueOffset.Both a o) (amode_base addr offset))
  (Amode.RegOffset a o))

;;; ISLE representation of the `AddrO32` ("*_o32") addressing mode in Pulley.
(type AddrO32
  (enum
    (Base
      (addr XReg)
      (offset i32))))

;; Constructor for the `AddrO32` type used in `*_o32` loads/stores
(decl addro32 (Value Offset32) AddrO32)
(rule (addro32 addr offset)
  (if-let (ValueOffset.Both reg off32) (amode_base addr offset))
  (AddrO32.Base reg off32))

;;; ISLE representation of the `AddrZ` ("*_z") addressing mode in Pulley.
(type AddrZ
  (enum
    (Base
      (addr XReg)
      (offset i32))))

;; Constructor for the `AddrZ` type used in `*_z` loads/stores
(decl addrz (Value Offset32) AddrZ)
(rule (addrz addr offset)
  (if-let (ValueOffset.Both reg off32) (amode_base addr offset))
  (AddrZ.Base reg off32))

;;; ISLE representation of the `AddrG32` ("*_g32") addressing mode in Pulley.
(type AddrG32
  (enum
    (RegisterBound
      (host_heap_base XReg)
      (host_heap_bound XReg)
      (wasm_addr XReg)
      (offset u16))))

;;; ISLE representation of the `AddrG32Bne` ("*_g32bne") addressing mode in Pulley.
(type AddrG32Bne
  (enum
    (BoundNe
      (host_heap_base XReg)
      (host_heap_bound_addr XReg)
      (host_heap_bound_offset u8)
      (wasm_addr XReg)
      (offset u8))))

;; Helper to determine the endianness of `MemFlags` taking the current target
;; into account.
(decl pure endianness (MemFlags) Endianness)
(extern constructor endianness endianness)
(type Endianness extern (enum Little Big))

(decl pure is_native_endianness (Endianness) bool)
(extern constructor is_native_endianness is_native_endianness)

;; Partial constructor and type representing a "sinkable load" which can be
;; moved into another instruction. Note that `SinkableLoad` should not be used
;; as-is and should instead be converted to a `SunkLoad`.
;;
;; To be a sinkable load the load must pass:
;;
;; * The `is_sinkable_inst` shared amongst backends test must be `true`
;; * The load must be in "native endianness"
;; * The static offset must fit in an unsigned 8-bit integer.
;;
;; If the last two requirements here are too restrictive then multiple helpers
;; might be needed in the future.
(type SinkableLoad (enum (Load (inst Inst) (ty Type) (addr Value) (offset u8))))
(decl pure partial sinkable_load (Value) SinkableLoad)
(rule (sinkable_load value @ (value_type ty))
  (if-let inst @ (load flags addr (offset32 offset)) (is_sinkable_inst value))
  (if-let true (is_native_endianness (endianness flags)))
  (if-let true (memflags_nontrapping flags))
  (if-let offset8 (i32_try_into_u8 offset))
  (SinkableLoad.Load inst ty addr offset8))

;; Representation of a "sunk load" where once this is created it must be used.
;;
;; This is paired with `sinkable_load` above where that's used in an `if-let`
;; and then once the rule is selected this is used to commit to using the load.
;; Callers will likely match on `SunkLoad` itself to extract the
;; type/value/offset that the load matches.
(type SunkLoad (enum (Load (ty Type) (addr Value) (offset u8))))
(decl sink_load (SinkableLoad) SunkLoad)
(rule (sink_load (SinkableLoad.Load inst ty addr offset))
  (let ((_ Unit (sink_inst inst)))
    (SunkLoad.Load ty addr offset)))

(convert SinkableLoad SunkLoad sink_load)

;; Helper for determining what the pointer width of the host is.
(type PointerWidth extern (enum PointerWidth32 PointerWidth64))
(decl pure pointer_width () PointerWidth)
(extern constructor pointer_width pointer_width)

(decl pure memflags_nontrapping (MemFlags) bool)
(extern constructor memflags_nontrapping memflags_nontrapping)

(decl pure memflags_is_wasm (MemFlags) bool)
(extern constructor memflags_is_wasm memflags_is_wasm)

;; Helper type to represent a "pending" `AddrG32` value.
(type G32 (enum (All (heap_base Value) (heap_bound Value) (wasm_addr Value) (offset u16))))

;; Auto-conversion from `G32` to `AddrG32`.
(decl gen_addrg32 (G32) AddrG32)
(rule (gen_addrg32 (G32.All base bound wasm offset))
  (AddrG32.RegisterBound base bound wasm offset))
(convert G32 AddrG32 gen_addrg32)

;; Helper type to represent a "pending" `AddrG32Bne` value.
(type G32Bne (enum (All (heap_base Value) (heap_bound SinkableLoad) (wasm_addr Value) (offset u8))))

;; Auto-conversion from `G32Bne` to `AddrG32Bne`.
(decl gen_addrg32bne (G32Bne) AddrG32Bne)
(rule (gen_addrg32bne (G32Bne.All base heap_bound_load wasm offset))
  (gen_addrg32bne_for_real base heap_bound_load wasm offset))
(convert G32Bne AddrG32Bne gen_addrg32bne)

;; Small workaround to pattern-match `SunkLoad` here.
(decl gen_addrg32bne_for_real (XReg SunkLoad XReg u8) AddrG32Bne)
(rule (gen_addrg32bne_for_real base (SunkLoad.Load _ bound_addr bound_offset) wasm_addr offset)
  (AddrG32Bne.BoundNe base bound_addr bound_offset wasm_addr offset))

;; Helper to extract `G32Bne` from `G32` if applicable.
;;
;; This is possible when the heap bound is itself a sinkable load which can get
;; folded into `G32Bne`.
(decl pure partial addrg32bne (G32) G32Bne)
(rule (addrg32bne (G32.All heap_base heap_bound wasm_addr offset))
  (if-let heap_bound_load (sinkable_load heap_bound))
  (if-let offset8 (u16_try_into_u8 offset))
  (G32Bne.All heap_base heap_bound_load wasm_addr offset8))

;; Main entrypoint for matching a `G32` address which can be used in `*_g32`
;; pulley instructions for loads/stores.
;;
;; Pulley loads/stores are emitted as fallible loads/stores where the only
;; defined trapping address is null. That's modeled as a load-from-`select`
;; where an out-of-bounds condition yields null.
;;
;; Here the top-layer of this rule matches the `(select ...)` node where 0 is
;; used if the oob condition is true. Otherwise the raw address is used for the
;; load/store.
(decl pure partial wasm_g32 (Value Offset32 MemFlags Type) G32)
(rule (wasm_g32 (select oob (u64_from_iconst 0) raw_addr) (offset32 0) flags ty)
  ;; This must be a wasm load/store according to `MemFlags`, namely that it's
  ;; got a "HEAP_OUT_OF_BOUNDS" trap code and it's little-endian.
  (if-let true (memflags_is_wasm flags))
  ;; Peel off the static wasm offset from `raw_addr`, if one is present. If
  ;; one isn't present then `heap_offset` will be zero. This handles the `N`
  ;; in wasm instructions `i32.load offset=N`.
  (if-let (HostOffset.All host_addr heap_offset) (host_offset raw_addr))
  ;; Next see if the `oob` and `raw_addr` combination match. This will attempt
  ;; extract a full bounds check from these values. If everything succeeds the
  ;; final step is then to extract an 8-bit offset of the load/store operation,
  ;; if appplicable, assuming that the constants used in various places all line
  ;; up just right.
  (if-let (OobSelect.All base bound wasm_addr access_size_plus_offset)
    (wasm_oob_select oob host_addr))
  (if-let offset16 (g32_offset heap_offset ty access_size_plus_offset))
  (G32.All base bound wasm_addr offset16))

;; Host helper to do the math to extract the offset here.
;;
;; Ensures that the first argument, the heap offset on the load, plus the size
;; of the type equals the third argument, the bounds-checked static offset. If
;; the offset then fits within `u16` it's returned.
(decl pure partial g32_offset (i32 Type u64) u16)
(extern constructor g32_offset g32_offset)

;; Helper used in `wasm_g32` above to extract `(iadd addr N)` where `N` is a
;; constant. If there is no constant then the constant 0 is returned instead.
;;
;; Note that this also requires `addr` itself to be an `iadd` internally to
;; represent the host address plus the guest offset. If `addr` isn't internally
;; an `iadd` then the `N` here is instead probably the static address in the
;; guest.
(decl pure host_offset (Value) HostOffset)
(type HostOffset (enum (All (a Value) (b i32))))
(rule 0 (host_offset val) (HostOffset.All val 0))
(rule 1 (host_offset (iadd val @ (iadd _ _) (i32_from_iconst n))) (HostOffset.All val n))
(rule 2 (host_offset (iadd (i32_from_iconst n) val @ (iadd _ _))) (HostOffset.All val n))

;; Helper to test whether the first argument `oob` contains a condition for
;; matching whether second argument `addr` is out-of-bounds. Searches for a
;; variety of structures that optimizations or the frontend may produce.
(decl pure partial wasm_oob_select (Value Value) OobSelect)
(type OobSelect (enum (All (a Value) (b Value) (c Value) (d u64))))

;; 32-bit hosts: search either side of the `iadd` for the base address within
;; `oob` to see if it's a matching condition.
(rule 0 (wasm_oob_select oob (iadd base wasm_addr @ (value_type $I32)))
  (if-let (OobCond.All bound n) (wasm_oob_cond wasm_addr oob))
  (if-let (PointerWidth.PointerWidth32) (pointer_width))
  (OobSelect.All base bound wasm_addr n))
(rule 1 (wasm_oob_select oob (iadd wasm_addr @ (value_type $I32) base))
  (if-let (OobCond.All bound n) (wasm_oob_cond wasm_addr oob))
  (if-let (PointerWidth.PointerWidth32) (pointer_width))
  (OobSelect.All base bound wasm_addr n))

;; 64-bit hosts: also search either side, but the wasm address must also be
;; a `uextend` from a 32-bit value.
(rule 0 (wasm_oob_select oob (iadd base wasm_addr_ext @ (value_type $I64)))
  (if-let (OobCond.All bound n) (wasm_oob_cond wasm_addr_ext oob))
  (if-let wasm_addr (wasm32_addr_for_host64 wasm_addr_ext))
  (if-let (PointerWidth.PointerWidth64) (pointer_width))
  (OobSelect.All base bound wasm_addr n))
(rule 1 (wasm_oob_select oob (iadd wasm_addr_ext @ (value_type $I64) base))
  (if-let (OobCond.All bound n) (wasm_oob_cond wasm_addr_ext oob))
  (if-let wasm_addr (wasm32_addr_for_host64 wasm_addr_ext))
  (if-let (PointerWidth.PointerWidth64) (pointer_width))
  (OobSelect.All base bound wasm_addr n))

;; Helper to extract a 32-bit `Value` from a 64-bit input. The returned value,
;; if one is returned, can losslessly represent the original value when zero
;; extended from 32-bits. That means that this only matches `(uextend ...)` or
;; an `iconst` which already fits in 32 bits.
(decl pure partial wasm32_addr_for_host64 (Value) Value)
(rule (wasm32_addr_for_host64 (uextend addr @ (value_type $I32))) addr)
(rule (wasm32_addr_for_host64 val @ (u32_from_iconst _)) val)

;; Helper to search for the first argument, `wasm_addr`, within the oob
;; condition second argument, `oob`. It should appear as an integer comparison
;; of the address against a particular bound.
(decl pure partial wasm_oob_cond (Value Value) OobCond)
(type OobCond (enum (All (a Value) (b u64))))
(rule (wasm_oob_cond wasm_addr (ugt wasm_addr (isub bound (u64_from_iconst n))))
  (OobCond.All bound n))
(rule (wasm_oob_cond wasm_addr (ult (isub bound (u64_from_iconst n)) wasm_addr))
  (OobCond.All bound n))

;;;; Newtypes for Different Register Classes ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(type XReg (primitive XReg))
(type WritableXReg (primitive WritableXReg))

(type FReg (primitive FReg))
(type WritableFReg (primitive WritableFReg))

(type VReg (primitive VReg))
(type WritableVReg (primitive WritableVReg))

;; Construct a new `XReg` from a `Reg`.
;;
;; Asserts that the register has an integer RegClass.
(decl xreg_new (Reg) XReg)
(extern constructor xreg_new xreg_new)
(convert Reg XReg xreg_new)

;; Construct a new `WritableXReg` from a `WritableReg`.
;;
;; Asserts that the register has an integer RegClass.
(decl writable_xreg_new (WritableReg) WritableXReg)
(extern constructor writable_xreg_new writable_xreg_new)
(convert WritableReg WritableXReg writable_xreg_new)

;; Put a value into a XReg.
;;
;; Asserts that the value goes into a XReg.
(decl put_in_xreg (Value) XReg)
(rule (put_in_xreg val) (xreg_new (put_in_reg val)))
(convert Value XReg put_in_xreg)

;; Construct an `InstOutput` out of a single XReg register.
(decl output_xreg (XReg) InstOutput)
(rule (output_xreg x) (output_reg x))
(convert XReg InstOutput output_xreg)

;; Convert a `WritableXReg` to an `XReg`.
(decl pure writable_xreg_to_xreg (WritableXReg) XReg)
(extern constructor writable_xreg_to_xreg writable_xreg_to_xreg)
(convert WritableXReg XReg writable_xreg_to_xreg)

;; Convert a `WritableXReg` to an `WritableReg`.
(decl pure writable_xreg_to_writable_reg (WritableXReg) WritableReg)
(extern constructor writable_xreg_to_writable_reg writable_xreg_to_writable_reg)
(convert WritableXReg WritableReg writable_xreg_to_writable_reg)

;; Convert a `WritableXReg` to an `Reg`.
(decl pure writable_xreg_to_reg (WritableXReg) Reg)
(rule (writable_xreg_to_reg x) (writable_xreg_to_writable_reg x))
(convert WritableXReg Reg writable_xreg_to_reg)

;; Convert an `XReg` to a `Reg`.
(decl pure xreg_to_reg (XReg) Reg)
(extern constructor xreg_to_reg xreg_to_reg)
(convert XReg Reg xreg_to_reg)

;; Convert a `XReg` to a `ValueRegs`.
(decl xreg_to_value_regs (XReg) ValueRegs)
(rule (xreg_to_value_regs x) (value_reg x))
(convert XReg ValueRegs xreg_to_reg)

;; Convert a `WritableXReg` to a `ValueRegs`.
(decl writable_xreg_to_value_regs (WritableXReg) ValueRegs)
(rule (writable_xreg_to_value_regs x) (value_reg x))
(convert WritableXReg ValueRegs writable_xreg_to_value_regs)

;; Allocates a new `WritableXReg`.
(decl temp_writable_xreg () WritableXReg)
(rule (temp_writable_xreg) (temp_writable_reg $I64))

;; Construct a new `FReg` from a `Reg`.
;;
;; Asserts that the register has a Float RegClass.
(decl freg_new (Reg) FReg)
(extern constructor freg_new freg_new)
(convert Reg FReg freg_new)

;; Construct a new `WritableFReg` from a `WritableReg`.
;;
;; Asserts that the register has a Float RegClass.
(decl writable_freg_new (WritableReg) WritableFReg)
(extern constructor writable_freg_new writable_freg_new)
(convert WritableReg WritableFReg writable_freg_new)

;; Put a value into a FReg.
;;
;; Asserts that the value goes into a FReg.
(decl put_in_freg (Value) FReg)
(rule (put_in_freg val) (freg_new (put_in_reg val)))
(convert Value FReg put_in_freg)

;; Construct an `InstOutput` out of a single FReg register.
(decl output_freg (FReg) InstOutput)
(rule (output_freg x) (output_reg x))
(convert FReg InstOutput output_freg)

;; Convert a `WritableFReg` to an `FReg`.
(decl pure writable_freg_to_freg (WritableFReg) FReg)
(extern constructor writable_freg_to_freg writable_freg_to_freg)
(convert WritableFReg FReg writable_freg_to_freg)

;; Convert a `WritableFReg` to an `WritableReg`.
(decl pure writable_freg_to_writable_reg (WritableFReg) WritableReg)
(extern constructor writable_freg_to_writable_reg writable_freg_to_writable_reg)
(convert WritableFReg WritableReg writable_freg_to_writable_reg)

;; Convert a `WritableFReg` to an `Reg`.
(decl pure writable_freg_to_reg (WritableFReg) Reg)
(rule (writable_freg_to_reg x) (writable_freg_to_writable_reg x))
(convert WritableFReg Reg writable_freg_to_reg)

;; Convert an `FReg` to a `Reg`.
(decl pure freg_to_reg (FReg) Reg)
(extern constructor freg_to_reg freg_to_reg)
(convert FReg Reg freg_to_reg)

;; Convert a `FReg` to a `ValueRegs`.
(decl freg_to_value_regs (FReg) ValueRegs)
(rule (freg_to_value_regs x) (value_reg x))
(convert FReg ValueRegs xreg_to_reg)

;; Convert a `WritableFReg` to a `ValueRegs`.
(decl writable_freg_to_value_regs (WritableFReg) ValueRegs)
(rule (writable_freg_to_value_regs x) (value_reg x))
(convert WritableFReg ValueRegs writable_freg_to_value_regs)

;; Allocates a new `WritableFReg`.
(decl temp_writable_freg () WritableFReg)
(rule (temp_writable_freg) (temp_writable_reg $F64))

;; Construct a new `VReg` from a `Reg`.
;;
;; Asserts that the register has a Vector RegClass.
(decl vreg_new (Reg) VReg)
(extern constructor vreg_new vreg_new)
(convert Reg VReg vreg_new)

;; Construct a new `WritableVReg` from a `WritableReg`.
;;
;; Asserts that the register has a Vector RegClass.
(decl writable_vreg_new (WritableReg) WritableVReg)
(extern constructor writable_vreg_new writable_vreg_new)
(convert WritableReg WritableVReg writable_vreg_new)

;; Put a value into a VReg.
;;
;; Asserts that the value goes into a VReg.
(decl put_in_vreg (Value) VReg)
(rule (put_in_vreg val) (vreg_new (put_in_reg val)))
(convert Value VReg put_in_vreg)

;; Construct an `InstOutput` out of a single VReg register.
(decl output_vreg (VReg) InstOutput)
(rule (output_vreg x) (output_reg x))
(convert VReg InstOutput output_vreg)

;; Convert a `WritableVReg` to an `VReg`.
(decl pure writable_vreg_to_vreg (WritableVReg) VReg)
(extern constructor writable_vreg_to_vreg writable_vreg_to_vreg)
(convert WritableVReg VReg writable_vreg_to_vreg)

;; Convert a `WritableVReg` to an `WritableReg`.
(decl pure writable_vreg_to_writable_reg (WritableVReg) WritableReg)
(extern constructor writable_vreg_to_writable_reg writable_vreg_to_writable_reg)
(convert WritableVReg WritableReg writable_vreg_to_writable_reg)

;; Convert a `WritableVReg` to an `Reg`.
(decl pure writable_vreg_to_reg (WritableVReg) Reg)
(rule (writable_vreg_to_reg x) (writable_vreg_to_writable_reg x))
(convert WritableVReg Reg writable_vreg_to_reg)

;; Convert an `VReg` to a `Reg`.
(decl pure vreg_to_reg (VReg) Reg)
(extern constructor vreg_to_reg vreg_to_reg)
(convert VReg Reg vreg_to_reg)

;; Convert a `VReg` to a `ValueRegs`.
(decl vreg_to_value_regs (VReg) ValueRegs)
(rule (vreg_to_value_regs x) (value_reg x))
(convert VReg ValueRegs xreg_to_reg)

;; Convert a `WritableVReg` to a `ValueRegs`.
(decl writable_vreg_to_value_regs (WritableVReg) ValueRegs)
(rule (writable_vreg_to_value_regs x) (value_reg x))
(convert WritableVReg ValueRegs writable_vreg_to_value_regs)

;; Allocates a new `WritableVReg`.
(decl temp_writable_vreg () WritableVReg)
(rule (temp_writable_vreg) (temp_writable_reg $I8X16))

;;;; Materializing Constants ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Lower a constant into a register.
(decl imm (i64) Reg)

;; Special case some instructions with no immediates
(rule 6 (imm 0) (pulley_xzero))
(rule 5 (imm 1) (pulley_xone))

;; For integer constants use the smallest instructions we can that fits the
;; desired value
(rule 4 (imm (i8_from_i64 imm)) (pulley_xconst8 imm))
(rule 3 (imm (i16_from_i64 imm)) (pulley_xconst16 imm))
(rule 2 (imm (i32_from_i64 imm)) (pulley_xconst32 imm))
(rule 1 (imm imm) (pulley_xconst64 imm))

;;;; Instruction Constructors ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(decl pulley_trap_if (Cond TrapCode) SideEffectNoResult)
(rule (pulley_trap_if cond code)
      (SideEffectNoResult.Inst (MInst.TrapIf cond code)))

(decl sp_reg () XReg)
(extern constructor sp_reg sp_reg)

(decl pulley_get_special (XReg) XReg)
(rule (pulley_get_special reg)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.GetSpecial dst reg))))
        dst))

(decl pulley_jump (MachLabel) SideEffectNoResult)
(rule (pulley_jump label)
      (SideEffectNoResult.Inst (MInst.Jump label)))

(decl pulley_br_if (Cond MachLabel MachLabel) SideEffectNoResult)
(rule (pulley_br_if cond taken not_taken)
      (SideEffectNoResult.Inst (MInst.BrIf cond taken not_taken)))

(decl pulley_xload (Amode Type MemFlags) XReg)
(rule (pulley_xload amode ty flags)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.XLoad dst amode ty flags))))
        dst))

(decl pulley_xstore (Amode XReg Type MemFlags) SideEffectNoResult)
(rule (pulley_xstore amode src ty flags)
      (SideEffectNoResult.Inst (MInst.XStore amode src ty flags)))

(decl pulley_fload (Amode Type MemFlags) FReg)
(rule (pulley_fload amode ty flags)
      (let ((dst WritableFReg (temp_writable_freg))
            (_ Unit (emit (MInst.FLoad dst amode ty flags))))
        dst))

(decl pulley_fstore (Amode FReg Type MemFlags) SideEffectNoResult)
(rule (pulley_fstore amode src ty flags)
      (SideEffectNoResult.Inst (MInst.FStore amode src ty flags)))

(decl pulley_vload (Amode Type MemFlags) VReg)
(rule (pulley_vload amode ty flags)
      (let ((dst WritableVReg (temp_writable_vreg))
            (_ Unit (emit (MInst.VLoad dst amode ty flags))))
        dst))

(decl pulley_vstore (Amode VReg Type MemFlags) SideEffectNoResult)
(rule (pulley_vstore amode src ty flags)
      (SideEffectNoResult.Inst (MInst.VStore amode src ty flags)))

(decl gen_br_table (XReg MachLabel BoxVecMachLabel) Unit)
(rule (gen_br_table idx default labels)
      (emit (MInst.BrTable idx default labels)))

;; Helper for creating `MInst.LoadExtNameNear` instructions.
(decl load_ext_name_near (BoxExternalName i64) XReg)
(rule (load_ext_name_near name offset)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.LoadExtNameNear dst name offset))))
        dst))

;; Helper for creating `MInst.LoadExtNameFar` instructions.
(decl load_ext_name_far (BoxExternalName i64) XReg)
(rule (load_ext_name_far name offset)
      (let ((dst WritableXReg (temp_writable_xreg))
            (_ Unit (emit (MInst.LoadExtNameFar dst name offset))))
        dst))

;; Helper for creating `MInst.LoadExtName*` instructions.
(decl load_ext_name (BoxExternalName i64 RelocDistance) XReg)
(rule (load_ext_name name offset (RelocDistance.Near))
  (load_ext_name_near name offset))
(rule (load_ext_name name offset (RelocDistance.Far))
  (load_ext_name_far name offset))

;;;; Helpers for Emitting Calls ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(decl gen_call_info (Sig ExternalName CallArgList CallRetList OptionTryCallInfo bool) BoxCallInfo)
(extern constructor gen_call_info gen_call_info)

(decl gen_call_ind_info (Sig Reg CallArgList CallRetList OptionTryCallInfo) BoxCallIndInfo)
(extern constructor gen_call_ind_info gen_call_ind_info)

(decl gen_call_host_info (Sig ExternalName CallArgList CallRetList OptionTryCallInfo) BoxCallIndirectHostInfo)
(extern constructor gen_call_host_info gen_call_host_info)

(decl gen_return_call_info (Sig ExternalName CallArgList) BoxReturnCallInfo)
(extern constructor gen_return_call_info gen_return_call_info)

(decl gen_return_call_ind_info (Sig Reg CallArgList) BoxReturnCallIndInfo)
(extern constructor gen_return_call_ind_info gen_return_call_ind_info)

;; Helper for creating `MInst.Call` instructions.
(decl call_impl (BoxCallInfo) SideEffectNoResult)
(rule (call_impl info)
      (SideEffectNoResult.Inst (MInst.Call info)))

;; Helper for creating `MInst.IndirectCall` instructions.
(decl indirect_call_impl (BoxCallIndInfo) SideEffectNoResult)
(rule (indirect_call_impl info)
      (SideEffectNoResult.Inst (MInst.IndirectCall info)))

;; Helper for creating `MInst.IndirectCallHost` instructions.
(decl indirect_call_host_impl (BoxCallIndirectHostInfo) SideEffectNoResult)
(rule (indirect_call_host_impl info)
      (SideEffectNoResult.Inst (MInst.IndirectCallHost info)))

;; Helper for creating `MInst.ReturnCall` instructions.
(decl return_call_impl (BoxReturnCallInfo) SideEffectNoResult)
(rule (return_call_impl info)
      (SideEffectNoResult.Inst (MInst.ReturnCall info)))

;; Helper for creating `MInst.ReturnIndirectCall` instructions.
(decl return_indirect_call_impl (BoxReturnCallIndInfo) SideEffectNoResult)
(rule (return_indirect_call_impl info)
      (SideEffectNoResult.Inst (MInst.ReturnIndirectCall info)))

;;;; Helpers for Sign extension ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Sign extend a `Value` to at least 32-bit
(decl zext32 (Value) XReg)
(rule (zext32 val @ (value_type $I8)) (pulley_zext8 val))
(rule (zext32 val @ (value_type $I16)) (pulley_zext16 val))
(rule (zext32 val @ (value_type $I32)) val)
(rule (zext32 val @ (value_type $I64)) val)

;; Same as `zext32` but for sign-extension
(decl sext32 (Value) XReg)
(rule (sext32 val @ (value_type $I8)) (pulley_sext8 val))
(rule (sext32 val @ (value_type $I16)) (pulley_sext16 val))
(rule (sext32 val @ (value_type $I32)) val)
(rule (sext32 val @ (value_type $I64)) val)

;; Sign extend a `Value` to at least 64-bit
(decl zext64 (Value) XReg)
(rule (zext64 val @ (value_type $I8)) (pulley_zext8 val))
(rule (zext64 val @ (value_type $I16)) (pulley_zext16 val))
(rule (zext64 val @ (value_type $I32)) (pulley_zext32 val))
(rule (zext64 val @ (value_type $I64)) val)

;; Same as `zext64` but for sign-extension
(decl sext64 (Value) XReg)
(rule (sext64 val @ (value_type $I8)) (pulley_sext8 val))
(rule (sext64 val @ (value_type $I16)) (pulley_sext16 val))
(rule (sext64 val @ (value_type $I32)) (pulley_sext32 val))
(rule (sext64 val @ (value_type $I64)) val)

;; Helper for creating an `LabelAddress` instruction.
(decl pulley_label_address (MachLabel) Reg)
(rule (pulley_label_address label)
      (let ((dst WritableReg (temp_writable_xreg))
            (_ Unit (emit (MInst.LabelAddress dst label))))
        dst))

;; Helper for creating a `SequencePoint` instruction.
(decl pulley_sequence_point () SideEffectNoResult)
(rule (pulley_sequence_point)
      (SideEffectNoResult.Inst (MInst.SequencePoint)))