diff options
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 3f3cb19c..43c8acb8 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -151,6 +151,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' -> @@ -170,6 +181,7 @@ Proof. - 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. - 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. |