From ea23f1260ff7d587b0db05090580efd8f56d617a Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 31 May 2008 08:50:20 +0000 Subject: 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 --- cfrontend/Csem.v | 32 ++++++++++++++++++++++---------- cfrontend/Cshmgen.v | 16 ++++++++++++---- cfrontend/Cshmgenproof2.v | 6 +++++- cfrontend/Csyntax.v | 3 +++ 4 files changed, 42 insertions(+), 15 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 871f8831..5e4f4e37 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 b3369ae2..20eb17f4 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 2491e525..98d057a4 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 6680efe2..ee1b8617 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. -- cgit