Merge branch 'master' into dwarf

3 files changed, 51 insertions, 88 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 9adf44dc..c7439c3d 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -49,6 +49,14 @@ Proof.
   exact TRANSF. 
 Qed.
 
+Lemma public_preserved:
+  forall id, Genv.public_symbol tge id = Genv.public_symbol ge id.
+Proof.
+  intros. unfold ge, tge. 
+  apply Genv.public_symbol_transf_partial with transf_fundef.
+  exact TRANSF. 
+Qed.
+
 Lemma varinfo_preserved:
   forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
 Proof.
@@ -755,7 +763,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   eapply exec_step_builtin. eauto. eauto.
   eapply find_instr_tail; eauto.
   eapply external_call_symbols_preserved'; eauto.
-  exact symbols_preserved. exact varinfo_preserved.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eauto.
   econstructor; eauto.
   Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto.
@@ -777,7 +785,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   eapply exec_step_annot. eauto. eauto.
   eapply find_instr_tail; eauto. eauto.
   eapply external_call_symbols_preserved'; eauto.
-  exact symbols_preserved. exact varinfo_preserved.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eapply match_states_intro with (ep := false); eauto with coqlib.
   unfold nextinstr. rewrite Pregmap.gss. 
   rewrite <- H1; simpl. econstructor; eauto.
@@ -960,7 +968,7 @@ Local Transparent destroyed_by_jumptable.
   left; econstructor; split.
   apply plus_one. eapply exec_step_external; eauto. 
   eapply external_call_symbols_preserved'; eauto. 
-  exact symbols_preserved. exact varinfo_preserved.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto.
   unfold loc_external_result.
   apply agree_set_other; auto. apply agree_set_mregs; auto.
@@ -1005,7 +1013,7 @@ Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
-  eexact symbols_preserved.
+  eexact public_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact step_simulation.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index dbec2755..3d5b1fc5 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -581,6 +581,22 @@ Proof.
   destruct c; simpl; auto; discriminate. 
 Qed.
 
+(** Global variables mentioned in an operation or addressing mode *)
+
+Definition globals_operation (op: operation) : list ident :=
+  match op with
+  | Oaddrsymbol s ofs => s :: nil
+  | Oaddsymbol s ofs => s :: nil
+  | _ => nil
+  end.
+
+Definition globals_addressing (addr: addressing) : list ident :=
+  match addr with
+  | Aglobal s n => s :: nil
+  | Abased s n => s :: nil
+  | _ => nil
+  end.
+
 (** * Invariance and compatibility properties. *)
 
 (** [eval_operation] and [eval_addressing] depend on a global environment
@@ -622,14 +638,11 @@ End GENV_TRANSF.
 
 Section EVAL_COMPAT.
 
-Variable F V: Type.
-Variable genv: Genv.t F V.
+Variable F1 F2 V1 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
 Variable f: meminj.
 
-Hypothesis symbol_address_inj: 
-  forall id ofs,
-  val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-
 Variable m1: mem.
 Variable m2: mem.
 
@@ -704,18 +717,22 @@ Ltac TrivialExists :=
 
 Lemma eval_operation_inj:
   forall op sp1 vl1 sp2 vl2 v1,
+  (forall id ofs,
+      In id (globals_operation op) ->
+      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
   val_inject f sp1 sp2 ->
   val_list_inject f vl1 vl2 ->
-  eval_operation genv sp1 op vl1 m1 = Some v1 ->
-  exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
+  eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
+  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  inv H; simpl; econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  apply GL; simpl; auto.
+  apply Values.val_add_inject; auto. 
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply GL; simpl; auto.
   inv H4; inv H2; simpl; auto. econstructor; eauto. 
     rewrite Int.sub_add_l. auto.
     destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. 
@@ -777,13 +794,18 @@ Qed.
 
 Lemma eval_addressing_inj:
   forall addr sp1 vl1 sp2 vl2 v1,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
   val_inject f sp1 sp2 ->
   val_list_inject f vl1 vl2 ->
-  eval_addressing genv sp1 addr vl1 = Some v1 ->
-  exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
+  eval_addressing ge1 sp1 addr vl1 = Some v1 ->
+  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists;
+  intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists;
     auto using Values.val_add_inject.
+  apply H; simpl; auto.
+  apply Values.val_add_inject; auto. apply H; simpl; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -864,11 +886,11 @@ Proof.
           eval_operation genv sp op vl2 m2 = Some v2
           /\ val_inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
-  intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
   apply weak_valid_pointer_extends; auto.
   apply weak_valid_pointer_no_overflow_extends; auto.
   apply valid_different_pointers_extends; auto.
+  intros. rewrite <- val_inject_lessdef; auto.
   rewrite <- val_inject_lessdef; auto.
   eauto. auto. 
   destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
@@ -939,7 +961,7 @@ Proof.
   intros. 
   rewrite eval_shift_stack_addressing. simpl.
   eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto.
-  exact symbol_address_inject.
+  intros. apply symbol_address_inject.
 Qed.
 
 Lemma eval_operation_inject:
@@ -954,11 +976,11 @@ Proof.
   intros. 
   rewrite eval_shift_stack_operation. simpl.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
-  exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
+  intros. apply symbol_address_inject.
 Qed.
 
 End EVAL_INJECT.
diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
deleted file mode 100644
index 2d3efe39..00000000
--- a/powerpc/Unusedglob1.ml
+++ /dev/null
@@ -1,67 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Identifiers referenced from a PowerPC Asm instruction *)
-
-open Datatypes
-open AST
-open Asm
-
-let referenced_constant = function
-  | Cint n -> []
-  | Csymbol_low(s, ofs) -> [s]
-  | Csymbol_high(s, ofs) -> [s]
-  | Csymbol_sda(s, ofs) -> [s]
-  | Csymbol_rel_low(s, ofs) -> [s]
-  | Csymbol_rel_high(s, ofs) -> [s]
-
-let referenced_builtin ef =
-  match ef with
-  | EF_vload_global(chunk, id, ofs) -> [id]
-  | EF_vstore_global(chunk, id, ofs) -> [id]
-  | _ -> []
-
-let referenced_instr = function
-  | Pbl(s, _) -> [s]
-  | Pbs(s, _) -> [s]
-  | Paddi(_, _, c)
-  | Paddic(_, _, c)
-  | Paddis(_, _, c)
-  | Pandi_(_, _, c)
-  | Pandis_(_, _, c)
-  | Pcmplwi(_, c)
-  | Pcmpwi(_, c)
-  | Plbz(_, c, _)
-  | Plfd(_, c, _)
-  | Plfd_a(_, c, _)
-  | Plfs(_, c, _)
-  | Plha(_, c, _)
-  | Plhz(_, c, _)
-  | Plwz(_, c, _)
-  | Plwz_a(_, c, _)
-  | Pmulli(_, _, c)
-  | Pori(_, _, c)
-  | Poris(_, _, c)
-  | Pstb(_, c, _)
-  | Pstfd(_, c, _)
-  | Pstfd_a(_, c, _)
-  | Pstfs(_, c, _)
-  | Psth(_, c, _) 
-  | Pstw(_, c, _) 
-  | Pstw_a(_, c, _) 
-  | Psubfic(_, _, c)
-  | Pxori(_, _, c)
-  | Pxoris(_, _, c) -> referenced_constant c
-  | Pbuiltin(ef, _, _) -> referenced_builtin ef
-  | _ -> []
-
-let code_of_function f = f.fn_code