Skip to content

Commit

Permalink
[uninit const] Suppress issue when there is missed capture type
Browse files Browse the repository at this point in the history
Summary:
This diff suppresses the uninit const issue when there is a missed capture type, like we do for
uninit method checker.

Note: The collected missed capture types are not used for reactive capture yet.

Reviewed By: geralt-encore

Differential Revision:
D64825940

Privacy Context Container: L1208441

fbshipit-source-id: 6739c525c081d9f1c5b4c97c096323a200f392e1
  • Loading branch information
skcho authored and facebook-github-bot committed Oct 23, 2024
1 parent 7304d70 commit f50c0bf
Show file tree
Hide file tree
Showing 6 changed files with 37 additions and 16 deletions.
18 changes: 14 additions & 4 deletions infer/src/IR/Tenv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -137,15 +137,25 @@ let resolve_field_info tenv name fieldname =


let resolve_fieldname tenv name fieldname_str =
(* problem is that it gets dummy, missed capture *)
let missed_capture_types = ref Typ.Name.Set.empty in
let find ~f =
find_map_supers ~ignore_require_extends:true tenv name ~f:(fun name str_opt ->
Option.bind str_opt ~f:(fun {Struct.fields} ->
if List.exists fields ~f then Some name else None ) )
match str_opt with
| None | Some {dummy= true} ->
if Language.curr_language_is Hack then
missed_capture_types := Typ.Name.Set.add name !missed_capture_types ;
None
| Some {Struct.fields} ->
if List.exists fields ~f then Some name else None )
in
let is_fld {Struct.name} = String.equal (Fieldname.get_field_name name) fieldname_str in
let is_non_abstract_fld ({Struct.annot} as x) = is_fld x && not (Annot.Item.is_abstract annot) in
(match find ~f:is_non_abstract_fld with Some _ as fld -> fld | None -> find ~f:is_fld)
|> Option.map ~f:(fun name -> Fieldname.make name fieldname_str)
let resolved_fld =
(match find ~f:is_non_abstract_fld with Some _ as fld -> fld | None -> find ~f:is_fld)
|> Option.map ~f:(fun name -> Fieldname.make name fieldname_str)
in
(resolved_fld, !missed_capture_types)


let mem_supers tenv name ~f =
Expand Down
4 changes: 2 additions & 2 deletions infer/src/IR/Tenv.mli
Original file line number Diff line number Diff line change
Expand Up @@ -154,8 +154,8 @@ val resolve_field_info : t -> Typ.Name.t -> Fieldname.t -> Struct.field_info opt
(** [resolve_field_info tenv class_name field] tries to find the first field declaration that
matches [field] name (ignoring its enclosing declared type), starting from class [class_name]. *)

val resolve_fieldname : t -> Typ.Name.t -> string -> Fieldname.t option
(** Similar to [resolve_field_info], but returns the resolved field name. *)
val resolve_fieldname : t -> Typ.Name.t -> string -> Fieldname.t option * Typ.Name.Set.t
(** Similar to [resolve_field_info], but returns the resolved field name and missed capture types. *)

val find_cpp_destructor : t -> Typ.Name.t -> Procname.t option

Expand Down
17 changes: 12 additions & 5 deletions infer/src/pulse/PulseModelsDSL.ml
Original file line number Diff line number Diff line change
Expand Up @@ -357,9 +357,10 @@ module Syntax = struct
PulseOperations.eval_deref path location exp |> exec_partial_operation


let load_access aval access : aval model_monad =
let load_access ?(no_access = false) aval access : aval model_monad =
let* {path; location} = get_data in
PulseOperations.eval_deref_access path Read location aval access
let mode = if no_access then NoAccess else Read in
PulseOperations.eval_deref_access path mode location aval access
>> sat |> exec_partial_operation


Expand Down Expand Up @@ -501,10 +502,16 @@ module Syntax = struct
ret info data astate


let tenv_resolve_fieldname typ_name name : Fieldname.t option model_monad =
let tenv_resolve_fieldname typ_name name :
(Fieldname.t option * Tenv.unresolved_reason option) model_monad =
fun ((_desc, {analysis_data= {tenv}}) as data) astate ->
let field_name = Tenv.resolve_fieldname tenv typ_name name in
ret field_name data astate
(* warning: we skipped missed capture informations here *)
let field_name, missed_capture_types = Tenv.resolve_fieldname tenv typ_name name in
let unresolved_reason =
if Typ.Name.Set.is_empty missed_capture_types then None
else Some Tenv.MaybeMissingDueToMissedCapture
in
ret (field_name, unresolved_reason) data astate


let tenv_resolve_method typ_name proc_name : Procname.t option model_monad =
Expand Down
5 changes: 3 additions & 2 deletions infer/src/pulse/PulseModelsDSL.mli
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ module Syntax : sig

val access : access_mode -> aval -> Access.t -> aval model_monad

val load_access : aval -> Access.t -> aval model_monad
val load_access : ?no_access:bool -> aval -> Access.t -> aval model_monad

val load : aval -> aval model_monad
(** read the Dereference access from the value *)
Expand Down Expand Up @@ -231,7 +231,8 @@ module Syntax : sig

val tenv_resolve_field_info : Typ.name -> Fieldname.t -> Struct.field_info option model_monad

val tenv_resolve_fieldname : Typ.name -> string -> Fieldname.t option model_monad
val tenv_resolve_fieldname :
Typ.name -> string -> (Fieldname.t option * Tenv.unresolved_reason option) model_monad

(** {2 Invalidation operations} *)

Expand Down
6 changes: 4 additions & 2 deletions infer/src/pulse/PulseModelsHack.ml
Original file line number Diff line number Diff line change
Expand Up @@ -935,7 +935,7 @@ let hack_array_idx this key default_val : model =

let eval_resolved_field ~model_desc typ_name fld_str =
let open DSL.Syntax in
let* fld_opt = tenv_resolve_fieldname typ_name fld_str in
let* fld_opt, unresolved_reason = tenv_resolve_fieldname typ_name fld_str in
let name, fld =
match fld_opt with
| None ->
Expand All @@ -945,7 +945,9 @@ let eval_resolved_field ~model_desc typ_name fld_str =
(Fieldname.get_class_name fld, fld)
in
let* class_object = get_static_companion_dsl ~model_desc name in
load_access class_object (FieldAccess fld)
(* Note: We avoid the MustBeInitialized attribute to be added when the field resolution is
incomplete to avoid false positives. *)
load_access ~no_access:(Option.is_some unresolved_reason) class_object (FieldAccess fld)


let internal_hack_field_get this field : DSL.aval DSL.model_monad =
Expand Down
3 changes: 2 additions & 1 deletion infer/src/pulse/PulseOperations.ml
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,8 @@ let eval_access path ?must_be_valid_reason mode location addr_hist access astate


let eval_deref_access path ?must_be_valid_reason mode location addr_hist access astate =
let* astate, addr_hist = eval_access path Read location addr_hist access astate in
let ptr_mode = match mode with NoAccess -> NoAccess | Read | Write -> Read in
let* astate, addr_hist = eval_access path ptr_mode location addr_hist access astate in
eval_access path ?must_be_valid_reason mode location addr_hist Dereference astate


Expand Down

0 comments on commit f50c0bf

Please sign in to comment.