From 5d1c52555bb166430402103afe9540cc4c296487 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Aug 2011 17:29:06 +0000 Subject: Cleaned up handling of composite conditions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgenproof.v | 126 +++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 109 insertions(+), 17 deletions(-) (limited to 'ia32/Asmgenproof.v') diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index d049737..45ac48d 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -401,6 +401,20 @@ Proof. destruct (preg_of src); inv H; auto. Qed. +Remark mk_setcc_label: + forall xc rd k, + find_label lbl (mk_setcc xc rd k) = find_label lbl k. +Proof. + intros. destruct xc; simpl; auto; destruct (ireg_eq rd EDX); auto. +Qed. + +Remark mk_jcc_label: + forall xc lbl' k, + find_label lbl (mk_jcc xc lbl' k) = find_label lbl k. +Proof. + intros. destruct xc; auto. +Qed. + Ltac ArgsInv := match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -441,7 +455,7 @@ Proof. eapply mk_shift_label; eauto. eapply mk_shrximm_label; eauto. eapply mk_shift_label; eauto. - eapply trans_eq. eapply transl_cond_label; eauto. auto. + eapply trans_eq. eapply transl_cond_label; eauto. apply mk_setcc_label. Qed. Remark transl_load_label: @@ -482,7 +496,7 @@ Opaque loadind. monadInv H; auto. inv H; simpl. destruct (peq lbl l). congruence. auto. monadInv H; auto. - eapply trans_eq. eapply transl_cond_label; eauto. auto. + eapply trans_eq. eapply transl_cond_label; eauto. apply mk_jcc_label. monadInv H; auto. monadInv H; auto. Qed. @@ -624,6 +638,43 @@ Proof. econstructor; eauto. eapply exec_straight_at; eauto. Qed. +Lemma exec_straight_steps_goto: + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack s -> + Mem.extends m2 m2' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mach.find_label lbl f.(fn_code) = Some c' -> + transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc -> + edx_preserved ep i = false -> + (forall k c, transl_instr f i ep k = OK c -> + exists jmp, exists k', exists rs2, + exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' + /\ agree ms2 sp rs2 + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Machsem.State s fb sp c' ms2 m2) st'. +Proof. + intros. inversion H3. subst. monadInv H9. + exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. + generalize (functions_transl _ _ _ H7 H8); intro FN. + generalize (transf_function_no_overflow _ _ H8); intro NOOV. + exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + traceEq. + econstructor; eauto. + apply agree_exten with rs2; auto with ppcgen. + congruence. +Qed. + Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. Proof. induction 1; simpl. congruence. auto. Qed. @@ -1053,22 +1104,40 @@ Lemma exec_Mcond_true_prop: Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - inv AT. monadInv H5. + left; eapply exec_straight_steps_goto; eauto. + intros. simpl in H2. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. - generalize (functions_transl _ _ _ FIND H4); intro FN. - generalize (transf_function_no_overflow _ _ H4); intro NOOV. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT3 INV3]]]]. - left; exists (State rs3 m'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. eauto. simpl. rewrite B. eauto. traceEq. - econstructor; eauto. - eapply agree_exten_temps; eauto. intros. rewrite INV3; auto with ppcgen. - congruence. + destruct (testcond_for_condition cond); simpl in *. +(* simple jcc *) + exists (Pjcc c1 lbl); exists k; exists rs'. + split. eexact A. + split. eapply agree_exten_temps; eauto. + simpl. rewrite B. auto. +(* jcc; jcc *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct b1. + (* first jcc jumps *) + exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'. + split. eexact A. + split. eapply agree_exten_temps; eauto. + simpl. rewrite Heqo. auto. + (* second jcc jumps *) + exists (Pjcc c2 lbl); exists k; exists (nextinstr rs'). + split. eapply exec_straight_trans. eexact A. + eapply exec_straight_one. simpl. rewrite Heqo. auto. auto. + split. eapply agree_exten_temps; eauto. + intros. rewrite nextinstr_inv; auto with ppcgen. + simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. + destruct b2; auto || discriminate. +(* jcc2 *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (andb_prop _ _ H4). subst. + exists (Pjcc2 c1 c2 lbl); exists k; exists rs'. + split. eexact A. + split. eapply agree_exten_temps; eauto. + simpl. rewrite Heqo; rewrite Heqo0; auto. Qed. Lemma exec_Mcond_false_prop: @@ -1083,11 +1152,34 @@ Proof. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps; eauto. intros. simpl in H0. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. + destruct (testcond_for_condition cond); simpl in *. +(* simple jcc *) econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. rewrite B. eauto. auto. split. apply agree_nextinstr. eapply agree_exten_temps; eauto. simpl; congruence. +(* jcc ; jcc *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (orb_false_elim _ _ H2); subst. + econstructor; split. + eapply exec_straight_trans. eexact A. + eapply exec_straight_two. simpl. rewrite Heqo. eauto. auto. + simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. eauto. auto. auto. + split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto. + simpl; congruence. +(* jcc2 *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + exists (nextinstr rs'); split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. + rewrite Heqo; rewrite Heqo0. + destruct b1. simpl in *. subst b2. auto. auto. + auto. + split. apply agree_nextinstr. eapply agree_exten_temps; eauto. + rewrite H2; congruence. Qed. Lemma exec_Mjumptable_prop: -- cgit v1.2.3