More accurate model of condition register flags for ARM and IA32.

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

2 files changed, 125 insertions, 8 deletions

diff --git a/lib/Floats.v b/lib/Floats.v
index 7ae1705..94c19d2 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -453,6 +453,12 @@ Proof.
   now apply cmp_le_lt_eq.
 Qed.
 
+Theorem cmp_lt_gt_false:
+  forall f1 f2, cmp Clt f1 f2 = true -> cmp Cgt f1 f2 = true -> False.
+Proof.
+  unfold cmp; intros; destruct (order_float f1 f2) as [ [] | ]; discriminate.
+Qed.
+
 (** Properties of conversions to/from in-memory representation.
   The double-precision conversions are bijective (one-to-one).
   The single-precision conversions lose precision exactly
diff --git a/lib/Integers.v b/lib/Integers.v
index 5eb4c82..49fa48f 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -257,11 +257,6 @@ Definition divu (x y: int) : int :=
 Definition modu (x y: int) : int :=
   repr ((unsigned x) mod (unsigned y)).
 
-Definition add_carry (x y cin: int): int :=
-  if zlt (unsigned x + unsigned y + unsigned cin) modulus
-  then zero
-  else one.
-
 (** Bitwise boolean operations. *)
 
 Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)).
@@ -291,10 +286,30 @@ Definition rolm (x a m: int): int := and (rol x a) m.
 Definition shrx (x y: int): int :=
   divs x (shl one y).
 
+(** Condition flags *)
+
+Definition negative (x: int): int :=
+  if lt x zero then one else zero.
+
+Definition add_carry (x y cin: int): int :=
+  if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one.
+
+Definition add_overflow (x y cin: int): int :=
+  let s := signed x + signed y + signed cin in
+  if zle min_signed s && zle s max_signed then zero else one.
+
+Definition sub_borrow (x y bin: int): int :=
+  if zlt (unsigned x - unsigned y - unsigned bin) 0 then one else zero.
+
+Definition sub_overflow (x y bin: int): int :=
+  let s := signed x - signed y - signed bin in
+  if zle min_signed s && zle s max_signed then zero else one.
+
 (** [shr_carry x y] is 1 if [x] is negative and at least one 1 bit is shifted away. *)
 
-Definition shr_carry (x y: int) :=
-  if lt x zero && negb (eq (and x (sub (shl one y) one)) zero) then one else zero.
+Definition shr_carry (x y: int) : int :=
+  if lt x zero && negb (eq (and x (sub (shl one y) one)) zero)
+  then one else zero.
 
 (** Zero and sign extensions *)
 
@@ -882,7 +897,7 @@ Proof.
   unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r.
   rewrite unsigned_repr_eq.
   generalize (unsigned_range x) (unsigned_range y). intros. 
-  destruct (zlt (unsigned x + unsigned y) modulus). 
+  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. 
@@ -983,6 +998,21 @@ Proof.
   apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned.
 Qed.
 
+Theorem unsigned_sub_borrow:
+  forall x y,
+  unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus.
+Proof.
+  intros.
+  unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r.
+  rewrite unsigned_repr_eq.
+  generalize (unsigned_range x) (unsigned_range y). intros. 
+  destruct (zlt (unsigned x - unsigned y) 0).
+  rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega. 
+  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega. 
+Qed. 
+
+
+
 (** ** Properties of multiplication *)
 
 Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -1783,6 +1813,16 @@ Proof.
   bit_solve. destruct (testbit x i); auto. 
 Qed.
 
+Lemma unsigned_not:
+  forall x, unsigned (not x) = max_unsigned - unsigned x.
+Proof.
+  intros. transitivity (unsigned (repr(-unsigned x - 1))).
+  f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega.
+  rewrite unsigned_repr_eq. apply Zmod_unique with (-1).
+  unfold max_unsigned. omega. 
+  generalize (unsigned_range x). unfold max_unsigned. omega.
+Qed.
+
 Theorem not_neg:
   forall x, not x = add (neg x) mone.
 Proof.
@@ -1807,6 +1847,23 @@ Proof.
   exists (-1). ring. 
 Qed.
 
+Theorem sub_borrow_add_carry:
+  forall x y b,
+  b = zero \/ b = one ->
+  sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one.
+Proof.
+  intros. unfold sub_borrow, add_carry. rewrite unsigned_not. 
+  replace (unsigned (xor b one)) with (1 - unsigned b).
+  destruct (zlt (unsigned x - unsigned y - unsigned b)).
+  rewrite zlt_true. rewrite xor_zero_l; auto.
+  unfold max_unsigned; omega.
+  rewrite zlt_false. rewrite xor_idem; auto.
+  unfold max_unsigned; omega. 
+  destruct H; subst b.
+  rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto.
+  rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto.
+Qed.
+
 (** Connections between [add] and bitwise logical operations. *)
 
 Lemma Z_add_is_or:
@@ -3382,6 +3439,23 @@ Proof.
   generalize wordsize_max_unsigned; omega.
 Qed.
 
+Theorem shr_lt_zero:
+  forall x,
+  shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero.
+Proof.
+  intros. apply same_bits_eq; intros.
+  rewrite bits_shr; auto.
+  rewrite unsigned_repr.
+  transitivity (testbit x (zwordsize - 1)).
+  f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega.
+  rewrite sign_bit_of_unsigned. 
+  unfold lt. rewrite signed_zero. unfold signed. 
+  destruct (zlt (unsigned x) half_modulus).
+  rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega. 
+  rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega.
+  generalize wordsize_max_unsigned; omega.
+Qed.
+
 Theorem ltu_range_test:
   forall x y,
   ltu x y = true -> unsigned y <= max_signed ->
@@ -3393,6 +3467,43 @@ Proof.
   generalize (unsigned_range x). omega. omega.
 Qed.
 
+Theorem lt_sub_overflow:
+  forall x y,
+  xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero.
+Proof.
+  intros. unfold negative, sub_overflow, lt. rewrite sub_signed. 
+  rewrite signed_zero. rewrite Zminus_0_r.
+  generalize (signed_range x) (signed_range y).
+  set (X := signed x); set (Y := signed y). intros RX RY.
+  unfold min_signed, max_signed in *.
+  generalize half_modulus_pos half_modulus_modulus; intros HM MM.
+  destruct (zle 0 (X - Y)).
+- unfold proj_sumbool at 1; rewrite zle_true at 1 by omega. simpl.
+  rewrite (zlt_false _ X) by omega.
+  destruct (zlt (X - Y) half_modulus).
+  + unfold proj_sumbool; rewrite zle_true by omega.
+    rewrite signed_repr. rewrite zlt_false by omega. apply xor_idem.
+    unfold min_signed, max_signed; omega.
+  + unfold proj_sumbool; rewrite zle_false by omega. 
+    replace (signed (repr (X - Y))) with (X - Y - modulus).
+    rewrite zlt_true by omega. apply xor_idem. 
+    rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y). 
+    rewrite zlt_false; auto. 
+    symmetry. apply Zmod_unique with 0; omega.
+- unfold proj_sumbool at 2. rewrite zle_true at 1 by omega. rewrite andb_true_r.
+  rewrite (zlt_true _ X) by omega.
+  destruct (zlt (X - Y) (-half_modulus)).
+  + unfold proj_sumbool; rewrite zle_false by omega. 
+    replace (signed (repr (X - Y))) with (X - Y + modulus).
+    rewrite zlt_false by omega. apply xor_zero.
+    rewrite signed_repr_eq. replace ((X - Y) mod modulus) with (X - Y + modulus). 
+    rewrite zlt_true by omega; auto.
+    symmetry. apply Zmod_unique with (-1); omega.
+  + unfold proj_sumbool; rewrite zle_true by omega.
+    rewrite signed_repr. rewrite zlt_true by omega. apply xor_zero_l.
+    unfold min_signed, max_signed; omega.
+Qed.
+
 (** Non-overlapping test *)
 
 Definition no_overlap (ofs1: int) (sz1: Z) (ofs2: int) (sz2: Z) : bool :=