Strengthen chunktype inference and use it to remove some useless casts.

Finished proof of chunktype_compat, which was incomplete.


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

2 files changed, 141 insertions, 23 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index ba3a2bfa..4ed4bc8e 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -70,7 +70,10 @@ Definition compilenv := PMap.t var_info.
 
 Definition chunktype_const (c: Csharpminor.constant) :=
   match c with
-  | Csharpminor.Ointconst n => Mint32
+  | Csharpminor.Ointconst n =>
+      if Int.ltu n (Int.repr 256) then Mint8unsigned 
+      else if Int.ltu n (Int.repr 65536) then Mint16unsigned
+      else Mint32
   | Csharpminor.Ofloatconst n => Mfloat64
   end.
 
@@ -81,7 +84,7 @@ Definition chunktype_unop (op: unary_operation) :=
   | Ocast16unsigned => Mint16unsigned
   | Ocast16signed => Mint16signed
   | Onegint => Mint32
-  | Onotbool => Mint32
+  | Onotbool => Mint8unsigned
   | Onotint => Mint32
   | Onegf => Mfloat64
   | Oabsf => Mfloat64
@@ -92,7 +95,16 @@ Definition chunktype_unop (op: unary_operation) :=
   | Ofloatofintu => Mfloat64
   end.
 
-Definition chunktype_binop (op: binary_operation) :=
+Definition chunktype_logical_op (chunk1 chunk2: memory_chunk) :=
+  match chunk1, chunk2 with
+  | Mint8unsigned, Mint8unsigned => Mint8unsigned
+  | Mint8unsigned, Mint16unsigned => Mint16unsigned
+  | Mint16unsigned, Mint8unsigned => Mint16unsigned
+  | Mint16unsigned, Mint16unsigned => Mint16unsigned
+  | _, _ => Mint32
+  end.
+
+Definition chunktype_binop (op: binary_operation) (chunk1 chunk2: memory_chunk) :=
   match op with
   | Oadd => Mint32
   | Osub => Mint32
@@ -101,9 +113,9 @@ Definition chunktype_binop (op: binary_operation) :=
   | Odivu => Mint32
   | Omod => Mint32
   | Omodu => Mint32
-  | Oand => Mint32
-  | Oor => Mint32
-  | Oxor => Mint32
+  | Oand => chunktype_logical_op chunk1 chunk2
+  | Oor => chunktype_logical_op chunk1 chunk2
+  | Oxor => chunktype_logical_op chunk1 chunk2
   | Oshl => Mint32
   | Oshr => Mint32
   | Oshru => Mint32
@@ -119,7 +131,7 @@ Definition chunktype_binop (op: binary_operation) :=
 Definition chunktype_compat (src dst: memory_chunk) : bool :=
   match src, dst with
   | Mint8unsigned, (Mint8unsigned|Mint16unsigned|Mint16signed|Mint32) => true
-  | Mint8signed, (Mint8signed|Mint16unsigned|Mint16signed|Mint32) => true
+  | Mint8signed, (Mint8signed|Mint16signed|Mint32) => true
   | Mint16unsigned, (Mint16unsigned|Mint32) => true
   | Mint16signed, (Mint16signed|Mint32) => true
   | Mint32, Mint32 => true
@@ -158,7 +170,9 @@ Fixpoint chunktype_expr (cenv: compilenv) (e: Csharpminor.expr)
   | Csharpminor.Eunop op e1 =>
       OK (chunktype_unop op)
   | Csharpminor.Ebinop op e1 e2 =>
-      OK (chunktype_binop op)
+      do chunk1 <- chunktype_expr cenv e1;
+      do chunk2 <- chunktype_expr cenv e2;
+      OK (chunktype_binop op chunk1 chunk2)
   | Csharpminor.Eload chunk e =>
       OK chunk
   | Csharpminor.Econdition e1 e2 e3 =>
@@ -219,6 +233,18 @@ Definition make_stackaddr (ofs: Z): expr :=
 Definition make_globaladdr (id: ident): expr :=
   Econst (Oaddrsymbol id Int.zero).
 
+(** Auxiliary to remove useless conversions. *)
+
+Definition unop_is_cast (op: unary_operation) : option memory_chunk :=
+  match op with
+  | Ocast8unsigned => Some Mint8unsigned
+  | Ocast8signed => Some Mint8signed
+  | Ocast16unsigned => Some Mint16unsigned
+  | Ocast16signed => Some Mint16signed
+  | Osingleoffloat => Some Mfloat32
+  | _ => None
+  end.
+
 (** Generation of a Cminor expression for reading a Csharpminor variable. *)
 
 Definition var_get (cenv: compilenv) (id: ident): res expr :=
@@ -308,7 +334,14 @@ Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr)
       OK (Econst (transl_constant cst))
   | Csharpminor.Eunop op e1 =>
       do te1 <- transl_expr cenv e1;
-      OK (Eunop op te1)
+      match unop_is_cast op with
+      | None => OK (Eunop op te1)
+      | Some chunk =>
+          do chunk1 <- chunktype_expr cenv e1;
+          if chunktype_compat chunk1 chunk
+          then OK te1
+          else OK (Eunop op te1)
+      end
   | Csharpminor.Ebinop op e1 e2 =>
       do te1 <- transl_expr cenv e1;
       do te2 <- transl_expr cenv e2;
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index c79555c0..19e13cbe 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -215,13 +215,48 @@ Proof.
   contradiction || reflexivity.
 Qed.
 
+Lemma chunktype_compat_correct:
+  forall src dst v,
+  chunktype_compat src dst = true ->
+  val_normalized v src -> val_normalized v dst.
+Proof.
+  unfold val_normalized; intros. rewrite <- H0.
+  assert (A: 0 < 8 < Z_of_nat Int.wordsize). compute; auto.
+  assert (B: 0 < 16 < Z_of_nat Int.wordsize). compute; auto.
+  assert (C: 8 <= 16 < Z_of_nat Int.wordsize). omega.
+  destruct src; destruct dst; simpl in H; try discriminate; auto;
+  destruct v; simpl; auto.
+  rewrite Int.sign_ext_idem; auto.
+  rewrite Int.sign_ext_widen; auto. 
+  rewrite Int.zero_ext_idem; auto.
+  rewrite Int.sign_zero_ext_widen; auto.
+  rewrite Int.zero_ext_widen; auto.
+  rewrite Int.sign_ext_widen; auto. omega.
+  rewrite Int.zero_ext_idem; auto.
+  rewrite Float.singleoffloat_idem; auto.
+Qed.
+
+Remark int_zero_ext_small:
+  forall x n,
+  0 <= Int.unsigned x < two_p n ->
+  Int.zero_ext n x = x.
+Proof.
+  intros. unfold Int.zero_ext. rewrite Zmod_small; auto. apply Int.repr_unsigned. 
+Qed.
+
 Lemma chunktype_const_correct:
   forall c v,
   Csharpminor.eval_constant c = Some v ->
   val_normalized v (chunktype_const c).
 Proof.
   unfold Csharpminor.eval_constant; intros. 
-  destruct c; inv H; unfold val_normalized; auto.
+  destruct c; inv H; unfold val_normalized; simpl.
+  case_eq (Int.ltu i (Int.repr 256)); intros.
+  simpl. decEq. apply int_zero_ext_small. exact (Int.ltu_inv _ _ H).
+  case_eq (Int.ltu i (Int.repr 65536)); intros.
+  simpl. decEq. apply int_zero_ext_small. exact (Int.ltu_inv _ _ H0). 
+  simpl; auto.
+  auto.
 Qed.
 
 Lemma chunktype_unop_correct:
@@ -246,10 +281,42 @@ Proof.
   destruct v1; inv H; auto.
 Qed.
 
+Lemma chunktype_logical_op_correct:
+  forall (logop: int -> int -> int)
+         (DISTR: forall a b c, logop (Int.and a c) (Int.and b c) =
+                               Int.and (logop a b) c)
+         n1 c1 n2 c2,
+  val_normalized (Vint n1) c1 -> val_normalized (Vint n2) c2 ->
+  val_normalized (Vint (logop n1 n2)) (chunktype_logical_op c1 c2).
+Proof.
+  intros. set (c := chunktype_logical_op c1 c2).
+  assert (val_normalized (Vint n1) c /\ val_normalized (Vint n2) c).
+    unfold c, chunktype_logical_op. 
+    destruct c1; destruct c2; split; try (auto; unfold val_normalized; reflexivity).
+    apply chunktype_compat_correct with Mint8unsigned; auto.
+    apply chunktype_compat_correct with Mint8unsigned; auto.
+  destruct H1. 
+  assert (c = Mint8unsigned \/ c = Mint16unsigned \/ c = Mint32).
+    unfold c. destruct c1; auto; destruct c2; auto.
+  destruct H3 as [A | [A | A]]; rewrite A in *.
+  unfold val_normalized in *. simpl in *.
+  assert (0 < 8 < Z_of_nat Int.wordsize). compute; auto.
+  rewrite Int.zero_ext_and in *; auto.
+  set (m := Int.repr (two_p 8 - 1)) in *.
+  rewrite <- DISTR. congruence.
+  unfold val_normalized in *. simpl in *.
+  assert (0 < 16 < Z_of_nat Int.wordsize). compute; auto.
+  rewrite Int.zero_ext_and in *; auto.
+  set (m := Int.repr (two_p 16 - 1)) in *.
+  rewrite <- DISTR. congruence.
+  red. auto.
+Qed.
+
 Lemma chunktype_binop_correct:
-  forall op v1 v2 m v,
+  forall op v1 v2 c1 c2 m v,
   Csharpminor.eval_binop op v1 v2 m = Some v ->
-  val_normalized v (chunktype_binop op).
+  val_normalized v1 c1 -> val_normalized v2 c2 ->
+  val_normalized v (chunktype_binop op c1 c2).
 Proof.
   intros; destruct op; simpl in *; unfold val_normalized;
   destruct v1; destruct v2; try (inv H; reflexivity).
@@ -258,6 +325,15 @@ Proof.
   destruct (Int.eq i0 Int.zero); inv H; auto.
   destruct (Int.eq i0 Int.zero); inv H; auto.
   destruct (Int.eq i0 Int.zero); inv H; auto.
+  inv H. apply chunktype_logical_op_correct; auto. 
+  intros. repeat rewrite Int.and_assoc. decEq. 
+  rewrite (Int.and_commut b c). rewrite <- Int.and_assoc. rewrite Int.and_idem. auto.
+  inv H. apply chunktype_logical_op_correct; auto. 
+  intros. rewrite (Int.and_commut a c). rewrite (Int.and_commut b c).
+  rewrite <- Int.and_or_distrib. apply Int.and_commut.
+  inv H. apply chunktype_logical_op_correct; auto. 
+  intros. rewrite (Int.and_commut a c). rewrite (Int.and_commut b c).
+  rewrite <- Int.and_xor_distrib. apply Int.and_commut.
   destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
   destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
   destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
@@ -269,21 +345,11 @@ Proof.
   destruct (Mem.valid_pointer m b (Int.signed i) &&
             Mem.valid_pointer m b0 (Int.signed i0)).
   destruct (eq_block b b0); inv H. destruct (Int.cmp c i i0); auto.
-  destruct c; inv H1; auto. inv H.
+  destruct c; inv H3; auto. inv H.
   inv H. destruct (Int.cmpu c i i0); auto.
   inv H. destruct (Float.cmp c f f0); auto.
 Qed.
 
-Lemma chunktype_compat_correct:
-  forall src dst v,
-  chunktype_compat src dst = true ->
-  val_normalized v src -> val_normalized v dst.
-Proof.
-  unfold val_normalized; intros. rewrite <- H0.
-  destruct src; destruct dst; simpl in H; try discriminate; auto;
-  destruct v; simpl; auto.
-Admitted.
-
 Lemma chunktype_merge_correct:
   forall c1 c2 c v,
   chunktype_merge c1 c2 = OK c ->
@@ -301,6 +367,7 @@ Proof.
   rewrite e. apply val_normalized_has_type. auto.
 Qed.
 
+
 (** * Correspondence between Csharpminor's and Cminor's environments and memory states *)
 
 (** In Csharpminor, every variable is stored in a separate memory block.
@@ -1482,6 +1549,14 @@ Proof.
   eapply eval_Econst. simpl. rewrite H. auto.
 Qed.
 
+Lemma unop_is_cast_correct:
+  forall op chunk v,
+  unop_is_cast op = Some chunk ->
+  Csharpminor.eval_unop op v = Some (Val.load_result chunk v).
+Proof.
+  intros. destruct op; simpl in H; inv H; reflexivity.
+Qed.
+
 (** Correctness of [make_store]. *)
 
 Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
@@ -2394,6 +2469,16 @@ Proof.
   (* Eunop *)
   exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]].
   exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]].
+  revert EQ0. case_eq (unop_is_cast op); intros; monadInv EQ0.
+  revert EQ2. case_eq (chunktype_compat x0 m0); intros; monadInv EQ2.
+  exploit unop_is_cast_correct; eauto. instantiate (1 := v1); intros.
+  assert (val_normalized v1 m0). 
+    eapply chunktype_compat_correct; eauto. 
+    eapply chunktype_expr_correct; eauto.
+  red in H4.
+  assert (v = v1) by congruence. subst v. 
+  exists tv1; auto.
+  exists tv; split. econstructor; eauto. auto.
   exists tv; split. econstructor; eauto. auto.
   (* Ebinop *)
   exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]].