[inferpython][unawaited awaitables] asyncio.run awaits its argument

Summary:
a call like asyncio.run needs to be treated as a special case. We add a new
mechanism of unresolved module. This is still preliminary since it does not abduce very well. See the FN.

Reviewed By: martintrojer

Differential Revision:
D66293588

Privacy Context Container: L1208441

fbshipit-source-id: 31c2a94820a3b78e47cbacfb378751d2468b8470

infer/src/pulse/PulseModelsPython.ml

@@ -8,6 +8,7 @@
 open! IStd
 module F = Format
 module L = Logging
+module IRAttributes = Attributes
 open PulseBasicInterface
 open PulseDomainInterface
 open PulseModelsImport
@@ -21,6 +22,8 @@ let none_tname = TextualSil.python_none_type_name
 
 let tuple_tname = TextualSil.python_tuple_type_name
 
+let unresolved_module_tname = TextualSil.python_unresolved_module_type_name
+
 let sil_fieldname_from_string_value_exn type_name ((address, _) : DSL.aval) :
     Fieldname.t DSL.model_monad =
   let f astate =
@@ -81,6 +84,19 @@ module Tuple = struct
         load_access tuple (FieldAccess field)
 end
 
+module UnresolvedModule = struct
+  let make name : DSL.aval DSL.model_monad =
+    let open DSL.Syntax in
+    constructor unresolved_module_tname [("name", name)]
+
+
+  let name module_ : string option DSL.model_monad =
+    let open DSL.Syntax in
+    let field = Fieldname.make unresolved_module_tname "name" in
+    let* aval = load_access module_ (FieldAccess field) in
+    as_constant_string aval
+end
+
 let build_tuple args : model =
   let open DSL.Syntax in
   start_model
@@ -112,15 +128,49 @@ let call closure globals arg_names args : model =
   assign_ret value
 
 
+let await_awaitable arg : unit DSL.model_monad =
+  fst arg |> AddressAttributes.await_awaitable |> DSL.Syntax.exec_command
+
+
 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 ~globals:obj ~arg_names ~args in
-  assign_ret value
+  let* res =
+    dynamic_dispatch obj
+      ~cases:
+        [ ( unresolved_module_tname
+          , fun () ->
+              let* opt_module_name = UnresolvedModule.name obj in
+              let* opt_method_name = as_constant_string name in
+              let* special, res =
+                match (opt_module_name, opt_method_name, args) with
+                | Some "asyncio", Some "run", [arg] ->
+                    let* () = await_awaitable arg in
+                    let* res = fresh () in
+                    ret (true, res)
+                | Some "asyncio", Some "sleep", _ ->
+                    let* res = fresh () in
+                    let* () = allocation Attribute.Awaitable res in
+                    ret (true, res)
+                | _, _, _ ->
+                    let* res = fresh () in
+                    ret (false, res)
+              in
+              if special then
+                L.d_printfln "special method call (%a, %a)" (Pp.option F.pp_print_string)
+                  opt_module_name (Pp.option F.pp_print_string) opt_method_name
+              else
+                L.d_printfln "unknown special method call (%a, %a)" (Pp.option F.pp_print_string)
+                  opt_module_name (Pp.option F.pp_print_string) opt_method_name ;
+              ret res ) ]
+      ~default:(fun () ->
+        let* closure = Dict.get obj name in
+        (* TODO: for OO method, gives self argument *)
+        call_dsl ~closure ~globals:obj ~arg_names ~args )
+  in
+  assign_ret res
 
 
 let gen_start_coroutine : model =
@@ -132,7 +182,7 @@ let get_awaitable arg : model =
   let open DSL.Syntax in
   start_model
   @@ fun () ->
-  let* () = fst arg |> AddressAttributes.await_awaitable |> DSL.Syntax.exec_command in
+  let* () = await_awaitable arg in
   assign_ret arg
 
 
@@ -156,10 +206,15 @@ let import_name name _fromlist _level : model =
   let class_name = PythonClassName.make module_name in
   let function_name = "__module_body__" in
   let proc_name = Procname.make_python ~class_name:(Some class_name) ~function_name in
-  let* globals = Dict.make [] [] in
-  (* TODO: call it only once! *)
-  let* _ = python_call proc_name [("globals", globals)] in
-  assign_ret globals
+  if IRAttributes.load proc_name |> Option.is_none then (
+    L.d_printfln "module %s is unresolved" module_name ;
+    let* module_ = UnresolvedModule.make name in
+    assign_ret module_ )
+  else
+    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 =

infer/src/textual/TextualSil.ml

@@ -145,6 +145,10 @@ let python_none_type_name = SilTyp.PythonClass (PythonClassName.make "PyNone")
 
 let python_tuple_type_name = SilTyp.PythonClass (PythonClassName.make "PyTuple")
 
+let python_unresolved_module_type_name =
+  SilTyp.PythonClass (PythonClassName.make "PyUnresolvedModule")
+
+
 let mk_python_mixed_type_textual loc = Typ.Struct TypeName.{value= "PyObject"; loc}
 
 let default_return_type (lang : Lang.t option) loc =

infer/src/textual/TextualSil.mli

@@ -62,6 +62,8 @@ val python_mixed_type_name : Typ.name
 
 val python_tuple_type_name : Typ.name
 
+val python_unresolved_module_type_name : Typ.name
+
 val wildcard_sil_fieldname : Textual.Lang.t -> string -> Fieldname.t
 
 val textual_ext : string

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

@@ -10,6 +10,8 @@
 async def sleep(i):
     await asyncio.sleep(i)
 
+async def FN_sleep_bad(i):
+    asyncio.sleep(i)
 
 async def call_sleep_ok():
     await sleep(1)
@@ -51,6 +53,9 @@ async def call_sleep_with_branchs_bad2(b):
 b = random.choice([True, False])
 
 
+asyncio.run(FN_sleep_bad(random.random()))
+
+
 asyncio.run(call_sleep_ok())
 
 
@@ -65,5 +70,5 @@ async def call_sleep_with_branchs_bad2(b):
 
 asyncio.run(call_sleep_with_branchs_bad1(b))
 
-#FP
+
 asyncio.run(call_sleep_with_branchs_bad2(b))

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

@@ -1,7 +1,6 @@
 async_level0.py, async_level0.call_sleep_bad, 1, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]
 async_level0.py, async_level0.call_sleep_with_branchs_bad1, 3, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]
 async_level0.py, async_level0.call_sleep_with_branchs_bad2, 4, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]
-async_level0.py, async_level0.__module_body__, 68, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]
 taint_import_simple.py, taint_import_simple.basic_flow_bad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `closure:taint:1.call`,source of the taint here: value returned from `taint.source` with kind `Simple`,return from call to `closure:taint:1.call`,when calling `closure:taint:0.call` here,flows to this sink: value passed as argument `#1` to `taint.sink` with kind `Simple`], source: taint.source, sink: taint.sink, tainted expression: UNKNOWN
 taint_import_with_package.py, taint_import_with_package.__module_body__, 62, TAINT_ERROR, no_bucket, ERROR, [in call to `dir1::testmod.__module_body__`,in call to `closure:taint:1.call`,source of the taint here: value returned from `taint.source` with kind `Simple`,return from call to `closure:taint:1.call`,return from call to `dir1::testmod.__module_body__`,when calling `closure:taint_import_with_package:0.call` here,when calling `taint_import_with_package.use1_bad` here,when calling `closure:taint:0.call` here,flows to this sink: value passed as argument `#1` to `taint.sink` with kind `Simple`], source: taint.source, sink: taint.sink, tainted expression: globals->tainted_global1
 taint_import_with_package.py, taint_import_with_package.__module_body__, 68, TAINT_ERROR, no_bucket, ERROR, [in call to `dir2::testmod.__module_body__`,in call to `closure:taint:1.call`,source of the taint here: value returned from `taint.source` with kind `Simple`,return from call to `closure:taint:1.call`,return from call to `dir2::testmod.__module_body__`,when calling `closure:taint_import_with_package:2.call` here,when calling `taint_import_with_package.use2_bad` here,when calling `closure:taint:0.call` here,flows to this sink: value passed as argument `#1` to `taint.sink` with kind `Simple`], source: taint.source, sink: taint.sink, tainted expression: globals->tainted_global2