[uninit][hack] Eval static companion variable

Summary: This diff does `eval` the static companion variable, instead of manually adding it to the stack. The difference is that the latter only updates the post state, but the former updates the pre together if necessary, which helps in propagating pre's attributes to callers.

Reviewed By: davidpichardie

Differential Revision: D50224282

fbshipit-source-id: aad5e92748378e6fcce8f833a10e39fb706deff8

infer/src/pulse/PulseModelsHack.ml

@@ -345,22 +345,12 @@ let get_static_companion_var type_name =
 let get_static_companion ~model_desc path location type_name astate =
   let pvar = get_static_companion_var type_name in
   let var = Var.of_pvar pvar in
-  (* we chose on purpose to not abduce [pvar] because we don't want to make a disjunctive case
-     if it is already assigned or not. This is problematic when the caller already defines the
-     variable because the Pulse summary application will not detect that the variable is set
-     both in the callee and the caller. But this is fine as long as both functions perform the
-     same initialization of the variable. *)
-  match AbductiveDomain.Stack.find_opt var astate with
-  | Some addr_hist ->
-      (addr_hist, astate)
-  | None ->
-      let addr = AbstractValue.mk_fresh () in
-      let hist = Hist.single_call path location model_desc in
-      let astate = AbductiveDomain.Stack.add var (addr, ValueHistory.epoch) astate in
-      let static_type_name = Typ.Name.Hack.static_companion type_name in
-      let typ = Typ.mk_struct static_type_name in
-      let astate = PulseOperations.add_dynamic_type typ addr astate in
-      ((addr, hist), astate)
+  let hist = Hist.single_call path location model_desc in
+  let astate, ((addr, _) as addr_hist) = AbductiveDomain.Stack.eval hist var astate in
+  let static_type_name = Typ.Name.Hack.static_companion type_name in
+  let typ = Typ.mk_struct static_type_name in
+  let astate = PulseOperations.add_dynamic_type typ addr astate in
+  (addr_hist, astate)
 
 
 let get_static_companion_dsl ~model_desc type_name : DSL.aval DSL.model_monad =
@@ -688,13 +678,9 @@ let hhbc_cls_cns this field : model =
   @@ let* typ_opt = get_dynamic_type ~ask_specialization:true this in
      let* field_v =
        match typ_opt with
-       | Some ({Typ.desc= Tstruct name} as typ) ->
+       | Some {Typ.desc= Tstruct name} ->
            let* string_field_name = read_boxed_string_value_dsl field in
            let fld = Fieldname.make name string_field_name in
-           let class_global_var = get_static_companion_var name in
-           (* Ideally, we should not need [eval_read] here since we call [eval_deref_access] below,
-              but somehow the latter does NOT update the pre state that we need. *)
-           let* _ = eval_read (Lfield (Lvar class_global_var, fld, typ)) in
            let* class_object = get_static_companion_dsl ~model_desc name in
            eval_deref_access Read class_object (FieldAccess fld)
        | _ ->

infer/tests/codetoanalyze/hack/pulse/issues.exp

@@ -118,7 +118,7 @@ type_propagation.hack, TypePropagation::Main$static.fromParamsBad, 1, TAINT_ERRO
 type_propagation.hack, TypePropagation::Main$static.fromPropertyThroughParamBad, 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()
 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,global variable `Uninit::A$static` accessed here,read to uninitialized value occurs here]
+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]
 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