diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:25:18 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:25:18 +0200 |
| commit | e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (patch) | |
| tree | 518d558674d3e1c6ff41c46d84c784e727ed5d04 /backend/SelectDivproof.v | |
| parent | ad2a2c862abef3aee701d1bca0524fcbf2d07b30 (diff) | |
| download | compcert-kvx-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.tar.gz compcert-kvx-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.zip | |
Support for 64-bit architectures: generic support
- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.
Diffstat (limited to 'backend/SelectDivproof.v')
| -rw-r--r-- | backend/SelectDivproof.v | 45 |
1 files changed, 18 insertions, 27 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index ffe607e4..5621acd5 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -12,21 +12,10 @@ (** Correctness of instruction selection for integer division *) -Require Import Coqlib. -Require Import Zquot. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. -Require Import SelectOp. -Require Import SelectOpproof. -Require Import SelectDiv. +Require Import Zquot Coqlib. +Require Import AST Integers Floats Values Memory Globalenvs Events. +Require Import Cminor Op CminorSel. +Require Import SelectOp SelectOpproof SelectDiv. Open Local Scope cminorsel_scope. @@ -191,18 +180,19 @@ Lemma divs_mul_params_sound: Int.min_signed <= n <= Int.max_signed -> Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). Proof with (try discriminate). - unfold divs_mul_params; intros d m' p' EQ. + unfold divs_mul_params; intros d m' p'. destruct (find_div_mul_params Int.wordsize (Int.half_modulus - Int.half_modulus mod d - 1) d 32) as [[p m] | ]... + generalize (p - 32). intro p1. destruct (zlt 0 d)... - destruct (zlt (two_p (32 + p)) (m * d))... - destruct (zle (m * d) (two_p (32 + p) + two_p (p + 1)))... + destruct (zlt (two_p (32 + p1)) (m * d))... + destruct (zle (m * d) (two_p (32 + p1) + two_p (p1 + 1)))... destruct (zle 0 m)... destruct (zlt m Int.modulus)... - destruct (zle 0 p)... - destruct (zlt p 32)... - simpl in EQ. inv EQ. + destruct (zle 0 p1)... + destruct (zlt p1 32)... + intros EQ; inv EQ. split. auto. split. auto. intros. replace (32 + p') with (31 + (p' + 1)) by omega. apply Zquot_mul; try omega. @@ -219,18 +209,19 @@ Lemma divu_mul_params_sound: 0 <= n < Int.modulus -> Zdiv n d = Zdiv (m * n) (two_p (32 + p)). Proof with (try discriminate). - unfold divu_mul_params; intros d m' p' EQ. + unfold divu_mul_params; intros d m' p'. destruct (find_div_mul_params Int.wordsize (Int.modulus - Int.modulus mod d - 1) d 32) as [[p m] | ]... + generalize (p - 32); intro p1. destruct (zlt 0 d)... - destruct (zle (two_p (32 + p)) (m * d))... - destruct (zle (m * d) (two_p (32 + p) + two_p p))... + destruct (zle (two_p (32 + p1)) (m * d))... + destruct (zle (m * d) (two_p (32 + p1) + two_p p1))... destruct (zle 0 m)... destruct (zlt m Int.modulus)... - destruct (zle 0 p)... - destruct (zlt p 32)... - simpl in EQ. inv EQ. + destruct (zle 0 p1)... + destruct (zlt p1 32)... + intros EQ; inv EQ. split. auto. split. auto. intros. apply Zdiv_mul_pos; try omega. assumption. Qed. |