aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/AsmToJSON.ml
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/AsmToJSON.ml')
-rw-r--r--powerpc/AsmToJSON.ml74
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