From 881bcb8fce2fdfe97cf72311b7b9a6b8ecb7288f Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Thu, 1 Nov 2018 09:16:33 -0700 Subject: [PATCH] [pulse] Clean up placement new model Summary: Do not create a new location for placement new argument if it already exists. Reviewed By: jvillard Differential Revision: D12839942 fbshipit-source-id: 758b67a82 --- infer/src/checkers/PulseDomain.mli | 2 -- infer/src/checkers/PulseModels.ml | 16 +++++++--------- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 3 ++- .../cpp/pulse/use_after_destructor.cpp | 9 +++++++++ 4 files changed, 18 insertions(+), 12 deletions(-) diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index e56b0e52c..18a6d99a9 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -11,8 +11,6 @@ module AbstractAddress : sig type t = private int [@@deriving compare] val nullptr : t - - val mk_fresh : unit -> t end type t diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index db6ad5d58..f7dcf5342 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -42,18 +42,16 @@ module Cplusplus = struct let placement_new : model = fun location ~ret:(ret_var, _) ~actuals astate -> + let read_all args astate = + PulseDomain.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate + in match List.rev actuals with | HilExp.AccessExpression expr :: other_actuals -> - let new_address = PulseDomain.AbstractAddress.mk_fresh () in - PulseDomain.write location expr new_address astate - >>| PulseDomain.write_var ret_var new_address - >>= PulseDomain.read_all location - (List.concat_map other_actuals ~f:HilExp.get_access_exprs) + PulseDomain.read location expr astate + >>= fun (astate, address) -> + Ok (PulseDomain.write_var ret_var address astate) >>= read_all other_actuals | _ :: other_actuals -> - PulseDomain.read_all location - (List.concat_map other_actuals ~f:HilExp.get_access_exprs) - astate - >>| PulseDomain.write_var ret_var (PulseDomain.AbstractAddress.mk_fresh ()) + read_all other_actuals astate >>| PulseDomain.havoc_var ret_var | _ -> Ok astate end diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 0854c3b68..63b1d71d1 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -11,8 +11,9 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, FP_reinit_after_explicit_destr codetoanalyze/cpp/pulse/use_after_destructor.cpp, double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 54, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 132, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 140, column 3 here,accessed `alias` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 149, column 3 here,accessed `alias` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 185, column 3 here,accessed `pc->f` here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 194, column 3 here,accessed `pc->f` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here] codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 here,accessed `*(elt)` here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 675d843f2..67d3df978 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -141,6 +141,15 @@ S* placement_new_aliasing2_bad() { return alias; // bad, returning freed memory } +S* placement_new_aliasing3_bad() { + S* s = new S(1); + s->~S(); + S* alias = s; + auto alias_placement = new (s) S(2); + delete s; // this deletes alias too + return alias; // bad, returning freed memory +} + void placement_new_non_var_ok() { struct M { S* s;