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;