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

4 files changed, 480 insertions, 248 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 769b3f9..43a1435 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -51,18 +51,10 @@ Proof. decide equality. Defined.
 (** Bits in the condition register. *)
 
 Inductive crbit: Type :=
-  | CReq: crbit    (**r equal *)
-  | CRne: crbit    (**r not equal *)
-  | CRhs: crbit    (**r unsigned higher or same *)
-  | CRlo: crbit    (**r unsigned lower *)
-  | CRmi: crbit    (**r negative *)
-  | CRpl: crbit    (**r positive *)
-  | CRhi: crbit    (**r unsigned higher *)
-  | CRls: crbit    (**r unsigned lower or same *)
-  | CRge: crbit    (**r signed greater or equal *)
-  | CRlt: crbit    (**r signed less than *)
-  | CRgt: crbit    (**r signed greater *)
-  | CRle: crbit.   (**r signed less than or equal *)
+  | CN: crbit    (**r negative *)
+  | CZ: crbit    (**r zero *)
+  | CC: crbit    (**r carry *)
+  | CV: crbit.   (**r overflow *)
 
 Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
@@ -123,12 +115,26 @@ Inductive shift_addr : Type :=
   | SAasr: ireg -> int -> shift_addr
   | SAror: ireg -> int -> shift_addr.
 
+Inductive testcond : Type :=
+  | TCeq: testcond    (**r equal *)
+  | TCne: testcond    (**r not equal *)
+  | TChs: testcond    (**r unsigned higher or same *)
+  | TClo: testcond    (**r unsigned lower *)
+  | TCmi: testcond    (**r negative *)
+  | TCpl: testcond    (**r positive *)
+  | TChi: testcond    (**r unsigned higher *)
+  | TCls: testcond    (**r unsigned lower or same *)
+  | TCge: testcond    (**r signed greater or equal *)
+  | TClt: testcond    (**r signed less than *)
+  | TCgt: testcond    (**r signed greater *)
+  | TCle: testcond.   (**r signed less than or equal *)
+
 Inductive instruction : Type :=
   (* Core instructions *)
   | Padd: ireg -> ireg -> shift_op -> instruction (**r integer addition *)
   | Pand: ireg -> ireg -> shift_op -> instruction (**r bitwise and *)
   | Pb: label -> instruction                      (**r branch to label *)
-  | Pbc: crbit -> label -> instruction            (**r conditional branch to label *)
+  | Pbc: testcond -> label -> instruction            (**r conditional branch to label *)
   | Pbsymb: ident -> signature -> instruction                  (**r branch to symbol *)
   | Pbreg: ireg -> signature -> instruction                    (**r computed branch *)
   | Pblsymb: ident -> signature -> instruction                 (**r branch and link to symbol *)
@@ -143,7 +149,7 @@ Inductive instruction : Type :=
   | Pldrsh: ireg -> ireg -> shift_addr -> instruction (**r unsigned int16 load *)
   | Pmla: ireg -> ireg -> ireg -> ireg -> instruction      (**r integer multiply-add *)
   | Pmov: ireg -> shift_op -> instruction          (**r integer move *)
-  | Pmovc: crbit -> ireg -> shift_op -> instruction (**r integer conditional move *)
+  | Pmovc: testcond -> ireg -> shift_op -> instruction (**r integer conditional move *)
   | Pmul: ireg -> ireg -> ireg -> instruction      (**r integer multiplication *)
   | Pmvn: ireg -> shift_op -> instruction          (**r integer complement *)
   | Porr: ireg -> ireg -> shift_op -> instruction  (**r bitwise or *)
@@ -376,44 +382,102 @@ Definition exec_store (chunk: memory_chunk) (addr: val) (r: preg)
   | Some m' => Next (nextinstr rs) m'
   end.
 
-(** Operations over condition bits. *)
+(** Comparisons. *)
 
 Definition compare_int (rs: regset) (v1 v2: val) (m: mem) :=
-  rs#CReq <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
-    #CRne <- (Val.cmpu (Mem.valid_pointer m) Cne v1 v2)
-    #CRhs <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
-    #CRlo <- (Val.cmpu (Mem.valid_pointer m) Clt v1 v2)
-    #CRmi <- Vundef
-    #CRpl <- Vundef
-    #CRhi <- (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2)
-    #CRls <- (Val.cmpu (Mem.valid_pointer m) Cle v1 v2)
-    #CRge <- (Val.cmp Cge v1 v2)
-    #CRlt <- (Val.cmp Clt v1 v2)
-    #CRgt <- (Val.cmp Cgt v1 v2)
-    #CRle <- (Val.cmp Cle v1 v2).
+  rs#CN <- (Val.negative (Val.sub v1 v2))
+    #CZ <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
+    #CC <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
+    #CV <- (Val.sub_overflow v1 v2).
 
 (** Semantics of [fcmpd] instruction:
 <<
-==	EQ=1 NE=0 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=0 LS=1 GE=1 LT=0 GT=0 LE=1 
-<	EQ=0 NE=1 HS=0 LO=1 MI=1 PL=0 VS=0 VC=1 HI=0 LS=1 GE=0 LT=1 GT=0 LE=1 
->	EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=0 VC=1 HI=1 LS=0 GE=1 LT=0 GT=1 LE=0 
-unord	EQ=0 NE=1 HS=1 LO=0 MI=0 PL=1 VS=1 VC=0 HI=1 LS=0 GE=0 LT=1 GT=0 LE=1 
+==	N=0 Z=1 C=1 V=0
+<	N=1 Z=0 C=0 V=0
+>	N=0 Z=0 C=1 V=0
+unord	N=0 Z=0 C=1 V=1
 >>
 *)
 
 Definition compare_float (rs: regset) (v1 v2: val) :=
-  rs#CReq <- (Val.cmpf Ceq v1 v2)
-    #CRne <- (Val.cmpf Cne v1 v2)
-    #CRhs <- (Val.notbool (Val.cmpf Clt v1 v2))      (**r not lt *)
-    #CRlo <- (Val.cmpf Clt v1 v2)                    (**r lt *)
-    #CRmi <- (Val.cmpf Clt v1 v2)                    (**r lt *)
-    #CRpl <- (Val.notbool (Val.cmpf Clt v1 v2))      (**r not lt *)
-    #CRhi <- (Val.notbool (Val.cmpf Cle v1 v2))      (**r not le *)
-    #CRls <- (Val.cmpf Cle v1 v2)                    (**r le *)
-    #CRge <- (Val.cmpf Cge v1 v2)                    (**r ge *)
-    #CRlt <- (Val.notbool (Val.cmpf Cge v1 v2))      (**r not ge *)
-    #CRgt <- (Val.cmpf Cgt v1 v2)                    (**r gt *)
-    #CRle <- (Val.notbool (Val.cmpf Cgt v1 v2)).     (**r not gt *)
+  match v1, v2 with
+  | Vfloat f1, Vfloat f2 =>
+      rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2))
+        #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2))
+        #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2)))
+        #CV <- (Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)))
+  | _, _ =>
+      rs#CN <- Vundef
+        #CZ <- Vundef
+        #CC <- Vundef
+        #CV <- Vundef
+  end.
+
+(** Testing a condition *)
+
+Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
+  match c with
+  | TCeq =>                             (**r equal *)
+      match rs CZ with
+      | Vint n => Some (Int.eq n Int.one)
+      | _ => None
+      end
+  | TCne =>                             (**r not equal *)
+      match rs CZ with
+      | Vint n => Some (Int.eq n Int.zero)
+      | _ => None
+      end
+  | TClo =>                             (**r unsigned less than  *)
+      match rs CC with
+      | Vint n => Some (Int.eq n Int.zero)
+      | _ => None
+      end
+  | TCls =>                             (**r unsigned less or equal *)
+      match rs CC, rs CZ with
+      | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
+      | _, _ => None
+      end
+  | TChs =>                             (**r unsigned greater or equal *)
+      match rs CC with
+      | Vint n => Some (Int.eq n Int.one)
+      | _ => None
+      end
+  | TChi =>                             (**r unsigned greater *)
+      match rs CC, rs CZ with
+      | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
+      | _, _ => None
+      end
+  | TClt =>                             (**r signed less than *)
+      match rs CV, rs CN with
+      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
+      | _, _ => None
+      end
+  | TCle =>                             (**r signed less or equal *)
+      match rs CV, rs CN, rs CZ with
+      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
+      | _, _, _ => None
+      end
+  | TCge =>                             (**r signed greater or equal *)
+      match rs CV, rs CN with
+      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
+      | _, _ => None
+      end
+  | TCgt =>                             (**r signed greater *)
+      match rs CV, rs CN, rs CZ with
+      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
+      | _, _, _ => None
+      end
+  | TCpl =>                             (**r positive *)
+      match rs CN with
+      | Vint n => Some (Int.eq n Int.zero)
+      | _ => None
+      end
+  | TCmi =>                             (**r negative *)
+      match rs CN with
+      | Vint n => Some (Int.eq n Int.one)
+      | _ => None
+      end
+  end.
 
 (** Execution of a single instruction [i] in initial state
     [rs] and [m].  Return updated state.  For instructions
@@ -441,10 +505,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#r1 <- (Val.and rs#r2 (eval_shift_op so rs)))) m
   | Pb lbl =>                      
       goto_label f lbl rs m
-  | Pbc bit lbl =>            
-      match rs#bit with
-      | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label f lbl rs m
-      | _ => Stuck
+  | Pbc cond lbl =>            
+      match eval_testcond cond rs with
+      | Some true => goto_label f lbl rs m
+      | Some false => Next (nextinstr rs) m
+      | None => Stuck
       end
   | Pbsymb id sg =>                  
       Next (rs#PC <- (symbol_offset id Int.zero)) m
@@ -474,12 +539,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#r1 <- (Val.add (Val.mul rs#r2 rs#r3) rs#r4))) m
   | Pmov r1 so =>          
       Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
-  | Pmovc bit r1 so =>          
-      match rs#bit with
-      | Vint n => if Int.eq n Int.zero 
-                  then Next (nextinstr rs) m
-                  else Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
-      | _ => Next (nextinstr (rs#r1 <- Vundef)) m
+  | Pmovc cond r1 so =>          
+      match eval_testcond cond rs with
+      | Some true => Next (nextinstr (rs#r1 <- (eval_shift_op so rs))) m
+      | Some false => Next (nextinstr rs) m
+      | None => Next (nextinstr (rs#r1 <- Vundef)) m
       end
   | Pmul r1 r2 r3 =>      
       Next (nextinstr (rs#r1 <- (Val.mul rs#r2 rs#r3))) m
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index d160b2d..6645149 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -189,58 +189,58 @@ Definition transl_cond
       Error(msg "Asmgen.transl_cond")
   end.
 
-Definition crbit_for_signed_cmp (cmp: comparison) :=
+Definition cond_for_signed_cmp (cmp: comparison) :=
   match cmp with
-  | Ceq => CReq
-  | Cne => CRne
-  | Clt => CRlt
-  | Cle => CRle
-  | Cgt => CRgt
-  | Cge => CRge
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TClt
+  | Cle => TCle
+  | Cgt => TCgt
+  | Cge => TCge
   end.
 
-Definition crbit_for_unsigned_cmp (cmp: comparison) :=
+Definition cond_for_unsigned_cmp (cmp: comparison) :=
   match cmp with
-  | Ceq => CReq
-  | Cne => CRne
-  | Clt => CRlo
-  | Cle => CRls
-  | Cgt => CRhi
-  | Cge => CRhs
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TClo
+  | Cle => TCls
+  | Cgt => TChi
+  | Cge => TChs
   end.
 
-Definition crbit_for_float_cmp (cmp: comparison) :=
+Definition cond_for_float_cmp (cmp: comparison) :=
   match cmp with
-  | Ceq => CReq
-  | Cne => CRne
-  | Clt => CRmi
-  | Cle => CRls
-  | Cgt => CRgt
-  | Cge => CRge
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TCmi
+  | Cle => TCls
+  | Cgt => TCgt
+  | Cge => TCge
   end.
 
-Definition crbit_for_float_not_cmp (cmp: comparison) :=
+Definition cond_for_float_not_cmp (cmp: comparison) :=
   match cmp with
-  | Ceq => CRne
-  | Cne => CReq
-  | Clt => CRpl
-  | Cle => CRhi
-  | Cgt => CRle
-  | Cge => CRlt
+  | Ceq => TCne
+  | Cne => TCeq
+  | Clt => TCpl
+  | Cle => TChi
+  | Cgt => TCle
+  | Cge => TClt
   end.
 
-Definition crbit_for_cond (cond: condition) :=
+Definition cond_for_cond (cond: condition) :=
   match cond with
-  | Ccomp cmp => crbit_for_signed_cmp cmp
-  | Ccompu cmp => crbit_for_unsigned_cmp cmp
-  | Ccompshift cmp s => crbit_for_signed_cmp cmp
-  | Ccompushift cmp s => crbit_for_unsigned_cmp cmp
-  | Ccompimm cmp n => crbit_for_signed_cmp cmp
-  | Ccompuimm cmp n => crbit_for_unsigned_cmp cmp
-  | Ccompf cmp => crbit_for_float_cmp cmp
-  | Cnotcompf cmp => crbit_for_float_not_cmp cmp
-  | Ccompfzero cmp => crbit_for_float_cmp cmp
-  | Cnotcompfzero cmp => crbit_for_float_not_cmp cmp
+  | Ccomp cmp => cond_for_signed_cmp cmp
+  | Ccompu cmp => cond_for_unsigned_cmp cmp
+  | Ccompshift cmp s => cond_for_signed_cmp cmp
+  | Ccompushift cmp s => cond_for_unsigned_cmp cmp
+  | Ccompimm cmp n => cond_for_signed_cmp cmp
+  | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
+  | Ccompf cmp => cond_for_float_cmp cmp
+  | Cnotcompf cmp => cond_for_float_not_cmp cmp
+  | Ccompfzero cmp => cond_for_float_cmp cmp
+  | Cnotcompfzero cmp => cond_for_float_not_cmp cmp
   end.
 
 (** Translation of the arithmetic operation [r <- op(args)].
@@ -360,7 +360,7 @@ Definition transl_op
       do r <- ireg_of res; do r1 <- ireg_of a1;
       OK (Pcmp r1 (SOimm Int.zero) ::
           addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one)
-             (Pmovc CRge IR14 (SOreg r1) ::
+             (Pmovc TCge IR14 (SOreg r1) ::
               Pmov r (SOasrimm IR14 n) :: k))
   | Onegf, a1 :: nil =>
       do r <- freg_of res; do r1 <- freg_of a1;
@@ -399,7 +399,7 @@ Definition transl_op
       do r <- ireg_of res;
       transl_cond cmp args
         (Pmov r (SOimm Int.zero) ::
-         Pmovc (crbit_for_cond cmp) r (SOimm Int.one) ::
+         Pmovc (cond_for_cond cmp) r (SOimm Int.one) ::
          k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
@@ -599,7 +599,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mgoto lbl =>
       OK (Pb lbl :: k)
   | Mcond cond args lbl =>
-      transl_cond cond args (Pbc (crbit_for_cond cond) lbl :: k)
+      transl_cond cond args (Pbc (cond_for_cond cond) lbl :: k)
   | Mjumptable arg tbl =>
       do r <- ireg_of arg;
       OK (Pbtbl r tbl :: k)
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 2f5f868..d77006a 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -536,39 +536,243 @@ Qed.
 Lemma compare_int_spec:
   forall rs v1 v2 m,
   let rs1 := nextinstr (compare_int rs v1 v2 m) in
-     rs1#CReq = (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
-  /\ rs1#CRne = (Val.cmpu (Mem.valid_pointer m) Cne v1 v2)
-  /\ rs1#CRhs = (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
-  /\ rs1#CRlo = (Val.cmpu (Mem.valid_pointer m) Clt v1 v2)
-  /\ rs1#CRhi = (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2)
-  /\ rs1#CRls = (Val.cmpu (Mem.valid_pointer m) Cle v1 v2)
-  /\ rs1#CRge = (Val.cmp Cge v1 v2)
-  /\ rs1#CRlt = (Val.cmp Clt v1 v2)
-  /\ rs1#CRgt = (Val.cmp Cgt v1 v2)
-  /\ rs1#CRle = (Val.cmp Cle v1 v2)
-  /\ forall r', data_preg r' = true -> rs1#r' = rs#r'.
+     rs1#CN = Val.negative (Val.sub v1 v2)
+  /\ rs1#CZ = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2
+  /\ rs1#CC = Val.cmpu (Mem.valid_pointer m) Cge v1 v2
+  /\ rs1#CV = Val.sub_overflow v1 v2.
 Proof.
-  intros. unfold rs1. intuition; try reflexivity.
-  unfold compare_int. Simpl. 
+  intros. unfold rs1. intuition.
+Qed.
+
+Lemma compare_int_inv:
+  forall rs v1 v2 m,
+  let rs1 := nextinstr (compare_int rs v1 v2 m) in
+  forall r', data_preg r' = true -> rs1#r' = rs#r'.
+Proof.
+  intros. unfold rs1, compare_int.
+  repeat Simplif. 
+Qed.
+
+Lemma int_signed_eq:
+  forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y).
+Proof.
+  intros. unfold Int.eq. unfold proj_sumbool. 
+  destruct (zeq (Int.unsigned x) (Int.unsigned y));
+  destruct (zeq (Int.signed x) (Int.signed y)); auto.
+  elim n. unfold Int.signed. rewrite e; auto.
+  elim n. apply Int.eqm_small_eq; auto with ints. 
+  eapply Int.eqm_trans. apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
+  rewrite e. apply Int.eqm_signed_unsigned. 
+Qed.
+
+Lemma int_not_lt:
+  forall x y, negb (Int.lt y x) = (Int.lt x y || Int.eq x y).
+Proof.
+  intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool.
+  destruct (zlt (Int.signed y) (Int.signed x)).
+  rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+  destruct (zeq (Int.signed x) (Int.signed y)). 
+  rewrite zlt_false. auto. omega. 
+  rewrite zlt_true. auto. omega.
+Qed.
+
+Lemma int_lt_not:
+  forall x y, Int.lt y x = negb (Int.lt x y) && negb (Int.eq x y).
+Proof.
+  intros. rewrite <- negb_orb. rewrite <- int_not_lt. rewrite negb_involutive. auto.
+Qed.
+
+Lemma int_not_ltu:
+  forall x y, negb (Int.ltu y x) = (Int.ltu x y || Int.eq x y).
+Proof.
+  intros. unfold Int.ltu, Int.eq.
+  destruct (zlt (Int.unsigned y) (Int.unsigned x)).
+  rewrite zlt_false. rewrite zeq_false. auto. omega. omega.
+  destruct (zeq (Int.unsigned x) (Int.unsigned y)). 
+  rewrite zlt_false. auto. omega. 
+  rewrite zlt_true. auto. omega.
+Qed.
+
+Lemma int_ltu_not:
+  forall x y, Int.ltu y x = negb (Int.ltu x y) && negb (Int.eq x y).
+Proof.
+  intros. rewrite <- negb_orb. rewrite <- int_not_ltu. rewrite negb_involutive. auto.
+Qed.
+
+Lemma cond_for_signed_cmp_correct:
+  forall c v1 v2 rs m b,
+  Val.cmp_bool c v1 v2 = Some b ->
+  eval_testcond (cond_for_signed_cmp c)
+                (nextinstr (compare_int rs v1 v2 m)) = Some b.
+Proof.
+  intros. generalize (compare_int_spec rs v1 v2 m).
+  set (rs' := nextinstr (compare_int rs v1 v2 m)).
+  intros [A [B [C D]]].
+  destruct v1; destruct v2; simpl in H; inv H.
+  unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+  simpl. unfold Val.cmp, Val.cmpu.
+  rewrite Int.lt_sub_overflow.
+  destruct c; simpl.
+  destruct (Int.eq i i0); auto.
+  destruct (Int.eq i i0); auto.
+  destruct (Int.lt i i0); auto.
+  rewrite int_not_lt. destruct (Int.lt i i0); simpl; destruct (Int.eq i i0); auto.
+  rewrite (int_lt_not i i0). destruct (Int.lt i i0); destruct (Int.eq i i0); reflexivity.
+  destruct (Int.lt i i0); reflexivity.
+Qed.
+
+Lemma cond_for_unsigned_cmp_correct:
+  forall c v1 v2 rs m b,
+  Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b ->
+  eval_testcond (cond_for_unsigned_cmp c)
+                (nextinstr (compare_int rs v1 v2 m)) = Some b.
+Proof.
+  intros. generalize (compare_int_spec rs v1 v2 m).
+  set (rs' := nextinstr (compare_int rs v1 v2 m)).
+  intros [A [B [C D]]].
+  unfold eval_testcond. rewrite B; rewrite C. unfold Val.cmpu, Val.cmp.
+  destruct v1; destruct v2; simpl in H; inv H.
+(* int int *)
+  destruct c; simpl; auto.
+  destruct (Int.eq i i0); reflexivity.
+  destruct (Int.eq i i0); auto.
+  destruct (Int.ltu i i0); auto.
+  rewrite (int_not_ltu i i0).  destruct (Int.ltu i i0); destruct (Int.eq i i0); auto.
+  rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
+  destruct (Int.ltu i i0); reflexivity.
+(* int ptr *)
+  destruct (Int.eq i Int.zero) eqn:?; try discriminate.
+  destruct c; simpl in *; inv H1.
+  rewrite Heqb1; reflexivity. 
+  rewrite Heqb1; reflexivity.
+(* ptr int *)
+  destruct (Int.eq i0 Int.zero) eqn:?; try discriminate.
+  destruct c; simpl in *; inv H1.
+  rewrite Heqb1; reflexivity. 
+  rewrite Heqb1; reflexivity.
+(* ptr ptr *)
+  simpl. 
+  fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
+  fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
+  destruct (eq_block b0 b1).
+  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) &&
+            Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1.
+  destruct c; simpl; auto.
+  destruct (Int.eq i i0); reflexivity.
+  destruct (Int.eq i i0); auto.
+  destruct (Int.ltu i i0); auto.
+  rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto.
+  rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
+  destruct (Int.ltu i i0); reflexivity.
+  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
+            Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+  destruct c; simpl in *; inv H1; reflexivity.
 Qed.
 
 Lemma compare_float_spec:
+  forall rs f1 f2,
+  let rs1 := nextinstr (compare_float rs (Vfloat f1) (Vfloat f2)) in
+     rs1#CN = Val.of_bool (Float.cmp Clt f1 f2)
+  /\ rs1#CZ = Val.of_bool (Float.cmp Ceq f1 f2)
+  /\ rs1#CC = Val.of_bool (negb (Float.cmp Clt f1 f2))
+  /\ rs1#CV = Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)).
+Proof.
+  intros. intuition.
+Qed.
+
+Lemma compare_float_inv:
   forall rs v1 v2,
-  let rs' := nextinstr (compare_float rs v1 v2) in
-     rs'#CReq = (Val.cmpf Ceq v1 v2)
-  /\ rs'#CRne = (Val.cmpf Cne v1 v2)
-  /\ rs'#CRmi = (Val.cmpf Clt v1 v2)              
-  /\ rs'#CRpl = (Val.notbool (Val.cmpf Clt v1 v2))
-  /\ rs'#CRhi = (Val.notbool (Val.cmpf Cle v1 v2))
-  /\ rs'#CRls = (Val.cmpf Cle v1 v2)              
-  /\ rs'#CRge = (Val.cmpf Cge v1 v2)              
-  /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2))
-  /\ rs'#CRgt = (Val.cmpf Cgt v1 v2)               
-  /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2))
-  /\ forall r', data_preg r' = true -> rs'#r' = rs#r'.
+  let rs1 := nextinstr (compare_float rs v1 v2) in
+  forall r', data_preg r' = true -> rs1#r' = rs#r'.
 Proof.
-  intros. unfold rs'. intuition; try reflexivity.
-  unfold compare_float. Simpl. 
+  intros. unfold rs1, compare_float.
+  assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r').
+  { repeat Simplif. }
+  destruct v1; destruct v2; auto.
+  repeat Simplif. 
+Qed.
+
+Lemma compare_float_nextpc:
+  forall rs v1 v2,
+  nextinstr (compare_float rs v1 v2) PC = Val.add (rs PC) Vone.
+Proof.
+  intros. unfold compare_float. destruct v1; destruct v2; reflexivity.
+Qed.
+
+Lemma cond_for_float_cmp_correct:
+  forall c n1 n2 rs,
+  eval_testcond (cond_for_float_cmp c)
+                (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))) =
+  Some(Float.cmp c n1 n2).
+Proof.
+  intros.
+  generalize (compare_float_spec rs n1 n2). 
+  set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))).
+  intros [A [B [C D]]].
+  unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+  destruct c; simpl.
+(* eq *)
+  destruct (Float.cmp Ceq n1 n2); auto.
+(* ne *)
+  rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto.
+(* lt *)
+  destruct (Float.cmp Clt n1 n2); auto.
+(* le *)
+  rewrite Float.cmp_le_lt_eq. 
+  destruct (Float.cmp Clt n1 n2); destruct (Float.cmp Ceq n1 n2); auto.
+(* gt *)
+  destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+  destruct (Float.cmp Clt n1 n2) eqn:LT;
+  destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+  exfalso; eapply Float.cmp_lt_gt_false; eauto.
+  exfalso; eapply Float.cmp_gt_eq_false; eauto.
+  exfalso; eapply Float.cmp_lt_gt_false; eauto.
+(* ge *)
+  rewrite Float.cmp_ge_gt_eq. 
+  destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+  destruct (Float.cmp Clt n1 n2) eqn:LT;
+  destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+  exfalso; eapply Float.cmp_lt_eq_false; eauto.
+  exfalso; eapply Float.cmp_lt_eq_false; eauto.
+  exfalso; eapply Float.cmp_lt_gt_false; eauto.
+Qed.
+
+Lemma cond_for_float_not_cmp_correct:
+  forall c n1 n2 rs,
+  eval_testcond (cond_for_float_not_cmp c)
+                (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2)))=
+  Some(negb(Float.cmp c n1 n2)).
+Proof.
+  intros.
+  generalize (compare_float_spec rs n1 n2).
+  set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))).
+  intros [A [B [C D]]].
+  unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D.
+  destruct c; simpl.
+(* eq *)
+  destruct (Float.cmp Ceq n1 n2); auto.
+(* ne *)
+  rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto.
+(* lt *)
+  destruct (Float.cmp Clt n1 n2); auto.
+(* le *)
+  rewrite Float.cmp_le_lt_eq. 
+  destruct (Float.cmp Clt n1 n2) eqn:LT; destruct (Float.cmp Ceq n1 n2) eqn:EQ; auto.
+(* gt *)
+  destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+  destruct (Float.cmp Clt n1 n2) eqn:LT;
+  destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+  exfalso; eapply Float.cmp_lt_gt_false; eauto.
+  exfalso; eapply Float.cmp_gt_eq_false; eauto.
+  exfalso; eapply Float.cmp_lt_gt_false; eauto.
+(* ge *)
+  rewrite Float.cmp_ge_gt_eq. 
+  destruct (Float.cmp Ceq n1 n2) eqn:EQ;
+  destruct (Float.cmp Clt n1 n2) eqn:LT;
+  destruct (Float.cmp Cgt n1 n2) eqn:GT; auto.
+  exfalso; eapply Float.cmp_lt_eq_false; eauto.
+  exfalso; eapply Float.cmp_lt_eq_false; eauto.
+  exfalso; eapply Float.cmp_lt_gt_false; eauto.
 Qed.
 
 Ltac ArgsInv :=
@@ -591,119 +795,92 @@ Lemma transl_cond_correct:
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ match eval_condition cond (map rs (map preg_of args)) m with
-     | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b
+     | Some b => eval_testcond (cond_for_cond cond) rs' = Some b
      | None => True
      end
   /\ forall r, data_preg r = true -> rs'#r = rs r.
 Proof.
   intros until c; intros TR. 
-  assert (MATCH: forall v ob,
-           v = Val.of_optbool ob ->
-           match ob with Some b => v = Val.of_bool b | None => True end).
-    intros. subst v. destruct ob; auto.  
-  assert (MATCH2: forall cmp v1 v2 v,
-           v = Val.cmpu (Mem.valid_pointer m) cmp v1 v2 ->
-           cmp = Ceq \/ cmp = Cne ->
-           match Val.cmp_bool cmp v1 v2 with
-           | Some b => v = Val.of_bool b
-           | None => True
-           end).
-     intros. destruct v1; simpl; auto; destruct v2; simpl; auto.
-     unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto.
-
   unfold transl_cond in TR; destruct cond; ArgsInv.
 - (* Ccomp *)
-  generalize (compare_int_spec rs (rs x) (rs x0) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  auto.
+  split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+  apply compare_int_inv. 
 - (* Ccompu *)
-  generalize (compare_int_spec rs (rs x) (rs x0) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  auto.
+  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+  apply compare_int_inv.
 - (* Ccompshift *)
-  generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  rewrite transl_shift_correct. 
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  auto.
+  split. rewrite transl_shift_correct.
+  destruct (Val.cmp_bool c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+  apply compare_int_inv.
 - (* Ccompushift *)
-  generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. apply exec_straight_one. simpl. eauto. auto.
-  rewrite transl_shift_correct. 
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  auto.
+  split. rewrite transl_shift_correct.
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+  apply compare_int_inv.
 - (* Ccompimm *)
   destruct (is_immed_arith i).
-  generalize (compare_int_spec rs (rs x) (Vint i) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
-  split. apply exec_straight_one. simpl. eauto. auto. 
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  auto.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+  apply compare_int_inv.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
-  generalize (compare_int_spec rs' (rs x) (Vint i) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
   rewrite Q. rewrite R; eauto with asmgen. auto.
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  intros. rewrite C; auto with asmgen.
+  split. rewrite <- R by (eauto with asmgen). 
+  destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto.
+  intros. rewrite compare_int_inv by auto. auto with asmgen. 
 - (* Ccompuimm *)
   destruct (is_immed_arith i).
-  generalize (compare_int_spec rs (rs x) (Vint i) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
-  split. apply exec_straight_one. simpl. eauto. auto. 
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  auto.
+  split. apply exec_straight_one. simpl. eauto. auto.
+  split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+  apply compare_int_inv.
   exploit (loadimm_correct IR14). intros [rs' [P [Q R]]].
-  generalize (compare_int_spec rs' (rs x) (Vint i) m).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
   split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl.
   rewrite Q. rewrite R; eauto with asmgen. auto.
-  split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto).
-  intros. rewrite C; auto with asmgen.
+  split. rewrite <- R by (eauto with asmgen). 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto.
+  intros. rewrite compare_int_inv by auto. auto with asmgen. 
 - (* Ccompf *)
-  generalize (compare_float_spec rs (rs x) (rs x0)).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
-  split. apply exec_straight_one. simpl. eauto. auto.
-  split. case c0; apply MATCH; assumption.
-  auto.
+  split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+  split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
+  destruct (rs x); try discriminate. destruct (rs x0); try discriminate.
+  simpl in CMP. inv CMP. apply cond_for_float_cmp_correct.
+  apply compare_float_inv.
 - (* Cnotcompf *)
-  generalize (compare_float_spec rs (rs x) (rs x0)).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
-  split. apply exec_straight_one. simpl. eauto. auto.
-  split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1.  
-  destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
-  auto.
+  split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+  split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto.
+  destruct (rs x); try discriminate. destruct (rs x0); try discriminate.
+  simpl in CMP. inv CMP.
+Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct.
+  exact I.
+  apply compare_float_inv.
 - (* Ccompfzero *)
-  generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
   econstructor.
-  split. apply exec_straight_one. simpl. eauto. auto.
-  split. case c0; apply MATCH; assumption.
-  auto.
-- (* Cnotcompf *)
-  generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)).
-  intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C).
+  split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+  split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto.
+  destruct (rs x); try discriminate.
+  simpl in CMP. inv CMP. apply cond_for_float_cmp_correct.
+  apply compare_float_inv.
+- (* Cnotcompfzero *)
   econstructor.
-  split. apply exec_straight_one. simpl. eauto. auto.
-  split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1.  
-  destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto.
-  auto.
+  split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc.
+  split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto.
+  destruct (rs x); try discriminate. simpl in CMP. inv CMP.
+Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct.
+  exact I.
+  apply compare_float_inv.
 Qed.
 
 (** Translation of arithmetic operations. *)
@@ -788,8 +965,7 @@ Proof.
   set (islt := Int.lt n Int.zero) in *.
   set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)).
   assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r').
-    generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m).
-    fold rs1. intros [A B]. intuition.
+  { apply compare_int_inv; auto. }
   exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)).
   intros [rs2 [EXEC2 [RES2 OTH2]]].
   set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))).
@@ -799,18 +975,19 @@ Proof.
   simpl. rewrite ARG1. auto. auto.
   eapply exec_straight_trans. eexact EXEC2.
   apply exec_straight_two with rs3 m.
-  simpl. rewrite OTH2; eauto with asmgen.
-    change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)).
-    unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt).
-    rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1. 
-    unfold rs3. case islt; reflexivity.
-    rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen.
-    auto.
-    unfold rs3. destruct islt; auto. auto. 
-    split. unfold rs4; Simpl. unfold rs3. destruct islt. 
-    Simpl. rewrite RES2. unfold rs1. Simpl.
-    Simpl. congruence.
-    intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. 
+  unfold exec_instr. 
+  assert (TC: eval_testcond TCge rs2 = Some (negb islt)).
+  { simpl. rewrite ! OTH2 by auto with asmgen. simpl. 
+    rewrite Int.lt_sub_overflow. fold islt. destruct islt; auto. }
+  rewrite TC. simpl. rewrite OTH2 by eauto with asmgen. rewrite OTH1. rewrite ARG1.
+  unfold rs3; destruct islt; reflexivity.
+  rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen.
+  reflexivity.
+  unfold rs3; destruct islt; reflexivity.
+  reflexivity.
+  split. unfold rs4; Simpl. unfold rs3. destruct islt. 
+  Simpl. rewrite RES2. unfold rs1. Simpl. Simpl. congruence.
+  intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. 
   (* intoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
 Transparent destroyed_by_op. 
@@ -848,25 +1025,22 @@ Proof.
   rewrite (ireg_of_eq _ _ EQ).
   exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
   set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))).
-  set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with
-             | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone
-             | _      => rs2#x <- Vundef
-             end)).
+  set (rs3 := nextinstr (match eval_testcond (cond_for_cond cmp) rs2 with
+                         | Some true => rs2 # x <- (Vint Int.one)
+                         | Some false => rs2
+                         | None => rs2 # x <- Vundef end)).
   exists rs3; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m.
   auto.
-  simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto.
-  auto. unfold rs3.  destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto.
-  split. unfold rs3. Simpl. 
-  replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)).
-  destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *.
-  rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero.  
-  rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl.
-  auto.
-  destruct cmp; reflexivity. 
+  simpl. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto.
+  auto. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto.
+  split. destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto.
+  unfold rs3.
+  change (eval_testcond (cond_for_cond cmp) rs2) with (eval_testcond (cond_for_cond cmp) rs1). rewrite B.
+  Simpl. destruct b. Simpl. unfold rs2. Simpl. 
   intros. transitivity (rs2 r). 
-  unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl.
-  unfold rs2. Simpl.
+  unfold rs3. Simpl. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; Simpl; auto.
+  unfold rs2. Simpl. 
 Qed.
 
 (** Translation of loads and stores. *)
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 3740c1f..d700326 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -93,18 +93,18 @@ let preg oc = function
   | _    -> assert false
 
 let condition_name = function
-  | CReq -> "eq"
-  | CRne -> "ne"
-  | CRhs -> "hs"
-  | CRlo -> "lo"
-  | CRmi -> "mi"
-  | CRpl -> "pl"
-  | CRhi -> "hi"
-  | CRls -> "ls"
-  | CRge -> "ge"
-  | CRlt -> "lt"
-  | CRgt -> "gt"
-  | CRle -> "le"
+  | TCeq -> "eq"
+  | TCne -> "ne"
+  | TChs -> "hs"
+  | TClo -> "lo"
+  | TCmi -> "mi"
+  | TCpl -> "pl"
+  | TChi -> "hi"
+  | TCls -> "ls"
+  | TCge -> "ge"
+  | TClt -> "lt"
+  | TCgt -> "gt"
+  | TCle -> "le"
 
 (* Names of sections *)
 
@@ -744,12 +744,6 @@ let rec print_instructions oc instrs =
       end;
       print_instructions oc il
 
-(* Base-2 log of a Caml integer *)
-
-let rec log2 n =
-  assert (n > 0);
-  if n = 1 then 0 else 1 + log2 (n lsr 1)
-
 let print_function oc name fn =
   Hashtbl.clear current_function_labels;
   reset_constants();
@@ -760,8 +754,8 @@ let print_function oc name fn =
     |   _    -> Section_text in
   section oc text;
   let alignment =
-    match !Clflags.option_falignfunctions with Some n -> log2 n | None -> 2 in
-  fprintf oc "	.align %d\n" alignment;
+    match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
+  fprintf oc "	.balign %d\n" alignment;
   if not (C2C.atom_is_static name) then
     fprintf oc "	.global	%a\n" print_symb name;
   fprintf oc "%a:\n" print_symb name;
@@ -815,11 +809,11 @@ let print_var oc name v =
         |  _  -> Section_data true
       and align =
         match C2C.atom_alignof name with
-        | Some a -> log2 a
-        | None -> 3 (* 8-alignment is a safe default *)
+        | Some a -> a
+        | None -> 8 (* 8-alignment is a safe default *)
       in
       section oc sec;
-      fprintf oc "	.align	%d\n" align;
+      fprintf oc "	.balign	%d\n" align;
       if not (C2C.atom_is_static name) then
         fprintf oc "	.global	%a\n" print_symb name;
       fprintf oc "%a:\n" print_symb name;