diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index ac2fab8f6..d35e62fe6 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -56,11 +56,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> None - let add_path_to_state exp typ pathdomainstate = + let add_path_to_state exp typ loc path_state = IList.fold_left - (fun pathdomainstate_acc rawpath -> ThreadSafetyDomain.PathDomain.add - rawpath pathdomainstate_acc) - pathdomainstate + (fun acc rawpath -> + ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc) + path_state (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ = @@ -90,9 +90,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end end - | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, _) -> + | Sil.Store ((Lfield ( _, _, typ) as lhsfield) , _, _, loc) -> if is_unprotected lockstate then (* abstracts no lock being held*) - (lockstate, (readstate, add_path_to_state lhsfield typ writestate)) + (lockstate, (readstate, add_path_to_state lhsfield typ loc writestate)) else astate (* Note: it appears that the third arg of Store is never an Lfield in the targets of, @@ -100,9 +100,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.Store (_, _, Lfield _, _) -> failwith "Unexpected store instruction with rhs field" - | Sil.Load (_, (Lfield ( _, _, typ) as rhsfield) , _, _) -> + | Sil.Load (_, (Lfield ( _, _, typ) as rhsfield) , _, loc) -> if is_unprotected lockstate then (* abstracts no lock being held*) - (lockstate, (add_path_to_state rhsfield typ readstate, writestate)) + (lockstate, (add_path_to_state rhsfield typ loc readstate, writestate)) else astate | _ -> @@ -190,11 +190,12 @@ let calculate_addendum_message tenv pname = | _ -> "" let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate = - let report_one_error access_path = + let report_one_error access_path loc = let description = - F.asprintf "Method %a writes to field %a outside of synchronization. %s" + F.asprintf "Method %a writes to field %a outside of synchronization at %a. %s" Procname.pp pname AccessPath.pp_access_list access_path + Location.pp loc (calculate_addendum_message tenv pname) in Checkers.ST.report_error tenv @@ -204,7 +205,12 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate = (Procdesc.get_loc pdesc) description in - IList.iter report_one_error (IList.map snd (ThreadSafetyDomain.PathDomain.elements writestate)) + ThreadSafetyDomain.PathDomain.Sinks.iter + (fun sink -> + let _, accesses = ThreadSafetyDomain.PathDomain.Sink.kind sink in + let loc = CallSite.loc (ThreadSafetyDomain.PathDomain.Sink.call_site sink) in + report_one_error accesses loc) + (ThreadSafetyDomain.PathDomain.sinks writestate) (* For now, just checks if there is one active element amongst the posts of the analyzed methods. diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 55ebf2875..826e63c34 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -6,11 +6,44 @@ * 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. *) -module PPrawpath = PrettyPrintable.MakePPSet(struct + +open! Utils + +module F = Format + +module TraceElem = struct + module Kind = struct type t = AccessPath.raw let compare = AccessPath.compare_raw - let pp_element = AccessPath.pp_raw - end) + let pp = AccessPath.pp_raw + end + + type t = { + site : CallSite.t; + kind : Kind.t; + } [@@deriving compare] + + let call_site { site; } = site + + let kind { kind; } = kind + + let make kind site = { kind; site; } + + let with_callsite t site = { t with site; } + + let pp fmt { site; kind; } = + F.fprintf fmt "Unprotected access to %a at %a" Kind.pp kind CallSite.pp site + + module Set = PrettyPrintable.MakePPSet (struct + type nonrec t = t + let compare = compare + let pp_element = pp + end) +end + +let make_access kind loc = + let site = CallSite.make Procname.empty_block loc in + TraceElem.make kind site (** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes the existence of one global lock. In the case that a lock is held on the access to a variable, @@ -19,7 +52,7 @@ module PPrawpath = PrettyPrintable.MakePPSet(struct and which memory locations correspond to the same lock. *) module LocksDomain = AbstractDomain.BooleanAnd -module PathDomain = AbstractDomain.FiniteSet(PPrawpath) +module PathDomain = SinkTrace.Make(TraceElem) module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain) diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index ab8833f27..4ccbfa6f7 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -1,10 +1,10 @@ -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.newmethodBad() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization. +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.newmethodBad() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization at [line 181]. Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.tsOK() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization. +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR, [Method void ExtendsThreadSafeExample.tsOK() writes to field codetoanalyze.java.checkers.ExtendsThreadSafeExample.field outside of synchronization at [line 186]. Note: Superclass class codetoanalyze.java.checkers.ThreadSafeExample is marked @ThreadSafe.] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_unlockOneLock(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_unlockOneLock() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterReentrantLockUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterReentrantLockUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.callPublicMethodBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.lockInOneBranchBad(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.lockInOneBranchBad(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] -codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.FP_unlockOneLock(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.FP_unlockOneLock() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 154]. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterReentrantLockUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterReentrantLockUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 71]. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.afterUnlockBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.afterUnlockBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 65]. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.callPublicMethodBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 82]. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.lockInOneBranchBad(boolean), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.lockInOneBranchBad(boolean) writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 56]. ] +codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR, [Method void ThreadSafeExample.tsBad() writes to field codetoanalyze.java.checkers.ThreadSafeExample.f outside of synchronization at [line 46]. ]