[infer][checkers] remove the `-a biabduction` option and the related code

Summary: This option was for compatibility with the command line options of the previous, but is no longer used. This diff removes the option and the deprecated code.

Reviewed By: sblackshear, mbouaziz

Differential Revision: D6351097

fbshipit-source-id: 0e4cfc5

DEFS

@@ -1,6 +1,6 @@
 import os
 
-analyzers = ['infer', 'checkers']
+analyzers = ['checkers']
 
 original_java_library = java_library
 def java_library(

infer/src/backend/InferAnalyze.ml

@@ -18,17 +18,6 @@ let analyze_exe_env_tasks cluster exe_env : Tasks.t =
   L.progressbar_file () ;
   Specs.clear_spec_tbl () ;
   Random.self_init () ;
-  let biabduction_only = Config.equal_analyzer Config.analyzer Config.BiAbduction in
-  if biabduction_only then
-    (* run the biabduction analysis only *)
-    Tasks.create
-      (Interproc.do_analysis_closures exe_env)
-      ~continuation:
-        ( if Config.write_html || Config.developer_mode then
-            Some (fun () -> if Config.write_html then Printer.write_all_html_files cluster)
-        else None )
-  else
-    (* run the registered checkers *)
   Tasks.create
     [ (fun () ->
         let call_graph = Exe_env.get_cg exe_env in
@@ -120,7 +109,7 @@ let register_active_checkers () =
   match Config.analyzer with
   | Checkers | Crashcontext ->
       RegisterCheckers.get_active_checkers () |> RegisterCheckers.register
-  | BiAbduction | CaptureOnly | CompileOnly | Linters ->
+  | CaptureOnly | CompileOnly | Linters ->
       ()
 
 

infer/src/backend/interproc.ml

@@ -1338,28 +1338,6 @@ let perform_transition proc_cfg tenv proc_name =
       ()
 
 
-(* Create closures for the interprocedural algorithm *)
-let interprocedural_algorithm_closures ~prepare_proc exe_env : Tasks.closure list =
-  let call_graph = Exe_env.get_cg exe_env in
-  let process_one_proc proc_name =
-    prepare_proc proc_name ;
-    let analyze proc_desc = ignore (Ondemand.analyze_proc_desc proc_desc proc_desc) in
-    match Exe_env.get_proc_desc exe_env proc_name with
-    | Some proc_desc
-      when Config.reactive_mode
-           (* in reactive mode, only analyze changed procedures *)
-           && (Procdesc.get_attributes proc_desc).ProcAttributes.changed ->
-        analyze proc_desc
-    | Some proc_desc ->
-        analyze proc_desc
-    | None ->
-        ()
-  in
-  let procs_to_analyze = Cg.get_defined_nodes call_graph in
-  let create_closure proc_name () = process_one_proc proc_name in
-  List.map ~f:create_closure procs_to_analyze
-
-
 let analyze_procedure_aux cg_opt tenv proc_desc =
   let proc_name = Procdesc.get_proc_name proc_desc in
   let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
@@ -1382,48 +1360,3 @@ let analyze_procedure {Callbacks.summary; proc_desc; tenv} : Specs.summary =
       reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ;
       Reporting.log_error_deprecated proc_name exn ) ;
   Specs.get_summary_unsafe __FILE__ proc_name
-
-
-(** Create closures to perform the analysis of an exe_env *)
-let do_analysis_closures exe_env : Tasks.closure list =
-  let get_calls caller_pdesc =
-    let calls = ref [] in
-    let f (callee_pname, loc) = calls := (callee_pname, loc) :: !calls in
-    Procdesc.iter_calls f caller_pdesc ;
-    List.rev !calls
-  in
-  let init_proc pname =
-    let pdesc =
-      match Exe_env.get_proc_desc exe_env pname with Some pdesc -> pdesc | None -> assert false
-    in
-    let nodes = List.map ~f:(fun n -> Procdesc.Node.get_id n) (Procdesc.get_nodes pdesc) in
-    let calls = get_calls pdesc in
-    ignore (Specs.init_summary (nodes, calls, pdesc))
-  in
-  let callbacks =
-    let get_proc_desc proc_name =
-      match Exe_env.get_proc_desc exe_env proc_name with
-      | Some pdesc ->
-          Some pdesc
-      | None ->
-          Option.map ~f:Specs.get_proc_desc (Specs.get_summary proc_name)
-    in
-    let analyze_ondemand _ proc_desc =
-      let proc_name = Procdesc.get_proc_name proc_desc in
-      let tenv = Exe_env.get_tenv exe_env proc_name in
-      let cg = Exe_env.get_cg exe_env in
-      analyze_procedure_aux (Some cg) tenv proc_desc
-    in
-    {Ondemand.analyze_ondemand; get_proc_desc}
-  in
-  let prepare_proc pn =
-    let should_init = Config.models_mode || is_none (Specs.get_summary pn) in
-    if should_init then init_proc pn
-  in
-  let closures =
-    List.map
-      ~f:(fun closure () ->
-        Ondemand.set_callbacks callbacks ; closure () ; Ondemand.unset_callbacks ())
-      (interprocedural_algorithm_closures ~prepare_proc exe_env)
-  in
-  closures

infer/src/backend/interproc.mli

@@ -14,6 +14,3 @@ open! IStd
 
 val analyze_procedure : Callbacks.proc_callback_t
 (** Run the biabduction analysis on the given procedure *)
-
-val do_analysis_closures : Exe_env.t -> Tasks.closure list
-(** Create closures to perform the analysis of an exe_env *)

infer/src/backend/specs.ml

@@ -21,7 +21,7 @@ module F = Format
 
 (** Module for joined props *)
 module Jprop = struct
-  (* type aliases for component of t values that compare should ignore *)
+  (** type aliases for component of t values that compare should ignore *)
   type id_ = int
 
   let compare_id_ _ _ = 0
@@ -320,9 +320,6 @@ module CallStats = struct
 *)
 end
 
-(** stats of the calls performed during the analysis *)
-type call_stats = CallStats.t
-
 (** Execution statistics *)
 type stats =
   { stats_failure: SymOp.failure_kind option
@@ -330,7 +327,7 @@ type stats =
   ; symops: int  (** Number of SymOp's throughout the whole analysis of the function *)
   ; mutable nodes_visited_fp: IntSet.t  (** Nodes visited during the footprint phase *)
   ; mutable nodes_visited_re: IntSet.t  (** Nodes visited during the re-execution phase *)
-  ; call_stats: call_stats }
+  ; call_stats: CallStats.t }
 
 type status = Pending | Analyzed [@@deriving compare]
 
@@ -568,12 +565,12 @@ let pp_summary_html source color fmt summary =
   F.fprintf fmt "</LISTING>@\n"
 
 
-let empty_stats calls =
+let empty_stats =
   { stats_failure= None
   ; symops= 0
   ; nodes_visited_fp= IntSet.empty
   ; nodes_visited_re= IntSet.empty
-  ; call_stats= CallStats.init calls }
+  ; call_stats= CallStats.init [] (* TODO(T23648322): remove the call_stats *) }
 
 
 let payload_compact sh payload =
@@ -757,13 +754,13 @@ let empty_payload =
 (** [init_summary (depend_list, nodes,
     proc_flags, calls, in_out_calls_opt, proc_attributes)]
     initializes the summary for [proc_name] given dependent procs in list [depend_list]. *)
-let init_summary (nodes, calls, proc_desc) =
+let init_summary proc_desc =
   let summary =
-    { nodes
+    { nodes= [] (* TODO(T23648322): remove this information from the summary *)
     ; phase= FOOTPRINT
     ; sessions= ref 0
     ; payload= empty_payload
-    ; stats= empty_stats calls
+    ; stats= empty_stats
     ; status= Pending
     ; proc_desc }
   in
@@ -774,10 +771,10 @@ let init_summary (nodes, calls, proc_desc) =
 let dummy =
   let dummy_attributes = ProcAttributes.default Typ.Procname.empty_block in
   let dummy_proc_desc = Procdesc.from_proc_attributes ~called_from_cfg:true dummy_attributes in
-  init_summary ([], [], dummy_proc_desc)
+  init_summary dummy_proc_desc
 
 
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
-let reset_summary proc_desc = init_summary ([], [], proc_desc)
+let reset_summary proc_desc = init_summary proc_desc
 
 (* =============== END of support for spec tables =============== *)

infer/src/backend/specs.mli

@@ -201,14 +201,6 @@ val get_summary_unsafe : string -> Typ.Procname.t -> summary
 val get_status : summary -> status
 (** Return the status (active v.s. inactive) of a procedure summary *)
 
-val init_summary :
-  Procdesc.Node.id list * (* nodes *)
-                          (Typ.Procname.t * Location.t) list * (* calls *)
-                                                               Procdesc.t
-  (* procdesc *) -> summary
-(** Initialize the summary for [proc_name] given dependent procs in list [depend_list].
-    This also stores the new summary in the spec table. *)
-
 val reset_summary : Procdesc.t -> summary
 (** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
 

infer/src/base/Config.ml

@@ -19,7 +19,6 @@ module CLOpt = CommandLineOption
 module L = Die
 
 type analyzer =
-  | BiAbduction
   | CaptureOnly
   | CompileOnly
   | Checkers
@@ -32,7 +31,6 @@ let equal_analyzer = [%compare.equal : analyzer]
 let string_to_analyzer =
   [ ("checkers", Checkers)
   ; ("infer", Checkers)
-  ; ("biabduction", BiAbduction)
   ; ("capture", CaptureOnly)
   ; ("compile", CompileOnly)
   ; ("crashcontext", Crashcontext)
@@ -659,10 +657,9 @@ and analysis_stops =
 
 and analyzer =
   let () =
-    match BiAbduction with
+    match Checkers with
     (* NOTE: if compilation fails here, it means you have added a new analyzer without updating the
        documentation of this option *)
-    | BiAbduction
     | CaptureOnly
     | CompileOnly
     | Checkers
@@ -2193,10 +2190,6 @@ let post_parsing_initialization command_opt =
       | _ ->
           () ) ;
   ( match !analyzer with
-  | Some BiAbduction ->
-      disable_all_checkers () ;
-      (* technically the biabduction checker doesn't run in this mode, but this gives an easy way to test if the biabduction *analysis* is active *)
-      biabduction := true
   | Some Crashcontext ->
       disable_all_checkers () ;
       crashcontext := true
@@ -2740,8 +2733,6 @@ let clang_frontend_action_string =
 let dynamic_dispatch =
   let default_mode =
     match analyzer with
-    | BiAbduction ->
-        Lazy
     | Checkers when biabduction ->
         Lazy
     | Checkers when quandary ->

infer/src/base/Config.mli

@@ -15,7 +15,6 @@ module CLOpt = CommandLineOption
     time by system calls, environment variables, or command line options *)
 
 type analyzer =
-  | BiAbduction
   | CaptureOnly
   | CompileOnly
   | Checkers

infer/src/integration/Buck.ml

@@ -41,7 +41,7 @@ module Target = struct
         add_flavor_internal target "compilation-database"
     | None, CompileOnly ->
         target
-    | None, (BiAbduction | CaptureOnly | Checkers | Linters) ->
+    | None, (CaptureOnly | Checkers | Linters) ->
         add_flavor_internal target "infer-capture-all"
     | None, Crashcontext ->
         L.(die UserError)
@@ -276,4 +276,3 @@ let filter_compatible subcommand args =
       List.filter args ~f:(fun arg -> not (String.equal blacklist arg))
   | _ ->
       args
-

infer/src/integration/Driver.ml

@@ -393,7 +393,7 @@ let analyze_and_report ?suppress_console_report ~changed_files mode =
         (false, true)
     | (Capture | Compile), _, _ | _, _, (CaptureOnly | CompileOnly) ->
         (false, false)
-    | _, _, (BiAbduction | Checkers | Crashcontext) ->
+    | _, _, (Checkers | Crashcontext) ->
         (true, true)
   in
   let should_merge =

infer/tests/build_systems/genrule/Makefile

@@ -10,10 +10,10 @@ ROOT_DIR = $(TESTS_DIR)/../..
 
 ANALYZER = checkers
 BUCK_TARGET = //infer/tests/build_systems/genrule/module2:module2
-INFER_TARGET = $(BUCK_TARGET)_infer
+INFER_TARGET = $(BUCK_TARGET)_checkers
 SOURCES = $(wildcard $(TESTS_DIR)/codetoanalyze/java/infer/*.java)
 OBJECTS = $(ROOT_DIR)/buck-out/genruletest/gen/infer/tests/build_systems/genrule/module2/lib__module2_compile__output/module2_compile.jar
-JSON_REPORT = $(ROOT_DIR)/buck-out/gen/infer/tests/build_systems/genrule/module2/module2_infer/infer_out/report.json
+JSON_REPORT = $(ROOT_DIR)/buck-out/gen/infer/tests/build_systems/genrule/module2/module2_checkers/checkers_out/report.json
 INFER_OPTIONS = --project-root $(ROOT_DIR)
 INFERPRINT_OPTIONS = --project-root $(ROOT_DIR) --issues-tests
 CLEAN_EXTRA = $(ROOT_DIR)/buck-out/genruletest