diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/Asm.v | 52 | ||||
-rw-r--r-- | ia32/Asmexpand.ml | 157 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 46 |
3 files changed, 253 insertions, 2 deletions
@@ -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) -> |