[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

@@ -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 ->

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

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