Introduce register pairs to describe calling conventions more precisely

This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations.

In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves.  We will need to change this in the future to support 64-bit processors.  The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting.  Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves.

Summary of changes:
- AST: introduce the type "rpair A" of register pairs
- Conventions1, Conventions: use it when describing calling conventions
- LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls
- Events: suppress external_call', no longer useful
- All passes from Allocation to Asmgen: adapt accordingly.

18 files changed, 438 insertions, 379 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 84606210..0d25d84a 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -616,51 +616,40 @@ Fixpoint add_equations (rl: list reg) (ml: list mreg) (e: eqs) : option eqs :=
   of pseudoregisters of type [Tlong] in two locations containing the
   two 32-bit halves of the 64-bit integer. *)
 
-Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list loc) (e: eqs) : option eqs :=
+Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc)) (e: eqs) : option eqs :=
   match rl, tyl, ll with
   | nil, nil, nil => Some e
-  | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll =>
-      add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e))
-  | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll =>
+  | r1 :: rl, ty :: tyl, One l1 :: ll =>
       add_equations_args rl tyl ll (add_equation (Eq Full r1 l1) e)
+  | r1 :: rl, Tlong :: tyl, Twolong l1 l2 :: ll =>
+      add_equations_args rl tyl ll (add_equation (Eq Low r1 l2) (add_equation (Eq High r1 l1) e))
   | _, _, _ => None
   end.
 
 (** [add_equations_res] is similar but is specialized to the case where
   there is only one pseudo-register. *)
 
-Function add_equations_res (r: reg) (oty: option typ) (ll: list loc) (e: eqs) : option eqs :=
-  match oty with
-  | Some Tlong =>
-      match ll with
-      | l1 :: l2 :: nil => Some (add_equation (Eq Low r l2) (add_equation (Eq High r l1) e))
-      | _ => None
-      end
-  | _ =>
-      match ll with
-      | l1 :: nil => Some (add_equation (Eq Full r l1) e)
-      | _ => None
-      end
+Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs :=
+  match p, oty with
+  | One mr, _ =>
+      Some (add_equation (Eq Full r (R mr)) e)
+  | Twolong mr1 mr2, Some Tlong =>
+      Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e))
+  | _, _ =>
+      None
   end.
 
 (** [remove_equations_res] is similar to [add_equations_res] but removes
   equations instead of adding them. *)
 
-Function remove_equations_res (r: reg) (oty: option typ) (ll: list loc) (e: eqs) : option eqs :=
-  match oty with
-  | Some Tlong =>
-      match ll with
-      | l1 :: l2 :: nil =>
-          if Loc.diff_dec l2 l1
-          then Some (remove_equation (Eq Low r l2) (remove_equation (Eq High r l1) e))
-          else None
-      | _ => None
-      end
-  | _ =>
-      match ll with
-      | l1 :: nil => Some (remove_equation (Eq Full r l1) e)
-      | _ => None
-      end
+Function remove_equations_res (r: reg) (p: rpair mreg) (e: eqs) : option eqs :=
+  match p with
+  | One mr =>
+      Some (remove_equation (Eq Full r (R mr)) e)
+  | Twolong mr1 mr2 =>
+      if mreg_eq mr2 mr1
+      then None
+      else Some (remove_equation (Eq Low r (R mr2)) (remove_equation (Eq High r (R mr1)) e))
   end.
 
 (** [add_equations_ros] adds an equation, if needed, between an optional
@@ -960,10 +949,11 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       track_moves env mv1 e3
   | BScall sg ros args res mv1 ros' mv2 s =>
       let args' := loc_arguments sg in
-      let res' := map R (loc_result sg) in
+      let res' := loc_result sg in
       do e1 <- track_moves env mv2 e;
-      do e2 <- remove_equations_res res (sig_res sg) res' e1;
-      assertion (forallb (fun l => reg_loc_unconstrained res l e2) res');
+      do e2 <- remove_equations_res res res' e1;
+      assertion (forallb (fun l => reg_loc_unconstrained res l e2)
+                         (map R (regs_of_rpair res')));
       assertion (no_caller_saves e2);
       do e3 <- add_equation_ros ros ros' e2;
       do e4 <- add_equations_args args (sig_args sg) args' e3;
@@ -1000,7 +990,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
   | BSreturn None mv =>
       track_moves env mv empty_eqs
   | BSreturn (Some arg) mv =>
-      let arg' := map R (loc_result (RTL.fn_sig f)) in
+      let arg' := loc_result (RTL.fn_sig f) in
       do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
       track_moves env mv e1
   end.
@@ -1184,15 +1174,15 @@ Definition analyze (f: RTL.function) (env: regenv) (bsh: PTree.t block_shape) :=
   involving pseudoregs [r'] not in [rparams]: these equations are
   automatically satisfied since the initial value of [r'] is [Vundef]. *)
 
-Function compat_entry (rparams: list reg) (tys: list typ) (lparams: list loc) (e: eqs)
+Function compat_entry (rparams: list reg) (lparams: list (rpair loc)) (e: eqs)
                       {struct rparams} : bool :=
-  match rparams, tys, lparams with
-  | nil, nil, nil => true
-  | r1 :: rl, Tlong :: tyl, l1 :: l2 :: ll =>
-      compat_left2 r1 l1 l2 e && compat_entry rl tyl ll e
-  | r1 :: rl, (Tint|Tfloat|Tsingle) :: tyl, l1 :: ll =>
-      compat_left r1 l1 e && compat_entry rl tyl ll e
-  | _, _, _ => false
+  match rparams, lparams with
+  | nil, nil => true
+  | r1 :: rl,  One l1 :: ll =>
+      compat_left r1 l1 e && compat_entry rl ll e
+  | r1 :: rl, Twolong l1 l2 :: ll =>
+      compat_left2 r1 l1 l2 e && compat_entry rl ll e
+  | _, _ => false
   end.
 
 (** Checking the satisfiability of equations inferred at function entry
@@ -1204,7 +1194,6 @@ Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function)
   do mv <- pair_entrypoints rtl ltl;
   do e2 <- track_moves env mv e1;
   assertion (compat_entry (RTL.fn_params rtl)
-                          (sig_args (RTL.fn_sig rtl))
                           (loc_parameters (RTL.fn_sig rtl)) e2);
   assertion (can_undef destroyed_at_function_entry e2);
   assertion (zeq (RTL.fn_stacksize rtl) (LTL.fn_stacksize ltl));
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index bf60a57f..154c1e2e 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -415,12 +415,10 @@ Lemma add_equations_args_satisf:
   satisf rs ls e' -> satisf rs ls e.
 Proof.
   intros until e'. functional induction (add_equations_args rl tyl ll e); intros.
-  inv H; auto.
-  eapply add_equation_satisf. eapply add_equation_satisf. eauto.
-  eapply add_equation_satisf. eauto.
-  eapply add_equation_satisf. eauto.
-  eapply add_equation_satisf. eauto.
-  congruence.
+- inv H; auto.
+- eapply add_equation_satisf; eauto.
+- eapply add_equation_satisf. eapply add_equation_satisf. eauto.
+- congruence.
 Qed.
 
 Lemma val_longofwords_eq:
@@ -438,22 +436,18 @@ Lemma add_equations_args_lessdef:
   add_equations_args rl tyl ll e = Some e' ->
   satisf rs ls e' ->
   Val.has_type_list (rs##rl) tyl ->
-  Val.lessdef_list (rs##rl) (decode_longs tyl (map ls ll)).
+  Val.lessdef_list (rs##rl) (map (fun p => Locmap.getpair p ls) ll).
 Proof.
   intros until e'. functional induction (add_equations_args rl tyl ll e); simpl; intros.
 - inv H; auto.
 - destruct H1. constructor; auto.
+  eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
+- destruct H1. constructor; auto.
   rewrite <- (val_longofwords_eq (rs#r1)); auto. apply Val.longofwords_lessdef.
   eapply add_equation_lessdef with (q := Eq High r1 l1).
   eapply add_equation_satisf. eapply add_equations_args_satisf; eauto.
   eapply add_equation_lessdef with (q := Eq Low r1 l2).
   eapply add_equations_args_satisf; eauto.
-- destruct H1. constructor; auto.
-  eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
-- destruct H1. constructor; auto.
-  eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
-- destruct H1. constructor; auto.
-  eapply add_equation_lessdef with (q := Eq Full r1 l1). eapply add_equations_args_satisf; eauto.
 - discriminate.
 Qed.
 
@@ -475,13 +469,13 @@ Proof.
 Qed.
 
 Lemma remove_equation_res_satisf:
-  forall rs ls r oty ll e e',
-  remove_equations_res r oty ll e = Some e' ->
+  forall rs ls r l e e',
+  remove_equations_res r l e = Some e' ->
   satisf rs ls e -> satisf rs ls e'.
 Proof.
   intros. functional inversion H.
-  apply remove_equation_satisf. apply remove_equation_satisf; auto.
   apply remove_equation_satisf; auto.
+  apply remove_equation_satisf. apply remove_equation_satisf; auto.
 Qed.
 
 Remark select_reg_l_monotone:
@@ -668,50 +662,36 @@ Proof.
 Qed.
 
 Lemma parallel_assignment_satisf_2:
-  forall rs ls res mres' oty e e' v v',
-  let res' := map R mres' in
-  remove_equations_res res oty res' e = Some e' ->
+  forall rs ls res res' e e' v v',
+  remove_equations_res res res' e = Some e' ->
   satisf rs ls e' ->
   reg_unconstrained res e' = true ->
-  forallb (fun l => loc_unconstrained l e') res' = true ->
+  forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true ->
   Val.lessdef v v' ->
-  satisf (rs#res <- v) (Locmap.setlist res' (encode_long oty v') ls) e.
+  satisf (rs#res <- v) (Locmap.setpair res' v' ls) e.
 Proof.
-  intros; red; intros.
-  assert (ISREG: forall l, In l res' -> exists mr, l = R mr).
-  { unfold res'; intros. exploit list_in_map_inv; eauto. intros [mr [A B]]. exists mr; auto. }
-  functional inversion H.
+  intros. functional inversion H.
+- (* One location *)
+  subst. simpl in H2. InvBooleans. simpl. 
+  apply parallel_assignment_satisf with Full; auto.
+  unfold reg_loc_unconstrained. rewrite H1, H4. auto.
 - (* Two 32-bit halves *)
   subst.
-  set (e' := remove_equation {| ekind := Low; ereg := res; eloc := l2 |}
-          (remove_equation {| ekind := High; ereg := res; eloc := l1 |} e)) in *.
-  rewrite <- H5 in H2. simpl in H2. InvBooleans. simpl.
-  destruct (OrderedEquation.eq_dec q (Eq Low res l2)).
-  subst q; simpl. rewrite Regmap.gss.
-  destruct (ISREG l2) as [r2 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+  set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |}
+          (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *.
+  simpl in H2. InvBooleans. simpl.
+  red; intros.
+  destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))).
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. 
   apply Val.loword_lessdef; auto.
-  destruct (OrderedEquation.eq_dec q (Eq High res l1)).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto.
-  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
+  destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))).
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. rewrite Locmap.gss. 
   apply Val.hiword_lessdef; auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
   rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
   eapply loc_unconstrained_sound; eauto.
   eapply loc_unconstrained_sound; eauto.
   eapply reg_unconstrained_sound; eauto.
-- (* One location *)
-  subst. rewrite <- H5 in H2. simpl in H2. InvBooleans.
-  replace (encode_long oty v') with (v' :: nil).
-  set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *.
-  destruct (OrderedEquation.eq_dec q (Eq Full res l1)).
-  subst q; simpl. rewrite Regmap.gss.
-  destruct (ISREG l1) as [r1 EQ]. rewrite <- H5; auto with coqlib. rewrite EQ. rewrite Locmap.gss.
-  auto.
-  assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec.
-  simpl. rewrite Regmap.gso. rewrite Locmap.gso. auto.
-  eapply loc_unconstrained_sound; eauto.
-  eapply reg_unconstrained_sound; eauto.
-  destruct oty as [[]|]; reflexivity || contradiction.
 Qed.
 
 Lemma in_subst_reg:
@@ -1101,21 +1081,20 @@ Proof.
 Qed.
 
 Lemma add_equations_res_lessdef:
-  forall r oty ll e e' rs ls,
-  add_equations_res r oty ll e = Some e' ->
+  forall r oty l e e' rs ls,
+  add_equations_res r oty l e = Some e' ->
   satisf rs ls e' ->
-  Val.lessdef_list (encode_long oty rs#r) (map ls ll).
-Proof.
-  intros. functional inversion H.
-- subst. simpl. constructor.
-  eapply add_equation_lessdef with (q := Eq High r l1).
+  Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) ->
+  Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls).
+Proof.
+  intros. functional inversion H; simpl.
+- subst. eapply add_equation_lessdef with (q := Eq Full r (R mr)); eauto.
+- subst. rewrite <- (val_longofwords_eq rs#r) by auto. 
+  apply Val.longofwords_lessdef.
+  eapply add_equation_lessdef with (q := Eq High r (R mr1)).
   eapply add_equation_satisf. eauto.
-  constructor.
-  eapply add_equation_lessdef with (q := Eq Low r l2). eauto.
-  constructor.
-- subst. replace (encode_long oty rs#r) with (rs#r :: nil). simpl. constructor; auto.
-  eapply add_equation_lessdef with (q := Eq Full r l1); eauto.
-  destruct oty as [[]|]; reflexivity || contradiction.
+  eapply add_equation_lessdef with (q := Eq Low r (R mr2)).
+  eauto.
 Qed.
 
 Definition callee_save_loc (l: loc) :=
@@ -1149,47 +1128,60 @@ Proof.
   lazy beta. destruct (eloc q). auto. destruct sl; congruence.
 Qed.
 
+Lemma val_hiword_longofwords:
+  forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1.
+Proof.
+  intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword.
+  rewrite Int64.hi_ofwords. auto.
+Qed.
+
+Lemma val_loword_longofwords:
+  forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2.
+Proof.
+  intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword.
+  rewrite Int64.lo_ofwords. auto.
+Qed.
+
 Lemma function_return_satisf:
   forall rs ls_before ls_after res res' sg e e' v,
-  res' = map R (loc_result sg) ->
-  remove_equations_res res (sig_res sg) res' e = Some e' ->
+  res' = loc_result sg ->
+  remove_equations_res res res' e = Some e' ->
   satisf rs ls_before e' ->
-  forallb (fun l => reg_loc_unconstrained res l e') res' = true ->
+  forallb (fun l => reg_loc_unconstrained res l e') (map R (regs_of_rpair res')) = true ->
   no_caller_saves e' = true ->
-  Val.lessdef_list (encode_long (sig_res sg) v) (map ls_after res') ->
+  Val.lessdef v (Locmap.getpair (map_rpair R res') ls_after) ->
   agree_callee_save ls_before ls_after ->
   satisf (rs#res <- v) ls_after e.
 Proof.
   intros; red; intros.
   functional inversion H0.
-- subst. rewrite <- H11 in *. unfold encode_long in H4. rewrite <- H7 in H4.
-  simpl in H4. inv H4. inv H14.
-  set (e' := remove_equation {| ekind := Low; ereg := res; eloc := l2 |}
-          (remove_equation {| ekind := High; ereg := res; eloc := l1 |} e)) in *.
-  simpl in H2. InvBooleans.
-  destruct (OrderedEquation.eq_dec q (Eq Low res l2)).
-  subst q; simpl. rewrite Regmap.gss. auto.
-  destruct (OrderedEquation.eq_dec q (Eq High res l1)).
-  subst q; simpl. rewrite Regmap.gss. auto.
-  assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
-  exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B].
-  exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D].
-  rewrite Regmap.gso; auto.
-  exploit no_caller_saves_sound; eauto. intros.
-  red in H5. rewrite <- H5; auto.
-- subst. rewrite <- H11 in *.
-  replace (encode_long (sig_res sg) v) with (v :: nil) in H4.
-  simpl in H4. inv H4.
-  simpl in H2. InvBooleans.
-  set (e' := remove_equation {| ekind := Full; ereg := res; eloc := l1 |} e) in *.
-  destruct (OrderedEquation.eq_dec q (Eq Full res l1)).
+- (* One register *)
+  subst. rewrite <- H8 in *. simpl in *. InvBooleans.
+  set (e' := remove_equation {| ekind := Full; ereg := res; eloc := R mr |} e) in *.
+  destruct (OrderedEquation.eq_dec q (Eq Full res (R mr))).
   subst q; simpl. rewrite Regmap.gss; auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl. ESD.fsetdec.
   exploit reg_loc_unconstrained_sound; eauto. intros [A B].
   rewrite Regmap.gso; auto.
   exploit no_caller_saves_sound; eauto. intros.
   red in H5. rewrite <- H5; auto.
-  destruct (sig_res sg) as [[]|]; reflexivity || contradiction.
+- (* Two 32-bit halves *)
+  subst. rewrite <- H9 in *. simpl in *. 
+  set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |}
+          (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *.
+  InvBooleans.
+  destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))).
+  subst q; simpl. rewrite Regmap.gss.
+  eapply Val.lessdef_trans. apply Val.loword_lessdef. eauto. apply val_loword_longofwords.
+  destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))).
+  subst q; simpl. rewrite Regmap.gss.
+  eapply Val.lessdef_trans. apply Val.hiword_lessdef. eauto. apply val_hiword_longofwords.
+  assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
+  exploit reg_loc_unconstrained_sound. eexact H. eauto. intros [A B].
+  exploit reg_loc_unconstrained_sound. eexact H2. eauto. intros [C D].
+  rewrite Regmap.gso; auto.
+  exploit no_caller_saves_sound; eauto. intros.
+  red in H5. rewrite <- H5; auto.
 Qed.
 
 Lemma compat_left_sound:
@@ -1225,31 +1217,22 @@ Proof.
   exact (select_reg_h_monotone r).
 Qed.
 
-Lemma val_hiword_longofwords:
-  forall v1 v2, Val.lessdef (Val.hiword (Val.longofwords v1 v2)) v1.
-Proof.
-  intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.hiword.
-  rewrite Int64.hi_ofwords. auto.
-Qed.
-
-Lemma val_loword_longofwords:
-  forall v1 v2, Val.lessdef (Val.loword (Val.longofwords v1 v2)) v2.
-Proof.
-  intros. destruct v1; simpl; auto. destruct v2; auto. unfold Val.loword.
-  rewrite Int64.lo_ofwords. auto.
-Qed.
-
 Lemma compat_entry_satisf:
-  forall rl tyl ll e,
-  compat_entry rl tyl ll e = true ->
+  forall rl ll e,
+  compat_entry rl ll e = true ->
   forall vl ls,
-  Val.lessdef_list vl (decode_longs tyl (map ls ll)) ->
+  Val.lessdef_list vl (map (fun p => Locmap.getpair p ls) ll) ->
   satisf (init_regs vl rl) ls e.
 Proof.
-  intros until e. functional induction (compat_entry rl tyl ll e); intros.
+  intros until e. functional induction (compat_entry rl ll e); intros.
 - (* no params *)
   simpl. red; intros. rewrite Regmap.gi. destruct (ekind q); simpl; auto.
-- (* a param of type Tlong *)
+- (* a param in a single location *)
+  InvBooleans. simpl in H0. inv H0. simpl.
+  red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
+  exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
+  eapply IHb; eauto.
+- (* a param split across two locations *)
   InvBooleans. simpl in H0. inv H0. simpl.
   red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
   exploit compat_left2_sound; eauto.
@@ -1259,47 +1242,37 @@ Proof.
   apply Val.lessdef_trans with (Val.loword (Val.longofwords (ls l1) (ls l2))).
   apply Val.loword_lessdef; auto. apply val_loword_longofwords.
   eapply IHb; eauto.
-- (* a param of type Tint *)
-  InvBooleans. simpl in H0. inv H0. simpl.
-  red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
-  exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
-  eapply IHb; eauto.
-- (* a param of type Tfloat *)
-  InvBooleans. simpl in H0. inv H0. simpl.
-  red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
-  exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
-  eapply IHb; eauto.
-- (* a param of type Tsingle *)
-  InvBooleans. simpl in H0. inv H0. simpl.
-  red; intros. rewrite Regmap.gsspec. destruct (peq (ereg q) r1).
-  exploit compat_left_sound; eauto. intros [A B]. rewrite A; rewrite B; auto.
-  eapply IHb; eauto.
 - (* error case *)
   discriminate.
 Qed.
 
 Lemma call_regs_param_values:
   forall sg ls,
-  map (call_regs ls) (loc_parameters sg) = map ls (loc_arguments sg).
+  map (fun p => Locmap.getpair p (call_regs ls)) (loc_parameters sg)
+  = map (fun p => Locmap.getpair p ls) (loc_arguments sg).
 Proof.
   intros. unfold loc_parameters. rewrite list_map_compose.
-  apply list_map_exten; intros. unfold call_regs, parameter_of_argument.
-  exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable.
-  destruct x; auto. destruct sl; tauto.
+  apply list_map_exten; intros. symmetry.
+  assert (A: forall l, loc_argument_acceptable l -> call_regs ls (parameter_of_argument l) = ls l).
+  { destruct l as [r | [] ofs ty]; simpl; auto; contradiction. }
+  exploit loc_arguments_acceptable; eauto. destruct x; simpl; intros.
+- auto.
+- destruct H0; f_equal; auto.
 Qed.
 
 Lemma return_regs_arg_values:
   forall sg ls1 ls2,
   tailcall_is_possible sg = true ->
-  map (return_regs ls1 ls2) (loc_arguments sg) = map ls2 (loc_arguments sg).
-Proof.
-  intros. apply list_map_exten; intros.
-  exploit loc_arguments_acceptable; eauto.
-  exploit tailcall_is_possible_correct; eauto.
-  unfold loc_argument_acceptable, return_regs.
-  destruct x; intros.
-  rewrite H2; auto.
-  contradiction.
+  map (fun p => Locmap.getpair p (return_regs ls1 ls2)) (loc_arguments sg) 
+  = map (fun p => Locmap.getpair p ls2) (loc_arguments sg).
+Proof.
+  intros.
+  apply tailcall_is_possible_correct in H.
+  apply list_map_exten; intros.
+  apply Locmap.getpair_exten; intros.
+  assert (In l (regs_of_rpairs (loc_arguments sg))) by (eapply in_regs_of_rpairs; eauto).
+  exploit loc_arguments_acceptable_2; eauto. exploit H; eauto. 
+  destruct l; simpl; intros; try contradiction. rewrite H4; auto.
 Qed.
 
 Lemma find_function_tailcall:
@@ -1542,7 +1515,7 @@ Inductive transf_function_spec (f: RTL.function) (tf: LTL.function) : Prop :=
       wf_moves mv ->
       transfer f env (pair_codes f tf) (RTL.fn_entrypoint f) an!!(RTL.fn_entrypoint f) = OK e1 ->
       track_moves env mv e1 = Some e2 ->
-      compat_entry (RTL.fn_params f) (sig_args (RTL.fn_sig f)) (loc_parameters (fn_sig tf)) e2 = true ->
+      compat_entry (RTL.fn_params f) (loc_parameters (fn_sig tf)) e2 = true ->
       can_undef destroyed_at_function_entry e2 = true ->
       RTL.fn_stacksize f = LTL.fn_stacksize tf ->
       RTL.fn_sig f = LTL.fn_sig tf ->
@@ -1702,7 +1675,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
         (WTRS: wt_regset env rs)
         (WTRES: env res = proj_sig_res sg)
         (STEPS: forall v ls1 m,
-           Val.lessdef_list (encode_long (sig_res sg) v) (map ls1 (map R (loc_result sg))) ->
+           Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) ->
            Val.has_type v (env res) ->
            agree_callee_save ls ls1 ->
            exists ls2,
@@ -1731,7 +1704,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
       forall s f args m ts tf ls m'
         (STACKS: match_stackframes s ts (funsig tf))
         (FUN: transf_fundef f = OK tf)
-        (ARGS: Val.lessdef_list args (decode_longs (sig_args (funsig tf)) (map ls (loc_arguments (funsig tf)))))
+        (ARGS: Val.lessdef_list args (map (fun p => Locmap.getpair p ls) (loc_arguments (funsig tf))))
         (AG: agree_callee_save (parent_locset ts) ls)
         (MEM: Mem.extends m m')
         (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
@@ -1740,7 +1713,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
   | match_states_return:
       forall s res m ts ls m' sg
         (STACKS: match_stackframes s ts sg)
-        (RES: Val.lessdef_list (encode_long (sig_res sg) res) (map ls (map R (loc_result sg))))
+        (RES: Val.lessdef res (Locmap.getpair (map_rpair R (loc_result sg)) ls))
         (AG: agree_callee_save (parent_locset ts) ls)
         (MEM: Mem.extends m m')
         (WTRES: Val.has_type res (proj_sig_res sg)),
@@ -2089,7 +2062,7 @@ Proof.
 (* call *)
 - set (sg := RTL.funsig fd) in *.
   set (args' := loc_arguments sg) in *.
-  set (res' := map R (loc_result sg)) in *.
+  set (res' := loc_result sg) in *.
   exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
   exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto.
   intros [tfd [E F]].
@@ -2203,7 +2176,6 @@ Proof.
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
   simpl. econstructor; eauto.
-  unfold encode_long, loc_result. rewrite <- H11; rewrite H13. simpl; auto.
   apply return_regs_agree_callee_save.
   constructor.
 + (* with an argument *)
@@ -2213,11 +2185,15 @@ Proof.
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
   simpl. econstructor; eauto. rewrite <- H11.
-  replace (map (return_regs (parent_locset ts) ls1) (map R (loc_result (RTL.fn_sig f))))
-     with (map ls1 (map R (loc_result (RTL.fn_sig f)))).
+  replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f)))
+                          (return_regs (parent_locset ts) ls1))
+  with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1).
   eapply add_equations_res_lessdef; eauto.
-  rewrite !list_map_compose. apply list_map_exten; intros.
-  unfold return_regs. erewrite loc_result_caller_save by eauto. auto.
+  rewrite H13. apply WTRS.
+  generalize (loc_result_caller_save (RTL.fn_sig f)). 
+  destruct (loc_result (RTL.fn_sig f)); simpl.
+  intros A; rewrite A; auto.
+  intros [A B]; rewrite A, B; auto.
   apply return_regs_agree_callee_save.
   unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS.
 
@@ -2230,7 +2206,7 @@ Proof.
   { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. }
   exploit (exec_moves mv). eauto. eauto.
     eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto.
-    rewrite call_regs_param_values. rewrite H9. eexact ARGS.
+    rewrite call_regs_param_values. eexact ARGS.
     exact WTRS.
   intros [ls1 [A B]].
   econstructor; split.
@@ -2246,22 +2222,20 @@ Proof.
   simpl in FUN; inv FUN.
   econstructor; split.
   apply plus_one. econstructor; eauto.
-  eapply external_call_symbols_preserved' with (ge1 := ge).
-  econstructor; eauto. apply senv_preserved.
-  econstructor; eauto. simpl.
-  replace (map
-           (Locmap.setlist (map R (loc_result (ef_sig ef)))
-                (encode_long (sig_res (ef_sig ef)) v') ls)
-           (map R (loc_result (ef_sig ef))))
-  with (encode_long (sig_res (ef_sig ef)) v').
-  apply encode_long_lessdef; auto.
-  unfold encode_long, loc_result.
-  destruct (sig_res (ef_sig ef)) as [[]|]; simpl; symmetry; f_equal; auto.
-  red; intros. rewrite Locmap.gsetlisto. apply AG; auto.
-  apply Loc.notin_iff. intros.
-  exploit list_in_map_inv; eauto. intros [r [A B]]; subst l'.
-  destruct l; simpl; auto. red in H0. apply loc_result_caller_save in B. congruence.
-  simpl. eapply external_call_well_typed; eauto.
+  eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved.
+  econstructor; eauto. 
+  simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl.
+  rewrite Locmap.gss; auto.
+  generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D). 
+  exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'.
+  rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. 
+  rewrite val_longofwords_eq by auto. auto.
+  red; intros. rewrite (AG l H0).
+  symmetry; apply Locmap.gpo. 
+  assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
+  { intros. destruct l; simpl in *. congruence. auto. }
+  generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto.
+  eapply external_call_well_typed; eauto.
 
 (* return *)
 - inv STACKS.
@@ -2287,7 +2261,7 @@ Proof.
   congruence.
   constructor; auto.
   constructor. rewrite SIG; rewrite H3; auto.
-  rewrite SIG; rewrite H3; simpl; auto.
+  rewrite SIG, H3, loc_arguments_main. auto.
   red; auto.
   apply Mem.extends_refl.
   rewrite SIG, H3. constructor.
@@ -2297,9 +2271,9 @@ Lemma final_states_simulation:
   forall st1 st2 r,
   match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv STACKS.
-  econstructor. simpl; reflexivity.
-  unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. inv H3; auto.
+  intros. inv H0. inv H. inv STACKS. 
+  econstructor.
+  unfold loc_result in RES; rewrite H in RES. simpl in RES. inv RES. auto. 
 Qed.
  
 Lemma wt_prog: wt_program prog.
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index cc27bd55..30d6990e 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -145,19 +145,6 @@ Proof.
   rewrite preg_notin_charact in H. auto.
 Qed.
 
-Lemma set_pregs_other_2:
-  forall r rl vl rs,
-  preg_notin r rl ->
-  set_regs (map preg_of rl) vl rs r = rs r.
-Proof.
-  induction rl; simpl; intros.
-  auto.
-  destruct vl; auto.
-  assert (r <> preg_of a) by (destruct rl; tauto).
-  assert (preg_notin r rl) by (destruct rl; simpl; tauto).
-  rewrite IHrl by auto. apply Pregmap.gso; auto.
-Qed.
-
 (** * Agreement between Mach registers and processor registers *)
 
 Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
@@ -230,6 +217,15 @@ Proof.
   red; intros; elim n. eapply preg_of_injective; eauto.
 Qed.
 
+Corollary agree_set_mreg_parallel:
+  forall ms sp rs r v v',
+  agree ms sp rs ->
+  Val.lessdef v v' ->
+  agree (Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs).
+Proof.
+  intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto.
+Qed.
+
 Lemma agree_set_other:
   forall ms sp rs r v,
   agree ms sp rs ->
@@ -247,18 +243,16 @@ Proof.
   intros. unfold nextinstr. apply agree_set_other. auto. auto.
 Qed.
 
-Lemma agree_set_mregs:
-  forall sp rl vl vl' ms rs,
+Lemma agree_set_pair:
+  forall sp p v v' ms rs,
   agree ms sp rs ->
-  Val.lessdef_list vl vl' ->
-  agree (Mach.set_regs rl vl ms) sp (set_regs (map preg_of rl) vl' rs).
+  Val.lessdef v v' ->
+  agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
 Proof.
-  induction rl; simpl; intros.
-  auto.
-  inv H0. auto. apply IHrl; auto.
-  eapply agree_set_mreg. eexact H.
-  rewrite Pregmap.gss. auto.
-  intros. apply Pregmap.gso; auto.
+  intros. destruct p; simpl.
+- apply agree_set_mreg_parallel; auto.
+- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
+  apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
 Qed.
 
 Lemma agree_undef_nondata_regs:
@@ -333,15 +327,29 @@ Proof.
   econstructor. eauto. assumption.
 Qed.
 
+Lemma extcall_arg_pair_match:
+  forall ms sp rs m m' p v,
+  agree ms sp rs ->
+  Mem.extends m m' ->
+  Mach.extcall_arg_pair ms m sp p v ->
+  exists v', Asm.extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
+Proof.
+  intros. inv H1.
+- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
+- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
+  exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
+  exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. 
+Qed.
+
 Lemma extcall_args_match:
   forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
   forall ll vl,
-  list_forall2 (Mach.extcall_arg ms m sp) ll vl ->
-  exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'.
+  list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl ->
+  exists vl', list_forall2 (Asm.extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'.
 Proof.
   induction 3; intros.
   exists (@nil val); split. constructor. constructor.
-  exploit extcall_arg_match; eauto. intros [v1' [A B]].
+  exploit extcall_arg_pair_match; eauto. intros [v1' [A B]].
   destruct IHlist_forall2 as [vl' [C D]].
   exists (v1' :: vl'); split; constructor; auto.
 Qed.
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index a498a654..e92be2b4 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -315,7 +315,7 @@ Proof.
   econstructor; eauto with coqlib.
 (* external function *)
   left; econstructor; split.
-  econstructor; eauto. eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+  econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto with coqlib.
 (* return *)
   inv H3. inv H1. left; econstructor; split.
@@ -341,7 +341,7 @@ Lemma transf_final_states:
   forall st1 st2 r,
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H6. econstructor; eauto.
+  intros. inv H0. inv H. inv H5. econstructor; eauto.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/Conventions.v b/backend/Conventions.v
index 69cdd07d..64a83a58 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -22,6 +22,18 @@ Require Export Conventions1.
     [arch/abi/Conventions1.v].  This file adds various processor-independent
     definitions and lemmas. *)
 
+Lemma loc_arguments_acceptable_2:
+  forall s l,
+  In l (regs_of_rpairs (loc_arguments s)) -> loc_argument_acceptable l.
+Proof.
+  intros until l. generalize (loc_arguments_acceptable s). generalize (loc_arguments s).
+  induction l0 as [ | p pl]; simpl; intros.
+- contradiction.
+- rewrite in_app_iff in H0. destruct H0.
+  exploit H; eauto. destruct p; simpl in *; intuition congruence.
+  apply IHpl; auto.
+Qed.
+  
 (** ** Location of function parameters *)
 
 (** A function finds the values of its parameter in the same locations
@@ -35,22 +47,25 @@ Definition parameter_of_argument (l: loc) : loc :=
   | _ => l
   end.
 
-Definition loc_parameters (s: signature) :=
-  List.map parameter_of_argument (loc_arguments s).
+Definition loc_parameters (s: signature) : list (rpair loc) :=
+  List.map (map_rpair parameter_of_argument) (loc_arguments s).
 
 Lemma incoming_slot_in_parameters:
   forall ofs ty sg,
-  In (S Incoming ofs ty) (loc_parameters sg) ->
-  In (S Outgoing ofs ty) (loc_arguments sg).
+  In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters sg)) ->
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)).
 Proof.
   intros.
-  unfold loc_parameters in H.
+  replace (regs_of_rpairs (loc_parameters sg)) with (List.map parameter_of_argument (regs_of_rpairs (loc_arguments sg))) in H.
   change (S Incoming ofs ty) with (parameter_of_argument (S Outgoing ofs ty)) in H.
   exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
-  exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
+  exploit loc_arguments_acceptable_2; eauto. unfold loc_argument_acceptable; intros.
   destruct x; simpl in A; try discriminate.
   destruct sl; try contradiction.
   inv A. auto.
+  unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros.
+  auto.
+  rewrite map_app. f_equal; auto. destruct p; auto. 
 Qed.
 
 (** * Tail calls *)
@@ -62,34 +77,27 @@ Qed.
     arguments are all passed in registers. *)
 
 Definition tailcall_possible (s: signature) : Prop :=
-  forall l, In l (loc_arguments s) ->
+  forall l, In l (regs_of_rpairs (loc_arguments s)) ->
   match l with R _ => True | S _ _ _ => False end.
 
 (** Decide whether a tailcall is possible. *)
 
 Definition tailcall_is_possible (sg: signature) : bool :=
-  let fix tcisp (l: list loc) :=
-    match l with
-    | nil => true
-    | R _ :: l' => tcisp l'
-    | S _ _ _ :: l' => false
-    end
-  in tcisp (loc_arguments sg).
+  List.forallb
+    (fun l => match l with R _ => true | S _ _ _ => false end)
+    (regs_of_rpairs (loc_arguments sg)).
 
 Lemma tailcall_is_possible_correct:
   forall s, tailcall_is_possible s = true -> tailcall_possible s.
 Proof.
-  intro s. unfold tailcall_is_possible, tailcall_possible.
-  generalize (loc_arguments s). induction l; simpl; intros.
-  elim H0.
-  destruct a.
-  destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
+  unfold tailcall_is_possible; intros. rewrite forallb_forall in H. 
+  red; intros. apply H in H0. destruct l; [auto|discriminate]. 
 Qed.
 
 Lemma zero_size_arguments_tailcall_possible:
   forall sg, size_arguments sg = 0 -> tailcall_possible sg.
 Proof.
-  intros; red; intros. exploit loc_arguments_acceptable; eauto.
+  intros; red; intros. exploit loc_arguments_acceptable_2; eauto.
   unfold loc_argument_acceptable.
   destruct l; intros. auto. destruct sl; try contradiction. destruct H1.
   generalize (loc_arguments_bounded _ _ _ H0).
diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index 110c0f26..0b8ff3c7 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -518,7 +518,7 @@ Proof.
 - (* external function *)
   monadInv H8. econstructor; split.
   apply plus_one. econstructor; eauto.
-  eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   constructor; auto.
 - (* return *)
   inv H3. inv H1.
@@ -544,7 +544,7 @@ Lemma transf_final_states:
   forall st1 st2 r,
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H6. econstructor; eauto.
+  intros. inv H0. inv H. inv H5. econstructor; eauto.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/LTL.v b/backend/LTL.v
index bb596fa2..5f7116ae 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -266,9 +266,9 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate s (Internal f) rs m)
         E0 (State s f (Vptr sp Int.zero) f.(fn_entrypoint) rs' m')
   | exec_function_external: forall s ef t args res rs m rs' m',
-      args = map rs (loc_arguments (ef_sig ef)) ->
-      external_call' ef ge args m t res m' ->
-      rs' = Locmap.setlist (map R (loc_result (ef_sig ef))) res rs ->
+      args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) ->
+      external_call ef ge args m t res m' ->
+      rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs ->
       step (Callstate s (External ef) rs m)
          t (Returnstate s rs' m')
   | exec_return: forall f sp rs1 bb s rs m,
@@ -292,9 +292,8 @@ Inductive initial_state (p: program): state -> Prop :=
       initial_state p (Callstate nil f (Locmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r retcode,
-      loc_result signature_main = r :: nil ->
-      rs (R r) = Vint retcode ->
+  | final_state_intro: forall rs m retcode,
+      Locmap.getpair (map_rpair R (loc_result signature_main)) rs = Vint retcode ->
       final_state (Returnstate nil rs m) retcode.
 
 Definition semantics (p: program) :=
diff --git a/backend/Linear.v b/backend/Linear.v
index 8c91a809..da1b4c04 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -246,9 +246,9 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs' m')
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
-      args = map rs1 (loc_arguments (ef_sig ef)) ->
-      external_call' ef ge args m t res m' ->
-      rs2 = Locmap.setlist (map R (loc_result (ef_sig ef))) res rs1 ->
+      args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) ->
+      external_call ef ge args m t res m' ->
+      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 ->
       step (Callstate s (External ef) rs1 m)
          t (Returnstate s rs2 m')
   | exec_return:
@@ -268,9 +268,8 @@ Inductive initial_state (p: program): state -> Prop :=
       initial_state p (Callstate nil f (Locmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r retcode,
-      loc_result signature_main = r :: nil ->
-      rs (R r) = Vint retcode ->
+  | final_state_intro: forall rs m retcode,
+      Locmap.getpair (map_rpair R (loc_result signature_main)) rs = Vint retcode ->
       final_state (Returnstate nil rs m) retcode.
 
 Definition semantics (p: program) :=
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 16717365..10a3d8b2 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -694,7 +694,7 @@ Proof.
   (* external function *)
   monadInv H8. left; econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 
   (* return *)
@@ -722,7 +722,7 @@ Lemma transf_final_states:
   forall st1 st2 r,
   match_states st1 st2 -> LTL.final_state st1 r -> Linear.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H6. econstructor; eauto.
+  intros. inv H0. inv H. inv H5. econstructor; eauto.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 50cd16d6..123c6b5a 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -37,7 +37,7 @@ Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
   match sl with
   | Local => zle 0 ofs
   | Outgoing => zle 0 ofs
-  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (loc_parameters funct.(fn_sig))
+  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
   end
   && Zdivide_dec (typealign ty) ofs (typealign_pos ty).
 
@@ -155,15 +155,19 @@ Proof.
   red; intros. unfold Locmap.init. red; auto.
 Qed.
 
-Lemma wt_setlist:
-  forall vl rl rs,
-  Val.has_type_list vl (map mreg_type rl) ->
+Lemma wt_setpair:
+  forall sg v rs,
+  Val.has_type v (proj_sig_res sg) ->
   wt_locset rs ->
-  wt_locset (Locmap.setlist (map R rl) vl rs).
+  wt_locset (Locmap.setpair (loc_result sg) v rs).
 Proof.
-  induction vl; destruct rl; simpl; intros; try contradiction.
+  intros. generalize (loc_result_pair sg) (loc_result_type sg).
+  destruct (loc_result sg); simpl Locmap.setpair.
+- intros. apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+- intros (A & B & C & D) E. 
+  apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
+  apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
   auto.
-  destruct H. apply IHvl; auto. apply wt_setreg; auto.
 Qed.
 
 Lemma wt_setres:
@@ -334,8 +338,8 @@ Proof.
   econstructor. eauto. eauto. eauto.
   apply wt_undef_regs. apply wt_call_regs. auto.
 - (* external function *)
-  econstructor. auto. apply wt_setlist; auto.
-  eapply Val.has_subtype_list. apply loc_result_type. eapply external_call_well_typed'; eauto.
+  econstructor. auto. apply wt_setpair; auto.
+  eapply external_call_well_typed; eauto.
 - (* return *)
   inv WTSTK. econstructor; eauto.
 Qed.
diff --git a/backend/Locations.v b/backend/Locations.v
index 6ca84ea7..52abfc46 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -386,17 +386,35 @@ Module Locmap.
     auto.
   Qed.
 
-  Fixpoint setlist (ll: list loc) (vl: list val) (m: t) {struct ll} : t :=
-    match ll, vl with
-    | l1 :: ls, v1 :: vs => setlist ls vs (set l1 v1 m)
-    | _, _ => m
+  Definition getpair (p: rpair loc) (m: t) : val :=
+    match p with
+    | One l => m l
+    | Twolong l1 l2 => Val.longofwords (m l1) (m l2)
     end.
 
-  Lemma gsetlisto: forall l ll vl m, Loc.notin l ll -> (setlist ll vl m) l = m l.
+  Definition setpair (p: rpair mreg) (v: val) (m: t) : t :=
+    match p with
+    | One r => set (R r) v m
+    | Twolong hi lo => set (R lo) (Val.loword  v) (set (R hi) (Val.hiword v) m)
+    end.
+
+  Lemma getpair_exten:
+    forall p ls1 ls2,
+    (forall l, In l (regs_of_rpair p) -> ls2 l = ls1 l) ->
+    getpair p ls2 = getpair p ls1.
   Proof.
-    induction ll; simpl; intros.
-    auto.
-    destruct vl; auto. destruct H. rewrite IHll; auto. apply gso; auto. apply Loc.diff_sym; auto.
+    intros. destruct p; simpl. 
+    apply H; simpl; auto.
+    f_equal; apply H; simpl; auto.
+  Qed.
+
+  Lemma gpo:
+    forall p v m l,
+    forall_rpair (fun r => Loc.diff l (R r)) p -> setpair p v m l = m l.
+  Proof.
+    intros; destruct p; simpl in *. 
+  - apply gso. apply Loc.diff_sym; auto.
+  - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto.
   Qed.
 
   Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t :=
diff --git a/backend/Mach.v b/backend/Mach.v
index 739c8212..3e15c97c 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -156,10 +156,10 @@ Proof.
   unfold Regmap.set. destruct (RegEq.eq r a); auto.
 Qed.
 
-Fixpoint set_regs (rl: list mreg) (vl: list val) (rs: regset) : regset :=
-  match rl, vl with
-  | r1 :: rl', v1 :: vl' => set_regs rl' vl' (Regmap.set r1 v1 rs)
-  | _, _ => rs
+Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset :=
+  match p with
+  | One r => rs#r <- v
+  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
   end.
 
 Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset :=
@@ -216,16 +216,25 @@ Definition find_function_ptr
 
 (** Extract the values of the arguments to an external call. *)
 
-Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop :=
-  | extcall_arg_reg: forall rs m sp r,
+Inductive extcall_arg (rs: regset) (m: mem) (sp: val): loc -> val -> Prop :=
+  | extcall_arg_reg: forall r,
       extcall_arg rs m sp (R r) (rs r)
-  | extcall_arg_stack: forall rs m sp ofs ty v,
+  | extcall_arg_stack: forall ofs ty v,
       load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v ->
       extcall_arg rs m sp (S Outgoing ofs ty) v.
 
+Inductive extcall_arg_pair (rs: regset) (m: mem) (sp: val): rpair loc -> val -> Prop :=
+  | extcall_arg_one: forall l v,
+      extcall_arg rs m sp l v ->
+      extcall_arg_pair rs m sp (One l) v
+  | extcall_arg_twolong: forall hi lo vhi vlo,
+      extcall_arg rs m sp hi vhi ->
+      extcall_arg rs m sp lo vlo ->
+      extcall_arg_pair rs m sp (Twolong hi lo) (Val.longofwords vhi vlo).
+
 Definition extcall_arguments
     (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
-  list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args.
+  list_forall2 (extcall_arg_pair rs m sp) (loc_arguments sg) args.
 
 (** Mach execution states. *)
 
@@ -391,8 +400,8 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s fb rs m t rs' ef args res m',
       Genv.find_funct_ptr ge fb = Some (External ef) ->
       extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
-      external_call' ef ge args m t res m' ->
-      rs' = set_regs (loc_result (ef_sig ef)) res rs ->
+      external_call ef ge args m t res m' ->
+      rs' = set_pair (loc_result (ef_sig ef)) res rs ->
       step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
@@ -411,7 +420,7 @@ Inductive initial_state (p: program): state -> Prop :=
 
 Inductive final_state: state -> int -> Prop :=
   | final_state_intro: forall rs m r retcode,
-      loc_result signature_main = r :: nil ->
+      loc_result signature_main = One r ->
       rs r = Vint retcode ->
       final_state (Returnstate nil rs m) retcode.
 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 57fc8b86..dec1b988 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -693,10 +693,8 @@ Proof.
   rewrite A; simpl; rewrite C; simpl.
   rewrite H2; rewrite dec_eq_true.
   replace (tailcall_is_possible sig) with true; auto.
-  revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig).
-  induction l; simpl; intros. auto.
-  exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl.
-  intros; apply H3; auto.
+  symmetry. unfold tailcall_is_possible. apply forallb_forall. 
+  intros. apply H3 in H4. destruct x; intuition auto.
 - (* builtin *)
   exploit type_builtin_args_complete; eauto. instantiate (1 := args). intros [e1 [A B]].
   exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]].
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 3432b79d..e6e07339 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -70,13 +70,6 @@ let vreg tyenv r = V(r, tyenv r)
 
 let vregs tyenv rl = List.map (vreg tyenv) rl
 
-let rec expand_regs tyenv = function
-  | [] -> []
-  | r :: rl ->
-      match tyenv r with
-      | Tlong -> V(r, Tint) :: V(twin_reg r, Tint) :: expand_regs tyenv rl
-      | ty    -> V(r, ty) :: expand_regs tyenv rl
-
 let constrain_reg v c =
   match c with
   | None -> v
@@ -105,12 +98,47 @@ let rec movelist vl1 vl2 k =
   | v1 :: vl1, v2 :: vl2 -> move v1 v2 (movelist vl1 vl2 k)
   | _, _ -> assert false
 
-let xparmove srcs dsts k =
+let parmove_regs2locs tyenv srcs dsts k =
   assert (List.length srcs = List.length dsts);
-  match srcs, dsts with
+  let rec expand srcs' dsts' rl ll =
+    match rl, ll with
+    | [], [] -> (srcs', dsts')
+    | r :: rl, One l :: ll ->
+        let ty = tyenv r in
+        expand (V(r, ty) :: srcs') (L l :: dsts') rl ll
+    | r :: rl, Twolong(l1, l2) :: ll ->
+        assert (tyenv r = Tlong);
+        expand (V(r, Tint) :: V(twin_reg r, Tint) :: srcs')
+               (L l1 :: L l2 :: dsts')
+               rl ll
+    | _, _ ->
+        assert false in
+  let (srcs', dsts') = expand [] [] srcs dsts in
+  match srcs', dsts' with
+  | [], [] -> k
+  | [src], [dst] -> move src dst k
+  | _, _ -> Xparmove(srcs', dsts', new_temp Tint, new_temp Tfloat) :: k
+
+let parmove_locs2regs tyenv srcs dsts k =
+  assert (List.length srcs = List.length dsts);
+  let rec expand srcs' dsts' ll rl =
+    match ll, rl with
+    | [], [] -> (srcs', dsts')
+    | One l :: ll, r :: rl ->
+        let ty = tyenv r in
+        expand (L l :: srcs') (V(r, ty) :: dsts') ll rl
+    | Twolong(l1, l2) :: ll, r :: rl ->
+        assert (tyenv r = Tlong);
+        expand (L l1 :: L l2 :: srcs')
+               (V(r, Tint) :: V(twin_reg r, Tint) :: dsts')
+               ll rl
+    | _, _ ->
+        assert false in
+  let (srcs', dsts') = expand [] [] srcs dsts in
+  match srcs', dsts' with
   | [], [] -> k
   | [src], [dst] -> move src dst k
-  | _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k
+  | _, _ -> Xparmove(srcs', dsts', new_temp Tint, new_temp Tfloat) :: k
 
 let rec convert_builtin_arg tyenv = function
   | BA r ->
@@ -228,16 +256,17 @@ let block_of_RTL_instr funsig tyenv = function
       end else
         [Xstore(chunk, addr, vregs tyenv args, vreg tyenv src); Xbranch s]
   | RTL.Icall(sg, ros, args, res, s) ->
-      let args' = vlocs (loc_arguments sg)
-      and res' = vmregs (loc_result sg) in
-      xparmove (expand_regs tyenv args) args'
-       (Xcall(sg, sum_left_map (vreg tyenv) ros, args', res') ::
-         xparmove res' (expand_regs tyenv [res])
+      let args' = loc_arguments sg
+      and res' = [map_rpair (fun r -> R r) (loc_result sg)] in
+      parmove_regs2locs tyenv args args'
+       (Xcall(sg, sum_left_map (vreg tyenv) ros,
+              vlocpairs args', vlocpairs res') ::
+         parmove_locs2regs tyenv res' [res]
            [Xbranch s])
   | RTL.Itailcall(sg, ros, args) ->
-      let args' = vlocs (loc_arguments sg) in
-      xparmove (expand_regs tyenv args) args'
-        [Xtailcall(sg, sum_left_map (vreg tyenv) ros, args')]
+      let args' = loc_arguments sg in
+      parmove_regs2locs tyenv args args'
+        [Xtailcall(sg, sum_left_map (vreg tyenv) ros, vlocpairs args')]
   | RTL.Ibuiltin(ef, args, res, s) ->
       let (cargs, cres) = mregs_for_builtin ef in
       let args1 = List.map (convert_builtin_arg tyenv) args
@@ -255,8 +284,8 @@ let block_of_RTL_instr funsig tyenv = function
   | RTL.Ireturn None ->
       [Xreturn []]
   | RTL.Ireturn (Some arg) ->
-      let args' = vmregs (loc_result funsig) in
-      xparmove (expand_regs tyenv [arg]) args' [Xreturn args']
+      let args' = [map_rpair (fun r -> R r) (loc_result funsig)] in
+      parmove_regs2locs tyenv [arg] args' [Xreturn (vlocpairs args')]
 
 (* One above the [pc] nodes of the given RTL function *)
 
@@ -272,8 +301,9 @@ let function_of_RTL_function f tyenv =
   (* Add moves for function parameters *)
   let pc_entrypoint = next_pc f in
   let b_entrypoint =
-     xparmove (vlocs (loc_parameters f.RTL.fn_sig))
-              (expand_regs tyenv f.RTL.fn_params)
+    parmove_locs2regs tyenv
+              (loc_parameters f.RTL.fn_sig)
+              f.RTL.fn_params
               [Xbranch f.RTL.fn_entrypoint] in
   { fn_sig = f.RTL.fn_sig;
     fn_stacksize = f.RTL.fn_stacksize;
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 15953131..da024a25 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -54,9 +54,9 @@ Qed.
 
 Lemma slot_outgoing_argument_valid:
   forall f ofs ty sg,
-  In (S Outgoing ofs ty) (loc_arguments sg) -> slot_valid f Outgoing ofs ty = true.
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) -> slot_valid f Outgoing ofs ty = true.
 Proof.
-  intros. exploit loc_arguments_acceptable; eauto. intros [A B].
+  intros. exploit loc_arguments_acceptable_2; eauto. intros [A B].
   unfold slot_valid. unfold proj_sumbool.
   rewrite zle_true by omega.
   rewrite pred_dec_true by auto.
@@ -511,12 +511,14 @@ Local Opaque sepconj.
 - apply frame_set_reg; auto. 
 Qed.
 
-Corollary frame_set_regs:
-  forall j sp ls0 parent retaddr m P rl vl ls,
+Corollary frame_set_regpair:
+  forall j sp ls0 parent retaddr m P p v ls,
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
-  m |= frame_contents j sp (Locmap.setlist (map R rl) vl ls) ls0 parent retaddr ** P.
+  m |= frame_contents j sp (Locmap.setpair p v ls) ls0 parent retaddr ** P.
 Proof.
-  induction rl; destruct vl; simpl; intros; trivial. apply IHrl. apply frame_set_reg; auto.
+  intros. destruct p; simpl.
+  apply frame_set_reg; auto.
+  apply frame_set_reg; apply frame_set_reg; auto.
 Qed.
 
 Corollary frame_set_res:
@@ -565,7 +567,7 @@ Record agree_locs (ls ls0: locset) : Prop :=
         corresponding Outgoing stack slots in the caller *)
     agree_incoming:
        forall ofs ty,
-       In (S Incoming ofs ty) (loc_parameters f.(Linear.fn_sig)) ->
+       In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters f.(Linear.fn_sig))) ->
        ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty)
 }.
 
@@ -614,16 +616,16 @@ Proof.
   rewrite Locmap.gso; auto. red. auto.
 Qed.
 
-Lemma agree_regs_set_regs:
-  forall j rl vl vl' ls rs,
+Lemma agree_regs_set_pair:
+  forall j p v v' ls rs,
   agree_regs j ls rs ->
-  Val.inject_list j vl vl' ->
-  agree_regs j (Locmap.setlist (map R rl) vl ls) (set_regs rl vl' rs).
+  Val.inject j v v' ->
+  agree_regs j (Locmap.setpair p v ls) (set_pair p v' rs).
 Proof.
-  induction rl; simpl; intros.
-  auto.
-  inv H0. auto.
-  apply IHrl; auto. apply agree_regs_set_reg; auto.
+  intros. destruct p; simpl.
+- apply agree_regs_set_reg; auto.
+- apply agree_regs_set_reg. apply agree_regs_set_reg; auto. 
+  apply Val.hiword_inject; auto. apply Val.loword_inject; auto.
 Qed.
 
 Lemma agree_regs_set_res:
@@ -706,14 +708,25 @@ Proof.
   rewrite Locmap.gso. auto. red. intuition congruence.
 Qed.
 
-Lemma agree_locs_set_regs:
-  forall ls0 rl vl ls,
+Lemma caller_save_reg_within_bounds:
+  forall r,
+  is_callee_save r = false -> mreg_within_bounds b r.
+Proof.
+  intros; red; intros. congruence.
+Qed.
+
+Lemma agree_locs_set_pair:
+  forall ls0 p v ls,
   agree_locs ls ls0 ->
-  (forall r, In r rl -> mreg_within_bounds b r) ->
-  agree_locs (Locmap.setlist (map R rl) vl ls) ls0.
+  forall_rpair (fun r => is_callee_save r = false) p ->
+  agree_locs (Locmap.setpair p v ls) ls0.
 Proof.
-  induction rl; destruct vl; simpl; intros; auto.
-  apply IHrl; auto. apply agree_locs_set_reg; auto.
+  intros.
+  destruct p; simpl in *.
+  apply agree_locs_set_reg; auto. apply caller_save_reg_within_bounds; auto.
+  destruct H0.
+  apply agree_locs_set_reg; auto. apply agree_locs_set_reg; auto.
+  apply caller_save_reg_within_bounds; auto. apply caller_save_reg_within_bounds; auto. 
 Qed.
 
 Lemma agree_locs_set_res:
@@ -739,13 +752,6 @@ Proof.
   apply agree_locs_set_reg; auto.
 Qed.
 
-Lemma caller_save_reg_within_bounds:
-  forall r,
-  is_callee_save r = false -> mreg_within_bounds b r.
-Proof.
-  intros; red; intros. congruence.
-Qed.
-
 Lemma agree_locs_undef_locs_1:
   forall ls0 regs ls,
   agree_locs ls ls0 ->
@@ -819,19 +825,14 @@ Proof.
 Qed.
 
 Lemma agree_callee_save_set_result:
-  forall sg vl ls1 ls2,
+  forall sg v ls1 ls2,
   agree_callee_save ls1 ls2 ->
-  agree_callee_save (Locmap.setlist (map R (loc_result sg)) vl ls1) ls2.
+  agree_callee_save (Locmap.setpair (loc_result sg) v ls1) ls2.
 Proof.
-  intros sg. generalize (loc_result_caller_save sg).
-  generalize (loc_result sg).
-  induction l; simpl; intros.
-  auto.
-  destruct vl; auto.
-  apply IHl; auto.
-  red; intros. rewrite Locmap.gso. apply H0; auto.
-  destruct l0; simpl; auto. red; intros; subst a. 
-  assert (is_callee_save r = false) by auto. congruence. 
+  intros; red; intros. rewrite Locmap.gpo. apply H; auto. 
+  assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
+  { intros. destruct l; auto. simpl; congruence. }
+  generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto.
 Qed.
 
 (** ** Properties of destroyed registers. *)
@@ -1355,7 +1356,7 @@ Inductive match_stacks (j: meminj):
         (TY_RA: Val.has_type ra Tint)
         (AGL: agree_locs f ls (parent_locset cs))
         (ARGS: forall ofs ty,
-           In (S Outgoing ofs ty) (loc_arguments sg) ->
+           In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) ->
            slot_within_bounds (function_bounds f) Outgoing ofs ty)
         (STK: match_stacks j cs cs' (Linear.fn_sig f)),
       match_stacks j
@@ -1617,11 +1618,11 @@ Hypothesis SEP: m' |= stack_contents j cs cs'.
 
 Lemma transl_external_argument:
   forall l,
-  In l (loc_arguments sg) ->
+  In l (regs_of_rpairs (loc_arguments sg)) ->
   exists v, extcall_arg rs m' (parent_sp cs') l v /\ Val.inject j (ls l) v.
 Proof.
   intros.
-  assert (loc_argument_acceptable l) by (apply loc_arguments_acceptable with sg; auto).
+  assert (loc_argument_acceptable l) by (apply loc_arguments_acceptable_2 with sg; auto).
   destruct l; red in H0.
 - exists (rs r); split. constructor. auto.
 - destruct sl; try contradiction.
@@ -1637,23 +1638,39 @@ Proof.
   constructor. exact A. red in AGCS. rewrite AGCS; auto.
 Qed.
 
+Lemma transl_external_argument_2:
+  forall p,
+  In p (loc_arguments sg) ->
+  exists v, extcall_arg_pair rs m' (parent_sp cs') p v /\ Val.inject j (Locmap.getpair p ls) v.
+Proof.
+  intros. destruct p as [l | l1 l2].
+- destruct (transl_external_argument l) as (v & A & B). eapply in_regs_of_rpairs; eauto; simpl; auto.
+  exists v; split; auto. constructor; auto. 
+- destruct (transl_external_argument l1) as (v1 & A1 & B1). eapply in_regs_of_rpairs; eauto; simpl; auto.
+  destruct (transl_external_argument l2) as (v2 & A2 & B2). eapply in_regs_of_rpairs; eauto; simpl; auto.
+  exists (Val.longofwords v1 v2); split. 
+  constructor; auto.
+  apply Val.longofwords_inject; auto.
+Qed.
+
 Lemma transl_external_arguments_rec:
   forall locs,
   incl locs (loc_arguments sg) ->
   exists vl,
-  list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ Val.inject_list j ls##locs vl.
+      list_forall2 (extcall_arg_pair rs m' (parent_sp cs')) locs vl
+   /\ Val.inject_list j (map (fun p => Locmap.getpair p ls) locs) vl.
 Proof.
   induction locs; simpl; intros.
   exists (@nil val); split. constructor. constructor.
-  exploit transl_external_argument; eauto with coqlib. intros [v [A B]].
+  exploit transl_external_argument_2; eauto with coqlib. intros [v [A B]].
   exploit IHlocs; eauto with coqlib. intros [vl [C D]].
   exists (v :: vl); split; constructor; auto.
 Qed.
 
 Lemma transl_external_arguments:
   exists vl,
-  extcall_arguments rs m' (parent_sp cs') sg vl /\
-  Val.inject_list j (ls ## (loc_arguments sg)) vl.
+      extcall_arguments rs m' (parent_sp cs') sg vl
+   /\ Val.inject_list j (map (fun p => Locmap.getpair p ls) (loc_arguments sg)) vl.
 Proof.
   unfold extcall_arguments.
   apply transl_external_arguments_rec.
@@ -2079,16 +2096,14 @@ Proof.
   simpl in TRANSL. inversion TRANSL; subst tf.
   exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]].
   rewrite sep_comm, sep_assoc in SEP.
-  inv H0. 
   exploit external_call_parallel_rule; eauto.
-  eapply decode_longs_inject; eauto. 
   intros (j' & res' & m1' & A & B & C & D & E).
   econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved'. econstructor; eauto. apply senv_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eapply match_states_return with (j := j').
   eapply match_stacks_change_meminj; eauto.
-  apply agree_regs_set_regs. apply agree_regs_inject_incr with j; auto. apply encode_long_inject; auto.
+  apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto.
   apply agree_callee_save_set_result; auto.
   apply stack_contents_change_meminj with j; auto. 
   rewrite sep_comm, sep_assoc; auto.
@@ -2135,7 +2150,9 @@ Lemma transf_final_states:
   match_states st1 st2 -> Linear.final_state st1 r -> Mach.final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv STACKS.
-  generalize (AGREGS r0). rewrite H2. intros A; inv A.
+  assert (R: exists r, loc_result signature_main = One r) by (econstructor; reflexivity). 
+  destruct R as [rres EQ]. rewrite EQ in H1. simpl in H1.
+  generalize (AGREGS rres). rewrite H1. intros A; inv A.
   econstructor; eauto.
 Qed.
 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 4f1f8143..4f3ba5cb 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -367,7 +367,7 @@ Proof.
   (* external function *)
   left; simpl; econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   simpl. econstructor; eauto.
   (* return *)
   inv H3. inv H1.
@@ -395,7 +395,7 @@ Lemma transf_final_states:
   forall st1 st2 r,
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H6. econstructor; eauto.
+  intros. inv H0. inv H. inv H5. econstructor; eauto.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/XTL.ml b/backend/XTL.ml
index 2ddbc50a..a1b7f23b 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -64,6 +64,11 @@ let vlocs ll = List.map vloc ll
 let vmreg mr = L(R mr)
 let vmregs mrl = List.map vmreg mrl
 
+let rec vlocpairs = function
+  | [] -> []
+  | One l :: ll -> L l :: vlocpairs ll
+  | Twolong(l1, l2) :: ll -> L l1 :: L l2 :: vlocpairs ll
+
 (* Tests over variables *)
 
 let is_stack_reg = function
diff --git a/backend/XTL.mli b/backend/XTL.mli
index 6bdcc8c6..54988d4b 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -64,6 +64,7 @@ val vloc: loc -> var
 val vlocs: loc list -> var list
 val vmreg: mreg -> var
 val vmregs: mreg list -> var list
+val vlocpairs: loc rpair list -> var list
 
 (* Tests over variables *)