New json printing interface.

The common json export functionallity is moved into an own File.
Bug 22472

3 files changed, 190 insertions, 1 deletions

diff --git a/lib/Json.ml b/lib/Json.ml
index 16819e8d..b8f66c08 100644
--- a/lib/Json.ml
+++ b/lib/Json.ml
@@ -11,6 +11,8 @@
 (* *********************************************************************)
 
 open Format
+open Camlcoq
+
 
 (* Simple functions for JSON printing *)
 
@@ -32,13 +34,14 @@ let pp_jopt pp_elem oc = function
   | None -> output_string oc "null"
   | Some i -> pp_elem oc i
 
+(* Print opening and closing curly braces for json dictionaries *)
 let pp_jobject_start pp =
   fprintf pp "@[<v 1>{"
 
 let pp_jobject_end pp =
   fprintf pp "@;<0 -1>}@]"
 
-(* Print a member *)
+(* Print a member of a json dictionary *)
 let pp_jmember ?(first=false) pp name pp_mem mem =
   let sep = if first then "" else "," in
   fprintf pp "%s@ \"%s\": %a" sep name pp_mem mem
@@ -58,3 +61,49 @@ let pp_jarray elem pp l =
     fprintf pp "%a" elem hd;
     List.iter (fun l -> fprintf pp ",@ %a" elem l) tail;
   fprintf pp "@;<0 -1>]@]"
+
+(* Helper functions for printing coq integer and floats *)
+let pp_int pp i =
+  fprintf pp "%ld" (camlint_of_coqint i)
+
+let pp_int64 pp i =
+  fprintf pp "%Ld" (camlint64_of_coqint i)
+
+let pp_float32 pp f =
+  fprintf pp "%ld" (camlint_of_coqint (Floats.Float32.to_bits f))
+
+let pp_float64 pp f =
+  fprintf pp "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f))
+
+let pp_z pp z =
+  fprintf pp "%s" (Z.to_string z)
+
+(* Helper functions for printing assembler constructs *)
+let pp_atom pp a =
+  pp_jstring pp (extern_atom a)
+
+let pp_atom_constant pp a =
+  pp_jsingle_object pp "Atom" pp_atom a
+
+let pp_int_constant pp i =
+  pp_jsingle_object pp "Integer" pp_int i
+
+let pp_float64_constant pp f =
+  pp_jsingle_object pp "Float" pp_float64 f
+
+let pp_float32_constant pp f =
+  pp_jsingle_object pp "Float" pp_float32 f
+
+let id = ref 0
+
+let next_id () =
+  let tmp = !id in
+  incr id;
+  tmp
+
+let reset_id () =
+  id := 0
+
+let pp_id_const pp () =
+  let i = next_id () in
+  pp_jsingle_object pp "Integer" (fun pp i -> fprintf pp "%d" i) i
diff --git a/lib/JsonAST.ml b/lib/JsonAST.ml
new file mode 100644
index 00000000..f3dd2dc6
--- /dev/null
+++ b/lib/JsonAST.ml
@@ -0,0 +1,124 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*          Michael Schmidt, 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.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Asm
+open AST
+open C2C
+open Json
+open Format
+open Sections
+
+
+let pp_storage pp static =
+  pp_jstring pp (if static then "Static" else "Extern")
+
+let pp_section pp sec =
+  let pp_simple name =
+    pp_jsingle_object pp "Section Name" pp_jstring name
+  and pp_complex name init =
+    pp_jobject_start pp;
+    pp_jmember ~first:true pp "Section Name" pp_jstring name;
+    pp_jmember pp "Init" pp_jbool init;
+    pp_jobject_end pp in
+  match sec with
+  | Section_text -> pp_simple "Text"
+  | Section_data init -> pp_complex "Data" init
+  | Section_small_data init -> pp_complex "Small Data" init
+  | Section_const init -> pp_complex "Const" init
+  | Section_small_const init -> pp_complex "Small Const" init
+  | Section_string -> pp_simple "String"
+  | Section_literal -> pp_simple "Literal"
+  | Section_jumptable -> pp_simple "Jumptable"
+  | Section_user (s,w,e) ->
+    pp_jobject_start pp;
+    pp_jmember ~first:true pp "Section Name" pp_jstring s;
+    pp_jmember pp "Writable" pp_jbool w;
+    pp_jmember pp "Executable" pp_jbool e;
+    pp_jobject_end pp
+  | Section_debug_info _
+  | Section_debug_abbrev
+  | Section_debug_line _
+  | Section_debug_loc
+  | Section_debug_ranges
+  | Section_debug_str
+  | Section_ais_annotation -> () (* There should be no info in the debug sections *)
+
+let pp_int_opt pp = function
+  | None -> fprintf pp "0"
+  | Some i -> fprintf pp "%d" i
+
+let pp_fundef pp_inst pp (name,fn) =
+  let alignment = atom_alignof name
+  and inline = atom_is_inline name
+  and static = atom_is_static name
+  and c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in
+  pp_jobject_start pp;
+  pp_jmember ~first:true pp "Fun Name" pp_atom name;
+  pp_jmember pp "Fun Storage Class" pp_storage static;
+  pp_jmember pp "Fun Alignment" pp_int_opt alignment;
+  pp_jmember pp "Fun Section Code" pp_section c_section;
+  pp_jmember pp "Fun Section Literals" pp_section l_section;
+  pp_jmember pp "Fun Section Jumptable" pp_section j_section;
+  pp_jmember pp "Fun Inline" pp_jbool inline;
+  pp_jmember pp "Fun Code" pp_inst fn.fn_code;
+  pp_jobject_end pp
+
+let pp_init_data pp = function
+  | Init_int8 ic -> pp_jsingle_object pp "Init_int8" pp_int ic
+  | Init_int16 ic -> pp_jsingle_object pp "Init_int16" pp_int ic
+  | Init_int32 ic -> pp_jsingle_object pp "Init_int32" pp_int ic
+  | Init_int64 lc -> pp_jsingle_object pp "Init_int64" pp_int64 lc
+  | Init_float32 f -> pp_jsingle_object pp "Init_float32" pp_float32 f
+  | Init_float64 f -> pp_jsingle_object pp "Init_float64" pp_float64 f
+  | Init_space z -> pp_jsingle_object pp "Init_space" pp_z z
+  | Init_addrof (p,i) ->
+    let pp_addr_of pp (p,i) =
+      pp_jobject_start pp;
+      pp_jmember ~first:true pp "Addr" pp_atom p;
+      pp_jmember  pp "Offset" pp_int i;
+      pp_jobject_end pp  in
+    pp_jsingle_object pp "Init_addrof" pp_addr_of (p,i)
+
+let pp_vardef pp (name,v) =
+  let alignment = atom_alignof name
+  and static = atom_is_static name
+  and section = match  (atom_sections name) with [s] -> s | _ -> assert false in(* Should only have one section *)
+  pp_jobject_start pp;
+  pp_jmember ~first:true pp "Var Name" pp_atom name;
+  pp_jmember pp "Var Readonly" pp_jbool v.gvar_readonly;
+  pp_jmember pp "Var Volatile" pp_jbool v.gvar_volatile;
+  pp_jmember pp "Var Storage Class" pp_storage static;
+  pp_jmember pp "Var Alignment" pp_int_opt alignment;
+  pp_jmember pp "Var Section" pp_section section;
+  pp_jmember pp "Var Init" (pp_jarray pp_init_data) v.gvar_init;
+  pp_jobject_end pp
+
+let pp_program pp pp_inst prog =
+  let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
+      match def with
+      | Gfun (Internal f) ->
+        if not (atom_is_iso_inline_definition ident) then
+          vars,(ident,f)::funs
+        else
+          vars,funs
+      | Gvar v -> (ident,v)::vars,funs
+      | _ -> vars,funs) ([],[]) prog.prog_defs in
+  pp_jobject_start pp;
+  pp_jmember ~first:true pp "Global Variables" (pp_jarray pp_vardef) prog_vars;
+  pp_jmember pp "Functions" (pp_jarray (pp_fundef pp_inst)) prog_funs;
+  pp_jobject_end pp
+
+let pp_mnemonics pp mnemonic_names =
+  let mnemonic_names = List.sort (String.compare) mnemonic_names in
+  let new_line pp () = pp_print_string pp "\n" in
+  pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names
diff --git a/lib/JsonAST.mli b/lib/JsonAST.mli
new file mode 100644
index 00000000..c6fd80c9
--- /dev/null
+++ b/lib/JsonAST.mli
@@ -0,0 +1,16 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+
+
+val pp_program : Format.formatter -> (Format.formatter  -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
+val pp_mnemonics : Format.formatter -> string list -> unit