The parent frame pointer is now R17 instead of R14

7 files changed, 21 insertions, 27 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 5279bd29..4757b9fc 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -85,7 +85,8 @@ Module Pregmap := EMap(PregEq).
 (** Conventional names for stack pointer ([SP]) and return address ([RA]). *)
 
 Notation "'SP'" := GPR12 (only parsing) : asm.
-Notation "'FP'" := GPR14 (only parsing) : asm.
+Notation "'FP'" := GPR17 (only parsing) : asm.
+Notation "'MFP'" := R17 (only parsing) : asm.
 Notation "'GPRA'" := GPR16 (only parsing) : asm.
 Notation "'RTMP'" := GPR32 (only parsing) : asm.
 
@@ -1445,7 +1446,7 @@ 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
-  | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | *) | R14  => GPR14
+  | 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
   | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29  => GPR29
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index c5b5bd56..b77fa47d 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -750,7 +750,7 @@ Proof.
       rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity.
     * Simpl.
     * intros rr; destruct rr; Simpl.
-      destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl.
+      destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
 (* Freeframe *)
   - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate.
     destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0.
@@ -758,7 +758,7 @@ Proof.
     * simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE.
       Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity.
     * Simpl.
-    * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR14)]]; subst; Simpl.
+    * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
 (* Pget *)
   - simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0.
     eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 9d682bed..f28102f8 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -25,8 +25,6 @@ Require Import Op Locations Machblock Asmblock.
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
 
-Notation "'MFP'" := R14 (only parsing). 
-
 (** The code generation functions take advantage of several
   characteristics of the [Mach] code generated by earlier passes of the
   compiler, mostly that argument and result registers are of the correct
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 84877488..ddc96f6c 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -758,9 +758,9 @@ Qed. *)
   the unwanted behaviour. *)

 

 

-Remark preg_of_not_FP: forall r, negb (mreg_eq r R14) = true -> IR FP <> preg_of r.

+Remark preg_of_not_FP: forall r, negb (mreg_eq r MFP) = true -> IR FP <> preg_of r.

 Proof.

-  intros. change (IR FP) with (preg_of R14). red; intros.

+  intros. change (IR FP) with (preg_of MFP). red; intros.

   exploit preg_of_injective; eauto. intros; subst r; discriminate.

 Qed.

 

diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index cd6cf1ec..22c424c1 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -401,16 +401,14 @@ let expand_instruction instr =
   match instr with
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
+      emit (Pmv (Asmblock.GPR17, stack_pointer));
       if sg.sig_cc.cc_vararg then begin
         let n = arguments_size sg in
         let extra_sz = if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize) in
-        let full_sz = Z.add sz (Z.of_uint extra_sz) in begin
-          expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg full_sz));
-          emit Psemi;
-          expand_storeind_ptr Asmblock.GPR14 stack_pointer ofs;
-          expand_addptrofs Asmblock.GPR14 stack_pointer (Ptrofs.repr full_sz)
-        end;
+        let full_sz = Z.add sz (Z.of_uint extra_sz) in
+        expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg full_sz));
         emit Psemi;
+        expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs;
         let va_ofs =
             sz in
           (*Z.add full_sz (Z.of_sint ((n - _nbregargs_) * wordsize)) in *)
@@ -419,9 +417,7 @@ let expand_instruction instr =
       end else begin
         expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.neg sz));
         emit Psemi;
-        expand_storeind_ptr Asmblock.GPR14 stack_pointer ofs;
-        expand_addptrofs Asmblock.GPR14 stack_pointer (Ptrofs.repr sz);
-        emit Psemi;
+        expand_storeind_ptr Asmblock.GPR17 stack_pointer ofs;
         vararg_start_ofs := None
       end
   | Pfreeframe (sz, ofs) ->
@@ -431,7 +427,6 @@ let expand_instruction instr =
         let n = arguments_size sg in
         if n >= _nbregargs_ then 0 else (* align _alignment_ *) ((_nbregargs_ - n) * wordsize)
       end else 0 in
-     expand_loadind_ptr Asmblock.GPR14 stack_pointer ofs;
      expand_addptrofs stack_pointer stack_pointer (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
 
 (*| Pseqw(rd, rs1, rs2) ->
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 1c1930da..28154c7f 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -41,7 +41,7 @@ Require Import Op.
 Inductive mreg: Type :=
   (* Allocatable General Purpose regs. *)
   | R0  | R1  | R2  | R3  | R4  | R5  | R6  | R7  | R8  | R9
-  | R10 | R11 | (* R12 | R13 | *) R14 | R15 (* | R16 *) | R17 | R18 | R19
+  | R10 | R11 (* | R12 | R13 | R14 *) | R15  (* | R16 *) | R17 | R18 | R19
   | R20 | R21 | R22 | R23 | R24 | R25 | R26 | R27 | R28 | R29
   | R30 | R31 (* | R32 *) | R33 | R34 | R35 | R36 | R37 | R38 | R39
   | R40 | R41 | R42 | R43 | R44 | R45 | R46 | R47 | R48 | R49
@@ -54,7 +54,7 @@ Global Opaque mreg_eq.
 
 Definition all_mregs :=
      R0  :: R1  :: R2  :: R3  :: R4  :: R5  :: R6  :: R7  :: R8  :: R9
-  :: R10 :: R11 (* :: R12 :: R13 *) :: R14 :: R15 (* :: R16 *) :: R17 :: R18 :: R19
+  :: R10 :: R11 (* :: R12 :: R13 :: R14 *) :: R15  (* :: R16 *) :: R17 :: R18 :: R19
   :: R20 :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29
   :: R30 :: R31 (* :: R32 *) :: R33 :: R34 :: R35 :: R36 :: R37 :: R38 :: R39
   :: R40 :: R41 :: R42 :: R43 :: R44 :: R45 :: R46 :: R47 :: R48 :: R49
@@ -86,7 +86,7 @@ Module IndexedMreg <: INDEXED_TYPE.
     match r with
     | R0  => 1  | R1  => 2  | R2  => 3  | R3  => 4  | R4  => 5
     | R5  => 6  | R6  => 7  | R7  => 8  | R8  => 9  | R9  => 10
-    | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 *) | R14 => 15
+    | R10 => 11 | R11 => 12 (* | R12 => 13 | R13 => 14 | R14 => 15 *)
     | 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
@@ -115,7 +115,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)
-  :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) *) :: ("R14", R14)
+  :: ("R10", R10) :: ("R11", R11) (* :: ("R12", R12) :: ("R13", R13) :: ("R14", R14) *)
   :: ("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)
@@ -174,9 +174,9 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
 
 Definition destroyed_by_setstack (ty: typ): list mreg := nil.
 
-Definition destroyed_at_function_entry: list mreg := R14 :: nil.
+Definition destroyed_at_function_entry: list mreg := R17 :: nil.
 
-Definition temp_for_parent_frame: mreg := R14. (* FIXME - ?? *)
+Definition temp_for_parent_frame: mreg := R17. (* Temporary used to store the parent frame, where the arguments are *)
 
 Definition destroyed_at_indirect_call: list mreg := nil.
   (* R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: R16 :: R17 :: nil. *)
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 2de49faa..33912203 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -67,8 +67,8 @@ Proof.
     erewrite exec_basic_instr_pc; eauto.
 Qed.
 
-Lemma next_eq {A: Type}:
-  forall (rs rs':A) m m',
+Lemma next_eq:
+  forall (rs rs': regset) m m',
   rs = rs' -> m = m' -> Next rs m = Next rs' m'.
 Proof.
   intros. congruence.
@@ -136,7 +136,7 @@ Proof.
     inv H. apply next_eq; auto. apply functional_extensionality. intros.
     rewrite (regset_double_set GPR32 PC); try discriminate.
     rewrite (regset_double_set GPR12 PC); try discriminate.
-    rewrite (regset_double_set GPR14 PC); try discriminate. reflexivity.
+    rewrite (regset_double_set FP PC); try discriminate. reflexivity.
   - repeat (rewrite Pregmap.gso; try discriminate).
     destruct (Mem.loadv _ _ _); try discriminate.
     destruct (rs GPR12); try discriminate.