aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/TargetPrinter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/TargetPrinter.ml')
-rw-r--r--aarch64/TargetPrinter.ml108
1 files changed, 75 insertions, 33 deletions
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index a9d47bdd..1ca3be16 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -21,23 +21,6 @@ open AisAnnot
open PrintAsmaux
open Fileinfo
-(* Recognition of FP numbers that are supported by the fmov #imm instructions:
- "a normalized binary floating point encoding with 1 sign bit,
- 4 bits of fraction and a 3-bit exponent"
-*)
-
-let is_immediate_float64 bits =
- let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
- let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
- exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
-
-let is_immediate_float32 bits =
- let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
- let mant = Int32.logand bits 0x7F_FFFFl in
- exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
-
-(* Naming and printing registers *)
-
let intsz oc (sz, n) =
match sz with X -> coqint64 oc n | W -> coqint oc n
@@ -107,14 +90,14 @@ let freg oc (sz, r) =
output_string oc (match sz with D -> dreg_name r | S -> sreg_name r)
let preg_asm oc ty = function
- | IR r -> if ty = Tint then wreg oc r else xreg oc r
- | FR r -> if ty = Tsingle then sreg oc r else dreg oc r
- | _ -> assert false
+ | DR (IR (RR1 r)) -> if ty = Tint then wreg oc r else xreg oc r
+ | DR (FR r) -> if ty = Tsingle then sreg oc r else dreg oc r
+| _ -> assert false
let preg_annot = function
- | IR r -> xreg_name r
- | FR r -> dreg_name r
- | _ -> assert false
+ | DR (IR (RR1 r)) -> xreg_name r
+ | DR (FR r) -> dreg_name r
+ | _ -> assert false
(* Base-2 log of a Caml integer *)
let rec log2 n =
@@ -156,12 +139,16 @@ module ELF_System : SYSTEM =
fprintf oc "#:lo12:%a" elf_label lbl
let load_symbol_address oc rd id =
- fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id;
- fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id
+ fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id;
+ fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id
+
+ (* Names of sections *)
let name_of_section = function
| Section_text -> ".text"
- | Section_data i | Section_small_data i ->
+ | Section_data(i, true) ->
+ failwith "_Thread_local unsupported on this platform"
+ | Section_data(i, false) | Section_small_data i ->
variable_section ~sec:".data" ~bss:".bss" i
| Section_const i | Section_small_const i ->
variable_section ~sec:".section .rodata" i
@@ -223,7 +210,9 @@ module MacOS_System : SYSTEM =
let name_of_section = function
| Section_text -> ".text"
- | Section_data i | Section_small_data i ->
+ | Section_data(i, true) ->
+ failwith "_Thread_local unsupported on this platform"
+ | Section_data(i, false) | Section_small_data i ->
variable_section ~sec:".data" i
| Section_const i | Section_small_const i ->
variable_section ~sec:".const" ~reloc:".const_data" i
@@ -343,6 +332,28 @@ module Target(System: SYSTEM): TARGET =
| (r, EOuxtw n) -> fprintf oc "%a, uxtw #%a" wreg r coqint n
| (r, EOuxtx n) -> fprintf oc "%a, uxtx #%a" xreg r coqint n
+ let next_profiling_label =
+ let atomic_incr_counter = ref 0 in
+ fun () ->
+ let r = sprintf ".Lcompcert_atomic_incr%d" !atomic_incr_counter in
+ incr atomic_incr_counter; r;;
+
+ let print_profiling_logger oc id kind =
+ assert (kind >= 0);
+ assert (kind <= 1);
+ fprintf oc "%s begin profiling %a %d: atomic increment\n" comment
+ Profilingaux.pp_id id kind;
+ let ofs = profiling_offset id kind and lbl = next_profiling_label () in
+ fprintf oc " adrp x15, %s+%d\n" profiling_counter_table_name ofs;
+ fprintf oc " add x15, x15, :lo12:(%s+%d)\n" profiling_counter_table_name ofs;
+ fprintf oc "%s:\n" lbl;
+ fprintf oc " ldaxr x17, [x15]\n";
+ fprintf oc " add x17, x17, 1\n";
+ fprintf oc " stlxr w29, x17, [x15]\n";
+ fprintf oc " cbnz w29, %s\n" lbl;
+ fprintf oc "%s end profiling %a %d\n" comment
+ Profilingaux.pp_id id kind;;
+
(* Printing of instructions *)
let print_instruction oc = function
(* Branches *)
@@ -386,7 +397,9 @@ module Target(System: SYSTEM): TARGET =
(* the upper 32 bits of Xrd are set to 0, performing zero-extension *)
| Pldrsw(rd, a) ->
fprintf oc " ldrsw %a, %a\n" xreg rd addressing a
- | Pldp(rd1, rd2, a) ->
+ | Pldpw(rd1, rd2, _, _, a) ->
+ fprintf oc " ldp %a, %a, %a\n" wreg rd1 wreg rd2 addressing a
+ | Pldpx(rd1, rd2, _, _, a) ->
fprintf oc " ldp %a, %a, %a\n" xreg rd1 xreg rd2 addressing a
| Pstrw(rs, a) | Pstrw_a(rs, a) ->
fprintf oc " str %a, %a\n" wreg rs addressing a
@@ -396,7 +409,9 @@ module Target(System: SYSTEM): TARGET =
fprintf oc " strb %a, %a\n" wreg rs addressing a
| Pstrh(rs, a) ->
fprintf oc " strh %a, %a\n" wreg rs addressing a
- | Pstp(rs1, rs2, a) ->
+ | Pstpw(rs1, rs2, _, _, a) ->
+ fprintf oc " stp %a, %a, %a\n" wreg rs1 wreg rs2 addressing a
+ | Pstpx(rs1, rs2, _, _, a) ->
fprintf oc " stp %a, %a, %a\n" xreg rs1 xreg rs2 addressing a
(* Integer arithmetic, immediate *)
| Paddimm(sz, rd, r1, n) ->
@@ -520,12 +535,20 @@ module Target(System: SYSTEM): TARGET =
fprintf oc " str %a, %a\n" sreg rd addressing a
| Pstrd(rd, a) | Pstrd_a(rd, a) ->
fprintf oc " str %a, %a\n" dreg rd addressing a
+ | Pldps(rd1, rd2, _, _, a) ->
+ fprintf oc " ldp %a, %a, %a\n" sreg rd1 sreg rd2 addressing a
+ | Pldpd(rd1, rd2, _, _, a) ->
+ fprintf oc " ldp %a, %a, %a\n" dreg rd1 dreg rd2 addressing a
+ | Pstps(rd1, rd2, _, _, a) ->
+ fprintf oc " stp %a, %a, %a\n" sreg rd1 sreg rd2 addressing a
+ | Pstpd(rd1, rd2, _, _, a) ->
+ fprintf oc " stp %a, %a, %a\n" dreg rd1 dreg rd2 addressing a
(* Floating-point move *)
| Pfmov(rd, r1) ->
fprintf oc " fmov %a, %a\n" dreg rd dreg r1
| Pfmovimmd(rd, f) ->
let d = camlint64_of_coqint (Floats.Float.to_bits f) in
- if is_immediate_float64 d then
+ if is_immediate_float64 f then
fprintf oc " fmov %a, #%.7f\n" dreg rd (Int64.float_of_bits d)
else begin
let lbl = label_literal64 d in
@@ -534,7 +557,7 @@ module Target(System: SYSTEM): TARGET =
end
| Pfmovimms(rd, f) ->
let d = camlint_of_coqint (Floats.Float32.to_bits f) in
- if is_immediate_float32 d then
+ if is_immediate_float32 f then
fprintf oc " fmov %a, #%.7f\n" sreg rd (Int32.float_of_bits d)
else begin
let lbl = label_literal32 d in
@@ -596,8 +619,8 @@ module Target(System: SYSTEM): TARGET =
| Pfsel(rd, r1, r2, c) ->
fprintf oc " fcsel %a, %a, %a, %s\n" dreg rd dreg r1 dreg r2 (condition_name c)
(* No-op *)
- | Pnop ->
- fprintf oc " nop\n"
+ | Pnop -> ()
+ (*fprintf oc " nop\n"*)
(* Pseudo-instructions expanded in Asmexpand *)
| Pallocframe(sz, linkofs) -> assert false
| Pfreeframe(sz, linkofs) -> assert false
@@ -640,6 +663,8 @@ module Target(System: SYSTEM): TARGET =
fprintf oc "%s begin inline assembly\n\t" comment;
print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res;
fprintf oc "%s end inline assembly\n" comment
+ | EF_profiling (id, coq_kind) ->
+ print_profiling_logger oc id (Z.to_int coq_kind)
| _ ->
assert false
end
@@ -689,7 +714,24 @@ module Target(System: SYSTEM): TARGET =
section oc Section_text;
end
+ let aarch64_profiling_stub oc nr_items
+ profiling_id_table_name
+ profiling_counter_table_name =
+ fprintf oc " adrp x2, %s\n" profiling_counter_table_name;
+ fprintf oc " adrp x1, %s\n" profiling_id_table_name;
+ fprintf oc " add x2, x2, :lo12:%s\n" profiling_counter_table_name;
+ fprintf oc " add x1, x1, :lo12:%s\n" profiling_id_table_name;
+ fprintf oc " mov w0, %d\n" nr_items;
+ fprintf oc " b %s\n" profiling_write_table_helper ;;
+
+ let print_atexit oc to_be_called =
+ fprintf oc " adrp x0, %s\n" to_be_called;
+ fprintf oc " add x0, x0, :lo12:%s\n" to_be_called;
+ fprintf oc " b atexit\n";;
+
+
let print_epilogue oc =
+ print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) aarch64_profiling_stub oc;
if !Clflags.option_g then begin
Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
section oc Section_text;
generated by cgit (git 2.34.1) at 2024-06-02 23:24:10 +0000