forked from kframework/c-semantics
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcabsDriver.ml
198 lines (171 loc) · 6.34 KB
/
cabsDriver.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
(*
*
* Copyright (c) 2001-2002,
* George C. Necula <[email protected]>
* Scott McPeak <[email protected]>
* Wes Weimer <[email protected]>
* 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.
*
*)
(* main.ml *)
(* this module is the program entry point for the 'cilly' program, *)
(* which reads a C program file, parses it, translates it to the CIL *)
(* intermediate language, and then renders that back into C *)
module F = Frontc
(* module C = Cil *)
(* module CK = Check *)
module E = Errormsg
open Printf
open XmlPrinter
type outfile =
{ fname: string;
fchan: out_channel }
(* let outChannel : outfile option ref = ref None *)
let replace input output =
Str.global_replace (Str.regexp_string input) output
let fileNames : string list ref = ref []
let recordFile fname =
fileNames := fname :: (!fileNames)
let isXML = ref false
let noscores s =
(replace "_" "-" s)
let fileContents : string ref = ref ""
let parse_helper fname =
let cabs = F.parse_to_cabs fname in
cabs
let parseOneFile (fname: string) =
(* PARSE *)
(* if !Cilutil.printStages then ignore (E.log "Parsing %s\n" fname); *)
(*let cil = F.parse fname () in *)
let cabs = parse_helper fname in
cabs
let trueFilename : string ref = ref ""
let rec processOneFile (cabs: Cabs.file) =
fileContents := "";
begin (
let (inputFilename, _) = cabs in
let ic = open_in inputFilename in (
try
while true do
let line = input_line ic in (* read line from in_channel and discard \n *)
if (String.length line < 5 or Str.first_chars line 5 <> "# 1 \"") then
fileContents := (!fileContents ^ line ^ "\n");
done
with e -> (* some unexpected exception occurs *)
close_in_noerr ic; (* emergency closing *)
);
let inputFilename =
if (compare !trueFilename "" == 0) then inputFilename else !trueFilename in
let data = cabsToXML cabs !fileContents inputFilename in
printf "%s\n" data;
(* )) *)
);
if !E.hadErrors then E.s ("Error: Error while processing file; see above for details.");
end
(***** MAIN *****)
let theMain () =
let usageMsg = "Usage: cparser [options] source-files" in
(* Processign of output file arguments *)
let openFile (what: string) (takeit: outfile -> unit) (fl: string) =
if !E.verboseFlag then
ignore (Printf.printf "Setting %s to %s\n" what fl);
(try takeit { fname = fl;
fchan = open_out fl }
with _ ->
raise (Arg.Bad ("Cannot open " ^ what ^ " file " ^ fl)))
in
let outName = ref "" in
(* sm: enabling this by default, since I think usually we
* want 'cilly' transformations to preserve annotations; I
* can easily add a command-line flag if someone sometimes
* wants these suppressed *)
(* C.print_CIL_Input := true; *)
(*********** COMMAND LINE ARGUMENTS *****************)
(* Construct the arguments for the features configured from the Makefile *)
let blankLine = ("", Arg.Unit (fun _ -> ()), "") in
let argDescr =
[
(* "--out", Arg.String (openFile "output"
(fun oc -> outChannel := Some oc)),
" the name of the output AST."; *)
(* "--xml", Arg.Set isXML,
" output should be in XML format"; *)
"--trueName", Arg.String (fun x -> trueFilename := x),
"filename The original name of the file"
] in
begin
(* this point in the code is the program entry point *)
(* Stats.reset Stats.HardwareIfAvail; *)
(* parse the command-line arguments *)
Arg.parse (Arg.align argDescr) recordFile usageMsg;
(* now we have just one CIL "file" to deal with *)
let one =
match !fileNames with
[one] -> parseOneFile one
| [] -> E.s ("Error: No arguments for CIL")
| _ -> E.s ("Error: Can only handle one input file")
in
if !E.hadErrors then
E.s ("Error: Cabs2cil had some errors");
(* process the CIL file (merged if necessary) *)
processOneFile one
end
;;
(* Define a wrapper for main to
* intercept the exit *)
let failed = ref false
let cleanup () =
(* if !E.verboseFlag || !Cilutil.printStats then
Stats.print stderr "Timings:\n"; *)
if !E.logChannel != stderr then
close_out (! E.logChannel);
(* (match ! outChannel with Some c -> close_out c.fchan | _ -> ()) *)
(* Without this handler, cilly.asm.exe will quit silently with return code 0
when a segfault happens. *)
(*
let handleSEGV code =
if !Cil.currentLoc == Cil.locUnknown then
E.log "**** Segmentation fault (possibly a stack overflow)\n"
else begin
E.log ("**** Segmentation fault (possibly a stack overflow) "^^
"while processing %a\n")
Cil.d_loc !Cil.currentLoc
end;
exit code
let _ = Sys.set_signal Sys.sigsegv (Sys.Signal_handle handleSEGV);
*)
;;
begin
try
theMain ();
with F.CabsOnly -> (* this is OK *) ()
end;
cleanup ();
exit (if !failed then 1 else 0)