[inferpython] assign the right param names during closure calls

Summary:
InferPython relies on a specific calling convention. Each function has
one parameter names `locals` which is a dicitonary. Its keys are the parameters of the
source function. In this diff we make sure this dicitonary is properly initialized during a
function call.

Reviewed By: skcho

Differential Revision:
D65416842

Privacy Context Container: L1208441

fbshipit-source-id: 13b4165fa2e18363bbaeddfa92f8bf6f46086816

infer/src/IR/ProcAttributes.ml

@@ -128,6 +128,9 @@ type t =
   ; hack_variadic_position: int option
         (** the procedure is variadic and [Some n] means the variadic vector is composed of the
             arguments n, n+1, ..., length formals -1 *)
+  ; python_args: string list
+        (** each python function has a list of parameters that we store as a special ProcAttribute
+            while list formals will only contain dict parameters like Python locals *)
   ; sentinel_attr: (int * int) option  (** __attribute__((sentinel(int, int))) *)
   ; specialized_with_aliasing_info: specialized_with_aliasing_info option
   ; specialized_with_closures_info: specialized_with_closures_info option
@@ -216,6 +219,7 @@ let default translation_unit proc_name =
   ; is_synthetic_method= false
   ; is_clang_variadic= false
   ; hack_variadic_position= None
+  ; python_args= []
   ; sentinel_attr= None
   ; clang_method_kind= ClangMethodKind.C_FUNCTION
   ; loc= Location.dummy
@@ -294,6 +298,7 @@ let pp f
      ; is_synthetic_method
      ; is_clang_variadic
      ; hack_variadic_position
+     ; python_args
      ; sentinel_attr
      ; clang_method_kind
      ; loc
@@ -382,6 +387,8 @@ let pp f
     () ;
   pp_bool_default ~default:default.is_clang_variadic "is_clang_variadic" is_clang_variadic f () ;
   Option.iter hack_variadic_position ~f:(fun n -> F.fprintf f "; hack_variadic_position= %d@," n) ;
+  if Language.curr_language_is Python then
+    F.fprintf f "; python_args= [%a]," (Pp.semicolon_seq F.pp_print_string) python_args ;
   if not ([%equal: (int * int) option] default.sentinel_attr sentinel_attr) then
     F.fprintf f "; sentinel_attr= %a@,"
       (Pp.option (Pp.pair ~fst:F.pp_print_int ~snd:F.pp_print_int))

infer/src/IR/ProcAttributes.mli

@@ -89,6 +89,9 @@ type t =
   ; hack_variadic_position: int option
         (** the procedure is variadic and [Some n] means the variadic vector is composed of the
             arguments n, n+1, ..., length formals -1 *)
+  ; python_args: string list
+        (** each python function has a list of parameters that we store as a special ProcAttribute
+            while list formals will only contain dict parameters like Python locals *)
   ; sentinel_attr: (int * int) option  (** __attribute__((sentinel(int, int))) *)
   ; specialized_with_aliasing_info: specialized_with_aliasing_info option
         (** the procedure is a clone specialized with captured variables and paramaters sharing

infer/src/pulse/PulseModelsDSL.ml

@@ -7,6 +7,7 @@
 
 open! IStd
 module L = Logging
+module IRAttributes = Attributes
 open PulseBasicInterface
 open PulseDomainInterface
 open PulseOperationResult.Import
@@ -802,7 +803,11 @@ module Syntax = struct
     |> exec_partial_command
 
 
-  let apply_closure lang (closure : aval) closure_args : aval model_monad =
+  type closure_args =
+    | Regular of aval list
+    | FromAttributes of (ProcAttributes.t -> aval list model_monad)
+
+  let apply_closure lang (closure : aval) unresolved_pname closure_args : aval model_monad =
     let mixed_type_name =
       match (lang : Textual.Lang.t) with
       | Hack ->
@@ -813,17 +818,6 @@ module Syntax = struct
           L.die InternalError "apply_closure is not supported on Java"
     in
     let typ = Typ.mk_ptr (Typ.mk_struct mixed_type_name) in
-    let args = closure :: closure_args in
-    let unresolved_pname =
-      match (lang : Textual.Lang.t) with
-      | Hack ->
-          Procname.make_hack ~class_name:(Some HackClassName.wildcard) ~function_name:"__invoke"
-            ~arity:(Some (List.length args))
-      | Python ->
-          Procname.make_python ~class_name:(Some PythonClassName.wildcard) ~function_name:"call"
-      | Java ->
-          L.die InternalError "apply_closure is not supported on Java"
-    in
     let* opt_dynamic_type_data = get_dynamic_type ~ask_specialization:true closure in
     match opt_dynamic_type_data with
     | Some {Formula.typ= {Typ.desc= Tstruct type_name}} -> (
@@ -837,6 +831,17 @@ module Syntax = struct
         | Some resolved_pname ->
             L.d_printfln "[ocaml model] Closure resolved to a call to %a" Procname.pp resolved_pname ;
             let ret_id = Ident.create_none () in
+            let* closure_args =
+              match closure_args with
+              | Regular closure_args ->
+                  ret closure_args
+              | FromAttributes gen_closure_args ->
+                  IRAttributes.load resolved_pname |> Option.map ~f:gen_closure_args
+                  |> Option.value_or_thunk ~default:(fun () ->
+                         L.d_printfln "[ocaml model] Failed to load attributes" ;
+                         ret [] )
+            in
+            let args = closure :: closure_args in
             let call_args =
               List.mapi args ~f:(fun i arg : ValueOrigin.t ProcnameDispatcher.Call.FuncArg.t ->
                   let pvar =
@@ -856,6 +861,21 @@ module Syntax = struct
         ret unknown_res
 
 
+  let apply_hack_closure closure closure_args =
+    let unresolved_pname =
+      Procname.make_hack ~class_name:(Some HackClassName.wildcard) ~function_name:"__invoke"
+        ~arity:(Some (1 + List.length closure_args))
+    in
+    apply_closure Hack closure unresolved_pname (Regular closure_args)
+
+
+  let apply_python_closure closure gen_closure_args =
+    let unresolved_pname =
+      Procname.make_python ~class_name:(Some PythonClassName.wildcard) ~function_name:"call"
+    in
+    apply_closure Python closure unresolved_pname (FromAttributes gen_closure_args)
+
+
   module Basic = struct
     (* See internal_new_. We do some crafty unboxing to make the external API nicer *)
     let return_alloc_not_null allocator size ~initialize : unit model_monad =

infer/src/pulse/PulseModelsDSL.mli

@@ -80,7 +80,9 @@ module Syntax : sig
     -> ValueOrigin.t ProcnameDispatcher.Call.FuncArg.t list
     -> unit model_monad
 
-  val apply_closure : Textual.Lang.t -> aval -> aval list -> aval model_monad
+  val apply_hack_closure : aval -> aval list -> aval model_monad
+
+  val apply_python_closure : aval -> (ProcAttributes.t -> aval list model_monad) -> aval model_monad
 
   val get_data : model_data model_monad
 

infer/src/pulse/PulseModelsHack.ml

@@ -183,16 +183,16 @@ module Vec = struct
       prune_eq_int size_val IntLit.one
       @@>
       let* fst_val = load_access arg (FieldAccess fst_field) in
-      let* mapped_fst_val = apply_closure Hack closure [fst_val] in
+      let* mapped_fst_val = apply_hack_closure closure [fst_val] in
       new_vec_dsl [mapped_fst_val]
     in
     let size_gt_1_case : DSL.aval DSL.model_monad =
       prune_gt_int size_val IntLit.one
       @@>
       let* fst_val = load_access arg (FieldAccess fst_field) in
       let* snd_val = load_access arg (FieldAccess snd_field) in
-      let* mapped_fst_val = apply_closure Hack closure [fst_val] in
-      let* mapped_snd_val = apply_closure Hack closure [snd_val] in
+      let* mapped_fst_val = apply_hack_closure closure [fst_val] in
+      let* mapped_snd_val = apply_hack_closure closure [snd_val] in
       new_vec_dsl ~know_size:(Some size_val) [mapped_fst_val; mapped_snd_val]
     in
     let* ret = disj [size_eq_0_case; size_eq_1_case; size_gt_1_case] in

infer/src/pulse/PulseModelsPython.ml

@@ -6,7 +6,6 @@
  *)
 
 open! IStd
-module F = Format
 module L = Logging
 open PulseBasicInterface
 open PulseModelsImport
@@ -16,11 +15,12 @@ let dict_tname = TextualSil.python_dict_type_name
 
 let none_tname = TextualSil.python_none_type_name
 
-let sil_fieldname_from_string_value_exn ((address, _) : DSL.aval) : Fieldname.t DSL.model_monad =
+let sil_fieldname_from_string_value_exn type_name ((address, _) : DSL.aval) :
+    Fieldname.t DSL.model_monad =
   let f astate =
     match PulseArithmetic.as_constant_string astate address with
     | Some str ->
-        (TextualSil.wildcard_sil_fieldname Python str, astate)
+        (Fieldname.make type_name str, astate)
     | None ->
         L.die InternalError "expecting constant string value"
   in
@@ -39,26 +39,27 @@ module Dict = struct
 
   let get dict key : DSL.aval DSL.model_monad =
     let open DSL.Syntax in
-    let* field = sil_fieldname_from_string_value_exn key in
+    let* field = sil_fieldname_from_string_value_exn dict_tname key in
     load_access dict (FieldAccess field)
 
 
   let set dict key value : unit DSL.model_monad =
     let open DSL.Syntax in
-    let* field = sil_fieldname_from_string_value_exn key in
+    let* field = sil_fieldname_from_string_value_exn dict_tname key in
     let* () = store_field ~ref:dict field value in
     ret ()
 end
 
 let call closure _arg_names args : model =
-  (* TODO: take into account arg_names *)
-  (* TODO: fix the name of the positional arguments *)
+  (* TODO: take into account named args *)
   let open DSL.Syntax in
   start_model
   @@ fun () ->
-  let keys = List.init (List.length args) ~f:(fun i -> F.asprintf "#%d" i) in
-  let* locals = Dict.make keys args in
-  let* value = apply_closure Python closure [locals] in
+  let gen_closure_args {ProcAttributes.python_args} =
+    let* locals = Dict.make python_args args in
+    ret [locals]
+  in
+  let* value = apply_python_closure closure gen_closure_args in
   assign_ret value
 
 

infer/src/python/PyIR2Textual.ml

@@ -47,7 +47,14 @@ let mk_qualified_proc_name ?loc kind =
   ; name= Textual.ProcName.of_string ?loc qual_name_str }
 
 
-let mk_procdecl ?loc kind =
+let mk_procdecl_attributes {CodeInfo.co_argcount; co_varnames} =
+  let values =
+    List.init co_argcount ~f:(fun i -> co_varnames.(i)) |> List.map ~f:(F.asprintf "%a" Ident.pp)
+  in
+  if List.is_empty values then [] else [Textual.Attr.mk_python_args values]
+
+
+let mk_procdecl ?loc kind code_info =
   let qualified_name = mk_qualified_proc_name ?loc kind in
   let formals_types =
     if is_module_body kind then Some []
@@ -56,7 +63,7 @@ let mk_procdecl ?loc kind =
         [Textual.Typ.mk_without_attributes Typ.globals; Textual.Typ.mk_without_attributes Typ.locals]
   in
   let result_type = Textual.Typ.mk_without_attributes Typ.value in
-  let attributes = [] in
+  let attributes = mk_procdecl_attributes code_info in
   {Textual.ProcDecl.qualified_name; formals_types; result_type; attributes}
 
 
@@ -438,9 +445,9 @@ let of_node is_module_body entry {Node.name; first_loc; last_loc; ssa_parameters
   {Textual.Node.label; ssa_parameters; exn_succs; last; instrs; last_loc; label_loc}
 
 
-let mk_procdesc proc_kind {CFG.entry; nodes; code_info= {co_firstlineno}} =
+let mk_procdesc proc_kind {CFG.entry; nodes; code_info= {co_firstlineno} as code_info} =
   let loc = Textual.Location.known ~line:co_firstlineno ~col:(-1) in
-  let procdecl = mk_procdecl ~loc proc_kind in
+  let procdecl = mk_procdecl ~loc proc_kind code_info in
   let is_module_body = is_module_body proc_kind in
   let nodes_bindings = NodeName.Map.bindings nodes in
   let nodes =

infer/src/python/unit/PyIR2TextualTest.ml

@@ -73,7 +73,7 @@ def g():
 
     }
 
-    define dummy::f(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
+    define .args = "y,l" dummy::f(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
       #b0:
           n0 = $builtins.py_load_fast("y", locals)
           if n0 then jmp b1 else jmp b2
@@ -134,7 +134,7 @@ def g():
 
     }
 
-    define dummy::f(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
+    define .args = "y,l" dummy::f(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
       #b0:
           n0 = $builtins.py_load_fast("y", [&locals:*PyLocals])
           if n0 then jmp b1 else jmp b2
@@ -195,7 +195,7 @@ def g():
 
     type closure:dummy:0 = {globals: *PyGlobals}
 
-    define closure:dummy:0.call(__this: *closure:dummy:0, locals: *PyLocals) : *PyObject {
+    define .args = "y,l" closure:dummy:0.call(__this: *closure:dummy:0, locals: *PyLocals) : *PyObject {
       #entry:
           n0:*closure:dummy:0 = load &__this
           n1:*PyGlobals = load n0.?.globals
@@ -243,7 +243,7 @@ def g():
 
     }
 
-    define dummy::f(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
+    define .args = "y,l" dummy::f(globals: *PyGlobals, locals: *PyLocals) : *PyObject {
       #b0:
           n13:*PyLocals = load &locals
           n0 = $builtins.py_load_fast("y", n13)

infer/src/textual/Textual.ml

@@ -268,6 +268,10 @@ module Attr = struct
 
   let is_variadic {name; values} = String.equal name "variadic" && List.is_empty values
 
+  let mk_python_args values = {name= "args"; values; loc= Location.Unknown}
+
+  let find_python_args {name; values} = if String.equal name "args" then Some values else None
+
   let pp fmt {name; values} =
     if List.is_empty values then F.fprintf fmt ".%s" name
     else F.fprintf fmt ".%s = \"%a\"" name (Pp.comma_seq F.pp_print_string) values

infer/src/textual/Textual.mli

@@ -127,6 +127,10 @@ module Attr : sig
 
   val is_const : t -> bool
 
+  val mk_python_args : string list -> t
+
+  val find_python_args : t -> string list option
+
   val mk_trait : t
 
   val pp : F.formatter -> t -> unit [@@warning "-unused-value-declaration"]

infer/src/textual/TextualSil.ml

@@ -1064,6 +1064,9 @@ module ProcDescBridge = struct
     let is_hack_async = List.exists procdecl.attributes ~f:Attr.is_async in
     let is_abstract = List.exists procdecl.attributes ~f:Attr.is_abstract in
     let is_hack_wrapper = List.exists procdecl.attributes ~f:Attr.is_hack_wrapper in
+    let python_args =
+      List.find_map procdecl.attributes ~f:Attr.find_python_args |> Option.value ~default:[]
+    in
     let hack_variadic_position =
       Option.value_map ~default:None procdecl.formals_types ~f:(fun formals_types ->
           List.findi formals_types ~f:(fun _ typ -> Typ.is_annotated typ ~f:Attr.is_variadic)
@@ -1078,6 +1081,7 @@ module ProcDescBridge = struct
       ; is_abstract
       ; is_hack_wrapper
       ; hack_variadic_position
+      ; python_args
       ; formals
       ; locals
       ; ret_type= sil_ret_type

infer/src/textual/TextualTransform.ml

@@ -344,6 +344,12 @@ module TransformClosures = struct
 
   let closure_call_procdecl loc typename (closure : ProcDesc.t) nb_captured : ProcDecl.t =
     let procdecl = closure.procdecl in
+    let attributes =
+      (* in Python, we transfert the 'args' attributes from the 'closure' proc to the generated 'call' proc *)
+      List.find_map procdecl.attributes ~f:Textual.Attr.find_python_args
+      |> Option.map ~f:Textual.Attr.mk_python_args
+      |> Option.to_list
+    in
     let unresolved_qualified_name = closure_call_qualified_procname loc in
     let qualified_name = {unresolved_qualified_name with enclosing_class= Enclosing typename} in
     let this_typ = Typ.mk_without_attributes (Ptr (Struct typename)) in
@@ -352,7 +358,7 @@ module TransformClosures = struct
           this_typ :: List.drop formals nb_captured )
     in
     let result_type = procdecl.result_type in
-    {qualified_name; formals_types; result_type; attributes= []}
+    {qualified_name; formals_types; result_type; attributes}
 
 
   let closure_call_procdesc loc typename state (closure : ProcDesc.t) fields params :

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

@@ -1,2 +1,4 @@
 level0.py, level0::__module_body__, 15, TAINT_ERROR, no_bucket, ERROR, [in call to `closure:level0:1.call`,source of the taint here: value returned from `level0::taint_source` with kind `Simple`,return from call to `closure:level0:1.call`,when calling `closure:level0:0.call` here,flows to this sink: value passed as argument `#1` to `level0::taint_sink` with kind `Simple`], source: level0::taint_source, sink: level0::taint_sink, tainted expression: UNKNOWN
 level1.py, level1::basic_flow_bad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `closure:level1:0.call`,source of the taint here: value returned from `level1::taint_source` with kind `Simple`,return from call to `closure:level1:0.call`,when calling `closure:level1:1.call` here,flows to this sink: value passed as argument `#1` to `level1::taint_sink` with kind `Simple`], source: level1::taint_source, sink: level1::taint_sink, tainted expression: UNKNOWN
+level1.py, level1::call_fst_bad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `closure:level1:0.call`,source of the taint here: value returned from `level1::taint_source` with kind `Simple`,return from call to `closure:level1:0.call`,when calling `closure:level1:1.call` here,flows to this sink: value passed as argument `#1` to `level1::taint_sink` with kind `Simple`], source: level1::taint_source, sink: level1::taint_sink, tainted expression: UNKNOWN
+level1.py, level1::call_sink_fst_arg_bad, 1, TAINT_ERROR, no_bucket, ERROR, [in call to `closure:level1:0.call`,source of the taint here: value returned from `level1::taint_source` with kind `Simple`,return from call to `closure:level1:0.call`,when calling `closure:level1:7.call` here,when calling `level1::sink_fst_arg` here,when calling `closure:level1:1.call` here,flows to this sink: value passed as argument `#1` to `level1::taint_sink` with kind `Simple`], source: level1::taint_source, sink: level1::taint_sink, tainted expression: closure:level1:0.call()

infer/tests/codetoanalyze/python/pulse/level1.py

@@ -20,7 +20,7 @@ def basic_flow_ok(untainted: int) -> None:
 def fst(x: int, y: int) -> int:
     return x
 
-def FN_call_fst_bad(untainted) -> None:
+def call_fst_bad(untainted) -> None:
     arg = fst(taint_source(), untainted)
     taint_sink(arg)
 
@@ -31,16 +31,34 @@ def call_fst_ok(untainted) -> None:
 def sink_fst_arg(x, y) -> None:
     taint_sink(x)
 
-def FN_call_sink_fst_arg_bad(untainted) -> None:
+def call_sink_fst_arg_bad(untainted) -> None:
     sink_fst_arg(taint_source(), untainted)
 
 def call_sink_fst_arg_ok(untainted) -> None:
     sink_fst_arg(untainted, taint_source())
 
+def FN_call_taint_sink_on_global_bad1():
+    global g
+    taint_sink(g)
+
+def call_taint_sink_on_global_ok():
+    global g
+    taint_sink(g)
+
+def FN_call_taint_sink_on_global_bad2():
+    global g
+    g = taint_source()
+    taint_sink(g)
+
 # we need to call these functions in order to activate specialization
 basic_flow_bad()
 basic_flow_ok(0)
-FN_call_fst_bad(0)
+call_fst_bad(0)
 call_fst_ok(0)
-FN_call_sink_fst_arg_bad(0)
+call_sink_fst_arg_bad(0)
 call_sink_fst_arg_ok(0)
+g = taint_source()
+FN_call_taint_sink_on_global_bad1()
+g = 0
+call_taint_sink_on_global_ok()
+FN_call_taint_sink_on_global_bad2()