diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 10:31:56 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 10:31:56 +0200 |
| commit | aa25ec270b651186154523ec71a3888b50994d70 (patch) | |
| tree | a4572adf5cde4f97642885cb1f90f73a20d169cd /mppa_k1c/Asmgen.v | |
| parent | 41a048fa4bb9ddefd4e4acff2207251bb3ddbf06 (diff) | |
| download | compcert-kvx-aa25ec270b651186154523ec71a3888b50994d70.tar.gz compcert-kvx-aa25ec270b651186154523ec71a3888b50994d70.zip | |
MPPA - Oshrximm + Mgetparam + FP is GPR10 + bug
Added Oshrximm and Mgetparam -> mmult.c divide & conqueer generates
FP is now GPR10 instead of being a mix of GPR30 and GPR32
Corrected a bug where Pgoto and Pj_l were given the same interpretation,
where in fact there's a fundamental difference : Pgoto is supposed to
have a function name (symbol), while Pj_l is supposed to have a label
name (print_label). This led to having undefinite labels in the code.
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 675cb065..8198fa78 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -346,7 +346,7 @@ Definition transl_op | Oshruimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psrliw rd rs n :: k) -(*| Oshrximm n, a1 :: nil => + | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs :: k else Psraiw GPR31 rs (Int.repr 31) :: @@ -355,7 +355,7 @@ Definition transl_op Psraiw rd GPR31 n :: k) (* [Omakelong], [Ohighlong] should not occur *) -*)| Olowlong, a1 :: nil => + | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pcvtl2w rd rs :: k) | Ocast32signed, a1 :: nil => @@ -675,12 +675,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) loadind SP ofs ty dst k | Msetstack src ofs ty => storeind src SP ofs ty k -(*| Mgetparam ofs ty dst => + | Mgetparam ofs ty dst => (* load via the frame pointer if it is valid *) - do c <- loadind GPR30 ofs ty dst k; + do c <- loadind FP ofs ty dst k; OK (if ep then c - else loadind_ptr SP f.(fn_link_ofs) GPR30 c) -*)| Mop op args res => + else loadind_ptr SP f.(fn_link_ofs) FP c) + | Mop op args res => transl_op op args res k | Mload chunk addr args dst => transl_load chunk addr args dst k @@ -716,8 +716,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := match i with | Msetstack src ofs ty => before - | Mgetparam ofs ty dst => negb (mreg_eq dst R32) - | Mop op args res => before && negb (mreg_eq res R32) + | Mgetparam ofs ty dst => negb (mreg_eq dst R10) + | Mop op args res => before && negb (mreg_eq res R10) | _ => false end. |