[inferpython] adding pulse-deep-release-model option

Summary: some lib provide "wait deeply" functions that await a collection (list, dict...) of arguments. We model them with a strong deep_wait behavior that recursively await all awaitable value reachable from the args. This diff refactor a bit the mechanism and provide a config regexp to choose which function will be given this behavior.

Reviewed By: Gabisampaio

Differential Revision:
D68942558

Privacy Context Container: L1208441

fbshipit-source-id: d65766cd47f0d2e28cc55bbc6a5ae4692e8b0131

infer/man/man1/infer-analyze.txt

@@ -788,6 +788,10 @@ PULSE CHECKER OPTIONS
        --pulse-model-cheap-copy-type-list +regex
            Regex of methods that should be cheap to copy in Pulse
 
+       --pulse-model-deep-release-pattern string
+           Regex of methods that should be modelled as deep release in Pulse
+           (i.e. await all unawaited values reachable from its arguments).
+
        --pulse-model-free-pattern string
            Regex of methods that should be modelled as wrappers to free(3) in
            Pulse. The pointer to be freed should be the first argument of the

infer/man/man1/infer-full.txt

@@ -1526,6 +1526,11 @@ OPTIONS
            Regex of methods that should be cheap to copy in Pulse
            See also infer-analyze(1).
 
+       --pulse-model-deep-release-pattern string
+           Regex of methods that should be modelled as deep release in Pulse
+           (i.e. await all unawaited values reachable from its arguments).
+           See also infer-analyze(1).
+
        --pulse-model-free-pattern string
            Regex of methods that should be modelled as wrappers to free(3) in
            Pulse. The pointer to be freed should be the first argument of the
@@ -3119,6 +3124,9 @@ INTERNAL OPTIONS
        --pulse-model-cheap-copy-type-reset
            Cancel the effect of --pulse-model-cheap-copy-type.
 
+       --pulse-model-deep-release-pattern-reset
+           Cancel the effect of --pulse-model-deep-release-pattern.
+
        --pulse-model-free-pattern-reset
            Cancel the effect of --pulse-model-free-pattern.
 

infer/man/man1/infer.txt

@@ -1526,6 +1526,11 @@ OPTIONS
            Regex of methods that should be cheap to copy in Pulse
            See also infer-analyze(1).
 
+       --pulse-model-deep-release-pattern string
+           Regex of methods that should be modelled as deep release in Pulse
+           (i.e. await all unawaited values reachable from its arguments).
+           See also infer-analyze(1).
+
        --pulse-model-free-pattern string
            Regex of methods that should be modelled as wrappers to free(3) in
            Pulse. The pointer to be freed should be the first argument of the

infer/src/base/Config.ml

@@ -2541,6 +2541,13 @@ and pulse_model_cheap_copy_type_list =
     "Regex of methods that should be cheap to copy in Pulse"
 
 
+and pulse_model_deep_release_pattern =
+  CLOpt.mk_string_opt ~long:"pulse-model-deep-release-pattern"
+    ~in_help:InferCommand.[(Analyze, manual_pulse)]
+    "Regex of methods that should be modelled as deep release in Pulse (i.e. await all unawaited \
+     values reachable from its arguments)."
+
+
 and pulse_model_free_pattern =
   CLOpt.mk_string_opt ~long:"pulse-model-free-pattern"
     ~in_help:InferCommand.[(Analyze, manual_pulse)]
@@ -4532,6 +4539,8 @@ and pulse_model_cheap_copy_type =
     ~pattern_list:pulse_model_cheap_copy_type_list
 
 
+and pulse_model_deep_release_pattern = Option.map ~f:Str.regexp !pulse_model_deep_release_pattern
+
 and pulse_model_free_pattern = Option.map ~f:Str.regexp !pulse_model_free_pattern
 
 and pulse_model_malloc_pattern = Option.map ~f:Str.regexp !pulse_model_malloc_pattern

infer/src/base/Config.mli

@@ -659,6 +659,8 @@ val pulse_model_alloc_pattern : Str.regexp option
 
 val pulse_model_cheap_copy_type : Str.regexp option
 
+val pulse_model_deep_release_pattern : Str.regexp option
+
 val pulse_model_free_pattern : Str.regexp option
 
 val pulse_model_malloc_pattern : Str.regexp option

infer/src/pulse/PulseModelsPython.ml

@@ -258,12 +258,6 @@ let as_constant_string_exn aval : string DSL.model_monad =
   ret str
 
 
-let is_release_model tname attr =
-  Option.exists Config.pulse_model_release_pattern ~f:(fun regexp ->
-      let str = Printf.sprintf "%s::%s" tname attr in
-      Str.string_match regexp str 0 )
-
-
 module Dict = struct
   let make keys args : DSL.aval DSL.model_monad =
     let open DSL.Syntax in
@@ -450,6 +444,42 @@ let make_int_internal arg : DSL.aval DSL.model_monad =
       ret res
 
 
+module LibModel = struct
+  let match_pattern ~pattern ~module_name ~name =
+    Option.exists pattern ~f:(fun regexp ->
+        let str = Printf.sprintf "%s::%s" module_name name in
+        Str.string_match regexp str 0 )
+
+
+  let is_release ~module_name ~name =
+    match_pattern ~pattern:Config.pulse_model_release_pattern ~module_name ~name
+
+
+  let is_deep_release ~module_name ~name =
+    match_pattern ~pattern:Config.pulse_model_deep_release_pattern ~module_name ~name
+
+
+  let gen_awaitable _args =
+    let open DSL.Syntax in
+    let* res = fresh () in
+    let* () = allocation Attribute.Awaitable res in
+    ret (Some res)
+
+
+  let deep_release args =
+    let open DSL.Syntax in
+    let* () = remove_allocation_attr_transitively args in
+    let* res = fresh () in
+    ret (Some res)
+
+
+  let release args =
+    let open DSL.Syntax in
+    let* () = list_iter args ~f:await_awaitable in
+    let* res = fresh () in
+    ret (Some res)
+end
+
 type pymodel =
   | PyLib of {module_name: string; name: string}
   | PyBuiltin of PythonClassName.builtin_closure
@@ -459,22 +489,16 @@ type pymodel =
 let modelled_python_call model args : DSL.aval option DSL.model_monad =
   let open DSL.Syntax in
   match (model, args) with
-  | PyLib {module_name= "asyncio"; name= "run"}, [arg] ->
-      let* () = await_awaitable arg in
-      let* res = fresh () in
-      ret (Some res)
-  | PyLib {module_name; name}, _ when is_release_model module_name name ->
-      let* () = list_iter args ~f:await_awaitable in
-      let* res = fresh () in
-      ret (Some res)
+  | PyLib {module_name= "asyncio"; name= "run"}, _ ->
+      LibModel.release args
+  | PyLib {module_name; name}, _ when LibModel.is_release ~module_name ~name ->
+      LibModel.release args
   | PyLib {module_name= "asyncio"; name= "gather"}, _ ->
-      let* res = fresh () in
-      let* () = remove_allocation_attr_transitively args in
-      ret (Some res)
+      LibModel.deep_release args
+  | PyLib {module_name; name}, _ when LibModel.is_deep_release ~module_name ~name ->
+      LibModel.deep_release args
   | PyLib {module_name= "asyncio"; name= "sleep"}, _ ->
-      let* res = fresh () in
-      let* () = allocation Attribute.Awaitable res in
-      ret (Some res)
+      LibModel.gen_awaitable args
   | PyBuiltin IntFun, [arg] ->
       let* res = make_int_internal arg in
       ret (Some res)
@@ -490,6 +514,15 @@ let modelled_python_call model args : DSL.aval option DSL.model_monad =
       ret None
 
 
+let try_catch_lib_model type_name args =
+  let open DSL.Syntax in
+  match Typ.Name.Python.split_module_attr type_name with
+  | Some (module_name, name) ->
+      modelled_python_call (PyLib {module_name; name}) args
+  | _ ->
+      ret None
+
+
 let call closure arg_names args : model =
   (* TODO: take into account named args *)
   let open DSL.Syntax in
@@ -509,13 +542,13 @@ let call closure arg_names args : model =
               (PythonClassName.to_string (BuiltinClosure builtin)) ;
             ret res )
     | Some {Formula.typ= {Typ.desc= Tstruct type_name}} -> (
-      (* we introspect the dyntype of the callee tyring to recognize a Pyton library model *)
-      match Typ.Name.Python.split_module_attr type_name with
-      | Some (module_name, name) -> (
-          let* opt_res = modelled_python_call (PyLib {module_name; name}) args in
-          match opt_res with Some res -> ret res | None -> call_dsl ~closure ~arg_names ~args )
-      | _ ->
-          call_dsl ~closure ~arg_names ~args )
+        let* opt_catched_lib_model_res = try_catch_lib_model type_name args in
+        match opt_catched_lib_model_res with
+        | Some res ->
+            L.d_printfln "catching reserved lib call using dynamic type %a" Typ.Name.pp type_name ;
+            ret res
+        | None ->
+            call_dsl ~closure ~arg_names ~args )
     | _ ->
         call_dsl ~closure ~arg_names ~args
   in
@@ -528,21 +561,31 @@ let call_function_ex closure tuple dict : model =
   start_model
   @@ fun () ->
   let* opt_dynamic_type_data = get_dynamic_type ~ask_specialization:true closure in
+  let args = [tuple; dict] in
   let* res =
     match opt_dynamic_type_data with
     | None -> (
         let* opt_static_type = get_static_type closure in
         match opt_static_type with
-        | Some (Typ.PythonClass (ModuleAttribute {module_name; attr_name= name})) -> (
-            let* opt_special_call =
-              modelled_python_call (PyLib {module_name; name}) [tuple; dict]
-            in
-            match opt_special_call with None -> fresh () | Some res -> ret res )
+        | Some (Typ.PythonClass (ModuleAttribute {module_name; attr_name= name}) as type_name) -> (
+            let* opt_special_call = modelled_python_call (PyLib {module_name; name}) args in
+            match opt_special_call with
+            | None ->
+                fresh ()
+            | Some res ->
+                L.d_printfln "catching reserved lib call using static type %a" Typ.Name.pp type_name ;
+                ret res )
         | _ ->
-            (* TODO: find situations where it happens and specific models are needed *)
+            fresh () )
+    | Some {Formula.typ= {Typ.desc= Tstruct type_name}} -> (
+        let* opt_catched_lib_model_res = try_catch_lib_model type_name args in
+        match opt_catched_lib_model_res with
+        | Some res ->
+            L.d_printfln "catching reserved lib call using dynamic type %a" Typ.Name.pp type_name ;
+            ret res
+        | None ->
             fresh () )
     | _ ->
-        (* TODO: model regular call using tuple and dict contents as arguments *)
         fresh ()
   in
   assign_ret res

infer/tests/codetoanalyze/python/pulse/.inferconfig

@@ -11,5 +11,6 @@
       "taint_target": ["ArgumentPositions", [1]]
     }
   ],
-  "pulse-model-release-pattern": "dir1::dir3::testmod::wait\\|not_captured::helper::not_captured_wait"
+  "pulse-model-release-pattern": "dir1::dir3::testmod::wait\\|not_captured::helper::not_captured_wait",
+  "pulse-model-deep-release-pattern": "dir1::dir3::testmod::deep_wait\\|not_captured::helper::not_captured_deep_wait"
 }

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

@@ -12,9 +12,13 @@
     await_it as await_it3,
     dont_await_it as dont_await_it3,
     C,
-    wait
+    wait,
+    deep_wait
+)
+from not_captured.helper import (
+    not_captured_wait,
+    not_captured_deep_wait
 )
-from not_captured.helper import not_captured_wait
 import dir1.dir4.testmod
 from dir2.testmod import (
     await_it as await_it2,
@@ -90,3 +94,34 @@ def use_pulse_model_release_option_ok():
 
 def use_pulse_model_release_option_not_captured_ok():
     not_captured_wait(asyncio.sleep())
+
+
+def use_pulse_model_deep_release_option_args_ok(l):
+    deep_wait(*[
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        ])
+
+
+def use_pulse_model_deep_release_option_not_captured_args_ok():
+    not_captured_deep_wait(*[
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        ])
+
+def use_pulse_model_deep_release_option_ok(l):
+    deep_wait(
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        )
+
+
+def use_pulse_model_deep_release_option_not_captured_ok():
+    not_captured_deep_wait(
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        asyncio.sleep(1),
+        )

infer/tests/codetoanalyze/python/pulse/dir1/dir3/testmod.py

@@ -19,6 +19,12 @@ async def async_fun():
 
 def wait(arg):
     """
-    This function is expected to be modeled as unknown by the analysis because of .inferconfig
+    This function is expected to be modeled as awaiting its argument because of .inferconfig
+    """
+    pass
+
+def deep_wait(*arg):
+    """
+    This function is expected to be modeled as awaiting deeply its arguments because of .inferconfig
     """
     pass