Refactor MCP.query'

Author: sim642

src/analyses/mCP.ml

@@ -264,46 +264,48 @@ struct
 
   (* Explicitly polymorphic type required here for recursive GADT call in ask. *)
   and query': type a. querycache:Obj.t QueryHash.t -> QuerySet.t -> (D.t, G.t, C.t, V.t) ctx -> a Queries.t -> a Queries.result = fun ~querycache asked ctx q ->
-    let module Result = (val Queries.Result.lattice q) in
-    if QuerySet.mem (Any q) asked then
-      Result.top () (* query cycle *)
-    else if QueryHash.mem querycache (Any q) then
-      Obj.obj (QueryHash.find querycache (Any q))
-    else
-      let asked' = QuerySet.add (Any q) asked in
-      let sides = ref [] in
-      let ctx'' = outer_ctx "query" ~sides ctx in
-      let f ~q a (n,(module S:MCPSpec),d) =
-        let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "query" ctx'' n d in
-        (* sideg is discouraged in query, because they would bypass sides grouping in other transfer functions.
-           See https://github.com/goblint/analyzer/pull/214. *)
-        let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
-          { ctx' with
-            ask    = (fun (type b) (q: b Queries.t) -> query' ~querycache asked' ctx q)
-          }
+    let anyq = Queries.Any q in
+    match QueryHash.find_option querycache anyq with
+    | Some r -> Obj.obj r
+    | None ->
+      let module Result = (val Queries.Result.lattice q) in
+      if QuerySet.mem anyq asked then
+        Result.top () (* query cycle *)
+      else
+        let asked' = QuerySet.add anyq asked in
+        let sides = ref [] in
+        let ctx'' = outer_ctx "query" ~sides ctx in
+        let f ~q a (n,(module S:MCPSpec),d) =
+          let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "query" ctx'' n d in
+          (* sideg is discouraged in query, because they would bypass sides grouping in other transfer functions.
+            See https://github.com/goblint/analyzer/pull/214. *)
+          let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+            { ctx' with
+              ask    = (fun (type b) (q: b Queries.t) -> query' ~querycache asked' ctx q)
+            }
+          in
+          (* meet results so that precision from all analyses is combined *)
+          Result.meet a @@ S.query ctx' q
         in
-        (* meet results so that precision from all analyses is combined *)
-        Result.meet a @@ S.query ctx' q
-      in
-      match q with
-      | Queries.PrintFullState ->
-        ignore (Pretty.printf "Current State:\n%a\n\n" D.pretty ctx.local);
-        ()
-      | Queries.WarnGlobal g ->
-        (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
-        let (n, g): V.t = Obj.obj g in
-        f ~q:(WarnGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
-      | Queries.PartAccess {exp; var_opt; write} ->
-        Obj.repr (access ctx exp var_opt write)
-      (* | EvalInt e ->
-        (* 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) *)
-      | _ ->
-        let r = fold_left (f ~q) (Result.top ()) @@ spec_list ctx.local in
-        do_sideg ctx !sides;
-        QueryHash.replace querycache (Any q) (Obj.repr r);
-        r
+        match q with
+        | Queries.PrintFullState ->
+          ignore (Pretty.printf "Current State:\n%a\n\n" D.pretty ctx.local);
+          ()
+        | Queries.WarnGlobal g ->
+          (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
+          let (n, g): V.t = Obj.obj g in
+          f ~q:(WarnGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
+        | Queries.PartAccess {exp; var_opt; write} ->
+          Obj.repr (access ctx exp var_opt write)
+        (* | EvalInt e ->
+          (* 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) *)
+        | _ ->
+          let r = fold_left (f ~q) (Result.top ()) @@ spec_list ctx.local in
+          do_sideg ctx !sides;
+          QueryHash.replace querycache anyq (Obj.repr r);
+          r
 
   and query: type a. (D.t, G.t, C.t, V.t) ctx -> a Queries.t -> a Queries.result = fun ctx q ->
     let querycache = QueryHash.create 13 in