diff options
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index da64c41d..0ceff6e5 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -128,6 +128,24 @@ Proof. - discriminate. Qed. +Lemma exec_load_offset_q_pc_var: + forall rs m rd ra ofs rs' m' v, + exec_load_q_offset rs m rd ra ofs = Next rs' m' -> + exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *. + destruct (gpreg_q_expand rd) as [rd0 rd1]. + destruct (ireg_eq rd0 ra); try discriminate. + rewrite Pregmap.gso; try discriminate. + destruct (Mem.loadv _ _ _); try discriminate. + inv H. + destruct (Mem.loadv _ _ _); try discriminate. + inv H1. f_equal. + rewrite (regset_double_set PC rd0) by discriminate. + rewrite (regset_double_set PC rd1) by discriminate. + reflexivity. +Qed. + Lemma exec_store_offset_pc_var: forall t rs m rd ra ofs rs' m' v, exec_store_offset t rs m rd ra ofs = Next rs' m' -> @@ -191,6 +209,7 @@ Proof. + exploreInst; apply exec_load_offset_pc_var; auto. + exploreInst; apply exec_load_reg_pc_var; auto. + exploreInst; apply exec_load_regxs_pc_var; auto. + + apply exec_load_offset_q_pc_var; auto. - destruct i. + exploreInst; apply exec_store_offset_pc_var; auto. + exploreInst; apply exec_store_reg_pc_var; auto. |