From eccc3a8e4e6181582d9b19cfd28050fb66175000 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 27 Mar 2017 11:06:38 -0700 Subject: [PATCH] [thread-safety] move reporting of unprotected reads into aggregation function Summary: Move all of the reporting on top of the aggregation functionality. This lets us delete lots of code Reviewed By: peterogithub Differential Revision: D4772223 fbshipit-source-id: 47cc51a --- infer/src/checkers/ThreadSafety.ml | 121 ++++-------------- .../java/threadsafety/issues.exp | 3 +- 2 files changed, 25 insertions(+), 99 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 7cc0cf66a..5ca1da9e9 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -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 *) - reported_sites + (* 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 *) diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 2884f09d2..96b5a7787 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -30,12 +30,13 @@ codetoanalyze/java/threadsafety/Containers.java, void Containers.mapPutAllBad(Ma codetoanalyze/java/threadsafety/Containers.java, void Containers.mapPutBad(String,String), 1, THREAD_SAFETY_VIOLATION, [access to container codetoanalyze.java.checkers.Containers.mMap] codetoanalyze/java/threadsafety/Containers.java, void Containers.mapRemoveBad(String), 1, THREAD_SAFETY_VIOLATION, [access to container codetoanalyze.java.checkers.Containers.mMap] codetoanalyze/java/threadsafety/Containers.java, void Containers.mapSubclassWriteBad(HashMap,String), 1, THREAD_SAFETY_VIOLATION, [access to container ] -codetoanalyze/java/threadsafety/DeDup.java, void DeDup.colocated_read_write(), 1, THREAD_SAFETY_VIOLATION, [call to void DeDup.read_and_write(),access to codetoanalyze.java.checkers.DeDup.colocated_write] +codetoanalyze/java/threadsafety/DeDup.java, void DeDup.colocated_read_write(), 1, THREAD_SAFETY_VIOLATION, [call to void DeDup.read_and_write(),access to codetoanalyze.java.checkers.DeDup.colocated_read] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.separate_write_to_colocated_read(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.colocated_read] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.twoWritesOneInCaller(), 1, THREAD_SAFETY_VIOLATION, [call to void DeDup.writeToField(),access to codetoanalyze.java.checkers.DeDup.field] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.twoWritesOneInCaller(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.field] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_fields(), 1, THREAD_SAFETY_VIOLATION, [call to void DeDup.foo(),access to codetoanalyze.java.checkers.DeDup.fielda] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_reads(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.field] +codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_reads(), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.field] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_writes(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.field] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_writes(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.field] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.write_read(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.DeDup.field]