Moved the information needed from the atoms to the ASM printer and removed unused information from the json dump.

3 files changed, 50 insertions, 100 deletions

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