From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgenproof.v | 402 ++++++++++++++++++++++++++++++++---------------------- 1 file changed, 242 insertions(+), 160 deletions(-) (limited to 'arm/Asmgenproof.v') diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index cc4d7ac5..d3e082f0 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -558,56 +558,84 @@ Inductive match_stack: list Machconcr.stackframe -> Prop := wt_function f -> incl c f.(fn_code) -> transl_code_at_pc ra fb f c -> + sp <> Vundef -> + ra <> Vundef -> match_stack s -> match_stack (Stackframe fb sp ra c :: s). Inductive match_states: Machconcr.state -> Asm.state -> Prop := | match_states_intro: - forall s fb sp c ms m rs f + forall s fb sp c ms m rs f m' (STACKS: match_stack s) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (WTF: wt_function f) (INCL: incl c f.(fn_code)) (AT: transl_code_at_pc (rs PC) fb f c) - (AG: agree ms sp rs), + (AG: agree ms sp rs) + (MEXT: Mem.extends m m'), match_states (Machconcr.State s fb sp c ms m) - (Asm.State rs m) + (Asm.State rs m') | match_states_call: - forall s fb ms m rs + forall s fb ms m rs m' (STACKS: match_stack s) (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (ATLR: rs IR14 = parent_ra s), + (ATLR: rs IR14 = parent_ra s) + (MEXT: Mem.extends m m'), match_states (Machconcr.Callstate s fb ms m) - (Asm.State rs m) + (Asm.State rs m') | match_states_return: - forall s ms m rs + forall s ms m rs m' (STACKS: match_stack s) (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s), + (ATPC: rs PC = parent_ra s) + (MEXT: Mem.extends m m'), match_states (Machconcr.Returnstate s ms m) - (Asm.State rs m). + (Asm.State rs m'). Lemma exec_straight_steps: - forall s fb sp m1 f c1 rs1 c2 m2 ms2, + forall s fb sp m1 m1' f c1 rs1 c2 m2 ms2, match_stack s -> Genv.find_funct_ptr ge fb = Some (Internal f) -> wt_function f -> incl c2 f.(fn_code) -> transl_code_at_pc (rs1 PC) fb f c1 -> - (exists rs2, - exec_straight tge (transl_function f) (transl_code f c1) rs1 m1 (transl_code f c2) rs2 m2 + Mem.extends m1 m1' -> + (exists m2', + Mem.extends m2 m2' /\ + exists rs2, + exec_straight tge (transl_function f) (transl_code f c1) rs1 m1' (transl_code f c2) rs2 m2' /\ agree ms2 sp rs2) -> exists st', - plus step tge (State rs1 m1) E0 st' /\ + plus step tge (State rs1 m1') E0 st' /\ match_states (Machconcr.State s fb sp c2 ms2 m2) st'. Proof. - intros. destruct H4 as [rs2 [A B]]. - exists (State rs2 m2); split. + intros. destruct H5 as [m2' [A [rs2 [B C]]]]. + exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. econstructor; eauto. eapply exec_straight_at; eauto. Qed. +Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. +Proof. induction 1; simpl. congruence. auto. Qed. + +Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. induction 1; simpl. unfold Vzero. congruence. auto. Qed. + +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. +Qed. + +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. +Proof. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. +Qed. + (** We need to show that, in the simulation diagram, we cannot take infinitely many Mach transitions that correspond to zero transitions on the ARM side. Actually, all Mach transitions @@ -642,6 +670,7 @@ Lemma exec_Mlabel_prop: Proof. intros; red; intros; inv MS. left; eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. exists (nextinstr rs); split. simpl. apply exec_straight_one. reflexivity. reflexivity. apply agree_nextinstr; auto. @@ -658,18 +687,15 @@ Proof. intros; red; intros; inv MS. unfold load_stack in H. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - generalize (loadind_correct tge (transl_function f) IR13 ofs ty - dst (transl_code f c) rs m v H H1). + intro WTI. inv WTI. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + exploit loadind_correct. eexact A. reflexivity. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. - simpl. exists rs2; split. auto. - apply agree_exten_2 with (rs#(preg_of dst) <- v). - auto with ppcgen. - intros. case (preg_eq r0 (preg_of dst)); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. + exists m'; split; auto. + simpl. exists rs2; split. eauto. + apply agree_set_mreg with rs; auto. congruence. auto with ppcgen. Qed. Lemma exec_Msetstack_prop: @@ -683,16 +709,16 @@ Proof. intros; red; intros; inv MS. unfold store_stack in H. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - rewrite (sp_val _ _ _ AG) in H. - rewrite (preg_val ms sp rs) in H; auto. - assert (NOTE: IR13 <> IR14) by congruence. - generalize (storeind_correct tge (transl_function f) IR13 ofs ty - src (transl_code f c) rs m m' H H1 NOTE). + intro WTI. inv WTI. + exploit preg_val; eauto. instantiate (1 := src). intros A. + exploit Mem.storev_extends; eauto. intros [m2 [B C]]. + rewrite (sp_val _ _ _ AG) in B. + exploit storeind_correct. eexact B. reflexivity. congruence. intros [rs2 [EX OTH]]. left; eapply exec_straight_steps; eauto with coqlib. - exists rs2; split; auto. - apply agree_exten_2 with rs; auto. + exists m2; split; auto. + exists rs2; split; eauto. + apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mgetparam_prop: @@ -703,29 +729,33 @@ Lemma exec_Mgetparam_prop: load_stack m sp Tint f.(fn_link_ofs) = Some parent -> load_stack m parent ty ofs = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set dst v ms) m). + (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inv WTI. auto. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. eauto. + intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (parent' = parent). inv B. auto. simpl in H1; discriminate. subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. eauto. + intros [v' [C D]]. exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_link_ofs) IR14 - rs m parent (loadind IR14 ofs ty dst (transl_code f c))). - rewrite <- (sp_val ms sp rs); auto. + rs m' parent (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))). + auto. intros [rs1 [EX1 [RES1 OTH1]]]. - exploit (loadind_correct tge (transl_function f) IR14 ofs ty dst - (transl_code f c) rs1 m v). - rewrite RES1. auto. - generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. auto. + exploit (loadind_correct tge (transl_function f) IR14 ofs (mreg_type dst) dst + (transl_code f c) rs1 m' v'). + rewrite RES1. auto. auto. intros [rs2 [EX2 [RES2 OTH2]]]. left. eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. exists rs2; split; simpl. eapply exec_straight_trans; eauto. - apply agree_exten_2 with (rs1#(preg_of dst) <- v). - apply agree_set_mreg. - apply agree_exten_2 with rs; auto. - intros. case (preg_eq r (preg_of dst)); intro. - subst r. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso; auto. + apply agree_set_mreg with rs1. + apply agree_set_mreg with rs. auto. auto. auto with ppcgen. + congruence. auto with ppcgen. Qed. Lemma exec_Mop_prop: @@ -734,14 +764,27 @@ Lemma exec_Mop_prop: (ms : mreg -> val) (m : mem) (v : val), eval_operation ge sp op ms ## args = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 - (Machconcr.State s fb sp c (Regmap.set res v ms) m). + (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. + intros [v' [A B]]. + assert (C: eval_operation tge sp op rs ## (preg_of ## args) = Some v'). + rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. + rewrite (sp_val _ _ _ AG) in C. + exploit transl_op_correct; eauto. intros [rs' [P [Q R]]]. left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_op_correct; auto. - rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exists m'; split; auto. + exists rs'; split. simpl. eexact P. + assert (agree (Regmap.set res v ms) sp rs'). + apply agree_set_mreg with rs; auto. congruence. + auto with ppcgen. + assert (agree (Regmap.set res v (undef_temps ms)) sp rs'). + apply agree_set_undef_mreg with rs; auto. congruence. + auto with ppcgen. + destruct op; assumption. Qed. Lemma exec_Mload_prop: @@ -752,7 +795,7 @@ Lemma exec_Mload_prop: eval_addressing ge sp addr ms ## args = Some a -> Mem.loadv chunk m a = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m) - E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m). + E0 (Machconcr.State s fb sp c (Regmap.set dst v (undef_temps ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -760,12 +803,14 @@ Proof. assert (eval_addressing tge sp addr ms##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. left; eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. destruct chunk; simpl; simpl in H6; (eapply transl_load_int_correct || eapply transl_load_float_correct); eauto; intros; reflexivity. Qed. -Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed. +Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed. + Lemma exec_Mstore_prop: forall (s : list stackframe) (fb : block) (sp : val) (chunk : memory_chunk) (addr : addressing) (args : list mreg) @@ -774,7 +819,7 @@ Lemma exec_Mstore_prop: eval_addressing ge sp addr ms ## args = Some a -> Mem.storev chunk m a (ms src) = Some m' -> exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 - (Machconcr.State s fb sp c ms m'). + (Machconcr.State s fb sp c (undef_temps ms) m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -788,6 +833,7 @@ Proof. simpl; (eapply transl_store_int_correct || eapply transl_store_float_correct); eauto; intros; simpl; auto. + econstructor; split. rewrite H2. eauto. intros. apply Pregmap.gso; auto. Qed. Lemma exec_Mcall_prop: @@ -817,17 +863,20 @@ Proof. rewrite RA_EQ. change (rs2 IR14) with (Val.add (rs PC) Vone). rewrite <- H2. reflexivity. - assert (AG3: agree ms sp rs2). - unfold rs2; auto 8 with ppcgen. - left; exists (State rs2 m); split. + assert (AG3: agree ms sp rs2). + unfold rs2. apply agree_set_other; auto. apply agree_set_other; auto. + left; exists (State rs2 m'); split. apply plus_one. destruct ros; simpl in H5. econstructor. eauto. apply functions_transl. eexact H0. eapply find_instr_tail. eauto. - simpl. rewrite <- (ireg_val ms sp rs); auto. - simpl in H. destruct (ms m0); try congruence. - generalize H; predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H7. - auto. + simpl. + assert (rs (ireg_of m0) = Vptr f' Int.zero). + generalize (ireg_val _ _ _ m0 AG H3). intro LD. simpl in H. inv LD. + destruct (ms m0); try congruence. + generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence. + rewrite <- H7 in H; congruence. + rewrite H6. auto. econstructor. eauto. apply functions_transl. eexact H0. eapply find_instr_tail. eauto. simpl. unfold symbol_offset. rewrite symbols_preserved. @@ -835,8 +884,19 @@ Proof. econstructor; eauto. econstructor; eauto with coqlib. rewrite RA_EQ. econstructor; eauto. + eapply agree_sp_def; eauto. congruence. Qed. +Lemma agree_change_sp: + forall ms sp rs sp', + agree ms sp rs -> sp' <> Vundef -> + agree ms sp' (rs#IR13 <- sp'). +Proof. + intros. inv H. split. apply Pregmap.gss. auto. + intros. rewrite Pregmap.gso; auto with ppcgen. +Qed. + + Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', find_function_ptr ge ros ms = Some f' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms m'). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -848,23 +908,31 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff loadind_int IR13 (fn_retaddr_ofs f) IR14 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)). unfold call_instr; destruct ros; auto. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. + exploit Mem.loadv_extends. eauto. eexact H2. auto. + intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. + exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14 - rs m (parent_ra s) + rs m'0 (parent_ra s) (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c)) as [rs1 [EXEC1 [RES1 OTH1]]]. rewrite <- (sp_val ms (Vptr stk soff) rs); auto. set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))). assert (EXEC2: exec_straight tge (transl_function f) - (transl_code f (Mtailcall sig ros :: c)) rs m - (call_instr :: transl_code f c) rs2 m'). + (transl_code f (Mtailcall sig ros :: c)) rs m'0 + (call_instr :: transl_code f c) rs2 m2'). rewrite TR. eapply exec_straight_trans. eexact EXEC1. apply exec_straight_one. simpl. rewrite OTH1; auto with ppcgen. rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - unfold load_stack in H1. simpl in H1. simpl. rewrite H1. - rewrite H3. auto. auto. + simpl chunk_of_type in A. rewrite A. + rewrite P. auto. auto. set (rs3 := rs2#PC <- (Vptr f' Int.zero)). - left. exists (State rs3 m'); split. + left. exists (State rs3 m2'); split. (* Execution *) eapply plus_right'. eapply exec_straight_exec; eauto. inv AT. exploit exec_straight_steps_2; eauto. @@ -877,24 +945,19 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff replace (rs2 (ireg_of m0)) with (Vptr f' Int.zero). auto. unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso. rewrite OTH1; auto with ppcgen. - rewrite <- (ireg_val ms (Vptr stk soff) rs); auto. - destruct (ms m0); try discriminate. - generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H10. - auto. - decEq. auto with ppcgen. decEq. auto with ppcgen. decEq. auto with ppcgen. - replace (symbol_offset tge i Int.zero) with (Vptr f' Int.zero). auto. - unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. + generalize (ireg_val _ _ _ m0 AG H7). intro LD. inv LD. + destruct (ms m0); try congruence. + generalize H. predSpec Int.eq Int.eq_spec i Int.zero; congruence. + rewrite <- H10 in H; congruence. + auto with ppcgen. + unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq. (* Match states *) constructor; auto. - assert (AG1: agree ms (Vptr stk soff) rs1). - eapply agree_exten_2; eauto. - assert (AG2: agree ms (parent_sp s) rs2). - inv AG1. constructor. auto. intros. unfold rs2. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso. auto. auto with ppcgen. - unfold rs3. apply agree_exten_2 with rs2; auto. - intros. rewrite Pregmap.gso; auto. + unfold rs3. apply agree_set_other; auto. + unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff). + apply agree_exten with rs; auto with ppcgen. + apply parent_sp_def. auto. Qed. Lemma exec_Mbuiltin_prop: @@ -904,28 +967,29 @@ Lemma exec_Mbuiltin_prop: (t : trace) (v : val) (m' : mem), external_call ef ge ms ## args m t v m' -> exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t - (Machconcr.State s f sp b (Regmap.set res v ms) m'). + (Machconcr.State s f sp b (Regmap.set res v (undef_temps ms)) m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. + exploit external_call_mem_extends; eauto. eapply preg_vals; eauto. + intros [vres' [m2' [A [B [C D]]]]]. inv AT. simpl in H3. generalize (functions_transl _ _ FIND); intro FN. generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - replace (rs##(preg_of##args)) with (ms##args). - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. - rewrite list_map_compose. apply list_map_exten. intros. - symmetry. eapply preg_val; eauto. + eapply external_call_symbols_preserved; eauto. + eexact symbols_preserved. eexact varinfo_preserved. econstructor; eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite <- H0. simpl. constructor; auto. eapply code_tail_next_int; eauto. - apply sym_not_equal. auto with ppcgen. - auto with ppcgen. + apply sym_not_equal. auto with ppcgen. + apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. + rewrite Pregmap.gss; auto. + intros. rewrite Pregmap.gso; auto. Qed. Lemma exec_Mgoto_prop: @@ -940,16 +1004,16 @@ Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. inv AT. simpl in H3. - generalize (find_label_goto_label f lbl rs m _ _ _ FIND (sym_equal H1) H0). + generalize (find_label_goto_label f lbl rs m' _ _ _ FIND (sym_equal H1) H0). intros [rs2 [GOTO [AT2 INV]]]. - left; exists (State rs2 m); split. + left; exists (State rs2 m'); split. apply plus_one. econstructor; eauto. apply functions_transl; eauto. eapply find_instr_tail; eauto. simpl; auto. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs; auto. + apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mcond_true_prop: @@ -961,32 +1025,32 @@ Lemma exec_Mcond_true_prop: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c' ms m). + (Machconcr.State s fb sp c' (undef_temps ms) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. - pose (k1 := Pbc (crbit_for_cond cond) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m true H3 AG H). - simpl. intros [rs2 [EX [RES AG2]]]. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A. + exploit transl_cond_correct. eauto. eauto. + intros [rs2 [EX [RES OTH]]]. inv AT. simpl in H5. generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. exploit exec_straight_steps_2; eauto. intros [ofs' [PC2 CT2]]. - generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H1). + generalize (find_label_goto_label f lbl rs2 m' _ _ _ FIND PC2 H1). intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. + left; exists (State rs3 m'); split. eapply plus_right'. eapply exec_straight_steps_1; eauto. econstructor; eauto. - eapply find_instr_tail. unfold k1 in CT2. eauto. + eapply find_instr_tail. eauto. simpl. rewrite RES. simpl. auto. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs2; auto. + apply agree_exten_temps with rs; auto. intros. + rewrite INV3; auto with ppcgen. Qed. Lemma exec_Mcond_false_prop: @@ -995,36 +1059,34 @@ Lemma exec_Mcond_false_prop: (c : list Mach.instruction) (ms : mreg -> val) (m : mem), eval_condition cond ms ## args = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 - (Machconcr.State s fb sp c ms m). + (Machconcr.State s fb sp c (undef_temps ms) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). - intro WTI. inversion WTI. - pose (k1 := Pbc (crbit_for_cond cond) lbl :: transl_code f c). - generalize (transl_cond_correct tge (transl_function f) - cond args k1 ms sp rs m false H1 AG H). - simpl. intros [rs2 [EX [RES AG2]]]. + intro WTI. inv WTI. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A. + exploit transl_cond_correct. eauto. eauto. + intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. + exists m'; split; auto. exists (nextinstr rs2); split. simpl. eapply exec_straight_trans. eexact EX. - unfold k1; apply exec_straight_one. - simpl. rewrite RES. reflexivity. - reflexivity. - auto with ppcgen. + apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity. + apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. Qed. Lemma exec_Mjumptable_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction) - (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) + (ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) (c' : Mach.code), - rs arg = Vint n -> + ms arg = Vint n -> list_nth_z tbl (Int.signed n) = Some lbl -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop - (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0 - (Machconcr.State s fb sp c' rs m). + (Machconcr.State s fb sp (Mjumptable arg tbl :: c) ms m) E0 + (Machconcr.State s fb sp c' (undef_temps ms) m). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -1039,19 +1101,21 @@ Proof. omega. inv AT. simpl in H7. set (k1 := Pbtbl IR14 tbl :: transl_code f c). - set (rs1 := nextinstr (rs0 # IR14 <- (Vint (Int.shl n (Int.repr 2))))). + set (rs1 := nextinstr (rs # IR14 <- (Vint (Int.shl n (Int.repr 2))))). generalize (functions_transl _ _ H4); intro FN. generalize (functions_transl_no_overflow _ _ H4); intro NOOV. + assert (rs (ireg_of arg) = Vint n). + exploit ireg_val; eauto. intros LD. inv LD. auto. congruence. assert (exec_straight tge (transl_function f) - (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs0 m - k1 rs1 m). + (Pmov IR14 (SOlslimm (ireg_of arg) (Int.repr 2)) :: k1) rs m' + k1 rs1 m'). apply exec_straight_one. - simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity. + simpl. rewrite H8. reflexivity. reflexivity. exploit exec_straight_steps_2; eauto. intros [ofs' [PC1 CT1]]. - generalize (find_label_goto_label f lbl rs1 m _ _ _ FIND PC1 H2). + generalize (find_label_goto_label f lbl rs1 m' _ _ _ FIND PC1 H2). intros [rs3 [GOTO [AT3 INV3]]]. - left; exists (State rs3 m); split. + left; exists (State rs3 m'); split. eapply plus_right'. eapply exec_straight_steps_1; eauto. econstructor; eauto. @@ -1064,15 +1128,25 @@ Opaque Zmod. Opaque Zdiv. change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs1; auto. + apply agree_exten with rs1; auto with ppcgen. unfold rs1. apply agree_nextinstr. apply agree_set_other; auto with ppcgen. + apply agree_undef_temps; auto. Qed. Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms m'). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. + intros [parent' [A B]]. + exploit lessdef_parent_sp; eauto. intros. subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14 - rs m (parent_ra s) + rs m'0 (parent_ra s) (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)). rewrite <- (sp_val ms (Vptr stk soff) rs); auto. intros [rs1 [EXEC1 [RES1 OTH1]]]. @@ -1080,14 +1154,13 @@ Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : assert (EXEC2: exec_straight tge (transl_function f) (loadind_int IR13 (fn_retaddr_ofs f) IR14 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c)) - rs m (Pbreg IR14 :: transl_code f c) rs2 m'). + rs m'0 (Pbreg IR14 :: transl_code f c) rs2 m2'). eapply exec_straight_trans. eexact EXEC1. apply exec_straight_one. simpl. rewrite OTH1; try congruence. - rewrite <- (sp_val ms (Vptr stk soff) rs); auto. - unfold load_stack in H0. simpl in H0; simpl; rewrite H0. rewrite H2. reflexivity. - reflexivity. + rewrite <- (sp_val ms (Vptr stk soff) rs); auto. + simpl chunk_of_type in A. rewrite A. rewrite E. auto. auto. set (rs3 := rs2#PC <- (parent_ra s)). - left; exists (State rs3 m'); split. + left; exists (State rs3 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. inv AT. exploit exec_straight_steps_2; eauto. @@ -1100,15 +1173,13 @@ Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : traceEq. (* match states *) constructor. auto. - assert (AG1: agree ms (Vptr stk soff) rs1). - apply agree_exten_2 with rs; auto. - assert (AG2: agree ms (parent_sp s) rs2). - constructor. reflexivity. intros; unfold rs2. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso; auto with ppcgen. - inv AG1; auto. - unfold rs3. auto with ppcgen. - reflexivity. + apply agree_exten with rs2. + unfold rs2. apply agree_nextinstr. apply agree_change_sp with (Vptr stk soff). + apply agree_exten with rs; auto with ppcgen. + apply parent_sp_def. auto. + intros. unfold rs3. apply Pregmap.gso; auto with ppcgen. + unfold rs3. apply Pregmap.gss. + auto. Qed. Hypothesis wt_prog: wt_program prog. @@ -1132,21 +1203,26 @@ Proof. generalize (functions_transl_no_overflow _ _ H); intro NOOV. set (rs2 := nextinstr (rs#IR13 <- sp)). set (rs3 := nextinstr rs2). + exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + intros [m1' [A B]]. + unfold store_stack in *; simpl chunk_of_type in *. + exploit Mem.storev_extends. eexact B. eauto. auto. auto. + intros [m2' [C D]]. + exploit Mem.storev_extends. eexact D. eauto. auto. auto. + intros [m3' [E F]]. (* Execution of function prologue *) assert (EXEC_PROLOGUE: exec_straight tge (transl_function f) - (transl_function f) rs m - (transl_code f f.(fn_code)) rs3 m3). + (transl_function f) rs m' + (transl_code f f.(fn_code)) rs3 m3'). unfold transl_function at 2. - apply exec_straight_two with rs2 m2. - unfold exec_instr. rewrite H0. fold sp. - rewrite <- (sp_val ms (parent_sp s) rs); auto. - unfold store_stack in H1. change Mint32 with (chunk_of_type Tint). rewrite H1. - auto. + apply exec_straight_two with rs2 m2'. + unfold exec_instr. rewrite A. fold sp. + rewrite <- (sp_val ms (parent_sp s) rs); auto. rewrite C. auto. unfold exec_instr. unfold eval_shift_addr. unfold exec_store. change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR. - unfold store_stack in H2. change Mint32 with (chunk_of_type Tint). rewrite H2. - auto. auto. auto. + rewrite E. auto. + auto. auto. (* Agreement at end of prologue *) assert (AT3: transl_code_at_pc rs3#PC fb f f.(fn_code)). change (rs3 PC) with (Val.add (Val.add (rs PC) Vone) Vone). @@ -1155,14 +1231,12 @@ Proof. eapply code_tail_next_int; auto. change (Int.unsigned Int.zero) with 0. unfold transl_function. constructor. - assert (AG2: agree ms sp rs2). - split. reflexivity. - intros. unfold rs2. rewrite nextinstr_inv. - repeat (rewrite Pregmap.gso). elim AG; auto. - auto with ppcgen. auto with ppcgen. assert (AG3: agree ms sp rs3). - unfold rs3; auto with ppcgen. - left; exists (State rs3 m3); split. + unfold rs3. apply agree_nextinstr. + unfold rs2. apply agree_nextinstr. + apply agree_change_sp with (parent_sp s); auto. + unfold sp. congruence. + left; exists (State rs3 m3'); split. (* execution *) eapply exec_straight_steps_1; eauto. change (Int.unsigned Int.zero) with 0. constructor. @@ -1183,15 +1257,21 @@ Lemma exec_function_external_prop: Proof. intros; red; intros; inv MS. exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. - left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14)) - m'); split. + intros [tf [A B]]. simpl in B. inv B. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [P [Q [R S]]]]]. + left; exists (State (rs#(loc_external_result (ef_sig ef)) <- vres' #PC <- (rs IR14)) + m2'); split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. - eapply extcall_arguments_match; eauto. econstructor; eauto. - unfold loc_external_result. auto with ppcgen. + unfold loc_external_result. + eapply agree_set_mreg; eauto. + rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. auto. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. Qed. Lemma exec_return_prop: @@ -1241,6 +1321,8 @@ Proof. with (Vptr fb Int.zero). econstructor; eauto. constructor. split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. + intros. unfold Regmap.init. auto. + apply Mem.extends_refl. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. unfold ge; rewrite H1. auto. @@ -1251,8 +1333,8 @@ Lemma transf_final_states: match_states st1 st2 -> Machconcr.final_state st1 r -> Asm.final_state st2 r. Proof. intros. inv H0. inv H. constructor. auto. - compute in H1. - rewrite (ireg_val _ _ _ R0 AG) in H1. auto. auto. + compute in H1. exploit ireg_val; eauto. instantiate (1 := R0); auto. + simpl. intros LD. inv LD; congruence. Qed. Theorem transf_program_correct: -- cgit