Add cfg/lookup request to server mode

src/framework/node.ml

@@ -63,7 +63,7 @@ let of_id s =
   let id = int_of_string (Str.string_after s ix) in
   let prefix = Str.string_before s ix in
   match ix with
-  | 0 -> Statement { dummyStmt with sid = id }
+  | 0 -> Statement (Option.get (Cilfacade.find_stmt_sid id))
   | _ ->
     let fundec = Cilfacade.find_varinfo_fundec {dummyFunDec.svar with vid = id} in
     match prefix with

src/util/cilfacade.ml

@@ -496,14 +496,35 @@ let original_names: string VarinfoH.t ResettableLazy.t =
     If it was inserted by CIL (or Goblint), then returns [None]. *)
 let find_original_name vi = VarinfoH.find_opt (ResettableLazy.force original_names) vi (* vi argument must be explicit, otherwise force happens immediately *)
 
+module IntH = Hashtbl.Make (struct type t = int [@@deriving eq, hash] end)
+
+class stmtSidVisitor h = object
+  inherit nopCilVisitor
+  method! vstmt s =
+    IntH.replace h s.sid s;
+    DoChildren
+end
+
+let stmt_sids: stmt IntH.t ResettableLazy.t =
+ResettableLazy.from_fun (fun () ->
+    let h = IntH.create 113 in
+    let visitor = new stmtSidVisitor h in
+    visitCilFileSameGlobals visitor !current_file;
+    h
+  )
+
+(** Find [stmt] by its [sid]. *)
+let find_stmt_sid sid = IntH.find_opt (ResettableLazy.force stmt_sids) sid
+
 
 let reset_lazy () =
   StmtH.clear pseudo_return_to_fun;
   ResettableLazy.reset stmt_fundecs;
   ResettableLazy.reset varinfo_fundecs;
   ResettableLazy.reset name_fundecs;
   ResettableLazy.reset varinfo_roles;
-  ResettableLazy.reset original_names
+  ResettableLazy.reset original_names;
+  ResettableLazy.reset stmt_sids
 
 
 let stmt_pretty_short () x =

src/util/server.ml

@@ -176,6 +176,38 @@ let increment_data (s: t) file reparsed = match Serialize.Cache.get_opt_data Sol
     Some { server = true; Analyses.changes; solver_data; restarting = [] }, false
   | _ -> None, true
 
+
+module Locator = WitnessUtil.Locator (Node)
+let node_locator: Locator.t ResettableLazy.t =
+  ResettableLazy.from_fun (fun () ->
+      let module Cfg = (val !MyCFG.current_cfg) in
+      let locator = Locator.create () in
+
+      (* DFS, copied from CfgTools.find_backwards_reachable *)
+      let module NH = MyCFG.NodeH in
+      let reachable = NH.create 100 in
+      let rec iter_node node =
+        if not (NH.mem reachable node) then begin
+          NH.replace reachable node ();
+          let loc = Node.location node in
+          if not loc.synthetic then
+            Locator.add locator loc node;
+          List.iter (fun (_, prev_node) ->
+              iter_node prev_node
+            ) (Cfg.prev node)
+        end
+      in
+
+      Cil.iterGlobals !Cilfacade.current_file (function
+          | GFun (fd, _) ->
+            let return_node = Node.Function fd in
+            iter_node return_node
+          | _ -> ()
+        );
+
+      locator
+    )
+
 let analyze ?(reset=false) (s: t) =
   Messages.Table.(MH.clear messages_table);
   Messages.Table.messages_list := [];
@@ -186,6 +218,7 @@ let analyze ?(reset=false) (s: t) =
     Serialize.Cache.reset_data SolverData;
     Serialize.Cache.reset_data AnalysisData);
   let increment_data, fresh = increment_data s file reparsed in
+  ResettableLazy.reset node_locator;
   Cilfacade.reset_lazy ();
   InvariantCil.reset_lazy ();
   WideningThresholds.reset_lazy ();
@@ -325,6 +358,54 @@ let () =
       { cfg }
   end);
 
+  register (module struct
+    let name = "cfg/lookup"
+    type params = {
+      node: string option [@default None];
+      location: CilType.Location.t option [@default None];
+    } [@@deriving of_yojson]
+    type response = {
+      node: string;
+      location: CilType.Location.t;
+      next: (Edge.t list * string) list;
+      prev: (Edge.t list * string) list;
+    } [@@deriving to_yojson]
+    let process (params: params) serv =
+      let node = match params.node, params.location with
+        | Some node_id, None ->
+          begin try
+              Node.of_id node_id
+            with Not_found ->
+              Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
+          end
+        | None, Some location ->
+          let node_opt =
+            let open GobOption.Syntax in
+            let* nodes = Locator.find_opt (ResettableLazy.force node_locator) location in
+            Locator.ES.choose_opt nodes
+          in
+          Option.get_exn node_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ()))
+        | _, _ ->
+          Response.Error.(raise (make ~code:RequestFailed ~message:"requires node xor location" ()))
+      in
+      let node_id = Node.show_id node in
+      let location = Node.location node in
+      let module Cfg = (val !MyCFG.current_cfg) in
+      let next =
+        Cfg.next node
+        |> List.map (fun (edges, to_node) ->
+            (List.map snd edges, Node.show_id to_node)
+          )
+      in
+      let prev =
+        Cfg.prev node
+        |> List.map (fun (edges, to_node) ->
+            (List.map snd edges, Node.show_id to_node)
+          )
+      in
+      {node = node_id; location; next; prev}
+  end);
+
   register (module struct
     let name = "node_state"
     type params = { nid: string }  [@@deriving of_yojson]