From 123e29ff13daa33d1316afaa6327588841af893b Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Thu, 23 Jan 2025 09:23:00 -0800 Subject: [PATCH] [inferpython] added model for comparison of singleton types Reviewed By: davidpichardie Differential Revision: D68491568 fbshipit-source-id: 4f557a0245ef34d9cbbed13fa7b4697121bf6b3b --- infer/src/pulse/PulseModelsPython.ml | 51 +++++++++++++++++-- infer/src/textual/TextualSil.ml | 2 +- infer/src/textual/TextualSil.mli | 4 +- .../python/pulse/async_typing.py | 28 +++++++++- .../codetoanalyze/python/pulse/issues.exp | 3 +- 5 files changed, 79 insertions(+), 9 deletions(-) diff --git a/infer/src/pulse/PulseModelsPython.ml b/infer/src/pulse/PulseModelsPython.ml index d305fe846f..20eadb5bbc 100644 --- a/infer/src/pulse/PulseModelsPython.ml +++ b/infer/src/pulse/PulseModelsPython.ml @@ -14,14 +14,16 @@ open PulseDomainInterface open PulseModelsImport module DSL = PulseModelsDSL +let bool_tname = TextualSil.python_bool_type_name + let dict_tname = TextualSil.python_dict_type_name let int_tname = TextualSil.python_int_type_name -let none_tname = TextualSil.python_none_type_name - let tuple_tname = TextualSil.python_tuple_type_name +let none_tname = Typ.PythonClass (PythonClassName.mk_reserved_builtin "None") + (* sys.stdlib_module_names *) let stdlib_modules : IString.Set.t = IString.Set.of_list @@ -753,6 +755,20 @@ let make_int arg : model = assign_ret res +let make_bool bool : DSL.aval DSL.model_monad = + let open DSL.Syntax in + let* bool = int (if bool then 1 else 0) in + let* () = and_dynamic_type_is bool (Typ.mk_struct bool_tname) in + ret bool + + +let make_random_bool () = + let open DSL.Syntax in + let* res = fresh () in + let* () = and_dynamic_type_is res (Typ.mk_struct bool_tname) in + ret res + + let make_none : model = let open DSL.Syntax in start_model @@ -817,6 +833,33 @@ let die_if_other_builtin (_, proc_name) _ = false +let is_builtin typename : bool = + match (typename : Typ.Name.t) with + | PythonClass pyclass -> + PythonClassName.is_reserved_builtin pyclass + | _ -> + false + + +let compare_eq arg1 arg2 : model = + let open DSL.Syntax in + start_model + @@ fun () -> + let* arg1_dynamic_type_data = get_dynamic_type ~ask_specialization:true arg1 in + let* arg2_dynamic_type_data = get_dynamic_type ~ask_specialization:true arg2 in + let* res = + match (arg1_dynamic_type_data, arg2_dynamic_type_data) with + | ( Some {Formula.typ= {desc= Tstruct arg1_type_name}} + , Some {Formula.typ= {desc= Tstruct arg2_type_name}} ) + when is_builtin arg1_type_name || is_builtin arg2_type_name -> + make_bool (Typ.Name.equal arg1_type_name arg2_type_name) + | _ -> + L.d_printfln "py_compare_eq: at least one unknown dynamic type: unknown result" ; + make_random_bool () + in + assign_ret res + + let matchers : matcher list = let open ProcnameDispatcher.Call in let arg = capt_arg_payload in @@ -854,12 +897,12 @@ let matchers : matcher list = ; -"$builtins" &:: "py_call_function_ex" &::.*+++> unknown ; -"$builtins" &:: "py_call_method" <>$ arg $+ arg $+ arg $+++$--> call_method ; -"$builtins" &:: "py_compare_bad" &::.*+++> unknown - ; -"$builtins" &:: "py_compare_eq" &::.*+++> unknown + ; -"$builtins" &:: "py_compare_eq" <>$ arg $+ arg $--> compare_eq ; -"$builtins" &:: "py_compare_exception" &::.*+++> unknown ; -"$builtins" &:: "py_compare_ge" &::.*+++> unknown ; -"$builtins" &:: "py_compare_gt" &::.*+++> unknown ; -"$builtins" &:: "py_compare_in" &::.*+++> unknown - ; -"$builtins" &:: "py_compare_is" &::.*+++> unknown + ; -"$builtins" &:: "py_compare_is" <>$ arg $+ arg $--> compare_eq ; -"$builtins" &:: "py_compare_is_not" &::.*+++> unknown ; -"$builtins" &:: "py_compare_le" &::.*+++> unknown ; -"$builtins" &:: "py_compare_lt" &::.*+++> unknown diff --git a/infer/src/textual/TextualSil.ml b/infer/src/textual/TextualSil.ml index 8eb146bc11..d14cbe9ff7 100644 --- a/infer/src/textual/TextualSil.ml +++ b/infer/src/textual/TextualSil.ml @@ -141,7 +141,7 @@ let python_dict_type_name = SilTyp.PythonClass (PythonClassName.make "PyDict") let python_int_type_name = SilTyp.PythonClass (PythonClassName.make "PyInt") -let python_none_type_name = SilTyp.PythonClass (PythonClassName.make "PyNone") +let python_bool_type_name = SilTyp.PythonClass (PythonClassName.make "PyBool") let python_tuple_type_name = SilTyp.PythonClass (PythonClassName.make "PyTuple") diff --git a/infer/src/textual/TextualSil.mli b/infer/src/textual/TextualSil.mli index 5bd9036ab7..8c87476975 100644 --- a/infer/src/textual/TextualSil.mli +++ b/infer/src/textual/TextualSil.mli @@ -55,12 +55,12 @@ val hack_builtins_type_name : Typ.name val hack_root_type_name : Typ.name +val python_bool_type_name : Typ.name + val python_dict_type_name : Typ.name val python_int_type_name : Typ.name -val python_none_type_name : Typ.name - val python_mixed_type_name : Typ.name val python_tuple_type_name : Typ.name diff --git a/infer/tests/codetoanalyze/python/pulse/async_typing.py b/infer/tests/codetoanalyze/python/pulse/async_typing.py index e8eb1eb506..62e3ba0e58 100644 --- a/infer/tests/codetoanalyze/python/pulse/async_typing.py +++ b/infer/tests/codetoanalyze/python/pulse/async_typing.py @@ -7,7 +7,7 @@ import types -async def fp_await_condition_typing_ok(): +async def await_condition_typing_ok(): x = int(5) if type(x) == int: await asyncio.sleep(1) @@ -50,3 +50,29 @@ def x(): await asyncio.sleep(1) else: asyncio.sleep(1) + + +async def await_condition_is_none_ok(): + x = None + if x is None: + await asyncio.sleep(1) + else: + asyncio.sleep(1) + + +async def fp_await_condition_val_equal_ok(): + x = Name("foo") + y = Name("foo") + if x == y: + await asyncio.sleep(1) + else: + asyncio.sleep(1) + + +async def await_condition_phys_equal_bad(): + x = Name("foo") + y = Name("foo") + if x is y: + await asyncio.sleep(1) + else: + asyncio.sleep(1) diff --git a/infer/tests/codetoanalyze/python/pulse/issues.exp b/infer/tests/codetoanalyze/python/pulse/issues.exp index 18cdf68172..9c27f53a31 100644 --- a/infer/tests/codetoanalyze/python/pulse/issues.exp +++ b/infer/tests/codetoanalyze/python/pulse/issues.exp @@ -23,8 +23,9 @@ async_level0.py, async_level0.tuple1_bad, 2, PULSE_UNAWAITED_AWAITABLE, no_bucke async_level0.py, async_level0.with_str_bad, 2, 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_fst_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_level1.py, async_level1.D::main, 1, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] -async_typing.py, async_typing.fp_await_condition_typing_ok, 5, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] async_typing.py, async_typing.await_condition_typing_bad, 4, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] async_typing.py, async_typing.await_condition_typing_with_arg_bad, 4, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] async_typing.py, async_typing.fp_await_condition_typing_user_defined_ok, 5, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] async_typing.py, async_typing.fp_await_condition_typing_fun_ok, 7, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] +async_typing.py, async_typing.fp_await_condition_val_equal_ok, 6, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here] +async_typing.py, async_typing.await_condition_phys_equal_bad, 6, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]