Fix server node_state request crash without analysis or on dead node …

…(issue #983)
goblint · Feb 15, 2023 · 59127e9 · 59127e9
1 parent 48fe7b4
commit 59127e9
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -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) =
@@ -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

diff --git a/src/util/server.ml b/src/util/server.ml
@@ -324,10 +324,10 @@ 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 !Control.current_node_state_json n with
+      | Some json -> json
+      | None -> Response.Error.(raise (make ~code:InvalidRequest ~message:"not analyzed, non-existent or dead node" ()))
   end);
 
   register (module struct