Type-safe global query system

src/analyses/base.ml

@@ -1236,14 +1236,14 @@ struct
     else
       Invariant.none
 
-  let query_invariant_global ctx g =
+  let query_invariant_global (gctx: _ gctx) g =
     if GobConfig.get_bool "ana.base.invariant.enabled" && get_bool "exp.earlyglobs" then (
       (* Currently these global invariants are only sound with earlyglobs enabled for both single- and multi-threaded programs.
          Otherwise, the values of globals in single-threaded mode are not accounted for. *)
       (* TODO: account for single-threaded values without earlyglobs. *)
       match g with
       | `Left g' -> (* priv *)
-        Priv.invariant_global (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) g'
+        Priv.invariant_global (Analyses.ask_of_gctx gctx) (priv_getg gctx.global) g'
       | `Right _ -> (* thread return *)
         Invariant.none
     )
@@ -1514,14 +1514,18 @@ struct
       let vf' x = vf (Obj.repr (V.priv x)) in
       Priv.iter_sys_vars (priv_getg ctx.global) vq vf'
     | Q.Invariant context -> query_invariant ctx context
-    | Q.InvariantGlobal g ->
-      let g: V.t = Obj.obj g in
-      query_invariant_global ctx g
     | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow ctx e in
                                 if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp e res; res
                                )
     | _ -> Q.Result.top q
 
+  let global_query gctx (type a) (q: a Q.t): a Q.result =
+    match gctx.var, q with
+    | Some g, Q.InvariantGlobal ->
+      query_invariant_global gctx g
+    | _, _ ->
+      Q.Result.top q
+
   let update_variable variable typ value cpa =
     if ((get_bool "exp.volatiles_are_top") && (is_always_unknown variable)) then
       CPA.add variable (VD.top_value ~varAttr:variable.vattr typ) cpa

src/analyses/deadlock.ml

@@ -47,11 +47,9 @@ struct
 
   module G = Arg.G (* help type checker using explicit constraint *)
 
-  let query ctx (type a) (q: a Queries.t): a Queries.result =
-    match q with
-    | WarnGlobal g ->
-      let g: V.t = Obj.obj g in
-
+  let global_query gctx (type a) (q: a Queries.t): a Queries.result =
+    match gctx.var, q with
+    | Some g, WarnGlobal ->
       let module LH = Hashtbl.Make (Lock) in
       let module LS = Set.Make (Lock) in
       (* TODO: find all cycles/SCCs *)
@@ -105,12 +103,12 @@ struct
                   let new_path_visited_lock_event_pairs' = lock_event_pair :: path_visited_lock_event_pairs in
                   iter_lock new_path_visited_locks new_path_visited_lock_event_pairs' to_lock
                 ) lock_event_pairs
-            ) (ctx.global lock)
+            ) (gctx.global lock)
         end
       in
 
       Timing.wrap ~args:[("lock", `String (Lock.show g))] "deadlock" (iter_lock LS.empty []) g
-    | _ -> Queries.Result.top q
+    | _, _ -> Queries.Result.top q
 end
 
 let _ =

src/analyses/loopTermination.ml

@@ -16,11 +16,6 @@ let check_bounded ctx varinfo =
   | `Lifted v -> not (is_top_of (ikind v) v)
   | `Bot -> failwith "Loop counter variable is Bot."
 
-(** We want to record termination information of loops and use the loop
- * statements for that. We use this lifting because we need to have a
- * lattice. *)
-module Statements = Lattice.Flat (CilType.Stmt)
-
 (** The termination analysis considering loops and gotos *)
 module Spec : Analyses.MCPSpec =
 struct
@@ -35,7 +30,7 @@ struct
     include UnitV
     let is_write_only _ = true
   end
-  module G = MapDomain.MapBot (Statements) (BoolDomain.MustBool)
+  module G = BoolDomain.MustBool
 
   let startstate _ = ()
   let exitstate = startstate
@@ -52,7 +47,7 @@ struct
         (try
            let loop_statement = find_loop ~loop_counter in
            let is_bounded = check_bounded ctx loop_counter in
-           ctx.sideg () (G.add (`Lifted loop_statement) is_bounded (ctx.global ()));
+           ctx.sideg () is_bounded;
            (* In case the loop is not bounded, a warning is created. *)
            if not (is_bounded) then (
              M.warn ~loc:(M.Location.CilLocation (Cilfacade.get_stmtLoc loop_statement)) ~category:Termination "The program might not terminate! (Loop analysis)"
@@ -63,23 +58,20 @@ struct
       | _ -> ()
     else ()
 
-  let query ctx (type a) (q: a Queries.t): a Queries.result =
+  let global_query (gctx: _ gctx) (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | Queries.MustTermLoop loop_statement ->
-      let multithreaded = ctx.ask Queries.IsEverMultiThreaded in
-      (not multithreaded)
-      && (match G.find_opt (`Lifted loop_statement) (ctx.global ()) with
-            Some b -> b
-          | None -> false)
-    | Queries.MustTermAllLoops ->
-      let multithreaded = ctx.ask Queries.IsEverMultiThreaded in
-      if multithreaded then (
-        M.warn ~category:Termination "The program might not terminate! (Multithreaded)";
-        false)
-      else
-        G.for_all (fun _ term_info -> term_info) (ctx.global ())
+    | WarnGlobal ->
+      let must_term_all_loops =
+        let multithreaded = gctx.ask Queries.IsEverMultiThreaded in
+        if multithreaded then (
+          M.warn ~category:Termination "The program might not terminate! (Multithreaded)";
+          false)
+        else
+          gctx.global ()
+      in
+      if not must_term_all_loops then
+        AnalysisState.svcomp_may_not_terminate := true;
     | _ -> Queries.Result.top q
-
 end
 
 let () =

src/analyses/mCP.ml

@@ -277,14 +277,6 @@ struct
             Result.meet a @@ res
           in
           match q with
-          | 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.InvariantGlobal g ->
-            (* InvariantGlobal 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:(InvariantGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
           | Queries.PartAccess a ->
             Obj.repr (access ctx a)
           | Queries.IterSysVars (vq, fi) ->
@@ -599,6 +591,32 @@ struct
 
   let event (ctx:(D.t, G.t, C.t, V.t) ctx) e _ = do_emits ctx [e] ctx.local false
 
+  let rec global_query: type a. (V.t, G.t) gctx -> a Queries.t -> a Queries.result = fun gctx q ->
+    match gctx.var with
+    | Some (n, g) ->
+      (* TODO: cache? *)
+      let module S: MCPSpec = (val spec n: MCPSpec) in
+      let gctx' = {
+        var = Some (Obj.obj g);
+        global = (fun v -> gctx.global (v_of n v) |> g_to n |> obj);
+        ask = (fun (type b) (q: b Queries.t) -> global_query {gctx with var = None} q);
+      }
+      in
+      S.global_query gctx' q
+    | None ->
+      let module Result = (val Queries.Result.lattice q) in
+      let f acc (n, spec_modules) =
+        let module S: MCPSpec = (val spec_modules.spec: MCPSpec) in
+        let gctx' = {
+          var = None;
+          global = (fun v -> gctx.global (v_of n v) |> g_to n |> obj);
+          ask = (fun (type b) (q: b Queries.t) -> global_query {gctx with var = None} q);
+        }
+        in
+        Result.meet acc (S.global_query gctx' q)
+      in
+      fold_left f (Result.top ()) (!activated)
+
   (* Just to satisfy signature *)
   let paths_as_set ctx = [ctx.local]
 end

src/analyses/mutexAnalysis.ml

@@ -246,27 +246,23 @@ struct
         ) protected (Queries.VS.empty ())
     | Queries.IterSysVars (Global g, f) ->
       f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *)
-    | WarnGlobal g ->
-      let g: V.t = Obj.obj g in
-      begin match g with
-        | `Left g' -> (* protecting *)
-          if GobConfig.get_bool "dbg.print_protection" then (
-            let protecting = GProtecting.get ~write:false Strong (G.protecting (ctx.global g)) in (* readwrite protecting *)
-            let s = Mutexes.cardinal protecting in
-            M.info_noloc ~category:Race "Variable %a read-write protected by %d mutex(es): %a" CilType.Varinfo.pretty g' s Mutexes.pretty protecting
-          )
-        | `Right m -> (* protected *)
-          if GobConfig.get_bool "dbg.print_protection" then (
-            let protected = GProtected.get ~write:false Strong (G.protected (ctx.global g)) in (* readwrite protected *)
-            let s = VarSet.cardinal protected in
-            max_protected := max !max_protected s;
-            sum_protected := !sum_protected + s;
-            incr num_mutexes;
-            M.info_noloc ~category:Race "Mutex %a read-write protects %d variable(s): %a" ValueDomain.Addr.pretty m s VarSet.pretty protected
-          )
-      end
     | _ -> Queries.Result.top q
 
+  let global_query gctx (type a) (q: a Queries.t): a Queries.result =
+    match gctx.var, q with
+    | Some (`Left g' as g), WarnGlobal when GobConfig.get_bool "dbg.print_protection" -> (* protecting *)
+      let protecting = GProtecting.get ~write:false Strong (G.protecting (gctx.global g)) in (* readwrite protecting *)
+      let s = Mutexes.cardinal protecting in
+      M.info_noloc ~category:Race "Variable %a read-write protected by %d mutex(es): %a" CilType.Varinfo.pretty g' s Mutexes.pretty protecting
+    | Some (`Right m as g), WarnGlobal when GobConfig.get_bool "dbg.print_protection" -> (* protected *)
+      let protected = GProtected.get ~write:false Strong (G.protected (gctx.global g)) in (* readwrite protected *)
+      let s = VarSet.cardinal protected in
+      max_protected := max !max_protected s;
+      sum_protected := !sum_protected + s;
+      incr num_mutexes;
+      M.info_noloc ~category:Race "Mutex %a read-write protects %d variable(s): %a" ValueDomain.Addr.pretty m s VarSet.pretty protected
+    | _, _ -> Queries.Result.top q
+
   module A =
   struct
     include Lockset

src/analyses/raceAnalysis.ml

@@ -247,55 +247,53 @@ struct
     | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *)
     | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)
 
-  let rec find_type_suffix' ctx ((root, offset) as memo : Access.Memo.t) : Access.AS.t =
-    let trie = G.access (ctx.global (V.access root)) in
+  let rec find_type_suffix' (gctx: _ gctx) ((root, offset) as memo : Access.Memo.t) : Access.AS.t =
+    let trie = G.access (gctx.global (V.access root)) in
     let accs =
       match OffsetTrie.find offset trie with
       | `Lifted accs -> accs
       | `Bot -> Access.AS.empty ()
     in
-    let type_suffix = find_type_suffix ctx memo in
+    let type_suffix = find_type_suffix gctx memo in
     Access.AS.union accs type_suffix
 
   (** Find accesses from all type_suffixes transitively. *)
-  and find_type_suffix ctx (memo : Access.Memo.t) : Access.AS.t =
+  and find_type_suffix gctx (memo : Access.Memo.t) : Access.AS.t =
     match type_suffix_memo memo with
-    | Some type_suffix_memo -> find_type_suffix' ctx type_suffix_memo
+    | Some type_suffix_memo -> find_type_suffix' gctx type_suffix_memo
     | None -> Access.AS.empty ()
 
+  let global_query gctx (type a) (q: a Queries.t): a Queries.result =
+    match gctx.var, q with
+    | Some (`Left g' as g), WarnGlobal -> (* accesses *)
+      (* Logs.debug "WarnGlobal %a" Access.MemoRoot.pretty g'; *)
+      let trie = G.access (gctx.global g) in
+      (** Distribute access to contained fields. *)
+      let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix =
+        let accs =
+          match accs with
+          | `Lifted accs -> accs
+          | `Bot -> Access.AS.empty ()
+        in
+        let type_suffix = find_type_suffix gctx (g', offset) in
+        if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then (
+          let memo = (g', offset) in
+          let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in
+          Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {node=accs; prefix; type_suffix; type_suffix_prefix}) memo
+        );
+
+        (* Recurse to children. *)
+        let prefix' = Access.AS.union prefix accs in
+        let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in
+        OffsetTrie.ChildMap.iter (fun child_key child_trie ->
+            distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~prefix:prefix' ~type_suffix_prefix:type_suffix_prefix'
+          ) children;
+      in
+      distribute_inner `NoOffset trie ~prefix:(Access.AS.empty ()) ~type_suffix_prefix:(Access.AS.empty ())
+    | _, _ -> Queries.Result.top q
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | WarnGlobal g ->
-      let g: V.t = Obj.obj g in
-      begin match g with
-        | `Left g' -> (* accesses *)
-          (* Logs.debug "WarnGlobal %a" Access.MemoRoot.pretty g'; *)
-          let trie = G.access (ctx.global g) in
-          (** Distribute access to contained fields. *)
-          let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix =
-            let accs =
-              match accs with
-              | `Lifted accs -> accs
-              | `Bot -> Access.AS.empty ()
-            in
-            let type_suffix = find_type_suffix ctx (g', offset) in
-            if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then (
-              let memo = (g', offset) in
-              let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in
-              Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {node=accs; prefix; type_suffix; type_suffix_prefix}) memo
-            );
-
-            (* Recurse to children. *)
-            let prefix' = Access.AS.union prefix accs in
-            let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in
-            OffsetTrie.ChildMap.iter (fun child_key child_trie ->
-                distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~prefix:prefix' ~type_suffix_prefix:type_suffix_prefix'
-              ) children;
-          in
-          distribute_inner `NoOffset trie ~prefix:(Access.AS.empty ()) ~type_suffix_prefix:(Access.AS.empty ())
-        | `Right _ -> (* vars *)
-          ()
-      end
     | IterSysVars (Global g, vf) ->
       MemoSet.iter (fun v ->
           vf (Obj.repr (V.access v))

src/analyses/threadFlag.ml

@@ -42,6 +42,11 @@ struct
     | _ ->
       ctx.local
 
+  let global_query (gctx: _ gctx) (type a) (x: a Queries.t): a Queries.result =
+    match x with
+    | Queries.IsEverMultiThreaded -> (gctx.global () : bool) (* requires annotation to compile *)
+    | _ -> Queries.Result.top x
+
   let query ctx (type a) (x: a Queries.t): a Queries.result =
     match x with
     | Queries.MustBeSingleThreaded _ -> not (Flag.is_multi ctx.local) (* If this analysis can tell, it is the case since the start *)