diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-06 23:37:22 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-06 23:37:22 +0200 |
| commit | dd4767e17235adb5de922626ed1fea15f4eb9e3b (patch) | |
| tree | 37843b101add33cf6ea56e055ddae2df96c6dc67 /riscV/PrintOp.ml | |
| parent | df9aab806ae8d20393b56e4175e210ed6cff1ef1 (diff) | |
| download | compcert-kvx-dd4767e17235adb5de922626ed1fea15f4eb9e3b.tar.gz compcert-kvx-dd4767e17235adb5de922626ed1fea15f4eb9e3b.zip | |
Important commit on expansions' mini CSE, and a draft for addptrofs
Diffstat (limited to 'riscV/PrintOp.ml')
| -rw-r--r-- | riscV/PrintOp.ml | 17 |
1 files changed, 10 insertions, 7 deletions
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) |