More aggressive common subexpression elimination (CSE) of memory loads.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 55 insertions, 0 deletions

diff --git a/ia32/Op.v b/ia32/Op.v
index 6389567..896badf 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -606,6 +606,61 @@ Proof.
   destruct c; simpl; try congruence. reflexivity. 
 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)
+  | Aglobal s1 ofs1, Aglobal s2 ofs2 => 
+      if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true
+  | Abased s1 ofs1, Abased s2 ofs2 => 
+      if ident_eq s1 s2 then Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2) else true
+  | Ainstack ofs1, Ainstack ofs2 =>
+      Int.no_overlap ofs1 (size_chunk chunk1) ofs2 (size_chunk chunk2)
+  | _, _ => false
+  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. 
+(* Aglobal *)
+  unfold symbol_address in *. 
+  destruct (Genv.find_symbol ge i1) as []_eqn; inv H2.
+  destruct (Genv.find_symbol ge i) as []_eqn; inv H1.
+  destruct (ident_eq i i1). subst.
+  replace (Int.unsigned n1) with (Int.unsigned (Int.add Int.zero n1)).
+  replace (Int.unsigned n2) with (Int.unsigned (Int.add Int.zero n2)).
+  right. apply Int.no_overlap_sound; auto. 
+  rewrite Int.add_commut; rewrite Int.add_zero; auto.
+  rewrite Int.add_commut; rewrite Int.add_zero; auto.
+  left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
+(* Abased *)
+  unfold symbol_address in *. 
+  destruct (Genv.find_symbol ge i1) as []_eqn; simpl in *; try discriminate.
+  destruct v; inv H2.
+  destruct (Genv.find_symbol ge i) as []_eqn; inv H1.
+  destruct (ident_eq i i1). subst.
+  rewrite (Int.add_commut i0 i3). rewrite (Int.add_commut i2 i3).
+  right. apply Int.no_overlap_sound; auto. 
+  left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
+(* Ainstack *)
+  destruct sp; simpl in *; inv H1; inv H2.
+  right. apply Int.no_overlap_sound; auto. 
+Qed.
+
 (** * Invariance and compatibility properties. *)
 
 (** [eval_operation] and [eval_addressing] depend on a global environment