Merge pull request #587 from goblint/deps_from_cil

Compute dependencies of file via CIL instead of from `.d` files generated during pre-processing

Author: michael-schwarz

goblint.opam

@@ -63,7 +63,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#f8c8fe4da12ebe59a7b87851366dfc49b6e4b9ae" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -110,7 +110,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#f8c8fe4da12ebe59a7b87851366dfc49b6e4b9ae"
+    "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#f8c8fe4da12ebe59a7b87851366dfc49b6e4b9ae" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

src/framework/analyses.ml

@@ -268,19 +268,10 @@ struct
       printf "Writing Sarif to file: %s\n%!" (get_string "outfile");
       Yojson.Safe.pretty_to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list));
     | "json-messages" ->
-      let files =
-        let module SH = BatHashtbl.Make (Basetype.RawStrings) in
-        let files = SH.create 100 in
-        iterGlobals file (function
-            | GFun (_, loc)
-            | GVar (_, _, loc) ->
-              SH.replace files loc.file (Hashtbl.find_option Preprocessor.dependencies loc.file)
-            | _ -> () (* TODO: add locs from everything else? would also include system headers *)
-          );
-        files |> SH.to_list
-      in
+      let files = Hashtbl.to_list Preprocessor.dependencies in
+      let filter_system = List.filter_map (fun (f,system) -> if system then None else Some f) in
       let json = `Assoc [
-          ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files));
+          ("files", `Assoc (List.map (Tuple2.map2 (fun deps -> [%to_yojson:string list] @@ filter_system deps)) files));
           ("messages", Messages.Table.to_yojson ());
         ]
       in

src/maingoblint.ml

@@ -159,14 +159,11 @@ let basic_preprocess ~all_cppflags fname =
   else
     (* Preprocess using cpp. *)
     (* ?? what is __BLOCKS__? is it ok to just undef? this? http://en.wikipedia.org/wiki/Blocks_(C_language_extension) *)
-    let deps_file = Filename.chop_extension nname ^ ".d" in
-    let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -MMD -MT " ^ fname ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
+    let command = (Preprocessor.get_cpp ()) ^ " --undef __BLOCKS__ " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " \"" ^ fname ^ "\" -o \"" ^ nname ^ "\"" in
     if get_bool "dbg.verbose" then print_endline command;
 
     try match Unix.system command with
-      | Unix.WEXITED 0 ->
-        Preprocessor.parse_makefile_deps deps_file;
-        nname
+      | Unix.WEXITED 0 -> nname
       | _ -> eprintf "Goblint: Preprocessing failed."; raise Exit
     with Unix.Unix_error (e, f, a) ->
       eprintf "%s at syscall %s with argument \"%s\".\n" (Unix.error_message e) f a; raise Exit
@@ -291,7 +288,13 @@ let preprocess_files () =
 let merge_preprocessed cpp_file_names =
   (* get the AST *)
   if get_bool "dbg.verbose" then print_endline "Parsing files.";
-  let files_AST = List.map Cilfacade.getAST cpp_file_names in
+  let get_ast_and_record_deps f =
+    let file = Cilfacade.getAST f in
+    (* Drop <built-in> and <command-line> from dependencies *)
+    Hashtbl.add Preprocessor.dependencies f @@ List.filter (fun (n,_) -> n <> "<built-in>" && n <> "<command-line>") file.files;
+    file
+  in
+  let files_AST = List.map (get_ast_and_record_deps) cpp_file_names in
 
   let cilout =
     if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")

src/util/compilationDatabase.ml

@@ -55,12 +55,11 @@ let load_and_preprocess ~all_cppflags filename =
     else
       let preprocessed_file = Filename.concat preprocessed_dir (Filename.chop_extension (GobFilename.chop_common_prefix database_dir file) ^ ".i") in
       GobSys.mkdir_parents preprocessed_file;
-      let deps_file = Filename.chop_extension preprocessed_file ^ ".d" in
       let preprocess_command = match obj.command, obj.arguments with
         | Some command, None ->
           (* TODO: extract o_file *)
           let command = reroot command in
-          let preprocess_command = Str.replace_first command_program_regexp ("\\1 " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -E -MMD -MT " ^ file) command in
+          let preprocess_command = Str.replace_first command_program_regexp ("\\1 " ^ String.join " " (List.map Filename.quote all_cppflags) ^ " -E") command in
           let preprocess_command = Str.replace_first command_o_regexp ("-o " ^ preprocessed_file) preprocess_command in
           if preprocess_command = command then (* easier way to check if match was found (and replaced) *)
             failwith "CompilationDatabase.preprocess: no -o argument found for " ^ file
@@ -72,7 +71,7 @@ let load_and_preprocess ~all_cppflags filename =
             | (o_i, _) ->
               begin match List.split_at o_i arguments with
                 | (arguments_program :: arguments_init, _ :: o_file :: arguments_tl) ->
-                  let preprocess_arguments = all_cppflags @ "-E" :: "-MMD" :: "-MT" :: file :: arguments_init @ "-o" :: preprocessed_file :: arguments_tl in
+                  let preprocess_arguments = all_cppflags @ "-E" :: arguments_init @ "-o" :: preprocessed_file :: arguments_tl in
                   Filename.quote_command arguments_program preprocess_arguments
                 | _ ->
                   failwith "CompilationDatabase.preprocess: no -o argument value found for " ^ file
@@ -89,7 +88,6 @@ let load_and_preprocess ~all_cppflags filename =
       if GobConfig.get_bool "dbg.verbose" then
         Printf.printf "Preprocessing %s\n  to %s\n  using %s\n  in %s\n" file preprocessed_file preprocess_command cwd;
       system ~cwd preprocess_command; (* command/arguments might have paths relative to directory *)
-      Preprocessor.parse_makefile_deps deps_file;
       Some preprocessed_file
     in
   parse_file filename

src/util/dune

@@ -1,2 +1,2 @@
-(ocamllex oilLexer makefileLexer)
-(ocamlyacc oilParser makefileParser)
+(ocamllex oilLexer)
+(ocamlyacc oilParser)

src/util/makefileLexer.mll

@@ -37,12 +37,4 @@ let cpp =
 let get_cpp () = Lazy.force cpp
 
 
-let dependencies: (string, string list) Hashtbl.t = Hashtbl.create 3
-
-let parse_makefile_deps makefile =
-  BatFile.with_file_in makefile (fun input ->
-      let lexbuf = Lexing.from_channel input in
-      let (rule, deps) = MakefileParser.deps MakefileLexer.token lexbuf in
-      let deps = List.remove deps rule in
-      Hashtbl.replace dependencies rule deps
-    )
+let dependencies: (string, (string*bool) list) Hashtbl.t = Hashtbl.create 3