diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-09 16:05:42 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-13 16:19:24 +0200 |
| commit | 0ef341c554aff8d70f879411bb0918fb8349f2e4 (patch) | |
| tree | adb56368a81714afdd37e221c3d593d86f0ba5b2 /mppa_k1c/Asm.v | |
| parent | 9fd4e33a6dd2c2dc88103711af62a7214dbd4109 (diff) | |
| download | compcert-kvx-0ef341c554aff8d70f879411bb0918fb8349f2e4.tar.gz compcert-kvx-0ef341c554aff8d70f879411bb0918fb8349f2e4.zip | |
MPPA - Added optim for long unsigned cmp to 0.
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 72bbff69..bc8c07e4 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -226,6 +226,7 @@ Inductive instruction : Type := (* Conditional branches *) | Pcb (bt: btest) (r: ireg) (l: label) (**r branch based on btest *) + | Pcbu (bt: btest) (r: ireg) (l: label) (**r branch based on btest with unsigned semantics *) | Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte *) | Plbu (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte unsigned *) @@ -646,6 +647,15 @@ Definition cmp_for_btest (bt: btest) := | BTdgtz => (Some Cgt, Long) end. +Definition cmpu_for_btest (bt: btest) := + match bt with + | BTwnez => (Some Cne, Int) + | BTweqz => (Some Ceq, Int) + | BTdnez => (Some Cne, Long) + | BTdeqz => (Some Ceq, Long) + | _ => (None, Int) + end. + (** Comparing integers *) Definition compare_int (t: itest) (v1 v2: val) (m: mem): val := match t with @@ -796,6 +806,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | (Some c, Long) => eval_branch f l rs m (Val.cmpl_bool c rs###r (Vlong (Int64.repr 0))) | (None, _) => Stuck end + | Pcbu bt r l => + match cmpu_for_btest bt with + | (Some c, Int) => eval_branch f l rs m (Val.cmpu_bool (Mem.valid_pointer m) c rs##r (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch f l rs m (Val.cmplu_bool (Mem.valid_pointer m) c rs###r (Vlong (Int64.repr 0))) + | (None, _) => Stuck + end (* (** Conditional branches, 32-bit comparisons *) | Pbeqw s1 s2 l => |