From 7c90480758e2b98bdcddeaa21fd48023efa7e7c3 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 11 Apr 2019 03:55:30 -0700 Subject: [PATCH] [pulse] do not create `&` back-edges eagerly Summary: This mostly doesn't make sense. The only thing this would have been good for was to give the most accurate result on access paths such as `*(&(x.f))`, but these are normalised anyway (into `x.f`) so we actually never see these. That said there might be some use to some similar logic in the future, but in the meantime let's delete the current feature as it wasn't thought through. Reviewed By: ezgicicek Differential Revision: D14753492 fbshipit-source-id: 597cec027 --- infer/src/pulse/PulseAbductiveDomain.ml | 11 ++--------- infer/src/pulse/PulseAbductiveDomain.mli | 3 --- infer/src/pulse/PulseDomain.ml | 15 --------------- infer/src/pulse/PulseDomain.mli | 2 -- infer/src/pulse/PulseOperations.ml | 2 +- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 1 - .../cpp/pulse/use_after_destructor.cpp | 2 +- 7 files changed, 4 insertions(+), 32 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 3c526b790..a0e8a9264 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -161,11 +161,6 @@ module Memory = struct map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap) - let add_edge_and_back_edge addr access new_addr_trace astate = - map_post_heap astate ~f:(fun heap -> - BaseMemory.add_edge_and_back_edge addr access new_addr_trace heap ) - - let materialize_edge addr access astate = match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with | Some addr_trace' -> @@ -173,13 +168,11 @@ module Memory = struct | None -> let addr_trace' = (AbstractAddress.mk_fresh (), []) in let post_heap = - BaseMemory.add_edge_and_back_edge addr access addr_trace' - (astate.post :> base_domain).heap + BaseMemory.add_edge addr access addr_trace' (astate.post :> base_domain).heap in let foot_heap = if BaseMemory.mem_edges addr (astate.pre :> base_domain).heap then - BaseMemory.add_edge_and_back_edge addr access addr_trace' - (astate.pre :> base_domain).heap + BaseMemory.add_edge addr access addr_trace' (astate.pre :> base_domain).heap |> BaseMemory.register_address (fst addr_trace') else (astate.pre :> base_domain).heap in diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index d73d3bb50..f8d9ce2f6 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -42,9 +42,6 @@ module Memory : sig val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t - val add_edge_and_back_edge : - AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t - val check_valid : HilExp.AccessExpression.t PulseTrace.action -> AbstractAddress.t diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index c1c714888..fe4e8f6b5 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -171,8 +171,6 @@ module Memory : sig val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t - val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t - val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t @@ -223,19 +221,6 @@ end = struct else (Graph.add addr_src new_edges (fst memory), snd memory) - (** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because - [*(&x) = &( *x ) = x]. *) - let add_edge_and_back_edge addr_src (access : Access.t) addr_trace_dst memory = - let memory = add_edge addr_src access addr_trace_dst memory in - match access with - | ArrayAccess _ | FieldAccess _ -> - memory - | TakeAddress -> - add_edge (fst addr_trace_dst) Dereference (addr_src, []) memory - | Dereference -> - add_edge (fst addr_trace_dst) TakeAddress (addr_src, []) memory - - let find_edge_opt addr access memory = let open Option.Monad_infix in Graph.find_opt addr (fst memory) >>= Edges.find_opt access diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 9d4430d78..b8d7e75a0 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -89,8 +89,6 @@ module Memory : sig val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t - val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t - val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 64ca64078..49ecdf44b 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -52,7 +52,7 @@ let rec walk ~dereference_to_ignore action ~on_last addr_trace path astate = | [a], `Overwrite new_addr_trace -> check_addr_access_optional action addr_trace astate >>| fun astate -> - let astate = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate in + let astate = Memory.add_edge (fst addr_trace) a new_addr_trace astate in (astate, new_addr_trace) | a :: path, _ -> check_addr_access_optional action addr_trace astate diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 1fce70b0a..b478adaf0 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -21,7 +21,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DE codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed `s->f` here,start of value trace,assigned to `s`] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed during call to `Simple` here,accessed `__param_0->f` here,start of value trace,assigned to `s`] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed `s->f` here,start of value trace,assigned to `s`] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_destruct_pointer_contents_then_placement_new2_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `~S` here,invalidated by during call to `__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,start of use after lifetime trace,accessed during call to `S` here,accessed `*(this->f)` here,start of value trace,returned from call to `(sizeof(use_after_destructor::S),&(s->f))`] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `~S` here,invalidated by during call to `__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,start of use after lifetime trace,accessed during call to `~S` here,accessed during call to `__infer_inner_destructor_~S` here,accessed `this->f` here,start of value trace,variable declared] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `alias` here,start of use after lifetime trace,accessed `s->f` here,start of value trace,assigned to `s`] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed `alias->f` here,start of value trace,assigned to `s`,returned from call to `(sizeof(use_after_destructor::S),s)`,assigned to `alias`] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index d010c42ea..b22d73846 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -135,7 +135,7 @@ int* destruct_pointer_contents_then_placement_new1_ok(S* s) { return s->f; } -int* FP_destruct_pointer_contents_then_placement_new2_ok(S* s) { +int* destruct_pointer_contents_then_placement_new2_ok(S* s) { s->~S(); new (&(s->f)) S(1); return s->f;