Merge pull request #688 from goblint/klever

Klever concurrency safety support

conf/ldv-races.json

@@ -29,7 +29,9 @@
       "escape",
       "expRelation",
       "mhp",
-      "assert"
+      "assert",
+      "var_eq",
+      "symb_locks"
     ],
     "malloc": {
       "wrappers": [
@@ -52,6 +54,19 @@
       ]
     }
   },
+  "lib": {
+    "activated": [
+      "c",
+      "posix",
+      "pthread",
+      "gcc",
+      "glibc",
+      "linux-userspace",
+      "goblint",
+      "ncurses",
+      "klever"
+    ]
+  },
   "witness": {
     "graphml": {
       "enabled": true,

src/analyses/base.ml

@@ -1953,8 +1953,8 @@ struct
 
 
 
-  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list) list * bool =
-    let create_thread lval arg v =
+  let forkfun (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) (lv: lval option) (f: varinfo) (args: exp list) : (lval option * varinfo * exp list * bool) list =
+    let create_thread ~multiple lval arg v =
       try
         (* try to get function declaration *)
         let fd = Cilfacade.find_varinfo_fundec v in
@@ -1963,7 +1963,7 @@ struct
           | Some x -> [x]
           | None -> List.map (fun x -> MyCFG.unknown_exp) fd.sformals
         in
-        Some (lval, v, args)
+        Some (lval, v, args, multiple)
       with Not_found ->
         if LF.use_special f.vname then None (* we handle this function *)
         else if isFunctionType v.vtype then
@@ -1973,7 +1973,7 @@ struct
             | Some x -> [x]
             | None -> List.map (fun x -> MyCFG.unknown_exp) (Cil.argsToList v_args)
           in
-          Some (lval, v, args)
+          Some (lval, v, args, multiple)
         else (
           M.debug ~category:Analyzer "Not creating a thread from %s because its type is %a" v.vname d_type v.vtype;
           None
@@ -1982,7 +1982,7 @@ struct
     let desc = LF.find f in
     match desc.special args, f.vname with
     (* handling thread creations *)
-    | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg }, _ -> begin
+    | ThreadCreate { thread = id; start_routine = start; arg = ptc_arg; multiple }, _ -> begin
         (* extra sync so that we do not analyze new threads with bottom global invariant *)
         publish_all ctx `Thread;
         (* Collect the threads. *)
@@ -1994,7 +1994,7 @@ struct
           else
             start_funvars
         in
-        List.filter_map (create_thread (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown, false
+        List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
@@ -2008,8 +2008,8 @@ struct
       let flist = shallow_flist @ deep_flist in
       let addrs = List.concat_map AD.to_var_may flist in
       if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
-      List.filter_map (create_thread None None) addrs, true
-    | _, _ -> [], false
+      List.filter_map (create_thread ~multiple:true None None) addrs
+    | _, _ -> []
 
   let assert_fn ctx e refine =
     (* make the state meet the assertion in the rest of the code *)
@@ -2140,9 +2140,9 @@ struct
       let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
       (addr, AD.type_of addr)
     in
-    let forks, multiple = forkfun ctx lv f args in
-    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple3.second forks);
-    List.iter (BatTuple.Tuple3.uncurry (ctx.spawn ~multiple)) forks;
+    let forks = forkfun ctx lv f args in
+    if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks);
+    List.iter (fun (lval, f, args, multiple) -> ctx.spawn ~multiple lval f args) forks;
     let st: store = ctx.local in
     let gs = ctx.global in
     let desc = LF.find f in

src/config/options.schema.json

@@ -1313,6 +1313,7 @@
               "linux-kernel",
               "goblint",
               "sv-comp",
+              "klever",
               "ncurses",
               "zstd",
               "pcre",

src/util/library/libraryDesc.ml

@@ -53,7 +53,7 @@ type special =
   | Assert of { exp: Cil.exp; check: bool; refine: bool; }
   | Lock of { lock: Cil.exp; try_: bool; write: bool; return_on_success: bool; }
   | Unlock of Cil.exp
-  | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
+  | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
   | Signal of Cil.exp

src/util/library/libraryFunctions.ml

@@ -436,7 +436,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 
 (** Pthread functions. *)
 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_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* 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_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
     ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
@@ -1019,6 +1019,21 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *)
   ]
 
+let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock]" intType)))
+
+(** LDV Klever functions. *)
+let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = true });
+    ("pthread_join_N", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
+    ("ldv_mutex_model_lock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true });
+    ("ldv_mutex_model_unlock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Unlock lock);
+    ("ldv_spin_model_lock", unknown [drop "sign" []]);
+    ("ldv_spin_model_unlock", unknown [drop "sign" []]);
+    ("rtnl_lock", special [] @@ Lock { lock = rtnl_lock; try_ = false; write = true; return_on_success = true });
+    ("rtnl_unlock", special [] @@ Unlock rtnl_lock);
+    ("__rtnl_unlock", special [] @@ Unlock rtnl_lock);
+  ]
+
 let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("echo", unknown []);
     ("noecho", unknown []);
@@ -1104,6 +1119,7 @@ let libraries = Hashtbl.of_list [
     ("linux-kernel", linux_kernel_descs_list);
     ("goblint", goblint_descs_list);
     ("sv-comp", svcomp_descs_list);
+    ("klever", klever_descs_list);
     ("ncurses", ncurses_descs_list);
     ("zstd", zstd_descs_list);
     ("pcre", pcre_descs_list);

tests/regression/51-threadjoins/08-klever-multiple.c

@@ -0,0 +1,24 @@
+//PARAM: --set ana.activated[+] threadJoins --set lib.activated[+] klever
+#include <pthread.h>
+#include <goblint.h>
+
+int g = 0;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create_N(&id, NULL, t_fun, NULL); // spawns multiple threads
+  pthread_join(id, NULL);
+
+  g++; // RACE!
+
+  pthread_join_N(id, NULL); // TODO: should this join one (do nothing) or all (like assume join)?
+
+  g++; // RACE!
+
+  return 0;
+}

unittest/analyses/libraryDslTest.ml

@@ -11,7 +11,7 @@ let pthread_mutex_lock_desc: LibraryDesc.t = LibraryDsl.(
   )
 
 let pthread_create_desc: LibraryDesc.t = LibraryDsl.(
-    special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [r]; __ "arg" [r]] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }
+    special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [r]; __ "arg" [r]] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }
   )
 
 let realloc_desc: LibraryDesc.t = LibraryDsl.(