From 3aaa28f99338c3cc64f74bbb1547094538df7301 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 8 Mar 2021 05:02:39 -0800 Subject: [PATCH] [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 | 23 +++++++++ infer/src/pulse/PulseAccessResult.mli | 19 +++++++ infer/src/pulse/PulseDomainInterface.ml | 3 ++ infer/src/pulse/PulseInterproc.ml | 22 +++++--- infer/src/pulse/PulseInterproc.mli | 3 +- infer/src/pulse/PulseLatentIssue.ml | 26 ++++++---- infer/src/pulse/PulseLatentIssue.mli | 8 +-- infer/src/pulse/PulseModels.ml | 10 ++-- infer/src/pulse/PulseModels.mli | 2 +- infer/src/pulse/PulseOperations.ml | 68 ++++++++++++++++--------- infer/src/pulse/PulseOperations.mli | 60 ++++++++++++---------- infer/src/pulse/PulseReport.ml | 48 ++++++++--------- infer/src/pulse/PulseReport.mli | 9 ++-- 13 files changed, 186 insertions(+), 115 deletions(-) create mode 100644 infer/src/pulse/PulseAccessResult.ml create mode 100644 infer/src/pulse/PulseAccessResult.mli diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml new file mode 100644 index 000000000..a222f5735 --- /dev/null +++ b/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} diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli new file mode 100644 index 000000000..31ad1f28c --- /dev/null +++ b/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 diff --git a/infer/src/pulse/PulseDomainInterface.ml b/infer/src/pulse/PulseDomainInterface.ml index d49e9c972..1c9d88ced 100644 --- a/infer/src/pulse/PulseDomainInterface.ml +++ b/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"] diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 5fd8fcf86..7714538c4 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/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) diff --git a/infer/src/pulse/PulseInterproc.mli b/infer/src/pulse/PulseInterproc.mli index 6ecdcd0a9..0b81c84f4 100644 --- a/infer/src/pulse/PulseInterproc.mli +++ b/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 diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml index 1387a47c6..caa873d02 100644 --- a/infer/src/pulse/PulseLatentIssue.ml +++ b/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) ) diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli index c150a18e7..9cee78081 100644 --- a/infer/src/pulse/PulseLatentIssue.mli +++ b/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 diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index b5192b920..fcaa8feb2 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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 *) diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 3c2cc11dd..3844cd92a 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 41b92b523..f929399a1 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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 = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 8c5de9dbb..727c1c5c5 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/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 *) diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index d959bf809..8c25d9f67 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/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 diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index 279c16892..bb0416a26 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/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