From 335c01eba7bfca53e9f44bbe74e9321475c4d012 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Jul 2011 17:11:44 +0000 Subject: Improved semantics of casts git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1685 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 39 +++++++++++++++ cfrontend/Cshmgen.v | 29 +++++++++++- cfrontend/Cshmgenproof.v | 108 +++++++++++++++++++++--------------------- cfrontend/Csyntax.v | 23 ++++++++- cfrontend/Initializersproof.v | 17 ++++--- 5 files changed, 150 insertions(+), 66 deletions(-) diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 5461353f..90bb2e31 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -61,6 +61,7 @@ Definition cast_float_float (sz: floatsize) (f: float) : float := | F64 => f end. +(* Definition neutral_for_cast (t: type) : bool := match t with | Tint I32 sg => true @@ -92,6 +93,44 @@ Function sem_cast (v: val) (t1 t2: type) : option val := | _, _, _ => None end. +*) + +Function sem_cast (v: val) (t1 t2: type) : option val := + match classify_cast t1 t2 with + | cast_case_neutral => + match v with + | Vint _ | Vptr _ _ => Some v + | _ => None + end + | cast_case_i2i sz2 si2 => + match v with + | Vint i => Some (Vint (cast_int_int sz2 si2 i)) + | _ => None + end + | cast_case_f2f sz2 => + match v with + | Vfloat f => Some (Vfloat (cast_float_float sz2 f)) + | _ => None + end + | cast_case_i2f si1 sz2 => + match v with + | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | _ => None + end + | cast_case_f2i sz2 si2 => + match v with + | Vfloat f => + match cast_float_int si2 f with + | Some i => Some (Vint (cast_int_int sz2 si2 i)) + | None => None + end + | _ => None + end + | cast_case_void => + Some v + | cast_case_default => + None + end. (** Interpretation of values as truth values. Non-zero integers, non-zero floats and non-null pointers are diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index e32001b9..9856b9ef 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -214,7 +214,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type - [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 @@ -234,6 +234,33 @@ Definition make_cast2 (from to: type) (e: expr) := Definition make_cast (from to: type) (e: expr) := make_cast2 from to (make_cast1 from to e). +*) + +Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := + match sz, si with + | I8, Signed => Eunop Ocast8signed e + | I8, Unsigned => Eunop Ocast8unsigned e + | I16, Signed => Eunop Ocast16signed e + | I16, Unsigned => Eunop Ocast16unsigned e + | I32, _ => e + end. + +Definition make_cast_float (e: expr) (sz: floatsize) := + match sz with + | F32 => Eunop Osingleoffloat e + | F64 => e + end. + +Definition make_cast (from to: type) (e: expr) := + match classify_cast from to with + | cast_case_neutral => e + | cast_case_i2i sz2 si2 => make_cast_int e sz2 si2 + | cast_case_f2f sz2 => make_cast_float e sz2 + | cast_case_i2f si1 sz2 => make_cast_float (make_floatofint e si1) sz2 + | cast_case_f2i sz2 si2 => make_cast_int (make_intoffloat e si2) sz2 si2 + | cast_case_void => e + | cast_case_default => e + end. (** [make_load addr ty_res] loads a value of type [ty_res] from the memory location denoted by the Csharpminor expression [addr]. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 11d8d595..fa9ba1d2 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -40,7 +40,7 @@ Proof. intros. unfold chunk_of_type in H. destruct ty; simpl in H; try monadInv H. destruct i; destruct s; monadInv H; reflexivity. destruct f; monadInv H; reflexivity. - reflexivity. reflexivity. + reflexivity. Qed. Remark transl_params_types: @@ -132,15 +132,13 @@ Proof. auto. Qed. -Remark neutral_for_cast_chunk: - forall ty chunk, - neutral_for_cast ty = true -> access_mode ty = By_value chunk -> chunk = Mint32. +Remark cast_neutral_normalized: + forall ty1 ty2 chunk, + classify_cast ty1 ty2 = cast_case_neutral -> + access_mode ty2 = By_value chunk -> + chunk = Mint32. Proof. - intros. destruct ty; inv H; simpl in H0. - destruct i; inv H2. congruence. - congruence. - congruence. - congruence. + intros. functional inversion H; subst; simpl in H0; congruence. Qed. Lemma cast_result_normalized: @@ -150,14 +148,13 @@ Lemma cast_result_normalized: val_normalized v2 chunk. Proof. intros. functional inversion H; subst. - apply cast_int_int_normalized; auto. - apply cast_int_int_normalized; auto. - apply cast_float_float_normalized; auto. - apply cast_float_float_normalized; auto. - destruct (andb_prop _ _ H8). - rewrite (neutral_for_cast_chunk _ _ H2 H0). red; auto. - destruct (andb_prop _ _ H9). - rewrite (neutral_for_cast_chunk _ _ H2 H0). red; auto. + rewrite (cast_neutral_normalized ty1 ty2 chunk); auto. red; auto. + rewrite (cast_neutral_normalized ty1 ty2 chunk); auto. red; auto. + functional inversion H2; subst. eapply cast_int_int_normalized; eauto. + functional inversion H2; subst. eapply cast_float_float_normalized; eauto. + functional inversion H2; subst. eapply cast_float_float_normalized; eauto. + functional inversion H2; subst. eapply cast_int_int_normalized; eauto. + functional inversion H5; subst. simpl in H0. congruence. Qed. Definition val_casted (v: val) (ty: type) : Prop := @@ -382,14 +379,49 @@ Hint Resolve make_intconst_correct make_floatconst_correct eval_Eunop eval_Ebinop: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. -Remark Vtrue_is_true: Val.is_true Vtrue. +Lemma make_cast_int_correct: + forall e le m a n sz si, + eval_expr ge e le m a (Vint n) -> + eval_expr ge e le m (make_cast_int a sz si) (Vint (cast_int_int sz si n)). Proof. - simpl. apply Int.one_not_zero. + intros. unfold make_cast_int, cast_int_int. + destruct sz. + destruct si; eauto with cshm. + destruct si; eauto with cshm. + auto. Qed. -Remark Vfalse_is_false: Val.is_false Vfalse. +Lemma make_cast_float_correct: + forall e le m a n sz, + eval_expr ge e le m a (Vfloat n) -> + eval_expr ge e le m (make_cast_float a sz) (Vfloat (cast_float_float sz n)). Proof. - simpl. auto. + intros. unfold make_cast_float, cast_float_float. + destruct sz. eauto with cshm. auto. +Qed. + +Hint Resolve make_cast_int_correct make_cast_float_correct: cshm. + +Lemma make_cast_correct: + forall e le m a v ty1 ty2 v', + eval_expr ge e le m a v -> + sem_cast v ty1 ty2 = Some v' -> + eval_expr ge e le m (make_cast ty1 ty2 a) v'. +Proof. + intros. unfold make_cast. functional inversion H0; subst. + (* neutral *) + rewrite H2; auto. + rewrite H2; auto. + (* int -> int *) + rewrite H2. auto with cshm. + (* float -> float *) + rewrite H2. auto with cshm. + (* int -> float *) + rewrite H2. auto with cshm. + (* float -> int *) + rewrite H2. eauto with cshm. + (* void *) + rewrite H5. auto. Qed. Lemma make_boolean_correct: @@ -644,40 +676,6 @@ Proof. eapply make_cmp_correct; eauto. Qed. -Lemma make_cast_neutral: - forall ty1 ty2 a, - neutral_for_cast ty1 && neutral_for_cast ty2 = true -> - make_cast ty1 ty2 a = a. -Proof. - intros. destruct (andb_prop _ _ H). - unfold make_cast. - replace (make_cast1 ty1 ty2 a) with a. - unfold make_cast2. destruct ty2; simpl in H1; inv H1; auto. destruct i; inv H3; auto. - unfold make_cast1. destruct ty1; simpl in H0; inv H0; auto. destruct ty2; simpl in H1; inv H1; auto. -Qed. - -Lemma make_cast_correct: - forall e le m a v ty1 ty2 v', - eval_expr ge e le m a v -> - sem_cast v ty1 ty2 = Some v' -> - eval_expr ge e le m (make_cast ty1 ty2 a) v'. -Proof. - intros. functional inversion H0; subst; simpl. - (* cast_int_int *) - destruct sz2; destruct si2; repeat econstructor; eauto with cshm. - (* cast_float_int *) - exploit make_intoffloat_correct; eauto. intros A. - destruct sz2; destruct si2; eauto with cshm. - (* cast_int_float *) - destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto. - (* cast_float_float *) - destruct sz2; repeat econstructor; eauto with cshm. - (* neutral, ptr *) - rewrite make_cast_neutral; auto. - (* neutral, int *) - rewrite make_cast_neutral; auto. -Qed. - Lemma make_load_correct: forall addr ty code b ofs v e le m, make_load addr ty = OK code -> diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index a199f33e..c76d9b95 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -662,7 +662,7 @@ Definition access_mode (ty: type) : mode := | Tfunction _ _ => By_reference | Tstruct _ fList => By_nothing | Tunion _ fList => By_nothing - | Tcomp_ptr _ => By_value Mint32 + | Tcomp_ptr _ => By_nothing end. (** Unroll the type of a structure or union field, substituting @@ -925,6 +925,27 @@ Definition classify_fun (ty: type) := | _ => fun_default end. +Inductive classify_cast_cases : Type := + | cast_case_neutral (**r int|pointer -> int32|pointer *) + | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) + | cast_case_f2f (sz2:floatsize) (**r float -> float *) + | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) + | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) + | cast_case_void (**r any -> void *) + | cast_case_default. + +Function classify_cast (tfrom tto: type) : classify_cast_cases := + match tto, tfrom with + | Tint I32 si2, (Tint _ _ | Tpointer _ | Tarray _ _ | Tfunction _ _) => cast_case_neutral + | Tint sz2 si2, Tint sz1 si1 => cast_case_i2i sz2 si2 + | Tint sz2 si2, Tfloat sz1 => cast_case_f2i sz2 si2 + | Tfloat sz2, Tfloat sz1 => cast_case_f2f sz2 + | Tfloat sz2, Tint sz1 si1 => cast_case_i2f si1 sz2 + | Tpointer _, (Tint _ _ | Tpointer _ | Tarray _ _ | Tfunction _ _) => cast_case_neutral + | Tvoid, _ => cast_case_void + | _, _ => cast_case_default + end. + (** Translating C types to Cminor types, function signatures, and external functions. *) diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index d321ac58..6563a352 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -399,15 +399,14 @@ Lemma sem_cast_match: match_val v2' v2. Proof. intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] _eqn; inv H1. - inv H0. - replace v2' with v2 by congruence. - functional inversion H; subst; constructor. - replace v2' with v2 by congruence. - functional inversion H; subst; constructor. - simpl in H; simpl in Heqo. - destruct (neutral_for_cast ty1 && neutral_for_cast ty2); inv H; inv Heqo. - constructor; auto. - functional inversion H. + unfold sem_cast in H; functional inversion Heqo; subst. + rewrite H2 in H. inv H0. inv H. constructor. + rewrite H2 in H. inv H0. inv H. constructor; auto. + rewrite H2 in H. inv H0. inv H. constructor. + rewrite H2 in H. inv H0. inv H. constructor. + rewrite H2 in H. inv H0. inv H. constructor. + rewrite H2 in H. inv H0. destruct (cast_float_int si2 f); inv H. inv H7. constructor. + rewrite H5 in H. inv H. auto. Qed. Lemma bool_val_match: -- cgit