From 55871dd2855fbe5d7e1cffda9ee2b3b39984c0f0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 17 Mar 2021 03:52:35 -0700 Subject: [PATCH] [pulse][2/2] generate latent issues when null is allocated Summary: See updated tests and code comments: this changes many arithmetic operations to detect when a contradiction "p|->- * p=0" is about to be detected, and generate a latent issue instead. It's hacky but it does what we want. Many APIs change because of this so there's some code churn but the overall end result is not much worse thanks to monadic operators. Reviewed By: skcho Differential Revision: D26918553 fbshipit-source-id: da2abc652 --- infer/src/pulse/Pulse.ml | 8 +- infer/src/pulse/PulseAbductiveDomain.ml | 73 +++++++-- infer/src/pulse/PulseAbductiveDomain.mli | 12 +- infer/src/pulse/PulseAccessResult.ml | 30 ++++ infer/src/pulse/PulseAccessResult.mli | 37 +++++ infer/src/pulse/PulseArithmetic.ml | 5 +- infer/src/pulse/PulseArithmetic.mli | 38 +++-- infer/src/pulse/PulseInterproc.ml | 45 ++++-- infer/src/pulse/PulseModels.ml | 120 +++++++------- infer/src/pulse/PulseObjectiveCSummary.ml | 4 +- infer/src/pulse/PulseOperations.ml | 149 +++++++++--------- infer/src/pulse/PulseOperations.mli | 3 + infer/src/pulse/PulseReport.ml | 33 +++- infer/src/pulse/PulseReport.mli | 7 + infer/src/pulse/PulseSummary.ml | 34 +++- infer/src/pulse/PulseSummary.mli | 4 +- .../codetoanalyze/cpp/pulse/aliasing.cpp | 7 +- .../cpp/pulse/conditional_temporaries.cpp | 3 + .../cpp/pulse/folly_DestructorGuard.cpp | 4 +- .../cpp/pulse/interprocedural.cpp | 4 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 6 + .../tests/codetoanalyze/cpp/pulse/nullptr.cpp | 6 +- 22 files changed, 431 insertions(+), 201 deletions(-) create mode 100644 infer/src/pulse/PulseAccessResult.mli diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 1b27a2d64..0f33f7a85 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -131,8 +131,8 @@ module PulseTransferFunctions = struct astate - let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc} as analysis_data) ret call_exp - actuals call_loc flags astate = + let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) ret + call_exp actuals call_loc flags astate = (* evaluate all actuals *) let<*> astate, rev_func_args = List.fold_result actuals ~init:(astate, []) @@ -204,7 +204,7 @@ module PulseTransferFunctions = struct | Error _ as err -> Some err | Ok exec_state -> - PulseSummary.force_exit_program tenv proc_desc exec_state + PulseSummary.force_exit_program tenv proc_desc err_log exec_state |> Option.map ~f:(fun exec_state -> Ok exec_state) ) else exec_states_res @@ -429,7 +429,7 @@ let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data let updated_posts = PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts in - let summary = PulseSummary.of_posts tenv proc_desc updated_posts in + let summary = PulseSummary.of_posts tenv proc_desc err_log updated_posts in report_topl_errors proc_desc err_log summary ; Some summary ) | None -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 8ae08a7af..4a80da29b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -673,12 +673,13 @@ let invalidate_locals pdesc astate : t = type summary = t [@@deriving compare, equal, yojson_of] -let is_allocated stack_allocations {post; pre} v = +let is_heap_allocated {post; pre} v = BaseMemory.is_allocated (post :> BaseDomain.t).heap v || BaseMemory.is_allocated (pre :> BaseDomain.t).heap v - || AbstractValue.Set.mem v (Lazy.force stack_allocations) +let is_stack_allocated stack_allocations v = AbstractValue.Set.mem v (Lazy.force stack_allocations) + let subst_var_in_post subst astate = let open SatUnsat.Import in let+ post = PostDomain.subst_var subst astate.post in @@ -695,23 +696,55 @@ let get_stack_allocated {post} = let incorporate_new_eqs astate new_eqs = let stack_allocations = lazy (get_stack_allocated astate) in - List.fold_until new_eqs ~init:astate - ~finish:(fun astate -> Sat astate) - ~f:(fun astate (new_eq : PulseFormula.new_eq) -> + List.fold_until new_eqs ~init:(astate, None) + ~finish:(fun astate_error -> Sat astate_error) + ~f:(fun (astate, error) (new_eq : PulseFormula.new_eq) -> match new_eq with | Equal (v1, v2) when AbstractValue.equal v1 v2 -> - Continue astate + Continue (astate, error) | Equal (v1, v2) -> ( match subst_var_in_post (v1, v2) astate with | Unsat -> Stop Unsat | Sat astate' -> - Continue astate' ) - | EqZero v when is_allocated stack_allocations astate v -> + Continue (astate', error) ) + | EqZero v when is_stack_allocated stack_allocations v -> L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ; Stop Unsat + | EqZero v when is_heap_allocated astate v -> ( + (* We want to detect when we know [v|->-] and [v=0] together. This is a contradiction, but + can also be the sign that there is a real issue. Consider: + + foo(p) { + if(p) {} + *p = 42; + } + + This creates two paths: + p=0 /\ p|->- + p≠0 /\ p|->- + + We could discard the first one straight away because it's equivalent to false, but + the second one will also get discarded when calling this foo(0) because it will fail + the p≠0 condition, creating FNs. Thus, we create a latent issue instead to report + on foo(0) calls. + + An alternative design that would be less hacky would be to detect this situation when + adding pointers from null values, but we'd need to know what values are null at all + times. This would require normalizing the arithmetic part at each step, which is too + expensive. *) + L.d_printfln "Potential ERROR: %a = 0 but is allocated" AbstractValue.pp v ; + match BaseAddressAttributes.get_must_be_valid v (astate.pre :> base_domain).attrs with + | None -> + (* we don't know why [v|->-] is in the state, weird and probably cannot happen; drop + the path because we won't be able to give a sensible error *) + L.d_printfln "Not clear why %a should be allocated in the first place, giving up" + AbstractValue.pp v ; + Stop Unsat + | Some must_be_valid -> + Stop (Sat (astate, Some (v, must_be_valid))) ) | EqZero _ (* [v] not allocated *) -> - Continue astate ) + Continue (astate, error) ) (** it's a good idea to normalize the path condition before calling this function *) @@ -766,10 +799,16 @@ let summary_of_post tenv pdesc astate = in let* () = if is_unsat then Unsat else Sat () in let astate = {astate with path_condition} in - let* astate = incorporate_new_eqs astate new_eqs in + let* astate, error = incorporate_new_eqs astate new_eqs in let* astate, new_eqs = filter_for_summary tenv astate in - let+ astate = incorporate_new_eqs astate new_eqs in - invalidate_locals pdesc astate + let+ astate, error = + match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error) + in + match error with + | None -> + Ok (invalidate_locals pdesc astate) + | Some (address, must_be_valid) -> + Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid)) let get_pre {pre} = (pre :> BaseDomain.t) @@ -778,13 +817,15 @@ let get_post {post} = (post :> BaseDomain.t) (* re-exported for mli *) let incorporate_new_eqs new_eqs astate = - if PathCondition.is_unsat_cheap astate.path_condition then astate + if PathCondition.is_unsat_cheap astate.path_condition then Ok astate else match incorporate_new_eqs astate new_eqs with | Unsat -> - {astate with path_condition= PathCondition.false_} - | Sat astate -> - astate + Ok {astate with path_condition= PathCondition.false_} + | Sat (astate, None) -> + Ok astate + | Sat (astate, Some (address, must_be_valid)) -> + Error (`PotentialInvalidAccess (astate, address, must_be_valid)) module Topl = struct diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index ecc816101..d92eea3de 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -186,7 +186,12 @@ type summary = private t [@@deriving compare, equal, yojson_of] val skipped_calls_match_pattern : summary -> bool -val summary_of_post : Tenv.t -> Procdesc.t -> t -> summary SatUnsat.t +val summary_of_post : + Tenv.t + -> Procdesc.t + -> t + -> (summary, [> `PotentialInvalidAccessSummary of summary * AbstractValue.t * Trace.t]) result + SatUnsat.t (** trim the state down to just the procedure's interface (formals and globals), and simplify and normalize the state *) @@ -196,7 +201,10 @@ val set_post_edges : AbstractValue.t -> BaseMemory.Edges.t -> t -> t val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t (** directly set the edges and attributes for the given address, bypassing abduction altogether *) -val incorporate_new_eqs : PathCondition.new_eqs -> t -> t +val incorporate_new_eqs : + PathCondition.new_eqs + -> t + -> (t, [> `PotentialInvalidAccess of t * AbstractValue.t * Trace.t]) result (** Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. [x = 0] is not compatible with [x] being allocated, and [x = y] is not compatible with [x] and [y] being allocated separately. In those cases, the resulting path condition is diff --git a/infer/src/pulse/PulseAccessResult.ml b/infer/src/pulse/PulseAccessResult.ml index c5c804eb1..cf810b266 100644 --- a/infer/src/pulse/PulseAccessResult.ml +++ b/infer/src/pulse/PulseAccessResult.ml @@ -10,9 +10,39 @@ open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain type 'astate error = + | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccessSummary of + {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate type ('a, 'astate) base_t = ('a, 'astate error) result type 'a t = ('a, AbductiveDomain.t) base_t + +type 'astate abductive_error = + [ `ISLError of 'astate + | `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t + | `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ] + +let of_abductive_error = function + | `ISLError astate -> + ISLError astate + | `PotentialInvalidAccess (astate, address, must_be_valid) -> + PotentialInvalidAccess {astate; address; must_be_valid} + | `PotentialInvalidAccessSummary (astate, address, must_be_valid) -> + PotentialInvalidAccessSummary {astate; address; must_be_valid} + + +let of_abductive_result abductive_result = Result.map_error abductive_result ~f:of_abductive_error + +let of_abductive_access_result access_trace abductive_result = + Result.map_error abductive_result ~f:(function + | `InvalidAccess (invalidation, invalidation_trace, astate) -> + ReportableError + { astate + ; diagnostic= + AccessToInvalidAddress + {calling_context= []; invalidation; invalidation_trace; access_trace} } + | (`ISLError _ | `PotentialInvalidAccess _ | `PotentialInvalidAccessSummary _) as error -> + of_abductive_error error ) diff --git a/infer/src/pulse/PulseAccessResult.mli b/infer/src/pulse/PulseAccessResult.mli new file mode 100644 index 000000000..0784f954f --- /dev/null +++ b/infer/src/pulse/PulseAccessResult.mli @@ -0,0 +1,37 @@ +(* + * 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 +module AbductiveDomain = PulseAbductiveDomain + +type 'astate error = + | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccessSummary of + {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} + | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} + | ISLError of 'astate + +type ('a, 'astate) base_t = ('a, 'astate error) result + +type 'a t = ('a, AbductiveDomain.t) base_t + +(** Intermediate datatype since {!AbductiveDomain} cannot refer to this module without creating a + circular dependency. *) +type 'astate abductive_error = + [ `ISLError of 'astate + | `PotentialInvalidAccess of 'astate * AbstractValue.t * Trace.t + | `PotentialInvalidAccessSummary of AbductiveDomain.summary * AbstractValue.t * Trace.t ] + +val of_abductive_error : 'astate abductive_error -> 'astate error + +val of_abductive_result : ('a, 'astate abductive_error) result -> ('a, 'astate) base_t + +val of_abductive_access_result : + Trace.t + -> ('a, [`InvalidAccess of Invalidation.t * Trace.t * 'astate | 'astate abductive_error]) result + -> ('a, 'astate) base_t diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 500b57828..d6e826152 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -8,10 +8,13 @@ open! IStd open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain +module AccessResult = PulseAccessResult let map_path_condition ~f astate = let phi, new_eqs = f astate.AbductiveDomain.path_condition in - AbductiveDomain.set_path_condition phi astate |> AbductiveDomain.incorporate_new_eqs new_eqs + AbductiveDomain.set_path_condition phi astate + |> AbductiveDomain.incorporate_new_eqs new_eqs + |> AccessResult.of_abductive_result let and_nonnegative v astate = diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 96aa69b2c..1fdc04c2f 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -8,32 +8,48 @@ open! IStd open PulseBasicInterface module AbductiveDomain = PulseAbductiveDomain +module AccessResult = PulseAccessResult (** Wrapper around {!PathCondition} that operates on {!AbductiveDomain.t}. *) -val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +val and_nonnegative : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t -val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +val and_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t -val and_eq_int : AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t +val and_eq_int : + AbstractValue.t -> IntLit.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t type operand = PathCondition.operand = | LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t val eval_binop : - AbstractValue.t -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t + AbstractValue.t + -> Binop.t + -> operand + -> operand + -> AbductiveDomain.t + -> AbductiveDomain.t AccessResult.t val eval_unop : - AbstractValue.t -> Unop.t -> AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t + AbstractValue.t + -> Unop.t + -> AbstractValue.t + -> AbductiveDomain.t + -> AbductiveDomain.t AccessResult.t val prune_binop : - negated:bool -> Binop.t -> operand -> operand -> AbductiveDomain.t -> AbductiveDomain.t + negated:bool + -> Binop.t + -> operand + -> operand + -> AbductiveDomain.t + -> AbductiveDomain.t AccessResult.t -val prune_eq_zero : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +val prune_eq_zero : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t (** helper function wrapping [prune_binop] *) -val prune_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t +val prune_positive : AbstractValue.t -> AbductiveDomain.t -> AbductiveDomain.t AccessResult.t (** helper function wrapping [prune_binop] *) val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool @@ -43,4 +59,8 @@ val is_unsat_cheap : AbductiveDomain.t -> bool val has_no_assumptions : AbductiveDomain.t -> bool val and_equal_instanceof : - AbstractValue.t -> AbstractValue.t -> Typ.t -> AbductiveDomain.t -> AbductiveDomain.t + AbstractValue.t + -> AbstractValue.t + -> Typ.t + -> AbductiveDomain.t + -> AbductiveDomain.t AccessResult.t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 852cf4141..5ba7b1bf1 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -262,6 +262,7 @@ let add_call_to_attributes proc_name call_location caller_history attrs = let conjoin_callee_arith pre_post call_state = + let open IResult.Let_syntax in L.d_printfln "applying callee path condition: (%a)[%a]" PathCondition.pp pre_post.AbductiveDomain.path_condition (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr)) @@ -270,13 +271,19 @@ let conjoin_callee_arith pre_post call_state = PathCondition.and_callee call_state.subst call_state.astate.path_condition ~callee:pre_post.AbductiveDomain.path_condition in - let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in - let astate = AbductiveDomain.incorporate_new_eqs new_eqs astate in - if PathCondition.is_unsat_cheap astate.path_condition then raise (Contradiction PathCondition) - else {call_state with astate; subst} + if PathCondition.is_unsat_cheap path_condition then raise (Contradiction PathCondition) + else + let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in + let+ astate = + AbductiveDomain.incorporate_new_eqs new_eqs astate |> AccessResult.of_abductive_result + in + if PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition then + raise (Contradiction PathCondition) + else {call_state with astate; subst} let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state = + let open IResult.Let_syntax in let one_address_sat callee_attrs (addr_caller, caller_history) call_state = let attrs_caller = add_call_to_attributes callee_proc_name call_location caller_history callee_attrs @@ -284,7 +291,7 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in if phys_equal astate call_state.astate then call_state else {call_state with astate} in - let call_state = conjoin_callee_arith pre_post call_state in + let+ call_state = conjoin_callee_arith pre_post call_state in (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *) if Config.pulse_isl then AddressMap.fold @@ -337,7 +344,7 @@ let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_ >>= materialize_pre_for_captured_vars callee_proc_name call_location pre_post ~captured_vars_with_actuals >>= materialize_pre_for_globals callee_proc_name call_location pre_post - >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in + >>= (* ...then relational arithmetic constraints in the callee's attributes will make sense in terms of the caller's values *) apply_arithmetic_constraints callee_proc_name call_location pre_post in @@ -576,18 +583,22 @@ let record_skipped_calls callee_proc_name call_loc pre_post call_state = let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals call_state = + let open IResult.Let_syntax in PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; let r = - apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state - |> apply_post_for_captured_vars callee_proc_name call_location pre_post - ~captured_vars_with_actuals - |> apply_post_for_globals callee_proc_name call_location pre_post - |> record_post_for_return callee_proc_name call_location pre_post - |> fun (call_state, return_caller) -> - record_post_remaining_attributes callee_proc_name call_location pre_post call_state - |> record_skipped_calls callee_proc_name call_location pre_post - |> conjoin_callee_arith pre_post - |> fun call_state -> (call_state, return_caller) + let call_state, return_caller = + apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state + |> apply_post_for_captured_vars callee_proc_name call_location pre_post + ~captured_vars_with_actuals + |> apply_post_for_globals callee_proc_name call_location pre_post + |> record_post_for_return callee_proc_name call_location pre_post + in + let+ call_state = + record_post_remaining_attributes callee_proc_name call_location pre_post call_state + |> record_skipped_calls callee_proc_name call_location pre_post + |> conjoin_callee_arith pre_post + in + (call_state, return_caller) in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r @@ -728,7 +739,7 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p let pre_astate = astate in let call_state = {call_state with astate; visited= AddressSet.empty} in (* apply the postcondition *) - let call_state, return_caller = + let* call_state, return_caller = apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals call_state in diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index fcaa8feb2..4a8d8bafa 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -50,19 +50,24 @@ module Misc = struct let early_exit : model = fun {tenv; proc_desc} ~callee_procname:_ _ ~ret:_ astate -> - match AbductiveDomain.summary_of_post tenv proc_desc astate with + let open SatUnsat.Import in + match + AbductiveDomain.summary_of_post tenv proc_desc astate >>| AccessResult.of_abductive_result + with | Unsat -> [] - | Sat astate -> + | Sat (Ok astate) -> [Ok (ExitProgram astate)] + | Sat (Error _ as error) -> + [error] let return_int : Int64.t -> model = fun i64 _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> 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 |> ok_continue + let<+> astate = PulseArithmetic.and_eq_int ret_addr i astate in + PulseOperations.write_id ret_id (ret_addr, []) astate let return_positive ~desc : model = @@ -70,16 +75,15 @@ module Misc = struct let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [event]) in + let<+> astate = PulseArithmetic.and_positive ret_addr astate in PulseOperations.write_id ret_id ret_value astate - |> PulseArithmetic.and_positive ret_addr - |> 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 |> ok_continue + let<+> astate = PulseArithmetic.and_nonnegative ret_addr astate in + PulseOperations.write_id ret_id (ret_addr, []) astate (** Pretend the function call is a call to an "unknown" function, i.e. a function for which we @@ -121,7 +125,7 @@ module Misc = struct match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete in let astates_alloc = - let astate = PulseArithmetic.and_positive (fst deleted_access) astate in + let<*> astate = PulseArithmetic.and_positive (fst deleted_access) astate in if Config.pulse_isl then PulseOperations.invalidate_biad_isl location invalidation deleted_access astate |> List.map ~f:(fun result -> @@ -131,7 +135,7 @@ module Misc = struct let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in astate in - let astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in + let<*> astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in Ok (ContinueProgram astate_zero) :: astates_alloc @@ -149,9 +153,8 @@ module Misc = struct This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *) astate in + let<+> astate = PulseArithmetic.and_positive ret_addr astate in PulseOperations.write_id ret_id ret_value astate - |> PulseArithmetic.and_positive ret_addr - |> ok_continue let alloc_not_null_call_ev ~desc arg = @@ -177,15 +180,15 @@ module C = struct (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) in let astate = PulseOperations.write_id ret_id ret_value astate in - let astate_alloc = - PulseArithmetic.and_positive ret_addr astate - |> PulseOperations.allocate callee_procname location ret_value + let<*> astate_alloc = + PulseOperations.allocate callee_procname location ret_value astate |> set_uninitialized tenv size_exp_opt location ret_addr + |> PulseArithmetic.and_positive ret_addr in let result_null = let+ astate_null = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate - |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value + >>= PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value in ContinueProgram astate_null in @@ -199,12 +202,12 @@ module C = struct (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) in let astate = PulseOperations.write_id ret_id ret_value astate in - let astate = + let<+> astate = PulseOperations.allocate callee_procname location ret_value astate - |> PulseArithmetic.and_positive ret_addr |> set_uninitialized tenv size_exp_opt location ret_addr + |> PulseArithmetic.and_positive ret_addr in - ok_continue astate + astate let malloc size_exp = malloc_common ~size_exp_opt:(Some size_exp) @@ -277,7 +280,7 @@ module Optional = struct let assign_none this ~desc : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let<*> astate, value = assign_value_fresh location this ~desc astate in - let astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in + let<*> astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in let<+> astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in astate @@ -285,8 +288,9 @@ module Optional = struct let assign_value this _value ~desc : model = fun _ ~callee_procname:_ location ~ret:_ astate -> (* TODO: call the copy constructor of a value *) - let<+> astate, value = assign_value_fresh location this ~desc astate in - PulseArithmetic.and_positive (fst value) astate + let<*> astate, value = assign_value_fresh location this ~desc astate in + let<+> astate = PulseArithmetic.and_positive (fst value) astate in + astate let assign_optional_value this init ~desc : model = @@ -319,10 +323,10 @@ module Optional = struct let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in let<*> astate, (value_addr, _) = to_internal_value_deref Read location optional astate in let astate = PulseOperations.write_id ret_id ret_value astate in - let astate_non_empty = PulseArithmetic.prune_positive value_addr astate in - let astate_true = PulseArithmetic.prune_positive ret_addr astate_non_empty in - let astate_empty = PulseArithmetic.prune_eq_zero value_addr astate in - let astate_false = PulseArithmetic.prune_eq_zero ret_addr astate_empty in + let<*> astate_non_empty = PulseArithmetic.prune_positive value_addr astate in + let<*> astate_true = PulseArithmetic.prune_positive ret_addr astate_non_empty in + let<*> astate_empty = PulseArithmetic.prune_eq_zero value_addr astate in + let<*> astate_false = PulseArithmetic.prune_eq_zero ret_addr astate_empty in [Ok (ContinueProgram astate_false); Ok (ContinueProgram astate_true)] @@ -331,7 +335,7 @@ module Optional = struct let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, value_addr = to_internal_value_deref Read location optional astate in let value_update_hist = (fst value_addr, event :: snd value_addr) in - let astate_value_addr = + let<*> astate_value_addr = PulseOperations.write_id ret_id value_update_hist astate |> PulseArithmetic.prune_positive (fst value_addr) in @@ -339,8 +343,8 @@ module Optional = struct let<*> astate_null = PulseOperations.write_id ret_id nullptr astate |> PulseArithmetic.prune_eq_zero (fst value_addr) - |> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero - |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr + >>= PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero + >>= PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr in [Ok (ContinueProgram astate_value_addr); Ok (ContinueProgram astate_null)] @@ -349,7 +353,7 @@ module Optional = struct fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, value_addr = to_internal_value_deref Read location optional astate in - let astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in + let<*> astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in let<*> astate_non_empty, value = PulseOperations.eval_access Read location value_addr Dereference astate_non_empty in @@ -359,7 +363,7 @@ module Optional = struct PulseOperations.eval_access Read location default Dereference astate in let default_value_hist = (default_val, event :: default_hist) in - let astate_empty = PulseArithmetic.prune_eq_zero (fst value_addr) astate in + let<*> astate_empty = PulseArithmetic.prune_eq_zero (fst value_addr) astate in let astate_default = PulseOperations.write_id ret_id default_value_hist astate_empty in [Ok (ContinueProgram astate_value); Ok (ContinueProgram astate_default)] end @@ -409,7 +413,7 @@ module StdAtomicInteger = struct let arith_bop prepost location event ret_id bop this operand astate = let* astate, int_addr, (old_int, hist) = load_backing_int location this astate in let bop_addr = AbstractValue.mk_fresh () in - let astate = + let* astate = PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate in let+ astate = @@ -718,15 +722,15 @@ module GenericArrayBackedCollectionIterator = struct | `NotEqual -> (IntLit.zero, IntLit.one) in - let astate_equal = + let<*> astate_equal = PulseArithmetic.and_eq_int ret_val ret_val_equal astate - |> PulseArithmetic.prune_binop ~negated:false Eq (AbstractValueOperand index_lhs) - (AbstractValueOperand index_rhs) + >>= PulseArithmetic.prune_binop ~negated:false Eq (AbstractValueOperand index_lhs) + (AbstractValueOperand index_rhs) in - let astate_notequal = + let<*> astate_notequal = PulseArithmetic.and_eq_int ret_val ret_val_notequal astate - |> PulseArithmetic.prune_binop ~negated:false Ne (AbstractValueOperand index_lhs) - (AbstractValueOperand index_rhs) + >>= PulseArithmetic.prune_binop ~negated:false Ne (AbstractValueOperand index_lhs) + (AbstractValueOperand index_rhs) in [Ok (ContinueProgram astate_equal); Ok (ContinueProgram astate_notequal)] @@ -858,7 +862,7 @@ module StdVector = struct let pointer_hist = event :: snd iter in let pointer_val = (AbstractValue.mk_fresh (), pointer_hist) in let index_zero = AbstractValue.mk_fresh () in - let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in + let<*> astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in let<*> astate, ((arr_addr, _) as arr) = GenericArrayBackedCollection.eval Read location vector astate in @@ -932,10 +936,11 @@ module Java = struct let res_addr = AbstractValue.mk_fresh () in match typeexpr with | Exp.Sizeof {typ} -> - PulseArithmetic.and_equal_instanceof res_addr argv typ astate - |> PulseArithmetic.prune_positive argv - |> PulseOperations.write_id ret_id (res_addr, event :: hist) - |> ok_continue + let<+> astate = + PulseArithmetic.and_equal_instanceof res_addr argv typ astate + >>= PulseArithmetic.prune_positive argv + in + PulseOperations.write_id ret_id (res_addr, event :: hist) astate (* The type expr is sometimes a Var expr but this is not expected. This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *) | _ -> @@ -1002,10 +1007,12 @@ module JavaCollection = struct fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "Collections.isEmpty"; location; in_call= []} in let fresh_elem = AbstractValue.mk_fresh () in - PulseArithmetic.prune_positive address astate - |> PulseArithmetic.and_eq_int fresh_elem IntLit.zero - |> PulseOperations.write_id ret_id (fresh_elem, event :: hist) - |> ok_continue + let<+> astate = + PulseArithmetic.prune_positive address astate + >>= PulseArithmetic.and_eq_int fresh_elem IntLit.zero + >>| PulseOperations.write_id ret_id (fresh_elem, event :: hist) + in + astate end module JavaInteger = struct @@ -1045,11 +1052,11 @@ module JavaInteger = struct let<*> astate, _int_addr1, (int1, hist) = load_backing_int location this astate in let<*> astate, _int_addr2, (int2, _) = load_backing_int location arg astate in let binop_addr = AbstractValue.mk_fresh () in - let astate = + let<+> astate = PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1) (AbstractValueOperand int2) astate in - PulseOperations.write_id ret_id (binop_addr, hist) astate |> ok_continue + PulseOperations.write_id ret_id (binop_addr, hist) astate let int_val this : model = @@ -1070,13 +1077,14 @@ module JavaPreconditions = struct let check_not_null (address, hist) : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "Preconditions.checkNotNull"; location; in_call= []} in - let astate = PulseArithmetic.prune_positive address astate in - PulseOperations.write_id ret_id (address, event :: hist) astate |> ok_continue + let<+> astate = PulseArithmetic.prune_positive address astate in + PulseOperations.write_id ret_id (address, event :: hist) astate let check_state_argument (address, _) : model = fun _ ~callee_procname:_ _ ~ret:_ astate -> - PulseArithmetic.prune_positive address astate |> ok_continue + let<+> astate = PulseArithmetic.prune_positive address astate in + astate end module Android = struct @@ -1085,12 +1093,12 @@ module Android = struct let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_val = AbstractValue.mk_fresh () in let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in - let astate_equal_zero = + let<*> astate_equal_zero = PulseArithmetic.and_eq_int ret_val IntLit.zero astate - |> PulseArithmetic.prune_positive address + >>= PulseArithmetic.prune_positive address in - let astate_not_zero = - PulseArithmetic.and_eq_int ret_val IntLit.one astate |> PulseArithmetic.prune_eq_zero address + let<*> astate_not_zero = + PulseArithmetic.and_eq_int ret_val IntLit.one astate >>= PulseArithmetic.prune_eq_zero address in [Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)] end diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index ecbdc6784..d2809eb0c 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -19,7 +19,7 @@ let mk_objc_method_nil_summary_aux proc_desc astate = let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in let* astate, self_value = PulseOperations.eval_deref location (Lvar self) astate in - let astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in + let* astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in let ret_var = Procdesc.get_ret_var proc_desc in let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:self_value astate @@ -52,7 +52,7 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} match astate with | ContinueProgram astate -> let result = - let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in + let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in PulseArithmetic.prune_positive (fst value) astate in PulseReport.report_result tenv proc_desc err_log result diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 664442446..b21ec3b3b 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -28,6 +28,9 @@ module Import = struct | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = + | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccessSummary of + {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate @@ -70,17 +73,8 @@ let check_and_abduce_addr_access_isl access_mode location (address, history) ?(n astate = let access_trace = Trace.Immediate {location; history} in AddressAttributes.check_valid_isl access_trace address ~null_noop astate - |> List.map ~f:(function - | Error (`InvalidAccess (invalidation, invalidation_trace, astate)) -> - Error - (ReportableError - { diagnostic= - Diagnostic.AccessToInvalidAddress - {calling_context= []; invalidation; invalidation_trace; access_trace} - ; astate }) - | Error (`ISLError astate) -> - Error (ISLError astate) - | Ok astate -> ( + |> List.map ~f:(fun access_result -> + let* astate = AccessResult.of_abductive_access_result access_trace access_result in match access_mode with | Read -> AddressAttributes.check_initialized access_trace address astate @@ -93,7 +87,7 @@ let check_and_abduce_addr_access_isl access_mode location (address, history) ?(n | Write -> Ok (AbductiveDomain.initialize address astate) | NoAccess -> - Ok astate ) ) + Ok astate ) module Closures = struct @@ -214,25 +208,28 @@ let eval mode location exp0 astate = eval mode exp' astate | Const (Cint i) -> let v = AbstractValue.Constants.get_int i in - let astate = + let+ astate = PulseArithmetic.and_eq_int v i astate - |> AddressAttributes.invalidate - (v, [ValueHistory.Assignment location]) - (ConstantDereference i) location + >>| AddressAttributes.invalidate + (v, [ValueHistory.Assignment location]) + (ConstantDereference i) location in - Ok (astate, (v, [])) + (astate, (v, [])) | UnOp (unop, exp, _typ) -> - let+ astate, (addr, hist) = eval Read exp astate in + let* astate, (addr, hist) = eval Read exp astate in let unop_addr = AbstractValue.mk_fresh () in - (PulseArithmetic.eval_unop unop_addr unop addr astate, (unop_addr, hist)) + let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in + (astate, (unop_addr, hist)) | BinOp (bop, e_lhs, e_rhs) -> let* astate, (addr_lhs, hist_lhs) = eval Read e_lhs astate in (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *) - let+ astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in + let* astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in let binop_addr = AbstractValue.mk_fresh () in - ( PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs) + let+ astate = + PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs) (AbstractValueOperand addr_rhs) astate - , (binop_addr, hist_lhs) ) + in + (astate, (binop_addr, hist_lhs)) | Const _ | Sizeof _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in @@ -253,7 +250,7 @@ let prune location ~condition astate = match (exp : Exp.t) with | BinOp (bop, exp_lhs, exp_rhs) -> let* astate, lhs_op = eval_to_operand Read location exp_lhs astate in - let+ astate, rhs_op = eval_to_operand Read location exp_rhs astate in + let* astate, rhs_op = eval_to_operand Read location exp_rhs astate in PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate | UnOp (LNot, exp', _) -> prune_aux ~negated:(not negated) exp' astate @@ -651,62 +648,72 @@ let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state map_call_result ~is_isl_error_prepost:false (astate :> AbductiveDomain.t) ~f:(fun subst astate -> - let* (astate_summary : AbductiveDomain.summary) = + let* astate_summary_result = AbductiveDomain.summary_of_post tenv caller_proc_desc astate + >>| AccessResult.of_abductive_result in - match callee_exec_state with - | ContinueProgram _ | ISLLatentMemoryError _ -> - assert false - | AbortProgram _ -> - Sat (Ok (AbortProgram astate_summary)) - | ExitProgram _ -> - Sat (Ok (ExitProgram astate_summary)) - | LatentAbortProgram {latent_issue} -> ( - let latent_issue = - LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue - in - let diagnostic = LatentIssue.to_diagnostic latent_issue in - match LatentIssue.should_report astate_summary diagnostic with - | `DelayReport latent_issue -> - Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) - | `ReportNow -> - 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) -> + match astate_summary_result with + | Error _ as error -> + Sat error + | Ok (astate_summary : AbductiveDomain.summary) -> ( + match callee_exec_state with + | ContinueProgram _ | ISLLatentMemoryError _ -> + assert false + | AbortProgram _ -> + Sat (Ok (AbortProgram astate_summary)) + | ExitProgram _ -> + Sat (Ok (ExitProgram astate_summary)) + | LatentAbortProgram {latent_issue} -> ( + let latent_issue = + LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue + in + let diagnostic = LatentIssue.to_diagnostic latent_issue in + match LatentIssue.should_report astate_summary diagnostic with + | `DelayReport latent_issue -> + Sat (Ok (LatentAbortProgram {astate= astate_summary; latent_issue})) + | `ReportNow -> Sat (Error - (ReportableError - { diagnostic= - AccessToInvalidAddress - { calling_context - ; invalidation - ; invalidation_trace - ; access_trace= must_be_valid } - ; astate= (astate_summary :> AbductiveDomain.t) })) ) ) ) + (ReportableError {diagnostic; astate= (astate_summary :> AbductiveDomain.t)})) + | `ISLDelay astate -> + Sat (Error (ISLError (astate :> 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 _subst astate -> - let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in - Ok (ISLLatentMemoryError astate_summary) ) + AbductiveDomain.summary_of_post tenv caller_proc_desc astate + >>| AccessResult.of_abductive_result + >>| Result.map ~f:(fun astate_summary -> ISLLatentMemoryError astate_summary) ) let get_captured_actuals location ~captured_vars ~actual_closure astate = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 4ea8b974f..e9b10ff96 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -35,6 +35,9 @@ module Import : sig | ISLLatentMemoryError of AbductiveDomain.summary type 'astate base_error = 'astate AccessResult.error = + | PotentialInvalidAccess of {astate: 'astate; address: AbstractValue.t; must_be_valid: Trace.t} + | PotentialInvalidAccessSummary of + {astate: AbductiveDomain.summary; address: AbstractValue.t; must_be_valid: Trace.t} | ReportableError of {astate: 'astate; diagnostic: Diagnostic.t} | ISLError of 'astate diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index bb5157902..6ae7dd9c5 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -16,10 +16,9 @@ let report ?(extra_trace = []) proc_desc err_log diagnostic = Pulse (get_issue_type diagnostic) (get_message diagnostic) -let report_latent_issue proc_desc err_log latent_issue = +let report_latent_diagnostic proc_desc err_log diagnostic = (* 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 @@ -29,6 +28,10 @@ let report_latent_issue proc_desc err_log latent_issue = report ~extra_trace proc_desc err_log diagnostic +let report_latent_issue proc_desc err_log latent_issue = + LatentIssue.to_diagnostic latent_issue |> report_latent_diagnostic proc_desc err_log + + let is_nullsafe_error tenv diagnostic jn = (not Config.pulse_nullsafe_report_npe) && IssueType.equal (Diagnostic.get_issue_type diagnostic) IssueType.nullptr_dereference @@ -46,8 +49,12 @@ let is_suppressed tenv proc_desc diagnostic astate = let summary_of_error_post tenv proc_desc mk_error astate = match AbductiveDomain.summary_of_post tenv proc_desc astate with - | Sat astate -> + | Sat (Ok astate) -> Sat (mk_error astate) + | Sat (Error error) -> + (* ignore the error we wanted to report (with [mk_error]): the abstract state contained a + potential error already so report [error] instead *) + Sat (AccessResult.of_abductive_error error) | Unsat -> Unsat @@ -55,17 +62,33 @@ let summary_of_error_post tenv proc_desc mk_error astate = let summary_error_of_error tenv proc_desc (error : AbductiveDomain.t AccessResult.error) : AbductiveDomain.summary AccessResult.error SatUnsat.t = match error with + | PotentialInvalidAccessSummary {astate; address; must_be_valid} -> + Sat (PotentialInvalidAccessSummary {astate; address; must_be_valid}) + | PotentialInvalidAccess {astate; address; must_be_valid} -> + summary_of_error_post tenv proc_desc + (fun astate -> PotentialInvalidAccess {astate; address; must_be_valid}) + astate | ReportableError {astate; diagnostic} -> summary_of_error_post tenv proc_desc - (fun astate -> AccessResult.ReportableError {astate; diagnostic}) + (fun astate -> ReportableError {astate; diagnostic}) astate | ISLError astate -> - summary_of_error_post tenv proc_desc (fun astate -> AccessResult.ISLError astate) astate + summary_of_error_post tenv proc_desc (fun astate -> ISLError astate) astate let report_summary_error tenv proc_desc err_log (access_error : AbductiveDomain.summary AccessResult.error) : _ ExecutionDomain.base_t = match access_error with + | PotentialInvalidAccess {astate; address; must_be_valid} + | PotentialInvalidAccessSummary {astate; address; must_be_valid} -> + if Config.pulse_report_latent_issues then + report_latent_diagnostic proc_desc err_log + (AccessToInvalidAddress + { calling_context= [] + ; invalidation= ConstantDereference IntLit.zero + ; invalidation_trace= Immediate {location= Procdesc.get_loc proc_desc; history= []} + ; access_trace= must_be_valid }) ; + LatentInvalidAccess {astate; address; must_be_valid; calling_context= []} | ISLError astate -> ISLLatentMemoryError astate | ReportableError {astate; diagnostic} -> ( diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index 65fedb6ed..4b77fcf3a 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -11,6 +11,13 @@ open PulseDomainInterface val report_result : Tenv.t -> Procdesc.t -> Errlog.t -> AbductiveDomain.t AccessResult.t -> ExecutionDomain.t list +val report_summary_error : + Tenv.t + -> Procdesc.t + -> Errlog.t + -> AbductiveDomain.summary AccessResult.error + -> _ ExecutionDomain.base_t + val report_results : Tenv.t -> Procdesc.t diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index 3bc951e04..fe2bc0701 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -21,15 +21,33 @@ let pp fmt summary = F.close_box () -let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate : ExecutionDomain.t) : - _ ExecutionDomain.base_t option = +let exec_summary_of_post_common tenv ~continue_program proc_desc err_log + (exec_astate : ExecutionDomain.t) : _ ExecutionDomain.base_t option = match exec_astate with | ContinueProgram astate -> ( match AbductiveDomain.summary_of_post tenv proc_desc astate with | Unsat -> None - | Sat astate -> - Some (continue_program astate) ) + | Sat (Ok astate) -> + Some (continue_program astate) + | Sat (Error (`PotentialInvalidAccessSummary (astate, address, must_be_valid))) -> ( + match + AbductiveDomain.find_post_cell_opt address (astate :> AbductiveDomain.t) + |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs) + with + | None -> + Some (LatentInvalidAccess {astate; address; must_be_valid; calling_context= []}) + | Some (invalidation, invalidation_trace) -> + PulseReport.report_summary_error tenv proc_desc err_log + (ReportableError + { diagnostic= + AccessToInvalidAddress + { calling_context= [] + ; invalidation + ; invalidation_trace + ; access_trace= must_be_valid } + ; astate }) + |> Option.some ) ) (* already a summary but need to reconstruct the variants to make the type system happy :( *) | AbortProgram astate -> Some (AbortProgram astate) @@ -43,13 +61,13 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc (exec_astate : Some (ISLLatentMemoryError astate) -let force_exit_program tenv proc_desc post = - exec_summary_of_post_common tenv proc_desc post ~continue_program:(fun astate -> +let force_exit_program tenv proc_desc err_log post = + exec_summary_of_post_common tenv proc_desc err_log post ~continue_program:(fun astate -> ExitProgram astate ) -let of_posts tenv proc_desc posts = +let of_posts tenv proc_desc err_log posts = List.filter_mapi posts ~f:(fun i exec_state -> L.d_printfln "Creating spec out of state #%d:@\n%a" i ExecutionDomain.pp exec_state ; - exec_summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate -> + exec_summary_of_post_common tenv proc_desc err_log exec_state ~continue_program:(fun astate -> ContinueProgram astate ) ) diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli index de7fdcf6c..c283e4aad 100644 --- a/infer/src/pulse/PulseSummary.mli +++ b/infer/src/pulse/PulseSummary.mli @@ -10,9 +10,9 @@ open PulseDomainInterface type t = ExecutionDomain.summary list [@@deriving yojson_of] -val of_posts : Tenv.t -> Procdesc.t -> ExecutionDomain.t list -> t +val of_posts : Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t list -> t val force_exit_program : - Tenv.t -> Procdesc.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option + Tenv.t -> Procdesc.t -> Errlog.t -> ExecutionDomain.t -> _ ExecutionDomain.base_t option val pp : Format.formatter -> t -> unit diff --git a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp index 40b6559b1..a31ad6f86 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp @@ -69,10 +69,11 @@ void stack_addresses_are_distinct_ok() { } } -void null_test_after_deref_ok(int* x) { - *x = 42; +// latent because of the condition "x==0" in the pre-condition +void null_test_after_deref_latent(int* x) { + *x = 42; // latent error given that x is tested for null below if (x == nullptr) { int* p = nullptr; - *p = 42; + *p = 42; // should be ignored as we can never get there } } diff --git a/infer/tests/codetoanalyze/cpp/pulse/conditional_temporaries.cpp b/infer/tests/codetoanalyze/cpp/pulse/conditional_temporaries.cpp index ef97ca6bb..ae7ea1670 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/conditional_temporaries.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/conditional_temporaries.cpp @@ -43,6 +43,9 @@ struct X { f = x.f + 10; copy_from(x); } + + // should realise [this] cannot be null to avoid FP latent (that can never be + // manifested) ~X() { std::cerr << "~X(" << f << ") " << name(); if (original_counter) { diff --git a/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp b/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp index 72f27acc5..1dab7d846 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp @@ -23,7 +23,9 @@ class UsingDelayedDestruction : folly::DelayedDestruction { delete this; } - void double_delete_ok() { + // should realise [this] cannot be null to avoid FP latent (that can never be + // manifested) + void FP_latent_double_delete_ok() { destroy(); // should not delete this double delete delete this; } diff --git a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp index c009df2a4..8f4e92c67 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp @@ -55,7 +55,9 @@ void delete_inner_then_write_bad(struct X& x) { wraps_read(x); } -void read_write_then_delete_good(struct X& x) { +// latent because delete(&x) creates a path where &x==0 but it was dereferences +// before, but that does not make sense as &x cannot be null +void FP_latent_read_write_then_delete_ok(struct X& x) { wraps_write(x, 10); wraps_read(x); wraps_delete(&x); diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 99e393e2b..c09dd54f4 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,6 @@ codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here] codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here] +codetoanalyze/cpp/pulse/aliasing.cpp, null_test_after_deref_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of null_test_after_deref_latent,invalid access occurs here] codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` accessed here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here] @@ -24,6 +25,7 @@ codetoanalyze/cpp/pulse/closures.cpp, struct_capture_by_val_ok_FP, 7, NULLPTR_DE codetoanalyze/cpp/pulse/closures.cpp, update_inside_lambda_as_argument_ok_FP, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `update_inside_lambda_as_argument` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `update_inside_lambda_as_argument`,return from call to `update_inside_lambda_as_argument`,invalid access occurs here] codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::FP_track_copy_operations_complex_ok, 16, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::FP_track_copy_operations_one_copy_ok, 17, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/conditional_temporaries.cpp, condtemp::X::__infer_inner_destructor_~X, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `this` of condtemp::X::__infer_inner_destructor_~X,when calling `condtemp::X::name` here,parameter `this` of condtemp::X::name,invalid access occurs here] codetoanalyze/cpp/pulse/conditionals.cpp, add_test3_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test3_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test3_latent,invalid access occurs here] codetoanalyze/cpp/pulse/conditionals.cpp, add_test5_latent, 5, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `x` of add_test5_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of add_test5_latent,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs here] @@ -31,6 +33,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_delete_function` here,parameter `a` of deduplication::templated_delete_function,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `deduplication::templated_access_function` here,parameter `a` of deduplication::templated_access_function,invalid access occurs here] codetoanalyze/cpp/pulse/exit_test.cpp, store_exit_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `store_exit` here,parameter `x` of store_exit,invalid access occurs here] +codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::FP_latent_double_delete_ok, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `this` of UsingDelayedDestruction::FP_latent_double_delete_ok,invalid access occurs here] codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here] codetoanalyze/cpp/pulse/frontend.cpp, frontend::FP_init_single_field_struct_ok, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_Frontend_constructor2_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] @@ -39,6 +42,7 @@ codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_set_field_via_local_bad, 5, codetoanalyze/cpp/pulse/frontend.cpp, frontend::conditional_expression_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/frontend.cpp, frontend::deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `frontend::some::thing::bad_ptr` 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 `frontend::some::thing::bad_ptr`,return from call to `frontend::some::thing::bad_ptr`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/frontend.cpp, frontend::not_boolean_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, FP_latent_read_write_then_delete_ok, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of FP_latent_read_write_then_delete_ok,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, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_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, access_to_invalidated_alias_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,assigned,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_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,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] @@ -51,11 +55,13 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, 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] +codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference2_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `test_after_dereference2_latent` here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, call_test_after_dereference_bad, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `FN_test_after_dereference_latent` here,parameter `x` of FN_test_after_dereference_latent,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, deref_nullptr_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `may_return_nullptr` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_nullptr`,return from call to `may_return_nullptr`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::operator=`,parameter `other` of folly::Optional::operator=,passed as argument to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional arg)` (modelled),return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/optional.cpp, cannot_be_empty_FP, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getOptionalValue` here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `getOptionalValue`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `getOptionalValue`,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp index 9cb93d707..ed4d067c7 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp @@ -206,12 +206,12 @@ void call_test_after_dereference_bad() { FN_test_after_dereference_latent(NULL); } -void FN_test_after_dereference2_latent(int* x) { +void test_after_dereference2_latent(int* x) { *x = 42; if (x == 0) ; } -void FN_call_test_after_dereference2_bad() { - FN_test_after_dereference2_latent(NULL); +void call_test_after_dereference2_bad() { + test_after_dereference2_latent(NULL); }