diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Json.ml | 109 | ||||
| -rw-r--r-- | backend/JsonAST.ml | 124 | ||||
| -rw-r--r-- | backend/JsonAST.mli | 16 |
3 files changed, 249 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 diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml new file mode 100644 index 00000000..73cac31e --- /dev/null +++ b/backend/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_inline name = Inline + 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/backend/JsonAST.mli b/backend/JsonAST.mli new file mode 100644 index 00000000..c6fd80c9 --- /dev/null +++ b/backend/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 |