diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Json.ml | 109 | ||||
| -rw-r--r-- | lib/JsonAST.ml | 124 | ||||
| -rw-r--r-- | lib/JsonAST.mli | 16 | ||||
| -rw-r--r-- | lib/Lattice.v | 1 | ||||
| -rw-r--r-- | lib/Ordered.v | 1 | ||||
| -rw-r--r-- | lib/Readconfig.mll | 15 |
6 files changed, 15 insertions, 251 deletions
diff --git a/lib/Json.ml b/lib/Json.ml deleted file mode 100644 index b8f66c08..00000000 --- a/lib/Json.ml +++ /dev/null @@ -1,109 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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/lib/JsonAST.ml b/lib/JsonAST.ml deleted file mode 100644 index 73cac31e..00000000 --- a/lib/JsonAST.ml +++ /dev/null @@ -1,124 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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/lib/JsonAST.mli b/lib/JsonAST.mli deleted file mode 100644 index c6fd80c9..00000000 --- a/lib/JsonAST.mli +++ /dev/null @@ -1,16 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 diff --git a/lib/Lattice.v b/lib/Lattice.v index b7ae837b..85fc03f3 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -6,7 +6,6 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) (* (at your option) any later version. This file is also distributed *) diff --git a/lib/Ordered.v b/lib/Ordered.v index c333cc50..bcf24cbd 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -6,7 +6,6 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 2 of the License, or *) (* (at your option) any later version. This file is also distributed *) diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll index 6cb3409d..e71c8fb7 100644 --- a/lib/Readconfig.mll +++ b/lib/Readconfig.mll @@ -1,3 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + { (* Recording key=val bindings *) |