diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-12-22 11:06:35 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-12-22 11:06:35 +0100 |
| commit | f531d386db7051761bd31f2740a893ff97ce65aa (patch) | |
| tree | 0e0d535d0e36927500441de21ac727dc1677ac4b /ia32 | |
| parent | 12b5eaf144285de569be7123913ee78f17dd9b03 (diff) | |
| download | compcert-f531d386db7051761bd31f2740a893ff97ce65aa.tar.gz compcert-f531d386db7051761bd31f2740a893ff97ce65aa.zip | |
Add CLZ builtins for ARM and IA32
ARM: add __builtin_clzl, __builtin_clzll
IA32: add __builtin_clzl, __builtin_clzll,
__builtin_ctzl, __builtin_ctzll
Add corresponding tests in tests/regression/
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asmexpand.ml | 27 | ||||
| -rw-r--r-- | ia32/CBuiltins.ml | 8 |
2 files changed, 33 insertions, 2 deletions
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index d7b554dc..7ca31902 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -245,11 +245,34 @@ let expand_builtin_inline name args res = if a1 <> res then emit (Pmov_rr (res,a1)); emit (Pbswap16 res) - | "__builtin_clz", [BA(IR a1)], BR(IR res) -> + | ("__builtin_clz"|"__builtin_clzl"), [BA(IR a1)], BR(IR res) -> emit (Pbsr (res,a1)); emit (Pxor_ri(res,coqint_of_camlint 31l)) - | "__builtin_ctz", [BA(IR a1)], BR(IR res) -> + | "__builtin_clzll", [BA_splitlong(BA (IR ah), BA (IR al))], BR(IR res) -> + let lbl1 = new_label() in + let lbl2 = new_label() in + emit (Ptest_rr(ah, ah)); + emit (Pjcc(Cond_e, lbl1)); + emit (Pbsr(res, ah)); + emit (Pxor_ri(res, coqint_of_camlint 31l)); + emit (Pjmp_l lbl2); + emit (Plabel lbl1); + emit (Pbsr(res, al)); + emit (Pxor_ri(res, coqint_of_camlint 63l)); + emit (Plabel lbl2) + | ("__builtin_ctz" | "__builtin_ctzl"), [BA(IR a1)], BR(IR res) -> emit (Pbsf (res,a1)) + | "__builtin_ctzll", [BA_splitlong(BA (IR ah), BA (IR al))], BR(IR res) -> + let lbl1 = new_label() in + let lbl2 = new_label() in + emit (Ptest_rr(al, al)); + emit (Pjcc(Cond_e, lbl1)); + emit (Pbsf(res, al)); + emit (Pjmp_l lbl2); + emit (Plabel lbl1); + emit (Pbsf(res, ah)); + emit (Padd_ri(res, coqint_of_camlint 32l)); + emit (Plabel lbl2) (* Float arithmetic *) | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> if a1 <> res then diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index 802588d4..79a839f3 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -31,8 +31,16 @@ let builtins = { (TInt(IUShort, []), [TInt(IUShort, [])], false); "__builtin_clz", (TInt(IInt, []), [TInt(IUInt, [])], false); + "__builtin_clzl", + (TInt(IInt, []), [TInt(IULong, [])], false); + "__builtin_clzll", + (TInt(IInt, []), [TInt(IULongLong, [])], false); "__builtin_ctz", (TInt(IInt, []), [TInt(IUInt, [])], false); + "__builtin_ctzl", + (TInt(IInt, []), [TInt(IULong, [])], false); + "__builtin_ctzll", + (TInt(IInt, []), [TInt(IULongLong, [])], false); (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); |