From d754d76fd0912b78e495cab0eb2fa73405c00952 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Apr 2022 14:19:21 +0000 Subject: [PATCH 1/7] Add direct Klever concurrency specials --- src/analyses/libraryFunctions.ml | 5 ++++- src/analyses/mutexEventsAnalysis.ml | 6 ++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 0c00391dcb..ce89391691 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -24,7 +24,8 @@ let classify' fn exps = `Unknown fn in match fn with - | "pthread_create" -> + | "pthread_create" + | "pthread_create_N" -> (* Klever *) begin match exps with | [id;_;fn;x] -> `ThreadCreate (id, fn, x) | _ -> strange_arguments () @@ -72,6 +73,7 @@ let classify' fn exps = | "pthread_rwlock_wrlock" | "GetResource" | "_raw_spin_lock" | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh" | "spin_lock_irqsave" | "spin_lock" + | "ldv_mutex_model_lock" | "ldv_spin_model_lock" (* Klever *) -> `Lock (get_bool "sem.lock.fail", true, true) | "pthread_mutex_lock" | "__pthread_mutex_lock" -> `Lock (get_bool "sem.lock.fail", true, false) @@ -84,6 +86,7 @@ let classify' fn exps = | "mutex_unlock" | "ReleaseResource" | "_write_unlock" | "_read_unlock" | "_raw_spin_unlock_irqrestore" | "pthread_mutex_unlock" | "__pthread_mutex_unlock" | "spin_unlock_irqrestore" | "up_read" | "up_write" | "up" + | "ldv_mutex_model_unlock" | "ldv_spin_model_unlock" (* Klever *) -> `Unlock | x -> `Unknown x diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 4a3ef078ce..050b8de600 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -77,7 +77,8 @@ struct let unlock remove_fn = match f.vname, arglist with | _, [arg] - | ("spin_unlock_irqrestore" | "_raw_spin_unlock_irqrestore"), [arg; _] -> + | ("spin_unlock_irqrestore" | "_raw_spin_unlock_irqrestore"), [arg; _] + | "ldv_mutex_model_unlock", [arg; _] -> (* Klever *) List.iter (fun e -> ctx.split () [Events.Unlock (remove_fn e)] ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg); @@ -92,7 +93,8 @@ struct | `Lock (failing, rw, nonzero_return_when_aquired), _ -> begin match f.vname, arglist with | _, [arg] - | "spin_lock_irqsave", [arg; _] -> + | "spin_lock_irqsave", [arg; _] + | "ldv_mutex_model_lock", [arg; _] -> (* Klever *) (*print_endline @@ "Mutex `Lock "^f.vname;*) lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arg | _ -> failwith "lock has multiple arguments" From 8f3160943db3dc36a622b0914242a3fa496a2978 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Apr 2022 14:20:08 +0000 Subject: [PATCH 2/7] Add special rtnl_lock from Linux --- src/analyses/mutexEventsAnalysis.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 050b8de600..a7448af4f4 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -11,6 +11,7 @@ open GobConfig let big_kernel_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType)) let console_sem = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType)) +let rtnl_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[rtnl_lock]" intType)) let verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType)) module Spec: MCPSpec = @@ -118,10 +119,14 @@ struct (*print_endline @@ "Mutex `Unlock "^f.vname;*) unlock remove_rw | _, "spinlock_check" -> () - | _, "acquire_console_sem" when get_bool "kernel" -> + | _, "acquire_console_sem"-> (* TODO: removed for Klever: when get_bool "kernel" *) ctx.emit (Events.Lock (console_sem, true)) - | _, "release_console_sem" when get_bool "kernel" -> + | _, "release_console_sem" -> (* TODO: removed for Klever: when get_bool "kernel" *) ctx.emit (Events.Unlock console_sem) + | _, "rtnl_lock"-> + ctx.emit (Events.Lock (rtnl_lock, true)) + | _, ("rtnl_unlock" | "__rtnl_unlock") -> + ctx.emit (Events.Unlock rtnl_lock) | _, "__builtin_prefetch" | _, "misc_deregister" -> () | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> From 1fbf9105c125d1bf4903d43ea477cd88cbb0df6b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 13 Apr 2022 14:20:19 +0000 Subject: [PATCH 3/7] Add symb_locks to ldv-races conf --- conf/ldv-races.json | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/conf/ldv-races.json b/conf/ldv-races.json index 2414413de4..2b30576e1b 100644 --- a/conf/ldv-races.json +++ b/conf/ldv-races.json @@ -27,7 +27,9 @@ "access", "escape", "expRelation", - "mhp" + "mhp", + "var_eq", + "symb_locks" ], "malloc": { "wrappers": [ From 717b6a85cb99521936a1d7e3b5c952dcfafb43af Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 27 Nov 2023 12:18:53 +0200 Subject: [PATCH 4/7] Add pthread_join_N to Klever library --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c9afb83617..b94f751568 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1008,6 +1008,7 @@ let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock (** 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 }); (* TODO: add multiple flag to ThreadCreate *) + ("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" []]); From 670e7cfe1665a527ce1c124bad8494e30d452bd4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 27 Nov 2023 12:23:06 +0200 Subject: [PATCH 5/7] Add test for Klever's multiple threads --- .../51-threadjoins/07-klever-multiple.c | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/regression/51-threadjoins/07-klever-multiple.c diff --git a/tests/regression/51-threadjoins/07-klever-multiple.c b/tests/regression/51-threadjoins/07-klever-multiple.c new file mode 100644 index 0000000000..24b2c0b1ca --- /dev/null +++ b/tests/regression/51-threadjoins/07-klever-multiple.c @@ -0,0 +1,24 @@ +//PARAM: --set ana.activated[+] threadJoins --set lib.activated[+] klever +#include +#include + +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; +} From 8a95c8a2d4fa776624da179a803c021058563577 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 27 Nov 2023 12:29:07 +0200 Subject: [PATCH 6/7] Add multiple flag to ThreadCreate --- src/analyses/base.ml | 22 +++++++++++----------- src/analyses/libraryDesc.ml | 2 +- src/analyses/libraryFunctions.ml | 4 ++-- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index bdae887b4a..3630395282 100644 --- a/src/analyses/base.ml +++ b/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 diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 4997b306a9..e426c32235 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/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 diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index b94f751568..ab0d04d3ec 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -422,7 +422,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" []]); @@ -1007,7 +1007,7 @@ let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock (** 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 }); (* TODO: add multiple flag to ThreadCreate *) + ("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); From 5a6362e1c0bda3ad0feb3332bf64e95fcea810b8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 27 Nov 2023 14:32:47 +0200 Subject: [PATCH 7/7] Fix LibraryDslTest compilation --- unittest/analyses/libraryDslTest.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/unittest/analyses/libraryDslTest.ml b/unittest/analyses/libraryDslTest.ml index e1fa23281c..077b81b8fa 100644 --- a/unittest/analyses/libraryDslTest.ml +++ b/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.(