Skip to content

Commit

Permalink
[uninit][hack] Fix model of sinit to visit all fields
Browse files Browse the repository at this point in the history
Summary: This diff fixes the model of `sinit` to set all fields, including that from super classes, as uninitialized in the beginning.

Reviewed By: davidpichardie

Differential Revision: D50235110

fbshipit-source-id: 5b89eec0d7404ad536dc1f1c4f9691194238b5af
  • Loading branch information
skcho authored and facebook-github-bot committed Oct 13, 2023
1 parent 7e655b8 commit 95ef448
Show file tree
Hide file tree
Showing 5 changed files with 22 additions and 2 deletions.
16 changes: 16 additions & 0 deletions infer/src/IR/Tenv.ml
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,22 @@ let implements_remodel_class tenv name =
mem_supers tenv name ~f:(fun name _ -> Typ.Name.equal name remodel_class) )


let get_fields_trans =
let module Fields = Caml.Set.Make (struct
type t = Struct.field

let compare (x, _, _) (y, _, _) =
String.compare (Fieldname.get_field_name x) (Fieldname.get_field_name y)
end) in
fun tenv name ->
fold_supers tenv name ~init:Fields.empty ~f:(fun _ struct_opt acc ->
Option.fold struct_opt ~init:acc ~f:(fun acc {Struct.fields} ->
List.fold fields ~init:acc ~f:(fun acc (fieldname, typ, annot) ->
let fieldname = Fieldname.make name (Fieldname.get_field_name fieldname) in
Fields.add (fieldname, typ, annot) acc ) ) )
|> Fields.elements


type per_file = Global | FileLocal of t

let pp_per_file fmt = function
Expand Down
3 changes: 3 additions & 0 deletions infer/src/IR/Tenv.mli
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,9 @@ val find_map_supers : t -> Typ.Name.t -> f:(Typ.Name.t -> Struct.t option -> 'a
val implements_remodel_class : t -> Typ.Name.t -> bool
(** Check if a class implements the Remodel class *)

val get_fields_trans : t -> Typ.Name.t -> Struct.fields
(** Get all fields from the super classes transitively *)

type per_file = Global | FileLocal of t

val pp_per_file : Format.formatter -> per_file -> unit
Expand Down
2 changes: 1 addition & 1 deletion infer/src/pulse/Pulse.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1431,7 +1431,7 @@ let set_uninitialize_prop path tenv ({ProcAttributes.loc} as proc_attrs) astate
if Procname.is_hack_sinit pname then
let ( let* ) x f = match x with None -> astate | Some x -> f x in
let* name = Procname.get_class_type_name pname in
let* {Struct.fields} = Tenv.lookup tenv name in
let fields = Tenv.get_fields_trans tenv name in
let class_global_var = PulseModelsHack.get_static_companion_var name in
let typ = Typ.mk_struct name in
List.fold fields ~init:astate ~f:(fun astate (fld, {Typ.quals= fld_quals}, _) ->
Expand Down
1 change: 1 addition & 0 deletions infer/tests/codetoanalyze/hack/pulse/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ type_propagation.hack, TypePropagation::Main$static.fromPropertyThroughParamBad,
type_propagation.hack, TypePropagation::Main$static.fromPropertyThroughNewBad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `TypePropagation::A.getTainted`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `TypePropagation::A.getTainted`,value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: TypePropagation::A.getTainted()
type_propagation.hack, TypePropagation::Main$static.fromGlobalBad, 1, TAINT_ERROR, no_bucket, ERROR, [in call to `TypePropagation::A.getTainted`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `TypePropagation::A.getTainted`,value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: TypePropagation::A.getTainted()
uninit.hack, $root.Uninit::call_get_field_bad, 1, PULSE_UNINITIALIZED_CONST, no_bucket, ERROR, [global variable `Uninit::A$static` accessed here,when calling `Uninit::A$static.get_field` here,in call to `hhbc_cls_cns` (modelled),read to uninitialized value occurs here]
uninit.hack, $root.Uninit::call_self_get_field_Bad, 1, PULSE_UNINITIALIZED_CONST, no_bucket, ERROR, [global variable `Uninit::AbstractUseTrait$static` accessed here,when calling `Uninit::AbstractUseTrait$static.self_get_field` here,in call to `add_self_for_hack_traits` (modelled),when calling `Uninit::MyTrait$static.get_field_from_trait` here,in call to `hhbc_cls_cns` (modelled),read to uninitialized value occurs here]
unknown.hack, $root.Unknown::basicFlowBad, 3, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#0` to `$root.Unknown::basicFlowBad` with kind `Simple`,value passed as argument `#0` to `Unknown::UnknownClass$static.explicitSinkAllArgs` with kind `Simple`], source: $root.Unknown::basicFlowBad, sink: Unknown::UnknownClass$static.explicitSinkAllArgs, tainted expression: $sc
unknown.hack, $root.Unknown::basicFlowReturnBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,in call to function `?.myUnknownFun` with no summary,value passed as argument `#0` to `Unknown::UnknownClass$static.explicitSinkAllArgs` with kind `Simple`], source: $root.Level1::taintSource, sink: Unknown::UnknownClass$static.explicitSinkAllArgs, tainted expression: ?.myUnknownFun()
variadic.hack, DictTests::Variadic$static.callVariadicWith2ArgsBad, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,when calling `DictTests::Variadic$static.variadicArgInSink` here,value passed as argument `#0` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $root.Level1::taintSource().__infer_model_backing_vec_fst
Expand Down
2 changes: 1 addition & 1 deletion infer/tests/codetoanalyze/hack/pulse/uninit.hack
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,6 @@ abstract class AbstractUseTrait extends A {
}
}

function call_self_get_field_Bad_FN(): string {
function call_self_get_field_Bad(): string {
return AbstractUseTrait::self_get_field();
}

0 comments on commit 95ef448

Please sign in to comment.