From 65cc3738e7436e46f70c0508638a71fbb49c50a8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 25 Feb 2012 10:42:34 +0000 Subject: Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr if b and c are simple. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1826 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplExprproof.v | 56 +++++++++++++++++++++++++++++++++------------- 1 file changed, 41 insertions(+), 15 deletions(-) (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 4df5f034..a88e4c35 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -110,32 +110,38 @@ Qed. Lemma tr_simple_nil: (forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> - dst = For_val \/ dst = For_effects -> simple r -> sl = nil) + dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil) /\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> - simplelist rl -> sl = nil). + simplelist rl = true -> sl = nil). Proof. assert (A: forall dst a, dst = For_val \/ dst = For_effects -> final dst a = nil). intros. destruct H; subst dst; auto. - apply tr_expr_exprlist; intros; simpl in *; try contradiction; auto. + apply tr_expr_exprlist; intros; simpl in *; try discriminate; auto. rewrite H0; auto. simpl; auto. rewrite H0; auto. simpl; auto. destruct H1; congruence. - destruct H6. inv H1; try congruence. rewrite H0; auto. simpl; auto. + destruct (andb_prop _ _ H6). inv H1. rewrite H0; auto. simpl; auto. + rewrite H9 in H8; discriminate. rewrite H0; auto. simpl; auto. - destruct H7. rewrite H0; auto. rewrite H2; auto. simpl; auto. rewrite H0; auto. simpl; auto. - destruct H6. rewrite H0; auto. + destruct (andb_prop _ _ H7). rewrite H0; auto. rewrite H2; auto. simpl; auto. + rewrite H0; auto. simpl; auto. + destruct (andb_prop _ _ H13). destruct (andb_prop _ _ H14). + rewrite H2; auto. simpl; auto. + destruct (andb_prop _ _ H14). destruct (andb_prop _ _ H15). intuition congruence. + destruct (andb_prop _ _ H13). destruct (andb_prop _ _ H14). intuition congruence. + destruct (andb_prop _ _ H6). rewrite H0; auto. Qed. Lemma tr_simple_expr_nil: forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> - dst = For_val \/ dst = For_effects -> simple r -> sl = nil. + dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil. Proof (proj1 tr_simple_nil). Lemma tr_simple_exprlist_nil: forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> - simplelist rl -> sl = nil. + simplelist rl = true -> sl = nil. Proof (proj2 tr_simple_nil). (** Evaluation of simple expressions and of their translation *) @@ -222,6 +228,16 @@ Opaque makeif. subst sl1; simpl. assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence. destruct dst; auto. simpl; econstructor; eauto. +(* condition *) + exploit H2; eauto. intros [A [B C]]. subst sl1. + assert (tr_expr le For_val (if b then r2 else r3) (if b then sl2 else sl3) (if b then a2 else a3) (if b then tmp2 else tmp3)). + destruct b; auto. + exploit H5; eauto. intros [D [E F]]. + assert (eval_expr tge e le m (Econdition a1 a2 a3 ty) v). + econstructor; eauto. congruence. rewrite <- E. auto. + destruct dst; auto. simpl; econstructor; eauto. + intuition congruence. + intuition congruence. (* sizeof *) destruct dst. split; auto. split; auto. constructor. @@ -445,12 +461,20 @@ Ltac UNCHANGED := intros. rewrite <- app_ass. econstructor; eauto. (* condition *) inv H1. + (* simple *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. auto. auto. eauto. + eapply tr_expr_invariant; eauto. UNCHANGED. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. auto. (* for val *) exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. TR. rewrite Q. rewrite app_ass. eauto. red; auto. - intros. rewrite <- app_ass. econstructor. apply S; auto. + intros. rewrite <- app_ass. econstructor. auto. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. auto. auto. @@ -459,7 +483,7 @@ Ltac UNCHANGED := TR. rewrite Q. rewrite app_ass. eauto. red; auto. - intros. rewrite <- app_ass. econstructor. auto. apply S; auto. + intros. rewrite <- app_ass. econstructor. auto. auto. apply S; auto. eapply tr_expr_invariant; eauto. UNCHANGED. eapply tr_expr_invariant; eauto. UNCHANGED. auto. auto. auto. auto. auto. @@ -1065,8 +1089,8 @@ Proof. rewrite (makeseq_nolabel sl2); auto. rewrite (makeseq_nolabel sl3); auto. apply makeif_nolabel; NoLabelTac. - rewrite (makeseq_nolabel sl2). auto. apply H3. apply nolabel_dest_cast; auto. - rewrite (makeseq_nolabel sl3). auto. apply H5. apply nolabel_dest_cast; auto. + rewrite (makeseq_nolabel sl2). auto. apply H4. apply nolabel_dest_cast; auto. + rewrite (makeseq_nolabel sl3). auto. apply H6. apply nolabel_dest_cast; auto. eapply tr_rvalof_nolabel; eauto. eapply tr_rvalof_nolabel; eauto. eapply tr_rvalof_nolabel; eauto. @@ -1341,10 +1365,12 @@ Proof. apply S. apply tr_val_gen. auto. intros. constructor. rewrite H5; auto. apply PTree.gss. intros. apply PTree.gso. red; intros; subst; elim H5; auto. auto. -(* condition true *) - exploit tr_top_leftcontext; eauto. clear H9. +(* condition *) + exploit tr_top_leftcontext; eauto. clear H10. intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. - inv P. inv H2. + inv P. inv H3. + (* simple *) + intuition congruence. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. subst sl0; simpl Kseqlist. destruct b. -- cgit