diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index e03e8a98d..621348ec5 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -80,11 +80,22 @@ module TransferFunctions (CFG : ProcCfg.S) = struct try Some (IdAccessPathMapDomain.find id id_map) with Not_found -> None - let add_path_to_state exp typ loc path_state id_map = + let add_path_to_state exp typ loc path_state id_map owned = + (* remove the last field of the access path, if it has any *) + let truncate = function + | base, [] + | base, _ :: [] -> base, [] + | base, accesses -> base, IList.rev (IList.tl (IList.rev accesses)) in let f_resolve_id = resolve_id id_map in + IList.fold_left (fun acc rawpath -> - ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc) + let base_path = truncate rawpath in + if not (ThreadSafetyDomain.OwnershipDomain.mem base_path owned) + then + ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc + else + acc) path_state (AccessPath.of_exp exp typ ~f_resolve_id) @@ -95,12 +106,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> id_map let exec_instr - ({ ThreadSafetyDomain.locks; reads; writes; id_map; } as astate) + ({ ThreadSafetyDomain.locks; reads; writes; id_map; owned; } as astate) { ProcData.pdesc; tenv; } _ = + let is_allocation pn = + Procname.equal pn BuiltinDecl.__new || + Procname.equal pn BuiltinDecl.__new_array in let is_unprotected is_locked = not is_locked && not (Procdesc.is_java_synchronized pdesc) in + let f_resolve_id = resolve_id id_map in function + | Sil.Call (Some (lhs_id, lhs_typ), Const (Cfun pn), _, _, _) when is_allocation pn -> + begin + match AccessPath.of_lhs_exp (Exp.Var lhs_id) lhs_typ ~f_resolve_id with + | Some lhs_access_path -> + let owned' = ThreadSafetyDomain.OwnershipDomain.add lhs_access_path owned in + { astate with owned = owned'; } + | None -> + astate + end | Sil.Call (_, Const (Cfun pn), _, loc, _) -> begin (* assuming that modeled procedures do not have useful summaries *) @@ -131,7 +155,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct { astate with reads = reads'; writes = writes'; } else astate in - { astate' with locks = locks' } + { astate' with locks = locks'; } | None -> astate end @@ -141,28 +165,43 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let id_map' = analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ astate in { astate with id_map = id_map'; } - | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, loc) -> - if is_unprotected locks (* abstracts no lock being held *) - then - let writes' = add_path_to_state lhsfield typ loc writes id_map in - { astate with writes = writes'; } - else - astate - - (* Note: it appears that the third arg of Store is never an Lfield in the targets of, - our translations, which is why we have not covered that case. *) - | Sil.Store (_, _, Lfield _, _) -> - failwith "Unexpected store instruction with rhs field" + | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) -> + let writes' = + match lhs_exp with + | Lfield ( _, _, typ) when is_unprotected locks -> (* abstracts no lock being held *) + add_path_to_state lhs_exp typ loc writes id_map owned + | _ -> writes in + (* if rhs is owned, propagate ownership to lhs. otherwise, remove lhs from ownerhsip set + (since it may have previously held an owned memory loc and is now being reassigned *) + let owned' = + match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id, + AccessPath.of_lhs_exp rhs_exp lhs_typ ~f_resolve_id with + | Some lhs_access_path, Some rhs_access_path -> + if ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path owned + then ThreadSafetyDomain.OwnershipDomain.add lhs_access_path owned + else ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path owned + | Some lhs_access_path, None -> + ThreadSafetyDomain.OwnershipDomain.remove lhs_access_path owned + | _ -> owned in + { astate with writes = writes'; owned = owned'; } | Sil.Load (lhs_id, rhs_exp, rhs_typ, loc) -> let id_map' = analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ astate in let reads' = match rhs_exp with | Lfield ( _, _, typ) when is_unprotected locks -> - add_path_to_state rhs_exp typ loc reads id_map + add_path_to_state rhs_exp typ loc reads id_map owned | _ -> reads in - { astate with Domain.reads = reads'; id_map = id_map'; } + (* if rhs is owned, propagate ownership to lhs *) + let owned' = + match AccessPath.of_lhs_exp rhs_exp rhs_typ ~f_resolve_id with + | Some rhs_access_path + when ThreadSafetyDomain.OwnershipDomain.mem rhs_access_path owned -> + ThreadSafetyDomain.OwnershipDomain.add (AccessPath.of_id lhs_id rhs_typ) owned + | _ -> + owned in + { astate with Domain.reads = reads'; id_map = id_map'; owned = owned'; } | _ -> astate end diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index f0e15fac3..259e0af94 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -11,12 +11,17 @@ open! IStd module F = Format +module RawAccessPath = struct + type t = AccessPath.raw + let compare = AccessPath.compare_raw + let pp = AccessPath.pp_raw + let pp_element = pp +end + +module OwnershipDomain = AbstractDomain.InvertedSet(PrettyPrintable.MakePPSet(RawAccessPath)) + module TraceElem = struct - module Kind = struct - type t = AccessPath.raw - let compare = AccessPath.compare_raw - let pp = AccessPath.pp_raw - end + module Kind = RawAccessPath type t = { site : CallSite.t; @@ -64,6 +69,8 @@ type astate = (** access paths written outside of synchronization *) id_map : IdAccessPathMapDomain.astate; (** map used to decompile temporary variables into access paths *) + owned : OwnershipDomain.astate; + (** access paths that must be owned by the current function *) } (** same as astate, but without [id_map] (since it's local) *) @@ -74,7 +81,8 @@ let initial = let reads = PathDomain.initial in let writes = PathDomain.initial in let id_map = IdAccessPathMapDomain.initial in - { locks; reads; writes; id_map; } + let owned = OwnershipDomain.initial in + { locks; reads; writes; id_map; owned; } let (<=) ~lhs ~rhs = if phys_equal lhs rhs @@ -83,7 +91,8 @@ let (<=) ~lhs ~rhs = LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks && PathDomain.(<=) ~lhs:lhs.reads ~rhs:rhs.reads && PathDomain.(<=) ~lhs:lhs.writes ~rhs:rhs.writes && - IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map + IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map && + OwnershipDomain.(<=) ~lhs:lhs.owned ~rhs:rhs.owned let join astate1 astate2 = if phys_equal astate1 astate2 @@ -94,7 +103,8 @@ let join astate1 astate2 = let reads = PathDomain.join astate1.reads astate2.reads in let writes = PathDomain.join astate1.writes astate2.writes in let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in - { locks; reads; writes; id_map; } + let owned = OwnershipDomain.join astate1.owned astate2.owned in + { locks; reads; writes; id_map; owned; } let widen ~prev ~next ~num_iters = if phys_equal prev next @@ -105,7 +115,8 @@ let widen ~prev ~next ~num_iters = let reads = PathDomain.widen ~prev:prev.reads ~next:next.reads ~num_iters in let writes = PathDomain.widen ~prev:prev.writes ~next:next.writes ~num_iters in let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in - { locks; reads; writes; id_map; } + let owned = OwnershipDomain.widen ~prev:prev.owned ~next:next.owned ~num_iters in + { locks; reads; writes; id_map; owned; } let pp_summary fmt (locks, reads, writes) = F.fprintf @@ -115,9 +126,10 @@ let pp_summary fmt (locks, reads, writes) = PathDomain.pp reads PathDomain.pp writes -let pp fmt { locks; reads; writes; id_map; } = +let pp fmt { locks; reads; writes; id_map; owned; } = F.fprintf fmt - "%a Id Map: %a" + "%a Id Map: %a Owned: %a" pp_summary (locks, reads, writes) IdAccessPathMapDomain.pp id_map + OwnershipDomain.pp owned diff --git a/infer/tests/codetoanalyze/java/threadsafety/Ownership.java b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java new file mode 100644 index 000000000..7cde6c08f --- /dev/null +++ b/infer/tests/codetoanalyze/java/threadsafety/Ownership.java @@ -0,0 +1,112 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.checkers; + +class Obj { + Object f; + Obj g; +} + +@ThreadSafe +public class Ownership { + + Obj field; + + public Ownership(Obj o) { + field = o; + } + + native void leakToAnotherThread(Object o); + + public void escapeViaConstructorBad() { + Obj local = new Obj(); + Ownership constructed = new Ownership(local); + local.f = new Object(); + } + + public void ownInOneBranchBad(Obj formal, boolean b) { + if (b) { + formal = new Obj(); + } + // we might not own formal + formal.f = new Object(); + } + + public void reassignToFormalBad(Obj formal) { + Obj local = new Obj(); + formal.g = local; // bad, we don't own formal + formal.g.f = new Object(); // ok; now that formal.g is reassigned to local, which we do own + } + + public void ownedLocalOk() { + Obj local = new Obj(); + local.f = new Object(); + } + + public Obj returnOwnedLocalOk() { + Obj local = new Obj(); + local.f = new Object(); + return local; + } + + public void writeOwnedLocalThenEscapeOk() { + Obj local = new Obj(); + local.f = new Object(); + leakToAnotherThread(local); + } + + public void ownInBranchesOk1(boolean b) { + Obj local; + if (b) { + local = new Obj(); + local.f = new Object(); + } else { + local = new Obj(); + local.f = new Integer(0); + } + local.f = new Boolean(false); + } + + public void ownedAccessPathOk() { + Obj local = new Obj(); + local.g = new Obj(); + local.g.f = new Object(); + } + + public void aliasOwnedLocalOk() { + Obj local = new Obj(); + Obj alias = local; + alias.f = new Object(); + local.f = new Object(); + } + + public void aliasOwnedLocalAccessPathOk() { + Obj local = new Obj(); + local.g = new Obj(); + Obj alias = local.g; + alias.f = new Object(); + } + + // we don't understand that ownership has been transferred from returnOwnedLocalOk to the current + // procedure + public void FP_ownershipNotInterproceduralOk() { + Obj local = returnOwnedLocalOk(); + local.f = new Object(); + } + + // we angelically assume that callees don't leak their arguments to another thread for now, so + // we'll miss this + public void FN_escapeThenWriteLocalBad() { + Obj local = new Obj(); + leakToAnotherThread(local); + local.f = new Object(); + } + +} diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index a86791499..5da645ff3 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -6,6 +6,9 @@ codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockB codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f] codetoanalyze/java/threadsafety/Locks.java, void Locks.afterWriteLockUnlockBad(), 3, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f] codetoanalyze/java/threadsafety/Locks.java, void Locks.lockInOneBranchBad(boolean), 4, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Locks.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.FP_ownershipNotInterproceduralOk(), 2, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Obj.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Obj.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.Obj.g] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_ERROR, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 1, THREAD_SAFETY_ERROR, [call to void ThreadSafeExample.assignInPrivateMethodOk(),access to codetoanalyze.java.checkers.ThreadSafeExample.f]