diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9029c1b4a1..3bfb8711a9 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -15,7 +15,38 @@ module Spec = struct module Arg = struct - module D = Lockset + module Multiplicity = struct + (* the maximum multiplicity which we keep track of precisely *) + let max_count () = 4 + + module Count = Lattice.Reverse( + Lattice.Chain (struct + let n () = max_count () + 1 + let names x = if x = max_count () then Format.asprintf ">= %d" x else Format.asprintf "%d" x + end) + ) + + include MapDomain.MapTop_LiftBot (ValueDomain.Addr) (Count) + + let increment v x = + let current = find v x in + if current = max_count () then + x + else + add v (current + 1) x + + let decrement v x = + let current = find v x in + if current = 0 then + (x, true) + else + (add v (current - 1) x, current - 1 = 0) + end + + module D = struct include Lattice.Prod(Lockset)(Multiplicity) + let empty () = (Lockset.empty (), Multiplicity.empty ()) + end + (** Global data is collected using dirty side-effecting. *) @@ -111,12 +142,28 @@ struct let create_protected protected = `Lifted2 protected end - let add ctx l = - D.add l ctx.local + let add ctx (l:Mutexes.elt*bool) = + let s,m = ctx.local in + let s' = Lockset.add l s in + match Addr.to_mval (fst l) with + | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval -> + (s', Multiplicity.increment (fst l) m) + | _ -> (s', m) + + let remove' ctx ~warn l = + let s, m = ctx.local in + let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in + if warn && (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex which may not be held"; + match Addr.to_mval l with + | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval -> + let m',rmed = Multiplicity.decrement l m in + if rmed then + (rm s, m') + else + (s, m') + | _ -> (rm s, m) - let remove ctx l = - if not (D.mem (l,true) ctx.local || D.mem (l,false) ctx.local) then M.warn "unlocking mutex which may not be held"; - D.remove (l, true) (D.remove (l, false) ctx.local) + let remove = remove' ~warn:true let remove_all ctx = (* Mutexes.iter (fun m -> @@ -124,7 +171,9 @@ struct ) (D.export_locks ctx.local); *) (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *) M.warn "unlocking unknown mutex which may not be held"; - D.empty () + (Lockset.empty (), Multiplicity.empty ()) + + let empty () = (Lockset.empty (), Multiplicity.empty ()) end include LocksetAnalysis.MakeMust (Arg) let name () = "mutex" @@ -149,22 +198,23 @@ struct sum_protected := 0 let query ctx (type a) (q: a Queries.t): a Queries.result = + let ls, m = ctx.local in (* get the set of mutexes protecting the variable v in the given mode *) let protecting ~write mode v = GProtecting.get ~write mode (G.protecting (ctx.global (V.protecting v))) in let non_overlapping locks1 locks2 = Mutexes.is_empty @@ Mutexes.inter locks1 locks2 in match q with - | Queries.MayBePublic _ when Lockset.is_bot ctx.local -> false + | Queries.MayBePublic _ when Lockset.is_bot ls -> false | Queries.MayBePublic {global=v; write; protection} -> - let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in + let held_locks = Lockset.export_locks (Lockset.filter snd ls) in let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if Mutexes.mem verifier_atomic (Lockset.export_locks ctx.local) then false else *) non_overlapping held_locks protecting - | Queries.MayBePublicWithout _ when Lockset.is_bot ctx.local -> false + | Queries.MayBePublicWithout _ when Lockset.is_bot ls -> false | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} -> - let held_locks = Lockset.export_locks (Lockset.remove (without_mutex, true) (Lockset.filter snd ctx.local)) in + let held_locks = Lockset.export_locks @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in let protecting = protecting ~write protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then @@ -180,7 +230,7 @@ struct else *) Mutexes.leq mutex_lockset protecting | Queries.MustLockset -> - let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in + let held_locks = Lockset.export_locks (Lockset.filter snd ls) in let ls = Mutexes.fold (fun addr ls -> match Addr.to_mval addr with | Some (var, offs) -> Queries.LS.add (var, Addr.Offs.to_exp offs) ls @@ -189,7 +239,7 @@ struct in ls | Queries.MustBeAtomic -> - let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in + let held_locks = Lockset.export_locks (Lockset.filter snd ls) in Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks | Queries.MustProtectedVars {mutex = m; write} -> let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in @@ -221,23 +271,23 @@ struct module A = struct - include D + include Lockset let name () = "lock" let may_race ls1 ls2 = (* not mutually exclusive *) - not @@ D.exists (fun ((m1, w1) as l1) -> + not @@ exists (fun ((m1, w1) as l1) -> if w1 then (* write lock is exclusive with write lock or read lock *) - D.mem l1 ls2 || D.mem (m1, false) ls2 + mem l1 ls2 || mem (m1, false) ls2 else (* read lock is exclusive with just write lock *) - D.mem (m1, true) ls2 + mem (m1, true) ls2 ) ls1 let should_print ls = not (is_empty ls) end let access ctx (a: Queries.access) = - ctx.local + fst ctx.local let event ctx e octx = match e with @@ -249,8 +299,8 @@ struct (*privatization*) match var_opt with | Some v -> - if not (Lockset.is_bot octx.local) then - let locks = Lockset.export_locks (Lockset.filter snd octx.local) in + if not (Lockset.is_bot (fst octx.local)) then + let locks = Lockset.export_locks (Lockset.filter snd (fst octx.local)) in let write = match kind with | Write | Free -> true | Read -> false diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml index 468b656372..00e49260b4 100644 --- a/src/analyses/mutexTypeAnalysis.ml +++ b/src/analyses/mutexTypeAnalysis.ml @@ -71,5 +71,8 @@ struct | _ -> Queries.Result.top q end +let must_be_recursive ctx (v,o) = + ctx.ask (Queries.MutexType (v, Offset.Unit.of_offs o)) = `Lifted MutexAttrDomain.MutexKind.Recursive + let _ = MCP.register_analysis (module Spec : MCPSpec) diff --git a/tests/regression/71-doublelocking/14-rec-dyn-no-race.c b/tests/regression/71-doublelocking/14-rec-dyn-no-race.c new file mode 100644 index 0000000000..b49f481eee --- /dev/null +++ b/tests/regression/71-doublelocking/14-rec-dyn-no-race.c @@ -0,0 +1,45 @@ +// PARAM: --set ana.activated[+] 'pthreadMutexType' +#define _GNU_SOURCE +#include +#include +#include +#include + +int g; + +void* f1(void* ptr) { + pthread_mutex_t* mut = (pthread_mutex_t*) ptr; + + pthread_mutex_lock(mut); //NOWARN + pthread_mutex_lock(mut); //NOWARN + pthread_mutex_unlock(mut); + g = 8; //NORACE + pthread_mutex_unlock(mut); + return NULL; +} + + +int main(int argc, char const *argv[]) +{ + pthread_t t1; + pthread_mutex_t mut; + + pthread_mutexattr_t attr; + pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE); + pthread_mutex_init(&mut, &attr); + + + pthread_create(&t1,NULL,f1,&mut); + + + pthread_mutex_lock(&mut); //NOWARN + pthread_mutex_lock(&mut); //NOWARN + pthread_mutex_unlock(&mut); + g = 9; //NORACE + pthread_mutex_unlock(&mut); + + pthread_join(t1, NULL); + + + return 0; +} diff --git a/tests/regression/71-doublelocking/15-rec-dyn-nested.c b/tests/regression/71-doublelocking/15-rec-dyn-nested.c new file mode 100644 index 0000000000..d5dac9cd81 --- /dev/null +++ b/tests/regression/71-doublelocking/15-rec-dyn-nested.c @@ -0,0 +1,41 @@ +// PARAM: --set ana.activated[+] 'pthreadMutexType' +// Check we don't have a stack overflow because of tracking multiplicities +#define _GNU_SOURCE +#include +#include +#include +#include + +int g; + +void f2(pthread_mutex_t* mut) { + int top1, top2; + pthread_mutex_lock(mut); + if(top1 == top2) { + // This would cause the number of contexts to explode + f2(mut); + } + pthread_mutex_unlock(mut); +} + +void* f1(void* ptr) { + pthread_mutex_t* mut = (pthread_mutex_t*) ptr; + f2(mut); + return NULL; +} + + +int main(int argc, char const *argv[]) +{ + pthread_t t1; + pthread_mutex_t mut; + + pthread_mutexattr_t attr; + pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE); + pthread_mutex_init(&mut, &attr); + + + pthread_create(&t1,NULL,f1,&mut); + pthread_join(t1, NULL); + return 0; +} diff --git a/tests/regression/71-doublelocking/16-rec-dyn-no-path-sense.c b/tests/regression/71-doublelocking/16-rec-dyn-no-path-sense.c new file mode 100644 index 0000000000..2457ed3f62 --- /dev/null +++ b/tests/regression/71-doublelocking/16-rec-dyn-no-path-sense.c @@ -0,0 +1,51 @@ +// PARAM: --set ana.activated[+] 'pthreadMutexType' --set ana.path_sens[-] 'mutex' +// Test that multiplicity also works when path-sensitivity is disabled. +#define _GNU_SOURCE +#include +#include +#include +#include + +int g; + +void* f1(void* ptr) { + pthread_mutex_t* mut = (pthread_mutex_t*) ptr; + int top; + + + pthread_mutex_lock(mut); + + if(top) { + pthread_mutex_lock(mut); + } + + pthread_mutex_unlock(mut); + g = 8; //RACE! + + + return NULL; +} + + +int main(int argc, char const *argv[]) +{ + pthread_t t1; + pthread_mutex_t mut; + + pthread_mutexattr_t attr; + pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE); + pthread_mutex_init(&mut, &attr); + + + pthread_create(&t1,NULL,f1,&mut); + + + pthread_mutex_lock(&mut); + g = 9; // RACE! + pthread_mutex_unlock(&mut); + + pthread_join(t1, NULL); + + + return 0; +}