Merge pull request #1500 from goblint/priv-nondefinite-mutex

Fix privatization unsoundness due to non-definite and unknown mutexes

src/analyses/apron/relationAnalysis.apron.ml

@@ -682,15 +682,18 @@ struct
     ctx.local
 
   let event ctx e octx =
+    let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
     match e with
-    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr
-    | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      if addr = UnknownPtr then
-        M.info ~category:Unsound "Unknown mutex unlocked, relation privatization unsound"; (* TODO: something more sound *)
+    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
+      CommonPriv.lift_lock ask (fun st m ->
+          Priv.lock ask ctx.global st m
+        ) st addr
+    | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       WideningTokens.with_local_side_tokens (fun () ->
-          Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr
+          CommonPriv.lift_unlock ask (fun st m ->
+              Priv.unlock ask ctx.global ctx.sideg st m
+            ) st addr
         )
     | Events.EnterMultiThreaded ->
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st

src/analyses/base.ml

@@ -3062,12 +3062,14 @@ struct
     match e with
     | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pretty addr;
-      Priv.lock ask (priv_getg ctx.global) st addr
+      CommonPriv.lift_lock ask (fun st m ->
+          Priv.lock ask (priv_getg ctx.global) st m
+        ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      if addr = UnknownPtr then
-        M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *)
       WideningTokens.with_local_side_tokens (fun () ->
-          Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
+          CommonPriv.lift_unlock ask (fun st m ->
+              Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m
+            ) st addr
         )
     | Events.Escape escaped ->
       Priv.escape ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped

src/analyses/commonPriv.ml

@@ -305,3 +305,41 @@ struct
 
   let startstate () = W.bot (), LMust.top (), L.bot ()
 end
+
+
+let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
+  (* Should be in sync with:
+     1. LocksetAnalysis.MakeMust.event
+     2. MutexAnalysis.Spec.Arg.add
+     3. LockDomain.MustLocksetRW.add_mval_rw *)
+  match addr with
+  | UnknownPtr -> st
+  | Addr (v, _) when ask.f (IsMultiple v) -> st
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr _
+  | NullPtr
+  | StrPtr _ -> st
+
+let lift_unlock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
+  (* Should be in sync with:
+     1. LocksetAnalysis.MakeMust.event
+     2. MutexAnalysis.Spec.Arg.remove
+     3. MutexAnalysis.Spec.Arg.remove_all
+     4. LockDomain.MustLocksetRW.remove_mval_rw *)
+  match addr with
+  | UnknownPtr ->
+    LockDomain.MustLockset.fold (fun ml st ->
+        (* call privatization's unlock only with definite lock *)
+        f st (LockDomain.Addr.Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+      ) (ask.f MustLockset) st
+  | StrPtr _
+  | NullPtr -> st
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr mv ->
+    LockDomain.MustLockset.fold (fun ml st ->
+        if LockDomain.MustLock.semantic_equal_mval ml mv = Some false then
+          st
+        else
+          (* call privatization's unlock only with definite lock *)
+          f st (Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+      ) (ask.f MustLockset) st

tests/regression/13-privatized/93-unlock-idx-ambiguous.c

@@ -0,0 +1,27 @@
+// PARAM: --set ana.base.privatization protection --enable ana.sv-comp.functions
+#include <pthread.h>
+#include <goblint.h>
+extern _Bool __VERIFIER_nondet_bool();
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  pthread_mutex_lock(&m[1]); // so we're unlocking a mutex we definitely hold
+  g++;
+  int r = __VERIFIER_nondet_bool();
+  pthread_mutex_unlock(&m[r]); // TODO NOWARN (definitely held either way)
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}

tests/regression/13-privatized/93-unlock-idx-ambiguous.t

@@ -0,0 +1,65 @@
+  $ goblint --set ana.base.privatization protection --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mutex-meet --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization lock --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization write --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mine-nothread --enable ana.sv-comp.functions 93-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (93-unlock-idx-ambiguous.c:14:3-14:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (93-unlock-idx-ambiguous.c:24:3-24:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+

tests/regression/13-privatized/94-unlock-unknown.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.base.privatization protection --enable ana.sv-comp.functions
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  g++;
+  pthread_mutex_t *r; // rand
+  pthread_mutex_unlock(r);
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}

tests/regression/13-privatized/94-unlock-unknown.t

@@ -0,0 +1,70 @@
+  $ goblint --set ana.base.privatization protection --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mutex-meet --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization lock --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization write --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.base.privatization mine-nothread --enable ana.sv-comp.functions 94-unlock-unknown.c
+  [Warning][Unknown] unlocking unknown mutex which may not be held (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Unknown] unlocking NULL mutex (94-unlock-unknown.c:12:3-12:26)
+  [Warning][Assert] Assertion "g == 0" is unknown. (94-unlock-unknown.c:22:3-22:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 11
+    dead: 0
+    total lines: 11
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+

tests/regression/13-privatized/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))

tests/regression/46-apron2/87-unlock-idx-ambiguous.c

@@ -0,0 +1,28 @@
+// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag
+// TODO: why nonterm without threadflag path-sens?
+#include <pthread.h>
+#include <goblint.h>
+extern _Bool __VERIFIER_nondet_bool();
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  pthread_mutex_lock(&m[1]); // so we're unlocking a mutex we definitely hold
+  g++;
+  int r = __VERIFIER_nondet_bool();
+  pthread_mutex_unlock(&m[r]); // TODO NOWARN (definitely held either way)
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}

tests/regression/46-apron2/87-unlock-idx-ambiguous.t

@@ -0,0 +1,39 @@
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+
+  $ goblint --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag 87-unlock-idx-ambiguous.c
+  [Warning][Unknown] unlocking mutex (m[def_exc:Unknown int([0,1])]) which may not be held (87-unlock-idx-ambiguous.c:15:3-15:30)
+  [Warning][Assert] Assertion "g == 0" is unknown. (87-unlock-idx-ambiguous.c:25:3-25:26)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 14
+    dead: 0
+    total lines: 14
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
+

tests/regression/46-apron2/88-unlock-unknown.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --enable ana.sv-comp.functions
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m[2] = {PTHREAD_MUTEX_INITIALIZER, PTHREAD_MUTEX_INITIALIZER};
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&m[0]);
+  g++;
+  pthread_mutex_t *r; // rand
+  pthread_mutex_unlock(r);
+  // could have unlocked m[0], so should have published g there
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_mutex_lock(&m[0]);
+  __goblint_check(g == 0); // UNKNOWN!
+  pthread_mutex_unlock(&m[0]);
+  return 0;
+}