blob: c07463222cb6937a15ae39f1ef23505e4f562c04 (
plain)
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
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* Handling of pragmas *)
open Printf
open Camlcoq
(* #pragma section *)
let process_section_pragma classname istring ustring addrmode accmode =
Sections.define_section classname
?iname: (if istring = "" then None else Some istring)
?uname: (if ustring = "" then None else Some ustring)
?writable:
(if accmode = "" then None else Some(String.contains accmode 'W'))
?executable:
(if accmode = "" then None else Some(String.contains accmode 'X'))
?access:
(match addrmode with
| "" -> None
| "near-data" -> Some Sections.Access_near
| "far-data" -> Some Sections.Access_far
| _ -> Some Sections.Access_default)
()
(* #pragma use_section *)
let re_c_ident = Str.regexp "[A-Za-z_][A-Za-z_0-9]*$"
let process_use_section_pragma classname id =
if id = "," || id = ";" then () else begin
if not (Str.string_match re_c_ident id 0) then
C2C.error (sprintf "bad identifier `%s' in #pragma use_section" id);
if not (Sections.use_section_for (intern_string id) classname) then
C2C.error (sprintf "unknown section name `%s'" classname)
end
(* #pragma reserve_register *)
let process_reserve_register_pragma name =
match Machregsaux.register_by_name name with
| None ->
C2C.error "unknown register in `reserve_register' pragma"
| Some r ->
if Machregsaux.can_reserve_register r then
IRC.reserved_registers := r :: !IRC.reserved_registers
else
C2C.error "cannot reserve this register (not a callee-save)"
(* Parsing of pragmas *)
let process_pragma name =
match Tokenize.string name with
| ["section"; classname; istring; ustring; addrmode; accmode] ->
process_section_pragma classname istring ustring addrmode accmode;
true
| "section" :: _ ->
C2C.error "ill-formed `section' pragma"; true
| "use_section" :: classname :: identlist ->
if identlist = [] then C2C.warning "vacuous `use_section' pragma";
List.iter (process_use_section_pragma classname) identlist;
true
| "use_section" :: _ ->
C2C.error "ill-formed `use_section' pragma"; true
| ["reserve_register"; reg] ->
process_reserve_register_pragma reg; true
| "reserve_register" :: _ ->
C2C.error "ill-formed `reserve_register' pragma"; true
| _ ->
false
let initialize () =
C2C.process_pragma_hook := process_pragma
|
