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

turn racerd and starvation into `interprocedural` and `file` checkers

Browse Source 
Summary: Almost a dune library now.

Reviewed By: ngorogiannis

Differential Revision: D21426394

fbshipit-source-id: 4ce58624e
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 3e76e48657
commit 0e40c62a7e
7 changed files with 115 additions and 124 deletions
Show Stats Download Patch File Download Diff File

17
infer/src/backend/registerCheckers.ml
Unescape View File

@ -97,12 +97,13 @@ let all_checkers =
; { name= "Starvation analysis" ; { name= "Starvation analysis"
; active= Config.is_checker_enabled Starvation ; active= Config.is_checker_enabled Starvation
; callbacks= ; callbacks=
(let starvation_file_reporting = (let starvation = interprocedural Payloads.Fields.starvation Starvation.analyze_procedure in
let starvation_file_reporting =
file StarvationIssues Payloads.Fields.starvation Starvation.reporting file StarvationIssues Payloads.Fields.starvation Starvation.reporting
in in
[ (Procedure Starvation.analyze_procedure, Language.Java) [ (starvation, Language.Java)
; (starvation_file_reporting, Language.Java) ; (starvation_file_reporting, Language.Java)
; (Procedure Starvation.analyze_procedure, Language.Clang) ; (starvation, Language.Clang)
; (starvation_file_reporting, Language.Clang) ] ) } ; (starvation_file_reporting, Language.Clang) ] ) }
; { name= "loop hoisting" ; { name= "loop hoisting"
; active= Config.is_checker_enabled LoopHoisting ; active= Config.is_checker_enabled LoopHoisting
@ -148,10 +149,12 @@ let all_checkers =
; { name= "RacerD" ; { name= "RacerD"
; active= Config.is_checker_enabled RacerD ; active= Config.is_checker_enabled RacerD
; callbacks= ; callbacks=
[ (Procedure RacerD.analyze_procedure, Language.Clang) (let racerd_proc = interprocedural Payloads.Fields.racerd RacerD.analyze_procedure in
; (Procedure RacerD.analyze_procedure, Language.Java) let racerd_file = file RacerDIssues Payloads.Fields.racerd RacerD.file_analysis in
; (File {callback= RacerD.file_analysis; issue_dir= RacerDIssues}, Language.Clang) [ (racerd_proc, Language.Clang)
; (File {callback= RacerD.file_analysis; issue_dir= RacerDIssues}, Language.Java) ] } ; (racerd_proc, Language.Java)
; (racerd_file, Language.Clang)
; (racerd_file, Language.Java) ] ) }
; { name= "quandary" ; { name= "quandary"
; active= Config.(is_checker_enabled Quandary) ; active= Config.(is_checker_enabled Quandary)
; callbacks= ; callbacks=

13
infer/src/concurrency/ConcurrencyUtils.ml
Unescape View File

@ -6,19 +6,20 @@
*) *)
open! IStd open! IStd
let get_java_class_initializer_summary_of caller_summary = let get_java_class_initializer_summary_of {InterproceduralAnalysis.proc_desc; analyze_dependency} =
let procname = Summary.get_proc_name caller_summary in let procname = Procdesc.get_proc_name proc_desc in
match procname with match procname with
| Procname.Java _ -> | Procname.Java _ ->
Procname.get_class_type_name procname Procname.get_class_type_name procname
|> Option.map ~f:(fun tname -> Procname.(Java (Java.get_class_initializer tname))) |> Option.map ~f:(fun tname -> Procname.(Java (Java.get_class_initializer tname)))
|> Option.bind ~f:(Ondemand.analyze_proc_name ~caller_summary) |> Option.bind ~f:analyze_dependency |> Option.map ~f:snd
| _ -> | _ ->
None None
let get_java_constructor_summaries_of tenv caller_summary = let get_java_constructor_summaries_of {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency}
let procname = Summary.get_proc_name caller_summary in =
let procname = Procdesc.get_proc_name proc_desc in
Procname.get_class_type_name procname Procname.get_class_type_name procname
(* retrieve its definition *) (* retrieve its definition *)
|> Option.bind ~f:(Tenv.lookup tenv) |> Option.bind ~f:(Tenv.lookup tenv)
@ -27,4 +28,4 @@ let get_java_constructor_summaries_of tenv caller_summary =
(* keep only the constructors *) (* keep only the constructors *)
|> List.filter ~f:Procname.(function Java jname -> Java.is_constructor jname | _ -> false) |> List.filter ~f:Procname.(function Java jname -> Java.is_constructor jname | _ -> false)
(* get the summaries of the constructors *) (* get the summaries of the constructors *)
|> List.filter_map ~f:(Ondemand.analyze_proc_name ~caller_summary) |> List.filter_map ~f:(fun pname -> analyze_dependency pname |> Option.map ~f:snd)

4
infer/src/concurrency/ConcurrencyUtils.mli
Unescape View File

@ -6,6 +6,6 @@
*) *)
open! IStd open! IStd
val get_java_class_initializer_summary_of : Summary.t -> Summary.t option val get_java_class_initializer_summary_of : 'payload InterproceduralAnalysis.t -> 'payload option
val get_java_constructor_summaries_of : Tenv.t -> Summary.t -> Summary.t list val get_java_constructor_summaries_of : 'payload InterproceduralAnalysis.t -> 'payload list

140
infer/src/concurrency/RacerD.ml
Unescape View File

@ -11,17 +11,14 @@ module F = Format
module L = Logging module L = Logging
module MF = MarkupFormatter module MF = MarkupFormatter
module Payload = SummaryPayload.Make (struct type analysis_data =
type t = RacerDDomain.summary {interproc: RacerDDomain.summary InterproceduralAnalysis.t; formals: FormalMap.t}
let field = Payloads.Fields.racerd
end)
module TransferFunctions (CFG : ProcCfg.S) = struct module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG module CFG = CFG
module Domain = RacerDDomain module Domain = RacerDDomain
type analysis_data = FormalMap.t ProcData.t type nonrec analysis_data = analysis_data
let rec get_access_exp = function let rec get_access_exp = function
| HilExp.AccessExpression access_expr -> | HilExp.AccessExpression access_expr ->
@ -63,10 +60,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_field_accesses base acc accesses ) add_field_accesses base acc accesses )
let make_container_access proc_data ret_base callee_pname ~is_write receiver_ap callee_loc let make_container_access {interproc= {tenv}; formals} ret_base callee_pname ~is_write receiver_ap
(astate : Domain.t) = callee_loc (astate : Domain.t) =
let open Domain in let open Domain in
let ProcData.{extras= formals; tenv} = proc_data in
if if
AttributeMapDomain.is_synchronized astate.attribute_map receiver_ap AttributeMapDomain.is_synchronized astate.attribute_map receiver_ap
|| RacerDModels.is_synchronized_container callee_pname receiver_ap tenv || RacerDModels.is_synchronized_container callee_pname receiver_ap tenv
@ -191,25 +187,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate with ownership} {astate with ownership}
let do_container_access ~is_write ret_base callee_pname actuals loc proc_data astate = let do_container_access ~is_write ret_base callee_pname actuals loc analysis_data astate =
match get_first_actual actuals with match get_first_actual actuals with
| Some receiver_expr -> | Some receiver_expr ->
make_container_access proc_data ret_base callee_pname ~is_write receiver_expr loc astate make_container_access analysis_data ret_base callee_pname ~is_write receiver_expr loc astate
| None -> | None ->
L.internal_error "Call to %a is marked as a container access, but has no receiver" L.internal_error "Call to %a is marked as a container access, but has no receiver"
Procname.pp callee_pname ; Procname.pp callee_pname ;
astate astate
let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; summary; extras} let do_proc_call ret_base callee_pname actuals call_flags loc
(astate : Domain.t) = {interproc= {tenv; analyze_dependency}; formals} (astate : Domain.t) =
let open Domain in let open Domain in
let open RacerDModels in let open RacerDModels in
let open ConcurrencyModels in let open ConcurrencyModels in
let ret_access_exp = AccessExpression.base ret_base in let ret_access_exp = AccessExpression.base ret_base in
let astate = let astate =
if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then
Domain.add_unannotated_call_access extras callee_pname actuals loc astate Domain.add_unannotated_call_access formals callee_pname actuals loc astate
else astate else astate
in in
let astate = let astate =
@ -258,11 +254,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate astate
| NoEffect -> ( | NoEffect -> (
let rebased_summary_opt = let rebased_summary_opt =
Payload.read ~caller_summary:summary ~callee_pname analyze_dependency callee_pname
|> Option.map ~f:(fun summary -> |> Option.map ~f:(fun (callee_proc_desc, summary) ->
let rebased_accesses = let rebased_accesses =
Ondemand.get_proc_desc callee_pname expand_actuals formals actuals summary.accesses callee_proc_desc
|> Option.fold ~init:summary.accesses ~f:(expand_actuals extras actuals)
in in
{summary with accesses= rebased_accesses} ) {summary with accesses= rebased_accesses} )
in in
@ -272,7 +267,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
LockDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks LockDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks
in in
let accesses = let accesses =
add_callee_accesses extras astate accesses locks threads actuals callee_pname loc add_callee_accesses formals astate accesses locks threads actuals callee_pname loc
in in
let ownership = let ownership =
OwnershipDomain.propagate_return ret_access_exp return_ownership actuals OwnershipDomain.propagate_return ret_access_exp return_ownership actuals
@ -306,11 +301,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate_callee with ownership; attribute_map} {astate_callee with ownership; attribute_map}
let do_assignment lhs_access_exp rhs_exp loc {ProcData.tenv; extras} (astate : Domain.t) = let do_assignment lhs_access_exp rhs_exp loc {interproc= {tenv}; formals} (astate : Domain.t) =
let open Domain in let open Domain in
let rhs_accesses = let rhs_accesses =
add_access extras loc ~is_write_access:false astate.locks astate.threads astate.ownership tenv add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership
astate.accesses rhs_exp tenv astate.accesses rhs_exp
in in
let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in
let is_functional = let is_functional =
@ -332,7 +327,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
report spurious read/write races *) report spurious read/write races *)
rhs_accesses rhs_accesses
else else
add_access extras loc ~is_write_access:true astate.locks astate.threads astate.ownership add_access formals loc ~is_write_access:true astate.locks astate.threads astate.ownership
tenv rhs_accesses (HilExp.AccessExpression lhs_access_exp) tenv rhs_accesses (HilExp.AccessExpression lhs_access_exp)
in in
let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in
@ -378,25 +373,25 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate' with accesses} {astate' with accesses}
let exec_instr astate ({ProcData.summary; extras; tenv} as proc_data) _ instr = let exec_instr astate ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ instr =
match (instr : HilInstr.t) with match (instr : HilInstr.t) with
| Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
let astate = add_reads extras actuals loc astate tenv in let astate = add_reads formals actuals loc astate tenv in
if RacerDModels.acquires_ownership callee_pname tenv then if RacerDModels.acquires_ownership callee_pname tenv then
do_call_acquiring_ownership ret_base astate do_call_acquiring_ownership ret_base astate
else if RacerDModels.is_container_write tenv callee_pname then else if RacerDModels.is_container_write tenv callee_pname then
do_container_access ~is_write:true ret_base callee_pname actuals loc proc_data astate do_container_access ~is_write:true ret_base callee_pname actuals loc analysis_data astate
else if RacerDModels.is_container_read tenv callee_pname then else if RacerDModels.is_container_read tenv callee_pname then
do_container_access ~is_write:false ret_base callee_pname actuals loc proc_data astate do_container_access ~is_write:false ret_base callee_pname actuals loc analysis_data astate
else do_proc_call ret_base callee_pname actuals call_flags loc proc_data astate else do_proc_call ret_base callee_pname actuals call_flags loc analysis_data astate
| Call (_, Indirect _, _, _, _) -> | Call (_, Indirect _, _, _, _) ->
if Procname.is_java (Summary.get_proc_name summary) then if Procname.is_java (Procdesc.get_proc_name proc_desc) then
L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr
else astate else astate
| Assign (lhs_access_expr, rhs_exp, loc) -> | Assign (lhs_access_expr, rhs_exp, loc) ->
do_assignment lhs_access_expr rhs_exp loc proc_data astate do_assignment lhs_access_expr rhs_exp loc analysis_data astate
| Assume (assume_exp, _, _, loc) -> | Assume (assume_exp, _, _, loc) ->
do_assume extras assume_exp loc tenv astate do_assume formals assume_exp loc tenv astate
| Metadata _ -> | Metadata _ ->
astate astate
@ -407,20 +402,20 @@ end
module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal)) module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal))
(** Compute the attributes (of static variables) set up by the class initializer. *) (** Compute the attributes (of static variables) set up by the class initializer. *)
let set_class_init_attributes summary (astate : RacerDDomain.t) = let set_class_init_attributes interproc (astate : RacerDDomain.t) =
let open RacerDDomain in let open RacerDDomain in
let attribute_map = let attribute_map =
ConcurrencyUtils.get_java_class_initializer_summary_of summary ConcurrencyUtils.get_java_class_initializer_summary_of interproc
|> Option.bind ~f:Payload.of_summary
|> Option.value_map ~default:AttributeMapDomain.top ~f:(fun summary -> summary.attributes) |> Option.value_map ~default:AttributeMapDomain.top ~f:(fun summary -> summary.attributes)
in in
({astate with attribute_map} : t) ({astate with attribute_map} : t)
(** Compute the attributes of instance variables that all constructors agree on. *) (** Compute the attributes of instance variables that all constructors agree on. *)
let set_constructor_attributes tenv summary (astate : RacerDDomain.t) = let set_constructor_attributes ({InterproceduralAnalysis.proc_desc} as interproc)
(astate : RacerDDomain.t) =
let open RacerDDomain in let open RacerDDomain in
let procname = Summary.get_proc_name summary in let procname = Procdesc.get_proc_name proc_desc in
(* make a local [this] variable, for replacing all constructor attribute map keys' roots *) (* make a local [this] variable, for replacing all constructor attribute map keys' roots *)
let local_this = Pvar.mk Mangled.this procname |> Var.of_pvar in let local_this = Pvar.mk Mangled.this procname |> Var.of_pvar in
let make_local exp = let make_local exp =
@ -437,8 +432,7 @@ let set_constructor_attributes tenv summary (astate : RacerDDomain.t) =
AttributeMapDomain.(fold (fun exp attr acc -> add (make_local exp) attr acc) attributes empty) AttributeMapDomain.(fold (fun exp attr acc -> add (make_local exp) attr acc) attributes empty)
in in
let attribute_map = let attribute_map =
ConcurrencyUtils.get_java_constructor_summaries_of tenv summary ConcurrencyUtils.get_java_constructor_summaries_of interproc
|> List.filter_map ~f:Payload.of_summary
(* make instances of [this] local to the current procedure and select only the attributes *) (* make instances of [this] local to the current procedure and select only the attributes *)
|> List.map ~f:(fun (summary : summary) -> localize_attrs summary.attributes) |> List.map ~f:(fun (summary : summary) -> localize_attrs summary.attributes)
(* join all the attribute maps together *) (* join all the attribute maps together *)
@ -448,8 +442,8 @@ let set_constructor_attributes tenv summary (astate : RacerDDomain.t) =
{astate with attribute_map} {astate with attribute_map}
let set_initial_attributes tenv summary astate = let set_initial_attributes ({InterproceduralAnalysis.proc_desc} as interproc) astate =
let procname = Summary.get_proc_name summary in let procname = Procdesc.get_proc_name proc_desc in
match procname with match procname with
| Procname.Java java_pname when Procname.Java.is_class_initializer java_pname -> | Procname.Java java_pname when Procname.Java.is_class_initializer java_pname ->
(* we are analyzing the class initializer, don't go through on-demand again *) (* we are analyzing the class initializer, don't go through on-demand again *)
@ -458,20 +452,18 @@ let set_initial_attributes tenv summary astate =
-> ->
(* analyzing a constructor or static method, so we need the attributes established by the (* analyzing a constructor or static method, so we need the attributes established by the
class initializer *) class initializer *)
set_class_init_attributes summary astate set_class_init_attributes interproc astate
| Procname.Java _ -> | Procname.Java _ ->
(* we are analyzing an instance method, so we need constructor-established attributes (* we are analyzing an instance method, so we need constructor-established attributes
which will include those by the class initializer *) which will include those by the class initializer *)
set_constructor_attributes tenv summary astate set_constructor_attributes interproc astate
| _ -> | _ ->
astate astate
let analyze_procedure {Callbacks.exe_env; summary} = let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv} as interproc) =
let open RacerDDomain in let open RacerDDomain in
let proc_desc = Summary.get_proc_desc summary in let proc_name = Procdesc.get_proc_name proc_desc in
let proc_name = Summary.get_proc_name summary in
let tenv = Exe_env.get_tenv exe_env proc_name in
let open ConcurrencyModels in let open ConcurrencyModels in
let add_owned_formal acc base = OwnershipDomain.add base OwnershipAbstractValue.owned acc in let add_owned_formal acc base = OwnershipDomain.add base OwnershipAbstractValue.owned acc in
let add_conditionally_owned_formal = let add_conditionally_owned_formal =
@ -521,13 +513,12 @@ let analyze_procedure {Callbacks.exe_env; summary} =
add_owned_formal acc base add_owned_formal acc base
else add_conditionally_owned_formal acc base index ) else add_conditionally_owned_formal acc base index )
in in
let initial = set_initial_attributes tenv summary {bottom with ownership; threads; locks} in let initial = set_initial_attributes interproc {bottom with ownership; threads; locks} in
let formal_map = FormalMap.make proc_desc in let formals = FormalMap.make proc_desc in
let proc_data = {ProcData.summary; tenv; extras= formal_map} in let analysis_data = {interproc; formals} in
Analyzer.compute_post proc_data ~initial proc_desc Analyzer.compute_post analysis_data ~initial proc_desc
|> Option.map ~f:(astate_to_summary proc_desc formal_map) |> Option.map ~f:(astate_to_summary proc_desc formals)
|> Option.value_map ~default:summary ~f:(fun post -> Payload.update_summary post summary) else Some empty_summary
else Payload.update_summary empty_summary summary
type conflict = RacerDDomain.AccessSnapshot.t type conflict = RacerDDomain.AccessSnapshot.t
@ -1074,18 +1065,16 @@ let make_results_table exe_env summaries =
(fun snapshot acc -> ReportMap.add {threads; snapshot; tenv; procname} acc) (fun snapshot acc -> ReportMap.add {threads; snapshot; tenv; procname} acc)
accesses acc accesses acc
in in
List.fold summaries ~init:ReportMap.empty ~f:(fun acc (summary : Summary.t) -> List.fold summaries ~init:ReportMap.empty ~f:(fun acc (proc_desc, summary) ->
let procname = Summary.get_proc_name summary in let procname = Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env procname in let tenv = Exe_env.get_tenv exe_env procname in
Payloads.racerd summary.payloads |> Option.fold ~init:acc ~f:(aggregate_post tenv procname) ) aggregate_post tenv procname acc summary )
let class_has_concurrent_method class_summaries = let class_has_concurrent_method class_summaries =
let open RacerDDomain in let open RacerDDomain in
let method_has_concurrent_context (summary : Summary.t) = let method_has_concurrent_context (_, summary) =
Payloads.racerd summary.payloads match (summary.threads : ThreadsDomain.t) with NoThread -> false | _ -> true
|> Option.exists ~f:(fun (payload : summary) ->
match (payload.threads : ThreadsDomain.t) with NoThread -> false | _ -> true )
in in
List.exists class_summaries ~f:method_has_concurrent_context List.exists class_summaries ~f:method_has_concurrent_context
@ -1102,32 +1091,33 @@ let should_report_on_class (classname : Typ.Name.t) class_summaries =
let filter_reportable_classes class_map = Typ.Name.Map.filter should_report_on_class class_map let filter_reportable_classes class_map = Typ.Name.Map.filter should_report_on_class class_map
(* aggregate all of the procedures in the file env by their declaring (** aggregate all of the procedures in the file env by their declaring class. this lets us analyze
class. this lets us analyze each class individually *) each class individually *)
let aggregate_by_class exe_env procedures = let aggregate_by_class {InterproceduralAnalysis.procedures; file_exe_env; analyze_file_dependency} =
List.fold procedures ~init:Typ.Name.Map.empty ~f:(fun acc procname -> List.fold procedures ~init:Typ.Name.Map.empty ~f:(fun acc procname ->
Procname.get_class_type_name procname Procname.get_class_type_name procname
|> Option.bind ~f:(fun classname -> |> Option.bind ~f:(fun classname ->
Ondemand.analyze_proc_name_no_caller procname analyze_file_dependency procname
|> Option.filter ~f:(fun summary -> |> Option.filter ~f:(fun (pdesc, _) ->
let pdesc = Summary.get_proc_desc summary in let tenv = Exe_env.get_tenv file_exe_env procname in
let tenv = Exe_env.get_tenv exe_env procname in
should_report_on_proc tenv pdesc ) should_report_on_proc tenv pdesc )
|> Option.map ~f:(fun summary -> |> Option.map ~f:(fun summary_proc_desc ->
Typ.Name.Map.update classname Typ.Name.Map.update classname
(function (function
| None -> Some [summary] | Some summaries -> Some (summary :: summaries) ) | None ->
Some [summary_proc_desc]
| Some summaries ->
Some (summary_proc_desc :: summaries) )
acc ) ) acc ) )
|> Option.value ~default:acc ) |> Option.value ~default:acc )
|> filter_reportable_classes |> filter_reportable_classes
(* Gathers results by analyzing all the methods in a file, then (** Gathers results by analyzing all the methods in a file, then post-processes the results to check
post-processes the results to check an (approximation of) thread an (approximation of) thread safety *)
safety *) let file_analysis ({InterproceduralAnalysis.file_exe_env} as file_t) =
let file_analysis ({procedures; exe_env} : Callbacks.file_callback_args) = let class_map = aggregate_by_class file_t in
let class_map = aggregate_by_class exe_env procedures in
Typ.Name.Map.fold Typ.Name.Map.fold
(fun classname methods issue_log -> (fun classname methods issue_log ->
make_results_table exe_env methods |> report_unsafe_accesses ~issue_log classname ) make_results_table file_exe_env methods |> report_unsafe_accesses ~issue_log classname )
class_map IssueLog.empty class_map IssueLog.empty

5
infer/src/concurrency/RacerD.mli
Unescape View File

@ -7,6 +7,7 @@
open! IStd open! IStd
val file_analysis : Callbacks.file_callback_t val file_analysis : RacerDDomain.summary InterproceduralAnalysis.file_t -> IssueLog.t
val analyze_procedure : Callbacks.proc_callback_t val analyze_procedure :
RacerDDomain.summary InterproceduralAnalysis.t -> RacerDDomain.summary option

57
infer/src/concurrency/starvation.ml
Unescape View File

@ -4,6 +4,7 @@
* This source code is licensed under the MIT license found in the * This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree. * LICENSE file in the root directory of this source tree.
*) *)
open! IStd open! IStd
module F = Format module F = Format
module L = Logging module L = Logging
@ -12,17 +13,14 @@ module Domain = StarvationDomain
let pname_pp = MF.wrap_monospaced Procname.pp let pname_pp = MF.wrap_monospaced Procname.pp
module Payload = SummaryPayload.Make (struct type analysis_data =
type t = Domain.summary {interproc: StarvationDomain.summary InterproceduralAnalysis.t; formals: FormalMap.t}
let field = Payloads.Fields.starvation
end)
module TransferFunctions (CFG : ProcCfg.S) = struct module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG module CFG = CFG
module Domain = Domain module Domain = Domain
type analysis_data = FormalMap.t ProcData.t type nonrec analysis_data = analysis_data
let log_parse_error error pname actuals = let log_parse_error error pname actuals =
L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Procname.pp pname L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Procname.pp pname
@ -115,7 +113,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate with attributes} ) {astate with attributes} )
let do_call ProcData.{tenv; summary; extras} lhs callee actuals loc (astate : Domain.t) = let do_call {interproc= {tenv; analyze_dependency}; formals} lhs callee actuals loc
(astate : Domain.t) =
let open Domain in let open Domain in
let make_ret_attr return_attribute = {empty_summary with return_attribute} in let make_ret_attr return_attribute = {empty_summary with return_attribute} in
let make_thread thread = {empty_summary with thread} in let make_thread thread = {empty_summary with thread} in
@ -146,7 +145,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
Some (make_ret_attr (Looper ForUIThread)) Some (make_ret_attr (Looper ForUIThread))
else None else None
in in
let get_callee_summary () = Payload.read ~caller_summary:summary ~callee_pname:callee in let get_callee_summary () = analyze_dependency callee |> Option.map ~f:snd in
let treat_handler_constructor () = let treat_handler_constructor () =
if StarvationModels.is_handler_constructor tenv callee actuals then if StarvationModels.is_handler_constructor tenv callee actuals then
match actuals_acc_exps with match actuals_acc_exps with
@ -203,7 +202,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
; get_mainLooper_summary ; get_mainLooper_summary
; get_callee_summary ] ; get_callee_summary ]
|> Option.map ~f:(fun summary -> |> Option.map ~f:(fun summary ->
let subst = Lock.make_subst extras actuals in let subst = Lock.make_subst formals actuals in
let callsite = CallSite.make callee loc in let callsite = CallSite.make callee loc in
Domain.integrate_summary ~tenv ~lhs ~subst callsite astate summary ) Domain.integrate_summary ~tenv ~lhs ~subst callsite astate summary )
in in
@ -212,12 +211,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|> Option.value ~default:astate |> Option.value ~default:astate
let exec_instr (astate : Domain.t) ({ProcData.summary; tenv; extras} as procdata) _ let exec_instr (astate : Domain.t) ({interproc= {proc_desc; tenv}; formals} as analysis_data) _
(instr : HilInstr.t) = (instr : HilInstr.t) =
let open ConcurrencyModels in let open ConcurrencyModels in
let open StarvationModels in let open StarvationModels in
let get_lock_path = Domain.Lock.make extras in let get_lock_path = Domain.Lock.make formals in
let procname = Summary.get_proc_name summary in let procname = Procdesc.get_proc_name proc_desc in
let is_java = Procname.is_java procname in let is_java = Procname.is_java procname in
let do_lock locks loc astate = let do_lock locks loc astate =
List.filter_map ~f:get_lock_path locks |> Domain.acquire ~tenv astate ~procname ~loc List.filter_map ~f:get_lock_path locks |> Domain.acquire ~tenv astate ~procname ~loc
@ -264,7 +263,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| NoEffect when is_java && is_strict_mode_violation tenv callee actuals -> | NoEffect when is_java && is_strict_mode_violation tenv callee actuals ->
Domain.strict_mode_call ~callee ~loc astate Domain.strict_mode_call ~callee ~loc astate
| NoEffect when is_java && is_monitor_wait tenv callee actuals -> | NoEffect when is_java && is_monitor_wait tenv callee actuals ->
Domain.wait_on_monitor ~loc extras actuals astate Domain.wait_on_monitor ~loc formals actuals astate
| NoEffect when is_java && is_future_get tenv callee actuals -> | NoEffect when is_java && is_future_get tenv callee actuals ->
Domain.future_get ~callee ~loc actuals astate Domain.future_get ~callee ~loc actuals astate
| NoEffect when is_java -> ( | NoEffect when is_java -> (
@ -274,11 +273,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Some sev -> | Some sev ->
Domain.blocking_call ~callee sev ~loc astate Domain.blocking_call ~callee sev ~loc astate
| None -> | None ->
do_call procdata ret_exp callee actuals loc astate ) do_call analysis_data ret_exp callee actuals loc astate )
| NoEffect -> | NoEffect ->
(* in C++/Obj C we only care about deadlocks, not starvation errors *) (* in C++/Obj C we only care about deadlocks, not starvation errors *)
let ret_exp = HilExp.AccessExpression.base ret_base in let ret_exp = HilExp.AccessExpression.base ret_base in
do_call procdata ret_exp callee actuals loc astate ) do_call analysis_data ret_exp callee actuals loc astate )
let pp_session_name _node fmt = F.pp_print_string fmt "starvation" let pp_session_name _node fmt = F.pp_print_string fmt "starvation"
@ -291,15 +290,15 @@ let set_class_init_attributes procname (astate : Domain.t) =
let open Domain in let open Domain in
let attributes = let attributes =
ConcurrencyUtils.get_java_class_initializer_summary_of procname ConcurrencyUtils.get_java_class_initializer_summary_of procname
|> Option.bind ~f:Payload.of_summary
|> Option.value_map ~default:AttributeDomain.top ~f:(fun summary -> summary.attributes) |> Option.value_map ~default:AttributeDomain.top ~f:(fun summary -> summary.attributes)
in in
({astate with attributes} : t) ({astate with attributes} : t)
(** Compute the attributes of instance variables that all constructors agree on. *) (** Compute the attributes of instance variables that all constructors agree on. *)
let set_constructor_attributes tenv summary (astate : Domain.t) = let set_constructor_attributes ({InterproceduralAnalysis.proc_desc} as interproc)
let procname = Summary.get_proc_name summary in (astate : Domain.t) =
let procname = Procdesc.get_proc_name proc_desc in
let open Domain in let open Domain in
(* make a local [this] variable, for replacing all constructor attribute map keys' roots *) (* make a local [this] variable, for replacing all constructor attribute map keys' roots *)
let local_this = Pvar.mk Mangled.this procname |> Var.of_pvar in let local_this = Pvar.mk Mangled.this procname |> Var.of_pvar in
@ -317,8 +316,7 @@ let set_constructor_attributes tenv summary (astate : Domain.t) =
AttributeDomain.(fold (fun exp attr acc -> add (make_local exp) attr acc) attributes empty) AttributeDomain.(fold (fun exp attr acc -> add (make_local exp) attr acc) attributes empty)
in in
let attributes = let attributes =
ConcurrencyUtils.get_java_constructor_summaries_of tenv summary ConcurrencyUtils.get_java_constructor_summaries_of interproc
|> List.filter_map ~f:Payload.of_summary
(* make instances of [this] local to the current procedure and select only the attributes *) (* make instances of [this] local to the current procedure and select only the attributes *)
|> List.map ~f:(fun (summary : Domain.summary) -> localize_attrs summary.attributes) |> List.map ~f:(fun (summary : Domain.summary) -> localize_attrs summary.attributes)
(* join all the attribute maps together *) (* join all the attribute maps together *)
@ -328,8 +326,8 @@ let set_constructor_attributes tenv summary (astate : Domain.t) =
{astate with attributes} {astate with attributes}
let set_initial_attributes tenv summary astate = let set_initial_attributes ({InterproceduralAnalysis.proc_desc} as interproc) astate =
let procname = Summary.get_proc_name summary in let procname = Procdesc.get_proc_name proc_desc in
if not Config.starvation_whole_program then astate if not Config.starvation_whole_program then astate
else else
match procname with match procname with
@ -340,23 +338,21 @@ let set_initial_attributes tenv summary astate =
when Procname.Java.(is_constructor java_pname || is_static java_pname) -> when Procname.Java.(is_constructor java_pname || is_static java_pname) ->
(* analyzing a constructor or static method, so we need the attributes established by the (* analyzing a constructor or static method, so we need the attributes established by the
class initializer *) class initializer *)
set_class_init_attributes summary astate set_class_init_attributes interproc astate
| Procname.Java _ -> | Procname.Java _ ->
(* we are analyzing an instance method, so we need constructor-established attributes (* we are analyzing an instance method, so we need constructor-established attributes
which will include those by the class initializer *) which will include those by the class initializer *)
set_constructor_attributes tenv summary astate set_constructor_attributes interproc astate
| _ -> | _ ->
astate astate
let analyze_procedure {Callbacks.exe_env; summary} = let analyze_procedure ({InterproceduralAnalysis.proc_desc; tenv} as interproc) =
let proc_desc = Summary.get_proc_desc summary in
let procname = Procdesc.get_proc_name proc_desc in let procname = Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env procname in if StarvationModels.should_skip_analysis tenv procname [] then None
if StarvationModels.should_skip_analysis tenv procname [] then summary
else else
let formals = FormalMap.make proc_desc in let formals = FormalMap.make proc_desc in
let proc_data = {ProcData.summary; tenv; extras= formals} in let proc_data = {interproc; formals} in
let loc = Procdesc.get_loc proc_desc in let loc = Procdesc.get_loc proc_desc in
let set_lock_state_for_synchronized_proc astate = let set_lock_state_for_synchronized_proc astate =
if Procdesc.is_java_synchronized proc_desc then if Procdesc.is_java_synchronized proc_desc then
@ -381,13 +377,12 @@ let analyze_procedure {Callbacks.exe_env; summary} =
let initial = let initial =
Domain.bottom Domain.bottom
(* set the attributes of instance variables set up by all constructors or the class initializer *) (* set the attributes of instance variables set up by all constructors or the class initializer *)
|> set_initial_attributes tenv summary |> set_initial_attributes interproc
|> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation
in in
Analyzer.compute_post proc_data ~initial proc_desc Analyzer.compute_post proc_data ~initial proc_desc
|> Option.map ~f:filter_blocks |> Option.map ~f:filter_blocks
|> Option.map ~f:(Domain.summary_of_astate proc_desc) |> Option.map ~f:(Domain.summary_of_astate proc_desc)
|> Option.fold ~init:summary ~f:(fun acc payload -> Payload.update_summary payload acc)
(** per-file report map, which takes care of deduplication *) (** per-file report map, which takes care of deduplication *)

3
infer/src/concurrency/starvation.mli
Unescape View File

@ -7,7 +7,8 @@
open! IStd open! IStd
val analyze_procedure : Callbacks.proc_callback_t val analyze_procedure :
StarvationDomain.summary InterproceduralAnalysis.t -> StarvationDomain.summary option
val reporting : StarvationDomain.summary InterproceduralAnalysis.file_t -> IssueLog.t val reporting : StarvationDomain.summary InterproceduralAnalysis.file_t -> IssueLog.t

Write Preview
Loading…
Cancel
Save