From 348aa9268bb3f7f2fe4357586a4e1d3181e0c9b3 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 16 Mar 2018 15:06:28 +0100 Subject: MPPA - code cleaning --- mppa_k1c/Asm.v | 45 ++++++++++++++++----------------------------- mppa_k1c/Asmexpand.ml | 2 +- mppa_k1c/Asmgen.v | 45 ++++----------------------------------------- mppa_k1c/Asmgenproof.v | 16 +++++++++------- mppa_k1c/Asmgenproof1.v | 18 +++++++++--------- mppa_k1c/Conventions1.v | 9 ++++++--- mppa_k1c/Machregs.v | 35 ++++++++++++++++++----------------- mppa_k1c/TargetPrinter.ml | 7 ++----- test/mppa/simple.c | 2 +- 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); } -- cgit