Skip to content

Add server command pre_files #740

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 9, 2022
Merged

Add server command pre_files #740

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3d9bf4b
Add server command pre_files (closes #739)
sim642 May 19, 2022
f60b16c
Optimize server pre_files by not merging files
sim642 May 19, 2022
8fc9b36
Merge branch 'interactive' into issue-739
sim642 Aug 9, 2022
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 src/goblint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ let main () =
print_endline (localtime ());
print_endline Goblintutil.command_line;
);
let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_and_merge) in
let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
if get_bool "server.enabled" then (
let file =
if get_bool "server.reparse" then
Expand Down
15 changes: 10 additions & 5 deletions src/maingoblint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -313,8 +313,8 @@ let preprocess_files () =
);
preprocessed

(** Possibly merge all postprocessed files *)
let merge_preprocessed preprocessed =
(** Parse preprocessed files *)
let parse_preprocessed preprocessed =
(* get the AST *)
if get_bool "dbg.verbose" then print_endline "Parsing files.";

Expand All @@ -339,8 +339,10 @@ let merge_preprocessed preprocessed =

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

(** Merge parsed files *)
let merge_parsed parsed =
let cilout =
if get_string "dbg.cilout" = "" then Legacy.stderr else Legacy.open_out (get_string "dbg.cilout")
in
Expand All @@ -349,7 +351,7 @@ let merge_preprocessed preprocessed =

(* we use CIL to merge all inputs to ONE file *)
let merged_AST =
match files_AST with
match parsed with
| [one] -> Cilfacade.callConstructors one
| [] ->
prerr_endline "No files to analyze!";
Expand All @@ -364,7 +366,10 @@ let merge_preprocessed preprocessed =
Cilfacade.current_file := merged_AST;
merged_AST

let preprocess_and_merge () = preprocess_files () |> merge_preprocessed
let preprocess_parse_merge () =
preprocess_files ()
|> parse_preprocessed
|> merge_parsed

let do_stats () =
if get_bool "printstats" then (
Expand Down
16 changes: 15 additions & 1 deletion src/util/server.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ let start file =
let reparse (s: t) =
if GobConfig.get_bool "server.reparse" then (
GoblintDir.init ();
let file = Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_and_merge in
let file = Fun.protect ~finally:GoblintDir.finalize Maingoblint.preprocess_parse_merge in
begin match s.file with
| None ->
let max_ids = MaxIdUtil.get_file_max_ids file in
Expand Down Expand Up @@ -257,6 +257,20 @@ let () =
let process () _ = Preprocessor.dependencies_to_yojson ()
end);

register (module struct
let name = "pre_files"
type params = unit [@@deriving of_yojson]
type response = Yojson.Safe.t [@@deriving to_yojson]
let process () s =
if GobConfig.get_bool "server.reparse" then (
GoblintDir.init ();
Fun.protect ~finally:GoblintDir.finalize (fun () ->
ignore Maingoblint.(preprocess_files () |> parse_preprocessed)
)
);
Preprocessor.dependencies_to_yojson ()
end);

register (module struct
let name = "functions"
type params = unit [@@deriving of_yojson]
Expand Down