[pulse] refactor errors

Summary:
This will enable further improvements: basically we want to be able to
abort the symbolic execution of a single disjunct whenever an error is
detected. Right now there is only one kind of error, which is now
explicitly called `ReportableError`.

The next diff refactors Pulse.ISL to add its own error type so that we
are able to get rid of the isl_status field (ISLOk/ISLError) inside
abductive states. ISLError states are really `Error _` states but
previously it would have been too much of an API change to expose that.
Now it's all going to be part of `AccessResult.t`.

A further change will add another error type for when a value is found
to be 0 after the fact by the arithmetic.

Reviewed By: ezgicicek

Differential Revision: D26821178

fbshipit-source-id: 2923db8e7

infer/src/pulse/PulseAccessResult.ml

@@ -0,0 +1,23 @@
+(*
+ * 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.
+ *)
+
+open! IStd
+open PulseBasicInterface
+module AbductiveDomain = PulseAbductiveDomain
+
+type 'astate error = ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
+
+type ('a, 'astate) base_t = ('a, 'astate error) result
+
+type 'a t = ('a, AbductiveDomain.t) base_t
+
+let to_summary tenv proc_desc error =
+  let open SatUnsat.Import in
+  match error with
+  | ReportableError {astate; diagnostic} ->
+      let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in
+      ReportableError {astate; diagnostic}

infer/src/pulse/PulseAccessResult.mli

@@ -0,0 +1,19 @@
+(*
+ * 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.
+ *)
+
+open! IStd
+open PulseBasicInterface
+module AbductiveDomain = PulseAbductiveDomain
+
+type 'astate error = ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
+
+type ('a, 'astate) base_t = ('a, 'astate error) result
+
+type 'a t = ('a, AbductiveDomain.t) base_t
+
+val to_summary :
+  Tenv.t -> Procdesc.t -> AbductiveDomain.t error -> AbductiveDomain.summary error SatUnsat.t

infer/src/pulse/PulseDomainInterface.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module AccessResult = PulseAccessResult
 module ExecutionDomain = PulseExecutionDomain
 
 (** if you do any mutations of the state in pulse you probably want this module *)
@@ -30,6 +31,8 @@ include struct
 
   module PulseAbductiveDomain = PulseAbductiveDomain
   [@@deprecated "use the short form AbductiveDomain instead"]
+  module PulseAccessResult = PulseAccessResult
+  [@@deprecated "use the short form AccessResult instead"]
   module PulseBaseDomain = PulseBaseDomain [@@deprecated "use the short form BaseDomain instead"]
   module PulseBaseStack = PulseBaseStack [@@deprecated "use the short form BaseStack instead"]
   module PulseBaseMemory = PulseBaseMemory [@@deprecated "use the short form BaseMemory instead"]

infer/src/pulse/PulseInterproc.ml

@@ -614,9 +614,11 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
             AddressAttributes.check_valid access_trace addr_caller astate
             |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
                    L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
-                   ( Diagnostic.AccessToInvalidAddress
-                       {calling_context= []; invalidation; invalidation_trace; access_trace}
-                   , astate ) )
+                   AccessResult.ReportableError
+                     { diagnostic=
+                         Diagnostic.AccessToInvalidAddress
+                           {calling_context= []; invalidation; invalidation_trace; access_trace}
+                     ; astate } )
       in
       match BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs with
       | None ->
@@ -626,8 +628,10 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call
           AddressAttributes.check_initialized access_trace addr_caller astate
           |> Result.map_error ~f:(fun () ->
                  L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ;
-                 ( Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
-                 , astate ) ) )
+                 AccessResult.ReportableError
+                   { diagnostic=
+                       Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
+                   ; astate } ) )
     call_state.subst (Ok call_state.astate)
 
 
@@ -664,9 +668,11 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location
                   let access_trace = mk_access_trace callee_access_trace in
                   L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
                   Error
-                    ( Diagnostic.AccessToInvalidAddress
-                        {calling_context= []; invalidation; invalidation_trace; access_trace}
-                    , AbductiveDomain.set_isl_status ISLError astate ) ) ) )
+                    (AccessResult.ReportableError
+                       { diagnostic=
+                           Diagnostic.AccessToInvalidAddress
+                             {calling_context= []; invalidation; invalidation_trace; access_trace}
+                       ; astate= AbductiveDomain.set_isl_status ISLError astate }) ) ) )
         invalid_addr_callers (Ok astate)
 
 

infer/src/pulse/PulseInterproc.mli

@@ -17,5 +17,4 @@ val apply_prepost :
   -> formals:Var.t list
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> AbductiveDomain.t
-  -> (AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) PulseReport.access_result
-     SatUnsat.t
+  -> (AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) AccessResult.t SatUnsat.t

infer/src/pulse/PulseLatentIssue.ml

@@ -29,19 +29,23 @@ let add_call call_and_loc = function
       ReadUninitializedValue {read with calling_context= call_and_loc :: read.calling_context}
 
 
-let should_report (astate : AbductiveDomain.summary) =
+let is_manifest (astate : AbductiveDomain.summary) =
   Arithmetic.has_no_assumptions (astate :> AbductiveDomain.t)
 
 
 (* require a summary because we don't want to stop reporting because some non-abducible condition is
    not true as calling context cannot possibly influence such conditions *)
-let should_report_diagnostic (astate : AbductiveDomain.summary) (diagnostic : Diagnostic.t) =
-  match diagnostic with
-  | MemoryLeak _ | StackVariableAddressEscape _ ->
-      (* these issues are reported regardless of the calling context, not sure if that's the right
-         decision yet *)
-      `ReportNow
-  | AccessToInvalidAddress diag ->
-      if should_report astate then `ReportNow else `DelayReport (AccessToInvalidAddress diag)
-  | ReadUninitializedValue diag ->
-      if should_report astate then `ReportNow else `DelayReport (ReadUninitializedValue diag)
+let should_report (access_error : AbductiveDomain.summary PulseAccessResult.error) =
+  match access_error with
+  | ReportableError {astate; diagnostic} -> (
+    match diagnostic with
+    | MemoryLeak _ | StackVariableAddressEscape _ ->
+        (* these issues are reported regardless of the calling context, not sure if that's the right
+           decision yet *)
+        `ReportNow (astate, diagnostic)
+    | AccessToInvalidAddress latent ->
+        if is_manifest astate then `ReportNow (astate, diagnostic)
+        else `DelayReport (astate, AccessToInvalidAddress latent)
+    | ReadUninitializedValue latent ->
+        if is_manifest astate then `ReportNow (astate, diagnostic)
+        else `DelayReport (astate, ReadUninitializedValue latent) )

infer/src/pulse/PulseLatentIssue.mli

@@ -20,9 +20,9 @@ type t =
 
 val to_diagnostic : t -> Diagnostic.t
 
-val should_report : AbductiveDomain.summary -> bool
-
-val should_report_diagnostic :
-  AbductiveDomain.summary -> Diagnostic.t -> [`ReportNow | `DelayReport of t]
+val should_report :
+     AbductiveDomain.summary PulseAccessResult.error
+  -> [> `DelayReport of AbductiveDomain.summary * t
+     | `ReportNow of AbductiveDomain.summary * Diagnostic.t ]
 
 val add_call : CallEvent.t * Location.t -> t -> t

infer/src/pulse/PulseModels.ml

@@ -18,7 +18,7 @@ type model =
   -> Location.t
   -> ret:Ident.t * Typ.t
   -> AbductiveDomain.t
-  -> ExecutionDomain.t PulseOperations.access_result list
+  -> ExecutionDomain.t AccessResult.t list
 
 let ok_continue post = [Ok (ContinueProgram post)]
 
@@ -671,9 +671,11 @@ module GenericArrayBackedCollectionIterator = struct
         let invalidation_trace = Trace.Immediate {location; history= []} in
         let access_trace = Trace.Immediate {location; history= snd pointer} in
         Error
-          ( Diagnostic.AccessToInvalidAddress
-              {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace}
-          , astate )
+          (ReportableError
+             { diagnostic=
+                 Diagnostic.AccessToInvalidAddress
+                   {calling_context= []; invalidation= EndIterator; invalidation_trace; access_trace}
+             ; astate })
       else Ok astate
     in
     (* We do not want to create internal array if iterator pointer has an invalid value *)

infer/src/pulse/PulseModels.mli

@@ -14,7 +14,7 @@ type model =
   -> Location.t
   -> ret:Ident.t * Typ.t
   -> AbductiveDomain.t
-  -> ExecutionDomain.t PulseOperations.access_result list
+  -> ExecutionDomain.t AccessResult.t list
 
 val dispatch :
      Tenv.t

infer/src/pulse/PulseOperations.ml

@@ -15,14 +15,15 @@ type t = AbductiveDomain.t
 module Import = struct
   type access_mode = Read | Write | NoAccess
 
-  type 'abductive_domain_t base_t = 'abductive_domain_t ExecutionDomain.base_t =
+  type 'abductive_domain_t execution_domain_base_t = 'abductive_domain_t ExecutionDomain.base_t =
     | ContinueProgram of 'abductive_domain_t
     | ExitProgram of AbductiveDomain.summary
     | AbortProgram of AbductiveDomain.summary
     | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
     | ISLLatentMemoryError of 'abductive_domain_t
 
-  type 'a access_result = 'a PulseReport.access_result
+  type 'astate base_error = 'astate AccessResult.error =
+    | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
 
   include IResult.Let_syntax
 
@@ -39,15 +40,20 @@ let check_addr_access access_mode location (address, history) astate =
   let* astate =
     AddressAttributes.check_valid access_trace address astate
     |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
-           ( Diagnostic.AccessToInvalidAddress
-               {calling_context= []; invalidation; invalidation_trace; access_trace}
-           , astate ) )
+           ReportableError
+             { diagnostic=
+                 Diagnostic.AccessToInvalidAddress
+                   {calling_context= []; invalidation; invalidation_trace; access_trace}
+             ; astate } )
   in
   match access_mode with
   | Read ->
       AddressAttributes.check_initialized access_trace address astate
       |> Result.map_error ~f:(fun () ->
-             (Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}, astate) )
+             ReportableError
+               { diagnostic=
+                   Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
+               ; astate } )
   | Write ->
       Ok (AbductiveDomain.initialize address astate)
   | NoAccess ->
@@ -60,17 +66,21 @@ let check_and_abduce_addr_access_isl access_mode location (address, history) ?(n
   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 ) ]
+          (ReportableError
+             { diagnostic=
+                 Diagnostic.AccessToInvalidAddress
+                   {calling_context= []; invalidation; invalidation_trace; access_trace}
+             ; astate }) ]
   | Ok astates -> (
     match access_mode with
     | Read ->
         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 ) ) )
+                   ReportableError
+                     { diagnostic=
+                         Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace}
+                     ; astate= AbductiveDomain.set_isl_status ISLError astate } ) )
     | Write ->
         List.map astates ~f:(fun astate ->
             match astate.AbductiveDomain.isl_status with
@@ -435,9 +445,11 @@ let check_address_escape escape_location proc_desc address history astate =
                    (* The returned address corresponds to a C++ temporary. It will have gone out of
                       scope by now except if it was bound to a global. *)
                    Error
-                     ( Diagnostic.StackVariableAddressEscape
-                         {variable; location= escape_location; history}
-                     , astate )
+                     (ReportableError
+                        { diagnostic=
+                            Diagnostic.StackVariableAddressEscape
+                              {variable; location= escape_location; history}
+                        ; astate })
                | _ ->
                    Ok () ) )
   in
@@ -454,8 +466,11 @@ let check_address_escape escape_location proc_desc address history astate =
           L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable
             AbstractValue.pp address ;
           Error
-            ( Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}
-            , astate ) )
+            (ReportableError
+               { diagnostic=
+                   Diagnostic.StackVariableAddressEscape
+                     {variable; location= escape_location; history}
+               ; astate }) )
         else Ok () )
   in
   let+ () = check_address_of_cpp_temporary () >>= check_address_of_stack_variable in
@@ -486,7 +501,10 @@ let check_memory_leak_unreachable unreachable_addrs location astate =
     match allocated_not_freed_opt with
     | Some (procname, trace), false ->
         (* allocated but not freed *)
-        Error (Diagnostic.MemoryLeak {procname; location; allocation_trace= trace}, astate)
+        Error
+          (ReportableError
+             { diagnostic= Diagnostic.MemoryLeak {procname; location; allocation_trace= trace}
+             ; astate })
     | _ ->
         result
   in
@@ -655,15 +673,19 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
               Ok (AbortProgram astate_summary)
           | ExitProgram _ ->
               Ok (ExitProgram astate_summary)
-          | LatentAbortProgram {latent_issue} ->
+          | LatentAbortProgram {latent_issue} -> (
               let latent_issue =
                 LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue
               in
-              if LatentIssue.should_report astate_summary then
-                Error
-                  ( LatentIssue.to_diagnostic latent_issue
-                  , (astate_summary : AbductiveDomain.summary :> AbductiveDomain.t) )
-              else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) )
+              let error =
+                ReportableError
+                  {diagnostic= LatentIssue.to_diagnostic latent_issue; astate= astate_summary}
+              in
+              match LatentIssue.should_report error with
+              | `DelayReport (astate, latent_issue) ->
+                  Ok (LatentAbortProgram {astate; latent_issue})
+              | `ReportNow (astate, diagnostic) ->
+                  Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)}) ) )
 
 
 let get_captured_actuals location ~captured_vars ~actual_closure astate =

infer/src/pulse/PulseOperations.mli

@@ -22,26 +22,30 @@ module Import : sig
   (** {2 Imported types for ease of use and so we can write variants without the corresponding
       module prefix} *)
 
-  type 'abductive_domain_t base_t = 'abductive_domain_t ExecutionDomain.base_t =
+  type 'abductive_domain_t execution_domain_base_t = 'abductive_domain_t ExecutionDomain.base_t =
     | ContinueProgram of 'abductive_domain_t
     | ExitProgram of AbductiveDomain.summary
     | AbortProgram of AbductiveDomain.summary
     | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
     | ISLLatentMemoryError of 'abductive_domain_t
 
-  type 'a access_result = 'a PulseReport.access_result
+  type 'astate base_error = 'astate AccessResult.error =
+    | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t}
 
   (** {2 Monadic syntax} *)
 
   include module type of IResult.Let_syntax
 
-  val ( let<*> ) : 'a access_result -> ('a -> 'b access_result list) -> 'b access_result list
-  (** monadic "bind" but not really that turns an [access_result] into a list of [access_result]s
-      (not really because the first type is not an [access_result list] but just an [access_result]) *)
+  val ( let<*> ) : 'a AccessResult.t -> ('a -> 'b AccessResult.t list) -> 'b AccessResult.t list
+  (** monadic "bind" but not really that turns an [AccessResult.t] into a list of [AccessResult.t]s
+      (not really because the first type is not an [AccessResult.t list] but just an
+      [AccessResult.t]) *)
 
   val ( let<+> ) :
-    'a access_result -> ('a -> 'abductive_domain_t) -> 'abductive_domain_t base_t access_result list
-  (** monadic "map" but even less really that turns an [access_result] into an analysis result *)
+       'a AccessResult.t
+    -> ('a -> 'abductive_domain_t)
+    -> 'abductive_domain_t execution_domain_base_t AccessResult.t list
+  (** monadic "map" but even less really that turns an [AccessResult.t] into an analysis result *)
 end
 
 include module type of Import
@@ -49,16 +53,16 @@ include module type of Import
 type t = AbductiveDomain.t
 
 val check_addr_access :
-  access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
+  access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t
 (** Check that the [address] is not known to be invalid *)
 
 module Closures : sig
-  val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result
+  val check_captured_addresses : Location.t -> AbstractValue.t -> t -> t AccessResult.t
   (** assert the validity of the addresses captured by the lambda *)
 end
 
 val eval :
-  access_mode -> Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
+  access_mode -> Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
 (** Use the stack and heap to evaluate the given expression down to an abstract address representing
     its value.
 
@@ -70,17 +74,17 @@ val eval_structure_isl :
   -> Location.t
   -> Exp.t
   -> t
-  -> (bool * (t * (AbstractValue.t * ValueHistory.t)) access_result list) access_result
+  -> (bool * (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list) AccessResult.t
 (** 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. *)
 
-val prune : Location.t -> condition:Exp.t -> t -> t access_result
+val prune : Location.t -> condition:Exp.t -> t -> t AccessResult.t
 
-val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
+val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
 (** Like [eval] but evaluates [*exp]. *)
 
 val eval_deref_isl :
-  Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result list
+  Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list
 
 val eval_access :
      access_mode
@@ -88,7 +92,7 @@ val eval_access :
   -> AbstractValue.t * ValueHistory.t
   -> BaseMemory.Access.t
   -> t
-  -> (t * (AbstractValue.t * ValueHistory.t)) access_result
+  -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
 (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if
     so dereferences it according to the access. *)
 
@@ -100,7 +104,7 @@ val havoc_field :
   -> Fieldname.t
   -> ValueHistory.t
   -> t
-  -> t access_result
+  -> t AccessResult.t
 
 val realloc_pvar : Tenv.t -> Pvar.t -> Typ.t -> Location.t -> t -> t
 
@@ -112,7 +116,7 @@ val write_field :
   -> Fieldname.t
   -> obj:AbstractValue.t * ValueHistory.t
   -> t
-  -> t access_result
+  -> t AccessResult.t
 (** write the edge [ref --.field--> obj] *)
 
 val write_arr_index :
@@ -121,7 +125,7 @@ val write_arr_index :
   -> index:AbstractValue.t
   -> obj:AbstractValue.t * ValueHistory.t
   -> t
-  -> t access_result
+  -> t AccessResult.t
 (** write the edge [ref\[index\]--> obj] *)
 
 val write_deref :
@@ -129,7 +133,7 @@ val write_deref :
   -> ref:AbstractValue.t * ValueHistory.t
   -> obj:AbstractValue.t * ValueHistory.t
   -> t
-  -> t access_result
+  -> t AccessResult.t
 (** write the edge [ref --*--> obj] *)
 
 val write_deref_biad_isl :
@@ -138,14 +142,14 @@ val write_deref_biad_isl :
   -> AbstractValue.t HilExp.Access.t
   -> obj:AbstractValue.t * ValueHistory.t
   -> t
-  -> t access_result list
+  -> t AccessResult.t list
 
 val invalidate :
-  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
+  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t
 (** record that the address is invalid *)
 
 val invalidate_biad_isl :
-  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result list
+  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t 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. *)
 
@@ -161,28 +165,28 @@ val invalidate_access :
   -> AbstractValue.t * ValueHistory.t
   -> BaseMemory.Access.t
   -> t
-  -> t access_result
+  -> t AccessResult.t
 (** record that what the address points via the access to is invalid *)
 
 val invalidate_array_elements :
-  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
+  Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t
 (** record that all the array elements that address points to is invalid *)
 
 val shallow_copy :
      Location.t
   -> AbstractValue.t * ValueHistory.t
   -> t
-  -> (t * (AbstractValue.t * ValueHistory.t)) access_result
+  -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t
 (** returns the address of a new cell with the same edges as the original *)
 
 val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.t) list
 (** Given a list of variables, computes the unreachable values if the variables were removed from
     the stack, then return the dynamic types of those values if they are available *)
 
-val remove_vars : Tenv.t -> Var.t list -> Location.t -> t -> t access_result
+val remove_vars : Tenv.t -> Var.t list -> Location.t -> t -> t AccessResult.t
 
 val check_address_escape :
-  Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result
+  Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t
 
 val call :
      Tenv.t
@@ -194,7 +198,7 @@ val call :
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> formals_opt:(Pvar.t * Typ.t) list option
   -> t
-  -> ExecutionDomain.t access_result list
+  -> ExecutionDomain.t AccessResult.t list
 (** perform an interprocedural call: apply the summary for the call proc name passed as argument if
     it exists *)
 

infer/src/pulse/PulseReport.ml

@@ -8,8 +8,7 @@
 open! IStd
 open PulseBasicInterface
 open PulseDomainInterface
-
-type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result
+open PulseOperations.Import
 
 let report ?(extra_trace = []) proc_desc err_log diagnostic =
   let open Diagnostic in
@@ -31,7 +30,7 @@ let report_latent_issue proc_desc err_log latent_issue =
   report ~extra_trace proc_desc err_log diagnostic
 
 
-let suppress_error tenv proc_desc diagnostic =
+let is_suppressed tenv proc_desc diagnostic =
   match Procdesc.get_proc_name proc_desc with
   | Procname.Java jn
     when (not Config.pulse_nullsafe_report_npe)
@@ -42,40 +41,33 @@ let suppress_error tenv proc_desc diagnostic =
       false
 
 
-let report_error tenv proc_desc err_log access_result =
-  let open SatUnsat.Import in
-  Result.map_error access_result ~f:(fun (diagnostic, astate) ->
-      let+ astate_summary = AbductiveDomain.summary_of_post tenv proc_desc astate in
-      let is_suppressed = suppress_error tenv proc_desc diagnostic in
-      match LatentIssue.should_report_diagnostic astate_summary diagnostic with
-      | `ReportNow ->
-          if not is_suppressed then report proc_desc err_log diagnostic ;
-          ExecutionDomain.AbortProgram astate_summary
-      | `DelayReport latent_issue ->
-          if Config.pulse_report_latent_issues && not is_suppressed then
-            report_latent_issue proc_desc err_log latent_issue ;
-          ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} )
-
-
-let post_of_report_result = function
-  | Ok post ->
-      Some post
-  | Error Unsat ->
-      None
-  | Error (Sat post) ->
-      Some post
+let report_error tenv proc_desc err_log access_error =
+  match LatentIssue.should_report access_error with
+  | `ReportNow (astate_summary, diagnostic) ->
+      if not (is_suppressed tenv proc_desc diagnostic) then report proc_desc err_log diagnostic ;
+      AbortProgram astate_summary
+  | `DelayReport (astate, latent_issue) ->
+      if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ;
+      LatentAbortProgram {astate; latent_issue}
 
 
 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 )
+      match exec_result with
+      | Ok post ->
+          Some post
+      | Error error -> (
+        match AccessResult.to_summary tenv proc_desc error with
+        | Unsat ->
+            None
+        | Sat error ->
+            Some (report_error tenv proc_desc err_log error) ) )
 
 
 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 )
+      ContinueProgram astate )
   |> report_exec_results analysis_data
 
 

infer/src/pulse/PulseReport.mli

@@ -6,22 +6,19 @@
  *)
 
 open! IStd
-open PulseBasicInterface
 open PulseDomainInterface
 
-type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result
-
 val report_result :
      PulseSummary.t InterproceduralAnalysis.t
-  -> AbductiveDomain.t access_result
+  -> AbductiveDomain.t AccessResult.t
   -> ExecutionDomain.t list
 
 val report_results :
      PulseSummary.t InterproceduralAnalysis.t
-  -> AbductiveDomain.t access_result list
+  -> AbductiveDomain.t AccessResult.t list
   -> ExecutionDomain.t list
 
 val report_exec_results :
      PulseSummary.t InterproceduralAnalysis.t
-  -> ExecutionDomain.t access_result list
+  -> ExecutionDomain.t AccessResult.t list
   -> ExecutionDomain.t list