1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
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
|
