Expand 64-bit integer comparisons into 32-bit integer comparisons.

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

10 files changed, 506 insertions, 249 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 3963e76..6b36b4d 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -309,8 +309,8 @@ Definition eval_binop
   | Ocmp c => Some (Val.cmp c arg1 arg2)
   | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2)
   | Ocmpf c => Some (Val.cmpf c arg1 arg2)
-  | Ocmpl c => Some (Val.cmpl c arg1 arg2)
-  | Ocmplu c => Some (Val.cmplu c arg1 arg2)
+  | Ocmpl c => Val.cmpl c arg1 arg2
+  | Ocmplu c => Val.cmplu c arg1 arg2
   end.
 
 (** Evaluation of an expression: [eval_expr ge sp e m a v]
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 3538dda..c80f424 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -40,7 +40,7 @@ Inductive expr : Type :=
   | Evar : ident -> expr
   | Eop : operation -> exprlist -> expr
   | Eload : memory_chunk -> addressing -> exprlist -> expr
-  | Econdition : condition -> exprlist -> expr -> expr -> expr
+  | Econdition : condexpr -> expr -> expr -> expr
   | Elet : expr -> expr -> expr
   | Eletvar : nat -> expr
   | Ebuiltin : external_function -> exprlist -> expr
@@ -48,7 +48,12 @@ Inductive expr : Type :=
 
 with exprlist : Type :=
   | Enil: exprlist
-  | Econs: expr -> exprlist -> exprlist.
+  | Econs: expr -> exprlist -> exprlist
+
+with condexpr : Type :=
+  | CEcond : condition -> exprlist -> condexpr
+  | CEcondition : condexpr -> condexpr -> condexpr -> condexpr
+  | CElet: expr -> condexpr -> condexpr.
 
 Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope.
 
@@ -65,7 +70,7 @@ Inductive stmt : Type :=
   | Stailcall: signature -> expr + ident -> exprlist -> stmt
   | Sbuiltin : option ident -> external_function -> exprlist -> stmt
   | Sseq: stmt -> stmt -> stmt
-  | Sifthenelse: condition -> exprlist -> stmt -> stmt -> stmt
+  | Sifthenelse: condexpr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
@@ -161,11 +166,10 @@ Inductive eval_expr: letenv -> expr -> val -> Prop :=
       eval_addressing ge sp addr vl = Some vaddr ->
       Mem.loadv chunk m vaddr = Some v ->     
       eval_expr le (Eload chunk addr al) v
-  | eval_Econdition: forall le cond al b c vl vb v,
-      eval_exprlist le al vl ->
-      eval_condition cond vl m = Some vb ->
-      eval_expr le (if vb then b else c) v ->
-      eval_expr le (Econdition cond al b c) v
+  | eval_Econdition: forall le a b c va v,
+      eval_condexpr le a va ->
+      eval_expr le (if va then b else c) v ->
+      eval_expr le (Econdition a b c) v
   | eval_Elet: forall le a b v1 v2,
       eval_expr le a v1 ->
       eval_expr (v1 :: le) b v2 ->
@@ -190,10 +194,25 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
       eval_exprlist le Enil nil
   | eval_Econs: forall le a1 al v1 vl,
       eval_expr le a1 v1 -> eval_exprlist le al vl ->
-      eval_exprlist le (Econs a1 al) (v1 :: vl).
+      eval_exprlist le (Econs a1 al) (v1 :: vl)
+
+with eval_condexpr: letenv -> condexpr -> bool -> Prop :=
+  | eval_CEcond: forall le cond al vl vb,
+      eval_exprlist le al vl ->
+      eval_condition cond vl m = Some vb ->
+      eval_condexpr le (CEcond cond al) vb
+  | eval_CEcondition: forall le a b c va v,
+      eval_condexpr le a va ->
+      eval_condexpr le (if va then b else c) v ->
+      eval_condexpr le (CEcondition a b c) v
+  | eval_CElet: forall le a b v1 v2,
+      eval_expr le a v1 ->
+      eval_condexpr (v1 :: le) b v2 ->
+      eval_condexpr le (CElet a b) v2.
 
-Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
-  with eval_exprlist_ind2 := Minimality for eval_exprlist Sort Prop.
+Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop
+  with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop
+  with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop.
 
 Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
   | eval_eos_e: forall le e v,
@@ -232,7 +251,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
       | Some sk => Some sk
       | None => find_label lbl s2 k
       end
-  | Sifthenelse cond al s1 s2 =>
+  | Sifthenelse c s1 s2 =>
       match find_label lbl s1 k with
       | Some sk => Some sk
       | None => find_label lbl s2 k
@@ -302,10 +321,9 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
 
-  | step_ifthenelse: forall f cond al s1 s2 k sp e m vl b,
-      eval_exprlist sp e m nil al vl ->
-      eval_condition cond vl m = Some b ->
-      step (State f (Sifthenelse cond al s1 s2) k sp e m)
+  | step_ifthenelse: forall f c s1 s2 k sp e m b,
+      eval_condexpr sp e m nil c b ->
+      step (State f (Sifthenelse c s1 s2) k sp e m)
         E0 (State f (if b then s1 else s2) k sp e m)
 
   | step_loop: forall f s k sp e m,
@@ -382,7 +400,7 @@ Inductive final_state: state -> int -> Prop :=
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
-Hint Constructors eval_expr eval_exprlist: evalexpr.
+Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
 
 (** * Lifting of let-bound variables *)
 
@@ -396,8 +414,8 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
   | Evar id => Evar id
   | Eop op bl => Eop op (lift_exprlist p bl)
   | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl)
-  | Econdition cond al b c =>
-      Econdition cond (lift_exprlist p al) (lift_expr p b) (lift_expr p c)
+  | Econdition a b c =>
+      Econdition (lift_condexpr p a) (lift_expr p b) (lift_expr p c)
   | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c)
   | Eletvar n =>
       if le_gt_dec p n then Eletvar (S n) else Eletvar n
@@ -409,6 +427,13 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist :=
   match a with
   | Enil => Enil
   | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl)
+  end
+
+with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr :=
+  match a with
+  | CEcond c al => CEcond c (lift_exprlist p al)
+  | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c)
+  | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b)
   end.
 
 Definition lift (a: expr): expr := lift_expr O a.
@@ -458,22 +483,28 @@ Lemma eval_lift_expr:
   eval_expr ge sp e m le' (lift_expr p a) v.
 Proof.
   intros until w.
-  apply (eval_expr_ind2 ge sp e m
+  apply (eval_expr_ind3 ge sp e m
     (fun le a v =>
       forall p le', insert_lenv le p w le' ->
       eval_expr ge sp e m le' (lift_expr p a) v)
     (fun le al vl =>
       forall p le', insert_lenv le p w le' ->
-      eval_exprlist ge sp e m le' (lift_exprlist p al) vl));
+      eval_exprlist ge sp e m le' (lift_exprlist p al) vl)
+    (fun le a b =>
+      forall p le', insert_lenv le p w le' ->
+      eval_condexpr ge sp e m le' (lift_condexpr p a) b));
   simpl; intros; eauto with evalexpr.
 
-  eapply eval_Econdition; eauto. destruct vb; eauto.
+  eapply eval_Econdition; eauto. destruct va; eauto.
 
   eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto.
 
   case (le_gt_dec p n); intro. 
   apply eval_Eletvar. eapply insert_lenv_lookup2; eauto.
   apply eval_Eletvar. eapply insert_lenv_lookup1; eauto.
+
+  eapply eval_CEcondition; eauto. destruct va; eauto.
+  eapply eval_CElet; eauto. apply H2. constructor; auto.
 Qed.
 
 Lemma eval_lift:
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index f5e34e4..193702e 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -401,12 +401,10 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node)
       do rl <- alloc_regs map al;
       do no <- add_instr (Iload chunk addr rl rd nd);
          transl_exprlist map al rl no
-  | Econdition cond al b c =>
-      do rl <- alloc_regs map al;
+  | Econdition a b c =>
       do nfalse <- transl_expr map c rd nd;
       do ntrue  <- transl_expr map b rd nd;
-      do nt <- add_instr (Icond cond rl ntrue nfalse);
-         transl_exprlist map al rl nt
+         transl_condexpr map a ntrue nfalse
   | Elet b c =>
       do r  <- new_reg;
       do nc <- transl_expr (add_letvar map r) c rd nd;
@@ -435,6 +433,26 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
       do no <- transl_exprlist map bs rs nd; transl_expr map b r no
   | _, _ =>
       error (Errors.msg "RTLgen.transl_exprlist")
+  end
+
+(** Translation of a conditional expression.  Branches to [ntrue] or
+  to [nfalse] depending on the truth value of the expression. *)
+
+with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node)
+                     {struct a} : mon node :=
+  match a with
+  | CEcond c al =>
+      do rl <- alloc_regs map al;
+      do nt <- add_instr (Icond c rl ntrue nfalse);
+         transl_exprlist map al rl nt
+  | CEcondition a b c =>
+      do nc <- transl_condexpr map c ntrue nfalse;
+      do nb <- transl_condexpr map b ntrue nfalse;
+         transl_condexpr map a nb nc
+  | CElet b c =>
+      do r  <- new_reg;
+      do nc <- transl_condexpr (add_letvar map r) c ntrue nfalse;
+         transl_expr map b r nc
   end.
 
 (** Auxiliary for branch prediction.  When compiling an if/then/else
@@ -445,7 +463,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node)
   no impact on program correctness.  We delegate the choice to an
   external heuristic (written in OCaml), declared below.  *)
 
-Parameter more_likely: condition -> stmt -> stmt -> bool.
+Parameter more_likely: condexpr -> stmt -> stmt -> bool.
 
 (** Auxiliary for translating [Sswitch] statements. *)
 
@@ -545,18 +563,15 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
-  | Sifthenelse cond al strue sfalse =>
-      do rl <- alloc_regs map al;
-      if more_likely cond strue sfalse then
+  | Sifthenelse c strue sfalse =>
+      if more_likely c strue sfalse then
         do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
         do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
-        do nt <- add_instr (Icond cond rl ntrue nfalse);
-           transl_exprlist map al rl nt
+           transl_condexpr map c ntrue nfalse
       else
         do ntrue  <- transl_stmt map strue  nd nexits ngoto nret rret;
         do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret;
-        do nt <- add_instr (Icond cond rl ntrue nfalse);
-           transl_exprlist map al rl nt
+           transl_condexpr map c ntrue nfalse
   | Sloop sbody =>
       do n1 <- reserve_instr;
       do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret;
@@ -611,7 +626,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
                         {struct s} : labelmap * state :=
   match s with
   | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
-  | Sifthenelse cond al s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
+  | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms)
   | Sloop s1 => reserve_labels s1 ms
   | Sblock s1 => reserve_labels s1 ms
   | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms)
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 150de5a..7590102 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -30,8 +30,8 @@ let rec size_expr = function
   | Evar id -> 0
   | Eop(op, args) -> 1 + size_exprs args
   | Eload(chunk, addr, args) -> 1 + size_exprs args
-  | Econdition(cond, args, e1, e2) ->
-      1 + size_exprs args + max (size_expr e1) (size_expr e2)
+  | Econdition(ce, e1, e2) ->
+      1 + size_condexpr ce + max (size_expr e1) (size_expr e2)
   | Elet(e1, e2) -> size_expr e1 + size_expr e2
   | Eletvar n -> 0
   | Ebuiltin(ef, el) -> 2 + size_exprs el
@@ -41,6 +41,13 @@ and size_exprs = function
   | Enil -> 0
   | Econs(e1, el) -> size_expr e1 + size_exprs el
 
+and size_condexpr = function
+  | CEcond(c, args) -> size_exprs args
+  | CEcondition(c1, c2, c3) ->
+      1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3
+  | CElet(a, c) ->
+      size_expr a + size_condexpr c
+
 let rec length_exprs = function
   | Enil -> 0
   | Econs(e1, el) -> 1 + length_exprs el
@@ -59,8 +66,8 @@ let rec size_stmt = function
       3 + size_eos eos + size_exprs args + length_exprs args
   | Sbuiltin(optid, ef, args) -> 1 + size_exprs args
   | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2
-  | Sifthenelse(cond, args, s1, s2) ->
-      1 + size_exprs args + max (size_stmt s1) (size_stmt s2)
+  | Sifthenelse(ce, s1, s2) ->
+      size_condexpr ce + max (size_stmt s1) (size_stmt s2)
   | Sloop s -> 1 + 4 * size_stmt s
   | Sblock s -> size_stmt s
   | Sexit n -> 1
@@ -70,7 +77,7 @@ let rec size_stmt = function
   | Slabel(lbl, s) -> size_stmt s
   | Sgoto lbl -> 1
 
-let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = 
+let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = 
   size_stmt ifso > size_stmt ifnot
 
 (* Compiling a switch table into a decision tree *)
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index c3cae28..51f1f27 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -546,6 +546,19 @@ Definition transl_exprlist_prop
   /\ (forall r, In r pr -> rs'#r = rs#r)
   /\ Mem.extends m tm'.
 
+Definition transl_condexpr_prop 
+     (le: letenv) (a: condexpr) (v: bool) : Prop :=
+  forall tm cs f map pr ns ntrue nfalse rs
+    (MWF: map_wf map)
+    (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse)
+    (ME: match_env map e le rs)
+    (EXT: Mem.extends m tm),
+  exists rs', exists tm',
+     plus step tge (State cs f sp ns rs tm) E0 (State cs f sp (if v then ntrue else nfalse) rs' tm')
+  /\ match_env map e le rs'
+  /\ (forall r, In r pr -> rs'#r = rs#r)
+  /\ Mem.extends m tm'.
+
 (** The correctness of the translation is a huge induction over
   the Cminor evaluation derivation for the source program.  To keep
   the proof manageable, we put each case of the proof in a separate
@@ -639,25 +652,22 @@ Proof.
 Qed.
 
 Lemma transl_expr_Econdition_correct:
-  forall (le : letenv) (cond : condition) (al: exprlist) (ifso ifnot : expr)
-         (vl: list val) (vcond : bool) (v : val),
-  eval_exprlist ge sp e m le al vl ->
-  transl_exprlist_prop le al vl ->
-  eval_condition cond vl m = Some vcond ->
-  eval_expr ge sp e m le (if vcond then ifso else ifnot) v ->
-  transl_expr_prop le (if vcond then ifso else ifnot) v ->
-  transl_expr_prop le (Econdition cond al ifso ifnot) v.
+  forall (le : letenv) (a: condexpr) (ifso ifnot : expr)
+         (va : bool) (v : val),
+  eval_condexpr ge sp e m le a va ->
+  transl_condexpr_prop le a va ->
+  eval_expr ge sp e m le (if va then ifso else ifnot) v ->
+  transl_expr_prop le (if va then ifso else ifnot) v ->
+  transl_expr_prop le (Econdition a ifso ifnot) v.
 Proof.
-  intros; red; intros; inv TE. inv H14.
-  exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. 
-  assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst).
-    destruct vcond; auto.
-  exploit H3; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]].
+  intros; red; intros; inv TE.
+  exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. 
+  assert (tr_expr f.(fn_code) map pr (if va then ifso else ifnot) (if va then ntrue else nfalse) nd rd dst).
+    destruct va; auto.
+  exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]].
   exists rs2; exists tm2.
 (* Exec *)
-  split. eapply star_trans. eexact EX1.
-  eapply star_left. eapply exec_Icond. eauto. eapply eval_condition_lessdef; eauto. reflexivity. 
-  eexact EX2. reflexivity. traceEq.
+  split. eapply star_trans. apply plus_star. eexact EX1. eexact EX2. traceEq.
 (* Match-env *)
   split. assumption.
 (* Result value *)
@@ -829,14 +839,85 @@ Proof.
   auto.
 Qed.
 
+Lemma transl_condexpr_CEcond_correct:
+  forall le cond al vl vb,
+  eval_exprlist ge sp e m le al vl ->
+  transl_exprlist_prop le al vl ->
+  eval_condition cond vl m = Some vb ->
+  transl_condexpr_prop le (CEcond cond al) vb.
+Proof.
+  intros; red; intros. inv TE. 
+  exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]].
+  exists rs1; exists tm1.
+(* Exec *)
+  split. eapply plus_right. eexact EX1. eapply exec_Icond. eauto. 
+  eapply eval_condition_lessdef; eauto. auto. traceEq.
+(* Match-env *)
+  split. assumption.
+(* Other regs *)
+  split. assumption. 
+(* Mem *)
+  auto.
+Qed.
+
+Lemma transl_condexpr_CEcondition_correct:
+  forall le a b c va v,
+  eval_condexpr ge sp e m le a va ->
+  transl_condexpr_prop le a va ->
+  eval_condexpr ge sp e m le (if va then b else c) v ->
+  transl_condexpr_prop le (if va then b else c) v ->
+  transl_condexpr_prop le (CEcondition a b c) v.
+Proof.
+  intros; red; intros. inv TE. 
+  exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]].
+  assert (tr_condition (fn_code f) map pr (if va then b else c) (if va then n2 else n3) ntrue nfalse).
+    destruct va; auto.
+  exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [OTHER2 EXT2]]]]].
+  exists rs2; exists tm2.
+(* Exec *)
+  split. eapply plus_trans. eexact EX1. eexact EX2. traceEq.
+(* Match-env *)
+  split. assumption.
+(* Other regs *)
+  split. intros. rewrite OTHER2; auto. 
+(* Mem *)
+  auto.
+Qed.
+
+Lemma transl_condexpr_CElet_correct:
+  forall le a b v1 v2,
+  eval_expr ge sp e m le a v1 ->
+  transl_expr_prop le a v1 ->
+  eval_condexpr ge sp e m (v1 :: le) b v2 ->
+  transl_condexpr_prop (v1 :: le) b v2 ->
+  transl_condexpr_prop le (CElet a b) v2.
+Proof.
+  intros; red; intros. inv TE. 
+  exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]].
+  assert (map_wf (add_letvar map r)).
+    eapply add_letvar_wf; eauto. 
+  exploit H2; eauto. eapply match_env_bind_letvar; eauto. 
+  intros [rs2 [tm2 [EX2 [ME3 [OTHER2 EXT2]]]]].
+  exists rs2; exists tm2.
+(* Exec *)
+  split. eapply star_plus_trans. eexact EX1. eexact EX2. traceEq.
+(* Match-env *)
+  split. eapply match_env_unbind_letvar; eauto.
+(* Other regs *)
+  split. intros. rewrite OTHER2; auto. 
+(* Mem *)
+  auto.
+Qed.
+
 Theorem transl_expr_correct:
   forall le a v,
   eval_expr ge sp e m le a v ->
   transl_expr_prop le a v.
 Proof
-  (eval_expr_ind2 ge sp e m
+  (eval_expr_ind3 ge sp e m
      transl_expr_prop
      transl_exprlist_prop
+     transl_condexpr_prop
      transl_expr_Evar_correct
      transl_expr_Eop_correct
      transl_expr_Eload_correct
@@ -846,16 +927,20 @@ Proof
      transl_expr_Ebuiltin_correct
      transl_expr_Eexternal_correct
      transl_exprlist_Enil_correct
-     transl_exprlist_Econs_correct).
+     transl_exprlist_Econs_correct
+     transl_condexpr_CEcond_correct
+     transl_condexpr_CEcondition_correct
+     transl_condexpr_CElet_correct).
 
 Theorem transl_exprlist_correct:
   forall le a v,
   eval_exprlist ge sp e m le a v ->
   transl_exprlist_prop le a v.
 Proof
-  (eval_exprlist_ind2 ge sp e m
+  (eval_exprlist_ind3 ge sp e m
      transl_expr_prop
      transl_exprlist_prop
+     transl_condexpr_prop
      transl_expr_Evar_correct
      transl_expr_Eop_correct
      transl_expr_Eload_correct
@@ -865,7 +950,33 @@ Proof
      transl_expr_Ebuiltin_correct
      transl_expr_Eexternal_correct
      transl_exprlist_Enil_correct
-     transl_exprlist_Econs_correct).
+     transl_exprlist_Econs_correct
+     transl_condexpr_CEcond_correct
+     transl_condexpr_CEcondition_correct
+     transl_condexpr_CElet_correct).
+
+Theorem transl_condexpr_correct:
+  forall le a v,
+  eval_condexpr ge sp e m le a v ->
+  transl_condexpr_prop le a v.
+Proof
+  (eval_condexpr_ind3 ge sp e m
+     transl_expr_prop
+     transl_exprlist_prop
+     transl_condexpr_prop
+     transl_expr_Evar_correct
+     transl_expr_Eop_correct
+     transl_expr_Eload_correct
+     transl_expr_Econdition_correct
+     transl_expr_Elet_correct
+     transl_expr_Eletvar_correct
+     transl_expr_Ebuiltin_correct
+     transl_expr_Eexternal_correct
+     transl_exprlist_Enil_correct
+     transl_exprlist_Econs_correct
+     transl_condexpr_CEcond_correct
+     transl_condexpr_CEcondition_correct
+     transl_condexpr_CElet_correct).
 
 End CORRECTNESS_EXPR.
 
@@ -877,7 +988,7 @@ Fixpoint size_stmt (s: stmt) : nat :=
   match s with
   | Sskip => 0
   | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
-  | Sifthenelse cond el s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
+  | Sifthenelse c s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
   | Sloop s1 => (size_stmt s1 + 1)
   | Sblock s1 => (size_stmt s1 + 1)
   | Sexit n => 0
@@ -1206,11 +1317,10 @@ Proof.
   econstructor; eauto. econstructor; eauto. 
 
   (* ifthenelse *)
-  inv TS. inv H13.
-  exploit transl_exprlist_correct; eauto. intros [rs' [tm' [A [B [C [D E]]]]]].
+  inv TS. 
+  exploit transl_condexpr_correct; eauto. intros [rs' [tm' [A [B [C D]]]]].
   econstructor; split.
-  left. eapply plus_right. eexact A. eapply exec_Icond; eauto.
-  eapply eval_condition_lessdef; eauto. traceEq.
+  left. eexact A.
   destruct b; econstructor; eauto. 
 
   (* loop *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index d8d5dc8..c82c051 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -703,11 +703,11 @@ Inductive tr_expr (c: code):
       c!n1 = Some (Iload chunk addr rl rd nd) ->
       reg_map_ok map rd dst -> ~In rd pr ->
       tr_expr c map pr (Eload chunk addr al) ns nd rd dst
-  | tr_Econdition: forall map pr cond bl ifso ifnot ns nd rd ntrue nfalse dst,
-      tr_condition c map pr cond bl ns ntrue nfalse ->
+  | tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst,
+      tr_condition c map pr a ns ntrue nfalse ->
       tr_expr c map pr ifso ntrue nd rd dst ->
       tr_expr c map pr ifnot nfalse nd rd dst ->
-      tr_expr c map pr (Econdition cond bl ifso ifnot) ns nd rd dst
+      tr_expr c map pr (Econdition a ifso ifnot) ns nd rd dst
   | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst,
       ~reg_in_map map r ->
       tr_expr c map pr b1 ns n1 r None ->
@@ -730,17 +730,27 @@ Inductive tr_expr (c: code):
       tr_expr c map pr (Eexternal id sg al) ns nd rd dst
 
 
-(** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c],
+(** [tr_condition c map pr a ns ntrue nfalse rd] holds if the graph [c],
   starting at node [ns], contains instructions that compute the truth
-  value of the Cminor conditional expression [cond] and terminate
+  value of the Cminor conditional expression [a] and terminate
   on node [ntrue] if the condition holds and on node [nfalse] otherwise. *)
 
 with tr_condition (c: code): 
-       mapping -> list reg -> condition -> exprlist -> node -> node -> node -> Prop :=
+       mapping -> list reg -> condexpr -> node -> node -> node -> Prop :=
   | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl,
       tr_exprlist c map pr bl ns n1 rl ->
       c!n1 = Some (Icond cond rl ntrue nfalse) ->
-      tr_condition c map pr cond bl ns ntrue nfalse
+      tr_condition c map pr (CEcond cond bl) ns ntrue nfalse
+  | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3,
+      tr_condition c map pr a1 ns n2 n3 ->
+      tr_condition c map pr a2 n2 ntrue nfalse ->
+      tr_condition c map pr a3 n3 ntrue nfalse ->
+      tr_condition c map pr (CEcondition a1 a2 a3) ns ntrue nfalse
+  | tr_CElet: forall map pr a b ns ntrue nfalse r n1,
+      ~reg_in_map map r ->
+      tr_expr c map pr a ns n1 r None ->
+      tr_condition c (add_letvar map r) pr b n1 ntrue nfalse ->
+      tr_condition c map pr (CElet a b) ns ntrue nfalse
 
 (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c],
   between nodes [ns] and [nd], contains instructions that compute the values
@@ -840,11 +850,11 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_stmt c map s2 n nd nexits ngoto nret rret ->
      tr_stmt c map s1 ns n nexits ngoto nret rret ->
      tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret
-  | tr_Sifthenelse: forall cond al strue sfalse ns nd nexits ngoto nret rret ntrue nfalse,
+  | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse,
      tr_stmt c map strue ntrue nd nexits ngoto nret rret ->
      tr_stmt c map sfalse nfalse nd nexits ngoto nret rret ->
-     tr_condition c map nil cond al ns ntrue nfalse ->
-     tr_stmt c map (Sifthenelse cond al strue sfalse) ns nd nexits ngoto nret rret
+     tr_condition c map nil a ns ntrue nfalse ->
+     tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret
   | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend,
      tr_stmt c map sbody nloop nend nexits ngoto nret rret ->
      c!ns = Some(Inop nloop) ->
@@ -914,9 +924,9 @@ Lemma tr_expr_incr:
   tr_expr s2.(st_code) map pr a ns nd rd dst
 with tr_condition_incr:
   forall s1 s2, state_incr s1 s2 ->
-  forall map pr cond al ns ntrue nfalse,
-  tr_condition s1.(st_code) map pr cond al ns ntrue nfalse ->
-  tr_condition s2.(st_code) map pr cond al ns ntrue nfalse
+  forall map pr a ns ntrue nfalse,
+  tr_condition s1.(st_code) map pr a ns ntrue nfalse ->
+  tr_condition s2.(st_code) map pr a ns ntrue nfalse
 with tr_exprlist_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map pr al ns nd rl,
@@ -962,7 +972,14 @@ with transl_exprlist_charact:
      (OK: target_regs_ok map pr al rl)
      (VALID1: regs_valid pr s)
      (VALID2: regs_valid rl s),
-   tr_exprlist s'.(st_code) map pr al ns nd rl.
+   tr_exprlist s'.(st_code) map pr al ns nd rl
+
+with transl_condexpr_charact:
+  forall a map ntrue nfalse s ns s' pr INCR
+     (TR: transl_condexpr map a ntrue nfalse s = OK ns s' INCR)
+     (WF: map_valid map s)
+     (VALID: regs_valid pr s),
+   tr_condition s'.(st_code) map pr a ns ntrue nfalse.
 
 Proof.
   induction a; intros; try (monadInv TR); saturateTrans.
@@ -981,12 +998,12 @@ Proof.
   eapply transl_exprlist_charact; eauto with rtlg. 
   (* Econdition *)
   inv OK.
-  econstructor; eauto with rtlg.
-  econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. 
-  apply tr_expr_incr with s2; auto. 
-  eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
+  econstructor.
+  eauto with rtlg.
   apply tr_expr_incr with s1; auto. 
   eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
+  apply tr_expr_incr with s0; auto. 
+  eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto.
   (* Elet *)
   inv OK.
   econstructor. eapply new_reg_not_in_map; eauto with rtlg.  
@@ -1031,6 +1048,22 @@ Proof.
   eapply transl_exprlist_charact; eauto with rtlg.
   apply regs_valid_cons. apply VALID2. auto with coqlib. auto. 
   red; intros; apply VALID2; auto with coqlib.
+
+(* Conditional expressions *)
+  induction a; intros; try (monadInv TR); saturateTrans.
+
+  (* CEcond *)
+  econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg.
+  (* CEcondition *)
+  econstructor; eauto with rtlg. 
+  apply tr_condition_incr with s1; eauto with rtlg.
+  apply tr_condition_incr with s0; eauto with rtlg.
+  (* CElet *)
+  econstructor; eauto with rtlg.
+  eapply transl_expr_charact; eauto with rtlg. 
+  apply tr_condition_incr with s1; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
+  apply add_letvar_valid; eauto with rtlg. 
 Qed.
 
 (** A variant of [transl_expr_charact], for use when the destination
@@ -1056,10 +1089,10 @@ Proof.
   eapply transl_exprlist_charact; eauto with rtlg. 
   (* Econdition *)
   econstructor; eauto with rtlg.
-  econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. 
-  apply tr_expr_incr with s2; auto. 
-  eapply IHa1; eauto 2 with rtlg. 
+  eapply transl_condexpr_charact; eauto with rtlg.
   apply tr_expr_incr with s1; auto. 
+  eapply IHa1; eauto 2 with rtlg. 
+  apply tr_expr_incr with s0; auto. 
   eapply IHa2; eauto 2 with rtlg.
   (* Elet *)
   econstructor. eapply new_reg_not_in_map; eauto with rtlg.  
@@ -1227,21 +1260,19 @@ Proof.
   eapply IHstmt2; eauto with rtlg.
   eapply IHstmt1; eauto with rtlg.
   (* Sifthenelse *)
-  destruct (more_likely c stmt1 stmt2); monadInv EQ0.
+  destruct (more_likely c stmt1 stmt2); monadInv TR.
   econstructor.
-  apply tr_stmt_incr with s2; auto. 
+  apply tr_stmt_incr with s1; auto. 
   eapply IHstmt1; eauto with rtlg.
-  apply tr_stmt_incr with s1; auto.
+  apply tr_stmt_incr with s0; auto.
   eapply IHstmt2; eauto with rtlg.
-  econstructor; eauto with rtlg. 
-  eapply transl_exprlist_charact; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
   econstructor.
-  apply tr_stmt_incr with s1; auto. 
+  apply tr_stmt_incr with s0; auto. 
   eapply IHstmt1; eauto with rtlg.
-  apply tr_stmt_incr with s2; auto.
+  apply tr_stmt_incr with s1; auto.
   eapply IHstmt2; eauto with rtlg.
-  econstructor; eauto with rtlg. 
-  eapply transl_exprlist_charact; eauto with rtlg.
+  eapply transl_condexpr_charact; eauto with rtlg.
   (* Sloop *)
   econstructor. 
   apply tr_stmt_incr with s1; auto. 
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index 8eb32c3..aad9d60 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -41,9 +41,7 @@ Record helper_functions : Type := mk_helper_functions {
   i64_umod: ident;                      (**r unsigned remainder *)
   i64_shl: ident;                       (**r shift left *)
   i64_shr: ident;                       (**r shift right unsigned *)
-  i64_sar: ident;                       (**r shift right signed *)
-  i64_scmp: ident;                      (**r signed comparison *)
-  i64_ucmp: ident                       (**r unsigned comparison *)
+  i64_sar: ident                        (**r shift right signed *)
 }.
 
 Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong).
@@ -51,7 +49,6 @@ Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat).
 Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong).
 Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong).
 Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong).
-Definition sig_ll_i := mksignature (Tlong :: Tlong :: nil) (Some Tint).
 Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong).
 
 Section SELECT.
@@ -291,6 +288,12 @@ Definition cmpl_eq_zero (e: expr) :=
 Definition cmpl_ne_zero (e: expr) :=
   splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)).
 
+Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
+    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
+               (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
+               (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))).
+
 Definition cmplu (c: comparison) (e1 e2: expr) :=
   match c with
   | Ceq =>
@@ -301,15 +304,23 @@ Definition cmplu (c: comparison) (e1 e2: expr) :=
       if is_longconst_zero e2
       then cmpl_ne_zero e1
       else cmpl_ne_zero (xorl e1 e2)
-  | _ =>
-      comp c (Eexternal hf.(i64_ucmp) sig_ll_i (e1 ::: e2 ::: Enil))
-             (Eop (Ointconst Int.zero) Enil)
+  | Clt =>
+      cmplu_gen Clt Clt e1 e2
+  | Cle =>
+      cmplu_gen Clt Cle e1 e2
+  | Cgt =>
+      cmplu_gen Cgt Cgt e1 e2
+  | Cge =>
+      cmplu_gen Cgt Cge e1 e2
   end.
 
+Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
+    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
+               (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
+               (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))).
+
 Definition cmpl (c: comparison) (e1 e2: expr) :=
-  let default := 
-    comp c (Eexternal hf.(i64_scmp) sig_ll_i (e1 ::: e2 ::: Enil))
-           (Eop (Ointconst Int.zero) Enil) in
   match c with
   | Ceq =>
       if is_longconst_zero e2
@@ -322,13 +333,15 @@ Definition cmpl (c: comparison) (e1 e2: expr) :=
   | Clt =>
       if is_longconst_zero e2
       then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil)
-      else default
+      else cmpl_gen Clt Clt e1 e2
+  | Cle =>
+      cmpl_gen Clt Cle e1 e2
+  | Cgt =>
+      cmpl_gen Cgt Cgt e1 e2
   | Cge =>
       if is_longconst_zero e2
       then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil)
-      else default
-  | _ =>
-      default
+      else cmpl_gen Cgt Cge e1 e2
   end.
 
 End SELECT.
@@ -359,10 +372,7 @@ Definition get_helpers (ge: Cminor.genv): res helper_functions :=
   do i64_shl <- get_helper ge "__i64_shl" sig_li_l ;
   do i64_shr <- get_helper ge "__i64_shr" sig_li_l ;
   do i64_sar <- get_helper ge "__i64_sar" sig_li_l ;
-  do i64_scmp <- get_helper ge "__i64_scmp" sig_ll_i ;
-  do i64_ucmp <- get_helper ge "__i64_ucmp" sig_ll_i ;
   OK (mk_helper_functions
      i64_dtos i64_dtou i64_stod i64_utod
      i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod
-     i64_shl i64_shr i64_sar
-     i64_scmp i64_ucmp).
+     i64_shl i64_shr i64_sar).
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index aca05bf..3eeeeb5 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -61,11 +61,7 @@ Definition i64_helpers_correct (hf: helper_functions) : Prop :=
   /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z)
   /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y))
   /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y))
-  /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y))
-  /\(forall c x y, exists z, helper_implements hf.(i64_scmp) sig_ll_i (x::y::nil) z
-                          /\ Val.cmpl c x y = Val.cmp c z Vzero)
-  /\(forall c x y, exists z, helper_implements hf.(i64_ucmp) sig_ll_i (x::y::nil) z
-                          /\ Val.cmplu c x y = Val.cmp c z Vzero).
+  /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)).
 
 End HELPERS.
 
@@ -180,6 +176,22 @@ Proof.
   destruct v; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
 Qed.
 
+Lemma eval_splitlong_strict:
+  forall le a f va v,
+  eval_expr ge sp e m le a (Vlong va) ->
+  (forall le a1 a2,
+     eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) ->
+     eval_expr ge sp e m le a2 (Vint (Int64.loword va)) ->
+     eval_expr ge sp e m le (f a1 a2) v) ->
+  eval_expr ge sp e m le (splitlong a f) v.
+Proof.
+  intros until v. 
+  unfold splitlong. case (splitlong_match a); intros.
+- InvEval. destruct v1; simpl in H; try discriminate. destruct v0; inv H. 
+  apply H0. rewrite Int64.hi_ofwords; auto. rewrite Int64.lo_ofwords; auto.
+- EvalOp. apply H0; EvalOp.
+Qed.
+
 Lemma eval_splitlong2:
   forall le a b f va vb sem,
   (forall le a1 a2 b1 b2 x1 x2 y1 y2,
@@ -198,7 +210,7 @@ Lemma eval_splitlong2:
   exists v, eval_expr ge sp e m le (splitlong2 a b f) v /\ Val.lessdef (sem va vb) v.
 Proof.
   intros until sem; intros EXEC UNDEF.
-  unfold splitlong2. case (splitlong2_match a); intros.
+  unfold splitlong2. case (splitlong2_match a b); intros.
 - InvEval. subst va vb.
   exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]].
   exists v; split; auto.
@@ -240,6 +252,35 @@ Proof.
   erewrite B; simpl; eauto. rewrite ! Int64.ofwords_recompose; auto.
 Qed.
 
+Lemma eval_splitlong2_strict:
+  forall le a b f va vb v,
+  eval_expr ge sp e m le a (Vlong va) ->
+  eval_expr ge sp e m le b (Vlong vb) ->
+  (forall le a1 a2 b1 b2,
+     eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) ->
+     eval_expr ge sp e m le a2 (Vint (Int64.loword va)) ->
+     eval_expr ge sp e m le b1 (Vint (Int64.hiword vb)) ->
+     eval_expr ge sp e m le b2 (Vint (Int64.loword vb)) ->
+     eval_expr ge sp e m le (f a1 a2 b1 b2) v) ->
+  eval_expr ge sp e m le (splitlong2 a b f) v.
+Proof.
+  assert (INV: forall v1 v2 n,
+    Val.longofwords v1 v2 = Vlong n -> v1 = Vint(Int64.hiword n) /\ v2 = Vint(Int64.loword n)).
+  {
+    intros. destruct v1; simpl in H; try discriminate. destruct v2; inv H.
+    rewrite Int64.hi_ofwords; rewrite Int64.lo_ofwords; auto.
+  }
+  intros until v. 
+  unfold splitlong2. case (splitlong2_match a b); intros.
+- InvEval. exploit INV. eexact H. intros [EQ1 EQ2]. exploit INV. eexact H0. intros [EQ3 EQ4]. 
+  subst. auto.
+- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. 
+  econstructor. eauto. apply H1; EvalOp. 
+- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. 
+  econstructor. eauto. apply H1; EvalOp.
+- EvalOp. apply H1; EvalOp.
+Qed.
+
 Lemma is_longconst_sound:
   forall le a x n,
   is_longconst a = Some n ->
@@ -891,35 +932,49 @@ Proof.
 Qed.
 
 Lemma eval_cmpl_eq_zero:
-  unary_constructor_sound cmpl_eq_zero (fun v => Val.cmpl Ceq v (Vlong Int64.zero)).
+  forall le a x,
+  eval_expr ge sp e m le a (Vlong x) ->
+  eval_expr ge sp e m le (cmpl_eq_zero a) (Val.of_bool (Int64.eq x Int64.zero)).
 Proof.
-  red; intros. unfold cmpl_eq_zero. 
-  apply eval_splitlong with (sem := fun x => Val.cmpl Ceq x (Vlong Int64.zero)); auto.
-- intros. 
-  exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]].
+  intros. unfold cmpl_eq_zero. 
+  eapply eval_splitlong_strict; eauto. intros.
+  exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1.
   exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
-  instantiate (1 := Ceq). intros [v2 [A2 B2]].
-  exists v2; split. auto. intros; subst. 
-  simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2.
-  unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. 
-  destruct (Int.eq (Int.or p q)); inv B2; auto.
-- destruct x; auto.
+  instantiate (1 := Ceq). intros [v2 [A2 B2]]. 
+  unfold Val.cmp in B2; simpl in B2. 
+  rewrite <- decompose_cmpl_eq_zero in B2. 
+  rewrite Int64.ofwords_recompose in B2. 
+  destruct (Int64.eq x Int64.zero); inv B2; auto.
 Qed.
 
 Lemma eval_cmpl_ne_zero:
-  unary_constructor_sound cmpl_ne_zero (fun v => Val.cmpl Cne v (Vlong Int64.zero)).
+  forall le a x,
+  eval_expr ge sp e m le a (Vlong x) ->
+  eval_expr ge sp e m le (cmpl_ne_zero a) (Val.of_bool (negb (Int64.eq x Int64.zero))).
 Proof.
-  red; intros. unfold cmpl_eq_zero. 
-  apply eval_splitlong with (sem := fun x => Val.cmpl Cne x (Vlong Int64.zero)); auto.
-- intros. 
-  exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]].
+  intros. unfold cmpl_ne_zero. 
+  eapply eval_splitlong_strict; eauto. intros.
+  exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1.
   exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
-  instantiate (1 := Cne). intros [v2 [A2 B2]].
-  exists v2; split. auto. intros; subst. 
-  simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2.
-  unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. 
-  destruct (Int.eq (Int.or p q)); inv B2; auto.
-- destruct x; auto.
+  instantiate (1 := Cne). intros [v2 [A2 B2]]. 
+  unfold Val.cmp in B2; simpl in B2. 
+  rewrite <- decompose_cmpl_eq_zero in B2. 
+  rewrite Int64.ofwords_recompose in B2. 
+  destruct (negb (Int64.eq x Int64.zero)); inv B2; auto.
+Qed.
+
+Lemma eval_cmplu_gen:
+  forall ch cl a b le x y,
+  eval_expr ge sp e m le a (Vlong x) ->
+  eval_expr ge sp e m le b (Vlong y) ->
+  eval_expr ge sp e m le (cmplu_gen ch cl a b)
+    (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y)
+                  then Int.cmpu cl (Int64.loword x) (Int64.loword y)
+                  else Int.cmpu ch (Int64.hiword x) (Int64.hiword y))).
+Proof.
+  intros. unfold cmplu_gen. eapply eval_splitlong2_strict; eauto. intros.
+  econstructor. econstructor. EvalOp. simpl. eauto. 
+  destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp.
 Qed.
 
 Remark int64_eq_xor:
@@ -933,44 +988,57 @@ Proof.
   auto.
 Qed.
 
-Theorem eval_cmplu: forall c, binary_constructor_sound (cmplu hf c) (Val.cmplu c).
+Theorem eval_cmplu:
+  forall c le a x b y v, 
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.cmplu c x y = Some v ->
+  eval_expr ge sp e m le (cmplu c a b) v.
 Proof.
-  intros; red; intros. unfold cmplu. 
-  set (default := comp c (Eexternal (i64_ucmp hf) sig_ll_i (a ::: b ::: Enil))
-                         (Eop (Ointconst Int.zero) Enil)).
-  assert (DEFAULT:
-    exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmplu c x y) v).
-  {
-    assert (HELP: exists z, helper_implements ge hf.(i64_ucmp) sig_ll_i (x::y::nil) z
-                            /\ Val.cmplu c x y = Val.cmp c z Vzero)
-    by UseHelper.
-    destruct HELP as [z [A B]].
-    exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. 
-    instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. 
-    instantiate (1 := c). fold Vzero. intros [v [C D]].
-    econstructor; split; eauto. congruence.
-  }
-  destruct c; auto.
+  intros. unfold Val.cmplu in H1.
+  destruct x; simpl in H1; try discriminate. destruct y; inv H1. 
+  rename i into x. rename i0 into y.
+  destruct c; simpl.
 - (* Ceq *)
   destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0.
++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
   apply eval_cmpl_eq_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]].
-  exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]].
-  exists v'; split; auto.
-  eapply Val.lessdef_trans; [idtac|eexact D]. 
-  destruct x; auto. destruct y; auto. simpl in B; inv B. 
-  unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto.
++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
+  rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.  
 - (* Cne *)
   destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0.
++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
   apply eval_cmpl_ne_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]].
-  exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]].
-  exists v'; split; auto.
-  eapply Val.lessdef_trans; [idtac|eexact D]. 
-  destruct x; auto. destruct y; auto. simpl in B; inv B. 
-  unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto.
++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B.
+  rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.  
+- (* Clt *)
+  exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl.
+  rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto.
+- (* Cle *)
+  exploit (eval_cmplu_gen Clt Cle). eexact H. eexact H0. intros. 
+  rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
+  rewrite Int64.decompose_leu. auto. 
+- (* Cgt *)
+  exploit (eval_cmplu_gen Cgt Cgt). eexact H. eexact H0. simpl.
+  rewrite Int.eq_sym. rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto.
+- (* Cge *)
+  exploit (eval_cmplu_gen Cgt Cge). eexact H. eexact H0. intros. 
+  rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
+  rewrite Int64.decompose_leu. rewrite Int.eq_sym. auto.
+Qed.
+
+Lemma eval_cmpl_gen:
+  forall ch cl a b le x y,
+  eval_expr ge sp e m le a (Vlong x) ->
+  eval_expr ge sp e m le b (Vlong y) ->
+  eval_expr ge sp e m le (cmpl_gen ch cl a b)
+    (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y)
+                  then Int.cmpu cl (Int64.loword x) (Int64.loword y)
+                  else Int.cmp ch (Int64.hiword x) (Int64.hiword y))).
+Proof.
+  intros. unfold cmpl_gen. eapply eval_splitlong2_strict; eauto. intros.
+  econstructor. econstructor. EvalOp. simpl. eauto. 
+  destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp.
 Qed.
 
 Remark decompose_cmpl_lt_zero:
@@ -991,72 +1059,61 @@ Proof.
   vm_compute. intuition congruence.
 Qed.
 
-Theorem eval_cmpl: forall c, binary_constructor_sound (cmpl hf c) (Val.cmpl c).
+Theorem eval_cmpl:
+  forall c le a x b y v, 
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.cmpl c x y = Some v ->
+  eval_expr ge sp e m le (cmpl c a b) v.
 Proof.
-  intros; red; intros. unfold cmpl. 
-  set (default := comp c (Eexternal (i64_scmp hf) sig_ll_i (a ::: b ::: Enil))
-                         (Eop (Ointconst Int.zero) Enil)).
-  assert (DEFAULT:
-    exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmpl c x y) v).
-  {
-    assert (HELP: exists z, helper_implements ge hf.(i64_scmp) sig_ll_i (x::y::nil) z
-                            /\ Val.cmpl c x y = Val.cmp c z Vzero)
-    by UseHelper.
-    destruct HELP as [z [A B]].
-    exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. 
-    instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. 
-    instantiate (1 := c). fold Vzero. intros [v [C D]].
-    econstructor; split; eauto. congruence.
-  }
-  destruct c; auto.
+  intros. unfold Val.cmpl in H1.
+  destruct x; simpl in H1; try discriminate. destruct y; inv H1. 
+  rename i into x. rename i0 into y.
+  destruct c; simpl.
 - (* Ceq *)
   destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0.
++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
   apply eval_cmpl_eq_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]].
-  exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]].
-  exists v'; split; auto.
-  eapply Val.lessdef_trans; [idtac|eexact D]. 
-  destruct x; auto. destruct y; auto. simpl in B; inv B. 
-  unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto.
++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
+  rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto.
 - (* Cne *)
   destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0.
++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
   apply eval_cmpl_ne_zero; auto.
-+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]].
-  exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]].
-  exists v'; split; auto.
-  eapply Val.lessdef_trans; [idtac|eexact D]. 
-  destruct x; auto. destruct y; auto. simpl in B; inv B. 
-  unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto.
++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B.
+  rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto.
 - (* Clt *)
   destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0.
-  exploit eval_highlong. eexact H. intros [v1 [A1 B1]].
++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
+  exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1. inv B1. 
   exploit eval_comp. eexact A1. 
   instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
   instantiate (1 := Clt). intros [v2 [A2 B2]].
-  econstructor; split. eauto. 
-  destruct x; simpl in *; auto. inv B1.
-  unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2.
-  unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp.
-  rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero.
-  auto. 
-+ apply DEFAULT.
+  unfold Val.cmp in B2. simpl in B2.
+  rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero.
+  destruct (Int.lt (Int64.hiword x) Int.zero); inv B2; auto.
++ exploit (eval_cmpl_gen Clt Clt). eexact H. eexact H0. simpl.
+  rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto.
+- (* Cle *)
+  exploit (eval_cmpl_gen Clt Cle). eexact H. eexact H0. intros. 
+  rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
+  rewrite Int64.decompose_le. auto. 
+- (* Cgt *)
+  exploit (eval_cmpl_gen Cgt Cgt). eexact H. eexact H0. simpl.
+  rewrite Int.eq_sym. rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto.
 - (* Cge *)
   destruct (is_longconst_zero b) eqn:LC.
-+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0.
-  exploit eval_highlong. eexact H. intros [v1 [A1 B1]].
++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0.
+  exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1; inv B1.
   exploit eval_comp. eexact A1. 
   instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp.
   instantiate (1 := Cge). intros [v2 [A2 B2]].
-  econstructor; split. eauto. 
-  destruct x; simpl in *; auto. inv B1.
-  unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2.
-  unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp.
-  rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero.
-  auto. 
-+ apply DEFAULT.
+  unfold Val.cmp in B2; simpl in B2. 
+  rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero.
+  destruct (negb (Int.lt (Int64.hiword x) Int.zero)); inv B2; auto.
++ exploit (eval_cmpl_gen Cgt Cge). eexact H. eexact H0. intros. 
+  rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y).
+  rewrite Int64.decompose_le. rewrite Int.eq_sym. auto.
 Qed.
 
 End CMCONSTR.
diff --git a/backend/Selection.v b/backend/Selection.v
index 7964feb..edc63cd 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -37,10 +37,12 @@ Open Local Scope cminorsel_scope.
 
 (** Conversion of conditions *)
 
-Function condition_of_expr (e: expr) : condition * exprlist :=
+Function condexpr_of_expr (e: expr) : condexpr :=
   match e with
-  | Eop (Ocmp c) el => (c, el)
-  | _ => (Ccompuimm Cne Int.zero, e ::: Enil)
+  | Eop (Ocmp c) el => CEcond c el
+  | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c)
+  | Elet a b => CElet a (condexpr_of_expr b)
+  | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil)
   end.
 
 (** Conversion of loads and stores *)
@@ -133,8 +135,8 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Ocmp c => comp c arg1 arg2
   | Cminor.Ocmpu c => compu c arg1 arg2
   | Cminor.Ocmpf c => compf c arg1 arg2
-  | Cminor.Ocmpl c => cmpl hf c arg1 arg2
-  | Cminor.Ocmplu c => cmplu hf c arg1 arg2
+  | Cminor.Ocmpl c => cmpl c arg1 arg2
+  | Cminor.Ocmplu c => cmplu c arg1 arg2
   end.
 
 (** Conversion from Cminor expression to Cminorsel expressions *)
@@ -205,8 +207,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt :=
       end
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2)
   | Cminor.Sifthenelse e ifso ifnot =>
-      let (cond, args) := condition_of_expr (sel_expr e) in
-      Sifthenelse cond args (sel_stmt ge ifso) (sel_stmt ge ifnot)
+      Sifthenelse (condexpr_of_expr (sel_expr e))
+                  (sel_stmt ge ifso) (sel_stmt ge ifnot)
   | Cminor.Sloop body => Sloop (sel_stmt ge body)
   | Cminor.Sblock body => Sblock (sel_stmt ge body)
   | Cminor.Sexit n => Sexit n
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 525a29d..93a5c51 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -117,8 +117,6 @@ Proof.
   repeat (match goal with [ H: _ /\ _ |- _ /\ _ ] => destruct H; split end);
   intros; try (eapply helper_implements_preserved; eauto);
   try (eapply builtin_implements_preserved; eauto).
-  exploit H14; eauto. intros [z [A B]]. exists z; split; eauto. eapply helper_implements_preserved; eauto.
-  exploit H15; eauto. intros [z [A B]]. exists z; split; eauto. eapply helper_implements_preserved; eauto.
 Qed.
 
 Section CMCONSTR.
@@ -127,22 +125,22 @@ Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
-Lemma eval_condition_of_expr:
-  forall le a v b,
+Lemma eval_condexpr_of_expr:
+  forall a le v b,
   eval_expr tge sp e m le a v ->
   Val.bool_of_val v b ->
-  match condition_of_expr a with (cond, args) =>
-    exists vl,
-    eval_exprlist tge sp e m le args vl /\
-    eval_condition cond vl m = Some b
-  end.
+  eval_condexpr tge sp e m le (condexpr_of_expr a) b.
 Proof.
-  intros until a. functional induction (condition_of_expr a); intros.
+  intros until a. functional induction (condexpr_of_expr a); intros.
 (* compare *)
-  inv H. exists vl; split; auto.
+  inv H. econstructor; eauto. 
   simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto.
+(* condition *)
+  inv H. econstructor; eauto. destruct va; eauto.
+(* let *)
+  inv H. econstructor; eauto.
 (* default *)
-  exists (v :: nil); split. constructor. auto. constructor.
+  econstructor. constructor. eauto. constructor. 
   simpl. inv H0. auto. auto. 
 Qed.
 
@@ -248,8 +246,8 @@ Proof.
   apply eval_comp; auto.
   apply eval_compu; auto.
   apply eval_compf; auto.
-  apply eval_cmpl; auto.
-  apply eval_cmplu; auto.
+  exists v; split; auto. eapply eval_cmpl; eauto.
+  exists v; split; auto. eapply eval_cmplu; eauto.
 Qed.
 
 End CMCONSTR.
@@ -495,7 +493,6 @@ Proof.
   destruct (find_label lbl (sel_stmt hf ge s1) (Kseq (sel_stmt hf ge s2) k')) as [[sy ky] | ];
   intuition. apply IHs2; auto.
 (* ifthenelse *)
-  destruct (condition_of_expr (sel_expr hf e)) as [cond args]. simpl.
   exploit (IHs1 k); eauto. 
   destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ];
   destruct (find_label lbl (sel_stmt hf ge s1) k') as [[sy ky] | ];
@@ -594,11 +591,8 @@ Proof.
   (* Sifthenelse *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   assert (Val.bool_of_val v' b). inv B. auto. inv H0.
-  exploit eval_condition_of_expr; eauto.
-  destruct (condition_of_expr (sel_expr hf a)) as [cond args].
-  intros [vl' [C D]].
   left; exists (State (sel_function hf ge f) (if b then sel_stmt hf ge s1 else sel_stmt hf ge s2) k' sp e' m'); split.
-  econstructor; eauto. 
+  econstructor; eauto. eapply eval_condexpr_of_expr; eauto. 
   constructor; auto. destruct b; auto.
   (* Sloop *)
   left; econstructor; split. constructor. constructor; auto. constructor; auto.