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/Archi.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/Archi.v')
| -rw-r--r-- | ia32/Archi.v | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/ia32/Archi.v b/ia32/Archi.v index ded460d2..936bacb3 100644 --- a/ia32/Archi.v +++ b/ia32/Archi.v @@ -2,8 +2,8 @@ (* *) (* The Compcert verified compiler *) (* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* Xavier Leroy, INRIA Paris *) +(* Jacques-Henri Jourdan, INRIA Paris *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -20,10 +20,19 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. +Parameter ptr64: bool. + Definition big_endian := false. -Notation align_int64 := 4%Z (only parsing). -Notation align_float64 := 4%Z (only parsing). +Definition align_int64 := if ptr64 then 8%Z else 4%Z. +Definition align_float64 := if ptr64 then 8%Z else 4%Z. + +Definition splitlong := negb ptr64. + +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. + unfold splitlong. destruct ptr64; simpl; congruence. +Qed. Program Definition default_pl_64 : bool * nan_pl 53 := (true, iter_nat 51 _ xO xH). @@ -39,7 +48,7 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := false. -Global Opaque big_endian +Global Opaque ptr64 big_endian splitlong default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. |