aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/Asmexpand.ml7
-rw-r--r--cfrontend/C2C.ml4
-rw-r--r--common/Builtins0.v24
-rw-r--r--doc/ccomp.12
-rw-r--r--powerpc/Asmexpand.ml28
-rw-r--r--powerpc/ConstpropOp.vp1
-rw-r--r--powerpc/ConstpropOpproof.v2
-rw-r--r--riscV/CBuiltins.ml3
-rw-r--r--x86/CBuiltins.ml2
9 files changed, 60 insertions, 13 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index d9424d11..89aab5c7 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -18,7 +18,7 @@ open Asm
open Asmexpandaux
open AST
open Camlcoq
-open Integers
+open! Integers
exception Error of string
@@ -304,6 +304,11 @@ let expand_builtin_va_start r =
let expand_builtin_inline name args res =
match name, args, res with
(* Integer arithmetic *)
+ | "__builtin_bswap64" , [BA_splitlong(BA(IR ah), BA(IR al))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
+ expand_int64_arith (rl = al) rl (fun rl ->
+ emit (Prev (rl, ah));
+ emit (Prev (rh, al)))
| ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
emit (Prev (res, a1))
| "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2e6bbe67..c1dfa9f4 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -161,7 +161,9 @@ let builtins_generic = {
@
[
(* Integer arithmetic *)
- "__builtin_bswap",
+ "__builtin_bswap64",
+ (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
+ "__builtin_bswap",
(TInt(IUInt, []), [TInt(IUInt, [])], false);
"__builtin_bswap32",
(TInt(IUInt, []), [TInt(IUInt, [])], false);
diff --git a/common/Builtins0.v b/common/Builtins0.v
index c6a299d9..b78006dd 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -16,7 +16,7 @@
(** Associating semantics to built-in functions *)
Require Import String Coqlib.
-Require Import AST Integers Floats Values.
+Require Import AST Integers Floats Values Memdata.
(** This module provides definitions and mechanisms to associate semantics
with names of built-in functions.
@@ -337,6 +337,9 @@ Inductive standard_builtin : Type :=
| BI_addl
| BI_subl
| BI_mull
+ | BI_i16_bswap
+ | BI_i32_bswap
+ | BI_i64_bswap
| BI_i64_umulh
| BI_i64_smulh
| BI_i64_sdiv
@@ -366,6 +369,10 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
:: ("__builtin_addl", BI_addl)
:: ("__builtin_subl", BI_subl)
:: ("__builtin_mull", BI_mull)
+ :: ("__builtin_bswap16", BI_i16_bswap)
+ :: ("__builtin_bswap", BI_i32_bswap)
+ :: ("__builtin_bswap32", BI_i32_bswap)
+ :: ("__builtin_bswap64", BI_i64_bswap)
:: ("__compcert_i64_umulh", BI_i64_umulh)
:: ("__compcert_i64_smulh", BI_i64_smulh)
:: ("__compcert_i64_sdiv", BI_i64_sdiv)
@@ -396,6 +403,12 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
| BI_mull =>
mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+ | BI_i32_bswap =>
+ mksignature (Tint :: nil) (Some Tint) cc_default
+ | BI_i64_bswap =>
+ mksignature (Tlong :: nil) (Some Tlong) cc_default
+ | BI_i16_bswap =>
+ mksignature (Tint :: nil) (Some Tint) cc_default
| BI_i64_shl | BI_i64_shr | BI_i64_sar =>
mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default
| BI_i64_dtos | BI_i64_dtou =>
@@ -420,6 +433,15 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (pro
| BI_addl => mkbuiltin_v2t Tlong Val.addl _ _
| BI_subl => mkbuiltin_v2t Tlong Val.subl _ _
| BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _
+ | BI_i16_bswap =>
+ mkbuiltin_n1t Tint Tint
+ (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n)))))
+ | BI_i32_bswap =>
+ mkbuiltin_n1t Tint Tint
+ (fun n => Int.repr (decode_int (List.rev (encode_int 4%nat (Int.unsigned n)))))
+ | BI_i64_bswap =>
+ mkbuiltin_n1t Tlong Tlong
+ (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
| BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
| BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
| BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _
diff --git a/doc/ccomp.1 b/doc/ccomp.1
index f4919867..89e8c823 100644
--- a/doc/ccomp.1
+++ b/doc/ccomp.1
@@ -485,7 +485,7 @@ Disabled by default.
.sp
\fIunused\-variable\fP:
Unused local variables.
-Enabled by default.
+Disabled by default.
.sp
\fIvarargs\fP:
Promotable vararg arguments.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 415b6651..704b0aba 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -14,7 +14,7 @@
of the PPC assembly code. *)
open Camlcoq
-open Integers
+open! Integers
open AST
open Asm
open Asmexpandaux
@@ -30,8 +30,8 @@ let eref =
(* Useful constants and helper functions *)
-let _0 = Integers.Int.zero
-let _1 = Integers.Int.one
+let _0 = Int.zero
+let _1 = Int.one
let _2 = coqint_of_camlint 2l
let _4 = coqint_of_camlint 4l
let _6 = coqint_of_camlint 6l
@@ -45,7 +45,7 @@ let _m4 = coqint_of_camlint (-4l)
let _m8 = coqint_of_camlint (-8l)
let _m16 = coqint_of_camlint (-16l)
-let _0L = Integers.Int64.zero
+let _0L = Int64.zero
let _32L = coqint_of_camlint64 32L
let _64L = coqint_of_camlint64 64L
let _m1L = coqint_of_camlint64 (-1L)
@@ -554,6 +554,26 @@ let expand_builtin_inline name args res =
emit (Plabel lbl2)
| "__builtin_cmpb", [BA(IR a1); BA(IR a2)], BR(IR res) ->
emit (Pcmpb (res,a1,a2))
+ | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))],
+ BR_splitlong(BR(IR rh), BR(IR rl))->
+ assert (not Archi.ppc64);
+ emit (Pstwu(ah, Cint _m8, GPR1));
+ emit (Pcfi_adjust _8);
+ emit (Pstwu(al, Cint _m8, GPR1));
+ emit (Pcfi_adjust _8);
+ emit (Plwbrx(rh, GPR0, GPR1));
+ emit (Paddi(GPR1, GPR1, Cint _8));
+ emit (Pcfi_adjust _m8);
+ emit (Plwbrx(rl, GPR0, GPR1));
+ emit (Paddi(GPR1, GPR1, Cint _8));
+ emit (Pcfi_adjust _m8)
+ | "__builtin_bswap64", [BA(IR a1)], BR(IR res) ->
+ assert (Archi.ppc64);
+ emit (Pstdu(a1, Cint _m8, GPR1));
+ emit (Pcfi_adjust _8);
+ emit (Pldbrx(res, GPR0, GPR1));
+ emit (Paddi(GPR1, GPR1, Cint _8));
+ emit (Pcfi_adjust _m8)
| ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
emit (Pstwu(a1, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index cf1dc6e8..8e90a849 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -23,6 +23,7 @@ Require Import ValueDomain ValueAOp.
Definition const_for_result (a: aval) : option operation :=
match a with
| I n => Some(Ointconst n)
+ | L n => if Archi.ppc64 then Some (Olongconst n) else None
| F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
| FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
| Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs)
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 38daefe4..8687b056 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -101,6 +101,8 @@ Proof.
destruct a; inv H; SimplVM.
- (* integer *)
exists (Vint n); auto.
+- (* long *)
+ destruct (Archi.ppc64); inv H2. exists (Vlong n); auto.
- (* float *)
destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto.
- (* single *)
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index edaf586d..a2087cb7 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -25,9 +25,6 @@ let builtins = {
(* Synchronization *)
"__builtin_fence",
(TVoid [], [], false);
- (* Integer arithmetic *)
- "__builtin_bswap64",
- (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
(* Float arithmetic *)
"__builtin_fmadd",
(TFloat(FDouble, []),
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 6fb8b697..f4f40a31 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -31,8 +31,6 @@ let builtins = {
];
builtin_functions = [
(* Integer arithmetic *)
- "__builtin_bswap64",
- (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
"__builtin_clz",
(TInt(IInt, []), [TInt(IUInt, [])], false);
"__builtin_clzl",
generated by cgit (git 2.34.1) at 2024-07-09 19:56:48 +0000