Improved semantics of casts

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

5 files changed, 150 insertions, 66 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 5461353..90bb2e3 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 e32001b..9856b9e 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 11d8d59..fa9ba1d 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 a199f33..c76d9b9 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 d321ac5..6563a35 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: