Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion goblint.opam
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,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#da5e1941db81643ef0d2133960cd28a7de311131" ]
[ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#faff341f1e8f070121d828aa6301370b4a8918d6" ]
# 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
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.locked
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ version: "dev"
pin-depends: [
[
"goblint-cil.1.8.2"
"git+https://github.com/goblint/cil.git#da5e1941db81643ef0d2133960cd28a7de311131"
"git+https://github.com/goblint/cil.git#faff341f1e8f070121d828aa6301370b4a8918d6"
]
[
"apron.v0.9.13"
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.template
Original file line number Diff line number Diff line change
@@ -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#da5e1941db81643ef0d2133960cd28a7de311131" ]
[ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#faff341f1e8f070121d828aa6301370b4a8918d6" ]
# 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
Expand Down
12 changes: 1 addition & 11 deletions src/domains/access.ml
Original file line number Diff line number Diff line change
Expand Up @@ -74,19 +74,9 @@ let d_acct () = function
| `Type t -> dprintf "(%a)" d_type t
| `Struct (s,o) -> dprintf "(struct %s)%a" s.cname d_offs o

let file_re = Str.regexp "\\(.*/\\|\\)\\([^/]*\\)"
let d_loc () loc =
let loc =
if Str.string_match file_re loc.file 0 then
{loc with file = Str.matched_group 2 loc.file}
else
loc
in
CilType.Location.pretty () loc

let d_memo () (t, lv) =
match lv with
| Some (v,o) -> dprintf "%a%a@@%a" Basetype.Variables.pretty v d_offs o d_loc v.vdecl
| Some (v,o) -> dprintf "%a%a@@%a" Basetype.Variables.pretty v d_offs o CilType.Location.pretty v.vdecl
| None -> dprintf "%a" d_acct t

let rec get_type (fb: typ) : exp -> acc_typ = function
Expand Down
4 changes: 1 addition & 3 deletions src/framework/analyses.ml
Original file line number Diff line number Diff line change
Expand Up @@ -268,10 +268,8 @@ struct
printf "Writing Sarif to file: %s\n%!" (get_string "outfile");
Yojson.Safe.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.map Fpath.to_string (fun deps -> [%to_yojson: GobFpath.t list] @@ filter_system deps)) files));
("files", Preprocessor.dependencies_to_yojson ());
("messages", Messages.Table.to_yojson ());
]
in
Expand Down
34 changes: 25 additions & 9 deletions src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ 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.FpathH.clear Preprocessor.dependencies; (* clear for server mode *)

(* Preprocessor flags *)
let cppflags = ref (get_string_list "pre.cppflags") in
Expand Down Expand Up @@ -317,19 +317,35 @@ let preprocess_files () =
in
ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated preprocess_tasks
);
List.map fst preprocessed
preprocessed

(** Possibly merge all postprocessed files *)
let merge_preprocessed cpp_file_names =
let merge_preprocessed preprocessed =
(* get the AST *)
if get_bool "dbg.verbose" then print_endline "Parsing files.";
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.map (Tuple2.map1 Fpath.v) @@ List.filter (fun (n,_) -> n <> "<built-in>" && n <> "<command-line>") file.files;
file

let goblint_cwd = GobFpath.cwd () in
let get_ast_and_record_deps (preprocessed_file, task_opt) =
let transform_file (path_str, system_header) = match path_str with
| "<built-in>" | "<command-line>" ->
(path_str, system_header) (* ignore special "paths" *)
| _ ->
let path = Fpath.v path_str in
let dir = (Option.get task_opt).ProcessPool.cwd |? goblint_cwd in (* relative to compilation database directory or goblint's cwd *)
let path' = Fpath.normalize @@ Fpath.append dir path in
let path' = Fpath.rem_prefix goblint_cwd path' |? path' in (* remove goblint cwd prefix (if has one) for readability *)
Preprocessor.FpathH.modify_def Fpath.Map.empty preprocessed_file (Fpath.Map.add path' system_header) Preprocessor.dependencies; (* record dependency *)
(Fpath.to_string path', system_header)
in
let transformLocation ~file ~line =
let file' = Option.map transform_file file in
Some (file', line)
in
Errormsg.transformLocation := transformLocation;

Cilfacade.getAST preprocessed_file
in
let files_AST = List.map (get_ast_and_record_deps) cpp_file_names in
let files_AST = List.map (get_ast_and_record_deps) preprocessed in

let cilout =
if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")
Expand Down
4 changes: 4 additions & 0 deletions src/util/gobFpath.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
type t = Fpath.t [@@deriving show]

let equal = Fpath.equal
let compare = Fpath.compare
let hash p = Hashtbl.hash (Fpath.to_string p)

let pretty () p = Pretty.text (Fpath.to_string p)

let to_yojson p = `String (Fpath.to_string p)
Expand Down
20 changes: 19 additions & 1 deletion src/util/preprocessor.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,5 +36,23 @@ let cpp =

let get_cpp () = Lazy.force cpp

module FpathH = Hashtbl.Make (GobFpath)
let dependencies: bool Fpath.Map.t FpathH.t = FpathH.create 3 (* bool is system_header *)

let dependencies: (Fpath.t, (Fpath.t * bool) list) Hashtbl.t = Hashtbl.create 3
let dependencies_to_yojson () =
dependencies
|> FpathH.enum
|> Enum.map (fun (p, deps) ->
let deps' =
deps
|> Fpath.Map.bindings
|> List.filter_map (function
| (dep, false) -> Some dep
| (_, true) -> None
)
|> [%to_yojson: GobFpath.t list]
in
(Fpath.to_string p, deps')
)
|> List.of_enum
|> (fun l -> `Assoc l)