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/SelectOp.vp | |
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/SelectOp.vp')
-rw-r--r-- | ia32/SelectOp.vp | 79 |
1 files changed, 43 insertions, 36 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index bc331b9c..db546d99 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -2,7 +2,7 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -38,33 +38,33 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats. +Require Import Op CminorSel. Open Local Scope cminorsel_scope. (** ** Constants **) -(** External oracle to determine whether a symbol is external and must - be addressed through [Oaddrsymbol], or is local and can be addressed - through [Olea Aglobal]. This is to accommodate MacOS X's limitations - on references to data symbols imported from shared libraries. *) +(** External oracle to determine whether a symbol should be addressed + through [Oindirectsymbol] or can be addressed via [Oleal Aglobal]. + This is to accommodate MacOS X's limitations on references to data + symbols imported from shared libraries. It can also help with PIC + code under ELF. *) Parameter symbol_is_external: ident -> bool. -Definition addrsymbol (id: ident) (ofs: int) := +Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. + +Definition addrsymbol (id: ident) (ofs: ptrofs) := if symbol_is_external id then - if Int.eq ofs Int.zero + if Ptrofs.eq ofs Ptrofs.zero then Eop (Oindirectsymbol id) Enil - else Eop (Olea (Aindexed ofs)) (Eop (Oindirectsymbol id) Enil ::: Enil) + else Eop (Olea_ptr (Aindexed (Ptrofs.unsigned ofs))) (Eop (Oindirectsymbol id) Enil ::: Enil) else - Eop (Olea (Aglobal id ofs)) Enil. + Eop (Olea_ptr (Aglobal id ofs)) Enil. -Definition addrstack (ofs: int) := - Eop (Olea (Ainstack ofs)) Enil. +Definition addrstack (ofs: ptrofs) := + Eop (Olea_ptr (Ainstack ofs)) Enil. (** ** Integer logical negation *) @@ -81,8 +81,8 @@ Nondetfunction addimm (n: int) (e: expr) := if Int.eq n Int.zero then e else match e with | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Olea addr) args => Eop (Olea (offset_addressing_total addr n)) args - | _ => Eop (Olea (Aindexed n)) (e ::: Enil) + | Eop (Olea addr) args => Eop (Olea (offset_addressing_total addr (Int.signed n))) args + | _ => Eop (Olea (Aindexed (Int.signed n))) (e ::: Enil) end. Nondetfunction add (e1: expr) (e2: expr) := @@ -90,19 +90,19 @@ Nondetfunction add (e1: expr) (e2: expr) := | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 | t1, Eop (Ointconst n2) Enil => addimm n2 t1 | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => - Eop (Olea (Aindexed2 (Int.add n1 n2))) (t1:::t2:::Enil) + Eop (Olea (Aindexed2 (n1 + n2))) (t1:::t2:::Enil) | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) => - Eop (Olea (Aindexed2scaled sc (Int.add n1 n2))) (t1:::t2:::Enil) + Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil) | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => - Eop (Olea (Aindexed2scaled sc (Int.add n1 n2))) (t2:::t1:::Enil) + Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil) | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => - Eop (Olea (Abased id (Int.add ofs n1))) (t1:::Enil) + Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil) | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) => - Eop (Olea (Abased id (Int.add ofs n2))) (t2:::Enil) + Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil) | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => - Eop (Olea (Abasedscaled sc id (Int.add ofs n1))) (t1:::Enil) + Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil) | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) => - Eop (Olea (Abasedscaled sc id (Int.add ofs n2))) (t2:::Enil) + Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil) | Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 => Eop (Olea (Aindexed2scaled sc n)) (t2:::t1:::Enil) | t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) => @@ -112,7 +112,7 @@ Nondetfunction add (e1: expr) (e2: expr) := | t1, Eop (Olea (Aindexed n)) (t2:::Enil) => Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil) | _, _ => - Eop (Olea (Aindexed2 Int.zero)) (e1:::e2:::Enil) + Eop (Olea (Aindexed2 0)) (e1:::e2:::Enil) end. (** ** Opposite *) @@ -129,11 +129,11 @@ Nondetfunction sub (e1: expr) (e2: expr) := match e1, e2 with | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1 | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => - addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil)) + addimm (Int.repr (n1 - n2)) (Eop Osub (t1:::t2:::Enil)) | Eop (Olea (Aindexed n1)) (t1:::Enil), t2 => - addimm n1 (Eop Osub (t1:::t2:::Enil)) + addimm (Int.repr n1) (Eop Osub (t1:::t2:::Enil)) | t1, Eop (Olea (Aindexed n2)) (t2:::Enil) => - addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) + addimm (Int.repr (-n2)) (Eop Osub (t1:::t2:::Enil)) | _, _ => Eop Osub (e1:::e2:::Enil) end. @@ -157,11 +157,12 @@ Nondetfunction shlimm (e1: expr) (n: int) := else Eop (Oshlimm n) (e1:::Enil) | Eop (Olea (Aindexed n1)) (t1:::Enil) => if shift_is_scale n - then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil) + then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) + (Int.unsigned (Int.shl (Int.repr n1) n)))) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil) | _ => if shift_is_scale n - then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil) + then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) 0)) (e1:::Enil) else Eop (Oshlimm n) (e1:::Enil) end. @@ -214,7 +215,7 @@ Nondetfunction mulimm (n1: int) (e2: expr) := else if Int.eq n1 Int.one then e2 else match e2 with | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil - | Eop (Olea (Aindexed n2)) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2) + | Eop (Olea (Aindexed n2)) (t2:::Enil) => addimm (Int.mul n1 (Int.repr n2)) (mulimm_base n1 t2) | _ => mulimm_base n1 e2 end. @@ -503,8 +504,11 @@ Nondetfunction singleofintu (e: expr) := Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with - | Eop (Olea addr) args => (addr, args) - | _ => (Aindexed Int.zero, e:::Enil) + | Eop (Olea addr) args => + if (negb Archi.ptr64) && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil) + | Eop (Oleal addr) args => + if Archi.ptr64 && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil) + | _ => (Aindexed 0, e:::Enil) end. (** ** Arguments of builtins *) @@ -512,8 +516,11 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := Nondetfunction builtin_arg (e: expr) := match e with | Eop (Ointconst n) Enil => BA_int n - | Eop (Olea (Aglobal id ofs)) Enil => BA_addrglobal id ofs - | Eop (Olea (Ainstack ofs)) Enil => BA_addrstack ofs + | Eop (Olongconst n) Enil => BA_long n + | Eop (Olea (Aglobal id ofs)) Enil => if Archi.ptr64 then BA e else BA_addrglobal id ofs + | Eop (Olea (Ainstack ofs)) Enil => if Archi.ptr64 then BA e else BA_addrstack ofs + | Eop (Oleal (Aglobal id ofs)) Enil => if Archi.ptr64 then BA_addrglobal id ofs else BA e + | Eop (Oleal (Ainstack ofs)) Enil => if Archi.ptr64 then BA_addrstack ofs else BA e | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => BA_long (Int64.ofwords h l) | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l) |