From 341c08d9fd5fddf08c5d8fd803e9aedac97c163d Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 8 Mar 2021 05:02:49 -0800 Subject: [PATCH] [pulse] change ISLOk/ISLError inside states into actual Ok/Error outside states Summary: This changes the results. I think it's because we cut short paths to ISL errors sooner now, before they are duplicated and moved. I could not really assess what was going on though so could be wrong. On OpenSSL 1.0.2d: Before: 106 issues After: 90 issues Reviewed By: ezgicicek Differential Revision: D26822331 fbshipit-source-id: e861e7fc2 --- infer/src/checkers/impurity.ml | 4 +- infer/src/pulse/Pulse.ml | 14 +-- infer/src/pulse/PulseAbductiveDomain.ml | 53 +++------- infer/src/pulse/PulseAbductiveDomain.mli | 16 +-- infer/src/pulse/PulseAccessResult.ml | 7 +- infer/src/pulse/PulseAccessResult.mli | 4 +- infer/src/pulse/PulseExecutionDomain.ml | 28 +++--- infer/src/pulse/PulseExecutionDomain.mli | 2 +- infer/src/pulse/PulseInterproc.ml | 79 ++++++++------- infer/src/pulse/PulseInterproc.mli | 3 +- infer/src/pulse/PulseLatentIssue.ml | 2 + infer/src/pulse/PulseLatentIssue.mli | 3 +- infer/src/pulse/PulseOperations.ml | 122 ++++++++++------------- infer/src/pulse/PulseOperations.mli | 3 +- infer/src/pulse/PulseReport.ml | 2 + 15 files changed, 148 insertions(+), 194 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index b9bf8abc9..db201fc11 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -164,9 +164,9 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur match exec_state with | ExitProgram astate -> ((astate :> AbductiveDomain.t), true) - | ContinueProgram astate | ISLLatentMemoryError astate -> + | ContinueProgram astate -> (astate, false) - | AbortProgram astate | LatentAbortProgram {astate} -> + | AbortProgram astate | LatentAbortProgram {astate} | ISLLatentMemoryError astate -> ((astate :> AbductiveDomain.t), false) in let pre_heap = (AbductiveDomain.get_pre astate).BaseDomain.heap in diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 652eb49f6..fbcda66b1 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -268,13 +268,7 @@ module PulseTransferFunctions = struct | ExitProgram _ -> (* program already exited, simply propagate the exited state upwards *) [astate] - | ContinueProgram ({isl_status= ISLError} as astate) -> ( - match instr with - | Prune (_, _, is_then_branch, _) when is_then_branch -> - [] - | _ -> - [ContinueProgram astate] ) - | ContinueProgram ({isl_status= ISLOk} as astate) -> ( + | ContinueProgram astate -> ( match instr with | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) @@ -315,11 +309,7 @@ module PulseTransferFunctions = struct 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 -> - write_function lhs_addr_hist astate - | true, ISLError -> - [Ok astate] ) + write_function lhs_addr_hist astate ) in let astates = if Topl.is_deep_active () then diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 28fd2093e..394cb4cc2 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -89,42 +89,25 @@ end (** represents the inferred pre-condition at each program point, biabduction style *) module PreDomain : BaseDomainSig = PostDomain -type isl_status = ISLOk | ISLError [@@deriving compare, equal, yojson_of] - -let pp_isl_status f s = - if Config.pulse_isl then - match s with - | ISLOk -> - F.pp_print_string f "ISLOk:" - | ISLError -> - F.pp_print_string f "ISLError:" - else () - - (* see documentation in this file's .mli *) type t = { post: PostDomain.t ; pre: PreDomain.t ; path_condition: PathCondition.t ; topl: (PulseTopl.state[@yojson.opaque]) - ; skipped_calls: SkippedCalls.t - ; isl_status: isl_status } + ; skipped_calls: SkippedCalls.t } [@@deriving compare, equal, yojson_of] -let pp f {post; pre; topl; path_condition; skipped_calls; isl_status} = - F.fprintf f "@[%a@;%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp - path_condition pp_isl_status isl_status PostDomain.pp post PreDomain.pp pre SkippedCalls.pp - skipped_calls PulseTopl.pp_state topl +let pp f {post; pre; topl; path_condition; skipped_calls} = + F.fprintf f "@[%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition + PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl -let set_isl_status status astate = {astate with isl_status= status} - let set_path_condition path_condition astate = {astate with path_condition} let leq ~lhs ~rhs = phys_equal lhs rhs || SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls - && ((not Config.pulse_isl) || equal_isl_status lhs.isl_status rhs.isl_status) && PathCondition.equal lhs.path_condition rhs.path_condition && match @@ -198,8 +181,7 @@ module Stack = struct ; pre ; topl= astate.topl ; skipped_calls= astate.skipped_calls - ; path_condition= astate.path_condition - ; isl_status= astate.isl_status } + ; path_condition= astate.path_condition } , addr_hist ) @@ -379,16 +361,13 @@ module AddressAttributes = struct let null_attr = Attribute.Invalid (Invalidation.ConstantDereference IntLit.zero, access_trace) in - let null_astate = - {astate with isl_status= (if null_noop then astate.isl_status else ISLError)} - |> add_one addr null_attr - in + let null_astate = add_one addr null_attr astate in let null_astate = if is_eq_null then null_astate else abduce_attribute addr null_attr null_astate in - [null_astate] + if null_noop then [Ok null_astate] else [Error (`ISLError null_astate)] in - if is_eq_null then Ok null_astates + if is_eq_null then null_astates else let valid_astate = let abdalloc = Attribute.ISLAbduced access_trace in @@ -399,15 +378,13 @@ module AddressAttributes = struct let invalid_free = (*C or Cpp?*) let invalid_attr = Attribute.Invalid (CFree, access_trace) in - {astate with isl_status= ISLError} - |> abduce_attribute addr invalid_attr - |> add_one addr invalid_attr + abduce_attribute addr invalid_attr astate |> add_one addr invalid_attr in - Ok ([valid_astate; invalid_free] @ null_astates) + Ok valid_astate :: Error (`ISLError invalid_free) :: null_astates | Some _ -> - Ok [astate] ) + [Ok astate] ) | Some (invalidation, invalidation_trace) -> - Error (invalidation, invalidation_trace, {astate with isl_status= ISLError}) + [Error (`InvalidAccess (invalidation, invalidation_trace, astate))] end module Memory = struct @@ -451,8 +428,7 @@ module Memory = struct ; pre= PreDomain.update astate.pre ~heap:foot_heap ; topl= astate.topl ; skipped_calls= astate.skipped_calls - ; path_condition= astate.path_condition - ; isl_status= astate.isl_status } + ; path_condition= astate.path_condition } , addr_hist_dst ) @@ -587,8 +563,7 @@ let mk_initial tenv proc_desc = ; post ; topl= PulseTopl.start () ; skipped_calls= SkippedCalls.empty - ; path_condition= PathCondition.true_ - ; isl_status= ISLOk } + ; path_condition= PathCondition.true_ } let add_skipped_call pname trace astate = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index f770d83cd..5a6959691 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -54,16 +54,6 @@ module PostDomain : BaseDomainSig collapse into one. * *) module PreDomain : BaseDomainSig -(** Execution status, similar to {!PulseExecutionDomain} but for ISL (Incorrectness Separation - Logic) mode, where {!PulseExecutionDomain.ContinueProgram} can also contain "error specs" that - describe what happens when some addresses are invalid explicitly instead of relying on - [MustBeValid] attributes. *) -type isl_status = - | ISLOk (** ok triple: the program executes without error *) - | ISLError - (** Error specification: an invalid address recorded in the precondition will cause an error *) -[@@deriving equal] - (** pre/post on a single program path *) type t = private { post: PostDomain.t (** state at the current program point*) @@ -74,15 +64,13 @@ type t = private ; topl: PulseTopl.state (** state at of the Topl monitor at the current program point, when Topl is enabled *) ; skipped_calls: SkippedCalls.t (** metadata: procedure calls for which no summary was found *) - ; isl_status: isl_status } + } [@@deriving equal] val leq : lhs:t -> rhs:t -> bool val pp : Format.formatter -> t -> unit -val set_isl_status : isl_status -> t -> t - val mk_initial : Tenv.t -> Procdesc.t -> t val get_pre : t -> BaseDomain.t @@ -176,7 +164,7 @@ module AddressAttributes : sig -> AbstractValue.t -> ?null_noop:bool -> t - -> (t list, Invalidation.t * Trace.t * t) result + -> (t, [> `ISLError of t | `InvalidAccess of Invalidation.t * Trace.t * t]) result list end val is_local : Var.t -> t -> bool diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml index a222f5735..41f82d3aa 100644 --- a/infer/src/pulse/PulseAccessResult.ml +++ b/infer/src/pulse/PulseAccessResult.ml @@ -9,7 +9,9 @@ open! IStd open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain -type 'astate error = ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} +type 'astate error = + | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ISLError of 'astate type ('a, 'astate) base_t = ('a, 'astate error) result @@ -21,3 +23,6 @@ let to_summary tenv proc_desc error = | ReportableError {astate; diagnostic} -> let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in ReportableError {astate; diagnostic} + | ISLError astate -> + let+ astate = AbductiveDomain.summary_of_post tenv proc_desc astate in + ISLError astate diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli index 31ad1f28c..0719d34e6 100644 --- a/infer/src/pulse/PulseAccessResult.mli +++ b/infer/src/pulse/PulseAccessResult.mli @@ -9,7 +9,9 @@ open! IStd open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain -type 'astate error = ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} +type 'astate error = + | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ISLError of 'astate type ('a, 'astate) base_t = ('a, 'astate error) result diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index b0e388440..86810e033 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -21,7 +21,7 @@ type 'abductive_domain_t base_t = | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} - | ISLLatentMemoryError of 'abductive_domain_t + | ISLLatentMemoryError of AbductiveDomain.summary [@@deriving equal, compare, yojson_of] type t = AbductiveDomain.t base_t @@ -34,10 +34,11 @@ let leq ~lhs ~rhs = phys_equal lhs rhs || match (lhs, rhs) with - | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> - AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) - | ContinueProgram astate1, ContinueProgram astate2 + | AbortProgram astate1, AbortProgram astate2 + | ExitProgram astate1, ExitProgram astate2 | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 -> + AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) + | ContinueProgram astate1, ContinueProgram astate2 -> AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 | ( LatentAbortProgram {astate= astate1; latent_issue= issue1} , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) -> @@ -51,7 +52,7 @@ let pp fmt = function | ContinueProgram astate -> AbductiveDomain.pp fmt astate | ISLLatentMemoryError astate -> - F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp astate + F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | ExitProgram astate -> F.fprintf fmt "{ExitProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | AbortProgram astate -> @@ -68,9 +69,12 @@ let pp fmt = function (* do not export this function as there lies wickedness: clients should generally care about what kind of state they are manipulating so let's not encourage them not to *) let get_astate : t -> AbductiveDomain.t = function - | ContinueProgram astate | ISLLatentMemoryError astate -> + | ContinueProgram astate -> astate - | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} -> + | ExitProgram astate + | AbortProgram astate + | LatentAbortProgram {astate} + | ISLLatentMemoryError astate -> (astate :> AbductiveDomain.t) @@ -79,7 +83,7 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] let summary_of_post_common tenv ~continue_program proc_desc = function - | ContinueProgram astate | ISLLatentMemoryError astate -> ( + | ContinueProgram astate -> ( match AbductiveDomain.summary_of_post tenv proc_desc astate with | Unsat -> None @@ -92,17 +96,15 @@ let summary_of_post_common tenv ~continue_program proc_desc = function Some (ExitProgram astate) | LatentAbortProgram {astate; latent_issue} -> Some (LatentAbortProgram {astate; latent_issue}) + | ISLLatentMemoryError astate -> + Some (ISLLatentMemoryError astate) let summary_of_posts tenv proc_desc posts = List.filter_mapi posts ~f:(fun i exec_state -> L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate -> - match (astate :> AbductiveDomain.t).isl_status with - | ISLOk -> - ContinueProgram astate - | ISLError -> - ISLLatentMemoryError astate ) ) + ContinueProgram astate ) ) let force_exit_program tenv proc_desc post = diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 8999062b4..8a642a794 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -17,7 +17,7 @@ type 'abductive_domain_t base_t = (** represents the state at the program point that caused an error *) | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} (** this path leads to an error but we don't have conclusive enough data to report it yet *) - | ISLLatentMemoryError of 'abductive_domain_t + | ISLLatentMemoryError of AbductiveDomain.summary (** represents the state at the program point that might cause an error; used for {!Config.pulse_isl} *) diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 7714538c4..0f406a9ca 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -637,43 +637,39 @@ let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location {AbductiveDomain.pre; _} pre_astate astate = - match astate.AbductiveDomain.isl_status with - | ISLOk -> - Ok astate - | ISLError -> - AbstractValue.Map.fold - (fun addr_pre (addr_caller, hist_caller) astate_result -> - let mk_access_trace callee_access_trace = - Trace.ViaCall - { in_call= callee_access_trace - ; f= Call callee_proc_name - ; location= call_location - ; history= hist_caller } - in - match astate_result with - | Error _ -> + AbstractValue.Map.fold + (fun addr_pre (addr_caller, hist_caller) astate_result -> + let mk_access_trace callee_access_trace = + Trace.ViaCall + { in_call= callee_access_trace + ; f= Call callee_proc_name + ; location= call_location + ; history= hist_caller } + in + match astate_result with + | Error _ -> + astate_result + | Ok astate -> ( + match + BaseAddressAttributes.get_invalid addr_caller + (pre_astate.AbductiveDomain.post :> BaseDomain.t).attrs + with + | None -> + astate_result + | Some (invalidation, invalidation_trace) -> ( + match BaseAddressAttributes.get_invalid addr_pre (pre :> BaseDomain.t).attrs with + | None -> astate_result - | Ok astate -> ( - match - BaseAddressAttributes.get_invalid addr_caller - (pre_astate.AbductiveDomain.post :> BaseDomain.t).attrs - with - | None -> - astate_result - | Some (invalidation, invalidation_trace) -> ( - match BaseAddressAttributes.get_invalid addr_pre (pre :> BaseDomain.t).attrs with - | None -> - astate_result - | Some (_, callee_access_trace) -> - let access_trace = mk_access_trace callee_access_trace in - L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; - Error - (AccessResult.ReportableError - { diagnostic= - Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} - ; astate= AbductiveDomain.set_isl_status ISLError astate }) ) ) ) - invalid_addr_callers (Ok astate) + | Some (_, callee_access_trace) -> + let access_trace = mk_access_trace callee_access_trace in + L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; + Error + (AccessResult.ReportableError + { diagnostic= + Diagnostic.AccessToInvalidAddress + {calling_context= []; invalidation; invalidation_trace; access_trace} + ; astate }) ) ) ) + invalid_addr_callers (Ok astate) (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff @@ -690,7 +686,7 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location the noise that this will introduce since we don't care about values. For instance, if the pre is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is to bake in some value analysis. *) -let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post +let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post ~captured_vars_with_actuals ~formals ~actuals astate = L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name (Pp.seq ~sep:"," Var.pp) formals AbductiveDomain.pp pre_post ; @@ -718,10 +714,13 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; match let open IResult.Let_syntax in + (* only call [check_all_valid] when ISL is not active: the ISL mode generates explicit error + specs (which we recognize here using [is_isl_error_prepost]) instead of relying on + [check_all_valid], whereas the "normal" mode encodes some error specs implicitly in the + ContinueProgram ok specs *) let* astate = if Config.pulse_isl then - Ok - (AbductiveDomain.set_isl_status pre_post.AbductiveDomain.isl_status call_state.astate) + if is_isl_error_prepost then Error (AccessResult.ISLError astate) else Ok astate else check_all_valid callee_proc_name call_location pre_post call_state in (* reset [visited] *) @@ -741,7 +740,7 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post else call_state.astate in let+ astate = - if Config.pulse_isl then + if is_isl_error_prepost then isl_check_all_invalid invalid_subst callee_proc_name call_location pre_post pre_astate astate else Ok astate diff --git a/infer/src/pulse/PulseInterproc.mli b/infer/src/pulse/PulseInterproc.mli index 0b81c84f4..3b5ae76f8 100644 --- a/infer/src/pulse/PulseInterproc.mli +++ b/infer/src/pulse/PulseInterproc.mli @@ -10,7 +10,8 @@ open PulseBasicInterface open PulseDomainInterface val apply_prepost : - Procname.t + is_isl_error_prepost:bool + -> Procname.t -> Location.t -> callee_prepost:AbductiveDomain.t -> captured_vars_with_actuals:(Var.t * (AbstractValue.t * ValueHistory.t)) list diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml index caa873d02..04d3014ef 100644 --- a/infer/src/pulse/PulseLatentIssue.ml +++ b/infer/src/pulse/PulseLatentIssue.ml @@ -49,3 +49,5 @@ let should_report (access_error : AbductiveDomain.summary PulseAccessResult.erro | ReadUninitializedValue latent -> if is_manifest astate then `ReportNow (astate, diagnostic) else `DelayReport (astate, ReadUninitializedValue latent) ) + | ISLError astate -> + `ISLDelay astate diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli index 9cee78081..f76a086b8 100644 --- a/infer/src/pulse/PulseLatentIssue.mli +++ b/infer/src/pulse/PulseLatentIssue.mli @@ -23,6 +23,7 @@ val to_diagnostic : t -> Diagnostic.t val should_report : AbductiveDomain.summary PulseAccessResult.error -> [> `DelayReport of AbductiveDomain.summary * t - | `ReportNow of AbductiveDomain.summary * Diagnostic.t ] + | `ReportNow of AbductiveDomain.summary * Diagnostic.t + | `ISLDelay of AbductiveDomain.summary ] val add_call : CallEvent.t * Location.t -> t -> t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index f929399a1..b41d9bf67 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -20,10 +20,11 @@ module Import = struct | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} - | ISLLatentMemoryError of 'abductive_domain_t + | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ISLError of 'astate include IResult.Let_syntax @@ -63,33 +64,31 @@ 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 - match AddressAttributes.check_valid_isl access_trace address ~null_noop astate with - | Error (invalidation, invalidation_trace, astate) -> - [ Error - (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 () -> - 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 - | ISLOk -> - Ok (AbductiveDomain.initialize address astate) - | ISLError -> - Ok astate ) - | NoAccess -> - List.map ~f:(fun astate -> Ok astate) astates ) + AddressAttributes.check_valid_isl access_trace address ~null_noop astate + |> List.map ~f:(function + | Error (`InvalidAccess (invalidation, invalidation_trace, astate)) -> + Error + (ReportableError + { diagnostic= + Diagnostic.AccessToInvalidAddress + {calling_context= []; invalidation; invalidation_trace; access_trace} + ; astate }) + | Error (`ISLError astate) -> + Error (ISLError astate) + | Ok astate -> ( + match access_mode with + | Read -> + AddressAttributes.check_initialized access_trace address astate + |> Result.map_error ~f:(fun () -> + ReportableError + { diagnostic= + Diagnostic.ReadUninitializedValue + {calling_context= []; trace= access_trace} + ; astate } ) + | Write -> + Ok (AbductiveDomain.initialize address astate) + | NoAccess -> + Ok astate ) ) module Closures = struct @@ -175,11 +174,7 @@ let eval_access_biad_isl mode location addr_hist access 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) ) + Memory.eval_edge addr_hist access astate ) in let results = check_and_abduce_addr_access_isl mode location addr_hist astate in map_ok addr_hist access results @@ -290,14 +285,10 @@ let eval_structure_isl mode loc exp astate = 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 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) ) + check_and_abduce_addr_access_isl Read location addr_hist astate + |> List.map ~f:(fun result -> + let+ astate = result in + Memory.eval_edge addr_hist access astate ) let eval_deref_isl location exp astate = @@ -307,12 +298,8 @@ let eval_deref_isl location exp astate = else [eval_deref location exp astate] in List.concat_map ls_astate_addr_hist ~f:(fun result -> - let<*> ((astate, _) as astate_addr) = result in - match astate.AbductiveDomain.isl_status with - | ISLOk -> - eval_deref_function astate_addr - | ISLError -> - [Ok astate_addr] ) + let<*> astate_addr = result in + eval_deref_function astate_addr ) let realloc_pvar tenv pvar typ location astate = @@ -338,14 +325,10 @@ 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 = - 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 astate - | ISLError -> - astate ) + let astates = check_and_abduce_addr_access_isl Write location addr_trace_ref astate in + List.map astates ~f:(fun result -> + let+ astate = result in + Memory.add_edge addr_trace_ref access addr_trace_obj location astate ) let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = @@ -386,11 +369,7 @@ let invalidate_biad_isl location cause (address, history) astate = check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true 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 ) + AddressAttributes.invalidate (address, history) cause location astate ) let invalidate_access location cause ref_addr_hist access astate = @@ -636,10 +615,10 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals ~actuals astate = - let map_call_result callee_prepost ~f = + let map_call_result ~is_isl_error_prepost callee_prepost ~f = match - PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals - ~formals ~actuals astate + PulseInterproc.apply_prepost ~is_isl_error_prepost callee_pname call_loc ~callee_prepost + ~captured_vars_with_actuals ~formals ~actuals astate with | (Sat (Error _) | Unsat) as path_result -> path_result @@ -658,11 +637,10 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state let open SatUnsat.Import in match callee_exec_state with | ContinueProgram astate -> - map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate))) - | ISLLatentMemoryError astate -> - map_call_result astate ~f:(fun astate -> Sat (Ok (ISLLatentMemoryError astate))) + map_call_result ~is_isl_error_prepost:false astate ~f:(fun astate -> + Sat (Ok (ContinueProgram astate)) ) | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} -> - map_call_result + map_call_result ~is_isl_error_prepost:false (astate :> AbductiveDomain.t) ~f:(fun astate -> let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in @@ -685,7 +663,15 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state | `DelayReport (astate, latent_issue) -> Ok (LatentAbortProgram {astate; latent_issue}) | `ReportNow (astate, diagnostic) -> - Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)}) ) ) + Error (ReportableError {diagnostic; astate= (astate :> AbductiveDomain.t)}) + | `ISLDelay astate -> + Error (ISLError (astate :> AbductiveDomain.t)) ) ) + | ISLLatentMemoryError astate -> + map_call_result ~is_isl_error_prepost:true + (astate :> AbductiveDomain.t) + ~f:(fun astate -> + let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in + Ok (ISLLatentMemoryError astate_summary) ) 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 727c1c5c5..66a1bf368 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -27,10 +27,11 @@ module Import : sig | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} - | ISLLatentMemoryError of 'abductive_domain_t + | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ISLError of 'astate (** {2 Monadic syntax} *) diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 8c25d9f67..b7f901914 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -49,6 +49,8 @@ let report_error tenv proc_desc err_log access_error = | `DelayReport (astate, latent_issue) -> if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ; LatentAbortProgram {astate; latent_issue} + | `ISLDelay astate -> + ISLLatentMemoryError astate let report_exec_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results =