Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

1 files changed, 48 insertions, 48 deletions

diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index c79ae4fd..db03d0b3 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -315,11 +315,11 @@ Corollary used_globals_valid:
   valid_used_set p u.
 Proof.
   intros. constructor.
-- intros. eapply used_globals_sound; eauto. 
+- intros. eapply used_globals_sound; eauto.
 - eapply used_globals_incl; eauto. apply seen_main_initial_workset.
 - intros. eapply used_globals_incl; eauto. apply seen_public_initial_workset; auto.
 - intros. apply ISF.for_all_iff in H0.
-+ red in H0. apply H0 in H1. unfold global_defined in H1. 
++ red in H0. apply H0 in H1. unfold global_defined in H1.
   destruct pm!id as [g|] eqn:E.
 * left. change id with (fst (id,g)). apply in_map. apply in_prog_defmap; auto.
 * InvBooleans; auto.
@@ -394,7 +394,7 @@ Lemma filter_globdefs_map:
 Proof.
   intros. unfold PTree_Properties.of_list. fold prog_map. unfold PTree.elt. fold add_def.
   destruct (IS.mem id u) eqn:MEM.
-- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity. 
+- erewrite filter_globdefs_map_2. rewrite List.rev_involutive. reflexivity.
   auto. auto.
 - apply filter_globdefs_map_1. auto. apply PTree.gempty.
 Qed.
@@ -419,7 +419,7 @@ Proof.
 - constructor.
 - destruct (IS.mem id1 u) eqn:MEM; auto.
   rewrite filter_globdefs_nil, map_app. simpl.
-  apply list_norepet_append; auto. 
+  apply list_norepet_append; auto.
   constructor. simpl; tauto. constructor.
   red; simpl; intros. destruct H0; try tauto. subst y.
   apply filter_globdefs_domain in H. rewrite ISF.remove_iff in H. intuition.
@@ -433,11 +433,11 @@ Proof.
   unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *.
   destruct (used_globals p pm) as [u|] eqn:U; try discriminate.
   destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR.
-  exists u; split. 
+  exists u; split.
   apply used_globals_valid; auto.
   constructor; simpl; auto.
   intros. unfold prog_defmap; simpl. apply filter_globdefs_map.
-  apply filter_globdefs_unique_names. 
+  apply filter_globdefs_unique_names.
 Qed.
 
 (** * Semantic preservation *)
@@ -480,7 +480,7 @@ Lemma transform_find_symbol_1:
   forall id b,
   Genv.find_symbol ge id = Some b -> kept id -> exists b', Genv.find_symbol tge id = Some b'.
 Proof.
-  intros. 
+  intros.
   assert (A: exists g, (prog_defmap p)!id = Some g).
   { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. }
   destruct A as (g & P).
@@ -493,13 +493,13 @@ Lemma transform_find_symbol_2:
   forall id b,
   Genv.find_symbol tge id = Some b -> kept id /\ exists b', Genv.find_symbol ge id = Some b'.
 Proof.
-  intros. 
+  intros.
   assert (A: exists g, (prog_defmap tp)!id = Some g).
   { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. }
   destruct A as (g & P).
-  erewrite match_prog_def in P by eauto. 
+  erewrite match_prog_def in P by eauto.
   destruct (IS.mem id used) eqn:U; try discriminate.
-  split. apply IS.mem_2; auto. 
+  split. apply IS.mem_2; auto.
   apply Genv.find_symbol_exists with g.
   apply in_prog_defmap. auto.
 Qed.
@@ -564,7 +564,7 @@ Proof.
   auto.
 - exploit transform_find_symbol_1; eauto. intros (b' & F). exists b'; split; auto.
   eapply init_meminj_eq; eauto.
-- exploit transform_find_symbol_2; eauto. intros (K & b & F). 
+- exploit transform_find_symbol_2; eauto. intros (K & b & F).
   exists b; split; auto. eapply init_meminj_eq; eauto.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C).
   assert (kept id) by (eapply transform_find_symbol_2; eauto).
@@ -573,7 +573,7 @@ Proof.
   assert ((prog_defmap tp)!id = Some gd).
   { erewrite match_prog_def by eauto. rewrite IS.mem_1 by auto. auto. }
   rewrite Genv.find_def_symbol in H3. destruct H3 as (b1 & P & Q).
-  fold tge in P. replace b' with b1 by congruence. split; auto. split; auto. 
+  fold tge in P. replace b' with b1 by congruence. split; auto. split; auto.
   intros. eapply kept_closed; eauto.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C).
   assert ((prog_defmap tp)!id = Some gd).
@@ -616,7 +616,7 @@ Proof.
     rewrite <- Genv.find_var_info_iff in A. rewrite A; auto.
     destruct (Genv.find_var_info tge b2) as [gv|] eqn:V2; auto.
     rewrite Genv.find_var_info_iff in V2.
-    exploit defs_rev_inject; eauto. intros (A & B). 
+    exploit defs_rev_inject; eauto. intros (A & B).
     rewrite <- Genv.find_var_info_iff in A. congruence.
 Qed.
 
@@ -805,15 +805,15 @@ Proof.
 - exploit Genv.find_funct_inv; eauto. intros (b & R). rewrite R in H0.
   rewrite Genv.find_funct_find_funct_ptr in H0.
   specialize (H1 r). rewrite R in H1. inv H1.
-  rewrite Genv.find_funct_ptr_iff in H0.  
+  rewrite Genv.find_funct_ptr_iff in H0.
   exploit defs_inject; eauto. intros (A & B & C).
-  rewrite <- Genv.find_funct_ptr_iff in A. 
+  rewrite <- Genv.find_funct_ptr_iff in A.
   rewrite B; auto.
 - destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
   exploit symbols_inject_2; eauto. intros (tb & P & Q). rewrite P.
-  rewrite Genv.find_funct_ptr_iff in H0.  
+  rewrite Genv.find_funct_ptr_iff in H0.
   exploit defs_inject; eauto. intros (A & B & C).
-  rewrite <- Genv.find_funct_ptr_iff in A. 
+  rewrite <- Genv.find_funct_ptr_iff in A.
   auto.
 Qed.
 
@@ -1057,7 +1057,7 @@ Proof.
   { induction l as [ | [id1 g1] l]; simpl; intros.
   - auto.
   - apply IHl. unfold Genv.add_global, P; simpl. intros LT. apply Plt_succ_inv in LT. destruct LT.
-  + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto. 
+  + rewrite PTree.gso. apply H; auto. apply Plt_ne; auto.
   + rewrite H0. rewrite PTree.gss. exists g1; auto. }
   apply H. red; simpl; intros. exfalso; xomega.
 Qed.
@@ -1074,14 +1074,14 @@ Lemma init_meminj_invert_strong:
   /\ Genv.find_def tge b' = Some gd
   /\ (forall i, ref_def gd i -> kept i).
 Proof.
-  intros. exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+  intros. exploit init_meminj_invert; eauto. intros (A & id & B & C).
   assert (exists gd, (prog_defmap p)!id = Some gd).
   { apply prog_defmap_dom. eapply Genv.find_symbol_inversion; eauto. }
   destruct H0 as [gd DM]. rewrite Genv.find_def_symbol in DM.
   destruct DM as (b'' & P & Q). fold ge in P. rewrite P in B; inv B.
   fold ge in Q. exploit defs_inject. apply init_meminj_preserves_globals.
-  eauto. eauto. intros (X & _ & Y). 
-  split. auto. exists id, gd; auto. 
+  eauto. eauto. intros (X & _ & Y).
+  split. auto. exists id, gd; auto.
 Qed.
 
 Section INIT_MEM.
@@ -1098,11 +1098,11 @@ Proof.
   induction il as [ | i1 il]; simpl; intros.
 - constructor.
 - apply list_forall2_app.
-+ destruct i1; simpl; try (apply inj_bytes_inject). 
++ destruct i1; simpl; try (apply inj_bytes_inject).
   induction (Z.to_nat z); simpl; constructor. constructor. auto.
   destruct (Genv.find_symbol ge i) as [b|] eqn:FS.
   assert (kept i). { apply H. red. exists i0; auto with coqlib. }
-  exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto. 
+  exploit symbols_inject_2. apply init_meminj_preserves_globals. eauto. eauto.
   intros (b' & A & B). rewrite A. apply inj_value_inject.
   econstructor; eauto. symmetry; apply Ptrofs.add_zero.
   destruct (Genv.find_symbol tge i) as [b'|] eqn:FS'.
@@ -1123,7 +1123,7 @@ Proof.
 - inv H. rewrite inj_S in H1. destruct (zeq i p0).
 + congruence.
 + apply IHn with (p0 + 1); auto. omega. omega.
-Qed. 
+Qed.
 
 Lemma init_mem_inj_1:
   Mem.mem_inj init_meminj m tm.
@@ -1138,9 +1138,9 @@ Proof.
   apply Mem.perm_cur. auto.
 + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1).
   apply Q1 in H0. destruct H0. subst.
-  apply Mem.perm_cur. eapply Mem.perm_implies; eauto. 
+  apply Mem.perm_cur. eapply Mem.perm_implies; eauto.
   apply P2. omega.
-- exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+- exploit init_meminj_invert; eauto. intros (A & id & B & C).
   subst delta. apply Zdivide_0.
 - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F).
   exploit (Genv.init_mem_characterization_gen p); eauto.
@@ -1157,9 +1157,9 @@ Local Transparent Mem.loadbytes.
   generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2.
   rewrite Zplus_0_r.
   apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))).
-  rewrite H3, H4. apply bytes_of_init_inject. auto. 
-  omega. 
-  rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega. 
+  rewrite H3, H4. apply bytes_of_init_inject. auto.
+  omega.
+  rewrite nat_of_Z_eq by (apply init_data_list_size_pos). omega.
 Qed.
 
 Lemma init_mem_inj_2:
@@ -1168,9 +1168,9 @@ Proof.
   constructor; intros.
 - apply init_mem_inj_1.
 - destruct (init_meminj b) as [[b' delta]|] eqn:INJ; auto.
-  elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+  elim H. exploit init_meminj_invert; eauto. intros (A & id & B & C).
   eapply Genv.find_symbol_not_fresh; eauto.
-- exploit init_meminj_invert; eauto. intros (A & id & B & C). 
+- exploit init_meminj_invert; eauto. intros (A & id & B & C).
   eapply Genv.find_symbol_not_fresh; eauto.
 - red; intros.
   exploit init_meminj_invert. eexact H0. intros (A1 & id1 & B1 & C1).
@@ -1187,7 +1187,7 @@ Proof.
   left; apply Mem.perm_cur; auto.
 + intros (P2 & Q2 & R2 & S2) (P1 & Q1 & R1 & S1).
   apply Q2 in H0. destruct H0. subst.
-  left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto. 
+  left. apply Mem.perm_cur. eapply Mem.perm_implies; eauto.
   apply P1. omega.
 Qed.
 
@@ -1198,7 +1198,7 @@ Lemma init_mem_exists:
   exists tm, Genv.init_mem tp = Some tm.
 Proof.
   intros. apply Genv.init_mem_exists.
-  intros. 
+  intros.
   assert (P: (prog_defmap tp)!id = Some (Gvar v)).
   { eapply prog_defmap_norepet; eauto. eapply match_prog_unique; eauto. }
   rewrite (match_prog_def _ _ _ TRANSF) in P. destruct (IS.mem id used) eqn:U; try discriminate.
@@ -1206,7 +1206,7 @@ Proof.
   split. auto.
   intros. exploit FV; eauto. intros (b & FS).
   apply transform_find_symbol_1 with b; auto.
-  apply kept_closed with id (Gvar v). 
+  apply kept_closed with id (Gvar v).
   apply IS.mem_2; auto. auto. red. red. exists o; auto.
 Qed.
 
@@ -1218,9 +1218,9 @@ Proof.
   intros.
   exploit init_mem_exists; eauto. intros [tm INIT].
   exists init_meminj, tm.
-  split. auto. 
-  split. eapply init_mem_inj_2; eauto. 
-  apply init_meminj_preserves_globals. 
+  split. auto.
+  split. eapply init_mem_inj_2; eauto.
+  apply init_meminj_preserves_globals.
 Qed.
 
 Lemma transf_initial_states:
@@ -1228,7 +1228,7 @@ Lemma transf_initial_states:
 Proof.
   intros. inv H. exploit init_mem_inject; eauto. intros (j & tm & A & B & C).
   exploit symbols_inject_2. eauto. eapply kept_main. eexact H1. intros (tb & P & Q).
-  rewrite Genv.find_funct_ptr_iff in H2. 
+  rewrite Genv.find_funct_ptr_iff in H2.
   exploit defs_inject. eauto. eexact Q. exact H2.
   intros (R & S & T).
   rewrite <- Genv.find_funct_ptr_iff in R.
@@ -1286,15 +1286,15 @@ Local Transparent Linker_def Linker_fundef Linker_varinit Linker_vardef Linker_u
   destruct (link_varinit init1 init2) as [init|] eqn:LI...
   destruct (eqb ro1 ro2) eqn:RO...
   destruct (eqb vo1 vo2) eqn:VO...
-  simpl. 
+  simpl.
   destruct info1, info2.
   assert (EITHER: init = init1 \/ init = init2).
-  { revert LI. unfold link_varinit. 
+  { revert LI. unfold link_varinit.
     destruct (classify_init init1), (classify_init init2); intro EQ; inv EQ; auto.
     destruct (zeq sz (Z.max sz0 0 + 0)); inv H0; auto.
     destruct (zeq sz (init_data_list_size il)); inv H0; auto.
     destruct (zeq sz (init_data_list_size il)); inv H0; auto. }
-  apply eqb_prop in RO. apply eqb_prop in VO. 
+  apply eqb_prop in RO. apply eqb_prop in VO.
   intro EQ; inv EQ. destruct EITHER; subst init; auto.
 Qed.
 
@@ -1339,7 +1339,7 @@ Proof.
 + (* common definition *)
   exploit Y; eauto. intros (PUB1 & PUB2 & _).
   exploit link_def_either; eauto. intros [EQ|EQ]; subst gd.
-* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto. 
+* left. eapply used_closed. eexact V1. eapply used_public. eexact V1. eauto. eauto. auto.
 * right. eapply used_closed. eexact V2. eapply used_public. eexact V2. eauto. eauto. auto.
 + (* left definition *)
   inv H0. destruct (ISP.In_dec id used1).
@@ -1358,7 +1358,7 @@ Proof.
 + (* no definition *)
   auto.
 - simpl. rewrite ISF.union_iff; left; eapply used_main; eauto.
-- simpl. intros id. rewrite in_app_iff, ISF.union_iff. 
+- simpl. intros id. rewrite in_app_iff, ISF.union_iff.
   intros [A|A]; [left|right]; eapply used_public; eauto.
 - intros. rewrite ISF.union_iff in H.
   destruct (ident_eq id (prog_main p1)).
@@ -1387,16 +1387,16 @@ Theorem link_match_program:
 Proof.
   intros. destruct H0 as (used1 & A1 & B1). destruct H1 as (used2 & A2 & B2).
   destruct (link_prog_inv _ _ _ H) as (U & V & W).
-  econstructor; split. 
+  econstructor; split.
 - apply link_prog_succeeds.
 + rewrite (match_prog_main _ _ _ B1), (match_prog_main _ _ _ B2). auto.
-+ intros. 
++ intros.
   rewrite (match_prog_def _ _ _ B1) in H0.
   rewrite (match_prog_def _ _ _ B2) in H1.
   destruct (IS.mem id used1) eqn:U1; try discriminate.
   destruct (IS.mem id used2) eqn:U2; try discriminate.
   edestruct V as (X & Y & gd & Z); eauto.
-  split. rewrite (match_prog_public _ _ _ B1); auto. 
+  split. rewrite (match_prog_public _ _ _ B1); auto.
   split. rewrite (match_prog_public _ _ _ B2); auto.
   congruence.
 - exists (IS.union used1 used2); split.
@@ -1411,7 +1411,7 @@ Proof.
   destruct (prog_defmap p1)!id as [gd1|] eqn:GD1;
   destruct (prog_defmap p2)!id as [gd2|] eqn:GD2.
 - (* both defined *)
-  exploit V; eauto. intros (PUB1 & PUB2 & _). 
+  exploit V; eauto. intros (PUB1 & PUB2 & _).
   assert (EQ1: IS.mem id used1 = true) by (apply IS.mem_1; eapply used_public; eauto).
   assert (EQ2: IS.mem id used2 = true) by (apply IS.mem_1; eapply used_public; eauto).
   rewrite EQ1, EQ2; auto.
@@ -1428,7 +1428,7 @@ Proof.
 - (* none defined *)
   destruct (IS.mem id used1), (IS.mem id used2); auto.
 }
-* intros. apply PTree.elements_keys_norepet. 
+* intros. apply PTree.elements_keys_norepet.
 Qed.
 
 Instance TransfSelectionLink : TransfLink match_prog := link_match_program.