Ccomp for long

8 files changed, 408 insertions, 52 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 17a2d3bb..f702d11a 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -347,7 +347,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
+  (* TODO | Ccomp c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_cond_int32s c rd r1 r2 k)
   | Ccompu c, a1 :: a2 :: nil =>
@@ -364,13 +364,13 @@ Definition transl_cond_op
       OK (transl_cond_int64s c rd r1 r2 k)
   | Ccomplu c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (transl_cond_int64u c rd r1 r2 k)
+     OK (transl_cond_int64u c rd r1 r2 k)
   | Ccomplimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (transl_condimm_int64s c rd r1 n k)
   | Ccompluimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (transl_condimm_int64u c rd r1 n k)
+     OK (transl_condimm_int64u c rd r1 n k)*)
   | Ccompf c, f1 :: f2 :: nil =>
       do r1 <- freg_of f1; do r2 <- freg_of f2;
       let (insn, normal) := transl_cond_float c rd r1 r2 in
@@ -754,6 +754,47 @@ Definition transl_op
   | OEaddiwr0 n, nil =>
       do rd <- ireg_of res;
       OK (Paddiw rd X0 n :: k)
+  | OEseql 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 (Pseql rd) rs1 rs2 :: k)
+  | OEsnel 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 (Psnel rd) rs1 rs2 :: k)
+  | OEsltl 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 (Psltl rd) rs1 rs2 :: k)
+  | OEsltul 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 (Psltul rd) rs1 rs2 :: k)
+  | OEsltil n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltil rd rs n :: k)
+  | OEsltiul n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Psltiul rd rs n :: k)
+  | OExoril n, a1 :: nil =>
+      do rd <- ireg_of res;
+      do rs <- ireg_of a1;
+      OK (Pxoril rd rs n :: k)
+  | OEluil n, nil =>
+      do rd <- ireg_of res;
+      OK (Pluil rd n :: k)
+  | OEaddilr0 n, nil =>
+      do rd <- ireg_of res;
+      OK (Paddil rd X0 n :: k)
+  | OEloadli n, nil =>
+      do rd <- ireg_of res;
+      OK (Ploadli rd n :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 369b8280..63ceed0d 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -219,7 +219,7 @@ Remark transl_cond_op_label:
   transl_cond_op cond r args k = OK c -> tail_nolabel k c.
 Proof.
   intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
+  (* TODO - destruct c0; simpl; TailNoLabel.
 - destruct c0; simpl; TailNoLabel. 
 - unfold transl_condimm_int32s.
   destruct (Int.eq n Int.zero).
@@ -238,7 +238,7 @@ Proof.
   try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]).
   apply opimm32_label; intros; exact I.
 - destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel. 
+     - destruct c0; simpl; TailNoLabel.
 - unfold transl_condimm_int64s.
   destruct (Int64.eq n Int64.zero).
 + destruct c0; simpl; TailNoLabel.
@@ -254,7 +254,7 @@ Proof.
 + destruct c0; simpl; TailNoLabel.
 + destruct c0; simpl; 
   try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]).
-  apply opimm64_label; intros; exact I.
+     apply opimm64_label; intros; exact I.*)
 - destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2.
   apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 
   destruct normal; TailNoLabel.
@@ -296,6 +296,10 @@ Opaque Int.eq.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
 - destruct optR0 as [[]|]; simpl; TailNoLabel.
+- 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 6c722798..ee203da4 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -844,7 +844,7 @@ Proof.
   { destruct ob as [[]|]; reflexivity. }
   intros until m; intros TR.
   destruct cond; simpl in TR; ArgsInv.
-+ (* cmp *)
+(* TODO + (* cmp *)
   exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
 + (* cmpu *)
   exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
@@ -858,7 +858,7 @@ Proof.
   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
 + (* cmplu *)
   exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
+   exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
 + (* cmplimm *)
   exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
   intros (rs' & A & B & C).
@@ -866,7 +866,7 @@ Proof.
 + (* cmpluimm *)
   exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
   intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
+   exists rs'; repeat split; eauto. rewrite MKTOT; eauto.*)
 + (* cmpf *)
   destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
   fold (Val.cmpf c0 (rs x) (rs x0)).
@@ -1137,11 +1137,13 @@ Opaque Int.eq.
   { 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;
+  5: econstructor; split; try apply exec_straight_one; simpl; eauto;
+  split; intros; Simpl; rewrite Int.add_commut; auto.
+  9: econstructor; split; try apply exec_straight_one; simpl; eauto;
+  split; intros; Simpl; rewrite Int64.add_commut; auto.
+  all: 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.
 
 (** Memory accesses *)
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 4d587b12..c3f2cb3f 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,7 +18,7 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
-open PrintRTL
+(*open PrintRTL*)
 open! Integers
 
 let reg = ref 1
@@ -28,7 +28,7 @@ let r2p () = Camlcoq.P.of_int !reg
 let n2p () = Camlcoq.P.of_int !node
 let n2pi () = node := !node + 1; n2p()
 
-type immt = Xori | Slti
+type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
 let load_hilo32 dest hi lo succ k =
   if Int.eq lo Int.zero then
@@ -36,15 +36,32 @@ let load_hilo32 dest hi lo succ k =
   else (
       Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)
 
+let load_hilo64 dest hi lo succ k =
+  if Int64.eq lo Int64.zero then
+    Iop (OEluil hi, [], dest, succ) :: k
+  else (
+      Iop (OEluil hi, [], dest, n2pi()) :: (Iop (Oaddlimm lo, [dest], dest, succ)) :: k)
+
 let loadimm32 dest n succ k =
   match make_immed32 n with
   | Imm32_single imm ->
       Iop (OEaddiwr0 imm, [], dest, succ) :: k
   | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k
 
+let loadimm64 dest n succ k =
+  match make_immed64 n with
+  | Imm64_single imm ->
+      Iop (OEaddilr0 imm, [], dest, succ) :: k
+  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k
+  | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
+
 let get_opimm imm = function
-  | Xori -> OExoriw imm
-  | Slti -> OEsltiw imm
+  | Xoriw -> OExoriw imm
+  | Sltiw -> OEsltiw imm
+  | Sltiuw -> OEsltiuw imm
+  | Xoril -> OExoril imm
+  | Sltil -> OEsltil imm
+  | Sltiul -> OEsltiul imm
 
 let opimm32 a1 dest n succ k op opimm =
   match make_immed32 n with
@@ -54,8 +71,23 @@ let opimm32 a1 dest n succ k op opimm =
       reg := !reg + 1;
       load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
 
-let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xori
-let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Slti
+let opimm64 a1 dest n succ k op opimm =
+  match make_immed64 n with
+  | Imm64_single imm ->
+      Iop (get_opimm imm opimm, [a1], dest, succ) :: k
+  | Imm64_pair (hi, lo) ->
+      reg := !reg + 1;
+      load_hilo64 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
+  | Imm64_large imm  ->
+      reg := !reg + 1;
+      Iop (OEloadli imm, [], r2p(), n2pi()) :: Iop (op, [a1;r2p()], dest, succ) :: k
+
+let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw
+let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw
+let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw
+let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
+let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil
+let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
 
 let cond_int32s_x0 cmp a1 dest succ k =
   match cmp with
@@ -75,6 +107,60 @@ let cond_int32s_reg cmp a1 a2 dest succ k =
   | Cgt -> Iop (OEsltw None, [a2;a1], dest, succ) :: k
   | Cge -> Iop (OEsltw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
 
+let cond_int32u_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltuw (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltuw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltuw (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltuw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], 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 cond_int64s_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltl (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltl (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltl (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltl (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int64s_reg cmp a1 a2 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k
+  | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k
+  | Clt -> Iop (OEsltl None, [a1;a2], dest, succ) :: k
+  | Cle -> Iop (OEsltl None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltl None, [a2;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltl None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int64u_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltul (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltul (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltul (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltul (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int64u_reg cmp a1 a2 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k
+  | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k
+  | Clt -> Iop (OEsltul None, [a1;a2], dest, succ) :: k
+  | Cle -> Iop (OEsltul None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltul None, [a2;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltul None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
 let expanse_condimm_int32s cmp a1 n dest succ k =
   if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k else
   match cmp with
@@ -87,22 +173,40 @@ 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 =
+let expanse_condimm_int32u cmp a1 n dest succ k =
+  if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k else
   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
+  | Clt -> sltuimm32 a1 dest n succ k
+  | _   -> reg := !reg + 1;
+           loadimm32 (r2p()) n (n2pi()) (cond_int32u_reg cmp a1 (r2p()) dest succ k)
+
+let expanse_condimm_int64s cmp a1 n dest succ k =
+  if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k else
+  match cmp with
+  | Ceq | Cne ->
+      reg := !reg + 1;
+      xorimm64 a1 (r2p()) n (n2pi()) (cond_int64s_x0 cmp (r2p()) dest succ k)
+  | Clt -> sltimm64 a1 dest n succ k
+  | Cle -> if Int64.eq n (Int64.repr Int64.max_signed)
+           then loadimm32 dest Int.one succ k
+            else sltimm64 a1 dest (Int64.add n Int64.one) succ k
+  | _   -> reg := !reg + 1;
+           loadimm64 (r2p()) n (n2pi()) (cond_int64s_reg cmp a1 (r2p()) dest succ k)
+ 
+let expanse_condimm_int64u cmp a1 n dest succ k =
+  if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k else
+  match cmp with
+  | Clt -> sltuimm64 a1 dest n succ k
+  | _   -> reg := !reg + 1;
+           loadimm64 (r2p()) n (n2pi()) (cond_int64u_reg cmp a1 (r2p()) dest succ k)
 
 let rec write_tree exp n code' =
   match exp with
   | (Iop (_,_,_,succ)) as inst :: k ->
-      print_instruction stderr (0,inst);
-      Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);
+      (*print_instruction stderr (0,inst);*)
+      (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*)
       code' := PTree.set n inst !code';
-      Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);
+      (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*)
       write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code'
   | _ -> !code'
 
@@ -135,34 +239,61 @@ let generate_head_order n start_node new_order =
 let expanse (sb: superblock) code =
   debug_flag := true;
   let new_order = ref [] in
+  let exp = ref [] in
+  let was_exp = ref false in
   let code' = ref code in
   Array.iter (fun n ->
+    was_exp := false;
     let inst = get_some @@ PTree.get n code in
+    let start_node = Camlcoq.P.of_int (!node + 1) in (
     match inst with
+    | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccomp\n";
+      exp := cond_int32s_reg c a1 a2 dest succ [];
+      was_exp := true)
     | 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);
-      Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);
-      debug "[EXPANSION] Replace this:\n";
-      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)
+      Printf.eprintf "Ccompu\n";
+      exp := cond_int32u_reg c a1 a2 dest succ [];
+      was_exp := true)
     | 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';
+      Printf.eprintf "Ccompimm\n";
+      exp := expanse_condimm_int32s c a1 imm dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccompuimm\n";
+      exp := expanse_condimm_int32u c a1 imm dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccompl\n";
+      exp := cond_int64s_reg c a1 a2 dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccomplu\n";
+      exp := cond_int64u_reg c a1 a2 dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> (
+      (*Printf.eprintf "Ccomplimm\n";*)
+      (*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);*)
+      (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*)
+      (*debug "[EXPANSION] Replace this:\n";*)
+      (*print_instruction stderr (0,inst);*)
+      (*debug "[EXPANSION] With:\n";*)
+      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
+      (*entry := n2p()*)
+      exp := expanse_condimm_int64s c a1 imm dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccompluimm\n";
+      exp := expanse_condimm_int64u c a1 imm dest succ [];
+      was_exp := true)
+    | _ -> new_order := !new_order @ [n]);
+    if !was_exp then (
+      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)
-      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
-      (*entry := n2p()*)
-    | _ -> new_order := !new_order @ [n]
   ) sb.instructions;
   sb.instructions <- Array.of_list !new_order;
   (*print_arrayp sb.instructions;*)
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 9fd79de4..67940c47 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -96,6 +96,16 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OExoriw n => op1 (bitwise nv)
   | OEluiw n => op1 (default nv)
   | OEaddiwr0 n => op1 (modarith nv)
+  | OEseql _ => op2 (default nv)
+  | OEsnel _ => op2 (default nv)
+  | OEsltl _ => op2 (default nv)
+  | OEsltul _ => op2 (default nv)
+  | OEsltil n => op1 (default nv)
+  | OEsltiul n => op1 (default nv)
+  | OExoril n => op1 (default nv)
+  | OEluil n => op1 (default nv)
+  | OEaddilr0 n => op1 (modarith nv)
+  | OEloadli n => op1 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -165,6 +175,7 @@ Proof.
 - apply shruimm_sound; auto.
 - apply xor_sound; auto with na.
 - auto with na.
+- auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/riscV/Op.v b/riscV/Op.v
index 4de168cc..ae38f361 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -158,10 +158,20 @@ Inductive operation : Type :=
   | 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 *)
+  | 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 *)
+  | OEaddiwr0 (n: int)                           (**r add immediate *)
+  | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
+  | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
+  | OEsltl (optR0: option bool)                  (**r set-less-than *)
+  | OEsltul (optR0: option bool)                 (**r set-less-than unsigned *)
+  | OEsltil (n: int64)                           (**r set-less-than immediate *)
+  | OEsltiul (n: int64)                          (**r set-less-than unsigned immediate *)
+  | OExoril (n: int64)                           (**r xor immediate *)
+  | OEluil (n: int64)                            (**r load upper-immediate *)
+  | OEaddilr0 (n: int64)                         (**r add immediate *)
+  | OEloadli (n: int64).                         (**r load an immediate int64 *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -215,6 +225,7 @@ Global Opaque eq_condition eq_addressing eq_operation.
   [eval_operation] and [eval_addressing] return a value. *)
   
 Definition zero32 := (Vint Int.zero).
+Definition zero64 := (Vlong Int64.zero).
   
 Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 vz: val): B :=
   match optR0 with
@@ -346,6 +357,16 @@ Definition eval_operation
   | 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)
+  | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
+  | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64))
+  | OEsltl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Clt) v1 v2 zero64))
+  | OEsltul optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64))
+  | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
+  | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
+  | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
+  | OEluil n, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
+  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
+  | OEloadli n, nil => Some (Vlong n)
   | _, _ => None
   end.
 
@@ -511,6 +532,16 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OExoriw _ => (Tint :: nil, Tint)
   | OEluiw _ => (nil, Tint)
   | OEaddiwr0 _ => (nil, Tint)
+  | OEseql _ => (Tlong :: Tlong :: nil, Tint)
+  | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
+  | OEsltl _ => (Tlong :: Tlong :: nil, Tint)
+  | OEsltul _ => (Tlong :: Tlong :: nil, Tint)
+  | OEsltil _ => (Tlong :: nil, Tint)
+  | OEsltiul _ => (Tlong :: nil, Tint)
+  | OExoril _ => (Tlong :: nil, Tlong)
+  | OEluil _ => (nil, Tlong)
+  | OEaddilr0 _ => (nil, Tlong)
+  | OEloadli _ => (nil, Tlong)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -732,6 +763,21 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
 - destruct v0...
 - trivial.
 - trivial.
+- destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
+  destruct Val.cmplu_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
+  destruct Val.cmplu_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
+  destruct Val.cmpl_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmplu;
+  destruct Val.cmplu_bool... all: destruct b...
+- unfold Val.cmpl; destruct Val.cmpl_bool...
+  all: destruct b...
+- unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
+- destruct v0...
+- trivial.
+- trivial.
+- trivial.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -926,6 +972,10 @@ Definition op_depends_on_memory (op: operation) : bool :=
   | OEsnew _ => negb Archi.ptr64
   | OEsltiuw _ => negb Archi.ptr64
   | OEsltuw _ => negb Archi.ptr64
+  | OEseql _ => Archi.ptr64
+  | OEsnel _ => Archi.ptr64
+  | OEsltul _ => Archi.ptr64
+  | OEsltiul _ => Archi.ptr64
   | _ => false
   end.
 
@@ -950,10 +1000,10 @@ Proof.
   intro DEPEND.
   f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
   all: intros; repeat (destruct args; auto);
-       unfold Val.cmpu, Val.cmpu_bool;
+       unfold Val.cmpu, Val.cmpu_bool, Val.cmplu, Val.cmplu_bool;
        try destruct optR0 as [[]|]; simpl;
        destruct v; try destruct v0; simpl; auto;
-       apply negb_false_iff in H; try rewrite H; auto.
+       try apply negb_false_iff in H; try rewrite H; auto.
 Qed.
 
 Lemma cond_valid_pointer_eq:
@@ -976,7 +1026,7 @@ Proof.
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
   all: intros MEM; repeat (destruct args; simpl; try congruence);
        try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto;
-       unfold Val.cmpu;
+       unfold Val.cmpu, Val.cmplu;
        erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.
 
@@ -1146,6 +1196,47 @@ Proof.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
 Qed.
 
+Lemma eval_cmplu_bool_inj': forall b c v v' v0 v0',
+  Val.inject f v v' ->
+  Val.inject f v0 v0' ->
+  Val.cmplu_bool (Mem.valid_pointer m1) c v v0 = Some b ->
+  Val.cmplu_bool (Mem.valid_pointer m2) c v' v0' = Some b.
+Proof.
+  intros.
+  eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
+Qed.
+
+Lemma eval_cmplu_bool_inj: forall c v v' v0 v'0,
+  Val.inject f v v' ->
+  Val.inject f v0 v'0 ->
+  Val.inject f (Val.maketotal (Val.cmplu (Mem.valid_pointer m1) c v v0))
+  (Val.maketotal (Val.cmplu (Mem.valid_pointer m2) c v' v'0)).
+Proof.
+  intros until v'0. intros HV1 HV2.
+  unfold Val.cmplu; 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto.
+  exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
+  intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+Qed.
+
+Lemma eval_cmplu_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 (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64))
+  (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)).
+Proof.
+  intros until optR0. intros HV1 HV2.
+  destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmplu; 
+  destruct (Val.cmplu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto;
+  assert (HVI: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long.
+  + exploit eval_cmplu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+  + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+  + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+Qed.
+
 Ltac TrivialExists :=
   match goal with
   | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
@@ -1362,6 +1453,15 @@ Proof.
   - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
   - apply eval_cmpu_bool_inj; auto.
   - inv H4; simpl; auto.
+  - apply eval_cmplu_bool_inj_opt; auto.
+  - apply eval_cmplu_bool_inj_opt; auto.
+  - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
+    inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
+  - apply eval_cmplu_bool_inj_opt; auto.
+  - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int.
+  - apply eval_cmplu_bool_inj; auto.
+  - inv H4; simpl; auto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index c1d65b4c..c222f777 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -170,6 +170,16 @@ let print_operation reg pp = function
   | 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)
+  | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
+  | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
+  | OEsltl optR0, [r1;r2] -> fprintf pp "OEsltl"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | OEsltul optR0, [r1;r2] -> fprintf pp "OEsltul"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | OEsltil n, [r1] -> fprintf pp "OEsltil(%a,%ld)" reg r1 (camlint_of_coqint n)
+  | OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n)
+  | OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n)
+  | OEluil n, [] -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
+  | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n)
+  | OEloadli n, [] -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 4c1f4625..9218d80d 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -18,6 +18,7 @@ Require Import Zbits.
 (** Value analysis for RISC V operators *)
 
 Definition zero32 := (I Int.zero).
+Definition zero64 := (L Int64.zero).
   
 Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B :=
   match optR0 with
@@ -155,6 +156,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | 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
+  | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
+  | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64)
+  | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64)
+  | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64)
+  | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
+  | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
+  | OExoril n, v1::nil => xorl v1 (L n)
+  | OEluil n, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
+  | OEaddilr0 n, nil => addl (L n) zero64
+  | OEloadli n, nil => L (n)
   | _, _ => Vbot
   end.
 
@@ -219,6 +230,20 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
 Qed.
 
+Lemma of_optbool_maketotal_sound:
+  forall ob ab, cmatch ob ab -> vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (of_optbool ab).
+Proof.
+  intros.
+  assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)).
+  {
+    destruct ob; simpl; auto with va.
+    destruct b; constructor; try omega.
+    change 1 with (usize Int.one). apply is_uns_usize.
+    red; intros. apply Int.bits_zero.
+  }
+  inv H; auto. simpl. destruct b; constructor.
+Qed.
+
 Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m,
   c = Ceq \/ c = Cne \/ c = Clt->
   vmatch bc a1 b1 ->
@@ -231,6 +256,21 @@ Proof.
   apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
 Qed.
 
+Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR0 m,
+  c = Ceq \/ c = Cne \/ c = Clt->
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc
+    (Val.maketotal
+       (Op.apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) c) a1 a0
+          Op.zero64))
+    (of_optbool (apply_bin_r0 optR0 (cmplu_bool c) b1 b0 zero64)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
+Qed.
+
 Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0,
   vmatch bc a1 b1 ->
   vmatch bc a0 b0 ->
@@ -242,6 +282,18 @@ Proof.
   apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
 Qed.
 
+Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0,
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc
+    (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl Clt) a1 a0 Op.zero64))
+    (of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) b1 b0 zero64)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
+Qed.
+
 Theorem eval_static_operation_sound:
   forall op vargs m vres aargs,
   eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
@@ -260,6 +312,11 @@ Proof.
   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.
+  1,2,4: apply eval_cmplu_sound; auto.
+  apply eval_cmpl_sound; auto.
+  unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va.
+  unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va.
+  unfold zero64; simpl. eauto with va.
 Qed.
 
 End SOUNDNESS.