From 3e2caa78ee030f29bac1fb3aec73cb5e828d2ab1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Feb 2023 16:47:30 +0200
Subject: [PATCH 01/25] Extract ARG creation from witness

---
 src/witness/argTools.ml | 120 ++++++++++++++++++++++++++++++++++++++++
 src/witness/witness.ml  |  97 ++------------------------------
 2 files changed, 124 insertions(+), 93 deletions(-)
 create mode 100644 src/witness/argTools.ml

diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
new file mode 100644
index 0000000000..a240337be3
--- /dev/null
+++ b/src/witness/argTools.ml
@@ -0,0 +1,120 @@
+open MyCFG
+open Graphml
+open Svcomp
+open GobConfig
+
+module type WitnessTaskResult = TaskResult with module Arg.Edge = MyARG.InlineEdge
+
+module type BiArg =
+sig
+  include MyARG.S with module Edge = MyARG.InlineEdge
+
+  val prev: Node.t -> (Edge.t * Node.t) list
+end
+
+module Make (R: ResultQuery.SpecSysSol2) =
+struct
+  open R
+  open SpecSys
+  open Svcomp
+
+  module Query = ResultQuery.Query (SpecSys)
+
+  let get: node * Spec.C.t -> Spec.D.t =
+    fun nc -> LHT.find_default lh nc (Spec.D.bot ())
+
+  let ask_indices lvar =
+    let indices = ref [] in
+    ignore (ask_local lvar (Queries.IterVars (fun i ->
+        indices := i :: !indices
+      )));
+    !indices
+
+  module CfgNode = Node
+
+  module Node =
+  struct
+    type t = MyCFG.node * Spec.C.t * int
+
+    let equal (n1, c1, i1) (n2, c2, i2) =
+      EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2
+
+    let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i
+
+    let cfgnode (n, c, i) = n
+
+    let to_string (n, c, i) =
+      (* copied from NodeCtxStackGraphMlWriter *)
+      let c_tag = Spec.C.tag c in
+      let i_str = string_of_int i in
+      match n with
+      | Statement stmt  -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str
+      | Function f      -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
+      | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
+
+    (* TODO: less hacky way (without ask_indices) to move node *)
+    let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c)))
+    let move_opt (n, c, i) to_n =
+      match ask_indices (to_n, c) with
+      | [] -> None
+      | [to_i] ->
+        let to_node = (to_n, c, to_i) in
+        BatOption.filter is_live (Some to_node)
+      | _ :: _ :: _ ->
+        failwith "Node.move_opt: ambiguous moved index"
+    let equal_node_context (n1, c1, i1) (n2, c2, i2) =
+      EQSys.LVar.equal (n1, c1) (n2, c2)
+  end
+
+  module NHT = BatHashtbl.Make (Node)
+
+  let create entrystates: (MyARG.inline_edge * Node.t) list NHT.t * (module BiArg with type Node.t = MyCFG.node * Spec.C.t * int) =
+    let (witness_prev_map, witness_prev, witness_next) =
+      let prev = NHT.create 100 in
+      let next = NHT.create 100 in
+      LHT.iter (fun lvar local ->
+          ignore (ask_local lvar ~local (Queries.IterPrevVars (fun i (prev_node, prev_c_obj, j) edge ->
+              let lvar' = (fst lvar, snd lvar, i) in
+              let prev_lvar: NHT.key = (prev_node, Obj.obj prev_c_obj, j) in
+              NHT.modify_def [] lvar' (fun prevs -> (edge, prev_lvar) :: prevs) prev;
+              NHT.modify_def [] prev_lvar (fun nexts -> (edge, lvar') :: nexts) next
+            )))
+        ) lh;
+
+      (prev,
+        (fun n ->
+          NHT.find_default prev n []), (* main entry is not in prev at all *)
+        (fun n ->
+          NHT.find_default next n [])) (* main return is not in next at all *)
+    in
+    let witness_main =
+      let lvar = WitnessUtil.find_main_entry entrystates in
+      let main_indices = ask_indices lvar in
+      (* TODO: get rid of this hack for getting index of entry state *)
+      assert (List.compare_length_with main_indices 1 = 0);
+      let main_index = List.hd main_indices in
+      (fst lvar, snd lvar, main_index)
+    in
+
+    let module Arg =
+    struct
+      module Node = Node
+      module Edge = MyARG.InlineEdge
+      let main_entry = witness_main
+      let next = witness_next
+    end
+    in
+    let module Arg =
+    struct
+      open MyARG
+      module ArgIntra = UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))
+      include Intra (ArgIntra) (Arg)
+
+      let prev = witness_prev
+    end
+    in
+    (witness_prev_map, (module Arg: BiArg with type Node.t = MyCFG.node * Spec.C.t * int))
+
+  let create entrystates =
+    Timing.wrap "arg create" create entrystates
+end
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 937f83473f..29ab5b7003 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -271,100 +271,12 @@ struct
   open Svcomp
 
   module Query = ResultQuery.Query (SpecSys)
+  module ArgTool = ArgTools.Make (R)
+  module NHT = ArgTool.NHT
 
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
-    let get: node * Spec.C.t -> Spec.D.t =
-      fun nc -> LHT.find_default lh nc (Spec.D.bot ())
-    in
-    let ask_indices lvar =
-      let indices = ref [] in
-      ignore (ask_local lvar (Queries.IterVars (fun i ->
-          indices := i :: !indices
-        )));
-      !indices
-    in
-
-    let module CfgNode = Node in
-
-    let module Node =
-    struct
-      type t = MyCFG.node * Spec.C.t * int
-
-      let equal (n1, c1, i1) (n2, c2, i2) =
-        EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2
-
-      let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i
-
-      let cfgnode (n, c, i) = n
-
-      let to_string (n, c, i) =
-        (* copied from NodeCtxStackGraphMlWriter *)
-        let c_tag = Spec.C.tag c in
-        let i_str = string_of_int i in
-        match n with
-        | Statement stmt  -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str
-        | Function f      -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
-        | FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
-
-      (* TODO: less hacky way (without ask_indices) to move node *)
-      let is_live (n, c, i) = not (Spec.D.is_bot (get (n, c)))
-      let move_opt (n, c, i) to_n =
-        match ask_indices (to_n, c) with
-        | [] -> None
-        | [to_i] ->
-          let to_node = (to_n, c, to_i) in
-          BatOption.filter is_live (Some to_node)
-        | _ :: _ :: _ ->
-          failwith "Node.move_opt: ambiguous moved index"
-      let equal_node_context (n1, c1, i1) (n2, c2, i2) =
-        EQSys.LVar.equal (n1, c1) (n2, c2)
-    end
-    in
-
-    let module NHT = BatHashtbl.Make (Node) in
-
-    let (witness_prev_map, witness_prev, witness_next) =
-      let prev = NHT.create 100 in
-      let next = NHT.create 100 in
-      LHT.iter (fun lvar local ->
-          ignore (ask_local lvar ~local (Queries.IterPrevVars (fun i (prev_node, prev_c_obj, j) edge ->
-              let lvar' = (fst lvar, snd lvar, i) in
-              let prev_lvar: NHT.key = (prev_node, Obj.obj prev_c_obj, j) in
-              NHT.modify_def [] lvar' (fun prevs -> (edge, prev_lvar) :: prevs) prev;
-              NHT.modify_def [] prev_lvar (fun nexts -> (edge, lvar') :: nexts) next
-            )))
-        ) lh;
-
-      (prev,
-        (fun n ->
-          NHT.find_default prev n []), (* main entry is not in prev at all *)
-        (fun n ->
-          NHT.find_default next n [])) (* main return is not in next at all *)
-    in
-    let witness_main =
-      let lvar = WitnessUtil.find_main_entry entrystates in
-      let main_indices = ask_indices lvar in
-      (* TODO: get rid of this hack for getting index of entry state *)
-      assert (List.compare_length_with main_indices 1 = 0);
-      let main_index = List.hd main_indices in
-      (fst lvar, snd lvar, main_index)
-    in
-
-    let module Arg =
-    struct
-      module Node = Node
-      module Edge = MyARG.InlineEdge
-      let main_entry = witness_main
-      let next = witness_next
-    end
-    in
-    let module Arg =
-    struct
-      open MyARG
-      module ArgIntra = UnCilTernaryIntra (UnCilLogicIntra (CfgIntra (FileCfg.Cfg)))
-      include Intra (ArgIntra) (Arg)
-    end
-    in
+    let (witness_prev_map, arg_module) = ArgTool.create entrystates in
+    let module Arg = (val arg_module) in
 
     let find_invariant (n, c, i) =
       let context = {Invariant.default_context with path = Some i} in
@@ -418,7 +330,6 @@ struct
         struct
           include Arg
 
-          let prev = witness_prev
           let violations = violations
         end
         in

From 6ccf76e7586fd0c3b86d3d9dbcd7145f7c55eb7a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 22 Feb 2023 16:58:26 +0200
Subject: [PATCH 02/25] Add option exp.arg for constructing ARG outside witness

---
 src/framework/control.ml     | 9 +++++----
 src/util/options.schema.json | 6 ++++++
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 7f5b3040e6..39d87919e1 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -12,6 +12,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
+  let arg_enabled = get_bool "ana.sv-comp.enabled" || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in
@@ -19,10 +20,10 @@ let spec_module: (module Spec) Lazy.t = lazy (
             (module MCP.MCP2 : Spec)
             |> lift true (module WidenContextLifterSide) (* option checked in functor *)
             (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
-            |> lift (get_bool "ana.opt.hashcons" || get_bool "ana.sv-comp.enabled") (module HashconsContextLifter)
-            |> lift (get_bool "ana.sv-comp.enabled") (module HashconsLifter)
-            |> lift (get_bool "ana.sv-comp.enabled") (module WitnessConstraints.PathSensitive3)
-            |> lift (not (get_bool "ana.sv-comp.enabled")) (module PathSensitive2)
+            |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
+            |> lift arg_enabled (module HashconsLifter)
+            |> lift arg_enabled (module WitnessConstraints.PathSensitive3)
+            |> lift (not arg_enabled) (module PathSensitive2)
             |> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
             |> lift true (module DeadCodeLifter)
             |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index c3346677d6..64d579e2c5 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1634,6 +1634,12 @@
           "description": "Hide standard extern globals (e.g. `stdout`) from cluttering local states.",
           "type": "boolean",
           "default": true
+        },
+        "arg": {
+          "title": "exp.arg",
+          "description": "Construct abstract reachability graph (ARG).",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false

From 4152d0527a8c190b683b2bd1605493c1c9cc15e0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 12:55:34 +0200
Subject: [PATCH 03/25] Add iter_nodes to BiArg

---
 src/witness/argTools.ml |  9 +++++++--
 src/witness/witness.ml  | 14 +++++++-------
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index a240337be3..83830eb817 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -10,6 +10,7 @@ sig
   include MyARG.S with module Edge = MyARG.InlineEdge
 
   val prev: Node.t -> (Edge.t * Node.t) list
+  val iter_nodes: (Node.t -> unit) -> unit
 end
 
 module Make (R: ResultQuery.SpecSysSol2) =
@@ -68,7 +69,7 @@ struct
 
   module NHT = BatHashtbl.Make (Node)
 
-  let create entrystates: (MyARG.inline_edge * Node.t) list NHT.t * (module BiArg with type Node.t = MyCFG.node * Spec.C.t * int) =
+  let create entrystates: (module BiArg with type Node.t = MyCFG.node * Spec.C.t * int) =
     let (witness_prev_map, witness_prev, witness_next) =
       let prev = NHT.create 100 in
       let next = NHT.create 100 in
@@ -111,9 +112,13 @@ struct
       include Intra (ArgIntra) (Arg)
 
       let prev = witness_prev
+      let iter_nodes f =
+        NHT.iter (fun n _ ->
+            f n
+          ) witness_prev_map
     end
     in
-    (witness_prev_map, (module Arg: BiArg with type Node.t = MyCFG.node * Spec.C.t * int))
+    (module Arg: BiArg with type Node.t = MyCFG.node * Spec.C.t * int)
 
   let create entrystates =
     Timing.wrap "arg create" create entrystates
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 29ab5b7003..faff689e4f 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -275,8 +275,7 @@ struct
   module NHT = ArgTool.NHT
 
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
-    let (witness_prev_map, arg_module) = ArgTool.create entrystates in
-    let module Arg = (val arg_module) in
+    let module Arg = (val ArgTool.create entrystates) in
 
     let find_invariant (n, c, i) =
       let context = {Invariant.default_context with path = Some i} in
@@ -319,12 +318,13 @@ struct
           |> List.exists (fun (_, to_n) -> is_violation to_n)
         in
         let violations =
-          NHT.fold (fun lvar _ acc ->
+          (* TODO: fold_nodes?s *)
+          let acc = ref [] in
+          Arg.iter_nodes (fun lvar ->
               if is_violation lvar then
-                lvar :: acc
-              else
-                acc
-            ) witness_prev_map []
+                acc := lvar :: !acc
+            );
+          !acc
         in
         let module ViolationArg =
         struct

From dd0e3fde692b1951512fdceb481dfcaa786dad13 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 13:57:26 +0200
Subject: [PATCH 04/25] Add arg/lookup request to server

---
 src/framework/control.ml | 10 ++++++
 src/util/server.ml       | 77 ++++++++++++++++++++++++++++++++++++++++
 src/witness/argTools.ml  |  3 ++
 3 files changed, 90 insertions(+)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 39d87919e1..98a45f2bf0 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -659,6 +659,16 @@ struct
     in
     Timing.wrap "warn_global" (GHT.iter warn_global) gh;
 
+    if get_bool "exp.arg" then (
+      let module ArgTool = ArgTools.Make (R) in
+      let module Arg = (val ArgTool.create entrystates) in
+      ArgTools.current_arg := Some (module Arg);
+      ignore (Pretty.printf "ARG main: %s\n" (Arg.Node.to_string Arg.main_entry));
+      Arg.iter_nodes (fun n ->
+          ignore (Pretty.printf "%s\n" (Arg.Node.to_string n))
+        )
+    );
+
     (* Before SV-COMP, so result can depend on YAML witness validation. *)
     if get_string "witness.yaml.validate" <> "" then (
       let module YWitness = YamlWitness.Validator (R) in
diff --git a/src/util/server.ml b/src/util/server.ml
index 486ee9fa39..d3ddf08997 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -208,6 +208,26 @@ let node_locator: Locator.t ResettableLazy.t =
       locator
     )
 
+module ArgNode =
+struct
+  type t = Node.t * Analyses.ControlSpecC.t * int [@@deriving ord]
+end
+module ArgLocator = WitnessUtil.Locator (ArgNode)
+let arg_node_locator: ArgLocator.t ResettableLazy.t =
+  ResettableLazy.from_fun (fun () ->
+      let module Arg = (val (Option.get !ArgTools.current_arg)) in
+      let locator = ArgLocator.create () in
+
+      Arg.iter_nodes (fun n ->
+          let cfgnode = Arg.Node.cfgnode n in
+          let loc = Node.location cfgnode in
+          if not loc.synthetic then
+            ArgLocator.add locator loc (Obj.magic n) (* TODO: bad magic *)
+        );
+
+      locator
+    )
+
 let analyze ?(reset=false) (s: t) =
   Messages.Table.(MH.clear messages_table);
   Messages.Table.messages_list := [];
@@ -406,6 +426,63 @@ let () =
       {node = node_id; location; next; prev}
   end);
 
+  register (module struct
+    let name = "arg/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: (MyARG.inline_edge * string) list;
+      prev: (MyARG.inline_edge * string) list;
+    } [@@deriving to_yojson]
+    let process (params: params) serv =
+      let module Arg = (val (Option.get !ArgTools.current_arg)) in
+      let n: Arg.Node.t = match params.node, params.location with
+        | Some node_id, None ->
+          let found = ref None in
+          begin try
+            (* TODO: better find *)
+            Arg.iter_nodes (fun n ->
+                if Arg.Node.to_string n = node_id then (
+                  found := Some n;
+                  raise Exit
+                )
+              )
+            with Exit -> ()
+          end;
+          Option.get_exn !found Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
+        | None, Some location ->
+          let node_opt =
+            let open GobOption.Syntax in
+            let* nodes = ArgLocator.find_opt (ResettableLazy.force arg_node_locator) location in
+            ArgLocator.ES.choose_opt nodes
+          in
+          Option.get_exn node_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ()))
+          |> Obj.magic (* TODO: bad magic *)
+        | _, _ ->
+          Response.Error.(raise (make ~code:RequestFailed ~message:"requires node xor location" ()))
+      in
+      let node = Arg.Node.cfgnode n in
+      let node_id = Node.show_id node in
+      let location = Node.location node in
+      let next =
+        Arg.next n
+        |> List.map (fun (edge, to_node) ->
+            (edge, Arg.Node.to_string to_node)
+          )
+      in
+      let prev =
+        Arg.prev n
+        |> List.map (fun (edge, to_node) ->
+            (edge, Arg.Node.to_string to_node)
+          )
+      in
+      {node = node_id; location; next; prev}
+  end);
+
   register (module struct
     let name = "node_state"
     type params = { nid: string }  [@@deriving of_yojson]
diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index 83830eb817..aee73f06ab 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -13,6 +13,8 @@ sig
   val iter_nodes: (Node.t -> unit) -> unit
 end
 
+let current_arg: (module BiArg) option ref = ref None
+
 module Make (R: ResultQuery.SpecSysSol2) =
 struct
   open R
@@ -113,6 +115,7 @@ struct
 
       let prev = witness_prev
       let iter_nodes f =
+        f main_entry;
         NHT.iter (fun n _ ->
             f n
           ) witness_prev_map

From fe00bc95ba5ecfee2ece13785e9034e24795600c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:19:42 +0200
Subject: [PATCH 05/25] Make ARG in server type safe

---
 src/util/server.ml      | 61 +++++++++++++++++++++++++----------------
 src/witness/argTools.ml |  7 +++++
 src/witness/myARG.ml    |  3 +-
 3 files changed, 46 insertions(+), 25 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index d3ddf08997..dcff98f57a 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -2,9 +2,17 @@ open Batteries
 open Jsonrpc
 open GoblintCil
 
+module type ArgWrapper =
+sig
+  module Arg: ArgTools.BiArg
+  module Locator: module type of WitnessUtil.Locator (Arg.Node)
+  val locator: Locator.t
+end
+
 type t = {
   mutable file: Cil.file option;
   mutable max_ids: MaxIdUtil.max_ids;
+  arg_wrapper: (module ArgWrapper) ResettableLazy.t;
   input: IO.input;
   output: unit IO.output;
 }
@@ -106,6 +114,29 @@ let serve serv =
   |> Seq.map Packet.t_of_yojson
   |> Seq.iter (handle_packet serv)
 
+let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
+  ResettableLazy.from_fun (fun () ->
+      let module Arg = (val (Option.get !ArgTools.current_arg)) in
+      let module Locator = WitnessUtil.Locator (Arg.Node) in
+
+      let locator = Locator.create () in
+      Arg.iter_nodes (fun n ->
+          let cfgnode = Arg.Node.cfgnode n in
+          let loc = Node.location cfgnode in
+          if not loc.synthetic then
+            Locator.add locator loc n
+        );
+
+      let module ArgWrapper =
+      struct
+        module Arg = Arg
+        module Locator = Locator
+        let locator = locator
+      end
+      in
+      (module ArgWrapper: ArgWrapper)
+    )
+
 let make ?(input=stdin) ?(output=stdout) file : t =
   let max_ids =
     match file with
@@ -115,6 +146,7 @@ let make ?(input=stdin) ?(output=stdout) file : t =
   {
     file;
     max_ids;
+    arg_wrapper;
     input;
     output
   }
@@ -208,26 +240,6 @@ let node_locator: Locator.t ResettableLazy.t =
       locator
     )
 
-module ArgNode =
-struct
-  type t = Node.t * Analyses.ControlSpecC.t * int [@@deriving ord]
-end
-module ArgLocator = WitnessUtil.Locator (ArgNode)
-let arg_node_locator: ArgLocator.t ResettableLazy.t =
-  ResettableLazy.from_fun (fun () ->
-      let module Arg = (val (Option.get !ArgTools.current_arg)) in
-      let locator = ArgLocator.create () in
-
-      Arg.iter_nodes (fun n ->
-          let cfgnode = Arg.Node.cfgnode n in
-          let loc = Node.location cfgnode in
-          if not loc.synthetic then
-            ArgLocator.add locator loc (Obj.magic n) (* TODO: bad magic *)
-        );
-
-      locator
-    )
-
 let analyze ?(reset=false) (s: t) =
   Messages.Table.(MH.clear messages_table);
   Messages.Table.messages_list := [];
@@ -239,6 +251,7 @@ let analyze ?(reset=false) (s: t) =
     Serialize.Cache.reset_data AnalysisData);
   let increment_data, fresh = increment_data s file reparsed in
   ResettableLazy.reset node_locator;
+  ResettableLazy.reset s.arg_wrapper;
   Cilfacade.reset_lazy ();
   InvariantCil.reset_lazy ();
   WideningThresholds.reset_lazy ();
@@ -439,7 +452,8 @@ let () =
       prev: (MyARG.inline_edge * string) list;
     } [@@deriving to_yojson]
     let process (params: params) serv =
-      let module Arg = (val (Option.get !ArgTools.current_arg)) in
+      let module ArgWrapper = (val (ResettableLazy.force serv.arg_wrapper)) in
+      let open ArgWrapper in
       let n: Arg.Node.t = match params.node, params.location with
         | Some node_id, None ->
           let found = ref None in
@@ -457,11 +471,10 @@ let () =
         | None, Some location ->
           let node_opt =
             let open GobOption.Syntax in
-            let* nodes = ArgLocator.find_opt (ResettableLazy.force arg_node_locator) location in
-            ArgLocator.ES.choose_opt nodes
+            let* nodes = Locator.find_opt 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" ()))
-          |> Obj.magic (* TODO: bad magic *)
         | _, _ ->
           Response.Error.(raise (make ~code:RequestFailed ~message:"requires node xor location" ()))
       in
diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index aee73f06ab..91e556dc52 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -42,6 +42,13 @@ struct
     let equal (n1, c1, i1) (n2, c2, i2) =
       EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2
 
+    let compare (n1, c1, i1) (n2, c2, i2) =
+      let r = EQSys.LVar.compare (n1, c1) (n2, c2) in
+      if r <> 0 then
+        r
+      else
+        Int.compare i1 i2
+
     let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i
 
     let cfgnode (n, c, i) = n
diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index a4ffeef5bd..80c827ad31 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -4,6 +4,7 @@ open GoblintCil
 module type Node =
 sig
   include Hashtbl.HashedType
+  include Set.OrderedType with type t := t
 
   val cfgnode: t -> MyCFG.node
   val to_string: t -> string
@@ -78,7 +79,7 @@ end
 module StackNode (Node: Node):
   Node with type t = Node.t list =
 struct
-  type t = Node.t list [@@deriving eq, hash]
+  type t = Node.t list [@@deriving eq, ord, hash]
 
   let cfgnode nl = Node.cfgnode (List.hd nl)
   let to_string nl =

From cbcaaeb7fd6d57853b90695866bcdad349ff9085 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:22:46 +0200
Subject: [PATCH 06/25] Make arg/lookup return entry if no params

---
 src/util/server.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index dcff98f57a..3b8cb2d0b2 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -455,6 +455,8 @@ let () =
       let module ArgWrapper = (val (ResettableLazy.force serv.arg_wrapper)) in
       let open ArgWrapper in
       let n: Arg.Node.t = match params.node, params.location with
+        | None, None ->
+          Arg.main_entry
         | Some node_id, None ->
           let found = ref None in
           begin try
@@ -475,8 +477,8 @@ let () =
             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" ()))
+        | Some _, Some _ ->
+          Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
       in
       let node = Arg.Node.cfgnode n in
       let node_id = Node.show_id node in

From f9c50a3b9a21d9d200d47b9b3800fc1773a33daf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:26:02 +0200
Subject: [PATCH 07/25] Add ARG node ID to arg/lookup response

---
 src/util/server.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 3b8cb2d0b2..c4e39ac617 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -447,6 +447,7 @@ let () =
     } [@@deriving of_yojson]
     type response = {
       node: string;
+      cfg_node: string;
       location: CilType.Location.t;
       next: (MyARG.inline_edge * string) list;
       prev: (MyARG.inline_edge * string) list;
@@ -480,9 +481,9 @@ let () =
         | Some _, Some _ ->
           Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
       in
-      let node = Arg.Node.cfgnode n in
-      let node_id = Node.show_id node in
-      let location = Node.location node in
+      let cfg_node = Arg.Node.cfgnode n in
+      let cfg_node_id = Node.show_id cfg_node in
+      let location = Node.location cfg_node in
       let next =
         Arg.next n
         |> List.map (fun (edge, to_node) ->
@@ -495,7 +496,7 @@ let () =
             (edge, Arg.Node.to_string to_node)
           )
       in
-      {node = node_id; location; next; prev}
+      {node = Arg.Node.to_string n; cfg_node = cfg_node_id; location; next; prev}
   end);
 
   register (module struct

From 0822be55ad6db8c49512be2aabc8a94c13164942 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:31:56 +0200
Subject: [PATCH 08/25] Make arg/lookup return all results

---
 src/util/server.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index c4e39ac617..954dee4fa3 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -445,19 +445,21 @@ let () =
       node: string option [@default None];
       location: CilType.Location.t option [@default None];
     } [@@deriving of_yojson]
-    type response = {
+    type one_response = {
       node: string;
       cfg_node: string;
       location: CilType.Location.t;
       next: (MyARG.inline_edge * string) list;
       prev: (MyARG.inline_edge * string) list;
     } [@@deriving to_yojson]
+    type response = one_response list [@@deriving to_yojson]
     let process (params: params) serv =
       let module ArgWrapper = (val (ResettableLazy.force serv.arg_wrapper)) in
       let open ArgWrapper in
-      let n: Arg.Node.t = match params.node, params.location with
+      let open GobList.Syntax in
+      let+ n: Arg.Node.t = match params.node, params.location with
         | None, None ->
-          Arg.main_entry
+          [Arg.main_entry]
         | Some node_id, None ->
           let found = ref None in
           begin try
@@ -470,14 +472,14 @@ let () =
               )
             with Exit -> ()
           end;
-          Option.get_exn !found Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
+          [Option.get_exn !found Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))]
         | None, Some location ->
-          let node_opt =
+          let nodes_opt =
             let open GobOption.Syntax in
-            let* nodes = Locator.find_opt locator location in
-            Locator.ES.choose_opt nodes
+            let+ nodes = Locator.find_opt locator location in
+            Locator.ES.elements nodes
           in
-          Option.get_exn node_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ()))
+          Option.get_exn nodes_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ()))
         | Some _, Some _ ->
           Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
       in

From 6606c88a0b31a66d7139cea4f3c7048eec8be763 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:36:00 +0200
Subject: [PATCH 09/25] Optimize arg/lookup by node ID

---
 src/util/server.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 954dee4fa3..bae06819ef 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -7,6 +7,7 @@ sig
   module Arg: ArgTools.BiArg
   module Locator: module type of WitnessUtil.Locator (Arg.Node)
   val locator: Locator.t
+  val find_node: string -> Arg.Node.t
 end
 
 type t = {
@@ -118,13 +119,16 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
       let module Arg = (val (Option.get !ArgTools.current_arg)) in
       let module Locator = WitnessUtil.Locator (Arg.Node) in
+      let module StringH = Hashtbl.Make (Printable.Strings) in
 
       let locator = Locator.create () in
+      let ids = StringH.create 113 in
       Arg.iter_nodes (fun n ->
           let cfgnode = Arg.Node.cfgnode n in
           let loc = Node.location cfgnode in
           if not loc.synthetic then
-            Locator.add locator loc n
+            Locator.add locator loc n;
+          StringH.replace ids (Arg.Node.to_string n) n;
         );
 
       let module ArgWrapper =
@@ -132,6 +136,7 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
         module Arg = Arg
         module Locator = Locator
         let locator = locator
+        let find_node = StringH.find ids
       end
       in
       (module ArgWrapper: ArgWrapper)
@@ -461,18 +466,11 @@ let () =
         | None, None ->
           [Arg.main_entry]
         | Some node_id, None ->
-          let found = ref None in
           begin try
-            (* TODO: better find *)
-            Arg.iter_nodes (fun n ->
-                if Arg.Node.to_string n = node_id then (
-                  found := Some n;
-                  raise Exit
-                )
-              )
-            with Exit -> ()
-          end;
-          [Option.get_exn !found Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))]
+              [ArgWrapper.find_node node_id]
+            with Not_found ->
+              Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
+          end
         | None, Some location ->
           let nodes_opt =
             let open GobOption.Syntax in

From f1ef2b08aadc55934bdfc133775d8b720f00e37b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:44:44 +0200
Subject: [PATCH 10/25] Remove exp.arg debug printing

---
 src/framework/control.ml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index 98a45f2bf0..aae02f724c 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -663,10 +663,6 @@ struct
       let module ArgTool = ArgTools.Make (R) in
       let module Arg = (val ArgTool.create entrystates) in
       ArgTools.current_arg := Some (module Arg);
-      ignore (Pretty.printf "ARG main: %s\n" (Arg.Node.to_string Arg.main_entry));
-      Arg.iter_nodes (fun n ->
-          ignore (Pretty.printf "%s\n" (Arg.Node.to_string n))
-        )
     );
 
     (* Before SV-COMP, so result can depend on YAML witness validation. *)

From 253b962641587c779f6dfb61ba04cdde7d0aa3bb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 14:47:32 +0200
Subject: [PATCH 11/25] Clean up ArgTools

---
 src/witness/argTools.ml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index 91e556dc52..f66f2bd403 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -1,9 +1,4 @@
 open MyCFG
-open Graphml
-open Svcomp
-open GobConfig
-
-module type WitnessTaskResult = TaskResult with module Arg.Edge = MyARG.InlineEdge
 
 module type BiArg =
 sig
@@ -19,7 +14,6 @@ module Make (R: ResultQuery.SpecSysSol2) =
 struct
   open R
   open SpecSys
-  open Svcomp
 
   module Query = ResultQuery.Query (SpecSys)
 

From e6ace71c44f090211784a1f0ef505bf566aa0dc7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 23 Feb 2023 15:10:40 +0200
Subject: [PATCH 12/25] Fix arg/lookup crash when exp.arg disabled

---
 src/util/server.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index bae06819ef..5d977f3ae1 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -117,7 +117,7 @@ let serve serv =
 
 let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
   ResettableLazy.from_fun (fun () ->
-      let module Arg = (val (Option.get !ArgTools.current_arg)) in
+      let module Arg = (val (Option.get_exn !ArgTools.current_arg Response.Error.(E (make ~code:RequestFailed ~message:"not analyzed or arg disabled" ())))) in
       let module Locator = WitnessUtil.Locator (Arg.Node) in
       let module StringH = Hashtbl.Make (Printable.Strings) in
 
@@ -469,7 +469,7 @@ let () =
           begin try
               [ArgWrapper.find_node node_id]
             with Not_found ->
-              Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
+              Response.Error.(raise (make ~code:RequestFailed ~message:"non-existent node" ()))
           end
         | None, Some location ->
           let nodes_opt =

From 4019627c3ea1038a32f7122931113112758b6f7d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Feb 2023 12:10:47 +0200
Subject: [PATCH 13/25] Add context and path fields to arg/lookup response

---
 src/util/server.ml      | 12 +++++++++++-
 src/witness/argTools.ml |  2 ++
 src/witness/myARG.ml    |  4 ++++
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 5d977f3ae1..cde8ab3873 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -453,6 +453,8 @@ let () =
     type one_response = {
       node: string;
       cfg_node: string;
+      context: string;
+      path: string;
       location: CilType.Location.t;
       next: (MyARG.inline_edge * string) list;
       prev: (MyARG.inline_edge * string) list;
@@ -496,7 +498,15 @@ let () =
             (edge, Arg.Node.to_string to_node)
           )
       in
-      {node = Arg.Node.to_string n; cfg_node = cfg_node_id; location; next; prev}
+      {
+        node = Arg.Node.to_string n;
+        cfg_node = cfg_node_id;
+        context = string_of_int (Arg.Node.context_id n);
+        path = string_of_int (Arg.Node.path_id n);
+        location;
+        next;
+        prev
+      }
   end);
 
   register (module struct
diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index f66f2bd403..91e097d714 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -46,6 +46,8 @@ struct
     let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i
 
     let cfgnode (n, c, i) = n
+    let context_id (n, c, i) = Spec.C.tag c
+    let path_id (n, c, i) = i
 
     let to_string (n, c, i) =
       (* copied from NodeCtxStackGraphMlWriter *)
diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index 80c827ad31..c035cccf06 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -7,6 +7,8 @@ sig
   include Set.OrderedType with type t := t
 
   val cfgnode: t -> MyCFG.node
+  val context_id: t -> int
+  val path_id: t -> int
   val to_string: t -> string
 
   val move_opt: t -> MyCFG.node -> t option
@@ -82,6 +84,8 @@ struct
   type t = Node.t list [@@deriving eq, ord, hash]
 
   let cfgnode nl = Node.cfgnode (List.hd nl)
+  let context_id nl = Node.context_id (List.hd nl)
+  let path_id nl = Node.path_id (List.hd nl)
   let to_string nl =
     nl
     |> List.map Node.to_string

From 3fc991a24a12328a5622cfc35227c1b82198b168 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Feb 2023 16:54:01 +0200
Subject: [PATCH 14/25] Add arg/lookup TODOs

---
 src/util/server.ml                | 8 +++++---
 src/witness/witnessConstraints.ml | 1 +
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index cde8ab3873..0456e41b3b 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -131,6 +131,8 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
           StringH.replace ids (Arg.Node.to_string n) n;
         );
 
+      (* TODO: lookup  by CFG node *)
+
       let module ArgWrapper =
       struct
         module Arg = Arg
@@ -456,7 +458,7 @@ let () =
       context: string;
       path: string;
       location: CilType.Location.t;
-      next: (MyARG.inline_edge * string) list;
+      next: (MyARG.inline_edge * string) list; (* TODO: tuple to record *)
       prev: (MyARG.inline_edge * string) list;
     } [@@deriving to_yojson]
     type response = one_response list [@@deriving to_yojson]
@@ -471,7 +473,7 @@ let () =
           begin try
               [ArgWrapper.find_node node_id]
             with Not_found ->
-              Response.Error.(raise (make ~code:RequestFailed ~message:"non-existent node" ()))
+              Response.Error.(raise (make ~code:RequestFailed ~message:"non-existent node" ())) (* TODO: empty list *)
           end
         | None, Some location ->
           let nodes_opt =
@@ -479,7 +481,7 @@ let () =
             let+ nodes = Locator.find_opt locator location in
             Locator.ES.elements nodes
           in
-          Option.get_exn nodes_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ()))
+          Option.get_exn nodes_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ())) (* TODO: empty list *)
         | Some _, Some _ ->
           Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
       in
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 60469adc9a..0cfeaf9010 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -238,6 +238,7 @@ struct
           let yr =
             if should_inline f then
               step_ctx ctx x' (InlineEntry a)
+              (* TODO: keep inlined Proc edge as well *)
             else
               R.bot ()
           in

From 534184f2e2a37af07b6942ef5c79787a239869dc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 10:06:28 +0200
Subject: [PATCH 15/25] Make arg/lookup request return empty lists instead of
 errors

---
 src/util/server.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 0456e41b3b..01b449072f 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -473,7 +473,7 @@ let () =
           begin try
               [ArgWrapper.find_node node_id]
             with Not_found ->
-              Response.Error.(raise (make ~code:RequestFailed ~message:"non-existent node" ())) (* TODO: empty list *)
+              [] (* non-existent node *)
           end
         | None, Some location ->
           let nodes_opt =
@@ -481,7 +481,7 @@ let () =
             let+ nodes = Locator.find_opt locator location in
             Locator.ES.elements nodes
           in
-          Option.get_exn nodes_opt Response.Error.(E (make ~code:RequestFailed ~message:"cannot find node for location" ())) (* TODO: empty list *)
+          Option.default [] nodes_opt (* cannot find node for location *)
         | Some _, Some _ ->
           Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
       in

From 90464b50bff29b0399e49faccf19a900ebefb365 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 10:11:05 +0200
Subject: [PATCH 16/25] Extract edge_node record for arg/lookup request

---
 src/util/server.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 01b449072f..533a702c28 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -452,16 +452,22 @@ let () =
       node: string option [@default None];
       location: CilType.Location.t option [@default None];
     } [@@deriving of_yojson]
+
+    type edge_node = {
+      edge: MyARG.inline_edge;
+      node: string;
+    } [@@deriving to_yojson]
     type one_response = {
       node: string;
       cfg_node: string;
       context: string;
       path: string;
       location: CilType.Location.t;
-      next: (MyARG.inline_edge * string) list; (* TODO: tuple to record *)
-      prev: (MyARG.inline_edge * string) list;
+      next: edge_node list;
+      prev: edge_node list;
     } [@@deriving to_yojson]
     type response = one_response list [@@deriving to_yojson]
+
     let process (params: params) serv =
       let module ArgWrapper = (val (ResettableLazy.force serv.arg_wrapper)) in
       let open ArgWrapper in
@@ -491,13 +497,13 @@ let () =
       let next =
         Arg.next n
         |> List.map (fun (edge, to_node) ->
-            (edge, Arg.Node.to_string to_node)
+            {edge; node = Arg.Node.to_string to_node}
           )
       in
       let prev =
         Arg.prev n
         |> List.map (fun (edge, to_node) ->
-            (edge, Arg.Node.to_string to_node)
+            {edge; node = Arg.Node.to_string to_node}
           )
       in
       {

From 5daf9c053adb94101c70e37a19c848462f15e989 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 10:17:47 +0200
Subject: [PATCH 17/25] Add arg/lookup by CFG node

---
 src/util/server.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 533a702c28..fb2ad9fb0a 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -8,6 +8,7 @@ sig
   module Locator: module type of WitnessUtil.Locator (Arg.Node)
   val locator: Locator.t
   val find_node: string -> Arg.Node.t
+  val find_cfg_node: string -> Arg.Node.t list
 end
 
 type t = {
@@ -123,22 +124,23 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
 
       let locator = Locator.create () in
       let ids = StringH.create 113 in
+      let cfg_nodes = StringH.create 113 in
       Arg.iter_nodes (fun n ->
           let cfgnode = Arg.Node.cfgnode n in
           let loc = Node.location cfgnode in
           if not loc.synthetic then
             Locator.add locator loc n;
           StringH.replace ids (Arg.Node.to_string n) n;
+          StringH.add cfg_nodes (Node.show_id cfgnode) n (* add for find_all *)
         );
 
-      (* TODO: lookup  by CFG node *)
-
       let module ArgWrapper =
       struct
         module Arg = Arg
         module Locator = Locator
         let locator = locator
         let find_node = StringH.find ids
+        let find_cfg_node = StringH.find_all cfg_nodes
       end
       in
       (module ArgWrapper: ArgWrapper)
@@ -451,6 +453,7 @@ let () =
     type params = {
       node: string option [@default None];
       location: CilType.Location.t option [@default None];
+      cfg_node: string option [@default None];
     } [@@deriving of_yojson]
 
     type edge_node = {
@@ -472,24 +475,26 @@ let () =
       let module ArgWrapper = (val (ResettableLazy.force serv.arg_wrapper)) in
       let open ArgWrapper in
       let open GobList.Syntax in
-      let+ n: Arg.Node.t = match params.node, params.location with
-        | None, None ->
+      let+ n: Arg.Node.t = match params.node, params.location, params.cfg_node with
+        | None, None, None ->
           [Arg.main_entry]
-        | Some node_id, None ->
+        | Some node_id, None, None ->
           begin try
               [ArgWrapper.find_node node_id]
             with Not_found ->
               [] (* non-existent node *)
           end
-        | None, Some location ->
+        | None, Some location, None ->
           let nodes_opt =
             let open GobOption.Syntax in
             let+ nodes = Locator.find_opt locator location in
             Locator.ES.elements nodes
           in
           Option.default [] nodes_opt (* cannot find node for location *)
-        | Some _, Some _ ->
-          Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
+        | None, None, Some cfg_node ->
+          ArgWrapper.find_cfg_node cfg_node
+        | _, _, _ ->
+          Response.Error.(raise (make ~code:RequestFailed ~message:"requires at most one of node, location and cfg_node" ()))
       in
       let cfg_node = Arg.Node.cfgnode n in
       let cfg_node_id = Node.show_id cfg_node in

From d9fc534a685ba13d2a42f7529c55a9d59d8075c3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 10:56:19 +0200
Subject: [PATCH 18/25] Add option exp.argdot

---
 .gitignore                   |  1 +
 src/framework/control.ml     | 11 +++++++++++
 src/util/options.schema.json |  6 ++++++
 src/witness/argTools.ml      | 25 +++++++++++++++++++++++++
 4 files changed, 43 insertions(+)

diff --git a/.gitignore b/.gitignore
index 480839d17e..512c8f865e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -44,6 +44,7 @@ _opam/
 cfgs/
 cfg.dot
 cilcfg.*.dot
+arg.dot
 
 *.graphml
 goblint.bc.js
diff --git a/src/framework/control.ml b/src/framework/control.ml
index aae02f724c..665e29e479 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -662,6 +662,17 @@ struct
     if get_bool "exp.arg" then (
       let module ArgTool = ArgTools.Make (R) in
       let module Arg = (val ArgTool.create entrystates) in
+      if get_bool "exp.argdot" then (
+        let module ArgDot = ArgTools.Dot (Arg) in
+        let oc = Stdlib.open_out "arg.dot" in
+        Fun.protect (fun () ->
+            let ppf = Format.formatter_of_out_channel oc in
+            ArgDot.dot ppf;
+            Format.pp_print_flush ppf ()
+          ) ~finally:(fun () ->
+            Stdlib.close_out oc
+          )
+      );
       ArgTools.current_arg := Some (module Arg);
     );
 
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 64d579e2c5..a2a96aec45 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1640,6 +1640,12 @@
           "description": "Construct abstract reachability graph (ARG).",
           "type": "boolean",
           "default": false
+        },
+        "argdot": {
+          "title": "exp.argdot",
+          "description": "Output ARG as dot file.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false
diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index 91e097d714..6c6c9d4e4f 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -8,6 +8,31 @@ sig
   val iter_nodes: (Node.t -> unit) -> unit
 end
 
+module Dot (Arg: BiArg) =
+struct
+  let dot_node_name ppf node =
+    Format.fprintf ppf "\"%s\"" (Arg.Node.to_string node)
+
+  let dot_edge ppf from_node (edge, to_node) =
+    Format.fprintf ppf "@,%a -> %a [label=\"%s\"];" dot_node_name from_node dot_node_name to_node (String.escaped (Arg.Edge.to_string edge))
+
+  let dot_node ppf node =
+    let shape = match Arg.Node.cfgnode node with
+      | Statement {skind=If (_,_,_,_,_); _}  -> "diamond"
+      | Statement _     -> "oval"
+      | Function _
+      | FunctionEntry _ -> "box"
+    in
+    Format.fprintf ppf "@,%a [shape=%s];" dot_node_name node shape;
+    List.iter (dot_edge ppf node) (Arg.next node)
+
+  let dot_nodes ppf =
+    Arg.iter_nodes (dot_node ppf)
+
+  let dot ppf =
+    Format.fprintf ppf "@[<v 2>digraph arg {%t@]@,}@\n" dot_nodes
+end
+
 let current_arg: (module BiArg) option ref = ref None
 
 module Make (R: ResultQuery.SpecSysSol2) =

From 265d63b78dc09763d7dcb6bddeaf24f9bfd061cd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 11:09:03 +0200
Subject: [PATCH 19/25] Add InlinedEdge to ARG edges

---
 src/witness/myARG.ml     |  2 ++
 src/witness/violation.ml |  9 +++++++--
 src/witness/witness.ml   | 15 ++++++++++++---
 3 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index c035cccf06..ee4cf5cd07 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -35,6 +35,7 @@ type inline_edge =
   | CFGEdge of Edge.t
   | InlineEntry of CilType.Exp.t list
   | InlineReturn of CilType.Lval.t option
+  | InlinedEdge of Edge.t
 [@@deriving eq, ord, hash, to_yojson]
 
 let pretty_inline_edge () = function
@@ -42,6 +43,7 @@ let pretty_inline_edge () = function
   | InlineEntry args -> Pretty.dprintf "InlineEntry '(%a)'" (Pretty.d_list ", " Cil.d_exp) args
   | InlineReturn None -> Pretty.dprintf "InlineReturn"
   | InlineReturn (Some ret) -> Pretty.dprintf "InlineReturn '%a'" Cil.d_lval ret
+  | InlinedEdge e -> Pretty.dprintf "Inlined %a" Edge.pretty_plain e
 
 module InlineEdgePrintable: Printable.S with type t = inline_edge =
 struct
diff --git a/src/witness/violation.ml b/src/witness/violation.ml
index 51952bb3c9..a3aec7d25f 100644
--- a/src/witness/violation.ml
+++ b/src/witness/violation.ml
@@ -94,8 +94,13 @@ let find_path (type node) (module Arg:ViolationArg with type Node.t = node) (mod
         else if not (NHT.mem itered_nodes node) then begin
           NHT.replace itered_nodes node ();
           List.iter (fun (edge, prev_node) ->
-              if not (NHT.mem itered_nodes prev_node) then
-                NHT.replace next_nodes prev_node (edge, node)
+              match edge with
+              | MyARG.CFGEdge _
+              | InlineEntry _
+              | InlineReturn _ ->
+                if not (NHT.mem itered_nodes prev_node) then
+                  NHT.replace next_nodes prev_node (edge, node)
+              | InlinedEdge _ -> ()
             ) (Arg.prev node);
           bfs curs' (List.map snd (Arg.prev node) @ nexts)
         end
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index faff689e4f..400016d516 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -231,11 +231,20 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
           (* TODO: keep control (Test) edges to dead (sink) nodes for violation witness? *)
         in
         List.iter (fun (edge, to_node) ->
-            write_node to_node;
-            write_edge node edge to_node
+            match edge with
+            | MyARG.CFGEdge _
+            | InlineEntry _
+            | InlineReturn _ ->
+              write_node to_node;
+              write_edge node edge to_node
+            | InlinedEdge _ -> ()
           ) edge_to_nodes;
         List.iter (fun (edge, to_node) ->
-            iter_node to_node
+            match edge with
+            | MyARG.CFGEdge _
+            | InlineEntry _
+            | InlineReturn _ -> iter_node to_node
+            | InlinedEdge _ -> ()
           ) edge_to_nodes
       end
     end

From 548bb069ed06cabf84190301ba162320d6328d05 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 11:18:27 +0200
Subject: [PATCH 20/25] Collect InlinedEdge in witness lifter

---
 src/witness/witnessConstraints.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 0cfeaf9010..015de7a936 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -137,6 +137,7 @@ struct
     with Ctx_failure _ ->
       R.bot ()
   let step_ctx_edge ctx x = step_ctx ctx x (CFGEdge ctx.edge)
+  let step_ctx_inlined_edge ctx x = step_ctx ctx x (InlinedEdge ctx.edge)
 
   let map ctx f g =
     (* we now use Sync for every tf such that threadspawn after tf could look up state before tf *)
@@ -258,7 +259,9 @@ struct
         if should_inline f then
           let nosync = (Sync.singleton x (SyncSet.singleton x)) in
           (* returns already post-sync in FromSpec *)
-          step (Function f) (Option.get fc) x (InlineReturn l) nosync (* fc should be Some outside of MCP *)
+          let returnr = step (Function f) (Option.get fc) x (InlineReturn l) nosync in (* fc should be Some outside of MCP *)
+          let procr = step_ctx_inlined_edge ctx cd in
+          R.join procr returnr
         else
           step_ctx_edge ctx cd
       in

From c3cc469b4cf80639dfe3c455cb7131edc1ca5d58 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 11:53:23 +0200
Subject: [PATCH 21/25] Improve edge to_yojson

---
 src/framework/edge.ml | 55 ++++++++++++++++++++++++++++++++++++++++++-
 src/witness/myARG.ml  | 24 ++++++++++++++++++-
 2 files changed, 77 insertions(+), 2 deletions(-)

diff --git a/src/framework/edge.ml b/src/framework/edge.ml
index 6202f6bd31..045bfb8dbf 100644
--- a/src/framework/edge.ml
+++ b/src/framework/edge.ml
@@ -29,7 +29,7 @@ type t =
     * appeared *)
   | Skip
   (** This is here for historical reasons. I never use Skip edges! *)
-[@@deriving eq, ord, hash, to_yojson]
+[@@deriving eq, ord, hash]
 
 
 let pretty () = function
@@ -55,3 +55,56 @@ let pretty_plain () = function
   | ASM _ -> text "ASM ..."
   | Skip -> text "Skip"
   | VDecl v -> dprintf "VDecl '%a %s;'" d_type v.vtype v.vname
+
+let to_yojson e =
+  let fields = match e with
+    | Assign (lval, exp) ->
+      [
+        ("type", `String "assign");
+        ("lval", CilType.Lval.to_yojson lval);
+        ("exp", CilType.Exp.to_yojson exp);
+      ]
+    | Test (exp, branch) ->
+      [
+        ("type", `String "branch");
+        ("exp", CilType.Exp.to_yojson exp);
+        ("branch", `Bool branch);
+      ]
+    | Proc (lval, function_, args) ->
+      [
+        ("type", `String "call");
+        ("lval", [%to_yojson: CilType.Lval.t option] lval);
+        ("function", CilType.Exp.to_yojson function_);
+        ("args", [%to_yojson: CilType.Exp.t list] args);
+      ]
+    | Entry function_ ->
+      [
+        ("type", `String "entry");
+        ("function", CilType.Fundec.to_yojson function_);
+      ]
+    | Ret (exp, function_) ->
+      [
+        ("type", `String "return");
+        ("function", CilType.Fundec.to_yojson function_);
+        ("exp", [%to_yojson: CilType.Exp.t option] exp);
+      ]
+    | ASM (instructions, output, input) ->
+      [
+        ("type", `String "asm");
+        ("instructions", [%to_yojson: string list] instructions);
+        ("output", asm_out_to_yojson output);
+        ("input", asm_in_to_yojson input);
+      ]
+    | VDecl variable ->
+      [
+        ("type", `String "declare");
+        ("variable", CilType.Varinfo.to_yojson variable);
+      ]
+    | Skip ->
+      [
+        ("type", `String "nop");
+      ]
+  in
+  `Assoc ([
+      ("string", `String (Pretty.sprint ~width:max_int (pretty () e)))
+    ] @ fields)
diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index ee4cf5cd07..bd3bf8c5f8 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -36,7 +36,7 @@ type inline_edge =
   | InlineEntry of CilType.Exp.t list
   | InlineReturn of CilType.Lval.t option
   | InlinedEdge of Edge.t
-[@@deriving eq, ord, hash, to_yojson]
+[@@deriving eq, ord, hash]
 
 let pretty_inline_edge () = function
   | CFGEdge e -> Edge.pretty_plain () e
@@ -45,6 +45,28 @@ let pretty_inline_edge () = function
   | InlineReturn (Some ret) -> Pretty.dprintf "InlineReturn '%a'" Cil.d_lval ret
   | InlinedEdge e -> Pretty.dprintf "Inlined %a" Edge.pretty_plain e
 
+let inline_edge_to_yojson = function
+  | CFGEdge e ->
+    `Assoc [
+      ("cfg", Edge.to_yojson e)
+    ]
+  | InlineEntry args ->
+    `Assoc [
+      ("entry", `Assoc [
+          ("args", [%to_yojson: CilType.Exp.t list] args);
+        ]);
+    ]
+  | InlineReturn lval ->
+    `Assoc [
+      ("return", `Assoc [
+          ("lval", [%to_yojson: CilType.Lval.t option] lval);
+        ]);
+    ]
+  | InlinedEdge e ->
+    `Assoc [
+      ("inlined", Edge.to_yojson e)
+    ]
+
 module InlineEdgePrintable: Printable.S with type t = inline_edge =
 struct
   include Printable.Std

From c97f8fbc2f874af270539e3ece267471b785468a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 11:58:33 +0200
Subject: [PATCH 22/25] Add more data to ARG edges

---
 src/witness/myARG.ml              | 18 +++++++++++-------
 src/witness/witnessConstraints.ml |  4 ++--
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml
index bd3bf8c5f8..330ae07909 100644
--- a/src/witness/myARG.ml
+++ b/src/witness/myARG.ml
@@ -33,16 +33,16 @@ end
 
 type inline_edge =
   | CFGEdge of Edge.t
-  | InlineEntry of CilType.Exp.t list
-  | InlineReturn of CilType.Lval.t option
+  | InlineEntry of CilType.Lval.t option * CilType.Fundec.t * CilType.Exp.t list
+  | InlineReturn of CilType.Lval.t option * CilType.Fundec.t * CilType.Exp.t list
   | InlinedEdge of Edge.t
 [@@deriving eq, ord, hash]
 
 let pretty_inline_edge () = function
   | CFGEdge e -> Edge.pretty_plain () e
-  | InlineEntry args -> Pretty.dprintf "InlineEntry '(%a)'" (Pretty.d_list ", " Cil.d_exp) args
-  | InlineReturn None -> Pretty.dprintf "InlineReturn"
-  | InlineReturn (Some ret) -> Pretty.dprintf "InlineReturn '%a'" Cil.d_lval ret
+  | InlineEntry (_, _, args) -> Pretty.dprintf "InlineEntry '(%a)'" (Pretty.d_list ", " Cil.d_exp) args
+  | InlineReturn (None, _, _) -> Pretty.dprintf "InlineReturn"
+  | InlineReturn (Some ret, _, _) -> Pretty.dprintf "InlineReturn '%a'" Cil.d_lval ret
   | InlinedEdge e -> Pretty.dprintf "Inlined %a" Edge.pretty_plain e
 
 let inline_edge_to_yojson = function
@@ -50,16 +50,20 @@ let inline_edge_to_yojson = function
     `Assoc [
       ("cfg", Edge.to_yojson e)
     ]
-  | InlineEntry args ->
+  | InlineEntry (lval, function_, args) ->
     `Assoc [
       ("entry", `Assoc [
+          ("lval", [%to_yojson: CilType.Lval.t option] lval);
+          ("function", CilType.Fundec.to_yojson function_);
           ("args", [%to_yojson: CilType.Exp.t list] args);
         ]);
     ]
-  | InlineReturn lval ->
+  | InlineReturn (lval, function_, args) ->
     `Assoc [
       ("return", `Assoc [
           ("lval", [%to_yojson: CilType.Lval.t option] lval);
+          ("function", CilType.Fundec.to_yojson function_);
+          ("args", [%to_yojson: CilType.Exp.t list] args);
         ]);
     ]
   | InlinedEdge e ->
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 015de7a936..8d320adf42 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -238,7 +238,7 @@ struct
           (* R.bot () isn't right here? doesn't actually matter? *)
           let yr =
             if should_inline f then
-              step_ctx ctx x' (InlineEntry a)
+              step_ctx ctx x' (InlineEntry (l, f, a))
               (* TODO: keep inlined Proc edge as well *)
             else
               R.bot ()
@@ -259,7 +259,7 @@ struct
         if should_inline f then
           let nosync = (Sync.singleton x (SyncSet.singleton x)) in
           (* returns already post-sync in FromSpec *)
-          let returnr = step (Function f) (Option.get fc) x (InlineReturn l) nosync in (* fc should be Some outside of MCP *)
+          let returnr = step (Function f) (Option.get fc) x (InlineReturn (l, f, a)) nosync in (* fc should be Some outside of MCP *)
           let procr = step_ctx_inlined_edge ctx cd in
           R.join procr returnr
         else

From cafbcc063ced149157ae28c6baf61a01c88e39af Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Feb 2023 12:01:13 +0200
Subject: [PATCH 23/25] Remove completed TODO in WitnessConstraints

---
 src/witness/witnessConstraints.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 8d320adf42..68a28a0e23 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -239,7 +239,6 @@ struct
           let yr =
             if should_inline f then
               step_ctx ctx x' (InlineEntry (l, f, a))
-              (* TODO: keep inlined Proc edge as well *)
             else
               R.bot ()
           in

From cb9c8d0d47e18ed372cf4a5ce3a7463dcf6f457a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 1 Mar 2023 11:06:18 +0200
Subject: [PATCH 24/25] Add ARG node details to arg/lookup next and prev

---
 src/util/server.ml | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index fb2ad9fb0a..181e26d9f8 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -459,6 +459,10 @@ let () =
     type edge_node = {
       edge: MyARG.inline_edge;
       node: string;
+      cfg_node: string;
+      context: string;
+      path: string;
+      location: CilType.Location.t;
     } [@@deriving to_yojson]
     type one_response = {
       node: string;
@@ -502,13 +506,29 @@ let () =
       let next =
         Arg.next n
         |> List.map (fun (edge, to_node) ->
-            {edge; node = Arg.Node.to_string to_node}
+            let cfg_to_node = Arg.Node.cfgnode to_node in
+            {
+              edge;
+              node = Arg.Node.to_string to_node;
+              cfg_node = Node.show_id cfg_to_node;
+              context = string_of_int (Arg.Node.context_id to_node);
+              path = string_of_int (Arg.Node.path_id to_node);
+              location = Node.location cfg_to_node;
+            }
           )
       in
       let prev =
         Arg.prev n
         |> List.map (fun (edge, to_node) ->
-            {edge; node = Arg.Node.to_string to_node}
+            let cfg_to_node = Arg.Node.cfgnode to_node in
+            {
+              edge;
+              node = Arg.Node.to_string to_node;
+              cfg_node = Node.show_id cfg_to_node;
+              context = string_of_int (Arg.Node.context_id to_node);
+              path = string_of_int (Arg.Node.path_id to_node);
+              location = Node.location cfg_to_node;
+            }
           )
       in
       {

From 4e3cbf9522f71d8f339a89ced4b94241df8f3fe1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 1 Mar 2023 11:12:07 +0200
Subject: [PATCH 25/25] Use UpdateCil.getLoc instead of Node.location in server
 for incrementality

---
 src/util/server.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/util/server.ml b/src/util/server.ml
index 181e26d9f8..7a9c793e33 100644
--- a/src/util/server.ml
+++ b/src/util/server.ml
@@ -127,7 +127,7 @@ let arg_wrapper: (module ArgWrapper) ResettableLazy.t =
       let cfg_nodes = StringH.create 113 in
       Arg.iter_nodes (fun n ->
           let cfgnode = Arg.Node.cfgnode n in
-          let loc = Node.location cfgnode in
+          let loc = UpdateCil.getLoc cfgnode in
           if not loc.synthetic then
             Locator.add locator loc n;
           StringH.replace ids (Arg.Node.to_string n) n;
@@ -230,7 +230,7 @@ let node_locator: Locator.t ResettableLazy.t =
       let rec iter_node node =
         if not (NH.mem reachable node) then begin
           NH.replace reachable node ();
-          let loc = Node.location node in
+          let loc = UpdateCil.getLoc node in
           if not loc.synthetic then
             Locator.add locator loc node;
           List.iter (fun (_, prev_node) ->
@@ -431,7 +431,7 @@ let () =
           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 location = UpdateCil.getLoc node in
       let module Cfg = (val !MyCFG.current_cfg) in
       let next =
         Cfg.next node
@@ -502,7 +502,7 @@ let () =
       in
       let cfg_node = Arg.Node.cfgnode n in
       let cfg_node_id = Node.show_id cfg_node in
-      let location = Node.location cfg_node in
+      let location = UpdateCil.getLoc cfg_node in
       let next =
         Arg.next n
         |> List.map (fun (edge, to_node) ->
@@ -513,7 +513,7 @@ let () =
               cfg_node = Node.show_id cfg_to_node;
               context = string_of_int (Arg.Node.context_id to_node);
               path = string_of_int (Arg.Node.path_id to_node);
-              location = Node.location cfg_to_node;
+              location = UpdateCil.getLoc cfg_to_node;
             }
           )
       in
@@ -527,7 +527,7 @@ let () =
               cfg_node = Node.show_id cfg_to_node;
               context = string_of_int (Arg.Node.context_id to_node);
               path = string_of_int (Arg.Node.path_id to_node);
-              location = Node.location cfg_to_node;
+              location = UpdateCil.getLoc cfg_to_node;
             }
           )
       in