From acb41b1af6e5e4c933e3be1b17f6e5012eca794d Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Sat, 6 Feb 2021 16:53:46 +0100
Subject: cond and branches expanded

---
 riscV/PrintOp.ml | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

(limited to 'riscV/PrintOp.ml')

diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index c222f777..2b5ae1f5 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -60,6 +60,30 @@ let print_condition reg pp = function
       fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2
   | (Cnotcompfs c, [r1;r2]) ->
       fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2
+  | (CEbeqw optR0, [r1;r2]) ->
+      fprintf pp "CEbeqw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
+  | (CEbnew optR0, [r1;r2]) ->
+      fprintf pp "CEbnew"; (get_optR0_s Cne reg pp r1 r2 optR0)
+  | (CEbltw optR0, [r1;r2]) ->
+      fprintf pp "CEbltw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbltuw optR0, [r1;r2]) ->
+      fprintf pp "CEbltuw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbgew optR0, [r1;r2]) ->
+      fprintf pp "CEbgew"; (get_optR0_s Cge reg pp r1 r2 optR0)
+  | (CEbgeuw optR0, [r1;r2]) ->
+      fprintf pp "CEbgeuw"; (get_optR0_s Cge reg pp r1 r2 optR0)
+  | (CEbeql optR0, [r1;r2]) ->
+      fprintf pp "CEbeql"; (get_optR0_s Ceq reg pp r1 r2 optR0)
+  | (CEbnel optR0, [r1;r2]) ->
+      fprintf pp "CEbnel"; (get_optR0_s Cne reg pp r1 r2 optR0)
+  | (CEbltl optR0, [r1;r2]) ->
+      fprintf pp "CEbltl"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbltul optR0, [r1;r2]) ->
+      fprintf pp "CEbltul"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | (CEbgel optR0, [r1;r2]) ->
+      fprintf pp "CEbgel"; (get_optR0_s Cge reg pp r1 r2 optR0)
+  | (CEbgeul optR0, [r1;r2]) ->
+      fprintf pp "CEbgeul"; (get_optR0_s Cge reg pp r1 r2 optR0)
   | _ ->
       fprintf pp "<bad condition>"
 
@@ -180,6 +204,12 @@ let print_operation reg pp = function
   | 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)
+  | 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
+  | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
+  | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
+  | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
-- 
cgit