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
125
126
127
128
129
130
131
132
133
134
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* Platform-dependent handling of pragmas *)
open Printf
open Cil
open Camlcoq
type section_info = {
sec_name_init: string;
sec_name_uninit: string;
sec_near_access: bool
}
let section_table : (string, section_info) Hashtbl.t =
Hashtbl.create 17
let use_section_table : (AST.ident, section_info) Hashtbl.t =
Hashtbl.create 51
let process_section_pragma classname istring ustring addrmode accmode =
let is_near = (addrmode = "near-absolute") || (addrmode = "near-data") in
let is_writable = String.contains accmode 'W'
and is_executable = String.contains accmode 'X' in
let sec_type =
match is_writable, is_executable with
| true, true -> 'm' (* text+data *)
| true, false -> 'd' (* data *)
| false, true -> 'c' (* text *)
| false, false -> 'r' (* const *)
in
let info =
{ sec_name_init = sprintf "%s,,%c" istring sec_type;
sec_name_uninit = sprintf "%s,,%c" ustring sec_type;
sec_near_access = is_near } in
Hashtbl.add section_table classname info
let process_use_section_pragma classname id =
try
let info = Hashtbl.find section_table classname in
Hashtbl.add use_section_table (intern_string id) info
with Not_found ->
Cil2Csyntax.error (sprintf "unknown section name `%s'" classname)
(* CIL does not parse the "section" and "use_section" pragmas, which
have irregular syntax, so we parse them using regexps *)
let re_start_pragma_section = Str.regexp "section\\b"
let re_pragma_section = Str.regexp
"section[ \t]+\
\\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\
\"\\([^\"]*\\)\"[ \t]+\
\"\\([^\"]*\\)\"[ \t]+\
\\([a-z-]+\\)[ \t]+\
\\([A-Z]+\\)"
let re_start_pragma_use_section = Str.regexp "use_section\\b"
let re_pragma_use_section = Str.regexp
"use_section[ \t]+\
\\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\
\\(.*\\)$"
let re_split_idents = Str.regexp "[ \t,]+"
let process_pragma (Attr(name, _)) =
if Str.string_match re_pragma_section name 0 then begin
process_section_pragma
(Str.matched_group 1 name) (* classname *)
(Str.matched_group 2 name) (* istring *)
(Str.matched_group 3 name) (* ustring *)
(Str.matched_group 4 name) (* addrmode *)
(Str.matched_group 5 name); (* accmode *)
true
end else if Str.string_match re_start_pragma_section name 0 then
Cil2Csyntax.error "ill-formed `section' pragma"
else if Str.string_match re_pragma_use_section name 0 then begin
let classname = Str.matched_group 1 name
and idents = Str.matched_group 2 name in
let identlist = Str.split re_split_idents idents in
if identlist = [] then Cil2Csyntax.warning "vacuous `use_section' pragma";
List.iter (process_use_section_pragma classname) identlist;
true
end else if Str.string_match re_start_pragma_use_section name 0 then
Cil2Csyntax.error "ill-formed `use_section' pragma"
else
false
let initialize () =
Cil2Csyntax.process_pragma := process_pragma
(* PowerPC-specific: say if an atom is in a small data area *)
let atom_is_small_data a ofs =
match Configuration.system with
| "diab" ->
begin try
let v = Hashtbl.find Cil2Csyntax.varinfo_atom a in
let sz = Cil.bitsSizeOf v.vtype / 8 in
let ofs = camlint_of_coqint ofs in
if ofs >= 0l && ofs < Int32.of_int sz then begin
try (Hashtbl.find use_section_table a).sec_near_access
with Not_found -> sz <= 8
end else
false
with Not_found ->
false
end
| _ ->
false
(* PowerPC-specific: determine section to use for a particular symbol *)
let section_for_atom a init =
try
let sinfo = Hashtbl.find use_section_table a in
Some(if init then sinfo.sec_name_init else sinfo.sec_name_uninit)
with Not_found ->
None
|
