Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10

5 files changed, 198 insertions, 4 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index eda3862f..19c641e3 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -25,8 +25,6 @@ Require Export List.
 Require Export Bool.
 Require Export Lia.
 
-Global Set Asymmetric Patterns.
-
 (** * Useful tactics *)
 
 Ltac inv H := inversion H; clear H; subst.
@@ -525,6 +523,60 @@ Proof.
   intros. unfold align. apply Z.divide_factor_r.
 Qed.
 
+Lemma align_lt: forall x y, y > 0 -> align x y < x + y.
+Proof.
+  intros. unfold align.
+  generalize (Z_div_mod_eq (x + y - 1) y H); intro.
+  generalize (Z_mod_lt (x + y - 1) y H); intro.
+  lia.
+Qed.
+
+Lemma align_same:
+  forall x y, y > 0 -> (y | x) -> align x y = x.
+Proof.
+  unfold align; intros. destruct H0 as [k E].
+  replace (x  + y - 1) with (x + (y - 1)) by lia.
+  rewrite E, Z.div_add_l, Z.div_small by lia.
+  lia.
+Qed.
+
+(** Floor: [floor n amount] returns the greatest multiple of [amount]
+    less than or equal to [n]. *)
+
+Definition floor (n: Z) (amount: Z) := (n / amount) * amount.
+
+Lemma floor_interval:
+  forall x y, y > 0 -> floor x y <= x < floor x y + y.
+Proof.
+  unfold floor; intros.
+  generalize (Z_div_mod_eq x y H) (Z_mod_lt x y H).
+  set (q := x / y). set (r := x mod y). intros. lia.
+Qed.
+
+Lemma floor_divides:
+  forall x y, y > 0 -> (y | floor x y).
+Proof.
+  unfold floor; intros. exists (x / y); auto.
+Qed.
+
+Lemma floor_same:
+  forall x y, y > 0 -> (y | x) -> floor x y = x.
+Proof.
+  unfold floor; intros. rewrite (Zdivide_Zdiv_eq y x) at 2; auto; lia.
+Qed.
+
+Lemma floor_align_interval:
+  forall x y, y > 0 ->
+  floor x y <= align x y <= floor x y + y.
+Proof.
+  unfold floor, align; intros.
+  replace (x / y * y + y) with ((x + 1 * y) / y * y).
+  assert (A: forall a b, a <= b -> a / y * y <= b / y * y).
+  { intros. apply Z.mul_le_mono_nonneg_r. lia. apply Z.div_le_mono; lia. }
+  split; apply A; lia.
+  rewrite Z.div_add by lia. lia.
+Qed.
+
 (** * Definitions and theorems on the data types [option], [sum] and [list] *)
 
 Set Implicit Arguments.
@@ -773,6 +825,32 @@ Proof.
   exists (a0 :: l1); exists l2; intuition. simpl; congruence.
 Qed.
 
+(** Properties of [List.app] (concatenation) *)
+
+Lemma list_append_injective_l:
+  forall (A: Type) (l1 l2 l1' l2': list A),
+  l1 ++ l2 = l1' ++ l2' -> List.length l1 = List.length l1' -> l1 = l1' /\ l2 = l2'.
+Proof.
+  intros until l2'. revert l1 l1'. induction l1 as [ | a l1]; destruct l1' as [ | a' l1']; simpl; intros.
+- auto.
+- discriminate.
+- discriminate.
+- destruct (IHl1 l1'). congruence. congruence. split; congruence.
+Qed.
+
+Lemma list_append_injective_r:
+  forall (A: Type) (l1 l2 l1' l2': list A),
+  l1 ++ l2 = l1' ++ l2' -> List.length l2 = List.length l2' -> l1 = l1' /\ l2 = l2'.
+Proof.
+  intros.
+  assert (X: rev l2 = rev l2' /\ rev l1 = rev l1').
+  { apply list_append_injective_l.
+    rewrite <- ! rev_app_distr. congruence.
+    rewrite ! rev_length; auto. }
+  rewrite <- (rev_involutive l1), <- (rev_involutive l1'), <- (rev_involutive l2), <- (rev_involutive l2').
+  intuition congruence.
+Qed.
+
 (** Folding a function over a list *)
 
 Section LIST_FOLD.
diff --git a/lib/Floats.v b/lib/Floats.v
index b10b3392..9ee5302d 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -26,6 +26,7 @@ Import ListNotations.
 
 Close Scope R_scope.
 Open Scope Z_scope.
+Set Asymmetric Patterns.
 
 Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *)
 
diff --git a/lib/Integers.v b/lib/Integers.v
index 2addc78b..b6c41d8d 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2851,7 +2851,7 @@ Qed.
 
 Corollary sign_ext_shr_shl:
   forall n x,
-  0 < n < zwordsize ->
+  0 < n <= zwordsize ->
   let y := repr (zwordsize - n) in
   sign_ext n x = shr (shl x y) y.
 Proof.
@@ -2886,7 +2886,7 @@ Qed.
 Lemma sign_ext_range:
   forall n x, 0 < n < zwordsize -> -two_p (n-1) <= signed (sign_ext n x) < two_p (n-1).
 Proof.
-  intros. rewrite sign_ext_shr_shl; auto.
+  intros. rewrite sign_ext_shr_shl by lia.
   set (X := shl x (repr (zwordsize - n))).
   assert (two_p (n - 1) > 0) by (apply two_p_gt_ZERO; lia).
   assert (unsigned (repr (zwordsize - n)) = zwordsize - n).
@@ -3474,6 +3474,118 @@ Proof.
   lia.
 Qed.
 
+(** ** Accessing bit fields *)
+
+Definition unsigned_bitfield_extract (pos width: Z) (n: int) : int :=
+  zero_ext width (shru n (repr pos)).
+
+Definition signed_bitfield_extract (pos width: Z) (n: int) : int :=
+  sign_ext width (shru n (repr pos)).
+
+Definition bitfield_insert (pos width: Z) (n p: int) : int :=
+  let mask := shl (repr (two_p width - 1)) (repr pos) in
+  or (shl (zero_ext width p) (repr pos))
+     (and n (not mask)).
+
+Lemma bits_unsigned_bitfield_extract:
+  forall pos width n i,
+  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
+  0 <= i < zwordsize ->
+  testbit (unsigned_bitfield_extract pos width n) i =
+  if zlt i width then testbit n (i + pos) else false.
+Proof.
+  intros. unfold unsigned_bitfield_extract. rewrite bits_zero_ext by lia.
+  destruct (zlt i width); auto.
+  rewrite bits_shru by auto. rewrite unsigned_repr, zlt_true. auto.
+  lia.
+  generalize wordsize_max_unsigned; lia.
+Qed.
+
+Lemma bits_signed_bitfield_extract:
+  forall pos width n i,
+  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
+  0 <= i < zwordsize ->
+  testbit (signed_bitfield_extract pos width n) i =
+  testbit n (if zlt i width then i + pos else width - 1 + pos).
+Proof.
+  intros. unfold signed_bitfield_extract. rewrite bits_sign_ext by lia.
+  rewrite bits_shru, unsigned_repr, zlt_true.
+  destruct (zlt i width); auto.
+  destruct (zlt i width); lia.
+  generalize wordsize_max_unsigned; lia.
+  destruct (zlt i width); lia.
+Qed.
+
+Lemma bits_bitfield_insert:
+  forall pos width n p i,
+  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
+  0 <= i < zwordsize ->
+  testbit (bitfield_insert pos width n p) i =
+  if zle pos i && zlt i (pos + width) then testbit p (i - pos) else testbit n i.
+Proof.
+  intros. unfold bitfield_insert.
+  assert (P: unsigned (repr pos) = pos).
+  { apply unsigned_repr. generalize wordsize_max_unsigned; lia. }
+  rewrite bits_or, bits_and, bits_not, ! bits_shl, ! P by auto.
+  destruct (zlt i pos).
+- unfold proj_sumbool; rewrite zle_false by lia. cbn. apply andb_true_r.
+- unfold proj_sumbool; rewrite zle_true by lia; cbn.
+  rewrite bits_zero_ext, testbit_repr, Ztestbit_two_p_m1 by lia.
+  destruct (zlt (i - pos) width); cbn.
++ rewrite zlt_true by lia. rewrite andb_false_r, orb_false_r. auto.
++ rewrite zlt_false by lia. apply andb_true_r.
+Qed.
+
+Lemma unsigned_bitfield_extract_by_shifts:
+  forall pos width n,
+  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
+  unsigned_bitfield_extract pos width n =
+  shru (shl n (repr (zwordsize - pos - width))) (repr (zwordsize - width)).
+Proof.
+  intros. apply same_bits_eq; intros.
+  rewrite bits_unsigned_bitfield_extract by lia.
+  rewrite bits_shru by auto.
+  rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia).
+  destruct (zlt i width).
+- rewrite bits_shl by lia.
+  rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia).
+  rewrite zlt_true by lia. rewrite zlt_false by lia. f_equal; lia.
+- rewrite zlt_false by lia. auto.
+Qed.
+
+Lemma signed_bitfield_extract_by_shifts:
+  forall pos width n,
+  0 <= pos -> 0 < width -> pos + width <= zwordsize ->
+  signed_bitfield_extract pos width n =
+  shr (shl n (repr (zwordsize - pos - width))) (repr (zwordsize - width)).
+Proof.
+  intros. apply same_bits_eq; intros.
+  rewrite bits_signed_bitfield_extract by lia.
+  rewrite bits_shr by auto.
+  rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia).
+  rewrite bits_shl.
+  rewrite unsigned_repr by (generalize wordsize_max_unsigned; lia).
+  symmetry. rewrite zlt_false. f_equal.
+  destruct (zlt i width); [rewrite zlt_true | rewrite zlt_false]; lia.
+  destruct zlt; lia.
+  destruct zlt; lia.
+Qed.
+
+Lemma bitfield_insert_alternative:
+  forall pos width n p,
+  0 <= width ->
+  bitfield_insert pos width n p =
+  let mask := shl (repr (two_p width - 1)) (repr pos) in
+  or (and (shl p (repr pos)) mask)
+     (and n (not mask)).
+Proof.
+  intros. unfold bitfield_insert. 
+  set (m1 := repr (two_p width - 1)).
+  set (m2 := shl m1 (repr pos)).
+  f_equal.
+  rewrite zero_ext_and by lia. fold m1. unfold m2. rewrite <- and_shl. auto.
+Qed.
+
 End Make.
 
 (** * Specialization to integers of size 8, 32, and 64 bits *)
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 82110bff..66bb3970 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -20,6 +20,8 @@ Require Import Axioms.
 Require Import Coqlib.
 Require Import Wfsimpl.
 
+Set Asymmetric Patterns.
+
 (** This modules defines several Coq encodings of a general "while" loop.
   The loop is presented in functional style as the iteration
   of a [step] function of type [A -> B + A]:
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index ee24a9a7..1c37a35b 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -21,6 +21,7 @@ Require Import Coqlib.
 
 Open Scope nat_scope.
 Set Implicit Arguments.
+Set Asymmetric Patterns.
 
 (* To avoid useless definitions of inductors in extracted code. *)
 Local Unset Elimination Schemes.