diff --git a/infer/src/absint/MethodMatcher.mli b/infer/src/absint/MethodMatcher.mli index 3c00df6db..8ef53d125 100644 --- a/infer/src/absint/MethodMatcher.mli +++ b/infer/src/absint/MethodMatcher.mli @@ -32,7 +32,7 @@ val of_json : Yojson.Basic.t -> t ["search_superclasses"] and ["method_prefix"]. If absent, the defaults are used. The resulting matcher matches if one of the matchers in the list does. *) -val of_list : t list -> t +val of_list : t list -> t [@@warning "-32"] (** Or combinator *) val of_records : record list -> t diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index 341c9e6be..c56a62475 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -6,7 +6,6 @@ *) open! IStd -module F = Format let is_synchronized_library_call = let targets = ["java.lang.StringBuffer"; "java.util.Hashtable"; "java.util.Vector"] in @@ -74,13 +73,6 @@ let float_of_const_int = function let is_excessive_secs duration = Float.(duration > android_anr_time_limit) -type severity = Low | Medium | High [@@deriving compare] - -let pp_severity fmt sev = - let msg = match sev with Low -> "Low" | Medium -> "Medium" | High -> "High" in - F.pp_print_string fmt msg - - let no_args_or_excessive_timeout_and_timeunit = function | [_] -> (* no arguments, unconditionally blocks *) @@ -111,38 +103,6 @@ let no_args_or_excessive_millis_and_nanos = function false -let standard_matchers = - let open MethodMatcher in - let high_sev = - [ {default with classname= "java.lang.Thread"; methods= ["sleep"]} - ; { default with - classname= "java.lang.Thread" - ; methods= ["join"] - ; actuals_pred= no_args_or_excessive_millis_and_nanos } - ; { default with - classname= "java.util.concurrent.CountDownLatch" - ; methods= ["await"] - ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } - (* an IBinder.transact call is an RPC. If the 4th argument (5th counting `this` as the first) - is int-zero then a reply is expected and returned from the remote process, thus potentially - blocking. If the 4th argument is anything else, we assume a one-way call which doesn't block. *) - ; { default with - classname= "android.os.IBinder" - ; methods= ["transact"] - ; actuals_pred= (fun actuals -> List.nth actuals 4 |> Option.exists ~f:HilExp.is_int_zero) } - ] - in - let low_sev = - [ { default with - classname= "android.os.AsyncTask" - ; methods= ["get"] - ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } ] - in - let high_sev_matcher = List.map high_sev ~f:of_record |> of_list in - let low_sev_matcher = List.map low_sev ~f:of_record |> of_list in - [(high_sev_matcher, High); (low_sev_matcher, Low)] - - let is_future_get = let open MethodMatcher in of_record @@ -157,10 +117,30 @@ let is_future_is_done = of_record {default with classname= "java.util.concurrent.Future"; methods= ["isDone"]}) -(* sort from High to Low *) -let may_block tenv pn actuals = - List.find_map standard_matchers ~f:(fun (matcher, sev) -> - Option.some_if (matcher tenv pn actuals) sev ) +let may_block = + MethodMatcher.( + of_records + [ {default with classname= "java.lang.Thread"; methods= ["sleep"]} + ; { default with + classname= "java.lang.Thread" + ; methods= ["join"] + ; actuals_pred= no_args_or_excessive_millis_and_nanos } + ; { default with + classname= "java.util.concurrent.CountDownLatch" + ; methods= ["await"] + ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } + (* an IBinder.transact call is an RPC. If the 4th argument (5th counting `this` as the first) + is int-zero then a reply is expected and returned from the remote process, thus potentially + blocking. If the 4th argument is anything else, we assume a one-way call which doesn't block. *) + ; { default with + classname= "android.os.IBinder" + ; methods= ["transact"] + ; actuals_pred= (fun actuals -> List.nth actuals 4 |> Option.exists ~f:HilExp.is_int_zero) + } + ; { default with + classname= "android.os.AsyncTask" + ; methods= ["get"] + ; actuals_pred= no_args_or_excessive_timeout_and_timeunit } ]) let is_monitor_wait = diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index 5fdf71a80..883450e38 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/infer/src/concurrency/StarvationModels.mli @@ -6,13 +6,8 @@ *) open! IStd -module F = Format -type severity = Low | Medium | High [@@deriving compare] - -val pp_severity : F.formatter -> severity -> unit - -val may_block : Tenv.t -> Procname.t -> HilExp.t list -> severity option +val may_block : Tenv.t -> Procname.t -> HilExp.t list -> bool (** is the method call potentially blocking, given the actuals passed? *) val is_strict_mode_violation : Tenv.t -> Procname.t -> HilExp.t list -> bool diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 4bbfdd2ac..797f868d9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -327,14 +327,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Domain.wait_on_monitor ~loc formals actuals astate | NoEffect when is_java && is_future_get tenv callee actuals -> Domain.future_get ~callee ~loc actuals astate - | NoEffect when is_java -> ( + | NoEffect when is_java -> let ret_exp = HilExp.AccessExpression.base ret_base in let astate = do_work_scheduling tenv callee actuals loc astate in - match may_block tenv callee actuals with - | Some sev -> - Domain.blocking_call ~callee sev ~loc astate - | None -> - do_call analysis_data ret_exp callee actuals loc astate ) + if may_block tenv callee actuals then Domain.blocking_call ~callee ~loc astate + else do_call analysis_data ret_exp callee actuals loc astate | NoEffect -> (* in C++/Obj C we only care about deadlocks, not starvation errors *) let ret_exp = HilExp.AccessExpression.base ret_base in @@ -461,7 +458,7 @@ module ReportMap : sig val add_deadlock : report_add_t - val add_starvation : StarvationModels.severity -> report_add_t + val add_starvation : report_add_t val add_strict_mode_violation : report_add_t @@ -476,7 +473,7 @@ module ReportMap : sig whole-program mode only *) end = struct type problem = - | Starvation of StarvationModels.severity + | Starvation of int | Deadlock of int | StrictModeViolation of int | LocklessViolation of int @@ -504,44 +501,39 @@ end = struct let empty : t = Location.Map.empty - let add tenv pattrs loc report loc_map = - if Reporting.is_suppressed tenv pattrs (issue_type_of_problem report.problem) then loc_map + let add tenv pattrs loc ltr message problem loc_map = + if Reporting.is_suppressed tenv pattrs (issue_type_of_problem problem) then loc_map else + let pname = ProcAttributes.get_proc_name pattrs in + let report = {problem; pname; ltr; message} in Location.Map.update loc - (function reports_opt -> Some (report :: Option.value reports_opt ~default:[])) + (fun reports_opt -> Some (report :: Option.value reports_opt ~default:[])) loc_map - let add_deadlock tenv pattrs loc ltr message (map : t) = - let pname = ProcAttributes.get_proc_name pattrs in - let report = {problem= Deadlock (-List.length ltr); pname; ltr; message} in - add tenv pattrs loc report map + let add_deadlock tenv pattrs loc ltr message map = + let problem = Deadlock (-List.length ltr) in + add tenv pattrs loc ltr message problem map - let add_starvation sev tenv pattrs loc ltr message map = - let pname = ProcAttributes.get_proc_name pattrs in - let report = {pname; problem= Starvation sev; ltr; message} in - add tenv pattrs loc report map + let add_starvation tenv pattrs loc ltr message map = + let problem = Starvation (-List.length ltr) in + add tenv pattrs loc ltr message problem map - let add_strict_mode_violation tenv pattrs loc ltr message (map : t) = - let pname = ProcAttributes.get_proc_name pattrs in - let report = {problem= StrictModeViolation (-List.length ltr); pname; ltr; message} in - add tenv pattrs loc report map + let add_strict_mode_violation tenv pattrs loc ltr message map = + let problem = StrictModeViolation (-List.length ltr) in + add tenv pattrs loc ltr message problem map - let add_lockless_violation tenv pattrs loc ltr message (map : t) = - let pname = ProcAttributes.get_proc_name pattrs in - let report = {problem= LocklessViolation (-List.length ltr); pname; ltr; message} in - add tenv pattrs loc report map + let add_lockless_violation tenv pattrs loc ltr message map = + let problem = LocklessViolation (-List.length ltr) in + add tenv pattrs loc ltr message problem map - let add_arbitrary_code_execution_under_lock tenv pattrs loc ltr message (map : t) = - let pname = ProcAttributes.get_proc_name pattrs in - let report = - {problem= ArbitraryCodeExecutionUnderLock (-List.length ltr); pname; ltr; message} - in - add tenv pattrs loc report map + let add_arbitrary_code_execution_under_lock tenv pattrs loc ltr message map = + let problem = ArbitraryCodeExecutionUnderLock (-List.length ltr) in + add tenv pattrs loc ltr message problem map let issue_log_of loc_map = @@ -606,7 +598,7 @@ end = struct in log_reports (compare_reports Int.compare) loc deadlocks issue_log |> log_reports (compare_reports Int.compare) loc lockless_violations - |> log_reports (compare_reports StarvationModels.compare_severity) loc starvations + |> log_reports (compare_reports Int.compare) loc starvations |> log_reports (compare_reports Int.compare) loc strict_mode_violations |> log_reports (compare_reports Int.compare) loc arbitrary_code_executions_under_lock in @@ -709,7 +701,7 @@ let report_on_parallel_composition ~should_report_starvation tenv pattrs pair lo if CriticalPair.can_run_in_parallel pair other_pair then let acquisitions = other_pair.CriticalPair.elem.acquisitions in match other_pair.CriticalPair.elem.event with - | MayBlock {severity} as event + | MayBlock _ as event when should_report_starvation && Acquisitions.lock_is_held_in_other_thread tenv lock acquisitions -> let error_message = @@ -718,7 +710,7 @@ let report_on_parallel_composition ~should_report_starvation tenv pattrs pair lo pname_pp pname Lock.pp_locks lock Event.describe event in let ltr, loc = make_trace_and_loc () in - ReportMap.add_starvation severity tenv pattrs loc ltr error_message report_map + ReportMap.add_starvation tenv pattrs loc ltr error_message report_map | MonitorWait {lock= monitor_lock} when should_report_starvation && Acquisitions.lock_is_held_in_other_thread tenv lock acquisitions @@ -729,7 +721,7 @@ let report_on_parallel_composition ~should_report_starvation tenv pattrs pair lo pname_pp pname Lock.pp_locks lock Event.describe other_pair.CriticalPair.elem.event in let ltr, loc = make_trace_and_loc () in - ReportMap.add_starvation High tenv pattrs loc ltr error_message report_map + ReportMap.add_starvation tenv pattrs loc ltr error_message report_map | LockAcquire _ -> ( match CriticalPair.may_deadlock tenv ~lhs:pair ~lhs_lock:lock ~rhs:other_pair with | Some other_lock when should_report_deadlock_on_current_proc pair other_pair -> @@ -762,20 +754,20 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t) (ltr, loc) in match event with - | MayBlock {severity} when is_not_private && should_report_starvation -> + | MayBlock _ when is_not_private && should_report_starvation -> let error_message = Format.asprintf "Method %a runs on UI thread and may block; %a." pname_pp pname Event.describe event in let ltr, loc = make_trace_and_loc () in - ReportMap.add_starvation severity tenv pattrs loc ltr error_message report_map + ReportMap.add_starvation tenv pattrs loc ltr error_message report_map | MonitorWait _ when is_not_private && should_report_starvation -> let error_message = Format.asprintf "Method %a runs on UI thread and may block; %a." pname_pp pname Event.describe event in let ltr, loc = make_trace_and_loc () in - ReportMap.add_starvation High tenv pattrs loc ltr error_message report_map + ReportMap.add_starvation tenv pattrs loc ltr error_message report_map | StrictModeCall _ when is_not_private && should_report_starvation -> let error_message = Format.asprintf "Method %a runs on UI thread and may violate Strict Mode; %a." pname_pp diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index e80315495..62a0d863b 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -190,7 +190,7 @@ end module Event = struct type t = | LockAcquire of {locks: Lock.t list; thread: ThreadDomain.t} - | MayBlock of {callee: Procname.t; severity: StarvationModels.severity; thread: ThreadDomain.t} + | MayBlock of {callee: Procname.t; thread: ThreadDomain.t} | MonitorWait of {lock: Lock.t; thread: ThreadDomain.t} | MustNotOccurUnderLock of {callee: Procname.t; thread: ThreadDomain.t} | StrictModeCall of {callee: Procname.t; thread: ThreadDomain.t} @@ -201,9 +201,8 @@ module Event = struct F.fprintf fmt "LockAcquire(%a, %a)" (PrettyPrintable.pp_collection ~pp_item:Lock.pp) locks ThreadDomain.pp thread - | MayBlock {callee; severity; thread} -> - F.fprintf fmt "MayBlock(%a, %a, %a)" Procname.pp callee StarvationModels.pp_severity - severity ThreadDomain.pp thread + | MayBlock {callee; thread} -> + F.fprintf fmt "MayBlock(%a, %a)" Procname.pp callee ThreadDomain.pp thread | StrictModeCall {callee; thread} -> F.fprintf fmt "StrictModeCall(%a, %a)" Procname.pp callee ThreadDomain.pp thread | MonitorWait {lock; thread} -> @@ -257,7 +256,7 @@ module Event = struct let make_acquire locks thread = LockAcquire {locks; thread} - let make_blocking_call callee severity thread = MayBlock {callee; severity; thread} + let make_blocking_call callee thread = MayBlock {callee; thread} let make_strict_mode_call callee thread = StrictModeCall {callee; thread} @@ -783,8 +782,8 @@ let make_call_with_event new_event ~loc astate = add_critical_pair ~tenv_opt:None astate.lock_state new_event ~loc astate.critical_pairs } -let blocking_call ~callee sev ~loc astate = - let new_event = Event.make_blocking_call callee sev astate.thread in +let blocking_call ~callee ~loc astate = + let new_event = Event.make_blocking_call callee astate.thread in make_call_with_event new_event ~loc astate @@ -806,7 +805,7 @@ let future_get ~callee ~loc actuals astate = |> Option.exists ~f:(function Attribute.FutureDoneState x -> x | _ -> false) -> astate | HilExp.AccessExpression _ :: _ -> - let new_event = Event.make_blocking_call callee Low astate.thread in + let new_event = Event.make_blocking_call callee astate.thread in make_call_with_event new_event ~loc astate | _ -> astate diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index cde5f0881..d3b5261b6 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -58,7 +58,7 @@ end module Event : sig type t = | LockAcquire of {locks: Lock.t list; thread: ThreadDomain.t} - | MayBlock of {callee: Procname.t; severity: StarvationModels.severity; thread: ThreadDomain.t} + | MayBlock of {callee: Procname.t; thread: ThreadDomain.t} | MonitorWait of {lock: Lock.t; thread: ThreadDomain.t} | MustNotOccurUnderLock of {callee: Procname.t; thread: ThreadDomain.t} | StrictModeCall of {callee: Procname.t; thread: ThreadDomain.t} @@ -191,7 +191,7 @@ val acquire : tenv:Tenv.t -> t -> procname:Procname.t -> loc:Location.t -> Lock. val release : t -> Lock.t list -> t (** simultaneously release a number of locks, no-op if list is empty *) -val blocking_call : callee:Procname.t -> StarvationModels.severity -> loc:Location.t -> t -> t +val blocking_call : callee:Procname.t -> loc:Location.t -> t -> t val wait_on_monitor : loc:Location.t -> FormalMap.t -> HilExp.t list -> t -> t