Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixed

13 files changed, 29 insertions, 103 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 4fb38ff8..d9901960 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -200,12 +200,9 @@ Inductive instruction : Type :=
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfadds: freg -> freg -> freg -> instruction               (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
-  | Pfcfi: freg -> ireg -> instruction                        (**r signed-int-to-float conversion (pseudo, PPC64) *)
   | Pfcfl: freg -> ireg -> instruction                        (**r signed-long-to-float conversion (pseudo, PPC64) *)
-  | Pfcfiu: freg -> ireg -> instruction                       (**r unsigned-int-to-float conversion (pseudo, PPC64) *)
   | Pfcfid: freg -> freg -> instruction                       (**r signed-long-to-float conversion (PPC64) *)
   | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion, round towards 0 (pseudo) *)
-  | Pfctiu: ireg -> freg -> instruction                       (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *)
   | Pfctid: ireg -> freg -> instruction                       (**r float-to-signed-int conversion, round towards 0 (pseudo, PPC64) *)
   | Pfctidz: freg -> freg -> instruction                      (**r float-to-signed-long conversion, round towards 0 (PPC64) *)
   | Pfctiw: freg -> freg -> instruction                       (**r float-to-signed-int conversion, round by default *)
@@ -825,16 +822,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m
   | Pfcmpu r1 r2 =>
       Next (nextinstr (compare_float rs rs#r1 rs#r2)) m
-  | Pfcfi rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m
   | Pfcfl rd r1 =>
       Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m
-  | Pfcfiu rd r1 =>
-      Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m
   | Pfcti rd r1 =>
       Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
-  | Pfctiu rd r1 =>
-      Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m
   | Pfctid rd r1 =>
       Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m
   | Pfdiv rd r1 r2 =>
@@ -1204,7 +1195,7 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
               (set_res res vres
-                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
+                (undef_regs (IR GPR0 :: map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 38f4bc75..1f32dd62 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -198,12 +198,9 @@ let pp_instructions pp ic =
   | Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3]
   | Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3]
   | Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2]
-  | Pfcfi (ir,fr)
   | Pfcfl (ir,fr) -> assert false (* Should not occur *)
   | Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2]
-  | Pfcfiu _ (* Should not occur *)
   | Pfcti _ (* Should not occur *)
-  | Pfctiu _ (* Should not occur *)
   | Pfctid _ -> assert false (* Should not occur *)
   | Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2]
   | Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2]
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index d8cbd94e..cb6a659f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -875,15 +875,6 @@ let expand_instruction instr =
         emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz)))
       else
         emit (Plwz(GPR1, Cint ofs, GPR1))
-  | Pfcfi(r1, r2) ->
-      assert (Archi.ppc64);
-      emit (Pextsw(GPR0, r2));
-      emit (Pstdu(GPR0, Cint _m8, GPR1));
-      emit (Pcfi_adjust _8);
-      emit (Plfd(r1, Cint _0, GPR1));
-      emit (Pfcfid(r1, r1));
-      emit (Paddi(GPR1, GPR1, Cint _8));
-      emit (Pcfi_adjust _m8)
   | Pfcfl(r1, r2) ->
       assert (Archi.ppc64);
       emit (Pstdu(r2, Cint _m8, GPR1));
@@ -892,15 +883,6 @@ let expand_instruction instr =
       emit (Pfcfid(r1, r1));
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
-  | Pfcfiu(r1, r2) ->
-      assert (Archi.ppc64);
-      emit (Prldicl(GPR0, r2, _0, _32));
-      emit (Pstdu(GPR0, Cint _m8, GPR1));
-      emit (Pcfi_adjust _8);
-      emit (Plfd(r1, Cint _0, GPR1));
-      emit (Pfcfid(r1, r1));
-      emit (Paddi(GPR1, GPR1, Cint _8));
-      emit (Pcfi_adjust _m8)
   | Pfcti(r1, r2) ->
       emit (Pfctiwz(FPR13, r2));
       emit (Pstfdu(FPR13, Cint _m8, GPR1));
@@ -908,14 +890,6 @@ let expand_instruction instr =
       emit (Plwz(r1, Cint _4, GPR1));
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
-  | Pfctiu(r1, r2) ->
-      assert (Archi.ppc64);
-      emit (Pfctidz(FPR13, r2));
-      emit (Pstfdu(FPR13, Cint _m8, GPR1));
-      emit (Pcfi_adjust _8);
-      emit (Plwz(r1, Cint _4, GPR1));
-      emit (Paddi(GPR1, GPR1, Cint _8));
-      emit (Pcfi_adjust _m8)
   | Pfctid(r1, r2) ->
       assert (Archi.ppc64);
       emit (Pfctidz(FPR13, r2));
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 29e2c028..d0c44f08 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -611,15 +611,6 @@ Definition transl_op
   | Ointoffloat, a1 :: nil =>
       do r1 <- freg_of a1; do r <- ireg_of res;
       OK (Pfcti r r1 :: k)
-  | Ointuoffloat, a1 :: nil =>
-      do r1 <- freg_of a1; do r <- ireg_of res;
-      OK (Pfctiu r r1 :: k)
-  | Ofloatofint, a1 :: nil =>
-      do r1 <- ireg_of a1; do r <- freg_of res;
-      OK (Pfcfi r r1 :: k)
-  | Ofloatofintu, a1 :: nil =>
-      do r1 <- ireg_of a1; do r <- freg_of res;
-      OK (Pfcfiu r r1 :: k)
   | Ofloatofwords, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res;
       OK (Pfmake r r1 r2 :: k)
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 21d5ce48..93589a31 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -789,16 +789,18 @@ Opaque loadind.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
   unfold nextinstr. rewrite Pregmap.gss.
-  rewrite set_res_other. rewrite undef_regs_other_2.
+  rewrite set_res_other. simpl. rewrite undef_regs_other_2.
+  rewrite Pregmap.gso by auto with asmgen.
   rewrite <- H1. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
   rewrite preg_notin_charact. intros. auto with asmgen.
   auto with asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
-  eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
+  eapply agree_undef_regs; eauto.
+  intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen.
   congruence.
   intros. Simpl. rewrite set_res_other by auto.
-  rewrite undef_regs_other_2; auto with asmgen.
+  simpl. rewrite undef_regs_other_2; auto with asmgen.
 
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 1b797999..850e95c7 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1500,18 +1500,6 @@ Opaque Val.add.
 - replace v with (Val.maketotal (Val.intoffloat (rs x))).
   TranslOpSimpl.
   rewrite H1; auto.
-  (* Ointuoffloat *)
-- replace v with (Val.maketotal (Val.intuoffloat (rs x))).
-  TranslOpSimpl.
-  rewrite H1; auto.
-  (* Ofloatofint *)
-- replace v with (Val.maketotal (Val.floatofint (rs x))).
-  TranslOpSimpl.
-  rewrite H1; auto.
-  (* Ofloatofintu *)
-- replace v with (Val.maketotal (Val.floatofintu (rs x))).
-  TranslOpSimpl.
-  rewrite H1; auto.
   (* Ocmp *)
 - destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto.
   exists rs'; auto with asmgen.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 07622a0e..9967bbae 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg :=
   | Ofloatconst _ => R12 :: nil
   | Osingleconst _ => R12 :: nil
   | Olongconst _ => R12 :: nil
-  | Ointoffloat | Ointuoffloat => F13 :: nil
+  | Ointoffloat => F13 :: nil
   | Olongoffloat => F13 :: nil
   | Oaddlimm _ => R12 :: nil
   | Oandlimm _ => R12 :: nil
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index 5ea09bd8..74ee6b85 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -61,7 +61,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Onegfs | Oabsfs => op1 (default nv)
   | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv)
   | Osingleoffloat | Ofloatofsingle => op1 (default nv)
-  | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv)
+  | Ointoffloat => op1 (default nv)
   | Ofloatofwords | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocmp c => needs_of_condition c
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 4f14bfac..3d84d95c 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -105,7 +105,7 @@ Inductive operation : Type :=
   | Osubl: operation                    (**r [rd = r1 - r2] *)
   | Onegl: operation                    (**r [rd = - r1] *)
   | Omull: operation                    (**r [rd = r1 * r2] *)
-  | Omullhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omullhs: operation                  (**r [rd = high part of r1 * r2, signed] *)
   | Omullhu: operation                  (**r [rd = high part of r1 * r2, unsigned] *)
   | Odivl: operation                    (**r [rd = r1 / r2] (signed) *)
   | Odivlu: operation                   (**r [rd = r1 / r2] (unsigned) *)
@@ -141,9 +141,6 @@ Inductive operation : Type :=
   | Ofloatofsingle: operation           (**r [rd] is [r1] extended to double-precision float *)
 (*c Conversions between int and float: *)
   | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
-  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *)
-  | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] (PPC64 only) *)
-  | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *)
   | Ofloatofwords: operation            (**r [rd = float_of_words(r1,r2)] *)
 (*c Manipulating 64-bit integers: *)
   | Omakelong: operation                (**r [rd = r1 << 32 | r2] *)
@@ -299,9 +296,6 @@ Definition eval_operation
   | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
   | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1)
   | Ointoffloat, v1::nil => Val.intoffloat v1
-  | Ointuoffloat, v1::nil => Val.intuoffloat v1
-  | Ofloatofint, v1::nil => Val.floatofint v1
-  | Ofloatofintu, v1::nil => Val.floatofintu v1
   | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2)
   | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
   | Olowlong, v1::nil => Some(Val.loword v1)
@@ -449,9 +443,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoffloat => (Tfloat :: nil, Tsingle)
   | Ofloatofsingle => (Tsingle :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
-  | Ointuoffloat => (Tfloat :: nil, Tint)
-  | Ofloatofint => (Tint :: nil, Tfloat)
-  | Ofloatofintu => (Tint :: nil, Tfloat)
   | Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
   | Omakelong => (Tint :: Tint :: nil, Tlong)
   | Olowlong => (Tlong :: nil, Tint)
@@ -570,9 +561,6 @@ Proof with (try exact I; try reflexivity).
   destruct v0...
   destruct v0...
   destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2...
-  destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2...
-  destruct v0; simpl in H0; inv H0...
-  destruct v0; simpl in H0; inv H0...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0...
@@ -1043,10 +1031,6 @@ Proof.
   inv H4; simpl; auto.
   inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2.
   exists (Vint i); auto.
-  inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2.
-  exists (Vint i); auto.
-  inv H4; simpl in H1; inv H1; simpl. TrivialExists.
-  inv H4; simpl in H1; inv H1; simpl. TrivialExists.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 52f4f855..fe8b5453 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -468,7 +468,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
 
 Definition intuoffloat (e: expr) :=
   if Archi.ppc64 then
-    Eop Ointuoffloat (e ::: Enil)
+    Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil)
   else
     Elet e
     (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
@@ -482,7 +482,8 @@ Nondetfunction floatofintu (e: expr) :=
       Eop (Ofloatconst (Float.of_intu n)) Enil
   | _ =>
       if Archi.ppc64 then
-        Eop Ofloatofintu (e ::: Enil)  else
+        Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil)
+      else
         subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
              (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
   end.
@@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) :=
       Eop (Ofloatconst (Float.of_int n)) Enil
   | _ =>
       if Archi.ppc64 then
-        Eop Ofloatofint (e ::: Enil) else
+        Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil)
+      else
         subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
                                  ::: addimm Float.ox8000_0000 e ::: Enil))
              (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 8135bad6..ed81c83f 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -855,8 +855,13 @@ Proof.
   destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
   exists (Vint n); split; auto. unfold intuoffloat.
   destruct Archi.ppc64.
-  econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto.
-  set (im := Int.repr Int.half_modulus).
+- apply Float.to_intu_to_long in Heqo.
+  econstructor. constructor. econstructor. econstructor; eauto. constructor.
+  simpl; rewrite Heqo; simpl; eauto. constructor.
+  simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto.
+  assert (Int.modulus < Int64.max_unsigned) by (compute; auto).
+  generalize (Int.unsigned_range n). omega.  
+- set (im := Int.repr Int.half_modulus).
   set (fm := Float.of_intu im).
   assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
     constructor. auto.
@@ -893,11 +898,12 @@ Theorem eval_floatofint:
 Proof.
   intros until y. unfold floatofint. destruct (floatofint_match a); intros.
   InvEval. TrivialExists.
-  destruct Archi.ppc64.
-  TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_int i)); split; auto.
-  set (t1 := addimm Float.ox8000_0000 a).
+  destruct Archi.ppc64.
+- rewrite Float.of_int_of_long.
+  EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
+- set (t1 := addimm Float.ox8000_0000 a).
   set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil).
   exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1.
@@ -917,12 +923,12 @@ Theorem eval_floatofintu:
 Proof.
   intros until y. unfold floatofintu. destruct (floatofintu_match a); intros.
   InvEval. TrivialExists.
-  destruct Archi.ppc64.
-  TrivialExists.
   rename e0 into a. destruct x; simpl in H0; inv H0.
   exists (Vfloat (Float.of_intu i)); split; auto.
-  unfold floatofintu.
-  set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
+  destruct Archi.ppc64.
+- rewrite Float.of_intu_of_long.
+  EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto.
+- set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)).
   set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil).
   exploit (eval_subf le t2).
   unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor.
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3ea03786..554bfe09 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -557,22 +557,16 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fadds	%a, %a, %a\n" freg r1 freg r2 freg r3
       | Pfcmpu(r1, r2) ->
           fprintf oc "	fcmpu	%a, %a, %a\n" creg 0 freg r1 freg r2
-      | Pfcfi(r1, r2) ->
-          assert false
       | Pfcfl(r1, r2) ->
           assert false
       | Pfcfid(r1, r2) ->
           fprintf oc "	fcfid	%a, %a\n" freg r1 freg r2
-      | Pfcfiu(r1, r2) ->
-          assert false
       | Pfcti(r1, r2) ->
           assert false
       | Pfctid(r1, r2) ->
           assert false
       | Pfctidz(r1, r2) ->
           fprintf oc "	fctidz	%a, %a\n" freg r1 freg r2
-      | Pfctiu(r1, r2) ->
-          assert false
       | Pfctiw(r1, r2) ->
           fprintf oc "	fctiw	%a, %a\n" freg r1 freg r2
       | Pfctiwz(r1, r2) ->
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index a270d857..c81f1a6c 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -133,9 +133,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoffloat, v1::nil => singleoffloat v1
   | Ofloatofsingle, v1::nil => floatofsingle v1
   | Ointoffloat, v1::nil => intoffloat v1
-  | Ointuoffloat, v1::nil => intuoffloat v1
-  | Ofloatofint, v1::nil => floatofint v1
-  | Ofloatofintu, v1::nil => floatofintu v1
   | Ofloatofwords, v1::v2::nil => floatofwords v1 v2
   | Omakelong, v1::v2::nil => longofwords v1 v2
   | Olowlong, v1::nil => loword v1