diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
| commit | d5b86a98560c36fbcb3ab8d2698e09147acda512 (patch) | |
| tree | f3ab850a1620fa5d3dbbe439998d09de8e0d817d /arm/Asmexpand.ml | |
| parent | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (diff) | |
| parent | 3872ce9f9806d9af334b1fde092145edf664d170 (diff) | |
| download | compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.tar.gz compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.zip | |
Merge branch 'master' into add-file
Diffstat (limited to 'arm/Asmexpand.ml')
| -rw-r--r-- | arm/Asmexpand.ml | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 8aef64e4..855ca9ad 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -30,6 +30,9 @@ let _2 = coqint_of_camlint 2l let _4 = coqint_of_camlint 4l let _8 = coqint_of_camlint 8l let _16 = coqint_of_camlint 16l +let _32 = coqint_of_camlint 32l +let _64 = coqint_of_camlint 64l +let _m1 = coqint_of_camlint (-1l) (* Emit instruction sequences that set or offset a register by a constant. *) (* No S suffix because they are applied to SP most of the time. *) @@ -294,6 +297,33 @@ let expand_builtin_inline name args res = emit (Pmovite (TCeq, IR14, SOreg IR14, SOimm _0)); emit (Pclz (res, ah)); emit (Padd (res, res, SOreg IR14)) + | ("__builtin_ctz" | "__builtin_ctzl"), [BA(IR a1)], BR(IR res) -> + emit (Padd(IR14, a1, SOimm _m1)); (* tmp := x-1 *) + emit (Pmvn(res, SOreg a1)); (* res := ~(x) *) + emit (Pand(res, IR14, SOreg res)); (* res := tmp & ~(x) *) + emit (Pclz(res, res)); (* res := #leading zeros *) + emit (Prsb(res, res, SOimm _32)) (* res := 32 - #leading zeros *) + | "__builtin_ctzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) -> + let lbl1 = new_label () in + let lbl2 = new_label () in + (* low word equal to zero? *) + emit (Pcmp (al, SOimm _0)); + emit (Pbne lbl1); + (* low word is zero, count trailing zeros in high word and increment by 32 *) + emit (Padd(IR14, ah, SOimm _m1)); + emit (Pmvn(res, SOreg ah)); + emit (Pand(res, IR14, SOreg res)); + emit (Pclz(res, res)); + emit (Prsb(res, res, SOimm _64)); + emit (Pb lbl2); + (* count trailing zeros in low word *) + emit (Plabel lbl1); + emit (Padd(IR14, al, SOimm _m1)); + emit (Pmvn(res, SOreg al)); + emit (Pand(res, IR14, SOreg res)); + emit (Pclz(res, res)); + emit (Prsb(res, res, SOimm _32)); + emit (Plabel lbl2) (* Float arithmetic *) | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> emit (Pfabsd (res,a1)) |