From 97ac7662f8f5c8d99a8d1041b75c6ad564ce414d Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 17 Apr 2018 04:37:20 -0700 Subject: [PATCH] [sqlite] options to output procedures db Summary: Add a `--procedures` option to `infer explore` to print information about the procedures captured by infer. More precisely, `infer explore --procedures` will print each row of the "procedures" table in the results database. A new `--procedures-filter` controls which procedures to print information about, and there is one flag per column in the db too to print more or less options about each procedure (in particular, we can now print attributes), with some defaults. Reviewed By: sblackshear Differential Revision: D7639062 fbshipit-source-id: 034a2b8 --- infer/src/IR/Attributes.ml | 29 ++++++++++-- infer/src/IR/Attributes.mli | 6 +++ infer/src/IR/PredSymb.ml | 13 ++++++ infer/src/IR/PredSymb.mli | 4 ++ infer/src/IR/ProcAttributes.ml | 78 ++++++++++++++++++++++++++++++++ infer/src/IR/ProcAttributes.mli | 2 + infer/src/IR/Typ.ml | 5 ++ infer/src/IR/Typ.mli | 2 + infer/src/backend/InferPrint.ml | 2 +- infer/src/backend/Procedures.ml | 68 ++++++++++++++++++++++++++++ infer/src/backend/Procedures.mli | 14 ++++++ infer/src/base/CommandDoc.ml | 9 +++- infer/src/base/Config.ml | 55 ++++++++++++++++++++++ infer/src/base/Config.mli | 12 +++++ infer/src/infer.ml | 7 +++ infer/src/istd/Pp.ml | 6 +++ infer/src/istd/Pp.mli | 8 ++++ 17 files changed, 313 insertions(+), 7 deletions(-) create mode 100644 infer/src/backend/Procedures.ml create mode 100644 infer/src/backend/Procedures.mli diff --git a/infer/src/IR/Attributes.ml b/infer/src/IR/Attributes.ml index 1c3769026..88775d11f 100644 --- a/infer/src/IR/Attributes.ml +++ b/infer/src/IR/Attributes.ml @@ -6,15 +6,27 @@ * 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. *) + open! IStd +module F = Format module L = Logging type attributes_kind = ProcUndefined | ProcObjCAccessor | ProcDefined [@@deriving compare] -let int64_of_attributes_kind = - (* only allocate this once *) - let int64_two = Int64.of_int 2 in - function ProcUndefined -> Int64.zero | ProcObjCAccessor -> Int64.one | ProcDefined -> int64_two +let equal_attributes_kind = [%compare.equal : attributes_kind] + +let attributes_kind_to_int64 = + [(ProcUndefined, Int64.zero); (ProcObjCAccessor, Int64.one); (ProcDefined, Int64.of_int 2)] + + +let int64_of_attributes_kind a = + List.Assoc.find_exn ~equal:equal_attributes_kind attributes_kind_to_int64 a + + +let deserialize_attributes_kind = + let int64_to_attributes_kind = List.Assoc.inverse attributes_kind_to_int64 in + function[@warning "-8"] + | Sqlite3.Data.INT n -> List.Assoc.find_exn ~equal:Int64.equal int64_to_attributes_kind n let proc_kind_of_attr (proc_attributes: ProcAttributes.t) = @@ -134,3 +146,12 @@ let find_file_capturing_procedure pname = `Source in (source_file, origin) ) + + +let pp_attributes_kind f = function + | ProcUndefined -> + F.pp_print_string f "" + | ProcObjCAccessor -> + F.pp_print_string f "" + | ProcDefined -> + F.pp_print_string f "" diff --git a/infer/src/IR/Attributes.mli b/infer/src/IR/Attributes.mli index 733f28c6b..ac61214d2 100644 --- a/infer/src/IR/Attributes.mli +++ b/infer/src/IR/Attributes.mli @@ -11,6 +11,10 @@ open! IStd +type attributes_kind + +val deserialize_attributes_kind : Sqlite3.Data.t -> attributes_kind + val store : ProcAttributes.t -> unit (** Save .attr file for the procedure into the attributes database. *) @@ -24,3 +28,5 @@ val find_file_capturing_procedure : Typ.Procname.t -> (SourceFile.t * [`Include (** Find the file where the procedure was captured, if a cfg for that file exists. Return also a boolean indicating whether the procedure is defined in an include file. *) + +val pp_attributes_kind : Format.formatter -> attributes_kind -> unit diff --git a/infer/src/IR/PredSymb.ml b/infer/src/IR/PredSymb.ml index 21cc891b5..fbae0af67 100644 --- a/infer/src/IR/PredSymb.ml +++ b/infer/src/IR/PredSymb.ml @@ -18,11 +18,24 @@ type func_attribute = | FA_sentinel of int * int (** __attribute__((sentinel(int, int))) *) [@@deriving compare] +let pp_func_attribute fmt = function FA_sentinel (i, j) -> F.fprintf fmt "sentinel(%d,%d)" i j + (** Visibility modifiers. *) type access = Default | Public | Private | Protected [@@deriving compare] let equal_access = [%compare.equal : access] +let string_of_access = function + | Default -> + "" + | Public -> + "" + | Private -> + "" + | Protected -> + "" + + (** Return the value of the FA_sentinel attribute in [attr_list] if it is found *) let get_sentinel_func_attribute_value attr_list = match attr_list with diff --git a/infer/src/IR/PredSymb.mli b/infer/src/IR/PredSymb.mli index 88f53e773..fe1b565f5 100644 --- a/infer/src/IR/PredSymb.mli +++ b/infer/src/IR/PredSymb.mli @@ -18,6 +18,8 @@ module F = Format type func_attribute = FA_sentinel of int * int [@@deriving compare] +val pp_func_attribute : F.formatter -> func_attribute -> unit + val get_sentinel_func_attribute_value : func_attribute list -> (int * int) option (** Return the value of the FA_sentinel attribute in [attr_list] if it is found *) @@ -26,6 +28,8 @@ type access = Default | Public | Private | Protected [@@deriving compare] val equal_access : access -> access -> bool +val string_of_access : access -> string + type mem_kind = | Mmalloc (** memory allocated with malloc *) | Mnew (** memory allocated with new *) diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index 4325a7c8d..f564b2f73 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -60,12 +60,32 @@ let kind_of_objc_accessor_type accessor = match accessor with Objc_getter _ -> "getter" | Objc_setter _ -> "setter" +let pp_objc_accessor_type fmt objc_accessor_type = + let fieldname, typ, annots = + match objc_accessor_type with Objc_getter field | Objc_setter field -> field + in + F.fprintf fmt "%s<%a:%a@,[%a]>" + (kind_of_objc_accessor_type objc_accessor_type) + Typ.Fieldname.pp fieldname (Typ.pp Pp.text) typ + (Pp.semicolon_seq (Pp.pair ~fst:Annot.pp ~snd:F.pp_print_bool)) + annots + + type var_attribute = Modify_in_block [@@deriving compare] +let string_of_var_attribute = function Modify_in_block -> "" + let var_attribute_equal = [%compare.equal : var_attribute] type var_data = {name: Mangled.t; typ: Typ.t; attributes: var_attribute list} [@@deriving compare] +let pp_var_data fmt {name; typ; attributes} = + F.fprintf fmt "{@[name=@ %a;@,typ=@ %a;@,attributes=@ %a@]}" Mangled.pp name (Typ.pp Pp.text) + typ + (Pp.semicolon_seq (Pp.to_string ~f:string_of_var_attribute)) + attributes + + type t = { access: PredSymb.access (** visibility access *) ; captured: (Mangled.t * Typ.t) list (** name and type of variables captured in blocks *) @@ -126,6 +146,64 @@ let default proc_name = ; source_file_captured= SourceFile.invalid __FILE__ } +let pp_parameters = Pp.semicolon_seq (Pp.pair ~fst:Mangled.pp ~snd:(Typ.pp Pp.text)) + +let pp fmt attributes = + let[@warning "+9"] { access + ; captured + ; did_preanalysis + ; err_log + ; exceptions + ; formals + ; const_formals + ; by_vals + ; func_attributes + ; is_abstract + ; is_bridge_method + ; is_defined + ; is_cpp_noexcept_method + ; is_java_synchronized_method + ; is_model + ; is_specialized + ; is_synthetic_method + ; clang_method_kind + ; loc + ; translation_unit + ; locals + ; method_annotation + ; objc_accessor + ; proc_flags + ; proc_name + ; ret_type + ; source_file_captured } = + attributes + in + Format.fprintf fmt + "{@[access= %a;@ captured= [@[%a@]];@ did_preanalysis= %b;@ err_log= [@[%a%a@]];@ exceptions= \ + [@[%a@]];@ formals= [@[%a@]];@ const_formals= [@[%a@]];@ by_vals= [@[%a@]];@ \ + func_attributes= [@[%a@]];@ is_abstract= %b;@ is_bridge_method= %b;@ is_defined= %b;@ \ + is_cpp_noexcept_method= %b;@ is_java_synchronized_method= %b;@ is_model= %b;@ \ + is_specialized= %b;@ is_synthetic_method= %b;@ clang_method_kind= %a;@ loc= %a;@ \ + translation_unit= %a;@ locals= [@[%a@]];@ method_annotation= %a;@ objc_accessor= %a;@ \ + proc_flags= [@[%a@]];@ proc_name= %a;@ ret_type= %a;@ source_file_captured=%a@]}" + (Pp.to_string ~f:PredSymb.string_of_access) + access pp_parameters captured did_preanalysis Errlog.pp_errors err_log Errlog.pp_warnings + err_log + (Pp.semicolon_seq F.pp_print_string) + exceptions pp_parameters formals (Pp.semicolon_seq F.pp_print_int) const_formals + (Pp.semicolon_seq F.pp_print_int) by_vals + (Pp.semicolon_seq PredSymb.pp_func_attribute) + func_attributes is_abstract is_bridge_method is_defined is_cpp_noexcept_method + is_java_synchronized_method is_model is_specialized is_synthetic_method + (Pp.to_string ~f:string_of_clang_method_kind) + clang_method_kind Location.pp loc (Pp.option SourceFile.pp) translation_unit + (Pp.semicolon_seq pp_var_data) locals (Annot.Method.pp "") method_annotation + (Pp.option pp_objc_accessor_type) objc_accessor + (Pp.hashtbl ~key:F.pp_print_string ~value:F.pp_print_string) + proc_flags Typ.Procname.pp proc_name (Typ.pp Pp.text) ret_type SourceFile.pp + source_file_captured + + module SQLite = SqliteUtils.MarshalledData (struct type nonrec t = t end) diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index 2f7a64f80..5f2211f2a 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -77,4 +77,6 @@ type t = val default : Typ.Procname.t -> t (** Create a proc_attributes with default values. *) +val pp : Format.formatter -> t -> unit + module SQLite : SqliteUtils.Data with type t = t diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 5002aadd5..125b73dd7 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -1160,6 +1160,11 @@ module Procname = struct Base.Hashtbl.find_or_add pname_to_key pname ~default + let deserialize : Sqlite3.Data.t -> t = function[@warning "-8"] + | Sqlite3.Data.BLOB b -> + Marshal.from_string b 0 + + let clear_cache () = Base.Hashtbl.clear pname_to_key end diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 0070f3964..ddbfeb2b7 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -464,6 +464,8 @@ module Procname : sig module SQLite : sig val serialize : t -> Sqlite3.Data.t + val deserialize : Sqlite3.Data.t -> t + val clear_cache : unit -> unit end diff --git a/infer/src/backend/InferPrint.ml b/infer/src/backend/InferPrint.ml index 5cec9f77b..bf962c895 100644 --- a/infer/src/backend/InferPrint.ml +++ b/infer/src/backend/InferPrint.ml @@ -593,7 +593,7 @@ module PreconditionStats = struct L.result "Procedures with data constraints: %d@." !nr_dataconstraints end -(* Wrapper of an issue that compares all parts except the procname *) +(** Wrapper of an issue that compares all parts except the procname *) module Issue = struct type err_data_ = Errlog.err_data diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml new file mode 100644 index 000000000..1c184d9ea --- /dev/null +++ b/infer/src/backend/Procedures.ml @@ -0,0 +1,68 @@ +(* + * Copyright (c) 2018 - 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. + *) +open! IStd +module F = Format +module L = Logging + +let select_all_procedures_like_statement = + ResultsDatabase.register_statement + "SELECT * FROM procedures WHERE proc_name LIKE :pname_like AND source_file LIKE \ + :source_file_like" + + +let pp_all ?filter ~proc_name ~attr_kind ~source_file ~proc_attributes fmt () = + let source_file_like, pname_like = + match filter with + | None -> + let wildcard = Sqlite3.Data.TEXT "%" in + (wildcard, wildcard) + | Some filter_string -> + match String.lsplit2 ~on:':' filter_string with + | Some (source_file_like, pname_like) -> + (Sqlite3.Data.TEXT source_file_like, Sqlite3.Data.TEXT pname_like) + | None -> + L.die UserError + "Invalid filter for procedures. Please see the documentation for --procedures-filter \ + in `infer explore --help`." + in + ResultsDatabase.with_registered_statement select_all_procedures_like_statement ~f:(fun db stmt -> + Sqlite3.bind stmt 1 (* :pname_like *) pname_like + |> SqliteUtils.check_sqlite_error db ~log:"procedures filter pname bind" ; + Sqlite3.bind stmt 2 (* :source_file_like *) source_file_like + |> SqliteUtils.check_sqlite_error db ~log:"procedures filter source file bind" ; + let pp_if ?(newline= false) condition deserialize pp fmt column = + if condition then ( + if newline then F.fprintf fmt "@\n " ; + F.fprintf fmt "%a@ " pp (Sqlite3.column stmt column |> deserialize) ) + in + let rec aux () = + match Sqlite3.step stmt with + | Sqlite3.Rc.ROW -> + let proc_name_hum = + (* same as proc_name for now, will change later *) + match[@warning "-8"] Sqlite3.column stmt 0 with Sqlite3.Data.TEXT s -> s + in + Format.fprintf fmt "@[

%s:@ %a%a%a%a@]@\n" proc_name_hum + (pp_if source_file SourceFile.SQLite.deserialize SourceFile.pp) + 2 + (pp_if proc_name Typ.Procname.SQLite.deserialize Typ.Procname.pp) + 0 + (pp_if attr_kind Attributes.deserialize_attributes_kind Attributes.pp_attributes_kind) + 1 + (pp_if ~newline:true proc_attributes ProcAttributes.SQLite.deserialize + ProcAttributes.pp) + 3 ; + aux () + | DONE -> + () + | err -> + L.die InternalError "procedures_iter: %s (%s)" (Sqlite3.Rc.to_string err) + (Sqlite3.errmsg db) + in + aux () ) diff --git a/infer/src/backend/Procedures.mli b/infer/src/backend/Procedures.mli new file mode 100644 index 000000000..40716657e --- /dev/null +++ b/infer/src/backend/Procedures.mli @@ -0,0 +1,14 @@ +(* + * Copyright (c) 2018 - 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. + *) + +open! IStd + +val pp_all : + ?filter:string -> proc_name:bool -> attr_kind:bool -> source_file:bool -> proc_attributes:bool + -> Format.formatter -> unit -> unit diff --git a/infer/src/base/CommandDoc.ml b/infer/src/base/CommandDoc.ml index a5fca4980..30cadb8b8 100644 --- a/infer/src/base/CommandDoc.ml +++ b/infer/src/base/CommandDoc.ml @@ -126,11 +126,16 @@ let diff = let explore = mk_command_doc ~title:"Infer Explore" ~short_description:"explore the error traces in infer reports" - ~synopsis:{|$(b,infer) $(b,explore) $(i,[options])|} + ~synopsis: + {|$(b,infer) $(b,explore) $(i,[options]) +$(b,infer) $(b,explore) $(b,--procedures) $(i,[options])|} ~description: [ `P "Show the list of bugs on the console and explore symbolic program traces emitted by \ - infer to explain a report. Can also generate an HTML report from a JSON report." ] + infer to explain a report. Can also generate an HTML report from a JSON report." + ; `P + "If $(b,--procedures) is passed, print information about each procedure captured by \ + infer." ] ~see_also:InferCommand.([Report; Run]) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 256cd38b4..190e97f4a 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1667,6 +1667,42 @@ and print_using_diff = "Highlight the difference w.r.t. the previous prop when printing symbolic execution debug info" +and procedures = + CLOpt.mk_bool ~long:"procedures" + ~in_help:InferCommand.([(Explore, manual_generic)]) + "Print functions and methods discovered by infer" + + +and procedures_attributes = + CLOpt.mk_bool ~long:"procedures-attributes" + ~in_help:InferCommand.([(Explore, manual_generic)]) + "Print the attributes of each procedure in the output of $(b,--procedures)" + + +and procedures_definedness = + CLOpt.mk_bool ~long:"procedures-definedness" ~default:true + ~in_help:InferCommand.([(Explore, manual_generic)]) + "Include procedures definedness in the output of $(b,--procedures), i.e. whether the \ + procedure definition was found, or only the procedure declaration, or the procedure is an \ + auto-generated Objective-C accessor" + + +and procedures_filter = + CLOpt.mk_string_opt ~long:"procedures-filter" ~meta:"filter" + ~in_help:InferCommand.([(Explore, manual_generic)]) + "With $(b,--procedures), only print functions and methods (procedures) matching the specified \ + $(i,filter). A procedure filter is of the form $(i,path_pattern:procedure_name). Patterns \ + are interpreted by SQLite: use $(b,_) to match any one character and $(b,%) to match any \ + sequence of characters. For instance, to keep only methods named \"foo\", one can use the \ + filter \"%:foo\"." + + +and procedures_name = + CLOpt.mk_bool ~long:"procedures-name" + ~in_help:InferCommand.([(Explore, manual_generic)]) + "Include procedures names in the output of $(b,--procedures)" + + and procedures_per_process = CLOpt.mk_int ~long:"procedures-per-process" ~default:1000 ~meta:"int" "Specify the number of procedures to analyze per process when using \ @@ -1674,6 +1710,13 @@ and procedures_per_process = groups of procedures." +and procedures_source_file = + CLOpt.mk_bool ~long:"procedures-source-file" ~default:true + ~in_help:InferCommand.([(Explore, manual_generic)]) + "Include the source file in which the procedure definition or declaration was found in the \ + output of $(b,--procedures)" + + and procs_csv = CLOpt.mk_path_opt ~deprecated:["procs"] ~long:"procs-csv" ~meta:"file" "Write statistics for each procedure in CSV format to a file" @@ -2607,8 +2650,20 @@ and print_types = !print_types and print_using_diff = !print_using_diff +and procedures = !procedures + +and procedures_attributes = !procedures_attributes + +and procedures_definedness = !procedures_definedness + +and procedures_filter = !procedures_filter + +and procedures_name = !procedures_name + and procedures_per_process = !procedures_per_process +and procedures_source_file = !procedures_source_file + and procs_csv = !procs_csv and project_root = !project_root diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 82b9b2520..4aeab399b 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -181,6 +181,18 @@ val pp_version : Format.formatter -> unit -> unit val proc_stats_filename : string +val procedures : bool + +val procedures_attributes : bool + +val procedures_definedness : bool + +val procedures_filter : string option + +val procedures_name : bool + +val procedures_source_file : bool + val property_attributes : string val report : bool diff --git a/infer/src/infer.ml b/infer/src/infer.ml index 1b0b61e81..9b6f366cf 100644 --- a/infer/src/infer.ml +++ b/infer/src/infer.ml @@ -145,6 +145,13 @@ let () = run (Lazy.force Driver.mode_from_command_line) | Diff -> Diff.diff (Lazy.force Driver.mode_from_command_line) + | Explore when Config.procedures -> + L.result "%a" + Config.( + Procedures.pp_all ?filter:procedures_filter ~proc_name:procedures_name + ~attr_kind:procedures_definedness ~source_file:procedures_source_file + ~proc_attributes:procedures_attributes) + () | Explore -> let if_some key opt args = match opt with None -> args | Some arg -> key :: string_of_int arg :: args diff --git a/infer/src/istd/Pp.ml b/infer/src/istd/Pp.ml index c35896887..c34bcb7a0 100644 --- a/infer/src/istd/Pp.ml +++ b/infer/src/istd/Pp.ml @@ -167,3 +167,9 @@ let cli_args fmt args = in pp_args fmt args ; pp_argfile_args String.Set.empty fmt args + + +let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b + +let hashtbl ~key ~value fmt h = + Caml.Hashtbl.iter (fun k v -> F.fprintf fmt "%a@ ->@ %a" key k value v) h diff --git a/infer/src/istd/Pp.mli b/infer/src/istd/Pp.mli index b7aa79101..3cf1fbf28 100644 --- a/infer/src/istd/Pp.mli +++ b/infer/src/istd/Pp.mli @@ -87,3 +87,11 @@ val current_time : F.formatter -> unit -> unit val elapsed_time : F.formatter -> unit -> unit (** Print the time in seconds elapsed since the beginning of the execution of the current command. *) + +val pair : + fst:(F.formatter -> 'a -> unit) -> snd:(F.formatter -> 'b -> unit) -> F.formatter -> 'a * 'b + -> unit + +val hashtbl : + key:(F.formatter -> 'a -> unit) -> value:(F.formatter -> 'b -> unit) -> F.formatter + -> ('a, 'b) Caml.Hashtbl.t -> unit