Added the first version of the sdump export to json.

1 files changed, 72 insertions, 0 deletions

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 "}"