[Pulse] model folly delayed destruction

Reviewed By: jvillard

Differential Revision: D15508919

fbshipit-source-id: f6073ef7c

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

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;
+  }
+};

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -6,6 +6,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::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<int>, 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]