diff options
Diffstat (limited to 'ia32/Asmgenproof.v')
| -rw-r--r-- | ia32/Asmgenproof.v | 248 |
1 files changed, 124 insertions, 124 deletions
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index d91e17a2..105347e7 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -43,17 +43,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: @@ -70,15 +70,15 @@ Lemma functions_transl: Genv.find_funct_ptr tge fb = Some (Internal tf). Proof. intros. exploit functions_translated; eauto. intros [tf' [A B]]. - monadInv B. rewrite H0 in EQ; inv EQ; auto. + monadInv B. rewrite H0 in EQ; inv EQ; auto. 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 *) @@ -88,7 +88,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned. Proof. intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); monadInv EQ0. - omega. + omega. Qed. Lemma exec_straight_exec: @@ -100,7 +100,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: @@ -110,8 +110,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']]. @@ -141,7 +141,7 @@ Section TRANSL_LABEL. Remark mk_mov_label: forall rd rs k c, mk_mov rd rs k = OK c -> tail_nolabel k c. Proof. - unfold mk_mov; intros. + unfold mk_mov; intros. destruct rd; try discriminate; destruct rs; TailNoLabel. Qed. Hint Resolve mk_mov_label: labels. @@ -154,20 +154,20 @@ Qed. Hint Resolve mk_shrximm_label: labels. Remark mk_intconv_label: - forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> + forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> (forall r r', nolabel (f r r')) -> tail_nolabel k c. Proof. - unfold mk_intconv; intros. TailNoLabel. + unfold mk_intconv; intros. TailNoLabel. Qed. Hint Resolve mk_intconv_label: labels. Remark mk_smallstore_label: - forall f addr r k c, mk_smallstore f addr r k = OK c -> + forall f addr r k c, mk_smallstore f addr r k = OK c -> (forall r addr, nolabel (f r addr)) -> tail_nolabel k c. Proof. - unfold mk_smallstore; intros. TailNoLabel. + unfold mk_smallstore; intros. TailNoLabel. Qed. Hint Resolve mk_smallstore_label: labels. @@ -233,7 +233,7 @@ Proof. destruct (Int.eq_dec i Int.zero); TailNoLabel. destruct (Float.eq_dec f Float.zero); TailNoLabel. destruct (Float32.eq_dec f Float32.zero); TailNoLabel. - eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label. Qed. Remark transl_load_label: @@ -262,13 +262,13 @@ Opaque loadind. eapply loadind_label; eauto. eapply storeind_label; eauto. eapply loadind_label; eauto. - eapply tail_nolabel_trans; eapply loadind_label; eauto. + eapply tail_nolabel_trans; eapply loadind_label; eauto. eapply transl_op_label; eauto. eapply transl_load_label; eauto. eapply transl_store_label; eauto. destruct s0; TailNoLabel. destruct s0; TailNoLabel. - eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_jcc_label. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_jcc_label. Qed. Lemma transl_instr_label': @@ -277,7 +277,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. @@ -292,7 +292,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. @@ -307,7 +307,7 @@ Lemma transl_find_label: end. 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. rewrite transl_code'_transl_code in EQ0; eauto. + monadInv EQ. simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ0; eauto. Qed. End TRANSL_LABEL. @@ -322,17 +322,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. @@ -345,10 +345,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. rewrite transl_code'_transl_code in EQ0. exists x; exists true; split; auto. unfold fn_code. repeat constructor. @@ -417,10 +417,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. @@ -445,15 +445,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. @@ -487,8 +487,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 *) @@ -504,88 +504,88 @@ 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. intros [rs' [P Q]]. exists rs'; split. eauto. - split. eapply agree_undef_regs; eauto. + split. eapply agree_undef_regs; eauto. simpl; intros. rewrite Q; auto with asmgen. Local Transparent destroyed_by_setstack. destruct ty; simpl; intuition congruence. - (* 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. + left; eapply exec_straight_steps; eauto; intros. assert (DIFF: negb (mreg_eq dst DX) = true -> IR EDX <> preg_of dst). - intros. change (IR EDX) with (preg_of DX). red; intros. + intros. change (IR EDX) with (preg_of DX). red; intros. unfold proj_sumbool in H1. destruct (mreg_eq dst DX); try discriminate. elim n. eapply preg_of_injective; eauto. destruct ep; simpl in TR. (* EDX contains parent *) exploit loadind_correct. eexact TR. - instantiate (2 := rs0). rewrite DXP; eauto. + 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. simpl; intros. rewrite R; auto. (* EDX does not contain parent *) monadInv TR. exploit loadind_correct. eexact EQ0. eauto. intros [rs1 [P [Q R]]]. simpl in Q. exploit loadind_correct. eexact EQ. instantiate (2 := rs1). rewrite Q. eauto. - intros [rs2 [S [T U]]]. + intros [rs2 [S [T U]]]. exists rs2; split. eapply exec_straight_trans; eauto. split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto. simpl; intros. rewrite U; 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]]]. + 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. simpl; congruence. - (* 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. - exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + 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 tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. destruct ros as [rf|fid]; simpl in H; monadInv H5. @@ -601,13 +601,13 @@ 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. - simpl. eauto. - econstructor; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. + econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simplifs. - Simplifs. rewrite <- H2. auto. + Simplifs. 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). @@ -615,9 +615,9 @@ 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. 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. Simplifs. @@ -625,7 +625,7 @@ Opaque loadind. - (* Mtailcall *) assert (f0 = f) by congruence. subst f0. - inv AT. + inv AT. assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. @@ -633,7 +633,7 @@ Opaque loadind. exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. 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]]. destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) assert (rs rf = Vptr f' Int.zero). @@ -644,26 +644,26 @@ Opaque loadind. generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. - apply star_one. eapply exec_step_internal. + apply star_one. eapply exec_step_internal. transitivity (Val.add rs0#PC Vone). auto. rewrite <- H4. simpl. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. econstructor; eauto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. eapply agree_change_sp; eauto. eapply parent_sp_def; eauto. - Simplifs. rewrite Pregmap.gso; auto. + Simplifs. rewrite Pregmap.gso; auto. generalize (preg_of_not_SP rf). rewrite (ireg_of_eq _ _ EQ1). congruence. + (* Direct call *) generalize (code_tail_next_int _ _ _ _ NOOV H8). intro CT1. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. - apply star_one. eapply exec_step_internal. + apply star_one. eapply exec_step_internal. transitivity (Val.add rs0#PC Vone). auto. rewrite <- H4. simpl. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. econstructor; eauto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. @@ -671,16 +671,16 @@ Opaque loadind. rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* 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. @@ -695,12 +695,12 @@ Opaque loadind. auto with asmgen. simpl; intros. intuition congruence. apply agree_nextinstr_nf. 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. @@ -717,26 +717,26 @@ Opaque loadind. left; eapply exec_straight_steps_goto; eauto. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR) - as [rs' [A [B C]]]. + as [rs' [A [B C]]]. rewrite EC in B. destruct (testcond_for_condition cond); simpl in *. (* simple jcc *) exists (Pjcc c1 lbl); exists k; exists rs'. split. eexact A. - split. eapply agree_exten; eauto. + split. eapply agree_exten; eauto. simpl. rewrite B. auto. (* jcc; jcc *) destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B. - destruct b1. + destruct b1. (* first jcc jumps *) exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'. split. eexact A. - split. eapply agree_exten; eauto. + split. eapply agree_exten; eauto. simpl. rewrite TC1. auto. (* second jcc jumps *) exists (Pjcc c2 lbl); exists k; exists (nextinstr rs'). - split. eapply exec_straight_trans. eexact A. + split. eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl. rewrite TC1. auto. auto. split. eapply agree_exten; eauto. intros; Simplifs. @@ -745,23 +745,23 @@ Opaque loadind. (* jcc2 *) destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B. - destruct (andb_prop _ _ H3). subst. + destruct (andb_prop _ _ H3). subst. exists (Pjcc2 c1 c2 lbl); exists k; exists rs'. split. eexact A. - split. eapply agree_exten; eauto. + split. eapply agree_exten; eauto. simpl. rewrite TC1; rewrite TC2; auto. - (* Mcond false *) exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR) - as [rs' [A [B C]]]. + as [rs' [A [B C]]]. rewrite EC in B. 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. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B. eauto. auto. split. apply agree_nextinstr. eapply agree_exten; eauto. simpl; congruence. (* jcc ; jcc *) @@ -769,8 +769,8 @@ Opaque loadind. destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B. destruct (orb_false_elim _ _ H1); subst. econstructor; split. - eapply exec_straight_trans. eexact A. - eapply exec_straight_two. simpl. rewrite TC1. eauto. auto. + eapply exec_straight_trans. eexact A. + eapply exec_straight_two. simpl. rewrite TC1. eauto. auto. simpl. rewrite eval_testcond_nextinstr. rewrite TC2. eauto. auto. auto. split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten; eauto. simpl; congruence. @@ -778,9 +778,9 @@ Opaque loadind. destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; destruct (eval_testcond c2 rs') as [b2|] eqn:TC2; inv B. exists (nextinstr rs'); split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. - rewrite TC1; rewrite TC2. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. + rewrite TC1; rewrite TC2. destruct b1. simpl in *. subst b2. auto. auto. auto. split. apply agree_nextinstr. eapply agree_exten; eauto. @@ -788,41 +788,41 @@ 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. + exploit find_label_goto_label; 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. eauto. - econstructor; eauto. -Transparent destroyed_by_jumptable. + econstructor; eauto. +Transparent destroyed_by_jumptable. simpl. eapply agree_exten; eauto. intros. rewrite C; auto with asmgen. congruence. - (* Mreturn *) assert (f0 = f) by congruence. subst f0. - inv AT. + inv AT. assert (NOOV: list_length_z tf.(fn_code) <= 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. exploit code_tail_next_int; eauto. intro CT1. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. rewrite C. rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. - apply star_one. eapply exec_step_internal. + apply star_one. eapply exec_step_internal. transitivity (Val.add rs0#PC Vone). auto. rewrite <- H3. simpl. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. constructor; auto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. @@ -833,40 +833,40 @@ Transparent destroyed_by_jumptable. generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inv EQ1. monadInv EQ0. rewrite transl_code'_transl_code in EQ1. - unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + 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]]. left; econstructor; split. - apply plus_one. econstructor; eauto. + apply plus_one. econstructor; eauto. simpl. rewrite Int.unsigned_zero. simpl. eauto. simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F. simpl in P. rewrite ATLR. rewrite P. eauto. econstructor; eauto. - unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. + unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. rewrite ATPC. simpl. constructor; eauto. - unfold fn_code. eapply code_tail_next_int. simpl in g. omega. - constructor. + unfold fn_code. eapply code_tail_next_int. simpl in g. omega. + constructor. apply agree_nextinstr. eapply agree_change_sp; eauto. Transparent destroyed_at_function_entry. apply agree_undef_regs with rs0; eauto. - simpl; intros. apply Pregmap.gso; auto with asmgen. tauto. - congruence. + simpl; intros. apply Pregmap.gso; auto with asmgen. tauto. + congruence. intros. Simplifs. eapply agree_sp; eauto. - (* 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. unfold loc_external_result. @@ -891,19 +891,19 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. + 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. constructor. auto. - compute in H1. inv H1. + intros. inv H0. inv H. constructor. auto. + compute in H1. inv H1. generalize (preg_val _ _ _ AX AG). rewrite H2. intros LD; inv LD. auto. Qed. |