diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-02 16:17:51 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-02 16:17:51 +0200 |
commit | f21a6b181dded86ef0e5c7ab94f74e5b960fd510 (patch) | |
tree | 01bb7b59e438c60d12d87d869b6c890095a977f4 /ia32/SelectLong.vp | |
parent | a14b9578ee5297d954103e05d7b2d322816ddd8f (diff) | |
download | compcert-f21a6b181dded86ef0e5c7ab94f74e5b960fd510.tar.gz compcert-f21a6b181dded86ef0e5c7ab94f74e5b960fd510.zip |
Improve code generation for 64-bit signed integer division
Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port.
Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
Diffstat (limited to 'ia32/SelectLong.vp')
-rw-r--r-- | ia32/SelectLong.vp | 51 |
1 files changed, 12 insertions, 39 deletions
diff --git a/ia32/SelectLong.vp b/ia32/SelectLong.vp index c28777e8..32fd9aca 100644 --- a/ia32/SelectLong.vp +++ b/ia32/SelectLong.vp @@ -286,45 +286,18 @@ Nondetfunction mull (e1: expr) (e2: expr) := | _, _ => Eop Omull (e1:::e2:::Enil) end. -Definition divl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divl e1 e2 else - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.divs n1 n2) - | _, _ => Eop Odivl (e1:::e2:::Enil) - end. - -Definition modl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modl e1 e2 else - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.mods n1 n2) - | _, _ => Eop Omodl (e1:::e2:::Enil) - end. - -Definition divlu (e1 e2: expr) := - if Archi.splitlong then SplitLong.divlu e1 e2 else - let default := Eop Odivlu (e1:::e2:::Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.divu n1 n2) - | _, Some n2 => - match Int64.is_power2 n2 with - | Some l => shrluimm e1 (Int.repr (Int64.unsigned l)) - | None => default - end - | _, _ => default - end. - -Definition modlu (e1 e2: expr) := - if Archi.splitlong then SplitLong.modlu e1 e2 else - let default := Eop Omodlu (e1:::e2:::Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.modu n1 n2) - | _, Some n2 => - match Int64.is_power2 n2 with - | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) - | None => default - end - | _, _ => default - end. +Definition shrxlimm (e: expr) (n: int) := + if Archi.splitlong then SplitLong.shrxlimm e n else + if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil). + +Definition divlu_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil). +Definition modlu_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.modlu_base e1 e2 else Eop Omodu (e1:::e2:::Enil). +Definition divls_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil). +Definition modls_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.modls_base e1 e2 else Eop Omodl (e1:::e2:::Enil). Definition cmplu (c: comparison) (e1 e2: expr) := if Archi.splitlong then SplitLong.cmplu c e1 e2 else |