Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

3 files changed, 29 insertions, 7 deletions

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/common/Separation.v b/common/Separation.v
index 1493b535..27065d1f 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -113,7 +113,7 @@ Proof.
   intros P Q [[A B] [C D]]. split; auto.
 Qed.
 
-Hint Resolve massert_imp_refl massert_eqv_refl.
+Hint Resolve massert_imp_refl massert_eqv_refl : core.
 
 (** * Separating conjunction *)
 
diff --git a/common/Values.v b/common/Values.v
index e4297183..59e6388f 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -1950,7 +1950,7 @@ Inductive lessdef_list: list val -> list val -> Prop :=
       lessdef v1 v2 -> lessdef_list vl1 vl2 ->
       lessdef_list (v1 :: vl1) (v2 :: vl2).
 
-Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.
+Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons : core.
 
 Lemma lessdef_list_inv:
   forall vl1 vl2, lessdef_list vl1 vl2 -> vl1 = vl2 \/ In Vundef vl1.
@@ -2175,7 +2175,7 @@ Inductive inject (mi: meminj): val -> val -> Prop :=
   | val_inject_undef: forall v,
       inject mi Vundef v.
 
-Hint Constructors inject.
+Hint Constructors inject : core.
 
 Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
   | inject_list_nil :
@@ -2184,7 +2184,7 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:=
       inject mi v v' -> inject_list mi vl vl'->
       inject_list mi (v :: vl) (v' :: vl').
 
-Hint Resolve inject_list_nil inject_list_cons.
+Hint Resolve inject_list_nil inject_list_cons : core.
 
 Lemma inject_ptrofs:
   forall mi i, inject mi (Vptrofs i) (Vptrofs i).
@@ -2192,7 +2192,7 @@ Proof.
   unfold Vptrofs; intros. destruct Archi.ptr64; auto.
 Qed.
 
-Hint Resolve inject_ptrofs.
+Hint Resolve inject_ptrofs : core.
 
 Section VAL_INJ_OPS.
 
@@ -2495,7 +2495,7 @@ Proof.
   constructor. eapply val_inject_incr; eauto. auto.
 Qed.
 
-Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr.
+Hint Resolve inject_incr_refl val_inject_incr val_inject_list_incr : core.
 
 Lemma val_inject_lessdef:
   forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2.