From dba4140a7b0eec3fe8338216c7da6131dff3701c Mon Sep 17 00:00:00 2001
From: Dulma Churchill <dulmarod@fb.com>
Date: Tue, 7 Apr 2020 02:37:01 -0700
Subject: [PATCH] [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               |  3 +++
 infer/src/pulse/PulseCItv.ml                  |  6 ++++++
 infer/src/pulse/PulseCItv.mli                 |  2 ++
 infer/src/pulse/PulseModels.ml                | 21 ++++++++++++++++---
 .../tests/codetoanalyze/c/pulse/memory_leak.c |  6 ++++--
 5 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index a56742eb4..ba298251f 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/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
diff --git a/infer/src/pulse/PulseCItv.ml b/infer/src/pulse/PulseCItv.ml
index d43568fba..fbd3dbb50 100644
--- a/infer/src/pulse/PulseCItv.ml
+++ b/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
diff --git a/infer/src/pulse/PulseCItv.mli b/infer/src/pulse/PulseCItv.mli
index 92fbbd863..a70ecd2d9 100644
--- a/infer/src/pulse/PulseCItv.mli
+++ b/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
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 2019fa076..a0a053022 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/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
diff --git a/infer/tests/codetoanalyze/c/pulse/memory_leak.c b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
index 5b430a8bf..a568be0d1 100644
--- a/infer/tests/codetoanalyze/c/pulse/memory_leak.c
+++ b/infer/tests/codetoanalyze/c/pulse/memory_leak.c
@@ -15,8 +15,10 @@ int* malloc_returned_ok() {
 
 void malloc_then_free_ok() {
   int* p = malloc(sizeof(p));
-  *p = 5;
-  free(p);
+  if (p) {
+    *p = 5;
+    free(p);
+  }
 }
 
 int* create_p() {