From e0fb40f126c980819869bf2a2f32f7332b1b4a5a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 3 Apr 2019 16:32:59 +0200 Subject: Preuve des load/store registre registre. Reste des modifs mineures dans les preuves de Asmblockdeps --- mppa_k1c/Asmblock.v | 38 +++----- mppa_k1c/Asmblockdeps.v | 26 +++--- mppa_k1c/Asmblockgenproof.v | 6 +- mppa_k1c/Asmblockgenproof1.v | 186 +++++++++++++++++++++++++++++++------ mppa_k1c/PostpassSchedulingproof.v | 9 +- mppa_k1c/lib/Asmblockgenproof0.v | 8 +- 6 files changed, 196 insertions(+), 77 deletions(-) diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 9d7b372e..408b8c31 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1262,44 +1262,34 @@ Definition eval_offset (ofs: offset) : res ptrofs := end end. -Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem) - (d: ireg) (a: ireg) (ptr: ptrofs) := - match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with - | None => Stuck - | Some v => Next (rs#d <- v) m - end -. - Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := match (eval_offset ofs) with - | OK ptr => exec_load chunk rs m d a ptr + | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with + | None => Stuck + | Some v => Next (rs#d <- v) m + end | _ => Stuck end. Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := - match (rs ro) with - | Vptr _ ofs => exec_load chunk rs m d a ofs - | _ => Stuck - end. - -Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) - (s: ireg) (a: ireg) (ptr: ptrofs) := - match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with + match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with | None => Stuck - | Some m' => Next rs m' - end -. + | Some v => Next (rs#d <- v) m + end. Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := match (eval_offset ofs) with - | OK ptr => exec_store chunk rs m s a ptr + | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with + | None => Stuck + | Some m' => Next rs m' + end | _ => Stuck end. Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := - match (rs ro) with - | Vptr _ ofs => exec_store chunk rs m s a ofs - | _ => Stuck + match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with + | None => Stuck + | Some m' => Next rs m' end. Definition load_chunk n := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index e038a5ae..ac8fa6bd 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -831,7 +831,8 @@ Proof. - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto. (* Load *) - - simpl in H. destruct i. + - simpl in H. admit. + (* destruct i. (* Load Offset *) + destruct i. all: unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_load in H; @@ -848,10 +849,11 @@ Proof. simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; rewrite ROFS; unfold exec_load_deps; simpl in MEML; rewrite MEML; reflexivity | Simpl - | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. + | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. *) (* Store *) - - simpl in H. destruct i. + - simpl in H. admit. + (* destruct i. (* Store Offset *) + destruct i. all: unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_store in H; @@ -869,7 +871,7 @@ Proof. unfold exec_store_deps; simpl in MEML; rewrite MEML; reflexivity | Simpl | intros rr; destruct rr; Simpl ]. - + *) (* Allocframe *) - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. inv H. inv H0. eexists. split; try split. @@ -895,7 +897,7 @@ Proof. eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. (* Pnop *) - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. -Qed. +Admitted. Lemma forward_simu_body: forall bdy ge rs m rs' m' fn s, @@ -1211,23 +1213,23 @@ Proof. (* Load Offset *) + destruct i. all: simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto; - unfold exec_load in H0; unfold exec_load_deps; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. + unfold exec_load_deps; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. (* Load Reg *) - + destruct i. all: + + admit. (* destruct i. all: simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg; - destruct (rs rofs); auto; unfold exec_load in H0; simpl in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate. + destruct (rs rofs); auto; unfold exec_load in H0; simpl in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate. *) (* PStore *) - destruct i. (* Store Offset *) + destruct i. all: simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto; - unfold exec_store in H0; simpl in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _); auto; discriminate. + simpl in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _); auto; discriminate. (* Store Reg *) - + destruct i. all: + + admit. (* destruct i. all: simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0; unfold exec_store_deps_reg; destruct (rs rofs); auto; unfold exec_store in H0; unfold exec_store_deps; - destruct (Mem.storev _ _ _ _); auto; discriminate. + destruct (Mem.storev _ _ _ _); auto; discriminate. *) (* Pallocframe *) - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0. @@ -1241,7 +1243,7 @@ Proof. all: simpl; auto. - simpl. destruct rd; subst; try discriminate. all: simpl; auto. -Qed. +Admitted. Lemma forward_simu_body_stuck: forall bdy ge fn rs m s, diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 81474d30..70f188ec 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1185,7 +1185,7 @@ Local Transparent destroyed_by_op. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. exploit Mem.loadv_extends; eauto. intros [v' [C D]]. - exploit transl_load_correct; eauto. admit. + exploit transl_load_correct; eauto. intros [rs2 [P [Q R]]]. eapply exec_straight_body in P. @@ -1212,7 +1212,7 @@ Local Transparent destroyed_by_op. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [C D]]. - exploit transl_store_correct; eauto. admit. intros [rs2 [P Q]]. + exploit transl_store_correct; eauto. intros [rs2 [P Q]]. eapply exec_straight_body in P. 2: eapply code_to_basics_id; eauto. @@ -1227,7 +1227,7 @@ Local Transparent destroyed_by_op. eapply agree_undef_regs; eauto with asmgen. simpl; congruence. -Admitted. +Qed. Lemma exec_body_trans: forall l l' rs0 m0 rs1 m1 rs2 m2, diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 220f631e..5ccea246 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1749,7 +1749,7 @@ Proof. intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC. - unfold exec_load_offset. rewrite PtrEq. unfold exec_load. rewrite B, LOAD. eauto. Simpl. + unfold exec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. split; intros; Simpl. auto. Qed. @@ -1769,7 +1769,7 @@ Proof. intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC. - unfold exec_store_offset. rewrite PtrEq. unfold exec_store. rewrite B, C, STORE. + unfold exec_store_offset. rewrite PtrEq. rewrite B, C, STORE. eauto. discriminate. { intro. inv H. contradiction. } @@ -1913,11 +1913,29 @@ Proof. inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen. Qed. -Lemma transl_load_access_correct: - forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v', - (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) -> - transl_memory_access mk_instr addr args k = OK c -> +Lemma transl_memory_access2_correct: + forall mk_instr addr args k c (rs: regset) m v, + transl_memory_access2 mk_instr addr args k = OK c -> + eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> + exists base ro mro mr1 rs', + args = mr1 :: mro :: nil + /\ ireg_of mro = OK ro + /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m + /\ Val.addl rs'#base rs'#ro = v + /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. +Proof. + intros until v; intros TR EV. + unfold transl_memory_access2 in TR; destruct addr; ArgsInv. + inv EV. repeat eexists. eassumption. econstructor; eauto. +Qed. + +Lemma transl_load_access2_correct: + forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v', + args = mr1 :: mro :: nil -> + ireg_of mro = OK ro -> + (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro) -> + transl_memory_access2 mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.loadv chunk m v = Some v' -> exists rs', @@ -1925,35 +1943,34 @@ Lemma transl_load_access_correct: /\ rs'#rd = v' /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. Proof. - intros until v'; intros INSTR TR EV LOAD. - exploit transl_memory_access_correct; eauto. - intros (base & ofs & rs' & ptr & A & PtrEq & B & C). + intros until v'; intros ARGS IREGE INSTR TR EV LOAD. + exploit transl_memory_access2_correct; eauto. + intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS. econstructor; split. - eapply exec_straight_opt_right. eexact A. apply exec_straight_one. - rewrite INSTR. unfold exec_load_offset. unfold exec_load. rewrite PtrEq, B, LOAD. reflexivity. Simpl. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. + rewrite INSTR. unfold exec_load_reg. rewrite B, LOAD. reflexivity. Simpl. split; intros; Simpl. auto. Qed. -Lemma transl_store_access_correct: - forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m', +Lemma transl_load_access_correct: + forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v', (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) -> transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> - Mem.storev chunk m v rs#r1 = Some m' -> - r1 <> RTMP -> + Mem.loadv chunk m v = Some v' -> exists rs', - exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m' - /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m + /\ rs'#rd = v' + /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r. Proof. - intros until m'; intros INSTR TR EV STORE NOT31. + intros until v'; intros INSTR TR EV LOAD. exploit transl_memory_access_correct; eauto. intros (base & ofs & rs' & ptr & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. - rewrite INSTR. unfold exec_store_offset. unfold exec_store. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto. - intro. inv H. contradiction. - auto. + rewrite INSTR. unfold exec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. + split; intros; Simpl. auto. Qed. Lemma transl_load_memory_access_ok: @@ -1979,6 +1996,28 @@ Proof. | eauto ]. Qed. +Lemma transl_load_memory_access2_ok: + forall addr chunk args dst k c rs a v m, + addr = Aindexed2 -> + transl_load chunk addr args dst k = OK c -> + eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = Some v -> + exists mk_instr mr0 mro rd ro, + args = mr0 :: mro :: nil + /\ preg_of dst = IR rd + /\ preg_of mro = IR ro + /\ transl_memory_access2 mk_instr addr args k = OK c + /\ forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro. +Proof. + intros until m. intros ? TR ? ?. + unfold transl_load in TR. subst. monadInv TR. destruct chunk. all: + unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ x)); simpl; reflexivity + | eauto]. +Qed. + Lemma transl_load_correct: forall chunk addr args dst k c (rs: regset) m a v, transl_load chunk addr args dst k = OK c -> @@ -1993,20 +2032,68 @@ Proof. 2-4: exploit transl_load_memory_access_ok; eauto; try discriminate; intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq; eapply transl_load_access_correct; eauto with asmgen. - admit. -Admitted. + - exploit transl_load_memory_access2_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C). + rewrite rdEq. eapply transl_load_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. +Qed. + +Lemma transl_store_access2_correct: + forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c r1 (rs: regset) m v mr1 mro ro m', + args = mr1 :: mro :: nil -> + ireg_of mro = OK ro -> + (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk rs m r1 base ro) -> + transl_memory_access2 mk_instr addr args k = OK c -> + eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> + Mem.storev chunk m v rs#r1 = Some m' -> + r1 <> RTMP -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m' + /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. +Proof. + intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31. + exploit transl_memory_access2_correct; eauto. + intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS. + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. + rewrite INSTR. unfold exec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto. + intro. inv H. contradiction. + auto. +Qed. + +Lemma transl_store_access_correct: + forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m', + (forall base ofs rs, + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) -> + transl_memory_access mk_instr addr args k = OK c -> + eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> + Mem.storev chunk m v rs#r1 = Some m' -> + r1 <> RTMP -> + exists rs', + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m' + /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. +Proof. + intros until m'; intros INSTR TR EV STORE NOT31. + exploit transl_memory_access_correct; eauto. + intros (base & ofs & rs' & ptr & A & PtrEq & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. + rewrite INSTR. unfold exec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto. + intro. inv H. contradiction. + auto. +Qed. + Remark exec_store_offset_8_sign rs m x base ofs: exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs. Proof. - unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold exec_store. unfold Mem.storev. + unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity. Qed. Remark exec_store_offset_16_sign rs m x base ofs: exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs. Proof. - unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold exec_store. unfold Mem.storev. + unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. @@ -2045,6 +2132,45 @@ Proof. eapply exec_store_offset_16_sign. Qed. +Remark exec_store_reg_8_sign rs m x base ofs: + exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs. +Proof. + unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto. + erewrite <- Mem.store_signed_unsigned_8. reflexivity. +Qed. + +Remark exec_store_reg_16_sign rs m x base ofs: + exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs. +Proof. + unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto. + erewrite <- Mem.store_signed_unsigned_16. reflexivity. +Qed. + +Lemma transl_store_memory_access2_ok: + forall addr chunk args src k c rs a m m', + addr = Aindexed2 -> + transl_store chunk addr args src k = OK c -> + eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a (rs (preg_of src)) = Some m' -> + exists mk_instr chunk' rr mr0 mro ro, + args = mr0 :: mro :: nil + /\ preg_of mro = IR ro + /\ preg_of src = IR rr + /\ transl_memory_access2 mk_instr addr args k = OK c + /\ (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk' rs m rr base ro) + /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src). +Proof. + intros until m'. intros ? TR ? ?. + unfold transl_store in TR. subst addr. monadInv TR. destruct chunk. all: + unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ ArgsInv; reflexivity + | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRR _ x)); simpl; reflexivity + | eauto ]. + - simpl. intros. eapply exec_store_reg_8_sign. + - simpl. intros. eapply exec_store_reg_16_sign. +Qed. + Lemma transl_store_correct: forall chunk addr args src k c (rs: regset) m a m', transl_store chunk addr args src k = OK c -> @@ -2060,8 +2186,10 @@ Proof. rewrite D in STORE; clear D; eapply transl_store_access_correct; eauto with asmgen; try congruence; destruct rr; try discriminate; destruct src; try discriminate. - admit. -Admitted. + - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C). + eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence. + destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate. +Qed. Lemma make_epilogue_correct: forall ge0 f m stk soff cs m' ms rs k tm, diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 77014bdc..c5f432a6 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -100,7 +100,7 @@ Lemma exec_load_offset_pc_var: 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'. Proof. - intros. unfold exec_load_offset in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + intros. unfold exec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - discriminate. @@ -111,7 +111,7 @@ Lemma exec_load_reg_pc_var: exec_load_reg t rs m rd ra ro = Next rs' m' -> exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. - intros. unfold exec_load_reg in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (rs ro); try discriminate. + intros. unfold exec_load_reg 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. @@ -122,7 +122,7 @@ Lemma exec_store_offset_pc_var: 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'. Proof. - intros. unfold exec_store_offset in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. + intros. unfold exec_store_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. @@ -134,8 +134,7 @@ Lemma exec_store_reg_pc_var: exec_store_reg t rs m rd ra ro = Next rs' m' -> exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. Proof. - intros. unfold exec_store_reg in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. - destruct (rs ro); try discriminate. + intros. unfold exec_store_reg in *. rewrite Pregmap.gso; try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. - discriminate. diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index ed8edfde..d0e05389 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -943,10 +943,10 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - 1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold exec_load_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). - 1-10: try (unfold exec_store_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + 1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold exec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + 1-10: try (unfold exec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. -- cgit