[InferPython] Adding dicts to py_subscript model

Summary:
Dict key access will now work for some cases when keys are constant strings. If given key is not a constant string, we return a fresh val (as was done before for any dict key access).

Example:
```
d = {"ABC": 1, "DEF": asyncio.sleep(1)}
# returns corresponding awaitable val
return d["DEF"]
```

Reviewed By: davidpichardie

Differential Revision:
D69542133

Privacy Context Container: L1208441

fbshipit-source-id: e3e3988e6399d42c82e54dd3c87d7bb2d84cb138

infer/src/pulse/PulseModelsPython.ml

@@ -318,13 +318,27 @@ module Dict = struct
 
 
   (* beware: key is expected to be a constant string! *)
-  let get dict key : DSL.aval DSL.model_monad =
+  let get_exn dict key : DSL.aval DSL.model_monad =
     let open DSL.Syntax in
     let* key = as_constant_string_exn key in
     let* load_res = get_str_key ~propagate_static_type:true dict key in
     ret load_res
 
 
+  (* similar to get_exn but doesn't throw error if key is not constant string *)
+  let get dict key : DSL.aval DSL.model_monad =
+    let open DSL.Syntax in
+    let* key = as_constant_string key in
+    let* res =
+      match key with
+      | None ->
+          fresh ()
+      | Some key ->
+          get_str_key ~propagate_static_type:true dict key
+    in
+    ret res
+
+
   let set_str_key dict key value : unit DSL.model_monad =
     let open DSL.Syntax in
     let field = Fieldname.make dict_tname key in
@@ -626,13 +640,13 @@ let call_method name obj arg_names args : model =
         match opt_special_call with
         | None ->
             L.d_printfln "calling method %s on module object %s" str_name module_name ;
-            let* closure = Dict.get obj name in
+            let* closure = Dict.get_exn obj name in
             call_dsl ~closure ~arg_names ~args
         | Some res ->
             L.d_printfln "catching special call %s on module object %s" str_name module_name ;
             ret res )
     | _ ->
-        let* closure = Dict.get obj name in
+        let* closure = Dict.get_exn obj name in
         (* TODO: for OO method, gives self argument *)
         call_dsl ~closure ~arg_names ~args
   in
@@ -833,7 +847,7 @@ let load_fast name locals : model =
   let open DSL.Syntax in
   start_model
   @@ fun () ->
-  let* value = Dict.get locals name in
+  let* value = Dict.get_exn locals name in
   assign_ret value
 
 
@@ -872,7 +886,7 @@ let load_name name locals _globals : model =
   let open DSL.Syntax in
   start_model
   @@ fun () ->
-  let* value = Dict.get locals name in
+  let* value = Dict.get_exn locals name in
   (* TODO: decide what we do if the binding is missing in locals *)
   assign_ret value
 
@@ -1015,7 +1029,8 @@ let subscript seq idx : model =
   @@ fun () ->
   let* res =
     dynamic_dispatch seq
-      ~cases:[(tuple_tname, fun () -> Tuple.get seq idx)] (* TODO: other sequence types *)
+      ~cases:[(tuple_tname, fun () -> Tuple.get seq idx); (dict_tname, fun () -> Dict.get seq idx)]
+        (* TODO: other sequence types *)
       ~default:(fun () -> fresh ())
   in
   assign_ret res

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

@@ -11,6 +11,16 @@ def fp_int_key_access_ok():
     return d[2]
 
 
-def fp_str_key_access_ok():
+def str_key_access_ok():
     d = {"ABC": 1, "DEF": asyncio.sleep(1)}
     return d["DEF"]
+
+
+def int_key_access_bad():
+    d = {123: 1, 456: asyncio.sleep(1)}
+    return d[123]
+
+
+async def str_key_access_bad():
+    d = {"ABC": asyncio.sleep(), 123: 456, "DEF": await asyncio.sleep(1)}
+    return d["DEF"]

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

@@ -1,5 +1,6 @@
 async_dict.py, async_dict.fp_int_key_access_ok, 2, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]
-async_dict.py, async_dict.fp_str_key_access_ok, 2, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]
+async_dict.py, async_dict.int_key_access_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_dict.py, async_dict.str_key_access_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_global.py, async_global.__module_body__, 24, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,parameter `globals` of async_global.__module_body__,assigned,when calling `Closure[async_global.set_unwaited_global].call` here,parameter `__this` of Closure[async_global.set_unwaited_global].call,when calling `async_global.set_unwaited_global` here,allocated by async call here,awaitable becomes unreachable here]
 async_import_simple.py, async_import_simple.with_import_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_import_simple.py, async_import_simple.with_from_import_bad, 1, PULSE_UNAWAITED_AWAITABLE, no_bucket, ERROR, [allocation part of the trace starts here,allocated by async call here,awaitable becomes unreachable here]