Skip to content
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.

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

Fix various server mode crashes #990

Merged
merged 10 commits into from
Feb 16, 2023
4 changes: 2 additions & 2 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
let get_spec (): (module Spec) =
Lazy.force spec_module

let current_node_state_json : (Node.t -> Yojson.Safe.t) ref = ref (fun _ -> assert false)
let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _ -> None)

(** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *)
module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) =
Expand Down Expand Up @@ -636,7 +636,7 @@ struct
let module R: ResultQuery.SpecSysSol2 with module SpecSys = SpecSys = ResultQuery.Make (FileCfg) (SpecSysSol) in

let local_xml = solver2source_result lh in
current_node_state_json := (fun node -> LT.to_yojson (Result.find local_xml node));
current_node_state_json := (fun node -> Option.map LT.to_yojson (Result.find_option local_xml node));

let liveness =
if get_bool "ana.dead-code.lines" || get_bool "ana.dead-code.branches" then
Expand Down
3 changes: 2 additions & 1 deletion src/framework/node.ml
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ let find_fundec (node: t) =
| Function fd -> fd
| FunctionEntry fd -> fd

(** @raise Not_found *)
let of_id s =
let ix = Str.search_forward (Str.regexp {|[0-9]+$|}) s 0 in
let id = int_of_string (Str.string_after s ix) in
Expand All @@ -68,5 +69,5 @@ let of_id s =
match prefix with
| "ret" -> Function fundec
| "fun" -> FunctionEntry fundec
| _ -> invalid_arg "Node.of_id: invalid prefix"
| _ -> raise Not_found

42 changes: 30 additions & 12 deletions src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -190,6 +190,9 @@ let parse_arguments () =
raise Exit
)


exception FrontendError of string

let basic_preprocess_counts = Preprocessor.FpathH.create 3

(** Use gcc to preprocess a file. Returns the path to the preprocessed file. *)
Expand Down Expand Up @@ -254,13 +257,17 @@ let preprocess_files () =
print_endline "Warning, cannot find goblint's custom include files.";

let find_custom_include subpath =
List.find_map (fun custom_include_dir ->
let custom_include_opt = List.find_map_opt (fun custom_include_dir ->
let path = Fpath.append custom_include_dir subpath in
if Sys.file_exists (Fpath.to_string path) then
Some path
else
None
) custom_include_dirs
in
match custom_include_opt with
| Some custom_include -> custom_include
| None -> raise (FrontendError (Format.asprintf "custom include %a not found" Fpath.pp subpath))
in

(* include flags*)
Expand Down Expand Up @@ -290,8 +297,7 @@ let preprocess_files () =
try
List.find (Sys.file_exists % Fpath.to_string) kernel_roots
with Not_found ->
prerr_endline "Root directory for kernel include files not found!";
raise Exit
raise (FrontendError "root directory for kernel include files not found")
in

let kernel_dir = Fpath.(kernel_root / "include") in
Expand Down Expand Up @@ -322,6 +328,9 @@ let preprocess_files () =
if get_bool "dbg.verbose" then print_endline "Preprocessing files.";

let rec preprocess_arg_file = function
| filename when not (Sys.file_exists (Fpath.to_string filename)) ->
raise (FrontendError (Format.asprintf "file argument %a not found" Fpath.pp filename))

| filename when Fpath.filename filename = "Makefile" ->
let comb_file = MakefileUtil.generate_and_combine filename ~all_cppflags in
[basic_preprocess ~all_cppflags comb_file]
Expand All @@ -339,8 +348,7 @@ let preprocess_files () =
[] (* don't recurse for anything else *)

| filename when Fpath.get_ext filename = ".json" ->
Format.eprintf "Unexpected JSON file argument (possibly missing --conf): %a\n" Fpath.pp filename;
raise Exit
raise (FrontendError (Format.asprintf "unexpected JSON file argument %a (possibly missing --conf)" Fpath.pp filename))

| filename ->
[basic_preprocess ~all_cppflags filename]
Expand All @@ -356,9 +364,10 @@ let preprocess_files () =
let preprocessed = List.concat_map preprocess_arg_file (!extra_files @ List.map Fpath.v (get_string_list "files")) in
if not (get_bool "pre.exist") then (
let preprocess_tasks = List.filter_map snd preprocessed in
let terminated task = function
let terminated (task: ProcessPool.task) = function
| Unix.WEXITED 0 -> ()
| process_status -> failwith (GobUnix.string_of_process_status process_status)
| process_status ->
raise (FrontendError (Format.sprintf "preprocessor %s: %s" (GobUnix.string_of_process_status process_status) task.command))
in
Timing.wrap "preprocess" (ProcessPool.run ~jobs:(Goblintutil.jobs ()) ~terminated) preprocess_tasks
);
Expand Down Expand Up @@ -388,7 +397,13 @@ let parse_preprocessed preprocessed =
in
Errormsg.transformLocation := transformLocation;

Cilfacade.getAST preprocessed_file
try
Cilfacade.getAST preprocessed_file
with
| Frontc.ParseError s ->
raise (FrontendError (Format.sprintf "Frontc.ParseError: %s" s))
| Errormsg.Error ->
raise (FrontendError "Errormsg.Error")
in
List.map get_ast_and_record_deps preprocessed

Expand All @@ -405,9 +420,12 @@ let merge_parsed parsed =
match parsed with
| [one] -> Cilfacade.callConstructors one
| [] ->
prerr_endline "No files to analyze!";
raise Exit
| xs -> Cilfacade.getMergedAST xs |> Cilfacade.callConstructors
raise (FrontendError "no files to analyze")
| xs ->
try
Cilfacade.getMergedAST xs |> Cilfacade.callConstructors
with Errormsg.Error ->
raise (FrontendError "Errormsg.Error")
in

Cilfacade.rmTemps merged_AST;
Expand Down Expand Up @@ -455,7 +473,7 @@ let do_analyze change_info merged_AST =
(* we first find the functions to analyze: *)
if get_bool "dbg.verbose" then print_endline "And now... the Goblin!";
let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in
if stf@exf@otf = [] then failwith "No suitable function to start from.";
if stf@exf@otf = [] then raise (FrontendError "no suitable function to start from");
if get_bool "dbg.verbose" then ignore (Pretty.printf "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a\n"
L.pretty stf L.pretty exf L.pretty otf);
(* and here we run the analysis! *)
Expand Down
12 changes: 11 additions & 1 deletion src/util/cilfacade.ml
Original file line number Diff line number Diff line change
Expand Up @@ -35,10 +35,16 @@ let init () =

let current_file = ref dummyFile

(** @raise GoblintCil.FrontC.ParseError
@raise GoblintCil.Errormsg.Error *)
let parse fileName =
let fileName_str = Fpath.to_string fileName in
Errormsg.hadErrors := false; (* reset because CIL doesn't *)
let cabs2cil = Timing.wrap ~args:[("file", `String fileName_str)] "FrontC" Frontc.parse fileName_str in
Timing.wrap ~args:[("file", `String fileName_str)] "Cabs2cil" cabs2cil ()
let file = Timing.wrap ~args:[("file", `String fileName_str)] "Cabs2cil" cabs2cil () in
if !E.hadErrors then
E.s (E.error "There were parsing errors in %s" fileName_str);
file

let print (fileAST: file) =
dumpFile defaultCilPrinter stdout "stdout" fileAST
Expand All @@ -60,6 +66,8 @@ let do_preprocess ast =
iterGlobals ast (function GFun (fd,_) -> List.iter (f fd) !visitors | _ -> ())


(** @raise GoblintCil.FrontC.ParseError
@raise GoblintCil.Errormsg.Error *)
let getAST fileName =
let fileAST = parse fileName in
(* rmTemps fileAST; *)
Expand Down Expand Up @@ -90,7 +98,9 @@ class addConstructors cons = object
method! vtype _ = SkipChildren
end

(** @raise GoblintCil.Errormsg.Error *)
let getMergedAST fileASTs =
Errormsg.hadErrors := false; (* reset because CIL doesn't *)
let merged = Timing.wrap "mergeCIL" (Mergecil.merge fileASTs) "stdout" in
if !E.hadErrors then
E.s (E.error "There were errors during merging\n");
Expand Down
38 changes: 25 additions & 13 deletions src/util/server.ml
Original file line number Diff line number Diff line change
Expand Up @@ -216,8 +216,11 @@ let () =
try
analyze serve ~reset;
{status = if !Goblintutil.verified = Some false then VerifyError else Success}
with Sys.Break ->
with
| Sys.Break ->
{status = Aborted}
| Maingoblint.FrontendError message ->
Response.Error.(raise (make ~code:RequestFailed ~message ()))
end);

register (module struct
Expand Down Expand Up @@ -289,20 +292,26 @@ let () =
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 ()
try
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 ()
with Maingoblint.FrontendError message ->
Response.Error.(raise (make ~code:RequestFailed ~message ()))
end);

register (module struct
let name = "functions"
type params = unit [@@deriving of_yojson]
type response = Function.t list [@@deriving to_yojson]
let process () serv = Function.getFunctionsList (Option.get serv.file).globals
let process () serv =
match serv.file with
| Some file -> Function.getFunctionsList file.globals
| None -> Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed" ()))
end);

register (module struct
Expand All @@ -321,10 +330,13 @@ let () =
type params = { nid: string } [@@deriving of_yojson]
type response = Yojson.Safe.t [@@deriving to_yojson]
let process { nid } serv =
let f = !Control.current_node_state_json in
let n = Node.of_id nid in
let json = f n in
json
match Node.of_id nid with
| n ->
begin match !Control.current_node_state_json n with
| Some json -> json
| None -> Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed, non-existent or dead node" ()))
end
| exception Not_found -> Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
end);

register (module struct
Expand Down