From 86decb83f6ec66297274b88ef2d9d18a6de43f9a Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 28 Jun 2019 09:27:29 -0700 Subject: [PATCH] [pulse] record attributes of address not edge-reachable in the post Summary: Sometimes the post of a function call has attributes on addresses that were mentioned in the pre but are no longer reachable in the post. We don't want to forget these, see added test. Reviewed By: mbouaziz Differential Revision: D16050050 fbshipit-source-id: 1ce522b97 --- infer/src/pulse/PulseAbductiveDomain.ml | 31 ++++++++++++++++++- infer/src/pulse/PulseDomain.ml | 4 +++ infer/src/pulse/PulseDomain.mli | 2 ++ .../cpp/pulse/interprocedural.cpp | 11 +++++++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + 5 files changed, 48 insertions(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 1341b7e40..dc9151c55 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -671,6 +671,32 @@ module PrePost = struct call_state + let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state = + let heap0 = (call_state.astate.post :> base_domain).heap in + let heap = + PulseDomain.Memory.fold_attrs + (fun addr_callee attrs heap -> + if AddressSet.mem addr_callee call_state.visited then + (* already recorded the attributes when we were walking the edges map *) heap + else + match AddressMap.find_opt addr_callee call_state.subst with + | None -> + (* callee address has no meaning for the caller *) heap + | Some addr_caller -> + let attrs' = + Attributes.map + ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr) + attrs + in + PulseDomain.Memory.set_attrs addr_caller attrs' heap ) + (pre_post.post :> PulseDomain.t).heap heap0 + in + if phys_equal heap heap0 then call_state + else + let post = Domain.make (call_state.astate.post :> PulseDomain.t).stack heap in + {call_state with astate= {call_state.astate with post}} + + let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; let r = @@ -678,7 +704,10 @@ module PrePost = struct call_state |> apply_post_for_globals callee_proc_name call_location pre_post |> record_post_for_return callee_proc_name call_location pre_post - |> fun ({astate; _}, return_caller) -> (astate, return_caller) + |> fun (call_state, return_caller) -> + ( record_post_remaining_attributes callee_proc_name call_location pre_post call_state + , return_caller ) + |> fun ({astate}, return_caller) -> (astate, return_caller) in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 9b8e5af30..813623dde 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -384,6 +384,8 @@ module Memory : sig val find_opt : AbstractAddress.t -> t -> cell option + val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t val set_edges : AbstractAddress.t -> edges -> t -> t @@ -515,6 +517,8 @@ end = struct Some (edges, attrs) + let fold_attrs f memory init = Graph.fold f (snd memory) init + let set_attrs addr attrs memory = (fst memory, Graph.add addr attrs (snd memory)) let set_edges addr edges memory = (Graph.add addr edges (fst memory), snd memory) diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 0fc1b75b3..d873974d8 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -143,6 +143,8 @@ module Memory : sig val find_opt : AbstractAddress.t -> t -> cell option + val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc + val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t val set_edges : AbstractAddress.t -> edges -> t -> t diff --git a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp index 533fcf830..4fbff9995 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp @@ -94,3 +94,14 @@ void feed_invalid_into_access_bad() { struct Y* y = may_return_invalid_ptr_ok(); call_store(y); } + +void invalidate_and_set_to_null(struct X** x_ptr) { + delete (*x_ptr); + *x_ptr = nullptr; +} + +void access_to_invalidated_alias(struct X* x, struct X* y) { + y = x; + invalidate_and_set_to_null(&x); + wraps_read(*y); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index ea35bcdef..1393c247a 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -9,6 +9,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here 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,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `invalidate_and_set_to_null()` here,memory was invalidated by `delete` here,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 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,memory was invalidated by `delete` here,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 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,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]