diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-21 13:32:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-21 13:32:24 +0000 |
commit | dc4bed2cf06f46687225275131f411c86c773598 (patch) | |
tree | 9d99e759d906d061b6f213e0b20cb4bd53580ea6 /backend/Op.v | |
parent | ec6d00d94bcb1a0adc5c698367634b5e2f370c6e (diff) |
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
Diffstat (limited to 'backend/Op.v')
-rw-r--r-- | backend/Op.v | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/backend/Op.v b/backend/Op.v index b1136f9..707bcb0 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. |