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 --- lib/Integers.v | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index 9f58de3..1e58c2d 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -782,6 +782,30 @@ Proof. auto with ints. omega. Qed. +Theorem unsigned_add_carry: + forall x y, + unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) * modulus. +Proof. + intros. + unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r. simpl. + generalize (unsigned_range x) (unsigned_range y). intros. + destruct (zlt (unsigned x + unsigned y) modulus). + rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. + rewrite unsigned_one. apply Zmod_unique with 1. omega. omega. +Qed. + +Corollary unsigned_add_either: + forall x y, + unsigned (add x y) = unsigned x + unsigned y + \/ unsigned (add x y) = unsigned x + unsigned y - modulus. +Proof. + intros. rewrite unsigned_add_carry. unfold add_carry. + rewrite unsigned_zero. rewrite Zplus_0_r. + destruct (zlt (unsigned x + unsigned y) modulus). + rewrite unsigned_zero. left; omega. + rewrite unsigned_one. right; omega. +Qed. + (** ** Properties of negation *) Theorem neg_repr: forall z, neg (repr z) = repr (-z). @@ -3023,6 +3047,32 @@ Proof. generalize (unsigned_range x). omega. omega. Qed. +(** Non-overlapping test *) + +Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool := + let x1 := unsigned ofs1 in let x2 := unsigned ofs2 in + zlt (x1 + sz1) modulus && zlt (x2 + sz2) modulus + && (zle (x1 + sz1) x2 || zle (x2 + sz2) x1). + +Lemma no_overlap_sound: + forall ofs1 sz1 ofs2 sz2 base, + sz1 > 0 -> sz2 > 0 -> no_overlap ofs1 sz1 ofs2 sz2 = true -> + unsigned (add base ofs1) + sz1 <= unsigned (add base ofs2) + \/ unsigned (add base ofs2) + sz2 <= unsigned (add base ofs1). +Proof. + intros. + destruct (andb_prop _ _ H1). clear H1. + destruct (andb_prop _ _ H2). clear H2. + exploit proj_sumbool_true. eexact H1. intro A; clear H1. + exploit proj_sumbool_true. eexact H4. intro B; clear H4. + assert (unsigned ofs1 + sz1 <= unsigned ofs2 \/ unsigned ofs2 + sz2 <= unsigned ofs1). + destruct (orb_prop _ _ H3). left. eapply proj_sumbool_true; eauto. right. eapply proj_sumbool_true; eauto. + clear H3. + generalize (unsigned_range ofs1) (unsigned_range ofs2). intros P Q. + generalize (unsigned_add_either base ofs1) (unsigned_add_either base ofs2). + intros [C|C] [D|D]; omega. +Qed. + End Make. (** * Specialization to integers of size 8, 32, and 64 bits *) -- cgit v1.2.3