From df9aab806ae8d20393b56e4175e210ed6cff1ef1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 12:48:51 +0200 Subject: a more general way to manage special registers before introducing SP --- riscV/PrintOp.ml | 98 +++++++++++++++++++++++++++----------------------------- 1 file changed, 47 insertions(+), 51 deletions(-) (limited to 'riscV/PrintOp.ml') 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 "" @@ -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) -- cgit