From 929c0ea6f02713f59c0862fa0c3a53e0cb89c334 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 10 Jun 2015 10:07:02 +0200 Subject: Moved the printing of the builtin functions etc. into Asmexpand for ARM in the same way as it is done for PPC. --- arm/Asm.v | 39 +++++- arm/Asmexpand.ml | 330 +++++++++++++++++++++++++++++++++++++++++++++++- arm/TargetPrinter.ml | 321 ++++++---------------------------------------- backend/Asmexpandaux.ml | 57 +++++++++ powerpc/Asmexpand.ml | 55 ++------ 5 files changed, 475 insertions(+), 327 deletions(-) create mode 100644 backend/Asmexpandaux.ml diff --git a/arm/Asm.v b/arm/Asm.v index 2a120dd4..dd434c02 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -148,6 +148,7 @@ 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 *) @@ -204,7 +205,24 @@ 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 *) + | 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 *) + (** The pseudo-instructions are the following: @@ -723,6 +741,25 @@ 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 4baaac3d..36db5f9e 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -11,8 +11,332 @@ (* *********************************************************************) (* Expanding built-ins and some pseudo-instructions by rewriting - of the ARM assembly code. Currently not done, this expansion - is performed on the fly in PrintAsm. *) + of the ARM assembly code. Currently not everything done, this + expansion is performed on the fly in PrintAsm. *) -let expand_program p = p +open Asm +open Asmexpandaux +open Asmgen +open AST +open Camlcoq +open Integers +(* 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 + | _ -> () + 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 505c3265..88261940 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -304,13 +304,6 @@ 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 *) @@ -322,167 +315,6 @@ 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, @@ -499,79 +331,6 @@ 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 @@ -716,11 +475,15 @@ 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 *) + (* Core instructions *) + | Padc (r1,r2,so) -> + fprintf oc " adc %a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1 | 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 @@ -731,6 +494,8 @@ 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; @@ -755,11 +520,19 @@ 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 - | Peor(r1, r2, so) -> + | Pdmb -> + fprintf oc " dmb\n"; 1 + | Pdsb -> + fprintf oc " dsb\n"; 1 + | 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) -> @@ -791,9 +564,22 @@ 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 + 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 | 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 @@ -818,6 +604,9 @@ 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 @@ -886,7 +675,11 @@ 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 + 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 | 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) -> @@ -938,25 +731,9 @@ 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) -> - 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) + assert false | Pfreeframe(sz, ofs) -> - 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 + assert false | Plabel lbl -> fprintf oc "%a:\n" print_label lbl; 0 | Ploadsymbol(r1, id, ofs) -> @@ -988,21 +765,6 @@ 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; @@ -1018,6 +780,7 @@ 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 diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml new file mode 100644 index 00000000..6ce6c005 --- /dev/null +++ b/backend/Asmexpandaux.ml @@ -0,0 +1,57 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Util functions used for the expansion of built-ins and some + pseudo-instructions *) + +open Asm +open AST +open Camlcoq + +(* Buffering the expanded code *) + +let current_code = ref ([]: instruction list) + +let emit i = current_code := i :: !current_code + +(* Generation of fresh labels *) + +let dummy_function = { fn_code = []; fn_sig = signature_main } +let current_function = ref dummy_function +let next_label = ref (None: label option) + +let new_label () = + let lbl = + match !next_label with + | Some l -> l + | None -> + (* on-demand computation of the next available label *) + List.fold_left + (fun next instr -> + match instr with + | Plabel l -> if P.lt l next then next else P.succ l + | _ -> next) + P.one (!current_function).fn_code + in + next_label := Some (P.succ lbl); + lbl + + +let set_current_function f = + current_function := f; next_label := None; current_code := [] + +let get_current_function () = + let c = List.rev !current_code in + let fn = !current_function in + set_current_function dummy_function; + {fn with fn_code = c} diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index aec8f66e..7f413661 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -19,48 +19,10 @@ open Integers open AST open Memdata open Asm +open Asmexpandaux -(* Buffering the expanded code *) -let current_code = ref ([]: instruction list) - -let emit i = current_code := i :: !current_code - -let emit_loadimm r n = - List.iter emit (Asmgen.loadimm r n []) - -let emit_addimm rd rs n = - List.iter emit (Asmgen.addimm rd rs n []) - -let get_code () = - let c = List.rev !current_code in current_code := []; c - -(* Generation of fresh labels *) - -let dummy_function = { fn_code = []; fn_sig = signature_main } -let current_function = ref dummy_function -let next_label = ref (None : label option) - -let new_label () = - let lbl = - match !next_label with - | Some l -> l - | None -> - (* on-demand computation of the next available label *) - List.fold_left - (fun next instr -> - match instr with - | Plabel l -> if P.lt l next then next else P.succ l - | _ -> next) - P.one (!current_function).fn_code - in - next_label := Some (P.succ lbl); - lbl - -let set_current_function f = - current_function := f; next_label := None - -(* Useful constants *) +(* Useful constants and helper functions *) let _0 = Integers.Int.zero let _1 = Integers.Int.one @@ -71,6 +33,14 @@ let _8 = coqint_of_camlint 8l let _m4 = coqint_of_camlint (-4l) let _m8 = coqint_of_camlint (-8l) +let emit_loadimm r n = + List.iter emit (Asmgen.loadimm r n []) + +let emit_addimm rd rs n = + List.iter emit (Asmgen.addimm rd rs n []) + + + (* Handling of annotations *) let expand_annot_val txt targ args res = @@ -533,11 +503,8 @@ let expand_instruction instr = let expand_function fn = set_current_function fn; - current_code := []; List.iter expand_instruction fn.fn_code; - let c = get_code() in - set_current_function dummy_function; - { fn with fn_code = c } + get_current_function () let expand_fundef = function | Internal f -> Internal (expand_function f) -- cgit From 0dda7b5a8c634b74af5e530e2cd31733ed9ba751 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 18 Jun 2015 18:35:59 +0200 Subject: Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32. --- ia32/Asm.v | 52 ++++++++++++++++- ia32/Asmexpand.ml | 157 ++++++++++++++++++++++++++++++++++++++++++++++++++ ia32/TargetPrinter.ml | 46 +++++++++++++++ 3 files changed, 253 insertions(+), 2 deletions(-) diff --git a/ia32/Asm.v b/ia32/Asm.v index b67c3cc5..d136bf9b 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -212,7 +212,30 @@ Inductive instruction: Type := | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) | Pbuiltin(ef: external_function)(args: list preg)(res: list preg) - | Pannot(ef: external_function)(args: list (annot_arg preg)). + | Pannot(ef: external_function)(args: list (annot_arg preg)) + | Padcl_ir (n: int) (r: ireg) + | Padcl_rr (r1: ireg) (r2: ireg) + | Paddl (r1: ireg) (r2: ireg) + | Pbsfl (r1: ireg) (r2: ireg) + | Pbslr (r1: ireg) (r2: ireg) + | Pbswap (r: ireg) + | Pfmadd132 (r1: freg) (r2: freg) (r3: freg) + | Pfmadd213 (r1: freg) (r2: freg) (r3: freg) + | Pfmadd231 (r1: freg) (r2: freg) (r3: freg) + | Pfmsub132 (r1: freg) (r2: freg) (r3: freg) + | Pfmsub213 (r1: freg) (r2: freg) (r3: freg) + | Pfmsub231 (r1: freg) (r2: freg) (r3: freg) + | Pfnmadd132 (r1: freg) (r2: freg) (r3: freg) + | Pfnmadd213 (r1: freg) (r2: freg) (r3: freg) + | Pfnmadd231 (r1: freg) (r2: freg) (r3: freg) + | Pfnmsub132 (r1: freg) (r2: freg) (r3: freg) + | Pfnmsub213 (r1: freg) (r2: freg) (r3: freg) + | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg) + | Pmaxsd (r1: freg) (r2: freg) + | Pminsd (r1: freg) (r2: freg) + | Prolw_8 (r: ireg) + | Psbbl (r1: ireg) (r2: ireg) + | Psqrtsd (r1: freg) (r2: freg). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -748,7 +771,32 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pbuiltin ef args res => Stuck (**r treated specially below *) | Pannot ef args => - Stuck (**r treated specially below *) + Stuck (**r treated specially below *) + (** The following instructions and directives are not generated directly by Asmgen, + so we do not model them. *) + | Padcl_ir _ _ + | Padcl_rr _ _ + | Paddl _ _ + | Pbswap _ + | Pbsfl _ _ + | Pbslr _ _ + | Pfmadd132 _ _ _ + | Pfmadd213 _ _ _ + | Pfmadd231 _ _ _ + | Pfmsub132 _ _ _ + | Pfmsub213 _ _ _ + | Pfmsub231 _ _ _ + | Pfnmadd132 _ _ _ + | Pfnmadd213 _ _ _ + | Pfnmadd231 _ _ _ + | Pfnmsub132 _ _ _ + | Pfnmsub213 _ _ _ + | Pfnmsub231 _ _ _ + | Pmaxsd _ _ + | Pminsd _ _ + | Prolw_8 _ + | Psbbl _ _ + | Psqrtsd _ _ => Stuck end. (** Translation of the LTL/Linear/Mach view of machine registers diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 9a458c37..e93de125 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -14,5 +14,162 @@ of the IA32 assembly code. Currently not done, this expansion is performed on the fly in PrintAsm. *) +open Asm +open Asmexpandaux +open AST +open Camlcoq + +(* Useful constants and helper functions *) + +let _0 = Integers.Int.zero + +(* Handling of compiler-inlined builtins *) + +let emit_builtin_inline oc name args res = + match name, args, res with + (* Integer arithmetic *) + | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> + if a1 <> res then + emit (Pmov_rr (res,a1)); + emit (Pbswap res) + | "__builtin_bswap16", [IR a1], [IR res] -> + if a1 <> res then + emit (Pmov_rr (res,a1)); + emit (Prolw_8 res) + | "__builtin_clz", [IR a1], [IR res] -> + emit (Pbslr (a1,res)); + emit (Pxor_ri(res,coqint_of_camlint 31l)) + | "__builtin_ctz", [IR a1], [IR res] -> + emit (Pbsfl (a1,res)) + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], [FR res] -> + if a1 <> res then + emit (Pmovsd_ff (a1,res)); + emit (Pabsd res) (* This ensures that need_masks is set to true *) + | "__builtin_fsqrt", [FR a1], [FR res] -> + emit (Psqrtsd (a1,res)) + | "__builtin_fmax", [FR a1; FR a2], [FR res] -> + if res = a1 then + emit (Pmaxsd (a2,res)) + else if res = a2 then + emit (Pmaxsd (a1,res)) + else begin + emit (Pmovsd_ff (a1,res)); + emit (Pmaxsd (a2,res)) + end + | "__builtin_fmin", [FR a1; FR a2], [FR res] -> + if res = a1 then + emit (Pminsd (a2,res)) + else if res = a2 then + emit (Pminsd (a1,res)) + else begin + emit (Pmovsd_ff (a1,res)); + emit (Pminsd (a2,res)) + end + | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] -> + if res = a1 then + emit (Pfmadd132 (a2,a3,res)) + else if res = a2 then + emit (Pfmadd213 (a2,a3,res)) + else if res = a3 then + emit (Pfmadd231 (a2,a3,res)) + else begin + emit (Pmovsd_ff (a2,res)); + emit (Pfmadd231 (a1,a2,res)) + end + |"__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] -> + if res = a1 then + emit (Pfmsub132 (a2,a3,res)) + else if res = a2 then + emit (Pfmsub213 (a2,a3,res)) + else if res = a3 then + emit (Pfmsub231 (a2,a3,res)) + else begin + emit (Pmovsd_ff (a2,res)); + emit (Pfmsub231 (a1,a2,res)) + end + | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] -> + if res = a1 then + emit (Pfnmadd132 (a2,a3,res)) + else if res = a2 then + emit (Pfnmadd213 (a2,a3,res)) + else if res = a3 then + emit (Pfnmadd231 (a2,a3,res)) + else begin + emit (Pmovsd_ff (a2,res)); + emit (Pfnmadd231 (a1,a2,res)) + end + |"__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] -> + if res = a1 then + emit (Pfnmsub132 (a2,a3,res)) + else if res = a2 then + emit (Pfnmsub213 (a2,a3,res)) + else if res = a3 then + emit (Pfnmsub231 (a2,a3,res)) + else begin + emit (Pmovsd_ff (a2,res)); + emit (Pfnmsub231 (a1,a2,res)) + end + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); + emit (Pneg EAX); + emit (Padcl_ir (_0,EDX)); + emit (Pneg EDX) + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + emit (Paddl (EBX,EAX)); + emit (Padcl_rr (ECX,EDX)) + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + emit (Psub_rr (EBX,EAX)); + emit (Psbbl (ECX,EDX)) + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + assert (a = EAX && b = EDX && rh = EDX && rl = EAX); + emit (Pmul_r EDX) + (* Memory accesses *) + (* | "__builtin_read16_reversed", [IR a1], [IR res] -> + fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_read32_reversed", [IR a1], [IR res] -> + fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + emit (Pmov_rr (a2,tmp)); + fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; + fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + emit (Pmov_rr (a2,tmp)); + emit (Pbswap res); + fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + (* Synchronization *) + | "__builtin_membar", [], _ -> + () + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a + (* Catch-all *) *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + +let expand_instruction instr = + match instr with + | _ -> emit instr + let expand_program p = p +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/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index a53a8fbd..a7aa9e90 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -841,6 +841,52 @@ module Target(System: SYSTEM):TARGET = fprintf oc " ret\n" end (** Pseudo-instructions *) + | Padcl_ir (n,res) -> + fprintf oc " adcl $%ld, %a\n" (camlint_of_coqint n) ireg res; + | Padcl_rr (a1,res) -> + fprintf oc " adcl %a, %a\n" ireg a1 ireg res; + | Paddl (a1,res) -> + fprintf oc " addl %a, %a\n" ireg a1 ireg res; + | Pbsfl (a1,res) -> + fprintf oc " bsfl %a, %a\n" ireg a1 ireg res + | Pbslr (a1,res) -> + fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; + | Pbswap res -> + fprintf oc " bswap %a\n" ireg res + | Pfmadd132 (a1,a2,res) -> + fprintf oc " vfmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfmadd213 (a1,a2,res) -> + fprintf oc " vfmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfmadd231 (a1,a2,res) -> + fprintf oc " vfmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfmsub132 (a1,a2,res) -> + fprintf oc " vfmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfmsub213 (a1,a2,res) -> + fprintf oc " vfmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfmsub231 (a1,a2,res) -> + fprintf oc " vfmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfnmadd132 (a1,a2,res) -> + fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfnmadd213 (a1,a2,res) -> + fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfnmadd231 (a1,a2,res) -> + fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfnmsub132 (a1,a2,res) -> + fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfnmsub213 (a1,a2,res) -> + fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pfnmsub231 (a1,a2,res) -> + fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res + | Pmaxsd (a1,res) -> + fprintf oc " maxsd %a, %a\n" freg a1 freg res + | Pminsd (a1,res) -> + fprintf oc " minsd %a, %a\n" freg a1 freg res + | Prolw_8 res -> + fprintf oc " rolw $8, %a\n" ireg16 res + | Psbbl (a1,res) -> + fprintf oc " sbbl %a, %a\n" ireg a1 ireg res + | Psqrtsd (a1,res) -> + fprintf oc " sqrtsd %a, %a\n" freg a1 freg res | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) | Pallocframe(sz, ofs_ra, ofs_link) -> -- cgit From 66b0512c64d39f30c103e4a1df470637c6cfd7bd Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 22 Jun 2015 00:50:02 +0200 Subject: Moved the rest of the ia32 builtins to asmexpand. --- arm/Asmexpand.ml | 4 +- ia32/Asm.v | 28 ++++- ia32/Asmexpand.ml | 256 ++++++++++++++++++++++++++++++++++++---- ia32/TargetPrinter.ml | 315 +++++--------------------------------------------- 4 files changed, 293 insertions(+), 310 deletions(-) diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 36db5f9e..95f35f37 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -324,7 +324,9 @@ let expand_instruction instr = | 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 diff --git a/ia32/Asm.v b/ia32/Asm.v index d136bf9b..b423b4fc 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -216,9 +216,12 @@ Inductive instruction: Type := | Padcl_ir (n: int) (r: ireg) | Padcl_rr (r1: ireg) (r2: ireg) | Paddl (r1: ireg) (r2: ireg) + | Paddl_mi (a: addrmode) (n: int) + | Paddl_ri (r1: ireg) (n: int) | Pbsfl (r1: ireg) (r2: ireg) | Pbslr (r1: ireg) (r2: ireg) | Pbswap (r: ireg) + | Pcfi_adjust (n: int) | Pfmadd132 (r1: freg) (r2: freg) (r3: freg) | Pfmadd213 (r1: freg) (r2: freg) (r3: freg) | Pfmadd231 (r1: freg) (r2: freg) (r3: freg) @@ -233,9 +236,18 @@ Inductive instruction: Type := | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg) | Pmaxsd (r1: freg) (r2: freg) | Pminsd (r1: freg) (r2: freg) + | Pmovb_rm (rs: ireg) (a: addrmode) + | Pmovq_rm (rs: freg) (a: addrmode) + | Pmovq_mr (a: addrmode) (rs: freg) + | Pmovsb + | Pmovsw + | Pmovw_rm (rs: ireg) (ad: addrmode) + | Prep_movsl | Prolw_8 (r: ireg) | Psbbl (r1: ireg) (r2: ireg) - | Psqrtsd (r1: freg) (r2: freg). + | Psqrtsd (r1: freg) (r2: freg) + | Psubl_ri (r1: ireg) (n: int) + | Pxchg (r1: ireg) (r2: ireg). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -777,9 +789,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Padcl_ir _ _ | Padcl_rr _ _ | Paddl _ _ + | Paddl_mi _ _ + | Paddl_ri _ _ | Pbswap _ | Pbsfl _ _ | Pbslr _ _ + | Pcfi_adjust _ | Pfmadd132 _ _ _ | Pfmadd213 _ _ _ | Pfmadd231 _ _ _ @@ -794,9 +809,18 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfnmsub231 _ _ _ | Pmaxsd _ _ | Pminsd _ _ + | Pmovb_rm _ _ + | Pmovq_rm _ _ + | Pmovq_mr _ _ + | Pmovsb + | Pmovsw + | Pmovw_rm _ _ + | Prep_movsl | Prolw_8 _ | Psbbl _ _ - | Psqrtsd _ _ => Stuck + | Psqrtsd _ _ + | Psubl_ri _ _ + | Pxchg _ _ => Stuck end. (** Translation of the LTL/Linear/Mach view of machine registers diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index e93de125..e07672a6 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -16,16 +16,198 @@ open Asm open Asmexpandaux +open Asmgen open AST open Camlcoq - +open Datatypes +open Integers + (* Useful constants and helper functions *) -let _0 = Integers.Int.zero +let _0 = Int.zero +let _1 = Int.one +let _2 = coqint_of_camlint 2l +let _4 = coqint_of_camlint 4l +let _8 = coqint_of_camlint 8l + +let stack_alignment () = + if Configuration.system = "macoxs" then 16 + else 8 + +(* SP adjustment to allocate or free a stack frame *) + +let int32_align n a = + if n >= 0l + then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a)) + else Int32.logand n (Int32.of_int (-a)) + +let sp_adjustment sz = + let sz = camlint_of_coqint sz in + (* Preserve proper alignment of the stack *) + let sz = int32_align sz (stack_alignment ()) in + (* The top 4 bytes have already been allocated by the "call" instruction. *) + let sz = Int32.sub sz 4l in + sz + + +(* 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 except ECX, EDX, XMM6 and XMM7. *) + +(* 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_rr (dst,src)) + | [FR src], [FR dst] -> + if dst <> src then emit (Pmovsd_ff (dst,src)) + | _, _ -> assert false + + +(* Handling of memcpy *) + +(* Unaligned memory accesses are quite fast on IA32, so use large + memory accesses regardless of alignment. *) + +let expand_builtin_memcpy_small sz al src dst = + assert (src = EDX && dst = EAX); + let rec copy ofs sz = + if sz >= 8 && !Clflags.option_ffpu then begin + emit (Pmovq_rm (XMM7,Addrmode (Some src, None, Coq_inl ofs))); + emit (Pmovq_mr (Addrmode (Some src, None, Coq_inl ofs),XMM7)); + copy (Int.add ofs _8) (sz - 8) + end else if sz >= 4 then begin + emit (Pmov_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); + emit (Pmov_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); + copy (Int.add ofs _4) (sz - 4) + end else if sz >= 2 then begin + emit (Pmovw_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); + emit (Pmovw_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); + copy (Int.add ofs _2) (sz - 2) + end else if sz >= 1 then begin + emit (Pmovb_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); + emit (Pmovb_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); + copy (Int.add ofs _1) (sz - 1) + end in + copy _0 sz + +let expand_builtin_memcpy_big sz al src dst = + assert (src = ESI && dst = EDI); + emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4)))); + emit Prep_movsl; + if sz mod 4 >= 2 then emit Pmovsw; + if sz mod 2 >= 1 then emit Pmovsb +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 offset_addressing (Addrmode(base, ofs, cst)) delta = + Addrmode(base, ofs, + match cst with + | Coq_inl n -> Coq_inl(Integers.Int.add n delta) + | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) + +let expand_builtin_vload_common chunk addr res = + match chunk, res with + | Mint8unsigned, [IR res] -> + emit (Pmovzb_rm (res,addr)) + | Mint8signed, [IR res] -> + emit (Pmovsb_rm (res,addr)) + | Mint16unsigned, [IR res] -> + emit (Pmovzw_rm (res,addr)) + | Mint16signed, [IR res] -> + emit (Pmovsw_rm (res,addr)) + | Mint32, [IR res] -> + emit (Pmov_rm (res,addr)) + | Mint64, [IR res1; IR res2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + if not (Asmgen.addressing_mentions addr res2) then begin + emit (Pmov_rm (res2,addr)); + emit (Pmov_rm (res1,addr')) + end else begin + emit (Pmov_rm (res1,addr')); + emit (Pmov_rm (res2,addr)) + end + | Mfloat32, [FR res] -> + emit (Pmovss_fm (res,addr)) + | Mfloat64, [FR res] -> + emit (Pmovsd_fm (res,addr)) + | _ -> + assert false + +let expand_builtin_vload chunk args res = + match args with + | [IR addr] -> + expand_builtin_vload_common chunk (Addrmode (Some addr,None, Coq_inl _0)) res + | _ -> + assert false + +let expand_builtin_vload_global chunk id ofs args res = + expand_builtin_vload_common chunk (Addrmode(None, None, Coq_inr(id,ofs))) res + +let expand_builtin_vstore_common chunk addr src tmp = + match chunk, src with + | (Mint8signed | Mint8unsigned), [IR src] -> + if Asmgen.low_ireg src then + emit (Pmovb_mr (addr,src)) + else begin + emit (Pmov_rr (tmp,src)); + emit (Pmovb_mr (addr,tmp)) + end + | (Mint16signed | Mint16unsigned), [IR src] -> + emit (Pmovw_mr (addr,src)) + | Mint32, [IR src] -> + emit (Pmov_mr (addr,src)) + | Mint64, [IR src1; IR src2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + emit (Pmov_mr (addr,src2)); + emit (Pmov_mr (addr',src1)) + | Mfloat32, [FR src] -> + emit (Pmovss_mf (addr,src)) + | Mfloat64, [FR src] -> + emit (Pmovsd_mf (addr,src)) + | _ -> + assert false + +let expand_builtin_vstore chunk args = + match args with + | IR addr :: src -> + expand_builtin_vstore_common chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src + (if addr = EAX then ECX else EAX) + | _ -> assert false + + +let expand_builtin_vstore_global chunk id ofs args = + expand_builtin_vstore_common chunk + (Addrmode(None, None, Coq_inr(id,ofs))) args EAX + + +(* Handling of varargs *) + +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 = coqint_of_camlint + Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) + (mul 4l (Z.to_int32 (Conventions1.size_arguments + !current_function.fn_sig)))) in + emit (Pmov_mr (Addrmode (Some r, None, Coq_inl _0),ESP)); + emit (Paddl_mi (Addrmode (Some r,None,Coq_inl _0),ofs)) + (* Handling of compiler-inlined builtins *) -let emit_builtin_inline oc name args res = +let expand_builtin_inline name args res = match name, args, res with (* Integer arithmetic *) | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> @@ -128,36 +310,70 @@ let emit_builtin_inline oc name args res = assert (a = EAX && b = EDX && rh = EDX && rl = EAX); emit (Pmul_r EDX) (* Memory accesses *) - (* | "__builtin_read16_reversed", [IR a1], [IR res] -> - fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_read16_reversed", [IR a1], [IR res] -> + let addr = Addrmode(Some a1,None,Coq_inl _0) in + emit (Pmovzw_rm (res,addr)); + emit (Prolw_8 res) | "__builtin_read32_reversed", [IR a1], [IR res] -> - fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res + let addr = Addrmode(Some a1,None,Coq_inl _0) in + emit (Pmov_rm (res,addr)); + emit (Pbswap res) | "__builtin_write16_reversed", [IR a1; IR a2], _ -> let tmp = if a1 = ECX then EDX else ECX in + let addr = Addrmode(Some a1,None,Coq_inl _0) in if a2 <> tmp then emit (Pmov_rr (a2,tmp)); - fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; - fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - emit (Pmov_rr (a2,tmp)); - emit (Pbswap res); - fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + emit (Pxchg (tmp,tmp)); + emit (Pmovw_mr (addr,tmp)) + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + expand_builtin_va_start a (* Synchronization *) | "__builtin_membar", [], _ -> () - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - print_builtin_va_start oc a - (* Catch-all *) *) + (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) + + let expand_instruction instr = match instr with + | Pallocframe (sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + let addr = Addrmode(Some ESP,None,Coq_inl (coqint_of_camlint (Int32.add sz 4l))) in + let addr' = Addrmode (Some ESP, None, Coq_inl ofs_link) in + let sz' = coqint_of_camlint sz in + emit (Psubl_ri (ESP,sz')); + emit (Pcfi_adjust sz'); + emit (Plea (EDX,addr)); + emit (Pmov_mr (addr',EDX)); + PrintAsmaux.current_function_stacksize := sz + | Pfreeframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + emit (Paddl_ri (ESP,coqint_of_camlint 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_memcpy(sz, al) -> + expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) + (Int32.to_int (camlint_of_coqint al)) args + | EF_annot_val(txt, targ) -> + expand_annot_val txt targ args res + | EF_inline_asm(txt, sg, clob) -> + emit instr + | _ -> assert false + end | _ -> emit instr let expand_program p = p diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index a7aa9e90..18aacebf 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -348,156 +348,7 @@ module Target(System: SYSTEM):TARGET = print_annot_stmt preg "%esp" 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 fprintf oc " movl %a, %a\n" ireg src ireg dst - | [FR src], [FR dst] -> - if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst - | _, _ -> assert false - -(* Handling of memcpy *) - -(* Unaligned memory accesses are quite fast on IA32, so use large - memory accesses regardless of alignment. *) - - let print_builtin_memcpy_small oc sz al src dst = - assert (src = EDX && dst = EAX); - let rec copy ofs sz = - if sz >= 8 && !Clflags.option_ffpu then begin - fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7; - fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst; - copy (ofs + 8) (sz - 8) - end else if sz >= 4 then begin - fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX; - fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst; - copy (ofs + 4) (sz - 4) - end else if sz >= 2 then begin - fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX; - fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst; - copy (ofs + 2) (sz - 2) - end else if sz >= 1 then begin - fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX; - fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst; - copy (ofs + 1) (sz - 1) - end in - copy 0 sz - - let print_builtin_memcpy_big oc sz al src dst = - assert (src = ESI && dst = EDI); - fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; - fprintf oc " rep movsl\n"; - if sz mod 4 >= 2 then fprintf oc " movsw\n"; - if sz mod 2 >= 1 then fprintf oc " movsb\n" - - 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; - if sz <= 32 - then print_builtin_memcpy_small oc sz al src dst - else print_builtin_memcpy_big oc sz al src dst; - fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment - -(* Handling of volatile reads and writes *) - - let offset_addressing (Addrmode(base, ofs, cst)) delta = - Addrmode(base, ofs, - match cst with - | Coq_inl n -> Coq_inl(Integers.Int.add n delta) - | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) - - let print_builtin_vload_common oc chunk addr res = - match chunk, res with - | Mint8unsigned, [IR res] -> - fprintf oc " movzbl %a, %a\n" addressing addr ireg res - | Mint8signed, [IR res] -> - fprintf oc " movsbl %a, %a\n" addressing addr ireg res - | Mint16unsigned, [IR res] -> - fprintf oc " movzwl %a, %a\n" addressing addr ireg res - | Mint16signed, [IR res] -> - fprintf oc " movswl %a, %a\n" addressing addr ireg res - | Mint32, [IR res] -> - fprintf oc " movl %a, %a\n" addressing addr ireg res - | Mint64, [IR res1; IR res2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - if not (Asmgen.addressing_mentions addr res2) then begin - fprintf oc " movl %a, %a\n" addressing addr ireg res2; - fprintf oc " movl %a, %a\n" addressing addr' ireg res1 - end else begin - fprintf oc " movl %a, %a\n" addressing addr' ireg res1; - fprintf oc " movl %a, %a\n" addressing addr ireg res2 - end - | Mfloat32, [FR res] -> - fprintf oc " movss %a, %a\n" addressing addr freg res - | Mfloat64, [FR res] -> - fprintf oc " movsd %a, %a\n" addressing addr freg res - | _ -> - assert false - - let print_builtin_vload oc chunk args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - begin match args with - | [IR addr] -> - print_builtin_vload_common oc chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res - | _ -> - assert false - end; - fprintf oc "%s end builtin __builtin_volatile_read\n" comment - - let print_builtin_vload_global oc chunk id ofs args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - print_builtin_vload_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) res; - fprintf oc "%s end builtin __builtin_volatile_read\n" comment - - let print_builtin_vstore_common oc chunk addr src tmp = - match chunk, src with - | (Mint8signed | Mint8unsigned), [IR src] -> - if Asmgen.low_ireg src then - fprintf oc " movb %a, %a\n" ireg8 src addressing addr - else begin - fprintf oc " movl %a, %a\n" ireg src ireg tmp; - fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr - end - | (Mint16signed | Mint16unsigned), [IR src] -> - fprintf oc " movw %a, %a\n" ireg16 src addressing addr - | Mint32, [IR src] -> - fprintf oc " movl %a, %a\n" ireg src addressing addr - | Mint64, [IR src1; IR src2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - fprintf oc " movl %a, %a\n" ireg src2 addressing addr; - fprintf oc " movl %a, %a\n" ireg src1 addressing addr' - | Mfloat32, [FR src] -> - fprintf oc " movss %a, %a\n" freg src addressing addr - | Mfloat64, [FR src] -> - fprintf oc " movsd %a, %a\n" freg src addressing addr - | _ -> - assert false - - let print_builtin_vstore oc chunk args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - begin match args with - | IR addr :: src -> - print_builtin_vstore_common oc chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src - (if addr = EAX then ECX else EAX) - | _ -> - assert false - end; - fprintf oc "%s end builtin __builtin_volatile_write\n" comment - - let print_builtin_vstore_global oc chunk id ofs args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - print_builtin_vstore_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; - fprintf oc "%s end builtin __builtin_volatile_write\n" comment - -(* Handling of varargs *) + (* Handling of varargs *) let print_builtin_va_start oc r = if not (!current_function_sig).sig_cc.cc_vararg then @@ -509,117 +360,6 @@ module Target(System: SYSTEM):TARGET = fprintf oc " movl %%esp, 0(%a)\n" ireg r; fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r -(* Handling of compiler-inlined builtins *) - - let print_builtin_inline oc name args res = - fprintf oc "%s begin builtin %s\n" comment name; - begin match name, args, res with - (* Integer arithmetic *) - | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> - if a1 <> res then - fprintf oc " movl %a, %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res - | "__builtin_bswap16", [IR a1], [IR res] -> - if a1 <> res then - fprintf oc " movl %a, %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res - | "__builtin_clz", [IR a1], [IR res] -> - fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; - fprintf oc " xorl $31, %a\n" ireg res - | "__builtin_ctz", [IR a1], [IR res] -> - fprintf oc " bsfl %a, %a\n" ireg a1 ireg res - (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> - need_masks := true; - if a1 <> res then - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res - | "__builtin_fsqrt", [FR a1], [FR res] -> - fprintf oc " sqrtsd %a, %a\n" freg a1 freg res - | "__builtin_fmax", [FR a1; FR a2], [FR res] -> - if res = a1 then - fprintf oc " maxsd %a, %a\n" freg a2 freg res - else if res = a2 then - fprintf oc " maxsd %a, %a\n" freg a1 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " maxsd %a, %a\n" freg a2 freg res - end - | "__builtin_fmin", [FR a1; FR a2], [FR res] -> - if res = a1 then - fprintf oc " minsd %a, %a\n" freg a2 freg res - else if res = a2 then - fprintf oc " minsd %a, %a\n" freg a1 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " minsd %a, %a\n" freg a2 freg res - end - | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"), - [FR a1; FR a2; FR a3], [FR res] -> - let opcode = - match name with - | "__builtin_fmadd" -> "vfmadd" - | "__builtin_fmsub" -> "vfmsub" - | "__builtin_fnmadd" -> "vfnmadd" - | "__builtin_fnmsub" -> "vfnmsub" - | _ -> assert false in - if res = a1 then - fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res - else if res = a2 then - fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res - else if res = a3 then - fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a3 freg res; - fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res - end - (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); - fprintf oc " negl %a\n" ireg EAX; - fprintf oc " adcl $0, %a\n" ireg EDX; - fprintf oc " negl %a\n" ireg EDX - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - fprintf oc " addl %a, %a\n" ireg EBX ireg EAX; - fprintf oc " adcl %a, %a\n" ireg ECX ireg EDX - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - fprintf oc " subl %a, %a\n" ireg EBX ireg EAX; - fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - assert (a = EAX && b = EDX && rh = EDX && rl = EAX); - fprintf oc " mull %a\n" ireg EDX - (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> - fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res - | "__builtin_read32_reversed", [IR a1], [IR res] -> - fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; - fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; - fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; - fprintf oc " bswap %a\n" ireg tmp; - fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 - (* Synchronization *) - | "__builtin_membar", [], _ -> - () - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - print_builtin_va_start oc a - (* Catch-all *) - | _ -> - invalid_arg ("unrecognized builtin " ^ name) - end; - fprintf oc "%s end builtin %s\n" comment name (* Printing of instructions *) @@ -847,12 +587,18 @@ module Target(System: SYSTEM):TARGET = fprintf oc " adcl %a, %a\n" ireg a1 ireg res; | Paddl (a1,res) -> fprintf oc " addl %a, %a\n" ireg a1 ireg res; + | Paddl_mi (addr,n) -> + fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) addressing addr + | Paddl_ri (res,n) -> + fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) ireg res | Pbsfl (a1,res) -> fprintf oc " bsfl %a, %a\n" ireg a1 ireg res | Pbslr (a1,res) -> - fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; + fprintf oc " bsrl %a, %a\n" ireg a1 ireg res | Pbswap res -> fprintf oc " bswap %a\n" ireg res + | Pcfi_adjust sz -> + cfi_adjust oc (camlint_of_coqint sz) | Pfmadd132 (a1,a2,res) -> fprintf oc " vfmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res | Pfmadd213 (a1,a2,res) -> @@ -881,42 +627,37 @@ module Target(System: SYSTEM):TARGET = fprintf oc " maxsd %a, %a\n" freg a1 freg res | Pminsd (a1,res) -> fprintf oc " minsd %a, %a\n" freg a1 freg res + | Pmovb_rm (r1,a) -> + fprintf oc " movb %a, %a\n" addressing a ireg8 r1 + | Pmovq_rm(rd, a) -> + fprintf oc " movq %a, %a\n" addressing a freg rd + | Pmovq_mr(a, r1) -> + fprintf oc " movq %a, %a\n" freg r1 addressing a + | Pmovsb -> + fprintf oc " movsb\n"; + | Pmovsw -> + fprintf oc " movsw\n"; + | Pmovw_rm (r1, a) -> + fprintf oc " movw %a, %a\n" addressing a ireg16 r1 + | Prep_movsl -> + fprintf oc " rep movsl\n" | Prolw_8 res -> fprintf oc " rolw $8, %a\n" ireg16 res | Psbbl (a1,res) -> fprintf oc " sbbl %a, %a\n" ireg a1 ireg res | Psqrtsd (a1,res) -> fprintf oc " sqrtsd %a, %a\n" freg a1 freg res + | Psubl_ri (res,n) -> + fprintf oc " subl $%ld, %a\n" (camlint_of_coqint n) ireg res; + | Pxchg (a1,a2) -> + fprintf oc " xchg %a, %a\n" ireg8 a1 high_ireg8 a2; | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - let ofs_link = camlint_of_coqint ofs_link in - fprintf oc " subl $%ld, %%esp\n" sz; - cfi_adjust oc sz; - fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); - fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; - current_function_stacksize := sz + | Pallocframe(sz, ofs_ra, ofs_link) | Pfreeframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - fprintf oc " addl $%ld, %%esp\n" sz + assert false | 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; -- cgit From 6b7b7a73f6d04517ffeb4c6faa59ea403d85925f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 26 Jun 2015 21:51:47 +0200 Subject: Adapt LICENSE file to include AbsInt and how to obtain a commercial license. --- LICENSE | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/LICENSE b/LICENSE index 21670791..5ffb39ab 100644 --- a/LICENSE +++ b/LICENSE @@ -1,14 +1,21 @@ All files in this distribution are part of the CompCert verified compiler. -The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007, -2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Institut National de -Recherche en Informatique et en Automatique (INRIA). +The CompCert verified compiler is Copyright by Institut National de +Recherche en Informatique et en Automatique (INRIA) and +AbsInt Angewandte Informatik GmbH. The CompCert verified compiler is distributed under the terms of the -INRIA Non-Commercial License Agreement given below. This is a -non-free license that grants you the right to use the CompCert verified -compiler for educational, research or evaluation purposes only, but -prohibits commercial uses. +INRIA Non-Commercial License Agreement given below or under the terms +of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH. +The latter is a separate contract document. + +The INRIA Non-Commercial License Agreement is a non-free license that +grants you the right to use the CompCert verified compiler for +educational, research or evaluation purposes only, but prohibits +any commercial uses. + +For commercial use you need a Software Usage Agreement from +AbsInt Angewandte Informatik GmbH. The following files in this distribution are dual-licensed both under the INRIA Non-Commercial License Agreement and under the Free Software -- cgit From daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 26 Jun 2015 21:53:02 +0200 Subject: Added --version option to print version string. --- driver/Driver.ml | 28 +++++++++++++++++++--------- 1 file changed, 19 insertions(+), 9 deletions(-) diff --git a/driver/Driver.ml b/driver/Driver.ml index 480cf665..805d5405 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -74,7 +74,7 @@ let print_error oc msg = let output_filename ?(final = false) source_file source_suffix output_suffix = match !option_o with | Some file when final -> file - | _ -> + | _ -> Filename.basename (Filename.chop_suffix source_file source_suffix) ^ output_suffix @@ -127,7 +127,7 @@ let parse_c_file sourcename ifile = let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc - end; + end; (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -176,7 +176,7 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> print_error stderr msg; exit 2 in - (* Dump Asm in binary format *) + (* Dump Asm in binary format *) if !option_sdump then dump_asm asm (output_filename sourcename ".c" ".sdump"); (* Print Asm in text form *) @@ -219,7 +219,7 @@ let compile_cminor_file ifile ofile = eprintf "File %s, character %d: Syntax error\n" ifile (Lexing.lexeme_start lb); exit 2 - | CMlexer.Error msg -> + | CMlexer.Error msg -> eprintf "File %s, character %d: %s\n" ifile (Lexing.lexeme_start lb) msg; exit 2 @@ -361,7 +361,7 @@ let process_h_file sourcename = end else begin eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename; exit 2 - end + end (* Record actions to be performed after parsing the command line *) @@ -386,9 +386,12 @@ let explode_comma_option s = | [] -> assert false | hd :: tl -> tl +let version_string = + "The CompCert C verified compiler, version "^ Configuration.version ^ "\n" + let usage_string = -"The CompCert C verified compiler, version " ^ Configuration.version ^ " -Usage: ccomp [options] + version_string ^ + "Usage: ccomp [options] Recognized source files: .c C source file .i or .p C source file that should not be preprocessed @@ -464,6 +467,7 @@ General options: -stdlib Set the path of the Compcert run-time library -v Print external commands before invoking them -timings Show the time spent in various compiler passes + -version Print the version string and exit Interpreter mode: -interp Execute given .c files using the reference interpreter -quiet Suppress diagnostic messages for the interpreter @@ -475,6 +479,9 @@ Interpreter mode: let print_usage_and_exit _ = printf "%s" usage_string; exit 0 +let print_version_and_exit _ = + printf "%s" version_string; exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_return; option_fvararg_calls; option_funprototyped; @@ -497,13 +504,16 @@ let cmdline_actions = (* Getting help *) Exact "-help", Self print_usage_and_exit; Exact "--help", Self print_usage_and_exit; +(* Getting version info *) + Exact "-version", Self print_version_and_exit; + Exact "--version", Self print_version_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in - option_o := Some s); + option_o := Some s); (* Preprocessing options *) Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); @@ -549,7 +559,7 @@ let cmdline_actions = Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; Exact "-sdump", Set option_sdump; -(* General options *) +(* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); Exact "-timings", Set option_timings; -- cgit From e24e4a9329885c80fbbb42a1c541880eff607e32 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 26 Jun 2015 22:02:02 +0200 Subject: Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert" This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1. --- arm/Asm.v | 39 +---- arm/Asmexpand.ml | 332 +----------------------------------------- arm/TargetPrinter.ml | 321 +++++++++++++++++++++++++++++++++++------ backend/Asmexpandaux.ml | 57 -------- ia32/Asm.v | 76 +--------- ia32/Asmexpand.ml | 373 ------------------------------------------------ ia32/TargetPrinter.ml | 359 ++++++++++++++++++++++++++++++++++++---------- powerpc/Asmexpand.ml | 55 +++++-- 8 files changed, 615 insertions(+), 997 deletions(-) delete mode 100644 backend/Asmexpandaux.ml diff --git a/arm/Asm.v b/arm/Asm.v index dd434c02..2a120dd4 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -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 diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml deleted file mode 100644 index 6ce6c005..00000000 --- a/backend/Asmexpandaux.ml +++ /dev/null @@ -1,57 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Util functions used for the expansion of built-ins and some - pseudo-instructions *) - -open Asm -open AST -open Camlcoq - -(* Buffering the expanded code *) - -let current_code = ref ([]: instruction list) - -let emit i = current_code := i :: !current_code - -(* Generation of fresh labels *) - -let dummy_function = { fn_code = []; fn_sig = signature_main } -let current_function = ref dummy_function -let next_label = ref (None: label option) - -let new_label () = - let lbl = - match !next_label with - | Some l -> l - | None -> - (* on-demand computation of the next available label *) - List.fold_left - (fun next instr -> - match instr with - | Plabel l -> if P.lt l next then next else P.succ l - | _ -> next) - P.one (!current_function).fn_code - in - next_label := Some (P.succ lbl); - lbl - - -let set_current_function f = - current_function := f; next_label := None; current_code := [] - -let get_current_function () = - let c = List.rev !current_code in - let fn = !current_function in - set_current_function dummy_function; - {fn with fn_code = c} diff --git a/ia32/Asm.v b/ia32/Asm.v index b423b4fc..b67c3cc5 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -212,42 +212,7 @@ Inductive instruction: Type := | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) | Pbuiltin(ef: external_function)(args: list preg)(res: list preg) - | Pannot(ef: external_function)(args: list (annot_arg preg)) - | Padcl_ir (n: int) (r: ireg) - | Padcl_rr (r1: ireg) (r2: ireg) - | Paddl (r1: ireg) (r2: ireg) - | Paddl_mi (a: addrmode) (n: int) - | Paddl_ri (r1: ireg) (n: int) - | Pbsfl (r1: ireg) (r2: ireg) - | Pbslr (r1: ireg) (r2: ireg) - | Pbswap (r: ireg) - | Pcfi_adjust (n: int) - | Pfmadd132 (r1: freg) (r2: freg) (r3: freg) - | Pfmadd213 (r1: freg) (r2: freg) (r3: freg) - | Pfmadd231 (r1: freg) (r2: freg) (r3: freg) - | Pfmsub132 (r1: freg) (r2: freg) (r3: freg) - | Pfmsub213 (r1: freg) (r2: freg) (r3: freg) - | Pfmsub231 (r1: freg) (r2: freg) (r3: freg) - | Pfnmadd132 (r1: freg) (r2: freg) (r3: freg) - | Pfnmadd213 (r1: freg) (r2: freg) (r3: freg) - | Pfnmadd231 (r1: freg) (r2: freg) (r3: freg) - | Pfnmsub132 (r1: freg) (r2: freg) (r3: freg) - | Pfnmsub213 (r1: freg) (r2: freg) (r3: freg) - | Pfnmsub231 (r1: freg) (r2: freg) (r3: freg) - | Pmaxsd (r1: freg) (r2: freg) - | Pminsd (r1: freg) (r2: freg) - | Pmovb_rm (rs: ireg) (a: addrmode) - | Pmovq_rm (rs: freg) (a: addrmode) - | Pmovq_mr (a: addrmode) (rs: freg) - | Pmovsb - | Pmovsw - | Pmovw_rm (rs: ireg) (ad: addrmode) - | Prep_movsl - | Prolw_8 (r: ireg) - | Psbbl (r1: ireg) (r2: ireg) - | Psqrtsd (r1: freg) (r2: freg) - | Psubl_ri (r1: ireg) (n: int) - | Pxchg (r1: ireg) (r2: ireg). + | Pannot(ef: external_function)(args: list (annot_arg preg)). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -783,44 +748,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | 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. *) - | Padcl_ir _ _ - | Padcl_rr _ _ - | Paddl _ _ - | Paddl_mi _ _ - | Paddl_ri _ _ - | Pbswap _ - | Pbsfl _ _ - | Pbslr _ _ - | Pcfi_adjust _ - | Pfmadd132 _ _ _ - | Pfmadd213 _ _ _ - | Pfmadd231 _ _ _ - | Pfmsub132 _ _ _ - | Pfmsub213 _ _ _ - | Pfmsub231 _ _ _ - | Pfnmadd132 _ _ _ - | Pfnmadd213 _ _ _ - | Pfnmadd231 _ _ _ - | Pfnmsub132 _ _ _ - | Pfnmsub213 _ _ _ - | Pfnmsub231 _ _ _ - | Pmaxsd _ _ - | Pminsd _ _ - | Pmovb_rm _ _ - | Pmovq_rm _ _ - | Pmovq_mr _ _ - | Pmovsb - | Pmovsw - | Pmovw_rm _ _ - | Prep_movsl - | Prolw_8 _ - | Psbbl _ _ - | Psqrtsd _ _ - | Psubl_ri _ _ - | Pxchg _ _ => Stuck + Stuck (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index e07672a6..9a458c37 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -14,378 +14,5 @@ of the IA32 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 Datatypes -open Integers - -(* Useful constants and helper functions *) - -let _0 = Int.zero -let _1 = Int.one -let _2 = coqint_of_camlint 2l -let _4 = coqint_of_camlint 4l -let _8 = coqint_of_camlint 8l - -let stack_alignment () = - if Configuration.system = "macoxs" then 16 - else 8 - -(* SP adjustment to allocate or free a stack frame *) - -let int32_align n a = - if n >= 0l - then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a)) - else Int32.logand n (Int32.of_int (-a)) - -let sp_adjustment sz = - let sz = camlint_of_coqint sz in - (* Preserve proper alignment of the stack *) - let sz = int32_align sz (stack_alignment ()) in - (* The top 4 bytes have already been allocated by the "call" instruction. *) - let sz = Int32.sub sz 4l in - sz - - -(* 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 except ECX, EDX, XMM6 and XMM7. *) - -(* 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_rr (dst,src)) - | [FR src], [FR dst] -> - if dst <> src then emit (Pmovsd_ff (dst,src)) - | _, _ -> assert false - - -(* Handling of memcpy *) - -(* Unaligned memory accesses are quite fast on IA32, so use large - memory accesses regardless of alignment. *) - -let expand_builtin_memcpy_small sz al src dst = - assert (src = EDX && dst = EAX); - let rec copy ofs sz = - if sz >= 8 && !Clflags.option_ffpu then begin - emit (Pmovq_rm (XMM7,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmovq_mr (Addrmode (Some src, None, Coq_inl ofs),XMM7)); - copy (Int.add ofs _8) (sz - 8) - end else if sz >= 4 then begin - emit (Pmov_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmov_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); - copy (Int.add ofs _4) (sz - 4) - end else if sz >= 2 then begin - emit (Pmovw_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmovw_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); - copy (Int.add ofs _2) (sz - 2) - end else if sz >= 1 then begin - emit (Pmovb_rm (ECX,Addrmode (Some src, None, Coq_inl ofs))); - emit (Pmovb_mr (Addrmode (Some src, None, Coq_inl ofs),ECX)); - copy (Int.add ofs _1) (sz - 1) - end in - copy _0 sz - -let expand_builtin_memcpy_big sz al src dst = - assert (src = ESI && dst = EDI); - emit (Pmov_ri (ECX,coqint_of_camlint (Int32.of_int (sz / 4)))); - emit Prep_movsl; - if sz mod 4 >= 2 then emit Pmovsw; - if sz mod 2 >= 1 then emit Pmovsb - -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 offset_addressing (Addrmode(base, ofs, cst)) delta = - Addrmode(base, ofs, - match cst with - | Coq_inl n -> Coq_inl(Integers.Int.add n delta) - | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) - -let expand_builtin_vload_common chunk addr res = - match chunk, res with - | Mint8unsigned, [IR res] -> - emit (Pmovzb_rm (res,addr)) - | Mint8signed, [IR res] -> - emit (Pmovsb_rm (res,addr)) - | Mint16unsigned, [IR res] -> - emit (Pmovzw_rm (res,addr)) - | Mint16signed, [IR res] -> - emit (Pmovsw_rm (res,addr)) - | Mint32, [IR res] -> - emit (Pmov_rm (res,addr)) - | Mint64, [IR res1; IR res2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - if not (Asmgen.addressing_mentions addr res2) then begin - emit (Pmov_rm (res2,addr)); - emit (Pmov_rm (res1,addr')) - end else begin - emit (Pmov_rm (res1,addr')); - emit (Pmov_rm (res2,addr)) - end - | Mfloat32, [FR res] -> - emit (Pmovss_fm (res,addr)) - | Mfloat64, [FR res] -> - emit (Pmovsd_fm (res,addr)) - | _ -> - assert false - -let expand_builtin_vload chunk args res = - match args with - | [IR addr] -> - expand_builtin_vload_common chunk (Addrmode (Some addr,None, Coq_inl _0)) res - | _ -> - assert false - -let expand_builtin_vload_global chunk id ofs args res = - expand_builtin_vload_common chunk (Addrmode(None, None, Coq_inr(id,ofs))) res - -let expand_builtin_vstore_common chunk addr src tmp = - match chunk, src with - | (Mint8signed | Mint8unsigned), [IR src] -> - if Asmgen.low_ireg src then - emit (Pmovb_mr (addr,src)) - else begin - emit (Pmov_rr (tmp,src)); - emit (Pmovb_mr (addr,tmp)) - end - | (Mint16signed | Mint16unsigned), [IR src] -> - emit (Pmovw_mr (addr,src)) - | Mint32, [IR src] -> - emit (Pmov_mr (addr,src)) - | Mint64, [IR src1; IR src2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - emit (Pmov_mr (addr,src2)); - emit (Pmov_mr (addr',src1)) - | Mfloat32, [FR src] -> - emit (Pmovss_mf (addr,src)) - | Mfloat64, [FR src] -> - emit (Pmovsd_mf (addr,src)) - | _ -> - assert false - -let expand_builtin_vstore chunk args = - match args with - | IR addr :: src -> - expand_builtin_vstore_common chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src - (if addr = EAX then ECX else EAX) - | _ -> assert false - - -let expand_builtin_vstore_global chunk id ofs args = - expand_builtin_vstore_common chunk - (Addrmode(None, None, Coq_inr(id,ofs))) args EAX - - -(* Handling of varargs *) - -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 = coqint_of_camlint - Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments - !current_function.fn_sig)))) in - emit (Pmov_mr (Addrmode (Some r, None, Coq_inl _0),ESP)); - emit (Paddl_mi (Addrmode (Some r,None,Coq_inl _0),ofs)) - -(* 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] -> - if a1 <> res then - emit (Pmov_rr (res,a1)); - emit (Pbswap res) - | "__builtin_bswap16", [IR a1], [IR res] -> - if a1 <> res then - emit (Pmov_rr (res,a1)); - emit (Prolw_8 res) - | "__builtin_clz", [IR a1], [IR res] -> - emit (Pbslr (a1,res)); - emit (Pxor_ri(res,coqint_of_camlint 31l)) - | "__builtin_ctz", [IR a1], [IR res] -> - emit (Pbsfl (a1,res)) - (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> - if a1 <> res then - emit (Pmovsd_ff (a1,res)); - emit (Pabsd res) (* This ensures that need_masks is set to true *) - | "__builtin_fsqrt", [FR a1], [FR res] -> - emit (Psqrtsd (a1,res)) - | "__builtin_fmax", [FR a1; FR a2], [FR res] -> - if res = a1 then - emit (Pmaxsd (a2,res)) - else if res = a2 then - emit (Pmaxsd (a1,res)) - else begin - emit (Pmovsd_ff (a1,res)); - emit (Pmaxsd (a2,res)) - end - | "__builtin_fmin", [FR a1; FR a2], [FR res] -> - if res = a1 then - emit (Pminsd (a2,res)) - else if res = a2 then - emit (Pminsd (a1,res)) - else begin - emit (Pmovsd_ff (a1,res)); - emit (Pminsd (a2,res)) - end - | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] -> - if res = a1 then - emit (Pfmadd132 (a2,a3,res)) - else if res = a2 then - emit (Pfmadd213 (a2,a3,res)) - else if res = a3 then - emit (Pfmadd231 (a2,a3,res)) - else begin - emit (Pmovsd_ff (a2,res)); - emit (Pfmadd231 (a1,a2,res)) - end - |"__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] -> - if res = a1 then - emit (Pfmsub132 (a2,a3,res)) - else if res = a2 then - emit (Pfmsub213 (a2,a3,res)) - else if res = a3 then - emit (Pfmsub231 (a2,a3,res)) - else begin - emit (Pmovsd_ff (a2,res)); - emit (Pfmsub231 (a1,a2,res)) - end - | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] -> - if res = a1 then - emit (Pfnmadd132 (a2,a3,res)) - else if res = a2 then - emit (Pfnmadd213 (a2,a3,res)) - else if res = a3 then - emit (Pfnmadd231 (a2,a3,res)) - else begin - emit (Pmovsd_ff (a2,res)); - emit (Pfnmadd231 (a1,a2,res)) - end - |"__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] -> - if res = a1 then - emit (Pfnmsub132 (a2,a3,res)) - else if res = a2 then - emit (Pfnmsub213 (a2,a3,res)) - else if res = a3 then - emit (Pfnmsub231 (a2,a3,res)) - else begin - emit (Pmovsd_ff (a2,res)); - emit (Pfnmsub231 (a1,a2,res)) - end - (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); - emit (Pneg EAX); - emit (Padcl_ir (_0,EDX)); - emit (Pneg EDX) - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - emit (Paddl (EBX,EAX)); - emit (Padcl_rr (ECX,EDX)) - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - emit (Psub_rr (EBX,EAX)); - emit (Psbbl (ECX,EDX)) - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - assert (a = EAX && b = EDX && rh = EDX && rl = EAX); - emit (Pmul_r EDX) - (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> - let addr = Addrmode(Some a1,None,Coq_inl _0) in - emit (Pmovzw_rm (res,addr)); - emit (Prolw_8 res) - | "__builtin_read32_reversed", [IR a1], [IR res] -> - let addr = Addrmode(Some a1,None,Coq_inl _0) in - emit (Pmov_rm (res,addr)); - emit (Pbswap res) - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - let addr = Addrmode(Some a1,None,Coq_inl _0) in - if a2 <> tmp then - emit (Pmov_rr (a2,tmp)); - emit (Pxchg (tmp,tmp)); - emit (Pmovw_mr (addr,tmp)) - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - expand_builtin_va_start a - (* Synchronization *) - | "__builtin_membar", [], _ -> - () - (* Catch-all *) - | _ -> - invalid_arg ("unrecognized builtin " ^ name) - - - -let expand_instruction instr = - match instr with - | Pallocframe (sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - let addr = Addrmode(Some ESP,None,Coq_inl (coqint_of_camlint (Int32.add sz 4l))) in - let addr' = Addrmode (Some ESP, None, Coq_inl ofs_link) in - let sz' = coqint_of_camlint sz in - emit (Psubl_ri (ESP,sz')); - emit (Pcfi_adjust sz'); - emit (Plea (EDX,addr)); - emit (Pmov_mr (addr',EDX)); - PrintAsmaux.current_function_stacksize := sz - | Pfreeframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - emit (Paddl_ri (ESP,coqint_of_camlint 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_memcpy(sz, al) -> - expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) - (Int32.to_int (camlint_of_coqint al)) args - | EF_annot_val(txt, targ) -> - expand_annot_val txt targ args res - | EF_inline_asm(txt, sg, clob) -> - emit instr - | _ -> assert false - end - | _ -> emit instr - let expand_program p = p -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/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 18aacebf..a53a8fbd 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -348,7 +348,156 @@ module Target(System: SYSTEM):TARGET = print_annot_stmt preg "%esp" oc txt targs args end - (* Handling of varargs *) + 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 fprintf oc " movl %a, %a\n" ireg src ireg dst + | [FR src], [FR dst] -> + if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst + | _, _ -> assert false + +(* Handling of memcpy *) + +(* Unaligned memory accesses are quite fast on IA32, so use large + memory accesses regardless of alignment. *) + + let print_builtin_memcpy_small oc sz al src dst = + assert (src = EDX && dst = EAX); + let rec copy ofs sz = + if sz >= 8 && !Clflags.option_ffpu then begin + fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7; + fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst; + copy (ofs + 8) (sz - 8) + end else if sz >= 4 then begin + fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX; + fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst; + copy (ofs + 4) (sz - 4) + end else if sz >= 2 then begin + fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX; + fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst; + copy (ofs + 2) (sz - 2) + end else if sz >= 1 then begin + fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX; + fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst; + copy (ofs + 1) (sz - 1) + end in + copy 0 sz + + let print_builtin_memcpy_big oc sz al src dst = + assert (src = ESI && dst = EDI); + fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; + fprintf oc " rep movsl\n"; + if sz mod 4 >= 2 then fprintf oc " movsw\n"; + if sz mod 2 >= 1 then fprintf oc " movsb\n" + + 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; + if sz <= 32 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst; + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment + +(* Handling of volatile reads and writes *) + + let offset_addressing (Addrmode(base, ofs, cst)) delta = + Addrmode(base, ofs, + match cst with + | Coq_inl n -> Coq_inl(Integers.Int.add n delta) + | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) + + let print_builtin_vload_common oc chunk addr res = + match chunk, res with + | Mint8unsigned, [IR res] -> + fprintf oc " movzbl %a, %a\n" addressing addr ireg res + | Mint8signed, [IR res] -> + fprintf oc " movsbl %a, %a\n" addressing addr ireg res + | Mint16unsigned, [IR res] -> + fprintf oc " movzwl %a, %a\n" addressing addr ireg res + | Mint16signed, [IR res] -> + fprintf oc " movswl %a, %a\n" addressing addr ireg res + | Mint32, [IR res] -> + fprintf oc " movl %a, %a\n" addressing addr ireg res + | Mint64, [IR res1; IR res2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + if not (Asmgen.addressing_mentions addr res2) then begin + fprintf oc " movl %a, %a\n" addressing addr ireg res2; + fprintf oc " movl %a, %a\n" addressing addr' ireg res1 + end else begin + fprintf oc " movl %a, %a\n" addressing addr' ireg res1; + fprintf oc " movl %a, %a\n" addressing addr ireg res2 + end + | Mfloat32, [FR res] -> + fprintf oc " movss %a, %a\n" addressing addr freg res + | Mfloat64, [FR res] -> + fprintf oc " movsd %a, %a\n" addressing addr freg res + | _ -> + assert false + + let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + begin match args with + | [IR addr] -> + print_builtin_vload_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + + let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + print_builtin_vload_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) res; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + + let print_builtin_vstore_common oc chunk addr src tmp = + match chunk, src with + | (Mint8signed | Mint8unsigned), [IR src] -> + if Asmgen.low_ireg src then + fprintf oc " movb %a, %a\n" ireg8 src addressing addr + else begin + fprintf oc " movl %a, %a\n" ireg src ireg tmp; + fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr + end + | (Mint16signed | Mint16unsigned), [IR src] -> + fprintf oc " movw %a, %a\n" ireg16 src addressing addr + | Mint32, [IR src] -> + fprintf oc " movl %a, %a\n" ireg src addressing addr + | Mint64, [IR src1; IR src2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + fprintf oc " movl %a, %a\n" ireg src2 addressing addr; + fprintf oc " movl %a, %a\n" ireg src1 addressing addr' + | Mfloat32, [FR src] -> + fprintf oc " movss %a, %a\n" freg src addressing addr + | Mfloat64, [FR src] -> + fprintf oc " movsd %a, %a\n" freg src addressing addr + | _ -> + assert false + + let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match args with + | IR addr :: src -> + print_builtin_vstore_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src + (if addr = EAX then ECX else EAX) + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + + let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + print_builtin_vstore_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +(* Handling of varargs *) let print_builtin_va_start oc r = if not (!current_function_sig).sig_cc.cc_vararg then @@ -360,6 +509,117 @@ module Target(System: SYSTEM):TARGET = fprintf oc " movl %%esp, 0(%a)\n" ireg r; fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r +(* Handling of compiler-inlined builtins *) + + let print_builtin_inline oc name args res = + fprintf oc "%s begin builtin %s\n" comment name; + begin match name, args, res with + (* Integer arithmetic *) + | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_bswap16", [IR a1], [IR res] -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_clz", [IR a1], [IR res] -> + fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; + fprintf oc " xorl $31, %a\n" ireg res + | "__builtin_ctz", [IR a1], [IR res] -> + fprintf oc " bsfl %a, %a\n" ireg a1 ireg res + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], [FR res] -> + need_masks := true; + if a1 <> res then + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res + | "__builtin_fsqrt", [FR a1], [FR res] -> + fprintf oc " sqrtsd %a, %a\n" freg a1 freg res + | "__builtin_fmax", [FR a1; FR a2], [FR res] -> + if res = a1 then + fprintf oc " maxsd %a, %a\n" freg a2 freg res + else if res = a2 then + fprintf oc " maxsd %a, %a\n" freg a1 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " maxsd %a, %a\n" freg a2 freg res + end + | "__builtin_fmin", [FR a1; FR a2], [FR res] -> + if res = a1 then + fprintf oc " minsd %a, %a\n" freg a2 freg res + else if res = a2 then + fprintf oc " minsd %a, %a\n" freg a1 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " minsd %a, %a\n" freg a2 freg res + end + | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"), + [FR a1; FR a2; FR a3], [FR res] -> + let opcode = + match name with + | "__builtin_fmadd" -> "vfmadd" + | "__builtin_fmsub" -> "vfmsub" + | "__builtin_fnmadd" -> "vfnmadd" + | "__builtin_fnmsub" -> "vfnmsub" + | _ -> assert false in + if res = a1 then + fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res + else if res = a2 then + fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res + else if res = a3 then + fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a3 freg res; + fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res + end + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); + fprintf oc " negl %a\n" ireg EAX; + fprintf oc " adcl $0, %a\n" ireg EDX; + fprintf oc " negl %a\n" ireg EDX + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + fprintf oc " addl %a, %a\n" ireg EBX ireg EAX; + fprintf oc " adcl %a, %a\n" ireg ECX ireg EDX + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + fprintf oc " subl %a, %a\n" ireg EBX ireg EAX; + fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + assert (a = EAX && b = EDX && rh = EDX && rl = EAX); + fprintf oc " mull %a\n" ireg EDX + (* Memory accesses *) + | "__builtin_read16_reversed", [IR a1], [IR res] -> + fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_read32_reversed", [IR a1], [IR res] -> + fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; + fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; + fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; + fprintf oc " bswap %a\n" ireg tmp; + fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + (* Synchronization *) + | "__builtin_membar", [], _ -> + () + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + end; + fprintf oc "%s end builtin %s\n" comment name (* Printing of instructions *) @@ -581,83 +841,36 @@ module Target(System: SYSTEM):TARGET = fprintf oc " ret\n" end (** Pseudo-instructions *) - | Padcl_ir (n,res) -> - fprintf oc " adcl $%ld, %a\n" (camlint_of_coqint n) ireg res; - | Padcl_rr (a1,res) -> - fprintf oc " adcl %a, %a\n" ireg a1 ireg res; - | Paddl (a1,res) -> - fprintf oc " addl %a, %a\n" ireg a1 ireg res; - | Paddl_mi (addr,n) -> - fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) addressing addr - | Paddl_ri (res,n) -> - fprintf oc " addl $%ld, %a\n" (camlint_of_coqint n) ireg res - | Pbsfl (a1,res) -> - fprintf oc " bsfl %a, %a\n" ireg a1 ireg res - | Pbslr (a1,res) -> - fprintf oc " bsrl %a, %a\n" ireg a1 ireg res - | Pbswap res -> - fprintf oc " bswap %a\n" ireg res - | Pcfi_adjust sz -> - cfi_adjust oc (camlint_of_coqint sz) - | Pfmadd132 (a1,a2,res) -> - fprintf oc " vfmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfmadd213 (a1,a2,res) -> - fprintf oc " vfmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfmadd231 (a1,a2,res) -> - fprintf oc " vfmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfmsub132 (a1,a2,res) -> - fprintf oc " vfmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfmsub213 (a1,a2,res) -> - fprintf oc " vfmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfmsub231 (a1,a2,res) -> - fprintf oc " vfmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfnmadd132 (a1,a2,res) -> - fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfnmadd213 (a1,a2,res) -> - fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfnmadd231 (a1,a2,res) -> - fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfnmsub132 (a1,a2,res) -> - fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfnmsub213 (a1,a2,res) -> - fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pfnmsub231 (a1,a2,res) -> - fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res - | Pmaxsd (a1,res) -> - fprintf oc " maxsd %a, %a\n" freg a1 freg res - | Pminsd (a1,res) -> - fprintf oc " minsd %a, %a\n" freg a1 freg res - | Pmovb_rm (r1,a) -> - fprintf oc " movb %a, %a\n" addressing a ireg8 r1 - | Pmovq_rm(rd, a) -> - fprintf oc " movq %a, %a\n" addressing a freg rd - | Pmovq_mr(a, r1) -> - fprintf oc " movq %a, %a\n" freg r1 addressing a - | Pmovsb -> - fprintf oc " movsb\n"; - | Pmovsw -> - fprintf oc " movsw\n"; - | Pmovw_rm (r1, a) -> - fprintf oc " movw %a, %a\n" addressing a ireg16 r1 - | Prep_movsl -> - fprintf oc " rep movsl\n" - | Prolw_8 res -> - fprintf oc " rolw $8, %a\n" ireg16 res - | Psbbl (a1,res) -> - fprintf oc " sbbl %a, %a\n" ireg a1 ireg res - | Psqrtsd (a1,res) -> - fprintf oc " sqrtsd %a, %a\n" freg a1 freg res - | Psubl_ri (res,n) -> - fprintf oc " subl $%ld, %a\n" (camlint_of_coqint n) ireg res; - | Pxchg (a1,a2) -> - fprintf oc " xchg %a, %a\n" ireg8 a1 high_ireg8 a2; | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(sz, ofs_ra, ofs_link) + | Pallocframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + let ofs_link = camlint_of_coqint ofs_link in + fprintf oc " subl $%ld, %%esp\n" sz; + cfi_adjust oc sz; + fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); + fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; + current_function_stacksize := sz | Pfreeframe(sz, ofs_ra, ofs_link) -> - assert false + let sz = sp_adjustment sz in + fprintf oc " addl $%ld, %%esp\n" sz | 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; diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index ec5a767f..699c841f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -19,10 +19,48 @@ open Integers open AST open Memdata open Asm -open Asmexpandaux +(* Buffering the expanded code *) -(* Useful constants and helper functions *) +let current_code = ref ([]: instruction list) + +let emit i = current_code := i :: !current_code + +let emit_loadimm r n = + List.iter emit (Asmgen.loadimm r n []) + +let emit_addimm rd rs n = + List.iter emit (Asmgen.addimm rd rs n []) + +let get_code () = + let c = List.rev !current_code in current_code := []; c + +(* Generation of fresh labels *) + +let dummy_function = { fn_code = []; fn_sig = signature_main } +let current_function = ref dummy_function +let next_label = ref (None : label option) + +let new_label () = + let lbl = + match !next_label with + | Some l -> l + | None -> + (* on-demand computation of the next available label *) + List.fold_left + (fun next instr -> + match instr with + | Plabel l -> if P.lt l next then next else P.succ l + | _ -> next) + P.one (!current_function).fn_code + in + next_label := Some (P.succ lbl); + lbl + +let set_current_function f = + current_function := f; next_label := None + +(* Useful constants *) let _0 = Integers.Int.zero let _1 = Integers.Int.one @@ -33,14 +71,6 @@ let _8 = coqint_of_camlint 8l let _m4 = coqint_of_camlint (-4l) let _m8 = coqint_of_camlint (-8l) -let emit_loadimm r n = - List.iter emit (Asmgen.loadimm r n []) - -let emit_addimm rd rs n = - List.iter emit (Asmgen.addimm rd rs n []) - - - (* Handling of annotations *) let expand_annot_val txt targ args res = @@ -503,8 +533,11 @@ let expand_instruction instr = let expand_function fn = set_current_function fn; + current_code := []; List.iter expand_instruction fn.fn_code; - get_current_function () + let c = get_code() in + set_current_function dummy_function; + { fn with fn_code = c } let expand_fundef = function | Internal f -> Internal (expand_function f) -- cgit