MPPA - Preuve de make_epilogue correct.

ça va un peu plus loin!

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. *)