From f411c7d131a439b511314335737270de47f734f2 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 13 Nov 2020 09:35:50 -0800 Subject: [PATCH] [pulse] do not stop at the first error in function calls Summary: We deliberately stopped as soon as an error was detected when applying a function call. This is not good as other pre/posts of the function may apply cleanly, which would allow us to cover more behaviours of the code. Went on a bit of a refactoring tangeant while fixing this, to clarify the `Ok None`/`Ok Some _`/`Error _` datatype returned by PulseInterproc. Now we report errors as soon as we find them during function calls but continue accumulating specs afterwards. Reviewed By: da319 Differential Revision: D24888768 fbshipit-source-id: d5f2c29d7 --- infer/src/istd/IContainer.mli | 2 + infer/src/pulse/Pulse.ml | 87 +++++++----------- infer/src/pulse/PulseInterproc.ml | 12 ++- infer/src/pulse/PulseInterproc.mli | 12 ++- infer/src/pulse/PulseModels.ml | 36 ++++---- infer/src/pulse/PulseOperations.ml | 89 ++++++++++--------- infer/src/pulse/PulseOperations.mli | 5 +- infer/src/pulse/PulseReport.ml | 48 ++++++++++ infer/src/pulse/PulseReport.mli | 20 +++++ .../cpp/pulse/interprocedural.cpp | 17 ++++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 + 11 files changed, 199 insertions(+), 131 deletions(-) create mode 100644 infer/src/pulse/PulseReport.ml create mode 100644 infer/src/pulse/PulseReport.mli diff --git a/infer/src/istd/IContainer.mli b/infer/src/istd/IContainer.mli index d313ab57d..4c8584985 100644 --- a/infer/src/istd/IContainer.mli +++ b/infer/src/istd/IContainer.mli @@ -8,6 +8,8 @@ open! IStd module F = Format +[@@@warning "-32"] + (** Extension of {!Base.Container}, i.e. generic definitions of container operations in terms of a [fold] function. *) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 98e13a53b..0abb88836 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -12,43 +12,23 @@ open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface -let report ?(extra_trace = []) proc_desc err_log diagnostic = - let open Diagnostic in - Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic) - ~ltr:(extra_trace @ get_trace diagnostic) - Pulse (get_issue_type diagnostic) (get_message diagnostic) +let exec_list_of_list_result = function + | Ok posts -> + posts + | Error PulseReport.InfeasiblePath -> + [] + | Error (PulseReport.FeasiblePath post) -> + [post] -let check_error_transform {InterproceduralAnalysis.proc_desc; err_log} ~f = function - | Ok astate -> - f astate - | Error (diagnostic, astate) -> ( - let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in - if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then [] - else - match LatentIssue.should_report_diagnostic astate_summary diagnostic with - | `ReportNow -> - report proc_desc err_log diagnostic ; - [ExecutionDomain.AbortProgram astate_summary] - | `DelayReport latent_issue -> - ( if Config.pulse_report_latent_issues then - (* HACK: report latent issues with a prominent message to distinguish them from - non-latent. Useful for infer's own tests. *) - let diagnostic = LatentIssue.to_diagnostic latent_issue in - let extra_trace = - let depth = 0 in - let tags = [] in - let location = Diagnostic.get_location diagnostic in - [Errlog.make_trace_element depth location "*** LATENT ***" tags] - in - report ~extra_trace proc_desc err_log diagnostic ) ; - [ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}] ) +let report_on_error {InterproceduralAnalysis.proc_desc; err_log} result = + PulseReport.report_error proc_desc err_log result + >>| (fun post -> [ExecutionDomain.ContinueProgram post]) + |> exec_list_of_list_result -let check_error_continue analysis_data result = - check_error_transform analysis_data - ~f:(fun astate -> [ExecutionDomain.ContinueProgram astate]) - result +let report_on_error_list {InterproceduralAnalysis.proc_desc; err_log} result = + PulseReport.report_error proc_desc err_log result |> exec_list_of_list_result let proc_name_of_call call_exp = @@ -69,19 +49,20 @@ module PulseTransferFunctions = struct AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals - let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret call_exp - actuals call_loc astate = + let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; err_log} ret + call_exp actuals call_loc astate = match proc_name_of_call call_exp with | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_pvar_formals callee_pname in let callee_data = analyze_dependency callee_pname in - PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret - ~actuals ~formals_opt astate + PulseOperations.call ~caller_proc_desc:proc_desc err_log ~callee_data call_loc callee_pname + ~ret ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; - PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals - ~formals_opt:None astate - |> PulseOperations.ok_continue + Ok + [ Domain.ContinueProgram + (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals + ~formals_opt:None astate) ] (** has an object just gone out of scope? *) @@ -204,7 +185,7 @@ module PulseTransferFunctions = struct [astate] | ContinueProgram astate -> dispatch_call analysis_data ret call_exp actuals location call_flags astate - |> check_error_transform analysis_data ~f:Fn.id + |> report_on_error_list analysis_data in List.rev_append astate astates ) ~init:[] astate_list @@ -239,7 +220,7 @@ module PulseTransferFunctions = struct let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in PulseOperations.write_id lhs_id rhs_addr_hist astate in - check_error_continue analysis_data result + report_on_error analysis_data result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in @@ -257,19 +238,19 @@ module PulseTransferFunctions = struct | _ -> Ok astate in - check_error_continue analysis_data result + report_on_error analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> - PulseOperations.prune loc ~condition astate - |> check_error_transform analysis_data ~f:(fun astate -> - if PulseArithmetic.is_unsat_cheap astate then - (* [condition] is known to be unsatisfiable: prune path *) - [] - else - (* [condition] is true or unknown value: go into the branch *) - [Domain.ContinueProgram astate] ) + (let+ astate = PulseOperations.prune loc ~condition astate in + if PulseArithmetic.is_unsat_cheap astate then + (* [condition] is known to be unsatisfiable: prune path *) + [] + else + (* [condition] is true or unknown value: go into the branch *) + [Domain.ContinueProgram astate]) + |> report_on_error_list analysis_data | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call analysis_data ret call_exp actuals loc call_flags astate - |> check_error_transform analysis_data ~f:(fun id -> id) + |> report_on_error_list analysis_data | Metadata (ExitScope (vars, location)) -> let remove_vars vars astates = List.fold @@ -280,7 +261,7 @@ module PulseTransferFunctions = struct | ContinueProgram astate -> let astate = PulseOperations.remove_vars vars location astate - |> check_error_continue analysis_data + |> report_on_error analysis_data in List.rev_append astate astates ) ~init:[] astates diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index a34fb486c..9bd73c105 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -554,10 +554,10 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post (* can't make sense of the pre-condition in the current context: give up on that particular pre/post pair *) L.d_printfln "Cannot apply precondition: %a" pp_contradiction reason ; - Ok None + PulseReport.InfeasiblePath | Error _ as error -> (* error: the function call requires to read some state known to be invalid *) - error + PulseReport.FeasiblePath error | Ok call_state -> ( L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; match @@ -569,10 +569,8 @@ let apply_prepost callee_proc_name call_location ~callee_prepost:pre_post apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals call_state with - | Ok post -> - Ok (Some post) + | post -> + PulseReport.FeasiblePath post | exception Contradiction reason -> L.d_printfln "Cannot apply post-condition: %a" pp_contradiction reason ; - Ok None - | Error _ as error -> - error ) + PulseReport.InfeasiblePath ) diff --git a/infer/src/pulse/PulseInterproc.mli b/infer/src/pulse/PulseInterproc.mli index b1079946c..0a2afbb10 100644 --- a/infer/src/pulse/PulseInterproc.mli +++ b/infer/src/pulse/PulseInterproc.mli @@ -7,17 +7,15 @@ open! IStd open PulseBasicInterface +open PulseDomainInterface val apply_prepost : Procname.t -> Location.t - -> callee_prepost:PulseAbductiveDomain.t + -> callee_prepost:AbductiveDomain.t -> captured_vars_with_actuals:(Var.t * (AbstractValue.t * ValueHistory.t)) list -> formals:Var.t list -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list - -> PulseAbductiveDomain.t - -> ( (PulseAbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) option - , Diagnostic.t * PulseAbductiveDomain.t ) - result -(** return the abstract state after the call along with an optional return value, or [None] if the - precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *) + -> AbductiveDomain.t + -> (AbductiveDomain.t * (AbstractValue.t * ValueHistory.t) option) PulseReport.access_result + PulseReport.path_feasibility diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 340241558..c285fe72d 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -20,6 +20,8 @@ type model = -> AbductiveDomain.t -> ExecutionDomain.t list PulseOperations.access_result +let ok_continue post = Ok [ExecutionDomain.ContinueProgram post] + let cpp_model_namespace = QualifiedCppName.of_list ["__infer_pulse_model"] module Misc = struct @@ -54,7 +56,7 @@ module Misc = struct let i = IntLit.of_int64 i64 in let ret_addr = AbstractValue.Constants.get_int i in let astate = PulseArithmetic.and_eq_int ret_addr i astate in - PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue + PulseOperations.write_id ret_id (ret_addr, []) astate |> ok_continue let return_positive ~desc : model = @@ -64,14 +66,14 @@ module Misc = struct let ret_value = (ret_addr, [event]) in PulseOperations.write_id ret_id ret_value astate |> PulseArithmetic.and_positive ret_addr - |> PulseOperations.ok_continue + |> ok_continue let return_unknown_size : model = fun _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let astate = PulseArithmetic.and_nonnegative ret_addr astate in - PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue + PulseOperations.write_id ret_id (ret_addr, []) astate |> ok_continue (** Pretend the function call is a call to an "unknown" function, i.e. a function for which we @@ -100,12 +102,12 @@ module Misc = struct let nondet ~fn_name : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model fn_name; location; in_call= []} in - PulseOperations.havoc_id ret_id [event] astate |> PulseOperations.ok_continue + PulseOperations.havoc_id ret_id [event] astate |> ok_continue let id_first_arg arg_access_hist : model = fun _ ~callee_procname:_ _ ~ret astate -> - PulseOperations.write_id (fst ret) arg_access_hist astate |> PulseOperations.ok_continue + PulseOperations.write_id (fst ret) arg_access_hist astate |> ok_continue let free_or_delete operation deleted_access : model = @@ -113,8 +115,7 @@ module Misc = struct (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we currently know about the value. This is purely to avoid contributing to path explosion. *) (* freeing 0 is a no-op *) - if PulseArithmetic.is_known_zero astate (fst deleted_access) then - PulseOperations.ok_continue astate + if PulseArithmetic.is_known_zero astate (fst deleted_access) then ok_continue astate else let astate = PulseArithmetic.and_positive (fst deleted_access) astate in let invalidation = @@ -154,14 +155,14 @@ module C = struct let astate = PulseOperations.write_id ret_id ret_value astate in PulseOperations.allocate callee_procname location ret_value astate |> PulseArithmetic.and_positive ret_addr - |> PulseOperations.ok_continue + |> ok_continue end module ObjCCoreFoundation = struct let cf_bridging_release access : model = fun _ ~callee_procname:_ _ ~ret:(ret_id, _) astate -> let astate = PulseOperations.write_id ret_id access astate in - PulseOperations.remove_allocation_attr (fst access) astate |> PulseOperations.ok_continue + PulseOperations.remove_allocation_attr (fst access) astate |> ok_continue end module ObjC = struct @@ -179,7 +180,7 @@ module ObjC = struct let astate = PulseOperations.write_id ret_id ret_value astate in PulseOperations.add_dynamic_type dynamic_type ret_addr astate |> PulseArithmetic.and_positive ret_addr - |> PulseOperations.ok_continue + |> ok_continue end module Optional = struct @@ -245,8 +246,7 @@ module Optional = struct in (* Check dereference to show an error at the callsite of `value()` *) let* astate, _ = PulseOperations.eval_access location value Dereference astate in - PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate - |> PulseOperations.ok_continue + PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate |> ok_continue let has_value optional ~desc : model = @@ -292,7 +292,7 @@ module Cplusplus = struct PulseOperations.write_id ret_id (address, event :: hist) astate | _ -> PulseOperations.havoc_id ret_id [event] astate ) - |> PulseOperations.ok_continue + |> ok_continue end module StdAtomicInteger = struct @@ -483,7 +483,7 @@ end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc; err_log} ~callee_procname:_ location ~ret astate -> let havoc_ret (ret_id, _) astate = let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] @@ -495,14 +495,16 @@ module StdFunction = struct match AddressAttributes.get_closure_proc_name lambda astate with | None -> (* we don't know what proc name this lambda resolves to *) - Ok (havoc_ret ret astate |> List.map ~f:ExecutionDomain.continue) + Ok + ( havoc_ret ret astate + |> List.map ~f:(fun astate -> ExecutionDomain.ContinueProgram astate) ) | Some callee_proc_name -> let actuals = (lambda_ptr_hist, typ) :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call ~caller_proc_desc:proc_desc + PulseOperations.call ~caller_proc_desc:proc_desc err_log ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate @@ -800,7 +802,7 @@ module StdVector = struct if AddressAttributes.is_std_vector_reserved (fst vector) astate then (* assume that any call to [push_back] is ok after one called [reserve] on the same vector (a perfect analysis would also make sure we don't exceed the reserved size) *) - PulseOperations.ok_continue astate + ok_continue astate else (* simulate a re-allocation of the underlying array every time an element is added *) reallocate_internal_array [crumb] vector PushBack location astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 45e6b0ff3..cd0dfa453 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -12,9 +12,7 @@ open PulseDomainInterface type t = AbductiveDomain.t -type 'a access_result = ('a, Diagnostic.t * t) result - -let ok_continue post = Ok [ExecutionDomain.ContinueProgram post] +type 'a access_result = 'a PulseReport.access_result let check_addr_access location (address, history) astate = let access_trace = Trace.Immediate {location; history} in @@ -437,13 +435,14 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals ~actuals astate = - let apply callee_prepost ~f = - PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals - ~formals ~actuals astate - >>= function - | None -> - (* couldn't apply pre/post pair *) Ok None - | Some (post, return_val_opt) -> + let map_call_result callee_prepost ~f = + match + PulseInterproc.apply_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals + ~formals ~actuals astate + with + | (FeasiblePath (Error _) | InfeasiblePath) as path_result -> + path_result + | FeasiblePath (Ok (post, return_val_opt)) -> let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in let post = match return_val_opt with @@ -457,28 +456,30 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret let open ExecutionDomain in match callee_exec_state with | AbortProgram astate -> - apply + map_call_result (astate :> AbductiveDomain.t) ~f:(fun astate -> let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in - Ok (Some (AbortProgram astate_summary)) ) + FeasiblePath (Ok (AbortProgram astate_summary)) ) | ContinueProgram astate -> - apply astate ~f:(fun astate -> Ok (Some (ContinueProgram astate))) + map_call_result astate ~f:(fun astate -> FeasiblePath (Ok (ContinueProgram astate))) | ExitProgram astate -> - apply astate ~f:(fun astate -> Ok (Some (ExitProgram astate))) + map_call_result astate ~f:(fun astate -> FeasiblePath (Ok (ExitProgram astate))) | LatentAbortProgram {astate; latent_issue} -> - apply + map_call_result (astate :> AbductiveDomain.t) ~f:(fun astate -> let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in - if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Ok None + if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then + InfeasiblePath else let latent_issue = LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue in - if LatentIssue.should_report astate_summary then - Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t)) - else Ok (Some (LatentAbortProgram {astate= astate_summary; latent_issue})) ) + FeasiblePath + ( if LatentIssue.should_report astate_summary then + Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t)) + else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) ) ) let get_captured_actuals location ~captured_vars ~actual_closure astate = @@ -493,9 +494,8 @@ let get_captured_actuals location ~captured_vars ~actual_closure astate = (astate, captured_vars_with_actuals) -let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc - callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) : - (ExecutionDomain.t list, Diagnostic.t * t) result = +let call ~caller_proc_desc err_log ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc + callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = match callee_data with | Some (callee_proc_desc, exec_states) -> let formals = @@ -508,7 +508,7 @@ let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) let pvar = Pvar.mk mangled callee_pname in Var.of_pvar pvar ) in - let* astate, captured_vars_with_actuals = + let+ astate, captured_vars_with_actuals = match actuals with | (actual_closure, _) :: _ when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) -> @@ -517,34 +517,35 @@ let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) | _ -> Ok (astate, []) in - let is_blacklist = + let should_keep_at_most_one_disjunct = Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex -> Str.string_match regex (Procname.to_string callee_pname) 0 ) in + if should_keep_at_most_one_disjunct then + L.d_printfln "Will keep at most one disjunct because %a is in blacklist" Procname.pp + callee_pname ; (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) - IContainer.fold_result_until + List.fold ~init:[] (exec_states :> ExecutionDomain.t list) - ~fold:List.fold ~init:[] ~f:(fun posts callee_exec_state -> - (* apply all pre/post specs *) - match - apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state - ~captured_vars_with_actuals ~formals ~actuals ~ret astate - with - | Ok None -> - (* couldn't apply pre/post pair *) - Continue (Ok posts) - | Ok (Some post) when is_blacklist -> - L.d_printfln "Keep only one disjunct because %a is in blacklist" Procname.pp - callee_pname ; - Stop [post] - | Ok (Some post) -> - Continue (Ok (post :: posts)) - | Error _ as x -> - Continue x ) - ~finish:(fun x -> x) + if should_keep_at_most_one_disjunct && not (List.is_empty posts) then posts + else + (* apply all pre/post specs *) + match + apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state + ~captured_vars_with_actuals ~formals ~actuals ~ret astate + with + | InfeasiblePath -> + (* couldn't apply pre/post pair *) + posts + | FeasiblePath post -> ( + match PulseReport.report_error caller_proc_desc err_log post with + | Error InfeasiblePath -> + posts + | Error (FeasiblePath post) | Ok post -> + post :: posts ) ) | None -> (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate - |> ok_continue + |> fun astate -> Ok [ExecutionDomain.ContinueProgram astate] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index b45c66454..6b6febc8f 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -11,9 +11,7 @@ open PulseDomainInterface type t = AbductiveDomain.t -type 'a access_result = ('a, Diagnostic.t * t) result - -val ok_continue : t -> (ExecutionDomain.t list, 'a) result +type 'a access_result = 'a PulseReport.access_result val check_addr_access : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result (** Check that the [address] is not known to be invalid *) @@ -125,6 +123,7 @@ val check_address_escape : val call : caller_proc_desc:Procdesc.t + -> Errlog.t -> callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t -> Procname.t diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml new file mode 100644 index 000000000..5924a2455 --- /dev/null +++ b/infer/src/pulse/PulseReport.ml @@ -0,0 +1,48 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open PulseBasicInterface +open PulseDomainInterface + +type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result + +type 'a path_feasibility = InfeasiblePath | FeasiblePath of 'a + +let report ?(extra_trace = []) proc_desc err_log diagnostic = + let open Diagnostic in + Reporting.log_issue proc_desc err_log ~loc:(get_location diagnostic) + ~ltr:(extra_trace @ get_trace diagnostic) + Pulse (get_issue_type diagnostic) (get_message diagnostic) + + +let report_latent_issue proc_desc err_log latent_issue = + (* HACK: report latent issues with a prominent message to distinguish them from + non-latent. Useful for infer's own tests. *) + let diagnostic = LatentIssue.to_diagnostic latent_issue in + let extra_trace = + let depth = 0 in + let tags = [] in + let location = Diagnostic.get_location diagnostic in + [Errlog.make_trace_element depth location "*** LATENT ***" tags] + in + report ~extra_trace proc_desc err_log diagnostic + + +let report_error proc_desc err_log access_result = + Result.map_error access_result ~f:(fun (diagnostic, astate) -> + let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in + if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then InfeasiblePath + else + match LatentIssue.should_report_diagnostic astate_summary diagnostic with + | `ReportNow -> + report proc_desc err_log diagnostic ; + FeasiblePath (ExecutionDomain.AbortProgram astate_summary) + | `DelayReport latent_issue -> + if Config.pulse_report_latent_issues then + report_latent_issue proc_desc err_log latent_issue ; + FeasiblePath (ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}) ) diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli new file mode 100644 index 000000000..4de6d5c3f --- /dev/null +++ b/infer/src/pulse/PulseReport.mli @@ -0,0 +1,20 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open PulseBasicInterface +open PulseDomainInterface + +type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result + +type 'a path_feasibility = InfeasiblePath | FeasiblePath of 'a + +val report_error : + Procdesc.t + -> Errlog.t + -> 'ok access_result + -> ('ok, _ ExecutionDomain.base_t path_feasibility) result diff --git a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp index 0c5710580..c009df2a4 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp @@ -111,3 +111,20 @@ void access_to_invalidated_alias2_bad(struct X* x, struct X* y) { invalidate_and_set_to_null(&y); wraps_read(*x); } + +void set_first_non_null_ok(int* x, int* y) { + if (x) { + *x = 42; + } else { + *y = 42; + } +} + +// should get two latent issues here, or at least one for the dereference of +// [p=nullptr] +void set_x_then_crash_double_latent(int* x) { + set_first_non_null_ok(x, nullptr); + set_first_non_null_ok(nullptr, x); + int* p = nullptr; + *p = 42; +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 2d1585d96..955a8b14b 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -39,6 +39,8 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,assigned,invalid access occurs here]