diff options
author | Michael Schmidt <github@mschmidt.me> | 2017-12-05 14:48:18 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-12-05 14:48:18 +0100 |
commit | 90b76a0842b7f080893dd70a7c0c6bc878f4056b (patch) | |
tree | 277edd1eecf7bc7574a4b4dc3b925e3479dab8fd /riscV/ConstpropOp.vp | |
parent | 442e82e6ffc6958192f73382d2270e926ead9c80 (diff) | |
download | compcert-90b76a0842b7f080893dd70a7c0c6bc878f4056b.tar.gz compcert-90b76a0842b7f080893dd70a7c0c6bc878f4056b.zip |
Optimization for division by one during constant propagation (#39)
Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
Diffstat (limited to 'riscV/ConstpropOp.vp')
-rw-r--r-- | riscV/ConstpropOp.vp | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp index 37241816..76a1e8f8 100644 --- a/riscV/ConstpropOp.vp +++ b/riscV/ConstpropOp.vp @@ -128,18 +128,24 @@ Definition make_xorimm (n: int) (r: reg) := else (Oxorimm n, r :: nil). Definition make_divimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm n (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oshruimm l, r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => (Oshruimm l, r1 :: nil) + | None => (Odivu, r1 :: r2 :: nil) + end. Definition make_moduimm n (r1 r2: reg) := match Int.is_power2 n with |