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

[threadsafety] Thumbs up step 1

Browse Source 
Summary:
This is a refactoring diff to put the info into the abstract domain
to track when we have done steps which would invalidate "I think I have a proof".
Subsequent diffs will start manipulating ThumbsUpDomain

Reviewed By: sblackshear

Differential Revision: D5172181

fbshipit-source-id: 51ceba6
master
Peter O'Hearn 8 years ago committed by Facebook Github Bot
parent 644066f4be
commit ddcbb419be
3 changed files with 36 additions and 25 deletions
Show Stats Download Patch File Download Diff File

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

@ -403,7 +403,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(Unprotected (Some 0))
(make_access dummy_access_ap Write callee_loc)
AccessDomain.empty in
Some (false, false, callee_accesses, AttributeSetDomain.empty)
Some (true, false, false, callee_accesses, AttributeSetDomain.empty)
let get_summary caller_pdesc callee_pname actuals callee_loc tenv =
if is_container_write callee_pname tenv
@ -514,12 +514,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
end
| NoEffect ->
match get_summary pdesc callee_pname actuals loc tenv with
| Some (callee_threads, callee_locks, callee_accesses, return_attributes) ->
| Some (callee_thumbs_up, callee_threads, callee_locks,
callee_accesses, return_attributes) ->
let update_caller_accesses pre callee_accesses caller_accesses =
let combined_accesses =
PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
|> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in
AccessDomain.add pre combined_accesses caller_accesses in
let thumbs_up = callee_thumbs_up && astate.thumbs_up in
let locks = callee_locks || astate.locks in
let threads = callee_threads || astate.threads in
let unprotected = is_unprotected locks threads pdesc in
@ -589,7 +591,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
actuals
astate.attribute_map
extras in
{ locks; threads; accesses; attribute_map; }
{ thumbs_up; locks; threads; accesses; attribute_map; }
| None ->
let should_assume_returns_ownership (call_flags : CallFlags.t) actuals =
(* assume non-interface methods with no summary and no parameters return
@ -840,10 +842,11 @@ let is_thread_safe_method pdesc tenv =
(Procdesc.get_proc_name pdesc)
let empty_post =
let initial_known_on_ui_thread = false
let initial_thumbs_up = true
and initial_known_on_ui_thread = false
and has_lock = false
and return_attrs = ThreadSafetyDomain.AttributeSetDomain.empty in
(initial_known_on_ui_thread, has_lock, ThreadSafetyDomain.AccessDomain.empty, return_attrs)
(initial_thumbs_up, initial_known_on_ui_thread, has_lock, ThreadSafetyDomain.AccessDomain.empty, return_attrs)
let analyze_procedure callback =
let is_initializer tenv proc_name =
@ -882,7 +885,7 @@ let analyze_procedure callback =
{ ThreadSafetyDomain.empty with threads; }, IdAccessPathMapDomain.empty in
match Analyzer.compute_post proc_data ~initial ~debug:false with
| Some ({ threads; locks; accesses; attribute_map; }, _) ->
| Some ({ thumbs_up; threads; locks; accesses; attribute_map; }, _) ->
let return_var_ap =
AccessPath.of_pvar
(Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc))
@ -890,7 +893,7 @@ let analyze_procedure callback =
let return_attributes =
try AttributeMapDomain.find return_var_ap attribute_map
with Not_found -> AttributeSetDomain.empty in
Some (threads, locks, accesses, return_attributes)
Some (thumbs_up, threads, locks, accesses, return_attributes)
| None ->
None
end
@ -982,7 +985,7 @@ let trace_of_pname orig_sink orig_pdesc callee_pname =
let open ThreadSafetyDomain in
let orig_access = PathDomain.Sink.kind orig_sink in
match Summary.read_summary orig_pdesc callee_pname with
| Some (_, _, access_map, _) ->
| Some (_, _, _, access_map, _) ->
get_all_accesses
(fun access ->
Int.equal (Access.compare (PathDomain.Sink.kind access) orig_access) 0)
@ -1303,7 +1306,7 @@ let should_filter_access (_, path) =
now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells
that x.f.g may point to during execution *)
let make_results_table file_env =
let aggregate_post (threaded, _, accesses, _) tenv pdesc acc =
let aggregate_post (_ , threaded, _, accesses, _) tenv pdesc acc =
let open ThreadSafetyDomain in
AccessDomain.fold
(fun pre accesses acc ->

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

@ -75,15 +75,10 @@ let make_access access_path access_kind loc =
*)
module LocksDomain = AbstractDomain.BooleanAnd
(* In this domain false<=true. The intended denotations [[.]] are
[[true]] = the set of all states where we know according, to annotations
or assertions, that we are on the UI thread (or some other specific thread).
[[false]] = the set of all states
The use of || for join in this domain enforces that, to not know for sure you are threaded,
it is enough to be unthreaded in one branch. (See RaceWithMainThread.java for examples)
*)
module ThreadsDomain = AbstractDomain.BooleanAnd
module ThumbsUpDomain = AbstractDomain.BooleanAnd
module PathDomain = SinkTrace.Make(TraceElem)
module Choice = struct
@ -205,6 +200,7 @@ end
type astate =
{
thumbs_up : ThumbsUpDomain.astate;
threads: ThreadsDomain.astate;
locks : LocksDomain.astate;
accesses : AccessDomain.astate;
@ -212,14 +208,16 @@ type astate =
}
type summary =
ThreadsDomain.astate * LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate
ThumbsUpDomain.astate * ThreadsDomain.astate * LocksDomain.astate
* AccessDomain.astate * AttributeSetDomain.astate
let empty =
let thumbs_up = true in
let threads = false in
let locks = false in
let accesses = AccessDomain.empty in
let attribute_map = AccessPath.RawMap.empty in
{ threads; locks; accesses; attribute_map; }
{ thumbs_up; threads; locks; accesses; attribute_map; }
let (<=) ~lhs ~rhs =
if phys_equal lhs rhs
@ -235,37 +233,42 @@ let join astate1 astate2 =
then
astate1
else
let thumbs_up = ThreadsDomain.join astate1.thumbs_up astate2.thumbs_up in
let threads = ThreadsDomain.join astate1.threads astate2.threads in
let locks = LocksDomain.join astate1.locks astate2.locks in
let accesses = AccessDomain.join astate1.accesses astate2.accesses in
let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
{ threads; locks; accesses; attribute_map; }
{ thumbs_up; threads; locks; accesses; attribute_map; }
let widen ~prev ~next ~num_iters =
if phys_equal prev next
then
prev
else
let thumbs_up = ThreadsDomain.widen ~prev:prev.thumbs_up ~next:next.thumbs_up ~num_iters in
let threads = ThreadsDomain.widen ~prev:prev.threads ~next:next.threads ~num_iters in
let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in
let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in
let attribute_map =
AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in
{ threads; locks; accesses; attribute_map; }
{ thumbs_up; threads; locks; accesses; attribute_map; }
let pp_summary fmt (threads, locks, accesses, return_attributes) =
let pp_summary fmt (thumbs_up, threads, locks,
accesses, return_attributes) =
F.fprintf
fmt
"Threads: %a Locks: %a Accesses %a Return Attributes: %a"
"\nThumbsUp: %a, Threads: %a, Locks: %a \nAccesses %a \nReturn Attributes: %a\n"
ThumbsUpDomain.pp thumbs_up
ThreadsDomain.pp threads
LocksDomain.pp locks
AccessDomain.pp accesses
AttributeSetDomain.pp return_attributes
let pp fmt { threads; locks; accesses; attribute_map; } =
let pp fmt { thumbs_up; threads; locks; accesses; attribute_map; } =
F.fprintf
fmt
"Threads: %a Locks: %a Accesses: %a Attribute Map: %a"
"\nThumbsUp: %a, Threads: %a, Locks: %a \nAccesses %a \nReturn Attributes: %a\n"
ThumbsUpDomain.pp thumbs_up
ThreadsDomain.pp threads
LocksDomain.pp locks
AccessDomain.pp accesses

7
infer/src/checkers/ThreadSafetyDomain.mli
Unescape View File

@ -41,6 +41,8 @@ module LocksDomain : AbstractDomain.S with type astate = bool
module ThreadsDomain : AbstractDomain.S with type astate = bool
module ThumbsUpDomain : AbstractDomain.S with type astate = bool
module PathDomain : module type of SinkTrace.Make(TraceElem)
(** attribute attached to a boolean variable specifying what it means when the boolean is true *)
@ -138,6 +140,8 @@ end
type astate =
{
thumbs_up : ThreadsDomain.astate;
(** boolean that is true if we think we have a proof *)
threads : ThreadsDomain.astate;
(** boolean that is true if we know we are on UI/main thread *)
locks : LocksDomain.astate;
@ -151,7 +155,8 @@ type astate =
(** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the
attributes associated with the return value *)
type summary =
ThreadsDomain.astate * LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate
ThumbsUpDomain.astate * ThreadsDomain.astate * LocksDomain.astate
* AccessDomain.astate * AttributeSetDomain.astate
include AbstractDomain.WithBottom with type astate := astate

Write Preview
Loading…
Cancel
Save