diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asm.v | 39 | ||||
-rw-r--r-- | arm/Asmexpand.ml | 332 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 321 |
3 files changed, 283 insertions, 409 deletions
@@ -148,7 +148,6 @@ Inductive instruction : Type := | Pmul: ireg -> ireg -> ireg -> instruction (**r integer multiplication *) | Pmvn: ireg -> shift_op -> instruction (**r integer complement *) | Porr: ireg -> ireg -> shift_op -> instruction (**r bitwise or *) - | Ppush: list ireg -> instruction (** push registers on the stack instruction *) | Prsb: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction *) | Psbfx: ireg -> ireg -> int -> int -> instruction (**r signed bitfield extract *) | Pstr: ireg -> ireg -> shift_op -> instruction (**r int32 store *) @@ -205,24 +204,7 @@ Inductive instruction : Type := | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *) - | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *) - | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) - | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) - | Pclz: preg -> preg -> instruction (**r count leading zeros. *) - | Pfsqrt: freg -> freg -> instruction (**r floating-point square root. *) - | Prev: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) - | Prev16: preg -> preg -> instruction (**r reverse bytes and reverse bits. *) - | Prsc: ireg -> ireg -> shift_op -> instruction (**r reverse subtract without carry. *) - | Psbc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) - (* Add, sub, rsb versions with s suffix *) - | Padds: ireg -> ireg -> shift_op -> instruction (**r integer addition with update of condition flags *) - | Psubs: ireg -> ireg -> shift_op -> instruction (**r integer subtraction with update of condition flags *) - | Prsbs: ireg -> ireg -> shift_op -> instruction (**r integer reverse subtraction with update of condition flags *) - | Pdmb: instruction (**r data memory barrier *) - | Pdsb: instruction (**r data synchronization barrier *) - | Pisb: instruction (**r instruction synchronization barrier *) - | Pbne: label -> instruction. (**r branch if negative macro *) - + | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *) (** The pseudo-instructions are the following: @@ -741,25 +723,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pbuiltin ef args res => Stuck (**r treated specially below *) | Pannot ef args => Stuck (**r treated specially below *) - (** The following instructions and directives are not generated directly by Asmgen, - so we do not model them. *) - | Ppush _ - | Padc _ _ _ - | Pcfi_adjust _ - | Pclz _ _ - | Prev _ _ - | Prev16 _ _ - | Pfsqrt _ _ - | Prsc _ _ _ - | Psbc _ _ _ - | Padds _ _ _ - | Psubs _ _ _ - | Prsbs _ _ _ - | Pdmb - | Pdsb - | Pisb - | Pbne _ => - Stuck end. (** Translation of the LTL/Linear/Mach view of machine registers diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 95f35f37..4baaac3d 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -11,334 +11,8 @@ (* *********************************************************************) (* Expanding built-ins and some pseudo-instructions by rewriting - of the ARM assembly code. Currently not everything done, this - expansion is performed on the fly in PrintAsm. *) + of the ARM assembly code. Currently not done, this expansion + is performed on the fly in PrintAsm. *) -open Asm -open Asmexpandaux -open Asmgen -open AST -open Camlcoq -open Integers +let expand_program p = p -(* Useful constants and helper functions *) - -let _0 = Integers.Int.zero -let _1 = Integers.Int.one -let _2 = coqint_of_camlint 2l -let _4 = coqint_of_camlint 4l -let _8 = coqint_of_camlint 8l -let _16 = coqint_of_camlint 16l - -(* Emit instruction sequences that set or offset a register by a constant. *) -(* No S suffix because they are applied to SP most of the time. *) - -let expand_movimm dst n = - match Asmgen.decompose_int n with - | [] -> assert false - | hd::tl-> - emit (Pmov (dst,SOimm hd)); - List.iter - (fun n -> emit (Porr (dst,dst, SOimm n))) tl - -let expand_subimm dst src n = - match Asmgen.decompose_int n with - | [] -> assert false - | hd::tl -> - emit (Psub(dst,src,SOimm hd)); - List.iter (fun n -> emit (Psub (dst,dst,SOimm n))) tl - -let expand_addimm dst src n = - match Asmgen.decompose_int n with - | [] -> assert false - | hd::tl -> - emit (Padd (dst,src,SOimm hd)); - List.iter (fun n -> emit (Padd (dst,dst,SOimm n))) tl - -let expand_int64_arith conflict rl fn = - if conflict then - begin - fn IR14; - emit (Pmov (rl,SOreg IR14)) - end else - fn rl - - -(* 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. -*) - -(* Handling of annotations *) - -let expand_annot_val txt targ args res = - emit (Pannot (EF_annot(txt,[targ]), List.map (fun r -> AA_base r) args)); - match args, res with - | [IR src], [IR dst] -> - if dst <> src then emit (Pmov (dst,SOreg src)) - | [FR src], [FR dst] -> - if dst <> src then emit (Pfcpyd (dst,src)) - | _, _ -> assert false - - -(* Handling of memcpy *) - -(* The ARM has strict alignment constraints for 2 and 4 byte accesses. - 8-byte accesses must be 4-aligned. *) - -let expand_builtin_memcpy_small sz al src dst = - let rec copy ofs sz = - if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin - emit (Pfldd (FR7,src,ofs)); - emit (Pfstd (FR7,dst,ofs)); - copy (Int.add ofs _8) (sz - 8) - end else if sz >= 4 && al >= 4 then begin - emit (Pldr (IR14,src,SOimm ofs)); - emit (Pstr (IR14,dst,SOimm ofs)); - copy (Int.add ofs _4) (sz - 4) - end else if sz >= 2 && al >= 2 then begin - emit (Pldrh (IR14,src,SOimm ofs)); - emit (Pstrh (IR14,dst,SOimm ofs)); - copy (Int.add ofs _2) (sz - 2) - end else if sz >= 1 then begin - emit (Pldrb (IR14,src,SOimm ofs)); - emit (Pstrb (IR14,dst,SOimm ofs)); - copy (Int.add ofs _1) (sz - 1) - end else - () in - copy _0 sz - -let expand_builtin_memcpy_big 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 (Pldr (IR12,src,SOimm _4), Pstr (IR12,dst,SOimm _4) , 4) - else if al = 2 then (Pldrh (IR12,src,SOimm _2), Pstrh (IR12,dst,SOimm _2), 2) - else (Pldrb (IR12,src,SOimm _1), Pstrb (IR12,dst,SOimm _1), 1) in - expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize))); - let lbl = new_label () in - emit (Plabel lbl); - emit load; - emit (Psubs (IR14,IR14,SOimm _1)); - emit store; - emit (Pbne lbl) - -let expand_builtin_memcpy sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in - if sz <= 32 - then expand_builtin_memcpy_small sz al src dst - else expand_builtin_memcpy_big sz al src dst - -(* Handling of volatile reads and writes *) - -let expand_builtin_vload_common chunk args res = - match chunk, args, res with - | Mint8unsigned, [IR addr], [IR res] -> - emit (Pldrb (res, addr,SOimm _0)) - | Mint8signed, [IR addr], [IR res] -> - emit (Pldrsb (res, addr,SOimm _0)) - | Mint16unsigned, [IR addr], [IR res] -> - emit (Pldrh (res, addr, SOimm _0)) - | Mint16signed, [IR addr], [IR res] -> - emit (Pldrsh (res, addr, SOimm _0)) - | Mint32, [IR addr], [IR res] -> - emit (Pldr (res,addr, SOimm _0)) - | Mint64, [IR addr], [IR res1; IR res2] -> - if addr <> res2 then begin - emit (Pldr (res2, addr, SOimm _0)); - emit (Pldr (res1, addr, SOimm _4)) - end else begin - emit (Pldr (res1,addr, SOimm _4)); - emit (Pldr (res2,addr, SOimm _0)) - end - | Mfloat32, [IR addr], [FR res] -> - emit (Pflds (res, addr, _0)) - | Mfloat64, [IR addr], [FR res] -> - emit (Pfldd (res,addr, _0)) - | _ -> - assert false - -let expand_builtin_vload chunk args res = - expand_builtin_vload_common chunk args res - -let expand_builtin_vload_global chunk id ofs args res = - emit (Ploadsymbol (IR14,id,ofs)); - expand_builtin_vload_common chunk args res - -let expand_builtin_vstore_common chunk args = - match chunk, args with - | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> - emit (Pstrb (src,addr, SOimm _0)) - | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> - emit (Pstrh (src,addr, SOimm _0)) - | Mint32, [IR addr; IR src] -> - emit (Pstr (src,addr, SOimm _0)) - | Mint64, [IR addr; IR src1; IR src2] -> - emit (Pstr (src2,addr,SOimm _0)); - emit (Pstr (src1,addr,SOimm _0)) - | Mfloat32, [IR addr; FR src] -> - emit (Pfstd (src,addr,_0)) - | Mfloat64, [IR addr; FR src] -> - emit (Pfsts (src,addr,_0)); - | _ -> - assert false - -let expand_builtin_vstore chunk args = - expand_builtin_vstore_common chunk args - -let expand_builtin_vstore_global chunk id ofs args = - emit (Ploadsymbol (IR14,id,ofs)); - expand_builtin_vstore_common chunk args - -(* Handling of varargs *) - -let align n a = (n + a - 1) land (-a) - -let rec next_arg_location ir ofs = function - | [] -> - Int32.of_int (ir * 4 + ofs) - | (Tint | Tsingle | Tany32) :: l -> - if ir < 4 - then next_arg_location (ir + 1) ofs l - else next_arg_location ir (ofs + 4) l - | (Tfloat | Tlong | Tany64) :: l -> - if ir < 3 - then next_arg_location (align ir 2 + 2) ofs l - else next_arg_location ir (align ofs 8 + 8) l - -let expand_builtin_va_start r = - if not !current_function.fn_sig.sig_cc.cc_vararg then - invalid_arg "Fatal error: va_start used in non-vararg function"; - let ofs = - Int32.add - (next_arg_location 0 0 !current_function.fn_sig.sig_args) - !PrintAsmaux.current_function_stacksize in - expand_addimm IR14 IR13 (coqint_of_camlint ofs); - emit (Pstr (IR14,r,SOimm _0)) - - -(* Handling of compiler-inlined builtins *) -let expand_builtin_inline name args res = - match name, args, res with - (* Integer arithmetic *) - | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> - emit (Prev (IR res,IR a1)) - | "__builtin_bswap16", [IR a1], [IR res] -> - emit (Prev16 (IR res,IR a1)) - | "__builtin_clz", [IR a1], [IR res] -> - emit (Pclz (IR res, IR a1)) - (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> - emit (Pfabsd (res,a1)) - | "__builtin_fsqrt", [FR a1], [FR res] -> - emit (Pfsqrt (res,a1)) - (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] -> - emit (Prsbs (rl,al,SOimm _0)); - if !Clflags.option_mthumb then begin - emit (Pmvn (rh,SOreg ah)); - emit (Padc (rh,rh,SOimm _0)) - end else - begin - emit (Prsc (rh,ah,SOimm _0)) - end - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - expand_int64_arith (rl = ah || rl = bh) rl - (fun rl -> - emit (Padds (rl,al,SOreg bl)); - emit (Padc (rh,ah,SOreg bh))) - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - expand_int64_arith (rl = ah || rl = bh) rl - (fun rl -> - emit (Psubs (rl,al,SOreg bl)); - emit (Psbc (rh,ah,SOreg bh))) - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - emit (Pumull (rl,rh,a,b)) - (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> - emit (Pldrh (res,a1,SOimm _0)); - emit (Prev16 (IR res,IR res)); - | "__builtin_read32_reversed", [IR a1], [IR res] -> - emit (Pldr (res,a1,SOimm _0)); - emit (Prev (IR res,IR res)); - | "__builtin_write16_reverse", [IR a1; IR a2], _ -> - emit (Prev16 (IR IR14, IR a2)); - emit (Pstrh (IR14, a1, SOimm _0)) - | "__builtin_write32_reverse", [IR a1; IR a2], _ -> - emit (Prev (IR IR14, IR a2)); - emit (Pstr (IR14, a1, SOimm _0)) - (* Synchronization *) - | "__builtin_membar",[], _ -> - () - | "__builtin_dmb", [], _ -> - emit Pdmb - | "__builtin_dsb", [], _ -> - emit Pdsb - | "__builtin_isb", [], _ -> - emit Pisb - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - expand_builtin_va_start a - (* Catch-all *) - | _ -> - invalid_arg ("unrecognized builtin " ^ name) - -let expand_instruction instr = - match instr with - | Pallocframe (sz, ofs) -> - emit (Pmov (IR12,SOreg IR13)); - if (!current_function).fn_sig.sig_cc.cc_vararg then begin - emit (Ppush [IR0;IR1;IR2;IR3]); - emit (Pcfi_adjust _16); - end; - expand_subimm IR13 IR13 sz; - emit (Pcfi_adjust sz); - emit (Pstr (IR12,IR13,SOimm ofs)) - | Pfreeframe (sz, ofs) -> - let sz = - if (!current_function).fn_sig.sig_cc.cc_vararg - then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)) - else sz in - if Asmgen.is_immed_arith sz - then emit (Padd (IR13,IR13,SOimm sz)) - else emit (Pldr (IR13,IR13,SOimm sz)) - | Pbuiltin (ef,args,res) -> - begin match ef with - | EF_builtin (name,sg) -> - expand_builtin_inline (extern_atom name) args res - | EF_vload chunk -> - expand_builtin_vload chunk args res - | EF_vstore chunk -> - expand_builtin_vstore chunk args - | EF_vload_global(chunk, id, ofs) -> - expand_builtin_vload_global chunk id ofs args res - | EF_vstore_global(chunk, id, ofs) -> - expand_builtin_vstore_global chunk id ofs args - | EF_annot_val (txt,targ) -> - expand_annot_val txt targ args res - | EF_memcpy(sz, al) -> - expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) - (Int32.to_int (camlint_of_coqint al)) args - | EF_inline_asm(txt, sg, clob) -> - emit instr - | _ -> assert false - end - | _ -> - emit instr - -let expand_function fn = - set_current_function fn; - List.iter expand_instruction fn.fn_code; - get_current_function () - -let expand_fundef = function - | Internal f -> Internal (expand_function f) - | External ef -> External ef - -let expand_program (p: Asm.program) : Asm.program = - AST.transform_program expand_fundef p diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 88261940..505c3265 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -304,6 +304,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) + +(* 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. +*) (* Handling of annotations *) @@ -315,6 +322,167 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc "%s annotation: " comment; print_annot_stmt preg "sp" oc txt targs args end + + let print_annot_val oc txt args res = + fprintf oc "%s annotation: " comment; + print_annot_val preg oc txt args; + match args, res with + | [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] -> + if dst = src then 0 else (fprintf oc " vmov.f64 %a, %a\n" freg dst freg src; 1) + | _, _ -> assert false + +(* Handling of memcpy *) + +(* The ARM has strict alignment constraints for 2 and 4 byte accesses. + 8-byte accesses must be 4-aligned. *) + + let print_builtin_memcpy_small oc sz al src dst = + let rec copy ofs sz ninstr = + if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin + fprintf oc " vldr %a, [%a, #%d]\n" freg FR7 ireg src ofs; + fprintf oc " vstr %a, [%a, #%d]\n" freg FR7 ireg dst ofs; + copy (ofs + 8) (sz - 8) (ninstr + 2) + end else if sz >= 4 && al >= 4 then begin + fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs; + fprintf oc " str %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; + copy (ofs + 4) (sz - 4) (ninstr + 2) + end else if sz >= 2 && al >= 2 then begin + fprintf oc " ldrh %a, [%a, #%d]\n" ireg IR14 ireg src ofs; + fprintf oc " strh %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; + copy (ofs + 2) (sz - 2) (ninstr + 2) + end else if sz >= 1 then begin + fprintf oc " ldrb %a, [%a, #%d]\n" ireg IR14 ireg src ofs; + fprintf oc " strb %a, [%a, #%d]\n" ireg IR14 ireg dst ofs; + copy (ofs + 1) (sz - 1) (ninstr + 2) + end else + ninstr in + copy 0 sz 0 + + 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 n = movimm oc "r14" (coqint_of_camlint (Int32.of_int (sz / chunksize))) in + let lbl = new_label() in + 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 IR12 ireg dst chunksize; + fprintf oc " bne .L%d\n" lbl; + n + 4 + + let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" + comment sz al; + let n = + if sz <= 32 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst in + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n + +(* Handling of volatile reads and writes *) + + let print_builtin_vload_common oc chunk args res = + match chunk, args, res with + | Mint8unsigned, [IR addr], [IR res] -> + fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint8signed, [IR addr], [IR res] -> + fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16unsigned, [IR addr], [IR res] -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint16signed, [IR addr], [IR res] -> + fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 + | Mint32, [IR addr], [IR res] -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 + | 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 " vldr %a, [%a, #0]\n" freg_single res ireg addr; 1 + | Mfloat64, [IR addr], [FR res] -> + fprintf oc " vldr %a, [%a, #0]\n" freg res ireg addr; 1 + | _ -> + assert false + + let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + let n = print_builtin_vload_common oc chunk args res in + fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n + + let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + let n1 = loadsymbol oc IR14 id ofs in + let n2 = print_builtin_vload_common oc chunk [IR IR14] res in + fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n1 + n2 + + let print_builtin_vstore_common oc chunk args = + match chunk, args with + | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> + fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> + 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 " vstr %a, [%a, #0]\n" freg_single src ireg addr; 1 + | Mfloat64, [IR addr; FR src] -> + fprintf oc " vstr %a, [%a, #0]\n" freg src ireg addr; 1 + | _ -> + assert false + + let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + let n = print_builtin_vstore_common oc chunk args in + fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + + let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + let n1 = loadsymbol oc IR14 id ofs in + let n2 = print_builtin_vstore_common oc chunk (IR IR14 :: args) in + fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n1 + n2 + +(* Handling of varargs *) + + let align n a = (n + a - 1) land (-a) + + let rec next_arg_location ir ofs = function + | [] -> + Int32.of_int (ir * 4 + ofs) + | (Tint | Tsingle | Tany32) :: l -> + if ir < 4 + then next_arg_location (ir + 1) ofs l + else next_arg_location ir (ofs + 4) l + | (Tfloat | Tlong | Tany64) :: l -> + if ir < 3 + then next_arg_location (align ir 2 + 2) ofs l + else next_arg_location ir (align ofs 8 + 8) l + + let print_builtin_va_start oc r = + if not (!current_function_sig).sig_cc.cc_vararg then + invalid_arg "Fatal error: va_start used in non-vararg function"; + let ofs = + Int32.add + (next_arg_location 0 0 (!current_function_sig).sig_args) + !current_function_stacksize in + let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in + fprintf oc " str r14, [%a, #0]\n" ireg r; + n + 1 (* Auxiliary for 64-bit integer arithmetic built-ins. They expand to two instructions, one computing the low 32 bits of the result, @@ -331,6 +499,79 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end else fn rl +(* Handling of compiler-inlined builtins *) + + 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" | "__builtin_bswap32"), [IR a1], [IR res] -> + fprintf oc " rev %a, %a\n" ireg res ireg a1; 1 + | "__builtin_bswap16", [IR a1], [IR res] -> + fprintf oc " rev16 %a, %a\n" ireg res ireg a1; 1 + | "__builtin_clz", [IR a1], [IR res] -> + fprintf oc " clz %a, %a\n" ireg res ireg a1; 1 + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], [FR res] -> + fprintf oc " vabs.f64 %a, %a\n" freg res freg a1; 1 + | "__builtin_fsqrt", [FR a1], [FR res] -> + fprintf oc " vsqrt.f64 %a, %a\n" freg res freg a1; 1 + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + print_int64_arith oc (rl = ah) rl (fun rl -> + fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al; + (* No "rsc" instruction in Thumb2. Emulate based on + rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry) + == mvn a, b; adc a, a, #0 *) + if !Clflags.option_mthumb then begin + fprintf oc " mvn %a, %a\n" ireg rh ireg ah; + fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3 + end else begin + 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] -> + print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> + 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) + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + print_int64_arith oc (rl = ah || rl = bh) rl (fun rl -> + 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) + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1 + (* Memory accesses *) + | "__builtin_read16_reversed", [IR a1], [IR res] -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1; + fprintf oc " rev16 %a, %a\n" ireg res ireg res; 2 + | "__builtin_read32_reversed", [IR a1], [IR res] -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1; + fprintf oc " rev %a, %a\n" ireg res ireg res; 2 + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + fprintf oc " rev16 %a, %a\n" ireg IR14 ireg a2; + fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 2 + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + fprintf oc " rev %a, %a\n" ireg IR14 ireg a2; + fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2 + (* Synchronization *) + | "__builtin_membar", [], _ -> + 0 + | "__builtin_dmb", [], _ -> + fprintf oc " dmb\n"; 1 + | "__builtin_dsb", [], _ -> + fprintf oc " dsb\n"; 1 + | "__builtin_isb", [], _ -> + fprintf oc " isb\n"; 1 + + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + in + fprintf oc "%s end %s\n" comment name; + n + (* Fixing up calling conventions *) type direction = Incoming | Outgoing @@ -475,15 +716,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n let print_instruction oc = function - (* Core instructions *) - | Padc (r1,r2,so) -> - fprintf oc " adc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 + (* Core instructions *) | Padd(r1, r2, so) -> fprintf oc " add%s %a, %a, %a\n" (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "") ireg r1 ireg r2 shift_op so; 1 - | Padds (r1,r2,so) -> - fprintf oc " adds %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 | Pand(r1, r2, so) -> fprintf oc " and%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 @@ -494,8 +731,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " b %a\n" print_label lbl; 1 | Pbc(bit, lbl) -> fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 - | Pbne lbl -> - fprintf oc " bne %a\n" print_label lbl; 1 | Pbsymb(id, sg) -> let n = fixup_arguments oc Outgoing sg in fprintf oc " b %a\n" symbol id; @@ -520,19 +755,11 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Pbic(r1, r2, so) -> fprintf oc " bic%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 - | Pclz (r1,r2) -> - fprintf oc " clz %a, %a\n" preg r1 preg r2; 1 | Pcmp(r1, so) -> fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1 - | Pdmb -> - fprintf oc " dmb\n"; 1 - | Pdsb -> - fprintf oc " dsb\n"; 1 - | Peor(r1, r2, so) -> + | Peor(r1, r2, so) -> fprintf oc " eor%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 - | Pisb -> - fprintf oc " isb\n"; 1 | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) -> fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1 | Pldrb(r1, r2, sa) -> @@ -564,22 +791,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Porr(r1, r2, so) -> fprintf oc " orr%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 - | Prev (r1,r2) -> - fprintf oc " rev %a, %a\n" preg r1 preg r2; 1 - | Prev16 (r1,r2) -> - fprintf oc " rev16 %a, %a\n" preg r1 preg r2; 1 | Prsb(r1, r2, so) -> - fprintf oc " rsb%t %a, %a, %a\n" - thumbS ireg r1 ireg r2 shift_op so; 1 - | Prsbs(r1, r2, so) -> - fprintf oc " rsbs %a, %a, %a\n" - ireg r1 ireg r2 shift_op so; 1 - | Prsc (r1,r2,so) -> - fprintf oc " rsc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 - | Pfsqrt (f1,f2) -> - fprintf oc " vsqrt.f64 %a, %a\n" freg f1 freg f2; 1 - | Psbc (r1,r2,sa) -> - fprintf oc " sbc %a, %a, %a\n" ireg r1 ireg r2 shift_op sa; 1 + fprintf oc " rsb%t %a, %a, %a\n" + thumbS ireg r1 ireg r2 shift_op so; 1 | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; begin match r1, r2, sa with @@ -604,9 +818,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Psub(r1, r2, so) -> fprintf oc " sub%t %a, %a, %a\n" thumbS ireg r1 ireg r2 shift_op so; 1 - | Psubs(r1, r2, so) -> - fprintf oc " subs %a, %a, %a\n" - ireg r1 ireg r2 shift_op so; 1 | Pudiv -> if Opt.hardware_idiv then begin fprintf oc " udiv r0, r0, r1\n"; 1 @@ -675,11 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Pfdivs(r1, r2, r3) -> fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 | Pfmuls(r1, r2, r3) -> - fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 - | Ppush rl -> - let first = ref true in - let sep () = if !first then first := false else output_string oc ", " in - fprintf oc " push {%a}\n" (fun oc rl -> List.iter (fun ir -> sep (); ireg oc ir) rl) rl; ;1 + fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 | Pfsubs(r1, r2, r3) -> fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1 | Pflis(r1, f) -> @@ -731,9 +938,25 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1 (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> - assert false + fprintf oc " mov r12, sp\n"; + if (!current_function_sig).sig_cc.cc_vararg then begin + fprintf oc " push {r0, r1, r2, r3}\n"; + cfi_adjust oc 16l + end; + let sz' = camlint_of_coqint sz in + let ninstr = subimm oc "sp" "sp" sz in + cfi_adjust oc sz'; + fprintf oc " str r12, [sp, #%a]\n" coqint ofs; + current_function_stacksize := sz'; + ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2) | Pfreeframe(sz, ofs) -> - assert false + let sz = + if (!current_function_sig).sig_cc.cc_vararg + then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)) + else sz in + if Asmgen.is_immed_arith sz + then fprintf oc " add sp, sp, #%a\n" coqint sz + else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 | Plabel lbl -> fprintf oc "%a:\n" print_label lbl; 0 | Ploadsymbol(r1, id, ofs) -> @@ -765,6 +988,21 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | Pbuiltin(ef, args, res) -> begin match ef with + | EF_builtin(name, sg) -> + print_builtin_inline oc (extern_atom name) args res + | EF_vload chunk -> + print_builtin_vload oc chunk args res + | EF_vstore chunk -> + print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args + | EF_memcpy(sz, al) -> + print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) + (Int32.to_int (camlint_of_coqint al)) args + | EF_annot_val(txt, targ) -> + print_annot_val oc (extern_atom txt) args res | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; @@ -780,7 +1018,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | _ -> assert false end - | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0 let no_fallthrough = function | Pb _ -> true |