From ce0892a2a279c2cf5777b630810749dcc85b6a6e Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 5 May 2010 13:42:31 +0000 Subject: 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 --- cfrontend/Cminorgen.v | 51 ++++++++++++++++---- cfrontend/Cminorgenproof.v | 113 +++++++++++++++++++++++++++++++++++++++------ 2 files changed, 141 insertions(+), 23 deletions(-) (limited to 'cfrontend') 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]]. -- cgit