diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /ia32/Asmgenproof.v | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) | |
download | compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.tar.gz compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.zip |
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc)
based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgenproof.v')
-rw-r--r-- | ia32/Asmgenproof.v | 131 |
1 files changed, 50 insertions, 81 deletions
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index e43392aa..ca0fd182 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -138,49 +138,8 @@ Proof. Qed. Hint Resolve mk_mov_label: labels. -Remark mk_shift_label: - forall f r1 r2 k c, mk_shift f r1 r2 k = OK c -> - (forall r, nolabel (f r)) -> - tail_nolabel k c. -Proof. - unfold mk_shift; intros. TailNoLabel. -Qed. -Hint Resolve mk_shift_label: labels. - -Remark mk_mov2_label: - forall r1 r2 r3 r4 k, - tail_nolabel k (mk_mov2 r1 r2 r3 r4 k). -Proof. - intros; unfold mk_mov2. - destruct (ireg_eq r1 r2); TailNoLabel. - destruct (ireg_eq r3 r4); TailNoLabel. - destruct (ireg_eq r3 r2); TailNoLabel. - destruct (ireg_eq r1 r4); TailNoLabel. -Qed. -Hint Resolve mk_mov2_label: labels. - -Remark mk_div_label: - forall f r1 r2 k c, mk_div f r1 r2 k = OK c -> - (forall r, nolabel (f r)) -> - tail_nolabel k c. -Proof. - unfold mk_div; intros. TailNoLabel. - eapply tail_nolabel_trans; TailNoLabel. -Qed. -Hint Resolve mk_div_label: labels. - -Remark mk_mod_label: - forall f r1 r2 k c, mk_mod f r1 r2 k = OK c -> - (forall r, nolabel (f r)) -> - tail_nolabel k c. -Proof. - unfold mk_mod; intros. TailNoLabel. - eapply tail_nolabel_trans; TailNoLabel. -Qed. -Hint Resolve mk_mod_label: labels. - Remark mk_shrximm_label: - forall r n k c, mk_shrximm r n k = OK c -> tail_nolabel k c. + forall n k c, mk_shrximm n k = OK c -> tail_nolabel k c. Proof. intros. monadInv H; TailNoLabel. Qed. @@ -212,6 +171,7 @@ Proof. unfold loadind; intros. destruct ty. TailNoLabel. destruct (preg_of dst); TailNoLabel. + discriminate. Qed. Remark storeind_label: @@ -222,13 +182,23 @@ Proof. unfold storeind; intros. destruct ty. TailNoLabel. destruct (preg_of src); TailNoLabel. + discriminate. +Qed. + +Remark mk_setcc_base_label: + forall xc rd k, + tail_nolabel k (mk_setcc_base xc rd k). +Proof. + intros. destruct xc; simpl; destruct (ireg_eq rd EAX); TailNoLabel. Qed. Remark mk_setcc_label: forall xc rd k, tail_nolabel k (mk_setcc xc rd k). Proof. - intros. destruct xc; simpl; destruct (ireg_eq rd EDX); TailNoLabel. + intros. unfold mk_setcc. destruct (low_ireg rd). + apply mk_setcc_base_label. + eapply tail_nolabel_trans. apply mk_setcc_base_label. TailNoLabel. Qed. Remark mk_jcc_label: @@ -534,7 +504,7 @@ Proof. rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. exploit storeind_correct; eauto. intros [rs' [P Q]]. exists rs'; split. eauto. - split. unfold undef_setstack. eapply agree_undef_move; eauto. + split. eapply agree_undef_regs; eauto. simpl; intros. rewrite Q; auto with asmgen. - (* Mgetparam *) @@ -547,9 +517,9 @@ Proof. intros [v' [C D]]. Opaque loadind. left; eapply exec_straight_steps; eauto; intros. - assert (DIFF: negb (mreg_eq dst IT1) = true -> IR EDX <> preg_of dst). - intros. change (IR EDX) with (preg_of IT1). red; intros. - unfold proj_sumbool in H1. destruct (mreg_eq dst IT1); try discriminate. + assert (DIFF: negb (mreg_eq dst DX) = true -> IR EDX <> preg_of dst). + 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 *) @@ -577,10 +547,7 @@ Opaque loadind. 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. - unfold undef_op. - destruct op; try (eapply agree_set_undef_mreg; eauto). - eapply agree_set_undef_move_mreg; eauto. + split. eapply agree_set_undef_mreg; eauto. simpl; congruence. - (* Mload *) @@ -606,7 +573,7 @@ Opaque loadind. intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. - split. eapply agree_exten_temps; eauto. + split. eapply agree_undef_regs; eauto. simpl; congruence. - (* Mcall *) @@ -700,22 +667,26 @@ Opaque loadind. inv AT. monadInv H3. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H2); intro NOOV. - exploit external_call_mem_extends; eauto. eapply preg_vals; eauto. + exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. + eauto. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss. - simpl undef_regs. repeat rewrite Pregmap.gso; auto with asmgen. + rewrite undef_regs_other. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. - apply agree_nextinstr_nf. eapply agree_set_undef_mreg; eauto. - rewrite Pregmap.gss. auto. - intros. Simplifs. + rewrite preg_notin_charact. intros. auto with asmgen. + rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. + simpl; intros. intuition congruence. + apply agree_nextinstr_nf. eapply agree_set_mregs; auto. + eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. - (* Mannot *) @@ -723,12 +694,12 @@ Opaque loadind. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends'; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. @@ -762,7 +733,7 @@ Opaque loadind. (* simple jcc *) exists (Pjcc c1 lbl); exists k; exists rs'. split. eexact A. - split. eapply agree_exten_temps; eauto. + split. eapply agree_exten; eauto. simpl. rewrite B. auto. (* jcc; jcc *) destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; @@ -771,13 +742,13 @@ Opaque loadind. (* first jcc jumps *) exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'. split. eexact A. - split. eapply agree_exten_temps; 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. eapply exec_straight_one. simpl. rewrite TC1. auto. auto. - split. eapply agree_exten_temps; eauto. + split. eapply agree_exten; eauto. intros; Simplifs. simpl. rewrite eval_testcond_nextinstr. rewrite TC2. destruct b2; auto || discriminate. @@ -787,7 +758,7 @@ Opaque loadind. destruct (andb_prop _ _ H3). subst. exists (Pjcc2 c1 c2 lbl); exists k; exists rs'. split. eexact A. - split. eapply agree_exten_temps; eauto. + split. eapply agree_exten; eauto. simpl. rewrite TC1; rewrite TC2; auto. - (* Mcond false *) @@ -801,7 +772,7 @@ Opaque loadind. 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. + split. apply agree_nextinstr. eapply agree_exten; eauto. simpl; congruence. (* jcc ; jcc *) destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; @@ -811,7 +782,7 @@ Opaque loadind. 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_temps; eauto. + split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten; eauto. simpl; congruence. (* jcc2 *) destruct (eval_testcond c1 rs') as [b1|] eqn:TC1; @@ -822,7 +793,7 @@ Opaque loadind. rewrite TC1; rewrite TC2. destruct b1. simpl in *. subst b2. auto. auto. auto. - split. apply agree_nextinstr. eapply agree_exten_temps; eauto. + split. apply agree_nextinstr. eapply agree_exten; eauto. rewrite H1; congruence. - (* Mjumptable *) @@ -830,8 +801,7 @@ Opaque loadind. 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#ECX <- Vundef #EDX <- Vundef). - repeat (rewrite Pregmap.gso by auto with asmgen). eauto. 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. @@ -839,7 +809,8 @@ Opaque loadind. eapply find_instr_tail; eauto. simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto. econstructor; eauto. - eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simplifs. +Transparent destroyed_by_jumptable. + simpl. eapply agree_exten; eauto. intros. rewrite C; auto with asmgen. congruence. - (* Mreturn *) @@ -890,8 +861,9 @@ Opaque loadind. subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega. constructor. apply agree_nextinstr. eapply agree_change_sp; eauto. - apply agree_exten_temps with rs0; eauto. - intros; Simplifs. +Transparent destroyed_at_function_entry. + apply agree_undef_regs with rs0; eauto. + simpl; intros. apply Pregmap.gso; auto with asmgen. tauto. congruence. intros. Simplifs. eapply agree_sp; eauto. @@ -900,17 +872,15 @@ Opaque loadind. intros [tf [A B]]. simpl in B. inv B. exploit extcall_arguments_match; eauto. intros [args' [C D]]. - exploit external_call_mem_extends; eauto. + 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. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. unfold loc_external_result. - eapply agree_set_mreg; eauto. - rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. - intros; Simplifs. + apply agree_set_other; auto. apply agree_set_mregs; auto. - (* return *) inv STACKS. simpl in *. @@ -942,10 +912,9 @@ Lemma transf_final_states: 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. - generalize (preg_val _ _ _ AX AG). rewrite H1. intros LD; inv LD. auto. + 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. Theorem transf_program_correct: |