Expansion of Ccompimm in RTL [Admitted checker]

1 files changed, 12 insertions, 0 deletions

diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 9ec474b3..7492b01c 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -30,6 +30,11 @@ let comparison_name = function
   | Cgt -> ">"
   | Cge -> ">="
 
+let get_optR0_s c reg pp r1 r2 = function
+  | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
+  | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
+  | Some false -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
+
 let print_condition reg pp = function
   | (Ccomp c, [r1;r2]) ->
       fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2
@@ -156,6 +161,13 @@ let print_operation reg pp = function
   | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
   | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
+  | 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)
+  | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%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)
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function