[uninit][hack] Add semantic model for hack_set_static_prop

Summary: This diff adds semantic model for `hack_set_static_prop`.

Reviewed By: davidpichardie

Differential Revision: D49727594

fbshipit-source-id: be65f391af0246c26e6619aac214e0df9b777cb5

infer/src/pulse/PulseModelsHack.ml

@@ -548,6 +548,17 @@ let hhbc_cls_cns this field : model =
      assign_ret field_v
 
 
+let hack_set_static_prop this prop obj : model =
+  let open DSL.Syntax in
+  start_model
+  @@ let* this = read_boxed_string_value_dsl this in
+     let this = String.substr_replace_all ~pattern:"\\" ~with_:":" this in
+     let* prop = read_boxed_string_value_dsl prop in
+     let name = Typ.HackClass (HackClassName.static_companion (HackClassName.make this)) in
+     let* class_object = get_static_companion_dsl ~model_desc:"hack_set_static_prop" name in
+     write_deref_field ~ref:class_object ~obj (Fieldname.make name prop)
+
+
 let matchers : matcher list =
   let open ProcnameDispatcher.Call in
   [ -"$builtins" &:: "nondet" <>$$--> Basic.nondet ~desc:"nondet"
@@ -569,6 +580,8 @@ let matchers : matcher list =
   ; -"$builtins" &:: "hhbc_cmp_nsame" <>$ capt_arg_payload $+ capt_arg_payload $--> hhbc_cmp_nsame
   ; -"$builtins" &:: "hack_get_static_class" <>$ capt_arg_payload $--> get_static_class
   ; -"$builtins" &:: "hhbc_cls_cns" <>$ capt_arg_payload $+ capt_arg_payload $--> hhbc_cls_cns
+  ; -"$builtins" &:: "hack_set_static_prop" <>$ capt_arg_payload $+ capt_arg_payload
+    $+ capt_arg_payload $--> hack_set_static_prop
   ; -"$root" &:: "FlibSL::Vec::from_async" <>$ capt_arg_payload $+ capt_arg_payload
     $--> Vec.vec_from_async ]
   |> List.map ~f:(ProcnameDispatcher.Call.contramap_arg_payload ~f:ValueOrigin.addr_hist)

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

@@ -117,7 +117,6 @@ 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,global variable `Uninit::A$static` accessed here,read to uninitialized value occurs here]
-uninit.hack, $root.Uninit::call_get_field_ok_FP, 1, PULSE_UNINITIALIZED_CONST, no_bucket, ERROR, [global variable `Uninit::B$static` accessed here,when calling `Uninit::A$static.get_field` here,global variable `Uninit::B$static` accessed here,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()
 vec_from_async.hack, $root.vecFromAsyncBad, 3, PULSE_RESOURCE_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated here,awaitable becomes unreachable here]

infer/tests/codetoanalyze/hack/pulse/uninit.hack

@@ -21,6 +21,20 @@ class B extends A {
   const string FIELD = "defined";
 }
 
-function call_get_field_ok_FP(): string {
+function call_get_field_ok(): string {
   return B::get_field();
 }
+
+abstract class RetField {
+  abstract const string ret;
+
+  public static function get_ret_field(): string {
+    return static::ret;
+  }
+}
+
+// Current frontend translates the field name of [ret] as [ret_] in the class declaration, due to
+// the reserved word in Textual.
+function call_get_ret_field_bad_FN(): string {
+  return RetField::get_ret_field();
+}