a more general way to manage special registers before introducing SP

1 files changed, 47 insertions, 51 deletions

diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 9b3e8835..e18d31f6 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -40,14 +40,10 @@ let get_immR0 pp = function
   | OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i)
   | OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i)
 
-let get_optR0_s c reg pp r1 r2 = function
+let get_optR_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 get_optR0_s_int reg pp r1 n = function
-  | None -> fprintf pp "(%a, %ld)" reg r1 n
-  | Some _ -> fprintf pp "(X0, %ld)" n
+  | Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
+  | Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
 
 let print_condition reg pp = function
   | (Ccomp c, [r1;r2]) ->
@@ -74,38 +70,38 @@ 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)
-  | (CEbequw optR0, [r1;r2]) ->
-      fprintf pp "CEbequw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
-  | (CEbneuw optR0, [r1;r2]) ->
-      fprintf pp "CEbneuw"; (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)
-  | (CEbequl optR0, [r1;r2]) ->
-      fprintf pp "CEbequl"; (get_optR0_s Ceq reg pp r1 r2 optR0)
-  | (CEbneul optR0, [r1;r2]) ->
-      fprintf pp "CEbneul"; (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)
+  | (CEbeqw optR, [r1;r2]) ->
+      fprintf pp "CEbeqw"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | (CEbnew optR, [r1;r2]) ->
+      fprintf pp "CEbnew"; (get_optR_s Cne reg pp r1 r2 optR)
+  | (CEbequw optR, [r1;r2]) ->
+      fprintf pp "CEbequw"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | (CEbneuw optR, [r1;r2]) ->
+      fprintf pp "CEbneuw"; (get_optR_s Cne reg pp r1 r2 optR)
+  | (CEbltw optR, [r1;r2]) ->
+      fprintf pp "CEbltw"; (get_optR_s Clt reg pp r1 r2 optR)
+  | (CEbltuw optR, [r1;r2]) ->
+      fprintf pp "CEbltuw"; (get_optR_s Clt reg pp r1 r2 optR)
+  | (CEbgew optR, [r1;r2]) ->
+      fprintf pp "CEbgew"; (get_optR_s Cge reg pp r1 r2 optR)
+  | (CEbgeuw optR, [r1;r2]) ->
+      fprintf pp "CEbgeuw"; (get_optR_s Cge reg pp r1 r2 optR)
+  | (CEbeql optR, [r1;r2]) ->
+      fprintf pp "CEbeql"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | (CEbnel optR, [r1;r2]) ->
+      fprintf pp "CEbnel"; (get_optR_s Cne reg pp r1 r2 optR)
+  | (CEbequl optR, [r1;r2]) ->
+      fprintf pp "CEbequl"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | (CEbneul optR, [r1;r2]) ->
+      fprintf pp "CEbneul"; (get_optR_s Cne reg pp r1 r2 optR)
+  | (CEbltl optR, [r1;r2]) ->
+      fprintf pp "CEbltl"; (get_optR_s Clt reg pp r1 r2 optR)
+  | (CEbltul optR, [r1;r2]) ->
+      fprintf pp "CEbltul"; (get_optR_s Clt reg pp r1 r2 optR)
+  | (CEbgel optR, [r1;r2]) ->
+      fprintf pp "CEbgel"; (get_optR_s Cge reg pp r1 r2 optR)
+  | (CEbgeul optR, [r1;r2]) ->
+      fprintf pp "CEbgeul"; (get_optR_s Cge reg pp r1 r2 optR)
   | _ ->
       fprintf pp "<bad condition>"
 
@@ -208,12 +204,12 @@ let print_operation reg pp = function
   | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
   | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi
-  | 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)
-  | OEsequw optR0, [r1;r2] -> fprintf pp "OEsequw"; (get_optR0_s Ceq reg pp r1 r2 optR0)
-  | OEsneuw optR0, [r1;r2] -> fprintf pp "OEsneuw"; (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)
-  | OEsltuw optR0, [r1;r2] -> fprintf pp "OEsltuw"; (get_optR0_s Clt reg pp r1 r2 optR0)
+  | OEseqw optR, [r1;r2] -> fprintf pp "OEseqw"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | OEsnew optR, [r1;r2] -> fprintf pp "OEsnew"; (get_optR_s Cne reg pp r1 r2 optR)
+  | OEsequw optR, [r1;r2] -> fprintf pp "OEsequw"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | OEsneuw optR, [r1;r2] -> fprintf pp "OEsneuw"; (get_optR_s Cne reg pp r1 r2 optR)
+  | OEsltw optR, [r1;r2] -> fprintf pp "OEsltw"; (get_optR_s Clt reg pp r1 r2 optR)
+  | OEsltuw optR, [r1;r2] -> fprintf pp "OEsltuw"; (get_optR_s Clt reg pp r1 r2 optR)
   | OEsltiw n, [r1] -> fprintf pp "OEsltiw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
@@ -221,12 +217,12 @@ let print_operation reg pp = function
   | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (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)
-  | OEsneul optR0, [r1;r2] -> fprintf pp "OEsneul"; (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)
+  | OEseql optR, [r1;r2] -> fprintf pp "OEseql"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | OEsnel optR, [r1;r2] -> fprintf pp "OEsnel"; (get_optR_s Cne reg pp r1 r2 optR)
+  | OEsequl optR, [r1;r2] -> fprintf pp "OEsequl"; (get_optR_s Ceq reg pp r1 r2 optR)
+  | OEsneul optR, [r1;r2] -> fprintf pp "OEsneul"; (get_optR_s Cne reg pp r1 r2 optR)
+  | OEsltl optR, [r1;r2] -> fprintf pp "OEsltl"; (get_optR_s Clt reg pp r1 r2 optR)
+  | OEsltul optR, [r1;r2] -> fprintf pp "OEsltul"; (get_optR_s Clt reg pp r1 r2 optR)
   | 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)