[biabd] rename models-related things to "biabduction-..."

Summary:
The models are only for biabduction so try to make that clearer in the
code and documentation.

Reviewed By: skcho

Differential Revision: D16603147

fbshipit-source-id: 4a2be53de

infer/man/man1/infer-full.txt

@@ -1133,6 +1133,10 @@ INTERNAL OPTIONS
        --biabduction-fallback-model-free-pattern-reset
            Cancel the effect of --biabduction-fallback-model-free-pattern.
 
+       --biabduction-models-mode
+           Activates: Mode for analyzing the biabduction models (Conversely:
+           --no-biabduction-models-mode)
+
        --bo-relational-domain-reset
            Cancel the effect of --bo-relational-domain.
 
@@ -1459,10 +1463,6 @@ INTERNAL OPTIONS
            Matcher or list of matchers for methods that should be considered
            expensive by the performance critical checker.
 
-       --models-mode
-           Activates: Mode for analyzing the models (Conversely:
-           --no-models-mode)
-
        --modified-lines path
            Specifies the file containing the modified lines when Infer is run
            Test Determinator mode with --test-determinator.

infer/models/Makefile

@@ -13,7 +13,7 @@ OBJC_MODELS_DIR = objc/src
 OBJCPP_MODELS_DIR = objcpp/src
 
 MODELS_INFER_OUT = infer-out
-MODELS_INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(MODELS_INFER_OUT) --models-mode
+MODELS_INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(MODELS_INFER_OUT) --biabduction-models-mode
 
 all:
 

infer/models/java/Makefile

@@ -30,7 +30,7 @@ $(INFER_REPORT): $(JAVA_DEPS_NO_MODELS) $(JAVA_SOURCES) $(MAKEFILE_LIST)
 	$(QUIET)$(MKDIR_P) $(MODELS_OUT)
 	$(QUIET)rm -f $(JAVA_MODELS_JAR)
 	$(QUIET)$(call silent_on_success,Building Java models,\
-	  $(INFER_BIN) --biabduction-only --results-dir $(INFER_RESULTS_DIR) --models-mode -- \
+	  $(INFER_BIN) --biabduction-only --results-dir $(INFER_RESULTS_DIR) --biabduction-models-mode -- \
 	  $(JAVAC) -bootclasspath $(ANDROID_JAR) -d $(MODELS_OUT) -classpath $(MODELS_CLASSPATH) \
 	    $(JAVA_SOURCES) -source 7 -target 7)
 

infer/src/IR/ProcAttributes.ml

@@ -45,11 +45,11 @@ type t =
   ; const_formals: int list  (** list of indices of formals that are const-qualified *)
   ; func_attributes: PredSymb.func_attribute list
   ; is_abstract: bool  (** the procedure is abstract *)
+  ; is_biabduction_model: bool  (** the procedure is a model for the biabduction analysis *)
   ; is_bridge_method: bool  (** the procedure is a bridge method *)
   ; is_defined: bool  (** true if the procedure is defined, and not just declared *)
   ; is_cpp_noexcept_method: bool  (** the procedure is an C++ method annotated with "noexcept" *)
   ; is_java_synchronized_method: bool  (** the procedure is a Java synchronized method *)
-  ; is_model: bool  (** the procedure is a model *)
   ; is_specialized: bool  (** the procedure is a clone specialized for dynamic dispatch handling *)
   ; is_synthetic_method: bool  (** the procedure is a synthetic method *)
   ; is_variadic: bool  (** the procedure is variadic, only supported for Clang procedures *)
@@ -71,11 +71,11 @@ let default translation_unit proc_name =
   ; const_formals= []
   ; func_attributes= []
   ; is_abstract= false
+  ; is_biabduction_model= false
   ; is_bridge_method= false
   ; is_cpp_noexcept_method= false
   ; is_java_synchronized_method= false
   ; is_defined= false
-  ; is_model= false
   ; is_specialized= false
   ; is_synthetic_method= false
   ; is_variadic= false
@@ -102,11 +102,11 @@ let pp f
      ; const_formals
      ; func_attributes
      ; is_abstract
+     ; is_biabduction_model
      ; is_bridge_method
      ; is_defined
      ; is_cpp_noexcept_method
      ; is_java_synchronized_method
-     ; is_model
      ; is_specialized
      ; is_synthetic_method
      ; is_variadic
@@ -151,7 +151,7 @@ let pp f
     is_cpp_noexcept_method f () ;
   pp_bool_default ~default:default.is_java_synchronized_method "is_java_synchronized_method"
     is_java_synchronized_method f () ;
-  pp_bool_default ~default:default.is_model "is_model" is_model f () ;
+  pp_bool_default ~default:default.is_biabduction_model "is_model" is_biabduction_model f () ;
   pp_bool_default ~default:default.is_specialized "is_specialized" is_specialized f () ;
   pp_bool_default ~default:default.is_synthetic_method "is_synthetic_method" is_synthetic_method f
     () ;

infer/src/IR/ProcAttributes.mli

@@ -28,11 +28,11 @@ type t =
   ; const_formals: int list  (** list of indices of formals that are const-qualified *)
   ; func_attributes: PredSymb.func_attribute list
   ; is_abstract: bool  (** the procedure is abstract *)
+  ; is_biabduction_model: bool  (** the procedure is a model for the biabduction analysis *)
   ; is_bridge_method: bool  (** the procedure is a bridge method *)
   ; is_defined: bool  (** true if the procedure is defined, and not just declared *)
   ; is_cpp_noexcept_method: bool  (** the procedure is an C++ method annotated with "noexcept" *)
   ; is_java_synchronized_method: bool  (** the procedure is a Java synchronized method *)
-  ; is_model: bool  (** the procedure is a model *)
   ; is_specialized: bool  (** the procedure is a clone specialized for dynamic dispatch handling *)
   ; is_synthetic_method: bool  (** the procedure is a synthetic method *)
   ; is_variadic: bool  (** the procedure is variadic, only supported for Clang procedures *)

infer/src/backend/InferPrint.ml

@@ -244,7 +244,8 @@ module JsonIssuePrinter = MakeJsonListPrinter (struct
         "Invalid source file for %a %a@.Trace: %a@." IssueType.pp err_key.err_name
         Localise.pp_error_desc err_key.err_desc Errlog.pp_loc_trace err_data.loc_trace ;
     let should_report_source_file =
-      (not (SourceFile.is_infer_model source_file)) || Config.debug_mode || Config.debug_exceptions
+      (not (SourceFile.is_biabduction_model source_file))
+      || Config.debug_mode || Config.debug_exceptions
     in
     if
       error_filter source_file err_key.err_name

infer/src/backend/Summary.ml

@@ -164,7 +164,7 @@ module OnDisk = struct
 
   (** paths to the .specs file for the given procedure in the models folder *)
   let specs_models_filename pname =
-    DB.filename_from_string (Filename.concat Config.models_dir (specs_filename pname))
+    DB.filename_from_string (Filename.concat Config.biabduction_models_dir (specs_filename pname))
 
 
   let has_model pname =

infer/src/base/Config.ml

@@ -408,11 +408,11 @@ let lib_dir = bin_dir ^/ Filename.parent_dir_name ^/ "lib"
 let etc_dir = bin_dir ^/ Filename.parent_dir_name ^/ "etc"
 
 (** Path to lib/specs to retrieve the default models *)
-let models_dir = lib_dir ^/ specs_dir_name
+let biabduction_models_dir = lib_dir ^/ specs_dir_name
 
-let models_jar = lib_dir ^/ "java" ^/ "models.jar"
+let biabduction_models_jar = lib_dir ^/ "java" ^/ "models.jar"
 
-let models_src_dir =
+let biabduction_models_src_dir =
   let root = Unix.getcwd () in
   let dir = bin_dir ^/ Filename.parent_dir_name ^/ "models" in
   Utils.filename_to_absolute ~root dir
@@ -1099,7 +1099,8 @@ and custom_symbols =
     "Specify named lists of symbols available to rules"
 
 
-and ( bo_debug
+and ( biabduction_models_mode
+    , bo_debug
     , developer_mode
     , debug
     , debug_exceptions
@@ -1112,7 +1113,6 @@ and ( bo_debug
     , frontend_tests
     , keep_going
     , linters_developer_mode
-    , models_mode
     , only_cheap_debug
     , print_buckets
     , print_logs
@@ -1126,7 +1126,10 @@ and ( bo_debug
     List.filter_map InferCommand.all_commands ~f:(fun cmd ->
         if InferCommand.equal Explore cmd then None else Some (cmd, manual_generic) )
   in
-  let bo_debug =
+  let biabduction_models_mode =
+    CLOpt.mk_bool_group ~long:"biabduction-models-mode" "Mode for analyzing the biabduction models"
+      [] []
+  and bo_debug =
     CLOpt.mk_int ~default:0 ~long:"bo-debug"
       ~in_help:InferCommand.[(Analyze, manual_buffer_overrun)]
       "Debug level for buffer-overrun checker (0-4)"
@@ -1224,8 +1227,6 @@ and ( bo_debug
       "Save filename.ext.test.dot with the cfg in dotty format for frontend tests (also sets \
        $(b,--print-types))"
       [print_types] []
-  and models_mode =
-    CLOpt.mk_bool_group ~long:"models-mode" "Mode for analyzing the models" [] [keep_going]
   and print_logs =
     CLOpt.mk_bool ~long:"print-logs"
       ~in_help:
@@ -1247,7 +1248,8 @@ and ( bo_debug
         debug )
       [debug; developer_mode] [default_linters; keep_going]
   in
-  ( bo_debug
+  ( biabduction_models_mode
+  , bo_debug
   , developer_mode
   , debug
   , debug_exceptions
@@ -1260,7 +1262,6 @@ and ( bo_debug
   , frontend_tests
   , keep_going
   , linters_developer_mode
-  , models_mode
   , only_cheap_debug
   , print_buckets
   , print_logs
@@ -2571,7 +2572,7 @@ let post_parsing_initialization command_opt =
   let symops_timeout, seconds_timeout =
     let default_symops_timeout = 1100 in
     let default_seconds_timeout = 10.0 in
-    if !models_mode then (* disable timeouts when analyzing models *)
+    if !biabduction_models_mode then (* disable timeouts when analyzing models *)
       (None, None)
     else (Some default_symops_timeout, Some default_seconds_timeout)
   in
@@ -2674,6 +2675,8 @@ and biabduction_model_alloc_pattern = Option.map ~f:Str.regexp !biabduction_mode
 
 and biabduction_model_free_pattern = Option.map ~f:Str.regexp !biabduction_model_free_pattern
 
+and biabduction_models_mode = !biabduction_models_mode
+
 and bootclasspath = !bootclasspath
 
 and bo_debug = !bo_debug
@@ -2945,8 +2948,6 @@ and merge = !merge
 
 and ml_buckets = !ml_buckets
 
-and models_mode = !models_mode
-
 and modified_lines = !modified_lines
 
 and monitor_prop_size = !monitor_prop_size

infer/src/base/Config.mli

@@ -53,9 +53,11 @@ val assign : string
 
 val backend_stats_dir_name : string
 
-val biabduction_model_alloc_pattern : Str.regexp option
+val biabduction_models_dir : string
 
-val biabduction_model_free_pattern : Str.regexp option
+val biabduction_models_jar : string
+
+val biabduction_models_src_dir : string
 
 val bin_dir : string
 
@@ -119,12 +121,6 @@ val max_widens : int
 
 val meet_level : int
 
-val models_dir : string
-
-val models_jar : string
-
-val models_src_dir : string
-
 val nsnotification_center_checker_backend : bool
 
 val os_type : os_type
@@ -235,6 +231,12 @@ val array_level : int
 
 val biabduction : bool
 
+val biabduction_model_alloc_pattern : Str.regexp option
+
+val biabduction_model_free_pattern : Str.regexp option
+
+val biabduction_models_mode : bool
+
 val bo_debug : int
 
 val bo_relational_domain : [`Bo_relational_domain_oct | `Bo_relational_domain_poly] option
@@ -488,8 +490,6 @@ val method_decls_info : string option
 val ml_buckets :
   [`MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown] list
 
-val models_mode : bool
-
 val modified_lines : string option
 
 val monitor_prop_size : bool

infer/src/base/SourceFile.ml

@@ -18,7 +18,7 @@ type t =
   | Invalid of {ml_source_file: string}
   | Absolute of string
   | RelativeProjectRoot of string  (** relative to project root *)
-  | RelativeInferModel of string  (** relative to infer models *)
+  | RelativeInferBiabductionModel of string  (** relative to infer models *)
 [@@deriving compare]
 
 let equal = [%compare.equal: t]
@@ -46,7 +46,7 @@ let from_abs_path ?(warn_on_error = true) fname =
   (* try to get realpath of source file. Use original if it fails *)
   let fname_real = try Utils.realpath ~warn_on_error fname with Unix.Unix_error _ -> fname in
   let project_root_real = Utils.realpath ~warn_on_error Config.project_root in
-  let models_dir_real = Config.models_src_dir in
+  let models_dir_real = Config.biabduction_models_src_dir in
   match
     Utils.filename_to_relative ~backtrack:Config.relative_path_backtrack ~root:project_root_real
       fname_real
@@ -58,7 +58,7 @@ let from_abs_path ?(warn_on_error = true) fname =
   | None -> (
     match Utils.filename_to_relative ~root:models_dir_real fname_real with
     | Some path ->
-        RelativeInferModel path
+        RelativeInferBiabductionModel path
     | None ->
         (* fname_real is absolute already *)
         Absolute fname_real )
@@ -70,7 +70,7 @@ let to_string =
     match fname with
     | Invalid {ml_source_file} ->
         "DUMMY from " ^ ml_source_file
-    | RelativeInferModel path ->
+    | RelativeInferBiabductionModel path ->
         "INFER_MODEL/" ^ path
     | RelativeProjectRoot path ->
         path
@@ -89,8 +89,8 @@ let to_abs_path fname =
         "cannot be called with Invalid source file originating in %s" ml_source_file
   | RelativeProjectRoot path ->
       Filename.concat Config.project_root path
-  | RelativeInferModel path ->
-      Filename.concat Config.models_src_dir path
+  | RelativeInferBiabductionModel path ->
+      Filename.concat Config.biabduction_models_src_dir path
   | Absolute path ->
       path
 
@@ -108,13 +108,13 @@ let invalid ml_source_file = Invalid {ml_source_file}
 
 let is_invalid = function Invalid _ -> true | _ -> false
 
-let is_infer_model source_file =
+let is_biabduction_model source_file =
   match source_file with
   | Invalid {ml_source_file} ->
       L.(die InternalError) "cannot be called with Invalid source file from %s" ml_source_file
   | RelativeProjectRoot _ | Absolute _ ->
       false
-  | RelativeInferModel _ ->
+  | RelativeInferBiabductionModel _ ->
       true
 
 
@@ -123,7 +123,7 @@ let is_under_project_root = function
       L.(die InternalError) "cannot be called with Invalid source file from %s" ml_source_file
   | RelativeProjectRoot _ ->
       true
-  | Absolute _ | RelativeInferModel _ ->
+  | Absolute _ | RelativeInferBiabductionModel _ ->
       false
 
 

infer/src/base/SourceFile.mli

@@ -41,7 +41,7 @@ val create : ?warn_on_error:bool -> string -> t
    WARNING: If warn_on_error is false, no warning will be shown whenever an error occurs for
    the given path (e.g. if it does not exist). *)
 
-val is_infer_model : t -> bool
+val is_biabduction_model : t -> bool
 
 val is_under_project_root : t -> bool
 (** Returns true if the file is in project root *)

infer/src/base/ZipLib.ml

@@ -45,8 +45,11 @@ let zip_libraries =
             line. *)
        List.rev_filter_map Config.specs_library ~f:load_zip
      in
-     if Config.biabduction && (not Config.models_mode) && Sys.file_exists Config.models_jar = `Yes
-     then mk_zip_lib Config.models_jar :: zip_libs
+     if
+       Config.biabduction
+       && (not Config.biabduction_models_mode)
+       && Sys.file_exists Config.biabduction_models_jar = `Yes
+     then mk_zip_lib Config.biabduction_models_jar :: zip_libs
      else zip_libs)
 
 

infer/src/biabduction/Tabulation.ml

@@ -836,7 +836,7 @@ let prop_set_exn tenv pname prop se_exn =
 let include_subtrace callee_pname =
   match Summary.OnDisk.proc_resolve_attributes callee_pname with
   | Some attrs ->
-      (not attrs.ProcAttributes.is_model)
+      (not attrs.ProcAttributes.is_biabduction_model)
       && SourceFile.is_under_project_root attrs.ProcAttributes.loc.Location.file
   | None ->
       false
@@ -1114,7 +1114,7 @@ let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hp
   in
   let callee_attributes = Summary.get_attributes callee_summary in
   (* if the callee is a model, then we don't have a tenv for it *)
-  if (not callee_attributes.ProcAttributes.is_model) && add_fields then
+  if (not callee_attributes.ProcAttributes.is_biabduction_model) && add_fields then
     let callee_tenv_opt =
       try Some (Exe_env.get_tenv exe_env callee_pname)
       with _ ->

infer/src/clang/cFrontend_decl.ml

@@ -41,7 +41,9 @@ let protect ~f ~recover ~pp_context (trans_unit_ctx : CFrontend_config.translati
 
 
 module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFrontend = struct
-  let model_exists procname = (not Config.models_mode) && Summary.OnDisk.has_model procname
+  let model_exists procname =
+    (not Config.biabduction_models_mode) && Summary.OnDisk.has_model procname
+
 
   (** Translates the method/function's body into nodes of the cfg. *)
   let add_method ?(is_destructor_wrapper = false) trans_unit_ctx tenv cfg class_decl_opt procname

infer/src/clang/cLocation.ml

@@ -65,7 +65,9 @@ let should_translate translation_unit (loc_start, loc_end) decl_trans_context ~t
   let file_in_project =
     map_file_of source_file_in_project loc_end || map_file_of source_file_in_project loc_start
   in
-  let translate_on_demand = translate_when_used || file_in_project || Config.models_mode in
+  let translate_on_demand =
+    translate_when_used || file_in_project || Config.biabduction_models_mode
+  in
   map_file_of equal_current_source loc_end
   || map_file_of equal_current_source loc_start
   || (Config.cxx && map_file_of equal_header_of_current_source loc_start)

infer/src/clang/cMethod_trans.ml

@@ -258,7 +258,7 @@ let create_local_procdesc ?(set_objc_accessor_attr = false) trans_unit_ctx cfg t
         ; func_attributes= attributes
         ; is_defined= defined
         ; is_cpp_noexcept_method= is_cpp_nothrow
-        ; is_model= Config.models_mode
+        ; is_biabduction_model= Config.biabduction_models_mode
         ; is_variadic= ms.CMethodSignature.is_variadic
         ; loc= loc_start
         ; clang_method_kind

infer/src/java/jMain.ml

@@ -60,7 +60,7 @@ let load_tenv () =
   match Tenv.load_global () with
   | None ->
       Tenv.create ()
-  | Some _ when Config.models_mode ->
+  | Some _ when Config.biabduction_models_mode ->
       L.(die InternalError)
         "Unexpected global tenv file found in '%s' while generating the models" Config.captured_dir
   | Some tenv ->
@@ -123,7 +123,9 @@ let do_all_files classpath sources classes =
 
 (* loads the source files and translates them *)
 let main load_sources_and_classes =
-  ( match (Config.models_mode, Sys.file_exists Config.models_jar = `Yes) with
+  ( match
+      (Config.biabduction_models_mode, Sys.file_exists Config.biabduction_models_jar = `Yes)
+    with
   | true, false ->
       ()
   | false, false ->
@@ -131,7 +133,7 @@ let main load_sources_and_classes =
   | true, true ->
       L.(die UserError) "Not expecting model file when analyzing the models"
   | false, true ->
-      JClasspath.add_models Config.models_jar ) ;
+      JClasspath.add_models Config.biabduction_models_jar ) ;
   JBasics.set_permissive true ;
   let classpath, sources, classes =
     match load_sources_and_classes with

infer/src/java/jTrans.ml

@@ -344,8 +344,8 @@ let create_am_procdesc source_file program icfg am proc_name : Procdesc.t =
       ; exceptions= List.map ~f:JBasics.cn_name am.Javalib.am_exceptions
       ; formals
       ; is_abstract= true
+      ; is_biabduction_model= Config.biabduction_models_mode
       ; is_bridge_method= am.Javalib.am_bridge
-      ; is_model= Config.models_mode
       ; is_synthetic_method= am.Javalib.am_synthetic
       ; method_annotation
       ; ret_type= JTransType.return_type program tenv ms
@@ -368,8 +368,8 @@ let create_native_procdesc source_file program icfg cm proc_name =
         ProcAttributes.access= trans_access cm.Javalib.cm_access
       ; exceptions= List.map ~f:JBasics.cn_name cm.Javalib.cm_exceptions
       ; formals
+      ; is_biabduction_model= Config.biabduction_models_mode
       ; is_bridge_method= cm.Javalib.cm_bridge
-      ; is_model= Config.models_mode
       ; is_synthetic_method= cm.Javalib.cm_synthetic
       ; method_annotation
       ; ret_type= JTransType.return_type program tenv ms
@@ -395,8 +395,8 @@ let create_empty_procdesc source_file program linereader icfg cm proc_name =
       ProcAttributes.access= trans_access cm.Javalib.cm_access
     ; exceptions= List.map ~f:JBasics.cn_name cm.Javalib.cm_exceptions
     ; formals
+    ; is_biabduction_model= Config.biabduction_models_mode
     ; is_bridge_method= cm.Javalib.cm_bridge
-    ; is_model= Config.models_mode
     ; is_synthetic_method= cm.Javalib.cm_synthetic
     ; is_java_synchronized_method= cm.Javalib.cm_synchronized
     ; loc= loc_start
@@ -432,9 +432,9 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name =
         ProcAttributes.access= trans_access cm.Javalib.cm_access
       ; exceptions= List.map ~f:JBasics.cn_name cm.Javalib.cm_exceptions
       ; formals
+      ; is_biabduction_model= Config.biabduction_models_mode
       ; is_bridge_method= cm.Javalib.cm_bridge
       ; is_defined= true
-      ; is_model= Config.models_mode
       ; is_synthetic_method= cm.Javalib.cm_synthetic
       ; is_java_synchronized_method= cm.Javalib.cm_synchronized
       ; loc= loc_start
@@ -706,7 +706,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
   let instrs =
     match call_args with
     (* modeling a class bypasses the treatment of Closeable *)
-    | _ when Config.models_mode || JClasspath.is_model callee_procname ->
+    | _ when Config.biabduction_models_mode || JClasspath.is_model callee_procname ->
         call_instrs
     | ((_, {Typ.desc= Typ.Tptr ({desc= Tstruct typename}, _)}) as exp) :: _
     (* add a file attribute when calling the constructor of a subtype of Closeable *)