aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/NeedOp.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-10-04 15:52:16 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-10-04 15:52:16 +0200
commitd2af79a77ed2936ff0ed90cadf8e48637d774d4c (patch)
tree09300943e12a98ae80598c79d455b31725271ead /ia32/NeedOp.v
parenta44893028eb1dd434c68001234ad56d030205a8e (diff)
downloadcompcert-d2af79a77ed2936ff0ed90cadf8e48637d774d4c.tar.gz
compcert-d2af79a77ed2936ff0ed90cadf8e48637d774d4c.zip
Turn 64-bit integer division and modulus by constants into multiply-high
This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
Diffstat (limited to 'ia32/NeedOp.v')
-rw-r--r--ia32/NeedOp.v5
1 files changed, 1 insertions, 4 deletions
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v
index 575532b1..09013cdd 100644
--- a/ia32/NeedOp.v
+++ b/ia32/NeedOp.v
@@ -95,10 +95,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Osubl => op2 (default nv)
| Omull => op2 (default nv)
| Omullimm _ => op1 (default nv)
- | Odivl => op2 (default nv)
- | Odivlu => op2 (default nv)
- | Omodl => op2 (default nv)
- | Omodlu => op2 (default nv)
+ | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv)
| Oandl => op2 (default nv)
| Oandlimm _ => op1 (default nv)
| Oorl => op2 (default nv)