aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/SelectLong.vp
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-10-25 17:27:48 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-10-25 17:27:48 +0200
commitfc8f28be257464c7b169a61b079ba19675f08e35 (patch)
tree05535928e3d87e0741c9c81026aea1dc72e09473 /ia32/SelectLong.vp
parent65ab86a0e3df080ca9a1c37631904d8d02c07596 (diff)
downloadcompcert-fc8f28be257464c7b169a61b079ba19675f08e35.tar.gz
compcert-fc8f28be257464c7b169a61b079ba19675f08e35.zip
x86-32: make sure is_longconst and mullimm work correctly in 32 bits
SelectLong.is_longconst was always returning 'false' in 32 bits. SelectLong.mullimm was generating a Omullimm insn even in 32 bits. Both functions are used by SelectDiv.
Diffstat (limited to 'ia32/SelectLong.vp')
-rw-r--r--ia32/SelectLong.vp4
1 files changed, 3 insertions, 1 deletions
diff --git a/ia32/SelectLong.vp b/ia32/SelectLong.vp
index 2869f823..b213e23f 100644
--- a/ia32/SelectLong.vp
+++ b/ia32/SelectLong.vp
@@ -29,6 +29,7 @@ Definition longconst (n: int64) : expr :=
if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil.
Definition is_longconst (e: expr) :=
+ if Archi.splitlong then SplitLong.is_longconst e else
match e with
| Eop (Olongconst n) Enil => Some n
| _ => None
@@ -269,7 +270,8 @@ Definition mullimm_base (n1: int64) (e2: expr) :=
end.
Nondetfunction mullimm (n1: int64) (e2: expr) :=
- if Int64.eq n1 Int64.zero then longconst Int64.zero
+ if Archi.splitlong then SplitLong.mullimm n1 e2
+ else if Int64.eq n1 Int64.zero then longconst Int64.zero
else if Int64.eq n1 Int64.one then e2
else match e2 with
| Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2)