From 9b8a908ad33b5f59e46efdfe7beba97b26106915 Mon Sep 17 00:00:00 2001 From: Peter O'Hearn Date: Thu, 30 May 2019 05:16:24 -0700 Subject: [PATCH] [Pulse] model folly delayed destruction Reviewed By: jvillard Differential Revision: D15508919 fbshipit-source-id: f6073ef7c --- infer/src/pulse/PulseModels.ml | 7 ++++- .../cpp/pulse/folly_DestructorGuard.cpp | 30 +++++++++++++++++++ .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + 3 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 4fabff7d6..0c5fabaf1 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -174,11 +174,16 @@ module StdVector = struct Ok [astate] end +module DelayedDestruction = struct + let destroy : model = fun _ ~ret:_ ~actuals:_ astate -> Ok [astate] +end + module ProcNameDispatcher = struct let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher = let open ProcnameDispatcher.ProcName in make_dispatcher - [ -"std" &:: "function" &:: "operator()" &--> Cplusplus.operator_call + [ -"folly" &:: "DelayedDestruction" &:: "destroy" &--> DelayedDestruction.destroy + ; -"std" &:: "function" &:: "operator()" &--> Cplusplus.operator_call ; -"std" &:: "vector" &:: "assign" &--> StdVector.invalidate_references Assign ; -"std" &:: "vector" &:: "clear" &--> StdVector.invalidate_references Clear ; -"std" &:: "vector" &:: "emplace" &--> StdVector.invalidate_references Emplace diff --git a/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp b/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp new file mode 100644 index 000000000..fddba9b9a --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp @@ -0,0 +1,30 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +namespace folly { + +class DelayedDestructionBase {}; + +class DelayedDestruction : public DelayedDestructionBase { + public: + virtual void destroy() { delete this; } // model ignores delete +}; + +} // namespace folly + +class UsingDelayedDestruction : folly::DelayedDestruction { + + void double_delete_bad() { + delete this; + delete this; + } + + void double_delete_ok() { + destroy(); // should not delete this double delete + delete this; + } +}; diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 350a66208..a6453dfae 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -6,6 +6,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `a->f` here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 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` on `a` here,use-after-lifetime part of the trace starts here,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `a->f` 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` on `a` here,use-after-lifetime part of the trace starts here,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `a->f` 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` on `this` here,use-after-lifetime part of the trace starts here,invalid access to `this` 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 to `y`,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,assigned to `z`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` 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` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` 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` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `x->f` here]