Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore utilisee dans le front-end C.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 55 insertions, 4 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index df541a11..c1e3bd18 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -50,7 +50,8 @@ Inductive unary_operation : Set :=
   | Onegf: unary_operation                 (**r float opposite *)
   | Oabsf: unary_operation                 (**r float absolute value *)
   | Osingleoffloat: unary_operation        (**r float truncation *)
-  | Ointoffloat: unary_operation           (**r integer to float *)
+  | Ointoffloat: unary_operation           (**r signed integer to float *)
+  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
   | Ofloatofint: unary_operation           (**r float to signed integer *)
   | Ofloatofintu: unary_operation.         (**r float to unsigned integer *)
 
@@ -239,6 +240,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Oabsf, Vfloat f1 => Some (Vfloat (Float.abs f1))
   | Osingleoffloat, _ => Some (Val.singleoffloat arg)
   | Ointoffloat, Vfloat f1 => Some (Vint (Float.intoffloat f1))
+  | Ointuoffloat, Vfloat f1 => Some (Vint (Float.intuoffloat f1))
   | Ofloatofint, Vint n1 => Some (Vfloat (Float.floatofint n1))
   | Ofloatofintu, Vint n1 => Some (Vfloat (Float.floatofintu n1))
   | _, _ => None
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 18fa589f..e7feb101 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -259,6 +259,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => I(Float.intoffloat n1)
+  | Ointuoffloat, F n1 :: nil => I(Float.intuoffloat n1)
   | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
   | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
   | Ocmp c, vl =>
@@ -412,6 +413,9 @@ Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx),
   | eval_static_operation_case49:
       forall n1,
       eval_static_operation_cases (Ocast16unsigned) (I n1 :: nil)
+  | eval_static_operation_case50:
+      forall n1,
+      eval_static_operation_cases (Ointuoffloat) (F n1 :: nil)
   | eval_static_operation_default:
       forall (op: operation) (vl: list approx),
       eval_static_operation_cases op vl.
@@ -512,6 +516,8 @@ Definition eval_static_operation_match (op: operation) (vl: list approx) :=
       eval_static_operation_case48 n1
   | Ocast16unsigned, I n1 :: nil =>
       eval_static_operation_case49 n1
+  | Ointuoffloat, F n1 :: nil =>
+      eval_static_operation_case50 n1
   | op, vl =>
       eval_static_operation_default op vl
   end.
@@ -615,6 +621,8 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       I(Int.cast8unsigned n1)
   | eval_static_operation_case49 n1 =>
       I(Int.cast16unsigned n1)
+  | eval_static_operation_case50 n1 =>
+      I(Float.intuoffloat n1)
   | eval_static_operation_default op vl =>
       Unknown
   end.
diff --git a/backend/Op.v b/backend/Op.v
index 51b5e530..2094d597 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -94,7 +94,8 @@ Inductive operation : Set :=
   | Omulsubf: operation                 (**r [rd = r1 * r2 - r3] *)
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
 (*c Conversions between int and float: *)
-  | Ointoffloat: operation              (**r [rd = int_of_float(r1)] *)
+  | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
+  | Ointuoffloat: operation             (**r [rd = unsigned_int_of_float(r1)] *)
   | Ofloatofint: operation              (**r [rd = float_of_signed_int(r1)] *)
   | Ofloatofintu: operation             (**r [rd = float_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
@@ -229,6 +230,8 @@ Definition eval_operation
       Some (Val.singleoffloat v1)
   | Ointoffloat, Vfloat f1 :: nil => 
       Some (Vint (Float.intoffloat f1))
+  | Ointuoffloat, Vfloat f1 :: nil => 
+      Some (Vint (Float.intuoffloat f1))
   | Ofloatofint, Vint n1 :: nil => 
       Some (Vfloat (Float.floatofint n1))
   | Ofloatofintu, Vint n1 :: nil => 
@@ -506,6 +509,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat)
   | Osingleoffloat => (Tfloat :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
+  | Ointuoffloat => (Tfloat :: nil, Tint)
   | Ofloatofint => (Tint :: nil, Tfloat)
   | Ofloatofintu => (Tint :: nil, Tfloat)
   | Ocmp c => (type_of_condition c, Tint)
@@ -666,6 +670,7 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Omulsubf, v1::v2::v3::nil => Val.subf (Val.mulf v1 v2) v3
   | Osingleoffloat, v1::nil => Val.singleoffloat 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
   | Ocmp c, _ => eval_condition_total c vl
diff --git a/backend/PPC.v b/backend/PPC.v
index 7a330639..cfd07405 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -125,7 +125,8 @@ Inductive instruction : Set :=
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
-  | Pfcti: ireg -> freg -> instruction                        (**r float-to-int conversion *)
+  | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion *)
+  | Pfctiu: ireg -> freg -> instruction                       (**r float-to-unsigned-int conversion *)
   | Pfdiv: freg -> freg -> freg -> instruction                (**r float division *)
   | Pfmadd: freg -> freg -> freg -> freg -> instruction       (**r float multiply-add *)
   | Pfmr: freg -> freg -> instruction                         (**r float move *)
@@ -199,7 +200,7 @@ lbl:    .double floatcst
 >>
   Initialized data in the constant data section are not modeled here,
   which is why we use a pseudo-instruction for this purpose.
-- [Pfcti]: convert a float to an integer.  This requires a transfer
+- [Pfcti]: convert a float to a signed integer.  This requires a transfer
   via memory of a 32-bit integer from a float register to an int register,
   which our memory model cannot express.  Expands to:
 <<
@@ -208,6 +209,30 @@ lbl:    .double floatcst
         lwz     rdst, 4(r1)
         addi    r1, r1, 8
 >>
+- [Pfctiu]: convert a float to an unsigned integer.  The PowerPC way
+  to do this is to compare the argument against the floating-point
+  constant [2^31], subtract [2^31] if bigger, then convert to a signed
+  integer as above, then add back [2^31] if needed.  Expands to:
+<<
+        addis   r2, 0, ha16(lbl1)
+        lfd     f13, lo16(lbl1)(r2)
+        fcmpu   cr7, rsrc, f13
+        cror    30, 29, 30
+        beq     cr7, lbl2
+        fctiwz  f13, rsrc
+        stfdu   f13, -8(r1)
+        lwz     rdst, 4(r1)
+        b       lbl3
+lbl2:   fsub    f13, rsrc, f13
+        fctiwz  f13, f13
+        stfdu   f13, -8(r1)
+        lwz     rdst, 4(r1)
+        addis   rdst, rdst, 0x8000
+lbl3:   addi    r1, r1, 8
+        .const_data
+lbl1:   .long   0x41e00000, 0x00000000    # 2^31 in double precision
+        .text
+>>
 - [Pictf]: convert a signed integer to a float.  This requires complicated
   bit-level manipulations of IEEE floats through mixed float and integer 
   arithmetic over a memory word, which our memory model and axiomatization
@@ -611,6 +636,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (compare_float rs rs#r1 rs#r2)) m
   | Pfcti rd r1 =>
       OK (nextinstr (rs#rd <- (Val.intoffloat rs#r1) #FPR13 <- Vundef)) m
+  | Pfctiu rd r1 =>
+      OK (nextinstr (rs#rd <- (Val.intuoffloat rs#r1) #FPR13 <- Vundef)) m
   | Pfdiv rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
   | Pfmadd rd r1 r2 r3 =>
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 1789fb13..f6d1fec0 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -362,6 +362,8 @@ Definition transl_op
       Pfrsp (freg_of r) (freg_of a1) :: k
   | Ointoffloat, a1 :: nil =>
       Pfcti (ireg_of r) (freg_of a1) :: k
+  | Ointuoffloat, a1 :: nil =>
+      Pfctiu (ireg_of r) (freg_of a1) :: k
   | Ofloatofint, a1 :: nil =>
       Pictf (freg_of r) (ireg_of a1) :: k
   | Ofloatofintu, a1 :: nil =>
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index d3ecbdd8..215a9a7b 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -1386,6 +1386,11 @@ Proof.
   split. apply exec_straight_one. 
   repeat (rewrite (freg_val ms sp rs); auto).
   reflexivity. auto with ppcgen.
+  (* Ointuoffloat *)
+  exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)) #FPR13 <- Vundef)).
+  split. apply exec_straight_one. 
+  repeat (rewrite (freg_val ms sp rs); auto).
+  reflexivity. auto with ppcgen.
   (* Ofloatofint *)
   exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR2 <- Vundef #FPR13 <- Vundef)).
   split. apply exec_straight_one. 
diff --git a/backend/Selection.v b/backend/Selection.v
index 23d8d22f..a55b1918 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -1095,6 +1095,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Oabsf => Eop Oabsf (arg ::: Enil)
   | Cminor.Osingleoffloat => singleoffloat arg
   | Cminor.Ointoffloat => Eop Ointoffloat (arg ::: Enil)
+  | Cminor.Ointuoffloat => Eop Ointuoffloat (arg ::: Enil)
   | Cminor.Ofloatofint => Eop Ofloatofint (arg ::: Enil)
   | Cminor.Ofloatofintu => Eop Ofloatofintu (arg ::: Enil)
   end.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 4674e1d9..07c3e7b9 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1088,6 +1088,7 @@ Proof.
   EvalOp.
   EvalOp.
   EvalOp.
+  EvalOp.
 Qed.
 
 Lemma eval_sel_binop: