From a14b9578ee5297d954103e05d7b2d322816ddd8f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:38:24 +0200 Subject: 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. --- ia32/Archi.v | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'ia32/Archi.v') 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. -- cgit