diff options
Diffstat (limited to 'checklink/Asm_printers.ml')
| -rw-r--r-- | checklink/Asm_printers.ml | 321 |
1 files changed, 0 insertions, 321 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml deleted file mode 100644 index 38a420f6..00000000 --- a/checklink/Asm_printers.ml +++ /dev/null @@ -1,321 +0,0 @@ -open Camlcoq -open Asm -open AST -open Library - -let string_of_pos p = Z.to_string (Z.Zpos p) -let string_of_coq_Z = Z.to_string -let string_of_ident = string_of_pos -let string_of_label = string_of_pos -let string_of_iint = string_of_coq_Z - -let string_of_ireg = function -| GPR0 -> "GPR0" -| GPR1 -> "GPR1" -| GPR2 -> "GPR2" -| GPR3 -> "GPR3" -| GPR4 -> "GPR4" -| GPR5 -> "GPR5" -| GPR6 -> "GPR6" -| GPR7 -> "GPR7" -| GPR8 -> "GPR8" -| GPR9 -> "GPR9" -| GPR10 -> "GPR10" -| GPR11 -> "GPR11" -| GPR12 -> "GPR12" -| GPR13 -> "GPR13" -| GPR14 -> "GPR14" -| GPR15 -> "GPR15" -| GPR16 -> "GPR16" -| GPR17 -> "GPR17" -| GPR18 -> "GPR18" -| GPR19 -> "GPR19" -| GPR20 -> "GPR20" -| GPR21 -> "GPR21" -| GPR22 -> "GPR22" -| GPR23 -> "GPR23" -| GPR24 -> "GPR24" -| GPR25 -> "GPR25" -| GPR26 -> "GPR26" -| GPR27 -> "GPR27" -| GPR28 -> "GPR28" -| GPR29 -> "GPR29" -| GPR30 -> "GPR30" -| GPR31 -> "GPR31" - -let string_of_freg = function -| FPR0 -> "FPR0" -| FPR1 -> "FPR1" -| FPR2 -> "FPR2" -| FPR3 -> "FPR3" -| FPR4 -> "FPR4" -| FPR5 -> "FPR5" -| FPR6 -> "FPR6" -| FPR7 -> "FPR7" -| FPR8 -> "FPR8" -| FPR9 -> "FPR9" -| FPR10 -> "FPR10" -| FPR11 -> "FPR11" -| FPR12 -> "FPR12" -| FPR13 -> "FPR13" -| FPR14 -> "FPR14" -| FPR15 -> "FPR15" -| FPR16 -> "FPR16" -| FPR17 -> "FPR17" -| FPR18 -> "FPR18" -| FPR19 -> "FPR19" -| FPR20 -> "FPR20" -| FPR21 -> "FPR21" -| FPR22 -> "FPR22" -| FPR23 -> "FPR23" -| FPR24 -> "FPR24" -| FPR25 -> "FPR25" -| FPR26 -> "FPR26" -| FPR27 -> "FPR27" -| FPR28 -> "FPR28" -| FPR29 -> "FPR29" -| FPR30 -> "FPR30" -| FPR31 -> "FPR31" - -let string_of_preg = function -| IR (i0) -> "IR(" ^ string_of_ireg i0 ^ ")" -| FR (f0) -> "FR(" ^ string_of_freg f0 ^ ")" -| PC -> "PC" -| LR -> "LR" -| CTR -> "CTR" -| CARRY -> "CARRY" -| CR0_0 -> "CR0_0" -| CR0_1 -> "CR0_1" -| CR0_2 -> "CR0_2" -| CR0_3 -> "CR0_3" -| CR1_2 -> "CR1_2" - -let string_of_external_function e = - match e with - | EF_builtin(name, sg) -> "EF_builtin" - | EF_vload(chunk) -> "EF_vload" - | EF_vstore(chunk) -> "EF_vstore" - | EF_vload_global(_, _, _) -> "EF_vload_global" - | EF_vstore_global(_, _, _) -> "EF_vstore_global" - | EF_malloc -> "EF_malloc" - | EF_free -> "EF_free" - | EF_memcpy(sz, al) -> - "EF_memcpy(" ^ string_of_z sz ^ ", " ^ string_of_z al ^ ")" - | EF_annot(_, _) -> "EF_annot" - | EF_annot_val(txt, targ) -> "EF_annot_val" - | _ -> "UNKNOWN" - -let string_of_constant = function -| Cint (i0) -> "Cint(" ^ string_of_iint i0 ^ ")" -| Csymbol_low (i0, i1) -> "Csymbol_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" -| Csymbol_high (i0, i1) -> "Csymbol_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" -| Csymbol_sda (i0, i1) -> "Csymbol_sda(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" -| Csymbol_rel_low (i0, i1) -> "Csymbol_rel_low(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" -| Csymbol_rel_high (i0, i1) -> "Csymbol_rel_high(" ^ string_of_ident i0 ^ ", " ^ string_of_iint i1 ^ ")" - -let string_of_crbit = function -| CRbit_0 -> "CRbit_0" -| CRbit_1 -> "CRbit_1" -| CRbit_2 -> "CRbit_2" -| CRbit_3 -> "CRbit_3" -| CRbit_6 -> "CRbit_6" - -let string_of_memory_chunk = function - | Mint8signed -> "int8s" - | Mint8unsigned -> "int8u" - | Mint16signed -> "int16s" - | Mint16unsigned -> "int16u" - | Mint32 -> "int32" - | Mint64 -> "int64" - | Mfloat32 -> "float32" - | Mfloat64 -> "float64" - | Many32 -> "any32" - | Many64 -> "any64" - -let rec string_of_annot_param sp_reg_name = function - | AA_base x -> string_of_preg x - | AA_int n -> Printf.sprintf "%ld" (camlint_of_coqint n) - | AA_long n -> Printf.sprintf "%Ld" (camlint64_of_coqint n) - | AA_float n -> Printf.sprintf "%.18g" (camlfloat_of_coqfloat n) - | AA_single n -> Printf.sprintf "%.18g" (camlfloat_of_coqfloat32 n) - | AA_loadstack(chunk, ofs) -> - Printf.sprintf "mem(%s + %ld, %s)" - sp_reg_name - (camlint_of_coqint ofs) - ((string_of_memory_chunk chunk)) - | AA_addrstack ofs -> - Printf.sprintf "(%s + %ld)" - sp_reg_name - (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> - Printf.sprintf "mem(\"%s\" + %ld, %s)" - (extern_atom id) - (camlint_of_coqint ofs) - (string_of_memory_chunk chunk) - | AA_addrglobal(id, ofs) -> - Printf.sprintf "(\"%s\" + %ld)" - (extern_atom id) - (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> - Printf.sprintf "(%s * 0x100000000 + %s)" - (string_of_annot_param sp_reg_name hi) - (string_of_annot_param sp_reg_name lo) - -let string_of_instruction = function -| Padd (i0, i1, i2) -> "Padd(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Paddc (i0, i1, i2) -> "Paddc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Padde (i0, i1, i2) -> "Padde(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Paddi (i0, i1, c2) -> "Paddi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Paddic (i0, i1, c2) -> "Paddic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Paddis (i0, i1, c2) -> "Paddis(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Paddze (i0, i1) -> "Paddze(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pallocframe(c0, i1) -> "Pallocframe(" ^ string_of_coq_Z c0 ^ ", " ^ string_of_iint i1 ^ ")" -| Pand_ (i0, i1, i2) -> "Pand_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pandc (i0, i1, i2) -> "Pandc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pandi_ (i0, i1, c2) -> "Pandi_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Pandis_ (i0, i1, c2) -> "Pandis_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Pb (l0) -> "Pb(" ^ string_of_label l0 ^ ")" -| Pbctr sg -> "Pbctr" -| Pbctrl sg -> "Pbctrl" -| Pbdnz (l1) -> "Pbdnz(" ^ string_of_label l1 ^ ")" -| Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" -| Pbl (i0, sg) -> "Pbl(" ^ string_of_ident i0 ^ ")" -| Pbs (i0, sg) -> "Pbs(" ^ string_of_ident i0 ^ ")" -| Pblr -> "Pblr" -| Pbt (c0, l1) -> "Pbt(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")" -| Pbtbl (i0, l1) -> "Pbtbl(" ^ string_of_ireg i0 ^ ", " ^ string_of_list string_of_label ", " l1 ^ ")" -| Pcmplw (i0, i1) -> "Pcmplw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pcmplwi (i0, c1) -> "Pcmplwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" -| Pcmpw (i0, i1) -> "Pcmpw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pcmpwi (i0, c1) -> "Pcmpwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" -| Pcntlzw (i0, i1) -> "Pcntlzw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pcreqv (c0, c1, c2) -> "Pcreqv(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" -| Pcror (c0, c1, c2) -> "Pcror(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" -| Pcrxor (c0, c1, c2) -> "Pcrxor(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" -| Pdivw (i0, i1, i2) -> "Pdivw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pdivwu (i0, i1, i2) -> "Pdivwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Peieio -> "Peieio" -| Peqv (i0, i1, i2) -> "Peqv(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pextsb (i0, i1) -> "Pextsb(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pextsh (i0, i1) -> "Pextsh(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pfreeframe(c0, i1) -> "Pfreeframe(" ^ string_of_coq_Z c0 ^ ", " ^ string_of_iint i1 ^ ")" -| Pfabs (f0, f1) -> "Pfabs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfabss (f0, f1) -> "Pfabss(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfadd (f0, f1, f2) -> "Pfadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfadds (f0, f1, f2) -> "Pfadds(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfcmpu (f0, f1) -> "Pfcmpu(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfcti (i0, f1) -> "Pfcti(" ^ string_of_ireg i0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfctiw (f0, f1) -> "Pfctiw(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfctiwz (f0, f1) -> "Pfctiwz(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfdiv (f0, f1, f2) -> "Pfdiv(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfdivs (f0, f1, f2) -> "Pfdivs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfmake (f0, i1, i2) -> "Pfmake(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pfmr (f0, f1) -> "Pfmr(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfmul (f0, f1, f2) -> "Pfmul(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfmuls (f0, f1, f2) -> "Pfmuls(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfneg (f0, f1) -> "Pfneg(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfnegs (f0, f1) -> "Pfnegs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfrsp (f0, f1) -> "Pfrsp(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfxdp (f0, f1) -> "Pfxdp(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfsub (f0, f1, f2) -> "Pfsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfsubs (f0, f1, f2) -> "Pfsubs(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ")" -| Pfmadd (f0, f1, f2, f3) -> "Pfmadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfmsub (f0, f1, f2, f3) -> "Pfmsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfnmadd (f0, f1, f2, f3) -> "Pfnmadd(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfnmsub (f0, f1, f2, f3) -> "Pfnmsub(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pfsqrt (f0, f1) -> "Pfsqrt(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfrsqrte (f0, f1) -> "Pfrsqrte(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfres (f0, f1) -> "Pfres(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ")" -| Pfsel (f0, f1, f2, f3) -> "Pfsel(" ^ string_of_freg f0 ^ ", " ^ string_of_freg f1 ^ ", " ^ string_of_freg f2 ^ ", " ^ string_of_freg f3 ^ ")" -| Pisync -> "Pisync" -| Plbz (i0, c1, i2) -> "Plbz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plbzx (i0, i1, i2) -> "Plbzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfd (f0, c1, i2) -> "Plfd(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfd_a (f0, c1, i2) -> "Plfd_a(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfdx (f0, i1, i2) -> "Plfdx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfdx_a (f0, i1, i2) -> "Plfdx_a(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfs (f0, c1, i2) -> "Plfs(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfsx (f0, i1, i2) -> "Plfsx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plha (i0, c1, i2) -> "Plha(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plhax (i0, i1, i2) -> "Plhax(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plhbrx (i0, i1, i2) -> "Plhbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plhz (i0, c1, i2) -> "Plhz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plhzx (i0, i1, i2) -> "Plhzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfi (f0, f1) -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat f1 ^ ")" -| Plfis (f0, f1) -> "Plfis(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat32 f1 ^ ")" -| Plwarx (i0, i1, i2) -> "Plwarx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwbrx (i0, i1, i2) -> "Plwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwz (i0, c1, i2) -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwzu (i0, c1, i2) -> "Plwzu(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwz_a (i0, c1, i2) -> "Plwz_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwzx (i0, i1, i2) -> "Plwzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plwzx_a (i0, i1, i2) -> "Plwzx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pmfcr (i0) -> "Pmfcr(" ^ string_of_ireg i0 ^ ")" -| Pmfcrbit (i0, c1) -> "Pmfcrbit(" ^ string_of_ireg i0 ^ ", " ^ string_of_crbit c1 ^ ")" -| Pmflr (i0) -> "Pmflr(" ^ string_of_ireg i0 ^ ")" -| Pmr (i0, i1) -> "Pmr(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Pmtctr (i0) -> "Pmtctr(" ^ string_of_ireg i0 ^ ")" -| Pmtlr (i0) -> "Pmtlr(" ^ string_of_ireg i0 ^ ")" -| Pmulli (i0, i1, c2) -> "Pmulli(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Pmullw (i0, i1, i2) -> "Pmullw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pmulhw (i0, i1, i2) -> "Pmulhw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pmulhwu (i0, i1, i2) -> "Pmulhwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pnand (i0, i1, i2) -> "Pnand(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pnor (i0, i1, i2) -> "Pnor(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Por (i0, i1, i2) -> "Por(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Porc (i0, i1, i2) -> "Porc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pori (i0, i1, c2) -> "Pori(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Poris (i0, i1, c2) -> "Poris(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Prlwinm (i0, i1, i2, i3) -> "Prlwinm(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_iint i2 ^ ", " ^ string_of_iint i3 ^ ")" -| Prlwimi (i0, i1, i2, i3) -> "Prlwimi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_iint i2 ^ ", " ^ string_of_iint i3 ^ ")" -| Pslw (i0, i1, i2) -> "Pslw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psraw (i0, i1, i2) -> "Psraw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psrawi (i0, i1, i2) -> "Psrawi(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_iint i2 ^ ")" -| Psrw (i0, i1, i2) -> "Psrw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstb (i0, c1, i2) -> "Pstb(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstbx (i0, i1, i2) -> "Pstbx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfd (f0, c1, i2) -> "Pstfd(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfd_a (f0, c1, i2) -> "Pstfd_a(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfdu (f0, c1, i2) -> "Pstfdu(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfdx (f0, i1, i2) -> "Pstfdx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfdx_a (f0, i1, i2) -> "Pstfdx_a(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfs (f0, c1, i2) -> "Pstfs(" ^ string_of_freg f0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstfsx (f0, i1, i2) -> "Pstfsx(" ^ string_of_freg f0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psth (i0, c1, i2) -> "Psth(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psthx (i0, i1, i2) -> "Psthx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psthbrx (i0, i1, i2) -> "Psthbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstw (i0, c1, i2) -> "Pstw(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstw_a (i0, c1, i2) -> "Pstw_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwu (i0, c1, i2) -> "Pstwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwx (i0, i1, i2) -> "Pstwx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwx_a (i0, i1, i2) -> "Pstwx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwux (i0, i1, i2) -> "Pstwux(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwbrx (i0, i1, i2) -> "Pstwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pstwcx_ (i0, i1, i2) -> "Pstwcx_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psubfc (i0, i1, i2) -> "Psubfc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psubfe (i0, i1, i2) -> "Psubfe(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Psubfze (i0, i1) -> "Psubfze(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" -| Psubfic (i0, i1, c2) -> "Psubfic(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Psync -> "Psync" -| Ptrap -> "Ptrap" -| Pxor (i0, i1, i2) -> "Pxor(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Pxori (i0, i1, c2) -> "Pxori(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Pxoris (i0, i1, c2) -> "Pxoris(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")" -| Plabel (l0) -> "Plabel(" ^ string_of_label l0 ^ ")" -| Pbuiltin (e0, p1, p2) -> "Pbuiltin(" ^ string_of_external_function e0 ^ ", " ^ string_of_list string_of_preg ", " p1 ^ ", " ^ string_of_list string_of_preg ", " p2 ^ ")" -| Pannot (e0, a1) -> - let sp_reg_name = string_of_external_function e0 in - "Pannot(" ^ string_of_external_function e0 ^ ", " ^ string_of_list (string_of_annot_param sp_reg_name) ", " a1 ^ ")" -| Pcfi_adjust n -> "Pcfi_adjust(" ^ string_of_coq_Z n ^ ")" -| Pcfi_rel_offset n -> "Pcfi_rel_offset(" ^ string_of_coq_Z n ^ ")" - -let string_of_init_data = function -| Init_int8(i) -> "Init_int8(" ^ string_of_int (z_int_lax i) ^ ")" -| Init_int16(i) -> "Init_int16(" ^ string_of_int (z_int_lax i) ^ ")" -| Init_int32(i) -> "Init_int32(" ^ string_of_int32i (z_int32 i) ^ ")" -| Init_int64(i) -> "Init_int64(" ^ string_of_int64i (z_int64 i) ^ ")" -| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat32 f ^ ")" -| Init_float64(f) -> "Init_float64(" ^ string_of_ffloat f ^ ")" -| Init_space(z) -> "Init_space(" ^ string_of_int (z_int z) ^ ")" -| Init_addrof(ident, ofs) -> - "Init_addrof(" ^ string_of_pos ident ^ ", " ^ string_of_int32i (z_int32 ofs) ^ ")" |