From 06b0b94626529fa32769a001414775e3855b1247 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 25 Apr 2017 23:07:07 -0700 Subject: [PATCH] [infer][java] simplify the domain logic of the annotation reachability checker Summary: The analysis logic was split between the treatment of the instructions and the definition of the domain, making the code more complicated that it should. This diff moves more of the logic into the domain definition and change to variable names to more descriptive ones Reviewed By: sblackshear Differential Revision: D4936414 fbshipit-source-id: ff59de7 --- infer/src/backend/specs.ml | 8 +- infer/src/backend/specs.mli | 2 +- infer/src/checkers/annotationReachability.ml | 152 ++++++++++--------- 3 files changed, 82 insertions(+), 80 deletions(-) diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 8c7782796..2688a122c 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -324,7 +324,7 @@ type payload = { preposts : NormSpec.t list option; (** list of specs *) typestate : unit TypeState.t option; (** final typestate *) - calls: AnnotReachabilityDomain.astate option; + annot_map : AnnotReachabilityDomain.astate option; crashcontext_frame: Stacktree_t.stacktree option; (** Proc location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; @@ -444,7 +444,7 @@ let pp_summary_no_stats_specs fmt summary = let pp_payload pe fmt { preposts; typestate; crashcontext_frame; - quandary; siof; threadsafety; buffer_overrun; calls } = + quandary; siof; threadsafety; buffer_overrun; annot_map } = let pp_opt prefix pp fmt = function | Some x -> F.fprintf fmt "%s: %a\n" prefix pp x | None -> () in @@ -456,7 +456,7 @@ let pp_payload pe fmt (pp_opt "Siof" SiofDomain.pp) siof (pp_opt "ThreadSafety" ThreadSafetyDomain.pp_summary) threadsafety (pp_opt "BufferOverrun" BufferOverrunDomain.Summary.pp) buffer_overrun - (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) calls + (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp) annot_map let pp_summary_text fmt summary = @@ -709,7 +709,7 @@ let empty_payload = { preposts = None; typestate = None; - calls = None; + annot_map = None; crashcontext_frame = None; quandary = None; siof = None; diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index d2e723e99..62ee22394 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -134,7 +134,7 @@ type payload = { preposts : NormSpec.t list option; (** list of specs *) typestate : unit TypeState.t option; (** final typestate *) - calls: AnnotReachabilityDomain.astate option; (** list of calls of the form (call, loc) *) + annot_map: AnnotReachabilityDomain.astate option; (** list of calls of the form (call, loc) *) crashcontext_frame: Stacktree_j.stacktree option; (** Procedure location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 89f18cd3b..3e8b23f31 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -18,7 +18,7 @@ let dummy_constructor_annot = "__infer_is_constructor" let annotation_of_str annot_str = { Annot.class_name = annot_str; parameters = []; } -let src_snk_pairs () = +let src_snk_pairs = (* parse user-defined specs from .inferconfig *) let parse_user_defined_specs = function | `List user_specs -> @@ -43,40 +43,52 @@ let src_snk_pairs () = module Domain = struct module TrackingVar = AbstractDomain.FiniteSet (Var.Set) - module TrackingDomain = AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingVar) - include TrackingDomain - - let add_call key call ((call_map, vars) as astate) = - let call_set = - try AnnotReachabilityDomain.find key call_map - with Not_found -> CallSite.SetDomain.empty in - let call_set' = CallSite.SetDomain.add call call_set in - if phys_equal call_set' call_set - then astate - else (AnnotReachabilityDomain.add key call_set' call_map, vars) - - let stop_tracking (_ : astate) = - (* The empty call map here prevents any subsequent calls to be added *) - (AnnotReachabilityDomain.empty, TrackingVar.empty) - - let add_tracking_var var (calls, previous_vars) = - (calls, TrackingVar.add var previous_vars) - - let remove_tracking_var var (calls, previous_vars) = - (calls, TrackingVar.remove var previous_vars) - - let is_tracked_var var (_, vars) = - TrackingVar.mem var vars + module TrackingDomain = AbstractDomain.BottomLifted (TrackingVar) + include AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingDomain) + + let add_call_site annot call_site ((annot_map, previous_vstate) as astate) = + match previous_vstate with + | TrackingDomain.Bottom -> astate + | TrackingDomain.NonBottom _ -> + let call_set = + try AnnotReachabilityDomain.find annot annot_map + with Not_found -> CallSite.SetDomain.empty in + let call_set' = CallSite.SetDomain.add call_site call_set in + if phys_equal call_set' call_set + then astate + else (AnnotReachabilityDomain.add annot call_set' annot_map, previous_vstate) + + let stop_tracking (annot_map, _ : astate) = + (annot_map, TrackingDomain.Bottom) + + let add_tracking_var var ((annot_map, previous_vstate) as astate) = + match previous_vstate with + | TrackingDomain.Bottom -> astate + | TrackingDomain.NonBottom vars -> + (annot_map, TrackingDomain.NonBottom (TrackingVar.add var vars)) + + let remove_tracking_var var ((annot_map, previous_vstate) as astate) = + match previous_vstate with + | TrackingDomain.Bottom -> astate + | TrackingDomain.NonBottom vars -> + (annot_map, TrackingDomain.NonBottom (TrackingVar.remove var vars)) + + let is_tracked_var var (_, vstate) = + match vstate with + | TrackingDomain.Bottom -> false + | TrackingDomain.NonBottom vars -> + TrackingVar.mem var vars + end module Summary = Summary.Make (struct type payload = AnnotReachabilityDomain.astate - let update_payload call_map (summary : Specs.summary) = - { summary with payload = { summary.payload with calls = Some call_map }} + let update_payload annot_map (summary : Specs.summary) = + { summary with payload = { summary.payload with annot_map = Some annot_map }} let read_payload (summary : Specs.summary) = - summary.payload.calls + summary.payload.annot_map end) (* Warning name when a performance critical method directly or indirectly @@ -139,10 +151,10 @@ let method_overrides_annot annot tenv pname = let lookup_annotation_calls caller_pdesc annot pname : CallSite.SetDomain.t = match Ondemand.analyze_proc_name ~propagate_exceptions:false caller_pdesc pname with - | Some { Specs.payload = { Specs.calls = Some call_map; }; } -> + | Some { Specs.payload = { Specs.annot_map = Some annot_map; }; } -> begin try - Annot.Map.find annot call_map + Annot.Map.find annot annot_map with Not_found -> CallSite.SetDomain.empty end @@ -210,7 +222,7 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site ca let callee_pname_str = string_of_pname callee_pname in let new_stack_str = stack_str ^ callee_pname_str ^ " -> " in let new_trace = update_trace call_loc trace |> update_trace callee_def_loc in - let unseen_pnames, updated_visited = + let unseen_callees, visited_callees = CallSite.SetDomain.fold (fun call_site ((unseen, visited) as accu) -> let p = CallSite.pname call_site in @@ -219,7 +231,7 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site ca else ((p, loc) :: unseen, Typ.Procname.Set.add p visited)) next_calls ([], visited_pnames) in - List.iter ~f:(loop fst_call_loc updated_visited (new_trace, new_stack_str)) unseen_pnames in + List.iter ~f:(loop fst_call_loc visited_callees (new_trace, new_stack_str)) unseen_callees in CallSite.SetDomain.iter (fun fst_call_site -> let fst_callee_pname = CallSite.pname fst_call_site in @@ -267,21 +279,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then method_has_ignore_allocation_annot tenv pname else false - let merge_call_map - callee_call_map tenv callee_pname caller_pname call_site ((call_map, _) as astate) = - let add_call_for_annot annot _ astate = - let calls = - try Annot.Map.find annot callee_call_map - with Not_found -> CallSite.SetDomain.empty in - if (not (CallSite.SetDomain.is_empty calls) || method_has_annot annot tenv callee_pname) && - (not (method_is_sanitizer annot tenv caller_pname)) - then - Domain.add_call annot call_site astate - else - astate in - (* for each annotation type T in domain(astate), check if method calls - something annotated with T *) - Annot.Map.fold add_call_for_annot call_map astate + let check_call tenv callee_pname caller_pname call_site astate = + List.fold + ~init:astate + ~f:(fun astate (_, annot) -> + if method_has_annot annot tenv callee_pname && + not (method_is_sanitizer annot tenv caller_pname) + then Domain.add_call_site annot call_site astate + else astate) + src_snk_pairs + + let merge_callee_map call_site pdesc callee_pname astate = + match Summary.read_summary pdesc callee_pname with + | None -> astate + | Some callee_call_map -> + Annot.Map.fold + (fun annot calls astate -> + if CallSite.SetDomain.is_empty calls + then astate + else Domain.add_call_site annot call_site astate) + callee_call_map + astate let exec_instr astate { ProcData.pdesc; tenv; } _ = function | Sil.Call (Some (id, _), Const (Cfun callee_pname), _, _, _) @@ -290,14 +308,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> let caller_pname = Procdesc.get_proc_name pdesc in let call_site = CallSite.make callee_pname call_loc in - begin - (* Runs the analysis of callee_pname if not already analyzed *) - match Summary.read_summary pdesc callee_pname with - | Some call_map -> - merge_call_map call_map tenv callee_pname caller_pname call_site astate - | None -> - merge_call_map Annot.Map.empty tenv callee_pname caller_pname call_site astate - end + check_call tenv callee_pname caller_pname call_site astate + |> merge_callee_map call_site pdesc callee_pname | Sil.Load (id, exp, _, _) when is_tracking_exp astate exp -> Domain.add_tracking_var (Var.of_id id) astate @@ -329,7 +341,6 @@ module Interprocedural = struct let check_and_report ({ Callbacks.proc_desc; tenv; summary } as proc_data) : Specs.summary = let proc_name = Procdesc.get_proc_name proc_desc in let loc = Procdesc.get_loc proc_desc in - let expensive = is_expensive tenv proc_name in (* TODO: generalize so we can check subtyping on arbitrary annotations *) let check_expensive_subtyping_rules overridden_pname = if not (method_is_expensive tenv overridden_pname) then @@ -344,14 +355,10 @@ module Interprocedural = struct (expensive_overrides_unexpensive, Localise.verbatim_desc description) in Reporting.log_error_from_summary summary ~loc exn in - if expensive then + if is_expensive tenv proc_name then PatternMatch.override_iter check_expensive_subtyping_rules tenv proc_name; - let report_src_snk_paths call_map (src_annot_list, (snk_annot: Annot.t)) = - let extract_calls_with_annot annot call_map = - try - Annot.Map.find annot call_map - with Not_found -> CallSite.SetDomain.empty in + let report_src_snk_paths annot_map (src_annot_list, (snk_annot: Annot.t)) = let report_src_snk_path (calls : CallSite.SetDomain.t) (src_annot: Annot.t) = if method_overrides_annot src_annot tenv proc_name then @@ -364,18 +371,13 @@ module Interprocedural = struct f_report (CallSite.make proc_name loc) calls in - let calls = extract_calls_with_annot snk_annot call_map in - if not (CallSite.SetDomain.is_empty calls) - then List.iter ~f:(report_src_snk_path calls) src_annot_list in + try + let sink_map = Annot.Map.find snk_annot annot_map in + List.iter ~f:(report_src_snk_path sink_map) src_annot_list + with Not_found -> () in let initial = - let init_map = - List.fold - ~f:(fun astate_acc (_, snk_annot) -> - AnnotReachabilityDomain.add snk_annot CallSite.SetDomain.empty astate_acc) - ~init:AnnotReachabilityDomain.empty - (src_snk_pairs ()) in - (init_map, Domain.TrackingVar.empty) in + (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) in let compute_post proc_data = Option.map ~f:fst (Analyzer.compute_post ~initial proc_data) in let updated_summary : Specs.summary = @@ -384,9 +386,9 @@ module Interprocedural = struct ~make_extras:ProcData.make_empty_extras proc_data in begin - match updated_summary.payload.calls with - | Some call_map -> - List.iter ~f:(report_src_snk_paths call_map) (src_snk_pairs ()) + match updated_summary.payload.annot_map with + | Some annot_map -> + List.iter ~f:(report_src_snk_paths annot_map) src_snk_pairs | None -> () end;