Utilisation de intoffloatu. Ajout du cas int + ptr.

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

4 files changed, 42 insertions, 15 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 871f883..5e4f4e3 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -119,22 +119,28 @@ Function sem_notbool (v: val) (ty: type) : option val :=
 
 Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_add t1 t2 with 
-  | add_case_ii =>  
+  | add_case_ii =>                      (**r integer addition *)
       match v1, v2 with
       | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
       | _,  _ => None
       end
-  | add_case_ff =>
+  | add_case_ff =>                      (**r float addition *)
       match v1, v2 with
       | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
       | _,  _ => None
       end
-  | add_case_pi ty=>
+  | add_case_pi ty =>                   (**r pointer plus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 => 
 	Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
       | _,  _ => None
       end   
+  | add_case_ip ty =>                   (**r integer plus pointer *)
+      match v1,v2 with
+      | Vint n1, Vptr b2 ofs2 => 
+	Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
+      | _,  _ => None
+      end   
   | add_default => None
 end.
 
@@ -358,6 +364,12 @@ Definition cast_int_float (si : signedness) (i: int) : float :=
   | Unsigned => Float.floatofintu i
   end.
 
+Definition cast_float_int (si : signedness) (f: float) : int :=
+  match si with
+  | Signed => Float.intoffloat f
+  | Unsigned => Float.intuoffloat f
+  end.
+
 Definition cast_float_float (sz: floatsize) (f: float) : float :=
   match sz with
   | F32 => Float.singleoffloat f
@@ -375,22 +387,22 @@ Inductive neutral_for_cast: type -> Prop :=
       neutral_for_cast (Tfunction targs tres).
 
 Inductive cast : val -> type -> type -> val -> Prop :=
-  | cast_ii:   forall i sz2 sz1 si1 si2,
+  | cast_ii:   forall i sz2 sz1 si1 si2,            (**r int to int  *)
       cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
            (Vint (cast_int_int sz2 si2 i))
-  | cast_fi:   forall f sz1 sz2 si2,
+  | cast_fi:   forall f sz1 sz2 si2,                (**r float to int *)
       cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
-           (Vint (cast_int_int sz2 si2 (Float.intoffloat f)))
-  | cast_if:   forall i sz1 sz2 si1,
+           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
+  | cast_if:   forall i sz1 sz2 si1,                (**r int to float  *)
       cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
           (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
-  | cast_ff:   forall f sz1 sz2,
+  | cast_ff:   forall f sz1 sz2,                    (**r float to float *)
       cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
            (Vfloat (cast_float_float sz2 f))
-  | cast_nn_p: forall b ofs t1 t2,
+  | cast_nn_p: forall b ofs t1 t2, (**r no change in data representation *)
       neutral_for_cast t1 -> neutral_for_cast t2 ->
       cast (Vptr b ofs) t1 t2 (Vptr b ofs)
-  | cast_nn_i: forall n t1 t2,
+  | cast_nn_i: forall n t1 t2,     (**r no change in data representation *)
       neutral_for_cast t1 -> neutral_for_cast t2 ->
       cast (Vint n) t1 t2 (Vint n).
 
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index b3369ae..20eb17f 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -90,6 +90,12 @@ Definition make_floatofint (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Ofloatofintu e
   end.
 
+Definition make_intoffloat (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Ointoffloat e
+  | Unsigned => Eunop Ointuoffloat e
+  end.
+
 (** [make_boolean e ty] returns a Csharpminor expression that evaluates
    to the boolean value of [e].  Recall that:
 -  in Csharpminor, [false] is the integer 0,
@@ -126,6 +132,9 @@ Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   | add_case_pi ty =>
       let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
       OK (Ebinop Oadd e1 (Ebinop Omul n e2))
+  | add_case_ip ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      OK (Ebinop Oadd e2 (Ebinop Omul n e1))
   | add_default => Error (msg "Cshmgen.make_add")
   end.
 
@@ -212,15 +221,14 @@ Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 (** [make_cast from to e] applies to [e] the numeric conversions needed
    to transform a result of type [from] to a result of type [to].
    It is decomposed in two functions:
--  [make_cast1]  converts between integer and pointers, on one side,
-     and floats on the other side.
--  [make_cast2]  converts to a "smaller" int or float type if necessary.
+-  [make_cast1]  converts from integers to floats or from floats to integers;
+-  [make_cast2]  converts to a "small" int or float type if necessary.
 *)
 
 Definition make_cast1 (from to: type) (e: expr) :=
   match from, to with
   | Tint _ uns, Tfloat _ => make_floatofint e uns
-  | Tfloat _, Tint _ _ => Eunop Ointoffloat e
+  | Tfloat _, Tint _ uns => make_intoffloat e uns
   | _, _ => e
   end.
 
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 2491e52..98d057a 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -206,6 +206,10 @@ Proof.
   eapply eval_Ebinop. eauto. 
   eapply eval_Ebinop. eauto with cshm. eauto.
   simpl. reflexivity. reflexivity. 
+  inversion H7. 
+  eapply eval_Ebinop. eauto. 
+  eapply eval_Ebinop. eauto with cshm. eauto. 
+  simpl. reflexivity. simpl. reflexivity.
 Qed.
 
 Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub.
@@ -369,7 +373,7 @@ Proof.
   (* cast_int_int *)
     destruct sz2; destruct si2; repeat econstructor; eauto with cshm.
   (* cast_float_int *)
-    destruct sz2; destruct si2; repeat econstructor; eauto with cshm; simpl; auto.
+    destruct sz2; destruct si2; unfold make_intoffloat; repeat econstructor; eauto with cshm; simpl; auto.
   (* cast_int_float *)
     destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto.
   (* cast_float_float *)
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 6680efe..ee1b861 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -396,6 +396,7 @@ Inductive classify_add_cases : Set :=
   | add_case_ii: classify_add_cases         (**r int , int *)
   | add_case_ff: classify_add_cases         (**r float , float *)
   | add_case_pi: type -> classify_add_cases (**r ptr or array, int *)
+  | add_case_ip: type -> classify_add_cases (**r int, ptr or array *)
   | add_default: classify_add_cases.        (**r other *)
 
 Definition classify_add (ty1: type) (ty2: type) :=
@@ -404,6 +405,8 @@ Definition classify_add (ty1: type) (ty2: type) :=
   | Tfloat _, Tfloat _ => add_case_ff
   | Tpointer ty, Tint _ _ => add_case_pi ty
   | Tarray ty _, Tint _ _ => add_case_pi ty 
+  | Tint _ _, Tpointer ty => add_case_ip ty
+  | Tint _ _, Tarray ty _ => add_case_ip ty 
   | _, _ => add_default
   end.