From a5f03d96eee482cd84861fc8cefff9eb451c0cad Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 29 Mar 2009 09:47:11 +0000 Subject: Cleaned up configure script. Distribution of CIL as an expanded source tree with changes applied (instead of original .tar.gz + patches to be applied at config time). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cil/src/main.ml | 288 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 288 insertions(+) create mode 100644 cil/src/main.ml (limited to 'cil/src/main.ml') diff --git a/cil/src/main.ml b/cil/src/main.ml new file mode 100644 index 00000000..bbdb7309 --- /dev/null +++ b/cil/src/main.ml @@ -0,0 +1,288 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula + * Scott McPeak + * Wes Weimer + * 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. + * + *) + +(* maincil *) +(* 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 Pretty +open Trace + +type outfile = + { fname: string; + fchan: out_channel } +let outChannel : outfile option ref = ref None +let mergedChannel : outfile option ref = ref None + + +let parseOneFile (fname: string) : C.file = + (* PARSE and convert to CIL *) + if !Cilutil.printStages then ignore (E.log "Parsing %s\n" fname); + let cil = F.parse fname () in + + if (not !Epicenter.doEpicenter) then ( + (* sm: remove unused temps to cut down on gcc warnings *) + (* (Stats.time "usedVar" Rmtmps.removeUnusedTemps cil); *) + (trace "sm" (dprintf "removing unused temporaries\n")); + (Rmtmps.removeUnusedTemps cil) + ); + cil + +(** These are the statically-configured features. To these we append the + * features defined in Feature_config.ml (from Makefile) *) + +let makeCFGFeature : C.featureDescr = + { C.fd_name = "makeCFG"; + C.fd_enabled = Cilutil.makeCFG; + C.fd_description = "make the program look more like a CFG" ; + C.fd_extraopt = []; + C.fd_doit = (fun f -> + ignore (Partial.calls_end_basic_blocks f) ; + ignore (Partial.globally_unique_vids f) ; + Cil.iterGlobals f (fun glob -> match glob with + Cil.GFun(fd,_) -> Cil.prepareCFG fd ; + (* jc: blockinggraph depends on this "true" arg *) + ignore (Cil.computeCFGInfo fd true) + | _ -> ()) + ); + C.fd_post_check = true; + } + +let features : C.featureDescr list = + [ Epicenter.feature; + Simplify.feature; + Canonicalize.feature; + Callgraph.feature; + Logwrites.feature; + Heapify.feature1; + Heapify.feature2; + Oneret.feature; + makeCFGFeature; (* ww: make CFG *must* come before Partial *) + Partial.feature; + Simplemem.feature; + Sfi.feature; + Dataslicing.feature; + Logcalls.feature; + Ptranal.feature; + Liveness.feature; + ] + @ Feature_config.features + +let rec processOneFile (cil: C.file) = + begin + + if !Cilutil.doCheck then begin + ignore (E.log "First CIL check\n"); + ignore (CK.checkFile [] cil); + end; + + (* Scan all the features configured from the Makefile and, if they are + * enabled then run them on the current file *) + List.iter + (fun fdesc -> + if ! (fdesc.C.fd_enabled) then begin + if !E.verboseFlag then + ignore (E.log "Running CIL feature %s (%s)\n" + fdesc.C.fd_name fdesc.C.fd_description); + (* Run the feature, and see how long it takes. *) + Stats.time fdesc.C.fd_name + fdesc.C.fd_doit cil; + (* See if we need to do some checking *) + if !Cilutil.doCheck && fdesc.C.fd_post_check then begin + ignore (E.log "CIL check after %s\n" fdesc.C.fd_name); + ignore (CK.checkFile [] cil); + end + end) + features; + + + (match !outChannel with + None -> () + | Some c -> Stats.time "printCIL" + (C.dumpFile (!C.printerForMaincil) c.fchan c.fname) cil); + + if !E.hadErrors then + E.s (E.error "Error while processing file; see above for details."); + + end + +(***** MAIN *****) +let rec theMain () = + let usageMsg = "Usage: cilly [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 featureArgs = + List.fold_right + (fun fdesc acc -> + if !(fdesc.C.fd_enabled) then + (* The feature is enabled by default *) + blankLine :: + ("--dont" ^ fdesc.C.fd_name, Arg.Clear(fdesc.C.fd_enabled), + " Disable " ^ fdesc.C.fd_description) :: + fdesc.C.fd_extraopt @ acc + else + (* Disabled by default *) + blankLine :: + ("--do" ^ fdesc.C.fd_name, Arg.Set(fdesc.C.fd_enabled), + " Enable " ^ fdesc.C.fd_description) :: + fdesc.C.fd_extraopt @ acc + ) + features + [blankLine] + in + let featureArgs = + ("", Arg.Unit (fun () -> ()), "\n\t\tCIL Features") :: featureArgs + in + + let argDescr = Ciloptions.options @ + [ + "--out", Arg.String (openFile "output" + (fun oc -> outChannel := Some oc)), + "the name of the output CIL file. The cilly script sets this for you."; + "--mergedout", Arg.String (openFile "merged output" + (fun oc -> mergedChannel := Some oc)), + "specify the name of the merged file"; + ] + @ F.args @ featureArgs in + begin + (* this point in the code is the program entry point *) + + Stats.reset (Stats.has_performance_counters ()); + + (* parse the command-line arguments *) + Arg.parse argDescr Ciloptions.recordFile usageMsg; + Cil.initCIL (); + + Ciloptions.fileNames := List.rev !Ciloptions.fileNames; + + if !Cilutil.testcil <> "" then begin + Testcil.doit !Cilutil.testcil + end else + (* parse each of the files named on the command line, to CIL *) + let files = List.map parseOneFile !Ciloptions.fileNames in + + (* if there's more than one source file, merge them together; *) + (* now we have just one CIL "file" to deal with *) + let one = + match files with + [one] -> one + | [] -> E.s (E.error "No arguments for CIL\n") + | _ -> + let merged = + Stats.time "merge" (Mergecil.merge files) + (if !outName = "" then "stdout" else !outName) in + if !E.hadErrors then + E.s (E.error "There were errors during merging\n"); + (* See if we must save the merged file *) + (match !mergedChannel with + None -> () + | Some mc -> begin + let oldpci = !C.print_CIL_Input in + C.print_CIL_Input := true; + Stats.time "printMerged" + (C.dumpFile !C.printerForMaincil mc.fchan mc.fname) merged; + C.print_CIL_Input := oldpci + end); + merged + in + + if !E.hadErrors then + E.s (E.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) + -- cgit