Test for mutex-meet-tid for ValidDeref & Move Afterconfig.run to ensure privatizations can potentially be auto-tuned

src/analyses/base.ml

@@ -1056,7 +1056,13 @@ struct
             );
             (* Warn if any of the addresses contains a non-local and non-global variable *)
             if AD.exists (function
-                | AD.Addr.Addr (v, _) -> not (CPA.mem v st.cpa) && not (is_global a v)
+                | AD.Addr.Addr (v, _) ->
+                  (M.tracel "wtf" "checking for %a\n" CilType.Varinfo.pretty v;
+                   if v.vglob then
+                     (* this is OK *)
+                     false
+                   else
+                     (not (CPA.mem v st.cpa)) || WeakUpdates.mem v st.weak)
                 | _ -> false
               ) adr then (
               AnalysisStateUtil.set_mem_safety_flag InvalidDeref;

src/autoTune.ml

@@ -222,7 +222,11 @@ let focusOnMemSafetySpecification (spec: Svcomp.Specification.t) =
     print_endline "Setting \"cil.addNestedScopeAttr\" to true";
     set_bool "cil.addNestedScopeAttr" true;
     print_endline @@ "Specification: ValidDeref -> enabling memOutOfBounds analysis \"" ^ (String.concat ", " memOobAna) ^ "\"";
-    enableAnalyses memOobAna
+    enableAnalyses memOobAna;
+    (* Set privatization to mutex-meet-tid *)
+    set_string "ana.base.privatization" "mutex-meet-tid";
+    (* Required for mutex-meet-tid privatization *)
+    GobConfig.set_auto "ana.path_sens[+]" "threadflag";
   | ValidMemtrack
   | ValidMemcleanup -> (* Enable the memLeak analysis *)
     let memLeakAna = ["memLeak"] in

src/maingoblint.ml

@@ -191,10 +191,10 @@ let handle_flags () =
 
 let handle_options () =
   check_arguments ();
-  AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
   if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then
     AutoTune.focusOnMemSafetySpecification ();
+  AfterConfig.run ();
   Cilfacade.init_options ();
   handle_flags ()
 

tests/regression/74-invalid_deref/31-multithreaded.c

@@ -0,0 +1,21 @@
+//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins --set ana.path_sens[+] threadflag  --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.base.arrays.domain partitioned --set ana.base.privatization mutex-meet-tid
+#include <pthread.h>
+
+int data;
+int *p = &data, *q;
+pthread_mutex_t mutex;
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex);
+  *p = 8;
+  pthread_mutex_unlock(&mutex);
+  return ((void *)0);
+}
+int main() {
+  pthread_t id;
+  pthread_create(&id, ((void *)0), t_fun, ((void *)0));
+  q = p;
+  pthread_mutex_lock(&mutex);
+  *q = 8;
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}