[inferpython] added model for comparison of singleton types

Reviewed By: davidpichardie

Differential Revision: D68491568

fbshipit-source-id: 4f557a0245ef34d9cbbed13fa7b4697121bf6b3b

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

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")
 

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

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)

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]