diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-04 09:28:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-04 09:28:33 +0000 |
| commit | 601569c2e0c9ec4748eefcbdb9f62c93f8aa822c (patch) | |
| tree | f32d726929b2d24eaa015d2a8f62b3600c471a08 | |
| parent | 4c36fcb770cf8e45bb6a23c8a176f61c1fbfd605 (diff) | |
Support for __builtin_fmax and __builtin_fmin
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | ia32/CBuiltins.ml | 4 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 19 |
2 files changed, 22 insertions, 1 deletions
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; |