[pulse] Add DynamicType attribute and use it in the model of ObjC alloc

Summary:
Adding a new attribute for dynamic type. It is set in the models of constructors, currently only in `alloc` in Objective-C. We use it in the following diff to figure out which `dealloc` method to call. However it could be useful for other things, such as dynamic dispatch.
#skipdeadcode

Reviewed By: jvillard

Differential Revision: D21739928

fbshipit-source-id: 9276c0a4d

infer/src/pulse/PulseAbductiveDomain.ml

@@ -203,6 +203,10 @@ module AddressAttributes = struct
     map_post_attrs astate ~f:(BaseAddressAttributes.allocate procname address location)
 
 
+  let add_dynamic_type typ address astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.add_dynamic_type typ address)
+
+
   let remove_allocation_attr address astate =
     map_post_attrs astate ~f:(BaseAddressAttributes.remove_allocation_attr address)
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -123,6 +123,8 @@ module AddressAttributes : sig
 
   val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
 
+  val add_dynamic_type : Typ.Name.t -> AbstractValue.t -> t -> t
+
   val remove_allocation_attr : AbstractValue.t -> t -> t
 
   val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option

infer/src/pulse/PulseAttribute.ml

@@ -29,6 +29,7 @@ module Attribute = struct
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
     | Allocated of Procname.t * Trace.t
     | Closure of Procname.t
+    | DynamicType of Typ.Name.t
     | Invalid of Invalidation.t * Trace.t
     | MustBeValid of Trace.t
     | StdVectorReserve
@@ -64,6 +65,8 @@ module Attribute = struct
 
   let allocated_rank = Variants.to_rank (Allocated (Procname.Linters_dummy_method, dummy_trace))
 
+  let dynamic_type_rank = Variants.to_rank (DynamicType (Typ.Name.Objc.from_string ""))
+
   let pp f attribute =
     let pp_string_if_debug string fmt =
       if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string
@@ -80,6 +83,8 @@ module Attribute = struct
           trace
     | Closure pname ->
         Procname.pp f pname
+    | DynamicType typ ->
+        F.fprintf f "DynamicType %a" Typ.Name.pp typ
     | Invalid (invalidation, trace) ->
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
@@ -146,6 +151,13 @@ module Attributes = struct
            (procname, trace) )
 
 
+  let get_dynamic_type attrs =
+    Set.find_rank attrs Attribute.dynamic_type_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.DynamicType typ) = attr in
+           typ )
+
+
   include Set
 end
 
@@ -158,6 +170,7 @@ let is_suitable_for_pre = function
   | AddressOfStackVariable _
   | Allocated _
   | Closure _
+  | DynamicType _
   | Invalid _
   | StdVectorReserve
   | WrittenTo _ ->
@@ -173,5 +186,9 @@ let map_trace ~f = function
       MustBeValid (f trace)
   | WrittenTo trace ->
       WrittenTo (f trace)
-  | (AddressOfCppTemporary _ | AddressOfStackVariable _ | Closure _ | StdVectorReserve) as attr ->
+  | ( AddressOfCppTemporary _
+    | AddressOfStackVariable _
+    | Closure _
+    | DynamicType _
+    | StdVectorReserve ) as attr ->
       attr

infer/src/pulse/PulseAttribute.mli

@@ -16,6 +16,7 @@ type t =
   | Allocated of Procname.t * Trace.t
       (** the {!Procname.t} is the function causing the allocation, eg [malloc] *)
   | Closure of Procname.t
+  | DynamicType of Typ.Name.t
   | Invalid of Invalidation.t * Trace.t
   | MustBeValid of Trace.t
   | StdVectorReserve
@@ -38,6 +39,8 @@ module Attributes : sig
 
   val get_allocation : t -> (Procname.t * Trace.t) option
 
+  val get_dynamic_type : t -> Typ.Name.t option
+
   val get_invalid : t -> (Invalidation.t * Trace.t) option
 
   val get_must_be_valid : t -> Trace.t option

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -70,6 +70,8 @@ let allocate procname (address, history) location memory =
   add_one address (Attribute.Allocated (procname, Immediate {location; history})) memory
 
 
+let add_dynamic_type typ address memory = add_one address (Attribute.DynamicType typ) 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

@@ -25,6 +25,8 @@ val add : AbstractValue.t -> Attributes.t -> t -> t
 
 val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
 
+val add_dynamic_type : Typ.Name.t -> AbstractValue.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

@@ -121,6 +121,24 @@ module ObjCCoreFoundation = struct
     PulseOperations.remove_allocation_attr (fst access) astate |> PulseOperations.ok_continue
 end
 
+module ObjC = struct
+  let alloc_not_null arg : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let dynamic_type =
+      match arg with
+      | Exp.Sizeof {typ= {desc= Tstruct name}} ->
+          name
+      | _ ->
+          Logging.die InternalError "Expected arg should be a sizeof expression"
+    in
+    let ret_addr = AbstractValue.mk_fresh () in
+    let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model "alloc"; location}]) in
+    let astate = PulseOperations.write_id ret_id ret_value astate in
+    PulseOperations.add_dynamic_type dynamic_type ret_addr astate
+    |> PulseArithmetic.and_positive ret_addr
+    |> PulseOperations.ok_continue
+end
+
 module Cplusplus = struct
   let delete deleted_access : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
@@ -861,7 +879,8 @@ module ProcNameDispatcher = struct
         ; -"CFAutorelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; -"CFBridgingRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; +match_builtin BuiltinDecl.__free_cf
-          <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release ] )
+          <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
+        ; +match_builtin BuiltinDecl.__objc_alloc_no_fail <>$ capt_exp $--> ObjC.alloc_not_null ] )
 end
 
 let dispatch tenv proc_name args = ProcNameDispatcher.dispatch tenv proc_name args

infer/src/pulse/PulseOperations.ml

@@ -221,6 +221,8 @@ let allocate procname location addr_trace astate =
   AddressAttributes.allocate procname addr_trace location astate
 
 
+let add_dynamic_type typ address astate = AddressAttributes.add_dynamic_type typ address astate
+
 let remove_allocation_attr address astate = AddressAttributes.remove_allocation_attr address astate
 
 let invalidate location cause addr_trace astate =

infer/src/pulse/PulseOperations.mli

@@ -90,6 +90,8 @@ val invalidate :
 
 val allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
+val add_dynamic_type : Typ.Name.t -> AbstractValue.t -> t -> t
+
 val remove_allocation_attr : AbstractValue.t -> t -> t
 
 val invalidate_access :