diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:38:24 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:38:24 +0200 |
commit | a14b9578ee5297d954103e05d7b2d322816ddd8f (patch) | |
tree | 93b7c2b6bd7de8a4dedaf399088257e0660959b8 /ia32/NeedOp.v | |
parent | 3bef0962079cf971673b4267b0142bd5fe092509 (diff) | |
download | compcert-a14b9578ee5297d954103e05d7b2d322816ddd8f.tar.gz compcert-a14b9578ee5297d954103e05d7b2d322816ddd8f.zip |
Support for 64-bit architectures: x86 in 64-bit mode
This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.
To activate x86-64 bit support, configure with "x86_64-linux".
Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode
To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
(currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.
Diffstat (limited to 'ia32/NeedOp.v')
-rw-r--r-- | ia32/NeedOp.v | 116 |
1 files changed, 89 insertions, 27 deletions
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v index 07eec160..9a75cba8 100644 --- a/ia32/NeedOp.v +++ b/ia32/NeedOp.v @@ -1,15 +1,20 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Neededness analysis for x86_64 operators *) + Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Op. -Require Import NeedDomain. -Require Import RTL. - -(** Neededness analysis for IA32 operators *) +Require Import AST Integers Floats Values Memory Globalenvs. +Require Import Op NeedDomain RTL. Definition op1 (nv: nval) := nv :: nil. Definition op2 (nv: nval) := nv :: nv :: nil. @@ -20,7 +25,7 @@ Definition needs_of_condition (cond: condition): list nval := | _ => nil end. -Definition needs_of_addressing (addr: addressing) (nv: nval): list nval := +Definition needs_of_addressing_32 (addr: addressing) (nv: nval): list nval := match addr with | Aindexed n => op1 (modarith nv) | Aindexed2 n => op2 (modarith nv) @@ -32,10 +37,26 @@ Definition needs_of_addressing (addr: addressing) (nv: nval): list nval := | Ainstack ofs => nil end. +Definition needs_of_addressing_64 (addr: addressing) (nv: nval): list nval := + match addr with + | Aindexed n => op1 (default nv) + | Aindexed2 n => op2 (default nv) + | Ascaled sc ofs => op1 (default nv) + | Aindexed2scaled sc ofs => op2 (default nv) + | Aglobal s ofs => nil + | Abased s ofs => op1 (default nv) + | Abasedscaled sc s ofs => op1 (default nv) + | Ainstack ofs => nil + end. + +Definition needs_of_addressing (addr: addressing) (nv: nval): list nval := + if Archi.ptr64 then needs_of_addressing_64 addr nv else needs_of_addressing_32 addr nv. + Definition needs_of_operation (op: operation) (nv: nval): list nval := match op with | Omove => op1 nv | Ointconst n => nil + | Olongconst n => nil | Ofloatconst n => nil | Osingleconst n => nil | Oindirectsymbol id => nil @@ -64,15 +85,42 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshruimm n => op1 (shruimm nv n) | Ororimm n => op1 (ror nv n) | Oshldimm n => op1 (default nv) - | Olea addr => needs_of_addressing addr nv + | Olea addr => needs_of_addressing_32 addr nv + | Omakelong => op2 (default nv) + | Olowlong | Ohighlong => op1 (default nv) + | Ocast32signed => op1 (default nv) + | Ocast32unsigned => op1 (default nv) + | Onegl => op1 (default nv) + | Oaddlimm _ => op1 (default nv) + | 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) + | Oandl => op2 (default nv) + | Oandlimm _ => op1 (default nv) + | Oorl => op2 (default nv) + | Oorlimm _ => op1 (default nv) + | Oxorl => op2 (default nv) + | Oxorlimm _ => op1 (default nv) + | Onotl => op1 (default nv) + | Oshll => op2 (default nv) + | Oshllimm _ => op1 (default nv) + | Oshrl => op2 (default nv) + | Oshrlimm _ => op1 (default nv) + | Oshrlu => op2 (default nv) + | Oshrluimm _ => op1 (default nv) + | Ororlimm _ => op1 (default nv) + | Oleal addr => needs_of_addressing_64 addr nv | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) | Ointoffloat | Ofloatofint | Ointofsingle | Osingleofint => op1 (default nv) - | Omakelong => op2 (default nv) - | Olowlong | Ohighlong => op1 (default nv) + | Olongoffloat | Ofloatoflong | Olongofsingle | Osingleoflong => op1 (default nv) | Ocmp c => needs_of_condition c end. @@ -117,19 +165,19 @@ Proof. try (eapply default_needs_of_condition_sound; eauto; fail); simpl in *; FuncInv; InvAgree. - eapply maskzero_sound; eauto. -- destruct (Val.maskzero_bool v i) as [b'|] eqn:MZ; try discriminate. +- destruct (Val.maskzero_bool v n) as [b'|] eqn:MZ; try discriminate. erewrite maskzero_sound; eauto. Qed. -Lemma needs_of_addressing_sound: - forall (ge: genv) sp addr args v nv args', - eval_addressing ge (Vptr sp Int.zero) addr args = Some v -> - vagree_list args args' (needs_of_addressing addr nv) -> +Lemma needs_of_addressing_32_sound: + forall sp addr args v nv args', + eval_addressing32 ge (Vptr sp Ptrofs.zero) addr args = Some v -> + vagree_list args args' (needs_of_addressing_32 addr nv) -> exists v', - eval_addressing ge (Vptr sp Int.zero) addr args' = Some v' + eval_addressing32 ge (Vptr sp Ptrofs.zero) addr args' = Some v' /\ vagree v v' nv. Proof. - unfold needs_of_addressing; intros. + unfold needs_of_addressing_32; intros. destruct addr; simpl in *; FuncInv; InvAgree; TrivialExists; auto using add_sound, mul_sound with na. apply add_sound; auto with na. apply add_sound; rewrite modarith_idem; auto. @@ -137,13 +185,23 @@ Proof. apply mul_sound; rewrite modarith_idem; auto with na. Qed. +(* +Lemma needs_of_addressing_64_sound: + forall sp addr args v nv args', + eval_addressing64 ge (Vptr sp Ptrofs.zero) addr args = Some v -> + vagree_list args args' (needs_of_addressing_64 addr nv) -> + exists v', + eval_addressing64 ge (Vptr sp Ptrofs.zero) addr args' = Some v' + /\ vagree v v' nv. +*) + Lemma needs_of_operation_sound: forall op args v nv args', - eval_operation ge (Vptr sp Int.zero) op args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> vagree_list args args' (needs_of_operation op nv) -> nv <> Nothing -> exists v', - eval_operation ge (Vptr sp Int.zero) op args' m' = Some v' + eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v' /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); @@ -166,8 +224,12 @@ Proof. - apply shrimm_sound; auto. - apply shruimm_sound; auto. - apply ror_sound; auto. -- eapply needs_of_addressing_sound; eauto. -- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. +- eapply needs_of_addressing_32_sound; eauto. +- change (eval_addressing64 ge (Vptr sp Ptrofs.zero) a args') + with (eval_operation ge (Vptr sp Ptrofs.zero) (Oleal a) args' m'). + eapply default_needs_of_operation_sound; eauto. + destruct a; simpl in H0; auto. +- destruct (eval_condition cond args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na. subst v; auto with na. @@ -176,7 +238,7 @@ Qed. Lemma operation_is_redundant_sound: forall op nv arg1 args v arg1' args', operation_is_redundant op nv = true -> - eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v -> vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. |