[pulse] monad, monads everywhere

Summary:
Add let*/+ syntax to `result` types to simplify all the applications of
`>>=`, `>>|` that are followed by a binding (eg `>>= fun x -> ...`) in
pulse.

Reviewed By: skcho

Differential Revision: D19940728

fbshipit-source-id: 4df159029

infer/src/istd/IResult.ml

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+module Let_syntax = struct
+  include Result.Monad_infix
+
+  let ( let+ ) x f = Result.map x ~f
+
+  let ( let* ) x f = Result.bind x ~f
+end

infer/src/istd/IResult.mli

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+module Let_syntax : sig
+  include module type of Result.Monad_infix
+
+  val ( let+ ) : ('ok, 'err) result -> ('ok -> 'okk) -> ('okk, 'err) result
+
+  val ( let* ) : ('ok, 'err) result -> ('ok -> ('okk, 'err) result) -> ('okk, 'err) result
+end

infer/src/pulse/Pulse.ml

@@ -4,10 +4,11 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  *)
+
 open! IStd
 module F = Format
 module L = Logging
-open Result.Monad_infix
+open IResult.Let_syntax
 open PulseBasicInterface
 
 let report summary diagnostic =
@@ -72,22 +73,21 @@ module PulseTransferFunctions = struct
   let exec_object_out_of_scope call_loc (pvar, typ) astate =
     let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
     (* invalidate [&x] *)
-    PulseOperations.eval call_loc (Exp.Lvar pvar) astate
-    >>= fun (astate, out_of_scope_base) ->
+    let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in
     PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
 
 
   let dispatch_call tenv summary ret call_exp actuals call_loc flags get_formals astate =
     (* evaluate all actuals *)
-    List.fold_result actuals ~init:(astate, [])
-      ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) ->
-        PulseOperations.eval call_loc actual_exp astate
-        >>| fun (astate, actual_evaled) ->
-        ( astate
-        , ProcnameDispatcher.Call.FuncArg.
-            {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ}
-          :: rev_func_args ) )
-    >>= fun (astate, rev_func_args) ->
+    let* astate, rev_func_args =
+      List.fold_result actuals ~init:(astate, [])
+        ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) ->
+          let+ astate, actual_evaled = PulseOperations.eval call_loc actual_exp astate in
+          ( astate
+          , ProcnameDispatcher.Call.FuncArg.
+              {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ}
+            :: rev_func_args ) )
+    in
     let func_args = List.rev rev_func_args in
     let model =
       match proc_name_of_call call_exp with
@@ -120,8 +120,7 @@ module PulseTransferFunctions = struct
     match get_out_of_scope_object call_exp actuals flags with
     | Some pvar_typ ->
         L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
-        posts
-        >>= fun posts ->
+        let* posts = posts in
         List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate)
         |> Result.all
     | None ->
@@ -134,22 +133,21 @@ module PulseTransferFunctions = struct
     | Load {id= lhs_id; e= rhs_exp; loc} ->
         (* [lhs_id := *rhs_exp] *)
         let result =
-          PulseOperations.eval_deref loc rhs_exp astate
-          >>| fun (astate, rhs_addr_hist) -> PulseOperations.write_id lhs_id rhs_addr_hist astate
+          let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
+          PulseOperations.write_id lhs_id rhs_addr_hist astate
         in
         [check_error summary result]
     | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
         (* [*lhs_exp := rhs_exp] *)
         let event = ValueHistory.Assignment loc in
         let result =
-          PulseOperations.eval loc rhs_exp astate
-          >>= fun (astate, (rhs_addr, rhs_history)) ->
-          PulseOperations.eval loc lhs_exp astate
-          >>= fun (astate, lhs_addr_hist) ->
-          PulseOperations.write_deref loc ~ref:lhs_addr_hist
-            ~obj:(rhs_addr, event :: rhs_history)
-            astate
-          >>= fun astate ->
+          let* astate, (rhs_addr, rhs_history) = PulseOperations.eval loc rhs_exp astate in
+          let* astate, lhs_addr_hist = PulseOperations.eval loc lhs_exp astate in
+          let* astate =
+            PulseOperations.write_deref loc ~ref:lhs_addr_hist
+              ~obj:(rhs_addr, event :: rhs_history)
+              astate
+          in
           match lhs_exp with
           | Lvar pvar when Pvar.is_return pvar ->
               PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr

infer/src/pulse/PulseAbductiveDomain.ml

@@ -165,7 +165,7 @@ module Stack = struct
 end
 
 module AddressAttributes = struct
-  open Result.Monad_infix
+  open IResult.Let_syntax
 
   (** if [address] is in [pre] then add the attribute [attr] *)
   let abduce_attribute address attribute astate =
@@ -180,8 +180,7 @@ module AddressAttributes = struct
 
 
   let check_valid access_trace addr astate =
-    BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs
-    >>| fun () ->
+    let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in
     (* if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
     abduce_attribute addr (MustBeValid access_trace) astate
 
@@ -559,11 +558,9 @@ module PrePost = struct
       [call_state.astate] *)
   let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state =
     L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractValue.pp (fst actual) ;
-    (let open Option.Monad_infix in
-    BaseStack.find_opt formal pre.BaseDomain.stack
-    >>= fun (addr_formal_pre, _) ->
-    BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap
-    >>| fun (formal_pre, _) ->
+    (let open IOption.Let_syntax in
+    let* addr_formal_pre, _ = BaseStack.find_opt formal pre.BaseDomain.stack in
+    let+ formal_pre, _ = BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap in
     materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre
       ~addr_hist_caller:actual call_state)
     |> function Some result -> result | None -> Ok call_state
@@ -724,7 +721,7 @@ module PrePost = struct
   let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state =
     PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ;
     let r =
-      let open Result.Monad_infix in
+      let open IResult.Let_syntax in
       (* first make as large a mapping as we can between callee values and caller values... *)
       materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
         call_state
@@ -814,10 +811,11 @@ module PrePost = struct
     in
     let attrs =
       let written_to =
-        let open Option.Monad_infix in
-        BaseAddressAttributes.find_opt addr_caller attrs
-        >>= (fun attrs -> Attributes.get_written_to attrs)
-        |> fun written_to_callee_opt ->
+        let written_to_callee_opt =
+          let open IOption.Let_syntax in
+          let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in
+          Attributes.get_written_to attrs
+        in
         let callee_trace =
           match written_to_callee_opt with
           | None ->
@@ -872,12 +870,14 @@ module PrePost = struct
     L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp
       (fst actual) ;
     match
-      let open Option.Monad_infix in
-      BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack
-      >>= fun (addr_formal_pre, _) ->
-      BaseMemory.find_edge_opt addr_formal_pre Dereference
-        (pre_post.pre :> BaseDomain.t).BaseDomain.heap
-      >>| fun (formal_pre, _) ->
+      let open IOption.Let_syntax in
+      let* addr_formal_pre, _ =
+        BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack
+      in
+      let+ formal_pre, _ =
+        BaseMemory.find_edge_opt addr_formal_pre Dereference
+          (pre_post.pre :> BaseDomain.t).BaseDomain.heap
+      in
       record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
         ~addr_hist_caller:actual call_state
     with
@@ -1060,9 +1060,8 @@ module PrePost = struct
     | Ok call_state -> (
         L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ;
         match
-          let open Result.Monad_infix in
-          check_all_valid callee_proc_name call_location pre_post call_state
-          >>| fun astate ->
+          let open IResult.Let_syntax in
+          let+ astate = check_all_valid callee_proc_name call_location pre_post call_state in
           (* reset [visited] *)
           let call_state = {call_state with astate; visited= AddressSet.empty} in
           (* apply the postcondition *)

infer/src/pulse/PulseModels.ml

@@ -5,7 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 open! IStd
-open Result.Monad_infix
+open IResult.Let_syntax
 open PulseBasicInterface
 open PulseDomainInterface
 
@@ -24,14 +24,14 @@ module Misc = struct
   let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
-    PulseOperations.eval_access location src_pointer_hist Dereference astate
-    >>= fun (astate, obj) ->
-    PulseOperations.shallow_copy location obj astate
-    >>= fun (astate, obj_copy) ->
-    PulseOperations.write_deref location ~ref:dest_pointer_hist
-      ~obj:(fst obj_copy, event :: snd obj_copy)
-      astate
-    >>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate]
+    let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
+    let* astate, obj_copy = PulseOperations.shallow_copy location obj astate in
+    let+ astate =
+      PulseOperations.write_deref location ~ref:dest_pointer_hist
+        ~obj:(fst obj_copy, event :: snd obj_copy)
+        astate
+    in
+    [PulseOperations.havoc_id ret_id [event] astate]
 
 
   let early_exit : model = fun ~caller_summary:_ _ ~ret:_ _ -> Ok []
@@ -85,8 +85,8 @@ module C = struct
     if is_known_zero then (* freeing 0 is a no-op *)
       Ok [astate]
     else
-      PulseOperations.invalidate location Invalidation.CFree deleted_access astate
-      >>| fun astate -> [astate]
+      let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
+      [astate]
 end
 
 module Cplusplus = struct
@@ -113,35 +113,35 @@ module StdAtomicInteger = struct
 
 
   let load_backing_int location this astate =
-    PulseOperations.eval_access location this Dereference astate
-    >>= fun (astate, obj) ->
-    PulseOperations.eval_access location obj (FieldAccess internal_int) astate
-    >>= fun (astate, int_addr) ->
-    PulseOperations.eval_access location int_addr Dereference astate
-    >>| fun (astate, int_val) -> (astate, int_addr, int_val)
+    let* astate, obj = PulseOperations.eval_access location this Dereference astate in
+    let* astate, int_addr =
+      PulseOperations.eval_access location obj (FieldAccess internal_int) astate
+    in
+    let+ astate, int_val = PulseOperations.eval_access location int_addr Dereference astate in
+    (astate, int_addr, int_val)
 
 
   let constructor this_address init_value : model =
    fun ~caller_summary:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::atomic()"; location; in_call= []} in
     let this = (AbstractValue.mk_fresh (), [event]) in
-    PulseOperations.eval_access location this (FieldAccess internal_int) astate
-    >>= fun (astate, int_field) ->
-    PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate
-    >>= fun astate ->
-    PulseOperations.write_deref location ~ref:this_address ~obj:this astate
-    >>| fun astate -> [astate]
+    let* astate, int_field =
+      PulseOperations.eval_access location this (FieldAccess internal_int) astate
+    in
+    let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in
+    let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in
+    [astate]
 
 
   let arith_bop prepost location event ret_id bop this operand astate =
-    load_backing_int location this astate
-    >>= fun (astate, int_addr, (old_int, old_int_hist)) ->
+    let* astate, int_addr, (old_int, old_int_hist) = load_backing_int location this astate in
     let astate, (new_int, hist) =
       PulseOperations.eval_binop location bop (AbstractValueOperand old_int) operand old_int_hist
         astate
     in
-    PulseOperations.write_deref location ~ref:int_addr ~obj:(new_int, event :: hist) astate
-    >>| fun astate ->
+    let+ astate =
+      PulseOperations.write_deref location ~ref:int_addr ~obj:(new_int, event :: hist) astate
+    in
     let ret_int = match prepost with `Pre -> new_int | `Post -> old_int in
     PulseOperations.write_id ret_id (ret_int, event :: hist) astate
 
@@ -149,22 +149,30 @@ module StdAtomicInteger = struct
   let fetch_add this (increment, _) _memory_ordering : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::fetch_add()"; location; in_call= []} in
-    arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) astate
-    >>| fun astate -> [astate]
+    let+ astate =
+      arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment)
+        astate
+    in
+    [astate]
 
 
   let fetch_sub this (increment, _) _memory_ordering : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::fetch_sub()"; location; in_call= []} in
-    arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) astate
-    >>| fun astate -> [astate]
+    let+ astate =
+      arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment)
+        astate
+    in
+    [astate]
 
 
   let operator_plus_plus_pre this : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::operator++()"; location; in_call= []} in
-    arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
-    >>| fun astate -> [astate]
+    let+ astate =
+      arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
+    in
+    [astate]
 
 
   let operator_plus_plus_post this _int : model =
@@ -172,15 +180,19 @@ module StdAtomicInteger = struct
     let event =
       ValueHistory.Call {f= Model "std::atomic<T>::operator++(T)"; location; in_call= []}
     in
-    arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
-    >>| fun astate -> [astate]
+    let+ astate =
+      arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
+    in
+    [astate]
 
 
   let operator_minus_minus_pre this : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::operator--()"; location; in_call= []} in
-    arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
-    >>| fun astate -> [astate]
+    let+ astate =
+      arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
+    in
+    [astate]
 
 
   let operator_minus_minus_post this _int : model =
@@ -188,15 +200,16 @@ module StdAtomicInteger = struct
     let event =
       ValueHistory.Call {f= Model "std::atomic<T>::operator--(T)"; location; in_call= []}
     in
-    arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
-    >>| fun astate -> [astate]
+    let+ astate =
+      arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
+    in
+    [astate]
 
 
   let load_instr model_desc this _memory_ordering_opt : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
-    load_backing_int location this astate
-    >>| fun (astate, _int_addr, (int, hist)) ->
+    let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in
     [PulseOperations.write_id ret_id (int, event :: hist) astate]
 
 
@@ -205,27 +218,26 @@ module StdAtomicInteger = struct
   let operator_t = load_instr "std::atomic<T>::operator_T()"
 
   let store_backing_int location this_address new_value astate =
-    PulseOperations.eval_access location this_address Dereference astate
-    >>= fun (astate, this) ->
-    PulseOperations.eval_access location this (FieldAccess internal_int) astate
-    >>= fun (astate, int_field) ->
+    let* astate, this = PulseOperations.eval_access location this_address Dereference astate in
+    let* astate, int_field =
+      PulseOperations.eval_access location this (FieldAccess internal_int) astate
+    in
     PulseOperations.write_deref location ~ref:int_field ~obj:new_value astate
 
 
   let store this_address (new_value, new_hist) _memory_ordering : model =
    fun ~caller_summary:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in
-    store_backing_int location this_address (new_value, event :: new_hist) astate
-    >>| fun astate -> [astate]
+    let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
+    [astate]
 
 
   let exchange this_address (new_value, new_hist) _memory_ordering : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::exchange()"; location; in_call= []} in
-    load_backing_int location this_address astate
-    >>= fun (astate, _int_addr, (old_int, old_hist)) ->
-    store_backing_int location this_address (new_value, event :: new_hist) astate
-    >>| fun astate -> [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate]
+    let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in
+    let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
+    [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate]
 end
 
 module StdBasicString = struct
@@ -244,10 +256,10 @@ module StdBasicString = struct
   let data this_hist : model =
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in
-    to_internal_string location this_hist astate
-    >>= fun (astate, string_addr_hist) ->
-    PulseOperations.eval_access location string_addr_hist Dereference astate
-    >>| fun (astate, (string, hist)) ->
+    let* astate, string_addr_hist = to_internal_string location this_hist astate in
+    let+ astate, (string, hist) =
+      PulseOperations.eval_access location string_addr_hist Dereference astate
+    in
     [PulseOperations.write_id ret_id (string, event :: hist) astate]
 
 
@@ -255,12 +267,11 @@ module StdBasicString = struct
    fun ~caller_summary:_ location ~ret:_ astate ->
     let model = CallEvent.Model "std::basic_string::~basic_string()" in
     let call_event = ValueHistory.Call {f= model; location; in_call= []} in
-    to_internal_string location this_hist astate
-    >>= fun (astate, (string_addr, string_hist)) ->
+    let* astate, (string_addr, string_hist) = to_internal_string location this_hist astate in
     let string_addr_hist = (string_addr, call_event :: string_hist) in
-    PulseOperations.invalidate_deref location CppDelete string_addr_hist astate
-    >>= fun astate ->
-    PulseOperations.invalidate location CppDelete string_addr_hist astate >>| fun astate -> [astate]
+    let* astate = PulseOperations.invalidate_deref location CppDelete string_addr_hist astate in
+    let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in
+    [astate]
 end
 
 module StdFunction = struct
@@ -270,10 +281,10 @@ module StdFunction = struct
       let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in
       [PulseOperations.havoc_id ret_id [event] astate]
     in
-    PulseOperations.eval_access location lambda_ptr_hist Dereference astate
-    >>= fun (astate, (lambda, _)) ->
-    PulseOperations.Closures.check_captured_addresses location lambda astate
-    >>= fun astate ->
+    let* astate, (lambda, _) =
+      PulseOperations.eval_access location lambda_ptr_hist Dereference astate
+    in
+    let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in
     match AddressAttributes.get_closure_proc_name lambda astate with
     | None ->
         (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate)
@@ -300,16 +311,14 @@ module StdVector = struct
 
 
   let element_of_internal_array location vector index astate =
-    to_internal_array location vector astate
-    >>= fun (astate, vector_internal_array) ->
+    let* astate, vector_internal_array = to_internal_array location vector astate in
     PulseOperations.eval_access location vector_internal_array
       (ArrayAccess (Typ.void, index))
       astate
 
 
   let reallocate_internal_array trace vector vector_f location astate =
-    to_internal_array location vector astate
-    >>= fun (astate, array_address) ->
+    let* astate, array_address = to_internal_array location vector astate in
     PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate
     >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address
     >>= PulseOperations.havoc_field location vector internal_array trace
@@ -329,8 +338,7 @@ module StdVector = struct
   let at ~desc vector index : model =
    fun ~caller_summary:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    element_of_internal_array location vector (fst index) astate
-    >>| fun (astate, (addr, hist)) ->
+    let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in
     [PulseOperations.write_id (fst ret) (addr, event :: hist) astate]
 
 
@@ -358,13 +366,16 @@ module JavaCollection = struct
   let set coll index new_elem : model =
    fun ~caller_summary:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in
-    StdVector.element_of_internal_array location coll (fst index) astate
-    >>= fun (astate, ((old_addr, old_hist) as old_elem)) ->
-    PulseOperations.write_deref location ~ref:new_elem
-      ~obj:(old_addr, ValueHistory.Assignment location :: old_hist)
-      astate
-    >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem
-    >>| fun astate -> [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate]
+    let* astate, ((old_addr, old_hist) as old_elem) =
+      StdVector.element_of_internal_array location coll (fst index) astate
+    in
+    let+ astate =
+      PulseOperations.write_deref location ~ref:new_elem
+        ~obj:(old_addr, ValueHistory.Assignment location :: old_hist)
+        astate
+      >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem
+    in
+    [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate]
 end
 
 module StringSet = Caml.Set.Make (String)

infer/src/pulse/PulseOperations.ml

@@ -6,7 +6,7 @@
  *)
 open! IStd
 module L = Logging
-open Result.Monad_infix
+open IResult.Let_syntax
 open PulseBasicInterface
 open PulseDomainInterface
 
@@ -55,17 +55,20 @@ module Closures = struct
     | None ->
         Ok astate
     | Some (edges, attributes) ->
-        IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function
-          | Attribute.Closure _ ->
-              IContainer.iter_result
-                ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges
-                ~f:(fun (access, addr_trace) ->
-                  if is_captured_fake_access access then
-                    check_addr_access action addr_trace astate >>| fun _ -> ()
-                  else Ok () )
-          | _ ->
-              Ok () )
-        >>| fun () -> astate
+        let+ () =
+          IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function
+            | Attribute.Closure _ ->
+                IContainer.iter_result
+                  ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges
+                  ~f:(fun (access, addr_trace) ->
+                    if is_captured_fake_access access then
+                      let+ _ = check_addr_access action addr_trace astate in
+                      ()
+                    else Ok () )
+            | _ ->
+                Ok () )
+        in
+        astate
 
 
   let record location pname captured astate =
@@ -92,8 +95,8 @@ end
 let eval_var var astate = Stack.eval var astate
 
 let eval_access location addr_hist access astate =
-  check_addr_access location addr_hist astate
-  >>| fun astate -> Memory.eval_edge addr_hist access astate
+  let+ astate = check_addr_access location addr_hist astate in
+  Memory.eval_edge addr_hist access astate
 
 
 type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t
@@ -180,29 +183,25 @@ let eval location exp0 astate =
     | Lvar pvar ->
         Ok (eval_var [ValueHistory.VariableAccessed (pvar, location)] (Var.of_pvar pvar) astate)
     | Lfield (exp', field, _) ->
-        eval exp' astate
-        >>= fun (astate, addr_hist) ->
-        check_addr_access location addr_hist astate
-        >>| fun astate -> Memory.eval_edge addr_hist (FieldAccess field) astate
+        let* astate, addr_hist = eval exp' astate in
+        let+ astate = check_addr_access location addr_hist astate in
+        Memory.eval_edge addr_hist (FieldAccess field) astate
     | Lindex (exp', exp_index) ->
-        eval exp_index astate
-        >>= fun (astate, addr_hist_index) ->
-        eval exp' astate
-        >>= fun (astate, addr_hist) ->
-        check_addr_access location addr_hist astate
-        >>| fun astate ->
+        let* astate, addr_hist_index = eval exp_index astate in
+        let* astate, addr_hist = eval exp' astate in
+        let+ astate = check_addr_access location addr_hist astate in
         Memory.eval_edge addr_hist (ArrayAccess (Typ.void, fst addr_hist_index)) astate
     | Closure {name; captured_vars} ->
-        List.fold_result captured_vars ~init:(astate, [])
-          ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) ->
-            eval capt_exp astate
-            >>| fun (astate, addr_trace) ->
-            let mode =
-              (* HACK: the frontend follows this discipline *)
-              match (capt_exp : Exp.t) with Lvar _ -> `ByReference | _ -> `ByValue
-            in
-            (astate, (captured_as, addr_trace, mode) :: rev_captured) )
-        >>| fun (astate, rev_captured) ->
+        let+ astate, rev_captured =
+          List.fold_result captured_vars ~init:(astate, [])
+            ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) ->
+              let+ astate, addr_trace = eval capt_exp astate in
+              let mode =
+                (* HACK: the frontend follows this discipline *)
+                match (capt_exp : Exp.t) with Lvar _ -> `ByReference | _ -> `ByValue
+              in
+              (astate, (captured_as, addr_trace, mode) :: rev_captured) )
+        in
         Closures.record location name (List.rev rev_captured) astate
     | Cast (_, exp') ->
         eval exp' astate
@@ -220,15 +219,16 @@ let eval location exp0 astate =
         in
         Ok (astate, (addr, []))
     | UnOp (unop, exp, _typ) ->
-        eval exp astate >>| fun (astate, (addr, hist)) -> eval_unop location unop addr hist astate
+        let+ astate, (addr, hist) = eval exp astate in
+        eval_unop location unop addr hist astate
     | BinOp (bop, e_lhs, e_rhs) ->
-        eval e_lhs astate
-        >>= fun (astate, (addr_lhs, hist_lhs)) ->
-        eval e_rhs astate
-        >>| fun ( astate
-                , ( addr_rhs
-                  , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *)
-                  _ ) ) ->
+        let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in
+        let+ ( astate
+             , ( addr_rhs
+               , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *)
+               _ ) ) =
+          eval e_rhs astate
+        in
         eval_binop location bop (AbstractValueOperand addr_lhs) (AbstractValueOperand addr_rhs)
           hist_lhs astate
     | Const _ | Sizeof _ | Exn _ ->
@@ -248,8 +248,7 @@ let eval_arith location exp astate =
             , Trace.Immediate {location; history= [ValueHistory.Assignment location]} )
         , Itv.ItvPure.of_int_lit i )
   | exp ->
-      eval location exp astate
-      >>| fun (astate, (value, _)) ->
+      let+ astate, (value, _) = eval location exp astate in
       ( astate
       , Some value
       , AddressAttributes.get_arithmetic value astate
@@ -296,10 +295,12 @@ let prune ~is_then_branch if_kind location ~condition astate =
   let rec prune_aux ~negated exp astate =
     match (exp : Exp.t) with
     | BinOp (bop, exp_lhs, exp_rhs) -> (
-        eval_arith location exp_lhs astate
-        >>= fun (astate, value_lhs_opt, arith_lhs_opt, bo_itv_lhs) ->
-        eval_arith location exp_rhs astate
-        >>| fun (astate, value_rhs_opt, arith_rhs_opt, bo_itv_rhs) ->
+        let* astate, value_lhs_opt, arith_lhs_opt, bo_itv_lhs =
+          eval_arith location exp_lhs astate
+        in
+        let+ astate, value_rhs_opt, arith_rhs_opt, bo_itv_rhs =
+          eval_arith location exp_rhs astate
+        in
         match
           Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt)
             (Option.map ~f:fst arith_rhs_opt)
@@ -340,10 +341,9 @@ let prune ~is_then_branch if_kind location ~condition astate =
 
 
 let eval_deref location exp astate =
-  eval location exp astate
-  >>= fun (astate, addr_hist) ->
-  check_addr_access location addr_hist astate
-  >>| fun astate -> Memory.eval_edge addr_hist Dereference astate
+  let* astate, addr_hist = eval location exp astate in
+  let+ astate = check_addr_access location addr_hist astate in
+  Memory.eval_edge addr_hist Dereference astate
 
 
 let realloc_pvar pvar location astate =
@@ -387,8 +387,7 @@ let invalidate_deref location cause ref_addr_hist astate =
 
 
 let invalidate_array_elements location cause addr_trace astate =
-  check_addr_access location addr_trace astate
-  >>| fun astate ->
+  let+ astate = check_addr_access location addr_trace astate in
   match Memory.find_opt (fst addr_trace) astate with
   | None ->
       astate
@@ -404,8 +403,7 @@ let invalidate_array_elements location cause addr_trace astate =
 
 
 let shallow_copy location addr_hist astate =
-  check_addr_access location addr_hist astate
-  >>| fun astate ->
+  let+ astate = check_addr_access location addr_hist astate in
   let cell =
     match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with
     | None ->
@@ -458,7 +456,8 @@ let check_address_escape escape_location proc_desc address history astate =
             (Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) )
         else Ok () )
   in
-  check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate
+  let+ () = check_address_of_cpp_temporary () >>= check_address_of_stack_variable in
+  astate
 
 
 let mark_address_of_cpp_temporary history variable address astate =