Skip to content

Commit

Permalink
[pulse] fix issue in return value history
Browse files Browse the repository at this point in the history
Summary:
We weren't handling return values correctly and this is why we needed
a special hack to avoid double traces in some cases, but it didn't even
work all the time.

Reviewed By: skcho

Differential Revision: D31479144

fbshipit-source-id: 6a83fdee4
  • Loading branch information
jvillard authored and facebook-github-bot committed Oct 26, 2021
1 parent 70c193d commit 1c02679
Show file tree
Hide file tree
Showing 6 changed files with 22 additions and 49 deletions.
14 changes: 2 additions & 12 deletions infer/src/pulse/PulseAttribute.ml
Original file line number Diff line number Diff line change
Expand Up @@ -218,18 +218,8 @@ module Attribute = struct
Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call}
in
match attr with
| Allocated (proc_name, trace) -> (
match
Trace.trace_up_to_key_event caller_history ~is_key_event:(function
| Allocation _ ->
true
| _ ->
false )
with
| Some alloc_trace ->
Allocated (proc_name, alloc_trace)
| None ->
Allocated (proc_name, add_call_to_trace trace) )
| Allocated (proc_name, trace) ->
Allocated (proc_name, add_call_to_trace trace)
| Invalid (invalidation, trace) ->
Invalid (invalidation, add_call_to_trace trace)
| ISLAbduced trace ->
Expand Down
32 changes: 16 additions & 16 deletions infer/src/pulse/PulseInterproc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -504,26 +504,26 @@ let record_post_for_return ({PathContext.timestamp} as path) callee_proc_name ca
| None ->
(call_state, None)
| Some (return_callee, return_callee_hist) ->
let return_caller_addr_hist =
let return_caller, return_caller_hist =
match AddressMap.find_opt return_callee call_state.subst with
| Some return_caller_hist ->
return_caller_hist
| None ->
(AbstractValue.mk_fresh (), [])
in
( return_caller
, ValueHistory.Call
{f= Call callee_proc_name; location= call_loc; in_call= return_callee_hist; timestamp}
:: return_caller_hist )
let return_caller, return_caller_hist =
match AddressMap.find_opt return_callee call_state.subst with
| Some return_caller_hist ->
return_caller_hist
| None ->
(AbstractValue.mk_fresh (), [])
in
L.d_printfln_escaped "Recording POST from [return] <-> %a" AbstractValue.pp
(fst return_caller_addr_hist) ;
L.d_printfln_escaped "Recording POST from [return] <-> %a" AbstractValue.pp return_caller ;
let call_state =
record_post_for_address path callee_proc_name call_loc pre_post ~addr_callee:return_callee
~addr_hist_caller:return_caller_addr_hist call_state
~addr_hist_caller:(return_caller, return_caller_hist)
call_state
in
(* need to add the call to the returned history too *)
let return_caller_hist =
ValueHistory.Call
{f= Call callee_proc_name; location= call_loc; in_call= return_callee_hist; timestamp}
:: return_caller_hist
in
(call_state, Some return_caller_addr_hist) )
(call_state, Some (return_caller, return_caller_hist)) )


let apply_post_for_parameters path callee_proc_name call_location pre_post ~formals ~actuals
Expand Down
14 changes: 0 additions & 14 deletions infer/src/pulse/PulseTrace.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,20 +15,6 @@ type t =
| ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: t}
[@@deriving compare, equal]

let rec trace_up_to_key_event ~is_key_event history =
match (history : ValueHistory.t) with
| [] ->
None
| event :: past when is_key_event event ->
Some (Immediate {location= ValueHistory.location_of_event event; history= past})
| Call {f; location; in_call} :: past ->
Option.map (trace_up_to_key_event ~is_key_event in_call) ~f:(fun in_call_trace ->
ViaCall {f; location; in_call= in_call_trace; history= past} )
| _event :: past ->
(* [_event ≠ key_event]: we are past the key event if it exists *)
trace_up_to_key_event ~is_key_event past


let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location

let get_outer_history = function Immediate {history; _} | ViaCall {history; _} -> history
Expand Down
3 changes: 0 additions & 3 deletions infer/src/pulse/PulseTrace.mli
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,3 @@ val get_invalidation : t -> Invalidation.t option

val has_invalidation : t -> bool
(** whether the trace contains an invalidation event *)

val trace_up_to_key_event : is_key_event:(ValueHistory.event -> bool) -> ValueHistory.t -> t option
(** turns a history containing a "key event" into a trace leading to the most recent such event *)
4 changes: 2 additions & 2 deletions infer/tests/codetoanalyze/cpp/pulse/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_Frontend_constructor2_bad,
codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_Frontend_constructor_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_set_field_via_local_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::conditional_expression_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,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,in call to `frontend::some::thing::bad_ptr`,allocated by call to `new` (modelled),assigned,returned,return from call to `frontend::some::thing::bad_ptr`,when calling `frontend::some::thing::bad_ptr` here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `frontend::some::thing::bad_ptr`,allocated by call to `new` (modelled),assigned,returned,return from call to `frontend::some::thing::bad_ptr`,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,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `frontend::some::thing::bad_ptr`,allocated by call to `new` (modelled),assigned,returned,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, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, FP_latent_read_write_then_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 `x` of FP_latent_read_write_then_delete_ok,when calling `wraps_write` here,parameter `x` of wraps_write,when calling `wraps_write_inner` here,parameter `x` of wraps_write_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]
Expand All @@ -64,7 +64,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, US
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_inner_then_write_bad,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_inner_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `may_return_invalid_ptr_ok`,allocated by call to `new` (modelled),assigned,returned,return from call to `may_return_invalid_ptr_ok`,when calling `may_return_invalid_ptr_ok` here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `may_return_invalid_ptr_ok`,allocated by call to `new` (modelled),assigned,returned,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `may_return_invalid_ptr_ok`,allocated by call to `new` (modelled),assigned,returned,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, 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,parameter `x` of set_x_then_crash_double_latent,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
Expand Down
4 changes: 2 additions & 2 deletions infer/tests/codetoanalyze/cpp/pulse/issues.exp-isl
Original file line number Diff line number Diff line change
Expand Up @@ -61,14 +61,14 @@ codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_Frontend_constructor2_bad,
codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_Frontend_constructor_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::call_set_field_via_local_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/frontend.cpp, frontend::conditional_expression_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,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,in call to `frontend::some::thing::bad_ptr`,allocated by call to `new` (modelled),assigned,returned,return from call to `frontend::some::thing::bad_ptr`,when calling `frontend::some::thing::bad_ptr` here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `frontend::some::thing::bad_ptr`,allocated by call to `new` (modelled),assigned,returned,return from call to `frontend::some::thing::bad_ptr`,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,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `frontend::some::thing::bad_ptr`,allocated by call to `new` (modelled),assigned,returned,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, [is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, FP_latent_read_write_then_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,when calling `wraps_write` here,when calling `wraps_write_inner` here,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,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner` here,was invalidated by `delete`,use-after-lifetime part of the trace starts here,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,was invalidated by `delete`,use-after-lifetime part of the trace starts here,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete` here,when calling `wraps_delete_inner` here,was invalidated by `delete`,use-after-lifetime part of the trace starts here,when calling `wraps_read` here,when calling `wraps_read_inner` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,in call to `may_return_invalid_ptr_ok`,allocated by call to `new` (modelled),assigned,returned,return from call to `may_return_invalid_ptr_ok`,when calling `may_return_invalid_ptr_ok` here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `may_return_invalid_ptr_ok`,allocated by call to `new` (modelled),assigned,returned,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,when calling `store` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,in call to `may_return_invalid_ptr_ok`,allocated by call to `new` (modelled),assigned,returned,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,when calling `store` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, 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,when calling `set_first_non_null_ok` here,invalid access occurs here]
codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here]
Expand Down

0 comments on commit 1c02679

Please sign in to comment.