bugfix and printOp

2 files changed, 29 insertions, 19 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index a5fa4a0a..6eb82274 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -59,14 +59,15 @@ type immt =
   | Sltil
   | Sltiul
 
-let find_or_addnmove op args rd succ map_consts node_dec =
+let find_or_addnmove op args rd succ map_consts not_final =
   let sop = Sop (op, args) in
   match Hashtbl.find_opt map_consts sop with
   | Some r ->
-      if node_dec then node := !node - 1;
+      if not_final then node := !node - 1;
       Sr (P.of_int r)
   | None ->
-      Hashtbl.add map_consts sop (p2i rd);
+      if not (List.exists (fun a -> a = rd) args) && not_final then
+        Hashtbl.add map_consts sop (p2i rd);
       Si (Iop (op, args, rd, succ))
 
 let build_head_tuple head sv =
@@ -75,59 +76,62 @@ let build_head_tuple head sv =
 let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r
 
 let unzip_head_tuple_move ht r succ =
-  match ht with l, Some r' -> [ Iop (Omove, [ r' ], r, succ) ] | l, None -> l
+  match ht with
+  | l, Some r' ->
+      if r' != r then [ Iop (Omove, [ r' ], r, succ) ] else [ Inop succ ]
+  | l, None -> l
 
 let build_full_ilist op args dest succ hd k map_consts =
   let sv = find_or_addnmove op args dest succ map_consts false in
   let ht = build_head_tuple hd sv in
   unzip_head_tuple_move ht dest succ @ k
 
-let load_hilo32 dest hi lo succ map_consts node_dec =
+let load_hilo32 dest hi lo succ map_consts not_final =
   let op1 = OEluiw hi in
   if Int.eq lo Int.zero then
-    let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in
+    let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
     build_head_tuple [] sv
   else
     let r = r2pi () in
-    let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in
+    let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in
     let ht1 = build_head_tuple [] sv1 in
     let r' = unzip_head_tuple ht1 r in
     let op2 = OEaddiw lo in
-    let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in
+    let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in
     build_head_tuple (fst ht1) sv2
 
-let load_hilo64 dest hi lo succ map_consts node_dec =
+let load_hilo64 dest hi lo succ map_consts not_final =
   let op1 = OEluil hi in
   if Int64.eq lo Int64.zero then
-    let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in
+    let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
     build_head_tuple [] sv
   else
     let r = r2pi () in
-    let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in
+    let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in
     let ht1 = build_head_tuple [] sv1 in
     let r' = unzip_head_tuple ht1 r in
     let op2 = OEaddil lo in
-    let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in
+    let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in
     build_head_tuple (fst ht1) sv2
 
-let loadimm32 dest n succ map_consts node_dec =
+let loadimm32 dest n succ map_consts not_final =
   match make_immed32 n with
   | Imm32_single imm ->
       let op1 = OEaddiwr0 imm in
-      let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in
+      let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
       build_head_tuple [] sv
-  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts node_dec
+  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final
 
-let loadimm64 dest n succ map_consts node_dec =
+let loadimm64 dest n succ map_consts not_final =
   match make_immed64 n with
   | Imm64_single imm ->
       let op1 = OEaddilr0 imm in
-      let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in
+      let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
       build_head_tuple [] sv
-  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts node_dec
+  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final
   | Imm64_large imm ->
       let op1 = OEloadli imm in
-      let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in
+      let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
       build_head_tuple [] sv
 
 let get_opimm imm = function
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index a37f5c9c..4494080e 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -209,6 +209,8 @@ let print_operation reg pp = function
   | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
   | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(X0,%ld)" (camlint_of_coqint n)
+  | OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n)
+  | OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (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)
   | OEsequl optR0, [r1;r2] -> fprintf pp "OEsequl"; (get_optR0_s Ceq reg pp r1 r2 optR0)
@@ -221,8 +223,12 @@ let print_operation reg pp = function
   | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
   | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(X0,%ld)" (camlint_of_coqint n)
+  | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n)
+  | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
   | OEmayundef isl, [r1;r2] -> fprintf pp "OEmayundef (%b,%a,%a)" isl reg r1 reg r2
+  | OEshrxundef n, [r1] -> fprintf pp "OEshrxundef (%ld,%a)" (camlint_of_coqint n) reg r1
+  | OEshrxlundef n, [r1] -> fprintf pp "OEshrxlundef (%ld,%a)" (camlint_of_coqint n) reg r1
   | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
   | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
   | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2