From 801ed5afd5e5f97818e73c06102510bfcf7170c5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 27 Apr 2015 17:02:07 +0200 Subject: Added the first version of the sdump export to json. --- arm/AsmToJSON.ml | 18 +++ cfrontend/C2CToJSON.ml | 72 ++++++++++ driver/Driver.ml | 16 ++- ia32/AsmToJSON.ml | 17 +++ powerpc/AsmToJSON.ml | 377 +++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 498 insertions(+), 2 deletions(-) create mode 100644 arm/AsmToJSON.ml create mode 100644 cfrontend/C2CToJSON.ml create mode 100644 ia32/AsmToJSON.ml create mode 100644 powerpc/AsmToJSON.ml diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml new file mode 100644 index 00000000..75724d43 --- /dev/null +++ b/arm/AsmToJSON.ml @@ -0,0 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize powerpc Asm to JSON *) + +(* Dummy function *) + +let p_program oc prog = + () diff --git a/cfrontend/C2CToJSON.ml b/cfrontend/C2CToJSON.ml new file mode 100644 index 00000000..dfcfc3e7 --- /dev/null +++ b/cfrontend/C2CToJSON.ml @@ -0,0 +1,72 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize the C2C information to JSON *) + +open C +open C2C +open Camlcoq +open Printf +open Sections + +let p_list elem oc l = + match l with + | [] -> fprintf oc "null" + | hd::tail -> + output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]" + +let p_int_opt oc = function + | None -> fprintf oc "null" + | Some i -> fprintf oc "%d" i + +let p_access oc ac = + let name = match ac with + | Access_default -> "Default" + | Access_near -> "Near" + | Access_far -> "Far" in + fprintf oc "\"%s\"" name + +let p_loc oc (f,l) = fprintf oc "\"%s,%d\"" f l + +let p_storage oc sto = + let storage = match sto with + | Storage_default -> "Default" + | Storage_extern -> "Extern" + | Storage_static -> "Static" + | Storage_register -> "Register" in + fprintf oc "\"%s\"" storage + +let p_section oc = function + | Section_text -> fprintf oc "{\"Section Name\":\"Text\"}" + | Section_data init -> fprintf oc "{\"Section Name\":\"Data\",\"Init\":%B}" init + | Section_small_data init -> fprintf oc "{\"Section Name\":\"Small Data\",\"Init\":%B}" init + | Section_const init -> fprintf oc "{\"Section Name\":\"Const\",\"Init\":%B}" init + | Section_small_const init -> fprintf oc "{\"Section Name\":\"Small Const\",\"Init\":%B}" init + | Section_string -> fprintf oc "{\"Section Name\":\"String\"}" + | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" + | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" + | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e + | Section_debug_info -> fprintf oc "{\"Section Name\":\"Debug Info\"}" + | Section_debug_abbrev -> fprintf oc "{\"Section Name\":\"Debug Abbreviation\"}" + + +let p_atom_info oc info = + fprintf oc "{\"Storage Class\":%a,\n\"Alignment\":%a,\n\"Sections\":%a,\n\"Access\":%a,\n\"Inline\":%b,\n\"Loc\":%a}" + p_storage info.a_storage p_int_opt info.a_alignment (p_list p_section) info.a_sections + p_access info.a_access info.a_inline p_loc info.a_loc + +let print_decl_atom oc = + let first = ref true in + let sep oc = if !first then first:=false else output_string oc "," in + output_string oc "{\n"; + Hashtbl.iter (fun id info -> fprintf oc "%t\"%s\":%a\n" sep (extern_atom id) p_atom_info info) decl_atom; + output_string oc "}" diff --git a/driver/Driver.ml b/driver/Driver.ml index d225ec4f..5a89d4d4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -155,6 +155,15 @@ let dump_asm asm destfile = output_value oc C2C.decl_atom; close_out oc +let jdump_magic_number = "CompCertJDUMP" ^ Configuration.version + +let dump_jasm asm destfile = + let oc = open_out_bin destfile in + fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a,\n\"C Declaration\":%t}" + jdump_magic_number AsmToJSON.p_program asm C2CToJSON.print_decl_atom; + close_out oc + + (* From CompCert C AST to asm *) let compile_c_ast sourcename csyntax ofile debug = @@ -176,9 +185,12 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> print_error stderr msg; exit 2 in - (* Dump Asm in binary format *) + (* Dump Asm in binary and JSON format *) if !option_sdump then - dump_asm asm (output_filename sourcename ".c" ".sdump"); + begin + dump_asm asm (output_filename sourcename ".c" ".sdump"); + dump_jasm asm (output_filename sourcename ".c" ".json") + end; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; diff --git a/ia32/AsmToJSON.ml b/ia32/AsmToJSON.ml new file mode 100644 index 00000000..de39cb9d --- /dev/null +++ b/ia32/AsmToJSON.ml @@ -0,0 +1,17 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize powerpc Asm to JSON *) + +(* Dummy function *) +let p_program oc prog = + () diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml new file mode 100644 index 00000000..0a5e6778 --- /dev/null +++ b/powerpc/AsmToJSON.ml @@ -0,0 +1,377 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize powerpc Asm to JSON *) + +open Asm +open AST +open BinNums +open Camlcoq +open Printf + +let p_ireg oc = function + | GPR0 -> fprintf oc "{\"Register\":\"GPR0\"}" + | GPR1 -> fprintf oc "{\"Register\":\"GPR1\"}" + | GPR2 -> fprintf oc "{\"Register\":\"GPR2\"}" + | GPR3 -> fprintf oc "{\"Register\":\"GPR3\"}" + | GPR4 -> fprintf oc "{\"Register\":\"GPR4\"}" + | GPR5 -> fprintf oc "{\"Register\":\"GPR5\"}" + | GPR6 -> fprintf oc "{\"Register\":\"GPR6\"}" + | GPR7 -> fprintf oc "{\"Register\":\"GPR7\"}" + | GPR8 -> fprintf oc "{\"Register\":\"GPR8\"}" + | GPR9 -> fprintf oc "{\"Register\":\"GPR9\"}" + | GPR10 -> fprintf oc "{\"Register\":\"GPR10\"}" + | GPR11 -> fprintf oc "{\"Register\":\"GPR11\"}" + | GPR12 -> fprintf oc "{\"Register\":\"GPR12\"}" + | GPR13 -> fprintf oc "{\"Register\":\"GPR13\"}" + | GPR14 -> fprintf oc "{\"Register\":\"GPR14\"}" + | GPR15 -> fprintf oc "{\"Register\":\"GPR15\"}" + | GPR16 -> fprintf oc "{\"Register\":\"GPR16\"}" + | GPR17 -> fprintf oc "{\"Register\":\"GPR17\"}" + | GPR18 -> fprintf oc "{\"Register\":\"GPR18\"}" + | GPR19 -> fprintf oc "{\"Register\":\"GPR19\"}" + | GPR20 -> fprintf oc "{\"Register\":\"GPR20\"}" + | GPR21 -> fprintf oc "{\"Register\":\"GPR21\"}" + | GPR22 -> fprintf oc "{\"Register\":\"GPR22\"}" + | GPR23 -> fprintf oc "{\"Register\":\"GPR23\"}" + | GPR24 -> fprintf oc "{\"Register\":\"GPR24\"}" + | GPR25 -> fprintf oc "{\"Register\":\"GPR25\"}" + | GPR26 -> fprintf oc "{\"Register\":\"GPR26\"}" + | GPR27 -> fprintf oc "{\"Register\":\"GPR27\"}" + | GPR28 -> fprintf oc "{\"Register\":\"GPR28\"}" + | GPR29 -> fprintf oc "{\"Register\":\"GPR29\"}" + | GPR30 -> fprintf oc "{\"Register\":\"GPR30\"}" + | GPR31 -> fprintf oc "{\"Register\":\"GPR31\"}" + +let p_freg oc = function + | FPR0 -> fprintf oc "{\"Register\":\"FPR0\"}" + | FPR1 -> fprintf oc "{\"Register\":\"FPR1\"}" + | FPR2 -> fprintf oc "{\"Register\":\"FPR2\"}" + | FPR3 -> fprintf oc "{\"Register\":\"FPR3\"}" + | FPR4 -> fprintf oc "{\"Register\":\"FPR4\"}" + | FPR5 -> fprintf oc "{\"Register\":\"FPR5\"}" + | FPR6 -> fprintf oc "{\"Register\":\"FPR6\"}" + | FPR7 -> fprintf oc "{\"Register\":\"FPR7\"}" + | FPR8 -> fprintf oc "{\"Register\":\"FPR8\"}" + | FPR9 -> fprintf oc "{\"Register\":\"FPR9\"}" + | FPR10 -> fprintf oc "{\"Register\":\"FPR10\"}" + | FPR11 -> fprintf oc "{\"Register\":\"FPR11\"}" + | FPR12 -> fprintf oc "{\"Register\":\"FPR12\"}" + | FPR13 -> fprintf oc "{\"Register\":\"FPR13\"}" + | FPR14 -> fprintf oc "{\"Register\":\"FPR14\"}" + | FPR15 -> fprintf oc "{\"Register\":\"FPR15\"}" + | FPR16 -> fprintf oc "{\"Register\":\"FPR16\"}" + | FPR17 -> fprintf oc "{\"Register\":\"FPR17\"}" + | FPR18 -> fprintf oc "{\"Register\":\"FPR18\"}" + | FPR19 -> fprintf oc "{\"Register\":\"FPR19\"}" + | FPR20 -> fprintf oc "{\"Register\":\"FPR20\"}" + | FPR21 -> fprintf oc "{\"Register\":\"FPR21\"}" + | FPR22 -> fprintf oc "{\"Register\":\"FPR22\"}" + | FPR23 -> fprintf oc "{\"Register\":\"FPR23\"}" + | FPR24 -> fprintf oc "{\"Register\":\"FPR24\"}" + | FPR25 -> fprintf oc "{\"Register\":\"FPR25\"}" + | FPR26 -> fprintf oc "{\"Register\":\"FPR26\"}" + | FPR27 -> fprintf oc "{\"Register\":\"FPR27\"}" + | FPR28 -> fprintf oc "{\"Register\":\"FPR28\"}" + | FPR29 -> fprintf oc "{\"Register\":\"FPR29\"}" + | FPR30 -> fprintf oc "{\"Register\":\"FPR30\"}" + | FPR31 -> fprintf oc "{\"Register\":\"FPR31\"}" + +let p_preg oc = function + | IR ir -> p_ireg oc ir + | FR fr -> p_freg oc fr + | PC -> fprintf oc "{\"Register\":\"PC\"}" + | LR -> fprintf oc "{\"Register\":\"LR\"}" + | CTR -> fprintf oc "{\"Register\":\"CTR\"}" + | CARRY -> fprintf oc "{\"Register\":\"CARRY\"}" + | CR0_0 -> fprintf oc "{\"Register\":\"CR0_0\"}" + | CR0_1 -> fprintf oc "{\"Register\":\"CR0_1\"}" + | CR0_2 -> fprintf oc "{\"Register\":\"CR0_2\"}" + | CR0_3 -> fprintf oc "{\"Register\":\"CR0_3\"}" + | CR1_2 -> fprintf oc "{\"Register\":\"CR1_2\"}" + +let p_atom oc a = fprintf oc "\"%s\"" (extern_atom a) + +let p_int oc i = fprintf oc "%ld" (camlint_of_coqint i) +let p_int64 oc i = fprintf oc "%Ld" (camlint64_of_coqint i) +let p_float32 oc f = fprintf oc "%f" (camlfloat_of_coqfloat32 f) +let p_float64 oc f = fprintf oc "%f" (camlfloat_of_coqfloat f) +let p_z oc z = fprintf oc "%s" (Z.to_string z) + + +let p_constant oc = function + | Cint i -> fprintf oc "{\"Integer\":%a}" p_int i + | Csymbol_low (i,c) -> fprintf oc "{\"Symbol_low\":[%a,%a]}" p_atom i p_int c + | Csymbol_high (i,c) -> fprintf oc "{\"Symbol_high\":[%a,%a]}" p_atom i p_int c + | Csymbol_sda (i,c) -> fprintf oc "{\"Symbol_sda\":[%a,%a]}" p_atom i p_int c + | Csymbol_rel_low (i,c) -> fprintf oc "{\"Symbol_rel_low\":[%a,%a]}" p_atom i p_int c + | Csymbol_rel_high (i,c) -> fprintf oc "{\"Symbol_rel_high\":[%a,%a]}" p_atom i p_int c + +let p_crbit oc c = + let number = match c with + | CRbit_0 -> 0 + | CRbit_1 -> 1 + | CRbit_2 -> 2 + | CRbit_3 -> 3 + | CRbit_6 -> 6 in + fprintf oc "{\"CRbit\":%d}" number + + +let p_label oc l = fprintf oc "{\"Label:\"%ld}" (P.to_int32 l) + +let p_list elem oc l = + match l with + | [] -> fprintf oc "null" + | hd::tail -> + output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]" + +let p_list_cont elem oc l = + match l with + | [] -> () + | _ -> + List.iter (fprintf oc ",%a" elem) l + +let p_typ oc = function + | Tint -> fprintf oc "\"Tint\"" + | Tfloat -> fprintf oc "\"Tfloat\"" + | Tlong -> fprintf oc "\"Tlong\"" + | Tsingle -> fprintf oc "\"Tsingle\"" + | Tany32 -> fprintf oc "\"Tany32\"" + | Tany64 -> fprintf oc "\"Tany64\"" + +let p_signature oc signature = + let p_result oc = function + | None -> fprintf oc "null" + | Some e -> p_typ oc e in + let p_calling_convention oc cc = + fprintf oc "{\"Vararg\":%B,\"Structreg\":%B}" cc.cc_vararg cc.cc_structret + in + fprintf oc "{\"Sig_args\":%a,\"Sig_res\":%a,\"Sig_cc\":%a}" + (p_list p_typ) signature.sig_args + p_result signature.sig_res + p_calling_convention signature.sig_cc + +let p_memory_chunk oc = function + | Mint8signed -> fprintf oc "\"Mint8signed\"" + | Mint8unsigned -> fprintf oc "\"Mint8unsigned\"" + | Mint16signed -> fprintf oc "\"Mint16signed\"" + | Mint16unsigned -> fprintf oc "\"Mint16unsigned\"" + | Mint32 -> fprintf oc "\"Mint32\"" + | Mint64 -> fprintf oc "\"Mint64\"" + | Mfloat32 -> fprintf oc "\"Mfloat32\"" + | Mfloat64 -> fprintf oc "\"Mfloat64\"" + | Many32 -> fprintf oc "\"Many32\"" + | Many64 -> fprintf oc "\"Many64\"" + + +let p_external_fun oc = function + | EF_external (i,s) -> fprintf oc "{\"Extern\":%a,\"Sig\":%a}" p_atom i p_signature s + | EF_builtin (i,s) -> fprintf oc "{\"Builtin\":%a,\"Sig\":%a}" p_atom i p_signature s + | EF_vload chunk -> fprintf oc "{\"Vload\":%a}" p_memory_chunk chunk + | EF_vstore chunk -> fprintf oc "{\"Vstore\":%a}" p_memory_chunk chunk + | EF_vload_global (chunk,indent,ic) -> fprintf oc "{\"Vload_global\":[%a,%a,%a]}" p_memory_chunk chunk p_atom indent p_int ic + | EF_vstore_global (chunk,indent,ic) -> fprintf oc "{\"Vstore_global\":[%a,%a,%a]}" p_memory_chunk chunk p_atom indent p_int ic + | EF_malloc -> fprintf oc "{\"Malloc\":null}" + | EF_free -> fprintf oc "{\"Free\":null}" + | EF_memcpy (sz,al) -> fprintf oc "{\"Memcpy\":[%a,%a]}" p_int sz p_int al + | EF_annot (i,t) -> fprintf oc "{\"Annot\":[%a%a]}" p_atom i (p_list_cont p_typ) t + | EF_annot_val (i,t) -> fprintf oc "{\"Annot_val\":[%a,%a]}" p_atom i p_typ t + | EF_inline_asm (i,s,il) -> fprintf oc "{\"Inline_asm\":[%a%a,%a]}" p_atom i p_signature s (p_list_cont p_atom) il + +let rec p_annot_arg elem oc = function + | AA_base e -> fprintf oc "{\"AA_base\":%a}" elem e + | AA_int i -> fprintf oc "{\"AA_int\":%a}" p_int i + | AA_long l -> fprintf oc "{\"AA_long\":%a}" p_int64 l + | AA_float f -> fprintf oc "{\"AA_float\":%a}" p_float64 f + | AA_single f -> fprintf oc "{\"AA_single\":%a}" p_float32 f + | AA_loadstack (c,i) -> fprintf oc "{\"AA_loadstack\":[%a,%a]}" p_memory_chunk c p_int i + | AA_addrstack i -> fprintf oc "{\"AA_addrstack\":%a}" p_int i + | AA_loadglobal (m,ident,i) -> fprintf oc "{\"AA_loadglobal\":[%a,%a,%a]}" p_memory_chunk m p_atom ident p_int i + | AA_addrglobal (ident,i) -> fprintf oc "{\"AA_addrgloabl\":[%a,%a]}" p_atom ident p_int i + | AA_longofwords (a,b) -> fprintf oc "{\"AA_longofwords\":[%a,%a]}" (p_annot_arg elem) a (p_annot_arg elem) b + +let p_instruction oc ic = + output_string oc "\n"; + match ic with + | Padd (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Padd\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Paddc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Paddc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Padde (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Padde\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Paddi (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddi\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Paddic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Paddis (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pallocframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pallocframe\",\"Args\":[%a,%a]}" p_z c p_int i + | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pandis_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandis_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l + | Pbctr s -> fprintf oc "{\"Instruction Name\":\"Pbctr\",\"Args\":[%a]}" p_signature s + | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[%a]}" p_signature s + | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l + | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l + | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a,%a]}" p_atom i p_signature s + | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a,%a]}" p_atom i p_signature s + | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":null}" + | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l + | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a,%a]}" p_ireg i (p_list p_label) lb + | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c + | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcmpwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmpwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c + | Pcntlz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":null}" + | Peqv (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Peqv\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pextsb (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsb\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pfreeframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pfreeframe\",\"Args\":[%ld,%a]}" (Z.to_int32 c) p_int i + | Pfabs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabss\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfadds (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadds\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfcmpu (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcmpu\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfcti (ir,fr) -> fprintf oc "{\"Instruction Name\":\"Pfcti\",\"Args\":[%a,%a]}" p_ireg ir p_freg fr + | Pfctiw (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiw\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfctiwz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiwz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfdiv (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdiv\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfdivs (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdivs\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfmake (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pfmake\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Pfmr (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfmr\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfmul (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfmul\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfmuls(fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfmuls\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfneg (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfneg\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfnegs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfnegs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfrsp (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfrsp\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfxdp (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfxdp\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfsub (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfsub\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfsubs (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfsubs\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfmadd (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmadd\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfmsub (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmsub\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfnmadd (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmadd\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfnmsub (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfnmsub\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfsqrt (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrt\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":null}" + | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plfd (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Plfdx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Plfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plha (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plha\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plhax (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhax\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plhbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plhz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plhz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plhzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float64 fc + | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float64 fc + | Plwz (ir1,ic,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant ic p_ireg ir2 + | Plwzu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwzu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plwzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plwz_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmfcr ir -> fprintf oc "{\"Instruction Name\":\"Pmfcr\",\"Args\":[%a]}" p_ireg ir + | Pmfcrbit (ir,crb) -> fprintf oc "{\"Instruction Name\":\"Pmfcrbit\",\"Args\":[%a,%a]}" p_ireg ir p_crbit crb + | Pmflr ir -> fprintf oc "{\"Instruction Name\":\"Pmflr\",\"Args\":[%a]}" p_ireg ir + | Pmr (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pmr\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pmtctr ir -> fprintf oc "{\"Instruction Name\":\"Pmtctr\",\"Args\":[%a]}" p_ireg ir + | Pmtlr ir -> fprintf oc "{\"Instruction Name\":\"Pmtlr\",\"Args\":[%a]}" p_ireg ir + | Pmulli (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pmulli\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmulhwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pnand (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pnand\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pnor (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pnor\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Por (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Por\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Porc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Porc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Poris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Poris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Prlwinm (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwinm\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int ic1 p_int ic2 + | Prlwimi (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwimi\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int ic1 p_int ic2 + | Pslw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pslw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psraw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psraw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psrawi (ir1,ir2,ic) -> fprintf oc "{\"Instruction Name\":\"Psrawi\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int ic + | Psrw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstb (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstfd (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfdx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfdx_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Pstfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Psth (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Psth\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Psthx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psthx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psthbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psthbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstw (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstwu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstwx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwxu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwxu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstw_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstw_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psubfe (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psubfze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Psubfic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Psubfic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Psync -> fprintf oc "{\"Instruction Name\":\"Psync\",\"Args\":null}" + | Ptrap -> fprintf oc "{\"Instruction Name\":\"Ptrap\",\"Args\":null}" + | Pxor (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pxor\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pxori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pxoris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxoris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Plabel l -> fprintf oc "{\"Instruction Name\":\"Plabel\",\"Args\":[%a]}" p_label l + | Pbuiltin (ef,args1,args2) -> fprintf oc "{\"Instruction Name\":\"Pbuiltin\",\"Args\":[%a,%a,%a]}" p_external_fun ef (p_list p_preg) args1 (p_list p_preg) args2 + | Pannot (ef,anargs) -> fprintf oc "{\"Instruction Name\":\"Pannot\",\"Args\":[%a,%a]}" p_external_fun ef (p_list (p_annot_arg p_preg)) anargs + | Pcfi_adjust ic -> fprintf oc "{\"Instruction Name\":\"Pcfi_adjust\",\"Args\":[%a]}" p_int ic + | Pcfi_rel_offset ic -> fprintf oc "{\"Instruction Name\":\"Pcfi_rel_offset\",\"Args\":[%a]}" p_int ic + +let p_fundef oc name = function + | Internal f -> fprintf oc "{\"Fun_name\":%a,\n\"Fun_sig\":%a,\n\"Fun_code\":%a}" + p_atom name + p_signature f.fn_sig (p_list p_instruction) f.fn_code + | External f ->fprintf oc "{\"Ext_name\":%a,\"Ext_fun\":%a}" p_atom name p_external_fun f + +let p_init_data oc = function + | Init_int8 ic -> fprintf oc "{\"Init_int8\":%a}" p_int ic + | Init_int16 ic -> fprintf oc "{\"Init_int16\":%a}" p_int ic + | Init_int32 ic -> fprintf oc "{\"Init_int32\":%a}" p_int ic + | Init_int64 lc -> fprintf oc "{\"Init_int64\":%a}" p_int64 lc + | Init_float32 f -> fprintf oc "{\"Init_float32\":%a}" p_float32 f + | Init_float64 f -> fprintf oc "{\"Init_float64\":%a}" p_float64 f + | Init_space z -> fprintf oc "{\"Init_space\":%a}" p_z z + | Init_addrof (p,i) -> fprintf oc "{\"Init_addrof\":[%a,%a]}" p_atom p p_int i + +let p_prog_def oc (ident,def) = + output_string oc "\n"; + match def with + | Gfun f -> p_fundef oc ident f + | Gvar v -> fprintf oc "{\"Var_name\":%a,\"Var_init\":%a,\"Var_readonly\":%B,\"Var_volatile\":%B}" + p_atom ident (p_list p_init_data) v.gvar_init v.gvar_readonly v.gvar_volatile + +let p_program oc prog = + fprintf oc "{\"Prog_efs\":%a,\n\"Prog_public\":%a,\n\"Prog_main\":%a}" + (p_list p_prog_def) prog.prog_defs + (p_list (fun oc -> fprintf oc "\n%a" p_atom)) prog.prog_public + p_atom prog.prog_main -- cgit From fff918a39813598c79aaf658fce753b86aac8af4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 5 May 2015 17:16:32 +0200 Subject: Removed printing of information for internals and externals that should be folded away prior. --- powerpc/AsmToJSON.ml | 77 +++++++++++++++++++--------------------------------- 1 file changed, 28 insertions(+), 49 deletions(-) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 0a5e6778..285606b5 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -160,45 +160,6 @@ let p_signature oc signature = p_result signature.sig_res p_calling_convention signature.sig_cc -let p_memory_chunk oc = function - | Mint8signed -> fprintf oc "\"Mint8signed\"" - | Mint8unsigned -> fprintf oc "\"Mint8unsigned\"" - | Mint16signed -> fprintf oc "\"Mint16signed\"" - | Mint16unsigned -> fprintf oc "\"Mint16unsigned\"" - | Mint32 -> fprintf oc "\"Mint32\"" - | Mint64 -> fprintf oc "\"Mint64\"" - | Mfloat32 -> fprintf oc "\"Mfloat32\"" - | Mfloat64 -> fprintf oc "\"Mfloat64\"" - | Many32 -> fprintf oc "\"Many32\"" - | Many64 -> fprintf oc "\"Many64\"" - - -let p_external_fun oc = function - | EF_external (i,s) -> fprintf oc "{\"Extern\":%a,\"Sig\":%a}" p_atom i p_signature s - | EF_builtin (i,s) -> fprintf oc "{\"Builtin\":%a,\"Sig\":%a}" p_atom i p_signature s - | EF_vload chunk -> fprintf oc "{\"Vload\":%a}" p_memory_chunk chunk - | EF_vstore chunk -> fprintf oc "{\"Vstore\":%a}" p_memory_chunk chunk - | EF_vload_global (chunk,indent,ic) -> fprintf oc "{\"Vload_global\":[%a,%a,%a]}" p_memory_chunk chunk p_atom indent p_int ic - | EF_vstore_global (chunk,indent,ic) -> fprintf oc "{\"Vstore_global\":[%a,%a,%a]}" p_memory_chunk chunk p_atom indent p_int ic - | EF_malloc -> fprintf oc "{\"Malloc\":null}" - | EF_free -> fprintf oc "{\"Free\":null}" - | EF_memcpy (sz,al) -> fprintf oc "{\"Memcpy\":[%a,%a]}" p_int sz p_int al - | EF_annot (i,t) -> fprintf oc "{\"Annot\":[%a%a]}" p_atom i (p_list_cont p_typ) t - | EF_annot_val (i,t) -> fprintf oc "{\"Annot_val\":[%a,%a]}" p_atom i p_typ t - | EF_inline_asm (i,s,il) -> fprintf oc "{\"Inline_asm\":[%a%a,%a]}" p_atom i p_signature s (p_list_cont p_atom) il - -let rec p_annot_arg elem oc = function - | AA_base e -> fprintf oc "{\"AA_base\":%a}" elem e - | AA_int i -> fprintf oc "{\"AA_int\":%a}" p_int i - | AA_long l -> fprintf oc "{\"AA_long\":%a}" p_int64 l - | AA_float f -> fprintf oc "{\"AA_float\":%a}" p_float64 f - | AA_single f -> fprintf oc "{\"AA_single\":%a}" p_float32 f - | AA_loadstack (c,i) -> fprintf oc "{\"AA_loadstack\":[%a,%a]}" p_memory_chunk c p_int i - | AA_addrstack i -> fprintf oc "{\"AA_addrstack\":%a}" p_int i - | AA_loadglobal (m,ident,i) -> fprintf oc "{\"AA_loadglobal\":[%a,%a,%a]}" p_memory_chunk m p_atom ident p_int i - | AA_addrglobal (ident,i) -> fprintf oc "{\"AA_addrgloabl\":[%a,%a]}" p_atom ident p_int i - | AA_longofwords (a,b) -> fprintf oc "{\"AA_longofwords\":[%a,%a]}" (p_annot_arg elem) a (p_annot_arg elem) b - let p_instruction oc ic = output_string oc "\n"; match ic with @@ -342,16 +303,25 @@ let p_instruction oc ic = | Pxori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pxoris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxoris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Plabel l -> fprintf oc "{\"Instruction Name\":\"Plabel\",\"Args\":[%a]}" p_label l - | Pbuiltin (ef,args1,args2) -> fprintf oc "{\"Instruction Name\":\"Pbuiltin\",\"Args\":[%a,%a,%a]}" p_external_fun ef (p_list p_preg) args1 (p_list p_preg) args2 - | Pannot (ef,anargs) -> fprintf oc "{\"Instruction Name\":\"Pannot\",\"Args\":[%a,%a]}" p_external_fun ef (p_list (p_annot_arg p_preg)) anargs - | Pcfi_adjust ic -> fprintf oc "{\"Instruction Name\":\"Pcfi_adjust\",\"Args\":[%a]}" p_int ic - | Pcfi_rel_offset ic -> fprintf oc "{\"Instruction Name\":\"Pcfi_rel_offset\",\"Args\":[%a]}" p_int ic + | Pbuiltin (ef,args1,args2) -> + begin match ef with + | EF_inline_asm (i,s,il) -> + fprintf oc "{\"Instruction Name\":\"Inline_asm\",\"Args\":[%a,%a%a%a%a]}" p_atom i p_signature s (p_list_cont p_atom) il + (p_list_cont p_preg) args1 (p_list_cont p_preg) args2 + | _ -> (* Should all be folded away *) + assert false + end + | Pannot _ -> () (* We do not check the annotations *) + | Pcfi_adjust _ -> () (* Only debug relevant *) + | Pcfi_rel_offset _ -> () (* Only debug relevant *) let p_fundef oc name = function - | Internal f -> fprintf oc "{\"Fun_name\":%a,\n\"Fun_sig\":%a,\n\"Fun_code\":%a}" + | Internal f -> + let instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + fprintf oc "{\"Fun_name\":%a,\n\"Fun_sig\":%a,\n\"Fun_code\":%a}" p_atom name - p_signature f.fn_sig (p_list p_instruction) f.fn_code - | External f ->fprintf oc "{\"Ext_name\":%a,\"Ext_fun\":%a}" p_atom name p_external_fun f + p_signature f.fn_sig (p_list p_instruction) instr + | External _ ->() (* Is of no interest *) let p_init_data oc = function | Init_int8 ic -> fprintf oc "{\"Init_int8\":%a}" p_int ic @@ -370,8 +340,17 @@ let p_prog_def oc (ident,def) = | Gvar v -> fprintf oc "{\"Var_name\":%a,\"Var_init\":%a,\"Var_readonly\":%B,\"Var_volatile\":%B}" p_atom ident (p_list p_init_data) v.gvar_init v.gvar_readonly v.gvar_volatile +let re_builtin = Str.regexp "__builtin_\\|__i64_\\|__compcert_" + +let p_public oc p = + let p = List.map extern_atom p in + let p = List.filter (fun s -> + not (Str.string_match re_builtin s 0)) p in + (p_list (fun oc s -> fprintf oc "\n\"%s\"" s)) oc p + let p_program oc prog = - fprintf oc "{\"Prog_efs\":%a,\n\"Prog_public\":%a,\n\"Prog_main\":%a}" - (p_list p_prog_def) prog.prog_defs - (p_list (fun oc -> fprintf oc "\n%a" p_atom)) prog.prog_public + let prog_defs = List.filter (function _,Gfun (External _) -> false | _ -> true) prog.prog_defs in + fprintf oc "{\"Prog_defs\":%a,\n\"Prog_public\":%a,\n\"Prog_main\":%a}" + (p_list p_prog_def) prog_defs + p_public prog.prog_public p_atom prog.prog_main -- cgit From 4705c24a336d831dd5afb02288fda17c0093c438 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 6 May 2015 15:10:39 +0200 Subject: Moved the information needed from the atoms to the ASM printer and removed unused information from the json dump. --- cfrontend/C2CToJSON.ml | 72 ------------------------------------------------ driver/Driver.ml | 4 +-- powerpc/AsmToJSON.ml | 74 ++++++++++++++++++++++++++++++++------------------ 3 files changed, 50 insertions(+), 100 deletions(-) delete mode 100644 cfrontend/C2CToJSON.ml diff --git a/cfrontend/C2CToJSON.ml b/cfrontend/C2CToJSON.ml deleted file mode 100644 index dfcfc3e7..00000000 --- a/cfrontend/C2CToJSON.ml +++ /dev/null @@ -1,72 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) -(* is distributed under the terms of the INRIA Non-Commercial *) -(* License Agreement. *) -(* *) -(* *********************************************************************) - -(* Simple functions to serialize the C2C information to JSON *) - -open C -open C2C -open Camlcoq -open Printf -open Sections - -let p_list elem oc l = - match l with - | [] -> fprintf oc "null" - | hd::tail -> - output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]" - -let p_int_opt oc = function - | None -> fprintf oc "null" - | Some i -> fprintf oc "%d" i - -let p_access oc ac = - let name = match ac with - | Access_default -> "Default" - | Access_near -> "Near" - | Access_far -> "Far" in - fprintf oc "\"%s\"" name - -let p_loc oc (f,l) = fprintf oc "\"%s,%d\"" f l - -let p_storage oc sto = - let storage = match sto with - | Storage_default -> "Default" - | Storage_extern -> "Extern" - | Storage_static -> "Static" - | Storage_register -> "Register" in - fprintf oc "\"%s\"" storage - -let p_section oc = function - | Section_text -> fprintf oc "{\"Section Name\":\"Text\"}" - | Section_data init -> fprintf oc "{\"Section Name\":\"Data\",\"Init\":%B}" init - | Section_small_data init -> fprintf oc "{\"Section Name\":\"Small Data\",\"Init\":%B}" init - | Section_const init -> fprintf oc "{\"Section Name\":\"Const\",\"Init\":%B}" init - | Section_small_const init -> fprintf oc "{\"Section Name\":\"Small Const\",\"Init\":%B}" init - | Section_string -> fprintf oc "{\"Section Name\":\"String\"}" - | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" - | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" - | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e - | Section_debug_info -> fprintf oc "{\"Section Name\":\"Debug Info\"}" - | Section_debug_abbrev -> fprintf oc "{\"Section Name\":\"Debug Abbreviation\"}" - - -let p_atom_info oc info = - fprintf oc "{\"Storage Class\":%a,\n\"Alignment\":%a,\n\"Sections\":%a,\n\"Access\":%a,\n\"Inline\":%b,\n\"Loc\":%a}" - p_storage info.a_storage p_int_opt info.a_alignment (p_list p_section) info.a_sections - p_access info.a_access info.a_inline p_loc info.a_loc - -let print_decl_atom oc = - let first = ref true in - let sep oc = if !first then first:=false else output_string oc "," in - output_string oc "{\n"; - Hashtbl.iter (fun id info -> fprintf oc "%t\"%s\":%a\n" sep (extern_atom id) p_atom_info info) decl_atom; - output_string oc "}" diff --git a/driver/Driver.ml b/driver/Driver.ml index 5a89d4d4..04dec9db 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -159,8 +159,8 @@ let jdump_magic_number = "CompCertJDUMP" ^ Configuration.version let dump_jasm asm destfile = let oc = open_out_bin destfile in - fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a,\n\"C Declaration\":%t}" - jdump_magic_number AsmToJSON.p_program asm C2CToJSON.print_decl_atom; + fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a}" + jdump_magic_number AsmToJSON.p_program asm; close_out oc diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 285606b5..be20e14a 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -15,8 +15,10 @@ open Asm open AST open BinNums +open C2C open Camlcoq open Printf +open Sections let p_ireg oc = function | GPR0 -> fprintf oc "{\"Register\":\"GPR0\"}" @@ -315,14 +317,42 @@ let p_instruction oc ic = | Pcfi_adjust _ -> () (* Only debug relevant *) | Pcfi_rel_offset _ -> () (* Only debug relevant *) -let p_fundef oc name = function - | Internal f -> - let instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in - fprintf oc "{\"Fun_name\":%a,\n\"Fun_sig\":%a,\n\"Fun_code\":%a}" - p_atom name - p_signature f.fn_sig (p_list p_instruction) instr - | External _ ->() (* Is of no interest *) +let p_storage oc sto = + let storage = match sto with + | C.Storage_default -> "Default" + | C.Storage_extern -> "Extern" + | C.Storage_static -> "Static" + | C.Storage_register -> "Register" in + fprintf oc "\"%s\"" storage + +let p_section oc = function + | Section_text -> fprintf oc "{\"Section Name\":\"Text\"}" + | Section_data init -> fprintf oc "{\"Section Name\":\"Data\",\"Init\":%B}" init + | Section_small_data init -> fprintf oc "{\"Section Name\":\"Small Data\",\"Init\":%B}" init + | Section_const init -> fprintf oc "{\"Section Name\":\"Const\",\"Init\":%B}" init + | Section_small_const init -> fprintf oc "{\"Section Name\":\"Small Const\",\"Init\":%B}" init + | Section_string -> fprintf oc "{\"Section Name\":\"String\"}" + | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" + | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" + | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e + | Section_debug_info -> fprintf oc "{\"Section Name\":\"Debug Info\"}" + | Section_debug_abbrev -> fprintf oc "{\"Section Name\":\"Debug Abbreviation\"}" + +let p_int_opt oc = function + | None -> fprintf oc "null" + | Some i -> fprintf oc "%d" i + +let p_atom_info oc ident = + let info = Hashtbl.find C2C.decl_atom ident in + fprintf oc "{\"Storage Class\":%a,\n\"Alignment\":%a,\n\"Sections\":%a,\n\"Inline\":%B}" + p_storage info.a_storage p_int_opt info.a_alignment (p_list p_section) info.a_sections + info.a_inline +let p_fundef oc (name,f) = + let instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + fprintf oc "{\"Fun Name\":%a,\n\"Fun Sig\":%a,\n\"Atom info\":%a,\n\"Fun Code\":%a}\n" + p_atom name p_signature f.fn_sig p_atom_info name (p_list p_instruction) instr + let p_init_data oc = function | Init_int8 ic -> fprintf oc "{\"Init_int8\":%a}" p_int ic | Init_int16 ic -> fprintf oc "{\"Init_int16\":%a}" p_int ic @@ -333,24 +363,16 @@ let p_init_data oc = function | Init_space z -> fprintf oc "{\"Init_space\":%a}" p_z z | Init_addrof (p,i) -> fprintf oc "{\"Init_addrof\":[%a,%a]}" p_atom p p_int i -let p_prog_def oc (ident,def) = - output_string oc "\n"; - match def with - | Gfun f -> p_fundef oc ident f - | Gvar v -> fprintf oc "{\"Var_name\":%a,\"Var_init\":%a,\"Var_readonly\":%B,\"Var_volatile\":%B}" - p_atom ident (p_list p_init_data) v.gvar_init v.gvar_readonly v.gvar_volatile - -let re_builtin = Str.regexp "__builtin_\\|__i64_\\|__compcert_" - -let p_public oc p = - let p = List.map extern_atom p in - let p = List.filter (fun s -> - not (Str.string_match re_builtin s 0)) p in - (p_list (fun oc s -> fprintf oc "\n\"%s\"" s)) oc p +let p_vardef oc (ident,v) = + fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\"Atom Info\":%a,\"Var Init\":%a}\n" + p_atom ident v.gvar_readonly v.gvar_volatile p_atom_info ident (p_list p_init_data) v.gvar_init let p_program oc prog = - let prog_defs = List.filter (function _,Gfun (External _) -> false | _ -> true) prog.prog_defs in - fprintf oc "{\"Prog_defs\":%a,\n\"Prog_public\":%a,\n\"Prog_main\":%a}" - (p_list p_prog_def) prog_defs - p_public prog.prog_public - p_atom prog.prog_main + let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> + match def with + | Gfun (Internal f) -> vars,(ident,f)::funs + | Gvar v -> (ident,v)::vars,funs + | _ -> vars,funs) ([],[]) prog.prog_defs in + fprintf oc "{\"Global Variables\":%a,\n\"Functions\":%a}" + (p_list p_vardef) prog_vars + (p_list p_fundef) prog_funs -- cgit From 6885cf5c6cf05886a7dd09a3d4bfad079b628376 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 18 May 2015 10:36:18 +0200 Subject: Updated the printing of iniline asm and simplified some structures. --- powerpc/AsmToJSON.ml | 254 ++++++++++++++++++++++++--------------------------- 1 file changed, 118 insertions(+), 136 deletions(-) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index be20e14a..6e71e01a 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -21,102 +21,99 @@ open Printf open Sections let p_ireg oc = function - | GPR0 -> fprintf oc "{\"Register\":\"GPR0\"}" - | GPR1 -> fprintf oc "{\"Register\":\"GPR1\"}" - | GPR2 -> fprintf oc "{\"Register\":\"GPR2\"}" - | GPR3 -> fprintf oc "{\"Register\":\"GPR3\"}" - | GPR4 -> fprintf oc "{\"Register\":\"GPR4\"}" - | GPR5 -> fprintf oc "{\"Register\":\"GPR5\"}" - | GPR6 -> fprintf oc "{\"Register\":\"GPR6\"}" - | GPR7 -> fprintf oc "{\"Register\":\"GPR7\"}" - | GPR8 -> fprintf oc "{\"Register\":\"GPR8\"}" - | GPR9 -> fprintf oc "{\"Register\":\"GPR9\"}" - | GPR10 -> fprintf oc "{\"Register\":\"GPR10\"}" - | GPR11 -> fprintf oc "{\"Register\":\"GPR11\"}" - | GPR12 -> fprintf oc "{\"Register\":\"GPR12\"}" - | GPR13 -> fprintf oc "{\"Register\":\"GPR13\"}" - | GPR14 -> fprintf oc "{\"Register\":\"GPR14\"}" - | GPR15 -> fprintf oc "{\"Register\":\"GPR15\"}" - | GPR16 -> fprintf oc "{\"Register\":\"GPR16\"}" - | GPR17 -> fprintf oc "{\"Register\":\"GPR17\"}" - | GPR18 -> fprintf oc "{\"Register\":\"GPR18\"}" - | GPR19 -> fprintf oc "{\"Register\":\"GPR19\"}" - | GPR20 -> fprintf oc "{\"Register\":\"GPR20\"}" - | GPR21 -> fprintf oc "{\"Register\":\"GPR21\"}" - | GPR22 -> fprintf oc "{\"Register\":\"GPR22\"}" - | GPR23 -> fprintf oc "{\"Register\":\"GPR23\"}" - | GPR24 -> fprintf oc "{\"Register\":\"GPR24\"}" - | GPR25 -> fprintf oc "{\"Register\":\"GPR25\"}" - | GPR26 -> fprintf oc "{\"Register\":\"GPR26\"}" - | GPR27 -> fprintf oc "{\"Register\":\"GPR27\"}" - | GPR28 -> fprintf oc "{\"Register\":\"GPR28\"}" - | GPR29 -> fprintf oc "{\"Register\":\"GPR29\"}" - | GPR30 -> fprintf oc "{\"Register\":\"GPR30\"}" - | GPR31 -> fprintf oc "{\"Register\":\"GPR31\"}" + | GPR0 -> fprintf oc "{\"Register\":\"r0\"}" + | GPR1 -> fprintf oc "{\"Register\":\"r1\"}" + | GPR2 -> fprintf oc "{\"Register\":\"r2\"}" + | GPR3 -> fprintf oc "{\"Register\":\"r3\"}" + | GPR4 -> fprintf oc "{\"Register\":\"r4\"}" + | GPR5 -> fprintf oc "{\"Register\":\"r5\"}" + | GPR6 -> fprintf oc "{\"Register\":\"r6\"}" + | GPR7 -> fprintf oc "{\"Register\":\"r7\"}" + | GPR8 -> fprintf oc "{\"Register\":\"r8\"}" + | GPR9 -> fprintf oc "{\"Register\":\"r9\"}" + | GPR10 -> fprintf oc "{\"Register\":\"r10\"}" + | GPR11 -> fprintf oc "{\"Register\":\"r11\"}" + | GPR12 -> fprintf oc "{\"Register\":\"r12\"}" + | GPR13 -> fprintf oc "{\"Register\":\"r13\"}" + | GPR14 -> fprintf oc "{\"Register\":\"r14\"}" + | GPR15 -> fprintf oc "{\"Register\":\"r15\"}" + | GPR16 -> fprintf oc "{\"Register\":\"r16\"}" + | GPR17 -> fprintf oc "{\"Register\":\"r17\"}" + | GPR18 -> fprintf oc "{\"Register\":\"r18\"}" + | GPR19 -> fprintf oc "{\"Register\":\"r19\"}" + | GPR20 -> fprintf oc "{\"Register\":\"r20\"}" + | GPR21 -> fprintf oc "{\"Register\":\"r21\"}" + | GPR22 -> fprintf oc "{\"Register\":\"r22\"}" + | GPR23 -> fprintf oc "{\"Register\":\"r23\"}" + | GPR24 -> fprintf oc "{\"Register\":\"r24\"}" + | GPR25 -> fprintf oc "{\"Register\":\"r25\"}" + | GPR26 -> fprintf oc "{\"Register\":\"r26\"}" + | GPR27 -> fprintf oc "{\"Register\":\"r27\"}" + | GPR28 -> fprintf oc "{\"Register\":\"r28\"}" + | GPR29 -> fprintf oc "{\"Register\":\"r29\"}" + | GPR30 -> fprintf oc "{\"Register\":\"r30\"}" + | GPR31 -> fprintf oc "{\"Register\":\"r31\"}" let p_freg oc = function - | FPR0 -> fprintf oc "{\"Register\":\"FPR0\"}" - | FPR1 -> fprintf oc "{\"Register\":\"FPR1\"}" - | FPR2 -> fprintf oc "{\"Register\":\"FPR2\"}" - | FPR3 -> fprintf oc "{\"Register\":\"FPR3\"}" - | FPR4 -> fprintf oc "{\"Register\":\"FPR4\"}" - | FPR5 -> fprintf oc "{\"Register\":\"FPR5\"}" - | FPR6 -> fprintf oc "{\"Register\":\"FPR6\"}" - | FPR7 -> fprintf oc "{\"Register\":\"FPR7\"}" - | FPR8 -> fprintf oc "{\"Register\":\"FPR8\"}" - | FPR9 -> fprintf oc "{\"Register\":\"FPR9\"}" - | FPR10 -> fprintf oc "{\"Register\":\"FPR10\"}" - | FPR11 -> fprintf oc "{\"Register\":\"FPR11\"}" - | FPR12 -> fprintf oc "{\"Register\":\"FPR12\"}" - | FPR13 -> fprintf oc "{\"Register\":\"FPR13\"}" - | FPR14 -> fprintf oc "{\"Register\":\"FPR14\"}" - | FPR15 -> fprintf oc "{\"Register\":\"FPR15\"}" - | FPR16 -> fprintf oc "{\"Register\":\"FPR16\"}" - | FPR17 -> fprintf oc "{\"Register\":\"FPR17\"}" - | FPR18 -> fprintf oc "{\"Register\":\"FPR18\"}" - | FPR19 -> fprintf oc "{\"Register\":\"FPR19\"}" - | FPR20 -> fprintf oc "{\"Register\":\"FPR20\"}" - | FPR21 -> fprintf oc "{\"Register\":\"FPR21\"}" - | FPR22 -> fprintf oc "{\"Register\":\"FPR22\"}" - | FPR23 -> fprintf oc "{\"Register\":\"FPR23\"}" - | FPR24 -> fprintf oc "{\"Register\":\"FPR24\"}" - | FPR25 -> fprintf oc "{\"Register\":\"FPR25\"}" - | FPR26 -> fprintf oc "{\"Register\":\"FPR26\"}" - | FPR27 -> fprintf oc "{\"Register\":\"FPR27\"}" - | FPR28 -> fprintf oc "{\"Register\":\"FPR28\"}" - | FPR29 -> fprintf oc "{\"Register\":\"FPR29\"}" - | FPR30 -> fprintf oc "{\"Register\":\"FPR30\"}" - | FPR31 -> fprintf oc "{\"Register\":\"FPR31\"}" + | FPR0 -> fprintf oc "{\"Register\":\"f0\"}" + | FPR1 -> fprintf oc "{\"Register\":\"f1\"}" + | FPR2 -> fprintf oc "{\"Register\":\"f2\"}" + | FPR3 -> fprintf oc "{\"Register\":\"f3\"}" + | FPR4 -> fprintf oc "{\"Register\":\"f4\"}" + | FPR5 -> fprintf oc "{\"Register\":\"f5\"}" + | FPR6 -> fprintf oc "{\"Register\":\"f6\"}" + | FPR7 -> fprintf oc "{\"Register\":\"f7\"}" + | FPR8 -> fprintf oc "{\"Register\":\"f8\"}" + | FPR9 -> fprintf oc "{\"Register\":\"f9\"}" + | FPR10 -> fprintf oc "{\"Register\":\"f10\"}" + | FPR11 -> fprintf oc "{\"Register\":\"f11\"}" + | FPR12 -> fprintf oc "{\"Register\":\"f12\"}" + | FPR13 -> fprintf oc "{\"Register\":\"f13\"}" + | FPR14 -> fprintf oc "{\"Register\":\"f14\"}" + | FPR15 -> fprintf oc "{\"Register\":\"f15\"}" + | FPR16 -> fprintf oc "{\"Register\":\"f16\"}" + | FPR17 -> fprintf oc "{\"Register\":\"f17\"}" + | FPR18 -> fprintf oc "{\"Register\":\"f18\"}" + | FPR19 -> fprintf oc "{\"Register\":\"f19\"}" + | FPR20 -> fprintf oc "{\"Register\":\"f20\"}" + | FPR21 -> fprintf oc "{\"Register\":\"f21\"}" + | FPR22 -> fprintf oc "{\"Register\":\"f22\"}" + | FPR23 -> fprintf oc "{\"Register\":\"f23\"}" + | FPR24 -> fprintf oc "{\"Register\":\"f24\"}" + | FPR25 -> fprintf oc "{\"Register\":\"f25\"}" + | FPR26 -> fprintf oc "{\"Register\":\"f26\"}" + | FPR27 -> fprintf oc "{\"Register\":\"f27\"}" + | FPR28 -> fprintf oc "{\"Register\":\"f28\"}" + | FPR29 -> fprintf oc "{\"Register\":\"f29\"}" + | FPR30 -> fprintf oc "{\"Register\":\"f30\"}" + | FPR31 -> fprintf oc "{\"Register\":\"f31\"}" let p_preg oc = function | IR ir -> p_ireg oc ir | FR fr -> p_freg oc fr - | PC -> fprintf oc "{\"Register\":\"PC\"}" - | LR -> fprintf oc "{\"Register\":\"LR\"}" - | CTR -> fprintf oc "{\"Register\":\"CTR\"}" - | CARRY -> fprintf oc "{\"Register\":\"CARRY\"}" - | CR0_0 -> fprintf oc "{\"Register\":\"CR0_0\"}" - | CR0_1 -> fprintf oc "{\"Register\":\"CR0_1\"}" - | CR0_2 -> fprintf oc "{\"Register\":\"CR0_2\"}" - | CR0_3 -> fprintf oc "{\"Register\":\"CR0_3\"}" - | CR1_2 -> fprintf oc "{\"Register\":\"CR1_2\"}" + | _ -> assert false (* This registers should not be used. *) let p_atom oc a = fprintf oc "\"%s\"" (extern_atom a) +let p_atom_constant oc a = fprintf oc "{\"Atom\":%a}" p_atom a + let p_int oc i = fprintf oc "%ld" (camlint_of_coqint i) let p_int64 oc i = fprintf oc "%Ld" (camlint64_of_coqint i) let p_float32 oc f = fprintf oc "%f" (camlfloat_of_coqfloat32 f) let p_float64 oc f = fprintf oc "%f" (camlfloat_of_coqfloat f) let p_z oc z = fprintf oc "%s" (Z.to_string z) +let p_int_constant oc i = fprintf oc "{\"Integer\":%a}" p_int i +let p_float_constant oc f = fprintf oc "{\"Float\":%.18g}" (camlfloat_of_coqfloat f) +let p_z_constant oc z = fprintf oc "{\"Integer\":%s}" (Z.to_string z) let p_constant oc = function - | Cint i -> fprintf oc "{\"Integer\":%a}" p_int i - | Csymbol_low (i,c) -> fprintf oc "{\"Symbol_low\":[%a,%a]}" p_atom i p_int c - | Csymbol_high (i,c) -> fprintf oc "{\"Symbol_high\":[%a,%a]}" p_atom i p_int c - | Csymbol_sda (i,c) -> fprintf oc "{\"Symbol_sda\":[%a,%a]}" p_atom i p_int c - | Csymbol_rel_low (i,c) -> fprintf oc "{\"Symbol_rel_low\":[%a,%a]}" p_atom i p_int c - | Csymbol_rel_high (i,c) -> fprintf oc "{\"Symbol_rel_high\":[%a,%a]}" p_atom i p_int c + | Cint i -> p_int_constant oc i + | Csymbol_low (i,c) -> fprintf oc "{\"Symbol_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_high (i,c) -> fprintf oc "{\"Symbol_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_sda (i,c) -> fprintf oc "{\"Symbol_sda\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_rel_low (i,c) -> fprintf oc "{\"Symbol_rel_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_rel_high (i,c) -> fprintf oc "{\"Symbol_rel_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c let p_crbit oc c = let number = match c with @@ -128,11 +125,13 @@ let p_crbit oc c = fprintf oc "{\"CRbit\":%d}" number -let p_label oc l = fprintf oc "{\"Label:\"%ld}" (P.to_int32 l) +let p_label oc l = fprintf oc "{\"Label\":%ld}" (P.to_int32 l) + +let p_char_list oc l = fprintf oc "{\"String\":\"%a\"}" (fun oc -> List.iter (output_char oc)) l let p_list elem oc l = match l with - | [] -> fprintf oc "null" + | [] -> fprintf oc "[]" | hd::tail -> output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]" @@ -142,26 +141,6 @@ let p_list_cont elem oc l = | _ -> List.iter (fprintf oc ",%a" elem) l -let p_typ oc = function - | Tint -> fprintf oc "\"Tint\"" - | Tfloat -> fprintf oc "\"Tfloat\"" - | Tlong -> fprintf oc "\"Tlong\"" - | Tsingle -> fprintf oc "\"Tsingle\"" - | Tany32 -> fprintf oc "\"Tany32\"" - | Tany64 -> fprintf oc "\"Tany64\"" - -let p_signature oc signature = - let p_result oc = function - | None -> fprintf oc "null" - | Some e -> p_typ oc e in - let p_calling_convention oc cc = - fprintf oc "{\"Vararg\":%B,\"Structreg\":%B}" cc.cc_vararg cc.cc_structret - in - fprintf oc "{\"Sig_args\":%a,\"Sig_res\":%a,\"Sig_cc\":%a}" - (p_list p_typ) signature.sig_args - p_result signature.sig_res - p_calling_convention signature.sig_cc - let p_instruction oc ic = output_string oc "\n"; match ic with @@ -172,21 +151,21 @@ let p_instruction oc ic = | Paddic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddis (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pallocframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pallocframe\",\"Args\":[%a,%a]}" p_z c p_int i + | Pallocframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pallocframe\",\"Args\":[%a,%a]}" p_z_constant c p_int_constant i | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pandis_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandis_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l - | Pbctr s -> fprintf oc "{\"Instruction Name\":\"Pbctr\",\"Args\":[%a]}" p_signature s - | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[%a]}" p_signature s + | Pbctr s -> fprintf oc "{\"Instruction Name\":\"Pbctr\",\"Args\":[]}" + | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[]}" | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l - | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a,%a]}" p_atom i p_signature s - | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a,%a]}" p_atom i p_signature s - | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":null}" + | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}" p_atom_constant i + | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}" p_atom_constant i + | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l - | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a,%a]}" p_ireg i (p_list p_label) lb + | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a%a]}" p_ireg i (p_list_cont p_label) lb | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 @@ -197,11 +176,11 @@ let p_instruction oc ic = | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":null}" + | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" | Peqv (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Peqv\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pextsb (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsb\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pfreeframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pfreeframe\",\"Args\":[%ld,%a]}" (Z.to_int32 c) p_int i + | Pfreeframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pfreeframe\",\"Args\":[%a,%a]}" p_z_constant c p_int_constant i | Pfabs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabss\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 @@ -230,7 +209,7 @@ let p_instruction oc ic = | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 - | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":null}" + | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plfd (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir @@ -244,8 +223,8 @@ let p_instruction oc ic = | Plhbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plhz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plhz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plhzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float64 fc - | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float64 fc + | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float_constant fc + | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float_constant fc | Plwz (ir1,ic,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant ic p_ireg ir2 | Plwzu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwzu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plwzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 @@ -269,11 +248,11 @@ let p_instruction oc ic = | Porc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Porc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Poris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Poris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c - | Prlwinm (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwinm\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int ic1 p_int ic2 - | Prlwimi (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwimi\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int ic1 p_int ic2 + | Prlwinm (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwinm\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 + | Prlwimi (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwimi\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 | Pslw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pslw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psraw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psraw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Psrawi (ir1,ir2,ic) -> fprintf oc "{\"Instruction Name\":\"Psrawi\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int ic + | Psrawi (ir1,ir2,ic) -> fprintf oc "{\"Instruction Name\":\"Psrawi\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic | Psrw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstb (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 @@ -299,8 +278,8 @@ let p_instruction oc ic = | Psubfe (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Psubfic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Psubfic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c - | Psync -> fprintf oc "{\"Instruction Name\":\"Psync\",\"Args\":null}" - | Ptrap -> fprintf oc "{\"Instruction Name\":\"Ptrap\",\"Args\":null}" + | Psync -> fprintf oc "{\"Instruction Name\":\"Psync\",\"Args\":[]}" + | Ptrap -> fprintf oc "{\"Instruction Name\":\"Ptrap\",\"Args\":[]}" | Pxor (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pxor\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pxori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pxoris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxoris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c @@ -308,13 +287,13 @@ let p_instruction oc ic = | Pbuiltin (ef,args1,args2) -> begin match ef with | EF_inline_asm (i,s,il) -> - fprintf oc "{\"Instruction Name\":\"Inline_asm\",\"Args\":[%a,%a%a%a%a]}" p_atom i p_signature s (p_list_cont p_atom) il + fprintf oc "{\"Instruction Name\":\"Inline_asm\",\"Args\":[%a%a%a%a]}" p_atom_constant i (p_list_cont p_char_list) il (p_list_cont p_preg) args1 (p_list_cont p_preg) args2 | _ -> (* Should all be folded away *) assert false end - | Pannot _ -> () (* We do not check the annotations *) - | Pcfi_adjust _ -> () (* Only debug relevant *) + | Pannot _ (* We do not check the annotations *) + | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> () (* Only debug relevant *) let p_storage oc sto = @@ -322,7 +301,7 @@ let p_storage oc sto = | C.Storage_default -> "Default" | C.Storage_extern -> "Extern" | C.Storage_static -> "Static" - | C.Storage_register -> "Register" in + | C.Storage_register -> "" (* This should not occur *) in fprintf oc "\"%s\"" storage let p_section oc = function @@ -335,23 +314,22 @@ let p_section oc = function | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e - | Section_debug_info -> fprintf oc "{\"Section Name\":\"Debug Info\"}" - | Section_debug_abbrev -> fprintf oc "{\"Section Name\":\"Debug Abbreviation\"}" + | Section_debug_info + | Section_debug_abbrev -> () (* There should be no info in the debug sections *) let p_int_opt oc = function - | None -> fprintf oc "null" + | None -> fprintf oc "0" | Some i -> fprintf oc "%d" i -let p_atom_info oc ident = - let info = Hashtbl.find C2C.decl_atom ident in - fprintf oc "{\"Storage Class\":%a,\n\"Alignment\":%a,\n\"Sections\":%a,\n\"Inline\":%B}" - p_storage info.a_storage p_int_opt info.a_alignment (p_list p_section) info.a_sections - info.a_inline let p_fundef oc (name,f) = - let instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in - fprintf oc "{\"Fun Name\":%a,\n\"Fun Sig\":%a,\n\"Atom info\":%a,\n\"Fun Code\":%a}\n" - p_atom name p_signature f.fn_sig p_atom_info name (p_list p_instruction) instr + let info = Hashtbl.find C2C.decl_atom name in + let instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + let c_section,l_section,j_section = match info.a_sections with [a;b;c] -> a,b,c | _ -> assert false in + fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n" + p_atom name p_storage info.a_storage p_int_opt info.a_alignment + p_section c_section p_section l_section p_section j_section info.a_inline + (p_list p_instruction) instr let p_init_data oc = function | Init_int8 ic -> fprintf oc "{\"Init_int8\":%a}" p_int ic @@ -361,11 +339,15 @@ let p_init_data oc = function | Init_float32 f -> fprintf oc "{\"Init_float32\":%a}" p_float32 f | Init_float64 f -> fprintf oc "{\"Init_float64\":%a}" p_float64 f | Init_space z -> fprintf oc "{\"Init_space\":%a}" p_z z - | Init_addrof (p,i) -> fprintf oc "{\"Init_addrof\":[%a,%a]}" p_atom p p_int i + | Init_addrof (p,i) -> fprintf oc "{\"Init_addrof\":{\"Addr\":%a,\"Offset\":%a}}" p_atom p p_int i let p_vardef oc (ident,v) = - fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\"Atom Info\":%a,\"Var Init\":%a}\n" - p_atom ident v.gvar_readonly v.gvar_volatile p_atom_info ident (p_list p_init_data) v.gvar_init + let info = Hashtbl.find C2C.decl_atom ident in + let section = match info.a_sections with [s] -> s | _ -> assert false (* Should only have one section *) in + fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n" + p_atom ident v.gvar_readonly v.gvar_volatile + p_storage info.a_storage p_int_opt info.a_alignment p_section section + (p_list p_init_data) v.gvar_init let p_program oc prog = let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> -- cgit From 50ed2827867238a98f2036f799d4d6f354a2581c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 19 May 2015 18:07:08 +0200 Subject: Added flag for the renaming of static functions. --- cparser/Parse.ml | 2 +- cparser/Rename.ml | 28 ++++++++++++++++++++++------ cparser/Rename.mli | 2 +- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ 5 files changed, 27 insertions(+), 8 deletions(-) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 317847a7..c9564c08 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -29,7 +29,7 @@ let transform_program t p name = Some (CtoDwarf.program_to_dwarf p p1 name) else None in - (Rename.program p1),debug + (Rename.program p1 (Filename.chop_suffix name ".c")),debug let parse_transformations s = let t = ref CharSet.empty in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 0d533b56..cf82bc9f 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -42,6 +42,16 @@ let enter_public env id = { re_id = IdentMap.add id id env.re_id; re_public = StringMap.add id.name id env.re_public; re_used = StringSet.add id.name env.re_used } + +let enter_static env id file = + try + let id' = StringMap.find id.name env.re_public in + { env with re_id = IdentMap.add id id' env.re_id } + with Not_found -> + let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in + { re_id = IdentMap.add id id' env.re_id; + re_public = env.re_public; + re_used = StringSet.add id'.name env.re_used } (* For static or local identifiers, we make up a new name if needed *) (* If the same identifier has already been declared, @@ -249,7 +259,7 @@ let reserve_builtins () = (* Reserve global declarations with public visibility *) -let rec reserve_public env = function +let rec reserve_public env file = function | [] -> env | dcl :: rem -> let env' = @@ -257,22 +267,28 @@ let rec reserve_public env = function | Gdecl(sto, id, _, _) -> begin match sto with | Storage_default | Storage_extern -> enter_public env id - | Storage_static -> env + | Storage_static -> if !Clflags.option_rename_static then + enter_static env id file + else + env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with | Storage_default | Storage_extern -> enter_public env f.fd_name - | Storage_static -> env + | Storage_static -> if !Clflags.option_rename_static then + enter_static env f.fd_name file + else + env | _ -> assert false end | _ -> env in - reserve_public env' rem + reserve_public env' file rem (* Rename the program *) -let program p = +let program p file = globdecls - (reserve_public (reserve_builtins()) p) + (reserve_public (reserve_builtins()) file p) [] p diff --git a/cparser/Rename.mli b/cparser/Rename.mli index 818a51bc..c4ef2228 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val program : C.program -> C.program +val program : C.program -> string -> C.program diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8899c2b0..d9c21a9c 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -59,3 +59,4 @@ let option_small_data = then 8 else 0) let option_small_const = ref (!option_small_data) let option_timings = ref false +let option_rename_static = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 04dec9db..90badb85 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -435,6 +435,7 @@ Language support options (use -fno- to turn off -f) : -fnone Turn off all language support options above Debugging options: -g Generate debugging information + -frename-static Rename static functions and declarations Optimization options: (use -fno- to turn off -f) -O Optimize the compiled code [on by default] -O0 Do not optimize the compiled code @@ -528,6 +529,7 @@ let cmdline_actions = Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true); + Exact "-frename-static", Self (fun s -> option_rename_static:= true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); -- cgit From 026f2fc382ba4f768ab985fa4c8afe9c0cd3b13b Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 29 May 2015 12:39:51 +0200 Subject: Merged instructions that are printed as same instruction already in printer. --- powerpc/AsmToJSON.ml | 52 ++++++++++++++++++++++++++-------------------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 6e71e01a..993cf441 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -151,13 +151,13 @@ let p_instruction oc ic = | Paddic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddis (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pallocframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pallocframe\",\"Args\":[%a,%a]}" p_z_constant c p_int_constant i + | Pallocframe (c,i) -> assert false(* Should not occur *) | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pandis_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandis_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l - | Pbctr s -> fprintf oc "{\"Instruction Name\":\"Pbctr\",\"Args\":[]}" + | Pbctr s -> assert false (* Should not occur *) | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[]}" | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l @@ -180,25 +180,25 @@ let p_instruction oc ic = | Peqv (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Peqv\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pextsb (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsb\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 - | Pfreeframe (c,i) -> fprintf oc "{\"Instruction Name\":\"Pfreeframe\",\"Args\":[%a,%a]}" p_z_constant c p_int_constant i - | Pfabs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 - | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabss\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfreeframe (c,i) -> assert false (* Should not occur *) + | Pfabs (fr1,fr2) + | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfadds (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadds\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfcmpu (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcmpu\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 - | Pfcti (ir,fr) -> fprintf oc "{\"Instruction Name\":\"Pfcti\",\"Args\":[%a,%a]}" p_ireg ir p_freg fr + | Pfcti (ir,fr) -> assert false (* Should not occur *) | Pfctiw (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiw\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfctiwz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiwz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfdiv (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdiv\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfdivs (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdivs\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 - | Pfmake (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pfmake\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Pfmake (fr,ir1,ir2) -> assert false (* Should not occur *) | Pfmr (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfmr\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfmul (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfmul\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfmuls(fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfmuls\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 - | Pfneg (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfneg\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 - | Pfnegs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfnegs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfneg (fr1,fr2) + | Pfnegs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfneg\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 | Pfrsp (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfrsp\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 - | Pfxdp (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfxdp\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfxdp (fr1,fr2) -> assert false (* Should not occur *) | Pfsub (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfsub\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfsubs (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfsubs\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 | Pfmadd (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmadd\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 @@ -212,10 +212,10 @@ let p_instruction oc ic = | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Plfd (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Plfdx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 - | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plfd (fr,c,ir) + | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Plfdx (fr,ir1,ir2) + | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Plfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Plfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Plha (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plha\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 @@ -226,14 +226,14 @@ let p_instruction oc ic = | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float_constant fc | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float_constant fc | Plwz (ir1,ic,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant ic p_ireg ir2 + | Plwz_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plwzu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwzu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 - | Plwzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Plwz_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 - | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plwzx (ir1,ir2,ir3) + | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pmfcr ir -> fprintf oc "{\"Instruction Name\":\"Pmfcr\",\"Args\":[%a]}" p_ireg ir - | Pmfcrbit (ir,crb) -> fprintf oc "{\"Instruction Name\":\"Pmfcrbit\",\"Args\":[%a,%a]}" p_ireg ir p_crbit crb + | Pmfcrbit (ir,crb) -> assert false (* Should not occur *) | Pmflr ir -> fprintf oc "{\"Instruction Name\":\"Pmflr\",\"Args\":[%a]}" p_ireg ir | Pmr (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pmr\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pmtctr ir -> fprintf oc "{\"Instruction Name\":\"Pmtctr\",\"Args\":[%a]}" p_ireg ir @@ -256,22 +256,22 @@ let p_instruction oc ic = | Psrw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstb (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Pstfd (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfd (fr,c,ir) + | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Pstfdx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 - | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir - | Pstfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfdx_a\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Pstfdx (fr,ir1,ir2) + | Pstfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Pstfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir | Pstfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 | Psth (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Psth\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Psthx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psthx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psthbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psthbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Pstw (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstw (ir1,c,ir2) + | Pstw_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Pstwu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 - | Pstwx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwx (ir1,ir2,ir3) + | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwxu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwxu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Pstw_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstw_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 - | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx_a\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 -- cgit From 29dbe852c1ce14032d92aaf5b61f8a12d50bdb0e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 22 Jun 2015 23:54:45 +0200 Subject: Fixed typo also in json export. --- powerpc/AsmToJSON.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 993cf441..f9c1ba9c 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -271,7 +271,7 @@ let p_instruction oc ic = | Pstwu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Pstwx (ir1,ir2,ir3) | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Pstwxu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwxu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwux (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwux\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 -- cgit From 6daf9d8bdc10bed02292ae6f672688f5f45db775 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 24 Jun 2015 16:34:32 +0200 Subject: Print bit representation of floats. --- powerpc/AsmToJSON.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index f9c1ba9c..4c3f9d97 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -99,12 +99,13 @@ let p_atom_constant oc a = fprintf oc "{\"Atom\":%a}" p_atom a let p_int oc i = fprintf oc "%ld" (camlint_of_coqint i) let p_int64 oc i = fprintf oc "%Ld" (camlint64_of_coqint i) -let p_float32 oc f = fprintf oc "%f" (camlfloat_of_coqfloat32 f) -let p_float64 oc f = fprintf oc "%f" (camlfloat_of_coqfloat f) +let p_float32 oc f = fprintf oc "%ld" (camlint_of_coqint (Floats.Float32.to_bits f)) +let p_float64 oc f = fprintf oc "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f)) let p_z oc z = fprintf oc "%s" (Z.to_string z) let p_int_constant oc i = fprintf oc "{\"Integer\":%a}" p_int i -let p_float_constant oc f = fprintf oc "{\"Float\":%.18g}" (camlfloat_of_coqfloat f) +let p_float64_constant oc f = fprintf oc "{\"Float\":%a}" p_float64 f +let p_float32_constant oc f = fprintf oc "{\"Float\":%a}" p_float32 f let p_z_constant oc z = fprintf oc "{\"Integer\":%s}" (Z.to_string z) let p_constant oc = function @@ -223,8 +224,8 @@ let p_instruction oc ic = | Plhbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 | Plhz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plhz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plhzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 - | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float_constant fc - | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float_constant fc + | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float64_constant fc + | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float32_constant fc | Plwz (ir1,ic,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant ic p_ireg ir2 | Plwz_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 | Plwzu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwzu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 -- cgit From aa780c7145a418b4a7264e828258034fc4629313 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 26 Jun 2015 15:53:08 +0200 Subject: Added diab specific size_t define in stddef. --- runtime/include/stddef.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 3da06c6f..0c3251f6 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -38,6 +38,14 @@ #define _STDDEF_H #endif +#ifdef __DCC__ +#if !defined(__size_t) && !defined(_SIZE_T) +#define __size_t +#define _SIZE_T +typedef unsigned int size_t; +#endif +#undef __need_size_t +#else #if defined(_STDDEF_H) || defined(__need_size_t) #ifndef _SIZE_T #define _SIZE_T @@ -45,6 +53,7 @@ typedef unsigned long size_t; #endif #undef __need_size_t #endif +#endif #if defined(_STDDEF_H) || defined(__need_ptrdiff_t) #ifndef _PTRDIFF_T -- cgit From 0a4cf6562122684811db5ed3dd059769ca1a06d9 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 Jul 2015 15:58:26 +0200 Subject: Use the functions from C2C to extract the information for the atoms. Simplified printing of storage class. --- powerpc/AsmToJSON.ml | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 36960821..520bc1ed 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -297,13 +297,11 @@ let p_instruction oc ic = | Pcfi_adjust _ (* Only debug relevant *) | Pcfi_rel_offset _ -> () (* Only debug relevant *) -let p_storage oc sto = - let storage = match sto with - | C.Storage_default -> "Default" - | C.Storage_extern -> "Extern" - | C.Storage_static -> "Static" - | C.Storage_register -> "" (* This should not occur *) in - fprintf oc "\"%s\"" storage +let p_storage oc static = + if static then + fprintf oc "\"Static\"" + else + fprintf oc "\"Extern\"" let p_section oc = function | Section_text -> fprintf oc "{\"Section Name\":\"Text\"}" @@ -324,12 +322,14 @@ let p_int_opt oc = function let p_fundef oc (name,f) = - let info = Hashtbl.find C2C.decl_atom name in - let instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in - let c_section,l_section,j_section = match info.a_sections with [a;b;c] -> a,b,c | _ -> assert false in + let alignment = atom_alignof name + and inline = atom_is_inline name + and static = atom_is_static name + and instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n" - p_atom name p_storage info.a_storage p_int_opt info.a_alignment - p_section c_section p_section l_section p_section j_section info.a_inline + p_atom name p_storage static p_int_opt alignment + p_section c_section p_section l_section p_section j_section inline (p_list p_instruction) instr let p_init_data oc = function @@ -342,12 +342,13 @@ let p_init_data oc = function | Init_space z -> fprintf oc "{\"Init_space\":%a}" p_z z | Init_addrof (p,i) -> fprintf oc "{\"Init_addrof\":{\"Addr\":%a,\"Offset\":%a}}" p_atom p p_int i -let p_vardef oc (ident,v) = - let info = Hashtbl.find C2C.decl_atom ident in - let section = match info.a_sections with [s] -> s | _ -> assert false (* Should only have one section *) in +let p_vardef oc (name,v) = + let alignment = atom_alignof name + and static = atom_is_static name + and section = match (atom_sections name) with [s] -> s | _ -> assert false (* Should only have one section *) in fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n" - p_atom ident v.gvar_readonly v.gvar_volatile - p_storage info.a_storage p_int_opt info.a_alignment p_section section + p_atom name v.gvar_readonly v.gvar_volatile + p_storage static p_int_opt alignment p_section section (p_list p_init_data) v.gvar_init let p_program oc prog = -- cgit