From 601569c2e0c9ec4748eefcbdb9f62c93f8aa822c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Sep 2010 09:28:33 +0000 Subject: Support for __builtin_fmax and __builtin_fmin git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/CBuiltins.ml | 4 ++++ ia32/PrintAsm.ml | 19 ++++++++++++++++++- 2 files changed, 22 insertions(+), 1 deletion(-) (limited to 'ia32') diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index d077fe5..14a2f10 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -24,5 +24,9 @@ let builtins = { (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_fmax", + (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); + "__builtin_fmin", + (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); ] } diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index e75032c..f614e97 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -241,7 +241,24 @@ let print_builtin_inlined oc name args 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 - (* Also: fmax, fmin *) + | "__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 " movsd %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 " movsd %a, %a\n" freg a1 freg res; + fprintf oc " minsd %a, %a\n" freg a2 freg res + end | _ -> invalid_arg ("unrecognized builtin " ^ name) end; -- cgit v1.2.3