From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/PrintAsm.ml | 77 +++++++++++++++++++++++++++++++++-------------------- 1 file changed, 48 insertions(+), 29 deletions(-) (limited to 'powerpc/PrintAsm.ml') diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index b90b9f21..e3f07244 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -395,11 +395,11 @@ let print_builtin_vload_common oc chunk base offset res = fprintf oc " lhz %a, %a(%a)\n" ireg res constant offset ireg base | Mint16signed, IR res -> fprintf oc " lha %a, %a(%a)\n" ireg res constant offset ireg base - | Mint32, IR res -> + | (Mint32 | Many32), IR res -> fprintf oc " lwz %a, %a(%a)\n" ireg res constant offset ireg base | Mfloat32, FR res -> fprintf oc " lfs %a, %a(%a)\n" freg res constant offset ireg base - | Mfloat64, FR res -> + | (Mfloat64 | Many64), FR res -> fprintf oc " lfd %a, %a(%a)\n" freg res constant offset ireg base (* Mint64 is special-cased below *) | _ -> @@ -451,12 +451,11 @@ let print_builtin_vstore_common oc chunk base offset src = fprintf oc " stb %a, %a(%a)\n" ireg src constant offset ireg base | (Mint16signed | Mint16unsigned), IR src -> fprintf oc " sth %a, %a(%a)\n" ireg src constant offset ireg base - | Mint32, IR src -> + | (Mint32 | Many32), IR src -> fprintf oc " stw %a, %a(%a)\n" ireg src constant offset ireg base | Mfloat32, FR src -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg src; - fprintf oc " stfs %a, %a(%a)\n" freg FPR13 constant offset ireg base - | Mfloat64, FR src -> + fprintf oc " stfs %a, %a(%a)\n" freg src constant offset ireg base + | (Mfloat64 | Many64), FR src -> fprintf oc " stfd %a, %a(%a)\n" freg src constant offset ireg base (* Mint64 is special-cased below *) | _ -> @@ -512,11 +511,11 @@ let align n a = (n + a - 1) land (-a) let rec next_arg_locations ir fr ofs = function | [] -> (ir, fr, ofs) - | Tint :: l -> + | (Tint | Tany32) :: l -> if ir < 8 then next_arg_locations (ir + 1) fr ofs l else next_arg_locations ir fr (ofs + 4) l - | (Tfloat | Tsingle) :: l -> + | (Tfloat | Tsingle | Tany64) :: l -> if fr < 8 then next_arg_locations ir (fr + 1) ofs l else next_arg_locations ir fr (align ofs 8 + 8) l @@ -676,6 +675,7 @@ let short_cond_branch tbl pc lbl_dest = (* Printing of instructions *) let float_literals : (int * int64) list ref = ref [] +let float32_literals : (int * int32) list ref = ref [] let jumptables : (int * label list) list ref = ref [] let print_instruction oc tbl pc fallthrough = function @@ -804,10 +804,12 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " addi %a, %a, %ld\n" ireg GPR1 ireg GPR1 sz else fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1 - | Pfabs(r1, r2) -> + | Pfabs(r1, r2) | Pfabss(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 | Pfadd(r1, r2, r3) -> fprintf oc " fadd %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfadds(r1, r2, r3) -> + fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfcmpu(r1, r2) -> fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 | Pfcti(r1, r2) -> @@ -821,6 +823,8 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc "%s end pseudoinstr fcti\n" comment | Pfdiv(r1, r2, r3) -> fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfdivs(r1, r2, r3) -> + fprintf oc " fdivs %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfmake(rd, r1, r2) -> fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n" comment freg rd ireg r1 ireg r2; @@ -835,25 +839,37 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " fmr %a, %a\n" freg r1 freg r2 | Pfmul(r1, r2, r3) -> fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfneg(r1, r2) -> + | Pfmuls(r1, r2, r3) -> + fprintf oc " fmuls %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfneg(r1, r2) | Pfnegs(r1, r2) -> fprintf oc " fneg %a, %a\n" freg r1 freg r2 | Pfrsp(r1, r2) -> fprintf oc " frsp %a, %a\n" freg r1 freg r2 + | Pfxdp(r1, r2) -> + if r1 <> r2 then + fprintf oc " fmr %a, %a\n" freg r1 freg r2 | Pfsub(r1, r2, r3) -> fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfsubs(r1, r2, r3) -> + fprintf oc " fsubs %a, %a, %a\n" freg r1 freg r2 freg r3 | Plbz(r1, c, r2) -> fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plbzx(r1, r2, r3) -> fprintf oc " lbzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plfd(r1, c, r2) -> + | Plfd(r1, c, r2) | Plfd_a(r1, c, r2) -> fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Plfdx(r1, r2, r3) -> + | Plfdx(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Plfi(r1, c) -> let lbl = new_label() 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); - float_literals := (lbl, camlint64_of_coqint (Floats.Float.bits_of_double c)) :: !float_literals; + float_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float_literals; + | Plfis(r1, c) -> + let lbl = new_label() 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; | Plfs(r1, c, r2) -> fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 | Plfsx(r1, r2, r3) -> @@ -866,9 +882,9 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plhzx(r1, r2, r3) -> fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plwz(r1, c, r2) -> + | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) -> fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plwzx(r1, r2, r3) -> + | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pmfcrbit(r1, bit) -> fprintf oc " mfcr %a\n" ireg r1; @@ -924,23 +940,21 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2 | Pstbx(r1, r2, r3) -> fprintf oc " stbx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstfd(r1, c, r2) -> + | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) -> fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfdx(r1, r2, r3) -> + | Pstfdx(r1, r2, r3) | Pstfdx_a(r1, r2, r3) -> fprintf oc " stfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Pstfs(r1, c, r2) -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg r1; - fprintf oc " stfs %a, %a(%a)\n" freg FPR13 constant c ireg r2 + fprintf oc " stfs %a, %a(%a)\n" freg r1 constant c ireg r2 | Pstfsx(r1, r2, r3) -> - fprintf oc " frsp %a, %a\n" freg FPR13 freg r1; - fprintf oc " stfsx %a, %a, %a\n" freg FPR13 ireg r2 ireg r3 + fprintf oc " stfsx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Psth(r1, c, r2) -> fprintf oc " sth %a, %a(%a)\n" ireg r1 constant c ireg r2 | Psthx(r1, r2, r3) -> fprintf oc " sthx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstw(r1, c, r2) -> + | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) -> fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstwx(r1, r2, r3) -> + | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psubfc(r1, r2, r3) -> fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -1061,11 +1075,14 @@ let rec print_instructions oc tbl pc fallthrough = function (* Print the code for a function *) -let print_literal oc (lbl, n) = +let print_literal64 oc (lbl, n) = 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) = + fprintf oc "%a: .long 0x%lx\n" label lbl n + let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; List.iter @@ -1075,6 +1092,7 @@ let print_jumptable oc (lbl, tbl) = let print_function oc name fn = Hashtbl.clear current_function_labels; float_literals := []; + float32_literals := []; jumptables := []; current_function_sig := fn.fn_sig; let (text, lit, jmptbl) = @@ -1095,11 +1113,12 @@ let print_function oc name fn = cfi_endproc oc; fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name; - if !float_literals <> [] then begin + if !float_literals <> [] || !float32_literals <> [] then begin section oc lit; fprintf oc " .balign 8\n"; - List.iter (print_literal oc) !float_literals; - float_literals := [] + List.iter (print_literal64 oc) !float_literals; + List.iter (print_literal32 oc) !float32_literals; + float_literals := []; float32_literals := [] end; if !jumptables <> [] then begin section oc jmptbl; @@ -1131,10 +1150,10 @@ let print_init oc = function (Int64.logand b 0xFFFFFFFFL) | Init_float32 n -> fprintf oc " .long 0x%lx %s %.18g\n" - (camlint_of_coqint (Floats.Float.bits_of_single n)) + (camlint_of_coqint (Floats.Float32.to_bits n)) comment (camlfloat_of_coqfloat n) | Init_float64 n -> - let b = camlint64_of_coqint (Floats.Float.bits_of_double n) in + let b = camlint64_of_coqint (Floats.Float.to_bits n) in fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" (Int64.shift_right_logical b 32) (Int64.logand b 0xFFFFFFFFL) -- cgit