diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-04 15:52:16 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-04 15:52:16 +0200 |
| commit | d2af79a77ed2936ff0ed90cadf8e48637d774d4c (patch) | |
| tree | 09300943e12a98ae80598c79d455b31725271ead /ia32/Op.v | |
| parent | a44893028eb1dd434c68001234ad56d030205a8e (diff) | |
| download | compcert-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/Op.v')
| -rw-r--r-- | ia32/Op.v | 10 |
1 files changed, 10 insertions, 0 deletions
@@ -120,6 +120,8 @@ Inductive operation : Type := | Osubl (**r [rd = r1 - r2] *) | Omull (**r [rd = r1 * r2] *) | Omullimm (n: int64) (**r [rd = r1 * n] *) + | Omullhs (**r [rd = high part of r1 * r2, signed] *) + | Omullhu (**r [rd = high part of r1 * r2, unsigned] *) | Odivl (**r [rd = r1 / r2] (signed) *) | Odivlu (**r [rd = r1 / r2] (unsigned) *) | Omodl (**r [rd = r1 % r2] (signed) *) @@ -339,6 +341,8 @@ Definition eval_operation | Osubl, v1::v2::nil => Some (Val.subl v1 v2) | Omull, v1::v2::nil => Some (Val.mull v1 v2) | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) + | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) + | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2) | Odivl, v1::v2::nil => Val.divls v1 v2 | Odivlu, v1::v2::nil => Val.divlu v1 v2 | Omodl, v1::v2::nil => Val.modls v1 v2 @@ -508,6 +512,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubl => (Tlong :: Tlong :: nil, Tlong) | Omull => (Tlong :: Tlong :: nil, Tlong) | Omullimm _ => (Tlong :: nil, Tlong) + | Omullhs => (Tlong :: Tlong :: nil, Tlong) + | Omullhu => (Tlong :: Tlong :: nil, Tlong) | Odivl => (Tlong :: Tlong :: nil, Tlong) | Odivlu => (Tlong :: Tlong :: nil, Tlong) | Omodl => (Tlong :: Tlong :: nil, Tlong) @@ -666,6 +672,8 @@ Proof with (try exact I). unfold Val.has_type; destruct Archi.ptr64; simpl; auto. destruct (eq_block b b0); auto. destruct v0; destruct v1... destruct v0... + destruct v0; destruct v1... + destruct v0; destruct v1... destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2... destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2... @@ -1210,6 +1218,8 @@ Proof. apply Val.subl_inject; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. inv H4; inv H3; simpl in H1; inv H1. simpl. destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists. inv H4; inv H3; simpl in H1; inv H1. simpl. |