MPPA - code cleaning

9 files changed, 66 insertions, 113 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 9c85dbbd..e7dfdc52 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -15,7 +15,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for RISC-V assembly language. *)
+(** Abstract syntax and semantics for K1c assembly language. *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -38,22 +38,22 @@ Require Import Conventions.
 Inductive gpreg: Type :=
   | GPR0:  gpreg | GPR1:  gpreg | GPR2:  gpreg | GPR3:  gpreg | GPR4:  gpreg
   | GPR5:  gpreg | GPR6:  gpreg | GPR7:  gpreg | GPR8:  gpreg | GPR9:  gpreg
-  | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg 
-  | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg 
-  | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg 
-  | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg 
-  | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg 
-  | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg 
-  | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg 
-  | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg 
-  | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg 
-  | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg 
+  | GPR10: gpreg | GPR11: gpreg | GPR12: gpreg | GPR13: gpreg | GPR14: gpreg
+  | GPR15: gpreg | GPR16: gpreg | GPR17: gpreg | GPR18: gpreg | GPR19: gpreg
+  | GPR20: gpreg | GPR21: gpreg | GPR22: gpreg | GPR23: gpreg | GPR24: gpreg
+  | GPR25: gpreg | GPR26: gpreg | GPR27: gpreg | GPR28: gpreg | GPR29: gpreg
+  | GPR30: gpreg | GPR31: gpreg | GPR32: gpreg | GPR33: gpreg | GPR34: gpreg
+  | GPR35: gpreg | GPR36: gpreg | GPR37: gpreg | GPR38: gpreg | GPR39: gpreg
+  | GPR40: gpreg | GPR41: gpreg | GPR42: gpreg | GPR43: gpreg | GPR44: gpreg
+  | GPR45: gpreg | GPR46: gpreg | GPR47: gpreg | GPR48: gpreg | GPR49: gpreg
+  | GPR50: gpreg | GPR51: gpreg | GPR52: gpreg | GPR53: gpreg | GPR54: gpreg
+  | GPR55: gpreg | GPR56: gpreg | GPR57: gpreg | GPR58: gpreg | GPR59: gpreg
   | GPR60: gpreg | GPR61: gpreg | GPR62: gpreg | GPR63: gpreg.
 
 Definition ireg := gpreg.
 
 (* FIXME - placeholder definitions to make sure the Risc-V instruction definitions work *)
-Inductive ireg0: Type := 
+Inductive ireg0: Type :=
   | GPR: gpreg -> ireg0.
 
 Coercion GPR: gpreg >-> ireg0.
@@ -138,7 +138,7 @@ Inductive instruction : Type :=
   | Pget    (rd: ireg) (rs: preg)                    (**r get system register *)
   | Pset    (rd: preg) (rs: ireg)                    (**r set system register *)
   | Pret                                             (**r return *)
-  
+
   | Pmv     (rd: ireg) (rs: ireg)                    (**r integer move *)
 
 (** 32-bit integer register-immediate instructions *)
@@ -175,7 +175,7 @@ Inductive instruction : Type :=
   | Psraw   (rd: ireg) (rs1 rs2: ireg0)              (**r shift-right-arith *)
 
 (** 64-bit integer register-immediate instructions *)
-*)  | Paddil  (rd: ireg) (rs: ireg0) (imm: int64)      (**r add immediate *) (*
+*)| Paddil  (rd: ireg) (rs: ireg0) (imm: int64)      (**r add immediate *) (*
   | Psltil  (rd: ireg) (rs: ireg0) (imm: int64)      (**r set-less-than immediate *)
   | Psltiul (rd: ireg) (rs: ireg0) (imm: int64)      (**r set-less-than unsigned immediate *)
   | Pandil  (rd: ireg) (rs: ireg0) (imm: int64)      (**r and immediate *)
@@ -339,15 +339,14 @@ Inductive instruction : Type :=
   | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
   | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
   | Plabel  (lbl: label)                            (**r define a code label *)
-(*  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
+(*| Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
   | Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
   | Ploadli (rd: ireg) (i: int64)                   (**r load an immediate int64 *)
   | Ploadfi (rd: freg) (f: float)                   (**r load an immediate float *)
   | Ploadsi (rd: freg) (f: float32)                 (**r load an immediate single *)
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
-              -> builtin_res preg -> instruction.   (**r built-in function (pseudo) *) (*
-*)
+              -> builtin_res preg -> instruction.   (**r built-in function (pseudo) *)
 
 (** The pseudo-instructions are the following:
 
@@ -444,23 +443,11 @@ Definition getw (rs: regset) (r: ireg0) : val :=
   match r with
   | GPR r => rs r
   end.
-(*
-  match r with
-  | X0 => Vint Int.zero
-  | X r => rs r
-  end.
-*)
 
 Definition getl (rs: regset) (r: ireg0) : val :=
   match r with
   | GPR r => rs r
   end.
-(*
-  match r with
-  | X0 => Vlong Int64.zero
-  | X r => rs r
-  end.
-*)
 
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
 Notation "a ## b" := (getw a b) (at level 1) : asm.
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index fea71f61..f21ad2eb 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -604,7 +604,7 @@ let int_reg_to_dwarf = function
 let preg_to_dwarf = function
    | IR r -> int_reg_to_dwarf r
    | FR r -> int_reg_to_dwarf r
-   | RA   -> 65 (* FIXME - No idea *)
+   | RA   -> 65 (* FIXME - No idea what is $ra DWARF number in k1-gdb *)
    | _ -> assert false
 
 let expand_function id fn =
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index efcafda2..2d2c2e3b 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -68,7 +68,7 @@ Definition make_immed64 (val: int64) := Imm64_single val.
 Definition load_hilo32 (r: ireg) (hi lo: int) k :=
   if Int.eq lo Int.zero then Pluiw r hi :: k
   else Pluiw r hi :: Paddiw r r lo :: k.
-*)  
+*)
 Definition loadimm32 (r: ireg) (n: int) (k: code) :=
   match make_immed32 n with
   | Imm32_single imm => Pmake r imm :: k
@@ -88,8 +88,7 @@ Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
 Definition sltimm32 := opimm32 Psltw Psltiw.
 Definition sltuimm32 := opimm32 Psltuw Psltiuw.
-*)
-(*
+
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
   else Pluil r hi :: Paddil r r lo :: k.
@@ -490,7 +489,7 @@ Definition transl_op
           Psraiw GPR31 rs (Int.repr 31) ::
           Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) ::
           Paddw GPR31 rs GPR31 ::
-          Psraiw rd GPR31 n :: k)  
+          Psraiw rd GPR31 n :: k)
 
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
@@ -579,7 +578,7 @@ Definition transl_op
           Psrail GPR31 rs (Int.repr 63) ::
           Psrlil GPR31 GPR31 (Int.sub Int64.iwordsize' n) ::
           Paddl GPR31 rs GPR31 ::
-          Psrail rd GPR31 n :: k)  
+          Psrail rd GPR31 n :: k)
 
   | Onegf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
@@ -802,37 +801,10 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
 
 (** Function epilogue *)
 
-(*
-Definition store_ra (base: ireg) (ofs: ptrofs) (k: code) :=
-  indexed_memory_access (Psd GPR8) base ofs (Pget GPR8 RA :: k)
-  .
-*)
-
-(*
-Definition make_ra (base: ireg) (ofs: ptrofs) (k: code) :=
-  Pset RA GPR8
-  :: (indexed_memory_access (Pld GPR8) base ofs k) (* FIXME - not sure about GPR8 *)
-  .
-*)
-
-(*
-Definition make_epilogue (f: Mach.function) (k: code) :=
-  Pset RA GPR8 :: (indexed_memory_access (Pld GPR8) SP f.(fn_retaddr_ofs) (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k))
-  (* make_ra SP f.(fn_retaddr_ofs)
-     (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k) *)
-  .
-*)
-
 Definition make_epilogue (f: Mach.function) (k: code) :=
   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) :=
-  loadind_ptr SP f.(fn_retaddr_ofs) RA
-    (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
-*)
-
 (** Translation of a Mach instruction. *)
 
 Definition transl_instr (f: Mach.function) (i: Mach.instruction)
@@ -926,15 +898,6 @@ Definition transl_function (f: Mach.function) :=
          Pget GPR8 RA ::
          storeind_ptr GPR8 SP f.(fn_retaddr_ofs) c)).
 
-(*
-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) ::
-         indexed_memory_access (Psd GPR8) SP f.(fn_retaddr_ofs) (Pget GPR8 RA :: c))).
-         (* store_ra SP f.(fn_retaddr_ofs) c)). *)
-*)
-
 Definition transf_function (f: Mach.function) : res Asm.function :=
   do tf <- transl_function f;
   if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code))
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index a5ea3bb9..45531e00 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -119,6 +119,7 @@ Remark loadimm32_label:
   forall r n k, tail_nolabel k (loadimm32 r n k).
 Proof.
   intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.
+(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
 Qed.
 Hint Resolve loadimm32_label: labels.
 (*
@@ -137,6 +138,7 @@ Remark loadimm64_label:
   forall r n k, tail_nolabel k (loadimm64 r n k).
 Proof.
   intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.
+(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)
 Qed.
 Hint Resolve loadimm64_label: labels.
 
@@ -658,7 +660,7 @@ Proof.
   rewrite (sp_val _ _ _ AG) in A.
   left; eapply exec_straight_steps; eauto. intros. simpl in TR.
   inversion TR.
-(*  
+(*
   intros [rs' [P [Q R]]].
 
   exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
@@ -689,7 +691,7 @@ Proof.
   intros [v' [C D]].
 (* Opaque loadind. *)
   left; eapply exec_straight_steps; eauto; intros. monadInv TR.
-(* 
+(*
   destruct ep.
 (* X30 contains parent *)
   exploit loadind_correct. eexact EQ.
@@ -752,7 +754,7 @@ Local Transparent destroyed_by_op.
   assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto.
   exploit Mem.storev_extends; eauto. intros [m2' [C D]].
   left; eapply exec_straight_steps; eauto.
-  intros. simpl in TR. 
+  intros. simpl in TR.
   inversion TR.
 (*exploit transl_store_correct; eauto. intros [rs2 [P Q]].
   exists rs2; split. eauto.
@@ -971,8 +973,8 @@ Local Transparent destroyed_by_op.
     assert (rs' GPR12 = rs2 GPR12). { apply V'; discriminate. }
     rewrite H3. rewrite H4.
     (* change (rs' GPR8) with (rs0 RA). *)
-    rewrite ATLR. 
-    change (rs2 GPR12) with sp. eexact P. 
+    rewrite ATLR.
+    change (rs2 GPR12) with sp. eexact P.
     congruence. congruence.
   intros (rs3 & U & V).
   assert (EXEC_PROLOGUE:
@@ -985,7 +987,7 @@ Local Transparent destroyed_by_op.
     rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. rewrite F. reflexivity.
     reflexivity.
     eapply exec_straight_trans.
-    - eexact U'.  
+    - eexact U'.
     - eexact U. }
   exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor.
   intros (ofs' & X & Y).                    
@@ -1003,7 +1005,7 @@ Local Transparent destroyed_at_function_entry.
   unfold sp; congruence.
 
   intros.
-  assert (r <> GPR31). { contradict H3; rewrite H3; unfold data_preg; auto. } 
+  assert (r <> GPR31). { contradict H3; rewrite H3; unfold data_preg; auto. }
   rewrite V.
   assert (r <> GPR8). { contradict H3; rewrite H3; unfold data_preg; auto. }
   assert (forall r : preg, r <> PC -> r <> GPR8 -> rs' r = rs2 r). { apply V'. }
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index f83275a1..6957ab87 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -175,7 +175,7 @@ Proof.
 Qed.
 
 (** 64-bit integer constants and arithmetic *)
-  
+
 Lemma load_hilo64_correct:
   forall rd hi lo k rs m,
   exists rs',
@@ -194,7 +194,7 @@ Proof.
   split. Simpl. 
   intros; Simpl.
 Qed.
-  
+
 Lemma loadimm64_correct:
   forall rd n k rs m,
   exists rs',
@@ -381,7 +381,7 @@ Qed.
 
 Remark branch_on_GPR31:
   forall normal lbl (rs: regset) m b,
-  rs#GPR31 = Val.of_bool (eqb normal b) -> 
+  rs#GPR31 = Val.of_bool (eqb normal b) ->
   exec_instr ge fn (if normal then Pbnew GPR31 X0 lbl else Pbeqw GPR31 X0 lbl) rs m =
   eval_branch fn lbl rs m (Some b).
 Proof.
@@ -1072,12 +1072,12 @@ Opaque Int.eq.
   assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
   rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
   rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto.
-  
+
 - (* addlimm *)
   exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
   exists rs'; split; eauto. rewrite B; auto with asmgen.
-  
+
 - (* andimm *)
   exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
@@ -1251,7 +1251,7 @@ Proof.
 - simpl. rewrite H. auto.
 - Simpl.
 - Simpl.
-- intros. rewrite H. Simpl. 
+- intros. rewrite H. Simpl.
 Qed.
 
 Lemma Pset_correct:
@@ -1431,14 +1431,14 @@ Proof.
   exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
   unfold make_epilogue. 
   rewrite chunk_of_Tptr in *.
-  
+
   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.  
+    + destruct AG.
       apply mkagree; auto.
       rewrite C1; discriminate || auto.
       intro. rewrite C1; auto; destruct r; simpl; try discriminate.
@@ -1457,7 +1457,7 @@ Proof.
     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. rewrite B2. auto.
   split. Simpl. 
   intros. Simpl.
   rewrite C2; auto.
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v
index 6bb616c8..68beb560 100644
--- a/mppa_k1c/Conventions1.v
+++ b/mppa_k1c/Conventions1.v
@@ -32,7 +32,7 @@ Require Import AST Machregs Locations.
   of callee- and caller-save registers.
 *)
 
-Definition is_callee_save (r: mreg): bool :=
+Definition is_callee_save (r: mreg) : bool :=
   match r with
   | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22
   | R23 | R24 | R25 | R26 | R27 | R28 | R29 | R30 => true
@@ -90,7 +90,7 @@ Definition is_float_reg (r: mreg) := false.
   with one integer result. *)
 
 Definition loc_result (s: signature) : rpair mreg :=
-   match s.(sig_res) with 
+   match s.(sig_res) with
    | None => One R0
    | Some (Tint | Tany32) => One R0
    | Some (Tfloat | Tsingle | Tany64) => One R0
@@ -334,7 +334,10 @@ Proof.
 
   cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)).
   unfold OK. eauto.
-  induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.  - red; simpl; tauto.  - destruct ty1.  + (* int *) apply A; auto.
+  induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
+  - red; simpl; tauto.
+  - destruct ty1.  
++ (* int *) apply A; auto.
 + (* float *) 
   apply A; auto.
 + (* long *)
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index ee7d91da..ce86a06f 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -85,18 +85,19 @@ Module IndexedMreg <: INDEXED_TYPE.
   Definition eq := mreg_eq.
   Definition index (r: mreg): positive :=
     match r with
-    R0  => 1  | R1  => 2  | R2  => 3  | R3  => 4  | R4  => 5 
-  | 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
-  | R30 => 31 |             R32 => 33 | R33 => 34 | R34 => 35 
-  | R35 => 36 | R36 => 37 | R37 => 38 | R38 => 39 | R39 => 40
-  | R40 => 41 | R41 => 42 | R42 => 43 | R43 => 44 | R44 => 45 
-  | R45 => 46 | R46 => 47 | R47 => 48 | R48 => 49 | R49 => 50
-  | R50 => 51 | R51 => 52 | R52 => 53 | R53 => 54 | R54 => 55 
-  | R55 => 56 | R56 => 57 | R57 => 58 | R58 => 59 | R59 => 60
-  | R60 => 61 | R61 => 62 | R62 => 63 | R63 => 64 end.
+    | R0  => 1  | R1  => 2  | R2  => 3  | R3  => 4  | R4  => 5
+    | 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
+    | R30 => 31 |             R32 => 33 | R33 => 34 | R34 => 35
+    | R35 => 36 | R36 => 37 | R37 => 38 | R38 => 39 | R39 => 40
+    | R40 => 41 | R41 => 42 | R42 => 43 | R43 => 44 | R44 => 45
+    | R45 => 46 | R46 => 47 | R47 => 48 | R48 => 49 | R49 => 50
+    | R50 => 51 | R51 => 52 | R52 => 53 | R53 => 54 | R54 => 55 
+    | R55 => 56 | R56 => 57 | R57 => 58 | R58 => 59 | R59 => 60
+    | R60 => 61 | R61 => 62 | R62 => 63 | R63 => 64 
+    end.
 
   Lemma index_inj:
     forall r1 r2, index r1 = index r2 -> r1 = r2.
@@ -112,8 +113,8 @@ Definition is_stack_reg (r: mreg) : bool := false.
 Local Open Scope string_scope.
 
 Definition register_names :=
-     ("R0", R0)   :: ("R1", R1)   :: ("R2", R2)   :: ("R3", R3)   :: ("R4", R4)  
-  :: ("R5", R5)   :: ("R6", R6)   :: ("R7", R7)                   :: ("R9", R9) 
+     ("R0" , R0)  :: ("R1" , R1)  :: ("R2" , R2)  :: ("R3" , R3)  :: ("R4" , R4)
+  :: ("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)
@@ -141,8 +142,8 @@ Definition destroyed_by_op (op: operation): list mreg := nil.
   | Olongoffloat | Olonguoffloat | Olongofsingle | Olonguofsingle
       => F6 :: nil
   | _ => nil
-  end. *)
-
+  end.
+*)
 
 Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg := nil.
 
@@ -166,7 +167,7 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
-  (* | EF_memcpy sz al => R5 :: R6 :: R7 :: F0 :: nil *)
+(*| EF_memcpy sz al => R5 :: R6 :: R7 :: F0 :: nil *)
   | _ => nil
   end.
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 3d348655..e256661a 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -61,10 +61,7 @@ module Target : TARGET =
     let ireg oc r = output_string oc (int_reg_name r)
 
     let ireg0 = ireg
-(*
-    let ireg0 oc = function
-      | GPR r -> ireg oc r
-*)
+
     let preg oc = function
       | IR r -> ireg oc r
       | FR r -> ireg oc r
@@ -620,7 +617,7 @@ module Target : TARGET =
     let address = if Archi.ptr64 then ".quad" else ".long"
 
     let print_prologue oc =
-      (* fprintf oc "	.option %s\n" (if Archi.pic_code() then "pic" else "nopic"); *)
+   (* fprintf oc "	.option %s\n" (if Archi.pic_code() then "pic" else "nopic"); *)
       if !Clflags.option_g then begin
         section oc Section_text;
       end
diff --git a/test/mppa/simple.c b/test/mppa/simple.c
index 5a54b3d8..725aff68 100644
--- a/test/mppa/simple.c
+++ b/test/mppa/simple.c
@@ -1,6 +1,6 @@
 int main(void){
     int a = 4;
     int b = 3;
-    
+
     return (a+b);
 }