diff options
Diffstat (limited to 'powerpc/AsmToJSON.ml')
-rw-r--r-- | powerpc/AsmToJSON.ml | 74 |
1 files changed, 67 insertions, 7 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 6a235742..a3e57e51 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -28,10 +28,14 @@ let pp_reg pp t n = let pp_ireg pp reg = pp_reg pp "r" (TargetPrinter.int_reg_name reg) - let pp_freg pp reg = pp_reg pp "f" (TargetPrinter.float_reg_name reg) +let preg_annot = function + | IR r -> sprintf "r%s" (TargetPrinter.int_reg_name r) + | FR r -> sprintf "f%s" (TargetPrinter.float_reg_name r) + | _ -> assert false + let pp_atom pp a = pp_jstring pp (extern_atom a) let pp_atom_constant pp a = pp_jsingle_object pp "Atom" pp_atom a @@ -82,6 +86,7 @@ type instruction_arg = | Float32 of Floats.float32 | Float64 of Floats.float | Atom of positive + | String of string let id = ref 0 @@ -105,23 +110,49 @@ let pp_arg pp = function | Float32 f -> pp_float32_constant pp f | Float64 f -> pp_float64_constant pp f | Atom a -> pp_atom_constant pp a + | String s -> pp_jsingle_object pp "String" pp_jstring s + +let mnemonic_names =["Padd"; "Paddc"; "Padde"; "Paddi"; "Paddic"; "Paddis"; "Paddze"; "Pand_"; + "Pandc"; "Pandi_"; "Pandis_"; "Pannot"; "Pb"; "Pbctr"; "Pbctrl"; "Pbdnz"; + "Pbf"; "Pbl"; "Pblr"; "Pbs"; "Pbt"; "Pbtbl"; "Pcmpb"; "Pcmpd"; "Pcmpdi"; + "Pcmpld"; "Pcmpldi"; "Pcmplw"; "Pcmplwi"; "Pcmpw"; "Pcmpwi"; "Pcntlzd"; + "Pcntlzw"; "Pcreqv"; "Pcror"; "Pcrxor"; "Pdcbf"; "Pdcbi"; "Pdcbt"; + "Pdcbtls"; "Pdcbtst"; "Pdcbz"; "Pdivd"; "Pdivdu"; "Pdivw"; "Pdivwu"; + "Peieio"; "Peqv"; "Pextsb"; "Pextsh"; "Pextsw"; "Pfabs"; "Pfadd"; "Pfadds"; + "Pfcfid"; "Pfcmpu"; "Pfctidz"; "Pfctiw"; "Pfctiwz"; "Pfdiv"; "Pfdivs"; + "Pfmadd"; "Pfmr"; "Pfmsub"; "Pfmul"; "Pfmuls"; "Pfneg"; "Pfnmadd"; + "Pfnmsub"; "Pfres"; "Pfrsp"; "Pfrsqrte"; "Pfsel"; "Pfsqrt"; "Pfsub"; + "Pfsubs"; "Picbi"; "Picbtls"; "Pinlineasm"; "Pisel"; "Pisync"; "Plabel"; + "Plbz"; "Plbzx"; "Pld"; "Pldi"; "Pldx"; "Plfd"; "Plfdx"; "Plfi"; "Plfis"; + "Plfs"; "Plfsx"; "Plha"; "Plhax"; "Plhbrx"; "Plhz"; "Plhzx"; "Plwarx"; + "Plwbrx"; "Plwsync"; "Plwz"; "Plwzu"; "Plwzx"; "Pmbar"; "Pmfcr"; "Pmflr"; + "Pmfspr"; "Pmr"; "Pmtctr"; "Pmtlr"; "Pmtspr"; "Pmulhd"; "Pmulhdu"; "Pmulhw"; + "Pmulhwu"; "Pmulld"; "Pmulli"; "Pmullw"; "Pnand"; "Pnor"; "Por"; "Porc"; + "Pori"; "Poris"; "Prldicl"; "Prldimi"; "Prldinm"; "Prlwimi"; "Prlwinm"; + "Psld"; "Pslw"; "Psrad"; "Psradi"; "Psraw"; "Psrawi"; "Psrd"; "Psrw"; + "Pstb"; "Pstbx"; "Pstd"; "Pstdu"; "Pstdx"; "Pstfd"; "Pstfdu"; "Pstfdx"; + "Pstfs"; "Pstfsx"; "Psth"; "Psthbrx"; "Psthx"; "Pstw"; "Pstwbrx"; "Pstwcx_"; + "Pstwu"; "Pstwux"; "Pstwx"; "Psubfc"; "Psubfe"; "Psubfic"; "Psubfze"; + "Psync"; "Ptrap"; "Pxor"; "Pxori"; "Pxoris"] let pp_instructions pp ic = let ic = List.filter (fun s -> match s with | Pbuiltin (ef,_,_) -> begin match ef with - | EF_inline_asm _ -> true + | EF_inline_asm _ + | EF_annot _ -> true | _ -> false end | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> false | _ -> true) ic in let instruction pp n args = + assert (List.mem n mnemonic_names); pp_jobject_start pp; pp_jmember ~first:true pp "Instruction Name" pp_jstring n; pp_jmember pp "Args" (pp_jarray pp_arg) args; pp_jobject_end pp in - let instruction pp = function + let [@ocaml.warning "+4"] instruction pp = function | Padd (ir1,ir2,ir3) | Padd64 (ir1,ir2,ir3) -> instruction pp "Padd" [Ireg ir1; Ireg ir2; Ireg ir3] | Paddc (ir1,ir2,ir3) -> instruction pp "Paddc" [Ireg ir1; Ireg ir2; Ireg ir3] @@ -331,12 +362,35 @@ let pp_instructions pp ic = | Pxoris (ir1,ir2,c) -> instruction pp "Pxoris" [Ireg ir1; Ireg ir2; Constant c] | Pxoris64 (ir1,ir2,n) -> instruction pp "Pxoris" [Ireg ir1; Ireg ir2; Constant (Cint n)] | Plabel l -> instruction pp "Plabel" [ALabel l] - | Pbuiltin (ef,_,_) -> + | Pbuiltin (ef,args,_) -> begin match ef with | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" - | _ -> assert false + | EF_annot (kind,txt,targs) -> + let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in + let len = String.length annot_string in + let buf = Buffer.create len in + String.iter (fun c -> begin match c with + | '\\' | '"' -> Buffer.add_char buf '\\' + | _ -> () end; + Buffer.add_char buf c) annot_string; + let annot_string = Buffer.contents buf in + let kind = match P.to_int kind with + | 1 -> "normal" + | 2 -> "ais" + | _ -> assert false in + instruction pp "Pannot" [String kind;String annot_string] + | EF_annot_val _ + | EF_builtin _ + | EF_debug _ + | EF_external _ + | EF_free + | EF_malloc + | EF_memcpy _ + | EF_runtime _ + | EF_vload _ + | EF_vstore _ -> assert false end | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> assert false in (* Only debug relevant *) @@ -366,14 +420,15 @@ let pp_section pp sec = pp_jobject_start pp; pp_jmember ~first:true pp "Section Name" pp_jstring s; pp_jmember pp "Writable" pp_jbool w; - pp_jmember pp "Writable" pp_jbool e; + pp_jmember pp "Executable" pp_jbool e; pp_jobject_end pp | Section_debug_info _ | Section_debug_abbrev | Section_debug_line _ | Section_debug_loc | Section_debug_ranges - | Section_debug_str -> () (* There should be no info in the debug sections *) + | Section_debug_str + | Section_ais_annotation -> () (* There should be no info in the debug sections *) let pp_int_opt pp = function | None -> fprintf pp "0" @@ -441,3 +496,8 @@ let pp_program pp prog = pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars; pp_jmember pp "Functions" (pp_jarray pp_fundef) prog_funs; pp_jobject_end pp + +let pp_mnemonics pp = + let mnemonic_names = List.sort (String.compare) mnemonic_names in + let new_line pp () = pp_print_string pp "\n" in + pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names |