From 427dfd219104d9ad98254e459314915394c38522 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 13:20:40 +0200 Subject: [PATCH 01/43] Extract mutexEvents analysis from mutex --- src/analyses/mutexEventsAnalysis.ml | 202 +++++++++++++++++++++++++ src/analyses/tutorials/unitAnalysis.ml | 2 +- 2 files changed, 203 insertions(+), 1 deletion(-) create mode 100644 src/analyses/mutexEventsAnalysis.ml diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml new file mode 100644 index 0000000000..fe7b40ee13 --- /dev/null +++ b/src/analyses/mutexEventsAnalysis.ml @@ -0,0 +1,202 @@ +(** Mutex analysis. *) + +module M = Messages +module Addr = ValueDomain.Addr +module Lockset = LockDomain.Lockset +module Mutexes = LockDomain.Mutexes +module LF = LibraryFunctions +open Prelude.Ana +open Analyses +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 verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType)) + +module Spec: MCPSpec = +struct + include UnitAnalysis.Spec + let name () = "mutexEvents" + + + (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain + element) answers with the string "unknown" on all non-concrete cases. *) + 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 rec conv_offset_inv = function + | `NoOffset -> `NoOffset + | `Field (f, o) -> `Field (f, conv_offset_inv o) + (* TODO: better indices handling *) + | `Index (_, o) -> `Index (MyCFG.unknown_exp, conv_offset_inv 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 lock ctx rw may_fail nonzero_return_when_aquired a lv arglist (ls: unit) = + let is_a_blob addr = + match LockDomain.Addr.to_var addr with + | Some a -> a.vname.[0] = '(' + | None -> false + in + let lock_one (e:LockDomain.Addr.t) = + if is_a_blob e then + ls + else begin + (* let nls = Lockset.add (e,rw) ls in *) + let nls = ls in + (* let changed = Lockset.compare ls nls <> 0 in *) + let changed = true in + match lv with + | None -> + if may_fail then + ls + else ( + (* If the lockset did not change, do not emit Lock event *) + if changed then ctx.emit (Events.Lock e); + nls + ) + | Some lv -> + let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in + if changed then + ctx.split nls [sb; Events.Lock e] + else + ctx.split nls [sb]; + if may_fail then ( + let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in + ctx.split ls [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] + ); + raise Analyses.Deadcode + end + in + match arglist with + | [x] -> begin match (eval_exp_addr a x) with + | [e] -> lock_one e + | _ -> ls + end + | _ -> + (* Lockset.top () *) + () + + + + let return ctx exp fundec : D.t = + (* deprecated but still valid SV-COMP convention for atomic block *) + if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then ( + ctx.emit (Events.Unlock verifier_atomic); + (* Lockset.remove (verifier_atomic, true) ctx.local *) + ctx.local + ) + else + ctx.local + + let body ctx f : D.t = + (* deprecated but still valid SV-COMP convention for atomic block *) + if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then ( + ctx.emit (Events.Lock verifier_atomic); + (* Lockset.add (verifier_atomic, true) ctx.local *) + ctx.local + ) + else + ctx.local + + let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = + let remove_rw x st = + ctx.emit (Events.Unlock x); + (* Lockset.remove (x,true) (Lockset.remove (x,false) st) *) + st + in + let unlock remove_fn = + let remove_nonspecial x = + (* if Lockset.is_top x then x else + Lockset.filter (fun (v,_) -> match LockDomain.Addr.to_var v with + | Some v when v.vname.[0] = '{' -> true + | _ -> false + ) x *) + () + in + match arglist with + | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with + | [] -> remove_nonspecial ctx.local + | es -> List.fold_right remove_fn es ctx.local + end + | _ -> ctx.local + in + match (LF.classify f.vname arglist, f.vname) with + | _, "_lock_kernel" -> + ctx.emit (Events.Lock big_kernel_lock); + (* Lockset.add (big_kernel_lock,true) ctx.local *) + ctx.local + | _, "_unlock_kernel" -> + ctx.emit (Events.Unlock big_kernel_lock); + (* Lockset.remove (big_kernel_lock,true) ctx.local *) + ctx.local + | `Lock (failing, rw, nonzero_return_when_aquired), _ + -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in + (*print_endline @@ "Mutex `Lock "^f.vname;*) + lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arglist ctx.local + | `Unlock, "__raw_read_unlock" + | `Unlock, "__raw_write_unlock" -> + let drop_raw_lock x = + let rec drop_offs o = + match o with + | `Field ({fname="raw_lock"; _},`NoOffset) -> `NoOffset + | `Field (f1,o1) -> `Field (f1, drop_offs o1) + | `Index (i1,o1) -> `Index (i1, drop_offs o1) + | `NoOffset -> `NoOffset + in + match Addr.to_var_offset x with + | Some (v,o) -> Addr.from_var_offset (v, drop_offs o) + | None -> x + in + unlock (fun l -> remove_rw (drop_raw_lock l)) + | `Unlock, _ -> + (*print_endline @@ "Mutex `Unlock "^f.vname;*) + unlock remove_rw + | _, "spinlock_check" -> ctx.local + | _, "acquire_console_sem" when get_bool "kernel" -> + ctx.emit (Events.Lock console_sem); + (* Lockset.add (console_sem,true) ctx.local *) + ctx.local + | _, "release_console_sem" when get_bool "kernel" -> + ctx.emit (Events.Unlock console_sem); + (* Lockset.remove (console_sem,true) ctx.local *) + ctx.local + | _, "__builtin_prefetch" | _, "misc_deregister" -> + ctx.local + | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> + ctx.emit (Events.Lock verifier_atomic); + (* Lockset.add (verifier_atomic, true) ctx.local *) + ctx.local + | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" -> + ctx.emit (Events.Unlock verifier_atomic); + (* Lockset.remove (verifier_atomic, true) ctx.local *) + ctx.local + | _, "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 ctx.local [Events.Unlock m; Events.Lock m]; + ) ms; + raise Deadcode (* splits cover all cases *) + | _, x -> + ctx.local + +end + +let _ = + MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml index 5d1cf1825f..30223b7c61 100644 --- a/src/analyses/tutorials/unitAnalysis.ml +++ b/src/analyses/tutorials/unitAnalysis.ml @@ -3,7 +3,7 @@ open Prelude.Ana open Analyses -module Spec : Analyses.MCPSpec = +module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Lattice.Unit = struct include Analyses.DefaultSpec From f7d1ec114307cd613a870e8448f2f1933548ee54 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 13:26:57 +0200 Subject: [PATCH 02/43] Add Lock2/Unlock2 events with write flag --- src/analyses/mutexEventsAnalysis.ml | 25 +++++++++++++------------ src/domains/events.ml | 4 ++++ 2 files changed, 17 insertions(+), 12 deletions(-) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index fe7b40ee13..6fcb3ccad8 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -62,13 +62,13 @@ struct ls else ( (* If the lockset did not change, do not emit Lock event *) - if changed then ctx.emit (Events.Lock e); + if changed then ctx.emit (Events.Lock2 (e, rw)); nls ) | Some lv -> let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in if changed then - ctx.split nls [sb; Events.Lock e] + ctx.split nls [sb; Events.Lock2 (e, rw)] else ctx.split nls [sb]; if may_fail then ( @@ -92,7 +92,7 @@ struct let return ctx exp fundec : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then ( - ctx.emit (Events.Unlock verifier_atomic); + ctx.emit (Events.Unlock2 (verifier_atomic, true)); (* Lockset.remove (verifier_atomic, true) ctx.local *) ctx.local ) @@ -102,7 +102,7 @@ struct let body ctx f : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then ( - ctx.emit (Events.Lock verifier_atomic); + ctx.emit (Events.Lock2 (verifier_atomic, true)); (* Lockset.add (verifier_atomic, true) ctx.local *) ctx.local ) @@ -111,7 +111,8 @@ struct let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = let remove_rw x st = - ctx.emit (Events.Unlock x); + ctx.emit (Events.Unlock2 (x, true)); + ctx.emit (Events.Unlock2 (x, false)); (* Lockset.remove (x,true) (Lockset.remove (x,false) st) *) st in @@ -133,11 +134,11 @@ struct in match (LF.classify f.vname arglist, f.vname) with | _, "_lock_kernel" -> - ctx.emit (Events.Lock big_kernel_lock); + ctx.emit (Events.Lock2 (big_kernel_lock, true)); (* Lockset.add (big_kernel_lock,true) ctx.local *) ctx.local | _, "_unlock_kernel" -> - ctx.emit (Events.Unlock big_kernel_lock); + ctx.emit (Events.Unlock2 (big_kernel_lock, true)); (* Lockset.remove (big_kernel_lock,true) ctx.local *) ctx.local | `Lock (failing, rw, nonzero_return_when_aquired), _ @@ -164,21 +165,21 @@ struct unlock remove_rw | _, "spinlock_check" -> ctx.local | _, "acquire_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Lock console_sem); + ctx.emit (Events.Lock2 (console_sem, true)); (* Lockset.add (console_sem,true) ctx.local *) ctx.local | _, "release_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Unlock console_sem); + ctx.emit (Events.Unlock2 (console_sem, true)); (* Lockset.remove (console_sem,true) ctx.local *) ctx.local | _, "__builtin_prefetch" | _, "misc_deregister" -> ctx.local | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Lock verifier_atomic); + ctx.emit (Events.Lock2 (verifier_atomic, true)); (* Lockset.add (verifier_atomic, true) ctx.local *) ctx.local | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Unlock verifier_atomic); + ctx.emit (Events.Unlock2 (verifier_atomic, true)); (* Lockset.remove (verifier_atomic, true) ctx.local *) ctx.local | _, "pthread_cond_wait" @@ -190,7 +191,7 @@ struct 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 ctx.local [Events.Unlock m; Events.Lock m]; + ctx.split ctx.local [Events.Unlock2 (m, true); Events.Lock2 (m, true)]; ) ms; raise Deadcode (* splits cover all cases *) | _, x -> diff --git a/src/domains/events.ml b/src/domains/events.ml index e62ac8bef9..b151c8d9d2 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -3,6 +3,8 @@ open Prelude.Ana type t = | Lock of LockDomain.Addr.t (** This is only emitted if the mutex was not previously held *) | Unlock of LockDomain.Addr.t + | Lock2 of LockDomain.Lockset.Lock.t + | Unlock2 of LockDomain.Lockset.Lock.t | Escape of EscapeDomain.EscapedVars.t | EnterMultiThreaded | SplitBranch of exp * bool (** Used to simulate old branch-based split. *) @@ -13,6 +15,8 @@ type t = let pretty () = function | Lock m -> dprintf "Lock %a" LockDomain.Addr.pretty m | Unlock m -> dprintf "Unock %a" LockDomain.Addr.pretty m + | Lock2 m -> dprintf "Lock2 %a" LockDomain.Lockset.Lock.pretty m + | Unlock2 m -> dprintf "Unock2 %a" LockDomain.Lockset.Lock.pretty m | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped | EnterMultiThreaded -> text "EnterMultiThreaded" | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv From dc878fc068c41946f83c2ac35a3904d88cdc117f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 14:59:40 +0200 Subject: [PATCH 03/43] Make mutex analysis depend on mutexEvents --- src/analyses/mutexAnalysis.ml | 162 ++---------------- src/util/options.schema.json | 2 +- tests/regression/02-base/06-side_effect1.c | 2 +- tests/regression/02-base/07-side_effect2.c | 2 +- tests/regression/02-base/09-ambigpointer.c | 2 +- tests/regression/02-base/10-init_allfuns.c | 2 +- tests/regression/02-base/23-malloc_globmt.c | 2 +- tests/regression/02-base/30-escape_sound.c | 2 +- tests/regression/02-base/41-calloc_globmt.c | 2 +- .../03-practical/14-call_by_pointer.c | 2 +- 10 files changed, 21 insertions(+), 159 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 21bc76686b..af2515ab8e 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -38,15 +38,6 @@ struct let should_join x y = D.equal x y - (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain - element) answers with the string "unknown" on all non-concrete cases. *) - 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 rec conv_offset_inv = function | `NoOffset -> `NoOffset | `Field (f, o) -> `Field (f, conv_offset_inv o) @@ -54,55 +45,6 @@ struct | `Index (_, o) -> `Index (MyCFG.unknown_exp, conv_offset_inv 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 lock ctx rw may_fail nonzero_return_when_aquired a lv arglist ls = - let is_a_blob addr = - match LockDomain.Addr.to_var addr with - | Some a -> a.vname.[0] = '(' - | None -> false - in - let lock_one (e:LockDomain.Addr.t) = - if is_a_blob e then - ls - else begin - let nls = Lockset.add (e,rw) ls in - let changed = Lockset.compare ls nls <> 0 in - match lv with - | None -> - if may_fail then - ls - else ( - (* If the lockset did not change, do not emit Lock event *) - if changed then ctx.emit (Events.Lock e); - nls - ) - | Some lv -> - let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in - if changed then - ctx.split nls [sb; Events.Lock e] - else - ctx.split nls [sb]; - if may_fail then ( - let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in - ctx.split ls [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] - ); - raise Analyses.Deadcode - end - in - match arglist with - | [x] -> begin match (eval_exp_addr a x) with - | [e] -> lock_one e - | _ -> ls - end - | _ -> Lockset.top () - (** We just lift start state, global and dependency functions: *) let startstate v = Lockset.empty () @@ -179,101 +121,13 @@ struct ctx.local let return ctx exp fundec : D.t = - (* deprecated but still valid SV-COMP convention for atomic block *) - if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then ( - ctx.emit (Events.Unlock verifier_atomic); - Lockset.remove (verifier_atomic, true) ctx.local - ) - else - ctx.local + ctx.local let body ctx f : D.t = - (* deprecated but still valid SV-COMP convention for atomic block *) - if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then ( - ctx.emit (Events.Lock verifier_atomic); - Lockset.add (verifier_atomic, true) ctx.local - ) - else - ctx.local + ctx.local let special ctx lv f arglist : D.t = - let remove_rw x st = - ctx.emit (Events.Unlock x); - Lockset.remove (x,true) (Lockset.remove (x,false) st) - in - let unlock remove_fn = - let remove_nonspecial x = - if Lockset.is_top x then x else - Lockset.filter (fun (v,_) -> match LockDomain.Addr.to_var v with - | Some v when v.vname.[0] = '{' -> true - | _ -> false - ) x - in - match arglist with - | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with - | [] -> remove_nonspecial ctx.local - | es -> List.fold_right remove_fn es ctx.local - end - | _ -> ctx.local - in - match (LF.classify f.vname arglist, f.vname) with - | _, "_lock_kernel" -> - ctx.emit (Events.Lock big_kernel_lock); - Lockset.add (big_kernel_lock,true) ctx.local - | _, "_unlock_kernel" -> - ctx.emit (Events.Unlock big_kernel_lock); - Lockset.remove (big_kernel_lock,true) ctx.local - | `Lock (failing, rw, nonzero_return_when_aquired), _ - -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in - (*print_endline @@ "Mutex `Lock "^f.vname;*) - lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arglist ctx.local - | `Unlock, "__raw_read_unlock" - | `Unlock, "__raw_write_unlock" -> - let drop_raw_lock x = - let rec drop_offs o = - match o with - | `Field ({fname="raw_lock"; _},`NoOffset) -> `NoOffset - | `Field (f1,o1) -> `Field (f1, drop_offs o1) - | `Index (i1,o1) -> `Index (i1, drop_offs o1) - | `NoOffset -> `NoOffset - in - match Addr.to_var_offset x with - | Some (v,o) -> Addr.from_var_offset (v, drop_offs o) - | None -> x - in - unlock (fun l -> remove_rw (drop_raw_lock l)) - | `Unlock, _ -> - (*print_endline @@ "Mutex `Unlock "^f.vname;*) - unlock remove_rw - | _, "spinlock_check" -> ctx.local - | _, "acquire_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Lock console_sem); - Lockset.add (console_sem,true) ctx.local - | _, "release_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Unlock console_sem); - Lockset.remove (console_sem,true) ctx.local - | _, "__builtin_prefetch" | _, "misc_deregister" -> - ctx.local - | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Lock verifier_atomic); - Lockset.add (verifier_atomic, true) ctx.local - | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Unlock verifier_atomic); - Lockset.remove (verifier_atomic, true) ctx.local - | _, "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 ctx.local [Events.Unlock m; Events.Lock m]; - ) ms; - raise Deadcode (* splits cover all cases *) - | _, x -> - ctx.local + ctx.local let enter ctx lv f args : (D.t * D.t) list = [(ctx.local,ctx.local)] @@ -298,6 +152,14 @@ struct | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." end; ctx.local + | Events.Lock2 l -> + let nls = D.add l ctx.local in + if not (D.equal ctx.local nls) then + ctx.emit (Lock (fst l)); + nls + | Events.Unlock2 l -> + ctx.emit (Unlock (fst l)); + D.remove l ctx.local | _ -> ctx.local @@ -334,4 +196,4 @@ end module Spec = MakeSpec (WriteBased) let _ = - MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec) + MCP.register_analysis ~dep:["mutexEvents"; "access"] (module Spec : MCPSpec) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 9f114ec749..68bfc6951d 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -291,7 +291,7 @@ "items": { "type": "string" }, "default": [ "expRelation", "base", "threadid", "threadflag", "threadreturn", - "escape", "mutex", "access", "mallocWrapper", "mhp" + "escape", "mutexEvents", "mutex", "access", "mallocWrapper", "mhp" ] }, "path_sens": { diff --git a/tests/regression/02-base/06-side_effect1.c b/tests/regression/02-base/06-side_effect1.c index 5805ad90a5..12f9339dbd 100644 --- a/tests/regression/02-base/06-side_effect1.c +++ b/tests/regression/02-base/06-side_effect1.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" #include #include diff --git a/tests/regression/02-base/07-side_effect2.c b/tests/regression/02-base/07-side_effect2.c index 54fa953a9d..eeb8af62b5 100644 --- a/tests/regression/02-base/07-side_effect2.c +++ b/tests/regression/02-base/07-side_effect2.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" #include #include diff --git a/tests/regression/02-base/09-ambigpointer.c b/tests/regression/02-base/09-ambigpointer.c index 085f44b7e7..c23d9a00f8 100644 --- a/tests/regression/02-base/09-ambigpointer.c +++ b/tests/regression/02-base/09-ambigpointer.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" #include #include diff --git a/tests/regression/02-base/10-init_allfuns.c b/tests/regression/02-base/10-init_allfuns.c index 22c84810a1..1f2a5de0df 100644 --- a/tests/regression/02-base/10-init_allfuns.c +++ b/tests/regression/02-base/10-init_allfuns.c @@ -1,4 +1,4 @@ -// PARAM: --enable allfuns --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --enable allfuns --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" int glob1 = 5; int glob2 = 7; diff --git a/tests/regression/02-base/23-malloc_globmt.c b/tests/regression/02-base/23-malloc_globmt.c index 2d008596af..66b8eb0047 100644 --- a/tests/regression/02-base/23-malloc_globmt.c +++ b/tests/regression/02-base/23-malloc_globmt.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" #include #include #include diff --git a/tests/regression/02-base/30-escape_sound.c b/tests/regression/02-base/30-escape_sound.c index cbafdd2678..1e72a4d044 100644 --- a/tests/regression/02-base/30-escape_sound.c +++ b/tests/regression/02-base/30-escape_sound.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" #include #include diff --git a/tests/regression/02-base/41-calloc_globmt.c b/tests/regression/02-base/41-calloc_globmt.c index 50ddba8622..7445dc1b85 100644 --- a/tests/regression/02-base/41-calloc_globmt.c +++ b/tests/regression/02-base/41-calloc_globmt.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" --set ana.int.interval true --set ana.base.arrays.domain partitioned +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" --set ana.int.interval true --set ana.base.arrays.domain partitioned #include #include #include diff --git a/tests/regression/03-practical/14-call_by_pointer.c b/tests/regression/03-practical/14-call_by_pointer.c index 9c1edd5248..b409c3dad3 100644 --- a/tests/regression/03-practical/14-call_by_pointer.c +++ b/tests/regression/03-practical/14-call_by_pointer.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutex','access','mallocWrapper']" +// PARAM: --set ana.activated "['base','threadid','threadflag','escape','mutexEvents','mutex','access','mallocWrapper']" #include /** From 4dfeca5844a55dcca7b92423b3056e9ac3d5f550 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 15:41:04 +0200 Subject: [PATCH 04/43] Emit special lock events from OSEK analysis --- src/analyses/osek.ml | 49 ++++++++++++++++++++++++++++++++++++++------ 1 file changed, 43 insertions(+), 6 deletions(-) diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml index dd62f1a898..2f9e147740 100644 --- a/src/analyses/osek.ml +++ b/src/analyses/osek.ml @@ -716,13 +716,20 @@ struct add_accesses ctx accessed (get_flags ctx.presub) ctx.local; ctx.local + let extract_lock lock = + match lock with + | AddrOf (Var varinfo,NoOffset) -> LockDomain.Addr.from_var varinfo + | _ -> assert false + let body ctx (f:fundec) : D.t = if tracing then trace "osek" "Analyzing function %s\n" f.svar.vname; let m_st = ctx.local in if (is_task f.svar.vname) then begin (* print_endline ( (string_of_int !Goblintutil.current_loc.line) ^ " in " ^ !Goblintutil.current_loc.file); *) (* print_endline ( "Looking for " ^ f.svar.vname); *) - M.special (swap_st ctx m_st) None (dummy_get f) [get_lock (trim f.svar.vname)] + let lock = get_lock (trim f.svar.vname) in + ctx.emit (Events.Lock2 (extract_lock lock, true)); + M.special (swap_st ctx m_st) None (dummy_get f) [lock] end else m_st @@ -738,7 +745,9 @@ struct let fname = f.svar.vname in if (is_task fname) then begin (* let _ = print_endline ( "Leaving task " ^ f.svar.vname) in *) - let x = M.special (swap_st ctx m_st) None (dummy_release f) [get_lock (trim fname)] in + let lock = get_lock (trim fname) in + ctx.emit (Events.Unlock2 (extract_lock lock, true)); + let x = M.special (swap_st ctx m_st) None (dummy_release f) [lock] in if (get_bool "ana.osek.check") && not(List.mem fname !warned) && not(D.is_empty x) then begin warned := fname :: !warned; let typ = if (Hashtbl.mem isrs fname) then "Interrupt " else "Task " in @@ -765,19 +774,45 @@ struct match fvname with (* suppress all fails *) | "GetResource" | "ReleaseResource" -> if (get_bool "ana.osek.check") then check_api_use 1 fvname (lockset_to_task (proj2_1 (partition ctx.local))); M.special ctx lval f (match arglist with - | [Lval (Var info,_)] -> [get_lock info.vname] + | [Lval (Var info,_)] -> + let lock = get_lock info.vname in + begin if fvname = "GetResource" then + ctx.emit (Events.Lock2 (extract_lock lock, true)) + else + ctx.emit (Events.Unlock2 (extract_lock lock, true)) + end; + [lock] | [CastE (_, Const c ) | Const c] -> if tracing then trace "osek" "Looking up Resource-ID %a\n" d_const c; let name = Hashtbl.find resourceids (Const c) in - [get_lock name] + let lock = get_lock name in + begin if fvname = "GetResource" then + ctx.emit (Events.Lock2 (extract_lock lock, true)) + else + ctx.emit (Events.Unlock2 (extract_lock lock, true)) + end; + [lock] | x -> x) | "GetSpinlock" | "ReleaseSpinlock" -> M.special ctx lval f (match arglist with - | [Lval (Var info,_)] -> [get_spinlock info.vname] + | [Lval (Var info,_)] -> + let lock = get_spinlock info.vname in + begin if fvname = "GetSpinlock" then + ctx.emit (Events.Lock2 (extract_lock lock, true)) + else + ctx.emit (Events.Unlock2 (extract_lock lock, true)) + end; + [lock] | [CastE (_, Const c ) | Const c] -> if tracing then trace "osek" "Looking up Spinlock-ID %a\n" d_const c; let name = Hashtbl.find spinlockids (Const c) in - [get_spinlock name] + let lock = get_spinlock name in + begin if fvname = "GetSpinlock" then + ctx.emit (Events.Lock2 (extract_lock lock, true)) + else + ctx.emit (Events.Unlock2 (extract_lock lock, true)) + end; + [lock] | x -> x) | "DisableAllInterrupts" -> let res = get_lock "DisableAllInterrupts" in if get_bool "ana.osek.check" && mem res ctx.local then print_endline "Nested calls of DisableAllInterrupts are not allowed!"; @@ -863,6 +898,8 @@ struct | _ -> M.special ctx lval f arglist (* with | _ -> M.special ctx lval f arglist (* suppress all fails *) *) + let event ctx e = M.event ctx e + let name () = "OSEK" let es_to_string f _ = f.svar.vname From 0b04e36492530503e02f7b54118d50c74322dd2c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 16:02:04 +0200 Subject: [PATCH 05/43] Use IdentitySpec for mutex analysis --- src/analyses/mutexAnalysis.ml | 29 +---------------------------- 1 file changed, 1 insertion(+), 28 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index af2515ab8e..42cfc9c0b7 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -23,7 +23,7 @@ end (** Mutex analyzer without base --- this is the new standard *) module MakeSpec (P: SpecParam) = struct - include Analyses.DefaultSpec + include Analyses.IdentitySpec (** name for the analysis (btw, it's "Only Mutex Must") *) let name () = "mutex" @@ -112,33 +112,6 @@ struct (* when reading: bump reader locks to exclusive as they protect reads *) Lockset.map (fun (x,_) -> (x,true)) ctx.local - (** Transfer functions: *) - - let assign ctx lval rval : D.t = - ctx.local - - let branch ctx exp tv : D.t = - ctx.local - - let return ctx exp fundec : D.t = - ctx.local - - let body ctx f : D.t = - ctx.local - - let special ctx lv f arglist : D.t = - ctx.local - - let enter ctx lv f args : (D.t * D.t) list = - [(ctx.local,ctx.local)] - - let combine ctx lv fexp f args fc al = - al - - - let threadspawn ctx lval f args fctx = - ctx.local - let event ctx e octx = match e with | Events.Access {var_opt; write} -> From cccb292ff09971b681d0537152ad25be28f0c5f4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 16:15:41 +0200 Subject: [PATCH 06/43] Simplify OSEK analysis fix by overridding M.special --- src/analyses/osek.ml | 68 +++++++++++++++++--------------------------- 1 file changed, 26 insertions(+), 42 deletions(-) diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml index 2f9e147740..7910faff8c 100644 --- a/src/analyses/osek.ml +++ b/src/analyses/osek.ml @@ -248,7 +248,26 @@ struct let check_fun = effect_fun end - module M = Mutex.MakeSpec (MyParam) + module M = + struct + include Mutex.MakeSpec (MyParam) + + let extract_lock lock = + match lock with + | AddrOf (Var varinfo,NoOffset) -> LockDomain.Addr.from_var varinfo + | _ -> assert false + + let special ctx lval f args = + (* simulate old mutex analysis special by emitting events directly, a la mutexEvents *) + begin match f.vname, args with + | ("GetResource" | "GetSpinlock"), [lock] -> + ctx.emit (Events.Lock2 (extract_lock lock, true)) + | ("ReleaseResource" | "ReleaseSpinlock"), [lock] -> + ctx.emit (Events.Unlock2 (extract_lock lock, true)) + | _, _ -> () + end; + special ctx lval f args + end module Offs = ValueDomain.Offs module Lockset = LockDomain.Lockset @@ -716,20 +735,13 @@ struct add_accesses ctx accessed (get_flags ctx.presub) ctx.local; ctx.local - let extract_lock lock = - match lock with - | AddrOf (Var varinfo,NoOffset) -> LockDomain.Addr.from_var varinfo - | _ -> assert false - let body ctx (f:fundec) : D.t = if tracing then trace "osek" "Analyzing function %s\n" f.svar.vname; let m_st = ctx.local in if (is_task f.svar.vname) then begin (* print_endline ( (string_of_int !Goblintutil.current_loc.line) ^ " in " ^ !Goblintutil.current_loc.file); *) (* print_endline ( "Looking for " ^ f.svar.vname); *) - let lock = get_lock (trim f.svar.vname) in - ctx.emit (Events.Lock2 (extract_lock lock, true)); - M.special (swap_st ctx m_st) None (dummy_get f) [lock] + M.special (swap_st ctx m_st) None (dummy_get f) [get_lock (trim f.svar.vname)] end else m_st @@ -745,9 +757,7 @@ struct let fname = f.svar.vname in if (is_task fname) then begin (* let _ = print_endline ( "Leaving task " ^ f.svar.vname) in *) - let lock = get_lock (trim fname) in - ctx.emit (Events.Unlock2 (extract_lock lock, true)); - let x = M.special (swap_st ctx m_st) None (dummy_release f) [lock] in + let x = M.special (swap_st ctx m_st) None (dummy_release f) [get_lock (trim fname)] in if (get_bool "ana.osek.check") && not(List.mem fname !warned) && not(D.is_empty x) then begin warned := fname :: !warned; let typ = if (Hashtbl.mem isrs fname) then "Interrupt " else "Task " in @@ -774,45 +784,19 @@ struct match fvname with (* suppress all fails *) | "GetResource" | "ReleaseResource" -> if (get_bool "ana.osek.check") then check_api_use 1 fvname (lockset_to_task (proj2_1 (partition ctx.local))); M.special ctx lval f (match arglist with - | [Lval (Var info,_)] -> - let lock = get_lock info.vname in - begin if fvname = "GetResource" then - ctx.emit (Events.Lock2 (extract_lock lock, true)) - else - ctx.emit (Events.Unlock2 (extract_lock lock, true)) - end; - [lock] + | [Lval (Var info,_)] -> [get_lock info.vname] | [CastE (_, Const c ) | Const c] -> if tracing then trace "osek" "Looking up Resource-ID %a\n" d_const c; let name = Hashtbl.find resourceids (Const c) in - let lock = get_lock name in - begin if fvname = "GetResource" then - ctx.emit (Events.Lock2 (extract_lock lock, true)) - else - ctx.emit (Events.Unlock2 (extract_lock lock, true)) - end; - [lock] + [get_lock name] | x -> x) | "GetSpinlock" | "ReleaseSpinlock" -> M.special ctx lval f (match arglist with - | [Lval (Var info,_)] -> - let lock = get_spinlock info.vname in - begin if fvname = "GetSpinlock" then - ctx.emit (Events.Lock2 (extract_lock lock, true)) - else - ctx.emit (Events.Unlock2 (extract_lock lock, true)) - end; - [lock] + | [Lval (Var info,_)] -> [get_spinlock info.vname] | [CastE (_, Const c ) | Const c] -> if tracing then trace "osek" "Looking up Spinlock-ID %a\n" d_const c; let name = Hashtbl.find spinlockids (Const c) in - let lock = get_spinlock name in - begin if fvname = "GetSpinlock" then - ctx.emit (Events.Lock2 (extract_lock lock, true)) - else - ctx.emit (Events.Unlock2 (extract_lock lock, true)) - end; - [lock] + [get_spinlock name] | x -> x) | "DisableAllInterrupts" -> let res = get_lock "DisableAllInterrupts" in if get_bool "ana.osek.check" && mem res ctx.local then print_endline "Nested calls of DisableAllInterrupts are not allowed!"; From 2225a10a1748c2e0b928c8bcba5baed0235d1da6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 16:33:18 +0200 Subject: [PATCH 07/43] Simplify mutexEvents analysis unit local state --- src/analyses/mutexEventsAnalysis.ml | 90 +++++++++-------------------- 1 file changed, 26 insertions(+), 64 deletions(-) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 6fcb3ccad8..8f28b04f27 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -42,38 +42,24 @@ struct Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) [] | _ -> [] - let lock ctx rw may_fail nonzero_return_when_aquired a lv arglist (ls: unit) = + let lock ctx rw may_fail nonzero_return_when_aquired a lv arglist = let is_a_blob addr = match LockDomain.Addr.to_var addr with | Some a -> a.vname.[0] = '(' | None -> false in let lock_one (e:LockDomain.Addr.t) = - if is_a_blob e then - ls - else begin - (* let nls = Lockset.add (e,rw) ls in *) - let nls = ls in - (* let changed = Lockset.compare ls nls <> 0 in *) - let changed = true in + if not (is_a_blob e) then begin match lv with | None -> - if may_fail then - ls - else ( - (* If the lockset did not change, do not emit Lock event *) - if changed then ctx.emit (Events.Lock2 (e, rw)); - nls - ) + if not may_fail then + ctx.emit (Events.Lock2 (e, rw)) | Some lv -> let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in - if changed then - ctx.split nls [sb; Events.Lock2 (e, rw)] - else - ctx.split nls [sb]; + ctx.split () [sb; Events.Lock2 (e, rw)]; if may_fail then ( let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in - ctx.split ls [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] + ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] ); raise Analyses.Deadcode end @@ -81,7 +67,7 @@ struct match arglist with | [x] -> begin match (eval_exp_addr a x) with | [e] -> lock_one e - | _ -> ls + | _ -> () end | _ -> (* Lockset.top () *) @@ -91,30 +77,18 @@ struct let return ctx exp fundec : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) - if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then ( - ctx.emit (Events.Unlock2 (verifier_atomic, true)); - (* Lockset.remove (verifier_atomic, true) ctx.local *) - ctx.local - ) - else - ctx.local + if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then + ctx.emit (Events.Unlock2 (verifier_atomic, true)) let body ctx f : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) - if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then ( - ctx.emit (Events.Lock2 (verifier_atomic, true)); - (* Lockset.add (verifier_atomic, true) ctx.local *) - ctx.local - ) - else - ctx.local + if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then + ctx.emit (Events.Lock2 (verifier_atomic, true)) let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = - let remove_rw x st = + let remove_rw x = ctx.emit (Events.Unlock2 (x, true)); - ctx.emit (Events.Unlock2 (x, false)); - (* Lockset.remove (x,true) (Lockset.remove (x,false) st) *) - st + ctx.emit (Events.Unlock2 (x, false)) in let unlock remove_fn = let remove_nonspecial x = @@ -128,23 +102,19 @@ struct match arglist with | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with | [] -> remove_nonspecial ctx.local - | es -> List.fold_right remove_fn es ctx.local + | es -> List.iter remove_fn es end - | _ -> ctx.local + | _ -> () in match (LF.classify f.vname arglist, f.vname) with | _, "_lock_kernel" -> - ctx.emit (Events.Lock2 (big_kernel_lock, true)); - (* Lockset.add (big_kernel_lock,true) ctx.local *) - ctx.local + ctx.emit (Events.Lock2 (big_kernel_lock, true)) | _, "_unlock_kernel" -> - ctx.emit (Events.Unlock2 (big_kernel_lock, true)); - (* Lockset.remove (big_kernel_lock,true) ctx.local *) - ctx.local + ctx.emit (Events.Unlock2 (big_kernel_lock, true)) | `Lock (failing, rw, nonzero_return_when_aquired), _ -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in (*print_endline @@ "Mutex `Lock "^f.vname;*) - lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arglist ctx.local + lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arglist | `Unlock, "__raw_read_unlock" | `Unlock, "__raw_write_unlock" -> let drop_raw_lock x = @@ -163,25 +133,17 @@ struct | `Unlock, _ -> (*print_endline @@ "Mutex `Unlock "^f.vname;*) unlock remove_rw - | _, "spinlock_check" -> ctx.local + | _, "spinlock_check" -> () | _, "acquire_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Lock2 (console_sem, true)); - (* Lockset.add (console_sem,true) ctx.local *) - ctx.local + ctx.emit (Events.Lock2 (console_sem, true)) | _, "release_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Unlock2 (console_sem, true)); - (* Lockset.remove (console_sem,true) ctx.local *) - ctx.local + ctx.emit (Events.Unlock2 (console_sem, true)) | _, "__builtin_prefetch" | _, "misc_deregister" -> - ctx.local + () | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Lock2 (verifier_atomic, true)); - (* Lockset.add (verifier_atomic, true) ctx.local *) - ctx.local + ctx.emit (Events.Lock2 (verifier_atomic, true)) | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Unlock2 (verifier_atomic, true)); - (* Lockset.remove (verifier_atomic, true) ctx.local *) - ctx.local + ctx.emit (Events.Unlock2 (verifier_atomic, true)) | _, "pthread_cond_wait" | _, "pthread_cond_timedwait" -> (* mutex is unlocked while waiting but relocked when returns *) @@ -191,11 +153,11 @@ struct 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 ctx.local [Events.Unlock2 (m, true); Events.Lock2 (m, true)]; + ctx.split () [Events.Unlock2 (m, true); Events.Lock2 (m, true)]; ) ms; raise Deadcode (* splits cover all cases *) | _, x -> - ctx.local + () end From 7a3363533a96b696287d6b587075cfd5d2b0719b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 16:47:11 +0200 Subject: [PATCH 08/43] Simplify mayLocks analysis using mutex events --- src/analyses/mayLocks.ml | 70 +++++++++++++--------------------------- 1 file changed, 22 insertions(+), 48 deletions(-) diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index f7354b4d86..d5a725cdde 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -5,38 +5,14 @@ open Analyses module Spec = struct - include Analyses.DefaultSpec + include Analyses.IdentitySpec let name () = "maylocks" module D = LockDomain.MayLockset module C = LockDomain.MayLockset - (* transfer functions : usual operation just propagates the value *) - 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 - - (* Helper function to convert query-offsets to valuedomain-offsets *) - let rec conv_offset x = - match x with - | `NoOffset -> `NoOffset - | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o) - | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o) - | `Field (f,o) -> `Field (f, conv_offset o) - - (* Query the value (of the locking argument) to a list of locks. *) - 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) -> - Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) [] - | b -> Messages.warn "Could not evaluate '%a' to an points-to set, instead got '%a'." d_exp exp Queries.LS.pretty b; [] - (* locking logic -- add all locks we can add *) - let lock ctx rw may_fail return_value_on_success a lv arglist ls : D.ReverseAddrSet.t = + (* let lock ctx rw may_fail return_value_on_success a lv arglist ls : D.ReverseAddrSet.t = let add_one ls e = D.add (e,rw) ls in let nls = List.fold_left add_one ls (List.concat_map (eval_exp_addr a) arglist) in match lv with @@ -44,32 +20,30 @@ struct | Some lv -> ctx.split nls [Events.SplitBranch (Lval lv, return_value_on_success)]; if may_fail then ctx.split ls [Events.SplitBranch (Lval lv, not return_value_on_success)]; - raise Analyses.Deadcode - - (* transfer function to handle library functions --- for us locking & unlocking *) - let special ctx (lv: lval option) (f:varinfo) (arglist:exp list) : D.t = - let remove_rw x st = D.remove (x,true) (D.remove (x,false) st) in - (* unlocking logic *) - let unlock remove_fn = - match arglist with - | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with - | [x] -> remove_fn x ctx.local - | _ -> ctx.local - end - | _ -> ctx.local - in - match (LibraryFunctions.classify f.vname arglist, f.vname) with - | `Lock (failing, rw, return_value_on_success), _ - -> lock ctx rw failing return_value_on_success (Analyses.ask_of_ctx ctx) lv arglist ctx.local - | `Unlock, _ - -> unlock remove_rw - - | _ -> ctx.local + raise Analyses.Deadcode *) + + (* let remove_rw x st = D.remove (x,true) (D.remove (x,false) st) + (* unlocking logic *) + let unlock remove_fn = + match arglist with + | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with + | [x] -> remove_fn x ctx.local + | _ -> ctx.local + end + | _ -> ctx.local *) let startstate v = D.empty () let threadenter ctx lval f args = [D.empty ()] - let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () + + let event ctx e octx = + match e with + | Events.Lock2 l -> + D.add l ctx.local + | Events.Unlock2 l -> + D.remove l ctx.local + | _ -> + ctx.local end let _ = From 930c908ec10f5972a8aaedb0b1a714e8a462be6b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 16:49:59 +0200 Subject: [PATCH 09/43] Simplify deadlock analysis using mutex events --- src/analyses/deadlock.ml | 74 +++++++--------------------------------- 1 file changed, 12 insertions(+), 62 deletions(-) diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index 8ee2433aed..f7a57990e3 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -8,7 +8,7 @@ let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref [] module Spec = struct - include Analyses.DefaultSpec + include Analyses.IdentitySpec let name () = "deadlock" @@ -44,69 +44,19 @@ struct (* Some required states *) let startstate _ : D.t = D.empty () let threadenter ctx lval f args = [D.empty ()] - let threadspawn ctx lval f args fctx = ctx.local let exitstate _ : D.t = D.empty () - (* ======== Transfer functions ======== *) - (* Called for assignments, branches, ... *) - - (* Assignment lval <- exp *) - let assign ctx (lval:lval) (rval:exp) : D.t = - ctx.local - - (* Branch *) - let branch ctx (exp:exp) (tv:bool) : D.t = - ctx.local - - (* Body of a function starts *) - let body ctx (f:fundec) : D.t = - ctx.local - - (* Returns from a function *) - let return ctx (exp:exp option) (f:fundec) : D.t = - ctx.local - - (* Calls/Enters a function *) - let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - [D.bot (),ctx.local] - - (* Leaves a function *) - let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = - au - - (* Helper function to convert query-offsets to valuedomain-offsets *) - let rec conv_offset x = - match x with - | `NoOffset -> `NoOffset - | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o) - | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o) - | `Field (f,o) -> `Field (f, conv_offset o) - - (* Query the value (of the locking argument) to a list of locks. *) - 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) -> - Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) [] - | b -> Messages.warn "Could not evaluate '%a' to an points-to set, instead got '%a'." d_exp exp Queries.LS.pretty b; [] - - (* Called when calling a special/unknown function *) - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - if D.is_top ctx.local then ctx.local else - match LibraryFunctions.classify f.vname arglist with - | `Lock (_, _, _) -> - List.fold_left (fun d lockAddr -> - addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; - D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local - ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist)) - | `Unlock -> - let lockAddrs = eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist) in - if List.compare_length_with lockAddrs 1 = 0 then - let inLockAddrs e = List.exists (fun r -> ValueDomain.Addr.equal r e.addr) lockAddrs in - D.filter (neg inLockAddrs) ctx.local - else ctx.local - | _ -> ctx.local - + let event ctx e octx = + match e with + | Events.Lock2 l -> + let lockAddr = fst l in + addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; + D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local + | Events.Unlock2 l -> + let inLockAddrs e = ValueDomain.Addr.equal (fst l) e.addr in + D.filter (neg inLockAddrs) ctx.local + | _ -> + ctx.local end let _ = From 0e8a0718e354ed82535ffc1c23132651a35d862d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 17:54:22 +0200 Subject: [PATCH 10/43] Fix typo in unlock event printing --- src/domains/events.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/domains/events.ml b/src/domains/events.ml index b151c8d9d2..448db92ee1 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -14,9 +14,9 @@ type t = let pretty () = function | Lock m -> dprintf "Lock %a" LockDomain.Addr.pretty m - | Unlock m -> dprintf "Unock %a" LockDomain.Addr.pretty m + | Unlock m -> dprintf "Unlock %a" LockDomain.Addr.pretty m | Lock2 m -> dprintf "Lock2 %a" LockDomain.Lockset.Lock.pretty m - | Unlock2 m -> dprintf "Unock2 %a" LockDomain.Lockset.Lock.pretty m + | Unlock2 m -> dprintf "Unlock2 %a" LockDomain.Lockset.Lock.pretty m | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped | EnterMultiThreaded -> text "EnterMultiThreaded" | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv From 1858dcd9e30d1f9592b8b9237acbc70ce7c3ccde Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 23 Mar 2022 17:55:51 +0200 Subject: [PATCH 11/43] Fix Unlock event emitted for both read and write lock This broke apron privatization because privatization saw double unlock. --- src/analyses/mutexAnalysis.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 42cfc9c0b7..1d1bbbfff9 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -131,7 +131,8 @@ struct ctx.emit (Lock (fst l)); nls | Events.Unlock2 l -> - ctx.emit (Unlock (fst l)); + if snd l then + ctx.emit (Unlock (fst l)); D.remove l ctx.local | _ -> ctx.local From 7c206445373ddaa987feb20182cdbebad6a251ac Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 12:04:22 +0200 Subject: [PATCH 12/43] Rename lock & unlock events --- src/analyses/apron/apronAnalysis.apron.ml | 4 ++-- src/analyses/base.ml | 4 ++-- src/analyses/deadlock.ml | 4 ++-- src/analyses/mayLocks.ml | 4 ++-- src/analyses/mutexAnalysis.ml | 8 +++---- src/analyses/mutexEventsAnalysis.ml | 26 +++++++++++------------ src/analyses/osek.ml | 4 ++-- src/domains/events.ml | 16 +++++++------- 8 files changed, 35 insertions(+), 35 deletions(-) diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 8fbe0660e4..cae8031962 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -411,9 +411,9 @@ struct let event ctx e aprx = let st = ctx.local in match e with - | Events.Lock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.MustLock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) Priv.lock (Analyses.ask_of_ctx aprx) aprx.global st addr - | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.MustUnlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) Priv.unlock (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st addr (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *) | Events.EnterMultiThreaded -> diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2e846da692..d5aecde6a5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2367,10 +2367,10 @@ struct let event ctx e octx = let st: store = ctx.local in match e with - | Events.Lock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.MustLock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr; Priv.lock (Analyses.ask_of_ctx octx) (priv_getg octx.global) st addr - | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.MustUnlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) Priv.unlock (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st addr | Events.Escape escaped -> Priv.escape (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st escaped diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index f7a57990e3..e8648b4657 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -48,11 +48,11 @@ struct let event ctx e octx = match e with - | Events.Lock2 l -> + | Events.Lock l -> let lockAddr = fst l in addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local - | Events.Unlock2 l -> + | Events.Unlock l -> let inLockAddrs e = ValueDomain.Addr.equal (fst l) e.addr in D.filter (neg inLockAddrs) ctx.local | _ -> diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index d5a725cdde..973a0fb0d2 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -38,9 +38,9 @@ struct let event ctx e octx = match e with - | Events.Lock2 l -> + | Events.Lock l -> D.add l ctx.local - | Events.Unlock2 l -> + | Events.Unlock l -> D.remove l ctx.local | _ -> ctx.local diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 1d1bbbfff9..c6975166fe 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -125,14 +125,14 @@ struct | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." end; ctx.local - | Events.Lock2 l -> + | Events.Lock l -> let nls = D.add l ctx.local in if not (D.equal ctx.local nls) then - ctx.emit (Lock (fst l)); + ctx.emit (MustLock (fst l)); nls - | Events.Unlock2 l -> + | Events.Unlock l -> if snd l then - ctx.emit (Unlock (fst l)); + ctx.emit (MustUnlock (fst l)); D.remove l ctx.local | _ -> ctx.local diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 8f28b04f27..029105bf88 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -53,10 +53,10 @@ struct match lv with | None -> if not may_fail then - ctx.emit (Events.Lock2 (e, rw)) + ctx.emit (Events.Lock (e, rw)) | Some lv -> let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in - ctx.split () [sb; Events.Lock2 (e, rw)]; + ctx.split () [sb; Events.Lock (e, rw)]; if may_fail then ( let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] @@ -78,17 +78,17 @@ struct let return ctx exp fundec : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then - ctx.emit (Events.Unlock2 (verifier_atomic, true)) + ctx.emit (Events.Unlock (verifier_atomic, true)) let body ctx f : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then - ctx.emit (Events.Lock2 (verifier_atomic, true)) + ctx.emit (Events.Lock (verifier_atomic, true)) let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = let remove_rw x = - ctx.emit (Events.Unlock2 (x, true)); - ctx.emit (Events.Unlock2 (x, false)) + ctx.emit (Events.Unlock (x, true)); + ctx.emit (Events.Unlock (x, false)) in let unlock remove_fn = let remove_nonspecial x = @@ -108,9 +108,9 @@ struct in match (LF.classify f.vname arglist, f.vname) with | _, "_lock_kernel" -> - ctx.emit (Events.Lock2 (big_kernel_lock, true)) + ctx.emit (Events.Lock (big_kernel_lock, true)) | _, "_unlock_kernel" -> - ctx.emit (Events.Unlock2 (big_kernel_lock, true)) + ctx.emit (Events.Unlock (big_kernel_lock, true)) | `Lock (failing, rw, nonzero_return_when_aquired), _ -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in (*print_endline @@ "Mutex `Lock "^f.vname;*) @@ -135,15 +135,15 @@ struct unlock remove_rw | _, "spinlock_check" -> () | _, "acquire_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Lock2 (console_sem, true)) + ctx.emit (Events.Lock (console_sem, true)) | _, "release_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Unlock2 (console_sem, true)) + ctx.emit (Events.Unlock (console_sem, true)) | _, "__builtin_prefetch" | _, "misc_deregister" -> () | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Lock2 (verifier_atomic, true)) + ctx.emit (Events.Lock (verifier_atomic, true)) | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Unlock2 (verifier_atomic, true)) + ctx.emit (Events.Unlock (verifier_atomic, true)) | _, "pthread_cond_wait" | _, "pthread_cond_timedwait" -> (* mutex is unlocked while waiting but relocked when returns *) @@ -153,7 +153,7 @@ struct 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.Unlock2 (m, true); Events.Lock2 (m, true)]; + ctx.split () [Events.Unlock (m, true); Events.Lock (m, true)]; ) ms; raise Deadcode (* splits cover all cases *) | _, x -> diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml index 7910faff8c..2841be98b1 100644 --- a/src/analyses/osek.ml +++ b/src/analyses/osek.ml @@ -261,9 +261,9 @@ struct (* simulate old mutex analysis special by emitting events directly, a la mutexEvents *) begin match f.vname, args with | ("GetResource" | "GetSpinlock"), [lock] -> - ctx.emit (Events.Lock2 (extract_lock lock, true)) + ctx.emit (Events.Lock (extract_lock lock, true)) | ("ReleaseResource" | "ReleaseSpinlock"), [lock] -> - ctx.emit (Events.Unlock2 (extract_lock lock, true)) + ctx.emit (Events.Unlock (extract_lock lock, true)) | _, _ -> () end; special ctx lval f args diff --git a/src/domains/events.ml b/src/domains/events.ml index 448db92ee1..54e7529ead 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -1,10 +1,10 @@ open Prelude.Ana type t = - | Lock of LockDomain.Addr.t (** This is only emitted if the mutex was not previously held *) - | Unlock of LockDomain.Addr.t - | Lock2 of LockDomain.Lockset.Lock.t - | Unlock2 of LockDomain.Lockset.Lock.t + | MustLock of LockDomain.Addr.t (** This is only emitted if the mutex was not previously held *) + | MustUnlock of LockDomain.Addr.t + | Lock of LockDomain.Lockset.Lock.t + | Unlock of LockDomain.Lockset.Lock.t | Escape of EscapeDomain.EscapedVars.t | EnterMultiThreaded | SplitBranch of exp * bool (** Used to simulate old branch-based split. *) @@ -13,10 +13,10 @@ type t = | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) let pretty () = function - | Lock m -> dprintf "Lock %a" LockDomain.Addr.pretty m - | Unlock m -> dprintf "Unlock %a" LockDomain.Addr.pretty m - | Lock2 m -> dprintf "Lock2 %a" LockDomain.Lockset.Lock.pretty m - | Unlock2 m -> dprintf "Unlock2 %a" LockDomain.Lockset.Lock.pretty m + | MustLock m -> dprintf "MustLock %a" LockDomain.Addr.pretty m + | MustUnlock m -> dprintf "MustUnlock %a" LockDomain.Addr.pretty m + | Lock m -> dprintf "Lock %a" LockDomain.Lockset.Lock.pretty m + | Unlock m -> dprintf "Unlock %a" LockDomain.Lockset.Lock.pretty m | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped | EnterMultiThreaded -> text "EnterMultiThreaded" | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv From 9fa79017c89a09ff000b3e2f401a598bdd3c4a8d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 12:08:37 +0200 Subject: [PATCH 13/43] Remove write argument from Unlock event --- src/analyses/deadlock.ml | 2 +- src/analyses/mayLocks.ml | 2 +- src/analyses/mutexAnalysis.ml | 5 ++--- src/analyses/mutexEventsAnalysis.ml | 13 ++++++------- src/analyses/osek.ml | 2 +- src/domains/events.ml | 4 ++-- 6 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index e8648b4657..f6cb9a8077 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -53,7 +53,7 @@ struct addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local | Events.Unlock l -> - let inLockAddrs e = ValueDomain.Addr.equal (fst l) e.addr in + let inLockAddrs e = ValueDomain.Addr.equal l e.addr in D.filter (neg inLockAddrs) ctx.local | _ -> ctx.local diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 973a0fb0d2..6f6d80e0e2 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -41,7 +41,7 @@ struct | Events.Lock l -> D.add l ctx.local | Events.Unlock l -> - D.remove l ctx.local + D.remove (l, true) (D.remove (l, false) ctx.local) | _ -> ctx.local end diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index c6975166fe..16001118bb 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -131,9 +131,8 @@ struct ctx.emit (MustLock (fst l)); nls | Events.Unlock l -> - if snd l then - ctx.emit (MustUnlock (fst l)); - D.remove l ctx.local + ctx.emit (MustUnlock l); + D.remove (l, true) (D.remove (l, false) ctx.local) | _ -> ctx.local diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 029105bf88..861b3ff7a3 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -78,7 +78,7 @@ struct let return ctx exp fundec : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then - ctx.emit (Events.Unlock (verifier_atomic, true)) + ctx.emit (Events.Unlock verifier_atomic) let body ctx f : D.t = (* deprecated but still valid SV-COMP convention for atomic block *) @@ -87,8 +87,7 @@ struct let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = let remove_rw x = - ctx.emit (Events.Unlock (x, true)); - ctx.emit (Events.Unlock (x, false)) + ctx.emit (Events.Unlock x) in let unlock remove_fn = let remove_nonspecial x = @@ -110,7 +109,7 @@ struct | _, "_lock_kernel" -> ctx.emit (Events.Lock (big_kernel_lock, true)) | _, "_unlock_kernel" -> - ctx.emit (Events.Unlock (big_kernel_lock, true)) + ctx.emit (Events.Unlock big_kernel_lock) | `Lock (failing, rw, nonzero_return_when_aquired), _ -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in (*print_endline @@ "Mutex `Lock "^f.vname;*) @@ -137,13 +136,13 @@ struct | _, "acquire_console_sem" when get_bool "kernel" -> ctx.emit (Events.Lock (console_sem, true)) | _, "release_console_sem" when get_bool "kernel" -> - ctx.emit (Events.Unlock (console_sem, true)) + ctx.emit (Events.Unlock console_sem) | _, "__builtin_prefetch" | _, "misc_deregister" -> () | _, "__VERIFIER_atomic_begin" when get_bool "ana.sv-comp.functions" -> ctx.emit (Events.Lock (verifier_atomic, true)) | _, "__VERIFIER_atomic_end" when get_bool "ana.sv-comp.functions" -> - ctx.emit (Events.Unlock (verifier_atomic, true)) + ctx.emit (Events.Unlock verifier_atomic) | _, "pthread_cond_wait" | _, "pthread_cond_timedwait" -> (* mutex is unlocked while waiting but relocked when returns *) @@ -153,7 +152,7 @@ struct 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, true); Events.Lock (m, true)]; + ctx.split () [Events.Unlock m; Events.Lock (m, true)]; ) ms; raise Deadcode (* splits cover all cases *) | _, x -> diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml index 2841be98b1..b6416c8a4b 100644 --- a/src/analyses/osek.ml +++ b/src/analyses/osek.ml @@ -263,7 +263,7 @@ struct | ("GetResource" | "GetSpinlock"), [lock] -> ctx.emit (Events.Lock (extract_lock lock, true)) | ("ReleaseResource" | "ReleaseSpinlock"), [lock] -> - ctx.emit (Events.Unlock (extract_lock lock, true)) + ctx.emit (Events.Unlock (extract_lock lock)) | _, _ -> () end; special ctx lval f args diff --git a/src/domains/events.ml b/src/domains/events.ml index 54e7529ead..e6efb99bd6 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -4,7 +4,7 @@ type t = | MustLock of LockDomain.Addr.t (** This is only emitted if the mutex was not previously held *) | MustUnlock of LockDomain.Addr.t | Lock of LockDomain.Lockset.Lock.t - | Unlock of LockDomain.Lockset.Lock.t + | Unlock of LockDomain.Addr.t | Escape of EscapeDomain.EscapedVars.t | EnterMultiThreaded | SplitBranch of exp * bool (** Used to simulate old branch-based split. *) @@ -16,7 +16,7 @@ let pretty () = function | MustLock m -> dprintf "MustLock %a" LockDomain.Addr.pretty m | MustUnlock m -> dprintf "MustUnlock %a" LockDomain.Addr.pretty m | Lock m -> dprintf "Lock %a" LockDomain.Lockset.Lock.pretty m - | Unlock m -> dprintf "Unlock %a" LockDomain.Lockset.Lock.pretty m + | Unlock m -> dprintf "Unlock %a" LockDomain.Addr.pretty m | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped | EnterMultiThreaded -> text "EnterMultiThreaded" | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv From 555ac531abb0d1cc2f99cbb2da8e531c66d4a6eb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 12:29:33 +0200 Subject: [PATCH 14/43] Remove lock/unlock multiple argument support --- src/analyses/mutexEventsAnalysis.ml | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 861b3ff7a3..ff1dbe28ef 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -42,7 +42,7 @@ struct Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) [] | _ -> [] - let lock ctx rw may_fail nonzero_return_when_aquired a lv arglist = + let lock ctx rw may_fail nonzero_return_when_aquired a lv arg = let is_a_blob addr = match LockDomain.Addr.to_var addr with | Some a -> a.vname.[0] = '(' @@ -64,14 +64,9 @@ struct raise Analyses.Deadcode end in - match arglist with - | [x] -> begin match (eval_exp_addr a x) with - | [e] -> lock_one e - | _ -> () - end - | _ -> - (* Lockset.top () *) - () + match eval_exp_addr a arg with + | [e] -> lock_one e + | _ -> () @@ -99,21 +94,25 @@ struct () in match arglist with - | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with + | [arg] -> + begin match eval_exp_addr (Analyses.ask_of_ctx ctx) arg with | [] -> remove_nonspecial ctx.local | es -> List.iter remove_fn es end - | _ -> () + | _ -> failwith "unlock has multiple arguments" in match (LF.classify f.vname arglist, f.vname) with | _, "_lock_kernel" -> ctx.emit (Events.Lock (big_kernel_lock, true)) | _, "_unlock_kernel" -> ctx.emit (Events.Unlock big_kernel_lock) - | `Lock (failing, rw, nonzero_return_when_aquired), _ - -> let arglist = if f.vname = "LAP_Se_WaitSemaphore" then [List.hd arglist] else arglist in - (*print_endline @@ "Mutex `Lock "^f.vname;*) - lock ctx rw failing nonzero_return_when_aquired (Analyses.ask_of_ctx ctx) lv arglist + | `Lock (failing, rw, nonzero_return_when_aquired), _ -> + begin match arglist with + | [arg] -> + (*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" + end | `Unlock, "__raw_read_unlock" | `Unlock, "__raw_write_unlock" -> let drop_raw_lock x = From 46d78bb24225f22e5d2135e51cb92dff3c831bea Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 12:31:09 +0200 Subject: [PATCH 15/43] Add mutexEvents analysis dependency to mayLocks & deadlock --- src/analyses/deadlock.ml | 2 +- src/analyses/mayLocks.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index f6cb9a8077..cc9bdf8bd1 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -60,4 +60,4 @@ struct end let _ = - MCP.register_analysis (module Spec : MCPSpec) + MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec) diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 6f6d80e0e2..487bc4d847 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -47,4 +47,4 @@ struct end let _ = - MCP.register_analysis (module Spec : MCPSpec) + MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec) From dbd6b3e85542d816e7d912a817fc430353c73068 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 12:52:59 +0200 Subject: [PATCH 16/43] Test mutexEvents based deadlock with failing locks --- .../regression/15-deadlock/19-fail_deadlock.c | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 tests/regression/15-deadlock/19-fail_deadlock.c diff --git a/tests/regression/15-deadlock/19-fail_deadlock.c b/tests/regression/15-deadlock/19-fail_deadlock.c new file mode 100644 index 0000000000..57973371b2 --- /dev/null +++ b/tests/regression/15-deadlock/19-fail_deadlock.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] deadlock --enable sem.lock.fail +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + pthread_mutex_lock(&mutex2); + pthread_mutex_lock(&mutex1); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(&mutex2); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 10000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From 41ec21dac087b0133b2d4f6737021d01fc5d7c5b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 12:53:23 +0200 Subject: [PATCH 17/43] Fix lock event not emitted with failing locks and no lhs --- src/analyses/mutexEventsAnalysis.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index ff1dbe28ef..5e03d7e2e3 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -52,8 +52,10 @@ struct if not (is_a_blob e) then begin match lv with | None -> - if not may_fail then - ctx.emit (Events.Lock (e, rw)) + ctx.split () [Events.Lock (e, rw)]; + if may_fail then + ctx.split () []; + raise Analyses.Deadcode | Some lv -> let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in ctx.split () [sb; Events.Lock (e, rw)]; From b3e905a92cc222d4fe6d4add70c2492a13dadaec Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 13:02:52 +0200 Subject: [PATCH 18/43] Replace name based blob check with IsMultiple query for lock --- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/mutexEventsAnalysis.ml | 35 ++++++++++++----------------- 2 files changed, 15 insertions(+), 22 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 16001118bb..d774bbec11 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -125,7 +125,7 @@ struct | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." end; ctx.local - | Events.Lock l -> + | Events.Lock ((Addr (v, _), _) as l) when not (ctx.ask (IsMultiple v)) -> let nls = D.add l ctx.local in if not (D.equal ctx.local nls) then ctx.emit (MustLock (fst l)); diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 5e03d7e2e3..3e753b59ae 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -43,28 +43,21 @@ struct | _ -> [] let lock ctx rw may_fail nonzero_return_when_aquired a lv arg = - let is_a_blob addr = - match LockDomain.Addr.to_var addr with - | Some a -> a.vname.[0] = '(' - | None -> false - in let lock_one (e:LockDomain.Addr.t) = - if not (is_a_blob e) then begin - match lv with - | None -> - ctx.split () [Events.Lock (e, rw)]; - if may_fail then - ctx.split () []; - raise Analyses.Deadcode - | Some lv -> - let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in - ctx.split () [sb; Events.Lock (e, rw)]; - if may_fail then ( - let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in - ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] - ); - raise Analyses.Deadcode - end + match lv with + | None -> + ctx.split () [Events.Lock (e, rw)]; + if may_fail then + ctx.split () []; + raise Analyses.Deadcode + | Some lv -> + let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in + ctx.split () [sb; Events.Lock (e, rw)]; + if may_fail then ( + let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in + ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] + ); + raise Analyses.Deadcode in match eval_exp_addr a arg with | [e] -> lock_one e From 078c11c1f5f1902db4018bfdb7b068ff22b512c6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 13:14:55 +0200 Subject: [PATCH 19/43] Fix lock event not emitted for ambiguous pointers --- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/mutexEventsAnalysis.ml | 44 +++++++++--------- .../15-deadlock/20-ambig_deadlock.c | 45 +++++++++++++++++++ 3 files changed, 68 insertions(+), 23 deletions(-) create mode 100644 tests/regression/15-deadlock/20-ambig_deadlock.c diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index d774bbec11..3885551e8e 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -125,7 +125,7 @@ struct | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." end; ctx.local - | Events.Lock ((Addr (v, _), _) as l) when not (ctx.ask (IsMultiple v)) -> + | Events.Lock ((Addr (v, _) as a, _) as l) when not (Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset))) && not (ctx.ask (IsMultiple v)) -> let nls = D.add l ctx.local in if not (D.equal ctx.local nls) then ctx.emit (MustLock (fst l)); diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 3e753b59ae..ea6adac46c 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -38,30 +38,30 @@ struct 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) [] - | _ -> [] + | a when Queries.LS.is_top a -> + [ValueDomain.Addr.from_var_offset (dummyFunDec.svar, `NoOffset)] + | a -> + Queries.LS.fold gather_addr a [] let lock ctx rw may_fail nonzero_return_when_aquired a lv arg = - let lock_one (e:LockDomain.Addr.t) = - match lv with - | None -> - ctx.split () [Events.Lock (e, rw)]; - if may_fail then - ctx.split () []; - raise Analyses.Deadcode - | Some lv -> - let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in - ctx.split () [sb; Events.Lock (e, rw)]; - if may_fail then ( - let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in - ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] - ); - raise Analyses.Deadcode - in - match eval_exp_addr a arg with - | [e] -> lock_one e - | _ -> () + match lv with + | None -> + List.iter (fun e -> + ctx.split () [Events.Lock (e, rw)] + ) (eval_exp_addr a arg); + if may_fail then + ctx.split () []; + raise Analyses.Deadcode + | Some lv -> + let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in + List.iter (fun e -> + ctx.split () [sb; Events.Lock (e, rw)]; + ) (eval_exp_addr a arg); + if may_fail then ( + let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in + ctx.split () [Events.SplitBranch (fail_exp, not nonzero_return_when_aquired)] + ); + raise Analyses.Deadcode diff --git a/tests/regression/15-deadlock/20-ambig_deadlock.c b/tests/regression/15-deadlock/20-ambig_deadlock.c new file mode 100644 index 0000000000..74b50dd7e1 --- /dev/null +++ b/tests/regression/15-deadlock/20-ambig_deadlock.c @@ -0,0 +1,45 @@ +// PARAM: --set ana.activated[+] deadlock --set ana.path_sens[-] mutex +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + int k = rand() % 2; + pthread_mutex_t *m; + if (k) + m = &mutex2; + else + m = &mutex3; + pthread_mutex_lock(m); + pthread_mutex_lock(&mutex1); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(m); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From bb9e600a5c38a8162017a7f393826e3f9702a6c3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 13:45:03 +0200 Subject: [PATCH 20/43] Fix deadlock with unknown pointer --- src/analyses/deadlock.ml | 11 ++++- .../15-deadlock/21-unknown_deadlock.c | 41 +++++++++++++++++++ 2 files changed, 51 insertions(+), 1 deletion(-) create mode 100644 tests/regression/15-deadlock/21-unknown_deadlock.c diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index cc9bdf8bd1..893ce183dc 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -3,6 +3,7 @@ open Prelude.Ana open Analyses open DeadlockDomain +open ValueDomain let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref [] @@ -22,10 +23,18 @@ struct else forbiddenList := (a,b)::!forbiddenList in + let may_equal l1 l2 = match l1, l2 with + | {addr = a; _}, _ when Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + true + | _, {addr = a; _} when Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + true + | _, _ -> MyLock.equal l1 l2 + in + (* Check forbidden list *) if !Goblintutil.postsolving then begin D.iter (fun e -> List.iter (fun (a,b) -> - if ((MyLock.equal a e) && (MyLock.equal b newLock)) then ( + if ((may_equal a e) && (may_equal b newLock)) then ( Messages.warn "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty e.addr ValueDomain.Addr.pretty newLock.addr CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc CilType.Location.pretty b.loc CilType.Location.pretty a.loc; Messages.warn ~loc:a.loc "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty newLock.addr ValueDomain.Addr.pretty e.addr CilType.Location.pretty b.loc CilType.Location.pretty a.loc CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc; ) diff --git a/tests/regression/15-deadlock/21-unknown_deadlock.c b/tests/regression/15-deadlock/21-unknown_deadlock.c new file mode 100644 index 0000000000..3bf73d61e0 --- /dev/null +++ b/tests/regression/15-deadlock/21-unknown_deadlock.c @@ -0,0 +1,41 @@ +// PARAM: --set ana.activated[+] deadlock +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + int k = rand() % 2; + pthread_mutex_t *m; // unknown + pthread_mutex_lock(m); + pthread_mutex_lock(&mutex1); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(m); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From 2db10a0ff2c40d085aa959998fc5f98a0cec8055 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 13:55:36 +0200 Subject: [PATCH 21/43] Fix must lockset unlock of unknown pointer --- src/analyses/mutexAnalysis.ml | 6 +++++ .../04-mutex/63-unknown_unlock_rc.c | 23 +++++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 tests/regression/04-mutex/63-unknown_unlock_rc.c diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 3885551e8e..8c5902c29b 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -130,6 +130,12 @@ struct if not (D.equal ctx.local nls) then ctx.emit (MustLock (fst l)); nls + | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + (* unlock everything! *) + Mutexes.iter (fun m -> + ctx.emit (MustUnlock m) + ) (D.export_locks ctx.local); + D.empty () | Events.Unlock l -> ctx.emit (MustUnlock l); D.remove (l, true) (D.remove (l, false) ctx.local) diff --git a/tests/regression/04-mutex/63-unknown_unlock_rc.c b/tests/regression/04-mutex/63-unknown_unlock_rc.c new file mode 100644 index 0000000000..0b896f3c6a --- /dev/null +++ b/tests/regression/04-mutex/63-unknown_unlock_rc.c @@ -0,0 +1,23 @@ +#include +#include + +int myglobal; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_t *m; // unknown + pthread_mutex_unlock(m); + myglobal=myglobal+1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex1); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex1); + pthread_join (id, NULL); + return 0; +} From b3db97dac9020268f954377a163dd5a876e62c5d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 14:11:44 +0200 Subject: [PATCH 22/43] Fix deadlock ambiguous unlock pointer --- src/analyses/mutexEventsAnalysis.ml | 16 +++--- .../15-deadlock/22-ambig_unlock_deadlock.c | 51 +++++++++++++++++++ 2 files changed, 58 insertions(+), 9 deletions(-) create mode 100644 tests/regression/15-deadlock/22-ambig_unlock_deadlock.c diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index ea6adac46c..5762c5f033 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -76,24 +76,22 @@ struct ctx.emit (Events.Lock (verifier_atomic, true)) let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = - let remove_rw x = - ctx.emit (Events.Unlock x) - in + let remove_rw x = x in let unlock remove_fn = - let remove_nonspecial x = + (* let remove_nonspecial x = (* if Lockset.is_top x then x else Lockset.filter (fun (v,_) -> match LockDomain.Addr.to_var v with | Some v when v.vname.[0] = '{' -> true | _ -> false ) x *) () - in + in *) match arglist with | [arg] -> - begin match eval_exp_addr (Analyses.ask_of_ctx ctx) arg with - | [] -> remove_nonspecial ctx.local - | es -> List.iter remove_fn es - end + List.iter (fun e -> + ctx.split () [Events.Unlock (remove_fn e)] + ) (eval_exp_addr (Analyses.ask_of_ctx ctx) arg); + raise Analyses.Deadcode | _ -> failwith "unlock has multiple arguments" in match (LF.classify f.vname arglist, f.vname) with diff --git a/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c b/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c new file mode 100644 index 0000000000..ec22bff992 --- /dev/null +++ b/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c @@ -0,0 +1,51 @@ +// PARAM: --set ana.activated[+] deadlock --set ana.path_sens[-] mutex +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + int k = rand() % 2; + int l = rand() % 2; + pthread_mutex_t *m, *n; + if (k) + m = &mutex2; + else + m = &mutex3; + if (l) + n = &mutex2; + else + n = &mutex3; + pthread_mutex_lock(m); + pthread_mutex_unlock(n); + pthread_mutex_lock(&mutex1); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(m); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From 16fc5bc0137652ce3b463c30d2c8321c22023f4b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 15:19:16 +0200 Subject: [PATCH 23/43] Fix maylocks & deadlock unknown unlock pointer --- src/analyses/deadlock.ml | 3 ++ src/analyses/mayLocks.ml | 4 ++ .../15-deadlock/23-unknown_unlock_deadlock.c | 42 +++++++++++++++++++ 3 files changed, 49 insertions(+) create mode 100644 tests/regression/15-deadlock/23-unknown_unlock_deadlock.c diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index 893ce183dc..a6ae442bee 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -61,6 +61,9 @@ struct let lockAddr = fst l in addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local + | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + (* unlock nothing *) + ctx.local | Events.Unlock l -> let inLockAddrs e = ValueDomain.Addr.equal l e.addr in D.filter (neg inLockAddrs) ctx.local diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 487bc4d847..7bba4f39bf 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -2,6 +2,7 @@ open Prelude.Ana open Analyses +open ValueDomain module Spec = struct @@ -40,6 +41,9 @@ struct match e with | Events.Lock l -> D.add l ctx.local + | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + (* unlock nothing *) + ctx.local | Events.Unlock l -> D.remove (l, true) (D.remove (l, false) ctx.local) | _ -> diff --git a/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c b/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c new file mode 100644 index 0000000000..80d9aca93a --- /dev/null +++ b/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c @@ -0,0 +1,42 @@ +// PARAM: --set ana.activated[+] deadlock +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + int k = rand() % 2; + pthread_mutex_t *m, *n; // unknown + pthread_mutex_lock(m); + pthread_mutex_unlock(n); + pthread_mutex_lock(&mutex1); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(m); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From ed693a25a7765f2aa59276c069aef01adb90e264 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 15:19:57 +0200 Subject: [PATCH 24/43] Fix maylocks & deadlock blob unlock pointer --- src/analyses/deadlock.ml | 3 ++ src/analyses/mayLocks.ml | 3 ++ .../15-deadlock/24-malloc_unlock_deadlock.c | 49 +++++++++++++++++++ .../15-deadlock/25-malloc_deadlock.c | 48 ++++++++++++++++++ 4 files changed, 103 insertions(+) create mode 100644 tests/regression/15-deadlock/24-malloc_unlock_deadlock.c create mode 100644 tests/regression/15-deadlock/25-malloc_deadlock.c diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index a6ae442bee..de548d8f76 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -64,6 +64,9 @@ struct | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> (* unlock nothing *) ctx.local + | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> + (* unlock nothing *) + ctx.local | Events.Unlock l -> let inLockAddrs e = ValueDomain.Addr.equal l e.addr in D.filter (neg inLockAddrs) ctx.local diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 7bba4f39bf..7a73ca8bc9 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -44,6 +44,9 @@ struct | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> (* unlock nothing *) ctx.local + | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> + (* unlock nothing *) + ctx.local | Events.Unlock l -> D.remove (l, true) (D.remove (l, false) ctx.local) | _ -> diff --git a/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c b/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c new file mode 100644 index 0000000000..890257e44e --- /dev/null +++ b/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c @@ -0,0 +1,49 @@ +// PARAM: --set ana.activated[+] deadlock +#include +#include + +int g1, g2; +pthread_mutex_t *p, *q; + +void *t1(void *arg) { + pthread_mutex_lock(p); + pthread_mutex_lock(q); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(q); + pthread_mutex_unlock(p); + return NULL; +} + +void *t2(void *arg) { + pthread_mutex_lock(p); + pthread_mutex_unlock(p); + pthread_mutex_lock(q); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(q); + pthread_mutex_unlock(p); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + pthread_mutex_t *a; + + for (i=0; i < 10; i++){ + a = malloc(sizeof(pthread_mutex_t)); + pthread_mutex_init(a,0); + if (i==3) + p = a; + if (i==7) + q = a; + } + + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} diff --git a/tests/regression/15-deadlock/25-malloc_deadlock.c b/tests/regression/15-deadlock/25-malloc_deadlock.c new file mode 100644 index 0000000000..72a86f7824 --- /dev/null +++ b/tests/regression/15-deadlock/25-malloc_deadlock.c @@ -0,0 +1,48 @@ +// PARAM: --set ana.activated[+] deadlock +#include +#include + +int g1, g2; +pthread_mutex_t *p, *q; + +void *t1(void *arg) { + pthread_mutex_lock(p); + pthread_mutex_lock(q); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(q); + pthread_mutex_unlock(p); + return NULL; +} + +void *t2(void *arg) { + pthread_mutex_lock(p); + pthread_mutex_lock(q); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(q); + pthread_mutex_unlock(p); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + pthread_mutex_t *a; + + for (i=0; i < 10; i++){ + a = malloc(sizeof(pthread_mutex_t)); + pthread_mutex_init(a,0); + if (i==3) + p = a; + if (i==7) + q = a; + } + + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From 5a0e33aed5ab2d33910f493b79c4215de56b1b14 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 15:40:53 +0200 Subject: [PATCH 25/43] Remove commented out lockset code --- src/analyses/mayLocks.ml | 21 --------------------- src/analyses/mutexAnalysis.ml | 1 + src/analyses/mutexEventsAnalysis.ml | 8 -------- 3 files changed, 1 insertion(+), 29 deletions(-) diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 7a73ca8bc9..45f1b49af7 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -12,27 +12,6 @@ struct module D = LockDomain.MayLockset module C = LockDomain.MayLockset - (* locking logic -- add all locks we can add *) - (* let lock ctx rw may_fail return_value_on_success a lv arglist ls : D.ReverseAddrSet.t = - let add_one ls e = D.add (e,rw) ls in - let nls = List.fold_left add_one ls (List.concat_map (eval_exp_addr a) arglist) in - match lv with - | None -> nls - | Some lv -> - ctx.split nls [Events.SplitBranch (Lval lv, return_value_on_success)]; - if may_fail then ctx.split ls [Events.SplitBranch (Lval lv, not return_value_on_success)]; - raise Analyses.Deadcode *) - - (* let remove_rw x st = D.remove (x,true) (D.remove (x,false) st) - (* unlocking logic *) - let unlock remove_fn = - match arglist with - | x::xs -> begin match (eval_exp_addr (Analyses.ask_of_ctx ctx) x) with - | [x] -> remove_fn x ctx.local - | _ -> ctx.local - end - | _ -> ctx.local *) - let startstate v = D.empty () let threadenter ctx lval f args = [D.empty ()] let exitstate v = D.top () diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 8c5902c29b..187fa1a5bb 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -135,6 +135,7 @@ struct Mutexes.iter (fun m -> ctx.emit (MustUnlock m) ) (D.export_locks ctx.local); + (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *) D.empty () | Events.Unlock l -> ctx.emit (MustUnlock l); diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 5762c5f033..267f7eb0ee 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -78,14 +78,6 @@ struct let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t = let remove_rw x = x in let unlock remove_fn = - (* let remove_nonspecial x = - (* if Lockset.is_top x then x else - Lockset.filter (fun (v,_) -> match LockDomain.Addr.to_var v with - | Some v when v.vname.[0] = '{' -> true - | _ -> false - ) x *) - () - in *) match arglist with | [arg] -> List.iter (fun e -> From a181629981e8ac95c482520c6e5e62ef6d9e5068 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 16:10:53 +0200 Subject: [PATCH 26/43] Extract functor for may lockset analysis --- src/analyses/deadlock.ml | 43 +++++++++------------------ src/analyses/locksetAnalysis.ml | 52 +++++++++++++++++++++++++++++++++ src/analyses/mayLocks.ml | 36 +++++++++-------------- 3 files changed, 79 insertions(+), 52 deletions(-) create mode 100644 src/analyses/locksetAnalysis.ml diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index de548d8f76..985809466c 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -7,15 +7,9 @@ open ValueDomain let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref [] -module Spec = +module Arg = struct - include Analyses.IdentitySpec - - let name () = "deadlock" - - (* The domain for the analysis *) - module D = DeadlockDomain.Lockset (* MayLockset *) - module C = DeadlockDomain.Lockset + module D = DeadlockDomain.Lockset let addLockingInfo newLock lockList = let add_comb a b = @@ -49,29 +43,20 @@ struct ) lockList end + let add ctx l = + let lockAddr = fst l in + addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; + D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local - (* Some required states *) - let startstate _ : D.t = D.empty () - let threadenter ctx lval f args = [D.empty ()] - let exitstate _ : D.t = D.empty () + let remove ctx l = + let inLockAddrs e = ValueDomain.Addr.equal l e.addr in + D.filter (neg inLockAddrs) ctx.local +end - let event ctx e octx = - match e with - | Events.Lock l -> - let lockAddr = fst l in - addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local; - D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local - | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> - (* unlock nothing *) - ctx.local - | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> - (* unlock nothing *) - ctx.local - | Events.Unlock l -> - let inLockAddrs e = ValueDomain.Addr.equal l e.addr in - D.filter (neg inLockAddrs) ctx.local - | _ -> - ctx.local +module Spec = +struct + include LocksetAnalysis.MakeMay (Arg) + let name () = "deadlock" end let _ = diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml new file mode 100644 index 0000000000..76eb1c11dd --- /dev/null +++ b/src/analyses/locksetAnalysis.ml @@ -0,0 +1,52 @@ +(** Basic lockset analyses. *) + +open Prelude.Ana +open Analyses +open ValueDomain + +module type Arg = +sig + module D: sig + include Lattice.S + val empty: unit -> t + end + + val add: (D.t, _, D.t, _) ctx -> LockDomain.Lockset.Lock.t -> D.t + val remove: (D.t, _, D.t, _) ctx -> Addr.t -> D.t +end + + +module Make (Arg: Arg): MCPSpec with module D = Arg.D and module C = Arg.D = +struct + include Analyses.IdentitySpec + let name () = "lockset" + + module D = Arg.D + module C = D + + let startstate v = D.empty () + let threadenter ctx lval f args = [D.empty ()] + let exitstate v = D.empty () +end + + +module MakeMay (Arg: Arg): MCPSpec with module D = Arg.D and module C = Arg.D = +struct + include Make (Arg) + let name () = "mayLockset" + + let event ctx e octx = + match e with + | Events.Lock l -> + Arg.add ctx l + | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + (* unlock nothing *) + ctx.local + | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> + (* unlock nothing *) + ctx.local + | Events.Unlock l -> + Arg.remove ctx l + | _ -> + ctx.local +end diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 45f1b49af7..d5a4175bfa 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -2,34 +2,24 @@ open Prelude.Ana open Analyses -open ValueDomain -module Spec = +module Arg = struct - include Analyses.IdentitySpec - - let name () = "maylocks" module D = LockDomain.MayLockset - module C = LockDomain.MayLockset - let startstate v = D.empty () - let threadenter ctx lval f args = [D.empty ()] - let exitstate v = D.top () + let add ctx l = + D.add l ctx.local + + let remove ctx l = + D.remove (l, true) (D.remove (l, false) ctx.local) +end + +module Spec = +struct + include LocksetAnalysis.MakeMay (Arg) + let name () = "maylocks" - let event ctx e octx = - match e with - | Events.Lock l -> - D.add l ctx.local - | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> - (* unlock nothing *) - ctx.local - | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> - (* unlock nothing *) - ctx.local - | Events.Unlock l -> - D.remove (l, true) (D.remove (l, false) ctx.local) - | _ -> - ctx.local + let exitstate v = D.top () (* TODO: why? *) end let _ = From 422ebdecec13e481c4f73f0dd13c2fa6c22c12f0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 16:35:55 +0200 Subject: [PATCH 27/43] Extract functor for must lockset analysis --- src/analyses/locksetAnalysis.ml | 52 +++++++++++++++++++++------- src/analyses/mutexAnalysis.ml | 60 +++++++++++++++------------------ 2 files changed, 66 insertions(+), 46 deletions(-) diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml index 76eb1c11dd..12e8da85e9 100644 --- a/src/analyses/locksetAnalysis.ml +++ b/src/analyses/locksetAnalysis.ml @@ -4,24 +4,19 @@ open Prelude.Ana open Analyses open ValueDomain -module type Arg = -sig - module D: sig - include Lattice.S - val empty: unit -> t - end - val add: (D.t, _, D.t, _) ctx -> LockDomain.Lockset.Lock.t -> D.t - val remove: (D.t, _, D.t, _) ctx -> Addr.t -> D.t +module type DS = +sig + include Lattice.S + val empty: unit -> t end - -module Make (Arg: Arg): MCPSpec with module D = Arg.D and module C = Arg.D = +module Make (D: DS) = struct include Analyses.IdentitySpec let name () = "lockset" - module D = Arg.D + module D = D module C = D let startstate v = D.empty () @@ -30,9 +25,16 @@ struct end -module MakeMay (Arg: Arg): MCPSpec with module D = Arg.D and module C = Arg.D = +module type MayArg = +sig + module D: DS + val add: (D.t, _, D.t, _) ctx -> LockDomain.Lockset.Lock.t -> D.t + val remove: (D.t, _, D.t, _) ctx -> Addr.t -> D.t +end + +module MakeMay (Arg: MayArg) = struct - include Make (Arg) + include Make (Arg.D) let name () = "mayLockset" let event ctx e octx = @@ -50,3 +52,27 @@ struct | _ -> ctx.local end + + +module type MustArg = +sig + include MayArg + val remove_all: (D.t, _, D.t, _) ctx -> D.t +end + +module MakeMust (Arg: MustArg) = +struct + include Make (Arg.D) + let name () = "mustLockset" + + let event ctx e octx = + match e with + | Events.Lock ((Addr (v, _) as a, _) as l) when not (Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset))) && not (ctx.ask (IsMultiple v)) -> + Arg.add ctx l + | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + Arg.remove_all ctx + | Events.Unlock l -> + Arg.remove ctx l + | _ -> + ctx.local +end diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 187fa1a5bb..0a9055df7b 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -13,6 +13,28 @@ let big_kernel_lock = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlob let console_sem = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[console semaphore]" intType)) let verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType)) +module Arg = +struct + module D = Lockset + + let add ctx l = + let nls = D.add l ctx.local in + if not (D.equal ctx.local nls) then + ctx.emit (MustLock (fst l)); + nls + + let remove ctx l = + ctx.emit (MustUnlock l); + D.remove (l, true) (D.remove (l, false) ctx.local) + + let remove_all ctx = + Mutexes.iter (fun m -> + ctx.emit (MustUnlock m) + ) (D.export_locks ctx.local); + (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *) + D.empty () +end + module type SpecParam = sig module G: Lattice.S @@ -23,34 +45,22 @@ end (** Mutex analyzer without base --- this is the new standard *) module MakeSpec (P: SpecParam) = struct - include Analyses.IdentitySpec - - (** name for the analysis (btw, it's "Only Mutex Must") *) + include LocksetAnalysis.MakeMust (Arg) let name () = "mutex" - (** Add current lockset alongside to the base analysis domain. Global data is collected using dirty side-effecting. *) - module D = Lockset - module C = Lockset + module D = Arg.D (* help type checker using explicit constraint *) + let should_join x y = D.equal x y - (** We do not add global state, so just lift from [BS]*) + (** Global data is collected using dirty side-effecting. *) module G = P.G module V = VarinfoV - let should_join x y = D.equal x y - let rec conv_offset_inv = function | `NoOffset -> `NoOffset | `Field (f, o) -> `Field (f, conv_offset_inv o) (* TODO: better indices handling *) | `Index (_, o) -> `Index (MyCFG.unknown_exp, conv_offset_inv o) - - - (** We just lift start state, global and dependency functions: *) - let startstate v = Lockset.empty () - let threadenter ctx lval f args = [Lockset.empty ()] - let exitstate v = Lockset.empty () - let query ctx (type a) (q: a Queries.t): a Queries.result = let non_overlapping locks1 locks2 = let intersect = G.join locks1 locks2 in @@ -125,24 +135,8 @@ struct | None -> M.info ~category:Unsound "Write to unknown address: privatization is unsound." end; ctx.local - | Events.Lock ((Addr (v, _) as a, _) as l) when not (Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset))) && not (ctx.ask (IsMultiple v)) -> - let nls = D.add l ctx.local in - if not (D.equal ctx.local nls) then - ctx.emit (MustLock (fst l)); - nls - | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> - (* unlock everything! *) - Mutexes.iter (fun m -> - ctx.emit (MustUnlock m) - ) (D.export_locks ctx.local); - (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *) - D.empty () - | Events.Unlock l -> - ctx.emit (MustUnlock l); - D.remove (l, true) (D.remove (l, false) ctx.local) | _ -> - ctx.local - + event ctx e octx end module MyParam = From f9233ccb643ce1bc9d1adb7ab8a87971853d1296 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 16:47:23 +0200 Subject: [PATCH 28/43] Comment lockset analysis cases --- src/analyses/locksetAnalysis.ml | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml index 12e8da85e9..46e014965a 100644 --- a/src/analyses/locksetAnalysis.ml +++ b/src/analyses/locksetAnalysis.ml @@ -40,15 +40,13 @@ struct let event ctx e octx = match e with | Events.Lock l -> - Arg.add ctx l + Arg.add ctx l (* add all locks, including blob and unknown *) | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> - (* unlock nothing *) - ctx.local + ctx.local (* don't remove any locks, including unknown itself *) | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> - (* unlock nothing *) - ctx.local + ctx.local (* don't remove non-unique lock *) | Events.Unlock l -> - Arg.remove ctx l + Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *) | _ -> ctx.local end @@ -67,12 +65,16 @@ struct let event ctx e octx = match e with - | Events.Lock ((Addr (v, _) as a, _) as l) when not (Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset))) && not (ctx.ask (IsMultiple v)) -> - Arg.add ctx l + | Events.Lock (a, _) when Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + ctx.local (* don't add unknown lock *) + | Events.Lock (Addr (v, _), _) when ctx.ask (IsMultiple v) -> + ctx.local (* don't add non-unique lock *) + | Events.Lock l -> + Arg.add ctx l (* add definite lock or none in parallel if ambiguous *) | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> - Arg.remove_all ctx + Arg.remove_all ctx (* remove all locks *) | Events.Unlock l -> - Arg.remove ctx l + Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *) | _ -> ctx.local end From 5829573a4e1010c7f69c4708741fe1d59c504cc1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 17:24:07 +0200 Subject: [PATCH 29/43] Replace unknown lock representation with Addr.UnknownPtr --- src/analyses/deadlock.ml | 5 ++--- src/analyses/locksetAnalysis.ml | 6 +++--- src/analyses/mutexEventsAnalysis.ml | 9 +++++++-- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index 985809466c..b8672ff84a 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -18,9 +18,8 @@ struct in let may_equal l1 l2 = match l1, l2 with - | {addr = a; _}, _ when Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> - true - | _, {addr = a; _} when Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + | {addr = UnknownPtr; _}, _ + | _, {addr = UnknownPtr; _} -> true | _, _ -> MyLock.equal l1 l2 in diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml index 46e014965a..3d4c65e516 100644 --- a/src/analyses/locksetAnalysis.ml +++ b/src/analyses/locksetAnalysis.ml @@ -41,7 +41,7 @@ struct match e with | Events.Lock l -> Arg.add ctx l (* add all locks, including blob and unknown *) - | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + | Events.Unlock UnknownPtr -> ctx.local (* don't remove any locks, including unknown itself *) | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) -> ctx.local (* don't remove non-unique lock *) @@ -65,13 +65,13 @@ struct let event ctx e octx = match e with - | Events.Lock (a, _) when Addr.equal a (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + | Events.Lock (UnknownPtr, _) -> ctx.local (* don't add unknown lock *) | Events.Lock (Addr (v, _), _) when ctx.ask (IsMultiple v) -> ctx.local (* don't add non-unique lock *) | Events.Lock l -> Arg.add ctx l (* add definite lock or none in parallel if ambiguous *) - | Events.Unlock l when Addr.equal l (Addr.from_var_offset (dummyFunDec.svar, `NoOffset)) -> + | Events.Unlock UnknownPtr -> Arg.remove_all ctx (* remove all locks *) | Events.Unlock l -> Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 267f7eb0ee..1b8cd6da55 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -39,9 +39,14 @@ struct 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 Queries.LS.is_top a -> - [ValueDomain.Addr.from_var_offset (dummyFunDec.svar, `NoOffset)] + [Addr.UnknownPtr] | a -> - Queries.LS.fold gather_addr a [] + let top_elt = (dummyFunDec.svar, `NoOffset) in + let addrs = Queries.LS.fold gather_addr (Queries.LS.remove top_elt a) [] in + if Queries.LS.mem top_elt a then + Addr.UnknownPtr :: addrs + else + addrs let lock ctx rw may_fail nonzero_return_when_aquired a lv arg = match lv with From d805791602dfbd2881b907b537c7ecef5076949f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 17:25:34 +0200 Subject: [PATCH 30/43] Remove duplicate special lock definitions from mutex analysis --- src/analyses/mutexAnalysis.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 0a9055df7b..2272b0a0c1 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -9,10 +9,6 @@ open Prelude.Ana open Analyses 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 verifier_atomic = LockDomain.Addr.from_var (Goblintutil.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType)) - module Arg = struct module D = Lockset @@ -102,7 +98,7 @@ struct ls | Queries.MustBeAtomic -> let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in - Mutexes.mem verifier_atomic held_locks + Mutexes.mem MutexEventsAnalysis.verifier_atomic held_locks | _ -> Queries.Result.top q module A = From 76b7ddc10e36685be9217067f2a9b15201ec6e88 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 24 Mar 2022 18:17:20 +0200 Subject: [PATCH 31/43] Remove unused opens, add delegation comment --- src/analyses/deadlock.ml | 1 - src/analyses/locksetAnalysis.ml | 3 +-- src/analyses/mutexAnalysis.ml | 2 +- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index b8672ff84a..3f973dce87 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -3,7 +3,6 @@ open Prelude.Ana open Analyses open DeadlockDomain -open ValueDomain let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref [] diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml index 3d4c65e516..78b0a21eca 100644 --- a/src/analyses/locksetAnalysis.ml +++ b/src/analyses/locksetAnalysis.ml @@ -2,7 +2,6 @@ open Prelude.Ana open Analyses -open ValueDomain module type DS = @@ -29,7 +28,7 @@ module type MayArg = sig module D: DS val add: (D.t, _, D.t, _) ctx -> LockDomain.Lockset.Lock.t -> D.t - val remove: (D.t, _, D.t, _) ctx -> Addr.t -> D.t + val remove: (D.t, _, D.t, _) ctx -> ValueDomain.Addr.t -> D.t end module MakeMay (Arg: MayArg) = diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 2272b0a0c1..cc077b5698 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -132,7 +132,7 @@ struct end; ctx.local | _ -> - event ctx e octx + event ctx e octx (* delegate to must lockset analysis *) end module MyParam = From aec788ef1b784f41d9bf9fb5289b49d9e7dcae77 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 25 Mar 2022 13:46:00 +0200 Subject: [PATCH 32/43] Rename query CurrentLockset -> MustLockset --- src/analyses/commonPriv.ml | 2 +- src/analyses/mutexAnalysis.ml | 2 +- src/analyses/osek.ml | 2 +- src/domains/queries.ml | 8 ++++---- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 98e140f86c..a12ed5a0fd 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -127,7 +127,7 @@ struct if !GU.global_initialization then Lockset.empty () else - let ls = ask.f Queries.CurrentLockset in + let ls = ask.f Queries.MustLockset in Q.LS.fold (fun (var, offs) acc -> Lockset.add (Lock.from_var_offset (var, conv_offset offs)) acc ) ls (Lockset.empty ()) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index cc077b5698..164647ae64 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -87,7 +87,7 @@ struct true else *) G.leq (ctx.global global) held_locks - | Queries.CurrentLockset -> + | Queries.MustLockset -> let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in let ls = Mutexes.fold (fun addr ls -> match Addr.to_var_offset addr with diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml index b6416c8a4b..05a26f3975 100644 --- a/src/analyses/osek.ml +++ b/src/analyses/osek.ml @@ -586,7 +586,7 @@ struct (* offpry_flags flagstate v *) (* end *) in off > pry - | Queries.CurrentLockset -> (* delegate for MinePriv *) + | Queries.MustLockset -> (* delegate for MinePriv *) (* TODO: delegate other queries? *) M.query ctx q | _ -> Queries.Result.top q diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 1dc44b3002..93b559f5e3 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -73,7 +73,7 @@ type _ t = | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *) | MayBePublicWithout: maybepublicwithout -> MayBool.t t | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t - | CurrentLockset: LS.t t + | MustLockset: LS.t t | MustBeAtomic: MustBool.t t | MustBeSingleThreaded: MustBool.t t | MustBeUniqueThread: MustBool.t t @@ -120,7 +120,7 @@ struct | MayPointTo _ -> (module LS) | ReachableFrom _ -> (module LS) | Regions _ -> (module LS) - | CurrentLockset -> (module LS) + | MustLockset -> (module LS) | EvalFunvar _ -> (module LS) | ReachableUkTypes _ -> (module TS) | MayEscape _ -> (module MayBool) @@ -171,7 +171,7 @@ struct | MayPointTo _ -> LS.top () | ReachableFrom _ -> LS.top () | Regions _ -> LS.top () - | CurrentLockset -> LS.top () + | MustLockset -> LS.top () | EvalFunvar _ -> LS.top () | ReachableUkTypes _ -> TS.top () | MayEscape _ -> MayBool.top () @@ -224,7 +224,7 @@ struct | Any (MayBePublic _) -> 7 | Any (MayBePublicWithout _) -> 8 | Any (MustBeProtectedBy _) -> 9 - | Any CurrentLockset -> 10 + | Any MustLockset -> 10 | Any MustBeAtomic -> 11 | Any MustBeSingleThreaded -> 12 | Any MustBeUniqueThread -> 13 From f5a7432cdfb85cd180a78fc198e556ee52cef002 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 25 Mar 2022 13:54:45 +0200 Subject: [PATCH 33/43] Move must lockset change check to mutex privatizations --- src/analyses/basePriv.ml | 52 +++++++++++++++++++++-------------- src/analyses/mutexAnalysis.ml | 3 +- 2 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 7d8d7179f2..da6c7b121b 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -276,18 +276,23 @@ struct cpa' *) let lock ask getg (st: BaseComponents (D).t) m = - let get_m = get_m_with_mutex_inits ask getg m in - (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events, - where our (necessary) original context still has the mutex, - so the query would be on the wrong lockset. - TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029. - Therefore, just use _without to exclude the mutex we shouldn't have. - In non-cond locks we don't have it anyway, so there's no difference. - No other privatization uses is_unprotected, so this hack is only needed here. *) - let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in - let cpa' = CPA.filter is_in_V get_m in - if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a\n" LockDomain.Addr.pretty m CPA.pretty cpa'; - {st with cpa = CPA.fold CPA.add cpa' st.cpa} + if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + let get_m = get_m_with_mutex_inits ask getg m in + (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events, + where our (necessary) original context still has the mutex, + so the query would be on the wrong lockset. + TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029. + Therefore, just use _without to exclude the mutex we shouldn't have. + In non-cond locks we don't have it anyway, so there's no difference. + No other privatization uses is_unprotected, so this hack is only needed here. *) + let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in + let cpa' = CPA.filter is_in_V get_m in + if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a\n" LockDomain.Addr.pretty m CPA.pretty cpa'; + {st with cpa = CPA.fold CPA.add cpa' st.cpa} + ) + else + st (* sound w.r.t. recursive lock *) + let unlock ask getg sideg (st: BaseComponents (D).t) m = let is_in_Gm x _ = is_protected_by ask m x in let side_m_cpa = CPA.filter is_in_Gm st.cpa in @@ -351,15 +356,20 @@ struct ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" d_varinfo x VD.pretty v CPA.pretty cpa'); cpa' *) - let lock ask getg (st: BaseComponents (D).t) m = - let get_m = get_m_with_mutex_inits ask getg m in - (* Additionally filter get_m in case it contains variables it no longer protects. *) - let is_in_Gm x _ = is_protected_by ask m x in - let get_m = CPA.filter is_in_Gm get_m in - let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in - let meet = long_meet st.cpa get_m in - if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a\n" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet; - {st with cpa = meet} + let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m = + if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + let get_m = get_m_with_mutex_inits ask getg m in + (* Additionally filter get_m in case it contains variables it no longer protects. *) + let is_in_Gm x _ = is_protected_by ask m x in + let get_m = CPA.filter is_in_Gm get_m in + let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in + let meet = long_meet st.cpa get_m in + if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a\n" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet; + {st with cpa = meet} + ) + else + st (* sound w.r.t. recursive lock *) + let unlock ask getg sideg (st: BaseComponents (D).t) m = let is_in_Gm x _ = is_protected_by ask m x in sideg (V.mutex m) (CPA.filter is_in_Gm st.cpa); diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 164647ae64..a6377cb3ea 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -15,8 +15,7 @@ struct let add ctx l = let nls = D.add l ctx.local in - if not (D.equal ctx.local nls) then - ctx.emit (MustLock (fst l)); + ctx.emit (MustLock (fst l)); nls let remove ctx l = From 531a83104381df9fd3e3edbc54b96d4975033ea2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 25 Mar 2022 14:46:00 +0200 Subject: [PATCH 34/43] Remove MustLock & MustUnlock events --- src/analyses/apron/apronAnalysis.apron.ml | 4 ++-- src/analyses/base.ml | 4 ++-- src/analyses/mutexAnalysis.ml | 10 ++++------ src/domains/events.ml | 4 ---- 4 files changed, 8 insertions(+), 14 deletions(-) diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index cae8031962..c008236d0d 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -411,9 +411,9 @@ struct let event ctx e aprx = let st = ctx.local in match e with - | Events.MustLock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) Priv.lock (Analyses.ask_of_ctx aprx) aprx.global st addr - | Events.MustUnlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) Priv.unlock (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st addr (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *) | Events.EnterMultiThreaded -> diff --git a/src/analyses/base.ml b/src/analyses/base.ml index d5aecde6a5..d6276e7a0c 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2367,10 +2367,10 @@ struct let event ctx e octx = let st: store = ctx.local in match e with - | Events.MustLock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr; Priv.lock (Analyses.ask_of_ctx octx) (priv_getg octx.global) st addr - | Events.MustUnlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) Priv.unlock (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st addr | Events.Escape escaped -> Priv.escape (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st escaped diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index a6377cb3ea..662a971ef1 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -14,18 +14,16 @@ struct module D = Lockset let add ctx l = - let nls = D.add l ctx.local in - ctx.emit (MustLock (fst l)); - nls + D.add l ctx.local let remove ctx l = - ctx.emit (MustUnlock l); D.remove (l, true) (D.remove (l, false) ctx.local) let remove_all ctx = - Mutexes.iter (fun m -> + (* TODO: implement in privatizations? *) + (* Mutexes.iter (fun m -> ctx.emit (MustUnlock m) - ) (D.export_locks ctx.local); + ) (D.export_locks ctx.local); *) (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *) D.empty () end diff --git a/src/domains/events.ml b/src/domains/events.ml index e6efb99bd6..7629da173d 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -1,8 +1,6 @@ open Prelude.Ana type t = - | MustLock of LockDomain.Addr.t (** This is only emitted if the mutex was not previously held *) - | MustUnlock of LockDomain.Addr.t | Lock of LockDomain.Lockset.Lock.t | Unlock of LockDomain.Addr.t | Escape of EscapeDomain.EscapedVars.t @@ -13,8 +11,6 @@ type t = | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) let pretty () = function - | MustLock m -> dprintf "MustLock %a" LockDomain.Addr.pretty m - | MustUnlock m -> dprintf "MustUnlock %a" LockDomain.Addr.pretty m | Lock m -> dprintf "Lock %a" LockDomain.Lockset.Lock.pretty m | Unlock m -> dprintf "Unlock %a" LockDomain.Addr.pretty m | Escape escaped -> dprintf "Escape %a" EscapeDomain.EscapedVars.pretty escaped From a6777d91fb30593159fee22d96ad67ab0b44f826 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 25 Mar 2022 14:50:14 +0200 Subject: [PATCH 35/43] Use event ctx for privatizations instead of octx --- src/analyses/apron/apronAnalysis.apron.ml | 8 ++++---- src/analyses/base.ml | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index c008236d0d..133bedec6e 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -408,16 +408,16 @@ struct let threadspawn ctx lval f args fctx = ctx.local - let event ctx e aprx = + let event ctx e octx = let st = ctx.local in match e with | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - Priv.lock (Analyses.ask_of_ctx aprx) aprx.global st addr + Priv.lock (Analyses.ask_of_ctx octx) octx.global st addr | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - Priv.unlock (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st addr + Priv.unlock (Analyses.ask_of_ctx octx) octx.global octx.sideg st addr (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *) | Events.EnterMultiThreaded -> - Priv.enter_multithreaded (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st + Priv.enter_multithreaded (Analyses.ask_of_ctx octx) octx.global octx.sideg st | _ -> st diff --git a/src/analyses/base.ml b/src/analyses/base.ml index d6276e7a0c..1383824e41 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2369,13 +2369,13 @@ struct match e with | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr; - Priv.lock (Analyses.ask_of_ctx octx) (priv_getg octx.global) st addr + Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - Priv.unlock (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st addr + Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr | Events.Escape escaped -> - Priv.escape (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st escaped + Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped | Events.EnterMultiThreaded -> - Priv.enter_multithreaded (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st + Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st | Events.AssignSpawnedThread (lval, tid) -> (* TODO: is this type right? *) set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid)) From 5f6b574eda6fc63c1068b4dd3fd9a8fb8cb2321e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Mar 2022 11:20:07 +0300 Subject: [PATCH 36/43] Fix deadlock detection with unknown pointers --- src/analyses/deadlock.ml | 17 ++++---- .../15-deadlock/21-unknown_deadlock.c | 6 +-- .../15-deadlock/23-unknown_unlock_deadlock.c | 6 +-- .../15-deadlock/26-unknown_deadlock2.c | 41 +++++++++++++++++++ 4 files changed, 56 insertions(+), 14 deletions(-) create mode 100644 tests/regression/15-deadlock/26-unknown_deadlock2.c diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index 8b927ff596..75a8f98562 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -31,12 +31,6 @@ struct in ctx.sideg (Tuple3.first before) d - (* let may_equal l1 l2 = match l1, l2 with - | (ValueDomain.Addr.UnknownPtr, _, _), _ - | _, (ValueDomain.Addr.UnknownPtr, _, _) -> - true - | _, _ -> Lock.equal l1 l2 *) - let part_access ctx: MCPAccess.A.t = Obj.obj (ctx.ask (PartAccess Point)) @@ -67,15 +61,22 @@ struct (* TODO: find all cycles/SCCs *) let global_visited_locks = LH.create 100 in + let may_equal l1 l2 = match l1, l2 with + | ValueDomain.Addr.UnknownPtr, _ + | _, ValueDomain.Addr.UnknownPtr -> + true + | _, _ -> Lock.equal l1 l2 + in + (* DFS *) let rec iter_lock (path_visited_locks: LS.t) (path_visited_lock_event_pairs: LockEventPair.t list) (lock: Lock.t) = - if LS.mem lock path_visited_locks then ( + if LS.mem lock path_visited_locks || LS.mem ValueDomain.Addr.UnknownPtr path_visited_locks || (not (LS.is_empty path_visited_locks) && lock = ValueDomain.Addr.UnknownPtr) then ( (* cycle may not return to first lock, but an intermediate one, cut off the non-cyclic stem *) let path_visited_lock_event_pairs = (* path_visited_lock_event_pairs cannot be empty *) List.hd path_visited_lock_event_pairs :: List.take_while (fun (_, (after_lock, _, _)) -> - not (Lock.equal after_lock lock) + not (may_equal after_lock lock) ) (List.tl path_visited_lock_event_pairs) in let mhp = diff --git a/tests/regression/15-deadlock/21-unknown_deadlock.c b/tests/regression/15-deadlock/21-unknown_deadlock.c index 3bf73d61e0..c68c76b592 100644 --- a/tests/regression/15-deadlock/21-unknown_deadlock.c +++ b/tests/regression/15-deadlock/21-unknown_deadlock.c @@ -8,8 +8,8 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; void *t1(void *arg) { - pthread_mutex_lock(&mutex1); - pthread_mutex_lock(&mutex2); // DEADLOCK + pthread_mutex_lock(&mutex1); // TODO DEADLOCK? + pthread_mutex_lock(&mutex2); // TODO DEADLOCK? g1 = g2 + 1; pthread_mutex_unlock(&mutex2); pthread_mutex_unlock(&mutex1); @@ -19,7 +19,7 @@ void *t1(void *arg) { void *t2(void *arg) { int k = rand() % 2; pthread_mutex_t *m; // unknown - pthread_mutex_lock(m); + pthread_mutex_lock(m); // DEADLOCK pthread_mutex_lock(&mutex1); // DEADLOCK g2 = g1 + 1; pthread_mutex_unlock(&mutex1); diff --git a/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c b/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c index 80d9aca93a..be54b8693f 100644 --- a/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c +++ b/tests/regression/15-deadlock/23-unknown_unlock_deadlock.c @@ -8,8 +8,8 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; void *t1(void *arg) { - pthread_mutex_lock(&mutex1); - pthread_mutex_lock(&mutex2); // DEADLOCK + pthread_mutex_lock(&mutex1); // TODO DEADLOCK? + pthread_mutex_lock(&mutex2); // TODO DEADLOCK? g1 = g2 + 1; pthread_mutex_unlock(&mutex2); pthread_mutex_unlock(&mutex1); @@ -19,7 +19,7 @@ void *t1(void *arg) { void *t2(void *arg) { int k = rand() % 2; pthread_mutex_t *m, *n; // unknown - pthread_mutex_lock(m); + pthread_mutex_lock(m); // DEADLOCK pthread_mutex_unlock(n); pthread_mutex_lock(&mutex1); // DEADLOCK g2 = g1 + 1; diff --git a/tests/regression/15-deadlock/26-unknown_deadlock2.c b/tests/regression/15-deadlock/26-unknown_deadlock2.c new file mode 100644 index 0000000000..398ff4e95b --- /dev/null +++ b/tests/regression/15-deadlock/26-unknown_deadlock2.c @@ -0,0 +1,41 @@ +// PARAM: --set ana.activated[+] deadlock +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex2); // TODO DEADLOCK? + pthread_mutex_lock(&mutex1); // TODO DEADLOCK? + g1 = g2 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(&mutex2); + return NULL; +} + +void *t2(void *arg) { + int k = rand() % 2; + pthread_mutex_t *m; // unknown + pthread_mutex_lock(&mutex1); // DEADLOCK + pthread_mutex_lock(m); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(m); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 1000000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From e37fa65978e486d0c7f9a9baa7b24231dc776469 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Mar 2022 11:22:35 +0300 Subject: [PATCH 37/43] Add extra DEADLOCK annotations to added tests --- tests/regression/15-deadlock/19-fail_deadlock.c | 4 ++-- tests/regression/15-deadlock/20-ambig_deadlock.c | 4 ++-- tests/regression/15-deadlock/22-ambig_unlock_deadlock.c | 4 ++-- tests/regression/15-deadlock/24-malloc_unlock_deadlock.c | 4 ++-- tests/regression/15-deadlock/25-malloc_deadlock.c | 4 ++-- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/tests/regression/15-deadlock/19-fail_deadlock.c b/tests/regression/15-deadlock/19-fail_deadlock.c index 57973371b2..0d35f7a2b5 100644 --- a/tests/regression/15-deadlock/19-fail_deadlock.c +++ b/tests/regression/15-deadlock/19-fail_deadlock.c @@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; void *t1(void *arg) { - pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex1); // DEADLOCK pthread_mutex_lock(&mutex2); // DEADLOCK g1 = g2 + 1; pthread_mutex_unlock(&mutex2); @@ -16,7 +16,7 @@ void *t1(void *arg) { } void *t2(void *arg) { - pthread_mutex_lock(&mutex2); + pthread_mutex_lock(&mutex2); // DEADLOCK pthread_mutex_lock(&mutex1); // DEADLOCK g2 = g1 + 1; pthread_mutex_unlock(&mutex1); diff --git a/tests/regression/15-deadlock/20-ambig_deadlock.c b/tests/regression/15-deadlock/20-ambig_deadlock.c index 74b50dd7e1..69e47a4d33 100644 --- a/tests/regression/15-deadlock/20-ambig_deadlock.c +++ b/tests/regression/15-deadlock/20-ambig_deadlock.c @@ -8,7 +8,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; void *t1(void *arg) { - pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex1); // DEADLOCK pthread_mutex_lock(&mutex2); // DEADLOCK g1 = g2 + 1; pthread_mutex_unlock(&mutex2); @@ -23,7 +23,7 @@ void *t2(void *arg) { m = &mutex2; else m = &mutex3; - pthread_mutex_lock(m); + pthread_mutex_lock(m); // DEADLOCK pthread_mutex_lock(&mutex1); // DEADLOCK g2 = g1 + 1; pthread_mutex_unlock(&mutex1); diff --git a/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c b/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c index ec22bff992..52009f9c14 100644 --- a/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c +++ b/tests/regression/15-deadlock/22-ambig_unlock_deadlock.c @@ -8,7 +8,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER; void *t1(void *arg) { - pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex1); // DEADLOCK pthread_mutex_lock(&mutex2); // DEADLOCK g1 = g2 + 1; pthread_mutex_unlock(&mutex2); @@ -28,7 +28,7 @@ void *t2(void *arg) { n = &mutex2; else n = &mutex3; - pthread_mutex_lock(m); + pthread_mutex_lock(m); // DEADLOCK pthread_mutex_unlock(n); pthread_mutex_lock(&mutex1); // DEADLOCK g2 = g1 + 1; diff --git a/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c b/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c index 890257e44e..2a1aa9dd6f 100644 --- a/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c +++ b/tests/regression/15-deadlock/24-malloc_unlock_deadlock.c @@ -6,7 +6,7 @@ int g1, g2; pthread_mutex_t *p, *q; void *t1(void *arg) { - pthread_mutex_lock(p); + pthread_mutex_lock(p); // DEADLOCK pthread_mutex_lock(q); // DEADLOCK g1 = g2 + 1; pthread_mutex_unlock(q); @@ -15,7 +15,7 @@ void *t1(void *arg) { } void *t2(void *arg) { - pthread_mutex_lock(p); + pthread_mutex_lock(p); // DEADLOCK pthread_mutex_unlock(p); pthread_mutex_lock(q); // DEADLOCK g2 = g1 + 1; diff --git a/tests/regression/15-deadlock/25-malloc_deadlock.c b/tests/regression/15-deadlock/25-malloc_deadlock.c index 72a86f7824..535bbf607c 100644 --- a/tests/regression/15-deadlock/25-malloc_deadlock.c +++ b/tests/regression/15-deadlock/25-malloc_deadlock.c @@ -6,7 +6,7 @@ int g1, g2; pthread_mutex_t *p, *q; void *t1(void *arg) { - pthread_mutex_lock(p); + pthread_mutex_lock(p); // DEADLOCK pthread_mutex_lock(q); // DEADLOCK g1 = g2 + 1; pthread_mutex_unlock(q); @@ -15,7 +15,7 @@ void *t1(void *arg) { } void *t2(void *arg) { - pthread_mutex_lock(p); + pthread_mutex_lock(p); // DEADLOCK pthread_mutex_lock(q); // DEADLOCK g2 = g1 + 1; pthread_mutex_unlock(q); From d163dff3277aee393e6a0091d6533097264697be Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Mar 2022 11:25:44 +0300 Subject: [PATCH 38/43] Fix event ctx in apron privatizations Incorrect in a6777d91fb30593159fee22d96ad67ab0b44f826. --- src/analyses/apron/apronAnalysis.apron.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 133bedec6e..1e025bac08 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -412,12 +412,12 @@ struct let st = ctx.local in match e with | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - Priv.lock (Analyses.ask_of_ctx octx) octx.global st addr + Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) - Priv.unlock (Analyses.ask_of_ctx octx) octx.global octx.sideg st addr + Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *) | Events.EnterMultiThreaded -> - Priv.enter_multithreaded (Analyses.ask_of_ctx octx) octx.global octx.sideg st + Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st | _ -> st From 31ec82799533db30a8ab535b6f1a5c9b9136fba5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 29 Mar 2022 17:20:20 +0300 Subject: [PATCH 39/43] Add self deadlock test --- .../regression/15-deadlock/27-self_deadlock.c | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 tests/regression/15-deadlock/27-self_deadlock.c diff --git a/tests/regression/15-deadlock/27-self_deadlock.c b/tests/regression/15-deadlock/27-self_deadlock.c new file mode 100644 index 0000000000..04b34b4a03 --- /dev/null +++ b/tests/regression/15-deadlock/27-self_deadlock.c @@ -0,0 +1,38 @@ +// PARAM: --set ana.activated[+] deadlock +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); // DEADLOCK + pthread_mutex_lock(&mutex1); // DEADLOCK + g1 = g2 + 1; + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + pthread_mutex_lock(&mutex2); // DEADLOCK + pthread_mutex_lock(&mutex2); // DEADLOCK + g2 = g1 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex2); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + for (i = 0; i < 10000; i++) { + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + } + return 0; +} From 9894c038914c0913ee048d2baac84b2fa487880b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 31 Mar 2022 14:07:24 +0300 Subject: [PATCH 40/43] Add privatization warnings about unsound unknown mutex unlock --- src/analyses/apron/apronAnalysis.apron.ml | 2 ++ src/analyses/base.ml | 2 ++ src/analyses/mutexAnalysis.ml | 1 - 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 1e025bac08..f99d5f3efa 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -414,6 +414,8 @@ struct | Events.Lock (addr, _) when ThreadFlag.is_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.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + if addr = UnknownPtr then + M.info ~category:Unsound "Unknown mutex unlocked, apron privatization unsound"; (* TODO: something more sound *) Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *) | Events.EnterMultiThreaded -> diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1383824e41..1aa137c76e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2371,6 +2371,8 @@ struct if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr; Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *) + if addr = UnknownPtr then + M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *) Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr | Events.Escape escaped -> Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 3ed7ab0e03..02a6d1f1ad 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -33,7 +33,6 @@ struct D.remove (l, true) (D.remove (l, false) ctx.local) let remove_all ctx = - (* TODO: implement in privatizations? *) (* Mutexes.iter (fun m -> ctx.emit (MustUnlock m) ) (D.export_locks ctx.local); *) From e93fc694e2a04708d2a89bc3378328c8575203e2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 31 Mar 2022 14:14:57 +0300 Subject: [PATCH 41/43] Deduplicate and fix conv_offset_inv --- src/analyses/mutexAnalysis.ml | 9 +++++++-- src/analyses/mutexEventsAnalysis.ml | 7 ------- 2 files changed, 7 insertions(+), 9 deletions(-) diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 02a6d1f1ad..e5602f9ea7 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -52,8 +52,13 @@ struct let rec conv_offset_inv = function | `NoOffset -> `NoOffset | `Field (f, o) -> `Field (f, conv_offset_inv o) - (* TODO: better indices handling *) - | `Index (_, o) -> `Index (MyCFG.unknown_exp, conv_offset_inv o) + | `Index (i, o) -> + let i_exp = + match ValueDomain.IndexDomain.to_int i with + | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i))) + | None -> MyCFG.unknown_exp + in + `Index (i_exp, conv_offset_inv o) let query ctx (type a) (q: a Queries.t): a Queries.result = let non_overlapping locks1 locks2 = diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 1b8cd6da55..9c3f6647cb 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -28,13 +28,6 @@ struct | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o) | `Field (f,o) -> `Field (f, conv_offset o) - let rec conv_offset_inv = function - | `NoOffset -> `NoOffset - | `Field (f, o) -> `Field (f, conv_offset_inv o) - (* TODO: better indices handling *) - | `Index (_, o) -> `Index (MyCFG.unknown_exp, conv_offset_inv 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 From 518b9e1f0d37eacd3cbb8d5878c1a67a1915334d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 31 Mar 2022 14:20:45 +0300 Subject: [PATCH 42/43] Update mutex analyses comments --- src/analyses/mayLocks.ml | 2 +- src/analyses/mutexAnalysis.ml | 3 +-- src/analyses/mutexEventsAnalysis.ml | 5 ++--- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 8b026316eb..20cffa6afb 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -1,4 +1,4 @@ -(** May-lockset analysis. *) +(** May lockset analysis (unused). *) open Prelude.Ana open Analyses diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index e5602f9ea7..18459b4d7e 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -1,4 +1,4 @@ -(** Mutex analysis. *) +(** Protecting mutex analysis. Must locksets locally and for globals. *) module M = Messages module Addr = ValueDomain.Addr @@ -17,7 +17,6 @@ sig val check_fun: ?write:bool -> Lockset.t -> G.t end -(** Mutex analyzer without base --- this is the new standard *) module MakeSpec (P: SpecParam) = struct module Arg = diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 9c3f6647cb..474ec3f63d 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -1,4 +1,4 @@ -(** Mutex analysis. *) +(** Mutex events analysis (Lock and Unlock). *) module M = Messages module Addr = ValueDomain.Addr @@ -19,8 +19,7 @@ struct let name () = "mutexEvents" - (* NB! Currently we care only about concrete indexes. Base (seeing only a int domain - element) answers with the string "unknown" on all non-concrete cases. *) + (* Currently we care only about concrete indexes. *) let rec conv_offset x = match x with | `NoOffset -> `NoOffset From 575a94ac413d742025fb29d612dc107e21275bca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 31 Mar 2022 14:35:51 +0300 Subject: [PATCH 43/43] Add relocking check to apron mutex-meet variants as well --- src/analyses/apron/apronPriv.apron.ml | 39 ++++++++++++++++----------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml index 0fe1b7b197..b2e0a64999 100644 --- a/src/analyses/apron/apronPriv.apron.ml +++ b/src/analyses/apron/apronPriv.apron.ml @@ -438,12 +438,17 @@ struct {st with apr = apr_local'} let lock ask getg (st: apron_components_t) m = - let apr = st.apr in - let get_m = get_m_with_mutex_inits ask getg m in - (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *) - let get_m = keep_only_protected_globals ask m get_m in - let apr' = AD.meet apr get_m in - {st with apr = apr'} + (* TODO: somehow actually unneeded here? *) + if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + let apr = st.apr in + let get_m = get_m_with_mutex_inits ask getg m in + (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *) + let get_m = keep_only_protected_globals ask m get_m in + let apr' = AD.meet apr get_m in + {st with apr = apr'} + ) + else + st (* sound w.r.t. recursive lock *) let unlock ask getg sideg (st: apron_components_t) m: apron_components_t = let apr = st.apr in @@ -942,15 +947,19 @@ struct {apr = apr_local'; priv = (W.add g w,LMust.add lm lmust,l')} let lock ask getg (st: apron_components_t) m = - let apr = st.apr in - let _,lmust,l = st.priv in - let lm = LLock.mutex m in - let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in - let local_m = BatOption.default (LAD.bot ()) (L.find_opt lm l) in - (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *) - let local_m = Cluster.keep_only_protected_globals ask m local_m in - let apr = Cluster.lock apr local_m get_m in - {st with apr} + if Locksets.(not (Lockset.mem m (current_lockset ask))) then ( + let apr = st.apr in + let _,lmust,l = st.priv in + let lm = LLock.mutex m in + let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in + let local_m = BatOption.default (LAD.bot ()) (L.find_opt lm l) in + (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *) + let local_m = Cluster.keep_only_protected_globals ask m local_m in + let apr = Cluster.lock apr local_m get_m in + {st with apr} + ) + else + st (* sound w.r.t. recursive lock *) let unlock ask getg sideg (st: apron_components_t) m: apron_components_t = let apr = st.apr in