From 566102d7f44524b0b53e43941e5162029e183a1c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 6 Jul 2021 03:19:12 -0700 Subject: [PATCH] [pulse] better trace when realising latent invalid accesses Summary: "glue" together the trace from the caller with the trace from the callee to form the access trace when applying LatentInvalidAccess summaries. This is consistent with what happens in function calls and allows Pulse to better keep track of the history of the value. The goal is to prevent bugs from getting filtered out because the access trace doesn't contain the invalidation event for the value. Reviewed By: da319 Differential Revision: D29550320 fbshipit-source-id: b600c188d --- infer/src/pulse/PulseCallOperations.ml | 29 +++++++++++++++++++------- infer/src/pulse/PulseReport.ml | 20 +++++++++++------- infer/src/pulse/PulseSummary.ml | 3 +++ 3 files changed, 36 insertions(+), 16 deletions(-) diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 8773a6d23..e4657244f 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -138,9 +138,9 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s | LatentInvalidAccess {astate} -> map_call_result ~is_isl_error_prepost:false (astate :> AbductiveDomain.t) - ~f:(fun subst astate -> + ~f:(fun subst astate_post_call -> let* astate_summary_result = - ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate + ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate_post_call >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result :> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t ) @@ -168,17 +168,27 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s Sat (Error (ReportableErrorSummary {diagnostic; astate= astate_summary})) | `ISLDelay astate -> Sat (Error (ISLError astate)) ) - | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> ( + | LatentInvalidAccess + { address= address_callee + ; must_be_valid= callee_access_trace, must_be_valid_reason + ; calling_context } -> ( match AbstractValue.Map.find_opt address_callee subst with | None -> (* the address became unreachable so the bug can never be reached; drop it *) Unsat - | Some (address, _history) -> ( + | Some (address, caller_history) -> ( + let access_trace = + Trace.ViaCall + { in_call= callee_access_trace + ; f= Call callee_pname + ; location= call_loc + ; history= caller_history } + in let calling_context = (CallEvent.Call callee_pname, call_loc) :: calling_context in match - AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t) + AbductiveDomain.find_post_cell_opt address astate_post_call |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs) with | None -> @@ -186,7 +196,10 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s Sat (Ok (LatentInvalidAccess - {astate= astate_summary; address; must_be_valid; calling_context})) + { astate= astate_summary + ; address + ; must_be_valid= (access_trace, must_be_valid_reason) + ; calling_context })) | Some (invalidation, invalidation_trace) -> Sat (Error @@ -196,8 +209,8 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s { calling_context ; invalidation ; invalidation_trace - ; access_trace= fst must_be_valid - ; must_be_valid_reason= snd must_be_valid } + ; access_trace + ; must_be_valid_reason } ; astate= astate_summary })) ) ) ) ) | ISLLatentMemoryError astate -> map_call_result ~is_isl_error_prepost:true diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 4f59c4659..e4340914e 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -6,6 +6,7 @@ *) open! IStd +module L = Logging open PulseBasicInterface open PulseDomainInterface @@ -66,14 +67,17 @@ let is_constant_deref_without_invalidation (diagnostic : Diagnostic.t) = let is_suppressed tenv proc_desc diagnostic astate = - is_constant_deref_without_invalidation diagnostic - || - match Procdesc.get_proc_name proc_desc with - | Procname.Java jn -> - is_nullsafe_error tenv diagnostic jn - || not (AbductiveDomain.skipped_calls_match_pattern astate) - | _ -> - false + if is_constant_deref_without_invalidation diagnostic then ( + L.d_printfln ~color:Red + "Dropping error: constant dereference with no invalidation in the access trace" ; + true ) + else + match Procdesc.get_proc_name proc_desc with + | Procname.Java jn -> + is_nullsafe_error tenv diagnostic jn + || not (AbductiveDomain.skipped_calls_match_pattern astate) + | _ -> + false let summary_of_error_post tenv proc_desc location mk_error astate = diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index f52a12a7f..bbb68bb3f 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -42,6 +42,9 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc err_log locatio | None -> Some (LatentInvalidAccess {astate; address; must_be_valid; calling_context= []}) | Some (invalidation, invalidation_trace) -> + (* NOTE: this probably leads to the error being dropped as the access trace is unlikely to + contain the reason for invalidation and thus we will filter out the report. TODO: + figure out if that's a problem. *) PulseReport.report_summary_error tenv proc_desc err_log (ReportableError { diagnostic=