From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 161 ++++++++++++++++++++++++++++++++------------------------ 1 file changed, 91 insertions(+), 70 deletions(-) (limited to 'arm/PrintAsm.ml') diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 5778286..1bac715 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -181,47 +181,11 @@ let emit_constants oc = symbol_labels; reset_constants () -(* Simulate instructions by calling helper functions *) - -let print_list_ireg oc l = - match l with - | [] -> assert false - | r1 :: rs -> ireg oc r1; List.iter (fun r -> fprintf oc ", %a" ireg r) rs - -let rec remove l r = - match l with - | [] -> [] - | hd :: tl -> if hd = r then remove tl r else hd :: remove tl r - -let call_helper oc fn dst arg1 arg2 = - (* Preserve caller-save registers r0...r3 except dst *) - let tosave = remove [IR0; IR1; IR2; IR3] dst in - fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave; - (* Copy arg1 to R0 and arg2 to R1 *) - let moves = - Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in - List.iter - (fun (s, d) -> - fprintf oc " mov %a, %a\n" ireg d ireg s) - moves; - (* Call the helper function *) - fprintf oc " bl %s\n" fn; - (* Move result to dst *) - begin match dst with - | IR0 -> () - | _ -> fprintf oc " mov %a, r0\n" ireg dst - end; - (* Restore the other caller-save registers *) - fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave; - (* ... for a total of at most 7 instructions *) - 7 - (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers the temporaries - (IR10, IR12, IR14, FP2, FP4) + registers; preserve all registers except IR2, IR3, IR12 and FP6. *) (* Handling of annotations *) @@ -234,9 +198,9 @@ let print_annot_val oc txt args res = fprintf oc "%s annotation: " comment; PrintAnnot.print_annot_val preg oc txt args; match args, res with - | IR src :: _, IR dst -> + | [IR src], [IR dst] -> if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1) - | FR src :: _, FR dst -> + | [FR src], [FR dst] -> if dst = src then 0 else (fprintf oc " fcpy %a, %a\n" freg dst freg src; 1) | _, _ -> assert false @@ -265,16 +229,12 @@ let print_builtin_memcpy_small oc sz al src dst = let print_builtin_memcpy_big oc sz al src dst = assert (sz >= al); assert (sz mod al = 0); + assert (src = IR2); + assert (dst = IR3); let (load, store, chunksize) = if al >= 4 then ("ldr", "str", 4) else if al = 2 then ("ldrh", "strh", 2) else ("ldrb", "strb", 1) in - let tmp = - if src <> IR0 && dst <> IR0 then IR0 - else if src <> IR1 && dst <> IR1 then IR1 - else IR2 in - let tosave = List.sort compare [tmp;src;dst] in - fprintf oc " stmfd sp!, {%a}\n" print_list_ireg tosave; begin match Asmgen.decompose_int (coqint_of_camlint (Int32.of_int (sz / chunksize))) with | [] -> assert false @@ -286,12 +246,11 @@ let print_builtin_memcpy_big oc sz al src dst = tl end; let lbl = new_label() in - fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg tmp ireg src chunksize; + fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize; fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14; - fprintf oc " %s %a, [%a], #%d\n" store ireg tmp ireg dst chunksize; + fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize; fprintf oc " bne .L%d\n" lbl; - fprintf oc " ldmfd sp!, {%a}\n" print_list_ireg tosave; - 9 + 8 let print_builtin_memcpy oc sz al args = let (dst, src) = @@ -308,20 +267,28 @@ let print_builtin_memcpy oc sz al args = let print_builtin_vload_common oc chunk args res = match chunk, args, res with - | Mint8unsigned, [IR addr], IR res -> + | Mint8unsigned, [IR addr], [IR res] -> fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint8signed, [IR addr], IR res -> + | Mint8signed, [IR addr], [IR res] -> fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16unsigned, [IR addr], IR res -> + | Mint16unsigned, [IR addr], [IR res] -> fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint16signed, [IR addr], IR res -> + | Mint16signed, [IR addr], [IR res] -> fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mint32, [IR addr], IR res -> + | Mint32, [IR addr], [IR res] -> fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 - | Mfloat32, [IR addr], FR res -> + | Mint64, [IR addr], [IR res1; IR res2] -> + if addr <> res2 then begin + fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr; + fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr + end else begin + fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr; + fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr + end; 2 + | Mfloat32, [IR addr], [FR res] -> fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr; fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2 - | (Mfloat64 | Mfloat64al32), [IR addr], FR res -> + | (Mfloat64 | Mfloat64al32), [IR addr], [FR res] -> fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1 | _ -> assert false @@ -346,6 +313,9 @@ let print_builtin_vstore_common oc chunk args = fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 | Mint32, [IR addr; IR src] -> fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | Mint64, [IR addr; IR src1; IR src2] -> + fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr; + fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2 | Mfloat32, [IR addr; FR src] -> fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src; fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2 @@ -386,22 +356,57 @@ let print_builtin_inline oc name args res = fprintf oc "%s begin %s\n" comment name; let n = match name, args, res with (* Integer arithmetic *) - | "__builtin_bswap", [IR a1], IR res -> + | "__builtin_bswap", [IR a1], [IR res] -> print_bswap oc a1 IR14 res; 4 - | "__builtin_cntlz", [IR a1], IR res -> + | "__builtin_cntlz", [IR a1], [IR res] -> fprintf oc " clz %a, %a\n" ireg res ireg a1; 1 (* Float arithmetic *) - | "__builtin_fabs", [FR a1], FR res -> + | "__builtin_fabs", [FR a1], [FR res] -> fprintf oc " fabsd %a, %a\n" freg res freg a1; 1 - | "__builtin_fsqrt", [FR a1], FR res -> + | "__builtin_fsqrt", [FR a1], [FR res] -> fprintf oc " fsqrtd %a, %a\n" freg res freg a1; 1 + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + if rl = ah then begin + fprintf oc " rsbs %a, %a, #0\n" ireg IR14 ireg al; + fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3 + end else begin + fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al; + fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2 + end + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + if rl = ah || rl = bh then begin + fprintf oc " adds %a, %a, %a\n" ireg IR14 ireg al ireg bl; + fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3 + end else begin + fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl; + fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2 + end + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + if rl = ah || rl = bh then begin + fprintf oc " subs %a, %a, %a\n" ireg IR14 ireg al ireg bl; + fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; + fprintf oc " mov %a, %a\n" ireg rl ireg IR14; 3 + end else begin + fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl; + fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2 + end + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + if rl = a || rh = a then begin + fprintf oc " mov %a, %a\n" ireg IR14 ireg a; + fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg IR14 ireg b; 2 + end else begin + fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1 + end (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], IR res -> + | "__builtin_read16_reversed", [IR a1], [IR res] -> fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1; fprintf oc " mov %a, %a, lsl #8\n" ireg IR14 ireg res; fprintf oc " and %a, %a, #0xFF00\n" ireg IR14 ireg IR14; fprintf oc " orr %a, %a, %a, lsr #8\n" ireg res ireg IR14 ireg res; 4 - | "__builtin_read32_reversed", [IR a1], IR res -> + | "__builtin_read32_reversed", [IR a1], [IR res] -> fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1; print_bswap oc res IR14 res; 5 | "__builtin_write16_reversed", [IR a1; IR a2], _ -> @@ -410,9 +415,19 @@ let print_builtin_inline oc name args res = fprintf oc " orr %a, %a, %a, lsl #8\n" ireg IR14 ireg IR14 ireg a2; fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 4 | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = IR10 then IR12 else IR10 in - print_bswap oc a2 IR14 tmp; - fprintf oc " str %a, [%a, #0]\n" ireg tmp ireg a1; 5 + if a1 <> IR12 then begin + print_bswap oc a2 IR14 IR12; + fprintf oc " str %a, [%a, #0]\n" ireg IR12 ireg a1; 5 + end else begin + fprintf oc " mov %a, %a, lsr #24\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; + fprintf oc " mov %a, %a, lsr #16\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #1]\n" ireg IR14 ireg a1; + fprintf oc " mov %a, %a, lsr #8\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #2]\n" ireg IR14 ireg a1; + fprintf oc " str %a, [%a, #3]\n" ireg IR14 ireg a1; + 7 + end (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -516,6 +531,8 @@ let print_instruction oc = function fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 | Pldrsh(r1, r2, sa) -> fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 + | Pmla(r1, r2, r3, r4) -> + fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1 | Pmov(r1, so) -> fprintf oc " mov %a, %a\n" ireg r1 shift_op so; 1 | Pmovc(bit, r1, so) -> @@ -535,11 +552,13 @@ let print_instruction oc = function | Pstrh(r1, r2, sa) -> fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1 | Psdiv(r1, r2, r3) -> - call_helper oc "__aeabi_idiv" r1 r2 r3 + assert (r1 = IR0 && r2 = IR0 && r3 = IR1); + fprintf oc " bl __aeabi_idiv\n"; 1 | Psub(r1, r2, so) -> fprintf oc " sub %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 | Pudiv(r1, r2, r3) -> - call_helper oc "__aeabi_uidiv" r1 r2 r3 + assert (r1 = IR0 && r2 = IR0 && r3 = IR1); + fprintf oc " bl __aeabi_uidiv\n"; 1 (* Floating-point coprocessor instructions *) | Pfcpyd(r1, r2) -> fprintf oc " fcpyd %a, %a\n" freg r1 freg r2; 1 @@ -593,14 +612,14 @@ let print_instruction oc = function fprintf oc " fsts %a, [%a, #%a]\n" freg_single FR6 ireg r2 coqint n; 2 (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> - fprintf oc " mov r10, sp\n"; + fprintf oc " mov r12, sp\n"; let ninstr = ref 0 in List.iter (fun n -> fprintf oc " sub sp, sp, #%a\n" coqint n; incr ninstr) (Asmgen.decompose_int sz); - fprintf oc " str r10, [sp, #%a]\n" coqint ofs; + fprintf oc " str r12, [sp, #%a]\n" coqint ofs; 2 + !ninstr | Pfreeframe(sz, ofs) -> if Asmgen.is_immed_arith sz @@ -620,7 +639,7 @@ let print_instruction oc = function List.iter (fun l -> fprintf oc " .word %a\n" print_label l) tbl; - 2 + List.length tbl + 3 + List.length tbl | Pbuiltin(ef, args, res) -> begin match ef with | EF_builtin(name, sg) -> @@ -713,6 +732,8 @@ let print_init oc = function fprintf oc " .short %ld\n" (camlint_of_coqint n) | Init_int32 n -> fprintf oc " .word %ld\n" (camlint_of_coqint n) + | Init_int64 n -> + fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) | Init_float32 n -> fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float.bits_of_single n)) comment (camlfloat_of_coqfloat n) -- cgit v1.2.3