From 5397e5e8be051cf10934d59505666d335c018d90 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 5 Nov 2018 14:25:21 +0100 Subject: Got the schema working again with the headers --- mppa_k1c/Asmblockgenproof.v | 87 +++++++++++++++++++++++++++++---------------- 1 file changed, 57 insertions(+), 30 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 33d1de66..8e9bc1fa 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -829,16 +829,16 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := |} . -Inductive match_asmblock fb: codestate -> Asmblock.state -> Prop := - | match_asmblock_some: +Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop := + | match_asmstate_some: forall rs f tf tc m tbb ofs ep tbdy tex lhd (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (TRANSF: transf_function f = OK tf) (PCeq: rs PC = Vptr fb ofs) (TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc)) - (HDROK: header tbb = lhd) +(* (HDROK: header tbb = lhd) *) , - match_asmblock fb + match_asmstate fb {| pstate := (Asmblock.State rs m); pheader := lhd; pbody1 := tbdy; @@ -1011,7 +1011,7 @@ Theorem match_state_codestate: mbs = (Machblock.State s fb sp (bb::c) ms m) -> match_states mbs abs -> exists cs fb f tbb tc ep, - match_codestate fb mbs cs /\ match_asmblock fb cs abs + match_codestate fb mbs cs /\ match_asmstate fb cs abs /\ Genv.find_funct_ptr ge fb = Some (Internal f) /\ transl_blocks f (bb::c) ep = OK (tbb::tc) /\ body tbb = pbody1 cs ++ pbody2 cs @@ -1097,7 +1097,7 @@ Theorem step_simu_control: pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex -> cur cs2 = Some tbb -> match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 -> - match_asmblock fb cs2 (Asmblock.State rs1 m1) -> + match_asmstate fb cs2 (Asmblock.State rs1 m1) -> exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') E0 S'' -> (exists rs3 m3 rs4 m4, exec_body tge tbdy2 rs2 m2 = Next rs3 m3 @@ -1407,22 +1407,45 @@ Qed. Definition mb_remove_header bb := {| MB.header := nil; MB.body := MB.body bb; MB.exit := MB.exit bb |}. +Program Definition remove_header tbb := {| header := nil; body := body tbb; exit := exit tbb |}. +Next Obligation. + destruct tbb. simpl. auto. +Qed. + +Inductive exec_header: codestate -> codestate -> Prop := + | exec_header_cons: forall cs1, + exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1; + pctl := pctl cs1; fpok := (if pheader cs1 then fpok cs1 else false); rem := rem cs1; + (* cur := match cur cs1 with None => None | Some bcur => Some (remove_header bcur) end *) + cur := cur cs1 |}. + Lemma step_simu_header: forall bb s fb sp c ms m rs1 m1 cs1, - (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> +(* (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> *) pstate cs1 = (State rs1 m1) -> match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> (exists cs1', - cs1' = {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1; - pctl := pctl cs1; fpok := (if MB.header bb then fpok cs1 else false); rem := rem cs1; cur := cur cs1 |} + exec_header cs1 cs1' /\ match_codestate fb (MB.State s fb sp (mb_remove_header bb::c) ms m) cs1'). Proof. - intros. + intros until cs1. intros Hpstate MCS. eexists. split; eauto. - inv H1. simpl in *. inv H0. + econstructor; eauto. + inv MCS. simpl in *. inv Hpstate. econstructor; eauto. Qed. +Lemma step_matchasm_header: + forall fb cs1 cs1' s1, + match_asmstate fb cs1 s1 -> + exec_header cs1 cs1' -> + match_asmstate fb cs1' s1. +Proof. + intros until s1. intros MAS EXH. + inv MAS. inv EXH. + simpl. econstructor; eauto. +Qed. + Lemma step_simu_body: forall bb s fb sp c ms m rs1 m1 ms' cs1 m', MB.header bb = nil -> @@ -1454,7 +1477,6 @@ Proof. rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto. Qed. - (* Lemma exec_body_straight: forall l rs0 m0 rs1 m1, l <> nil -> @@ -1518,15 +1540,16 @@ Qed. (* Alternative form of step_simulation_bblock, easier to prove *) Lemma step_simulation_bblock': - forall sf f sp bb bb' rs m rs' m' s'' c S1, - body_step ge sf f sp (Machblock.body bb) rs m rs' m' -> - bb' = mb_remove_body bb -> - (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) -> - exit_step return_address_offset ge (Machblock.exit bb') (Machblock.State sf f sp (bb' :: c) rs' m') E0 s'' -> + forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1, + bb' = mb_remove_header bb -> + body_step ge sf f sp (Machblock.body bb') rs m rs' m' -> + bb'' = mb_remove_body bb' -> + (forall ef args res, MB.exit bb'' <> Some (MBbuiltin ef args res)) -> + exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') E0 s'' -> match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> exists S2 : state, plus step tge S1 E0 S2 /\ match_states s'' S2. Proof. - intros until S1. intros BSTEP Hbb' Hbuiltin ESTEP MS. + intros until S1. intros Hbb' BSTEP Hbb'' Hbuiltin ESTEP MS. destruct (mbsize bb) eqn:SIZE. - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit). destruct bb as [hd bdy ex]; simpl in *; subst. @@ -1559,17 +1582,18 @@ Proof. destruct H as (rs1 & m1 & Hpstate2). subst. assert (f = fb). { inv MCS. auto. } subst fb. exploit step_simu_header. - 3: eapply MCS. + 2: eapply MCS. all: eauto. - intros (cs1' & Heqcs1' & MCS2). + intros (cs1' & EXEH & MCS2). (* step_simu_body part *) - assert (MB.body bb = MB.body (mb_remove_header bb)). { destruct bb; simpl; auto. } - rewrite H in BSTEP. clear H. +(* assert (MB.body bb = MB.body (mb_remove_header bb)). { destruct bb; simpl; auto. } + rewrite H in BSTEP. clear H. *) + assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. } exploit step_simu_body. 3: eapply BSTEP. - all: eauto. - { (* TODO *) } + 4: eapply MCS2. + all: eauto. rewrite Hpstate'. eauto. intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS'). (* step_simu_control part *) @@ -1579,12 +1603,14 @@ Proof. assert (exists tex, pbody2 cs1 = extract_basic tex /\ pctl cs1 = extract_ctl tex). { inv MAS. simpl in *. eauto. } destruct H as (tex & Hpbody2 & Hpctl). + inv EXEH. simpl in *. subst. exploit step_simu_control. - 9: eapply MCS'. + 9: eapply MCS'. all: simpl. + 10: eapply ESTEP. all: simpl; eauto. rewrite Hpbody2. rewrite Hpctl. rewrite Hcur. - { inv MAS; simpl in *. inv Hcur. inv Hpstate2. eapply match_asmblock_some; eauto. - erewrite exec_body_pc; eauto. destruct TODO. (* TODO *) } + { inv MAS; simpl in *. inv Hcur. inv Hpstate2. eapply match_asmstate_some; eauto. + erewrite exec_body_pc; eauto. } intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS'). (* bringing the pieces together *) @@ -1598,14 +1624,14 @@ Proof. intros EXECB. inv EXECB. exists (State rs4 m4). split; auto. eapply plus_one. rewrite Hpstate2. - assert (exists ofs, rs1 PC = Vptr fb ofs). + assert (exists ofs, rs1 PC = Vptr f ofs). { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. } destruct H0 as (ofs & Hrs1pc). eapply exec_step_internal; eauto. (* proving the initial find_bblock *) rewrite Hpstate2 in MAS. inv MAS. simpl in *. - assert (f = f0) by congruence. subst f0. + assert (f1 = f0) by congruence. subst f0. rewrite PCeq in Hrs1pc. inv Hrs1pc. exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''. inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. inv Hcur. @@ -1621,7 +1647,8 @@ Lemma step_simulation_bblock: exists S2' : state, plus step tge S1' E0 S2' /\ match_states S2 S2'. Proof. intros until c. intros BSTEP Hbuiltin ESTEP S1' MS. - eapply step_simulation_bblock'; eauto. destruct bb as [hd bdy ex]; simpl in *. + eapply step_simulation_bblock'; eauto. + all: destruct bb as [hd bdy ex]; simpl in *; eauto. inv ESTEP. - econstructor. inv H; try (econstructor; eauto; fail). - econstructor. -- cgit