Update the ARM port.

1 files changed, 26 insertions, 46 deletions

diff --git a/arm/Op.v b/arm/Op.v
index e7971f0b..bda99e3c 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -720,36 +720,15 @@ Proof.
   intros. destruct c; simpl; auto; congruence.
 Qed.
 
-(** Checking whether two addressings, applied to the same arguments, produce
-  separated memory addresses.  Used in [CSE]. *)
-
-Definition addressing_separated (chunk1: memory_chunk) (addr1: addressing)
-                               (chunk2: memory_chunk) (addr2: addressing) : bool :=
-  match addr1, addr2 with
-  | Aindexed ofs1, Aindexed ofs2 => 
-      Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
-  | Ainstack ofs1, Ainstack ofs2 =>
-      Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
-  | _, _ => false
+(** Global variables mentioned in an operation or addressing mode *)
+
+Definition globals_operation (op: operation) : list ident :=
+  match op with
+  | Oaddrsymbol s ofs => s :: nil
+  | _ => nil
   end.
 
-Lemma addressing_separated_sound:
-  forall (F V: Type) (ge: Genv.t F V) sp chunk1 addr1 chunk2 addr2 vl b1 n1 b2 n2,
-  addressing_separated chunk1 addr1 chunk2 addr2 = true ->
-  eval_addressing ge sp addr1 vl = Some(Vptr b1 n1) ->
-  eval_addressing ge sp addr2 vl = Some(Vptr b2 n2) ->
-  b1 <> b2 \/ Int.unsigned n1 + size_chunk chunk1 <= Int.unsigned n2 \/ Int.unsigned n2 + size_chunk chunk2 <= Int.unsigned n1.
-Proof.
-  unfold addressing_separated; intros.
-  generalize (size_chunk_pos chunk1) (size_chunk_pos chunk2); intros SZ1 SZ2.
-  destruct addr1; destruct addr2; try discriminate; simpl in *; FuncInv.
-(* Aindexed *)
-  destruct v; simpl in *; inv H1; inv H2.
-  right. apply Int.no_overlap_sound; auto. 
-(* Ainstack *)
-  destruct sp; simpl in *; inv H1; inv H2.
-  right. apply Int.no_overlap_sound; auto. 
-Qed.
+Definition globals_addressing (addr: addressing) : list ident := nil.
 
 (** * Invariance and compatibility properties. *)
 
@@ -791,14 +770,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.
 
@@ -885,12 +861,16 @@ 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.
+  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.
@@ -976,15 +956,15 @@ 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.
-  assert (UNUSED: forall id ofs,
-            val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs)).
-  exact symbol_address_inj.
-  intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
@@ -1069,11 +1049,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.
   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. 
@@ -1144,7 +1124,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:
@@ -1159,11 +1139,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.