From caa55342e5b3d63e03201b15d06cd8d8fb2cfc4a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 10:49:48 +0200 Subject: [PATCH 1/3] Add global-state request to server --- src/framework/constraints.ml | 2 ++ src/framework/control.ml | 32 ++++++++++++++++++++++++++++++-- src/util/server.ml | 27 +++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 2 deletions(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 2364234580..57d62c8df9 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -477,6 +477,8 @@ module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment) and module GVar = GVarF (S.V) and module D = S.D and module G = GVarG (S.G) (S.C) + + val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit end = struct diff --git a/src/framework/control.ml b/src/framework/control.ml index 2d18814ad2..a2319e5166 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -45,11 +45,13 @@ 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 - module SpecSys: SpecSys with module Spec = Spec = + module SpecSys (*: SpecSys with module Spec = Spec *) = struct (* Must be created in module, because cannot be wrapped in a module later. *) module Spec = Spec @@ -640,11 +642,37 @@ struct let gh = gh end in - let module R: ResultQuery.SpecSysSol2 with module SpecSys = SpecSys = ResultQuery.Make (FileCfg) (SpecSysSol) in + let module R (*: ResultQuery.SpecSysSol2 with module SpecSys = SpecSys *) = ResultQuery.Make (FileCfg) (SpecSysSol) in 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 3c99d44cb7..b64e39149d 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -595,6 +595,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 = "exp_eval" type params = ExpressionEvaluation.query [@@deriving of_yojson] From 9feb075ad4cddf9ca79c3dc3799a3801f2c1b49b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Mar 2023 11:15:09 +0200 Subject: [PATCH 2/3] Improve JSON of global domain names --- src/analyses/mCPRegistry.ml | 11 ++++++++--- src/framework/analyses.ml | 1 + src/framework/constraints.ml | 7 ++++++- 3 files changed, 15 insertions(+), 4 deletions(-) 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..846cab2d4b 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) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 57d62c8df9..393320f322 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1220,11 +1220,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 () From 16f612478eb437e463dd1e2b7ca44b942ba73686 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 21 Mar 2023 14:05:31 +0200 Subject: [PATCH 3/3] Add iter_vars to GlobConstrSys --- src/framework/analyses.ml | 1 + src/framework/constraints.ml | 2 -- src/framework/control.ml | 4 ++-- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 846cab2d4b..2398bd4199 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -472,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 393320f322..c289a805a0 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -477,8 +477,6 @@ module FromSpec (S:Spec) (Cfg:CfgBackward) (I: Increment) and module GVar = GVarF (S.V) and module D = S.D and module G = GVarG (S.G) (S.C) - - val iter_vars: (LVar.t -> D.t) -> (GVar.t -> G.t) -> VarQuery.t -> LVar.t VarQuery.f -> GVar.t VarQuery.f -> unit end = struct diff --git a/src/framework/control.ml b/src/framework/control.ml index a2319e5166..ab4b9960f2 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -51,7 +51,7 @@ let current_varquery_global_state_json: (VarQuery.t option -> Yojson.Safe.t) ref module AnalyzeCFG (Cfg:CfgBidir) (Spec:Spec) (Inc:Increment) = struct - module SpecSys (*: SpecSys with module Spec = Spec *) = + module SpecSys: SpecSys with module Spec = Spec = struct (* Must be created in module, because cannot be wrapped in a module later. *) module Spec = Spec @@ -642,7 +642,7 @@ struct let gh = gh end in - let module R (*: ResultQuery.SpecSysSol2 with module SpecSys = SpecSys *) = ResultQuery.Make (FileCfg) (SpecSysSol) in + let module R: ResultQuery.SpecSysSol2 with module SpecSys = SpecSys = ResultQuery.Make (FileCfg) (SpecSysSol) in let local_xml = solver2source_result lh in current_node_state_json := (fun node -> Option.map LT.to_yojson (Result.find_option local_xml node));