From 0e76ac320601a81a67c700759526d0f8b7a8ed7b Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 23 Feb 2012 14:00:06 +0000 Subject: 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 --- arm/Op.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) (limited to 'arm') diff --git a/arm/Op.v b/arm/Op.v index 905068f..99ba924 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -610,6 +610,37 @@ 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 + 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. + (** * Invariance and compatibility properties. *) (** [eval_operation] and [eval_addressing] depend on a global environment -- cgit v1.2.3