diff options
| -rw-r--r-- | backend/PrintAsmaux.ml | 27 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 34 | ||||
| -rw-r--r-- | riscV/TargetPrinter.ml | 76 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml | 26 |
4 files changed, 71 insertions, 92 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 4099d76f..f7a30b22 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -69,15 +69,30 @@ let elf_label oc lbl = (* List of literals and jumptables used in the code *) -let float64_literals : (int * int64) list ref = ref [] -let float32_literals : (int * int32) list ref = ref [] -let int64_literals : (int * int64) list ref = ref [] let jumptables : (int * label list) list ref = ref [] + +let label_constant (h: ('a, int) Hashtbl.t) (cst: 'a) = + try + Hashtbl.find h cst + with Not_found -> + let lbl = new_label() in + Hashtbl.add h cst lbl; + lbl + +let literal32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) +let literal64_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) + +let label_literal32 bf = label_constant literal32_labels bf +let label_literal64 n = label_constant literal64_labels n + let reset_constants () = - float64_literals := []; - float32_literals := []; - jumptables := [] + jumptables := []; + Hashtbl.clear literal32_labels; + Hashtbl.clear literal64_labels + +let exists_constants () = + Hashtbl.length literal32_labels > 0 || Hashtbl.length literal64_labels > 0 (* Variables used for the handling of varargs *) diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 390fb385..17bd06b5 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -638,10 +638,10 @@ module Target (System : SYSTEM):TARGET = | Plhzx(r1, r2, r3) -> fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pldi(r1, c) -> - let lbl = new_label() in + let c = camlint64_of_coqint c in + let lbl = label_literal64 c in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " ld %a, %a(%a) %s %Ld\n" ireg r1 label_low lbl ireg GPR12 comment (camlint64_of_coqint c); - int64_literals := (lbl, camlint64_of_coqint c) :: !int64_literals; + fprintf oc " ld %a, %a(%a) %s %Ld\n" ireg r1 label_low lbl ireg GPR12 comment c | Plmake(_, _, _) -> assert false | Pllo _ -> @@ -649,15 +649,13 @@ module Target (System : SYSTEM):TARGET = | Plhi(_, _) -> assert false | Plfi(r1, c) -> - let lbl = new_label() in + let lbl = label_literal64 (camlint64_of_coqint (Floats.Float.to_bits c)) in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); - float64_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float64_literals; + fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c) | Plfis(r1, c) -> - let lbl = new_label() in + let lbl = label_literal32 (camlint_of_coqint (Floats.Float32.to_bits c)) in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c); - float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals; + fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c) | Plwarx(r1, r2, r3) -> fprintf oc " lwarx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Plwbrx(r1, r2, r3) -> @@ -904,12 +902,12 @@ module Target (System : SYSTEM):TARGET = (* Print the code for a function *) - let print_literal64 oc (lbl, n) = + let print_literal64 oc n lbl = let nlo = Int64.to_int32 n and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - let print_literal32 oc (lbl, n) = + let print_literal32 oc n lbl = fprintf oc "%a: .long 0x%lx\n" label lbl n let print_init oc = function @@ -945,17 +943,13 @@ module Target (System : SYSTEM):TARGET = let print_fun_info = elf_print_fun_info let emit_constants oc lit = - if !float64_literals <> [] || !float32_literals <> [] - || !int64_literals <> [] then begin + if exists_constants () then begin section oc lit; fprintf oc " .balign 8\n"; - List.iter (print_literal64 oc) !int64_literals; - int64_literals := []; - List.iter (print_literal64 oc) !float64_literals; - float64_literals := []; - List.iter (print_literal32 oc) !float32_literals; - float32_literals := [] - end + Hashtbl.iter (print_literal64 oc) literal64_labels; + Hashtbl.iter (print_literal32 oc) literal32_labels; + end; + reset_constants () let print_optional_fun_info _ = () diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 5c6edc46..4b976e17 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -129,51 +129,28 @@ module Target : TARGET = (* Associate labels to floating-point constants and to symbols. *) - let label_constant (h: ('a, int) Hashtbl.t) (cst: 'a) = - try - Hashtbl.find h cst - with Not_found -> - let lbl = new_label() in - Hashtbl.add h cst lbl; - lbl - - let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) - let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) - let int64_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) - - let label_float bf = label_constant float_labels bf - let label_float32 bf = label_constant float32_labels bf - let label_int64 n = label_constant int64_labels n - - let reset_constants () = - Hashtbl.clear float_labels; - Hashtbl.clear float32_labels; - Hashtbl.clear int64_labels - - let emit_constants oc = - if Hashtbl.length int64_labels > 0 then - begin - fprintf oc " .align 3\n"; - Hashtbl.iter - (fun bf lbl -> fprintf oc "%a: .quad 0x%Lx\n" label lbl bf) - int64_labels - end; - if Hashtbl.length float_labels > 0 then - begin - fprintf oc " .align 3\n"; - Hashtbl.iter - (fun bf lbl -> fprintf oc "%a: .quad 0x%Lx\n" label lbl bf) - float_labels - end; - if Hashtbl.length float32_labels > 0 then - begin - fprintf oc " .align 2\n"; - Hashtbl.iter - (fun bf lbl -> - fprintf oc "%a: .long 0x%lx\n" label lbl bf) - float32_labels - end; - reset_constants () + let reset_constants () = reset_constants () + + let emit_constants oc lit = + if exists_constants () then begin + section oc lit; + if Hashtbl.length literal64_labels > 0 then + begin + fprintf oc " .align 3\n"; + Hashtbl.iter + (fun bf lbl -> fprintf oc "%a: .quad 0x%Lx\n" label lbl bf) + literal64_labels + end; + if Hashtbl.length literal32_labels > 0 then + begin + fprintf oc " .align 2\n"; + Hashtbl.iter + (fun bf lbl -> + fprintf oc "%a: .long 0x%lx\n" label lbl bf) + literal32_labels + end; + reset_constants () + end (* Generate code to load the address of id + ofs in register r *) @@ -563,16 +540,16 @@ module Target : TARGET = fprintf oc " lui %a, %%hi(%a)\n" ireg rd symbol_offset (id, ofs) | Ploadli(rd, n) -> let d = camlint64_of_coqint n in - let lbl = label_int64 d in + let lbl = label_literal64 d in fprintf oc " ld %a, %a %s %Lx\n" ireg rd label lbl comment d | Ploadfi(rd, f) -> let d = camlint64_of_coqint(Floats.Float.to_bits f) in - let lbl = label_float d in + let lbl = label_literal64 d in fprintf oc " fld %a, %a, x31 %s %.18g\n" freg rd label lbl comment (camlfloat_of_coqfloat f) | Ploadsi(rd, f) -> let s = camlint_of_coqint(Floats.Float32.to_bits f) in - let lbl = label_float32 s in + let lbl = label_literal32 s in fprintf oc " flw %a, %a, x31 %s %.18g\n" freg rd label lbl comment (camlfloat_of_coqfloat32 f) | Pbtbl(r, tbl) -> @@ -654,9 +631,6 @@ module Target : TARGET = current_function_sig := fn.fn_sig; List.iter (print_instruction oc) fn.fn_code - let emit_constants oc lit = - section oc lit; - emit_constants oc (* Data *) diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index d0f8ef5a..52c2de49 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -378,8 +378,7 @@ module Target(System: SYSTEM):TARGET = fprintf oc "$%ld" n2 else begin (* put the constant in memory and use a PC-relative memory operand *) - let lbl = new_label() in - float64_literals := (lbl, n1) :: !float64_literals; + let lbl = label_literal64 n1 in fprintf oc "%a(%%rip)" label lbl end @@ -426,22 +425,20 @@ module Target(System: SYSTEM):TARGET = fprintf oc " movapd %a, %a\n" freg r1 freg rd | Pmovsd_fi(rd, n) -> let b = camlint64_of_coqint (Floats.Float.to_bits n) in - let lbl = new_label() in + let lbl = label_literal64 b in fprintf oc " movsd %a%s, %a %s %.18g\n" label lbl rip_rel - freg rd comment (camlfloat_of_coqfloat n); - float64_literals := (lbl, b) :: !float64_literals + freg rd comment (camlfloat_of_coqfloat n) | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> fprintf oc " movsd %a, %a\n" addressing a freg rd | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> fprintf oc " movsd %a, %a\n" freg r1 addressing a | Pmovss_fi(rd, n) -> let b = camlint_of_coqint (Floats.Float32.to_bits n) in - let lbl = new_label() in + let lbl = label_literal32 b in fprintf oc " movss %a%s, %a %s %.18g\n" label lbl rip_rel - freg rd comment (camlfloat_of_coqfloat32 n); - float32_literals := (lbl, b) :: !float32_literals + freg rd comment (camlfloat_of_coqfloat32 n) | Pmovss_fm(rd, a) -> fprintf oc " movss %a, %a\n" addressing a freg rd | Pmovss_mf(a, r1) -> @@ -820,9 +817,9 @@ module Target(System: SYSTEM):TARGET = assert false end - let print_literal64 oc (lbl, n) = + let print_literal64 oc n lbl = fprintf oc "%a: .quad 0x%Lx\n" label lbl n - let print_literal32 oc (lbl, n) = + let print_literal32 oc n lbl = fprintf oc "%a: .long 0x%lx\n" label lbl n let print_jumptable oc jmptbl = @@ -876,13 +873,12 @@ module Target(System: SYSTEM):TARGET = let name_of_section = name_of_section let emit_constants oc lit = - if !float64_literals <> [] || !float32_literals <> [] then begin + if exists_constants () then begin section oc lit; print_align oc 8; - List.iter (print_literal64 oc) !float64_literals; - float64_literals := []; - List.iter (print_literal32 oc) !float32_literals; - float32_literals := [] + Hashtbl.iter (print_literal64 oc) literal64_labels; + Hashtbl.iter (print_literal32 oc) literal32_labels; + reset_constants () end let cfi_startproc = cfi_startproc |