From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 33 +++++++++++++++------------------ 1 file changed, 15 insertions(+), 18 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 55cdd6b1..c5182db4 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -427,22 +427,22 @@ Proof. (* ifeq *) caseEq (Int.eq i key); intro EQ; rewrite EQ in H5. inv H5. exists nfound; exists rs; intuition. - apply star_one. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. + apply star_one. eapply exec_Icond with (b := true); eauto. + simpl. rewrite H2. simpl. congruence. exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. + eapply star_step. eapply exec_Icond with (b := false); eauto. + simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. (* iflt *) caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5. exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond_true; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. + eapply star_step. eapply exec_Icond with (b := true); eauto. + simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]]. exists nd1; exists rs1; intuition. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. rewrite H2. congruence. eexact EX. traceEq. + eapply star_step. eapply exec_Icond with (b := false); eauto. + simpl. rewrite H2. simpl. congruence. eexact EX. traceEq. (* jumptable *) set (rs1 := rs#rt <- (Vint(Int.sub i ofs))). assert (ME1: match_env map e nil rs1). @@ -451,21 +451,21 @@ Proof. eapply exec_Iop; eauto. predSpec Int.eq Int.eq_spec ofs Int.zero; simpl. rewrite H10. rewrite Int.sub_zero_l. congruence. - rewrite H6. rewrite <- Int.sub_add_opp. auto. + rewrite H6. simpl. rewrite <- Int.sub_add_opp. auto. caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9. exploit H5; eauto. intros [nd [A B]]. exists nd; exists rs1; intuition. eapply star_step. eexact EX1. - eapply star_step. eapply exec_Icond_true; eauto. - simpl. unfold rs1. rewrite Regmap.gss. congruence. + eapply star_step. eapply exec_Icond with (b := true); eauto. + simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss. reflexivity. traceEq. exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto. intros [nd [rs' [EX [NTH ME]]]]. exists nd; exists rs'; intuition. eapply star_step. eexact EX1. - eapply star_step. eapply exec_Icond_false; eauto. - simpl. unfold rs1. rewrite Regmap.gss. congruence. + eapply star_step. eapply exec_Icond with (b := false); eauto. + simpl. unfold rs1. rewrite Regmap.gss. simpl. congruence. eexact EX. reflexivity. traceEq. Qed. @@ -739,11 +739,8 @@ Proof. exists rs1. (* Exec *) split. eapply star_right. eexact EX1. - destruct b. - eapply exec_Icond_true; eauto. - rewrite RES1. assumption. - eapply exec_Icond_false; eauto. - rewrite RES1. assumption. + eapply exec_Icond with (b := b); eauto. + rewrite RES1. auto. traceEq. (* Match-env *) split. assumption. -- cgit