Ccompu expansion

1 files changed, 18 insertions, 9 deletions

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;