Ccompu expansion

8 files changed, 223 insertions, 178 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 8d1e3a5c..17a2d3bb 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -731,10 +731,19 @@ Definition transl_op
       do rs1 <- ireg_of a1;
       do rs2 <- ireg_of a2;
       OK (apply_bin_r0_r0r0 optR0 (Psltw rd) rs1 rs2 :: k)
+  | OEsltuw optR0, a1 :: a2 :: nil =>
+      do rd <- ireg_of res;
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0 optR0 (Psltuw rd) rs1 rs2 :: k)
   | OEsltiw n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
       OK (Psltiw rd rs n :: k)
+  | OEsltiuw n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltiuw rd rs n :: k)
   | OExoriw n, a1 :: nil =>
       do rd <- ireg_of res;
       do rs <- ireg_of a1;
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 8aa3d3b2..369b8280 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -295,6 +295,7 @@ Opaque Int.eq.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
+- destruct optR0 as [[]|]; simpl; TailNoLabel.
 Qed.
 
 Remark indexed_memory_access_label:
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 06b33592..6c722798 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -964,190 +964,183 @@ Proof.
 Opaque Int.eq.
   intros until c; intros TR EV.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
-- (* move *)
-  destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl.
-- (* intconst *)
-  exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* longconst *)
-  exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* floatconst *)
-  destruct (Float.eq_dec n Float.zero).
-+ subst n. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-- (* singleconst *)
-  destruct (Float32.eq_dec n Float32.zero).
-+ subst n. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-- (* addrsymbol *)
-  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
-  exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
-  intros (rs2 & A & B & C).
-  exists rs2; split. 
-  apply exec_straight_step with rs1 m; auto.
-  split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
-  rewrite Genv.shift_symbol_address.
-  replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
-  exact B.
-  intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
-+ TranslOpSimpl.
-- (* stackoffset *)
-  exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
-  exists rs'; split; eauto. auto with asmgen.
-- (* cast8signed *)
-  econstructor; split.
+  (* move *)
+  { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. }
+  (* intconst *)
+  { exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* longconst *)
+  { exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* floatconst *)
+  { destruct (Float.eq_dec n Float.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* singleconst *)
+  { destruct (Float32.eq_dec n Float32.zero).
+    + subst n. econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. 
+    + econstructor; split. 
+      apply exec_straight_one. simpl; eauto. auto.
+      split; intros; Simpl. }
+  (* addrsymbol *)
+  { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+    + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
+      exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
+      intros (rs2 & A & B & C).
+      exists rs2; split. 
+      apply exec_straight_step with rs1 m; auto.
+      split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
+      rewrite Genv.shift_symbol_address.
+      replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
+      exact B.
+      intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
+    + TranslOpSimpl. }
+  (* stackoffset *)
+  { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
+  exists rs'; split; eauto. auto with asmgen. }
+  (* cast8signed *)
+  { econstructor; split.
   eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
   split; intros; Simpl.
   assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
   destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
-- (* cast16signed *)
-  econstructor; split.
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* cast16signed *)
+  { econstructor; split.
   eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto.
   split; intros; Simpl.
   assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
   destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. 
-  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
-- (* addimm *)
-  exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
+  apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. }
+  (* addimm *)
+  { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. 
-- (* andimm *)
-  exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* orimm *)
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
   exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen.
+  { intros (rs' & A & B & C).
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* xorimm *)
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* shrximm *)
-  destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
-  {
-  exploit Val.shrx_shr_3; eauto. intros E; subst v.
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-  * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  }
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-  * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  
-- (* longofintu *)
-  econstructor; split.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrximm *)
+  { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
+    {
+    exploit Val.shrx_shr_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+    * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* longofintu *)
+  { econstructor; split.
   eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
   split; intros; Simpl. destruct (rs x0); auto. simpl. 
   assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
   rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
-  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto.
-- (* addlimm *)
-  exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
+  rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. }
+  (* addlimm *)
+  { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. 
-- (* andimm *)
-  exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* andimm *)
+  { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* orimm *)
-  exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* orimm *)
+  { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* xorimm *)
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* xorimm *)
+  { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* shrxlimm *)
-  destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
-  {
-   exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-
-  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  }
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ destruct (Int.eq n Int.one).
-  * econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    eapply exec_straight_step. simpl; reflexivity. auto.
-    apply exec_straight_one. simpl; reflexivity. auto.
-    split; intros; Simpl.
-
-  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
-    econstructor; split.
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    eapply exec_straight_step. simpl; reflexivity. auto. 
-    apply exec_straight_one. simpl; reflexivity. auto. 
-    split; intros; Simpl.
-  
-- (* cond *)
-  exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. eauto with asmgen.
-- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
+  exists rs'; split; eauto. rewrite B; auto with asmgen. }
+  (* shrxlimm *)
+  { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
+    {
+     exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl.
+    }
+    destruct (Int.eq n Int.zero).
+  + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+    split; intros; Simpl. 
+  + destruct (Int.eq n Int.one).
+    * econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      eapply exec_straight_step. simpl; reflexivity. auto.
+      apply exec_straight_one. simpl; reflexivity. auto.
+      split; intros; Simpl.
+
+    * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+      econstructor; split.
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      eapply exec_straight_step. simpl; reflexivity. auto. 
+      apply exec_straight_one. simpl; reflexivity. auto. 
+      split; intros; Simpl. }
+  (* cond *)
+  { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
+  exists rs'; split. eexact A. eauto with asmgen. }
+  (* Expanded instructions from RTL *)
+  1-4: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
   econstructor; split; try apply exec_straight_one; simpl; eauto;
   split; intros; Simpl.
-- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
   econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl.
-- destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
-  econstructor; split; try apply exec_straight_one; simpl; eauto;
-  split; intros; Simpl.
-- econstructor; split; try apply exec_straight_one; simpl; eauto;
   split; intros; Simpl. rewrite Int.add_commut. auto.
 Qed.
 
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 15a418fd..4d587b12 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -87,6 +87,15 @@ let expanse_condimm_int32s cmp a1 n dest succ k =
   | _   -> reg := !reg + 1;
            loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k)
 
+let cond_int32u_reg cmp a1 a2 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k
+  | Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k
+  | Clt -> Iop (OEsltuw None, [a1;a2], dest, succ) :: k
+  | Cle -> Iop (OEsltuw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltuw None, [a2;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltuw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
 let rec write_tree exp n code' =
   match exp with
   | (Iop (_,_,_,succ)) as inst :: k ->
@@ -130,7 +139,7 @@ let expanse (sb: superblock) code =
   Array.iter (fun n ->
     let inst = get_some @@ PTree.get n code in
     match inst with
-    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
+    | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> (
       Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;
       Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;
       Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);
@@ -139,20 +148,20 @@ let expanse (sb: superblock) code =
       print_instruction stderr (0,inst);
       debug "[EXPANSION] With:\n";
       let start_node = Camlcoq.P.of_int (!node + 1) in
+      let exp = cond_int32u_reg c a1 a2 dest succ [] in
+      code' := write_tree (List.rev exp) start_node code';
+      let first = Inop (n2pi()) in
+      code' := PTree.set n first !code';
+      generate_head_order n start_node new_order)
+    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
+      let start_node = Camlcoq.P.of_int (!node + 1) in
       let exp = expanse_condimm_int32s c a1 imm dest succ [] in
       code' := write_tree (List.rev exp) start_node code';
       let first = Inop (n2pi()) in
       code' := PTree.set n first !code';
-      generate_head_order n start_node new_order;
+      generate_head_order n start_node new_order)
       (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
       (*entry := n2p()*)
-    (*| Icond (cond,args,ifso,ifnot,info) -> (code' :=
-        match cond, args with
-        | Ccompimm (c, imm), a1 :: nil ->
-            expanse_condimm_int32s cond a1 imm info ifso ifnot
-            PTree.set n (Icond (cond,args,ifso,ifnot,info)) !code'
-        | (_, _) -> !code'*)
-        (*PTree.set node*))
     | _ -> new_order := !new_order @ [n]
   ) sb.instructions;
   sb.instructions <- Array.of_list !new_order;
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index da406d8a..9fd79de4 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -90,7 +90,9 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEseqw _ => op2 (default nv)
   | OEsnew _ => op2 (default nv)
   | OEsltw _ => op2 (default nv)
+  | OEsltuw _ => op2 (default nv)
   | OEsltiw n => op1 (default nv)
+  | OEsltiuw n => op1 (default nv)
   | OExoriw n => op1 (bitwise nv)
   | OEluiw n => op1 (default nv)
   | OEaddiwr0 n => op1 (modarith nv)
diff --git a/riscV/Op.v b/riscV/Op.v
index c55479ff..4de168cc 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -156,7 +156,9 @@ Inductive operation : Type :=
   | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
   | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
   | OEsltw (optR0: option bool)                  (**r set-less-than *)
+  | OEsltuw (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
+  | OEsltiuw (n: int)                             (**r set-less-than unsigned immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
   | OEluiw (n: int)                              (**r load upper-immediate *)
   | OEaddiwr0 (n: int).                          (**r add immediate *)
@@ -338,7 +340,9 @@ Definition eval_operation
   | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
   | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
   | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32)
+  | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32)
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
+  | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
   | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12)))
   | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
@@ -501,7 +505,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEseqw _ => (Tint :: Tint :: nil, Tint)
   | OEsnew _ => (Tint :: Tint :: nil, Tint)
   | OEsltw _ => (Tint :: Tint :: nil, Tint)
+  | OEsltuw _ => (Tint :: Tint :: nil, Tint)
   | OEsltiw _ => (Tint :: nil, Tint)
+  | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
   | OEluiw _ => (nil, Tint)
   | OEaddiwr0 _ => (nil, Tint)
@@ -718,8 +724,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   destruct Val.cmpu_bool... all: destruct b...
 - destruct optR0 as [[]|]; simpl; unfold Val.cmp;
   destruct Val.cmp_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+  destruct Val.cmpu_bool... all: destruct b...
 - unfold Val.cmp; destruct Val.cmp_bool...
   all: destruct b...
+- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
 - destruct v0...
 - trivial.
 - trivial.
@@ -915,6 +924,8 @@ Definition op_depends_on_memory (op: operation) : bool :=
   | Ocmp cmp => cond_depends_on_memory cmp
   | OEseqw _ => negb Archi.ptr64
   | OEsnew _ => negb Archi.ptr64
+  | OEsltiuw _ => negb Archi.ptr64
+  | OEsltuw _ => negb Archi.ptr64
   | _ => false
   end.
 
@@ -940,8 +951,8 @@ Proof.
   f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
   all: intros; repeat (destruct args; auto);
        unfold Val.cmpu, Val.cmpu_bool;
-       destruct optR0 as [[]|]; simpl;
-       destruct v, v0; simpl; auto;
+       try destruct optR0 as [[]|]; simpl;
+       destruct v; try destruct v0; simpl; auto;
        apply negb_false_iff in H; try rewrite H; auto.
 Qed.
 
@@ -1104,7 +1115,20 @@ Proof.
   eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
 Qed.
 
-Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0 optR0,
+Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0,
+  Val.inject f v v' ->
+  Val.inject f v0 v'0 ->
+  Val.inject f (Val.cmpu (Mem.valid_pointer m1) c v v0)
+  (Val.cmpu (Mem.valid_pointer m2) c v' v'0).
+Proof.
+  intros until v'0. intros HV1 HV2.
+  unfold Val.cmpu; 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto.
+  exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
+  intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+Qed.
+
+Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR0,
   Val.inject f v v' ->
   Val.inject f v0 v'0 ->
   Val.inject f (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32)
@@ -1329,12 +1353,14 @@ Proof.
     destruct b; simpl; constructor.
     simpl; constructor.
 
-  - apply eval_cmpu_bool_inj; auto.
-  - apply eval_cmpu_bool_inj; auto.
+  - apply eval_cmpu_bool_inj_opt; auto.
+  - apply eval_cmpu_bool_inj_opt; auto.
   - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
     inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto;
     try apply Val.inject_int.
+  - apply eval_cmpu_bool_inj_opt; auto.
   - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
+  - apply eval_cmpu_bool_inj; auto.
   - inv H4; simpl; auto.
 Qed.
 
@@ -1593,4 +1619,4 @@ Definition builtin_arg_ok
   match ba with
   | (BA _ | BA_splitlong (BA _) (BA _)) => true
   | _ => builtin_arg_ok_1 ba c
-  end.  
+  end.
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 7492b01c..c1d65b4c 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -164,7 +164,9 @@ let print_operation reg pp = function
   | OEseqw optR0, [r1;r2] -> fprintf pp "OEseqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
   | OEsnew optR0, [r1;r2] -> fprintf pp "OEsnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
   | OEsltw optR0, [r1;r2] -> fprintf pp "OEsltw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | OEsltuw optR0, [r1;r2] -> fprintf pp "OEsltuw"; (get_optR0_s Clt reg pp r1 r2 optR0)
   | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n)
+  | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEluiw n, [] -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
   | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n)
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index ec4492ff..4c1f4625 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -149,7 +149,9 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32)
   | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32)
   | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32)
+  | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32)
   | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
+  | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
   | OExoriw n, v1::nil => xor v1 (I n)
   | OEluiw n, nil => I (Int.shl n (Int.repr 12))
   | OEaddiwr0 n, nil => add (I n) zero32
@@ -218,7 +220,7 @@ Proof.
 Qed.
 
 Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m,
-  c = Ceq \/ c = Cne ->
+  c = Ceq \/ c = Cne \/ c = Clt->
   vmatch bc a1 b1 ->
   vmatch bc a0 b0 ->
   vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32)
@@ -253,9 +255,10 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   
-  1,2: apply eval_cmpu_sound; auto.
+  1,2,4: apply eval_cmpu_sound; auto.
   apply eval_cmp_sound; auto.
   unfold Val.cmp; apply of_optbool_sound; eauto with va.
+  unfold Val.cmpu; apply of_optbool_sound; eauto with va.
   unfold zero32; simpl. eauto with va.
 Qed.