diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-19 13:32:09 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-19 13:32:09 +0000 |
| commit | ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67 (patch) | |
| tree | 7bd176bb0dbf60617954fabadd8aedc64b4cf647 /powerpc/SelectOp.v | |
| parent | cdf83055d96e2af784a97c783c94b83ba2032ae1 (diff) | |
| download | compcert-ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67.tar.gz compcert-ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67.zip | |
Revised lib/Integers.v to make it parametric w.r.t. word size.
Introduced Int.iwordsize and used it in place of "Int.repr 32" or
"Int.repr (Z_of_nat wordsize)".
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/SelectOp.v')
| -rw-r--r-- | powerpc/SelectOp.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index ef55b8bb..40201e77 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -396,7 +396,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) := | rolm_case1 n1 => Eop (Ointconst(Int.and (Int.rol n1 amount2) mask2)) Enil | rolm_case2 amount1 mask1 t1 => - let amount := Int.and (Int.add amount1 amount2) (Int.repr 31) in + let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in let mask := Int.and (Int.rol mask1 amount2) mask2 in if Int.is_rlw_mask mask then Eop (Orolm amount mask) (t1:::Enil) @@ -408,7 +408,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) := Definition shlimm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 - else if Int.ltu n2 (Int.repr 32) then + else if Int.ltu n2 Int.iwordsize then rolm e1 n2 (Int.shl Int.mone n2) else Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil). @@ -416,8 +416,8 @@ Definition shlimm (e1: expr) (n2: int) := Definition shruimm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 - else if Int.ltu n2 (Int.repr 32) then - rolm e1 (Int.sub (Int.repr 32) n2) (Int.shru Int.mone n2) + else if Int.ltu n2 Int.iwordsize then + rolm e1 (Int.sub Int.iwordsize n2) (Int.shru Int.mone n2) else Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil). |