[inferpython] basic import

Summary: we treat each import as a call to the corresponding module's body. We left as future work the modeling of "initialized only once" mechanism.

Reviewed By: ngorogiannis

Differential Revision:
D65651833

Privacy Context Container: L1208441

fbshipit-source-id: 33bea3b32dcb19d2def0a6d4264834f1cfb34cb9

infer/src/pulse/PulseModelsDSL.ml

@@ -824,17 +824,32 @@ module Syntax = struct
     | 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 call lang proc_name named_args =
     let mixed_type_name =
       match (lang : Textual.Lang.t) with
       | Hack ->
           TextualSil.hack_mixed_type_name
       | Python ->
           TextualSil.python_mixed_type_name
       | Java ->
-          L.die InternalError "apply_closure is not supported on Java"
+          L.die InternalError "DSL.call not supported on Java"
     in
     let typ = Typ.mk_ptr (Typ.mk_struct mixed_type_name) in
+    let ret_id = Ident.create_none () in
+    let call_args =
+      List.map named_args ~f:(fun (str, arg) : ValueOrigin.t ProcnameDispatcher.Call.FuncArg.t ->
+          let pvar = Pvar.mk (Mangled.from_string str) proc_name in
+          let exp = Exp.Lvar pvar in
+          let arg_payload = ValueOrigin.OnStack {var= Var.of_pvar pvar; addr_hist= arg} in
+          {exp; typ; arg_payload} )
+    in
+    let* () = dispatch_call (ret_id, typ) proc_name call_args in
+    read (Exp.Var ret_id)
+
+
+  let python_call = call Python
+
+  let apply_closure lang (closure : aval) unresolved_pname closure_args : aval model_monad =
     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}} -> (
@@ -847,7 +862,6 @@ module Syntax = struct
             ret unknown_res
         | 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 ->
@@ -859,17 +873,10 @@ module Syntax = struct
                          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 =
-                    Pvar.mk (Mangled.from_string (Printf.sprintf "CLOSURE_ARG%d" i)) resolved_pname
-                  in
-                  let exp = Exp.Lvar pvar in
-                  let arg_payload = ValueOrigin.OnStack {var= Var.of_pvar pvar; addr_hist= arg} in
-                  {exp; typ; arg_payload} )
+            let named_args =
+              List.mapi args ~f:(fun i arg -> (Printf.sprintf "CLOSURE_ARG%d" i, arg))
             in
-            let* () = dispatch_call (ret_id, typ) resolved_pname call_args in
-            let* res = read (Exp.Var ret_id) in
+            let* res = call lang resolved_pname named_args in
             L.d_printfln "[ocaml model] Closure return value is %a." AbstractValue.pp (fst res) ;
             ret res )
     | _ ->

infer/src/pulse/PulseModelsDSL.mli

@@ -80,6 +80,8 @@ module Syntax : sig
     -> ValueOrigin.t ProcnameDispatcher.Call.FuncArg.t list
     -> unit model_monad
 
+  val python_call : Procname.t -> (string * 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

infer/src/pulse/PulseModelsPython.ml

@@ -88,19 +88,60 @@ let build_tuple args : model =
   assign_ret tuple
 
 
-let call closure _arg_names args : model =
+let call_dsl closure _arg_names args : DSL.aval DSL.model_monad =
   (* TODO: take into account named args *)
   let open DSL.Syntax in
-  start_model
-  @@ fun () ->
   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
+  apply_python_closure closure gen_closure_args
+
+
+let call closure arg_names args : model =
+  (* TODO: take into account named args *)
+  let open DSL.Syntax in
+  start_model
+  @@ fun () ->
+  let* value = call_dsl closure arg_names args in
   assign_ret value
 
 
+let call_method name obj arg_names args : model =
+  (* TODO: take into account named args *)
+  let open DSL.Syntax in
+  start_model
+  @@ fun () ->
+  let* closure = Dict.get obj name in
+  (* TODO: for OO method, gives self argument *)
+  let* value = call_dsl closure arg_names args in
+  assign_ret value
+
+
+let import_from name module_ : model =
+  let open DSL.Syntax in
+  start_model
+  @@ fun () ->
+  let* res = Dict.get module_ name in
+  assign_ret res
+
+
+let import_name name _fromlist _level : model =
+  let open DSL.Syntax in
+  start_model
+  @@ fun () ->
+  let* opt_str = as_constant_string name in
+  let function_name =
+    Option.value_or_thunk opt_str ~default:(fun () ->
+        L.die InternalError "frontend should always give a string here" )
+  in
+  let proc_name = Procname.make_python ~class_name:None ~function_name in
+  let* globals = Dict.make [] [] in
+  (* TODO: call it only once! *)
+  let* _ = python_call proc_name [("globals", globals)] in
+  assign_ret globals
+
+
 let load_fast name locals : model =
   let open DSL.Syntax in
   start_model
@@ -198,7 +239,10 @@ let matchers : matcher list =
   let open ProcnameDispatcher.Call in
   let arg = capt_arg_payload in
   [ -"$builtins" &:: "py_call" <>$ arg $+ arg $+++$--> call
+  ; -"$builtins" &:: "py_call_method" <>$ arg $+ arg $+ arg $+++$--> call_method
   ; -"$builtins" &:: "py_build_tuple" &::.*+++> build_tuple
+  ; -"$builtins" &:: "py_import_from" <>$ arg $+ arg $--> import_from
+  ; -"$builtins" &:: "py_import_name" <>$ arg $+ arg $+ arg $--> import_name
   ; -"$builtins" &:: "py_make_dictionary" &::.*+++> make_dictionary
   ; -"$builtins" &:: "py_make_function" <>$ arg $+ arg $+ arg $+ arg $+ arg $--> make_function
   ; -"$builtins" &:: "py_make_int" <>$ arg $--> make_int

infer/src/python/PyIR2Textual.ml

@@ -31,6 +31,8 @@ module Typ = struct
   let value = Textual.(Typ.Ptr (Typ.Struct (TypeName.of_string "PyObject")))
 end
 
+let str_module_body name = F.asprintf "%a.__module_body__" Ident.pp name
+
 type proc_kind = ModuleBody of Ident.t | RegularFunction of QualName.t
 
 let is_module_body = function ModuleBody _ -> true | _ -> false
@@ -39,7 +41,7 @@ let mk_qualified_proc_name ?loc kind =
   let qual_name_str =
     match kind with
     | ModuleBody name ->
-        F.asprintf "%a.__module_body__" Ident.pp name
+        str_module_body name
     | RegularFunction qual_name ->
         F.asprintf "%a" QualName.pp qual_name
   in
@@ -57,7 +59,7 @@ let mk_procdecl_attributes {CodeInfo.co_argcount; co_varnames} =
 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 []
+    if is_module_body kind then Some [Textual.Typ.mk_without_attributes Typ.globals]
     else
       Some
         [Textual.Typ.mk_without_attributes Typ.globals; Textual.Typ.mk_without_attributes Typ.locals]
@@ -126,7 +128,10 @@ let rec of_exp exp : Textual.Exp.t =
   | LoadClassDeref {name; slot= _} ->
       call_builtin "py_load_class_deref" [exp_of_ident_str name] (* TODO: more arg needed *)
   | ImportName {name; fromlist; level} ->
-      call_builtin "py_import_name" [exp_of_ident_str name; of_exp fromlist; of_exp level]
+      let str =
+        str_module_body name |> Textual.ProcName.of_string |> F.asprintf "%a" Textual.ProcName.pp
+      in
+      call_builtin "py_import_name" [Textual.Exp.Const (Str str); of_exp fromlist; of_exp level]
   | ImportFrom {name; exp} ->
       call_builtin "py_import_from" [exp_of_ident_str name; of_exp exp]
   | Temp ssa ->
@@ -431,12 +436,10 @@ let of_node is_module_body entry {Node.name; first_loc; last_loc; ssa_parameters
       let loc = label_loc in
       Textual.(
         Instr.Store
-          {exp1= Lvar Parameter.globals; exp2= call_builtin "py_make_dictionary" []; typ= None; loc}
-        :: Instr.Store
-             { exp1= Lvar Parameter.locals
-             ; exp2= Load {exp= Lvar Parameter.globals; typ= None}
-             ; typ= None
-             ; loc }
+          { exp1= Lvar Parameter.locals
+          ; exp2= Load {exp= Lvar Parameter.globals; typ= None}
+          ; typ= None
+          ; loc }
         :: instrs )
     else instrs
   in
@@ -454,11 +457,11 @@ let mk_procdesc proc_kind {CFG.entry; nodes; code_info= {co_firstlineno} as code
     List.map nodes_bindings ~f:(fun (_node_name, node) -> of_node is_module_body entry node)
   in
   let start = mk_node_name entry in
-  let params = if is_module_body then [] else [Parameter.globals; Parameter.locals] in
+  let params =
+    if is_module_body then [Parameter.globals] else [Parameter.globals; Parameter.locals]
+  in
   let locals =
-    if is_module_body then
-      [ (Parameter.globals, Textual.Typ.mk_without_attributes Typ.globals)
-      ; (Parameter.locals, Textual.Typ.mk_without_attributes Typ.locals) ]
+    if is_module_body then [(Parameter.locals, Textual.Typ.mk_without_attributes Typ.locals)]
     else []
   in
   let exit_loc =

infer/src/python/unit/PyIR2TextualTest.ml

@@ -59,10 +59,9 @@ def g():
     TRANSFORMATION PyIR -> Textual
     .source_language = "python"
 
-    define dummy::__module_body__() : *PyObject {
-      local globals: *PyGlobals, locals: *PyLocals
+    define dummy::__module_body__(globals: *PyGlobals) : *PyObject {
+      local locals: *PyLocals
       #b0:
-          store &globals <- $builtins.py_make_dictionary()
           store &locals <- globals
           _ = $builtins.py_store_name("x", locals, globals, $builtins.py_make_int(0))
           n0 = $builtins.py_make_function(fun (locals) -> dummy::f(globals, locals), $builtins.py_make_none(), $builtins.py_make_none(), $builtins.py_make_none(), $builtins.py_make_none())
@@ -120,10 +119,9 @@ def g():
     TYPE INFERENCE
     .source_language = "python"
 
-    define dummy::__module_body__() : *PyObject {
-      local globals: *PyGlobals, locals: *PyLocals
+    define dummy::__module_body__(globals: *PyGlobals) : *PyObject {
+      local locals: *PyLocals
       #b0:
-          store &globals <- $builtins.py_make_dictionary():*PyObject
           store &locals <- [&globals:*PyGlobals]:*PyGlobals
           _ = $builtins.py_store_name("x", [&locals:*PyLocals], [&globals:*PyGlobals], $builtins.py_make_int(0))
           n0 = $builtins.py_make_function(fun (locals) -> dummy::f([&globals:*PyGlobals], locals), $builtins.py_make_none(), $builtins.py_make_none(), $builtins.py_make_none(), $builtins.py_make_none())
@@ -205,41 +203,39 @@ def g():
 
     }
 
-    define dummy::__module_body__() : *PyObject {
-      local globals: *PyGlobals, locals: *PyLocals
+    define dummy::__module_body__(globals: *PyGlobals) : *PyObject {
+      local locals: *PyLocals
       #b0:
-          n2 = $builtins.py_make_dictionary()
-          store &globals <- n2:*PyObject
-          n3:*PyGlobals = load &globals
-          store &locals <- n3:*PyGlobals
-          n4:*PyLocals = load &locals
-          n5:*PyGlobals = load &globals
-          n6 = $builtins.py_make_int(0)
-          n7 = $builtins.py_store_name("x", n4, n5, n6)
-          n8:*PyGlobals = load &globals
-          n9 = __sil_allocate(<closure:dummy:0>)
-          store n9.?.globals <- n8:*PyGlobals
+          n2:*PyGlobals = load &globals
+          store &locals <- n2:*PyGlobals
+          n3:*PyLocals = load &locals
+          n4:*PyGlobals = load &globals
+          n5 = $builtins.py_make_int(0)
+          n6 = $builtins.py_store_name("x", n3, n4, n5)
+          n7:*PyGlobals = load &globals
+          n8 = __sil_allocate(<closure:dummy:0>)
+          store n8.?.globals <- n7:*PyGlobals
+          n10 = $builtins.py_make_none()
           n11 = $builtins.py_make_none()
           n12 = $builtins.py_make_none()
           n13 = $builtins.py_make_none()
-          n14 = $builtins.py_make_none()
-          n0 = $builtins.py_make_function(n9, n11, n12, n13, n14)
-          n15:*PyLocals = load &locals
-          n16:*PyGlobals = load &globals
-          n17 = $builtins.py_store_name("f", n15, n16, n0)
-          n18:*PyGlobals = load &globals
-          n19 = __sil_allocate(<closure:dummy:1>)
-          store n19.?.globals <- n18:*PyGlobals
+          n0 = $builtins.py_make_function(n8, n10, n11, n12, n13)
+          n14:*PyLocals = load &locals
+          n15:*PyGlobals = load &globals
+          n16 = $builtins.py_store_name("f", n14, n15, n0)
+          n17:*PyGlobals = load &globals
+          n18 = __sil_allocate(<closure:dummy:1>)
+          store n18.?.globals <- n17:*PyGlobals
+          n20 = $builtins.py_make_none()
           n21 = $builtins.py_make_none()
           n22 = $builtins.py_make_none()
           n23 = $builtins.py_make_none()
-          n24 = $builtins.py_make_none()
-          n1 = $builtins.py_make_function(n19, n21, n22, n23, n24)
-          n25:*PyLocals = load &locals
-          n26:*PyGlobals = load &globals
-          n27 = $builtins.py_store_name("g", n25, n26, n1)
-          n28 = $builtins.py_make_none()
-          ret n28
+          n1 = $builtins.py_make_function(n18, n20, n21, n22, n23)
+          n24:*PyLocals = load &locals
+          n25:*PyGlobals = load &globals
+          n26 = $builtins.py_store_name("g", n24, n25, n1)
+          n27 = $builtins.py_make_none()
+          ret n27
 
     }
 

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

@@ -5,3 +5,4 @@ level1.py, level1::call_fst_bad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `
 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()
 level1.py, level1::call_taint_sink_on_global_bad2, 3, 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::__module_body__, 60, TAINT_ERROR, no_bucket, ERROR, [in call to `closure:level1:2.call`,in call to `level1::basic_flow_bad`,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`,return from call to `level1::basic_flow_bad`,return from call to `closure:level1:2.call`,when calling `closure:level1:10.call` here,when calling `level1::call_taint_sink_on_global_bad1` 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: globals->call_taint_sink_on_global_bad1->globals->g
+simple-import.py, simple-import::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

infer/tests/codetoanalyze/python/pulse/simple-import.py

@@ -4,11 +4,14 @@
 # LICENSE file in the root directory of this source tree.
 
 import level1
-from level1 import taintSink
+from level1 import taint_sink
 
-def basicFlowBad() -> None:
-    tainted = level1.taintSource()
-    taintSink(tainted)
+def basic_flow_bad() -> None:
+    tainted = level1.taint_source()
+    taint_sink(tainted)
 
-def basicFlowOk(untainted: int) -> None:
-    level1.taintSink(untainted)
+def basic_flow_ok(untainted: int) -> None:
+    level1.taint_sink(untainted)
+
+basic_flow_bad()
+basic_flow_ok(0)