Started implementing a printer for Clflags.

4 files changed, 80 insertions, 12 deletions

diff --git a/driver/Clflagsprinter.ml b/driver/Clflagsprinter.ml
new file mode 100644
index 00000000..11dcc818
--- /dev/null
+++ b/driver/Clflagsprinter.ml
@@ -0,0 +1,41 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Clflags
+open Json
+open Printf
+
+let print_member oc name p_mem mem =
+  fprintf oc "\n%a:%a" p_jstring name p_mem mem
+
+let print_list oc name l =
+  print_member oc name (p_jarray p_jstring) l
+
+let print oc ((): unit) =
+  fprintf oc "{";
+  print_list oc "Preprocessor Options" !prepro_options;
+  print_list oc "Linker Options" !linker_options;
+  print_list oc "Assembler Options" !assembler_options;
+  print_member oc "Flongdouble" p_jbool !option_flongdouble;
+  print_member oc "Fstruct_passing" p_jbool !option_fstruct_passing;
+  print_member oc "Fbitfields" p_jbool !option_fbitfields;
+  print_member oc "Fvarag_calls" p_jbool !option_fvararg_calls;
+  print_member oc "Funprototyped" p_jbool !option_funprototyped;
+  print_member oc "Fpacked_structs" p_jbool !option_fpacked_structs;
+  print_member oc "Ffpu" p_jbool !option_ffpu;
+  print_member oc "Ffloatconstprop" p_jint !option_ffloatconstprop;
+  print_member oc "Ftailcalls" p_jbool !option_ftailcalls;
+  print_member oc "Fconstprop" p_jbool !option_fconstprop;
+  print_member oc "Fcse" p_jbool !option_fcse;
+  print_member oc "Fredundance" p_jbool !option_fredundancy;
+  
+  fprintf oc "\n}"
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 78d141c1..d827fd94 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -14,6 +14,7 @@ open Printf
 open Commandline
 open Camlcoq
 open Clflags
+open Clflagsprinter
 open Timing
 
 (* Location of the compatibility library *)
diff --git a/lib/Json.ml b/lib/Json.ml
new file mode 100644
index 00000000..db2de5d4
--- /dev/null
+++ b/lib/Json.ml
@@ -0,0 +1,33 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Printf
+
+(* Simple functions for JSON printing *)
+
+(* Print a string as json string *)
+let p_jstring oc s = fprintf oc "\"%s\"" s
+
+(* Print a list as json array *)
+let p_jarray elem oc l =
+  match l with
+  | [] -> fprintf oc "[]"
+  | hd::tail ->
+      output_string oc "["; elem oc hd;
+      List.iter (fprintf oc ",%a" elem) tail;
+      output_string oc "]"
+
+(* Print a bool as json bool *)
+let p_jbool oc = fprintf oc "%B"
+
+(* Print a int as json int *)
+let p_jint oc = fprintf oc "%d"
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 42ad4f97..4ca7dbde 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -17,11 +17,10 @@ open AST
 open BinNums
 open C2C
 open Camlcoq
+open Json
 open Printf
 open Sections
 
-let p_jstring oc s = fprintf oc "\"%s\"" s
-
 let p_ireg oc = function
   | GPR0 -> fprintf oc "{\"Register\":\"r0\"}"
   | GPR1 -> fprintf oc "{\"Register\":\"r1\"}"
@@ -129,12 +128,6 @@ let p_crbit oc c =
 
 let p_label oc l = fprintf oc "{\"Label\":%ld}" (P.to_int32 l)
 
-let p_list elem oc l =
-  match l with
-  | [] -> fprintf oc "[]"
-  | hd::tail ->
-     output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]"
-
 type instruction_arg =
   | Ireg of ireg
   | Freg of freg
@@ -156,7 +149,7 @@ let p_arg oc = function
   | Atom a -> p_atom_constant oc a
 
 let p_instruction oc ic =
-  let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_list p_arg) l
+  let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_jarray p_arg) l
   and inst_name oc s = fprintf  oc"%a:%a" p_jstring "Instruction Name" p_jstring s in
   let first = ref true in
   let sep oc = if !first then first := false else output_string oc ", " in
@@ -385,7 +378,7 @@ let p_vardef oc (name,v) =
   fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n"
     p_atom name v.gvar_readonly v.gvar_volatile
     p_storage static p_int_opt alignment p_section section
-    (p_list p_init_data) v.gvar_init
+    (p_jarray p_init_data) v.gvar_init
 
 let p_program oc prog =
   let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) ->
@@ -394,5 +387,5 @@ let p_program oc prog =
     | 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
+    (p_jarray p_vardef) prog_vars
+    (p_jarray p_fundef) prog_funs