[pulse] Adding null case to malloc's model

Summary:
Malloc returns either an allocated object or a null pointer if there is no memory available. Modelling that.
This has always been a bit contentious because this leads to NPEs that people often ignores because they don't care. But if we don't model this, then we have FPs when people do take this into account when freeing the memory.

Reviewed By: jvillard

Differential Revision: D20791692

fbshipit-source-id: 6fd259f12

infer/src/bufferoverrun/itv.mli

@@ -31,6 +31,9 @@ module ItvPure : sig
 
   val nat : t
 
+  val pos : t
+  (** [1, +oo] *)
+
   val of_int : int -> t
 
   val lb : t -> Bound.t

infer/src/pulse/PulseCItv.ml

@@ -121,6 +121,8 @@ module Unsafe : sig
   val equal_to : IntLit.t -> t
 
   val not_equal_to : IntLit.t -> t
+
+  val ge_to : IntLit.t -> t
 end = struct
   type t = Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t [@@deriving compare]
 
@@ -140,6 +142,10 @@ end = struct
 
 
   let not_equal_to i = Outside (i, i)
+
+  let ge_to i =
+    let b = Bound.Int i in
+    Between (b, Bound.PlusInfinity)
 end
 
 include Unsafe

infer/src/pulse/PulseCItv.mli

@@ -39,3 +39,5 @@ val binop : Binop.t -> t -> t -> t option
 val unop : Unop.t -> t -> t option
 
 val zero_inf : t
+
+val ge_to : IntLit.t -> t

infer/src/pulse/PulseModels.ml

@@ -88,10 +88,25 @@ module C = struct
       [astate]
 
 
-  let malloc access : model =
+  let malloc _ : model =
    fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate ->
-    let astate = PulseOperations.allocate callee_procname location access astate in
-    Ok [PulseOperations.write_id ret_id access astate]
+    let ret_addr = AbstractValue.mk_fresh () in
+    let astate_alloc =
+      PulseOperations.allocate callee_procname location (ret_addr, []) astate
+      |> PulseOperations.write_id ret_id (ret_addr, [])
+      |> AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.pos)
+      |> AddressAttributes.add_one ret_addr
+           (CItv (CItv.ge_to IntLit.one, Immediate {location; history= []}))
+    in
+    let+ astate_null =
+      AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit IntLit.zero)) astate
+      |> AddressAttributes.add_one ret_addr
+           (CItv (CItv.equal_to IntLit.zero, Immediate {location; history= []}))
+      |> PulseOperations.write_id ret_id (ret_addr, [])
+      |> PulseOperations.invalidate location (Invalidation.ConstantDereference IntLit.zero)
+           (ret_addr, [])
+    in
+    [astate_alloc; astate_null]
 end
 
 module Cplusplus = struct

infer/tests/codetoanalyze/c/pulse/memory_leak.c

@@ -15,9 +15,11 @@ int* malloc_returned_ok() {
 
 void malloc_then_free_ok() {
   int* p = malloc(sizeof(p));
+  if (p) {
     *p = 5;
     free(p);
   }
+}
 
 int* create_p() {
   int* p = malloc(sizeof(p));