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=