Merge of the nonstrict-ops branch:

- Most RTL operators now evaluate to Some Vundef instead of None
  when undefined behavior occurs.
- More aggressive instruction selection.
- "Bertotization" of pattern-matchings now implemented by a proper preprocessor.
- Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim.


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

4 files changed, 296 insertions, 237 deletions

diff --git a/common/Memdata.v b/common/Memdata.v
index fde8b47..47ed79e 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -1029,22 +1029,6 @@ Proof.
   apply repeat_Undef_inject_any. apply encode_val_length. 
 Qed.
 
-(** The identity injection has interesting properties. *)
-
-Definition inject_id : meminj := fun b => Some(b, 0).
-
-Lemma val_inject_id:
-  forall v1 v2,
-  val_inject inject_id v1 v2 <-> Val.lessdef v1 v2.
-Proof.
-  intros; split; intros.
-  inv H. constructor. constructor.
-  unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor.
-  constructor.
-  inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto.
-  constructor.
-Qed.
-
 Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id.
 
 Lemma memval_lessdef_refl:
diff --git a/common/Memory.v b/common/Memory.v
index 157867e..e1c68bd 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -3105,6 +3105,15 @@ Proof.
   eapply mi_access; eauto. auto. 
 Qed.
 
+Theorem valid_pointer_extends:
+  forall m1 m2 b ofs,
+  extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
+Proof.
+  intros. 
+  rewrite valid_pointer_valid_access in *. 
+  eapply valid_access_extends; eauto.
+Qed.
+
 (*
 Theorem bounds_extends:
   forall m1 m2 b,
diff --git a/common/Memtype.v b/common/Memtype.v
index 40e03a3..f763581 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -917,6 +917,9 @@ Axiom perm_extends:
 Axiom valid_access_extends:
   forall m1 m2 chunk b ofs p,
   extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p.
+Axiom valid_pointer_extends:
+  forall m1 m2 b ofs,
+  extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.
 
 (** * Memory injections *)
 
diff --git a/common/Values.v b/common/Values.v
index 4dc74b2..7fae3b7 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -54,8 +54,6 @@ Definition Vfalse: val := Vint Int.zero.
 
 Module Val.
 
-Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.
-
 Definition has_type (v: val) (t: typ) : Prop :=
   match v, t with
   | Vundef, _ => True
@@ -115,28 +113,31 @@ Definition absf (v: val) : val :=
   | _ => Vundef
   end.
 
-Definition intoffloat (v: val) : val :=
+Definition maketotal (ov: option val) : val :=
+  match ov with Some v => v | None => Vundef end.
+
+Definition intoffloat (v: val) : option val :=
   match v with
-  | Vfloat f => match Float.intoffloat f with Some n => Vint n | None => Vundef end
-  | _ => Vundef
+  | Vfloat f => option_map Vint (Float.intoffloat f)
+  | _ => None
   end.
 
-Definition intuoffloat (v: val) : val :=
+Definition intuoffloat (v: val) : option val :=
   match v with
-  | Vfloat f => match Float.intuoffloat f with Some n => Vint n | None => Vundef end
-  | _ => Vundef
+  | Vfloat f => option_map Vint (Float.intuoffloat f)
+  | _ => None
   end.
 
-Definition floatofint (v: val) : val :=
+Definition floatofint (v: val) : option val :=
   match v with
-  | Vint n => Vfloat (Float.floatofint n)
-  | _ => Vundef
+  | Vint n => Some (Vfloat (Float.floatofint n))
+  | _ => None
   end.
 
-Definition floatofintu (v: val) : val :=
+Definition floatofintu (v: val) : option val :=
   match v with
-  | Vint n => Vfloat (Float.floatofintu n)
-  | _ => Vundef
+  | Vint n => Some (Vfloat (Float.floatofintu n))
+  | _ => None
   end.
 
 Definition floatofwords (v1 v2: val) : val :=
@@ -145,12 +146,20 @@ Definition floatofwords (v1 v2: val) : val :=
   | _, _ => Vundef
   end.
 
+Definition negint (v: val) : val :=
+  match v with
+  | Vint n => Vint (Int.neg n)
+  | _ => Vundef
+  end.
+
 Definition notint (v: val) : val :=
   match v with
-  | Vint n => Vint (Int.xor n Int.mone)
+  | Vint n => Vint (Int.not n)
   | _ => Vundef
   end.
 
+Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.
+
 Definition notbool (v: val) : val :=
   match v with
   | Vint n => of_bool (Int.eq n Int.zero)
@@ -199,32 +208,32 @@ Definition mul (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
-Definition divs (v1 v2: val): val :=
+Definition divs (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then Vundef else Vint(Int.divs n1 n2)
-  | _, _ => Vundef
+      if Int.eq n2 Int.zero then None else Some(Vint(Int.divs n1 n2))
+  | _, _ => None
   end.
 
-Definition mods (v1 v2: val): val :=
+Definition mods (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
-  | _, _ => Vundef
+      if Int.eq n2 Int.zero then None else Some(Vint(Int.mods n1 n2))
+  | _, _ => None
   end.
 
-Definition divu (v1 v2: val): val :=
+Definition divu (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
-  | _, _ => Vundef
+      if Int.eq n2 Int.zero then None else Some(Vint(Int.divu n1 n2))
+  | _, _ => None
   end.
 
-Definition modu (v1 v2: val): val :=
+Definition modu (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
-  | _, _ => Vundef
+      if Int.eq n2 Int.zero then None else Some(Vint(Int.modu n1 n2))
+  | _, _ => None
   end.
 
 Definition add_carry (v1 v2 cin: val): val :=
@@ -278,13 +287,13 @@ Definition shr_carry (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
-Definition shrx (v1 v2: val): val :=
+Definition shrx (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-     if Int.ltu n2 Int.iwordsize
-     then Vint(Int.shrx n1 n2)
-     else Vundef
-  | _, _ => Vundef
+     if Int.ltu n2 (Int.repr 31)
+     then Some(Vint(Int.shrx n1 n2))
+     else None
+  | _, _ => None
   end.
 
 Definition shru (v1 v2: val): val :=
@@ -335,48 +344,60 @@ Definition divf (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
-Definition cmp_mismatch (c: comparison): val :=
-  match c with
-  | Ceq => Vfalse
-  | Cne => Vtrue
-  | _   => Vundef
-  end.
+Section COMPARISONS.
 
-Definition cmp (c: comparison) (v1 v2: val): val :=
+Variable valid_ptr: block -> Z -> bool.
+
+Definition cmp_bool (c: comparison) (v1 v2: val): option bool :=
   match v1, v2 with
-  | Vint n1, Vint n2 => of_bool (Int.cmp c n1 n2)
-  | Vint n1, Vptr b2 ofs2 =>
-      if Int.eq n1 Int.zero then cmp_mismatch c else Vundef
-  | Vptr b1 ofs1, Vptr b2 ofs2 =>
-      if zeq b1 b2
-      then of_bool (Int.cmp c ofs1 ofs2)
-      else cmp_mismatch c
-  | Vptr b1 ofs1, Vint n2 =>
-      if Int.eq n2 Int.zero then cmp_mismatch c else Vundef
-  | _, _ => Vundef
+  | Vint n1, Vint n2 => Some (Int.cmp c n1 n2)
+  | _, _ => None
   end.
 
-Definition cmpu (c: comparison) (v1 v2: val): val :=
+Definition cmp_different_blocks (c: comparison): option bool :=
+  match c with
+  | Ceq => Some false
+  | Cne => Some true
+  | _   => None
+  end.
+
+Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      of_bool (Int.cmpu c n1 n2)
+      Some (Int.cmpu c n1 n2)
   | Vint n1, Vptr b2 ofs2 =>
-      if Int.eq n1 Int.zero then cmp_mismatch c else Vundef
+      if Int.eq n1 Int.zero then cmp_different_blocks c else None
   | Vptr b1 ofs1, Vptr b2 ofs2 =>
-      if zeq b1 b2
-      then of_bool (Int.cmpu c ofs1 ofs2)
-      else cmp_mismatch c
+      if valid_ptr b1 (Int.unsigned ofs1) && valid_ptr b2 (Int.unsigned ofs2) then
+        if zeq b1 b2
+        then Some (Int.cmpu c ofs1 ofs2)
+        else cmp_different_blocks c
+      else None
   | Vptr b1 ofs1, Vint n2 =>
-      if Int.eq n2 Int.zero then cmp_mismatch c else Vundef
-  | _, _ => Vundef
+      if Int.eq n2 Int.zero then cmp_different_blocks c else None
+  | _, _ => None
   end.
 
-Definition cmpf (c: comparison) (v1 v2: val): val :=
+Definition cmpf_bool (c: comparison) (v1 v2: val): option bool :=
   match v1, v2 with
-  | Vfloat f1, Vfloat f2 => of_bool (Float.cmp c f1 f2)
-  | _, _ => Vundef
+  | Vfloat f1, Vfloat f2 => Some (Float.cmp c f1 f2)
+  | _, _ => None
   end.
 
+Definition of_optbool (ob: option bool): val :=
+  match ob with Some true => Vtrue | Some false => Vfalse | None => Vundef end.
+
+Definition cmp (c: comparison) (v1 v2: val): val :=
+  of_optbool (cmp_bool c v1 v2).
+
+Definition cmpu (c: comparison) (v1 v2: val): val :=
+  of_optbool (cmpu_bool c v1 v2).
+
+Definition cmpf (c: comparison) (v1 v2: val): val :=
+  of_optbool (cmpf_bool c v1 v2).
+
+End COMPARISONS.
+
 (** [load_result] is used in the memory model (library [Mem])
   to post-process the results of a memory read.  For instance,
   consider storing the integer value [0xFFF] on 1 byte at a
@@ -483,6 +504,12 @@ Proof.
   destruct b; reflexivity.
 Qed.
 
+Theorem notbool_negb_3:
+  forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob).
+Proof.
+  destruct ob; auto. destruct b; auto.
+Qed.
+
 Theorem notbool_idem2:
   forall b, notbool(notbool(of_bool b)) = of_bool b.
 Proof.
@@ -496,6 +523,12 @@ Proof.
   case (Int.eq i Int.zero); reflexivity.
 Qed.
 
+Theorem notbool_idem4:
+  forall ob, notbool (notbool (of_optbool ob)) = of_optbool ob.
+Proof.
+  destruct ob; auto. destruct b; auto.
+Qed.
+
 Theorem add_commut: forall x y, add x y = add y x.
 Proof.
   destruct x; destruct y; simpl; auto.
@@ -612,59 +645,59 @@ Proof.
 Qed.  
 
 Theorem mods_divs:
-  forall x y, mods x y = sub x (mul (divs x y) y).
+  forall x y z,
+  mods x y = Some z -> exists v, divs x y = Some v /\ z = sub x (mul v y).
 Proof.
-  destruct x; destruct y; simpl; auto.
-  case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs.
+  intros. destruct x; destruct y; simpl in *; try discriminate.
+  destruct (Int.eq i0 Int.zero); inv H. 
+  exists (Vint (Int.divs i i0)); split; auto. 
+  simpl. rewrite Int.mods_divs. auto.
 Qed.
 
 Theorem modu_divu:
-  forall x y, modu x y = sub x (mul (divu x y) y).
+  forall x y z,
+  modu x y = Some z -> exists v, divu x y = Some v /\ z = sub x (mul v y).
 Proof.
-  destruct x; destruct y; simpl; auto.
-  generalize (Int.eq_spec i0 Int.zero);
-  case (Int.eq i0 Int.zero); simpl. auto. 
-  intro. decEq. apply Int.modu_divu. auto.
+  intros. destruct x; destruct y; simpl in *; try discriminate.
+  destruct (Int.eq i0 Int.zero) as []_eqn; inv H. 
+  exists (Vint (Int.divu i i0)); split; auto. 
+  simpl. rewrite Int.modu_divu. auto.
+  generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto. 
 Qed.
 
 Theorem divs_pow2:
-  forall x n logn,
-  Int.is_power2 n = Some logn ->
-  divs x (Vint n) = shrx x (Vint logn).
+  forall x n logn y,
+  Int.is_power2 n = Some logn -> Int.ltu logn (Int.repr 31) = true ->
+  divs x (Vint n) = Some y ->
+  shrx x (Vint logn) = Some y.
 Proof.
-  intros; destruct x; simpl; auto.
-  change 32 with (Z_of_nat Int.wordsize).
-  rewrite (Int.is_power2_range _ _ H). 
-  generalize (Int.eq_spec n Int.zero);
-  case (Int.eq n Int.zero); intro.
-  subst n. compute in H. discriminate.
-  decEq. apply Int.divs_pow2. auto.
+  intros; destruct x; simpl in H1; inv H1.
+  destruct (Int.eq n Int.zero); inv H3. 
+  simpl. rewrite H0. decEq. decEq. symmetry. apply Int.divs_pow2. auto.
 Qed.
 
 Theorem divu_pow2:
-  forall x n logn,
+  forall x n logn y,
   Int.is_power2 n = Some logn ->
-  divu x (Vint n) = shru x (Vint logn).
+  divu x (Vint n) = Some y ->
+  shru x (Vint logn) = y.
 Proof.
-  intros; destruct x; simpl; auto.
-  change 32 with (Z_of_nat Int.wordsize).
-  rewrite (Int.is_power2_range _ _ H). 
-  generalize (Int.eq_spec n Int.zero);
-  case (Int.eq n Int.zero); intro.
-  subst n. compute in H. discriminate.
-  decEq. apply Int.divu_pow2. auto.
+  intros; destruct x; simpl in H0; inv H0.
+  destruct (Int.eq n Int.zero); inv H2. 
+  simpl. 
+  rewrite (Int.is_power2_range _ _ H).
+  decEq. symmetry. apply Int.divu_pow2. auto.
 Qed.
 
 Theorem modu_pow2:
-  forall x n logn,
+  forall x n logn y,
   Int.is_power2 n = Some logn ->
-  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).
+  modu x (Vint n) = Some y ->
+  and x (Vint (Int.sub n Int.one)) = y.
 Proof.
-  intros; destruct x; simpl; auto.
-  generalize (Int.eq_spec n Int.zero);
-  case (Int.eq n Int.zero); intro.
-  subst n. compute in H. discriminate.
-  decEq. eapply Int.modu_and; eauto.
+  intros; destruct x; simpl in H0; inv H0.
+  destruct (Int.eq n Int.zero); inv H2. 
+  simpl. decEq. symmetry. eapply Int.modu_and; eauto.
 Qed.
 
 Theorem and_commut: forall x y, and x y = and y x.
@@ -700,7 +733,7 @@ Proof.
   decEq. apply Int.xor_assoc.
 Qed.
 
-Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
+Theorem shl_mul: forall x y, mul x (shl Vone y) = shl x y.
 Proof.
   destruct x; destruct y; simpl; auto. 
   case (Int.ltu i0 Int.iwordsize); auto.
@@ -726,12 +759,32 @@ Proof.
 Qed.
 
 Theorem shrx_carry:
-  forall x y,
-  add (shr x y) (shr_carry x y) = shrx x y.
-Proof.
-  destruct x; destruct y; simpl; auto.
-  case (Int.ltu i0 Int.iwordsize); auto.
-  simpl. decEq. apply Int.shrx_carry.
+  forall x y z,
+  shrx x y = Some z ->
+  add (shr x y) (shr_carry x y) = z.
+Proof.
+  intros. destruct x; destruct y; simpl in H; inv H. 
+  destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1.
+  exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
+  assert (Int.ltu i0 Int.iwordsize = true). 
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. 
+  simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto.
+Qed.
+
+Theorem shrx_shr:
+  forall x y z,
+  shrx x y = Some z ->
+  exists p, exists q,
+    x = Vint p /\ y = Vint q /\
+    z = shr (if Int.lt p Int.zero then add x (Vint (Int.sub (Int.shl Int.one q) Int.one)) else x) (Vint q).
+Proof.
+  intros. destruct x; destruct y; simpl in H; inv H. 
+  destruct (Int.ltu i0 (Int.repr 31)) as []_eqn; inv H1.
+  exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros.
+  assert (Int.ltu i0 Int.iwordsize = true). 
+    unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. 
+  exists i; exists i0; intuition. 
+  rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto.
 Qed.
 
 Theorem or_rolm:
@@ -765,173 +818,112 @@ Proof.
   destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut.
 Qed.
 
-Lemma negate_cmp_mismatch:
-  forall c,
-  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).
+Theorem negate_cmp_bool:
+  forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y).
 Proof.
-  destruct c; reflexivity.
+  destruct x; destruct y; simpl; auto. rewrite Int.negate_cmp. auto.
 Qed.
 
-Theorem negate_cmp:
-  forall c x y,
-  cmp (negate_comparison c) x y = notbool (cmp c x y).
+Theorem negate_cmpu_bool:
+  forall valid_ptr c x y,
+  cmpu_bool valid_ptr (negate_comparison c) x y = option_map negb (cmpu_bool valid_ptr c x y).
 Proof.
+  assert (forall c,
+    cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)).
+  destruct c; auto. 
   destruct x; destruct y; simpl; auto.
-  rewrite Int.negate_cmp. apply notbool_negb_1.
-  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
-  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
-  case (zeq b b0); intro.
-  rewrite Int.negate_cmp. apply notbool_negb_1.
-  apply negate_cmp_mismatch.
+  rewrite Int.negate_cmpu. auto.
+  destruct (Int.eq i Int.zero); auto. 
+  destruct (Int.eq i0 Int.zero); auto.
+  destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto.
+  destruct (zeq b b0); auto. rewrite Int.negate_cmpu. auto.
 Qed.
 
-Theorem negate_cmpu:
+Lemma not_of_optbool:
+  forall ob, of_optbool (option_map negb ob) = notbool (of_optbool ob).
+Proof.
+  destruct ob; auto. destruct b; auto. 
+Qed.
+
+Theorem negate_cmp:
   forall c x y,
-  cmpu (negate_comparison c) x y = notbool (cmpu c x y).
+  cmp (negate_comparison c) x y = notbool (cmp c x y).
 Proof.
-  destruct x; destruct y; simpl; auto.
-  rewrite Int.negate_cmpu. apply notbool_negb_1.
-  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
-  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
-  case (zeq b b0); intro.
-  rewrite Int.negate_cmpu. apply notbool_negb_1.
-  apply negate_cmp_mismatch.
+  intros. unfold cmp. rewrite negate_cmp_bool. apply not_of_optbool.
 Qed.
 
-Lemma swap_cmp_mismatch:
-  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.
+Theorem negate_cmpu:
+  forall valid_ptr c x y,
+  cmpu valid_ptr (negate_comparison c) x y = notbool (cmpu valid_ptr c x y).
 Proof.
-  destruct c; reflexivity.
+  intros. unfold cmpu. rewrite negate_cmpu_bool. apply not_of_optbool.
 Qed.
-  
-Theorem swap_cmp:
+
+Theorem swap_cmp_bool:
   forall c x y,
-  cmp (swap_comparison c) x y = cmp c y x.
+  cmp_bool (swap_comparison c) x y = cmp_bool c y x.
 Proof.
-  destruct x; destruct y; simpl; auto.
-  rewrite Int.swap_cmp. auto.
-  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
-  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
-  case (zeq b b0); intro.
-  subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto.
-  rewrite zeq_false. apply swap_cmp_mismatch. auto.
+  destruct x; destruct y; simpl; auto. rewrite Int.swap_cmp. auto.
 Qed.
 
-Theorem swap_cmpu:
-  forall c x y,
-  cmpu (swap_comparison c) x y = cmpu c y x.
+Theorem swap_cmpu_bool:
+  forall valid_ptr c x y,
+  cmpu_bool valid_ptr (swap_comparison c) x y = cmpu_bool valid_ptr c y x.
 Proof.
+  assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
+    destruct c; auto.
   destruct x; destruct y; simpl; auto.
   rewrite Int.swap_cmpu. auto.
-  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
-  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
-  case (zeq b b0); intro.
-  subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto.
-  rewrite zeq_false. apply swap_cmp_mismatch. auto.
+  case (Int.eq i Int.zero); auto.
+  case (Int.eq i0 Int.zero); auto.
+  destruct (valid_ptr b (Int.unsigned i)); destruct (valid_ptr b0 (Int.unsigned i0)); auto.
+  simpl. destruct (zeq b b0); subst. 
+  rewrite zeq_true. rewrite Int.swap_cmpu. auto.
+  rewrite zeq_false; auto.
 Qed.
 
 Theorem negate_cmpf_eq:
   forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
 Proof.
-  destruct v1; destruct v2; simpl; auto.
-  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. 
-  apply notbool_idem2.
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
 Theorem negate_cmpf_ne:
   forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
 Proof.
-  destruct v1; destruct v2; simpl; auto.
-  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto. 
-Qed.
-
-Lemma or_of_bool:
-  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
-Proof.
-  destruct b1; destruct b2; reflexivity.
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
 Theorem cmpf_le:
   forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
 Proof.
-  destruct v1; destruct v2; simpl; auto.
-  rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq.
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  rewrite Float.cmp_le_lt_eq.
+  destruct (Float.cmp Clt f f0); destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
 Theorem cmpf_ge:
   forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
 Proof.
-  destruct v1; destruct v2; simpl; auto.
-  rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq.
-Qed.
-
-Definition is_bool (v: val) :=
-  v = Vundef \/ v = Vtrue \/ v = Vfalse.
-
-Lemma of_bool_is_bool:
-  forall b, is_bool (of_bool b).
-Proof.
-  destruct b; unfold is_bool; simpl; tauto.
-Qed.
-
-Lemma undef_is_bool: is_bool Vundef.
-Proof.
-  unfold is_bool; tauto.
+  destruct v1; destruct v2; auto. unfold cmpf, cmpf_bool. 
+  rewrite Float.cmp_ge_gt_eq.
+  destruct (Float.cmp Cgt f f0); destruct (Float.cmp Ceq f f0); auto.
 Qed.
 
-Lemma cmp_mismatch_is_bool:
-  forall c, is_bool (cmp_mismatch c).
+Lemma zero_ext_and:
+  forall n v, 
+  0 < n < Z_of_nat Int.wordsize ->
+  Val.zero_ext n v = Val.and v (Vint (Int.repr (two_p n - 1))).
 Proof.
-  destruct c; simpl; unfold is_bool; tauto.
-Qed.
-
-Lemma cmp_is_bool:
-  forall c v1 v2, is_bool (cmp c v1 v2).
-Proof.
-  destruct v1; destruct v2; simpl; try apply undef_is_bool.
-  apply of_bool_is_bool.
-  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
-  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
-  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
-Qed.
-
-Lemma cmpu_is_bool:
-  forall c v1 v2, is_bool (cmpu c v1 v2).
-Proof.
-  destruct v1; destruct v2; simpl; try apply undef_is_bool.
-  apply of_bool_is_bool.
-  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
-  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
-  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
-Qed.
-
-Lemma cmpf_is_bool:
-  forall c v1 v2, is_bool (cmpf c v1 v2).
-Proof.
-  destruct v1; destruct v2; simpl;
-  apply undef_is_bool || apply of_bool_is_bool.
-Qed.
-
-Lemma notbool_is_bool:
-  forall v, is_bool (notbool v).
-Proof.
-  destruct v; simpl.
-  apply undef_is_bool. apply of_bool_is_bool. 
-  apply undef_is_bool. unfold is_bool; tauto.
-Qed.
-
-Lemma notbool_xor:
-  forall v, is_bool v -> v = xor (notbool v) Vone.
-Proof.
-  intros. elim H; intro.  
-  subst v. reflexivity.
-  elim H0; intro; subst v; reflexivity.
+  intros. destruct v; simpl; auto. decEq. apply Int.zero_ext_and; auto.
 Qed.
 
 Lemma rolm_lt_zero:
   forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
 Proof.
-  intros. destruct v; simpl; auto.
+  intros. unfold cmp, cmp_bool; destruct v; simpl; auto.
   transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
   decEq. symmetry. rewrite Int.shru_rolm. auto. auto. 
   rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto. 
@@ -942,7 +934,7 @@ Lemma rolm_ge_zero:
   xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
 Proof.
   intros. rewrite rolm_lt_zero. destruct v; simpl; auto.
-  destruct (Int.lt i Int.zero); auto.
+  unfold cmp; simpl. destruct (Int.lt i Int.zero); auto.
 Qed.
 
 (** The ``is less defined'' relation between values. 
@@ -953,6 +945,12 @@ Inductive lessdef: val -> val -> Prop :=
   | lessdef_refl: forall v, lessdef v v
   | lessdef_undef: forall v, lessdef Vundef v.
 
+Lemma lessdef_trans:
+  forall v1 v2 v3, lessdef v1 v2 -> lessdef v2 v3 -> lessdef v1 v3.
+Proof.
+  intros. inv H. auto. constructor.
+Qed.
+
 Inductive lessdef_list: list val -> list val -> Prop :=
   | lessdef_list_nil:
       lessdef_list nil nil
@@ -972,6 +970,8 @@ Proof.
   left; congruence. tauto. tauto.
 Qed.
 
+(** Compatibility of operations with the [lessdef] relation. *)
+
 Lemma load_result_lessdef:
   forall chunk v1 v2,
   lessdef v1 v2 -> lessdef (load_result chunk v1) (load_result chunk v2).
@@ -997,6 +997,37 @@ Proof.
   intros; inv H; simpl; auto.
 Qed.
 
+Lemma add_lessdef:
+  forall v1 v1' v2 v2',
+  lessdef v1 v1' -> lessdef v2 v2' -> lessdef (add v1 v2) (add v1' v2').
+Proof.
+  intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
+Qed.
+
+Lemma cmpu_bool_lessdef:
+  forall valid_ptr valid_ptr' c v1 v1' v2 v2' b,
+  (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) ->
+  lessdef v1 v1' -> lessdef v2 v2' ->
+  cmpu_bool valid_ptr c v1 v2 = Some b ->
+  cmpu_bool valid_ptr' c v1' v2' = Some b.
+Proof.
+  intros. 
+  destruct v1; simpl in H2; try discriminate;
+  destruct v2; simpl in H2; try discriminate;
+  inv H0; inv H1; simpl; auto.
+  destruct (valid_ptr b0 (Int.unsigned i)) as []_eqn; try discriminate.
+  destruct (valid_ptr b1 (Int.unsigned i0)) as []_eqn; try discriminate.
+  rewrite (H _ _ Heqb2). rewrite (H _ _ Heqb0). auto.
+Qed.
+
+Lemma of_optbool_lessdef:
+  forall ob ob',
+  (forall b, ob = Some b -> ob' = Some b) ->
+  lessdef (of_optbool ob) (of_optbool ob').
+Proof.
+  intros. destruct ob; simpl; auto. rewrite (H b); auto. 
+Qed.
+
 End Val.
 
 (** * Values and memory injections *)
@@ -1085,3 +1116,35 @@ Qed.
 
 Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
 
+Lemma val_inject_lessdef:
+  forall v1 v2, Val.lessdef v1 v2 <-> val_inject (fun b => Some(b, 0)) v1 v2.
+Proof.
+  intros; split; intros.
+  inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. 
+  inv H; auto. inv H0. rewrite Int.add_zero; auto.
+Qed.
+
+Lemma val_list_inject_lessdef:
+  forall vl1 vl2, Val.lessdef_list vl1 vl2 <-> val_list_inject (fun b => Some(b, 0)) vl1 vl2.
+Proof.
+  intros; split.
+  induction 1; constructor; auto. apply val_inject_lessdef; auto.
+  induction 1; constructor; auto. apply val_inject_lessdef; auto.
+Qed.
+
+(** The identity injection gives rise to the "less defined than" relation. *)
+
+Definition inject_id : meminj := fun b => Some(b, 0).
+
+Lemma val_inject_id:
+  forall v1 v2,
+  val_inject inject_id v1 v2 <-> Val.lessdef v1 v2.
+Proof.
+  intros; split; intros.
+  inv H. constructor. constructor.
+  unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor.
+  constructor.
+  inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto.
+  constructor.
+Qed.
+