diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 1e5cd3827..937d1a380 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1504,6 +1504,10 @@ INTERNAL OPTIONS Deactivates: Use the multirange subtyping domain (Conversely: --subtype-multirange) + --summary-stats + Activates: Print stats about summaries to standard output + (Conversely: --no-summary-stats) + --symops-per-iteration int Set the number of symbolic operations per iteration (see --iterations) diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 5ec68ae2a..b308211d5 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -682,6 +682,170 @@ module PreconditionStats = struct L.result "Procedures with data constraints: %d@." !nr_dataconstraints end +module SummaryStats = struct + module MetricTypes = struct + type 't typ = Bool : bool typ | Int : int typ + end + + module MakeTopN (V : PrettyPrintable.PrintableOrderedType) = struct + type 'k t = {capacity: int; filter: V.t -> bool; size: int; sorted_elements: (V.t * 'k) list} + + let make capacity ~filter = {capacity; filter; size= 0; sorted_elements= []} + + let add top k v = + if top.filter v then + let smaller, greater = + List.split_while top.sorted_elements ~f:(fun (v', _) -> V.compare v v' > 0) + in + if top.size >= top.capacity then + match smaller with + | [] -> + top + | _ :: tl -> + let sorted_elements = tl @ ((v, k) :: greater) in + {top with sorted_elements} + else + let sorted_elements = smaller @ ((v, k) :: greater) in + {top with size= top.size + 1; sorted_elements} + else top + + + let is_empty top = top.size <= 0 + + let pp ~pp_k f top = + if top.size > 0 then + let pp1 f (v, k) = F.fprintf f "@[%a -> %a@]" V.pp v pp_k k in + Pp.seq pp1 f (List.rev top.sorted_elements) + end + + module IntTopN = MakeTopN (Int) + + module MetricAggregator = struct + open MetricTypes + + type ('i, 'k) t = + | A : + { name: string + ; value: 'o + ; is_empty: 'o -> bool + ; add: 'o -> 'k -> 'i -> 'o + ; pp: pp_k:(F.formatter -> 'k -> unit) -> F.formatter -> 'o -> unit } + -> ('i, 'k) t + + let add (A aggr) k i = A {aggr with value= aggr.add aggr.value k i} + + let pp ~pp_k f (A {name; pp; value; is_empty}) = + if not (is_empty value) then F.fprintf f "@[%s: @[%a@]@]" name (pp ~pp_k) value + + + let no_k pp ~pp_k:_ = pp + + let int name add = A {name; value= 0; is_empty= Int.(( = ) 0); add; pp= no_k F.pp_print_int} + + let int_sum = int "sum" (fun acc _ v -> acc + v) + + let int_top3 = + A + { name= "top3" + ; value= IntTopN.make 3 ~filter:(fun x -> x > 1) + ; is_empty= IntTopN.is_empty + ; add= IntTopN.add + ; pp= IntTopN.pp } + + + let true_count = int "True" (fun acc _ b -> if b then acc + 1 else acc) + + let false_count = int "False" (fun acc _ b -> if b then acc else acc + 1) + + type 'k get = {get: 'i. 'i typ -> ('i, 'k) t list} + + let aggregators = + let get : type i. i typ -> (i, _) t list = function + | Bool -> + [true_count; false_count] + | Int -> + [int_sum; int_top3] + in + {get} + + + let get aggregators typ = aggregators.get typ + end + + module Metrics = struct + open MetricTypes + + type 'i metric = M : {get: 'i -> 't; typ: 't typ} -> 'i metric + + let for_fields poly_fields obj_metrics = + PolyFields.map poly_fields + { f= + (fun field_name field_get -> + let prefix = field_name ^ ":" in + List.map obj_metrics ~f:(fun (metric_name, M {typ; get= metric_get}) -> + let name = prefix ^ metric_name in + let get r = r |> field_get |> Obj.repr |> metric_get in + (name, M {typ; get}) ) ) } + |> List.concat + end + + module ObjMetrics = struct + open MetricTypes + open Metrics + + let obj_is_zero = phys_equal (Obj.repr 0) + + let obj_marshaled_size x = String.length (Marshal.to_string x []) - Marshal.header_size + + let metrics = + let bool name get = (name, M {typ= Bool; get}) in + let int name get = (name, M {typ= Int; get}) in + [ int "reachable_words" Obj.reachable_words + ; int "marshaled size" obj_marshaled_size + ; bool "is_zero" obj_is_zero ] + end + + module MetricResults = struct + open MetricTypes + open Metrics + module StringMap = PrettyPrintable.MakePPMap (String) + + type ('i, 'k) result = + | R : + { typ: 't typ + ; get: 'i -> 't + ; aggrs: ('t, 'k) MetricAggregator.t list } + -> ('i, 'k) result + + let init metrics aggregators = + List.fold metrics ~init:StringMap.empty ~f:(fun acc (name, M {typ; get}) -> + StringMap.add name (R {typ; get; aggrs= MetricAggregator.get aggregators typ}) acc ) + + + let add results k x = + StringMap.map + (fun (R res) -> + let v = res.get x in + R {res with aggrs= List.map res.aggrs ~f:(fun aggr -> MetricAggregator.add aggr k v)} ) + results + + + let pp ~pp_k f results = + let pp_value f (R {aggrs}) = Pp.seq (MetricAggregator.pp ~pp_k) f aggrs in + StringMap.pp ~pp_value f results + end + + let results = + let summary_fields_obj_metrics = Metrics.for_fields Summary.poly_fields ObjMetrics.metrics in + let init = MetricResults.init summary_fields_obj_metrics MetricAggregator.aggregators in + ref init + + + let do_summary proc_name summary = results := MetricResults.add !results proc_name summary + + let pp_stats () = L.result "%a@\n" (MetricResults.pp ~pp_k:Typ.Procname.pp) !results +end + let error_filter filters proc_name file error_name = (Config.write_html || not (IssueType.(equal skip_function) error_name)) && filters.Inferconfig.path_filter file @@ -920,6 +1084,7 @@ let process_summary filters formats_by_report_kind linereader stats summary issu issues_acc in if Config.precondition_stats then PreconditionStats.do_summary proc_name summary ; + if Config.summary_stats then SummaryStats.do_summary proc_name summary ; issues_acc' @@ -1054,6 +1219,7 @@ let pp_summary_and_issues formats_by_report_kind issue_formats = issue_formats ) !all_issues ; if Config.precondition_stats then PreconditionStats.pp_stats () ; + if Config.summary_stats then SummaryStats.pp_stats () ; List.iter [Config.lint_issues_dir_name; Config.starvation_issues_dir_name; Config.racerd_issues_dir_name] ~f:(fun dir_name -> diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index 97fda6321..44f6bda0b 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -27,6 +27,8 @@ type t = ; uninit: UninitDomain.Summary.t option } [@@deriving fields] +let poly_fields = PolyFields.make Fields.map_poly + type 'a pp = Pp.env -> F.formatter -> 'a -> unit type field = F : {field: (t, 'a option) Field.t; name: string; pp: 'a pp} -> field diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 9535e8ec9..ebb2cd9e7 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -7,29 +7,34 @@ open! IStd -(* ignore dead modules added by @@deriving fields *) -[@@@warning "-60"] +include + sig + (* ignore dead modules added by @@deriving fields *) + [@@@warning "-60"] -(** analysis results *) -type t = - { annot_map: AnnotReachabilityDomain.t option - ; biabduction: BiabductionSummary.t option - ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option - ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option - ; class_loads: ClassLoadsDomain.summary option - ; cost: CostDomain.summary option - ; lab_resource_leaks: ResourceLeakDomain.summary option - ; litho: LithoDomain.t option - ; pulse: PulseSummary.t option - ; purity: PurityDomain.summary option - ; quandary: QuandarySummary.t option - ; racerd: RacerDDomain.summary option - ; siof: SiofDomain.Summary.t option - ; starvation: StarvationDomain.summary option - ; typestate: TypeState.t option - ; uninit: UninitDomain.Summary.t option } -[@@deriving fields] + (** analysis results *) + type t = + { annot_map: AnnotReachabilityDomain.t option + ; biabduction: BiabductionSummary.t option + ; buffer_overrun_analysis: BufferOverrunAnalysisSummary.t option + ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option + ; class_loads: ClassLoadsDomain.summary option + ; cost: CostDomain.summary option + ; lab_resource_leaks: ResourceLeakDomain.summary option + ; litho: LithoDomain.t option + ; pulse: PulseSummary.t option + ; purity: PurityDomain.summary option + ; quandary: QuandarySummary.t option + ; racerd: RacerDDomain.summary option + ; siof: SiofDomain.Summary.t option + ; starvation: StarvationDomain.summary option + ; typestate: TypeState.t option + ; uninit: UninitDomain.Summary.t option } + [@@deriving fields] +end val pp : Pp.env -> Format.formatter -> t -> unit val empty : t + +val poly_fields : t PolyFields.t diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index 2a8d4daf3..b27737cb4 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -61,13 +61,23 @@ module Status = struct let is_analyzed = function Analyzed -> true | _ -> false end -type t = - { payloads: Payloads.t - ; sessions: int ref - ; stats: Stats.t - ; status: Status.t - ; proc_desc: Procdesc.t - ; err_log: Errlog.t } +include struct + (* ignore dead modules added by @@deriving fields *) + [@@@warning "-60"] + + type t = + { payloads: Payloads.t + ; sessions: int ref + ; stats: Stats.t + ; status: Status.t + ; proc_desc: Procdesc.t + ; err_log: Errlog.t } + [@@deriving fields] +end + +let poly_fields = + PolyFields.(make Fields.map_poly ~subfields:[S (Fields.payloads, Payloads.poly_fields)]) + let get_status summary = summary.status diff --git a/infer/src/backend/Summary.mli b/infer/src/backend/Summary.mli index a16e45346..dd7047076 100644 --- a/infer/src/backend/Summary.mli +++ b/infer/src/backend/Summary.mli @@ -48,6 +48,8 @@ type t = ; proc_desc: Procdesc.t ; err_log: Errlog.t } +val poly_fields : t PolyFields.t + val dummy : t (** dummy summary for testing *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index a61f6749a..cfd003617 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2164,6 +2164,10 @@ and subtype_multirange = "Use the multirange subtyping domain" +and summary_stats = + CLOpt.mk_bool ~long:"summary-stats" "Print stats about summaries to standard output" + + and symops_per_iteration = CLOpt.mk_int_opt ~deprecated:["symops_per_iteration"] ~long:"symops-per-iteration" ~meta:"int" "Set the number of symbolic operations per iteration (see $(b,--iterations))" @@ -3025,6 +3029,8 @@ and stats_report = !stats_report and subtype_multirange = !subtype_multirange +and summary_stats = !summary_stats + and custom_symbols = (* Convert symbol lists to regexps just once, here *) match !custom_symbols with diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index d699e0729..12b154e33 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -650,6 +650,8 @@ val stats_report : string option val subtype_multirange : bool +val summary_stats : bool + val symops_per_iteration : int option val test_determinator : bool diff --git a/infer/src/base/polyFields.ml b/infer/src/base/polyFields.ml new file mode 100644 index 000000000..5016c3321 --- /dev/null +++ b/infer/src/base/polyFields.ml @@ -0,0 +1,37 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd +module StringMap = Map.Make (String) + +type ('r, 'a) user = {f: 'f. string -> ('r -> 'f) -> 'a} [@@unboxed] + +type 'r elt = E : {name: string; get: 'r -> 'a} -> 'r elt + +type 'r t = 'r elt list + +type 'r sub = S : ('r, 'f) Field.t * 'f t -> 'r sub + +let make ?(subfields = []) (map_poly : _ Field.user -> _) = + let subfields = + List.fold subfields ~init:StringMap.empty ~f:(fun acc (S (field, elts)) -> + let name = Field.name field in + let prefix = name ^ "." in + let get = Field.get field in + let elts = + List.map elts ~f:(fun (E {name= subname; get= subget}) -> + E {name= prefix ^ subname; get= (fun r -> get r |> subget)} ) + in + StringMap.add_exn acc ~key:name ~data:elts ) + in + let f field = + let name = Field.name field in + StringMap.find subfields name |> Option.value ~default:[E {name; get= Field.get field}] + in + E {name= "ALL"; get= Fn.id} :: List.concat (map_poly {f}) + + +let map elts {f} = List.map elts ~f:(fun (E {name; get}) -> f name get) diff --git a/infer/src/base/polyFields.mli b/infer/src/base/polyFields.mli new file mode 100644 index 000000000..bea209afe --- /dev/null +++ b/infer/src/base/polyFields.mli @@ -0,0 +1,33 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** Datastructure for polymorphic getters of record fields *) +type 'r t + +type 'r sub = S : ('r, 'f) Field.t * 'f t -> 'r sub + +type ('r, 'a) user = {f: 'f. string -> ('r -> 'f) -> 'a} [@@unboxed] + +val make : ?subfields:'r sub list -> ((_, 'r, 'r t) Field.user -> 'r t list) -> 'r t +(** + Pass [Fields.map_poly] generated by [@@deriving fields] for the record ['r] you are interested + in to get the polymorphic getters of the fields of ['r]. + A dummy field "ALL" is added too. + + Subfields appearing in [subfields] will be added too. + Each subfield is specified by [S (field, poly_fields)] where [field] is the corresponding + [Field.t] value (generated by [@@deriving fields]) and [poly_fields] is the result of this + function for the field record type. +*) + +val map : 'r t -> ('r, 'a) user -> 'a list +(** + [map r f] maps each field of [r] with the function [f]. + [f] is called with two arguments: the name and the getter of the field. +*)