From dc4bed2cf06f46687225275131f411c86c773598 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 21 Dec 2008 13:32:24 +0000
Subject: Revised back-end so that only 2 integer registers are reserved for
 reloading.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@925 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Op.v | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

(limited to 'backend/Op.v')

diff --git a/backend/Op.v b/backend/Op.v
index b1136f97..707bcb0a 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -254,7 +254,7 @@ Definition eval_addressing
   | Aindexed2, Vptr b1 n1 :: Vint n2 :: nil =>
       Some (Vptr b1 (Int.add n1 n2))
   | Aindexed2, Vint n1 :: Vptr b2 n2 :: nil =>
-      Some (Vptr b2 (Int.add n1 n2))
+      Some (Vptr b2 (Int.add n2 n1))
   | Aglobal s ofs, nil =>
       match Genv.find_symbol genv s with
       | None => None
@@ -759,7 +759,6 @@ Proof.
   intros.
   unfold eval_addressing in H; destruct addr; FuncInv;
   try subst v; simpl; try reflexivity.
-  decEq. apply Int.add_commut.
   unfold find_symbol_offset. 
   destruct (Genv.find_symbol genv i); congruence.
   unfold find_symbol_offset.
@@ -876,3 +875,32 @@ Proof.
 Qed.
 
 End EVAL_LESSDEF.
+
+(** Transformation of addressing modes with two operands or more
+  into an equivalent arithmetic operation.  This is used in the [Reload]
+  pass when a store instruction cannot be reloaded directly because
+  it runs out of temporary registers. *)
+
+(** For the PowerPC, there is only one binary addressing mode: [Aindexed2].
+  The corresponding operation is [Oadd]. *)
+
+Definition op_for_binary_addressing (addr: addressing) : operation := Oadd.
+
+Lemma eval_op_for_binary_addressing:
+  forall (F: Set) (ge: Genv.t F) sp addr args m v,
+  (length args >= 2)%nat ->
+  eval_addressing ge sp addr args = Some v ->
+  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
+Proof.
+  intros.
+  unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction;
+  simpl; congruence.
+Qed.
+
+Lemma type_op_for_binary_addressing:
+  forall addr,
+  (length (type_of_addressing addr) >= 2)%nat ->
+  type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint).
+Proof.
+  intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
+Qed.
-- 
cgit