[pulse] change ISL functions to return list of results

Summary:
It makes more sense to return a list of results than a result of lists:
the latter stops the execution on *all* the disjuncts that would have
been in the list as soon as *one* of them fails. This is the same issue
we solved for non-ISL pulse models earlier.

Reviewed By: skcho

Differential Revision: D26818409

fbshipit-source-id: 7cc1d8b39

infer/src/pulse/Pulse.ml

@@ -243,7 +243,7 @@ module PulseTransferFunctions = struct
               [astate]
           | ContinueProgram astate ->
               dispatch_call analysis_data ret call_exp actuals location call_flags astate
-              |> PulseReport.report_results analysis_data )
+              |> PulseReport.report_exec_results analysis_data )
     in
     let dynamic_types_unreachable =
       PulseOperations.get_dynamic_type_unreachable_values vars astate
@@ -279,30 +279,28 @@ module PulseTransferFunctions = struct
       | Load {id= lhs_id; e= rhs_exp; loc} ->
           (* [lhs_id := *rhs_exp] *)
           let result =
-            let+ astate_rhs_addr_hists =
             if Config.pulse_isl then
-                let+ astate_rhs_addr_hists = PulseOperations.eval_deref_isl loc rhs_exp astate in
-                astate_rhs_addr_hists
-              else
-                let+ astate_rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
-                [astate_rhs_addr_hist]
-            in
-            List.map astate_rhs_addr_hists ~f:(fun (astate, rhs_addr_hist) ->
+              PulseOperations.eval_deref_isl loc rhs_exp astate
+              |> List.map ~f:(fun result ->
+                     let+ astate, rhs_addr_hist = result in
                      PulseOperations.write_id lhs_id rhs_addr_hist astate )
+            else
+              [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in
+                 PulseOperations.write_id lhs_id rhs_addr_hist astate) ]
           in
-          PulseReport.report_list_result analysis_data result
+          PulseReport.report_results analysis_data result
       | Store {e1= lhs_exp; e2= rhs_exp; loc} ->
           (* [*lhs_exp := rhs_exp] *)
           let event = ValueHistory.Assignment loc in
           let result =
-            let* astate, (rhs_addr, rhs_history) =
+            let<*> astate, (rhs_addr, rhs_history) =
               PulseOperations.eval NoAccess loc rhs_exp astate
             in
-            let* is_structured, ls_astate_lhs_addr_hist =
+            let<*> is_structured, ls_astate_lhs_addr_hist =
               if Config.pulse_isl then PulseOperations.eval_structure_isl Write loc lhs_exp astate
               else
-                let* astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in
-                Ok (false, [(astate, lhs_addr_hist)])
+                let+ astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in
+                (false, [Ok (astate, lhs_addr_hist)])
             in
             let write_function lhs_addr_hist astate =
               if is_structured then
@@ -310,40 +308,35 @@ module PulseTransferFunctions = struct
                   ~obj:(rhs_addr, event :: rhs_history)
                   astate
               else
-                let+ astate =
-                  PulseOperations.write_deref loc ~ref:lhs_addr_hist
+                [ PulseOperations.write_deref loc ~ref:lhs_addr_hist
                     ~obj:(rhs_addr, event :: rhs_history)
-                    astate
+                    astate ]
             in
-                [astate]
-            in
-            let* astates =
-              List.fold_result ls_astate_lhs_addr_hist ~init:[]
-                ~f:(fun acc_astates (astate, lhs_addr_hist) ->
+            let astates =
+              List.concat_map ls_astate_lhs_addr_hist ~f:(fun result ->
+                  let<*> astate, lhs_addr_hist = result in
                   match (Config.pulse_isl, astate.AbductiveDomain.isl_status) with
                   | false, _ | true, ISLOk ->
-                      let+ astates = write_function lhs_addr_hist astate in
-                      List.rev_append astates acc_astates
+                      write_function lhs_addr_hist astate
                   | true, ISLError ->
-                      Ok (astate :: acc_astates) )
+                      [Ok astate] )
             in
             let astates =
               if Topl.is_deep_active () then
-                List.map astates ~f:(fun astate ->
+                List.map astates ~f:(fun result ->
+                    let+ astate = result in
                     topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate )
               else astates
             in
             match lhs_exp with
             | Lvar pvar when Pvar.is_return pvar ->
-                List.fold_result astates ~init:[] ~f:(fun acc astate ->
-                    let+ astate =
-                      PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate
-                    in
-                    astate :: acc )
+                List.map astates ~f:(fun result ->
+                    let* astate = result in
+                    PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate )
             | _ ->
-                Ok astates
+                astates
           in
-          PulseReport.report_list_result analysis_data result
+          PulseReport.report_results analysis_data result
       | Prune (condition, loc, _is_then_branch, _if_kind) ->
           (let<*> astate = PulseOperations.prune loc ~condition astate in
            if PulseArithmetic.is_unsat_cheap astate then
@@ -352,10 +345,10 @@ module PulseTransferFunctions = struct
            else
              (* [condition] is true or unknown value: go into the branch *)
              [Ok (ContinueProgram astate)])
-          |> PulseReport.report_results analysis_data
+          |> PulseReport.report_exec_results analysis_data
       | Call (ret, call_exp, actuals, loc, call_flags) ->
           dispatch_call analysis_data ret call_exp actuals loc call_flags astate
-          |> PulseReport.report_results analysis_data
+          |> PulseReport.report_exec_results analysis_data
       | Metadata (ExitScope (vars, location)) ->
           let remove_vars vars astates =
             List.concat_map astates ~f:(fun (astate : Domain.t) ->
@@ -363,12 +356,8 @@ module PulseTransferFunctions = struct
                 | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ ->
                     [astate]
                 | ContinueProgram astate ->
-                    ( match PulseOperations.remove_vars tenv vars location astate with
-                    | Ok astate ->
-                        Ok [astate]
-                    | Error _ as error ->
-                        error )
-                    |> PulseReport.report_list_result analysis_data )
+                    PulseOperations.remove_vars tenv vars location astate
+                    |> PulseReport.report_result analysis_data )
           in
           if Procname.is_java (Procdesc.get_proc_name proc_desc) then
             remove_vars vars [ContinueProgram astate]

infer/src/pulse/PulseModels.ml

@@ -123,11 +123,10 @@ module Misc = struct
     let astates_alloc =
       let astate = PulseArithmetic.and_positive (fst deleted_access) astate in
       if Config.pulse_isl then
-        match PulseOperations.invalidate_biad_isl location invalidation deleted_access astate with
-        | Error _ as err ->
-            [err]
-        | Ok astates ->
-            List.map astates ~f:(fun astate -> Ok (ContinueProgram astate))
+        PulseOperations.invalidate_biad_isl location invalidation deleted_access astate
+        |> List.map ~f:(fun result ->
+               let+ astate = result in
+               ContinueProgram astate )
       else
         let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in
         astate

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -22,10 +22,7 @@ let mk_objc_method_nil_summary_aux proc_desc astate =
   let astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in
   let ret_var = Procdesc.get_ret_var proc_desc in
   let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in
-  let+ astate =
   PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate
-  in
-  [astate]
 
 
 let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_data) initial =
@@ -39,7 +36,7 @@ let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_
          However, there is an exception in the case where the return type is non-POD.
          In that case it's UB and we want to report an error. *)
       let result = mk_objc_method_nil_summary_aux proc_desc astate in
-      Some (PulseReport.report_list_result analysis_data result)
+      Some (PulseReport.report_result analysis_data result)
   | ContinueProgram _, _
   | ExitProgram _, _
   | AbortProgram _, _
@@ -55,10 +52,9 @@ let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_d
   | ContinueProgram astate ->
       let result =
         let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in
-        let astate = PulseArithmetic.prune_positive (fst value) astate in
-        [astate]
+        PulseArithmetic.prune_positive (fst value) astate
       in
-      PulseReport.report_list_result analysis_data result
+      PulseReport.report_result analysis_data result
   | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ ->
       [astate]
 

infer/src/pulse/PulseOperations.ml

@@ -57,33 +57,29 @@ let check_addr_access access_mode location (address, history) astate =
 let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false)
     astate =
   let access_trace = Trace.Immediate {location; history} in
-  let* astates =
-    AddressAttributes.check_valid_isl access_trace address ~null_noop astate
-    |> Result.map_error ~f:(fun (invalidation, invalidation_trace, astate) ->
+  match AddressAttributes.check_valid_isl access_trace address ~null_noop astate with
+  | Error (invalidation, invalidation_trace, astate) ->
+      [ Error
           ( Diagnostic.AccessToInvalidAddress
               {calling_context= []; invalidation; invalidation_trace; access_trace}
-           , astate ) )
-  in
+          , astate ) ]
+  | Ok astates -> (
     match access_mode with
     | Read ->
-      List.fold_result astates ~init:[] ~f:(fun astates astate ->
-          match AddressAttributes.check_initialized access_trace address astate with
-          | Error _ ->
-              Error
+        List.map astates ~f:(fun astate ->
+            AddressAttributes.check_initialized access_trace address astate
+            |> Result.map_error ~f:(fun () ->
                    ( Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
-                , AbductiveDomain.set_isl_status ISLError astate )
-          | Ok ok_astate ->
-              Ok (ok_astate :: astates) )
+                   , AbductiveDomain.set_isl_status ISLError astate ) ) )
     | Write ->
-      Ok
-        (List.map astates ~f:(fun astate ->
+        List.map astates ~f:(fun astate ->
             match astate.AbductiveDomain.isl_status with
             | ISLOk ->
-                 AbductiveDomain.initialize address astate
+                Ok (AbductiveDomain.initialize address astate)
             | ISLError ->
-                 astate ))
+                Ok astate )
     | NoAccess ->
-      Ok astates
+        List.map ~f:(fun astate -> Ok astate) astates )
 
 
 module Closures = struct
@@ -166,18 +162,17 @@ let eval_access mode location addr_hist access astate =
 
 
 let eval_access_biad_isl mode location addr_hist access astate =
-  let map_ok addr_hist access astates =
-    List.map
-      ~f:(fun astate ->
+  let map_ok addr_hist access results =
+    List.map results ~f:(fun result ->
+        let+ astate = result in
         match astate.AbductiveDomain.isl_status with
         | ISLOk ->
             Memory.eval_edge addr_hist access astate
         | ISLError ->
             (astate, addr_hist) )
-      astates
   in
-  let+ astates = check_and_abduce_addr_access_isl mode location addr_hist astate in
-  map_ok addr_hist access astates
+  let results = check_and_abduce_addr_access_isl mode location addr_hist astate in
+  map_ok addr_hist access results
 
 
 let eval mode location exp0 astate =
@@ -267,52 +262,47 @@ let eval_deref location exp astate =
 let eval_structure_isl mode loc exp astate =
   match (exp : Exp.t) with
   | Lfield (exp', field, _) ->
-      let* astate, addr_hist = eval mode loc exp' astate in
-      let+ astates =
-        eval_access_biad_isl mode loc addr_hist (HilExp.Access.FieldAccess field) astate
-      in
+      let+ astate, addr_hist = eval mode loc exp' astate in
+      let astates = eval_access_biad_isl mode loc addr_hist (FieldAccess field) astate in
       (false, astates)
   | Lindex (exp', exp_index) ->
       let* astate, addr_hist_index = eval mode loc exp_index astate in
-      let* astate, addr_hist = eval mode loc exp' astate in
-      let+ astates =
+      let+ astate, addr_hist = eval mode loc exp' astate in
+      let astates =
         eval_access_biad_isl mode loc addr_hist
-          (HilExp.Access.ArrayAccess (StdTyp.void, fst addr_hist_index))
+          (ArrayAccess (StdTyp.void, fst addr_hist_index))
           astate
       in
       (false, astates)
   | _ ->
       let+ astate, (addr, history) = eval mode loc exp astate in
-      (true, [(astate, (addr, history))])
+      (true, [Ok (astate, (addr, history))])
 
 
 let eval_deref_biad_isl location access addr_hist astate =
-  let+ astates = check_and_abduce_addr_access_isl Read location addr_hist astate in
-  List.map
-    ~f:(fun astate ->
+  let astates = check_and_abduce_addr_access_isl Read location addr_hist astate in
+  List.map astates ~f:(fun astate ->
+      let+ astate = astate in
       match astate.AbductiveDomain.isl_status with
       | ISLOk ->
           Memory.eval_edge addr_hist access astate
       | ISLError ->
           (astate, addr_hist) )
-    astates
 
 
 let eval_deref_isl location exp astate =
-  let* is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in
+  let<*> is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in
   let eval_deref_function (astate, addr_hist) =
     if is_structured then eval_deref_biad_isl location Dereference addr_hist astate
-    else
-      let+ astate = eval_deref location exp astate in
-      [astate]
+    else [eval_deref location exp astate]
   in
-  List.fold_result ls_astate_addr_hist ~init:[] ~f:(fun acc_astates ((astate, _) as astate_addr) ->
+  List.concat_map ls_astate_addr_hist ~f:(fun result ->
+      let<*> ((astate, _) as astate_addr) = result in
       match astate.AbductiveDomain.isl_status with
       | ISLOk ->
-          let+ astates = eval_deref_function astate_addr in
-          acc_astates @ astates
+          eval_deref_function astate_addr
       | ISLError ->
-          Ok (acc_astates @ [astate_addr]) )
+          [Ok astate_addr] )
 
 
 let realloc_pvar tenv pvar typ location astate =
@@ -338,16 +328,14 @@ let write_access location addr_trace_ref access addr_trace_obj astate =
 
 
 let write_access_biad_isl location addr_trace_ref access addr_trace_obj astate =
-  let* astates = check_and_abduce_addr_access_isl Write location addr_trace_ref astate in
-  List.fold_result astates ~init:[] ~f:(fun acc ast ->
-      let astate =
-        match ast.AbductiveDomain.isl_status with
+  check_and_abduce_addr_access_isl Write location addr_trace_ref astate
+  |> List.map ~f:(fun result ->
+         let+ astate = result in
+         match astate.AbductiveDomain.isl_status with
          | ISLOk ->
-            Memory.add_edge addr_trace_ref access addr_trace_obj location ast
+             Memory.add_edge addr_trace_ref access addr_trace_obj location astate
          | ISLError ->
-            ast
-      in
-      Ok (astate :: acc) )
+             astate )
 
 
 let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
@@ -385,17 +373,14 @@ let invalidate location cause addr_trace astate =
 
 
 let invalidate_biad_isl location cause (address, history) astate =
-  let+ astates =
   check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate
-  in
-  List.map
-    ~f:(fun astate ->
+  |> List.map ~f:(fun result ->
+         let+ astate = result in
          match astate.AbductiveDomain.isl_status with
          | ISLOk ->
              AddressAttributes.invalidate (address, history) cause location astate
          | ISLError ->
              astate )
-    astates
 
 
 let invalidate_access location cause ref_addr_hist access astate =

infer/src/pulse/PulseOperations.mli

@@ -70,7 +70,7 @@ val eval_structure_isl :
   -> Location.t
   -> Exp.t
   -> t
-  -> (bool * (t * (AbstractValue.t * ValueHistory.t)) list) access_result
+  -> (bool * (t * (AbstractValue.t * ValueHistory.t)) access_result list) access_result
 (** Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states
     (ISLOk and ISLErs); The boolean indicates whether it is data structures or not. *)
 
@@ -80,7 +80,7 @@ val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistor
 (** Like [eval] but evaluates [*exp]. *)
 
 val eval_deref_isl :
-  Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) list access_result
+  Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result list
 
 val eval_access :
      access_mode
@@ -138,14 +138,14 @@ val write_deref_biad_isl :
   -> AbstractValue.t HilExp.Access.t
   -> obj:AbstractValue.t * ValueHistory.t
   -> t
-  -> t list access_result
+  -> t access_result list
 
 val invalidate :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** record that the address is invalid *)
 
 val invalidate_biad_isl :
-  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t list access_result
+  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result list
 (** record that the address is invalid. If the address has not been allocated, abduce ISL specs for
     both invalid (null, free, unint) and allocated heap. *)
 

infer/src/pulse/PulseReport.ml

@@ -57,22 +57,6 @@ let report_error tenv proc_desc err_log access_result =
           ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} )
 
 
-let exec_list_of_list_result = function
-  | Ok posts ->
-      posts
-  | Error Unsat ->
-      []
-  | Error (Sat post) ->
-      [post]
-
-
-let report_list_result {tenv; InterproceduralAnalysis.proc_desc; err_log} result =
-  let open Result.Monad_infix in
-  report_error tenv proc_desc err_log result
-  >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post)
-  |> exec_list_of_list_result
-
-
 let post_of_report_result = function
   | Ok post ->
       Some post
@@ -82,6 +66,17 @@ let post_of_report_result = function
       Some post
 
 
-let report_results {tenv; InterproceduralAnalysis.proc_desc; err_log} results =
+let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results =
   List.filter_map results ~f:(fun exec_result ->
       report_error tenv proc_desc err_log exec_result |> post_of_report_result )
+
+
+let report_results analysis_data results =
+  List.map results ~f:(fun result ->
+      let open IResult.Let_syntax in
+      let+ astate = result in
+      ExecutionDomain.ContinueProgram astate )
+  |> report_exec_results analysis_data
+
+
+let report_result analysis_data result = report_results analysis_data [result]

infer/src/pulse/PulseReport.mli

@@ -11,12 +11,17 @@ open PulseDomainInterface
 
 type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result
 
-val report_list_result :
+val report_result :
      PulseSummary.t InterproceduralAnalysis.t
-  -> AbductiveDomain.t list access_result
+  -> AbductiveDomain.t access_result
   -> ExecutionDomain.t list
 
 val report_results :
      PulseSummary.t InterproceduralAnalysis.t
+  -> AbductiveDomain.t access_result list
+  -> ExecutionDomain.t list
+
+val report_exec_results :
+     PulseSummary.t InterproceduralAnalysis.t
   -> ExecutionDomain.t access_result list
   -> ExecutionDomain.t list