From e3aed59a6d58f4486da40e0a7a381ea0bf10ba81 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 12 Mar 2018 18:17:09 +0100 Subject: MPPA - Preuve de make_epilogue correct. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ça va un peu plus loin! --- mppa_k1c/Asm.v | 3 ++- mppa_k1c/Asmgen.v | 7 ++++--- mppa_k1c/Asmgenproof1.v | 54 ++++++++++++++++++++++++++++++++++++++----------- mppa_k1c/Conventions1.v | 2 +- mppa_k1c/Machregs.v | 10 ++++----- 5 files changed, 54 insertions(+), 22 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f5ff7c78..4122ac29 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -1019,7 +1019,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Definition preg_of (r: mreg) : preg := match r with | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4 - | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9 + | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R9 => GPR9 (*| R10 => GPR10 | R11 => GPR11 | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *) | R15 => GPR15 | R16 => GPR16 | R17 => GPR17 | R18 => GPR18 | R19 => GPR19 | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 @@ -1186,6 +1186,7 @@ Definition data_preg (r: preg) : bool := match r with | RA => false | IR GPR31 => false (* FIXME - GPR31 is used as temporary in some instructions.. ??? *) + | IR GPR8 => false (* FIXME - idem *) | IR _ => true | FR _ => true | PC => false diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 1edb209d..ba9e6fe8 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -843,8 +843,8 @@ Definition make_epilogue (f: Mach.function) (k: code) := *) Definition make_epilogue (f: Mach.function) (k: code) := - Pset RA GPR8 :: loadind_ptr SP f.(fn_retaddr_ofs) GPR8 - (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). + loadind_ptr SP f.(fn_retaddr_ofs) GPR8 + (Pset RA GPR8 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k). (* Definition make_epilogue (f: Mach.function) (k: code) := @@ -942,7 +942,8 @@ Definition transl_function (f: Mach.function) := do c <- transl_code' f f.(Mach.fn_code) true; OK (mkfunction f.(Mach.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - storeind_ptr GPR8 SP f.(fn_retaddr_ofs) (Pget GPR8 RA :: c))). + Pget GPR8 RA :: + storeind_ptr GPR8 SP f.(fn_retaddr_ofs) c)). (* Definition transl_function (f: Mach.function) := diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index b782608b..7fe9b3f7 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -1235,6 +1235,22 @@ Proof. eapply indexed_store_access_correct; eauto with asmgen. Qed. *) + +Lemma Pset_correct: + forall (dst: preg) (src: gpreg) k (rs: regset) m, + dst = RA -> + exists rs', + exec_straight ge fn (Pset dst src :: k) rs m k rs' m + /\ rs'#dst = rs#src + /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r. +Proof. + intros. econstructor; econstructor; econstructor; simpl. + rewrite H. auto. + Simpl. + Simpl. + intros. rewrite H. Simpl. +Qed. + Lemma loadind_ptr_correct: forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v, Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v -> @@ -1387,7 +1403,7 @@ Lemma make_epilogue_correct: /\ Mem.extends m' tm' /\ rs'#RA = parent_ra cs /\ rs'#SP = parent_sp cs - /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> GPR31 -> rs'#r = rs#r). + /\ (forall r, r <> PC -> r <> RA -> r <> SP -> r <> GPR31 -> r <> GPR8 -> rs'#r = rs#r). Proof. intros until tm; intros LP LRA FREE AG MEXT MCS. exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP'). @@ -1398,21 +1414,35 @@ Proof. unfold make_epilogue. rewrite chunk_of_Tptr in *. - exploit (loadind_ptr_correct SP (fn_retaddr_ofs f) RA (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs tm). - rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. congruence. - intros (rs1 & A1 & B1 & C1). - econstructor; econstructor; split. - eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. - rewrite (C1 X2) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. - rewrite FREE'. eauto. auto. - split. apply agree_nextinstr. apply agree_set_other; auto with asmgen. + exploit (loadind_ptr_correct SP (fn_retaddr_ofs f) GPR8 (Pset RA GPR8 + :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs tm). + - rewrite <- (sp_val _ _ rs AG). simpl. eexact LRA'. + - congruence. + - intros (rs1 & A1 & B1 & C1). + assert (agree ms (Vptr stk soff) rs1) as AG1. + + destruct AG. + apply mkagree; auto. + rewrite C1; discriminate || auto. + intro. rewrite C1; auto; destruct r; simpl; try discriminate. + + exploit (Pset_correct RA GPR8 (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs1 tm). auto. + intros (rs2 & A2 & B2 & C2). + econstructor; econstructor; split. + * eapply exec_straight_trans. + { eexact A1. } + { eapply exec_straight_trans. + { eapply A2. } + { apply exec_straight_one. simpl. + rewrite (C2 GPR12) by auto with asmgen. rewrite <- (sp_val _ _ rs1 AG1). simpl; rewrite LP'. + rewrite FREE'; eauto. auto. } } + * split. apply agree_nextinstr. apply agree_set_other; auto with asmgen. apply agree_change_sp with (Vptr stk soff). - apply agree_exten with rs; auto. intros; apply C1; auto with asmgen. + apply agree_exten with rs; auto. intros; rewrite C2; auto with asmgen. eapply parent_sp_def; eauto. split. auto. + split. Simpl. rewrite B2. auto. split. Simpl. - split. Simpl. - intros. Simpl. + intros. Simpl. + rewrite C2; auto. Qed. End CONSTRUCTORS. diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index 42905b30..6bb616c8 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -40,7 +40,7 @@ Definition is_callee_save (r: mreg): bool := end. Definition int_caller_save_regs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 :: R40 :: R41 :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49 :: R50 :: R51 :: R52 :: R53 :: R54 :: R55 :: R56 :: R57 :: R58 :: R59 :: R60 :: R61 diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 09a6a237..d30cdbbd 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -41,7 +41,7 @@ Require Import Op. (* FIXME - no R31 *) Inductive mreg: Type := (* Allocatable General Purpose regs. *) - | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R8 | R9 + | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 | R9 (* R10 to R14 are reserved *) | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 | R32 | R33 | R34 | R35 | R36 | R37 | R38 | R39 @@ -54,7 +54,7 @@ Proof. decide equality. Defined. Global Opaque mreg_eq. Definition all_mregs := - R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: R9 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R32 :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39 @@ -86,7 +86,7 @@ Module IndexedMreg <: INDEXED_TYPE. Definition index (r: mreg): positive := match r with R0 => 1 | R1 => 2 | R2 => 3 | R3 => 4 | R4 => 5 - | R5 => 6 | R6 => 7 | R7 => 8 | R8 => 9 | R9 => 10 + | R5 => 6 | R6 => 7 | R7 => 8 | R9 => 10 | R15 => 16 | R16 => 17 | R17 => 18 | R18 => 19 | R19 => 20 | R20 => 21 | R21 => 22 | R22 => 23 | R23 => 24 | R24 => 25 | R25 => 26 | R26 => 27 | R27 => 28 | R28 => 29 | R29 => 30 @@ -113,7 +113,7 @@ Local Open Scope string_scope. Definition register_names := ("R0", R0) :: ("R1", R1) :: ("R2", R2) :: ("R3", R3) :: ("R4", R4) - :: ("R5", R5) :: ("R6", R6) :: ("R7", R7) :: ("R8", R8) :: ("R9", R9) + :: ("R5", R5) :: ("R6", R6) :: ("R7", R7) :: ("R9", R9) :: ("R15", R15) :: ("R16", R16) :: ("R17", R17) :: ("R18", R18) :: ("R19", R19) :: ("R20", R20) :: ("R21", R21) :: ("R22", R22) :: ("R23", R23) :: ("R24", R24) :: ("R25", R25) :: ("R26", R26) :: ("R27", R27) :: ("R28", R28) :: ("R29", R29) @@ -175,7 +175,7 @@ Definition destroyed_by_setstack (ty: typ): list mreg := nil. (* Definition destroyed_at_function_entry: list mreg := R30 :: nil. *) Definition destroyed_at_function_entry: list mreg := nil. -Definition temp_for_parent_frame: mreg := R8. (* FIXME - and R9 ?? *) +Definition temp_for_parent_frame: mreg := R9. (* FIXME - and R8 ?? *) Definition destroyed_at_indirect_call: list mreg := nil. (* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *) -- cgit