[uninit][hack] Revise lazy_class_initialize model to call sinit

Summary: This diff revises the `lazy_class_initialize` model as calling `sinit`, so that it can get the information that which static fields are initialized/uninitialized statically.

Reviewed By: davidpichardie

Differential Revision: D49727580

fbshipit-source-id: 26bd90bc8f65690950a1312cc6a2e7a390f19535

infer/src/IR/Procname.ml

@@ -678,6 +678,10 @@ module Hack = struct
 
 
   let get_class_name_as_a_string {class_name} = Option.map class_name ~f:HackClassName.classname
+
+  let get_static_init class_name =
+    let static_class_name = HackClassName.static_companion class_name in
+    {class_name= Some static_class_name; function_name= "_86sinit"; arity= Some 1}
 end
 
 module Python = struct
@@ -1581,6 +1585,8 @@ let erlang_call_qualified ~arity = Erlang (Erlang.call_qualified arity)
 
 let get_hack_arity = function Hack hack_proc_name -> Hack.get_arity hack_proc_name | _ -> None
 
+let get_hack_static_init class_name = Hack (Hack.get_static_init class_name)
+
 module Hashable = struct
   type nonrec t = t [@@deriving compare, equal]
 

infer/src/IR/Procname.mli

@@ -509,6 +509,9 @@ val get_qualifiers : t -> QualifiedCppName.t
 val get_hack_arity : t -> int option
 (** get the arity of a Hack procname *)
 
+val get_hack_static_init : HackClassName.t -> t
+(** get the sinit procname in Hack *)
+
 val pp_name_only : F.formatter -> t -> unit
 (** Print name of procedure with at most one-level path. For example,
 

infer/src/pulse/PulseModelsDSL.ml

@@ -209,6 +209,11 @@ module Syntax = struct
     PulseOperations.eval path Read location exp |> exec_partial_operation
 
 
+  let eval_to_value_origin exp : ValueOrigin.t model_monad =
+    let* {path; location} = get_data in
+    PulseOperations.eval_to_value_origin path Read location exp |> exec_partial_operation
+
+
   let allocation attr (addr, _) : unit model_monad =
     let* {location} = get_data in
     PulseOperations.allocate attr location addr |> exec_command
@@ -294,4 +299,11 @@ module Syntax = struct
     | _ ->
         Logging.d_printfln "[ocaml model] No dynamic type found!" ;
         Option.value_map default ~default:(disjuncts []) ~f:Fn.id
+
+
+  let dispatch_call ret pname actuals func_args : unit model_monad =
+    lift_to_monad
+    @@ fun {analysis_data; dispatch_call_eval_args; path; location} astate ->
+    dispatch_call_eval_args analysis_data path ret (Const (Cfun pname)) actuals func_args location
+      CallFlags.default astate (Some pname)
 end

infer/src/pulse/PulseModelsDSL.mli

@@ -40,6 +40,13 @@ module Syntax : sig
   val dynamic_dispatch :
     cases:(Typ.name * 'a model_monad) list -> ?default:'a model_monad -> aval -> 'a model_monad
 
+  val dispatch_call :
+       Ident.t * Typ.t
+    -> Procname.t
+    -> (Exp.t * Typ.t) list
+    -> ValueOrigin.t ProcnameDispatcher.Call.FuncArg.t list
+    -> unit model_monad
+
   val get_data : PulseModelsImport.model_data model_monad
 
   (* disjunctive reasonning *)
@@ -70,6 +77,8 @@ module Syntax : sig
 
   val eval_read : Exp.t -> aval model_monad
 
+  val eval_to_value_origin : Exp.t -> ValueOrigin.t model_monad
+
   val eval_deref_access : access_mode -> aval -> Access.t -> aval model_monad
 
   val get_dynamic_type : ask_specialization:bool -> aval -> Typ.t option model_monad

infer/src/pulse/PulseModelsHack.ml

@@ -236,6 +236,8 @@ let get_static_companion_dsl ~model_desc type_name : DSL.aval DSL.model_monad =
   exec_operation (get_static_companion ~model_desc path location type_name)
 
 
+(* NOTE: We model [lazy_class_initialize] as invoking the corresponding [sinit] procedure.  This is
+   unsound in terms of that it gets non-final values. *)
 let lazy_class_initialize size_exp : model =
   let open DSL.Syntax in
   start_model
@@ -249,6 +251,19 @@ let lazy_class_initialize size_exp : model =
           "lazy_class_initialize: the Hack frontend should never generate such argument type"
   in
   let* class_object = get_static_companion_dsl ~model_desc:"lazy_class_initialize" type_name in
+  let* () =
+    match type_name with
+    | HackClass class_name ->
+        let ret_id = Ident.create_none () in
+        let ret_typ = Typ.mk_ptr (Typ.mk_struct TextualSil.hack_mixed_type_name) in
+        let pname = Procname.get_hack_static_init class_name in
+        let exp = Exp.Lvar (get_static_companion_var type_name) in
+        let typ = Typ.mk_struct type_name in
+        let* arg_payload = eval_to_value_origin exp in
+        dispatch_call (ret_id, ret_typ) pname [(exp, typ)] [{exp; typ; arg_payload}]
+    | _ ->
+        ret ()
+  in
   assign_ret class_object
 
 

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

@@ -116,6 +116,8 @@ 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_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

@@ -13,14 +13,14 @@ abstract class A {
   }
 }
 
-function call_get_field_bad_FN(): string {
+function call_get_field_bad(): string {
   return A::get_field();
 }
 
 class B extends A {
   const string FIELD = "defined";
 }
 
-function call_get_field_ok(): string {
+function call_get_field_ok_FP(): string {
   return B::get_field();
 }