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.

1 files changed, 37 insertions, 11 deletions

diff --git a/ia32/CombineOpproof.v b/ia32/CombineOpproof.v
index 8f600054..f59e582b 100644
--- a/ia32/CombineOpproof.v
+++ b/ia32/CombineOpproof.v
@@ -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       *)
@@ -14,12 +14,8 @@
   during the [CSE] phase. *)
 
 Require Import Coqlib.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Op.
-Require Import RTL.
-Require Import CSEdomain.
+Require Import Integers Values Memory.
+Require Import Op RTL CSEdomain.
 Require Import CombineOp.
 
 Section COMBINE.
@@ -122,14 +118,36 @@ Proof.
   simpl; eapply combine_compimm_eq_1_sound; eauto.
 Qed.
 
+Theorem combine_addr_32_sound:
+  forall addr args addr' args',
+  combine_addr_32 get addr args = Some(addr', args') ->
+  eval_addressing32 ge sp addr' (map valu args') = eval_addressing32 ge sp addr (map valu args).
+Proof.
+  intros. functional inversion H; subst.
+  (* indexed - lea *)
+  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. 
+  eapply eval_offset_addressing_total_32; eauto.
+Qed.
+
+Theorem combine_addr_64_sound:
+  forall addr args addr' args',
+  combine_addr_64 get addr args = Some(addr', args') ->
+  eval_addressing64 ge sp addr' (map valu args') = eval_addressing64 ge sp addr (map valu args).
+Proof.
+  intros. functional inversion H; subst.
+  (* indexed - leal *)
+  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. 
+  eapply eval_offset_addressing_total_64; eauto.
+Qed.
+
 Theorem combine_addr_sound:
   forall addr args addr' args',
   combine_addr get addr args = Some(addr', args') ->
   eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
 Proof.
-  intros. functional inversion H; subst.
-  (* indexed - lea *)
-  UseGetSound. simpl. eapply eval_offset_addressing_total; eauto.
+  unfold combine_addr, eval_addressing; intros; destruct Archi.ptr64.
+  apply combine_addr_64_sound; auto.
+  apply combine_addr_32_sound; auto.
 Qed.
 
 Theorem combine_op_sound:
@@ -139,13 +157,21 @@ Theorem combine_op_sound:
 Proof.
   intros. functional inversion H; subst.
 (* lea-lea *)
-  simpl. eapply combine_addr_sound; eauto.
+  simpl. eapply combine_addr_32_sound; eauto.
+(* leal-leal *)
+  simpl. eapply combine_addr_64_sound; eauto.
 (* andimm - andimm *)
   UseGetSound; simpl. rewrite <- H0. rewrite Val.and_assoc. auto.
 (* orimm - orimm *)
   UseGetSound; simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
 (* xorimm - xorimm *)
   UseGetSound; simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
+(* andimm - andimm *)
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.andl_assoc. auto.
+(* orimm - orimm *)
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.orl_assoc. auto.
+(* xorimm - xorimm *)
+  UseGetSound; simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto.
 (* cmp *)
   simpl. decEq; decEq. eapply combine_cond_sound; eauto.
 Qed.