pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[thread-safety] Lay the groundwork for interprocedural trace-based reporting

Browse Source 
Summary: We'll eventually want fancy interprocedural traces. This diff adds the required boilerplate for this and adds the line number of each access to the error message. Real traces will come in a follow-up

Reviewed By: peterogithub

Differential Revision: D4251985

fbshipit-source-id: c9d9823
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent ea4cf13992
commit 579b982359
3 changed files with 62 additions and 23 deletions
Show Stats Download Patch File Download Diff File

28
infer/src/checkers/ThreadSafety.ml
Unescape View File

@ -56,11 +56,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ -> | _ ->
None None
let add_path_to_state exp typ pathdomainstate = let add_path_to_state exp typ loc path_state =
IList.fold_left IList.fold_left
(fun pathdomainstate_acc rawpath -> ThreadSafetyDomain.PathDomain.add (fun acc rawpath ->
rawpath pathdomainstate_acc) ThreadSafetyDomain.PathDomain.add_sink (ThreadSafetyDomain.make_access rawpath loc) acc)
pathdomainstate path_state
(AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None)) (AccessPath.of_exp exp typ ~f_resolve_id:(fun _ -> None))
let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ = let exec_instr ((lockstate, (readstate,writestate)) as astate) { ProcData.pdesc; } _ =
@ -90,9 +90,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
end end
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*) 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 else astate
(* Note: it appears that the third arg of Store is never an Lfield in the targets of, (* 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 _, _) -> | Sil.Store (_, _, Lfield _, _) ->
failwith "Unexpected store instruction with rhs field" 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*) 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 else astate
| _ -> | _ ->
@ -190,11 +190,12 @@ let calculate_addendum_message tenv pname =
| _ -> "" | _ -> ""
let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate = let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate =
let report_one_error access_path = let report_one_error access_path loc =
let description = 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 Procname.pp pname
AccessPath.pp_access_list access_path AccessPath.pp_access_list access_path
Location.pp loc
(calculate_addendum_message tenv pname) (calculate_addendum_message tenv pname)
in in
Checkers.ST.report_error tenv Checkers.ST.report_error tenv
@ -204,7 +205,12 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate =
(Procdesc.get_loc pdesc) (Procdesc.get_loc pdesc)
description description
in 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. (* For now, just checks if there is one active element amongst the posts of the analyzed methods.

39
infer/src/checkers/ThreadSafetyDomain.ml
Unescape View File

@ -6,11 +6,44 @@
* LICENSE file in the root directory of this source tree. An additional grant * 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. * 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 type t = AccessPath.raw
let compare = AccessPath.compare_raw let compare = AccessPath.compare_raw
let pp_element = AccessPath.pp_raw 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)
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 (** 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, 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. *) and which memory locations correspond to the same lock. *)
module LocksDomain = AbstractDomain.BooleanAnd module LocksDomain = AbstractDomain.BooleanAnd
module PathDomain = AbstractDomain.FiniteSet(PPrawpath) module PathDomain = SinkTrace.Make(TraceElem)
module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain) module ReadWriteDomain = AbstractDomain.Pair (PathDomain) (PathDomain)

16
infer/tests/codetoanalyze/java/threadsafety/issues.exp
Unescape View File

@ -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.] 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.] 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.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. ] 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. ] 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. ] 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. ] 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. ] 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]. ]

Write Preview
Loading…
Cancel
Save