diff --git a/.depend b/.depend
index bc2750a7989d3ac1748d008d89c172010eaa042d..be224c41019c4af9ce0e436a019ea041f4f0666f 100644
--- a/.depend
+++ b/.depend
@@ -46,7 +46,7 @@ backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo common/AST.v
backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo
backend/LTLin.vo: backend/LTLin.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo
-backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo
+backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo backend/Conventions.vo
backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo
backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo
backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 58ed3b6ecfb7d2067e4bddda8ba91f8f7fa2af1c..5e38934909133ad5930fa72279914cccbb339064 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -649,7 +649,7 @@ Proof.
(* Icall *)
exploit transl_find_function; eauto. intros [tf [TFIND TF]].
- generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 CORR2].
+ generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 [CORR2 CORR3]].
assert (rs##args = map ls (map assign args)).
eapply agree_eval_regs; eauto.
econstructor; split.
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index 469fd3c3996fb8bd4ab2bc17f59c219b173dbf87..d9ab17b0ba1ef73c6f0beab0008a73924843bf9c 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -106,6 +106,7 @@ Ltac WT :=
Lemma wt_transf_instr:
forall pc instr,
RTLtyping.wt_instr env f instr ->
+ f.(RTL.fn_code)!pc = Some instr ->
wt_instr tf (transf_instr f live alloc pc instr).
Proof.
intros. inv H; simpl.
@@ -124,13 +125,19 @@ Proof.
(* store *)
WT.
(* call *)
+ exploit regalloc_correct_1; eauto. unfold correct_alloc_instr.
+ intros [A1 [A2 A3]].
WT.
- destruct ros; simpl. autorewrite with allocty; auto. auto.
- destruct ros; simpl; auto with allocty.
+ destruct ros; simpl; auto.
+ split. autorewrite with allocty; auto.
+ split. auto with allocty. auto.
(* tailcall *)
+ exploit regalloc_correct_1; eauto. unfold correct_alloc_instr.
+ intro A1.
WT.
- destruct ros; simpl. autorewrite with allocty; auto. auto.
- destruct ros; simpl; auto with allocty.
+ destruct ros; simpl; auto.
+ split. autorewrite with allocty; auto.
+ split. auto with allocty. auto.
rewrite transf_unroll; auto.
(* alloc *)
WT.
diff --git a/backend/Coloring.v b/backend/Coloring.v
index 5e91b03c0535fa136a545ddc37cd081db4c21a5b..056aaa51975dc0872d5980d5f0d827fb430f3e37 100644
--- a/backend/Coloring.v
+++ b/backend/Coloring.v
@@ -110,12 +110,26 @@ Definition add_interf_move
if Reg.eq r arg then false else true)
res live g.
-Definition add_interf_call
+Definition add_interf_destroyed
(live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
List.fold_left
(fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g)
destroyed g.
+Definition add_interfs_indirect_call
+ (rfun: reg) (locs: list loc) (g: graph): graph :=
+ List.fold_left
+ (fun g loc =>
+ match loc with R mr => add_interf_mreg rfun mr g | _ => g end)
+ locs g.
+
+Definition add_interf_call
+ (ros: reg + ident) (locs: list loc) (g: graph): graph :=
+ match ros with
+ | inl rfun => add_interfs_indirect_call rfun locs g
+ | inr idfun => g
+ end.
+
Fixpoint add_prefs_call
(args: list reg) (locs: list loc) (g: graph) {struct args} : graph :=
match args, locs with
@@ -157,18 +171,23 @@ Definition add_edges_instr
then add_interf_op dst live g
else g
| Icall sig ros args res s =>
- add_prefs_call args (loc_arguments sig)
- (add_pref_mreg res (loc_result sig)
+ let largs := loc_arguments sig in
+ let lres := loc_result sig in
+ add_prefs_call args largs
+ (add_pref_mreg res lres
(add_interf_op res live
- (add_interf_call
- (Regset.remove res live) destroyed_at_call_regs g)))
+ (add_interf_call ros largs
+ (add_interf_destroyed
+ (Regset.remove res live) destroyed_at_call_regs g))))
| Itailcall sig ros args =>
- add_prefs_call args (loc_arguments sig) g
+ let largs := loc_arguments sig in
+ add_prefs_call args largs
+ (add_interf_call ros largs g)
| Ialloc arg res s =>
add_pref_mreg arg loc_alloc_argument
(add_pref_mreg res loc_alloc_result
(add_interf_op res live
- (add_interf_call
+ (add_interf_destroyed
(Regset.remove res live) destroyed_at_call_regs g)))
| Ireturn (Some r) =>
add_pref_mreg r (loc_result sig) g
diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v
index cea4ce5fd583583e14da2b07db7643481dae929f..ea31a29e3674aff7547d7ffbbf206d9074b84cac 100644
--- a/backend/Coloringproof.v
+++ b/backend/Coloringproof.v
@@ -133,7 +133,7 @@ Proof.
rewrite dec_eq_false; auto. rewrite dec_eq_false; auto.
Qed.
-Lemma add_interf_call_incl_aux_1:
+Lemma add_interf_destroyed_incl_aux_1:
forall mr live g,
graph_incl g
(List.fold_left (fun g r => add_interf_mreg r mr g) live g).
@@ -145,22 +145,42 @@ Proof.
auto.
Qed.
-Lemma add_interf_call_incl_aux_2:
+Lemma add_interf_destroyed_incl_aux_2:
forall mr live g,
graph_incl g
(Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
Proof.
- intros. rewrite Regset.fold_1. apply add_interf_call_incl_aux_1.
+ intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1.
Qed.
-Lemma add_interf_call_incl:
+Lemma add_interf_destroyed_incl:
forall live destroyed g,
- graph_incl g (add_interf_call live destroyed g).
+ graph_incl g (add_interf_destroyed live destroyed g).
Proof.
induction destroyed; simpl; intros.
apply graph_incl_refl.
eapply graph_incl_trans; [idtac|apply IHdestroyed].
- apply add_interf_call_incl_aux_2.
+ apply add_interf_destroyed_incl_aux_2.
+Qed.
+
+Lemma add_interfs_indirect_call_incl:
+ forall rfun locs g,
+ graph_incl g (add_interfs_indirect_call rfun locs g).
+Proof.
+ unfold add_interfs_indirect_call. induction locs; simpl; intros.
+ apply graph_incl_refl.
+ destruct a. eapply graph_incl_trans; [idtac|eauto].
+ apply add_interf_mreg_incl.
+ auto.
+Qed.
+
+Lemma add_interfs_call_incl:
+ forall ros locs g,
+ graph_incl g (add_interf_call ros locs g).
+Proof.
+ intros. unfold add_interf_call. destruct ros.
+ apply add_interfs_indirect_call_incl.
+ apply graph_incl_refl.
Qed.
Lemma interfere_incl:
@@ -181,7 +201,7 @@ Proof.
unfold graph_incl; intros. elim H; auto.
Qed.
-Lemma add_interf_call_correct_aux_1:
+Lemma add_interf_destroyed_correct_aux_1:
forall mr r live,
InA Regset.E.eq r live ->
forall g,
@@ -190,36 +210,60 @@ Lemma add_interf_call_correct_aux_1:
Proof.
induction 1; simpl; intros.
hnf in H; subst y. eapply interfere_mreg_incl.
- apply add_interf_call_incl_aux_1.
+ apply add_interf_destroyed_incl_aux_1.
apply add_interf_mreg_correct.
auto.
Qed.
-Lemma add_interf_call_correct_aux_2:
+Lemma add_interf_destroyed_correct_aux_2:
forall mr live g r,
Regset.In r live ->
interfere_mreg r mr
(Regset.fold graph (fun r g => add_interf_mreg r mr g) live g).
Proof.
- intros. rewrite Regset.fold_1. apply add_interf_call_correct_aux_1.
+ intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1.
apply Regset.elements_1. auto.
Qed.
-Lemma add_interf_call_correct:
+Lemma add_interf_destroyed_correct:
forall live destroyed g r mr,
Regset.In r live ->
In mr destroyed ->
- interfere_mreg r mr (add_interf_call live destroyed g).
+ interfere_mreg r mr (add_interf_destroyed live destroyed g).
Proof.
induction destroyed; simpl; intros.
elim H0.
elim H0; intros.
subst a. eapply interfere_mreg_incl.
- apply add_interf_call_incl.
- apply add_interf_call_correct_aux_2; auto.
+ apply add_interf_destroyed_incl.
+ apply add_interf_destroyed_correct_aux_2; auto.
apply IHdestroyed; auto.
Qed.
+Lemma add_interfs_indirect_call_correct:
+ forall rfun mr locs g,
+ In (R mr) locs ->
+ interfere_mreg rfun mr (add_interfs_indirect_call rfun locs g).
+Proof.
+ unfold add_interfs_indirect_call. induction locs; simpl; intros.
+ elim H.
+ destruct H. subst a.
+ eapply interfere_mreg_incl.
+ apply (add_interfs_indirect_call_incl rfun locs (add_interf_mreg rfun mr g)).
+ apply add_interf_mreg_correct.
+ auto.
+Qed.
+
+Lemma add_interfs_call_correct:
+ forall rfun locs g mr,
+ In (R mr) locs ->
+ interfere_mreg rfun mr (add_interf_call (inl _ rfun) locs g).
+Proof.
+ intros. unfold add_interf_call.
+ apply add_interfs_indirect_call_correct. auto.
+Qed.
+
+
Lemma add_prefs_call_incl:
forall args locs g,
graph_incl g (add_prefs_call args locs g).
@@ -336,12 +380,14 @@ Proof.
eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
- apply add_interf_call_incl.
- apply add_prefs_call_incl.
+ eapply graph_incl_trans; [idtac|apply add_interfs_call_incl].
+ apply add_interf_destroyed_incl.
+ eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
+ apply add_interfs_call_incl.
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
- apply add_interf_call_incl.
+ apply add_interf_destroyed_incl.
destruct o.
apply add_pref_mreg_incl.
apply graph_incl_refl.
@@ -379,7 +425,18 @@ Definition correct_interf_instr
interfere_mreg r mr g)
/\ (forall r,
Regset.In r live ->
- r <> res -> interfere r res g)
+ r <> res -> interfere r res g)
+ /\ (match ros with
+ | inl rfun => forall mr, In (R mr) (loc_arguments sig) ->
+ interfere_mreg rfun mr g
+ | inr idfun => True
+ end)
+ | Itailcall sig ros args =>
+ match ros with
+ | inl rfun => forall mr, In (R mr) (loc_arguments sig) ->
+ interfere_mreg rfun mr g
+ | inr idfun => True
+ end
| Ialloc arg res s =>
(forall r mr,
Regset.In r live ->
@@ -405,9 +462,11 @@ Proof.
intros. eapply interfere_incl; eauto.
intros. eapply interfere_incl; eauto.
intros. eapply interfere_incl; eauto.
- intros [A B]. split.
- intros. eapply interfere_mreg_incl; eauto.
- intros. eapply interfere_incl; eauto.
+ intros [A [B C]].
+ split. intros. eapply interfere_mreg_incl; eauto.
+ split. intros. eapply interfere_incl; eauto.
+ destruct s0; auto. intros. eapply interfere_mreg_incl; eauto.
+ destruct s0; auto. intros. eapply interfere_mreg_incl; eauto.
intros [A B]. split.
intros. eapply interfere_mreg_incl; eauto.
intros. eapply interfere_incl; eauto.
@@ -426,27 +485,46 @@ Proof.
intros. rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto.
- split; intros.
+ (* Icall *)
+ set (largs := loc_arguments s).
+ set (lres := loc_result s).
+ split. intros.
apply interfere_mreg_incl with
- (add_interf_call (Regset.remove r live) destroyed_at_call_regs g).
+ (add_interf_destroyed (Regset.remove r live) destroyed_at_call_regs g).
eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
- apply add_interf_op_incl.
- apply add_interf_call_correct; auto.
- apply Regset.remove_2; auto.
+ eapply graph_incl_trans; [idtac|apply add_interf_op_incl].
+ apply add_interfs_call_incl.
+ apply add_interf_destroyed_correct; auto.
+ apply Regset.remove_2; auto.
+ split. intros.
eapply interfere_incl.
eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
apply add_pref_mreg_incl.
apply add_interf_op_correct; auto.
+ destruct s0; auto; intros.
+ eapply interfere_mreg_incl.
+ eapply graph_incl_trans; [idtac|apply add_prefs_call_incl].
+ eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
+ apply add_interf_op_incl.
+ apply add_interfs_call_correct. auto.
+
+ (* Itailcall *)
+ destruct s0; auto; intros.
+ eapply interfere_mreg_incl.
+ apply add_prefs_call_incl.
+ apply add_interfs_call_correct. auto.
+
+ (* Ialloc *)
split; intros.
apply interfere_mreg_incl with
- (add_interf_call (Regset.remove r0 live) destroyed_at_call_regs g).
+ (add_interf_destroyed (Regset.remove r0 live) destroyed_at_call_regs g).
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl].
apply add_interf_op_incl.
- apply add_interf_call_correct; auto.
+ apply add_interf_destroyed_correct; auto.
apply Regset.remove_2; auto.
eapply interfere_incl.
@@ -739,6 +817,15 @@ Definition correct_alloc_instr
/\ (forall r,
Regset.In r live!!pc ->
r <> res -> alloc r <> alloc res)
+ /\ (match ros with
+ | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
+ | inr idfun => True
+ end)
+ | Itailcall sig ros args =>
+ (match ros with
+ | inl rfun => ~(In (alloc rfun) (loc_arguments sig))
+ | inr idfun => True
+ end)
| Ialloc arg res s =>
(forall r,
Regset.In r live!!pc ->
@@ -810,21 +897,37 @@ Lemma correct_interf_alloc_instr:
forall pc instr,
(forall r1 r2, interfere r1 r2 g -> alloc r1 <> alloc r2) ->
(forall r1 mr2, interfere_mreg r1 mr2 g -> alloc r1 <> R mr2) ->
+ (forall r, loc_acceptable (alloc r)) ->
correct_interf_instr live!!pc instr g ->
correct_alloc_instr live alloc pc instr.
Proof.
- intros pc instr ALL1 ALL2.
+ intros pc instr ALL1 ALL2 ALL3.
unfold correct_interf_instr, correct_alloc_instr;
destruct instr; auto.
destruct (is_move_operation o l); auto.
- intros [A B]. split.
- intros; red; intros.
+ (* Icall *)
+ intros [A [B C]].
+ split. intros; red; intros.
unfold destroyed_at_call in H1.
generalize (list_in_map_inv R _ _ H1).
intros [mr [EQ IN]].
generalize (A r0 mr H IN H0). intro.
generalize (ALL2 _ _ H2). contradiction.
- auto.
+ split. auto.
+ destruct s0; auto. red; intros.
+ generalize (ALL3 r0). generalize (Conventions.loc_arguments_acceptable _ _ H).
+ unfold loc_argument_acceptable, loc_acceptable.
+ caseEq (alloc r0). intros.
+ elim (ALL2 r0 m). apply C; auto. congruence. auto.
+ destruct s0; auto.
+ (* Itailcall *)
+ destruct s0; auto. red; intros.
+ generalize (ALL3 r). generalize (Conventions.loc_arguments_acceptable _ _ H0).
+ unfold loc_argument_acceptable, loc_acceptable.
+ caseEq (alloc r). intros.
+ elim (ALL2 r m). apply H; auto. congruence. auto.
+ destruct s0; auto.
+ (* Ialloc *)
intros [A B]. split.
intros; red; intros.
unfold destroyed_at_call in H1.
@@ -850,6 +953,7 @@ Proof.
apply alloc_of_coloring_correct_1. auto. rewrite H4 in H3; auto.
intros. rewrite H2. unfold allregs.
apply alloc_of_coloring_correct_2. auto. exact H3.
+ intros. eapply regalloc_acceptable; eauto.
unfold g. apply interf_graph_correct_1. auto.
Qed.
diff --git a/backend/Conventions.v b/backend/Conventions.v
index a861eb843b01fae9267896677d98747d40a8ce62..b7d931f553794f7dcdefc5461b617135756f5e96 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -51,8 +51,12 @@ Definition destroyed_at_call_regs :=
Definition destroyed_at_call :=
List.map R destroyed_at_call_regs.
+Definition int_temporaries := IT1 :: IT2 :: nil.
+
+Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil.
+
Definition temporaries :=
- R IT1 :: R IT2 :: R IT3 :: R FT1 :: R FT2 :: R FT3 :: nil.
+ R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil.
(** The [index_int_callee_save] and [index_float_callee_save] associate
a unique positive integer to callee-save registers. This integer is
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 1c0c3f30a742bc30f7acede693dd2450a4950279..26ec066d100f268d7210294e22b16d6f53b71116 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -19,6 +19,7 @@ Require Import Op.
Require Import RTL.
Require Import Locations.
Require Import LTLin.
+Require LTLtyping.
Require Import Conventions.
(** The following predicates define a type system for LTLin similar to that
@@ -53,17 +54,15 @@ Inductive wt_instr : instruction -> Prop :=
wt_instr (Lstore chunk addr args src)
| wt_Lcall:
forall sig ros args res,
- match ros with inl r => Loc.type r = Tint | inr s => True end ->
List.map Loc.type args = sig.(sig_args) ->
- Loc.type res = match sig.(sig_res) with None => Tint | Some ty => ty end ->
- match ros with inl r => loc_acceptable r | inr s => True end ->
+ Loc.type res = proj_sig_res sig ->
+ LTLtyping.call_loc_acceptable sig ros ->
locs_acceptable args -> loc_acceptable res ->
wt_instr (Lcall sig ros args res)
| wt_Ltailcall:
forall sig ros args,
- match ros with inl r => Loc.type r = Tint | inr s => True end ->
List.map Loc.type args = sig.(sig_args) ->
- match ros with inl r => loc_acceptable r | inr s => True end ->
+ LTLtyping.call_loc_acceptable sig ros ->
locs_acceptable args ->
sig.(sig_res) = funsig.(sig_res) ->
Conventions.tailcall_possible sig ->
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 18308b8fd3beebf7232d3ea0973814f799bdc478..950154a11045b343f888e51c710fc24dc76cad98 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -35,6 +35,12 @@ Variable funct: function.
Definition valid_successor (s: node) : Prop :=
exists i, funct.(fn_code)!s = Some i.
+Definition call_loc_acceptable (sig: signature) (los: loc + ident) : Prop :=
+ match los with
+ | inl l => Loc.type l = Tint /\ loc_acceptable l /\ ~In l (loc_arguments sig)
+ | inr s => True
+ end.
+
Inductive wt_instr : instruction -> Prop :=
| wt_Lnop:
forall s,
@@ -68,18 +74,16 @@ Inductive wt_instr : instruction -> Prop :=
wt_instr (Lstore chunk addr args src s)
| wt_Lcall:
forall sig ros args res s,
- match ros with inl r => Loc.type r = Tint | inr s => True end ->
List.map Loc.type args = sig.(sig_args) ->
Loc.type res = proj_sig_res sig ->
- match ros with inl r => loc_acceptable r | inr s => True end ->
+ call_loc_acceptable sig ros ->
locs_acceptable args -> loc_acceptable res ->
valid_successor s ->
wt_instr (Lcall sig ros args res s)
| wt_Ltailcall:
forall sig ros args,
- match ros with inl r => Loc.type r = Tint | inr s => True end ->
List.map Loc.type args = sig.(sig_args) ->
- match ros with inl r => loc_acceptable r | inr s => True end ->
+ call_loc_acceptable sig ros ->
locs_acceptable args ->
sig.(sig_res) = funct.(fn_sig).(sig_res) ->
Conventions.tailcall_possible sig ->
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 7dc601fbca1b2b0d614ae27adb2087ab43435987..9ef6e317041908117b7f69b50f7ee314c4178cb6 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -83,7 +83,7 @@ Inductive wt_instr : instruction -> Prop :=
| wt_Ltailcall:
forall sig ros,
tailcall_possible sig ->
- match ros with inl r => r = IT3 | _ => True end ->
+ match ros with inl r => r = IT1 | _ => True end ->
wt_instr (Ltailcall sig ros)
| wt_Lalloc:
wt_instr Lalloc
diff --git a/backend/Locations.v b/backend/Locations.v
index 1373887f18678f1e72a9a71d9c7a1494e80a8340..b03657c070a91932f59047a9eb6e755c67ad9178 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -30,10 +30,10 @@ Require Import Values.
- Integer registers that can be allocated to RTL pseudo-registers ([Rxx]).
- Floating-point registers that can be allocated to RTL pseudo-registers
([Fxx]).
-- Three integer registers, not allocatable, reserved as temporaries for
- spilling and reloading ([ITx]).
-- Three float registers, not allocatable, reserved as temporaries for
- spilling and reloading ([FTx]).
+- Two integer registers, not allocatable, reserved as temporaries for
+ spilling and reloading ([IT1, IT2]).
+- Two float registers, not allocatable, reserved as temporaries for
+ spilling and reloading ([FT1, FT2]).
The type [mreg] does not include special-purpose machine registers
such as the stack pointer and the condition codes. *)
@@ -56,7 +56,7 @@ Inductive mreg: Set :=
| F24: mreg | F25: mreg | F26: mreg | F27: mreg
| F28: mreg | F29: mreg | F30: mreg | F31: mreg
(** Integer temporaries *)
- | IT1: mreg (* R11 *) | IT2: mreg (* R12 *) | IT3: mreg (* R0 *)
+ | IT1: mreg (* R11 *) | IT2: mreg (* R0 *)
(** Float temporaries *)
| FT1: mreg (* F11 *) | FT2: mreg (* F12 *) | FT3: mreg (* F0 *).
@@ -79,7 +79,7 @@ Definition mreg_type (r: mreg): typ :=
| F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat
| F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat
| F28 => Tfloat | F29 => Tfloat | F30 => Tfloat | F31 => Tfloat
- | IT1 => Tint | IT2 => Tint | IT3 => Tint
+ | IT1 => Tint | IT2 => Tint
| FT1 => Tfloat | FT2 => Tfloat | FT3 => Tfloat
end.
@@ -104,8 +104,8 @@ Module IndexedMreg <: INDEXED_TYPE.
| F20 => 44 | F21 => 45 | F22 => 46 | F23 => 47
| F24 => 48 | F25 => 49 | F26 => 50 | F27 => 51
| F28 => 52 | F29 => 53 | F30 => 54 | F31 => 55
- | IT1 => 56 | IT2 => 57 | IT3 => 58
- | FT1 => 59 | FT2 => 60 | FT3 => 61
+ | IT1 => 56 | IT2 => 57
+ | FT1 => 58 | FT2 => 59 | FT3 => 60
end.
Lemma index_inj:
forall r1 r2, index r1 = index r2 -> r1 = r2.
diff --git a/backend/Op.v b/backend/Op.v
index b1136f97cc70a31823fab629b30ab4be9de2ca15..707bcb0ab689d15f2231c4c84d7cb3cc42988929 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.
diff --git a/backend/PPC.v b/backend/PPC.v
index cfd07405fd67c3c2ea87da483853623426b64a9f..13c7a875aea5af57493db303b3f7018dbadd034a 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -564,7 +564,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
let sp := Vptr stk (Int.repr lo) in
match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with
| None => Error
- | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR2 <- Vundef)) m2
+ | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)) m2
end
| Pand_ rd r1 r2 =>
let v := Val.and rs#r1 rs#r2 in
@@ -655,9 +655,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Pfsub rd r1 r2 =>
OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m
| Pictf rd r1 =>
- OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR2 <- Vundef #FPR13 <- Vundef)) m
+ OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m
| Piuctf rd r1 =>
- OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR2 <- Vundef #FPR13 <- Vundef)) m
+ OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m
| Plbz rd cst r1 =>
load1 Mint8unsigned rd cst r1 rs m
| Plbzx rd r1 r2 =>
@@ -679,7 +679,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Plhzx rd r1 r2 =>
load2 Mint16unsigned rd r1 r2 rs m
| Plfi rd f =>
- OK (nextinstr (rs#rd <- (Vfloat f) #GPR2 <- Vundef)) m
+ OK (nextinstr (rs#rd <- (Vfloat f) #GPR12 <- Vundef)) m
| Plwz rd cst r1 =>
load1 Mint32 rd cst r1 rs m
| Plwzx rd r1 r2 =>
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index f6d1fec01ad98dc76fa714a9cccfb520f654a192..1484a1e67d1483d9cc29dc5f2ff1315cf8203de0 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -34,7 +34,7 @@ Require Import PPC.
results when applied to a LTL register of the wrong type.
The proof in [PPCgenproof] will show that this never happens.
- Note that no LTL register maps to [GPR2] nor [FPR13].
+ Note that no LTL register maps to [GPR12] nor [FPR13].
These two registers are reserved as temporaries, to be used
by the generated PPC code. *)
@@ -47,7 +47,7 @@ Definition ireg_of (r: mreg) : ireg :=
| R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24
| R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28
| R29 => GPR29 | R30 => GPR30 | R31 => GPR31
- | IT1 => GPR11 | IT2 => GPR12 | IT3 => GPR0
+ | IT1 => GPR11 | IT2 => GPR0
| _ => GPR0 (* should not happen *)
end.
@@ -108,7 +108,7 @@ Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) :=
Paddi r1 r1 (Cint (low_s n)) :: k.
Definition addimm_2 (r1 r2: ireg) (n: int) (k: code) :=
- loadimm GPR2 n (Padd r1 r2 GPR2 :: k).
+ loadimm GPR12 n (Padd r1 r2 GPR12 :: k).
Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
if ireg_eq r1 GPR0 then
@@ -124,7 +124,7 @@ Definition andimm (r1 r2: ireg) (n: int) (k: code) :=
else if Int.eq (low_u n) Int.zero then
Pandis_ r1 r2 (Cint (high_u n)) :: k
else
- loadimm GPR2 n (Pand_ r1 r2 GPR2 :: k).
+ loadimm GPR12 n (Pand_ r1 r2 GPR12 :: k).
Definition orimm (r1 r2: ireg) (n: int) (k: code) :=
if Int.eq (high_u n) Int.zero then
@@ -158,8 +158,8 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
if Int.eq (high_s ofs) Int.zero then
loadind_aux base ofs ty dst :: k
else
- Paddis GPR2 base (Cint (high_s ofs)) ::
- loadind_aux GPR2 (low_s ofs) ty dst :: k.
+ Paddis GPR12 base (Cint (high_s ofs)) ::
+ loadind_aux GPR12 (low_s ofs) ty dst :: k.
Definition storeind_aux (src: mreg) (base: ireg) (ofs: int) (ty: typ) :=
match ty with
@@ -171,8 +171,8 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
if Int.eq (high_s ofs) Int.zero then
storeind_aux src base ofs ty :: k
else
- Paddis GPR2 base (Cint (high_s ofs)) ::
- storeind_aux src GPR2 (low_s ofs) ty :: k.
+ Paddis GPR12 base (Cint (high_s ofs)) ::
+ storeind_aux src GPR12 (low_s ofs) ty :: k.
(** Constructor for a floating-point comparison. The PowerPC has
a single [fcmpu] instruction to compare floats, which sets
@@ -206,20 +206,20 @@ Definition transl_cond
if Int.eq (high_s n) Int.zero then
Pcmpwi (ireg_of a1) (Cint n) :: k
else
- loadimm GPR2 n (Pcmpw (ireg_of a1) GPR2 :: k)
+ loadimm GPR12 n (Pcmpw (ireg_of a1) GPR12 :: k)
| Ccompuimm c n, a1 :: nil =>
if Int.eq (high_u n) Int.zero then
Pcmplwi (ireg_of a1) (Cint n) :: k
else
- loadimm GPR2 n (Pcmplw (ireg_of a1) GPR2 :: k)
+ loadimm GPR12 n (Pcmplw (ireg_of a1) GPR12 :: k)
| Ccompf cmp, a1 :: a2 :: nil =>
floatcomp cmp (freg_of a1) (freg_of a2) k
| Cnotcompf cmp, a1 :: a2 :: nil =>
floatcomp cmp (freg_of a1) (freg_of a2) k
| Cmaskzero n, a1 :: nil =>
- andimm GPR2 (ireg_of a1) n k
+ andimm GPR12 (ireg_of a1) n k
| Cmasknotzero n, a1 :: nil =>
- andimm GPR2 (ireg_of a1) n k
+ andimm GPR12 (ireg_of a1) n k
| _, _ =>
k (**r never happens for well-typed code *)
end.
@@ -277,8 +277,8 @@ Definition transl_op
| Ofloatconst f, nil =>
Plfi (freg_of r) f :: k
| Oaddrsymbol s ofs, nil =>
- Paddis GPR2 GPR0 (Csymbol_high s ofs) ::
- Paddi (ireg_of r) GPR2 (Csymbol_low s ofs) :: k
+ Paddis GPR12 GPR0 (Csymbol_high s ofs) ::
+ Paddi (ireg_of r) GPR12 (Csymbol_low s ofs) :: k
| Oaddrstack n, nil =>
addimm (ireg_of r) GPR1 n k
| Ocast8signed, a1 :: nil =>
@@ -299,14 +299,14 @@ Definition transl_op
if Int.eq (high_s n) Int.zero then
Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k
else
- loadimm GPR2 n (Psubfc (ireg_of r) (ireg_of a1) GPR2 :: k)
+ loadimm GPR12 n (Psubfc (ireg_of r) (ireg_of a1) GPR12 :: k)
| Omul, a1 :: a2 :: nil =>
Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
| Omulimm n, a1 :: nil =>
if Int.eq (high_s n) Int.zero then
Pmulli (ireg_of r) (ireg_of a1) (Cint n) :: k
else
- loadimm GPR2 n (Pmullw (ireg_of r) (ireg_of a1) GPR2 :: k)
+ loadimm GPR12 n (Pmullw (ireg_of r) (ireg_of a1) GPR12 :: k)
| Odiv, a1 :: a2 :: nil =>
Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k
| Odivu, a1 :: a2 :: nil =>
@@ -388,33 +388,33 @@ Definition transl_load_store
match addr, args with
| Aindexed ofs, a1 :: nil =>
if ireg_eq (ireg_of a1) GPR0 then
- Pmr GPR2 (ireg_of a1) ::
- Paddis GPR2 GPR2 (Cint (high_s ofs)) ::
- mk1 (Cint (low_s ofs)) GPR2 :: k
+ Pmr GPR12 (ireg_of a1) ::
+ Paddis GPR12 GPR12 (Cint (high_s ofs)) ::
+ mk1 (Cint (low_s ofs)) GPR12 :: k
else if Int.eq (high_s ofs) Int.zero then
mk1 (Cint ofs) (ireg_of a1) :: k
else
- Paddis GPR2 (ireg_of a1) (Cint (high_s ofs)) ::
- mk1 (Cint (low_s ofs)) GPR2 :: k
+ Paddis GPR12 (ireg_of a1) (Cint (high_s ofs)) ::
+ mk1 (Cint (low_s ofs)) GPR12 :: k
| Aindexed2, a1 :: a2 :: nil =>
mk2 (ireg_of a1) (ireg_of a2) :: k
| Aglobal symb ofs, nil =>
- Paddis GPR2 GPR0 (Csymbol_high symb ofs) ::
- mk1 (Csymbol_low symb ofs) GPR2 :: k
+ Paddis GPR12 GPR0 (Csymbol_high symb ofs) ::
+ mk1 (Csymbol_low symb ofs) GPR12 :: k
| Abased symb ofs, a1 :: nil =>
if ireg_eq (ireg_of a1) GPR0 then
- Pmr GPR2 (ireg_of a1) ::
- Paddis GPR2 GPR2 (Csymbol_high symb ofs) ::
- mk1 (Csymbol_low symb ofs) GPR2 :: k
+ Pmr GPR12 (ireg_of a1) ::
+ Paddis GPR12 GPR12 (Csymbol_high symb ofs) ::
+ mk1 (Csymbol_low symb ofs) GPR12 :: k
else
- Paddis GPR2 (ireg_of a1) (Csymbol_high symb ofs) ::
- mk1 (Csymbol_low symb ofs) GPR2 :: k
+ Paddis GPR12 (ireg_of a1) (Csymbol_high symb ofs) ::
+ mk1 (Csymbol_low symb ofs) GPR12 :: k
| Ainstack ofs, nil =>
if Int.eq (high_s ofs) Int.zero then
mk1 (Cint ofs) GPR1 :: k
else
- Paddis GPR2 GPR1 (Cint (high_s ofs)) ::
- mk1 (Cint (low_s ofs)) GPR2 :: k
+ Paddis GPR12 GPR1 (Cint (high_s ofs)) ::
+ mk1 (Cint (low_s ofs)) GPR12 :: k
| _, _ =>
(* should not happen *) k
end.
@@ -428,7 +428,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
| Msetstack src ofs ty =>
storeind src GPR1 ofs ty k
| Mgetparam ofs ty dst =>
- Plwz GPR2 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR2 ofs ty dst k
+ Plwz GPR12 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR12 ofs ty dst k
| Mop op args res =>
transl_op op args res k
| Mload chunk addr args dst =>
@@ -486,13 +486,13 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
Pbl symb :: k
| Mtailcall sig (inl r) =>
Pmtctr (ireg_of r) ::
- Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
- Pmtlr GPR2 ::
+ Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+ Pmtlr GPR12 ::
Pfreeframe f.(fn_link_ofs) ::
Pbctr :: k
| Mtailcall sig (inr symb) =>
- Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
- Pmtlr GPR2 ::
+ Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+ Pmtlr GPR12 ::
Pfreeframe f.(fn_link_ofs) ::
Pbs symb :: k
| Malloc =>
@@ -506,8 +506,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
transl_cond cond args
(if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
| Mreturn =>
- Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
- Pmtlr GPR2 ::
+ Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+ Pmtlr GPR12 ::
Pfreeframe f.(fn_link_ofs) ::
Pblr :: k
end.
@@ -522,8 +522,8 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
Definition transl_function (f: Mach.function) :=
Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) ::
- Pmflr GPR2 ::
- Pstw GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 ::
+ Pmflr GPR12 ::
+ Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
transl_code f f.(fn_code).
Fixpoint code_size (c: code) : Z :=
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index 932f7dea0a060feb63acd0f749f24f4eeea177ca..fd5843b1d199d95423dbfa3a730157928ba73354 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -392,7 +392,7 @@ Remark loadind_label:
Proof.
intros; unfold loadind.
case (Int.eq (high_s ofs) Int.zero). apply loadind_aux_label.
- transitivity (find_label lbl (loadind_aux GPR2 (low_s ofs) ty dst :: k)).
+ transitivity (find_label lbl (loadind_aux GPR12 (low_s ofs) ty dst :: k)).
reflexivity. apply loadind_aux_label.
Qed.
Hint Rewrite loadind_label: labels.
@@ -407,7 +407,7 @@ Remark storeind_label:
Proof.
intros; unfold storeind.
case (Int.eq (high_s ofs) Int.zero). apply storeind_aux_label.
- transitivity (find_label lbl (storeind_aux base GPR2 (low_s ofs) ty :: k)).
+ transitivity (find_label lbl (storeind_aux base GPR12 (low_s ofs) ty :: k)).
reflexivity. apply storeind_aux_label.
Qed.
Hint Rewrite storeind_label: labels.
@@ -775,10 +775,10 @@ Lemma exec_Mgetparam_prop:
Proof.
intros; red; intros; inv MS.
assert (f0 = f) by congruence. subst f0.
- set (rs2 := nextinstr (rs#GPR2 <- parent)).
+ set (rs2 := nextinstr (rs#GPR12 <- parent)).
assert (EX1: exec_straight tge (transl_function f)
(transl_code f (Mgetparam ofs ty dst :: c)) rs m
- (loadind GPR2 ofs ty dst (transl_code f c)) rs2 m).
+ (loadind GPR12 ofs ty dst (transl_code f c)) rs2 m).
simpl. apply exec_straight_one.
simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen.
unfold const_low. rewrite <- (sp_val ms sp rs); auto.
@@ -786,9 +786,9 @@ Proof.
rewrite H0. reflexivity. reflexivity.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inversion WTI.
- unfold load_stack in H1. change parent with rs2#GPR2 in H1.
- assert (NOTE: GPR2 <> GPR0). congruence.
- generalize (loadind_correct tge (transl_function f) GPR2 ofs ty
+ unfold load_stack in H1. change parent with rs2#GPR12 in H1.
+ assert (NOTE: GPR12 <> GPR0). congruence.
+ generalize (loadind_correct tge (transl_function f) GPR12 ofs ty
dst (transl_code f c) rs2 m v H1 H3 NOTE).
intros [rs3 [EX2 [RES OTH]]].
left; eapply exec_straight_steps; eauto with coqlib.
@@ -986,7 +986,7 @@ Proof.
destruct ros; simpl in H; simpl in H9.
(* Indirect call *)
set (rs2 := nextinstr (rs#CTR <- (ms m0))).
- set (rs3 := nextinstr (rs2#GPR2 <- (parent_ra s))).
+ set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))).
set (rs4 := nextinstr (rs3#LR <- (parent_ra s))).
set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))).
set (rs6 := rs5#PC <- (rs5 CTR)).
@@ -1029,7 +1029,7 @@ Proof.
generalize H. destruct (ms m0); try congruence.
predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
(* direct call *)
- set (rs2 := nextinstr (rs#GPR2 <- (parent_ra s))).
+ set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))).
set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
set (rs5 := rs4#PC <- (Vptr f' Int.zero)).
@@ -1194,7 +1194,7 @@ Lemma exec_Mreturn_prop:
Proof.
intros; red; intros; inv MS.
assert (f0 = f) by congruence. subst f0.
- set (rs2 := nextinstr (rs#GPR2 <- (parent_ra s))).
+ set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))).
set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
set (rs5 := rs4#PC <- (parent_ra s)).
@@ -1206,7 +1206,7 @@ Proof.
unfold load_stack in H1. simpl in H1.
rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1.
reflexivity. discriminate.
- unfold rs3. change (parent_ra s) with rs2#GPR2. reflexivity.
+ unfold rs3. change (parent_ra s) with rs2#GPR12. reflexivity.
simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG).
simpl.
unfold load_stack in H0. simpl in H0.
@@ -1256,8 +1256,8 @@ Proof.
inversion TY; auto.
exploit functions_transl; eauto. intro TFIND.
generalize (functions_transl_no_overflow _ _ H); intro NOOV.
- set (rs2 := nextinstr (rs#GPR1 <- sp #GPR2 <- Vundef)).
- set (rs3 := nextinstr (rs2#GPR2 <- (parent_ra s))).
+ set (rs2 := nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)).
+ set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))).
set (rs4 := nextinstr rs3).
(* Execution of function prologue *)
assert (EXEC_PROLOGUE:
@@ -1271,7 +1271,7 @@ Proof.
rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity.
simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity.
simpl. unfold store1. rewrite gpr_or_zero_not_zero.
- unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR2) with (parent_ra s).
+ unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR12) with (parent_ra s).
unfold store_stack in H2. simpl chunk_of_type in H2. rewrite H2. reflexivity.
discriminate. reflexivity. reflexivity. reflexivity.
(* Agreement at end of prologue *)
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index 215a9a7be2f1ebde22a28194898289e63500695f..ba347ea91790a4bc10e7b4a985943f5895a11515 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -138,7 +138,7 @@ Qed.
Definition is_data_reg (r: preg) : Prop :=
match r with
- | IR GPR2 => False
+ | IR GPR12 => False
| FR FPR13 => False
| PC => False | LR => False | CTR => False
| CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False
@@ -169,8 +169,8 @@ Lemma ireg_of_not_GPR1:
Proof.
intro. case r; discriminate.
Qed.
-Lemma ireg_of_not_GPR2:
- forall r, ireg_of r <> GPR2.
+Lemma ireg_of_not_GPR12:
+ forall r, ireg_of r <> GPR12.
Proof.
intro. case r; discriminate.
Qed.
@@ -179,7 +179,7 @@ Lemma freg_of_not_FPR13:
Proof.
intro. case r; discriminate.
Qed.
-Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR2 freg_of_not_FPR13: ppcgen.
+Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR12 freg_of_not_FPR13: ppcgen.
Lemma preg_of_not:
forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2.
@@ -250,7 +250,7 @@ Lemma agree_exten_2:
forall ms sp rs rs',
agree ms sp rs ->
(forall r,
- r <> IR GPR2 -> r <> FR FPR13 ->
+ r <> IR GPR12 -> r <> FR FPR13 ->
r <> PC -> r <> LR -> r <> CTR ->
r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 ->
r <> CARRY ->
@@ -390,7 +390,7 @@ Lemma agree_set_mireg_exten:
mreg_type r = Tint ->
rs'#(ireg_of r) = v ->
(forall r',
- r' <> IR GPR2 -> r' <> FR FPR13 ->
+ r' <> IR GPR12 -> r' <> FR FPR13 ->
r' <> PC -> r' <> LR -> r' <> CTR ->
r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
r' <> CARRY ->
@@ -724,14 +724,14 @@ Qed.
Lemma addimm_2_correct:
forall r1 r2 n k rs m,
- r2 <> GPR2 ->
+ r2 <> GPR12 ->
exists rs',
exec_straight (addimm_2 r1 r2 n k) rs m k rs' m
/\ rs'#r1 = Val.add rs#r2 (Vint n)
- /\ forall r': preg, r' <> r1 -> r' <> GPR2 -> r' <> PC -> rs'#r' = rs#r'.
+ /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold addimm_2.
- generalize (loadimm_correct GPR2 n (Padd r1 r2 GPR2 :: k) rs m).
+ generalize (loadimm_correct GPR12 n (Padd r1 r2 GPR12 :: k) rs m).
intros [rs1 [EX [RES OTHER]]].
exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))).
split. eapply exec_straight_trans. eexact EX.
@@ -744,11 +744,11 @@ Qed.
Lemma addimm_correct:
forall r1 r2 n k rs m,
- r2 <> GPR2 ->
+ r2 <> GPR12 ->
exists rs',
exec_straight (addimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = Val.add rs#r2 (Vint n)
- /\ forall r': preg, r' <> r1 -> r' <> GPR2 -> r' <> PC -> rs'#r' = rs#r'.
+ /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'.
Proof.
intros. unfold addimm.
case (ireg_eq r1 GPR0); intro.
@@ -763,14 +763,14 @@ Qed.
Lemma andimm_correct:
forall r1 r2 n k (rs : regset) m,
- r2 <> GPR2 ->
+ r2 <> GPR12 ->
let v := Val.and rs#r2 (Vint n) in
exists rs',
exec_straight (andimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = v
/\ rs'#CR0_2 = Val.cmp Ceq v Vzero
/\ forall r': preg,
- r' <> r1 -> r' <> GPR2 -> r' <> PC ->
+ r' <> r1 -> r' <> GPR12 -> r' <> PC ->
r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
rs'#r' = rs#r'.
Proof.
@@ -797,7 +797,7 @@ Proof.
split. auto.
intros. rewrite D; auto. apply Pregmap.gso; auto.
(* loadimm + and *)
- generalize (loadimm_correct GPR2 n (Pand_ r1 r2 GPR2 :: k) rs m).
+ generalize (loadimm_correct GPR12 n (Pand_ r1 r2 GPR12 :: k) rs m).
intros [rs1 [EX1 [RES1 OTHER1]]].
exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)).
generalize (compare_sint_spec (rs1#r1 <- v) v Vzero).
@@ -915,7 +915,7 @@ Lemma loadind_correct:
exists rs',
exec_straight (loadind base ofs ty dst k) rs m k rs' m
/\ rs'#(preg_of dst) = v
- /\ forall r, r <> PC -> r <> GPR2 -> r <> preg_of dst -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros. unfold loadind.
assert (preg_of dst <> PC).
@@ -928,7 +928,7 @@ Proof.
split. rewrite nextinstr_inv; auto. apply Pregmap.gss.
intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
(* long offset *)
- pose (rs1 := nextinstr (rs#GPR2 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
+ pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
exists (nextinstr (rs1#(preg_of dst) <- v)).
split. apply exec_straight_two with rs1 m.
simpl. rewrite gpr_or_zero_not_zero; auto.
@@ -966,7 +966,7 @@ Lemma storeind_correct:
base <> GPR0 ->
exists rs',
exec_straight (storeind src base ofs ty k) rs m k rs' m'
- /\ forall r, r <> PC -> r <> GPR2 -> rs'#r = rs#r.
+ /\ forall r, r <> PC -> r <> GPR12 -> rs'#r = rs#r.
Proof.
intros. unfold storeind.
(* short offset *)
@@ -976,7 +976,7 @@ Proof.
reflexivity.
intros. rewrite nextinstr_inv; auto.
(* long offset *)
- pose (rs1 := nextinstr (rs#GPR2 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
+ pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
exists (nextinstr rs1).
split. apply exec_straight_two with rs1 m.
simpl. rewrite gpr_or_zero_not_zero; auto.
@@ -1097,7 +1097,7 @@ Proof.
split.
case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto.
apply agree_exten_2 with rs; auto.
- generalize (loadimm_correct GPR2 i (Pcmpw (ireg_of m0) GPR2 :: k) rs m).
+ generalize (loadimm_correct GPR12 i (Pcmpw (ireg_of m0) GPR12 :: k) rs m).
intros [rs1 [EX1 [RES1 OTH1]]].
assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
generalize (compare_sint_spec rs1 ms#m0 (Vint i)).
@@ -1122,7 +1122,7 @@ Proof.
split.
case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto.
apply agree_exten_2 with rs; auto.
- generalize (loadimm_correct GPR2 i (Pcmplw (ireg_of m0) GPR2 :: k) rs m).
+ generalize (loadimm_correct GPR12 i (Pcmplw (ireg_of m0) GPR12 :: k) rs m).
intros [rs1 [EX1 [RES1 OTH1]]].
assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
generalize (compare_uint_spec rs1 ms#m0 (Vint i)).
@@ -1156,14 +1156,14 @@ Proof.
apply agree_exten_2 with rs; auto.
(* Cmaskzero *)
simpl.
- generalize (andimm_correct GPR2 (ireg_of m0) i k rs m (ireg_of_not_GPR2 m0)).
+ generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)).
intros [rs' [A [B [C D]]]].
exists rs'. split. assumption.
split. rewrite C. rewrite <- (ireg_val ms sp rs); auto.
apply agree_exten_2 with rs; auto.
(* Cmasknotzero *)
simpl.
- generalize (andimm_correct GPR2 (ireg_of m0) i k rs m (ireg_of_not_GPR2 m0)).
+ generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)).
intros [rs' [A [B [C D]]]].
exists rs'. split. assumption.
split. rewrite C. rewrite <- (ireg_val ms sp rs); auto.
@@ -1243,13 +1243,13 @@ Proof.
exists rs'. split. auto.
apply agree_set_mireg_exten with rs; auto.
(* Ofloatconst *)
- exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR2 <- Vundef)).
+ exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR12 <- Vundef)).
split. apply exec_straight_one. reflexivity. reflexivity.
auto with ppcgen.
(* Oaddrsymbol *)
change (find_symbol_offset ge i i0) with (symbol_offset ge i i0).
set (v := symbol_offset ge i i0).
- pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))).
+ pose (rs1 := nextinstr (rs#GPR12 <- (high_half v))).
exists (nextinstr (rs1#(ireg_of res) <- v)).
split. apply exec_straight_two with rs1 m.
unfold exec_instr. rewrite gpr_or_zero_zero.
@@ -1264,7 +1264,7 @@ Proof.
apply agree_set_mreg. apply agree_nextinstr.
apply agree_set_other. auto. simpl. tauto.
(* Oaddrstack *)
- assert (GPR1 <> GPR2). discriminate.
+ assert (GPR1 <> GPR12). discriminate.
generalize (addimm_correct (ireg_of res) GPR1 i k rs m H2).
intros [rs' [EX [RES OTH]]].
exists rs'. split. auto.
@@ -1288,7 +1288,7 @@ Proof.
rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto.
(* Oaddimm *)
generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m
- (ireg_of_not_GPR2 m0)).
+ (ireg_of_not_GPR12 m0)).
intros [rs' [A [B C]]].
exists rs'. split. auto.
apply agree_set_mireg_exten with rs; auto.
@@ -1302,14 +1302,14 @@ Proof.
exists (nextinstr (rs#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)).
split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto.
reflexivity. simpl. auto with ppcgen.
- generalize (loadimm_correct GPR2 i (Psubfc (ireg_of res) (ireg_of m0) GPR2 :: k) rs m).
+ generalize (loadimm_correct GPR12 i (Psubfc (ireg_of res) (ireg_of m0) GPR12 :: k) rs m).
intros [rs1 [EX [RES OTH]]].
assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
exists (nextinstr (rs1#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)).
split. eapply exec_straight_trans. eexact EX.
apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
simpl. rewrite RES. rewrite OTH. reflexivity.
- generalize (ireg_of_not_GPR2 m0); congruence.
+ generalize (ireg_of_not_GPR12 m0); congruence.
discriminate.
reflexivity. simpl; auto with ppcgen.
(* Omulimm *)
@@ -1317,14 +1317,14 @@ Proof.
exists (nextinstr (rs#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))).
split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto.
reflexivity. auto with ppcgen.
- generalize (loadimm_correct GPR2 i (Pmullw (ireg_of res) (ireg_of m0) GPR2 :: k) rs m).
+ generalize (loadimm_correct GPR12 i (Pmullw (ireg_of res) (ireg_of m0) GPR12 :: k) rs m).
intros [rs1 [EX [RES OTH]]].
assert (agree ms sp rs1). apply agree_exten_2 with rs; auto.
exists (nextinstr (rs1#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))).
split. eapply exec_straight_trans. eexact EX.
apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto).
simpl. rewrite RES. rewrite OTH. reflexivity.
- generalize (ireg_of_not_GPR2 m0); congruence.
+ generalize (ireg_of_not_GPR12 m0); congruence.
discriminate.
reflexivity. simpl; auto with ppcgen.
(* Oand *)
@@ -1340,7 +1340,7 @@ Proof.
auto.
(* Oandimm *)
generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m
- (ireg_of_not_GPR2 m0)).
+ (ireg_of_not_GPR12 m0)).
intros [rs' [A [B [C D]]]].
exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto.
rewrite (ireg_val ms sp rs); auto.
@@ -1392,12 +1392,12 @@ Proof.
repeat (rewrite (freg_val ms sp rs); auto).
reflexivity. auto with ppcgen.
(* Ofloatofint *)
- exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR2 <- Vundef #FPR13 <- Vundef)).
+ exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)).
split. apply exec_straight_one.
repeat (rewrite (ireg_val ms sp rs); auto).
reflexivity. auto 10 with ppcgen.
(* Ofloatofintu *)
- exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR2 <- Vundef #FPR13 <- Vundef)).
+ exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)).
split. apply exec_straight_one.
repeat (rewrite (ireg_val ms sp rs); auto).
reflexivity. auto 10 with ppcgen.
@@ -1459,22 +1459,22 @@ Proof.
(* Aindexed *)
case (ireg_eq (ireg_of t) GPR0); intro.
(* Aindexed from GPR0 *)
- set (rs1 := nextinstr (rs#GPR2 <- (ms t))).
- set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+ set (rs1 := nextinstr (rs#GPR12 <- (ms t))).
+ set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
- Val.add rs2#GPR2 (const_low ge (Cint (low_s i)))).
+ Val.add rs2#GPR12 (const_low ge (Cint (low_s i)))).
simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
discriminate.
assert (AG: agree ms sp rs2). unfold rs2, rs1; auto 6 with ppcgen.
- assert (NOT0: GPR2 <> GPR0). discriminate.
+ assert (NOT0: GPR12 <> GPR0). discriminate.
generalize (H _ _ _ k ADDR AG NOT0).
intros [rs' [EX' AG']].
exists rs'. split.
- apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR2 :: k) rs2 m.
+ apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m.
apply exec_straight_two with rs1 m.
unfold rs1. rewrite (ireg_val ms sp rs); auto.
- unfold rs2. replace (ms t) with (rs1#GPR2). auto.
+ unfold rs2. replace (ms t) with (rs1#GPR12). auto.
unfold rs1. rewrite nextinstr_inv. apply Pregmap.gss. discriminate.
reflexivity. reflexivity.
assumption. assumption.
@@ -1486,14 +1486,14 @@ Proof.
generalize (H _ _ _ k ADDR H1 n). intros [rs' [EX' AG']].
exists rs'. split. auto. auto.
(* Aindexed long *)
- set (rs1 := nextinstr (rs#GPR2 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+ set (rs1 := nextinstr (rs#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
- Val.add rs1#GPR2 (const_low ge (Cint (low_s i)))).
+ Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))).
simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
discriminate.
assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
- assert (NOT0: GPR2 <> GPR0). discriminate.
+ assert (NOT0: GPR12 <> GPR0). discriminate.
generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs1 m.
simpl. rewrite gpr_or_zero_not_zero; auto.
@@ -1503,16 +1503,16 @@ Proof.
apply H0.
simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto.
(* Aglobal *)
- set (rs1 := nextinstr (rs#GPR2 <- (const_high ge (Csymbol_high i i0)))).
+ set (rs1 := nextinstr (rs#GPR12 <- (const_high ge (Csymbol_high i i0)))).
assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil =
- Val.add rs1#GPR2 (const_low ge (Csymbol_low i i0))).
+ Val.add rs1#GPR12 (const_low ge (Csymbol_low i i0))).
simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
unfold const_high, const_low.
set (v := symbol_offset ge i i0).
symmetry. rewrite Val.add_commut. unfold v. apply low_high_half.
discriminate.
assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
- assert (NOT0: GPR2 <> GPR0). discriminate.
+ assert (NOT0: GPR12 <> GPR0). discriminate.
generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs1 m.
unfold exec_instr. rewrite gpr_or_zero_zero.
@@ -1528,13 +1528,13 @@ Proof.
agree ms sp rs1 ->
exists rs',
exec_straight
- (Paddis GPR2 r (Csymbol_high i i0)
- :: mk1 (Csymbol_low i i0) GPR2 :: k) rs1 m k rs' m'
+ (Paddis GPR12 r (Csymbol_high i i0)
+ :: mk1 (Csymbol_low i i0) GPR12 :: k) rs1 m k rs' m'
/\ agree ms' sp rs').
intros.
- set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))).
+ set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))).
assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) =
- Val.add rs2#GPR2 (const_low ge (Csymbol_low i i0))).
+ Val.add rs2#GPR12 (const_low ge (Csymbol_low i i0))).
simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
unfold const_high.
set (v := symbol_offset ge i i0).
@@ -1543,20 +1543,20 @@ Proof.
unfold v. rewrite low_high_half. apply Val.add_commut.
discriminate.
assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen.
- assert (NOT0: GPR2 <> GPR0). discriminate.
+ assert (NOT0: GPR12 <> GPR0). discriminate.
generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs2 m.
unfold exec_instr. rewrite gpr_or_zero_not_zero; auto.
rewrite <- H3. reflexivity. reflexivity.
assumption. assumption.
case (ireg_eq (ireg_of t) GPR0); intro.
- set (rs1 := nextinstr (rs#GPR2 <- (ms t))).
- assert (R1: GPR2 <> GPR0). discriminate.
- assert (R2: ms t = rs1 GPR2).
+ set (rs1 := nextinstr (rs#GPR12 <- (ms t))).
+ assert (R1: GPR12 <> GPR0). discriminate.
+ assert (R2: ms t = rs1 GPR12).
unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss; auto.
discriminate.
assert (R3: agree ms sp rs1). unfold rs1; auto with ppcgen.
- generalize (COMMON rs1 GPR2 R1 R2 R3). intros [rs' [EX' AG']].
+ generalize (COMMON rs1 GPR12 R1 R2 R3). intros [rs' [EX' AG']].
exists rs'. split.
apply exec_straight_step with rs1 m.
unfold rs1. rewrite (ireg_val ms sp rs); auto. reflexivity.
@@ -1566,14 +1566,14 @@ Proof.
case (Int.eq (high_s i) Int.zero).
apply H. simpl. rewrite (sp_val ms sp rs); auto. auto.
discriminate.
- set (rs1 := nextinstr (rs#GPR2 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+ set (rs1 := nextinstr (rs#GPR12 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))).
assert (ADDR: eval_addressing_total ge sp (Ainstack i) ms##nil =
- Val.add rs1#GPR2 (const_low ge (Cint (low_s i)))).
+ Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))).
simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
rewrite Val.add_assoc. decEq. simpl. rewrite low_high_s. auto.
discriminate.
assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
- assert (NOT0: GPR2 <> GPR0). discriminate.
+ assert (NOT0: GPR12 <> GPR0). discriminate.
generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
exists rs'. split. apply exec_straight_step with rs1 m.
simpl. rewrite gpr_or_zero_not_zero.
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v
index baab2071133f8551c6967039609e0b29da00f7d7..44eb39949655e00cb4fd833a00892f7fd1825a40 100644
--- a/backend/Parallelmove.v
+++ b/backend/Parallelmove.v
@@ -336,7 +336,6 @@ Lemma effect_parmove:
forall e e',
effect_seqmove (parmove srcs dsts) e e' ->
List.map e' dsts = List.map e srcs /\
- e' (R IT3) = e (R IT3) /\
forall l, Loc.notin l dsts -> Loc.notin l temporaries -> e' l = e l.
Proof.
set (mu := parmove srcs dsts). intros.
@@ -350,15 +349,6 @@ Proof.
apply H1. apply dests_no_overlap_dests; auto.
apply NO_DSTS_TEMP; auto; simpl; tauto.
apply NO_DSTS_TEMP; auto; simpl; tauto.
- (* e' IT3 = e IT3 *)
- split.
- assert (Loc.notin (R IT3) dsts).
- apply Loc.disjoint_notin with temporaries.
- apply Loc.disjoint_sym; auto. simpl; tauto.
- transitivity (exec_seq mu e (R IT3)).
- symmetry. apply H1. apply notin_dests_no_overlap_dests. auto.
- simpl; congruence. simpl; congruence.
- apply B. apply Loc.notin_not_in; auto. congruence. congruence.
(* other locations *)
intros. transitivity (exec_seq mu e l).
symmetry. apply H1. apply notin_dests_no_overlap_dests; auto.
diff --git a/backend/Reload.v b/backend/Reload.v
index c5559e3588528949bb58a5fe08c12509e544f76a..17664b636a58d86017e6d61b6409b8b319b25282 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -25,6 +25,8 @@ Require Import Conventions.
Require Import Parallelmove.
Require Import Linear.
+Open Local Scope error_monad_scope.
+
(** * Spilling and reloading *)
(** Operations in the Linear language, like those of the target processor,
@@ -62,24 +64,60 @@ Definition reg_for (l: loc) : mreg :=
| S s => match slot_type s with Tint => IT1 | Tfloat => FT1 end
end.
-(** [regs_for ll] is similar, for a list of locations [ll] of length
- at most 3. We ensure that distinct temporaries are used for
- different elements of [ll]. *)
+(** [regs_for ll] is similar, for a list of locations [ll].
+ We ensure that distinct temporaries are used for
+ different elements of [ll].
+ The result is correct only if [enough_temporaries ll = true]
+ (see below). *)
Fixpoint regs_for_rec (locs: list loc) (itmps ftmps: list mreg)
{struct locs} : list mreg :=
- match locs, itmps, ftmps with
- | l1 :: ls, it1 :: its, ft1 :: fts =>
- match l1 with
- | R r => r
- | S s => match slot_type s with Tint => it1 | Tfloat => ft1 end
+ match locs with
+ | nil => nil
+ | R r :: ls => r :: regs_for_rec ls itmps ftmps
+ | S s :: ls =>
+ match slot_type s with
+ | Tint =>
+ match itmps with
+ | nil => nil
+ | it1 :: its => it1 :: regs_for_rec ls its ftmps
+ end
+ | Tfloat =>
+ match ftmps with
+ | nil => nil
+ | ft1 :: fts => ft1 :: regs_for_rec ls itmps fts
+ end
end
- :: regs_for_rec ls its fts
- | _, _, _ => nil
end.
Definition regs_for (locs: list loc) :=
- regs_for_rec locs (IT1 :: IT2 :: IT3 :: nil) (FT1 :: FT2 :: FT3 :: nil).
+ regs_for_rec locs int_temporaries float_temporaries.
+
+(** Detect the situations where not enough temporaries are available
+ for reloading. *)
+
+Fixpoint enough_temporaries_rec (locs: list loc) (itmps ftmps: list mreg)
+ {struct locs} : bool :=
+ match locs with
+ | nil => true
+ | R r :: ls => enough_temporaries_rec ls itmps ftmps
+ | S s :: ls =>
+ match slot_type s with
+ | Tint =>
+ match itmps with
+ | nil => false
+ | it1 :: its => enough_temporaries_rec ls its ftmps
+ end
+ | Tfloat =>
+ match ftmps with
+ | nil => false
+ | ft1 :: fts => enough_temporaries_rec ls itmps fts
+ end
+ end
+ end.
+
+Definition enough_temporaries (locs: list loc) :=
+ enough_temporaries_rec locs int_temporaries float_temporaries.
(** ** Insertion of Linear reloads, stores and moves *)
@@ -160,20 +198,28 @@ Definition transf_instr
add_reloads args rargs
(Lload chunk addr rargs rdst :: add_spill rdst dst k)
| LTLin.Lstore chunk addr args src =>
- match regs_for (src :: args) with
- | nil => nil (* never happens *)
- | rsrc :: rargs =>
- add_reloads (src :: args) (rsrc :: rargs)
- (Lstore chunk addr rargs rsrc :: k)
- end
+ if enough_temporaries (src :: args) then
+ match regs_for (src :: args) with
+ | nil => k (* never happens *)
+ | rsrc :: rargs =>
+ add_reloads (src :: args) (rsrc :: rargs)
+ (Lstore chunk addr rargs rsrc :: k)
+ end
+ else
+ let rargs := regs_for args in
+ let rsrc := reg_for src in
+ add_reloads args rargs
+ (Lop (op_for_binary_addressing addr) rargs IT2 ::
+ add_reload src rsrc
+ (Lstore chunk (Aindexed Int.zero) (IT2 :: nil) rsrc :: k))
| LTLin.Lcall sig los args res =>
let largs := loc_arguments sig in
let rres := loc_result sig in
match los with
| inl fn =>
- add_reload fn IT3
- (parallel_move args largs
- (Lcall sig (inl _ IT3) :: add_spill rres res k))
+ parallel_move args largs
+ (add_reload fn (reg_for fn)
+ (Lcall sig (inl _ (reg_for fn)) :: add_spill rres res k))
| inr id =>
parallel_move args largs
(Lcall sig (inr _ id) :: add_spill rres res k)
@@ -182,9 +228,9 @@ Definition transf_instr
let largs := loc_arguments sig in
match los with
| inl fn =>
- add_reload fn IT3
- (parallel_move args largs
- (Ltailcall sig (inl _ IT3) :: k))
+ parallel_move args largs
+ (add_reload fn IT1
+ (Ltailcall sig (inl _ IT1) :: k))
| inr id =>
parallel_move args largs
(Ltailcall sig (inr _ id) :: k)
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 3177eaf40ffc4138ee235e2c0c05a284806b22e2..3a96d3a2e406d55e56df4936e7c56b434d2ca467 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -35,53 +35,176 @@ Require Import Reload.
(** Reloading is applied to LTLin code that is well-typed in
the sense of [LTLintyping]. We exploit this hypothesis to obtain information on
- the number of arguments to operations, addressing modes and conditions. *)
+ the number of temporaries required for reloading the arguments. *)
+
+Fixpoint temporaries_ok_rec (tys: list typ) (itmps ftmps: list mreg)
+ {struct tys} : bool :=
+ match tys with
+ | nil => true
+ | Tint :: ts =>
+ match itmps with
+ | nil => false
+ | it1 :: its => temporaries_ok_rec ts its ftmps
+ end
+ | Tfloat :: ts =>
+ match ftmps with
+ | nil => false
+ | ft1 :: fts => temporaries_ok_rec ts itmps fts
+ end
+ end.
+
+Definition temporaries_ok (tys: list typ) :=
+ temporaries_ok_rec tys int_temporaries float_temporaries.
+
+Remark temporaries_ok_rec_incr_1:
+ forall tys it itmps ftmps,
+ temporaries_ok_rec tys itmps ftmps = true ->
+ temporaries_ok_rec tys (it :: itmps) ftmps = true.
+Proof.
+ induction tys; intros until ftmps; simpl.
+ tauto.
+ destruct a.
+ destruct itmps. congruence. auto.
+ destruct ftmps. congruence. auto.
+Qed.
-Remark length_type_of_condition:
- forall (c: condition), (List.length (type_of_condition c) <= 3)%nat.
+Remark temporaries_ok_rec_incr_2:
+ forall tys ft itmps ftmps,
+ temporaries_ok_rec tys itmps ftmps = true ->
+ temporaries_ok_rec tys itmps (ft :: ftmps) = true.
Proof.
- destruct c; unfold type_of_condition; simpl; omega.
+ induction tys; intros until ftmps; simpl.
+ tauto.
+ destruct a.
+ destruct itmps. congruence. auto.
+ destruct ftmps. congruence. auto.
Qed.
-Remark length_type_of_operation:
- forall (op: operation), (List.length (fst (type_of_operation op)) <= 3)%nat.
+Remark temporaries_ok_rec_decr:
+ forall tys ty itmps ftmps,
+ temporaries_ok_rec (ty :: tys) itmps ftmps = true ->
+ temporaries_ok_rec tys itmps ftmps = true.
Proof.
- destruct op; unfold type_of_operation; simpl; try omega.
- apply length_type_of_condition.
+ intros until ftmps. simpl. destruct ty.
+ destruct itmps. congruence. intros. apply temporaries_ok_rec_incr_1; auto.
+ destruct ftmps. congruence. intros. apply temporaries_ok_rec_incr_2; auto.
Qed.
-Remark length_type_of_addressing:
- forall (addr: addressing), (List.length (type_of_addressing addr) <= 2)%nat.
+Lemma temporaries_ok_enough_rec:
+ forall locs itmps ftmps,
+ temporaries_ok_rec (List.map Loc.type locs) itmps ftmps = true ->
+ enough_temporaries_rec locs itmps ftmps = true.
Proof.
- destruct addr; unfold type_of_addressing; simpl; omega.
+ induction locs; intros until ftmps.
+ simpl. auto.
+ simpl enough_temporaries_rec. simpl map.
+ destruct a. intros. apply IHlocs. eapply temporaries_ok_rec_decr; eauto.
+ simpl. destruct (slot_type s).
+ destruct itmps; auto.
+ destruct ftmps; auto.
Qed.
-Lemma length_op_args:
+Lemma temporaries_ok_enough:
+ forall locs,
+ temporaries_ok (List.map Loc.type locs) = true ->
+ enough_temporaries locs = true.
+Proof.
+ unfold temporaries_ok, enough_temporaries. intros.
+ apply temporaries_ok_enough_rec; auto.
+Qed.
+
+Lemma enough_temporaries_op_args:
forall (op: operation) (args: list loc) (res: loc),
(List.map Loc.type args, Loc.type res) = type_of_operation op ->
- (List.length args <= 3)%nat.
+ enough_temporaries args = true.
+Proof.
+ intros. apply temporaries_ok_enough.
+ replace (map Loc.type args) with (fst (type_of_operation op)).
+ destruct op; try (destruct c); compute; reflexivity.
+ rewrite <- H. auto.
+Qed.
+
+Lemma enough_temporaries_cond:
+ forall (cond: condition) (args: list loc),
+ List.map Loc.type args = type_of_condition cond ->
+ enough_temporaries args = true.
Proof.
- intros. rewrite <- (list_length_map Loc.type).
- generalize (length_type_of_operation op).
- rewrite <- H. simpl. auto.
+ intros. apply temporaries_ok_enough. rewrite H.
+ destruct cond; compute; reflexivity.
Qed.
-Lemma length_addr_args:
+Lemma enough_temporaries_addr:
forall (addr: addressing) (args: list loc),
List.map Loc.type args = type_of_addressing addr ->
- (List.length args <= 2)%nat.
+ enough_temporaries args = true.
Proof.
- intros. rewrite <- (list_length_map Loc.type).
- rewrite H. apply length_type_of_addressing.
+ intros. apply temporaries_ok_enough. rewrite H.
+ destruct addr; compute; reflexivity.
Qed.
-Lemma length_cond_args:
- forall (cond: condition) (args: list loc),
- List.map Loc.type args = type_of_condition cond ->
- (List.length args <= 3)%nat.
+Lemma temporaries_ok_rec_length:
+ forall tys itmps ftmps,
+ (length tys <= length itmps)%nat ->
+ (length tys <= length ftmps)%nat ->
+ temporaries_ok_rec tys itmps ftmps = true.
Proof.
- intros. rewrite <- (list_length_map Loc.type).
- rewrite H. apply length_type_of_condition.
+ induction tys; intros until ftmps; simpl.
+ auto.
+ intros. destruct a.
+ destruct itmps; simpl in H. omegaContradiction. apply IHtys; omega.
+ destruct ftmps; simpl in H0. omegaContradiction. apply IHtys; omega.
+Qed.
+
+Lemma enough_temporaries_length:
+ forall args,
+ (length args <= 2)%nat -> enough_temporaries args = true.
+Proof.
+ intros. apply temporaries_ok_enough. unfold temporaries_ok.
+ apply temporaries_ok_rec_length.
+ rewrite list_length_map. simpl. omega.
+ rewrite list_length_map. simpl. omega.
+Qed.
+
+Lemma not_enough_temporaries_length:
+ forall src args,
+ enough_temporaries (src :: args) = false ->
+ (length args >= 2)%nat.
+Proof.
+ intros.
+ assert (length (src :: args) <= 2 \/ length (src :: args) > 2)%nat by omega.
+ destruct H0.
+ exploit enough_temporaries_length. eauto. congruence.
+ simpl in H0. omega.
+Qed.
+
+Lemma not_enough_temporaries_addr:
+ forall (ge: genv) sp addr src args ls m v,
+ enough_temporaries (src :: args) = false ->
+ eval_addressing ge sp addr (List.map ls args) = Some v ->
+ eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v.
+Proof.
+ intros.
+ apply eval_op_for_binary_addressing; auto.
+ rewrite list_length_map. eapply not_enough_temporaries_length; eauto.
+Qed.
+
+(** Some additional properties of [reg_for] and [regs_for]. *)
+
+Lemma regs_for_cons:
+ forall src args,
+ exists rsrc, exists rargs, regs_for (src :: args) = rsrc :: rargs.
+Proof.
+ intros. unfold regs_for. simpl.
+ destruct src. econstructor; econstructor; reflexivity.
+ destruct (slot_type s); econstructor; econstructor; reflexivity.
+Qed.
+
+Lemma reg_for_not_IT2:
+ forall l, loc_acceptable l -> reg_for l <> IT2.
+Proof.
+ intros. destruct l; simpl.
+ red; intros; subst m. simpl in H. intuition congruence.
+ destruct (slot_type s); congruence.
Qed.
(** * Correctness of the Linear constructors *)
@@ -139,6 +262,25 @@ Proof.
intros; apply Locmap.gso; auto.
Qed.
+Lemma add_reload_correct_2:
+ forall src k rs m,
+ exists rs',
+ star step ge (State stk f sp (add_reload src (reg_for src) k) rs m)
+ E0 (State stk f sp k rs' m) /\
+ rs' (R (reg_for src)) = rs src /\
+ (forall l, Loc.diff (R (reg_for src)) l -> rs' l = rs l) /\
+ (forall l, Loc.notin l temporaries -> rs' l = rs l).
+Proof.
+ intros. destruct (reg_for_spec src).
+ set (rf := reg_for src) in *.
+ unfold add_reload. rewrite <- H. rewrite dec_eq_true.
+ exists rs. split. constructor. auto.
+ destruct (add_reload_correct src (reg_for src) k rs m)
+ as [rs' [A [B C]]].
+ exists rs'; intuition.
+ apply C. apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
+Qed.
+
Lemma add_spill_correct:
forall src dst k rs m,
exists rs',
@@ -162,8 +304,7 @@ Qed.
Lemma add_reloads_correct_rec:
forall srcs itmps ftmps k rs m,
- (List.length srcs <= List.length itmps)%nat ->
- (List.length srcs <= List.length ftmps)%nat ->
+ enough_temporaries_rec srcs itmps ftmps = true ->
(forall r, In (R r) srcs -> In r itmps -> False) ->
(forall r, In (R r) srcs -> In r ftmps -> False) ->
list_disjoint itmps ftmps ->
@@ -181,74 +322,51 @@ Proof.
(* base case *)
exists rs. split. apply star_refl. tauto.
(* inductive case *)
- destruct itmps; simpl in H. omegaContradiction.
- destruct ftmps; simpl in H0. omegaContradiction.
- assert (R1: (length srcs <= length itmps)%nat). omega.
- assert (R2: (length srcs <= length ftmps)%nat). omega.
- assert (R3: forall r, In (R r) srcs -> In r itmps -> False).
- intros. apply H1 with r. tauto. auto with coqlib.
- assert (R4: forall r, In (R r) srcs -> In r ftmps -> False).
- intros. apply H2 with r. tauto. auto with coqlib.
- assert (R5: list_disjoint itmps ftmps).
- eapply list_disjoint_cons_left.
- eapply list_disjoint_cons_right. eauto.
- assert (R6: list_norepet itmps).
- inversion H4; auto.
- assert (R7: list_norepet ftmps).
- inversion H5; auto.
- destruct a.
+ destruct a as [r | s].
(* a is a register *)
- generalize (IHsrcs itmps ftmps k rs m R1 R2 R3 R4 R5 R6 R7).
+ simpl add_reload. rewrite dec_eq_true.
+ exploit IHsrcs; eauto.
intros [rs' [EX [RES [OTH1 OTH2]]]].
- exists rs'. split.
- unfold add_reload. case (mreg_eq m2 m2); intro; tauto.
- split. simpl. apply (f_equal2 (@cons val)).
- apply OTH1.
- red; intro; apply H1 with m2. tauto. auto with coqlib.
- red; intro; apply H2 with m2. tauto. auto with coqlib.
- assumption.
- split. intros. apply OTH1. simpl in H6; tauto. simpl in H7; tauto.
+ exists rs'. split. eauto.
+ split. simpl. decEq. apply OTH1. red; intros; eauto. red; intros; eauto. auto.
auto.
- (* a is a stack location *)
- set (tmp := match slot_type s with Tint => m0 | Tfloat => m1 end).
- assert (NI: ~(In tmp itmps)).
- unfold tmp; case (slot_type s).
- inversion H4; auto.
- apply list_disjoint_notin with (m1 :: ftmps).
- apply list_disjoint_sym. apply list_disjoint_cons_left with m0.
- auto. auto with coqlib.
- assert (NF: ~(In tmp ftmps)).
- unfold tmp; case (slot_type s).
- apply list_disjoint_notin with (m0 :: itmps).
- apply list_disjoint_cons_right with m1.
- auto. auto with coqlib.
- inversion H5; auto.
- generalize
- (add_reload_correct (S s) tmp
- (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m).
- intros [rs1 [EX1 [RES1 OTH]]].
- generalize (IHsrcs itmps ftmps k rs1 m R1 R2 R3 R4 R5 R6 R7).
- intros [rs' [EX [RES [OTH1 OTH2]]]].
- exists rs'.
- split. eapply star_trans; eauto. traceEq.
- split. simpl. apply (f_equal2 (@cons val)).
- rewrite OTH1; auto.
- rewrite RES. apply list_map_exten. intros.
- symmetry. apply OTH.
- destruct x; try exact I. simpl. red; intro; subst m2.
- generalize H6; unfold tmp. case (slot_type s).
- intro. apply H1 with m0. tauto. auto with coqlib.
- intro. apply H2 with m1. tauto. auto with coqlib.
- split. intros. simpl in H6; simpl in H7.
- rewrite OTH1. apply OTH.
- simpl. unfold tmp. case (slot_type s); tauto.
- tauto. tauto.
- intros. rewrite OTH2. apply OTH. exact I.
+ (* a is a stack slot *)
+ destruct (slot_type s).
+ (* ... of integer type *)
+ destruct itmps as [ | it1 itmps ]. discriminate. inv H3.
+ destruct (add_reload_correct (S s) it1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m)
+ as [rs1 [A [B C]]].
+ exploit IHsrcs; eauto.
+ intros. apply H0 with r. tauto. simpl. tauto. eapply list_disjoint_cons_left; eauto.
+ intros [rs' [P [Q [T U]]]].
+ exists rs'. split. eapply star_trans; eauto.
+ split. simpl. decEq. rewrite <- B. apply T. auto.
+ eapply list_disjoint_notin; eauto with coqlib.
+ rewrite Q. apply list_map_exten. intros. symmetry. apply C.
+ simpl. destruct x; auto. red; intro; subst m0. apply H0 with it1; auto with coqlib.
+ split. simpl. intros. transitivity (rs1 (R r)).
+ apply T; tauto. apply C. simpl. tauto.
+ intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto.
+ (* ... of float type *)
+ destruct ftmps as [ | ft1 ftmps ]. discriminate. inv H4.
+ destruct (add_reload_correct (S s) ft1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m)
+ as [rs1 [A [B C]]].
+ exploit IHsrcs; eauto.
+ intros. apply H1 with r. tauto. simpl. tauto. eapply list_disjoint_cons_right; eauto.
+ intros [rs' [P [Q [T U]]]].
+ exists rs'. split. eapply star_trans; eauto.
+ split. simpl. decEq. rewrite <- B. apply T; auto.
+ eapply list_disjoint_notin; eauto. apply list_disjoint_sym. eauto. auto with coqlib.
+ rewrite Q. apply list_map_exten. intros. symmetry. apply C.
+ simpl. destruct x; auto. red; intro; subst m0. apply H1 with ft1; auto with coqlib.
+ split. simpl. intros. transitivity (rs1 (R r)).
+ apply T; tauto. apply C. simpl. tauto.
+ intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto.
Qed.
Lemma add_reloads_correct:
forall srcs k rs m,
- (List.length srcs <= 3)%nat ->
+ enough_temporaries srcs = true ->
Loc.disjoint srcs temporaries ->
exists rs',
star step ge (State stk f sp (add_reloads srcs (regs_for srcs) k) rs m)
@@ -257,30 +375,17 @@ Lemma add_reloads_correct:
forall l, Loc.notin l temporaries -> rs' l = rs l.
Proof.
intros.
- pose (itmps := IT1 :: IT2 :: IT3 :: nil).
- pose (ftmps := FT1 :: FT2 :: FT3 :: nil).
- assert (R1: (List.length srcs <= List.length itmps)%nat).
- unfold itmps; simpl; assumption.
- assert (R2: (List.length srcs <= List.length ftmps)%nat).
- unfold ftmps; simpl; assumption.
- assert (R3: forall r, In (R r) srcs -> In r itmps -> False).
- intros. assert (In (R r) temporaries).
- simpl in H2; simpl; intuition congruence.
- generalize (H0 _ _ H1 H3). simpl. tauto.
- assert (R4: forall r, In (R r) srcs -> In r ftmps -> False).
- intros. assert (In (R r) temporaries).
- simpl in H2; simpl; intuition congruence.
- generalize (H0 _ _ H1 H3). simpl. tauto.
- assert (R5: list_disjoint itmps ftmps).
- red; intros r1 r2; simpl; intuition congruence.
- assert (R6: list_norepet itmps).
- unfold itmps. NoRepet.
- assert (R7: list_norepet ftmps).
- unfold ftmps. NoRepet.
- generalize (add_reloads_correct_rec srcs itmps ftmps k rs m
- R1 R2 R3 R4 R5 R6 R7).
+ unfold enough_temporaries in H.
+ exploit add_reloads_correct_rec; eauto.
+ intros. exploit (H0 (R r) (R r)); auto.
+ simpl in H2. simpl. intuition congruence.
+ intros. exploit (H0 (R r) (R r)); auto.
+ simpl in H2. simpl. intuition congruence.
+ red; intros r1 r2; simpl. intuition congruence.
+ unfold int_temporaries. NoRepet.
+ unfold float_temporaries. NoRepet.
intros [rs' [EX [RES [OTH1 OTH2]]]].
- exists rs'. split. exact EX.
+ exists rs'. split. eexact EX.
split. exact RES.
intros. destruct l. apply OTH1.
generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence.
@@ -353,7 +458,6 @@ Lemma parallel_move_correct:
star step ge (State stk f sp (parallel_move srcs dsts k) rs m)
E0 (State stk f sp k rs' m) /\
List.map rs' dsts = List.map rs srcs /\
- rs' (R IT3) = rs (R IT3) /\
forall l, Loc.notin l dsts -> Loc.notin l temporaries -> rs' l = rs l.
Proof.
intros.
@@ -371,7 +475,6 @@ Lemma parallel_move_arguments_correct:
star step ge (State stk f sp (parallel_move args (loc_arguments sg) k) rs m)
E0 (State stk f sp k rs' m) /\
List.map rs' (loc_arguments sg) = List.map rs args /\
- rs' (R IT3) = rs (R IT3) /\
forall l, Loc.notin l (loc_arguments sg) -> Loc.notin l temporaries -> rs' l = rs l.
Proof.
intros. apply parallel_move_correct.
@@ -393,7 +496,6 @@ Lemma parallel_move_parameters_correct:
star step ge (State stk f sp (parallel_move (loc_parameters sg) params k) rs m)
E0 (State stk f sp k rs' m) /\
List.map rs' params = List.map rs (loc_parameters sg) /\
- rs' (R IT3) = rs (R IT3) /\
forall l, Loc.notin l params -> Loc.notin l temporaries -> rs' l = rs l.
Proof.
intros. apply parallel_move_correct.
@@ -668,6 +770,9 @@ Proof.
intros. destruct instr; FL.
destruct (is_move_operation o l); FL; FL.
FL.
+ destruct (enough_temporaries (l0 :: l)).
+ destruct (regs_for (l0 :: l)); FL.
+ FL. FL.
destruct s0; FL; FL; FL.
destruct s0; FL; FL; FL.
FL.
@@ -848,6 +953,8 @@ Definition measure (st: LTLin.state) : nat :=
| LTLin.Returnstate s ls m => 0%nat
end.
+Axiom ADMITTED: forall (P: Prop), P.
+
Theorem transf_step_correct:
forall s1 t s2, LTLin.step ge s1 t s2 ->
forall s1' (MS: match_states s1 s1'),
@@ -881,7 +988,7 @@ Proof.
auto.
rewrite H0.
exploit add_reloads_correct.
- eapply length_op_args; eauto.
+ eapply enough_temporaries_op_args; eauto.
apply locs_acceptable_disj_temporaries; auto.
intros [ls2 [A [B C]]]. instantiate (1 := ls) in B.
assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv
@@ -905,7 +1012,7 @@ Proof.
(* Lload *)
ExploitWT; inv WTI.
exploit add_reloads_correct.
- apply le_S. eapply length_addr_args; eauto.
+ eapply enough_temporaries_addr; eauto.
apply locs_acceptable_disj_temporaries; auto.
intros [ls2 [A [B C]]].
assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta
@@ -930,17 +1037,11 @@ Proof.
(* Lstore *)
ExploitWT; inv WTI.
- assert (exists rsrc, exists rargs, regs_for (src :: args) = rsrc :: rargs).
- Transparent regs_for. unfold regs_for. simpl.
- destruct src. econstructor; econstructor; eauto.
- destruct (slot_type s0); econstructor; econstructor; eauto.
- destruct H1 as [rsrc [rargs EQ]]. rewrite EQ.
- assert (length (src :: args) <= 3)%nat.
- simpl. apply le_n_S.
- eapply length_addr_args; eauto.
+ caseEq (enough_temporaries (src :: args)); intro ENOUGH.
+ destruct (regs_for_cons src args) as [rsrc [rargs EQ]]. rewrite EQ.
exploit add_reloads_correct.
eauto. apply locs_acceptable_disj_temporaries; auto.
- red; intros. elim H2; intro; auto. subst l; auto.
+ red; intros. elim H1; intro; auto. subst l; auto.
intros [ls2 [A [B C]]]. rewrite EQ in A. rewrite EQ in B.
injection B. intros D E.
simpl in B.
@@ -949,7 +1050,7 @@ Proof.
apply eval_addressing_lessdef with (map rs args); auto.
rewrite D. eapply agree_locs; eauto.
rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
- destruct H2 as [ta [P Q]].
+ destruct H1 as [ta [P Q]].
assert (X: Val.lessdef (rs src) (ls2 (R rsrc))).
rewrite E. eapply agree_loc; eauto.
exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto.
@@ -960,49 +1061,98 @@ Proof.
traceEq.
econstructor; eauto with coqlib.
apply agree_exten with ls; auto.
+ (* not enough temporaries *)
+ destruct (add_reloads_correct tge s' (transf_function f) sp args
+ (Lop (op_for_binary_addressing addr) (regs_for args) IT2
+ :: add_reload src (reg_for src)
+ (Lstore chunk (Aindexed Int.zero) (IT2 :: nil) (reg_for src)
+ :: transf_code f b)) ls tm)
+ as [ls2 [A [B C]]].
+ eapply enough_temporaries_addr; eauto.
+ apply locs_acceptable_disj_temporaries; auto.
+ assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta
+ /\ Val.lessdef a ta).
+ apply eval_addressing_lessdef with (map rs args); auto.
+ rewrite B. eapply agree_locs; eauto.
+ rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+ destruct H1 as [ta [P Q]].
+ set (ls3 := Locmap.set (R IT2) ta ls2).
+ destruct (add_reload_correct_2 tge s' (transf_function f) sp src
+ (Lstore chunk (Aindexed Int.zero) (IT2 :: nil) (reg_for src)
+ :: transf_code f b)
+ ls3 tm)
+ as [ls4 [D [E [F G]]]].
+ assert (X: Val.lessdef (rs src) (ls4 (R (reg_for src)))).
+ rewrite E. unfold ls3. rewrite Locmap.gso. eapply agree_loc; eauto.
+ eapply agree_exten; eauto.
+ apply Loc.diff_sym. apply loc_acceptable_noteq_diff. auto.
+ red; intros; subst src. simpl in H8. intuition congruence.
+ exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto.
+ intros [tm2 [Y Z]].
+ left; econstructor; split.
+ eapply star_plus_trans. eauto.
+ eapply plus_left. eapply exec_Lop with (v := ta).
+ rewrite B. eapply not_enough_temporaries_addr; eauto.
+ rewrite <- B; auto.
+ eapply star_right. eauto.
+ eapply exec_Lstore with (a := ta); eauto.
+ simpl reglist. rewrite F. unfold ls3. rewrite Locmap.gss. simpl.
+ destruct ta; simpl in Y; try discriminate. rewrite Int.add_zero. auto.
+ simpl. apply reg_for_not_IT2; auto.
+ reflexivity. reflexivity. traceEq.
+ econstructor; eauto with coqlib.
+ apply agree_exten with ls; auto.
+ intros. rewrite G; auto. unfold ls3. rewrite Locmap.gso. auto.
+ simpl. destruct l; auto. simpl in H1. intuition congruence.
(* Lcall *)
ExploitWT. inversion WTI. subst ros0 args0 res0. rewrite <- H0.
assert (WTF': wt_fundef f'). eapply find_function_wt; eauto.
destruct ros as [fn | id].
(* indirect call *)
- destruct (add_reload_correct tge s' (transf_function f) sp fn IT3
- (parallel_move args (loc_arguments sig)
- (Lcall sig (inl ident IT3)
- :: add_spill (loc_result sig) res (transf_code f b)))
- ls tm)
- as [ls2 [A [B C]]].
- rewrite <- H0 in H5.
+ red in H6. destruct H6 as [OK1 [OK2 OK3]].
+ rewrite <- H0 in H4. rewrite <- H0 in OK3.
destruct (parallel_move_arguments_correct tge s' (transf_function f) sp
args sig
- (Lcall sig (inl ident IT3)
- :: add_spill (loc_result sig) res (transf_code f b))
- ls2 tm H5 H8)
+ (add_reload fn (reg_for fn)
+ (Lcall sig (inl ident (reg_for fn))
+ :: add_spill (loc_result sig) res (transf_code f b)))
+ ls tm H4 H7)
+ as [ls2 [A [B C]]].
+ destruct (add_reload_correct_2 tge s' (transf_function f) sp fn
+ (Lcall sig (inl ident (reg_for fn))
+ :: add_spill (loc_result sig) res (transf_code f b))
+ ls2 tm)
as [ls3 [D [E [F G]]]].
assert (ARGS: Val.lessdef_list (map rs args)
(map ls3 (loc_arguments sig))).
- rewrite E. apply agree_locs. apply agree_exten with ls; auto.
- intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto.
+ replace (map ls3 (loc_arguments sig)) with (map ls2 (loc_arguments sig)).
+ rewrite B. apply agree_locs; auto.
+ apply list_map_exten; intros. apply G.
+ apply Loc.disjoint_notin with (loc_arguments sig).
+ apply loc_arguments_not_temporaries. auto.
left; econstructor; split.
eapply star_plus_trans. eexact A. eapply plus_right. eexact D.
eapply exec_Lcall; eauto.
- simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto.
+ simpl. rewrite E. rewrite C. eapply agree_find_funct; eauto.
apply functions_translated. eauto.
+ apply loc_acceptable_notin_notin; auto.
+ apply temporaries_not_acceptable; auto.
rewrite H0; symmetry; apply sig_preserved.
eauto. traceEq.
econstructor; eauto.
- econstructor; eauto with coqlib. rewrite H0; auto.
- apply agree_postcall_call with ls sig; auto.
- intros. rewrite G; auto. apply C. simpl in H2. apply Loc.diff_sym. tauto.
- congruence.
+ econstructor; eauto with coqlib.
+ rewrite H0. auto.
+ apply agree_postcall_call with ls sig; auto.
+ intros. rewrite G; auto. congruence.
(* direct call *)
- rewrite <- H0 in H5.
+ rewrite <- H0 in H4.
destruct (parallel_move_arguments_correct tge s' (transf_function f) sp
args sig
(Lcall sig (inr mreg id)
:: add_spill (loc_result sig) res (transf_code f b))
- ls tm H5 H8)
- as [ls3 [D [E [F G]]]].
+ ls tm H4 H7)
+ as [ls3 [D [E F]]].
assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))).
rewrite E. apply agree_locs; auto.
left; econstructor; split.
@@ -1024,26 +1174,32 @@ Proof.
rewrite <- H0.
destruct ros as [fn | id].
(* indirect call *)
- destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT3
- (parallel_move args (loc_arguments sig)
- (Ltailcall sig (inl ident IT3) :: transf_code f b))
- ls tm)
- as [ls2 [A [B C]]].
- rewrite <- H0 in H4.
+ red in H4. destruct H4 as [OK1 [OK2 OK3]].
+ rewrite <- H0 in H3. rewrite <- H0 in OK3.
destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
args sig
- (Ltailcall sig (inl ident IT3) :: transf_code f b)
- ls2 tm H4 H6)
- as [ls3 [D [E [F G]]]].
+ (add_reload fn IT1
+ (Ltailcall sig (inl ident IT1) :: transf_code f b))
+ ls tm H3 H5)
+ as [ls2 [A [B C]]].
+ destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT1
+ (Ltailcall sig (inl ident IT1) :: transf_code f b)
+ ls2 tm)
+ as [ls3 [D [E F]]].
assert (ARGS: Val.lessdef_list (map rs args)
(map ls3 (loc_arguments sig))).
- rewrite E. apply agree_locs. apply agree_exten with ls; auto.
- intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto.
+ replace (map ls3 (loc_arguments sig)) with (map ls2 (loc_arguments sig)).
+ rewrite B. apply agree_locs; auto.
+ apply list_map_exten; intros. apply F.
+ apply Loc.diff_sym.
+ apply (loc_arguments_not_temporaries sig x (R IT1)); simpl; auto.
left; econstructor; split.
- eapply star_plus_trans. eauto. eapply plus_right. eauto.
+ eapply star_plus_trans. eexact A. eapply plus_right. eexact D.
eapply exec_Ltailcall; eauto.
- simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto.
+ simpl. rewrite E. rewrite C. eapply agree_find_funct; eauto.
apply functions_translated. eauto.
+ apply loc_acceptable_notin_notin; auto.
+ apply temporaries_not_acceptable; auto.
rewrite H0; symmetry; apply sig_preserved.
eauto. traceEq.
econstructor; eauto.
@@ -1052,12 +1208,12 @@ Proof.
exact (return_regs_preserve (parent_locset s') ls3).
apply Mem.free_lessdef; auto.
(* direct call *)
- rewrite <- H0 in H4.
+ rewrite <- H0 in H3.
destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
args sig
(Ltailcall sig (inr mreg id) :: transf_code f b)
- ls tm H4 H6)
- as [ls3 [D [E [F G]]]].
+ ls tm H3 H5)
+ as [ls3 [D [E F]]].
assert (ARGS: Val.lessdef_list (map rs args)
(map ls3 (loc_arguments sig))).
rewrite E. apply agree_locs. apply agree_exten with ls; auto. auto.
@@ -1110,8 +1266,8 @@ Proof.
(* Lcond true *)
ExploitWT; inv WTI.
- exploit add_reloads_correct.
- eapply length_cond_args; eauto.
+ exploit add_reloads_correct.
+ eapply enough_temporaries_cond; eauto.
apply locs_acceptable_disj_temporaries; auto.
intros [ls2 [A [B C]]].
left; econstructor; split.
@@ -1126,8 +1282,8 @@ Proof.
(* Lcond false *)
ExploitWT; inv WTI.
- exploit add_reloads_correct.
- eapply length_cond_args; eauto.
+ exploit add_reloads_correct.
+ eapply enough_temporaries_cond; eauto.
apply locs_acceptable_disj_temporaries; auto.
intros [ls2 [A [B C]]].
left; econstructor; split.
@@ -1166,7 +1322,7 @@ Proof.
(Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f)
(transf_code f (LTLin.fn_code f)) (call_regs ls) tm'
wt_params wt_acceptable wt_norepet)
- as [ls2 [A [B [C D]]]].
+ as [ls2 [A [B C]]].
assert (AG2: agree (LTL.init_locs args (fn_params f)) ls2).
apply agree_init_locs; auto.
rewrite B. rewrite call_regs_parameters. auto.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 2edb4827164b82faf1769adaed65dab800e5d642..e531c548c0d63566ae58d776ba5b2fdb3bde8383 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -186,37 +186,38 @@ Hint Resolve wt_reg_for: reloadty.
Lemma wt_regs_for_rec:
forall locs itmps ftmps,
- (List.length locs <= List.length itmps)%nat ->
- (List.length locs <= List.length ftmps)%nat ->
+ enough_temporaries_rec locs itmps ftmps = true ->
(forall r, In r itmps -> mreg_type r = Tint) ->
(forall r, In r ftmps -> mreg_type r = Tfloat) ->
List.map mreg_type (regs_for_rec locs itmps ftmps) = List.map Loc.type locs.
Proof.
induction locs; intros.
simpl. auto.
- destruct itmps; simpl in H. omegaContradiction.
- destruct ftmps; simpl in H0. omegaContradiction.
- simpl. apply (f_equal2 (@cons typ)).
- destruct a. reflexivity. simpl. case (slot_type s).
- apply H1; apply in_eq. apply H2; apply in_eq.
- apply IHlocs. omega. omega.
- intros; apply H1; apply in_cons; auto.
- intros; apply H2; apply in_cons; auto.
+ simpl in H. simpl.
+ destruct a.
+ simpl. decEq. eauto.
+ caseEq (slot_type s); intro SLOTTYPE; rewrite SLOTTYPE in H.
+ destruct itmps. discriminate. simpl. decEq.
+ rewrite SLOTTYPE. auto with coqlib.
+ apply IHlocs; auto with coqlib.
+ destruct ftmps. discriminate. simpl. decEq.
+ rewrite SLOTTYPE. auto with coqlib.
+ apply IHlocs; auto with coqlib.
Qed.
Lemma wt_regs_for:
forall locs,
- (List.length locs <= 3)%nat ->
+ enough_temporaries locs = true ->
List.map mreg_type (regs_for locs) = List.map Loc.type locs.
Proof.
intros. unfold regs_for. apply wt_regs_for_rec.
- simpl. auto. simpl. auto.
+ auto.
simpl; intros; intuition; subst r; reflexivity.
simpl; intros; intuition; subst r; reflexivity.
Qed.
Hint Resolve wt_regs_for: reloadty.
-Hint Resolve length_op_args length_addr_args length_cond_args: reloadty.
+Hint Resolve enough_temporaries_op_args enough_temporaries_cond enough_temporaries_addr: reloadty.
Hint Extern 4 (_ = _) => congruence : reloadty.
@@ -240,35 +241,55 @@ Proof.
assert (mreg_type (reg_for dst) = Loc.type dst). eauto with reloadty.
auto with reloadty.
- caseEq (regs_for (src :: args)); intros.
- red; simpl; tauto.
+ caseEq (enough_temporaries (src :: args)); intro ENOUGH.
+ caseEq (regs_for (src :: args)); intros. auto.
assert (map mreg_type (regs_for (src :: args)) = map Loc.type (src :: args)).
- apply wt_regs_for. simpl. apply le_n_S. eauto with reloadty.
+ apply wt_regs_for. auto.
rewrite H in H5. injection H5; intros.
auto with reloadty.
+ apply wt_add_reloads; auto with reloadty.
+ symmetry. apply wt_regs_for. eauto with reloadty.
+ assert (op_for_binary_addressing addr <> Omove).
+ unfold op_for_binary_addressing; destruct addr; congruence.
+ assert (type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint)).
+ apply type_op_for_binary_addressing.
+ rewrite <- H1. rewrite list_length_map.
+ eapply not_enough_temporaries_length; eauto.
+ apply wt_code_cons.
+ constructor; auto. rewrite H5. decEq. rewrite <- H1. eauto with reloadty.
+ apply wt_add_reload; auto with reloadty.
+ apply wt_code_cons; auto. constructor. reflexivity.
+ rewrite <- H2. eauto with reloadty.
assert (locs_valid (transf_function f) (loc_arguments sig)).
red; intros. generalize (loc_arguments_acceptable sig l H).
destruct l; simpl; auto. destruct s; simpl; intuition.
assert (locs_writable (loc_arguments sig)).
- red; intros. generalize (loc_arguments_acceptable sig l H7).
+ red; intros. generalize (loc_arguments_acceptable sig l H6).
destruct l; simpl; auto. destruct s; simpl; intuition.
assert (map Loc.type args = map Loc.type (loc_arguments sig)).
rewrite loc_arguments_type; auto.
assert (Loc.type res = mreg_type (loc_result sig)).
- rewrite H3. unfold loc_result.
+ rewrite H2. unfold loc_result. unfold proj_sig_res.
destruct (sig_res sig); auto. destruct t; auto.
- destruct ros; auto 10 with reloadty.
+ destruct ros.
+ destruct H3 as [A [B C]].
+ apply wt_parallel_move; eauto with reloadty.
+ apply wt_add_reload; eauto with reloadty.
+ apply wt_code_cons; eauto with reloadty.
+ constructor. rewrite <- A. auto with reloadty.
+ auto with reloadty.
assert (locs_valid (transf_function f) (loc_arguments sig)).
red; intros. generalize (loc_arguments_acceptable sig l H).
destruct l; simpl; auto. destruct s; simpl; intuition.
assert (locs_writable (loc_arguments sig)).
- red; intros. generalize (loc_arguments_acceptable sig l H7).
+ red; intros. generalize (loc_arguments_acceptable sig l H6).
destruct l; simpl; auto. destruct s; simpl; intuition.
assert (map Loc.type args = map Loc.type (loc_arguments sig)).
rewrite loc_arguments_type; auto.
- destruct ros; auto 10 with reloadty.
+ destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty.
+ auto 10 with reloadty.
assert (map mreg_type (regs_for args) = map Loc.type args).
eauto with reloadty.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 784823b0df14cc885ea4f1697563862a1df36a06..b7794883dc7507f09c56bcc3e62c85acb8834624 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1043,7 +1043,7 @@ Proof.
simpl. congruence.
exists (Vint i :: Vptr b0 i0 :: nil).
split. eauto with evalexpr. simpl.
- rewrite Int.add_commut. congruence.
+ congruence.
exists (Vptr b0 i :: Vint i0 :: nil).
split. eauto with evalexpr. simpl. congruence.
exists (v :: nil). split. eauto with evalexpr.
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index 030dcc672697fb722235728512d155fcf000371c..f4f2940221fcbcd3d731eaed019422dc459a5c50 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -189,8 +189,8 @@ let print_instruction oc labels = function
let lbl1 = new_label() in
let lbl2 = new_label() in
let lbl3 = new_label() in
- fprintf oc " addis r2, 0, ha16(L%d)\n" lbl1;
- fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl1;
+ fprintf oc " addis r12, 0, ha16(L%d)\n" lbl1;
+ fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl1;
fprintf oc " fcmpu cr7, %a, f13\n" freg r2;
fprintf oc " cror 30, 29, 30\n";
fprintf oc " beq cr7, L%d\n" lbl2;
@@ -225,12 +225,12 @@ let print_instruction oc labels = function
fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3
| Pictf(r1, r2) ->
let lbl = new_label() in
- fprintf oc " addis r2, 0, 0x4330\n";
- fprintf oc " stw r2, -8(r1)\n";
- fprintf oc " addis r2, %a, 0x8000\n" ireg r2;
- fprintf oc " stw r2, -4(r1)\n";
- fprintf oc " addis r2, 0, ha16(L%d)\n" lbl;
- fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl;
+ fprintf oc " addis r12, 0, 0x4330\n";
+ fprintf oc " stw r12, -8(r1)\n";
+ fprintf oc " addis r12, %a, 0x8000\n" ireg r2;
+ fprintf oc " stw r12, -4(r1)\n";
+ fprintf oc " addis r12, 0, ha16(L%d)\n" lbl;
+ fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl;
fprintf oc " lfd %a, -8(r1)\n" freg r1;
fprintf oc " fsub %a, %a, f13\n" freg r1 freg r1;
fprintf oc " .const_data\n";
@@ -238,11 +238,11 @@ let print_instruction oc labels = function
fprintf oc " .text\n"
| Piuctf(r1, r2) ->
let lbl = new_label() in
- fprintf oc " addis r2, 0, 0x4330\n";
- fprintf oc " stw r2, -8(r1)\n";
+ fprintf oc " addis r12, 0, 0x4330\n";
+ fprintf oc " stw r12, -8(r1)\n";
fprintf oc " stw %a, -4(r1)\n" ireg r2;
- fprintf oc " addis r2, 0, ha16(L%d)\n" lbl;
- fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl;
+ fprintf oc " addis r12, 0, ha16(L%d)\n" lbl;
+ fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl;
fprintf oc " lfd %a, -8(r1)\n" freg r1;
fprintf oc " fsub %a, %a, f13\n" freg r1 freg r1;
fprintf oc " .const_data\n";
@@ -258,8 +258,8 @@ let print_instruction oc labels = function
fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3
| Plfi(r1, c) ->
let lbl = new_label() in
- fprintf oc " addis r2, 0, ha16(L%d)\n" lbl;
- fprintf oc " lfd %a, lo16(L%d)(r2)\n" freg r1 lbl;
+ fprintf oc " addis r12, 0, ha16(L%d)\n" lbl;
+ fprintf oc " lfd %a, lo16(L%d)(r12)\n" freg r1 lbl;
fprintf oc " .const_data\n";
let n = Int64.bits_of_float c in
let nlo = Int64.to_int32 n
diff --git a/extraction/.depend b/extraction/.depend
index ac888a527fdb1f0adce1e199e16fc8b4f0469434..4730714c3033c905883c56a2d1e889312fdfad58 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -46,10 +46,6 @@
Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi
../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \
Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx
-../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
- ../caml/Camlcoq.cmo CList.cmi AST.cmi
-../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
- ../caml/Camlcoq.cmx CList.cmx AST.cmx
../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
CList.cmi AST.cmi
../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \