Add global-state request to server mode

src/analyses/mCPRegistry.ml

@@ -161,12 +161,13 @@ struct
 
   let hash     = unop_fold (fun a n (module S : Printable.S) x -> hashmul a @@ S.hash (obj x)) 0
 
-  let name () =
+  (* let name () =
     let domain_name (n, (module D: Printable.S)) =
       let analysis_name = find_spec_name n in
       analysis_name ^ ":(" ^ D.name () ^ ")"
     in
-    IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) (map domain_name @@ domain_list ())
+    IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) (map domain_name @@ domain_list ()) *)
+  let name () = "MCP.C"
 
   let printXml f xs =
     let print_one a n (module S : Printable.S) x : unit =
@@ -317,6 +318,7 @@ struct
   open Obj
 
   include DomVariantPrintable (PrintableOfLatticeSpec (DLSpec))
+  let name () = "MCP.G"
 
   let binop_map' (f: int -> (module Lattice.S) -> Obj.t -> Obj.t -> 'a) (n1, d1) (n2, d2) =
     assert (n1 = n2);
@@ -346,7 +348,10 @@ struct
 end
 
 module DomVariantLattice (DLSpec : DomainListLatticeSpec) =
-  Lattice.Lift (DomVariantLattice0 (DLSpec)) (Printable.DefaultNames)
+struct
+  include Lattice.Lift (DomVariantLattice0 (DLSpec)) (Printable.DefaultNames)
+  let name () = "MCP.G"
+end
 
 module LocalDomainListSpec : DomainListLatticeSpec =
 struct

src/framework/analyses.ml

@@ -98,6 +98,7 @@ struct
         let printXml f c = BatPrintf.fprintf f "<value>%a</value>" printXml c (* wrap in <value> for HTML printing *)
       end
       )
+    let name () = "contexts"
   end
 
   include Lattice.Lift2 (G) (CSet) (Printable.DefaultNames)
@@ -471,6 +472,7 @@ sig
   module D : Lattice.S
   module G : Lattice.S
   val system : LVar.t -> ((LVar.t -> D.t) -> (LVar.t -> D.t -> unit) -> (GVar.t -> G.t) -> (GVar.t -> G.t -> unit) -> D.t) option
+  val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit
   val sys_change: (LVar.t -> D.t) -> (GVar.t -> G.t) -> [`L of LVar.t | `G of GVar.t] sys_change_info
 end
 

src/framework/constraints.ml

@@ -1218,11 +1218,16 @@ struct
       | `Right _ -> true
   end
 
-  module EM = MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
+  module EM =
+  struct
+    include MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
+    let name () = "branches"
+  end
 
   module G =
   struct
     include Lattice.Lift2 (S.G) (EM) (Printable.DefaultNames)
+    let name () = "deadbranch"
 
     let s = function
       | `Bot -> S.G.bot ()

src/framework/control.ml

@@ -45,6 +45,8 @@ let get_spec (): (module Spec) =
 
 let current_node_state_json : (Node.t -> Yojson.Safe.t option) ref = ref (fun _ -> None)
 
+let current_varquery_global_state_json: (VarQuery.t option -> Yojson.Safe.t) ref = ref (fun _ -> `Null)
+
 (** Given a [Cfg], a [Spec], and an [Inc], computes the solution to [MCP.Path] *)
 module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) =
 struct
@@ -645,6 +647,32 @@ struct
     let local_xml = solver2source_result lh in
     current_node_state_json := (fun node -> Option.map LT.to_yojson (Result.find_option local_xml node));
 
+    current_varquery_global_state_json := (fun vq_opt ->
+        let iter_vars f = match vq_opt with
+          | None -> GHT.iter (fun v _ -> f v) gh
+          | Some vq ->
+            EQSys.iter_vars
+              (fun x -> try LHT.find lh x with Not_found -> EQSys.D.bot ())
+              (fun x -> try GHT.find gh x with Not_found -> EQSys.G.bot ())
+              vq
+              (fun _ -> ())
+              f
+        in
+        (* TODO: optimize this once server has a way to properly convert vid -> varinfo *)
+        let vars = GHT.create 113 in
+        iter_vars (fun x ->
+            GHT.replace vars x ()
+          );
+        let assoc = GHT.fold (fun x g acc ->
+            if GHT.mem vars x then
+              (EQSys.GVar.show x, EQSys.G.to_yojson g) :: acc
+            else
+              acc
+          ) gh []
+        in
+        `Assoc assoc
+      );
+
     let liveness =
       if get_bool "ana.dead-code.lines" || get_bool "ana.dead-code.branches" then
         print_dead_code local_xml !uncalled_dead

src/util/server.ml

@@ -648,6 +648,33 @@ let () =
       | exception Not_found -> Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
   end);
 
+  register (module struct
+    let name = "global-state"
+    type params = {
+      vid: int option [@default None];
+      node: string option [@default None];
+    } [@@deriving of_yojson]
+    type response = Yojson.Safe.t [@@deriving to_yojson]
+    let process (params: params) serv =
+      let vq_opt = match params.vid, params.node with
+        | None, None ->
+          None
+        | Some vid, None ->
+          let vi = {Cil.dummyFunDec.svar with vid} in (* Equal to actual varinfo by vid. *)
+          Some (VarQuery.Global vi)
+        | None, Some node_id ->
+          let node = try
+              Node.of_id node_id
+            with Not_found ->
+              Response.Error.(raise (make ~code:RequestFailed ~message:"not analyzed or non-existent node" ()))
+          in
+          Some (VarQuery.Node {node; fundec = None})
+        | Some _, Some _ ->
+          Response.Error.(raise (make ~code:RequestFailed ~message:"requires at most one of vid and node" ()))
+      in
+      !Control.current_varquery_global_state_json vq_opt
+  end);
+
   register (module struct
     let name = "arg/state"
     type params = {