@ -1030,49 +1030,6 @@ let collect_conflicts sink (*kind*) threaded tab = (*kind implicitly Read for no
)
procs_and_threaded_and_accesses
(* keep only the first copy of an access per procedure,
and keep at most one warning per line ( they are usually interprocedural accesses
to different fields generated by the same call ) * )
let de_dup trace =
let select_representatives original_sinks predicate =
let list_of_original_sinks = ThreadSafetyDomain . PathDomain . Sinks . elements original_sinks in
ThreadSafetyDomain . PathDomain . Sinks . filter
( fun sink ->
(* for each sink we will keep one in the equivalence class of those
satisfying predicate . We select that by using find_exn to get
the first element equivalent ot sink in a list of sinks . This
first element is the dedup representative , and it happens to
typically be the first such access in a method . * )
let first_sink =
List . find_exn
~ f : ( fun sink2 -> predicate sink sink2 )
list_of_original_sinks in
Int . equal ( ThreadSafetyDomain . TraceElem . compare sink first_sink ) 0
)
original_sinks in
let de_duped_sinks_by_accesses = select_representatives
( ThreadSafetyDomain . PathDomain . sinks trace )
equal_accesses in
let de_duped_sinks_by_locs_and_accesses = select_representatives
de_duped_sinks_by_accesses
equal_locs in
ThreadSafetyDomain . PathDomain . update_sinks trace de_duped_sinks_by_locs_and_accesses
let strip_reads_that_have_co_located_write reads writes =
let set_of_read_sinks = ThreadSafetyDomain . PathDomain . sinks reads in
let set_of_write_sinks = ThreadSafetyDomain . PathDomain . sinks writes in
let stripped_read_sinks =
ThreadSafetyDomain . PathDomain . Sinks . filter
( fun sink -> not ( ThreadSafetyDomain . PathDomain . Sinks . exists
( fun sink2 -> equal_locs sink sink2 )
set_of_write_sinks
)
)
set_of_read_sinks in
ThreadSafetyDomain . PathDomain . update_sinks reads stripped_read_sinks
(* A helper function used in the error reporting *)
let pp_accesses_sink fmt ~ is_write_access sink =
let access_path , _ = ThreadSafetyDomain . PathDomain . Sink . kind sink in
@ -1116,7 +1073,7 @@ let report_thread_safety_violations
List . iter
~ f : report_one_path
( PathDomain . get_reportable_sink_paths ( de_dup trace ) ~ trace_of_pname )
( PathDomain . get_reportable_sink_paths trace ~ trace_of_pname )
let make_unprotected_write_description
tenv pname final_sink_site initial_sink_site final_sink _ _ =
@ -1190,8 +1147,27 @@ let report_unsafe_accesses tab ~should_report aggregated_access_map =
(* protected write, do nothing *)
reported_sites
| Access . Read , AccessPrecondition . Unprotected _ ->
(* unprotected read. TODO: report all writes as conflicts *)
(* unprotected read. report all writes as conflicts *)
let all_writes =
List . filter
~ f : ( fun ( other_access , _ , other_threaded , _ , _ ) ->
TraceElem . is_write other_access && not ( threaded && other_threaded ) )
accesses in
if List . is_empty all_writes
then
reported_sites
else
begin
report_thread_safety_violations
tenv
pdesc
~ get_unsafe_accesses : get_possibly_unsafe_reads
make_read_write_race_description
( PathDomain . of_sink access )
threaded
tab ;
CallSite . Set . add call_site reported_sites
end ;
| Access . Read , AccessPrecondition . Protected ->
(* protected read. report unprotected writes as conflicts *)
let unprotected_writes =
@ -1251,30 +1227,6 @@ let aggregate_accesses tab =
tab
AccessListMap . empty
(* find those elements of reads which have conflicts
somewhere else , and report them * )
let report_reads ( tenv , pdesc ) reads threaded tab =
let racy_read_sinks =
ThreadSafetyDomain . PathDomain . Sinks . filter
( fun sink ->
(* there exists a postcondition whose write set conflicts with
sink * )
not ( List . is_empty ( collect_conflicts sink threaded tab ) )
)
( ThreadSafetyDomain . PathDomain . sinks reads )
in
let racy_reads =
ThreadSafetyDomain . PathDomain . update_sinks reads racy_read_sinks
in
report_thread_safety_violations
tenv
pdesc
~ get_unsafe_accesses : get_possibly_unsafe_reads
make_read_write_race_description
racy_reads
threaded
tab
(* Currently we analyze if there is an @ThreadSafe annotation on at least one of
the classes in a file . This might be tightened in future or even broadened in future
based on other criteria * )
@ -1293,7 +1245,6 @@ let should_report_on_file file_env =
not ( List . exists ~ f : current_class_marked_not_threadsafe file_env ) &&
List . exists ~ f : current_class_or_super_marked_threadsafe file_env
(* *
Principles for race reporting .
Two accesses are excluded if they are both protetected by the same lock or
@ -1327,33 +1278,7 @@ let process_results_table file_env tab =
is_thread_safe_method pdesc tenv in
aggregate_accesses tab
| > report_unsafe_accesses tab ~ should_report ;
ResultsTableType . iter (* report errors for each method *)
( fun ( ( tenv , pdesc ) as proc_env ) ( threaded , _ , accesses , _ ) ->
if should_report pdesc tenv
then
let open ThreadSafetyDomain in
let reads , writes =
AccessDomain . fold
( fun pre accesses ( reads_acc , writes_acc ) ->
let read_accesses , write_accesses =
PathDomain . Sinks . partition TraceElem . is_read ( PathDomain . sinks accesses ) in
AccessDomain . add pre ( PathDomain . update_sinks accesses read_accesses ) reads_acc ,
AccessDomain . add pre ( PathDomain . update_sinks accesses write_accesses ) writes_acc )
accesses
( AccessDomain . empty , AccessDomain . empty ) in
begin
let unsafe_writes = get_possibly_unsafe_writes writes in
let unsafe_reads = get_possibly_unsafe_reads reads in
let stripped_unsafe_reads = strip_reads_that_have_co_located_write
unsafe_reads
unsafe_writes in
report_reads proc_env stripped_unsafe_reads threaded tab
end
)
tab
| > report_unsafe_accesses tab ~ should_report
(* Gathers results by analyzing all the methods in a file, then post-processes the results to check
an ( approximation of ) thread safety * )
Sam Blackshear
8 years ago
committed by
Facebook Github Bot