aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/Machregs.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-10-02 16:17:51 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-10-02 16:17:51 +0200
commitf21a6b181dded86ef0e5c7ab94f74e5b960fd510 (patch)
tree01bb7b59e438c60d12d87d869b6c890095a977f4 /ia32/Machregs.v
parenta14b9578ee5297d954103e05d7b2d322816ddd8f (diff)
downloadcompcert-kvx-f21a6b181dded86ef0e5c7ab94f74e5b960fd510.tar.gz
compcert-kvx-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/Machregs.v')
-rw-r--r--ia32/Machregs.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 34d88328..a9383d18 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -137,6 +137,7 @@ Definition destroyed_by_op (op: operation): list mreg :=
| Odivlu => AX :: DX :: nil
| Omodl => AX :: DX :: nil
| Omodlu => AX :: DX :: nil
+ | Oshrxlimm _ => DX :: nil
| Ocmp _ => AX :: CX :: nil
| _ => nil
end.
@@ -217,6 +218,7 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
| Oshll => (None :: Some CX :: nil, None)
| Oshrl => (None :: Some CX :: nil, None)
| Oshrlu => (None :: Some CX :: nil, None)
+ | Oshrxlimm _ => (Some AX :: nil, Some AX)
| _ => (nil, None)
end.
@@ -313,6 +315,7 @@ Definition two_address_op (op: operation) : bool :=
| Oshllimm _ => true
| Oshrl => true
| Oshrlimm _ => true
+ | Oshrxlimm _ => false
| Oshrlu => true
| Oshrluimm _ => true
| Ororlimm _ => true