← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to cil/src/frontc/frontc.ml

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
cil/src/frontc/frontc.ml
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  Copyright (C) 2001-2003,                                              *)
 
4
(*   George C. Necula    <necula@cs.berkeley.edu>                         *)
 
5
(*   Scott McPeak        <smcpeak@cs.berkeley.edu>                        *)
 
6
(*   Wes Weimer          <weimer@cs.berkeley.edu>                         *)
 
7
(*   Ben Liblit          <liblit@cs.berkeley.edu>                         *)
 
8
(*  All rights reserved.                                                  *)
 
9
(*                                                                        *)
 
10
(*  Redistribution and use in source and binary forms, with or without    *)
 
11
(*  modification, are permitted provided that the following conditions    *)
 
12
(*  are met:                                                              *)
 
13
(*                                                                        *)
 
14
(*  1. Redistributions of source code must retain the above copyright     *)
 
15
(*  notice, this list of conditions and the following disclaimer.         *)
 
16
(*                                                                        *)
 
17
(*  2. Redistributions in binary form must reproduce the above copyright  *)
 
18
(*  notice, this list of conditions and the following disclaimer in the   *)
 
19
(*  documentation and/or other materials provided with the distribution.  *)
 
20
(*                                                                        *)
 
21
(*  3. The names of the contributors may not be used to endorse or        *)
 
22
(*  promote products derived from this software without specific prior    *)
 
23
(*  written permission.                                                   *)
 
24
(*                                                                        *)
 
25
(*  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS   *)
 
26
(*  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT     *)
 
27
(*  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS     *)
 
28
(*  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE        *)
 
29
(*  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,   *)
 
30
(*  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,  *)
 
31
(*  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;      *)
 
32
(*  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER      *)
 
33
(*  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT    *)
 
34
(*  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN     *)
 
35
(*  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE       *)
 
36
(*  POSSIBILITY OF SUCH DAMAGE.                                           *)
 
37
(*                                                                        *)
 
38
(*  File modified by CEA (Commissariat � l'�nergie Atomique).             *)
 
39
(**************************************************************************)
 
40
 
 
41
module E = Errormsg
 
42
open Trace
 
43
open Pretty
 
44
module Stats = struct
 
45
  let time _ x y = x y
 
46
end
 
47
(* Output management *)
 
48
let out : out_channel option ref = ref None
 
49
let close_me = ref false
 
50
 
 
51
let close_output _ =
 
52
  match !out with
 
53
    None -> ()
 
54
  | Some o -> begin
 
55
      flush o;
 
56
      if !close_me then close_out o else ();
 
57
      close_me := false
 
58
  end
 
59
 
 
60
let set_output filename =
 
61
  close_output ();
 
62
  let out_chan = try open_out filename 
 
63
    with Sys_error msg -> 
 
64
    (output_string stderr ("Error while opening output: " ^ msg); exit 1) in
 
65
  out := Some out_chan;
 
66
  Whitetrack.setOutput out_chan;
 
67
  close_me := true
 
68
 
 
69
   (* Signal that we are in MS VC mode *)
 
70
let setMSVCMode () =
 
71
  Cprint.msvcMode := true
 
72
 
 
73
(* filename for patching *)
 
74
let patchFileName : string ref = ref ""      (* by default do no patching *)
 
75
 
 
76
(* patching file contents *)
 
77
let patchFile : Cabs.file option ref = ref None
 
78
 
 
79
(* whether to print the patched CABS files *)
 
80
let printPatchedFiles : bool ref = ref false
 
81
 
 
82
(* whether to print a file of prototypes after parsing *)
 
83
let doPrintProtos : bool ref = ref false
 
84
 
 
85
(* this seems like something that should be built-in.. *)
 
86
let isNone (o : 'a option) : bool =
 
87
begin
 
88
  match o with
 
89
  | Some _ -> false
 
90
  | None -> true
 
91
end
 
92
 
 
93
let printNotice = ref false
 
94
 
 
95
(*
 
96
** Argument definition
 
97
*)
 
98
let args : (string * Arg.spec * string) list =
 
99
[
 
100
  "--cabsonly", Arg.String set_output, "<fname>: CABS output file name";
 
101
  "--printComments", Arg.Unit (fun _ -> Cprint.printComments := true),
 
102
             ": print cabs tree structure in comments in cabs output";
 
103
  "--patchFile", Arg.String (fun pf -> patchFileName := pf),
 
104
             "<fname>: name the file containing patching transformations";
 
105
  "--printPatched", Arg.Unit (fun _ -> printPatchedFiles := true),
 
106
             ": print patched CABS files after patching, to *.patched";
 
107
  "--printProtos", Arg.Unit (fun _ -> doPrintProtos := true),
 
108
             ": print prototypes to safec.proto.h after parsing";
 
109
  "--printNotice", Arg.Set printNotice,
 
110
             ": include a comment saying printed by FrontC";
 
111
]
 
112
 
 
113
exception ParseError of string
 
114
exception CabsOnly
 
115
 
 
116
(* parse, and apply patching *)
 
117
let rec parse_to_cabs fname =
 
118
begin
 
119
  (* parse the patch file if it isn't parsed already *)
 
120
  if ((!patchFileName <> "") && (isNone !patchFile)) then (
 
121
    (* parse the patch file *)
 
122
    patchFile := Some(parse_to_cabs_inner !patchFileName);
 
123
    if !E.hadErrors then
 
124
      (failwith "There were parsing errors in the patch file")
 
125
  );
 
126
 
 
127
  (* now parse the file we came here to parse *)
 
128
  let cabs = parse_to_cabs_inner fname in
 
129
  if !E.hadErrors then 
 
130
    E.s (E.error "There were parsing errors in %s\n" fname);
 
131
  (* and apply the patch file, return transformed file *)
 
132
  let patched = match !patchFile with
 
133
 
 
134
    | Some(pf) -> (
 
135
        (* save old value of out so I can use it for debugging during patching *)
 
136
        let oldOut = !out in
 
137
 
 
138
        (* reset out so we don't try to print the patch file to it *)
 
139
        out := None;
 
140
 
 
141
        (trace "patch" (dprintf "newpatching %s\n" fname));
 
142
        let result = (Stats.time "newpatch" (Patch.applyPatch pf) cabs) in
 
143
 
 
144
        if (!printPatchedFiles) then begin                              
 
145
          let outFname:string = fname ^ ".patched" in
 
146
          (trace "patch" (dprintf "printing patched version of %s to %s\n"
 
147
                                  fname outFname));
 
148
          let o = (open_out outFname) in
 
149
          (Cprint.printFile o result);
 
150
          (close_out o)
 
151
        end;
 
152
 
 
153
        (* restore out *)
 
154
        Cprint.flush ();
 
155
        out := oldOut;
 
156
 
 
157
        result
 
158
      )
 
159
    | None -> cabs
 
160
  in
 
161
  (* print it ... *)
 
162
  (match !out with
 
163
    Some o -> begin
 
164
      (trace "sm" (dprintf "writing the cabs output\n"));
 
165
      if !printNotice then output_string o ("/* Generated by Frontc */\n");
 
166
      Stats.time "printCABS" (Cprint.printFile o) patched;
 
167
      close_output ();
 
168
      raise CabsOnly
 
169
    end
 
170
  | None -> ());
 
171
  if !E.hadErrors then
 
172
    raise Parsing.Parse_error;
 
173
 
 
174
  (* and return the patched source *)
 
175
  patched
 
176
end
 
177
 
 
178
and clexer lexbuf =
 
179
    Clexer.clear_white ();
 
180
    Clexer.clear_lexeme ();
 
181
    let token = Clexer.initial lexbuf in
 
182
    let white = Clexer.get_white () in
 
183
    let cabsloc = Clexer.currentLoc () in
 
184
    let lexeme = Clexer.get_extra_lexeme () ^ Lexing.lexeme lexbuf in
 
185
    white,lexeme,token,cabsloc
 
186
 
 
187
(* just parse *)
 
188
and parse_to_cabs_inner (fname : string) =
 
189
  try
 
190
    if !E.verboseFlag then ignore (E.log "Frontc is parsing %s\n" fname);
 
191
    flush !E.logChannel;
 
192
    E.hadErrors := false;
 
193
    let lexbuf = Clexer.init fname in
 
194
    let cabs = Stats.time "parse" (Cparser.file (Whitetrack.wraplexer clexer)) lexbuf in
 
195
(*    Cprint.print_defs cabs;*)
 
196
    Whitetrack.setFinalWhite (Clexer.get_white ());
 
197
    Clexer.finish ();
 
198
    let fname = match !E.first_filename_encountered with 
 
199
      | None -> fname 
 
200
      | Some f -> f
 
201
    in
 
202
    (fname, cabs)
 
203
  with (Sys_error msg) -> begin
 
204
    ignore (E.log "Cannot open %s : %s\n" fname msg);
 
205
    Clexer.finish ();
 
206
    close_output ();
 
207
    raise (ParseError("Cannot open " ^ fname ^ ": " ^ msg ^ "\n"))
 
208
  end
 
209
  | Parsing.Parse_error -> begin
 
210
      ignore (E.log "Parsing error\n");
 
211
      Clexer.finish ();
 
212
      close_output ();
 
213
      raise (ParseError("Parse error"))
 
214
  end
 
215
  (*| e -> begin
 
216
      ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
 
217
      Clexer.finish ();
 
218
      raise e
 
219
  end
 
220
  *)
 
221
  
 
222
(* print to safec.proto.h the prototypes of all functions that are defined *)
 
223
let printPrototypes ((_fname, file) : Cabs.file) : unit =
 
224
begin
 
225
  (*ignore (E.log "file has %d defns\n" (List.length file));*)
 
226
 
 
227
  let chan = open_out "safec.proto.h" in
 
228
  ignore (fprintf chan "/* generated prototypes file, %d defs */\n" (List.length file));
 
229
  Cprint.out := chan;
 
230
 
 
231
  let counter : int ref = ref 0 in
 
232
 
 
233
  let rec loop (_ghost,(d : Cabs.definition)) = begin
 
234
    match d with
 
235
    | Cabs.FUNDEF(_,name, _, loc, _) -> (
 
236
        match name with
 
237
        | (_, (funcname, Cabs.PROTO(_,_,_), _, _)) -> (
 
238
            incr counter;          
 
239
            ignore (fprintf chan "\n/* %s from %s:%d */\n"
 
240
                                 funcname (fst loc).Lexing.pos_fname (fst loc).Lexing.pos_lnum);
 
241
            flush chan;
 
242
            Cprint.print_single_name name;
 
243
            Cprint.print_unescaped_string ";";
 
244
            Cprint.force_new_line ();
 
245
            Cprint.flush ()
 
246
          )
 
247
        | _ -> ()
 
248
      )
 
249
 
 
250
    | _ -> ()
 
251
  end in
 
252
  (List.iter loop file);
 
253
 
 
254
  ignore (fprintf chan "\n/* wrote %d prototypes */\n" !counter);
 
255
  close_out chan;
 
256
  ignore (E.log "printed %d prototypes from %d defns to safec.proto.h\n"
 
257
                !counter (List.length file))
 
258
end
 
259
 
 
260
 
 
261
 
 
262
let parse fname =
 
263
  (trace "sm" (dprintf "parsing %s to Cabs\n" fname));
 
264
  let cabs = parse_to_cabs fname in
 
265
 (*Cprint.printFile stdout cabs;*)
 
266
  (* Now (return a function that will) convert to CIL *)
 
267
  fun _ ->
 
268
    (trace "sm" (dprintf "converting %s from Cabs to CIL\n" fname));
 
269
    let cil = Stats.time "conv" Cabs2cil.convFile cabs in
 
270
    if !doPrintProtos then (printPrototypes cabs);
 
271
    (*Cil.dumpFile Cil.defaultCilPrinter stdout "behue" cil;*)
 
272
    cil,cabs
 
273
 
 
274
 
 
275
 
 
276
 
 
277
 
 
278
 
 
279
 
 
280