forked from cil-project/cil
-
Notifications
You must be signed in to change notification settings - Fork 20
/
Copy pathfrontc.ml
266 lines (227 loc) · 8.36 KB
/
frontc.ml
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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
(*
*
* Copyright (c) 2001-2002,
* George C. Necula <necula@cs.berkeley.edu>
* Scott McPeak <smcpeak@cs.berkeley.edu>
* Wes Weimer <weimer@cs.berkeley.edu>
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
*
* 3. The names of the contributors may not be used to endorse or promote
* products derived from this software without specific prior written
* permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
* OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
*)
module E = Errormsg
open Trace
open Pretty
(* Output management *)
let out : out_channel option ref = ref None
let close_me = ref false
let close_output _ =
match !out with
None -> ()
| Some o -> begin
flush o;
if !close_me then close_out o else ();
close_me := false
end
let set_output filename =
close_output ();
let out_chan = try open_out filename
with Sys_error msg ->
(output_string stderr ("Error while opening output: " ^ msg); exit 1) in
out := Some out_chan;
Whitetrack.setOutput out_chan;
close_me := true
(* Signal that we are in MS VC mode *)
let setMSVCMode () =
Cprint.msvcMode := true
(* filename for patching *)
let patchFileName : string ref = ref "" (* by default do no patching *)
(* patching file contents *)
let patchFile : Cabs.file option ref = ref None
(* whether to print the patched CABS files *)
let printPatchedFiles : bool ref = ref false
(* whether to print a file of prototypes after parsing *)
let doPrintProtos : bool ref = ref false
(* this seems like something that should be built-in.. *)
let isNone (o : 'a option) : bool =
begin
match o with
| Some _ -> false
| None -> true
end
let printNotice = ref false
(*
** Argument definition
*)
let args : (string * Arg.spec * string) list =
[
"--cabsonly", Arg.String set_output, "<fname> CABS output file name";
"--printComments", Arg.Unit (fun _ -> Cprint.printComments := true),
" print cabs tree structure in comments in cabs output";
"--patchFile", Arg.String (fun pf -> patchFileName := pf),
"<fname> name the file containing patching transformations";
"--printPatched", Arg.Unit (fun _ -> printPatchedFiles := true),
" print patched CABS files after patching, to *.patched";
"--printProtos", Arg.Unit (fun _ -> doPrintProtos := true),
" print prototypes to safec.proto.h after parsing";
"--printNotice", Arg.Set printNotice,
" include a comment saying printed by FrontC";
]
exception ParseError of string
exception CabsOnly
(* parse, and apply patching *)
let rec parse_to_cabs fname =
begin
(* parse the patch file if it isn't parsed already *)
if ((!patchFileName <> "") && (isNone !patchFile)) then (
(* parse the patch file *)
patchFile := Some(parse_to_cabs_inner !patchFileName);
if !E.hadErrors then
(failwith "There were parsing errors in the patch file")
);
(* now parse the file we came here to parse *)
let cabs = parse_to_cabs_inner fname in
if !E.hadErrors then
E.s (E.error "There were parsing errors in %s" fname);
(* and apply the patch file, return transformed file *)
let patched = match !patchFile with
| Some(pf) -> (
(* save old value of out so I can use it for debugging during patching *)
let oldOut = !out in
(* reset out so we don't try to print the patch file to it *)
out := None;
(trace "patch" (dprintf "newpatching %s\n" fname));
let result = (Stats.time "newpatch" (Patch.applyPatch pf) cabs) in
if (!printPatchedFiles) then begin
let outFname:string = fname ^ ".patched" in
(trace "patch" (dprintf "printing patched version of %s to %s\n"
fname outFname));
let o = (open_out outFname) in
(Cprint.printFile o result);
(close_out o)
end;
(* restore out *)
Cprint.flush ();
out := oldOut;
result
)
| None -> cabs
in
(* print it ... *)
(match !out with
Some o -> begin
(trace "sm" (dprintf "writing the cabs output\n"));
if !printNotice then output_string o ("/* Generated by Frontc */\n");
Stats.time "printCABS" (Cprint.printFile o) patched;
close_output ();
raise CabsOnly
end
| None -> ());
if !E.hadErrors then
raise Parsing.Parse_error;
(* and return the patched source *)
patched
end
and clexer lexbuf =
Clexer.clear_white ();
Clexer.clear_lexeme ();
let token = Clexer.initial lexbuf in
let white = Clexer.get_white () in
let cabsloc = Clexer.currentLoc () in
let lexeme = Clexer.get_extra_lexeme () ^ Lexing.lexeme lexbuf in
white,lexeme,token,cabsloc
(* just parse *)
and parse_to_cabs_inner (fname : string) =
try
if !E.verboseFlag then ignore (E.log "Frontc is parsing %s\n" fname);
flush !E.logChannel;
let lexbuf = Clexer.init ~filename:fname in
let cabs = Stats.time "parse" (Cparser.interpret (Whitetrack.wraplexer clexer)) lexbuf in
Whitetrack.setFinalWhite (Clexer.get_white ());
Clexer.finish ();
(fname, cabs)
with (Sys_error msg) -> begin
ignore (E.log "Cannot open %s : %s\n" fname msg);
Clexer.finish ();
close_output ();
raise (ParseError("Cannot open " ^ fname ^ ": " ^ msg ^ "\n"))
end
| Parsing.Parse_error -> begin
ignore (E.log "Parsing error");
Clexer.finish ();
close_output ();
raise (ParseError("Parse error"))
end
| e -> begin
ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
Clexer.finish ();
raise e
end
(* print to safec.proto.h the prototypes of all functions that are defined *)
let printPrototypes ((fname, file) : Cabs.file) : unit =
begin
(*ignore (E.log "file has %d defns\n" (List.length file));*)
let chan = open_out "safec.proto.h" in
ignore (fprintf chan "/* generated prototypes file, %d defs */\n" (List.length file));
Whitetrack.setOutput chan;
let counter : int ref = ref 0 in
let loop (d : Cabs.definition) = begin
match d with
| Cabs.FUNDEF(name, _, loc, _) -> (
match name with
| (_, (funcname, Cabs.PROTO(_,_,_), _, _)) -> (
incr counter;
ignore (fprintf chan "\n/* %s from %s:%d */\n"
funcname loc.Cabs.filename loc.Cabs.lineno);
flush chan;
Cprint.print_single_name name;
Cprint.print_unescaped_string ";";
Cprint.force_new_line ();
Cprint.flush ()
)
| _ -> ()
)
| _ -> ()
end in
(List.iter loop file);
ignore (fprintf chan "\n/* wrote %d prototypes */\n" !counter);
close_out chan;
ignore (E.log "printed %d prototypes from %d defns to safec.proto.h\n"
!counter (List.length file))
end
let parse_helper fname =
(trace "sm" (dprintf "parsing %s to Cabs\n" fname));
let cabs = parse_to_cabs fname in
(* Now (return a function that will) convert to CIL *)
fun _ ->
(trace "sm" (dprintf "converting %s from Cabs to CIL\n" fname));
let cil = Stats.time "convert to CIL" Cabs2cil.convFile cabs in
if !doPrintProtos then (printPrototypes cabs);
cabs, cil
let parse fname = (fun () -> snd(parse_helper fname ()))
let parse_with_cabs fname = (fun () -> parse_helper fname ())