diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-24 12:15:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-24 12:15:45 +0200 |
| commit | 0372e87d41994a24cf001eba00a5797f80192c29 (patch) | |
| tree | f5dc67971078f96b0c83568fa2e9ba1b454f03c3 | |
| parent | 2cad56ee1f3d508d1671628a10da1852c5ee95a7 (diff) | |
| download | compcert-kvx-0372e87d41994a24cf001eba00a5797f80192c29.tar.gz compcert-kvx-0372e87d41994a24cf001eba00a5797f80192c29.zip | |
op printing (still incomplete)
| -rw-r--r-- | mppa_k1c/PrintOp.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/mppa_k1c/PrintOp.ml b/mppa_k1c/PrintOp.ml index 8417571a..575fa94f 100644 --- a/mppa_k1c/PrintOp.ml +++ b/mppa_k1c/PrintOp.ml @@ -168,6 +168,7 @@ 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) + | Oextfz(stop, start), [r1] -> fprintf pp "extfz(%ld, %ld, %a)" (camlint_of_coqint stop) (camlint_of_coqint start) reg r1 | Oextfs(stop, start), [r1] -> fprintf pp "extfs(%ld, %ld, %a)" (camlint_of_coqint stop) (camlint_of_coqint start) reg r1 | Oextfzl(stop, start), [r1] -> fprintf pp "extfzl(%ld, %ld, %a)" (camlint_of_coqint stop) (camlint_of_coqint start) reg r1 @@ -184,14 +185,24 @@ let print_operation reg pp = function print_condition0 reg pp cond0 rc; fprintf pp " ? %a :l %Ld" reg r1 (camlint64_of_coqint imm) | Oaddx(s14), [r1; r2] -> fprintf pp "(%a << %d) + %a" reg r1 (int_of_s14 s14) reg r2 + | Oaddximm(s14, imm), [r1] -> fprintf pp "(%a << %d) + %ld" reg r1 (int_of_s14 s14) (camlint_of_coqint imm) | Oaddxl(s14), [r1; r2] -> fprintf pp "(%a <<l %d) +l %a" reg r1 (int_of_s14 s14) reg r2 + | Oaddxlimm(s14, imm), [r1] -> fprintf pp "(%a <<l %d) +l %Ld" reg r1 (int_of_s14 s14) (camlint64_of_coqint imm) | Orevsubimm(imm), [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint imm) reg r1 | Orevsubximm(s14, imm), [r1] -> fprintf pp "%ld - (%a << %d)" (camlint_of_coqint imm) reg r1 (int_of_s14 s14) | Orevsublimm(imm), [r1] -> fprintf pp "%Ld -l %a" (camlint64_of_coqint imm) reg r1 | Orevsubxlimm(s14, imm), [r1] -> fprintf pp "%Ld -l (%a <<l %d)" (camlint64_of_coqint imm) reg r1 (int_of_s14 s14) | Orevsubx(s14), [r1; r2] -> fprintf pp "%a - (%a << %d)" reg r2 reg r1 (int_of_s14 s14) | Orevsubxl(s14), [r1; r2] -> fprintf pp "%a -l (%a <<l %d)" reg r2 reg r1 (int_of_s14 s14) - | _ -> fprintf pp "<bad operator>" + | Omulimm(imm), [r1] -> fprintf pp "%a * %ld" reg r1 (camlint_of_coqint imm) + | Omullimm(imm), [r1] -> fprintf pp "%a *l %Ld" reg r1 (camlint64_of_coqint imm) + | Omadd, [r1; r2; r3] -> fprintf pp "%a + %a * %a" reg r1 reg r2 reg r3 + | Omaddl, [r1; r2; r3] -> fprintf pp "%a +l %a *l %a" reg r1 reg r2 reg r3 + | (Omaddimm imm), [r1; r2] -> fprintf pp "%a + %a * %ld" reg r1 reg r2 (camlint_of_coqint imm) + | (Omaddlimm imm), [r1; r2] -> fprintf pp "%a +l %a *l %Ld" reg r1 reg r2 (camlint64_of_coqint imm) + | Omsub, [r1; r2; r3] -> fprintf pp "%a - %a * %a" reg r1 reg r2 reg r3 + | Omsubl, [r1; r2; r3] -> fprintf pp "%a -l %a *l %a" reg r1 reg r2 reg r3 + | _, _ -> fprintf pp "<bad operator>" let print_addressing reg pp = function | Aindexed n, [r1] -> fprintf pp "%a + %Ld" reg r1 (camlint64_of_ptrofs n) |