[pulse] Model Core Graphics create and copy functions

Summary:
This models all the Create and Copy functions from CoreGraphics, examples in the tests.
These functions all allocate memory that needs to be manually released.

The modelling of the release functions will happen in a following diff. Until then, we have some false positives in the tests.

This check is currently in biabduction, and we aim to move it to Pulse.

Reviewed By: jvillard

Differential Revision: D20626395

fbshipit-source-id: b39eae2d9

infer/src/absint/PatternMatch.ml

@@ -472,3 +472,11 @@ let is_override_of_java_lang_object_equals curr_pname =
   in
   String.equal (Procname.get_method curr_pname) "equals"
   && is_only_param_of_object_type (Procname.get_parameters curr_pname)
+
+
+module ObjectiveC = struct
+  let is_core_graphics_create_or_copy _ procname =
+    String.is_prefix ~prefix:"CG" procname
+    && ( String.is_substring ~substring:"Create" procname
+       || String.is_substring ~substring:"Copy" procname )
+end

infer/src/absint/PatternMatch.mli

@@ -160,3 +160,7 @@ val has_same_signature : Procname.t -> (Procname.t -> bool) Staged.t
 val is_override_of_java_lang_object_equals : Procname.t -> bool
 (** Whether the method is an override of `java.lang.Object.equals(Object)` or
     `java.lang.Object.equals(Object)` itself *)
+
+module ObjectiveC : sig
+  val is_core_graphics_create_or_copy : Tenv.t -> string -> bool
+end

infer/src/pulse/PulseAbductiveDomain.ml

@@ -213,8 +213,8 @@ 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 allocate procname address location astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.allocate procname address location)
 
 
   let add_one address attributes astate =
@@ -696,8 +696,9 @@ module PrePost = struct
             (invalidation, add_call_to_trace proc_name call_location caller_history trace)
       | CItv (arith, trace) ->
           Attribute.CItv (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)
+      | Allocated (procname, trace) ->
+          Attribute.Allocated
+            (procname, add_call_to_trace proc_name call_location caller_history trace)
       | AddressOfCppTemporary _
       | AddressOfStackVariable _
       | BoItv _

infer/src/pulse/PulseAbductiveDomain.mli

@@ -77,7 +77,7 @@ 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 allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
 
   val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 

infer/src/pulse/PulseAttribute.ml

@@ -28,7 +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
+    | Allocated of Procname.t * Trace.t
     | CItv of CItv.t * Trace.t
     | BoItv of Itv.ItvPure.t
     | Closure of Procname.t
@@ -76,8 +76,11 @@ 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
+    | Allocated (procname, trace) ->
+        F.fprintf f "Allocated %a"
+          (Trace.pp
+             ~pp_immediate:(pp_string_if_debug ("allocation with " ^ Procname.to_string procname)))
+          trace
     | BoItv bo_itv ->
         F.fprintf f "BoItv (%a)" Itv.ItvPure.pp bo_itv
     | Closure pname ->

infer/src/pulse/PulseAttribute.mli

@@ -14,7 +14,8 @@ module ValueHistory = PulseValueHistory
 type t =
   | AddressOfCppTemporary of Var.t * ValueHistory.t
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
-  | Allocated of Trace.t
+  | Allocated of Procname.t * Trace.t
+      (** the {!Procname.t} is the function causing the allocation, eg [malloc] *)
   | CItv of CItv.t * Trace.t
   | BoItv of Itv.ItvPure.t
   | Closure of Procname.t

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -53,8 +53,8 @@ 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 allocate procname (address, history) location memory =
+  add_one address (Attribute.Allocated (procname, Immediate {location; history})) memory
 
 
 let check_valid address attrs =

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -22,7 +22,7 @@ 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 allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
 
 val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a
 

infer/src/pulse/PulseDiagnostic.ml

@@ -15,7 +15,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AccessToInvalidAddress of
       {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
-  | MemoryLeak of {allocation_trace: Trace.t; location: Location.t}
+  | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 let get_location = function
@@ -67,7 +67,7 @@ let get_message = function
       F.asprintf "%a%a" pp_access_trace access_trace
         (pp_invalidation_trace invalidation_line invalidation)
         invalidation_trace
-  | MemoryLeak {location; allocation_trace} ->
+  | MemoryLeak {procname; location; allocation_trace} ->
       let allocation_line =
         let {Location.line; _} = Trace.get_outer_location allocation_trace in
         line
@@ -75,7 +75,7 @@ let get_message = function
       let pp_allocation_trace fmt (trace : Trace.t) =
         match trace with
         | Immediate _ ->
-            F.fprintf fmt "by call to `malloc()`"
+            F.fprintf fmt "by call to `%a`" Procname.pp procname
         | ViaCall {f; _} ->
             F.fprintf fmt "by call to %a" CallEvent.describe f
       in

infer/src/pulse/PulseDiagnostic.mli

@@ -14,7 +14,7 @@ module ValueHistory = PulseValueHistory
 type t =
   | AccessToInvalidAddress of
       {invalidation: Invalidation.t; invalidation_trace: Trace.t; access_trace: Trace.t}
-  | MemoryLeak of {allocation_trace: Trace.t; location: Location.t}
+  | MemoryLeak of {procname: Procname.t; allocation_trace: Trace.t; location: Location.t}
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 val get_message : t -> string

infer/src/pulse/PulseModels.ml

@@ -89,8 +89,8 @@ module C = struct
 
 
   let malloc access : model =
-   fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
-    let astate = PulseOperations.allocate location access astate in
+   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]
 end
 
@@ -245,6 +245,17 @@ module StdAtomicInteger = struct
     [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate]
 end
 
+module ObjectiveC = struct
+  let alloc _ : model =
+   fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate ->
+    let hist =
+      [ValueHistory.Call {f= Model (Procname.to_string callee_procname); location; in_call= []}]
+    in
+    let ret_addr = AbstractValue.mk_fresh () in
+    let astate = PulseOperations.allocate callee_procname location (ret_addr, []) astate in
+    Ok [PulseOperations.write_id ret_id (ret_addr, hist) astate]
+end
+
 module JavaObject = struct
   (* naively modeled as shallow copy. *)
   let clone src_pointer_hist : model =
@@ -513,7 +524,8 @@ module ProcNameDispatcher = struct
       ; ( +PatternMatch.implements_enumeration
         &:: "nextElement" <>$ capt_arg_payload
         $!--> fun x -> StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), [])
-        ) ]
+        )
+      ; +PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> ObjectiveC.alloc ]
 end
 
 let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args

infer/src/pulse/PulseOperations.ml

@@ -374,7 +374,9 @@ 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 allocate procname location addr_trace astate =
+  AddressAttributes.allocate procname addr_trace location astate
+
 
 let invalidate location cause addr_trace astate =
   check_addr_access location addr_trace astate
@@ -474,17 +476,17 @@ let check_memory_leak_unreachable unreachable_attrs location =
       Attributes.fold attributes ~init:(None (* allocation trace *), false (* freed *))
         ~f:(fun acc attr ->
           match (attr : Attribute.t) with
-          | Allocated trace ->
-              (Some trace, snd acc)
+          | Allocated (procname, trace) ->
+              (Some (procname, trace), snd acc)
           | Invalid (CFree, _) ->
               (fst acc, true)
           | _ ->
               acc )
     in
     match allocated_not_freed_opt with
-    | Some trace, false ->
+    | Some (procname, trace), false ->
         (* allocated but not freed *)
-        Error (Diagnostic.MemoryLeak {location; allocation_trace= trace})
+        Error (Diagnostic.MemoryLeak {procname; location; allocation_trace= trace})
     | _ ->
         result
   in

infer/src/pulse/PulseOperations.mli

@@ -82,7 +82,7 @@ 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 allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
 val invalidate_deref :
   Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result

infer/tests/codetoanalyze/objc/pulse/MemoryLeaks.m

@@ -0,0 +1,49 @@
+/*
+ * 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.
+ */
+
+#import <UIKit/UIKit.h>
+
+@interface MemoryLeaks
+
+@property(strong) UIView* backgroundCoveringView;
+@property(strong) UIView* attachmentContainerView;
+
+@end
+
+@implementation MemoryLeaks
+
+- (void)cg_path_create_with_rect_no_leak_good_FP {
+  UIView* attachmentContainerView = [UIView alloc];
+  CGPathRef shadowPath =
+      CGPathCreateWithRect(attachmentContainerView.bounds, NULL);
+  CGPathRelease(shadowPath);
+}
+
+- (void)cg_path_create_with_rect_leak_bad {
+  CGPathRef shadowPath =
+      CGPathCreateWithRect(self.backgroundCoveringView.bounds, NULL);
+  self.backgroundCoveringView.layer.shadowPath = shadowPath;
+}
+
++ (void)cg_path_create_mutable_leak_bad:(CGRect)rect {
+  0.20f * CGRectGetHeight(rect);
+  CGPathCreateMutable();
+}
+
++ (void)cg_path_create_mutable_no_leak_good_FP:(CGRect)rect {
+  CGFloat lineThickness = 0.20f * CGRectGetHeight(rect);
+  // One rectangle
+  CGMutablePathRef path1 = CGPathCreateMutable();
+  CFRelease(path1);
+}
+
++ (void)cg_bitmap_context_create_image_no_leak_good_FP {
+  CGImageRef newImage = CGBitmapContextCreateImage(nil);
+  CGImageRelease(newImage);
+}
+
+@end

infer/tests/codetoanalyze/objc/pulse/issues.exp

@@ -1,2 +1,7 @@
+codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_bitmap_context_create_image_no_leak_good_FP, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here]
+codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_mutable_leak_bad:, 2, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here]
+codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_mutable_no_leak_good_FP:, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here]
+codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_leak_bad, 3, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here]
+codetoanalyze/objc/pulse/MemoryLeaks.m, MemoryLeaks::cg_path_create_with_rect_no_leak_good_FP, 4, PULSE_MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocation occurs here,memory becomes unreachable here]
 codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,invalid access occurs here]
 codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]