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, 282 insertions, 49 deletions

diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v
index 08a86815..dbc8b064 100644
--- a/ia32/Conventions1.v
+++ b/ia32/Conventions1.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,11 +13,8 @@
 (** Function calling conventions and other conventions regarding the use of
     machine registers and stack slots. *)
 
-Require Import Coqlib.
-Require Import Decidableplus.
-Require Import AST.
-Require Import Events.
-Require Import Locations.
+Require Import Coqlib Decidableplus.
+Require Import AST Machregs Locations.
 
 (** * Classification of machine registers *)
 
@@ -26,23 +23,37 @@ Require Import Locations.
 - Callee-save registers, whose value is preserved across a function call.
 - Caller-save registers that can be modified during a function call.
 
-  We follow the x86-32 application binary interface (ABI) in our choice
-  of callee- and caller-save registers.
+  We follow the x86-32 and x86-64 application binary interfaces (ABI)
+  in our choice of callee- and caller-save registers.
 *)
 
 Definition is_callee_save (r: mreg) : bool :=
   match r with
   | AX | CX | DX => false
-  | BX | SI | DI | BP => true
+  | BX | BP => true
+  | SI | DI => negb Archi.ptr64 (**r callee-save in 32 bits but not in 64 bits *)
+  | R8 | R9 | R10 | R11 => false
+  | R12 | R13 | R14 | R15 => true
   | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false
+  | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => false
   | FP0 => false
   end.
 
-Definition int_caller_save_regs := AX :: CX :: DX :: nil.
+Definition int_caller_save_regs :=
+  if Archi.ptr64
+  then AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil
+  else AX :: CX :: DX :: nil.
 
-Definition float_caller_save_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil.
+Definition float_caller_save_regs :=
+  if Archi.ptr64
+  then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 ::
+       X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil
+  else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil.
 
-Definition int_callee_save_regs := BX :: SI :: DI :: BP :: nil.
+Definition int_callee_save_regs :=
+  if Archi.ptr64
+  then BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil
+  else BX :: SI :: DI :: BP :: nil.
 
 Definition float_callee_save_regs : list mreg := nil.
 
@@ -52,6 +63,14 @@ Definition destroyed_at_call :=
 Definition dummy_int_reg := AX.     (**r Used in [Regalloc]. *)
 Definition dummy_float_reg := X0.   (**r Used in [Regalloc]. *)
 
+Definition is_float_reg (r: mreg) :=
+  match r with
+  | AX | BX | CX | DX | SI | DI | BP
+  | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => false
+  | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7
+  | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | FP0 => true
+  end.
+
 (** * Function calling conventions *)
 
 (** The functions in this section determine the locations (machine registers
@@ -68,15 +87,16 @@ Definition dummy_float_reg := X0.   (**r Used in [Regalloc]. *)
   of function arguments), but this leaves much liberty in choosing actual
   locations.  To ensure binary interoperability of code generated by our
   compiler with libraries compiled by another compiler, we
-  implement the standard x86 conventions. *)
+  implement the standard x86-32 and x86-64 conventions. *)
 
 (** ** Location of function result *)
 
-(** The result value of a function is passed back to the caller in
-  registers [AX] or [DX:AX] or [FP0], depending on the type of the returned value.
-  We treat a function without result as a function with one integer result. *)
+(** In 32 bit mode, the result value of a function is passed back to the
+  caller in registers [AX] or [DX:AX] or [FP0], depending on the type
+  of the returned value.  We treat a function without result as a
+  function with one integer result. *)
 
-Definition loc_result (s: signature) : rpair mreg :=
+Definition loc_result_32 (s: signature) : rpair mreg :=
   match s.(sig_res) with
   | None => One AX
   | Some (Tint | Tany32) => One AX
@@ -85,13 +105,27 @@ Definition loc_result (s: signature) : rpair mreg :=
   | Some Tlong => Twolong DX AX
   end.
 
+(** In 64 bit mode, he result value of a function is passed back to
+  the caller in registers [AX] or [X0]. *)
+
+Definition loc_result_64 (s: signature) : rpair mreg :=
+  match s.(sig_res) with
+  | None => One AX
+  | Some (Tint | Tlong | Tany32 | Tany64) => One AX
+  | Some (Tfloat | Tsingle) => One X0
+  end.
+
+Definition loc_result :=
+  if Archi.ptr64 then loc_result_64 else loc_result_32.
+
 (** The result registers have types compatible with that given in the signature. *)
 
 Lemma loc_result_type:
   forall sig,
   subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
 Proof.
-  intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
+  intros. unfold proj_sig_res, loc_result, loc_result_32, loc_result_64, mreg_type;
+  destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto.
 Qed.
 
 (** The result locations are caller-save registers *)
@@ -100,8 +134,8 @@ Lemma loc_result_caller_save:
   forall (s: signature),
   forall_rpair (fun r => is_callee_save r = false) (loc_result s).
 Proof.
-  intros.
-  unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
+  intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save;
+  destruct Archi.ptr64; destruct (sig_res s) as [[]|]; simpl; auto.
 Qed.
 
 (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
@@ -110,17 +144,32 @@ Lemma loc_result_pair:
   forall sg,
   match loc_result sg with
   | One _ => True
-  | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+  | Twolong r1 r2 =>
+       r1 <> r2 /\ sg.(sig_res) = Some Tlong
+    /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true 
+    /\ Archi.splitlong = true
   end.
 Proof.
-  intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence. 
+  intros. change Archi.splitlong with (negb Archi.ptr64).
+  unfold loc_result, loc_result_32, loc_result_64, mreg_type;
+  destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto.
+  split; auto. congruence.
+Qed.
+
+(** The location of the result depends only on the result part of the signature *)
+
+Lemma loc_result_exten:
+  forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
+Proof.
+  intros. unfold loc_result, loc_result_32, loc_result_64.
+  destruct Archi.ptr64; rewrite H; auto.  
 Qed.
 
 (** ** Location of function arguments *)
 
-(** All arguments are passed on stack. (Snif.) *)
+(** In the x86-32 ABI, all arguments are passed on stack. (Snif.) *)
 
-Fixpoint loc_arguments_rec
+Fixpoint loc_arguments_32
     (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
@@ -129,27 +178,77 @@ Fixpoint loc_arguments_rec
       | Tlong => Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint)
       | _     => One (S Outgoing ofs ty)
       end
-      :: loc_arguments_rec tys (ofs + typesize ty)
+      :: loc_arguments_32 tys (ofs + typesize ty)
+  end.
+
+(** In the x86-64 ABI:
+- The first 6 integer arguments are passed in registers [DI], [SI], [DX], [CX], [R8], [R9].
+- The first 8 floating-point arguments are passed in registers [X0] to [X7].
+- Extra arguments are passed on the stack, in [Outgoing] slots.
+  Consecutive stack slots are separated by 8 bytes, even if only 4 bytes
+  of data is used in a slot.
+*)
+
+Definition int_param_regs := DI :: SI :: DX :: CX :: R8 :: R9 :: nil.
+Definition float_param_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil.
+
+Fixpoint loc_arguments_64
+    (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) :=
+  match tyl with
+  | nil => nil
+  | (Tint | Tlong | Tany32 | Tany64) as ty :: tys =>
+      match list_nth_z int_param_regs ir with
+      | None =>
+          One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2)
+      | Some ireg =>
+          One (R ireg) :: loc_arguments_64 tys (ir + 1) fr ofs
+      end
+  | (Tfloat | Tsingle) as ty :: tys =>
+      match list_nth_z float_param_regs fr with
+      | None =>
+          One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2)
+      | Some freg =>
+          One (R freg) :: loc_arguments_64 tys ir (fr + 1) ofs
+      end
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_args) 0.
+  if Archi.ptr64
+  then loc_arguments_64 s.(sig_args) 0 0 0
+  else loc_arguments_32 s.(sig_args) 0.
 
 (** [size_arguments s] returns the number of [Outgoing] slots used
   to call a function with signature [s]. *)
 
-Fixpoint size_arguments_rec
+Fixpoint size_arguments_32
     (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
   match tyl with
   | nil => ofs
-  | ty :: tys => size_arguments_rec tys (ofs + typesize ty)
+  | ty :: tys => size_arguments_32 tys (ofs + typesize ty)
+  end.
+
+Fixpoint size_arguments_64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
+  match tyl with
+  | nil => ofs
+  | (Tint | Tlong | Tany32 | Tany64) :: tys =>
+      match list_nth_z int_param_regs ir with
+      | None => size_arguments_64 tys ir fr (ofs + 2)
+      | Some ireg => size_arguments_64 tys (ir + 1) fr ofs
+      end
+  | (Tfloat | Tsingle) :: tys =>
+      match list_nth_z float_param_regs fr with
+      | None => size_arguments_64 tys ir fr (ofs + 2)
+      | Some freg => size_arguments_64 tys ir (fr + 1) ofs
+      end
   end.
 
 Definition size_arguments (s: signature) : Z :=
-  size_arguments_rec s.(sig_args) 0.
+  if Archi.ptr64
+  then size_arguments_64 s.(sig_args) 0 0 0
+  else size_arguments_32 s.(sig_args) 0.
 
 (** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -161,19 +260,26 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
   | _ => False
   end.
 
-Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
+Definition loc_argument_32_charact (ofs: Z) (l: loc) : Prop :=
   match l with
   | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
   | _ => False
   end.
 
-Remark loc_arguments_rec_charact:
+Definition loc_argument_64_charact (ofs: Z) (l: loc) : Prop :=
+  match l with
+  | R r => In r int_param_regs \/ In r float_param_regs
+  | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs')
+  | _ => False
+  end.
+
+Remark loc_arguments_32_charact:
   forall tyl ofs p,
-  In p (loc_arguments_rec tyl ofs) -> forall_rpair (loc_argument_charact ofs) p.
+  In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p.
 Proof.
-  assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l).
+  assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l).
   { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
-  induction tyl as [ | ty tyl]; simpl loc_arguments_rec; intros.
+  induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros.
 - contradiction.
 - destruct H.
 + destruct ty; subst p; simpl; omega.
@@ -182,23 +288,73 @@ Proof.
 * destruct H; split; eapply X; eauto; omega.
 Qed.
 
+Remark loc_arguments_64_charact:
+  forall tyl ir fr ofs p,
+  In p (loc_arguments_64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_64_charact ofs) p.
+Proof.
+  assert (X: forall ofs1 ofs2 l, loc_argument_64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_64_charact ofs1 l).
+  { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. }
+  assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p).
+  { destruct p; simpl; intuition eauto. }
+  assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
+  { intros. apply Z.divide_add_r; auto. apply Zdivide_refl. }
+Opaque list_nth_z.
+  induction tyl; simpl loc_arguments_64; intros.
+  elim H.
+  assert (A: forall ty, In p
+      match list_nth_z int_param_regs ir with
+      | Some ireg => One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs
+      | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2)
+      end ->
+      forall_rpair (loc_argument_64_charact ofs) p).
+  { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1.
+    subst. left. eapply list_nth_z_in; eauto.
+    eapply IHtyl; eauto.
+    subst. split. omega. assumption. 
+    eapply Y; eauto. omega. }
+  assert (B: forall ty, In p
+      match list_nth_z float_param_regs fr with
+      | Some ireg => One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs
+      | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2)
+      end ->
+      forall_rpair (loc_argument_64_charact ofs) p).
+  { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1.
+    subst. right. eapply list_nth_z_in; eauto.
+    eapply IHtyl; eauto.
+    subst. split. omega. assumption. 
+    eapply Y; eauto. omega. }
+  destruct a; eauto.
+Qed.
+
 Lemma loc_arguments_acceptable:
   forall (s: signature) (p: rpair loc),
   In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
 Proof.
-  unfold loc_arguments; intros.
-  exploit loc_arguments_rec_charact; eauto.
-  assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
+  unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF.
+- (* 64 bits *)
+  assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal).
+  assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal.
+  assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l).
+  { unfold loc_argument_64_charact, loc_argument_acceptable.
+    destruct l as [r | [] ofs ty]; auto.  intros [C|C]; auto.
+    intros [C D]. split; auto. apply Zdivide_trans with 2; auto. 
+    exists (2 / typealign ty); destruct ty; reflexivity.
+  }
+  exploit loc_arguments_64_charact; eauto using Zdivide_0. 
+  unfold forall_rpair; destruct p; intuition auto.
+- (* 32 bits *)
+  assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l).
   { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. }
-  destruct p; simpl; intuition auto.
+  exploit loc_arguments_32_charact; eauto. 
+  unfold forall_rpair; destruct p; intuition auto.
 Qed.
 
 Hint Resolve loc_arguments_acceptable: locs.
 
 (** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
 
-Remark size_arguments_rec_above:
-  forall tyl ofs0, ofs0 <= size_arguments_rec tyl ofs0.
+Remark size_arguments_32_above:
+  forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0.
 Proof.
   induction tyl; simpl; intros.
   omega.
@@ -206,23 +362,45 @@ Proof.
   generalize (typesize_pos a); omega.
 Qed.
 
+Remark size_arguments_64_above:
+  forall tyl ir fr ofs0,
+  ofs0 <= size_arguments_64 tyl ir fr ofs0.
+Proof.
+  induction tyl; simpl; intros.
+  omega.
+  assert (A: ofs0 <=
+    match list_nth_z int_param_regs ir with
+    | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
+    | None => size_arguments_64 tyl ir fr (ofs0 + 2)
+    end).
+  { destruct (list_nth_z int_param_regs ir); eauto. 
+    apply Zle_trans with (ofs0 + 2); auto. omega. }
+  assert (B: ofs0 <=
+    match list_nth_z float_param_regs fr with
+    | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
+    | None => size_arguments_64 tyl ir fr (ofs0 + 2)
+    end).
+  { destruct (list_nth_z float_param_regs fr); eauto. 
+    apply Zle_trans with (ofs0 + 2); auto. omega. }
+  destruct a; auto.
+Qed.
+
 Lemma size_arguments_above:
   forall s, size_arguments s >= 0.
 Proof.
   intros; unfold size_arguments. apply Zle_ge.
-  apply size_arguments_rec_above.
+  destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above].
 Qed.
 
-Lemma loc_arguments_bounded:
-  forall (s: signature) (ofs: Z) (ty: typ),
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
-  ofs + typesize ty <= size_arguments s.
+Lemma loc_arguments_32_bounded:
+  forall ofs ty tyl ofs0,
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) ->
+  ofs + typesize ty <= size_arguments_32 tyl ofs0.
 Proof.
-  intros until ty. unfold loc_arguments, size_arguments. generalize (sig_args s) 0.
-  induction l as [ | t l]; simpl; intros x IN.
+  induction tyl as [ | t l]; simpl; intros x IN.
 - contradiction.
 - rewrite in_app_iff in IN; destruct IN as [IN|IN].
-+ apply Zle_trans with (x + typesize t); [|apply size_arguments_rec_above].
++ apply Zle_trans with (x + typesize t); [|apply size_arguments_32_above].
   Ltac decomp :=
   match goal with
   | [ H: _ \/ _ |- _ ] => destruct H; decomp
@@ -233,8 +411,63 @@ Proof.
 + apply IHl; auto.
 Qed.
 
+Lemma loc_arguments_64_bounded:
+  forall ofs ty tyl ir fr ofs0,
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) ->
+  ofs + typesize ty <= size_arguments_64 tyl ir fr ofs0.
+Proof.
+  induction tyl; simpl; intros.
+  contradiction.
+  assert (T: forall ty0, typesize ty0 <= 2).
+  { destruct ty0; simpl; omega. }
+  assert (A: forall ty0, 
+             In (S Outgoing ofs ty) (regs_of_rpairs
+              match list_nth_z int_param_regs ir with
+              | Some ireg =>
+                  One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs0
+              | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2)
+              end) ->
+             ofs + typesize ty <=
+             match list_nth_z int_param_regs ir with
+             | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0
+             | None => size_arguments_64 tyl ir fr (ofs0 + 2)
+             end).
+  { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
+  - discriminate.
+  - eapply IHtyl; eauto.
+  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.  
+  - eapply IHtyl; eauto. }
+  assert (B: forall ty0, 
+             In (S Outgoing ofs ty) (regs_of_rpairs
+              match list_nth_z float_param_regs fr with
+              | Some ireg =>
+                  One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs0
+              | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2)
+              end) ->
+             ofs + typesize ty <=
+             match list_nth_z float_param_regs fr with
+             | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
+             | None => size_arguments_64 tyl ir fr (ofs0 + 2)
+             end).
+  { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
+  - discriminate.
+  - eapply IHtyl; eauto.
+  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.  
+  - eapply IHtyl; eauto. }
+  destruct a; eauto.
+Qed.
+
+Lemma loc_arguments_bounded:
+  forall (s: signature) (ofs: Z) (ty: typ),
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
+  ofs + typesize ty <= size_arguments s.
+Proof.
+  unfold loc_arguments, size_arguments; intros.
+  destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded.
+Qed.
+
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.
-  reflexivity.
+  unfold loc_arguments; destruct Archi.ptr64; reflexivity.
 Qed.