From cfef9be0c46ae2d24f9b50c537cb7e8fb5802d48 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 10:27:51 +0100 Subject: [PATCH 01/12] Revert "Fix Preprocessor indentation (PR #535)" This reverts commit cf405d840728ea24a74bcb472439e2e5891e2b15. --- src/util/preprocessor.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 956bf390fc..264447a282 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -41,8 +41,8 @@ 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 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 + ) From e1ba3315f4df8ad75ded2e6d9b9f71141ea9aec0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 10:28:02 +0100 Subject: [PATCH 02/12] Revert "Fix json-messages files indentation (PR #535)" This reverts commit 4536c2c1a5e0f8885ad83f3cfc636b20320a8e3b. --- src/framework/analyses.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index a1bca72492..a132f1a948 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -280,9 +280,9 @@ struct files |> SH.to_list in let json = `Assoc [ - ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files)); - ("messages", Messages.Table.to_yojson ()); - ] + ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files)); + ("messages", Messages.Table.to_yojson ()); + ] in Yojson.Safe.pretty_to_channel ~std:true out json | "none" -> () From d9b18b56e4c24792985258c36004c2fef3697b03 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 10:28:10 +0100 Subject: [PATCH 03/12] Revert "Merge pull request #535 from goblint/json-files" This reverts commit d054af352b73ced99c0e4829fcc99c69d1835fa6, reversing changes made to 13193e78c5e40ee4366d2b53c0624039c1283165. --- src/framework/analyses.ml | 18 +----------------- src/maingoblint.ml | 9 ++------- src/util/compilationDatabase.ml | 6 ++---- src/util/dune | 4 ++-- src/util/makefileLexer.mll | 11 ----------- src/util/makefileParser.mly | 24 ------------------------ src/util/preprocessor.ml | 11 ----------- 7 files changed, 7 insertions(+), 76 deletions(-) delete mode 100644 src/util/makefileLexer.mll delete mode 100644 src/util/makefileParser.mly diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index a132f1a948..bb5882a4f0 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -268,23 +268,7 @@ 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 json = `Assoc [ - ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files)); - ("messages", Messages.Table.to_yojson ()); - ] - in - Yojson.Safe.pretty_to_channel ~std:true out json + Yojson.Safe.pretty_to_channel ~std:true out (Messages.Table.to_yojson ()) | "none" -> () | s -> failwith @@ "Unsupported value for option `result`: "^s end diff --git a/src/maingoblint.ml b/src/maingoblint.ml index e664ef1de1..cc6f6ca5c6 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -159,22 +159,17 @@ 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 (** Preprocess all files. Return list of preprocessed files and the temp directory name. *) let preprocess_files () = - Hashtbl.clear Preprocessor.dependencies; (* clear for server mode *) - (* Preprocessor flags *) let cppflags = ref (get_string_list "cppflags") in diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index 54a46e2bf8..d93fb0bf4e 100644 --- a/src/util/compilationDatabase.ml +++ b/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 diff --git a/src/util/dune b/src/util/dune index d8632e1989..72f5b63234 100644 --- a/src/util/dune +++ b/src/util/dune @@ -1,2 +1,2 @@ -(ocamllex oilLexer makefileLexer) -(ocamlyacc oilParser makefileParser) +(ocamllex oilLexer) +(ocamlyacc oilParser) diff --git a/src/util/makefileLexer.mll b/src/util/makefileLexer.mll deleted file mode 100644 index 6eb51caaa6..0000000000 --- a/src/util/makefileLexer.mll +++ /dev/null @@ -1,11 +0,0 @@ -{ - open MakefileParser -} - -rule token = parse - | ' ' { token lexbuf } - | "\\\n" { token lexbuf } - | '\n' { NEWLINE } - | eof { EOF } - | ':' { COLON } - | [^':'' ''\n']+ { IDENTIFIER (Lexing.lexeme lexbuf) } diff --git a/src/util/makefileParser.mly b/src/util/makefileParser.mly deleted file mode 100644 index 6a2946a7d7..0000000000 --- a/src/util/makefileParser.mly +++ /dev/null @@ -1,24 +0,0 @@ -%token IDENTIFIER -%token COLON -%token NEWLINE -%token EOF - -%type deps - -%start deps - -%% - -deps: - | IDENTIFIER COLON identifier_list NEWLINE EOF { ($1, $3) } - ; - -identifier_list: - | { [] } - | identifier_nonempty_list { $1 } - ; - -identifier_nonempty_list: - | IDENTIFIER { [$1] } - | IDENTIFIER identifier_nonempty_list { $1 :: $2 } - ; diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 264447a282..80ce33ce62 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -35,14 +35,3 @@ 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 - ) From 4334fa390f7f7365754f713af439449040dc3cff Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 10:35:29 +0100 Subject: [PATCH 04/12] Bump goblint-cil --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/goblint.opam b/goblint.opam index b235f85adc..669c791bdf 100644 --- a/goblint.opam +++ b/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#b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1" ] # 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 diff --git a/goblint.opam.locked b/goblint.opam.locked index d3b76bbe39..e968251db2 100644 --- a/goblint.opam.locked +++ b/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#b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index bf9cbbcd8e..2517de8c7a 100644 --- a/goblint.opam.template +++ b/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#b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1" ] # 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 From 76173161456ce4efab672cdf5f526e687397b73c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 11:23:56 +0100 Subject: [PATCH 05/12] Generate dependencies from CIL --- src/framework/analyses.ml | 18 +++++++++++++++++- src/maingoblint.ml | 13 ++++++++++--- src/util/compilationDatabase.ml | 2 +- src/util/preprocessor.ml | 2 ++ 4 files changed, 30 insertions(+), 5 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index bb5882a4f0..76ba957fa9 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -268,7 +268,23 @@ 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" -> - Yojson.Safe.pretty_to_channel ~std:true out (Messages.Table.to_yojson ()) + 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_default Preprocessor.dependencies loc.file []) + | _ -> () (* TODO: add locs from everything else? would also include system headers *) + ); + files |> SH.to_list + in + let json = `Assoc [ + ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list]) files)); + ("messages", Messages.Table.to_yojson ()); + ] + in + Yojson.Safe.pretty_to_channel ~std:true out json | "none" -> () | s -> failwith @@ "Unsupported value for option `result`: "^s end diff --git a/src/maingoblint.ml b/src/maingoblint.ml index cc6f6ca5c6..802229c96b 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -170,6 +170,8 @@ let basic_preprocess ~all_cppflags fname = (** Preprocess all files. Return list of preprocessed files and the temp directory name. *) let preprocess_files () = + Hashtbl.clear Preprocessor.dependencies; (* clear for server mode *) + (* Preprocessor flags *) let cppflags = ref (get_string_list "cppflags") in @@ -251,7 +253,7 @@ let preprocess_files () = let rec preprocess_arg_file = function | filename when Filename.basename filename = "Makefile" -> let comb_file = MakefileUtil.generate_and_combine filename ~all_cppflags in - [basic_preprocess ~all_cppflags comb_file] + [(comb_file, basic_preprocess ~all_cppflags comb_file)] | filename when Filename.basename filename = CompilationDatabase.basename -> CompilationDatabase.load_and_preprocess ~all_cppflags filename @@ -270,7 +272,7 @@ let preprocess_files () = raise Exit | filename -> - [basic_preprocess ~all_cppflags filename] + [(filename, basic_preprocess ~all_cppflags filename)] in let extra_arg_files = ref [] in @@ -286,7 +288,12 @@ 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 (orig, f) = + let file = Cilfacade.getAST f in + Hashtbl.add Preprocessor.dependencies orig 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") diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index d93fb0bf4e..74f9275379 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -88,7 +88,7 @@ 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 *) - Some preprocessed_file + Some (file, preprocessed_file) in parse_file filename |> BatList.filter_map preprocess diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 80ce33ce62..5f66dae419 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -34,4 +34,6 @@ let cpp = ) ) +let dependencies: (string, string list) Hashtbl.t = Hashtbl.create 3 + let get_cpp () = Lazy.force cpp From 43accce5b62b3cd821330715aaf98198cd1584dc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 12:40:50 +0100 Subject: [PATCH 06/12] Bump goblint-cil --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/goblint.opam b/goblint.opam index 669c791bdf..e9c8bab892 100644 --- a/goblint.opam +++ b/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#b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1" ] + [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#2a759462d74aabf33d41e92076ec0e79c51a6c3f" ] # 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 diff --git a/goblint.opam.locked b/goblint.opam.locked index e968251db2..d6bea28947 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -110,7 +110,7 @@ version: "dev" pin-depends: [ [ "goblint-cil.1.8.2" - "git+https://github.com/goblint/cil.git#b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1" + "git+https://github.com/goblint/cil.git#2a759462d74aabf33d41e92076ec0e79c51a6c3f" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index 2517de8c7a..2d0ab67632 100644 --- a/goblint.opam.template +++ b/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#b3bfde07bd6a5dcbeb73f9c7a9d08f48a454e5b1" ] + [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#2a759462d74aabf33d41e92076ec0e79c51a6c3f" ] # 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 From 865e3d668c0ecdef6a5656b2df0042e5eb125543 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 16:23:39 +0100 Subject: [PATCH 07/12] Dependencies: keep null if dependencies not recorded --- src/framework/analyses.ml | 4 ++-- src/util/preprocessor.ml | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 76ba957fa9..a1bca72492 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -274,13 +274,13 @@ struct iterGlobals file (function | GFun (_, loc) | GVar (_, _, loc) -> - SH.replace files loc.file (Hashtbl.find_default Preprocessor.dependencies loc.file []) + 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 json = `Assoc [ - ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list]) files)); + ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files)); ("messages", Messages.Table.to_yojson ()); ] in diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 5f66dae419..abed3dfe7a 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -34,6 +34,7 @@ let cpp = ) ) -let dependencies: (string, string list) Hashtbl.t = Hashtbl.create 3 - let get_cpp () = Lazy.force cpp + + +let dependencies: (string, string list) Hashtbl.t = Hashtbl.create 3 From 5450bbe8a8b2f04c6113a38d7df2c74c526535dc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Feb 2022 16:27:17 +0100 Subject: [PATCH 08/12] Add comment about dependecy tracking not working properly for Makefiles --- src/maingoblint.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 802229c96b..0792c99f35 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -253,6 +253,7 @@ let preprocess_files () = let rec preprocess_arg_file = function | filename when Filename.basename filename = "Makefile" -> let comb_file = MakefileUtil.generate_and_combine filename ~all_cppflags in + (* The resulting dependency information will not be correctly tracked, because the merge happens in cilly *) [(comb_file, basic_preprocess ~all_cppflags comb_file)] | filename when Filename.basename filename = CompilationDatabase.basename -> From 3d6a946599e7db8254e0ce65ae71ec8ca63c5678 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Feb 2022 16:17:23 +0100 Subject: [PATCH 09/12] Bump goblint-cil & dump dependencies as-is --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- src/framework/analyses.ml | 14 ++------------ src/maingoblint.ml | 9 +++++---- src/util/compilationDatabase.ml | 2 +- src/util/preprocessor.ml | 2 +- 7 files changed, 12 insertions(+), 21 deletions(-) diff --git a/goblint.opam b/goblint.opam index e9c8bab892..b4e6249d1a 100644 --- a/goblint.opam +++ b/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#2a759462d74aabf33d41e92076ec0e79c51a6c3f" ] + [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#4c91e95918f03b4696f4dfb02c7a3dfef2955db9" ] # 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 diff --git a/goblint.opam.locked b/goblint.opam.locked index d6bea28947..c5caa81519 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -110,7 +110,7 @@ version: "dev" pin-depends: [ [ "goblint-cil.1.8.2" - "git+https://github.com/goblint/cil.git#2a759462d74aabf33d41e92076ec0e79c51a6c3f" + "git+https://github.com/goblint/cil.git#4c91e95918f03b4696f4dfb02c7a3dfef2955db9" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index 2d0ab67632..6707c6f6bf 100644 --- a/goblint.opam.template +++ b/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#2a759462d74aabf33d41e92076ec0e79c51a6c3f" ] + [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#4c91e95918f03b4696f4dfb02c7a3dfef2955db9" ] # 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 diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index a1bca72492..45130ebcab 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -268,19 +268,9 @@ 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 json = `Assoc [ - ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: string list option]) files)); + ("files", `Assoc (List.map (Tuple2.map2 [%to_yojson: (string*bool) list]) files)); ("messages", Messages.Table.to_yojson ()); ] in diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 0792c99f35..b00cb4ee51 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -254,7 +254,7 @@ let preprocess_files () = | filename when Filename.basename filename = "Makefile" -> let comb_file = MakefileUtil.generate_and_combine filename ~all_cppflags in (* The resulting dependency information will not be correctly tracked, because the merge happens in cilly *) - [(comb_file, basic_preprocess ~all_cppflags comb_file)] + [basic_preprocess ~all_cppflags comb_file] | filename when Filename.basename filename = CompilationDatabase.basename -> CompilationDatabase.load_and_preprocess ~all_cppflags filename @@ -273,7 +273,7 @@ let preprocess_files () = raise Exit | filename -> - [(filename, basic_preprocess ~all_cppflags filename)] + [basic_preprocess ~all_cppflags filename] in let extra_arg_files = ref [] in @@ -289,9 +289,10 @@ let preprocess_files () = let merge_preprocessed cpp_file_names = (* get the AST *) if get_bool "dbg.verbose" then print_endline "Parsing files."; - let get_ast_and_record_deps (orig, f) = + let get_ast_and_record_deps f = let file = Cilfacade.getAST f in - Hashtbl.add Preprocessor.dependencies orig file.files; + (* Drop and from dependencies *) + Hashtbl.add Preprocessor.dependencies f @@ List.filter (fun (n,_) -> n <> "" && n <> "") file.files; file in let files_AST = List.map (get_ast_and_record_deps) cpp_file_names in diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index 74f9275379..d93fb0bf4e 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -88,7 +88,7 @@ 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 *) - Some (file, preprocessed_file) + Some preprocessed_file in parse_file filename |> BatList.filter_map preprocess diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index abed3dfe7a..d70dbce9a5 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -37,4 +37,4 @@ let cpp = let get_cpp () = Lazy.force cpp -let dependencies: (string, string list) Hashtbl.t = Hashtbl.create 3 +let dependencies: (string, (string*bool) list) Hashtbl.t = Hashtbl.create 3 From 997d65c881b214000d0d79be33e9a2a450543b13 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Feb 2022 16:33:13 +0100 Subject: [PATCH 10/12] Bump goblint-cil --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/goblint.opam b/goblint.opam index b4e6249d1a..99fc9efdfe 100644 --- a/goblint.opam +++ b/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#4c91e95918f03b4696f4dfb02c7a3dfef2955db9" ] + [ "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 diff --git a/goblint.opam.locked b/goblint.opam.locked index c5caa81519..01762c0300 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -110,7 +110,7 @@ version: "dev" pin-depends: [ [ "goblint-cil.1.8.2" - "git+https://github.com/goblint/cil.git#4c91e95918f03b4696f4dfb02c7a3dfef2955db9" + "git+https://github.com/goblint/cil.git#908790cb6c85f5ce053a0616bcc6b327758b8966" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index 6707c6f6bf..3a224e0e5b 100644 --- a/goblint.opam.template +++ b/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#4c91e95918f03b4696f4dfb02c7a3dfef2955db9" ] + [ "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 From 2fef118c95a8e4bb42c98dcd6545b08812074b10 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 10 Feb 2022 15:01:43 +0100 Subject: [PATCH 11/12] Rm outdated comment --- src/maingoblint.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index b00cb4ee51..80958a7783 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -253,7 +253,6 @@ let preprocess_files () = let rec preprocess_arg_file = function | filename when Filename.basename filename = "Makefile" -> let comb_file = MakefileUtil.generate_and_combine filename ~all_cppflags in - (* The resulting dependency information will not be correctly tracked, because the merge happens in cilly *) [basic_preprocess ~all_cppflags comb_file] | filename when Filename.basename filename = CompilationDatabase.basename -> From 074ca0b66acb15aeacebdaf4d174a7227f8c4f70 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 10 Feb 2022 15:14:34 +0100 Subject: [PATCH 12/12] Do not print system deps --- src/framework/analyses.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 45130ebcab..562da97b5c 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -269,8 +269,9 @@ struct Yojson.Safe.pretty_to_channel ~std:true out (Sarif.to_yojson (List.rev !Messages.Table.messages_list)); | "json-messages" -> 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*bool) list]) files)); + ("files", `Assoc (List.map (Tuple2.map2 (fun deps -> [%to_yojson:string list] @@ filter_system deps)) files)); ("messages", Messages.Table.to_yojson ()); ] in