diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 0d50ab4fe..1b2352080 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -162,7 +162,10 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur ((astate :> AbductiveDomain.t), true) | ContinueProgram astate -> (astate, false) - | AbortProgram astate | LatentAbortProgram {astate} | ISLLatentMemoryError astate -> + | AbortProgram astate + | LatentAbortProgram {astate} + | LatentInvalidAccess {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 f4318abcd..1b27a2d64 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -86,7 +86,11 @@ module PulseTransferFunctions = struct (* invalidate [&x] *) PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate >>| ExecutionDomain.continue - | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ + | AbortProgram _ + | ExitProgram _ + | LatentAbortProgram _ + | LatentInvalidAccess _ -> Ok exec_state @@ -104,7 +108,11 @@ module PulseTransferFunctions = struct match exec_state with | ContinueProgram astate -> ContinueProgram (do_astate astate) - | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ -> + | ISLLatentMemoryError _ + | AbortProgram _ + | LatentAbortProgram _ + | ExitProgram _ + | LatentInvalidAccess _ -> exec_state in List.map ~f:(Result.map ~f:do_one_exec_state) exec_state_res @@ -240,7 +248,11 @@ module PulseTransferFunctions = struct call_instr ; List.concat_map astate_list ~f:(fun (astate : Domain.t) -> match astate with - | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ + | AbortProgram _ + | ExitProgram _ + | LatentAbortProgram _ + | LatentInvalidAccess _ -> [astate] | ContinueProgram astate -> dispatch_call analysis_data ret call_exp actuals location call_flags astate @@ -262,9 +274,7 @@ module PulseTransferFunctions = struct ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node (instr : Sil.instr) : Domain.t list = match astate with - | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ -> - (* We can also continue the analysis with the error state here - but there might be a risk we would get nonsense. *) + | AbortProgram _ | ISLLatentMemoryError _ | LatentAbortProgram _ | LatentInvalidAccess _ -> [astate] | ExitProgram _ -> (* program already exited, simply propagate the exited state upwards *) @@ -344,7 +354,11 @@ module PulseTransferFunctions = struct let remove_vars vars astates = List.concat_map astates ~f:(fun (astate : Domain.t) -> match astate with - | ISLLatentMemoryError _ | AbortProgram _ | ExitProgram _ | LatentAbortProgram _ -> + | ISLLatentMemoryError _ + | AbortProgram _ + | ExitProgram _ + | LatentAbortProgram _ + | LatentInvalidAccess _ -> [astate] | ContinueProgram astate -> PulseOperations.remove_vars tenv vars location astate diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 02ca1349e..0b4057cc4 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -20,6 +20,11 @@ type 'abductive_domain_t base_t = | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + | LatentInvalidAccess of + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: (Trace.t[@yojson.opaque]) + ; calling_context: ((CallEvent.t * Location.t) list[@yojson.opaque]) } | ISLLatentMemoryError of AbductiveDomain.summary [@@deriving equal, compare, yojson_of] @@ -43,19 +48,23 @@ let leq ~lhs ~rhs = , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) -> LatentIssue.equal issue1 issue2 && AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) + | ( LatentInvalidAccess {astate= astate1; address= v1; must_be_valid= _} + , LatentInvalidAccess {astate= astate2; address= v2; must_be_valid= _} ) -> + AbstractValue.equal v1 v2 + && AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) | _ -> false let pp fmt = function + | AbortProgram astate -> + F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | ContinueProgram astate -> AbductiveDomain.pp fmt astate - | ISLLatentMemoryError 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 -> - F.fprintf fmt "{AbortProgram %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) + | ISLLatentMemoryError astate -> + F.fprintf fmt "{ISLLatentMemoryError %a}" AbductiveDomain.pp (astate :> AbductiveDomain.t) | LatentAbortProgram {astate; latent_issue} -> let diagnostic = LatentIssue.to_diagnostic latent_issue in let message = Diagnostic.get_message diagnostic in @@ -63,6 +72,9 @@ let pp fmt = function F.fprintf fmt "{LatentAbortProgram(%a: %s) %a}" Location.pp location message AbductiveDomain.pp (astate :> AbductiveDomain.t) + | LatentInvalidAccess {astate; address; must_be_valid= _} -> + F.fprintf fmt "{LatentInvalidAccess(%a) %a}" AbstractValue.pp address AbductiveDomain.pp + (astate :> AbductiveDomain.t) (* do not export this function as there lies wickedness: clients should generally care about what @@ -73,6 +85,7 @@ let get_astate : t -> AbductiveDomain.t = function | ExitProgram astate | AbortProgram astate | LatentAbortProgram {astate} + | LatentInvalidAccess {astate} | ISLLatentMemoryError astate -> (astate :> AbductiveDomain.t) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index e6fb02394..b880f3a2a 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -6,6 +6,7 @@ *) open! IStd +open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain module LatentIssue = PulseLatentIssue @@ -17,6 +18,13 @@ 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 *) + | LatentInvalidAccess of + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t + ; calling_context: (CallEvent.t * Location.t) list } + (** if [address] is ever observed to be invalid then there is an invalid access because it + [must_be_valid] *) | 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 0f406a9ca..852cf4141 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -745,10 +745,10 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p astate else Ok astate in - (astate, return_caller) + (astate, return_caller, call_state.subst) with - | post -> - Sat post + | result -> + Sat result | exception Contradiction reason -> L.d_printfln "Cannot apply post-condition: %a" pp_contradiction reason ; Unsat ) diff --git a/infer/src/pulse/PulseInterproc.mli b/infer/src/pulse/PulseInterproc.mli index 3b5ae76f8..763f17da2 100644 --- a/infer/src/pulse/PulseInterproc.mli +++ b/infer/src/pulse/PulseInterproc.mli @@ -18,4 +18,15 @@ val apply_prepost : -> formals:Var.t list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> AbductiveDomain.t - -> (AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) AccessResult.t SatUnsat.t + -> ( AbductiveDomain.t + * (AbstractValue.t * ValueHistory.t) option + * (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t ) + AccessResult.t + SatUnsat.t +(** result of applying one pre/post pair of a callee's summary: + + - {!SatUnsat.Unsat} if that path in the callee is infeasible + - otherwise, there can be an error detected + - otherwise, the result is a new abstract state, an optional return value, and a substitution + [callee_abstract_value -> caller_abstract_value] mapping callee's abstract values to what they + became in the new (caller) state *) diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index eab331f3e..ecbdc6784 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -41,6 +41,7 @@ let mk_objc_method_nil_summary {InterproceduralAnalysis.tenv; proc_desc; err_log | ExitProgram _, _ | AbortProgram _, _ | LatentAbortProgram _, _ + | LatentInvalidAccess _, _ | ISLLatentMemoryError _, _ -> None @@ -55,7 +56,11 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} PulseArithmetic.prune_positive (fst value) astate in PulseReport.report_result tenv proc_desc err_log result - | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ -> + | ExitProgram _ + | AbortProgram _ + | LatentAbortProgram _ + | LatentInvalidAccess _ + | ISLLatentMemoryError _ -> [astate] diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 8d32252dd..664442446 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -20,6 +20,11 @@ module Import = struct | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + | LatentInvalidAccess of + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t + ; calling_context: (CallEvent.t * Location.t) list } | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = @@ -622,7 +627,7 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state with | (Sat (Error _) | Unsat) as path_result -> path_result - | Sat (Ok (post, return_val_opt)) -> + | Sat (Ok (post, return_val_opt, subst)) -> let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in let post = match return_val_opt with @@ -631,28 +636,31 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state | None -> havoc_id (fst ret) [event] post in - f post + f subst post in let open ExecutionDomain in let open SatUnsat.Import in match callee_exec_state with | ContinueProgram astate -> - map_call_result ~is_isl_error_prepost:false astate ~f:(fun astate -> + map_call_result ~is_isl_error_prepost:false astate ~f:(fun _subst astate -> Sat (Ok (ContinueProgram astate)) ) - | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} -> + | AbortProgram astate + | ExitProgram astate + | LatentAbortProgram {astate} + | LatentInvalidAccess {astate} -> map_call_result ~is_isl_error_prepost:false (astate :> AbductiveDomain.t) - ~f:(fun astate -> - let+ (astate_summary : AbductiveDomain.summary) = + ~f:(fun subst astate -> + let* (astate_summary : AbductiveDomain.summary) = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in match callee_exec_state with | ContinueProgram _ | ISLLatentMemoryError _ -> assert false | AbortProgram _ -> - Ok (AbortProgram astate_summary) + Sat (Ok (AbortProgram astate_summary)) | ExitProgram _ -> - Ok (ExitProgram astate_summary) + Sat (Ok (ExitProgram astate_summary)) | LatentAbortProgram {latent_issue} -> ( let latent_issue = LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue @@ -660,15 +668,43 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state let diagnostic = LatentIssue.to_diagnostic latent_issue in match LatentIssue.should_report astate_summary diagnostic with | `DelayReport latent_issue -> - Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) + Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) | `ReportNow -> - Error - (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)}) ) - ) + Sat + (Error + (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)})) + ) + | LatentInvalidAccess {address= address_callee; must_be_valid; 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) -> ( + let calling_context = (CallEvent.Call callee_pname, call_loc) :: calling_context in + match + AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t) + |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs) + with + | None -> + (* still no proof that the address is invalid *) + Sat + (Ok + (LatentInvalidAccess + {astate= astate_summary; address; must_be_valid; calling_context})) + | Some (invalidation, invalidation_trace) -> + Sat + (Error + (ReportableError + { diagnostic= + AccessToInvalidAddress + { calling_context + ; invalidation + ; invalidation_trace + ; access_trace= must_be_valid } + ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) | ISLLatentMemoryError astate -> map_call_result ~is_isl_error_prepost:true (astate :> AbductiveDomain.t) - ~f:(fun astate -> + ~f:(fun _subst astate -> let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in Ok (ISLLatentMemoryError astate_summary) ) diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 66a1bf368..4ea8b974f 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -27,6 +27,11 @@ module Import : sig | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + | LatentInvalidAccess of + { astate: AbductiveDomain.summary + ; address: AbstractValue.t + ; must_be_valid: Trace.t + ; calling_context: (CallEvent.t * Location.t) list } | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index bd3bbb863..3bc951e04 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -37,6 +37,8 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate : Some (ExitProgram astate) | LatentAbortProgram {astate; latent_issue} -> Some (LatentAbortProgram {astate; latent_issue}) + | LatentInvalidAccess {astate; address; must_be_valid; calling_context} -> + Some (LatentInvalidAccess {astate; address; must_be_valid; calling_context}) | ISLLatentMemoryError astate -> Some (ISLLatentMemoryError astate)