Merge pull request #73 from goblint/input_filelist

stilscher · web-flow · commit 147b210c7673 · 2022-02-10T11:53:46.000+01:00
Maintain a list of all input files that CIL encountered during lexing
diff --git a/.merlin b/.merlin
@@ -9,4 +9,5 @@ B _build/src/ext/
 B _build/src/ext/pta/
 B _build/src/frontc/
 B _build/src/ocamlutil/
-PKG findlib, zarith
+PKG findlib
+PKG zarith
diff --git a/src/cil.ml b/src/cil.ml
@@ -156,6 +156,9 @@ type file =
           should always be false if there is no global initializer. When
           you create a global initialization CIL will try to insert code in
           main to call it. *)
+      files: (string * bool) list;
+      (** A list of those files that were encountered during parsing of this CIL file,
+          and whether they are system header files  *)
     }
 
 and comment = location * string
@@ -5001,7 +5004,8 @@ let dummyFile =
   { globals = [];
     fileName = "<dummy>";
     globinit = None;
-    globinitcalled = false;}
+    globinitcalled = false;
+    files = []; }
 
 (***** Load and store files as unmarshalled Ocaml binary data. ****)
 type savedFile =
diff --git a/src/cil.mli b/src/cil.mli
@@ -93,6 +93,9 @@ type file =
        * create a global initialization CIL will try to insert code in main
        * to call it. This will not happen if your file does not contain a
        * function called "main" *)
+       files: (string * bool) list;
+       (** A list of those files that were encountered during parsing of this CIL file,
+        * and whether they are system header files *)
     }
 (** Top-level representation of a C source file *)
 
diff --git a/src/formatcil.ml b/src/formatcil.ml
@@ -80,15 +80,15 @@ let doParse (prog: string)
       Formatparse.initialize Formatlex.initial lexbuf;
       let res = theParser Formatlex.initial lexbuf in
       H.add memoTable prog res;
-      Formatlex.finish ();
+      ignore @@ Formatlex.finish ();
       res
     with Parsing.Parse_error -> begin
-      Formatlex.finish ();
+      ignore @@ Formatlex.finish ();
       E.s (E.error "Parsing error: %s" prog)
     end
     | e -> begin
         ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
-        Formatlex.finish ();
+        ignore @@ Formatlex.finish ();
         raise e
     end
   end
diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
@@ -189,8 +189,9 @@ and definition =
  | STATIC_ASSERT of expression * string * cabsloc
 
 
-(* the string is a file name, and then the list of toplevel forms *)
-and file = string * definition list
+(* the string is a file name, then the list of toplevel forms, and finally a list of filenames
+   encountered during parsing and whether they are system headers *)
+and file = string * definition list * (string * bool) list
 
 
 (*
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
@@ -5996,7 +5996,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function
                  sformals = []; (* Not final yet *)
                  smaxid   = 0;
                  sbody    = dummyFunDec.sbody; (* Not final yet *)
-		 smaxstmtid = None;
+                 smaxstmtid = None;
                  sallstmts = [];
                };
 	    !currentFunctionFDEC.svar.vdecl <- funloc;
@@ -6899,7 +6899,7 @@ let convFile (f : A.file) : Cil.file =
   Cil.initCIL (); (* make sure we have initialized CIL *)
 
   (* remove parentheses from the Cabs *)
-  let fname,dl = stripParenFile f in
+  let fname,dl,files = stripParenFile f in
 
   (* Clean up the global types *)
   initGlobals();
@@ -6988,4 +6988,5 @@ let convFile (f : A.file) : Cil.file =
     globals  = !globals;
     globinit = None;
     globinitcalled = false;
+    files = files;
   }
diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml
@@ -582,7 +582,7 @@ and childrenAttribute vis ((n, el) as input) =
 and visitCabsAttributes vis (al: attribute list) : attribute list =
   mapNoCopyList (visitCabsAttribute vis) al
 
-let visitCabsFile (vis: cabsVisitor) ((fname, f): file) : file =
-  (fname, mapNoCopyList (visitCabsDefinition vis) f)
+let visitCabsFile (vis: cabsVisitor) ((fname, f, files): file) : file =
+  (fname, mapNoCopyList (visitCabsDefinition vis) f, files)
 
     (* end of file *)
diff --git a/src/frontc/clexer.mli b/src/frontc/clexer.mli
@@ -1,11 +1,11 @@
 (*
  *
- * Copyright (c) 2001-2002, 
+ * 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:
@@ -36,14 +36,15 @@
  *)
 
 
-(* This interface is generated manually. The corresponding .ml file is 
- * generated automatically and is placed in ../obj/clexer.ml. The reason we 
- * want this interface is to avoid confusing make with freshly generated 
+(* This interface is generated manually. The corresponding .ml file is
+ * generated automatically and is placed in ../obj/clexer.ml. The reason we
+ * want this interface is to avoid confusing make with freshly generated
  * interface files *)
 
 
 val init: filename:string -> Lexing.lexbuf
-val finish: unit -> unit
+val finish: unit -> (string * bool) list (* Return the list of filenames encountered during lexing
+                                            and whether they are system headers *)
 
 (* This is the main parser function *)
 val initial: Lexing.lexbuf -> Cparser.token
@@ -59,4 +60,3 @@ val get_extra_lexeme: unit -> string
 val clear_white: unit -> unit
 val clear_lexeme: unit -> unit
 val currentLoc : unit -> Cabs.cabsloc
-
diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll
@@ -634,11 +634,9 @@ and hash = parse
 and file =  parse
         '\n'		        {addWhite lexbuf; E.newline (); initial lexbuf}
 |	blank			{addWhite lexbuf; file lexbuf}
-|	'"' [^ '\012' '\t' '"']* '"' 	{ addWhite lexbuf;  (* '"' *)
-                                   let n = Lexing.lexeme lexbuf in
-                                   let n1 = String.sub n 1
-                                       ((String.length n) - 2) in
-                                   E.setCurrentFile n1;
+|	'"' ([^ '\012' '\t' '"']* as filename) '"' ((' ' ['1' -'4'])* as flags)
+       { addWhite lexbuf;  (* '"' *)
+         E.setCurrentFile filename (String.contains flags '3');
 				 endline lexbuf}
 
 |	_			{addWhite lexbuf; endline lexbuf}
diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
@@ -933,7 +933,7 @@ end
 (*  print abstrac_syntax -> ()
 **		Pretty printing the given abstract syntax program.
 *)
-let printFile (result : out_channel) ((fname, defs) : file) =
+let printFile (result : out_channel) ((fname, defs, _) : file) =
   Whitetrack.setOutput result;
   print_defs defs;
   Whitetrack.printEOF ();
diff --git a/src/frontc/frontc.ml b/src/frontc/frontc.ml
@@ -188,31 +188,31 @@ and parse_to_cabs_inner (fname : string) =
     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)
+    let files = Clexer.finish () in
+    (fname, cabs, files)
   with (Sys_error msg) -> begin
     ignore (E.log "Cannot open %s : %s\n" fname msg);
-    Clexer.finish ();
+    ignore @@ Clexer.finish ();
     close_output ();
     raise (ParseError("Cannot open " ^ fname ^ ": " ^ msg ^ "\n"))
   end
   | Parsing.Parse_error -> begin
       ignore (E.log "Parsing error");
-      Clexer.finish ();
+      ignore @@ Clexer.finish ();
       close_output ();
       (* raise (ParseError("Parse error")) *)
       let backtrace = Printexc.get_raw_backtrace () in
       Printexc.raise_with_backtrace (ParseError("Parse error")) backtrace (* re-raise with captured inner backtrace *)
   end
   | e -> begin
       ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
-      Clexer.finish ();
+      ignore @@ 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 =
+let printPrototypes ((fname, file, _) : Cabs.file) : unit =
 begin
   (*ignore (E.log "file has %d defns\n" (List.length file));*)
 
diff --git a/src/frontc/patch.ml b/src/frontc/patch.ml
@@ -333,9 +333,8 @@ let gettime () : float =
 
 let rec applyPatch (patchFile : file) (srcFile : file) : file =
 begin
-  let patch : definition list = (snd patchFile) in
-  let srcFname : string = (fst srcFile) in
-  let src : definition list = (snd srcFile) in
+  let (_, patch, _) = patchFile in
+  let (srcFname, src, srcFiles) = srcFile in
 
   (trace "patchTime" (dprintf "applyPatch start: %f\n" (gettime ())));
   if (traceActive "patchDebug") then
@@ -417,7 +416,7 @@ begin
   );
 
   (trace "patchTime" (dprintf "applyPatch finish: %f\n" (gettime ())));
-  (srcFname, result)
+  (srcFname, result, srcFiles)
 end
 
 
diff --git a/src/mergecil.ml b/src/mergecil.ml
@@ -1775,6 +1775,9 @@ let merge (files: file list) (newname: string) : file =
   currentFidx := 0;
   List.iter (fun f -> oneFilePass2 f; incr currentFidx) files;
 
+  let filesH = Hashtbl.create 50 in
+  List.iter (fun f -> List.iter (fun f -> Hashtbl.replace filesH f ()) f.files) files;
+
   (* Now reverse the result and return the resulting file *)
   let rec revonto acc = function
       [] -> acc
@@ -1784,7 +1787,9 @@ let merge (files: file list) (newname: string) : file =
     { fileName = newname;
       globals  = revonto (revonto [] !theFile) !theFileTypes;
       globinit = None;
-      globinitcalled = false;} in
+      globinitcalled = false;
+      files = Hashtbl.fold (fun k v acc -> k::acc) filesH []; (* keys are unique *)}
+  in
   init (); (* Make the GC happy *)
   (* We have made many renaming changes and sometimes we have just guessed a
    * name wrong. Make sure now that the local names are unique. *)
diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml
@@ -170,7 +170,8 @@ let theLexbuf = ref (Lexing.from_string "")
 let fail format = Pretty.gprintf (fun x -> Pretty.fprint stderr ~width:80 x;
                                            raise (Failure "")) format
 
-
+(***** Keep track of encountered files ******)
+let files = Hashtbl.create 10
 
 (***** Handling parsing errors ********)
 type parseinfo =
@@ -256,6 +257,7 @@ let startParsing ?(useBasename=true) (fname: string) =
       num_errors = 0 } in
 
   current := i;
+  Hashtbl.clear files;
   lexbuf
 
 let startParsingFromString ?(file="<string>") ?(line=1) (str: string) =
@@ -269,12 +271,15 @@ let startParsingFromString ?(file="<string>") ?(line=1) (str: string) =
       num_errors = 0 }
   in
   current := i;
+  Hashtbl.clear files;
   lexbuf
 
 let finishParsing () =
   let i = !current in
   (match i.inchan with Some c -> close_in c | _ -> ());
-  current := dummyinfo
+  current := dummyinfo;
+  (* keys are unique *)
+  Hashtbl.fold (fun k v acc -> (k,v)::acc) files []
 
 
 (* Call this function to announce a new line *)
@@ -290,8 +295,10 @@ let newHline () =
 let setCurrentLine (i: int) =
   !current.linenum <- i
 
-let setCurrentFile (n: string) =
-  !current.fileName <- cleanFileName n
+let setCurrentFile (n: string) (system_header: bool) =
+  let cn = cleanFileName n in
+  Hashtbl.replace files cn system_header;
+  !current.fileName <- cn
 
 
 let max_errors = 20  (* Stop after 20 errors *)
diff --git a/src/ocamlutil/errormsg.mli b/src/ocamlutil/errormsg.mli

Original file line number	Diff line number	Diff line change
`@@ -93,6 +93,9 @@ type file =`
`93`	`93`	`* create a global initialization CIL will try to insert code in main`
`94`	`94`	`* to call it. This will not happen if your file does not contain a`
`95`	`95`	`* function called "main" *)`
	`96`	`+ files: (string * bool) list;`
	`97`	`+ (** A list of those files that were encountered during parsing of this CIL file,`
	`98`	`+ * and whether they are system header files *)`
`96`	`99`	`}`
`97`	`100`	`(** Top-level representation of a C source file *)`
`98`	`101`