From ba4b3ba3ebf01c202cdd847796eccd00f20f63b0 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 24 Oct 2018 17:06:23 +0200 Subject: MBsetstack done! --- mppa_k1c/Asmblock.v | 4 ++-- mppa_k1c/Asmblockgenproof.v | 24 +++++++++++++++++++----- mppa_k1c/Asmblockgenproof1.v | 43 +++++++++++++++++-------------------------- 3 files changed, 38 insertions(+), 33 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index fb0f8c37..cf6fef3b 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -816,14 +816,14 @@ Definition eval_offset (ofs: offset) : ptrofs := end. Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem) - (d: ireg) (a: ireg) (ofs: offset) := + (d: preg) (a: ireg) (ofs: offset) := match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with | None => Stuck | Some v => Next (rs#d <- v) m end. Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) - (s: ireg) (a: ireg) (ofs: offset) := + (s: preg) (a: ireg) (ofs: offset) := match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with | None => Stuck | Some m' => Next rs m' diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 6b83d110..ba6ecb66 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1445,11 +1445,9 @@ Admitted. Lemma step_simu_basic: forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy, MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> -(* (bdy <> nil \/ MB.exit bb <> None) -> *) bb' = {| MB.header := MB.header bb; MB.body := bdy; MB.exit := MB.exit bb |} -> basic_step ge s fb sp ms m bi ms' m' -> pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy -> -(* pstate cs2 = (State rs2 m2) -> pbody1 cs2 = tbdy' -> *) match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> (exists rs2 m2 l cs2 tbdy', cs2 = {| pstate := (State rs2 m2); pheader := pheader cs1; pbody1 := tbdy'; pbody2 := pbody2 cs1; @@ -1467,7 +1465,7 @@ Proof. unfold Mach.load_stack in H. exploit Mem.loadv_extends; eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. - exploit loadind_correct; eauto with asmgen. { destruct TODO. } + exploit loadind_correct; eauto with asmgen. intros (rs2 & EXECS & Hrs'1 & Hrs'2). eapply exec_straight_body in EXECS. destruct EXECS as (l & Hlbi & EXECB). exists rs2, m1, l. @@ -1479,7 +1477,23 @@ Proof. eapply agree_set_mreg; eauto with asmgen. intro Hep. simpl in Hep. inv Hep. - (* MBsetstack *) - destruct TODO. + simpl in EQ0. + unfold Mach.store_stack in H. + assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. } + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + exploit storeind_correct; eauto with asmgen. + rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]]. + + eapply exec_straight_body in P. destruct P as (l & Hlbi & EXECB). + exists rs', m2', l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + rewrite <- Hheadereq. subst. + eapply match_codestate_intro; eauto. + + eapply agree_undef_regs; eauto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. - (* MBgetparam *) destruct TODO. - (* MBop *) @@ -1733,7 +1747,7 @@ Proof. left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0. all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto). - + destruct TODO. (* MBbuiltin *) + + (* MBbuiltin *) destruct TODO. + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto. - (* internal function *) 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: -- cgit