From 668901b9b791705a9611facce8cb3c32ff1c2ad8 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 11 Oct 2023 02:11:48 -0700 Subject: [PATCH] [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 | 6 ++++++ infer/src/IR/Procname.mli | 3 +++ infer/src/pulse/PulseModelsDSL.ml | 12 ++++++++++++ infer/src/pulse/PulseModelsDSL.mli | 9 +++++++++ infer/src/pulse/PulseModelsHack.ml | 15 +++++++++++++++ infer/tests/codetoanalyze/hack/pulse/issues.exp | 2 ++ infer/tests/codetoanalyze/hack/pulse/uninit.hack | 4 ++-- 7 files changed, 49 insertions(+), 2 deletions(-) diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml index 600d70b2558..7944b713251 100644 --- a/infer/src/IR/Procname.ml +++ b/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] diff --git a/infer/src/IR/Procname.mli b/infer/src/IR/Procname.mli index 59641bab5f4..24ef9daec79 100644 --- a/infer/src/IR/Procname.mli +++ b/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, diff --git a/infer/src/pulse/PulseModelsDSL.ml b/infer/src/pulse/PulseModelsDSL.ml index dfa282cdc05..91863c98df0 100644 --- a/infer/src/pulse/PulseModelsDSL.ml +++ b/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 diff --git a/infer/src/pulse/PulseModelsDSL.mli b/infer/src/pulse/PulseModelsDSL.mli index 0484c7a29a6..5aa87443755 100644 --- a/infer/src/pulse/PulseModelsDSL.mli +++ b/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 diff --git a/infer/src/pulse/PulseModelsHack.ml b/infer/src/pulse/PulseModelsHack.ml index e268fdc8869..c428db9741f 100644 --- a/infer/src/pulse/PulseModelsHack.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/hack/pulse/issues.exp b/infer/tests/codetoanalyze/hack/pulse/issues.exp index ca5bb150f03..b5b19a60289 100644 --- a/infer/tests/codetoanalyze/hack/pulse/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/hack/pulse/uninit.hack b/infer/tests/codetoanalyze/hack/pulse/uninit.hack index 7c3c3bad7f1..62f222a3105 100644 --- a/infer/tests/codetoanalyze/hack/pulse/uninit.hack +++ b/infer/tests/codetoanalyze/hack/pulse/uninit.hack @@ -13,7 +13,7 @@ abstract class A { } } -function call_get_field_bad_FN(): string { +function call_get_field_bad(): string { return A::get_field(); } @@ -21,6 +21,6 @@ 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(); }