Merge pull request #520 from goblint/signals

Analysis of `pthread_cond`

Author: michael-schwarz

src/analyses/accessAnalysis.ml

@@ -203,8 +203,8 @@ struct
       ctx.local
     | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" ->
       ctx.local
-    | _, "pthread_cond_wait"
-    | _, "pthread_cond_timedwait" ->
+    | Wait _ , _
+    | TimedWait _, _ ->
       ctx.local
     | _, _ ->
       LibraryDesc.Accesses.iter desc.accs (fun {kind; deep = reach} exp ->

src/analyses/extractPthread.ml

@@ -1228,15 +1228,15 @@ module Spec : Analyses.MCPSpec = struct
         add_actions
         @@ List.map (fun id -> Action.CondVarInit id)
         @@ ExprEval.eval_ptr_id ctx cond_var Tbls.CondVarIdTbl.get
-      | Unknown, "pthread_cond_broadcast", [ cond_var ] ->
+      | Broadcast cond_var, _, _ ->
         add_actions
         @@ List.map (fun id -> Action.CondVarBroadcast id)
         @@ ExprEval.eval_ptr_id ctx cond_var Tbls.CondVarIdTbl.get
-      | Unknown, "pthread_cond_signal", [ cond_var ] ->
+      | Signal cond_var, _, _ ->
         add_actions
         @@ List.map (fun id -> Action.CondVarSignal id)
         @@ ExprEval.eval_ptr_id ctx cond_var Tbls.CondVarIdTbl.get
-      | Unknown, "pthread_cond_wait", [ cond_var; mutex ] ->
+      | Wait {cond = cond_var; mutex = mutex}, _, _ ->
         let cond_vars = ExprEval.eval_ptr ctx cond_var in
         let mutex_vars = ExprEval.eval_ptr ctx mutex in
         let cond_var_action (v, m) =

src/analyses/libraryDesc.ml

@@ -41,6 +41,10 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | Signal of Cil.exp
+  | Broadcast of Cil.exp
+  | Wait of { cond: Cil.exp; mutex: Cil.exp; }
+  | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; }
   | Math of { fun_args: math; }
   | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
   | Bzero of { dest: Cil.exp; count: Cil.exp; }

src/analyses/libraryFunctions.ml

@@ -30,6 +30,10 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
+    ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond);
+    ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond);
+    ("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex});
+    ("pthread_cond_timedwait", special [__ "cond" []; __ "mutex" []; __ "abstime" [r]] @@ fun cond mutex abstime -> TimedWait {cond; mutex; abstime});
   ]
 
 (** GCC builtin functions.

src/analyses/mHPAnalysis.ml

@@ -14,12 +14,7 @@ struct
     let should_print _ = true
   end
 
-  let access ctx _: MHP.t =
-    {
-      tid = ctx.ask CurrentThreadId;
-      created = ctx.ask CreatedThreads;
-      must_joined = ctx.ask MustJoinedThreads
-    }
+  let access ctx _: MHP.t = MHP.current (Analyses.ask_of_ctx ctx)
 end
 
 let _ =

src/analyses/mutexEventsAnalysis.ml

@@ -116,6 +116,17 @@ struct
     | Unlock _, _ ->
       (*print_endline @@ "Mutex `Unlock "^f.vname;*)
       unlock remove_rw
+    | Wait {cond = cond; mutex = mutex}, _
+    | TimedWait {cond = cond; mutex = mutex; _}, _ ->
+      (* mutex is unlocked while waiting but relocked when returns *)
+      (* emit unlock-lock events for privatization *)
+      let ms = eval_exp_addr (Analyses.ask_of_ctx ctx) mutex in
+      List.iter (fun m ->
+          (* unlock-lock each possible mutex as a split to be dependent *)
+          (* otherwise may-point-to {a, b} might unlock a, but relock b *)
+          ctx.split () [Events.Unlock m; Events.Lock (m, true)];
+        ) ms;
+      raise Deadcode (* splits cover all cases *)
     | _, "spinlock_check" -> ()
     | _, "acquire_console_sem" when get_bool "kernel" ->
       ctx.emit (Events.Lock (console_sem, true))
@@ -127,18 +138,6 @@ struct
       ctx.emit (Events.Lock (verifier_atomic, true))
     | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" ->
       ctx.emit (Events.Unlock verifier_atomic)
-    | _, "pthread_cond_wait"
-    | _, "pthread_cond_timedwait" ->
-      (* mutex is unlocked while waiting but relocked when returns *)
-      (* emit unlock-lock events for privatization *)
-      let m_arg = List.nth arglist 1 in
-      let ms = eval_exp_addr (Analyses.ask_of_ctx ctx) m_arg in
-      List.iter (fun m ->
-          (* unlock-lock each possible mutex as a split to be dependent *)
-          (* otherwise may-point-to {a, b} might unlock a, but relock b *)
-          ctx.split () [Events.Unlock m; Events.Lock (m, true)];
-        ) ms;
-      raise Deadcode (* splits cover all cases *)
     | _, x ->
       ()
 

src/analyses/pthreadSignals.ml

@@ -0,0 +1,113 @@
+(** Analysis of must-received pthread_signals. *)
+
+open Prelude.Ana
+open Analyses
+module LF = LibraryFunctions
+
+module Spec : Analyses.MCPSpec =
+struct
+  module Signals = SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All signals" end)
+  module MustSignals = Lattice.Reverse (Signals)
+
+  include Analyses.DefaultSpec
+  module V = VarinfoV
+
+  let name () = "pthreadSignals"
+  module D = MustSignals
+  module C = MustSignals
+  module G = SetDomain.ToppedSet (MHP) (struct let topname = "All Threads" end)
+
+  let rec conv_offset x =
+    match x with
+    | `NoOffset    -> `NoOffset
+    | `Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
+    | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
+    | `Field (f,o) -> `Field (f, conv_offset o)
+
+  let eval_exp_addr (a: Queries.ask) exp =
+    let gather_addr (v,o) b = ValueDomain.Addr.from_var_offset (v,conv_offset o) :: b in
+    match a.f (Queries.MayPointTo exp) with
+    | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar,`NoOffset) a) ->
+      Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
+    | _ -> []
+
+  let possible_vinfos a cv_arg =
+    List.filter_map ValueDomain.Addr.to_var_may (eval_exp_addr a cv_arg)
+
+  (* transfer functions *)
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    ctx.local
+
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    ctx.local
+
+  let body ctx (f:fundec) : D.t =
+    ctx.local
+
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    ctx.local
+
+  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [ctx.local, ctx.local]
+
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
+    au
+
+  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let desc = LF.find f in
+    match desc.special arglist with
+    | Signal cond
+    | Broadcast cond ->
+      let mhp = G.singleton @@ MHP.current (Analyses.ask_of_ctx ctx) in
+      let publish_one a = ctx.sideg a mhp in
+      let possible_vars = possible_vinfos (Analyses.ask_of_ctx ctx) cond in
+      List.iter publish_one possible_vars;
+      ctx.local
+    | Wait {cond = cond; _} ->
+      let current_mhp = MHP.current (Analyses.ask_of_ctx ctx) in
+      let module Signalled = struct
+        type signalled = Never | NotConcurrently | PossiblySignalled
+
+        let (|||) a b = match a,b with
+          | PossiblySignalled, _
+          | _, PossiblySignalled -> PossiblySignalled
+          | NotConcurrently , _
+          | _, NotConcurrently -> NotConcurrently
+          | Never, Never -> Never
+
+        let can_be_signalled a =
+          let signalling_tids = ctx.global a in
+          if G.is_top signalling_tids then
+            PossiblySignalled
+          else if G.is_empty signalling_tids then
+            Never
+          else if not @@ G.exists (MHP.may_happen_in_parallel current_mhp) signalling_tids then
+            NotConcurrently
+          else
+            PossiblySignalled
+      end
+      in
+      let open Signalled in
+      let add_if_singleton conds = match conds with | [a] -> Signals.add (ValueDomain.Addr.from_var a) ctx.local | _ -> ctx.local in
+      let conds = possible_vinfos (Analyses.ask_of_ctx ctx) cond in
+      (match List.fold_left (fun acc cond -> can_be_signalled cond ||| acc) Never conds with
+       | PossiblySignalled -> add_if_singleton conds
+       | NotConcurrently ->
+         (M.warn ~category:Deadcode "The condition variable(s) pointed to by %a are never signalled concurrently, succeeding code is live due to spurious wakeups only!" Basetype.CilExp.pretty cond; ctx.local)
+       | Never ->
+         (M.warn ~category:Deadcode "The condition variable(s) pointed to by %a are never signalled, succeeding code is live due to spurious wakeups only!" Basetype.CilExp.pretty cond; ctx.local)
+      )
+
+    | TimedWait _ ->
+      (* Time could simply have elapsed *)
+      ctx.local
+    | _ -> ctx.local
+
+  let startstate v = Signals.empty ()
+  let threadenter ctx lval f args = [ctx.local]
+  let threadspawn ctx lval f args fctx = ctx.local
+  let exitstate  v = Signals.empty ()
+end
+
+let _ =
+  MCP.register_analysis ~dep:["mutex"] (module Spec : MCPSpec)

src/cdomains/mHP.ml

@@ -9,6 +9,13 @@ type t = {
   must_joined: ConcDomain.ThreadSet.t;
 } [@@deriving eq, ord, hash]
 
+let current (ask:Queries.ask) =
+  {
+    tid = ask.f Queries.CurrentThreadId;
+    created = ask.f Queries.CreatedThreads;
+    must_joined = ask.f Queries.MustJoinedThreads
+  }
+
 let pretty () {tid; created; must_joined} =
   let tid_doc = Some (Pretty.dprintf "tid=%a" ThreadIdDomain.ThreadLifted.pretty tid) in
   (* avoid useless empty sets in race output *)

tests/regression/59-signals/01-simple.c

@@ -0,0 +1,43 @@
+// PARAM: --set ana.activated[+] 'pthreadSignals'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+pthread_cond_t cond = PTHREAD_COND_INITIALIZER;
+
+void* f1(void* ptr) {
+    int top;
+    pthread_mutex_lock(&mut);
+    g = 1;
+    if(top) {
+        pthread_cond_wait(&cond,&mut); //NOWARN
+    }
+    pthread_mutex_unlock(&mut);
+    return NULL;
+}
+
+void* f2(void* ptr) {
+    pthread_mutex_lock(&mut);
+    pthread_cond_signal(&cond);
+    pthread_mutex_unlock(&mut);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+    sleep(1);
+    pthread_create(&t2,NULL,f2,NULL);
+
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+
+    return 0;
+}

tests/regression/59-signals/02-unsignaled.c

@@ -0,0 +1,30 @@
+// PARAM: --set ana.activated[+] 'pthreadSignals'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+
+pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+pthread_cond_t cond = PTHREAD_COND_INITIALIZER;
+
+void* f1(void* ptr) {
+    int top;
+    pthread_mutex_lock(&mut);
+    int res = 0;
+    pthread_cond_wait(&cond,&mut); //WARN
+    assert(res == 0);
+    pthread_mutex_unlock(&mut);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    pthread_create(&t1,NULL,f1,NULL);
+
+    return 0;
+}