Tweak default implementation of array_cow_set to await discarded value

Reviewed By: davidpichardie

Differential Revision: D52017880

fbshipit-source-id: ebd7d5d678619256cabf185fcd83dc9498638b43

Author: Nick Benton

infer/src/pulse/PulseModelsDSL.ml

@@ -81,6 +81,11 @@ module Syntax = struct
     Option.value_map o ~default:(ret ()) ~f
 
 
+  let ignore (m : 'a model_monad) : unit model_monad =
+    let* _ = m in
+    ret ()
+
+
   let get_data : model_data model_monad = fun data astate -> ret data data astate
 
   let ok x = Ok x

infer/src/pulse/PulseModelsDSL.mli

@@ -34,6 +34,8 @@ module Syntax : sig
 
   val option_iter : 'a option -> f:('a -> unit model_monad) -> unit model_monad
 
+  val ignore : 'a model_monad -> unit model_monad
+
   val assign_ret : aval -> unit model_monad
   (** assign the value to the return variable of the current function *)
 

infer/src/pulse/PulseModelsHack.ml

@@ -660,6 +660,9 @@ let hack_array_cow_set this args : model =
   let this = payload_of_arg this in
   let args = payloads_of_args args in
   let default () =
+    let* () =
+      option_iter (List.last args) ~f:(fun value_written -> ignore (await_hack_value value_written))
+    in
     let* fresh = mk_fresh ~model_desc:"hack_array_cow_set" () in
     assign_ret fresh
   in

infer/tests/codetoanalyze/hack/pulse/asyncvec.hack

@@ -32,3 +32,8 @@ async function vecupdateFN(): Awaitable<void> {
   await $v[1];
   await $v[0];
 }
+
+async function nodynamictypeOK(mixed $c): Awaitable<void> {
+  $c[0] = genInt3();
+  await ($c[0]);
+}