Merge branch 'main' into main

Makefile.config

@@ -119,7 +119,7 @@ define copy_or_same_file
  $(COPY) "$(1)" "$(2)" || diff -q "$(1)" "$(2)"
 endef
 
-INTERACTIVE := $(shell [ -t 0 ] && echo 1)
+INTERACTIVE := $(shell [ -t 0 ] && ! [ x"$$TERM" = xdumb ] && echo 1)
 SILENT := $(findstring s,$(filter-out -%,$(firstword $(MAKEFLAGS))))
 
 ifeq (1,$(INTERACTIVE))

infer/documentation/issues/PULSE_UNNECESSARY_COPY_OPTIONAL.md

@@ -0,0 +1,15 @@
+This is reported when Infer detects an unnecessary copy of an object via `optional` value
+construction where the source is not modified before it goes out of scope. To avoid the copy, we
+can move the source object or change the callee's type.
+
+For example,
+
+```cpp
+void get_optional_value(std::optional<A> x) {}
+
+void pass_non_optional_value(A x) {
+ get_optional_value(x);
+ // fix is to move as follows
+ // get_optional_value(std::move(x));
+}
+```

infer/man/man1/infer-capture.txt

@@ -202,9 +202,17 @@ BUCK OPTIONS
  Skip capture of buck targets matched by the specified regular
  expression.
 
+ --buck2-bxl-target string
+ Buck2 BXL script (as a buck target) to run when capturing with
+ buck2/clang integration.
+
  --buck2-root dir
  Specify the parent directory of buck-out (used only for buck2).
 
+ --buck2-use-bxl
+ Activates: Use BXL script when capturing with buck2. (Conversely:
+ --no-buck2-use-bxl)
+
  --Xbuck +string
  Pass values as command-line arguments to invocations of `buck
  build`. Only valid for --buck-clang.

infer/man/man1/infer-full.txt

@@ -223,10 +223,18 @@ OPTIONS
  Skip capture of buck targets matched by the specified regular
  expression. See also infer-capture(1) and infer-run(1).
 
+ --buck2-bxl-target string
+ Buck2 BXL script (as a buck target) to run when capturing with
+ buck2/clang integration. See also infer-capture(1).
+
  --buck2-root dir
  Specify the parent directory of buck-out (used only for buck2). 
  See also infer-capture(1) and infer-run(1).
 
+ --buck2-use-bxl
+ Activates: Use BXL script when capturing with buck2. (Conversely:
+ --no-buck2-use-bxl) See also infer-capture(1).
+
  --bufferoverrun
  Activates: checker bufferoverrun: InferBO is a detector for
  out-of-bounds array accesses. (Conversely: --no-bufferoverrun) 
@@ -615,19 +623,20 @@ OPTIONS
  PRECONDITION_NOT_MET (enabled by default),
  PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
  PULSE_CONST_REFABLE (disabled by default),
- PULSE_READONLY_SHARED_PTR_PARAM (disabled by default),
+ PULSE_READONLY_SHARED_PTR_PARAM (enabled by default),
  PULSE_RESOURCE_LEAK (enabled by default),
  PULSE_UNINITIALIZED_VALUE (enabled by default),
  PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default),
- PULSE_UNNECESSARY_COPY (disabled by default),
- PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default),
+ PULSE_UNNECESSARY_COPY (enabled by default),
+ PULSE_UNNECESSARY_COPY_ASSIGNMENT (enabled by default),
  PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST (disabled by default),
- PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by
- default),
+ PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (enabled by default),
  PULSE_UNNECESSARY_COPY_INTERMEDIATE (disabled by default),
  PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by
  default),
- PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default),
+ PULSE_UNNECESSARY_COPY_MOVABLE (enabled by default),
+ PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default),
+ PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default),
  PULSE_UNNECESSARY_COPY_RETURN (disabled by default),
  PURE_FUNCTION (enabled by default),
  QUANDARY_TAINT_ERROR (enabled by default),
@@ -1918,6 +1927,9 @@ INTERNAL OPTIONS
  --buck-targets-block-list-reset
  Set --buck-targets-block-list to the empty list.
 
+ --buck2-bxl-target-reset
+ Cancel the effect of --buck2-bxl-target.
+
  --buck2-root-reset
  Cancel the effect of --buck2-root.
 

infer/man/man1/infer-report.txt

@@ -265,19 +265,20 @@ OPTIONS
  PRECONDITION_NOT_MET (enabled by default),
  PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
  PULSE_CONST_REFABLE (disabled by default),
- PULSE_READONLY_SHARED_PTR_PARAM (disabled by default),
+ PULSE_READONLY_SHARED_PTR_PARAM (enabled by default),
  PULSE_RESOURCE_LEAK (enabled by default),
  PULSE_UNINITIALIZED_VALUE (enabled by default),
  PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default),
- PULSE_UNNECESSARY_COPY (disabled by default),
- PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default),
+ PULSE_UNNECESSARY_COPY (enabled by default),
+ PULSE_UNNECESSARY_COPY_ASSIGNMENT (enabled by default),
  PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST (disabled by default),
- PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by
- default),
+ PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (enabled by default),
  PULSE_UNNECESSARY_COPY_INTERMEDIATE (disabled by default),
  PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by
  default),
- PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default),
+ PULSE_UNNECESSARY_COPY_MOVABLE (enabled by default),
+ PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default),
+ PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default),
  PULSE_UNNECESSARY_COPY_RETURN (disabled by default),
  PURE_FUNCTION (enabled by default),
  QUANDARY_TAINT_ERROR (enabled by default),

infer/man/man1/infer.txt

@@ -223,10 +223,18 @@ OPTIONS
  Skip capture of buck targets matched by the specified regular
  expression. See also infer-capture(1) and infer-run(1).
 
+ --buck2-bxl-target string
+ Buck2 BXL script (as a buck target) to run when capturing with
+ buck2/clang integration. See also infer-capture(1).
+
  --buck2-root dir
  Specify the parent directory of buck-out (used only for buck2). 
  See also infer-capture(1) and infer-run(1).
 
+ --buck2-use-bxl
+ Activates: Use BXL script when capturing with buck2. (Conversely:
+ --no-buck2-use-bxl) See also infer-capture(1).
+
  --bufferoverrun
  Activates: checker bufferoverrun: InferBO is a detector for
  out-of-bounds array accesses. (Conversely: --no-bufferoverrun) 
@@ -615,19 +623,20 @@ OPTIONS
  PRECONDITION_NOT_MET (enabled by default),
  PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
  PULSE_CONST_REFABLE (disabled by default),
- PULSE_READONLY_SHARED_PTR_PARAM (disabled by default),
+ PULSE_READONLY_SHARED_PTR_PARAM (enabled by default),
  PULSE_RESOURCE_LEAK (enabled by default),
  PULSE_UNINITIALIZED_VALUE (enabled by default),
  PULSE_UNINITIALIZED_VALUE_LATENT (disabled by default),
- PULSE_UNNECESSARY_COPY (disabled by default),
- PULSE_UNNECESSARY_COPY_ASSIGNMENT (disabled by default),
+ PULSE_UNNECESSARY_COPY (enabled by default),
+ PULSE_UNNECESSARY_COPY_ASSIGNMENT (enabled by default),
  PULSE_UNNECESSARY_COPY_ASSIGNMENT_CONST (disabled by default),
- PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (disabled by
- default),
+ PULSE_UNNECESSARY_COPY_ASSIGNMENT_MOVABLE (enabled by default),
  PULSE_UNNECESSARY_COPY_INTERMEDIATE (disabled by default),
  PULSE_UNNECESSARY_COPY_INTERMEDIATE_CONST (disabled by
  default),
- PULSE_UNNECESSARY_COPY_MOVABLE (disabled by default),
+ PULSE_UNNECESSARY_COPY_MOVABLE (enabled by default),
+ PULSE_UNNECESSARY_COPY_OPTIONAL (disabled by default),
+ PULSE_UNNECESSARY_COPY_OPTIONAL_CONST (disabled by default),
  PULSE_UNNECESSARY_COPY_RETURN (disabled by default),
  PURE_FUNCTION (enabled by default),
  QUANDARY_TAINT_ERROR (enabled by default),

infer/models/Makefile

@@ -13,6 +13,8 @@ OBJC_MODELS_DIR = objc/src
 
 RESULTS_DIR = infer-out
 RESULTS_DB = $(RESULTS_DIR)/results.db
+CAPTURE_DB = $(RESULTS_DIR)/capture.db
+
 INFER_OPTIONS = --jobs 1 --biabduction-only --results-dir $(RESULTS_DIR) --biabduction-models-mode
 
 JAVA_MODELS_OUT = java/models
@@ -28,6 +30,10 @@ SQL_DUMP_MODEL_SPECS = \
  -cmd ".output $(MODELS_RESULTS_FILE)" \
  -cmd "select * from specs order by proc_uid ;"
 
+SQL_DUMP_MODEL_PROCS = \
+ -cmd ".mode insert procedures" \
+ -cmd "select * from procedures order by proc_uid ;"
+
 
 .PHONY: all
 all: $(MODELS_RESULTS_FILE)
@@ -66,7 +72,7 @@ $(MODELS_RESULTS_FILE): $(MAKEFILE_LIST)
  $(MAKE) capture
  $(QUIET)$(call silent_on_success,Analyzing models,$(INFER_BIN) analyze $(INFER_OPTIONS))
  sqlite3 $(RESULTS_DB) $(SQL_DUMP_MODEL_SPECS) </dev/null
-
+ sqlite3 $(CAPTURE_DB) $(SQL_DUMP_MODEL_PROCS) </dev/null >> $(MODELS_RESULTS_FILE)
 
 ifeq ($(BUILD_C_ANALYZERS),yes)
 $(MODELS_RESULTS_FILE): $(CLANG_DEPS_NO_MODELS)

infer/src/IR/Attributes.ml

@@ -68,6 +68,8 @@ let load_from_uid, load, clear_cache, store =
  (load_from_uid, load, clear_cache, store)
 
 
+let load_exn pname = Option.value_exn (load pname)
+
 let load_formal_types pname =
  match load pname with Some {formals} -> List.map formals ~f:snd3 | None -> []
 

infer/src/IR/Attributes.mli

@@ -18,6 +18,9 @@ val load_from_uid : string -> ProcAttributes.t option
 val load : Procname.t -> ProcAttributes.t option
 (** Load the attributes for the procedure from the attributes database. *)
 
+val load_exn : Procname.t -> ProcAttributes.t
+(** like [load], but raises an exception if no attributes are found. *)
+
 val is_no_return : Procname.t -> bool
 
 val load_formal_types : Procname.t -> Typ.t list

infer/src/IR/ProcAttributes.ml

@@ -57,7 +57,7 @@ type specialized_with_aliasing_info = {orig_proc: Procname.t; aliases: Pvar.t li
 
 type 'captured_var passed_closure =
  | Closure of (Procname.t * 'captured_var list)
- | Fields of 'captured_var passed_closure Fieldname.Map.t
+ | Fields of (Fieldname.t * 'captured_var passed_closure) list
 [@@deriving compare, equal]
 
 type specialized_with_closures_info =
@@ -130,6 +130,8 @@ let get_proc_name attributes = attributes.proc_name
 
 let get_loc attributes = attributes.loc
 
+let get_loc_instantiated attributes = attributes.loc_instantiated
+
 let to_return_type attributes =
  if attributes.has_added_return_param then
  match List.last attributes.formals with
@@ -201,7 +203,10 @@ let pp_specialized_with_closures_info fmt info =
  let pp_captured_vars = Pp.semicolon_seq ~print_env:Pp.text_break CapturedVar.pp in
  Pp.pair ~fst:Procname.pp ~snd:pp_captured_vars fmt closure
  | Fields field_to_function_map ->
- Fieldname.Map.pp ~pp_value:pp_passed_closure fmt field_to_function_map
+ PrettyPrintable.pp_collection
+ ~pp_item:(fun fmt (fld, func) ->
+ F.fprintf fmt "%a->%a" Fieldname.pp fld pp_passed_closure func )
+ fmt field_to_function_map
  in
  F.fprintf fmt "orig_procname=%a, formals_to_closures=%a" Procname.pp info.orig_proc
  (Pvar.Map.pp ~pp_value:pp_passed_closure)

infer/src/IR/ProcAttributes.mli

@@ -35,7 +35,7 @@ type specialized_with_aliasing_info =
 
 type 'captured_var passed_closure =
  | Closure of (Procname.t * 'captured_var list)
- | Fields of 'captured_var passed_closure Fieldname.Map.t
+ | Fields of (Fieldname.t * 'captured_var passed_closure) list
 [@@deriving compare, equal]
 
 type specialized_with_closures_info =
@@ -109,6 +109,9 @@ val get_formals : t -> (Mangled.t * Typ.t * Annot.Item.t) list
 val get_loc : t -> Location.t
 (** Return loc information for the procedure *)
 
+val get_loc_instantiated : t -> Location.t option
+(** Return instantiated loc information for the procedure *)
+
 val get_proc_name : t -> Procname.t
 
 val get_pvar_formals : t -> (Pvar.t * Typ.t) list

infer/src/IR/Procdesc.ml

@@ -774,19 +774,19 @@ end
 
 module WTO = WeakTopologicalOrder.Bourdoncle_SCC (PreProcCfg)
 
+let init_wto pdesc =
+ let wto = WTO.make pdesc in
+ let (_ : int) =
+ WeakTopologicalOrder.Partition.fold_nodes wto ~init:0 ~f:(fun idx node ->
+ node.Node.wto_index <- idx ;
+ idx + 1 )
+ in
+ pdesc.wto <- Some wto
+
+
 let get_wto pdesc =
- match pdesc.wto with
- | Some wto ->
- wto
- | None ->
- let wto = WTO.make pdesc in
- let (_ : int) =
- WeakTopologicalOrder.Partition.fold_nodes wto ~init:0 ~f:(fun idx node ->
- node.Node.wto_index <- idx ;
- idx + 1 )
- in
- pdesc.wto <- Some wto ;
- wto
+ if Option.is_none pdesc.wto then init_wto pdesc ;
+ Option.value_exn pdesc.wto
 
 
 (** Get loop heads for widening. It collects all target nodes of back-edges in a depth-first
@@ -965,6 +965,8 @@ let load =
  (run_query load_statement_adb)
 
 
+let load_exn procname = load procname |> Option.value_exn
+
 let mark_if_unchanged ~old_pdesc ~new_pdesc =
  (* map from exp names in [old_pdesc] to exp names in [new_pdesc] *)
  let exp_map = ref Exp.Map.empty in

infer/src/IR/Procdesc.mli

@@ -344,6 +344,8 @@ val set_exit_node : t -> Node.t -> unit
 
 val set_start_node : t -> Node.t -> unit
 
+val init_wto : t -> unit
+
 val get_wto : t -> Node.t WeakTopologicalOrder.Partition.t
 
 val is_loop_head : t -> Node.t -> bool
@@ -380,5 +382,8 @@ module SQLite : SqliteUtils.Data with type t = t option
 
 val load : Procname.t -> t option
 
+val load_exn : Procname.t -> t
+(** like [load], but raises an exception if no procdesc is available. *)
+
 val mark_if_unchanged : old_pdesc:t -> new_pdesc:t -> unit
 (** Record the [changed] attribute in-place on [new_pdesc] if it is unchanged wrt [old_pdsec] *)

infer/src/IR/Procname.mli

@@ -156,6 +156,7 @@ module ObjC_Cpp : sig
  ; kind: kind
  ; method_name: string
  ; parameters: Parameter.clang_parameter list
+ (** NOTE: [parameters] should NOT include additional [this/self] or [__return_param]. *)
  ; template_args: Typ.template_spec_info }
  [@@deriving compare]
 

infer/src/absint/AnalysisCallbacks.ml

@@ -15,8 +15,7 @@ type callbacks =
  -> pp_name:(Format.formatter -> unit)
  -> Procdesc.Node.t
  -> f:(unit -> 'a)
- -> 'a
- ; get_model_proc_desc_f: Procname.t -> Procdesc.t option }
+ -> 'a }
 
 let callbacks_ref : callbacks option ref = ref None
 
@@ -32,6 +31,3 @@ let get_callbacks () =
 
 let html_debug_new_node_session ?kind ~pp_name node ~f =
  (get_callbacks ()).html_debug_new_node_session_f ?kind ~pp_name node ~f
-
-
-let get_model_proc_desc proc_name = (get_callbacks ()).get_model_proc_desc_f proc_name

infer/src/absint/AnalysisCallbacks.mli

@@ -9,9 +9,6 @@ open! IStd
 
 (** {2 Analysis API} *)
 
-val get_model_proc_desc : Procname.t -> Procdesc.t option
-(** get the preanalysed procdesc of a model; raises if procname given is not a biabduction model *)
-
 val html_debug_new_node_session :
  ?kind:[`ComputePre | `ExecNode | `ExecNodeNarrowing | `WTO]
  -> pp_name:(Format.formatter -> unit)
@@ -32,8 +29,7 @@ type callbacks =
  -> pp_name:(Format.formatter -> unit)
  -> Procdesc.Node.t
  -> f:(unit -> 'a)
- -> 'a
- ; get_model_proc_desc_f: Procname.t -> Procdesc.t option }
+ -> 'a }
 
 val set_callbacks : callbacks -> unit
 (** make sure this is called before starting any actual analysis *)

infer/src/absint/ClosureSpecialization.ml

@@ -16,9 +16,8 @@ let pname_with_closure_actuals callee_pname formals_to_closures =
  | ProcAttributes.Closure (pname, _) when Procname.is_objc_block pname || Procname.is_c pname ->
  Procname.to_function_parameter pname :: acc
  | ProcAttributes.Fields passed_closures ->
- Fieldname.Map.fold
- (fun _ passed_closure acc -> get_function_parameters acc passed_closure)
- passed_closures acc
+ List.fold_right passed_closures ~init:acc ~f:(fun (_, passed_closure) acc ->
+ get_function_parameters acc passed_closure )
  | _ ->
  acc
  in
@@ -56,9 +55,9 @@ let rec get_captured_in_passed_closure captured_vars_acc = function
  | ProcAttributes.Closure (_, captured_vars) ->
  captured_vars :: captured_vars_acc
  | ProcAttributes.Fields passed_closures ->
- Fieldname.Map.fold
- (fun _ actual captured_vars_acc -> get_captured_in_passed_closure captured_vars_acc actual)
- passed_closures captured_vars_acc
+ List.fold_right passed_closures ~init:captured_vars_acc
+ ~f:(fun (_, actual) captured_vars_acc ->
+  get_captured_in_passed_closure captured_vars_acc actual )
 
 
 let get_captured actuals =