From 4467453e0edca993c175690b7141d4916af3dc19 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 25 Jan 2016 10:03:11 +0100 Subject: Started implementing a printer for Clflags. --- driver/Clflagsprinter.ml | 41 +++++++++++++++++++++++++++++++++++++++++ driver/Driver.ml | 1 + lib/Json.ml | 33 +++++++++++++++++++++++++++++++++ powerpc/AsmToJSON.ml | 17 +++++------------ 4 files changed, 80 insertions(+), 12 deletions(-) create mode 100644 driver/Clflagsprinter.ml create mode 100644 lib/Json.ml 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 -- cgit