From 0b78a7b471eecd1ab983bbc48dfe8b39a0985d47 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 5 Nov 2014 15:32:52 +0100
Subject: Update PowerPC port.

---
 powerpc/Op.v | 56 +++++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 39 insertions(+), 17 deletions(-)

(limited to 'powerpc/Op.v')

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.
-- 
cgit