From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- arm/Asmgenproof.v | 282 +++++++++++++++++++++++++++--------------------------- 1 file changed, 141 insertions(+), 141 deletions(-) (limited to 'arm/Asmgenproof.v') diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 93c50bfb..7a29e4a5 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -45,17 +45,17 @@ Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. Proof. - intros. unfold ge, tge. + intros. unfold ge, tge. apply Genv.find_symbol_transf_partial with transf_fundef. - exact TRANSF. + exact TRANSF. Qed. Lemma public_preserved: forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. Proof. - intros. unfold ge, tge. + intros. unfold ge, tge. apply Genv.public_symbol_transf_partial with transf_fundef. - exact TRANSF. + exact TRANSF. Qed. Lemma functions_translated: @@ -71,7 +71,7 @@ Lemma functions_transl: transf_function f = OK tf -> Genv.find_funct_ptr tge b = Some (Internal tf). Proof. - intros. + intros. destruct (functions_translated _ _ H) as [tf' [A B]]. rewrite A. monadInv B. f_equal. congruence. Qed. @@ -79,9 +79,9 @@ Qed. Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. - intros. unfold ge, tge. + intros. unfold ge, tge. apply Genv.find_var_info_transf_partial with transf_fundef. - exact TRANSF. + exact TRANSF. Qed. (** * Properties of control flow *) @@ -102,7 +102,7 @@ Proof. intros. inv H. eapply exec_straight_steps_1; eauto. eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. + eapply functions_transl; eauto. Qed. Lemma exec_straight_at: @@ -112,8 +112,8 @@ Lemma exec_straight_at: exec_straight tge tf tc rs m tc' rs' m' -> transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. Proof. - intros. inv H. - exploit exec_straight_steps_2; eauto. + intros. inv H. + exploit exec_straight_steps_2; eauto. eapply transf_function_no_overflow; eauto. eapply functions_transl; eauto. intros [ofs' [PC' CT']]. @@ -134,22 +134,22 @@ Lemma label_pos_code_tail: forall lbl c pos c', find_label lbl c = Some c' -> exists pos', - label_pos lbl pos c = Some pos' + label_pos lbl pos c = Some pos' /\ code_tail (pos' - pos) c c' /\ pos < pos' <= pos + list_length_z c. Proof. - induction c. + induction c. simpl; intros. discriminate. simpl; intros until c'. case (is_label lbl a). intro EQ; injection EQ; intro; subst c'. exists (pos + 1). split. auto. split. - replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. + replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. + rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. - constructor. auto. + constructor. auto. rewrite list_length_z_cons. omega. Qed. @@ -242,7 +242,7 @@ Remark indexed_memory_access_label: (forall r n, nolabel (mk_instr r n)) -> tail_nolabel k (indexed_memory_access mk_instr mk_immed base ofs k). Proof. - intros. unfold indexed_memory_access. + intros. unfold indexed_memory_access. destruct (Int.eq ofs (mk_immed ofs)). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. @@ -310,18 +310,18 @@ Proof. eapply loadind_label; eauto. eapply storeind_label; eauto. destruct ep. eapply loadind_label; eauto. - eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel. + eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel. eapply transl_op_label; eauto. - unfold transl_load, transl_memory_access_int, transl_memory_access_float in H. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. - unfold transl_store, transl_memory_access_int, transl_memory_access_float in H. - destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. + unfold transl_load, transl_memory_access_int, transl_memory_access_float in H. + destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. + unfold transl_store, transl_memory_access_int, transl_memory_access_float in H. + destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. destruct s0; monadInv H; TailNoLabel. destruct s0; monadInv H; unfold loadind_int; eapply tail_nolabel_trans. eapply indexed_memory_access_label; auto with labels. TailNoLabel. eapply indexed_memory_access_label; auto with labels. TailNoLabel. eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. - eapply tail_nolabel_trans. unfold loadind_int. eapply indexed_memory_access_label; auto with labels. TailNoLabel. + eapply tail_nolabel_trans. unfold loadind_int. eapply indexed_memory_access_label; auto with labels. TailNoLabel. Qed. Lemma transl_instr_label': @@ -330,7 +330,7 @@ Lemma transl_instr_label': find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. Proof. intros. exploit transl_instr_label; eauto. - destruct i; try (intros [A B]; apply B). + destruct i; try (intros [A B]; apply B). intros. subst c. simpl. auto. Qed. @@ -345,7 +345,7 @@ Proof. induction c; simpl; intros. inv H. auto. monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). - generalize (Mach.is_label_correct lbl a). + generalize (Mach.is_label_correct lbl a). destruct (Mach.is_label lbl a); intros. subst a. simpl in EQ. exists x; auto. eapply IHc; eauto. @@ -361,7 +361,7 @@ Lemma transl_find_label: Proof. intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. simpl. - eapply transl_code_label; eauto. + eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -376,17 +376,17 @@ Lemma find_label_goto_label: rs PC = Vptr b ofs -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> exists tc', exists rs', - goto_label tf lbl rs m = Next rs' m + goto_label tf lbl rs m = Next rs' m /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' /\ forall r, r <> PC -> rs'#r = rs#r. Proof. - intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. + intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. intros [tc [A B]]. exploit label_pos_code_tail; eauto. instantiate (1 := 0). intros [pos' [P [Q R]]]. exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))). split. unfold goto_label. rewrite P. rewrite H1. auto. - split. rewrite Pregmap.gss. constructor; auto. + split. rewrite Pregmap.gss. constructor; auto. rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q. auto. omega. generalize (transf_function_no_overflow _ _ H0). omega. @@ -399,10 +399,10 @@ Lemma return_address_exists: forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> exists ra, return_address_offset f c ra. Proof. - intros. eapply Asmgenproof0.return_address_exists; eauto. -- intros. exploit transl_instr_label; eauto. + intros. eapply Asmgenproof0.return_address_exists; eauto. +- intros. exploit transl_instr_label; eauto. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. -- intros. monadInv H0. +- intros. monadInv H0. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. exists x; exists true; split; auto. repeat constructor. - exact transf_function_no_overflow. @@ -470,10 +470,10 @@ Lemma exec_straight_steps: plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. Proof. - intros. inversion H2. subst. monadInv H7. - exploit H3; eauto. intros [rs2 [A [B C]]]. + intros. inversion H2. subst. monadInv H7. + exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. - eapply exec_straight_exec; eauto. + eapply exec_straight_exec; eauto. econstructor; eauto. eapply exec_straight_at; eauto. Qed. @@ -498,15 +498,15 @@ Proof. 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. + exploit exec_straight_steps_2; eauto. intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. + 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. + eapply exec_straight_steps_1; eauto. econstructor; eauto. - eapply find_instr_tail. eauto. + eapply find_instr_tail. eauto. rewrite C. eexact GOTO. traceEq. econstructor; eauto. @@ -531,8 +531,8 @@ Definition measure (s: Mach.state) : nat := Remark preg_of_not_R12: forall r, negb (mreg_eq r R12) = true -> IR IR12 <> preg_of r. Proof. - intros. change (IR IR12) with (preg_of R12). red; intros. - exploit preg_of_injective; eauto. intros; subst r. + intros. change (IR IR12) with (preg_of R12). red; intros. + exploit preg_of_injective; eauto. intros; subst r. unfold proj_sumbool in H; rewrite dec_eq_true in H; discriminate. Qed. @@ -547,8 +547,8 @@ Proof. induction 1; intros; inv MS. - (* Mlabel *) - left; eapply exec_straight_steps; eauto; intros. - monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. + left; eapply exec_straight_steps; eauto; intros. + monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. split. apply agree_nextinstr; auto. simpl; congruence. - (* Mgetstack *) @@ -564,7 +564,7 @@ Proof. - (* Msetstack *) unfold store_stack in H. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. - exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. left; eapply exec_straight_steps; eauto. rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. @@ -574,11 +574,11 @@ Proof. - (* Mgetparam *) assert (f0 = f) by congruence; subst f0. - unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. - exploit Mem.loadv_extends. eauto. eexact H1. auto. + exploit Mem.loadv_extends. eauto. eexact H1. auto. intros [v' [C D]]. Opaque loadind. left; eapply exec_straight_steps; eauto; intros. @@ -587,63 +587,63 @@ Opaque loadind. exploit loadind_correct. eexact EQ. instantiate (2 := rs0). rewrite DXP; eauto. intros [rs1 [P [Q R]]]. - exists rs1; split. eauto. + exists rs1; split. eauto. split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. - simpl; intros. rewrite R; auto with asmgen. + simpl; intros. rewrite R; auto with asmgen. apply preg_of_not_R12; auto. (* GPR11 does not contain parent *) exploit loadind_int_correct. eexact A. instantiate (1 := IR12). intros [rs1 [P [Q R]]]. - exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]]. + exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. intros [rs2 [S [T U]]]. exists rs2; split. eapply exec_straight_trans; eauto. split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. instantiate (1 := rs1#IR12 <- (rs2#IR12)). intros. rewrite Pregmap.gso; auto with asmgen. - congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR12). congruence. auto with asmgen. - simpl; intros. rewrite U; auto with asmgen. + congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' IR12). congruence. auto with asmgen. + simpl; intros. rewrite U; auto with asmgen. apply preg_of_not_R12; auto. - (* Mop *) - assert (eval_operation tge sp op rs##args m = Some v). + assert (eval_operation tge sp op rs##args m = Some v). rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. - intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. left; eapply exec_straight_steps; eauto; intros. simpl in TR. exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto). exists rs2; split. eauto. split. eapply agree_set_undef_mreg; eauto with asmgen. - simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. + simpl. destruct op; try congruence. destruct ep; simpl; try congruence. intros. rewrite R; auto. apply preg_of_not_R12; auto. exact I. - (* Mload *) - assert (eval_addressing tge sp addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. exploit Mem.loadv_extends; eauto. intros [v' [C D]]. left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. + exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. exists rs2; split. eauto. split. eapply agree_set_undef_mreg; eauto. congruence. simpl; congruence. - (* Mstore *) - assert (eval_addressing tge sp addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [C D]]. left; eapply exec_straight_steps; eauto. - intros. simpl in TR. + intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. - split. eapply agree_undef_regs; eauto. + split. eapply agree_undef_regs; eauto. simpl; congruence. - (* Mcall *) assert (f0 = f) by congruence. subst f0. - inv AT. + inv AT. assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. destruct ros as [rf|fid]; simpl in H; monadInv H5. @@ -659,23 +659,23 @@ Opaque loadind. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. - econstructor; eauto. + econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. + simpl. eapply agree_exten; eauto. intros. Simpl. Simpl. rewrite <- H2. auto. + (* Direct call *) generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). - econstructor; eauto. + econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. - econstructor; eauto. + econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl. @@ -692,7 +692,7 @@ Opaque loadind. unfold chunk_of_type. rewrite (sp_val _ _ _ AG). intros [ra' [C D]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. - exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. assert (X: forall k, exists rs2, exec_straight tge tf (loadind_int IR13 (fn_retaddr_ofs f) IR14 @@ -702,13 +702,13 @@ Opaque loadind. /\ rs2#RA = parent_ra s /\ forall r, if_preg r = true -> r <> SP -> r <> IR14 -> rs2#r = rs0#r). { - intros. - exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. + intros. + exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. econstructor; split. - eapply exec_straight_trans. eexact P. apply exec_straight_one. - simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. - rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. - split. Simpl. split. Simpl. intros. Simpl. + eapply exec_straight_trans. eexact P. apply exec_straight_one. + simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. + split. Simpl. split. Simpl. intros. Simpl. } destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) @@ -718,45 +718,45 @@ Opaque loadind. assert (rs0 x0 = Vptr f' Int.zero). exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. destruct (X (Pbreg x0 sig :: x)) as [rs2 [P [Q [R S]]]]. - exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. + exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. intros [ofs' [Y Z]]. left; econstructor; split. - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eauto. eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl. reflexivity. + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eauto. eapply functions_transl; eauto. + eapply find_instr_tail; eauto. + simpl. reflexivity. traceEq. - econstructor; eauto. - split. Simpl. eapply parent_sp_def; eauto. - intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + econstructor; eauto. + split. Simpl. eapply parent_sp_def; eauto. + intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. Simpl. rewrite S; auto with asmgen. rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen. rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen. + (* Direct call *) destruct (X (Pbsymb fid sig :: x)) as [rs2 [P [Q [R S]]]]. - exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. + exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. intros [ofs' [Y Z]]. left; econstructor; split. - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eauto. eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. reflexivity. + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eauto. eapply functions_transl; eauto. + eapply find_instr_tail; eauto. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. reflexivity. traceEq. econstructor; eauto. - split. Simpl. eapply parent_sp_def; eauto. - intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + split. Simpl. eapply parent_sp_def; eauto. + intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. - (* Mbuiltin *) - inv AT. monadInv H4. + inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. - left. econstructor; split. apply plus_one. + left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - erewrite <- sp_val by eauto. + erewrite <- sp_val by eauto. eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. @@ -770,12 +770,12 @@ Opaque loadind. rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. + eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H4. + inv AT. monadInv H4. exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. @@ -793,9 +793,9 @@ Opaque loadind. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. rewrite EC in B. destruct B as [Bpos Bneg]. - econstructor; econstructor; econstructor; split. eexact A. + econstructor; econstructor; econstructor; split. eexact A. split. eapply agree_undef_regs; eauto with asmgen. - simpl. rewrite Bpos. reflexivity. + simpl. rewrite Bpos. reflexivity. - (* Mcond false *) exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. @@ -803,7 +803,7 @@ Opaque loadind. destruct (transl_cond_correct tge tf cond args _ rs0 m' _ TR) as [rs' [A [B C]]]. rewrite EC in B. destruct B as [Bpos Bneg]. econstructor; split. - eapply exec_straight_trans. eexact A. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. rewrite Bpos. reflexivity. auto. split. eapply agree_undef_regs; eauto with asmgen. intros; Simpl. @@ -811,32 +811,32 @@ Opaque loadind. - (* Mjumptable *) assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H6. + inv AT. monadInv H6. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H5); intro NOOV. exploit find_label_goto_label. eauto. eauto. - instantiate (2 := rs0#IR14 <- Vundef). + instantiate (2 := rs0#IR14 <- Vundef). Simpl. eauto. - eauto. + eauto. intros [tc' [rs' [A [B C]]]]. exploit ireg_val; eauto. rewrite H. intros LD; inv LD. left; econstructor; split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail; eauto. + apply plus_one. econstructor; eauto. + eapply find_instr_tail; eauto. simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. - econstructor; eauto. - eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. Simpl. + econstructor; eauto. + eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. Simpl. congruence. - (* Mreturn *) assert (f0 = f) by congruence. subst f0. - inversion AT; subst. + inversion AT; subst. assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. monadInv H6. @@ -849,40 +849,40 @@ Opaque loadind. /\ rs2#RA = parent_ra s /\ forall r, if_preg r = true -> r <> SP -> r <> IR14 -> rs2#r = rs0#r). { - intros. - exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. + intros. + exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]]. econstructor; split. - eapply exec_straight_trans. eexact P. apply exec_straight_one. - simpl. rewrite R; auto with asmgen. rewrite A. - rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. + eapply exec_straight_trans. eexact P. apply exec_straight_one. + simpl. rewrite R; auto with asmgen. rewrite A. + rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto. split. Simpl. split. Simpl. - intros. Simpl. + intros. Simpl. } destruct (X (Pbreg IR14 (Mach.fn_sig f) :: x)) as [rs2 [P [Q [R S]]]]. - exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. + exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. intros [ofs' [Y Z]]. left; econstructor; split. - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eauto. eapply functions_transl; eauto. - eapply find_instr_tail; eauto. + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eauto. eapply functions_transl; eauto. + eapply find_instr_tail; eauto. simpl. reflexivity. traceEq. - econstructor; eauto. + econstructor; eauto. split. Simpl. eapply parent_sp_def; eauto. intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. - generalize EQ; intros EQ'. monadInv EQ'. + generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. - monadInv EQ0. - unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + monadInv EQ0. + unfold store_stack in *. + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. - exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. + exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. - exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. + exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. intros [m3' [P Q]]. (* Execution of function prologue *) set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))). @@ -894,34 +894,34 @@ Opaque loadind. rewrite <- H5 at 2; unfold fn_code. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. + rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. simpl. auto. - simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). + simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P. - rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto. + rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto. left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. - econstructor; eauto. + eapply exec_straight_steps_1; eauto. omega. constructor. + econstructor; eauto. change (rs3 PC) with (Val.add (Val.add (rs0 PC) Vone) Vone). rewrite ATPC. simpl. constructor; eauto. - subst x. eapply code_tail_next_int. omega. - eapply code_tail_next_int. omega. constructor. + subst x. eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. constructor. unfold rs3, rs2. apply agree_nextinstr. apply agree_nextinstr. - eapply agree_change_sp. + eapply agree_change_sp. apply agree_undef_regs with rs0; eauto. intros. Simpl. congruence. - (* external function *) exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. - exploit extcall_arguments_match; eauto. + exploit extcall_arguments_match; eauto. intros [args' [C D]]. exploit external_call_mem_extends'; eauto. intros [res' [m2' [P [Q [R S]]]]]. left; econstructor; split. - apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved'; eauto. + apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply agree_set_other; auto with asmgen. @@ -946,20 +946,20 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. - unfold Genv.symbol_address. + split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. + unfold Genv.symbol_address. rewrite (transform_partial_program_main _ _ TRANSF). - rewrite symbols_preserved. + rewrite symbols_preserved. unfold ge; rewrite H1. auto. Qed. Lemma transf_final_states: - forall st1 st2 r, + forall st1 st2 r, match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. Proof. intros. inv H0. inv H. inv STACKS. constructor. - auto. - compute in H1. inv H1. + auto. + compute in H1. inv H1. generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. Qed. -- cgit