Merge pull request #1001 from goblint/arg-lookup

Add `arg/lookup` request to server mode

.gitignore

@@ -44,6 +44,7 @@ _opam/
 cfgs/
 cfg.dot
 cilcfg.*.dot
+arg.dot
 
 *.graphml
 goblint.bc.js

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)
@@ -663,6 +664,23 @@ 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
+      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);
+    );
+
     (* 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/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)

src/util/options.schema.json

@@ -1634,6 +1634,18 @@
           "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
+        },
+        "argdot": {
+          "title": "exp.argdot",
+          "description": "Output ARG as dot file.",
+          "type": "boolean",
+          "default": false
         }
       },
       "additionalProperties": false

src/util/server.ml

@@ -2,9 +2,19 @@ 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
+  val find_cfg_node: string -> Arg.Node.t list
+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 +116,36 @@ 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
+      let cfg_nodes = StringH.create 113 in
+      Arg.iter_nodes (fun n ->
+          let cfgnode = Arg.Node.cfgnode n 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;
+          StringH.add cfg_nodes (Node.show_id cfgnode) n (* add for find_all *)
+        );
+
+      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)
+    )
+
 let make ?(input=stdin) ?(output=stdout) file : t =
   let max_ids =
     match file with
@@ -115,6 +155,7 @@ let make ?(input=stdin) ?(output=stdout) file : t =
   {
     file;
     max_ids;
+    arg_wrapper;
     input;
     output
   }
@@ -189,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) ->
@@ -219,6 +260,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 ();
@@ -389,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
@@ -406,6 +448,100 @@ 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];
+      cfg_node: string option [@default None];
+    } [@@deriving of_yojson]
+
+    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;
+      cfg_node: string;
+      context: string;
+      path: string;
+      location: CilType.Location.t;
+      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
+      let open GobList.Syntax in
+      let+ n: Arg.Node.t = match params.node, params.location, params.cfg_node with
+        | None, None, None ->
+          [Arg.main_entry]
+        | Some node_id, None, None ->
+          begin try
+              [ArgWrapper.find_node node_id]
+            with Not_found ->
+              [] (* non-existent node *)
+          end
+        | 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 *)
+        | 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
+      let location = UpdateCil.getLoc cfg_node in
+      let next =
+        Arg.next n
+        |> List.map (fun (edge, 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 = UpdateCil.getLoc cfg_to_node;
+            }
+          )
+      in
+      let prev =
+        Arg.prev n
+        |> List.map (fun (edge, 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 = UpdateCil.getLoc cfg_to_node;
+            }
+          )
+      in
+      {
+        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
     let name = "node_state"
     type params = { nid: string }  [@@deriving of_yojson]