diff options
| -rw-r--r-- | aarch64/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | arm/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
| -rw-r--r-- | common/Builtins0.v | 1 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | riscV/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | x86/Asmexpand.ml | 2 |
7 files changed, 8 insertions, 5 deletions
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 02c27053..ea2ee703 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -353,7 +353,7 @@ let expand_builtin_inline name args res = emit (Prbit(X, res, a1)); emit (Pclz(X, res, res)) (* Float arithmetic *) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(D, res, a1)) | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfmadd(D, res, a1, a2, a3)) diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index e1e72dbc..f4e79a37 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -349,7 +349,7 @@ let expand_builtin_inline name args res = emit (Prsb(res, res, SOimm _32)); emit (Plabel lbl2) (* Float arithmetic *) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Pfsqrt (res,a1)) (* 64-bit integer arithmetic *) | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c7cd4937..2386eed9 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -200,6 +200,8 @@ let builtins_generic = { (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_sqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], diff --git a/common/Builtins0.v b/common/Builtins0.v index 4afe6f1a..d84c9112 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -367,6 +367,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_fabs", BI_fabs) :: ("__builtin_fabsf", BI_fabsf) :: ("__builtin_fsqrt", BI_fsqrt) + :: ("__builtin_sqrt", BI_fsqrt) :: ("__builtin_negl", BI_negl) :: ("__builtin_addl", BI_addl) :: ("__builtin_subl", BI_subl) diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 9b7c3cc7..d8cbd94e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -594,7 +594,7 @@ let expand_builtin_inline name args res = emit (Pfnmadd(res, a1, a2, a3)) | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfnmsub(res, a1, a2, a3)) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(res, a1)) | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) -> emit (Pfrsqrte(res, a1)) diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 96fd3766..810514a3 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -528,7 +528,7 @@ let expand_builtin_inline name args res = assert (al = X5 && ah = X6 && res = X7); expand_ctz ~sixtyfour:false ~splitlong:true (* Float arithmetic *) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Pfsqrtd(res, a1)) | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfmaddd(res, a1, a2, a3)) diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index e4cf028f..caa9775a 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -378,7 +378,7 @@ let expand_builtin_inline name args res = emit (Paddl_ri(res, coqint_of_camlint 32l)); emit (Plabel lbl2) (* Float arithmetic *) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Psqrtsd (res,a1)) | "__builtin_fmax", [BA(FR a1); BA(FR a2)], BR(FR res) -> if res = a1 then |