1 files changed, 109 insertions, 0 deletions
diff --git a/backend/Json.ml b/backend/Json.ml
new file mode 100644
index 00000000..b8f66c08
--- /dev/null
+++ b/backend/Json.ml
@@ -0,0 +1,109 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                                                 *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Format
+open Camlcoq
+
+
+(* Simple functions for JSON printing *)
+
+(* Print a string as json string *)
+let pp_jstring oc s =
+  fprintf oc "\"%s\"" s
+
+(* Print a bool as json bool *)
+let pp_jbool oc = fprintf oc "%B"
+
+(* Print an int as json int *)
+let pp_jint oc = fprintf oc "%d"
+
+(* Print an int32 as json int *)
+let pp_jint32 oc = fprintf oc "%ld"
+
+(* Print optional value *)
+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 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
+
+(* Print singleton object *)
+let pp_jsingle_object pp name pp_mem mem =
+  pp_jobject_start pp;
+  pp_jmember ~first:true pp name pp_mem mem;
+  pp_jobject_end pp
+
+(* Print a list as json array *)
+let pp_jarray elem pp l =
+  match l with
+  | []  ->  fprintf pp "[]";
+  | hd::tail ->
+    fprintf pp "@[<v 1>[";
+    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