Merge pull request #99 from AbsInt/register-pairs

Introduce register pairs to describe calling conventions more precisely

1 files changed, 26 insertions, 8 deletions

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 :=