From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 13 Jun 2011 18:11:19 +0000 Subject: Revised handling of annotation statements, and more generally built-in functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/PrintAsm.ml | 122 +++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 82 insertions(+), 40 deletions(-) (limited to 'ia32/PrintAsm.ml') diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 9facf85..c9ee970 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -17,6 +17,7 @@ open Datatypes open Camlcoq open Sections open AST +open Memdata open Asm (* Recognition of target ABI and asm syntax *) @@ -217,20 +218,20 @@ let need_masks = ref false (* Built-in functions *) -(* Built-ins. They come in two flavors: +(* Built-ins. They come in three 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 - inlined while printing asm code; take their arguments in locations dictated by the calling conventions; preserve callee-save regs only. *) -(* Handling of __builtin_annotation *) - -let re_builtin_annotation = Str.regexp "__builtin_annotation_\"\\(.*\\)\"$" +(* Handling of annotations *) let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -let print_annotation oc txt args res = +let print_annot_text print_arg oc txt args = fprintf oc "%s annotation: " comment; let print_fragment = function | Str.Text s -> @@ -240,28 +241,36 @@ let print_annotation oc txt args res = | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - preg oc (List.nth args (n-1)) + print_arg oc (List.nth args (n-1)) with Failure _ -> fprintf oc "" s in List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n"; + fprintf oc "\n" + +let print_annot_stmt oc txt args = + let print_annot_param oc = function + | APreg r -> preg oc r + | APstack(chunk, ofs) -> + fprintf oc "mem(ESP + %a, %a)" coqint ofs coqint (size_chunk chunk) in + print_annot_text print_annot_param oc txt args + +let print_annot_val oc txt args res = + print_annot_text 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 " movsd %a, %a\n" freg src freg dst | _, _ -> assert false -(* Handling of __builtin_memcpy_alX_szY *) - -let re_builtin_memcpy = - Str.regexp "__builtin_memcpy\\(_al\\([248]\\)\\)?_sz\\([0-9]+\\)$" +(* Handling of memcpy *) (* Unaligned memory accesses are quite fast on IA32, so use large memory accesses regardless of alignment. *) -let print_builtin_memcpy oc sz dst src = +let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in let tmp = if src <> ECX && dst <> ECX then ECX else if src <> EDX && dst <> EDX then EDX @@ -284,54 +293,73 @@ let print_builtin_memcpy oc sz dst src = fprintf oc " movb %a, %d(%a)\n" ireg8 tmp ofs ireg dst; copy (ofs + 1) (sz - 1) end in + fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n" + comment sz al; if tmp = EAX && sz mod 4 <> 0 then fprintf oc " movd %a, %a\n" ireg EAX freg XMM7; copy 0 sz; if tmp = EAX && sz mod 4 <> 0 then - fprintf oc " movd %a, %a\n" freg XMM7 ireg EAX + fprintf oc " movd %a, %a\n" freg XMM7 ireg EAX; + fprintf oc "%s end builtin __builtin_memcpy\n" comment -(* Handling of compiler-inlined builtins *) +(* Handling of volatile reads and writes *) -let print_builtin_inlined oc name args res = - fprintf oc "%s begin builtin %s\n" comment name; - begin match name, args, res with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> +let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + begin match chunk, args, res with + | Mint8unsigned, [IR addr], IR res -> fprintf oc " movzbl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + | Mint8signed, [IR addr], IR res -> fprintf oc " movsbl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + | Mint16unsigned, [IR addr], IR res -> fprintf oc " movzwl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + | Mint16signed, [IR addr], IR res -> fprintf oc " movswl 0(%a), %a\n" ireg addr ireg res - | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + | Mint32, [IR addr], IR res -> fprintf oc " movl 0(%a), %a\n" ireg addr ireg res - | "__builtin_volatile_read_float32", [IR addr], FR res -> + | Mfloat32, [IR addr], FR res -> fprintf oc " cvtss2sd 0(%a), %a\n" ireg addr freg res - | "__builtin_volatile_read_float64", [IR addr], FR res -> + | Mfloat64, [IR addr], FR res -> fprintf oc " movsd 0(%a), %a\n" ireg addr freg res - (* Volatile writes *) - | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + +let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match chunk, args with + | (Mint8signed | Mint8unsigned), [IR addr; IR src] -> if Asmgen.low_ireg src then fprintf oc " movb %a, 0(%a)\n" ireg8 src ireg addr else begin fprintf oc " movl %a, %%ecx\n" ireg src; fprintf oc " movb %%cl, 0(%a)\n" ireg addr end - | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + | (Mint16signed | Mint16unsigned), [IR addr; IR src] -> if Asmgen.low_ireg src then fprintf oc " movw %a, 0(%a)\n" ireg16 src ireg addr else begin fprintf oc " movl %a, %%ecx\n" ireg src; fprintf oc " movw %%cx, 0(%a)\n" ireg addr end - | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + | Mint32, [IR addr; IR src] -> fprintf oc " movl %a, 0(%a)\n" ireg src ireg addr - | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + | Mfloat32, [IR addr; FR src] -> fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src; fprintf oc " movss %%xmm7, 0(%a)\n" ireg addr - | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + | Mfloat64, [IR addr; FR src] -> fprintf oc " movsd %a, 0(%a)\n" freg src ireg addr + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +(* 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 (* Memory accesses *) | "__builtin_read_int16_reversed", [IR a1], IR res -> let tmp = if Asmgen.low_ireg res then res else ECX in @@ -380,10 +408,6 @@ let print_builtin_inlined oc name args res = fprintf oc " movsd %a, %a\n" freg a1 freg res; fprintf oc " minsd %a, %a\n" freg a2 freg res end - (* Inlined memcpy *) - | name, [IR dst; IR src], _ when Str.string_match re_builtin_memcpy name 0 -> - let sz = int_of_string (Str.matched_group 3 name) in - print_builtin_memcpy oc sz dst src (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -655,10 +679,28 @@ let print_instruction oc = function let sz = sp_adjustment sz in fprintf oc " addl $%ld, %%esp\n" sz | Pbuiltin(ef, args, res) -> - let name = extern_atom ef.ef_id in - if Str.string_match re_builtin_annotation name 0 - then print_annotation oc (Str.matched_group 1 name) args res - else print_builtin_inlined oc name 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_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 + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) args + | _ -> + assert false + end let print_literal oc (lbl, n) = fprintf oc "%a: .quad 0x%Lx\n" label lbl n -- cgit v1.2.3