diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-18 17:09:17 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-18 17:09:17 +0200 |
commit | d6ac402cfec2443ecb1a73a92838701236889afe (patch) | |
tree | a1364917ae05903e1b8013142114912b0dded0e8 | |
parent | 7048a1fe04f45695aa6f7c4a35a6f9dcb5456c2b (diff) | |
download | compcert-kvx-d6ac402cfec2443ecb1a73a92838701236889afe.tar.gz compcert-kvx-d6ac402cfec2443ecb1a73a92838701236889afe.zip |
Avancement dans le cas MBgetstack du step_simu_basic
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 64 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 11 |
2 files changed, 64 insertions, 11 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 2a412e98..ec5f2f3e 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1390,9 +1390,23 @@ Qed. Definition mb_remove_first (bb: MB.bblock) :=
{| MB.header := MB.header bb; MB.body := tail (MB.body bb); MB.exit := MB.exit bb |}.
+Lemma exec_straight_body:
+ forall c c' rs1 m1 rs2 m2,
+ exec_straight tge c rs1 m1 c' rs2 m2 ->
+ exists l,
+ c = l ++ c'
+ /\ exec_body tge l rs1 m1 = Next rs2 m2.
+Proof.
+ induction c; try (intros; inv H; fail).
+ intros. inv H.
+ - exists (a ::i nil). split; auto. simpl. rewrite H7. auto.
+ - apply IHc in H8. destruct H8 as (l & Hc & EXECB). subst.
+ exists (a ::i l). split; auto. simpl. rewrite H2. auto.
+Qed.
+
Lemma step_simu_basic:
forall bb bb' s fb sp tbb c ms m rs1 m1 tc ms' m' bi bdy,
- MB.body bb = bi::(bdy) ->
+ MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
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' ->
match_codestate fb (MB.State s fb sp (bb::c) ms m) (Codestate (State rs1 m1) (tbb::tc) (Some tbb)) ->
@@ -1403,7 +1417,41 @@ Lemma step_simu_basic: (Codestate (State rs2 m2) (tbb'::tc) (Some tbb'))
/\ exit tbb' = exit tbb).
Proof.
-Admitted.
+(* intros until bdy. intros Hbody Hnobuiltin Hbb' BSE MCS. inv MCS.
+ exploit transl_blocks_distrib; eauto. intros (TLB & TLBS).
+ exploit transl_block_nobuiltin; eauto. left; rewrite Hbody; discriminate.
+ intros (lbi & le & TBC & TIC & Htbody & Htexit).
+ rewrite Hbody in TBC. monadInv TBC.
+ inv BSE.
+ - (* MBgetstack *)
+ simpl in EQ0.
+
+ 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. }
+ intros (rs2 & EXECS & Hrs'1 & Hrs'2).
+ eapply exec_straight_body in EXECS. destruct EXECS as (l & Hlbi & EXECB).
+ exists rs2 m1 (* something *) l.
+(* TODO *)
+
+
+ left; eapply exec_straight_steps; eauto. intros. simpl in TR.
+ exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
+ exists rs'; split. eauto.
+ split. eapply agree_set_mreg; eauto with asmgen. congruence.
+ simpl; congruence.
+ - (* MBsetstack *)
+ destruct TODO.
+ - (* MBgetparam *)
+ destruct TODO.
+ - (* MBop *)
+ destruct TODO.
+ - (* MBload *)
+ destruct TODO.
+ - (* MBstore *)
+ destruct TODO.
+ *)Admitted.
Lemma exec_body_trans:
forall l l' rs0 m0 rs1 m1 rs2 m2,
@@ -1420,6 +1468,7 @@ Qed. Lemma step_simu_body':
forall bb s fb sp tbb c ms m rs1 m1 tc ms' m',
+ (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
body_step ge s fb sp (MB.body bb) ms m ms' m' ->
match_codestate fb (MB.State s fb sp (bb::c) ms m) (Codestate (State rs1 m1) (tbb::tc) (Some tbb)) ->
(exists rs2 m2 tbb' l,
@@ -1430,15 +1479,15 @@ Lemma step_simu_body': /\ exit tbb' = exit tbb ).
Proof.
intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy].
- - intros until m'. intros BSTEP MCS. inv BSTEP.
+ - intros until m'. intros Hnobuiltin BSTEP MCS. inv BSTEP.
exists rs1, m1, tbb, nil.
repeat (split; simpl; auto).
- - intros until m'. intros BSTEP MCS. inv BSTEP.
+ - intros until m'. intros Hnobuiltin BSTEP MCS. inv BSTEP.
rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'.
- exploit (step_simu_basic); eauto. simpl. eauto.
+ exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto.
intros (rs2 & m2 & tbb' & l & Hbody & EBODY & MCS' & Hexit).
simpl in *.
- exploit IHbdy. eapply H6. eauto.
+ exploit IHbdy; simpl; auto. eapply H6. eauto.
intros (rs3 & m3 & tbb'' & l' & Hbody' & EBODY' & MCS'' & Hexit').
exists rs3, m3, tbb'', (l++l').
repeat (split; simpl; auto).
@@ -1449,6 +1498,7 @@ Qed. Theorem step_simu_body:
forall bb s fb sp tbb c ms m rs1 m1 tc ms' m',
+ (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) ->
body_step ge s fb sp (MB.body bb) ms m ms' m' ->
match_codestate fb (MB.State s fb sp (bb::c) ms m) (Codestate (State rs1 m1) (tbb::tc) (Some tbb)) ->
(exists rs2 m2 tbb' l,
@@ -1532,6 +1582,8 @@ Proof. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. rename tc' into tc.
exploit match_state_codestate; eauto.
intros (S1' & MCS & MAS & cseq). subst.
+ assert (Hnobuiltin': forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)).
+ intros. destruct bb as [hd bdy ex]. simpl in *. apply Hbuiltin.
exploit step_simu_body; eauto. intros (rs2 & m2 & tbb' & l & Hbody & EXES & MCS' & Hexit).
remember (mb_remove_body bb) as bb'.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 81123c9b..08be374a 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1324,18 +1324,18 @@ Proof. Qed. -(* + Lemma loadind_correct: forall (base: ireg) ofs ty dst k c (rs: regset) m v, loadind base ofs ty dst k = OK c -> Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> exists rs', - exec_straight ge fn c rs m k rs' m + 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. - intros until v; intros TR LOAD NOT31. +Proof. Admitted. +(* intros until v; intros TR LOAD NOT31. assert (A: exists mk_instr, c = indexed_memory_access mk_instr base ofs k /\ forall base' ofs' rs', @@ -1345,8 +1345,9 @@ Proof. 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 -> |