[pulse] model the fact `free(0)` is a no-op

Summary:
It's a well-known fact that pulse should know too. To avoid splitting
the abstract state systematically, only act if we know the pointer is
exactly 0 to avoid reporting a nullptr dereference on `free(x)`.

Reviewed By: ezgicicek

Differential Revision: D18708575

fbshipit-source-id: 1cc3f6908

infer/src/pulse/PulseArithmetic.ml

@@ -161,6 +161,13 @@ let pp fmt = function
       F.fprintf fmt "∉[%a,%a]" IntLit.pp l IntLit.pp u
 
 
+let is_equal_to_zero = function
+  | Between (Int l, Int u) when IntLit.iszero l && IntLit.iszero u ->
+      true
+  | _ ->
+      false
+
+
 let has_empty_intersection a1 a2 =
   match (a1, a2) with
   | Outside _, Outside _ ->

infer/src/pulse/PulseArithmetic.mli

@@ -7,15 +7,12 @@
 open! IStd
 module F = Format
 
-module Bound : sig
+type t [@@deriving compare]
-  type t = Int of IntLit.t | MinusInfinity | PlusInfinity
-end
-
-type t = private Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t
-[@@deriving compare]
 
 val equal_to : IntLit.t -> t
 
+val is_equal_to_zero : t -> bool
+
 val pp : F.formatter -> t -> unit
 
 type abduction_result =

infer/src/pulse/PulseModels.ml

@@ -57,7 +57,13 @@ end
 module C = struct
   let free deleted_access : model =
    fun ~caller_summary:_ location ~ret:_ astate ->
-    PulseOperations.invalidate location Invalidation.CFree deleted_access astate >>| List.return
+    match Memory.get_arithmetic (fst deleted_access) astate with
+    | Some (arith, _) when Arithmetic.is_equal_to_zero arith ->
+        (* freeing 0 is a no-op *)
+        Ok [astate]
+    | _ ->
+        PulseOperations.invalidate location Invalidation.CFree deleted_access astate
+        >>| fun astate -> [astate]
 end
 
 module Cplusplus = struct

infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp

@@ -24,3 +24,8 @@ void double_free_global_bad() {
   free_global_pointer_ok();
   free_global_pointer_ok();
 }
+
+void free_nullptr_ok() {
+  int* p = nullptr;
+  free(p);
+}