From bf55514b8539b9ae5deb344a7c17db1abb373745 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Fri, 31 Mar 2017 21:00:58 -0700 Subject: [PATCH] [infer][checkers] Add a pretty print of the annotation reachability payload when printing summaries Summary: Useful for debugging. The pretty-print now looks like: > infer -g -a checkers -- javac Test.java > InferPrint infer-out/specs/Test.callsExpensive\(\)\:void.62c98ff4bca3529caf7daec79add8b47.specs Procedure: void Test.callsExpensive() void void Test.callsExpensive()(class Test* this) Analyzed Phase: FOOTPRINT ERRORS: WARNINGS: FAILURE:NONE SYMOPS:0 ThreadSafety: Threads: false Locks: false Accesses { } Return Attributes: { } AnnotationReachability: { _Expensive -> { void Test.expensive1() at [line 19], void Test.expensive2() at [line 21] }, _ForNonUiThread -> { }, _UiThread -> { }, ___infer_is_constructor -> { } } Reviewed By: jberdine Differential Revision: D4813995 fbshipit-source-id: 928d951 --- infer/src/IR/CallSite.ml | 2 ++ infer/src/IR/CallSite.mli | 2 ++ infer/src/backend/specs.ml | 29 ++++++++++--------- infer/src/backend/specs.mli | 4 +-- infer/src/checkers/AnnotReachabilityDomain.ml | 10 +++++++ infer/src/checkers/annotationReachability.ml | 29 +++++++++---------- 6 files changed, 43 insertions(+), 33 deletions(-) create mode 100644 infer/src/checkers/AnnotReachabilityDomain.ml diff --git a/infer/src/IR/CallSite.ml b/infer/src/IR/CallSite.ml index 9598b85a4..56f17b15c 100644 --- a/infer/src/IR/CallSite.ml +++ b/infer/src/IR/CallSite.ml @@ -40,3 +40,5 @@ module Set = PrettyPrintable.MakePPSet(struct let compare = compare let pp = pp end) + +module SetDomain = AbstractDomain.FiniteSet (Set) diff --git a/infer/src/IR/CallSite.mli b/infer/src/IR/CallSite.mli index 0bdb69eab..2b2513627 100644 --- a/infer/src/IR/CallSite.mli +++ b/infer/src/IR/CallSite.mli @@ -26,3 +26,5 @@ val dummy : t val pp : F.formatter -> t -> unit module Set : PrettyPrintable.PPSet with type elt = t + +module SetDomain : module type of AbstractDomain.FiniteSet (Set) diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 4b4b3fa27..3d13602bc 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -319,14 +319,12 @@ type phase = FOOTPRINT | RE_EXECUTION [@@deriving compare] let equal_phase = [%compare.equal : phase] -type call_summary = CallSite.Set.t Annot.Map.t - (** Payload: results of some analysis *) type payload = { preposts : NormSpec.t list option; (** list of specs *) typestate : unit TypeState.t option; (** final typestate *) - calls: call_summary option; + calls: AnnotReachabilityDomain.astate option; crashcontext_frame: Stacktree_t.stacktree option; (** Proc location and blame_range info for crashcontext analysis *) quandary : QuandarySummary.t option; @@ -444,18 +442,21 @@ let pp_summary_no_stats_specs fmt summary = F.fprintf fmt "%a@\n" pp_status summary.status; F.fprintf fmt "%a@\n" pp_pair (describe_phase summary) -let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } = - let pp_opt pp fmt = function - | Some x -> pp fmt x +let pp_payload pe fmt + { preposts; typestate; crashcontext_frame; + quandary; siof; threadsafety; buffer_overrun; calls } = + let pp_opt prefix pp fmt = function + | Some x -> F.fprintf fmt "%s: %a\n" prefix pp x | None -> () in - F.fprintf fmt "%a%a%a%a%a%a%a@\n" - (pp_specs pe) (get_specs_from_preposts preposts) - (pp_opt (TypeState.pp TypeState.unit_ext)) typestate - (pp_opt Crashcontext.pp_stacktree) crashcontext_frame - (pp_opt QuandarySummary.pp) quandary - (pp_opt SiofDomain.pp) siof - (pp_opt ThreadSafetyDomain.pp_summary) threadsafety - (pp_opt BufferOverrunDomain.Summary.pp) buffer_overrun + F.fprintf fmt "%a%a%a%a%a%a%a%a@\n" + (pp_opt "PrePosts" (pp_specs pe)) (Option.map ~f:NormSpec.tospecs preposts) + (pp_opt "TypeState" (TypeState.pp TypeState.unit_ext)) typestate + (pp_opt "CrashContext" Crashcontext.pp_stacktree) crashcontext_frame + (pp_opt "Quandary" QuandarySummary.pp) quandary + (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 let pp_summary_text fmt summary = diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 737cb9738..d2e723e99 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -129,14 +129,12 @@ type phase = FOOTPRINT | RE_EXECUTION val equal_phase : phase -> phase -> bool -type call_summary = CallSite.Set.t Annot.Map.t - (** Payload: results of some analysis *) type payload = { preposts : NormSpec.t list option; (** list of specs *) typestate : unit TypeState.t option; (** final typestate *) - calls: call_summary option; (** list of calls of the form (call, loc) *) + calls: 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/AnnotReachabilityDomain.ml b/infer/src/checkers/AnnotReachabilityDomain.ml new file mode 100644 index 000000000..3261a1069 --- /dev/null +++ b/infer/src/checkers/AnnotReachabilityDomain.ml @@ -0,0 +1,10 @@ +(* + * 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. + *) + +include AbstractDomain.Map (Annot.Map) (CallSite.SetDomain) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index a32ecd5b3..ed743d755 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -13,9 +13,6 @@ module F = Format module L = Logging module MF = MarkupFormatter -module CallSiteSet = AbstractDomain.FiniteSet (CallSite.Set) -module CallsDomain = AbstractDomain.Map (Annot.Map) (CallSiteSet) - let dummy_constructor_annot = "__infer_is_constructor" let annotation_of_str annot_str = @@ -46,21 +43,21 @@ let src_snk_pairs () = module Domain = struct module TrackingVar = AbstractDomain.FiniteSet (Var.Set) - module TrackingDomain = AbstractDomain.Pair (CallsDomain) (TrackingVar) + module TrackingDomain = AbstractDomain.Pair (AnnotReachabilityDomain) (TrackingVar) include TrackingDomain let add_call key call ((call_map, vars) as astate) = let call_set = - try CallsDomain.find key call_map - with Not_found -> CallSiteSet.empty in - let call_set' = CallSiteSet.add call call_set in + 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 (CallsDomain.add key call_set' call_map, vars) + 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 *) - (CallsDomain.empty, TrackingVar.empty) + (AnnotReachabilityDomain.empty, TrackingVar.empty) let add_tracking_var var (calls, previous_vars) = (calls, TrackingVar.add var previous_vars) @@ -73,7 +70,7 @@ module Domain = struct end module Summary = Summary.Make (struct - type payload = CallsDomain.astate + type payload = AnnotReachabilityDomain.astate let update_payload call_map (summary : Specs.summary) = { summary with payload = { summary.payload with calls = Some call_map }} @@ -146,7 +143,7 @@ let lookup_annotation_calls caller_pdesc annot pname : CallSite.t list = begin try Annot.Map.find annot call_map - |> CallSiteSet.elements + |> CallSite.SetDomain.elements with Not_found -> [] end @@ -276,8 +273,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_call_for_annot annot _ astate = let calls = try Annot.Map.find annot callee_call_map - with Not_found -> CallSiteSet.empty in - if (not (CallSiteSet.is_empty calls) || method_has_annot annot tenv callee_pname) && + 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 @@ -355,7 +352,7 @@ module Interprocedural = struct let extract_calls_with_annot annot call_map = try Annot.Map.find annot call_map - |> CallSiteSet.elements + |> CallSite.SetDomain.elements with Not_found -> [] in let report_src_snk_path (calls : CallSite.t list) (src_annot: Annot.t) = if method_overrides_annot src_annot tenv proc_name @@ -377,8 +374,8 @@ module Interprocedural = struct let init_map = List.fold ~f:(fun astate_acc (_, snk_annot) -> - CallsDomain.add snk_annot CallSiteSet.empty astate_acc) - ~init:CallsDomain.empty + AnnotReachabilityDomain.add snk_annot CallSite.SetDomain.empty astate_acc) + ~init:AnnotReachabilityDomain.empty (src_snk_pairs ()) in (init_map, Domain.TrackingVar.empty) in let compute_post proc_data =