Add arg/lookup request to server mode

src/framework/control.ml

@@ -12,17 +12,18 @@ 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
   let module S1 = (val
             (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)
@@ -658,6 +659,12 @@ 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);
+    );
+
     (* 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

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

src/util/server.ml

@@ -2,9 +2,18 @@ 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
+  val find_node: string -> Arg.Node.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 +115,33 @@ 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_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
+
+      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;
+          StringH.replace ids (Arg.Node.to_string n) n;
+        );
+
+      let module ArgWrapper =
+      struct
+        module Arg = Arg
+        module Locator = Locator
+        let locator = locator
+        let find_node = StringH.find ids
+      end
+      in
+      (module ArgWrapper: ArgWrapper)
+    )
+
 let make ?(input=stdin) ?(output=stdout) file : t =
   let max_ids =
     match file with
@@ -115,6 +151,7 @@ let make ?(input=stdin) ?(output=stdout) file : t =
   {
     file;
     max_ids;
+    arg_wrapper;
     input;
     output
   }
@@ -219,6 +256,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 ();
@@ -406,6 +444,61 @@ 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 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 open GobList.Syntax in
+      let+ n: Arg.Node.t = match params.node, params.location with
+        | None, None ->
+          [Arg.main_entry]
+        | Some node_id, None ->
+          begin try
+              [ArgWrapper.find_node node_id]
+            with Not_found ->
+              Response.Error.(raise (make ~code:RequestFailed ~message:"non-existent node" ()))
+          end
+        | None, Some location ->
+          let nodes_opt =
+            let open GobOption.Syntax in
+            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" ()))
+        | Some _, Some _ ->
+          Response.Error.(raise (make ~code:RequestFailed ~message:"requires node nand location" ()))
+      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) ->
+            (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 = Arg.Node.to_string n; cfg_node = cfg_node_id; location; next; prev}
+  end);
+
   register (module struct
     let name = "node_state"
     type params = { nid: string }  [@@deriving of_yojson]

src/witness/argTools.ml

@@ -0,0 +1,129 @@
+open MyCFG
+
+module type BiArg =
+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
+
+let current_arg: (module BiArg) option ref = ref None
+
+module Make (R: ResultQuery.SpecSysSol2) =
+struct
+  open R
+  open SpecSys
+
+  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 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
+
+    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: (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
+      let iter_nodes f =
+        f main_entry;
+        NHT.iter (fun n _ ->
+            f n
+          ) witness_prev_map
+    end
+    in
+    (module Arg: BiArg with type Node.t = MyCFG.node * Spec.C.t * int)
+
+  let create entrystates =
+    Timing.wrap "arg create" create entrystates
+end

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 =