From 186b10e4f59f835774fb8195290b6fc04d673e2b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 5 May 2021 03:45:18 -0700 Subject: [PATCH] [pulse] record all the invalidations we can in histories Summary: Building on the infra in the previous commits, "fix" all the call sites that introduce invalidations to make sure they also update the corresponding histories. This is only possible to do when the access leading to the invalidation can be recorded. Right now the only place that's untraceable is the model of `free`/`delete`, because it happens to be the only place where we invalidate an address without knowing where it comes from (`free(v)`: what was v's access path? we could track this in the future). Reviewed By: skcho Differential Revision: D28118764 fbshipit-source-id: de67f449e --- infer/src/pulse/Pulse.ml | 4 +- infer/src/pulse/PulseModels.ml | 49 +++++++++++++------ infer/src/pulse/PulseOperations.ml | 44 +++++++++++++++-- infer/src/pulse/PulseOperations.mli | 18 ++++++- infer/tests/codetoanalyze/c/pulse/issues.exp | 6 +-- infer/tests/codetoanalyze/c/pulse/traces.c | 1 + .../tests/codetoanalyze/cpp/pulse/issues.exp | 29 +++++------ .../tests/codetoanalyze/cpp/pulse/traces.cpp | 17 +++++++ .../tests/codetoanalyze/java/pulse/issues.exp | 12 ++--- 9 files changed, 137 insertions(+), 43 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/traces.cpp diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 50c80a2d4..ca42e830c 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -84,7 +84,9 @@ module PulseTransferFunctions = struct PulseOperations.eval NoAccess call_loc (Exp.Lvar pvar) astate in (* invalidate [&x] *) - PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate + PulseOperations.invalidate + (StackAddress (Var.of_pvar pvar, [])) + call_loc gone_out_of_scope out_of_scope_base astate >>| ExecutionDomain.continue | ISLLatentMemoryError _ | AbortProgram _ diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 09c6e7f5c..be0e74f92 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -135,7 +135,9 @@ module Misc = struct let+ astate = result in ContinueProgram astate ) else - let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in + let<+> astate = + PulseOperations.invalidate UntraceableAccess location invalidation deleted_access astate + in astate in let<*> astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in @@ -179,9 +181,10 @@ module C = struct let malloc_common ~size_exp_opt : model = fun {analysis_data= {tenv}; callee_procname; location; ret= ret_id, _} astate -> let ret_addr = AbstractValue.mk_fresh () in - let ret_value = - (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) + let ret_hist = + [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}] in + let ret_value = (ret_addr, ret_hist) in let astate = PulseOperations.write_id ret_id ret_value astate in let<*> astate_alloc = PulseOperations.allocate callee_procname location ret_value astate @@ -191,7 +194,9 @@ module C = struct 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 + (StackAddress (Var.of_id ret_id, ret_hist)) + location (ConstantDereference IntLit.zero) ret_value in ContinueProgram astate_null in @@ -285,7 +290,7 @@ module Optional = struct let* astate, value_field = to_internal_value Read location this astate in let value_hist = (fst value, event :: snd value) in let+ astate = PulseOperations.write_deref location ~ref:value_field ~obj:value_hist astate in - (astate, value_hist) + (astate, value_field, value_hist) let assign_value_fresh location this ~desc astate = @@ -294,16 +299,20 @@ module Optional = struct let assign_none this ~desc : model = fun {location} astate -> - let<*> astate, value = assign_value_fresh location this ~desc astate in + let<*> astate, pointer, value = assign_value_fresh location this ~desc astate in let<*> astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in - let<+> astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in + let<+> astate = + PulseOperations.invalidate + (MemoryAccess {pointer; access= Dereference; hist_obj_default= snd value}) + location Invalidation.OptionalEmpty value astate + in astate let assign_value this _value ~desc : model = fun {location} astate -> (* TODO: call the copy constructor of a value *) - let<*> astate, value = assign_value_fresh location this ~desc astate in + let<*> astate, _, value = assign_value_fresh location this ~desc astate in let<+> astate = PulseArithmetic.and_positive (fst value) astate in astate @@ -311,13 +320,13 @@ module Optional = struct let assign_optional_value this init ~desc : model = fun {location} astate -> let<*> astate, value = to_internal_value_deref Read location init astate in - let<+> astate, _ = write_value location this ~value ~desc astate in + let<+> astate, _, _ = write_value location this ~value ~desc astate in astate let emplace optional ~desc : model = fun {location} astate -> - let<+> astate, _ = assign_value_fresh location optional ~desc astate in + let<+> astate, _, _ = assign_value_fresh location optional ~desc astate in astate @@ -359,7 +368,9 @@ module Optional = struct 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 + >>= PulseOperations.invalidate + (StackAddress (Var.of_id ret_id, snd nullptr)) + location (ConstantDereference IntLit.zero) nullptr in [Ok (ContinueProgram astate_value_addr); Ok (ContinueProgram astate_null)] @@ -581,7 +592,14 @@ module StdBasicString = struct let<*> astate = PulseOperations.invalidate_access location CppDelete string_addr_hist Dereference astate in - let<+> astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in + let<+> astate = + PulseOperations.invalidate + (MemoryAccess + { pointer= this_hist + ; access= internal_string_access + ; hist_obj_default= snd string_addr_hist }) + location CppDelete string_addr_hist astate + in astate end @@ -1189,8 +1207,11 @@ module JavaCollection = struct >>= PulseArithmetic.and_eq_int not_found_val IntLit.zero >>= PulseArithmetic.and_eq_int is_empty_expected_val IntLit.one in - let astate = PulseOperations.write_id ret_id (not_found_val, [event]) astate in - PulseOperations.invalidate location (ConstantDereference IntLit.zero) + let hist = [event] in + let astate = PulseOperations.write_id ret_id (not_found_val, hist) astate in + PulseOperations.invalidate + (StackAddress (Var.of_id ret_id, hist)) + location (ConstantDereference IntLit.zero) (not_found_val, [event]) astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 3d47f6727..c78be3cdc 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -372,9 +372,38 @@ let add_dynamic_type typ address astate = AddressAttributes.add_dynamic_type typ let remove_allocation_attr address astate = AddressAttributes.remove_allocation_attr address astate -let invalidate location cause addr_trace astate = +type invalidation_access = + | MemoryAccess of + { pointer: AbstractValue.t * ValueHistory.t + ; access: BaseMemory.Access.t + ; hist_obj_default: ValueHistory.t } + | StackAddress of Var.t * ValueHistory.t + | UntraceableAccess + +let record_invalidation access_path location cause astate = + match access_path with + | StackAddress (x, hist0) -> + let astate, (addr, hist) = Stack.eval location hist0 x astate in + Stack.add x (addr, Invalidated (cause, location) :: hist) astate + | MemoryAccess {pointer; access; hist_obj_default} -> + let addr_obj, hist_obj = + match Memory.find_edge_opt (fst pointer) access astate with + | Some addr_hist -> + addr_hist + | None -> + (AbstractValue.mk_fresh (), hist_obj_default) + in + Memory.add_edge pointer access + (addr_obj, Invalidated (cause, location) :: hist_obj) + location astate + | UntraceableAccess -> + astate + + +let invalidate access_path location cause addr_trace astate = check_addr_access NoAccess location addr_trace astate >>| AddressAttributes.invalidate addr_trace cause location + >>| record_invalidation access_path location cause let invalidate_biad_isl location cause (address, history) astate = @@ -385,8 +414,12 @@ let invalidate_biad_isl location cause (address, history) astate = let invalidate_access location cause ref_addr_hist access astate = - let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist access astate in - invalidate location cause (addr_obj, snd ref_addr_hist) astate + let astate, (addr_obj, hist_obj) = Memory.eval_edge ref_addr_hist access astate in + invalidate + (MemoryAccess {pointer= ref_addr_hist; access; hist_obj_default= hist_obj}) + location cause + (addr_obj, snd ref_addr_hist) + astate let invalidate_array_elements location cause addr_trace astate = @@ -397,8 +430,11 @@ let invalidate_array_elements location cause addr_trace astate = | Some edges -> Memory.Edges.fold edges ~init:astate ~f:(fun astate (access, dest_addr_trace) -> match (access : Memory.Access.t) with - | ArrayAccess _ -> + | ArrayAccess _ as access -> AddressAttributes.invalidate dest_addr_trace cause location astate + |> record_invalidation + (MemoryAccess {pointer= addr_trace; access; hist_obj_default= snd dest_addr_trace}) + location cause | _ -> astate ) diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 38f0d577e..41d423bc4 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -158,8 +158,24 @@ val write_deref_biad_isl : -> t -> t AccessResult.t list +(** the way that was used to get to the invalidated address in the state; this is used to record the + invalidation point in its history in addition to inside the [Invalid] attribute *) +type invalidation_access = + | MemoryAccess of + { pointer: AbstractValue.t * ValueHistory.t + ; access: BaseMemory.Access.t + ; hist_obj_default: ValueHistory.t } + (** the value was read from the heap following the [access] edge at address [pointer] *) + | StackAddress of Var.t * ValueHistory.t (** the value was read from the stack *) + | UntraceableAccess (** we don't know where the value came from; avoid using if possible *) + val invalidate : - Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t + invalidation_access + -> Location.t + -> Invalidation.t + -> AbstractValue.t * ValueHistory.t + -> t + -> t AccessResult.t (** record that the address is invalid *) val invalidate_biad_isl : diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 60c82246b..1551ea6ea 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -15,15 +15,15 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_buck codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here] -codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,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,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] +codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, simple_deref, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, simple_deref_via_alias, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,assigned,invalid access occurs here] -codetoanalyze/c/pulse/traces.c, something_about_strings_latent, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,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,allocated by call to `malloc` (modelled),assigned,invalid access occurs here] +codetoanalyze/c/pulse/traces.c, something_about_strings_latent, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,allocated by call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, interprocedural_nop_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/traces.c b/infer/tests/codetoanalyze/c/pulse/traces.c index 65ad186fa..5defbb4ff 100644 --- a/infer/tests/codetoanalyze/c/pulse/traces.c +++ b/infer/tests/codetoanalyze/c/pulse/traces.c @@ -4,6 +4,7 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. */ + #include #include diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index a960a245f..4d2f32733 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -63,23 +63,23 @@ codetoanalyze/cpp/pulse/nullptr.cpp, no_check_return_bad, 2, NULLPTR_DEREFERENCE codetoanalyze/cpp/pulse/nullptr.cpp, std_false_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,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, get_pointer_no_check_none_check_bad, 3, 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::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, inside_try_catch_FP, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `might_return_none` 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 `might_return_none`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `might_return_none`,invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, 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::Optional(folly::Optional arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional arg)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, 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),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, not_none_check_value_ok_FP, 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),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts 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 `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),passed as argument to `std::optional::operator=(std::optional arg)` (modelled),return from call to `std::optional::operator=(std::optional arg)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts 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 `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),passed as argument to `std::optional::optional(std::optional arg)` (modelled),return from call to `std::optional::optional(std::optional arg)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts 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 `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, std_not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts 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 `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here] -codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 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, 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),is optional empty,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, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,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, get_pointer_no_check_none_check_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, inside_try_catch_FP, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `might_return_none` 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 `might_return_none`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,return from call to `might_return_none`,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,passed as argument to `folly::Optional::Optional(folly::Optional arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional arg)` (modelled),invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, std_assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),is optional empty,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, std_assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,passed as argument to `std::optional::operator=(std::optional arg)` (modelled),return from call to `std::optional::operator=(std::optional arg)` (modelled),invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, std_none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,passed as argument to `std::optional::optional(std::optional arg)` (modelled),return from call to `std::optional::optional(std::optional arg)` (modelled),invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, std_none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, std_not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,invalid access occurs here] +codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 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),is optional empty,return from call to `folly::Optional::operator=`,invalid access occurs here] codetoanalyze/cpp/pulse/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,source of the null value part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/path.cpp, only_bad_on_42_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here] -codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here] +codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,returned here] @@ -97,6 +97,7 @@ codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::load_store_possible_npe_ba codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_test_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `new` (modelled),return from call to `new` (modelled),passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr::~UniquePtr` here,parameter `this` of temporaries::UniquePtr::~UniquePtr,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `new` (modelled),return from call to `new` (modelled),passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::get`,return from call to `temporaries::UniquePtr::get`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/traces.cpp, access_destructed_string, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,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,variable `s` declared here,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/uninit.cpp, Uninit::call_init_by_store_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `i` created,read to uninitialized value occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/traces.cpp b/infer/tests/codetoanalyze/cpp/pulse/traces.cpp new file mode 100644 index 000000000..6c935b240 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/traces.cpp @@ -0,0 +1,17 @@ +/* + * 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. + */ + +#include + +void access_destructed_string() { + const char* ptr; + { + std::string s = "blah"; + ptr = s.data(); + } + char first_char = *ptr; +} diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 1869d2785..f11efe8b1 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -14,10 +14,10 @@ codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicD codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object DynamicDispatch$Subtype.foo()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object DynamicDispatch$Subtype.foo()`,return from call to `Object DynamicDispatch$Subtype.foo()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicResolutionWithVariadicMethodBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,return from call to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object DynamicDispatch$Impl.foo()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object DynamicDispatch$Impl.foo()`,return from call to `Object DynamicDispatch$Impl.foo()`,assigned,invalid access occurs here] -codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.FP_latent_getFromKeySetOk(java.util.HashMap):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] -codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,invalid access occurs here] -codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,invalid access occurs here] -codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getOneIntegerWithoutCheckBad():int, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.FP_latent_getFromKeySetOk(java.util.HashMap):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getOneIntegerWithoutCheckBad():int, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.checkInstanceArray(java.lang.Object):void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfBooleanArrayBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `void InstanceOfExample.checkInstanceArray(Object)`,is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfNullIntraBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] @@ -44,14 +44,14 @@ codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.Nu codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_sinkWithNeverNullSource():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `T NeverNullSource.get()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `T NeverNullSource.get()`,return from call to `T NeverNullSource.get()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.NPEvalueOfFromHashmapBad(java.util.HashMap,int):int, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),invalid access occurs here] +codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.NPEvalueOfFromHashmapBad(java.util.HashMap,int):int, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.getObj()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.getObj()`,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNull():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.derefUndefinedCallee()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.derefUndefinedCallee()`,return from call to `Object NullPointerExceptions.derefUndefinedCallee()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.nullableRet(boolean)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.nullableRet(boolean)`,return from call to `Object NullPointerExceptions.nullableRet(boolean)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)`,return from call to `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,invalid access occurs here] +codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerException():int, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionArrayLength():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionCallArrayReadMethod():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)`,return from call to `Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)`,assigned,invalid access occurs here]