From c4924047e03f3c7024c17a6f367897f695c4cd63 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 26 Oct 2018 17:51:45 +0200 Subject: Changing exec_straight to allow all instructions (prepare for MBtailcall proof) --- mppa_k1c/Asmblock.v | 35 +++++++++++++++ mppa_k1c/Asmblockgenproof.v | 105 ++++++++++++++++++++++++++++++++----------- mppa_k1c/Asmblockgenproof0.v | 36 ++++++++------- mppa_k1c/Asmblockgenproof1.v | 32 ++++++------- 4 files changed, 151 insertions(+), 57 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index c6c549cd..9da85fd0 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -506,6 +506,41 @@ Coercion PControl: control >-> instruction. Definition code := list instruction. Definition bcode := list basic. +Fixpoint basics_to_code (l: list basic) := + match l with + | nil => nil + | bi::l => (PBasic bi)::(basics_to_code l) + end. + +Fixpoint code_to_basics (c: code) := + match c with + | (PBasic i)::c => + match code_to_basics c with + | None => None + | Some l => Some (i::l) + end + | _::c => None + | nil => Some nil + end. + +Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c. +Proof. + intros. induction c as [|i c]; simpl; auto. + rewrite IHc. auto. +Qed. + +Lemma code_to_basics_dist: + forall c c' l l', + code_to_basics c = Some l -> + code_to_basics c' = Some l' -> + code_to_basics (c ++ c') = Some (l ++ l'). +Proof. + induction c as [|i c]; simpl; auto. + - intros. inv H. simpl. auto. + - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate. + inv H. erewrite IHc; eauto. auto. +Qed. + (** Asmblockgen will have to translate a Mach control into a list of instructions of the form i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index f72d8386..78aeba2a 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -925,7 +925,7 @@ Definition mb_remove_body (bb: MB.bblock) := Lemma exec_straight_pnil: forall c rs1 m1 rs2 m2, - exec_straight tge c rs1 m1 (Pnop::nil) rs2 m2 -> + exec_straight tge c rs1 m1 (Pnop::gnil) rs2 m2 -> exec_straight tge c rs1 m1 nil rs2 m2. Proof. intros. eapply exec_straight_trans. eapply H. econstructor; eauto. @@ -1006,9 +1006,20 @@ Proof. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl. Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H14. rewrite H14. auto. Simpl. simpl. subst. Simpl. simpl. unfold Val.offset_ptr. rewrite PCeq. auto. - + (* MBtailcall *) - destruct TODO. - + (* MBbuiltin *) + + (* MBtailcall *) destruct TODO. +(* destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + exploit Mem.loadv_extends. eauto. eexact H15. auto. simpl. intros [parent' [A B]]. + destruct s1 as [rf|fid]; simpl in H13. + * inv H1. + * monadInv H1. inv Hpstate. inv Hcur. assert (f = f1) by congruence. subst f1. clear FIND1. clear H14. + exploit make_epilogue_correct; eauto. + *) + + (* MBbuiltin (contradiction) *) assert (MB.exit bb' <> Some (MBbuiltin e l b)) by (apply Hbuiltin). rewrite <- H in H1. contradict H1; auto. + (* MBgoto *) @@ -1040,17 +1051,44 @@ 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, + forall c c' lc rs1 m1 rs2 m2, exec_straight tge c rs1 m1 c' rs2 m2 -> - exists l, + code_to_basics c = Some lc -> + exists l ll, c = l ++ c' - /\ exec_body tge l rs1 m1 = Next rs2 m2. + /\ code_to_basics l = Some ll + /\ exec_body tge ll 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. + intros until m2. intros EXES CTB. inv EXES. + - exists (i1 ::g nil),(i1::nil). repeat (split; simpl; auto). rewrite H6. auto. + - inv CTB. destruct (code_to_basics c); try discriminate. inv H0. + eapply IHc in H7; eauto. destruct H7 as (l' & ll & Hc & CTB & EXECB). subst. + exists (i ::g l'),(i::ll). repeat (split; simpl; auto). + rewrite CTB. auto. + rewrite H1. auto. +Qed. + +Lemma basics_to_code_app: + forall c l x ll, + basics_to_code c = l ++ basics_to_code x -> + code_to_basics l = Some ll -> + c = ll ++ x. +Proof. + intros. apply (f_equal code_to_basics) in H. + erewrite code_to_basics_dist in H; eauto. 2: eapply code_to_basics_id. + rewrite code_to_basics_id in H. inv H. auto. +Qed. + +Lemma basics_to_code_app2: + forall i c l x ll, + (PBasic i) :: basics_to_code c = l ++ basics_to_code x -> + code_to_basics l = Some ll -> + i :: c = ll ++ x. +Proof. + intros until ll. intros. + exploit basics_to_code_app. instantiate (3 := (i::c)). simpl. + all: eauto. Qed. Lemma step_simu_basic: @@ -1078,12 +1116,17 @@ Proof. rewrite (sp_val _ _ _ AG) in A. 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. + eapply exec_straight_body in EXECS. + 2: eapply code_to_basics_id; eauto. + destruct EXECS as (l & Hlbi & BTC & CTB & EXECB). + exists rs2, m1, Hlbi. eexists. eexists. split. instantiate (1 := x). eauto. - repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + repeat (split; auto). + eapply basics_to_code_app; eauto. + 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_set_mreg; eauto with asmgen. intro Hep. simpl in Hep. inv Hep. @@ -1095,10 +1138,14 @@ Proof. 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. + eapply exec_straight_body in P. + 2: eapply code_to_basics_id; eauto. + destruct P as (l & ll & TBC & CTB & EXECB). + exists rs', m2', ll. eexists. eexists. split. instantiate (1 := x). eauto. - repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + repeat (split; auto). + eapply basics_to_code_app; eauto. + 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. @@ -1125,10 +1172,14 @@ Proof. instantiate (2 := rs1). rewrite DXP; eauto. congruence. intros [rs2 [P [Q R]]]. - eapply exec_straight_body in P. destruct P as (l & Hlbi & EXECB). - exists rs2, m1, l. + eapply exec_straight_body in P. + 2: eapply code_to_basics_id; eauto. + destruct P as (l & ll & BTC & CTB & EXECB). + exists rs2, m1, ll. eexists. eexists. split. instantiate (1 := x). eauto. - repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + repeat (split; auto). + eapply basics_to_code_app; eauto. + 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. @@ -1147,10 +1198,14 @@ Proof. eapply S. intros EXES. - eapply exec_straight_body in EXES. destruct EXES as (l & Hlbi & EXECB). - exists rs3, m1, l. + eapply exec_straight_body in EXES. + 2: simpl. 2: erewrite code_to_basics_id; eauto. + destruct EXES as (l & ll & BTC & CTB & EXECB). + exists rs3, m1, ll. eexists. eexists. split. instantiate (1 := x). eauto. - repeat (split; auto). remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + repeat (split; auto). + eapply basics_to_code_app2; eauto. + 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. @@ -1213,7 +1268,7 @@ Proof. rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto. Qed. -Lemma exec_body_straight: +(* Lemma exec_body_straight: forall l rs0 m0 rs1 m1, l <> nil -> exec_body tge l rs0 m0 = Next rs1 m1 -> @@ -1228,7 +1283,7 @@ Proof. - intros until m1. intros _ EXEB. simpl in EXEB. simpl in IHl. destruct (exec_basic_instr tge i1 rs0 m0) eqn:EBI; try discriminate. econstructor; eauto. eapply IHl; eauto. discriminate. -Qed. +Qed. *) Lemma exec_body_pc: forall l rs1 m1 rs2 m2, diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 13100cdc..2b9fe5ef 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -678,17 +678,17 @@ Variable fn: function. Instructions are taken from the first list instead of being fetched from memory. *) -Inductive exec_straight: list basic -> regset -> mem -> - list basic -> regset -> mem -> Prop := +Inductive exec_straight: list instruction -> regset -> mem -> + list instruction -> regset -> mem -> Prop := | exec_straight_one: forall i1 c rs1 m1 rs2 m2, exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_straight (i1 :: c) rs1 m1 c rs2 m2 + exec_straight ((PBasic i1) ::g c) rs1 m1 c rs2 m2 | exec_straight_step: forall i c rs1 m1 rs2 m2 c' rs3 m3, exec_basic_instr ge i rs1 m1 = Next rs2 m2 -> exec_straight c rs2 m2 c' rs3 m3 -> - exec_straight (i :: c) rs1 m1 c' rs3 m3. + exec_straight ((PBasic i) :: c) rs1 m1 c' rs3 m3. Inductive exec_control_rel: option control -> bblock -> regset -> mem -> regset -> mem -> Prop := @@ -705,21 +705,23 @@ Inductive exec_bblock_rel: bblock -> regset -> mem -> regset -> mem -> Prop := exec_bblock_rel b rs1 m1 rs2 m2. Lemma exec_straight_body: - forall c rs1 m1 rs2 m2, + forall c l rs1 m1 rs2 m2, exec_straight c rs1 m1 nil rs2 m2 -> - exec_body ge c rs1 m1 = Next rs2 m2. + code_to_basics c = Some l -> + exec_body ge l rs1 m1 = Next rs2 m2. Proof. induction c as [|i c]. - - intros. inv H. - - intros. inv H. - + simpl. rewrite H7. auto. - + apply IHc in H8. rewrite <- H8. simpl. rewrite H2. auto. + - intros until m2. intros EXES CTB. inv EXES. + - intros until m2. intros EXES CTB. inv EXES. + + inv CTB. simpl. rewrite H6. auto. + + inv CTB. destruct (code_to_basics c); try discriminate. inv H0. eapply IHc in H7; eauto. + rewrite <- H7. simpl. rewrite H1. auto. Qed. (* + contradict H4. generalize i1. induction c; simpl; try discriminate. intros i0 X; inversion X. subst. eapply IHc. eauto. *) -Theorem exec_straight_bblock: +(* Theorem exec_straight_bblock: forall rs1 m1 rs2 m2 rs3 m3 b, exec_straight (body b) rs1 m1 nil rs2 m2 -> exec_control_rel (exit b) b rs2 m2 rs3 m3 -> @@ -728,7 +730,7 @@ Proof. intros. econstructor; eauto. unfold exec_bblock. erewrite exec_straight_body; eauto. inv H0. auto. -Qed. +Qed. *) Lemma exec_straight_trans: forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, @@ -747,7 +749,7 @@ Lemma exec_straight_two: exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one -> - exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. + exec_straight (i1 ::g i2 ::g c) rs1 m1 c rs3 m3. Proof. intros. apply exec_straight_step with rs2 m2; auto. apply exec_straight_one; auto. @@ -761,7 +763,7 @@ Lemma exec_straight_three: rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one -> rs4#PC = Val.offset_ptr rs3#PC Ptrofs.one -> - exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. + exec_straight (i1 ::g i2 ::g i3 ::g c) rs1 m1 c rs4 m4. Proof. intros. apply exec_straight_step with rs2 m2; auto. eapply exec_straight_two; eauto. @@ -847,7 +849,7 @@ Proof. erewrite exec_basic_instr_pc; eauto. Qed. -Lemma exec_straight_through: +(* Lemma exec_straight_through: forall c i b lb rs1 m1 rs2 m2 rs2' m2', bblock_basic_ctl c i = b -> exec_straight c rs1 m1 nil rs2 m2 -> @@ -864,11 +866,11 @@ Proof. + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto. Qed. - + *) Lemma exec_straight_through_singleinst: forall a b rs1 m1 rs2 m2 rs2' m2' lb, bblock_single_inst (PBasic a) = b -> - exec_straight (a::nil) rs1 m1 nil rs2 m2 -> + exec_straight (a ::g nil) rs1 m1 nil rs2 m2 -> nextblock b rs2 = rs2' -> m2 = m2' -> exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'. Proof. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 74b8f8b5..40e3f444 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -320,7 +320,7 @@ Ltac ArgsInv := Definition bla := 0. -Inductive exec_straight_opt: list basic -> regset -> mem -> list basic -> regset -> mem -> Prop := +Inductive exec_straight_opt: list instruction -> regset -> mem -> list instruction -> regset -> mem -> Prop := | exec_straight_opt_refl: forall c rs m, exec_straight_opt c rs m c rs m | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2, @@ -1235,8 +1235,8 @@ Lemma indexed_memory_access_correct: forall mk_instr base ofs k rs m, base <> GPR31 -> exists base' ofs' rs', - exec_straight_opt (indexed_memory_access mk_instr base ofs :: k) rs m - (mk_instr base' ofs' :: k) rs' m + exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m + (mk_instr base' ofs' ::g k) rs' m /\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. @@ -1286,7 +1286,7 @@ Lemma indexed_load_access_correct: Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> rd <> PC -> exists rs', - exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m + exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m /\ rs'#rd = v /\ forall r, r <> PC -> r <> GPR31 -> r <> rd -> rs'#r = rs#r. Proof. @@ -1307,7 +1307,7 @@ Lemma indexed_store_access_correct: Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' -> base <> GPR31 -> r1 <> GPR31 -> r1 <> PC -> exists rs', - exec_straight ge (indexed_memory_access mk_instr base ofs :: k) rs m k rs' m' + exec_straight ge (indexed_memory_access mk_instr base ofs ::g k) rs m k rs' m' /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31' NOTPC. @@ -1325,7 +1325,7 @@ Lemma loadind_correct: Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> exists rs', - exec_straight ge c rs m k rs' m + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> GPR31 -> r <> preg_of dst -> rs'#r = rs#r. Proof. @@ -1347,7 +1347,7 @@ Lemma storeind_correct: 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 c rs m k rs' m' + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m' /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros until m'; intros TR STORE NOT31. @@ -1367,7 +1367,7 @@ Lemma Pget_correct: forall (dst: gpreg) (src: preg) k (rs: regset) m, src = RA -> exists rs', - exec_straight ge (Pget dst src :: k) rs m k rs' m + exec_straight ge (Pget dst src ::g k) rs m k rs' m /\ rs'#dst = rs#src /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r. Proof. @@ -1401,7 +1401,7 @@ Lemma loadind_ptr_correct: Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR31 -> exists rs', - exec_straight ge (loadind_ptr base ofs dst :: k) rs m k rs' m + exec_straight ge (loadind_ptr base ofs dst ::g k) rs m k rs' m /\ rs'#dst = v /\ forall r, r <> PC -> r <> GPR31 -> r <> dst -> rs'#r = rs#r. Proof. @@ -1414,7 +1414,7 @@ Lemma storeind_ptr_correct: Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' -> base <> GPR31 -> src <> GPR31 -> exists rs', - exec_straight ge (storeind_ptr src base ofs :: k) rs m k rs' m' + exec_straight ge (storeind_ptr src base ofs ::g k) rs m k rs' m' /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen. @@ -1544,17 +1544,20 @@ Proof. rewrite D in STORE; clear D. eapply transl_store_access_correct; eauto with asmgen. Qed. +*) +Definition noscroll := 0. +(* Lemma make_epilogue_correct: forall ge0 f m stk soff cs m' ms rs k tm, - load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) -> - load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) -> + Mach.load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) -> + Mach.load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> agree ms (Vptr stk soff) rs -> Mem.extends m tm -> match_stack ge0 cs -> exists rs', exists tm', - exec_straight ge fn (make_epilogue f k) rs tm k rs' tm' + exec_straight ge (make_epilogue f k) rs tm k rs' tm' /\ agree ms (parent_sp cs) rs' /\ Mem.extends m' tm' /\ rs'#RA = parent_ra cs @@ -1600,8 +1603,7 @@ Proof. intros. Simpl. rewrite C2; auto. Qed. - -*) + *) End CONSTRUCTORS. -- cgit