[pulse] Add model for malloc

Summary:
Adding a model for malloc: we add an attribute "Allocated". This can be used for implementing memory leaks: whenever the variables get out of scope, we can check that if the variable has an attribute Allocated, it also has an attribute Invalid CFree.

Possibly we will need more details in the Allocated attribute, to know if it's malloc, or other allocation function, but we can add that later when we know how it should look like.

Reviewed By: jvillard

Differential Revision: D20364541

fbshipit-source-id: 5e667a8c3

Makefile

@@ -55,6 +55,7 @@ DIRECT_TESTS += \
   c_errors \
   c_frontend \
   c_performance \
+  c_pulse \
   c_purity \
   c_uninit \
   cpp_annotation-reachability \

infer/src/pulse/PulseAbductiveDomain.ml

@@ -203,6 +203,10 @@ module AddressAttributes = struct
     map_post_attrs astate ~f:(BaseAddressAttributes.invalidate address invalidation location)
 
 
+  let allocate address location astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.allocate address location)
+
+
   let add_one address attributes astate =
     map_post_attrs astate ~f:(BaseAddressAttributes.add_one address attributes)
 
@@ -662,6 +666,7 @@ module PrePost = struct
       )
     | AddressOfCppTemporary _
     | AddressOfStackVariable _
+    | Allocated _
     | Closure _
     | Invalid _
     | MustBeValid _
@@ -681,6 +686,8 @@ module PrePost = struct
       | Arithmetic (arith, trace) ->
           Attribute.Arithmetic
             (arith, add_call_to_trace proc_name call_location caller_history trace)
+      | Allocated trace ->
+          Attribute.Allocated (add_call_to_trace proc_name call_location caller_history trace)
       | AddressOfCppTemporary _
       | AddressOfStackVariable _
       | BoItv _

infer/src/pulse/PulseAbductiveDomain.mli

@@ -76,6 +76,8 @@ module AddressAttributes : sig
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
+  val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
+
   val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
   val is_std_vector_reserved : AbstractValue.t -> t -> bool

infer/src/pulse/PulseAttribute.ml

@@ -28,6 +28,7 @@ module Attribute = struct
   type t =
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
+    | Allocated of Trace.t
     | Arithmetic of Arithmetic.t * Trace.t
     | BoItv of Itv.ItvPure.t
     | Closure of Procname.t
@@ -75,6 +76,8 @@ module Attribute = struct
         F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history
     | AddressOfStackVariable (var, location, history) ->
         F.fprintf f "s&%a (%a) at %a" Var.pp var ValueHistory.pp history Location.pp location
+    | Allocated trace ->
+        F.fprintf f "Allocated %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "allocation")) trace
     | BoItv bo_itv ->
         F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv
     | Closure pname ->
@@ -164,6 +167,7 @@ let is_suitable_for_pre = function
       true
   | AddressOfCppTemporary _
   | AddressOfStackVariable _
+  | Allocated _
   | Closure _
   | Invalid _
   | StdVectorReserve

infer/src/pulse/PulseAttribute.mli

@@ -14,6 +14,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AddressOfCppTemporary of Var.t * ValueHistory.t
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
+  | Allocated of Trace.t
   | Arithmetic of Arithmetic.t * Trace.t
   | BoItv of Itv.ItvPure.t
   | Closure of Procname.t

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -51,6 +51,10 @@ let invalidate (address, history) invalidation location memory =
   add_one address (Attribute.Invalid (invalidation, Immediate {location; history})) memory
 
 
+let allocate (address, history) location memory =
+  add_one address (Attribute.Allocated (Immediate {location; history})) memory
+
+
 let check_valid address attrs =
   L.d_printfln "Checking validity of %a" AbstractValue.pp address ;
   match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_invalid with

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -20,6 +20,8 @@ val add_one : AbstractValue.t -> Attribute.t -> t -> t
 
 val add : AbstractValue.t -> Attributes.t -> t -> t
 
+val allocate : AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
+
 val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a
 
 val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result

infer/src/pulse/PulseModels.ml

@@ -87,6 +87,12 @@ module C = struct
     else
       let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in
       [astate]
+
+
+  let malloc access : model =
+   fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
+    let astate = PulseOperations.allocate location access astate in
+    Ok [PulseOperations.write_id ret_id access astate]
 end
 
 module Cplusplus = struct
@@ -397,6 +403,7 @@ module ProcNameDispatcher = struct
     let pushback_modeled = StringSet.of_list ["add"; "put"; "addAll"; "putAll"; "remove"] in
     make_dispatcher
       [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
+      ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
       ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
       ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
       ; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit

infer/src/pulse/PulseOperations.ml

@@ -376,6 +376,8 @@ let havoc_field location addr_trace field trace_obj astate =
   write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate
 
 
+let allocate location addr_trace astate = AddressAttributes.allocate addr_trace location astate
+
 let invalidate location cause addr_trace astate =
   check_addr_access location addr_trace astate
   >>| AddressAttributes.invalidate addr_trace cause location

infer/src/pulse/PulseOperations.mli

@@ -82,6 +82,8 @@ val invalidate :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** record that the address is invalid *)
 
+val allocate : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t
+
 val invalidate_deref :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** record that what the address points to is invalid *)

infer/tests/codetoanalyze/c/pulse/Makefile

@@ -0,0 +1,15 @@
+# Copyright (c) Facebook, Inc. and its affiliates.
+#
+# This source code is licensed under the MIT license found in the
+# LICENSE file in the root directory of this source tree.
+
+TESTS_DIR = ../../..
+
+CLANG_OPTIONS = -c
+INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
+
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.c)
+
+include $(TESTS_DIR)/clang.make

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

@@ -0,0 +1,22 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+void malloc_no_free_bad() { // TODO implement the check
+  int* p = malloc(sizeof(p));
+}
+
+int* malloc_returned_ok() {
+  int* p = malloc(sizeof(p));
+  return p;
+}
+
+void malloc_then_free_ok() {
+  int* p = malloc(sizeof(p));
+  *p = 5;
+  free(p);
+}