[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

@@ -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 "<undefined>"
+  | ProcObjCAccessor ->
+      F.pp_print_string f "<ObjC accessor>"
+  | ProcDefined ->
+      F.pp_print_string f "<defined>"

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

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 ->
+      "<Default>"
+  | Public ->
+      "<Public>"
+  | Private ->
+      "<Private>"
+  | Protected ->
+      "<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

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 *)

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 -> "<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 "{@[<h>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)

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

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
 

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
 

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
 

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 "@[<h2>%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 () )

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

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])
 
 

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

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

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

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

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