diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-07-05 12:20:18 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-07-05 12:23:42 +0200 |
| commit | 92fc8a425034abc1247203a4c0d471e8b6d0e941 (patch) | |
| tree | e5fb2b099e1cab906b2a72adf54a2c0e1148f062 /powerpc/ConstpropOp.vp | |
| parent | 1971ab6cd3aff8939edd0e1ca9779b4b44bcc88e (diff) | |
| download | compcert-kvx-92fc8a425034abc1247203a4c0d471e8b6d0e941.tar.gz compcert-kvx-92fc8a425034abc1247203a4c0d471e8b6d0e941.zip | |
Issue #16P: wrong rlwinm instruction generated by constant propagation
This happens when the divisor of an unsigned int32 division is constant-propagated to 1.
Diffstat (limited to 'powerpc/ConstpropOp.vp')
| -rw-r--r-- | powerpc/ConstpropOp.vp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 8946ae27..886655a0 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -92,11 +92,15 @@ Definition make_shrimm (n: int) (r1 r2: reg) := else (Oshr, r1 :: r2 :: nil). -Definition make_shruimm (n: int) (r1 r2: reg) := +Definition make_shruimm_aux (n: int) (r1: reg) := if Int.eq n Int.zero then (Omove, r1 :: nil) - else if Int.ltu n Int.iwordsize then - (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r1 :: nil) + else + (Orolm (Int.sub Int.iwordsize n) (Int.shru Int.mone n), r1 :: nil). + +Definition make_shruimm (n: int) (r1 r2: reg) := + if Int.ltu n Int.iwordsize then + make_shruimm_aux n r1 else (Oshru, r1 :: r2 :: nil). @@ -121,7 +125,7 @@ Definition make_divimm (n: int) (r1 r2: reg) := Definition make_divuimm (n: int) (r1 r2: reg) := match Int.is_power2 n with - | Some l => (Orolm (Int.sub Int.iwordsize l) (Int.shru Int.mone l), r1 :: nil) + | Some l => make_shruimm_aux l r1 | None => (Odivu, r1 :: r2 :: nil) end. |