diff options
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 76 |
1 files changed, 47 insertions, 29 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index bc90dd4c..da64c41d 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -96,11 +96,11 @@ Proof. Qed. Lemma exec_load_offset_pc_var: - forall ge t rs m rd ra ofs rs' m' v, - exec_load_offset ge t rs m rd ra ofs = Next rs' m' -> - exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall t rs m rd ra ofs rs' m' v, + exec_load_offset t rs m rd ra ofs = Next rs' m' -> + exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - discriminate. @@ -117,18 +117,42 @@ Proof. - discriminate. Qed. +Lemma exec_load_regxs_pc_var: + forall t rs m rd ra ro rs' m' v, + exec_load_regxs t rs m rd ra ro = Next rs' m' -> + exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. + destruct (Mem.loadv _ _ _). + - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. + - discriminate. +Qed. + Lemma exec_store_offset_pc_var: - forall ge t rs m rd ra ofs rs' m' v, - exec_store_offset ge t rs m rd ra ofs = Next rs' m' -> - exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall t rs m rd ra ofs rs' m' v, + exec_store_offset t rs m rd ra ofs = Next rs' m' -> + exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate. - destruct (eval_offset ge ofs); try discriminate. + destruct (eval_offset ofs); try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. - discriminate. Qed. +Lemma exec_store_q_offset_pc_var: + forall rs m rd ra ofs rs' m' v, + exec_store_q_offset rs m rd ra ofs = Next rs' m' -> + exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. + simpl in *. + destruct (gpreg_q_expand _) as [s0 s1]. + destruct (Mem.storev _ _ _); try discriminate. + destruct (Mem.storev _ _ _); try discriminate. + inv H. apply next_eq; auto. +Qed. + Lemma exec_store_reg_pc_var: forall t rs m rd ra ro rs' m' v, exec_store_reg t rs m rd ra ro = Next rs' m' -> @@ -140,6 +164,17 @@ Proof. - discriminate. Qed. +Lemma exec_store_regxs_pc_var: + forall t rs m rd ra ro rs' m' v, + exec_store_regxs t rs m rd ra ro = Next rs' m' -> + exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate. + destruct (Mem.storev _ _ _). + - inv H. apply next_eq; auto. + - discriminate. +Qed. + Lemma exec_basic_instr_pc_var: forall ge i rs m rs' m' v, exec_basic_instr ge i rs m = Next rs' m' -> @@ -155,9 +190,12 @@ Proof. - destruct i. + exploreInst; apply exec_load_offset_pc_var; auto. + exploreInst; apply exec_load_reg_pc_var; auto. + + exploreInst; apply exec_load_regxs_pc_var; auto. - destruct i. + exploreInst; apply exec_store_offset_pc_var; auto. + exploreInst; apply exec_store_reg_pc_var; auto. + + exploreInst; apply exec_store_regxs_pc_var; auto. + + apply exec_store_q_offset_pc_var; auto. - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). destruct (Mem.storev _ _ _ _); try discriminate. inv H. apply next_eq; auto. apply functional_extensionality. intros. @@ -576,32 +614,12 @@ Proof. unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto. Qed. -Lemma eval_offset_preserved: - forall ofs, eval_offset ge ofs = eval_offset tge ofs. -Proof. - intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto. -Qed. - -Lemma transf_exec_load_offset: - forall t rs m rd ra ofs, exec_load_offset ge t rs m rd ra ofs = exec_load_offset tge t rs m rd ra ofs. -Proof. - intros. unfold exec_load_offset. unfold parexec_load_offset. rewrite eval_offset_preserved. reflexivity. -Qed. - -Lemma transf_exec_store_offset: - forall t rs m rs0 ra ofs, exec_store_offset ge t rs m rs0 ra ofs = exec_store_offset tge t rs m rs0 ra ofs. -Proof. - intros. unfold exec_store_offset. unfold parexec_store_offset. rewrite eval_offset_preserved. reflexivity. -Qed. - Lemma transf_exec_basic_instr: forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. Proof. intros. pose symbol_address_preserved. unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence. - - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. - - apply transf_exec_load_offset. - - apply transf_exec_store_offset. + unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. Qed. Lemma transf_exec_body: |