diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 43 |
1 files changed, 17 insertions, 26 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 08be374a..4abf1d52 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1277,16 +1277,16 @@ Proof. *)*) Qed. -(* + Lemma indexed_load_access_correct: - forall chunk (mk_instr: ireg -> offset -> instruction) rd m, + forall chunk (mk_instr: ireg -> offset -> basic) rd m, (forall base ofs rs, - exec_instr ge fn (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) -> forall (base: ireg) ofs k (rs: regset) v, Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> rd <> PC -> exists rs', - exec_straight ge fn (indexed_memory_access mk_instr base ofs k) rs m k rs' m + exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m /\ rs'#rd = v /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r. Proof. @@ -1296,11 +1296,8 @@ Proof. econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC. unfold exec_load. rewrite B, LOAD. eauto. Simpl. - split; intros; Simpl. + split; intros; Simpl. auto. Qed. -*) - -Definition noscroll := 0. Lemma indexed_store_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) r1 m, @@ -1308,7 +1305,7 @@ Lemma indexed_store_access_correct: exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) -> forall (base: ireg) ofs k (rs: regset) m', Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' -> - base <> GPR31 -> r1 <> GPR31 -> IR r1 <> PC -> + base <> GPR31 -> r1 <> GPR31 -> r1 <> PC -> exists rs', exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m' /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. @@ -1318,13 +1315,10 @@ Proof. intros (base' & ofs' & rs' & A & B & C). econstructor; split. eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC. - unfold exec_store. rewrite B, C, STORE. eauto. eauto. - destruct r1; try discriminate. contradiction NOT31'. auto. auto. -(* intros; Simpl. *) + unfold exec_store. rewrite B, C, STORE. eauto. eauto. auto. + intros; Simpl. rewrite C; auto. Qed. - - Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> @@ -1334,42 +1328,39 @@ Lemma loadind_correct: exec_straight ge c rs m k rs' m /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r. -Proof. Admitted. -(* intros until v; intros TR LOAD NOT31. +Proof. + intros until v; intros TR LOAD NOT31. assert (A: exists mk_instr, - c = indexed_memory_access mk_instr base ofs k + c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', - exec_instr ge fn (mk_instr base' ofs') rs' m = + exec_basic_instr ge (mk_instr base' ofs') rs' m = exec_load ge (chunk_of_type ty) rs' m (preg_of dst) base' ofs'). { unfold loadind in TR. destruct ty, (preg_of dst); inv TR; econstructor; split; eauto. } destruct A as (mk_instr & B & C). subst c. eapply indexed_load_access_correct; eauto with asmgen. -Qed. *) +Qed. -(* Lemma storeind_correct: forall (base: ireg) ofs ty src k c (rs: regset) m m', storeind src base ofs ty k = OK c -> Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' -> base <> GPR31 -> exists rs', - exec_straight ge fn c rs m k rs' m' + exec_straight ge c rs m k rs' m' /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. - intros until m'; intros TR STORE NOT31. + intros until m'; intros TR STORE NOT31. assert (A: exists mk_instr, - c = indexed_memory_access mk_instr base ofs k + c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', - exec_instr ge fn (mk_instr base' ofs') rs' m = + exec_basic_instr ge (mk_instr base' ofs') rs' m = exec_store ge (chunk_of_type ty) rs' m (preg_of src) base' ofs'). { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; split; eauto. } destruct A as (mk_instr & B & C). subst c. eapply indexed_store_access_correct; eauto with asmgen. Qed. -*) - Ltac bsimpl := unfold exec_bblock; simpl. Lemma Pget_correct: |