From 8a1213962e0f2579eb493cd87512dc97a3916e04 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 17 Mar 2021 03:52:04 -0700 Subject: [PATCH] [pulse][1/2] new kind of latent issues to remove some FNs Summary: This first commit introduces test cases and the new summary type, in particular how it is propagated during function calls. We don't yet actually generate these summary types, this is for the next diff. The goal is to catch this pattern: ``` foo(p) { if(p) {} *p = 42; } goo() { foo(NULL); } ``` We went foo(p) to be a latent error when p=0. Right now we detect a contradiction p|->- * p=0 |- false. The next diff will fix it. Reviewed By: skcho Differential Revision: D26918552 fbshipit-source-id: 6614db17b --- infer/src/checkers/impurity.ml | 5 +- infer/src/pulse/Pulse.ml | 28 +++++++--- infer/src/pulse/PulseExecutionDomain.ml | 21 ++++++-- infer/src/pulse/PulseExecutionDomain.mli | 8 +++ infer/src/pulse/PulseInterproc.ml | 6 +-- infer/src/pulse/PulseInterproc.mli | 13 ++++- infer/src/pulse/PulseObjectiveCSummary.ml | 7 ++- infer/src/pulse/PulseOperations.ml | 62 ++++++++++++++++++----- infer/src/pulse/PulseOperations.mli | 5 ++ infer/src/pulse/PulseSummary.ml | 2 + 10 files changed, 127 insertions(+), 30 deletions(-) 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)