diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 620fbc8c79..cb16a2bb97 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/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
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index d834a6928a..2398bd4199 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -98,6 +98,7 @@ struct
let printXml f c = BatPrintf.fprintf f "%a" printXml c (* wrap in 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
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 2364234580..c289a805a0 100644
--- a/src/framework/constraints.ml
+++ b/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 ()
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 2d18814ad2..ab4b9960f2 100644
--- a/src/framework/control.ml
+++ b/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
diff --git a/src/util/server.ml b/src/util/server.ml
index 2adb5782a2..8ee1fe579e 100644
--- a/src/util/server.ml
+++ b/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 = {