aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/PrintOp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/PrintOp.ml')
-rw-r--r--riscV/PrintOp.ml125
1 files changed, 71 insertions, 54 deletions
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 84380251..0d47192a 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -30,10 +30,20 @@ let comparison_name = function
| Cgt -> ">"
| Cge -> ">="
-let get_optR0_s c reg pp r1 r2 = function
+let mu_name pp = function
+ | MUint -> fprintf pp "MUint"
+ | MUlong -> fprintf pp "MUlong"
+ | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i)
+ | MUshrxl i -> fprintf pp "MUshrxl(%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 true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
- | Some false -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
+ | 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 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"
let print_condition reg pp = function
| (Ccomp c, [r1;r2]) ->
@@ -60,47 +70,47 @@ 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>"
let print_operation reg pp = function
| Omove, [r1] -> reg pp r1
- | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
- | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n)
- | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
- | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
+ | Ointconst n, [] -> fprintf pp "Ointconst(%ld)" (camlint_of_coqint n)
+ | Olongconst n, [] -> fprintf pp "Olongconst(%LdL)" (camlint64_of_coqint n)
+ | Ofloatconst n, [] -> fprintf pp "Ofloatconst(%F)" (camlfloat_of_coqfloat n)
+ | Osingleconst n, [] -> fprintf pp "Osingleconst(%Ff)" (camlfloat_of_coqfloat32 n)
| Oaddrsymbol(id, ofs), [] ->
fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs)
| Oaddrstack ofs, [] ->
@@ -193,29 +203,36 @@ 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)
- | 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)
- | OEluiw (n, _), _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
- | OEaddiwr0 (n, _), _ -> fprintf pp "OEaddiwr0(%ld,X0)" (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)
+ | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (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)
+ | 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)
| OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
- | OEaddilr0 n, _ -> fprintf pp "OEaddilr0(%ld,X0)" (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)
+ | OEmayundef mu, [r1;r2] -> fprintf pp "OEmayundef (%a,%a,%a)" mu_name mu reg r1 reg r2
| 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
generated by cgit (git 2.34.1) at 2024-05-20 02:16:29 +0000