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, 41 insertions, 8 deletions

diff --git a/ia32/CombineOp.v b/ia32/CombineOp.v
index cdd16071..34c1c9cc 100644
--- a/ia32/CombineOp.v
+++ b/ia32/CombineOp.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,10 +14,8 @@
   during the [CSE] phase. *)
 
 Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Op.
-Require Import CSEdomain.
+Require Import AST Integers.
+Require Import Op CSEdomain.
 
 Definition valnum := positive.
 
@@ -72,23 +70,43 @@ Function combine_cond (cond: condition) (args: list valnum) : option(condition *
   | _, _ => None
   end.
 
-Function combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+Function combine_addr_32 (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
   match addr, args with
   | Aindexed n, x::nil =>
       match get x with
-      | Some(Op (Olea a) ys) => Some(offset_addressing_total a n, ys)
+      | Some(Op (Olea a) ys) =>
+          match offset_addressing a n with Some a' => Some (a', ys) | None => None end
       | _ => None
       end
   | _, _ => None
   end.
 
+Function combine_addr_64 (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  match addr, args with
+  | Aindexed n, x::nil =>
+      match get x with
+      | Some(Op (Oleal a) ys) =>
+          match offset_addressing a n with Some a' => Some (a', ys) | None => None end
+      | _ => None
+      end
+  | _, _ => None
+  end.
+
+Definition combine_addr (addr: addressing) (args: list valnum) : option(addressing * list valnum) :=
+  if Archi.ptr64 then combine_addr_64 addr args else combine_addr_32 addr args.
+
 Function combine_op (op: operation) (args: list valnum) : option(operation * list valnum) :=
   match op, args with
   | Olea addr, _ =>
-      match combine_addr addr args with
+      match combine_addr_32 addr args with
       | Some(addr', args') => Some(Olea addr', args')
       | None => None
       end
+  | Oleal addr, _ =>
+      match combine_addr_64 addr args with
+      | Some(addr', args') => Some(Oleal addr', args')
+      | None => None
+      end
   | Oandimm n, x :: nil =>
       match get x with
       | Some(Op (Oandimm m) ys) => Some(Oandimm (Int.and m n), ys)
@@ -104,6 +122,21 @@ Function combine_op (op: operation) (args: list valnum) : option(operation * lis
       | Some(Op (Oxorimm m) ys) => Some(Oxorimm (Int.xor m n), ys)
       | _ => None
       end
+  | Oandlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oandlimm m) ys) => Some(Oandlimm (Int64.and m n), ys)
+      | _ => None
+      end
+  | Oorlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oorlimm m) ys) => Some(Oorlimm (Int64.or m n), ys)
+      | _ => None
+      end
+  | Oxorlimm n, x :: nil =>
+      match get x with
+      | Some(Op (Oxorlimm m) ys) => Some(Oxorlimm (Int64.xor m n), ys)
+      | _ => None
+      end
   | Ocmp cond, _ =>
       match combine_cond cond args with
       | Some(cond', args') => Some(Ocmp cond', args')