From dd4767e17235adb5de922626ed1fea15f4eb9e3b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 6 Apr 2021 23:37:22 +0200 Subject: Important commit on expansions' mini CSE, and a draft for addptrofs --- riscV/PrintOp.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'riscV/PrintOp.ml') diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index e18d31f6..53730a1b 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -36,14 +36,16 @@ let mu_name pp = function | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i) | MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i) -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_optR_s c reg pp r1 r2 = function | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2 | 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) + | Some SP_S -> failwith "PrintOp: SP_S in get_optR_s instruction (problem with RTL expansions?)" + +let get_optR_a pp = function + | None -> failwith "PrintOp: None in get_optR_a instruction (problem with RTL expansions?)" + | Some X0_L | Some X0_R -> fprintf pp "X0" + | Some SP_S -> fprintf pp "SP" let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> @@ -203,7 +205,6 @@ 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) - | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi | 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) @@ -214,7 +215,8 @@ let print_operation reg pp = function | 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) | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) - | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEaddiw (optR, n), [] -> fprintf pp "OEaddiw(%a,%ld)" get_optR_a optR (camlint_of_coqint n) + | OEaddiw (optR, 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 optR, [r1;r2] -> fprintf pp "OEseql"; (get_optR_s Ceq reg pp r1 r2 optR) @@ -227,7 +229,8 @@ let print_operation reg pp = function | 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) | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) - | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEaddil (optR, n), [] -> fprintf pp "OEaddil(%a,%ld)" get_optR_a optR (camlint_of_coqint n) + | OEaddil (optR, n), [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (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) -- cgit