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