diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
commit | acb41b1af6e5e4c933e3be1b17f6e5012eca794d (patch) | |
tree | db57a6b2543871312a952ffa2e462e35aef674e0 /riscV/PrintOp.ml | |
parent | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (diff) | |
download | compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.tar.gz compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.zip |
cond and branches expanded
Diffstat (limited to 'riscV/PrintOp.ml')
-rw-r--r-- | riscV/PrintOp.ml | 30 |
1 files changed, 30 insertions, 0 deletions
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 |