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

make annot reach an `interprocedural`

Browse Source 
Summary: Making checkers/ its own dune library.

Reviewed By: ngorogiannis

Differential Revision: D21407073

fbshipit-source-id: 34f2b8b53
master
Jules Villard 5 years ago committed by Facebook GitHub Bot
parent 87f031ec38
commit 34ae47a1b3
3 changed files with 74 additions and 67 deletions
Show Stats Download Patch File Download Diff File

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

@ -214,8 +214,10 @@ let all_checkers =
; { name= "annotation reachability" ; { name= "annotation reachability"
; active= Config.is_checker_enabled AnnotationReachability ; active= Config.is_checker_enabled AnnotationReachability
; callbacks= ; callbacks=
[ (Procedure AnnotationReachability.checker, Language.Java) (let annot_reach =
; (Procedure AnnotationReachability.checker, Language.Clang) ] } ] interprocedural Payloads.Fields.annot_map AnnotationReachability.checker
in
[(annot_reach, Language.Java); (annot_reach, Language.Clang)] ) } ]
let get_active_checkers () = let get_active_checkers () =

132
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -15,12 +15,6 @@ let dummy_constructor_annot = "__infer_is_constructor"
module Domain = AnnotationReachabilityDomain module Domain = AnnotationReachabilityDomain
module Payload = SummaryPayload.Make (struct
type t = Domain.t
let field = Payloads.Fields.annot_map
end)
let is_modeled_expensive tenv = function let is_modeled_expensive tenv = function
| Procname.Java proc_name_java as proc_name -> | Procname.Java proc_name_java as proc_name ->
(not (BuiltinDecl.is_declared proc_name)) (not (BuiltinDecl.is_declared proc_name))
@ -67,9 +61,9 @@ let method_has_annot annot tenv pname =
let method_overrides_annot annot tenv pname = method_overrides (method_has_annot annot) tenv pname let method_overrides_annot annot tenv pname = method_overrides (method_has_annot annot) tenv pname
let lookup_annotation_calls ~caller_summary annot pname = let lookup_annotation_calls {InterproceduralAnalysis.analyze_dependency} annot pname =
Payload.read ~caller_summary ~callee_pname:pname analyze_dependency pname
|> Option.bind ~f:(Domain.find_opt annot) |> Option.bind ~f:(fun (_, astate) -> Domain.find_opt annot astate)
|> Option.value ~default:Domain.SinkMap.empty |> Option.value ~default:Domain.SinkMap.empty
@ -80,8 +74,9 @@ let update_trace loc trace =
let string_of_pname = Procname.to_simplified_string ~withclass:true let string_of_pname = Procname.to_simplified_string ~withclass:true
let report_allocation_stack src_annot summary fst_call_loc trace constructor_pname call_loc = let report_allocation_stack {InterproceduralAnalysis.proc_desc; err_log} src_annot fst_call_loc
let pname = Summary.get_proc_name summary in trace constructor_pname call_loc =
let pname = Procdesc.get_proc_name proc_desc in
let final_trace = List.rev (update_trace call_loc trace) in let final_trace = List.rev (update_trace call_loc trace) in
let constr_str = string_of_pname constructor_pname in let constr_str = string_of_pname constructor_pname in
let description = let description =
@ -90,14 +85,16 @@ let report_allocation_stack src_annot summary fst_call_loc trace constructor_pna
MF.pp_monospaced ("@" ^ src_annot) MF.pp_monospaced constr_str MF.pp_monospaced MF.pp_monospaced ("@" ^ src_annot) MF.pp_monospaced constr_str MF.pp_monospaced
("new " ^ constr_str) ("new " ^ constr_str)
in in
SummaryReporting.log_error summary ~loc:fst_call_loc ~ltr:final_trace let attrs = Procdesc.get_attributes proc_desc in
Reporting.log_error attrs err_log ~loc:fst_call_loc ~ltr:final_trace
IssueType.checkers_allocates_memory description IssueType.checkers_allocates_memory description
let report_annotation_stack src_annot snk_annot src_summary loc trace snk_pname call_loc = let report_annotation_stack ({InterproceduralAnalysis.proc_desc; err_log} as analysis_data)
let src_pname = Summary.get_proc_name src_summary in src_annot snk_annot loc trace snk_pname call_loc =
let src_pname = Procdesc.get_proc_name proc_desc in
if String.equal snk_annot dummy_constructor_annot then if String.equal snk_annot dummy_constructor_annot then
report_allocation_stack src_annot src_summary loc trace snk_pname call_loc report_allocation_stack analysis_data src_annot loc trace snk_pname call_loc
else else
let final_trace = List.rev (update_trace call_loc trace) in let final_trace = List.rev (update_trace call_loc trace) in
let exp_pname_str = string_of_pname snk_pname in let exp_pname_str = string_of_pname snk_pname in
@ -113,15 +110,17 @@ let report_annotation_stack src_annot snk_annot src_summary loc trace snk_pname
IssueType.checkers_calls_expensive_method IssueType.checkers_calls_expensive_method
else IssueType.checkers_annotation_reachability_error else IssueType.checkers_annotation_reachability_error
in in
SummaryReporting.log_error src_summary ~loc ~ltr:final_trace issue_type description let attrs = Procdesc.get_attributes proc_desc in
Reporting.log_error attrs err_log ~loc ~ltr:final_trace issue_type description
let report_call_stack summary end_of_stack lookup_next_calls report call_site sink_map = let report_call_stack end_of_stack lookup_next_calls report call_site sink_map =
let lookup_location pname = let lookup_location pname =
Option.value_map ~f:Procdesc.get_loc ~default:Location.dummy (Ondemand.get_proc_desc pname) Option.value_map ~f:Procdesc.get_loc ~default:Location.dummy
(AnalysisCallbacks.get_proc_desc pname)
in in
let rec loop fst_call_loc visited_pnames trace (callee_pname, call_loc) = let rec loop fst_call_loc visited_pnames trace (callee_pname, call_loc) =
if end_of_stack callee_pname then report summary fst_call_loc trace callee_pname call_loc if end_of_stack callee_pname then report fst_call_loc trace callee_pname call_loc
else else
let callee_def_loc = lookup_location callee_pname in let callee_def_loc = lookup_location callee_pname in
let next_calls = lookup_next_calls callee_pname in let next_calls = lookup_next_calls callee_pname in
@ -152,15 +151,16 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si
sink_map sink_map
let report_src_snk_path {Callbacks.exe_env; summary} sink_map snk_annot src_annot = let report_src_snk_path ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) sink_map
let proc_desc = Summary.get_proc_desc summary in snk_annot src_annot =
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env proc_name in
let loc = Procdesc.get_loc proc_desc in let loc = Procdesc.get_loc proc_desc in
if method_overrides_annot src_annot tenv proc_name then if method_overrides_annot src_annot tenv proc_name then
let f_report = report_annotation_stack src_annot.Annot.class_name snk_annot.Annot.class_name in let f_report =
report_call_stack summary (method_has_annot snk_annot tenv) report_annotation_stack analysis_data src_annot.Annot.class_name snk_annot.Annot.class_name
(lookup_annotation_calls ~caller_summary:summary snk_annot) in
report_call_stack (method_has_annot snk_annot tenv)
(lookup_annotation_calls analysis_data snk_annot)
f_report (CallSite.make proc_name loc) sink_map f_report (CallSite.make proc_name loc) sink_map
@ -182,7 +182,7 @@ module AnnotationSpec = struct
; sink_predicate: predicate ; sink_predicate: predicate
; sanitizer_predicate: predicate ; sanitizer_predicate: predicate
; sink_annotation: Annot.t ; sink_annotation: Annot.t
; report: Callbacks.proc_callback_args -> Domain.t -> unit } ; report: Domain.t InterproceduralAnalysis.t -> Domain.t -> unit }
(* The default sanitizer does not sanitize anything *) (* The default sanitizer does not sanitize anything *)
let default_sanitizer _ _ = false let default_sanitizer _ _ = false
@ -207,7 +207,7 @@ end
module CxxAnnotationSpecs = struct module CxxAnnotationSpecs = struct
let src_path_of pname = let src_path_of pname =
match Ondemand.get_proc_desc pname with match AnalysisCallbacks.get_proc_desc pname with
| Some proc_desc -> | Some proc_desc ->
let loc = Procdesc.get_loc proc_desc in let loc = Procdesc.get_loc proc_desc in
SourceFile.to_string loc.file SourceFile.to_string loc.file
@ -314,8 +314,9 @@ module CxxAnnotationSpecs = struct
in in
let sanitizer_pred = debug_pred ~spec_name ~desc:"sanitizer" sanitizer_pred in let sanitizer_pred = debug_pred ~spec_name ~desc:"sanitizer" sanitizer_pred in
let call_str = "\n -> " in let call_str = "\n -> " in
let report_cxx_annotation_stack src_summary loc trace snk_pname call_loc = let report_cxx_annotation_stack {InterproceduralAnalysis.proc_desc; err_log} loc trace snk_pname
let src_pname = Summary.get_proc_name src_summary in call_loc =
let src_pname = Procdesc.get_proc_name proc_desc in
let final_trace = List.rev (update_trace call_loc trace) in let final_trace = List.rev (update_trace call_loc trace) in
let snk_pname_str = cxx_string_of_pname snk_pname in let snk_pname_str = cxx_string_of_pname snk_pname in
let src_pname_str = cxx_string_of_pname src_pname in let src_pname_str = cxx_string_of_pname src_pname in
@ -332,19 +333,20 @@ module CxxAnnotationSpecs = struct
let linters_def_file = Option.value_map ~default:"" ~f:Fn.id Config.inferconfig_file in let linters_def_file = Option.value_map ~default:"" ~f:Fn.id Config.inferconfig_file in
IssueType.register_from_string spec_name ~doc_url ~linters_def_file IssueType.register_from_string spec_name ~doc_url ~linters_def_file
in in
SummaryReporting.log_error src_summary ~loc ~ltr:final_trace issue_type description let attrs = Procdesc.get_attributes proc_desc in
Reporting.log_error attrs err_log ~loc ~ltr:final_trace issue_type description
in in
let snk_annot = annotation_of_str snk_name in let snk_annot = annotation_of_str snk_name in
let report proc_data annot_map = let report ({InterproceduralAnalysis.proc_desc} as analysis_data) annot_map =
let proc_desc = Summary.get_proc_desc proc_data.Callbacks.summary in
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
if src_pred proc_name then if src_pred proc_name then
let loc = Procdesc.get_loc proc_desc in let loc = Procdesc.get_loc proc_desc in
try try
let sink_map = Domain.find snk_annot annot_map in let sink_map = Domain.find snk_annot annot_map in
report_call_stack proc_data.Callbacks.summary snk_pred report_call_stack snk_pred
(lookup_annotation_calls ~caller_summary:proc_data.Callbacks.summary snk_annot) (lookup_annotation_calls analysis_data snk_annot)
report_cxx_annotation_stack (CallSite.make proc_name loc) sink_map (report_cxx_annotation_stack analysis_data)
(CallSite.make proc_name loc) sink_map
with Caml.Not_found -> () with Caml.Not_found -> ()
in in
{ AnnotationSpec.description= Printf.sprintf "CxxAnnotationSpecs %s from config" spec_name { AnnotationSpec.description= Printf.sprintf "CxxAnnotationSpecs %s from config" spec_name
@ -399,10 +401,9 @@ module ExpensiveAnnotationSpec = struct
let method_is_expensive tenv pname = is_modeled_expensive tenv pname || is_expensive tenv pname let method_is_expensive tenv pname = is_modeled_expensive tenv pname || is_expensive tenv pname
let check_expensive_subtyping_rules {Callbacks.exe_env; summary} overridden_pname = let check_expensive_subtyping_rules {InterproceduralAnalysis.proc_desc; tenv; err_log}
let proc_desc = Summary.get_proc_desc summary in overridden_pname =
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env proc_name in
let loc = Procdesc.get_loc proc_desc in let loc = Procdesc.get_loc proc_desc in
if not (method_is_expensive tenv overridden_pname) then if not (method_is_expensive tenv overridden_pname) then
let description = let description =
@ -411,7 +412,8 @@ module ExpensiveAnnotationSpec = struct
(Procname.to_string overridden_pname) (Procname.to_string overridden_pname)
MF.pp_monospaced ("@" ^ Annotations.expensive) MF.pp_monospaced ("@" ^ Annotations.expensive)
in in
SummaryReporting.log_error summary ~loc IssueType.checkers_expensive_overrides_unexpensive let attrs = Procdesc.get_attributes proc_desc in
Reporting.log_error attrs err_log ~loc IssueType.checkers_expensive_overrides_unexpensive
description description
@ -426,13 +428,14 @@ module ExpensiveAnnotationSpec = struct
; sanitizer_predicate= default_sanitizer ; sanitizer_predicate= default_sanitizer
; sink_annotation= expensive_annot ; sink_annotation= expensive_annot
; report= ; report=
(fun ({Callbacks.exe_env; summary} as proc_data) astate -> (fun ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) astate ->
let proc_desc = Summary.get_proc_desc summary in
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env proc_name in
if is_expensive tenv proc_name then if is_expensive tenv proc_name then
PatternMatch.override_iter (check_expensive_subtyping_rules proc_data) tenv proc_name ; PatternMatch.override_iter
report_src_snk_paths proc_data astate [performance_critical_annot] expensive_annot ) } (check_expensive_subtyping_rules analysis_data)
tenv proc_name ;
report_src_snk_paths analysis_data astate [performance_critical_annot] expensive_annot )
}
end end
(* parse user-defined specs from .inferconfig *) (* parse user-defined specs from .inferconfig *)
@ -480,11 +483,12 @@ let get_annot_specs pname =
List.Assoc.find_exn ~equal:Language.equal annot_specs language List.Assoc.find_exn ~equal:Language.equal annot_specs language
module TransferFunctions (CFG : ProcCfg.S) = struct module MakeTransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG module CFG = CFG
module Domain = Domain module Domain = Domain
type analysis_data = AnnotationSpec.t list ProcData.t type analysis_data =
{specs: AnnotationSpec.t list; analysis_data: Domain.t InterproceduralAnalysis.t}
let is_sink tenv (spec : AnnotationSpec.t) ~caller_pname ~callee_pname = let is_sink tenv (spec : AnnotationSpec.t) ~caller_pname ~callee_pname =
spec.sink_predicate tenv callee_pname spec.sink_predicate tenv callee_pname
@ -501,11 +505,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
else astate ) else astate )
let merge_callee_map call_site summary ~caller_pname ~callee_pname tenv specs astate = let merge_callee_map {analysis_data= {proc_desc; tenv; analyze_dependency}; specs} call_site
match Payload.read ~caller_summary:summary ~callee_pname with ~callee_pname astate =
match analyze_dependency callee_pname with
| None -> | None ->
astate astate
| Some callee_call_map -> | Some (_, callee_call_map) ->
L.d_printf "Applying summary for `%a`@\n" Procname.pp callee_pname ; L.d_printf "Applying summary for `%a`@\n" Procname.pp callee_pname ;
let add_call_site annot sink calls astate = let add_call_site annot sink calls astate =
if Domain.CallSites.is_empty calls then astate if Domain.CallSites.is_empty calls then astate
@ -514,6 +519,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
that sink. Ideally we would check only the spec that was responsible for adding the that sink. Ideally we would check only the spec that was responsible for adding the
sink but it is not obvious how to link back from annot to specs. Instead see if one sink but it is not obvious how to link back from annot to specs. Instead see if one
of the specs thinks that this sink is indeed a sink. *) of the specs thinks that this sink is indeed a sink. *)
let caller_pname = Procdesc.get_proc_name proc_desc in
List.fold ~init:astate specs ~f:(fun astate (spec : AnnotationSpec.t) -> List.fold ~init:astate specs ~f:(fun astate (spec : AnnotationSpec.t) ->
if is_sink tenv spec ~caller_pname ~callee_pname:sink then ( if is_sink tenv spec ~caller_pname ~callee_pname:sink then (
L.d_printf "%s: Adding sink call from `%a`'s summary `%a -> %a`@\n" L.d_printf "%s: Adding sink call from `%a`'s summary `%a -> %a`@\n"
@ -527,12 +533,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
callee_call_map astate callee_call_map astate
let exec_instr astate {ProcData.summary; tenv; ProcData.extras} _ = function let exec_instr astate ({analysis_data= {proc_desc; tenv}; specs} as analysis_data) _ = function
| Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) ->
let caller_pname = Summary.get_proc_name summary in let caller_pname = Procdesc.get_proc_name proc_desc in
let call_site = CallSite.make callee_pname call_loc in let call_site = CallSite.make callee_pname call_loc in
check_call tenv ~callee_pname ~caller_pname call_site astate extras check_call tenv ~callee_pname ~caller_pname call_site astate specs
|> merge_callee_map call_site summary ~callee_pname ~caller_pname tenv extras |> merge_callee_map analysis_data call_site ~callee_pname
| _ -> | _ ->
astate astate
@ -540,17 +546,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pp_session_name _node fmt = F.pp_print_string fmt "annotation reachability" let pp_session_name _node fmt = F.pp_print_string fmt "annotation reachability"
end end
module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional)) module TransferFunctions = MakeTransferFunctions (ProcCfg.Exceptional)
module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions)
let checker ({Callbacks.exe_env; summary} as callback) : Summary.t = let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) : Domain.t option =
let proc_name = Summary.get_proc_name summary in let proc_name = Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env proc_name in
let initial = Domain.empty in let initial = Domain.empty in
let specs = get_annot_specs proc_name in let specs = get_annot_specs proc_name in
let proc_data = {ProcData.summary; tenv; extras= specs} in let proc_data = {TransferFunctions.analysis_data; specs} in
match Analyzer.compute_post proc_data ~initial (Summary.get_proc_desc summary) with let post = Analyzer.compute_post proc_data ~initial proc_desc in
| Some annot_map -> Option.iter post ~f:(fun annot_map ->
List.iter specs ~f:(fun spec -> spec.AnnotationSpec.report callback annot_map) ; List.iter specs ~f:(fun spec -> spec.AnnotationSpec.report analysis_data annot_map) ) ;
Payload.update_summary annot_map summary post
| None ->
summary

3
infer/src/checkers/annotationReachability.mli
Unescape View File

@ -7,4 +7,5 @@
open! IStd open! IStd
val checker : Callbacks.proc_callback_t val checker :
AnnotationReachabilityDomain.t InterproceduralAnalysis.t -> AnnotationReachabilityDomain.t option

Write Preview
Loading…
Cancel
Save