Add arg/dot, arg/state, arg/eval and arg/eval-int requests to server mode

src/analyses/base.ml

@@ -1261,6 +1261,9 @@ struct
         | `Bot -> Queries.Result.bot q (* TODO: remove *)
         | _ -> Queries.Result.top q
       end
+    | Q.EvalValueYojson e ->
+      let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
+      `Lifted (VD.to_yojson v)
     | Q.BlobSize e -> begin
         let p = eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in
         (* ignore @@ printf "BlobSize %a MayPointTo %a\n" d_plainexp e VD.pretty p; *)

src/analyses/mCP.ml

@@ -307,6 +307,8 @@ struct
              (* TODO: only query others that actually respond to EvalInt *)
              (* 2x speed difference on SV-COMP nla-digbench-scaling/ps6-ll_valuebound5.c *)
              f (Result.top ()) (!base_id, spec !base_id, assoc !base_id ctx.local) *)
+          | Queries.DYojson ->
+            `Lifted (D.to_yojson ctx.local)
           | _ ->
             let r = fold_left (f ~q) (Result.top ()) @@ spec_list ctx.local in
             do_sideg ctx !sides;

src/cdomains/apron/apronDomain.apron.ml

@@ -473,7 +473,6 @@ struct
   let is_top_env = A.is_top Man.mgr
   let is_bot_env = A.is_bottom Man.mgr
 
-  let to_yojson x = failwith "TODO implement to_yojson"
   let invariant _ = []
   let tag _ = failwith "Std: no tag"
   let arbitrary () = failwith "no arbitrary"
@@ -494,6 +493,20 @@ struct
     Stdlib.compare x y
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)))
 
+  let to_yojson (x: t) =
+    let constraints =
+      A.to_lincons_array Man.mgr x
+      |> SharedFunctions.Lincons1Set.of_earray
+      |> SharedFunctions.Lincons1Set.elements
+      |> List.map (fun lincons1 -> `String (SharedFunctions.Lincons1.show lincons1))
+    in
+    let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))
+    in
+    `Assoc [
+      ("constraints", `List constraints);
+      ("env", env);
+    ]
+
   let unify x y =
     A.unify Man.mgr x y
 

src/cdomains/valueDomain.ml

@@ -49,17 +49,19 @@ sig
 end
 
 (* ZeroInit is true if malloc was used to allocate memory and it's false if calloc was used *)
-module ZeroInit = Lattice.Fake(Basetype.RawBools)
+module ZeroInit =
+struct
+  include Lattice.Fake(Basetype.RawBools)
+  let name () = "no zeroinit"
+end
 
 module Blob (Value: S) (Size: IntDomain.Z)=
 struct
-  include Lattice.Prod3 (Value) (Size) (ZeroInit)
+  include Lattice.Prod3 (struct include Value let name () = "value" end) (struct include Size let name () = "size" end) (ZeroInit)
   let name () = "blob"
   type value = Value.t
   type size = Size.t
   type origin = ZeroInit.t
-  let printXml f (x, y, z) =
-    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\nsize\n</key>\n%a<key>\norigin\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Value.name ())) Value.printXml x Size.printXml y ZeroInit.printXml z
 
   let value (a, b, c) = a
   let invalidate_value ask t (v, s, o) = Value.invalidate_value ask t v, s, o

src/domains/printable.ml

@@ -620,3 +620,25 @@ let get_short_list begin_str end_str list =
 
   let str = String.concat separator cut_str_list in
   begin_str ^ str ^ end_str
+
+
+module Yojson =
+struct
+  include Std
+  type t = Yojson.Safe.t [@@deriving eq]
+  let name () = "yojson"
+
+  let compare = Stdlib.compare
+  let hash = Hashtbl.hash
+
+  let pretty = GobYojson.pretty
+
+  include SimplePretty (
+    struct
+      type nonrec t = t
+      let pretty = pretty
+    end
+    )
+
+  let to_yojson x = x (* override SimplePretty *)
+end

src/domains/queries.ml

@@ -54,6 +54,11 @@ type itervar = int -> unit
 let compare_itervar _ _ = 0
 let compare_iterprevvar _ _ = 0
 
+module FlatYojson = Lattice.Flat (Printable.Yojson) (struct
+  let top_name = "top yojson"
+  let bot_name = "bot yojson"
+end)
+
 module SD = Basetype.Strings
 
 module MayBool = BoolDomain.MayBool
@@ -99,11 +104,14 @@ type _ t =
   | EvalInt: exp -> ID.t t
   | EvalStr: exp -> SD.t t
   | EvalLength: exp -> ID.t t (* length of an array or string *)
+  | EvalValueYojson: exp -> FlatYojson.t t (** Yojson because [ValueDomain] would have dependency cycle. *)
   | BlobSize: exp -> ID.t t (* size of a dynamically allocated `Blob pointed to by exp *)
   | CondVars: exp -> ES.t t
   | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *)
   | IterPrevVars: iterprevvar -> Unit.t t
   | IterVars: itervar -> Unit.t t
+  | PathQuery: int * 'a t -> 'a t (** Query only one path under witness lifter. *)
+  | DYojson: FlatYojson.t t (** Get local state Yojson of one path under [PathQuery]. *)
   | HeapVar: VI.t t
   | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
   | IsMultiple: varinfo -> MustBool.t t (* Is no other copy of this local variable reachable via pointers? *)
@@ -130,7 +138,7 @@ type ask = { f: 'a. 'a t -> 'a result }
 (* Result cannot implement Lattice.S because the function types are different due to GADT. *)
 module Result =
 struct
-  let lattice (type a) (q: a t): (module Lattice.S with type t = a) =
+  let rec lattice: type a. a t -> (module Lattice.S with type t = a) = fun q ->
     match q with
     (* Cannot group these GADTs... *)
     | EqualSet _ -> (module ES)
@@ -152,12 +160,15 @@ struct
     | MustBeUniqueThread -> (module MustBool)
     | EvalInt _ -> (module ID)
     | EvalLength _ -> (module ID)
+    | EvalValueYojson _ -> (module FlatYojson)
     | BlobSize _ -> (module ID)
     | CurrentThreadId -> (module ThreadIdDomain.ThreadLifted)
     | HeapVar -> (module VI)
     | EvalStr _ -> (module SD)
     | IterPrevVars _ -> (module Unit)
     | IterVars _ -> (module Unit)
+    | PathQuery (_, q) -> lattice q
+    | DYojson -> (module FlatYojson)
     | PartAccess _ -> Obj.magic (module Unit: Lattice.S) (* Never used, MCP handles PartAccess specially. Must still return module (instead of failwith) here, but the module is never used. *)
     | IsMultiple _ -> (module MustBool) (* see https://github.com/goblint/analyzer/pull/310#discussion_r700056687 on why this needs to be MustBool *)
     | EvalThread _ -> (module ConcDomain.ThreadSet)
@@ -177,7 +188,7 @@ struct
     Result.bot ()
 
   (** Get top result for query. *)
-  let top (type a) (q: a t): a result =
+  let rec top: type a. a t -> a result = fun q ->
     (* let module Result = (val lattice q) in
     Result.top () *)
     (* [lattice] and [top] manually inlined to avoid first-class module
@@ -204,12 +215,15 @@ struct
     | MustBeUniqueThread -> MustBool.top ()
     | EvalInt _ -> ID.top ()
     | EvalLength _ -> ID.top ()
+    | EvalValueYojson _ -> FlatYojson.top ()
     | BlobSize _ -> ID.top ()
     | CurrentThreadId -> ThreadIdDomain.ThreadLifted.top ()
     | HeapVar -> VI.top ()
     | EvalStr _ -> SD.top ()
     | IterPrevVars _ -> Unit.top ()
     | IterVars _ -> Unit.top ()
+    | PathQuery (_, q) -> top q
+    | DYojson -> FlatYojson.top ()
     | PartAccess _ -> failwith "Queries.Result.top: PartAccess" (* Never used, MCP handles PartAccess specially. *)
     | IsMultiple _ -> MustBool.top ()
     | EvalThread _ -> ConcDomain.ThreadSet.top ()
@@ -271,8 +285,11 @@ struct
     | Any (MustProtectedVars _) -> 39
     | Any MayAccessed -> 40
     | Any MayBeTainted -> 41
+    | Any (PathQuery _) -> 42
+    | Any DYojson -> 43
+    | Any (EvalValueYojson _) -> 44
 
-  let compare a b =
+  let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
     if r <> 0 then
       r
@@ -291,25 +308,32 @@ struct
       | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2
       | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
+      | Any (EvalValueYojson e1), Any (EvalValueYojson e2) -> CilType.Exp.compare e1 e2
       | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2
       | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2
       | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2
       | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2
       | Any (IterVars i1), Any (IterVars i2) -> compare_itervar i1 i2
+      | Any (PathQuery (i1, q1)), Any (PathQuery (i2, q2)) ->
+        let r = Stdlib.compare i1 i2 in
+        if r <> 0 then
+          r
+        else
+          compare (Any q1) (Any q2)
       | Any (IsHeapVar v1), Any (IsHeapVar v2) -> CilType.Varinfo.compare v1 v2
       | Any (IsMultiple v1), Any (IsMultiple v2) -> CilType.Varinfo.compare v1 v2
       | Any (EvalThread e1), Any (EvalThread e2) -> CilType.Exp.compare e1 e2
-      | Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
+      | Any (WarnGlobal vi1), Any (WarnGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (Invariant i1), Any (Invariant i2) -> compare_invariant_context i1 i2
-      | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
+      | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
       | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
   let equal x y = compare x y = 0
 
-  let hash_arg = function
+  let rec hash_arg = function
     | Any (EqualSet e) -> CilType.Exp.hash e
     | Any (MayPointTo e) -> CilType.Exp.hash e
     | Any (ReachableFrom e) -> CilType.Exp.hash e
@@ -323,11 +347,13 @@ struct
     | Any (EvalInt e) -> CilType.Exp.hash e
     | Any (EvalStr e) -> CilType.Exp.hash e
     | Any (EvalLength e) -> CilType.Exp.hash e
+    | Any (EvalValueYojson e) -> CilType.Exp.hash e
     | Any (BlobSize e) -> CilType.Exp.hash e
     | Any (CondVars e) -> CilType.Exp.hash e
     | Any (PartAccess p) -> hash_access p
     | Any (IterPrevVars i) -> 0
     | Any (IterVars i) -> 0
+    | Any (PathQuery (i, q)) -> 31 * i + hash (Any q)
     | Any (IsHeapVar v) -> CilType.Varinfo.hash v
     | Any (IsMultiple v) -> CilType.Varinfo.hash v
     | Any (EvalThread e) -> CilType.Exp.hash e
@@ -338,9 +364,9 @@ struct
     (* only argumentless queries should remain *)
     | _ -> 0
 
-  let hash x = 31 * order x + hash_arg x
+  and hash x = 31 * order x + hash_arg x
 
-  let pretty () = function
+  let rec pretty () = function
     | Any (EqualSet e) -> Pretty.dprintf "EqualSet %a" CilType.Exp.pretty e
     | Any (MayPointTo e) -> Pretty.dprintf "MayPointTo %a" CilType.Exp.pretty e
     | Any (ReachableFrom e) -> Pretty.dprintf "ReachableFrom %a" CilType.Exp.pretty e
@@ -360,11 +386,13 @@ struct
     | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e
     | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e
     | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e
+    | Any (EvalValueYojson e) -> Pretty.dprintf "EvalValueYojson %a" CilType.Exp.pretty e
     | Any (BlobSize e) -> Pretty.dprintf "BlobSize %a" CilType.Exp.pretty e
     | Any (CondVars e) -> Pretty.dprintf "CondVars %a" CilType.Exp.pretty e
     | Any (PartAccess p) -> Pretty.dprintf "PartAccess _"
     | Any (IterPrevVars i) -> Pretty.dprintf "IterPrevVars _"
     | Any (IterVars i) -> Pretty.dprintf "IterVars _"
+    | Any (PathQuery (i, q)) -> Pretty.dprintf "PathQuery (%d, %a)" i pretty (Any q)
     | Any HeapVar -> Pretty.dprintf "HeapVar"
     | Any (IsHeapVar v) -> Pretty.dprintf "IsHeapVar %a" CilType.Varinfo.pretty v
     | Any (IsMultiple v) -> Pretty.dprintf "IsMultiple %a" CilType.Varinfo.pretty v
@@ -378,6 +406,7 @@ struct
     | Any (InvariantGlobal i) -> Pretty.dprintf "InvariantGlobal _"
     | Any MayAccessed -> Pretty.dprintf "MayAccessed"
     | Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
+    | Any DYojson -> Pretty.dprintf "DYojson"
 end
 
 

src/util/gobZ.ml

@@ -0,0 +1,4 @@
+type t = Z.t
+
+let to_yojson z =
+  `Intlit (Z.to_string z)