Add privatization of effectively thread-local globals

src/analyses/accessAnalysis.ml

@@ -29,7 +29,7 @@ struct
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
+    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated || List.mem (ThreadAccess.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
 
   let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;

src/analyses/threadAccess.ml

@@ -0,0 +1,42 @@
+open Analyses
+
+module Spec =
+struct
+  include UnitAnalysis.Spec
+
+  let name () = "threadAccess"
+
+  module V =
+  struct
+    include CilType.Varinfo
+    let is_write_only _ = false
+  end
+
+  module G = ConcDomain.ThreadSet
+
+  let query man (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | MayBePublic {global; _} ->
+      if G.cardinal (man.global global) = 1 then
+        false
+      else
+        Queries.Result.top q
+    | _ -> Queries.Result.top q
+
+  let event man e oman =
+    match e with
+    | Events.Access {ad; _} ->
+      Queries.AD.iter (function
+          | Queries.AD.Addr.Addr (v, _) when v.vglob ->
+            begin match man.ask CurrentThreadId with
+              | `Lifted tid -> man.sideg v (G.singleton tid)
+              | _ -> () (* TODO: what here? *)
+            end
+          | _ -> ()
+        ) ad
+    | _ ->
+      man.local
+end
+
+let _ =
+  MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec)

tests/regression/03-practical/39-signal-effectively-local.c

@@ -0,0 +1,19 @@
+// PARAM: --set ana.activated[+] threadAccess
+#include <signal.h>
+#include <goblint.h>
+
+int g = 0;
+
+void handler(int sig) {
+}
+
+int main() {
+  __goblint_check(g == 0);
+  g = 1;
+  __goblint_check(g == 1);
+  signal(SIGTERM, handler);
+  __goblint_check(g == 1);
+  g = 2;
+  __goblint_check(g == 2);
+  return 0;
+}