1 files changed, 117 insertions, 220 deletions

diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v
index f1ddc23..1731eba 100644
--- a/arm/linux/Conventions1.v
+++ b/arm/linux/Conventions1.v
@@ -32,34 +32,19 @@ Require Import Locations.
 *)
 
 Definition int_caller_save_regs :=
-  R0 :: R1 :: R2 :: R3 :: nil.
+  R0 :: R1 :: R2 :: R3 :: R12 :: nil.
 
 Definition float_caller_save_regs :=
-  F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: nil.
+  F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil.
 
 Definition int_callee_save_regs :=
-  R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R11 :: nil.
+  R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: nil.
 
 Definition float_callee_save_regs :=
   F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil.
 
-Definition destroyed_at_call_regs :=
-  int_caller_save_regs ++ float_caller_save_regs.
-
 Definition destroyed_at_call :=
-  List.map R destroyed_at_call_regs.
-
-Definition int_temporaries := IT1 :: IT2 :: nil.
-
-Definition float_temporaries := FT1 :: FT2 :: nil.
-  
-Definition temporary_regs := int_temporaries ++ float_temporaries.
-
-Definition temporaries := List.map R temporary_regs.
-
-Definition destroyed_at_move_regs: list mreg := nil.
-
-Definition destroyed_at_move := List.map R destroyed_at_move_regs.
+  int_caller_save_regs ++ float_caller_save_regs.
 
 Definition dummy_int_reg := R0.     (**r Used in [Coloring]. *)
 Definition dummy_float_reg := F0.   (**r Used in [Coloring]. *)
@@ -72,7 +57,7 @@ Definition dummy_float_reg := F0.   (**r Used in [Coloring]. *)
 Definition index_int_callee_save (r: mreg) :=
   match r with
   | R4 => 0  | R5 => 1  | R6 => 2  | R7 => 3
-  | R8 => 4  | R9 => 5  | R11 => 6
+  | R8 => 4  | R9 => 5  | R10 => 6 | R11 => 7
   | _ => -1
   end.
 
@@ -169,34 +154,27 @@ Qed.
 
 Lemma register_classification:
   forall r, 
-  (In (R r) temporaries \/ In (R r) destroyed_at_call) \/
-  (In r int_callee_save_regs \/ In r float_callee_save_regs).
+  In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs.
 Proof.
   destruct r; 
-  try (left; left; simpl; OrEq);
-  try (left; right; simpl; OrEq);
+  try (left; simpl; OrEq);
   try (right; left; simpl; OrEq);
   try (right; right; simpl; OrEq).
 Qed.
 
+
 Lemma int_callee_save_not_destroyed:
   forall r, 
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    ~(In r int_callee_save_regs).
+    In r destroyed_at_call -> In r int_callee_save_regs -> False.
 Proof.
-  intros; red; intros. elim H.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
+  intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
 Qed.
 
 Lemma float_callee_save_not_destroyed:
   forall r, 
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    ~(In r float_callee_save_regs).
+    In r destroyed_at_call -> In r float_callee_save_regs -> False.
 Proof.
-  intros; red; intros. elim H.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
+  intros. revert H0 H. simpl. ElimOrEq; NotOrEq.
 Qed.
 
 Lemma int_callee_save_type:
@@ -245,51 +223,33 @@ Qed.
   Calling conventions are largely arbitrary: they must respect the properties
   proved in this section (such as no overlapping between the locations
   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 ARM EABI compiler, we
-  implement *almost* the standard conventions defined in the ARM EABI application
-  binary interface, with two exceptions:
-- Double-precision arguments and results are passed in VFP double registers
-  instead of pairs of integer registers.
-- Single-precision arguments and results are passed as double-precision floats.
-*)
+  locations.  *)
 
 (** ** Location of function result *)
 
 (** The result value of a function is passed back to the caller in
-  registers [R0] or [F0], depending on the type of the returned value.
-  We treat a function without result as a function with one integer result. *)
+  registers [R0] or [F0] or [R0,R1], 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) : mreg :=
+Definition loc_result (s: signature) : list mreg :=
   match s.(sig_res) with
-  | None => R0
-  | Some Tint => R0
-  | Some Tfloat => F0
+  | None => R0 :: nil
+  | Some Tint => R0 :: nil
+  | Some Tfloat => F0 :: nil
+  | Some Tlong => R1 :: R0 :: nil
   end.
 
-(** The result location has the type stated in the signature. *)
-
-Lemma loc_result_type:
-  forall sig,
-  mreg_type (loc_result sig) =
-  match sig.(sig_res) with None => Tint | Some ty => ty end.
-Proof.
-  intros; unfold loc_result.
-  destruct (sig_res sig). 
-  destruct t; reflexivity.
-  reflexivity.
-Qed.
-
 (** The result location is a caller-save register or a temporary *)
 
 Lemma loc_result_caller_save:
-  forall (s: signature), 
-  In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries.
+  forall (s: signature) (r: mreg), 
+  In r (loc_result s) -> In r destroyed_at_call.
 Proof.
-  intros; unfold loc_result. left;
-  destruct (sig_res s). 
-  destruct t; simpl; OrEq.
-  simpl; OrEq.
+  intros.
+  assert (r = R0 \/ r = R1 \/ r = F0).
+    unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition.
+  destruct H0 as [A | [A | A]]; subst r; simpl; OrEq.
 Qed.
 
 (** ** Location of function arguments *)
@@ -299,34 +259,37 @@ Qed.
 - The first 2 float arguments are passed in registers [F0] and [F1].
 - Each float argument passed in a float register ``consumes'' an aligned pair
   of two integer registers.
+- Each long integer argument is passed in an aligned pair of two integer
+  registers.
 - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively
-  assigned (1 word for an integer argument, 2 words for a float),
+  assigned (1 word for an integer argument, 2 words for a float or a long),
   starting at word offset 0.
 *)
 
-Function ireg_param (n: Z) : mreg :=
+Definition ireg_param (n: Z) : mreg :=
   if zeq n (-4) then R0
   else if zeq n (-3) then R1
   else if zeq n (-2) then R2
-  else if zeq n (-1) then R3
-  else R4. (**r should not happen *)
-
-Function freg_param (n: Z) : mreg :=
-  if zeq n (-4) then F0
-  else if zeq n (-3) then F1
-  else if zeq n (-2) then F1
-  else F2.  (**r should not happen *)
+  else R3.
 
+Definition freg_param (n: Z) : mreg :=
+  if zeq n (-4) then F0 else F1.
 
 Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
   match tyl with
   | nil => nil
   | Tint :: tys =>
-      (if zle 0 ofs then S (Outgoing ofs Tint) else R (ireg_param ofs))
+      (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs))
       :: loc_arguments_rec tys (ofs + 1)
   | Tfloat :: tys =>
-      (if zle (-1) ofs then S (Outgoing (align ofs 2) Tfloat) else R (freg_param ofs))
-      :: loc_arguments_rec tys (align ofs 2 + 2)
+      let ofs := align ofs 2 in
+      (if zle 0 ofs then S Outgoing ofs Tfloat else R (freg_param ofs))
+      :: loc_arguments_rec tys (ofs + 2)
+  | Tlong :: tys =>
+      let ofs := align ofs 2 in
+      (if zle 0 ofs then S Outgoing (ofs + 1) Tint else R (ireg_param (ofs + 1)))
+      :: (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs))
+      :: loc_arguments_rec tys (ofs + 2)
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
@@ -342,7 +305,7 @@ Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
   match tyl with
   | nil => ofs
   | Tint :: tys => size_arguments_rec tys (ofs + 1)
-  | Tfloat :: tys => size_arguments_rec tys (align ofs 2 + 2)
+  | (Tfloat | Tlong) :: tys => size_arguments_rec tys (align ofs 2 + 2)
   end.
 
 Definition size_arguments (s: signature) : Z :=
@@ -353,109 +316,85 @@ Definition size_arguments (s: signature) : Z :=
 
 Definition loc_argument_acceptable (l: loc) : Prop :=
   match l with
-  | R r => ~(In l temporaries)
-  | S (Outgoing ofs ty) => ofs >= 0
+  | R r => In r destroyed_at_call
+  | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong
   | _ => False
   end.
 
+(*
 Lemma align_monotone:
   forall x1 x2 y, y > 0 -> x1 <= x2 -> align x1 y <= align x2 y.
 Proof.
   intros. unfold align. apply Zmult_le_compat_r. apply Z_div_le. 
   omega. omega. omega.
 Qed.
+*)
+
+Remark ireg_param_caller_save:
+  forall n, In (ireg_param n) destroyed_at_call.
+Proof.
+  unfold ireg_param; intros.
+  destruct (zeq n (-4)). simpl; auto. 
+  destruct (zeq n (-3)). simpl; auto. 
+  destruct (zeq n (-2)); simpl; auto.
+Qed.
+
+Remark freg_param_caller_save:
+  forall n, In (freg_param n) destroyed_at_call.
+Proof.
+  unfold freg_param; intros. destruct (zeq n (-4)); simpl; OrEq.
+Qed.
 
 Remark loc_arguments_rec_charact:
   forall tyl ofs l,
   In l (loc_arguments_rec tyl ofs) ->
   match l with
-  | R r => 
-       (exists n, ofs <= n < 0 /\ r = ireg_param n)
-    \/ (exists n, ofs <= n < -1 /\ r = freg_param n)
-  | S (Outgoing ofs' ty) => ofs' >= 0 /\ ofs' >= ofs
-  | S _ => False
+  | R r => In r destroyed_at_call
+  | S Outgoing ofs' ty => ofs' >= 0 /\ ofs <= ofs' /\ ty <> Tlong
+  | S _ _ _ => False
   end.
 Proof.
   induction tyl; simpl loc_arguments_rec; intros.
   elim H.
-  destruct a; elim H; intro.
-  subst l. destruct (zle 0 ofs). omega.
-  left. exists ofs; split; auto; omega.
-  generalize (IHtyl _ _ H0). 
-  destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega.
-  destruct s; auto; omega.
-  subst l. destruct (zle (-1) ofs).
-  split. apply Zle_ge. change 0 with (align (-1) 2). apply align_monotone; omega.
-  apply Zle_ge. apply align_le. omega.
-  right. exists ofs. intuition.
+  destruct a.
+- (* Tint *)
+  destruct H.
+  subst l. destruct (zle 0 ofs).
+  split. omega. split. omega. congruence.
+  apply ireg_param_caller_save.
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* Tfloat *)
   assert (ofs <= align ofs 2) by (apply align_le; omega).
-  generalize (IHtyl _ _ H0). 
-  destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega.
-  destruct s; auto; omega.
-Qed.
-
-Lemma loc_notin_in_diff:
-  forall l ll,
-  Loc.notin l ll <-> (forall l', In l' ll -> Loc.diff l l').
-Proof.
-  induction ll; simpl; intuition. subst l'. auto. 
-Qed.
-  
-Remark loc_arguments_rec_notin_local:
-  forall tyl ofs ofs0 ty0,
-  Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl ofs).
-Proof.
-  intros. rewrite loc_notin_in_diff. intros. 
-  exploit loc_arguments_rec_charact; eauto. 
-  destruct l'; intros; simpl; auto. destruct s; auto; contradiction.
+  destruct H.
+  subst l. destruct (zle 0 (align ofs 2)).
+  split. omega. split. auto. congruence.
+  apply freg_param_caller_save.
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* Tlong *)
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  destruct H.
+  subst l. destruct (zle 0 (align ofs 2)).
+  split. omega. split. omega. congruence.
+  apply ireg_param_caller_save.
+  destruct H.
+  subst l. destruct (zle 0 (align ofs 2)).
+  split. omega. split. omega. congruence.
+  apply ireg_param_caller_save.
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
 Qed.
 
 Lemma loc_arguments_acceptable:
   forall (s: signature) (r: loc),
   In r (loc_arguments s) -> loc_argument_acceptable r.
 Proof.
-  unfold loc_arguments; intros.
+  unfold loc_arguments, loc_argument_acceptable; intros.
   generalize (loc_arguments_rec_charact _ _ _ H).
-  destruct r; simpl.
-  intros [[n [A B]] | [n [A B]]]; subst m.
-  functional induction (ireg_param n); intuition congruence.
-  functional induction (freg_param n); intuition congruence.
-  destruct s0; tauto.
+  destruct r; auto.
+  destruct sl; auto.
+  tauto.
 Qed.
 Hint Resolve loc_arguments_acceptable: locs.
 
-(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *)
-
-Lemma loc_arguments_norepet:
-  forall (s: signature), Loc.norepet (loc_arguments s).
-Proof.
-  unfold loc_arguments; intros. 
-  assert (forall tyl ofs, -4 <= ofs -> Loc.norepet (loc_arguments_rec tyl ofs)).
-    induction tyl; simpl; intros.
-    constructor.
-    destruct a; constructor.
-    rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. 
-    destruct (zle 0 ofs); destruct l'; simpl; auto.
-    destruct s0; intuition.
-    intros [[n [A B]] | [n [A B]]]; subst m.
-    functional induction (ireg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction.
-    functional induction (ireg_param ofs); functional induction (freg_param n); congruence || omegaContradiction.
-    apply IHtyl. omega.
-    rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. 
-    destruct (zle (-1) ofs); destruct l'; simpl; auto.
-    destruct s0; intuition.
-    intros [[n [A B]] | [n [A B]]]; subst m.
-    functional induction (freg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction.
-    functional induction (freg_param ofs); functional induction (freg_param n); try (congruence || omegaContradiction).
-    compute in A. intuition.
-    compute in A. intuition.
-    compute in A. intuition.
-    compute in A. intuition.
-    compute in A. intuition.
-    apply IHtyl. assert (ofs <= align ofs 2) by (apply align_le; omega). omega.
-  apply H. omega.
-Qed.
-
 (** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
 
 Remark size_arguments_rec_above:
@@ -468,6 +407,8 @@ Proof.
   apply Zle_trans with (ofs + 1); auto; omega.
   assert (ofs <= align ofs 2) by (apply align_le; omega).
   apply Zle_trans with (align ofs 2 + 2); auto; omega.
+  assert (ofs <= align ofs 2) by (apply align_le; omega).
+  apply Zle_trans with (align ofs 2 + 2); auto; omega.
 Qed.
 
 Lemma size_arguments_above:
@@ -478,79 +419,35 @@ Qed.
 
 Lemma loc_arguments_bounded:
   forall (s: signature) (ofs: Z) (ty: typ),
-  In (S (Outgoing ofs ty)) (loc_arguments s) ->
+  In (S Outgoing ofs ty) (loc_arguments s) ->
   ofs + typesize ty <= size_arguments s.
 Proof.
   intros.
   assert (forall tyl ofs0,
           0 <= ofs0 ->
           ofs0 <= Zmax 0 (size_arguments_rec tyl ofs0)).
+  {
     intros. generalize (size_arguments_rec_above tyl ofs0). intros.
-    rewrite Zmax_spec. rewrite zlt_false. auto. omega. 
+    rewrite Zmax_spec. rewrite zlt_false. auto. omega.
+  } 
   assert (forall tyl ofs0,
-    In (S (Outgoing ofs ty)) (loc_arguments_rec tyl ofs0) ->
+    In (S Outgoing ofs ty) (loc_arguments_rec tyl ofs0) ->
     ofs + typesize ty <= Zmax 0 (size_arguments_rec tyl ofs0)).
-  induction tyl; simpl; intros.
-  elim H1.
-  destruct a; elim H1; intros.
-  destruct (zle 0 ofs0); inv H2. apply H0. omega. auto.
-  destruct (zle (-1) ofs0); inv H2. apply H0. 
-  assert (align (-1) 2 <= align ofs0 2). apply align_monotone. omega. auto.
-  change (align (-1) 2) with 0 in H2. omega. 
-  auto.
- 
+  {
+    induction tyl; simpl; intros.
+    elim H1.
+    destruct a.
+  - (* Tint *)
+    destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega. 
+  - (* Tfloat *)
+    destruct H1; auto. destruct (zle 0 (align ofs0 2)); inv H1. apply H0. omega.
+  - (* Tlong *)
+    destruct H1.
+    destruct (zle 0 (align ofs0 2)); inv H1.
+    eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega. 
+    destruct H1; auto.
+    destruct (zle 0 (align ofs0 2)); inv H1.
+    eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega.
+  }
   unfold size_arguments. apply H1. auto.  
 Qed.
-
-(** Temporary registers do not overlap with argument locations. *)
-
-Lemma loc_arguments_not_temporaries:
-  forall sig, Loc.disjoint (loc_arguments sig) temporaries.
-Proof.
-  intros; red; intros x1 x2 A B.
-  exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable. 
-  destruct x1; intros. simpl. destruct x2; auto. intuition congruence.
-  destruct s; try contradiction. revert B. simpl. ElimOrEq; auto.
-Qed.
-Hint Resolve loc_arguments_not_temporaries: locs.
-
-(** Argument registers are caller-save. *)
-
-Lemma arguments_caller_save:
-  forall sig r,
-  In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call.
-Proof.
-  unfold loc_arguments; intros.
-  destruct (loc_arguments_rec_charact _ _ _ H) as [[n [A B]] | [n [A B]]]; subst r.
-  functional induction (ireg_param n); simpl; auto. omegaContradiction.
-  functional induction (freg_param n); simpl; auto 10.
-Qed.
-
-(** Argument locations agree in number with the function signature. *)
-
-Lemma loc_arguments_length:
-  forall sig,
-  List.length (loc_arguments sig) = List.length sig.(sig_args).
-Proof.
-  assert (forall tyl ofs, List.length (loc_arguments_rec tyl ofs) = List.length tyl).
-  induction tyl; simpl; intros.
-  auto.
-  destruct a; simpl; decEq; auto.
-
-  intros. unfold loc_arguments. auto.
-Qed.
-
-(** Argument locations agree in types with the function signature. *)
-
-Lemma loc_arguments_type:
-  forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args).
-Proof.
-  assert (forall tyl ofs, List.map Loc.type (loc_arguments_rec tyl ofs) = tyl).
-  induction tyl; simpl; intros.
-  auto.
-  destruct a; simpl; decEq; auto.
-  destruct (zle 0 ofs). auto. functional induction (ireg_param ofs); auto.
-  destruct (zle (-1) ofs). auto. functional induction (freg_param ofs); auto.
-
-  intros. unfold loc_arguments. apply H. 
-Qed.