From 5278cb7374a6ec3133f32c77a0d7d6e35e854d4f Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Tue, 25 Aug 2020 01:52:54 -0700
Subject: [PATCH] [pulse] `delete nullptr` is a no-op

Summary:
`delete` works exactly like `free` so merge both models together. Also
move the `free(0)` test to nullptr.cpp as it seems more appropriate.

Reviewed By: da319

Differential Revision: D23241297

fbshipit-source-id: 20a32ac54
---
 infer/src/pulse/PulseModels.ml                | 21 +++++++++----------
 .../tests/codetoanalyze/cpp/pulse/nullptr.cpp | 10 +++++++++
 .../cpp/pulse/use_after_free.cpp              |  5 -----
 3 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 011731ddd..19172a3ba 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -81,10 +81,9 @@ module Misc = struct
   let id_first_arg arg_access_hist : model =
    fun _ ~callee_procname:_ _ ~ret astate ->
     PulseOperations.write_id (fst ret) arg_access_hist astate |> PulseOperations.ok_continue
-end
 
-module C = struct
-  let free deleted_access : model =
+
+  let free_or_delete operation deleted_access : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we
        currently know about the value. This is purely to avoid contributing to path explosion. *)
@@ -93,9 +92,15 @@ module C = struct
       PulseOperations.ok_continue astate
     else
       let astate = PulseArithmetic.and_positive (fst deleted_access) astate in
-      let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
+      let invalidation =
+        match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete
+      in
+      let+ astate = PulseOperations.invalidate location invalidation deleted_access astate in
       [ExecutionDomain.ContinueProgram astate]
+end
 
+module C = struct
+  let free deleted_access : model = Misc.free_or_delete `Free deleted_access
 
   let malloc _ : model =
    fun _ ~callee_procname location ~ret:(ret_id, _) astate ->
@@ -225,13 +230,7 @@ module FollyOptional = struct
 end
 
 module Cplusplus = struct
-  let delete deleted_access : model =
-   fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let+ astate =
-      PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate
-    in
-    [ExecutionDomain.ContinueProgram astate]
-
+  let delete deleted_access : model = Misc.free_or_delete `Delete deleted_access
 
   let placement_new actuals : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
diff --git a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp
index 85d216e23..67f4723c8 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/nullptr.cpp
@@ -184,3 +184,13 @@ void explicit_check_for_null_ok(Handle h) { return h->foo(); }
 X* checks_for_null() { return getX(true) == nullptr ? nullptr : new X(); }
 
 void cannot_be_null_ok() { return checks_for_null()->foo(); }
+
+void free_nullptr_ok() {
+  int* p = nullptr;
+  free(p);
+}
+
+void delete_nullptr_ok() {
+  int* p = nullptr;
+  delete p;
+}
diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp
index 9e5cf5b5d..7ff1679d3 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp
@@ -24,8 +24,3 @@ void double_free_global_bad() {
   free_global_pointer_ok();
   free_global_pointer_ok();
 }
-
-void free_nullptr_ok() {
-  int* p = nullptr;
-  free(p);
-}