diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index c8c964314..3637dddba 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -760,6 +760,7 @@ let calculate_addendum_message tenv pname = else "" | _ -> "" + let combine_conditional_unconditional_writes conditional_writes unconditional_writes = let open ThreadSafetyDomain in ConditionalWritesDomain.fold @@ -767,7 +768,51 @@ let combine_conditional_unconditional_writes conditional_writes unconditional_wr conditional_writes unconditional_writes -let report_thread_safety_violations ( _, tenv, pname, pdesc) trace = +let conflicting_accesses (sink1 : ThreadSafetyDomain.TraceElem.t) + (sink2 : ThreadSafetyDomain.TraceElem.t) = + AccessPath.equal_access_list + (snd (ThreadSafetyDomain.TraceElem.kind sink1)) + (snd (ThreadSafetyDomain.TraceElem.kind sink2)) + +(* trace is really reads or writes set. Fix terminology later *) +let filter_conflicting_sinks sink trace = + let conflicts = + ThreadSafetyDomain.PathDomain.Sinks.filter + (fun sink2 -> conflicting_accesses sink sink2) + (ThreadSafetyDomain.PathDomain.sinks trace) in + ThreadSafetyDomain.PathDomain.update_sinks trace conflicts + +(* Given a sink representing a read access, + return a list of (proc_env,access-astate) pairs where + access-astate is a non-empty collection of conflicting + write accesses*) +let collect_conflicting_writes sink tab = + let procs_and_writes = + IList.map + (fun (key,(_, _, conditional_writes, unconditional_writes, _)) -> + let conflicting_writes = + combine_conditional_unconditional_writes + conditional_writes unconditional_writes + |> filter_conflicting_sinks sink in + key, conflicting_writes + ) + (ResultsTableType.bindings tab) in + List.filter + ~f:(fun (proc_env,writes) -> + (should_report_on_proc proc_env) + && not (ThreadSafetyDomain.PathDomain.Sinks.is_empty + (ThreadSafetyDomain.PathDomain.sinks writes)) + ) + procs_and_writes + +(*A helper function used int he error reporting*) +let pp_accesses_sink fmt sink = + let _, accesses = ThreadSafetyDomain.PathDomain.Sink.kind sink in + AccessPath.pp_access_list fmt accesses + + +(* trace is really a set of accesses*) +let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description trace tab = let open ThreadSafetyDomain in let trace_of_pname callee_pname = match Summary.read_summary pdesc callee_pname with @@ -776,9 +821,6 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace = | _ -> PathDomain.empty in let report_one_path ((_, sinks) as path) = - let pp_accesses fmt sink = - let _, accesses = PathDomain.Sink.kind sink in - AccessPath.pp_access_list fmt accesses in let initial_sink, _ = List.last_exn sinks in let final_sink, _ = List.hd_exn sinks in let initial_sink_site = PathDomain.Sink.call_site initial_sink in @@ -786,19 +828,15 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace = let desc_of_sink sink = if CallSite.equal (PathDomain.Sink.call_site sink) final_sink_site then - Format.asprintf "access to %a" pp_accesses sink + Format.asprintf "access to %a" pp_accesses_sink sink else Format.asprintf "call to %a" Procname.pp (CallSite.pname (PathDomain.Sink.call_site sink)) in let loc = CallSite.loc (PathDomain.Sink.call_site initial_sink) in let ltr = PathDomain.to_sink_loc_trace ~desc_of_sink path in let msg = Localise.to_string Localise.thread_safety_violation in - let description = - Format.asprintf "Public method %a%s writes to field %a outside of synchronization.%s" - Procname.pp pname - (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly") - pp_accesses final_sink - (calculate_addendum_message tenv pname) in + let description = make_description tenv pname final_sink_site + initial_sink_site final_sink tab in let exn = Exceptions.Checkers (msg, Localise.verbatim_desc description) in Reporting.log_error pname ~loc ~ltr exn in @@ -806,6 +844,58 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace = report_one_path (PathDomain.get_reportable_sink_paths trace ~trace_of_pname) + +let make_unprotected_write_description + tenv pname final_sink_site initial_sink_site final_sink _ = + Format.asprintf + "Unprotected write. Public method %a%s writes to field %a outside of synchronization.%s" + Procname.pp pname + (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly") + pp_accesses_sink final_sink + (calculate_addendum_message tenv pname) + +let make_read_write_race_description tenv pname final_sink_site initial_sink_site final_sink tab = + let conflicting_proc_envs = IList.map + fst + (collect_conflicting_writes final_sink tab) in + let conflicting_proc_names = IList.map + (fun (_,_,proc_name,_) -> proc_name) + conflicting_proc_envs in + let pp_proc_name_list fmt proc_names = + let pp_sep _ _ = F.fprintf fmt " , " in + F.pp_print_list ~pp_sep Procname.pp fmt proc_names in + let conflicts_description = + Format.asprintf "Potentially races with writes in method%s %a." + (if IList.length conflicting_proc_names > 1 then "s" else "") + pp_proc_name_list conflicting_proc_names in + Format.asprintf "Read/Write race. Public method %a%s reads from field %a. %s %s" + Procname.pp pname + (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly") + pp_accesses_sink final_sink + conflicts_description + (calculate_addendum_message tenv pname) + + +(* find those elements of reads which have conflicts + somewhere else, and report them *) +let report_reads proc_env reads 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_conflicting_writes sink tab)) + ) + (ThreadSafetyDomain.PathDomain.sinks reads) + in + let racy_reads = + ThreadSafetyDomain.PathDomain.update_sinks reads racy_read_sinks + in + report_thread_safety_violations proc_env + make_read_write_race_description + racy_reads + 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 *) @@ -842,12 +932,19 @@ let process_results_table file_env tab = (should_report_on_all_procs || is_thread_safe_method pdesc tenv) && should_report_on_proc proc_env in ResultsTableType.iter (* report errors for each method *) - (fun proc_env (_, _, conditional_writes, unconditional_writes, _) -> + (fun proc_env (_, reads, conditional_writes, unconditional_writes, _) -> if should_report proc_env then - combine_conditional_unconditional_writes conditional_writes unconditional_writes - |> report_thread_safety_violations proc_env) + let writes = combine_conditional_unconditional_writes + conditional_writes unconditional_writes in + begin + report_thread_safety_violations + proc_env make_unprotected_write_description writes tab + ; report_reads proc_env reads tab + end + ) tab + (*This is a "cluster checker" *) (*Gathers results by analyzing all the methods in a file, then post-processes the results to check (approximation of) thread safety *) diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 4cf8c527e..130a8a061 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -31,6 +31,9 @@ type access = let equal_access = [%compare.equal : access] + +let equal_access_list l1 l2 = Int.equal (List.compare compare_access l1 l2) 0 + let pp_base fmt (pvar, _) = Var.pp fmt pvar diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 61176c90a..2291f650b 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -45,6 +45,8 @@ val equal_base : base -> base -> bool val equal_access : access -> access -> bool +val equal_access_list : access list -> access list -> bool + val equal : t -> t -> bool (** create a base from a pvar *) diff --git a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java index 2f8a2bc97..50364a901 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java @@ -59,6 +59,7 @@ interface Interface { @ThreadSafe class Annotations implements Interface { Object f; + boolean b; @UiThread public void setF(Object newF) { @@ -178,18 +179,18 @@ class Annotations implements Interface { // writes to doubles are not atomic on all platforms, so this is not a benign race public double functionalDoubleBad() { - if (mDouble == 0.0) { + if (b) { mDouble = returnDouble(); } - return mDouble; + return 0.0; } // writes to longs are not atomic on all platforms, so this is not a benign race public long functionaLongBad() { - if (mLong == 0L) { + if (b) { mLong = returnLong(); } - return mLong; + return 2; } Boolean mBoxedBool; @@ -197,46 +198,52 @@ class Annotations implements Interface { @Functional native boolean returnBool(); public boolean functionalAcrossBoxingOk() { - if (mBoxedBool != null) { + if (b) { mBoxedBool = returnBool(); } - return mBoxedBool; + return b; } boolean mBool; @Functional native Boolean returnBoxedBool(); + boolean mBool2; + public boolean FP_functionalAcrossUnboxingOk() { - if (!mBool) { - mBool = returnBoxedBool(); + if (b) { + mBool2 = returnBoxedBool(); } - return mBool; + return b; } Long mBoxedLong; @Functional native Long returnBoxedLong(); - public Long functionalBoxedLongOk() { - if (mBoxedLong == null) { + public int functionalBoxedLongOk() { + if (b) { mBoxedLong = returnBoxedLong(); } - return mBoxedLong; + return 22; } - public long functionalAcrossUnboxingLongBad() { - if (mLong != 0L) { - mLong = returnBoxedLong(); + long mLong2; + + public int functionalAcrossUnboxingLongBad() { + if (b) { + mLong2 = returnBoxedLong(); } - return mLong; + return 2; } - public long FP_functionalAcrossBoxingLongOk() { - if (mBoxedLong != null) { - mBoxedLong = returnLong(); + long mBoxedLong2; + + public int FP_functionalAcrossBoxingLongOk() { + if (b) { + mBoxedLong2 = returnLong(); } - return mBoxedLong; + return 2; } public boolean propagateFunctional() { diff --git a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java new file mode 100644 index 000000000..f5f85488e --- /dev/null +++ b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java @@ -0,0 +1,43 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * 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. + */ + +package codetoanalyze.java.checkers; + +import javax.annotation.concurrent.ThreadSafe; + +@ThreadSafe +class ReadWriteRaces{ + +Integer safe_read; +Integer racy; + + void m0_OK(){ + Integer local; + local = safe_read; + } + + void m0_OK2(){ //parallel reads are OK + Integer local; + local = safe_read; + } + + void m1(){ // A read where there are other writes + Integer local; + local = racy; + } + + public void m2(){ + racy = 88; + } + + public void m3(){ + racy = 99; + } + +} diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index cb417b6d7..76b60f883 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -1,9 +1,9 @@ codetoanalyze/java/threadsafety/AndroidModels.java, void AndroidModels.someResourceMethodsNotFunctionalBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.AndroidModels.mField] -codetoanalyze/java/threadsafety/Annotations.java, boolean Annotations.FP_functionalAcrossUnboxingOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBool] +codetoanalyze/java/threadsafety/Annotations.java, boolean Annotations.FP_functionalAcrossUnboxingOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBool2] codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalDoubleBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mDouble] -codetoanalyze/java/threadsafety/Annotations.java, long Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBoxedLong] +codetoanalyze/java/threadsafety/Annotations.java, int Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mBoxedLong2] +codetoanalyze/java/threadsafety/Annotations.java, int Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong2] codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong] -codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mLong] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.functionalAndNonfunctionalBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.mInt] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.f] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Obj.f] @@ -37,9 +37,14 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.cantOwnThisBad(), codetoanalyze/java/threadsafety/Ownership.java, void Ownership.notOwnedInCalleeBad(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.mutateIfNotNull(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.g] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Obj.g] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad1(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f] +codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Ownership.field] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void NonThreadSafeClass.threadSafeMethod(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.NonThreadSafeClass.field]