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, 38 insertions, 32 deletions

diff --git a/ia32/Stacklayout.v b/ia32/Stacklayout.v
index f19f036c..44fd43b2 100644
--- a/ia32/Stacklayout.v
+++ b/ia32/Stacklayout.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       *)
@@ -13,9 +13,11 @@
 (** Machine- and ABI-dependent layout information for activation records. *)
 
 Require Import Coqlib.
-Require Import Memory Separation.
+Require Import AST Memory Separation.
 Require Import Bounds.
 
+Local Open Scope sep_scope.
+
 (** The general shape of activation records is as follows,
   from bottom (lowest offsets) to top:
 - Space for outgoing arguments to function calls.
@@ -29,16 +31,14 @@ Require Import Bounds.
 
 Definition fe_ofs_arg := 0.
 
-(** Computation of the frame environment from the bounds of the current
-  function. *)
-
 Definition make_env (b: bounds) : frame_env :=
-  let olink := 4 * b.(bound_outgoing) in  (* back link *)
-  let ocs := olink + 4 in                 (* callee-saves *)
+  let w := if Archi.ptr64 then 8 else 4 in
+  let olink := align (4 * b.(bound_outgoing)) w in  (* back link *)
+  let ocs := olink + w in                           (* callee-saves *)
   let ol :=  align (size_callee_save_area b ocs) 8 in (* locals *)
   let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *)
-  let oretaddr := align (ostkdata + b.(bound_stack_data)) 4 in (* return address *)
-  let sz := oretaddr + 4 in (* total size *)
+  let oretaddr := align (ostkdata + b.(bound_stack_data)) w in (* return address *)
+  let sz := oretaddr + w in (* total size *)
   {| fe_size := sz;
      fe_ofs_link := olink;
      fe_ofs_retaddr := oretaddr;
@@ -47,31 +47,31 @@ Definition make_env (b: bounds) : frame_env :=
      fe_stack_data := ostkdata;
      fe_used_callee_save := b.(used_callee_save) |}.
 
-(** Separation property *)
-
-Local Open Scope sep_scope.
-
 Lemma frame_env_separated:
   forall b sp m P,
   let fe := make_env b in
   m |= range sp 0 (fe_stack_data fe) ** range sp (fe_stack_data fe + bound_stack_data b) (fe_size fe) ** P ->
   m |= range sp (fe_ofs_local fe) (fe_ofs_local fe + 4 * bound_local b)
        ** range sp fe_ofs_arg (fe_ofs_arg + 4 * bound_outgoing b)
-       ** range sp (fe_ofs_link fe) (fe_ofs_link fe + 4)
-       ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4)
+       ** range sp (fe_ofs_link fe) (fe_ofs_link fe + size_chunk Mptr)
+       ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + size_chunk Mptr)
        ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe))
        ** P.
 Proof.
 Local Opaque Z.add Z.mul sepconj range.
   intros; simpl.
-  set (olink := 4 * b.(bound_outgoing)).
-  set (ocs := olink + 4).
+  set (w := if Archi.ptr64 then 8 else 4).
+  set (olink := align (4 * b.(bound_outgoing)) w).
+  set (ocs := olink + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4).
+  set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
+  replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= olink) by (unfold olink; omega).
-  assert (olink + 4 <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by omega.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
+  assert (olink + w <= ocs) by (unfold ocs; omega).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
   assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
   assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
@@ -88,7 +88,7 @@ Local Opaque Z.add Z.mul sepconj range.
   rewrite sep_swap34.
 (* Apply range_split and range_split2 repeatedly *)
   unfold fe_ofs_arg.
-  apply range_split. omega.
+  apply range_split_2. fold olink. omega. omega. 
   apply range_split. omega.
   apply range_split_2. fold ol. omega. omega.
   apply range_drop_right with ostkdata. omega.
@@ -104,14 +104,17 @@ Lemma frame_env_range:
   0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe.
 Proof.
   intros; simpl.
-  set (olink := 4 * b.(bound_outgoing)).
-  set (ocs := olink + 4).
+  set (w := if Archi.ptr64 then 8 else 4).
+  set (olink := align (4 * b.(bound_outgoing)) w).
+  set (ocs := olink + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4).
+  set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
   generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
-  assert (0 <= olink) by (unfold olink; omega).
-  assert (olink + 4 <= ocs) by (unfold ocs; omega).
+  assert (0 <= 4 * b.(bound_outgoing)) by omega.
+  assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega).
+  assert (olink + w <= ocs) by (unfold ocs; omega).
   assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). 
   assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega).
   assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
@@ -125,18 +128,21 @@ Lemma frame_env_aligned:
      (8 | fe_ofs_arg)
   /\ (8 | fe_ofs_local fe)
   /\ (8 | fe_stack_data fe)
-  /\ (4 | fe_ofs_link fe)
-  /\ (4 | fe_ofs_retaddr fe).
+  /\ (align_chunk Mptr | fe_ofs_link fe)
+  /\ (align_chunk Mptr | fe_ofs_retaddr fe).
 Proof.
   intros; simpl.
-  set (olink := 4 * b.(bound_outgoing)).
-  set (ocs := olink + 4).
+  set (w := if Archi.ptr64 then 8 else 4).
+  set (olink := align (4 * b.(bound_outgoing)) w).
+  set (ocs := olink + w).
   set (ol :=  align (size_callee_save_area b ocs) 8).
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
-  set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4).
+  set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
+  assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
+  replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
   split. apply Zdivide_0.
   split. apply align_divides; omega.
   split. apply align_divides; omega.
-  split. apply Z.divide_factor_l.
+  split. apply align_divides; omega.
   apply align_divides; omega.
 Qed.