[inferpython] new strategy to pass the globals dictionnary into funct…

…ions

Summary: The way we currently wire globals into each function generate a lot of aliases. It stress specialization too much and reveals a current bug. I will try to fix the specialization bug later but this new strategy seems lighter anyway.

Reviewed By: ngorogiannis

Differential Revision:
D65752451

Privacy Context Container: L1208441

fbshipit-source-id: 9fc950a57a4d346c0f6a11c87b4d4afc683d207d

infer/man/man1/infer-analyze.txt

@@ -1068,6 +1068,14 @@ PULSE CHECKER OPTIONS
        --pulse-widen-threshold int
            Stop exploring new paths after int loop iterations
 
+       --python-globals { own-by-closures | own-by-module }
+           Specify the strategy to wire globals dictionnaire into each
+           function
+                - own-by-closures: each closure captured the global
+           dictionary
+           - own-by-module: each function is given the global dictionary as
+           argument (not referenced in the heap to avoid aliases)
+
 RACERD CHECKER OPTIONS
        --racerd-always-report-java
            Activates: Every Java class analysed is treated as if it were

infer/man/man1/infer-full.txt

@@ -1881,6 +1881,15 @@ OPTIONS
            file2.py but not with --pyc-file.
            See also infer-capture(1).
 
+       --python-globals { own-by-closures | own-by-module }
+           Specify the strategy to wire globals dictionnaire into each
+           function
+                - own-by-closures: each closure captured the global
+           dictionary
+           - own-by-module: each function is given the global dictionary as
+           argument (not referenced in the heap to avoid aliases)
+           See also infer-analyze(1).
+
        --qualified-cpp-name-block-list +string
            Skip analyzing the procedures under the qualified cpp type name.
            See also infer-analyze(1).

infer/man/man1/infer.txt

@@ -1881,6 +1881,15 @@ OPTIONS
            file2.py but not with --pyc-file.
            See also infer-capture(1).
 
+       --python-globals { own-by-closures | own-by-module }
+           Specify the strategy to wire globals dictionnaire into each
+           function
+                - own-by-closures: each closure captured the global
+           dictionary
+           - own-by-module: each function is given the global dictionary as
+           argument (not referenced in the heap to avoid aliases)
+           See also infer-analyze(1).
+
        --qualified-cpp-name-block-list +string
            Skip analyzing the procedures under the qualified cpp type name.
            See also infer-analyze(1).

infer/src/base/Config.ml

@@ -54,6 +54,10 @@ let string_of_scheduler scheduler =
   List.Assoc.find_exn (List.Assoc.inverse scheduler_symbols) ~equal:equal_scheduler scheduler
 
 
+type python_globals = OwnByClosures | OwnByModule [@@deriving equal]
+
+let python_globals_symbols = [("own-by-closures", OwnByClosures); ("own-by-module", OwnByModule)]
+
 type pulse_taint_config =
   { sources: Pulse_config_t.matchers
   ; sanitizers: Pulse_config_t.matchers
@@ -2986,6 +2990,16 @@ and python_skip_db =
   CLOpt.mk_bool ~long:"python-skip-db" ~default:false "Skip the DB writing during Python capture"
 
 
+and python_globals =
+  CLOpt.mk_symbol ~long:"python-globals" ~default:OwnByModule ~eq:equal_python_globals
+    ~in_help:InferCommand.[(Analyze, manual_pulse)]
+    ~symbols:python_globals_symbols
+    "Specify the strategy to wire globals dictionnaire into each function\n\
+    \     - own-by-closures: each closure captured the global dictionary\n\
+     - own-by-module: each function is given the global dictionary as argument (not referenced in \
+     the heap to avoid aliases)"
+
+
 and qualified_cpp_name_block_list =
   CLOpt.mk_string_list ~long:"qualified-cpp-name-block-list" ~meta:"string"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -4687,6 +4701,8 @@ and python_files_index = !python_files_index
 
 and python_skip_db = !python_skip_db
 
+and python_globals = !python_globals
+
 and qualified_cpp_name_block_list = RevList.to_list !qualified_cpp_name_block_list
 
 and quiet = !quiet

infer/src/base/Config.mli

@@ -35,6 +35,8 @@ type scheduler = File | Restart | SyntacticCallGraph [@@deriving equal]
 
 val string_of_scheduler : scheduler -> string
 
+type python_globals = OwnByClosures | OwnByModule [@@deriving equal]
+
 val build_system_of_exe_name : string -> build_system
 
 val string_of_build_system : build_system -> string
@@ -751,6 +753,8 @@ val python_files_index : string option
 
 val python_skip_db : bool
 
+val python_globals : python_globals
+
 val qualified_cpp_name_block_list : string list
 
 val quiet : bool

infer/src/pulse/PulseModelsPython.ml

@@ -88,22 +88,26 @@ let build_tuple args : model =
   assign_ret tuple
 
 
-let call_dsl closure _arg_names args : DSL.aval DSL.model_monad =
+let call_dsl ~closure ~globals ~arg_names:_ ~args : DSL.aval DSL.model_monad =
   (* TODO: take into account named args *)
   let open DSL.Syntax in
   let gen_closure_args {ProcAttributes.python_args} =
     let* locals = Dict.make python_args args in
-    ret [locals]
+    match Config.python_globals with
+    | OwnByClosures ->
+        ret [locals]
+    | OwnByModule ->
+        ret [globals; locals]
   in
   apply_python_closure closure gen_closure_args
 
 
-let call closure arg_names args : model =
+let call closure globals 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
+  let* value = call_dsl ~closure ~globals ~arg_names ~args in
   assign_ret value
 
 
@@ -114,7 +118,7 @@ let call_method name obj arg_names args : 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
+  let* value = call_dsl ~closure ~globals:obj ~arg_names ~args in
   assign_ret value
 
 
@@ -238,7 +242,7 @@ let subscript seq idx : model =
 let matchers : matcher list =
   let open ProcnameDispatcher.Call in
   let arg = capt_arg_payload in
-  [ -"$builtins" &:: "py_call" <>$ arg $+ arg $+++$--> call
+  [ -"$builtins" &:: "py_call" <>$ arg $+ 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

infer/src/python/PyIR2Textual.ml

@@ -170,7 +170,11 @@ let rec of_exp exp : Textual.Exp.t =
     ->
       let proc = mk_qualified_proc_name (RegularFunction qual_name) in
       let closure =
-        Textual.Exp.Closure {proc; captured= [exp_globals]; params= [Parameter.locals]}
+        match Config.python_globals with
+        | OwnByClosures ->
+            Textual.Exp.Closure {proc; captured= [exp_globals]; params= [Parameter.locals]}
+        | OwnByModule ->
+            Textual.Exp.Closure {proc; captured= []; params= [Parameter.globals; Parameter.locals]}
       in
       call_builtin "py_make_function"
         ( closure
@@ -371,10 +375,8 @@ let of_stmt loc stmt : Textual.Instr.t =
         ; exp= call_builtin "py_store_subscript" [of_exp lhs; of_exp index; of_exp rhs]
         ; loc }
   | Call {lhs; exp; args; arg_names} ->
-      Let
-        { id= Some (mk_ident lhs)
-        ; exp= call_builtin "py_call" (of_exp exp :: of_exp arg_names :: List.map ~f:of_exp args)
-        ; loc }
+      let args = of_exp exp :: exp_globals :: of_exp arg_names :: List.map ~f:of_exp args in
+      Let {id= Some (mk_ident lhs); exp= call_builtin "py_call" args; loc}
   | CallMethod {lhs; name; self_if_needed; args; arg_names} ->
       Let
         { id= Some (mk_ident lhs)