[pulse] Computing dynamic type information

Summary:
Adapting existing model for `new` used in ObjC to Java.
This allows to compute dynamic type information and will facilitate
handling `instanceof`, for instance.
Changing attribute value type from Typ.Name.t to Typ.t to handle arrays.

Reviewed By: da319

Differential Revision: D26687839

fbshipit-source-id: 2cfcd0625

infer/src/pulse/Pulse.ml

@@ -205,7 +205,9 @@ module PulseTransferFunctions = struct
      type needed to execute a call to dealloc for the given variables for which the dynamic type
      is an Objective-C class. *)
   let get_dealloc_from_dynamic_types dynamic_types_unreachable =
-    let get_dealloc (var, name) =
+    let get_dealloc (var, typ) =
+      Typ.name typ
+      |> Option.bind ~f:(fun name ->
              let cls_typ = Typ.mk (Typ.Tstruct name) in
              match Var.get_ident var with
              | Some id when Typ.is_objc_class cls_typ ->
@@ -214,7 +216,7 @@ module PulseTransferFunctions = struct
                  let typ = Typ.mk_ptr cls_typ in
                  Some (ret_id, id, typ, dealloc)
              | _ ->
-          None
+                 None )
     in
     List.filter_map ~f:get_dealloc dynamic_types_unreachable
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -153,7 +153,7 @@ 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 add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
 
   val remove_allocation_attr : AbstractValue.t -> t -> t
 

infer/src/pulse/PulseAttribute.ml

@@ -29,7 +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
+    | DynamicType of Typ.t
     | EndOfCollection
     | Invalid of Invalidation.t * Trace.t
     | ISLAbduced of Trace.t
@@ -69,7 +69,7 @@ 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 dynamic_type_rank = Variants.to_rank (DynamicType StdTyp.void)
 
   let end_of_collection_rank = Variants.to_rank EndOfCollection
 
@@ -112,7 +112,7 @@ module Attribute = struct
     | Closure pname ->
         Procname.pp f pname
     | DynamicType typ ->
-        F.fprintf f "DynamicType %a" Typ.Name.pp typ
+        F.fprintf f "DynamicType %a" (Typ.pp Pp.text) typ
     | EndOfCollection ->
         F.pp_print_string f "EndOfCollection"
     | Invalid (invalidation, trace) ->

infer/src/pulse/PulseAttribute.mli

@@ -16,7 +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
+  | DynamicType of Typ.t
   | EndOfCollection
   | Invalid of Invalidation.t * Trace.t
   | ISLAbduced of Trace.t  (** The allocation is abduced so as the analysis could run normally *)
@@ -45,7 +45,7 @@ module Attributes : sig
 
   val get_allocation : t -> (Procname.t * Trace.t) option
 
-  val get_dynamic_type : t -> Typ.Name.t option
+  val get_dynamic_type : t -> Typ.t option
 
   val is_end_of_collection : t -> bool
 

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -25,8 +25,6 @@ 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
@@ -45,6 +43,8 @@ val get_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> Trace.t option
 
 val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option
 
+val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
+
 val std_vector_reserve : AbstractValue.t -> t -> t
 
 val is_std_vector_reserved : AbstractValue.t -> t -> bool

infer/src/pulse/PulseModels.ml

@@ -134,6 +134,31 @@ module Misc = struct
     in
     let astate_zero = PulseArithmetic.prune_eq_zero (fst deleted_access) astate in
     Ok (ContinueProgram astate_zero) :: astates_alloc
+
+
+  let alloc_not_null ~event arg : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let ret_addr = AbstractValue.mk_fresh () in
+    let event = event location in
+    let ret_value = (ret_addr, [event]) in
+    let astate =
+      match arg with
+      | Exp.Sizeof {typ} ->
+          PulseOperations.add_dynamic_type typ ret_addr astate
+      | _ ->
+          (* The type expr is sometimes a Var expr in Java but this is not expected.
+             This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *)
+          astate
+    in
+    PulseOperations.write_id ret_id ret_value astate
+    |> PulseArithmetic.and_positive ret_addr
+    |> ok_continue
+
+
+  let alloc_not_null_call_ev ~desc arg =
+    alloc_not_null
+      ~event:(fun location -> ValueHistory.Call {f= Model desc; location; in_call= []})
+      arg
 end
 
 module C = struct
@@ -200,21 +225,10 @@ module ObjCCoreFoundation = struct
 end
 
 module ObjC = struct
-  let alloc_not_null arg : model =
+  let alloc_not_null_alloc_ev ~desc arg =
-   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    Misc.alloc_not_null
-    let dynamic_type =
+      ~event:(fun location -> ValueHistory.Allocation {f= Model desc; location})
-      match arg with
+      arg
-      | 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
-    |> ok_continue
 
 
   let dispatch_sync args : model =
@@ -1104,7 +1118,10 @@ module ProcNameDispatcher = struct
       @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
         ; +match_builtin BuiltinDecl.malloc <>$ capt_exp $--> C.malloc
         ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
-        ; +match_builtin BuiltinDecl.__new &--> Misc.return_positive ~desc:"new"
+        ; +match_builtin BuiltinDecl.__new <>$ capt_exp $--> Misc.alloc_not_null_call_ev ~desc:"new"
+        ; +match_builtin BuiltinDecl.__new_array
+          <>$ capt_exp
+          $--> Misc.alloc_not_null_call_ev ~desc:"new"
         ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
         ; +match_builtin BuiltinDecl.objc_cpp_throw <>--> Misc.early_exit
         ; +match_builtin BuiltinDecl.__cast <>$ capt_arg_payload $+...$--> Misc.id_first_arg
@@ -1398,7 +1415,9 @@ module ProcNameDispatcher = struct
         ; -"CFBridgingRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; +match_builtin BuiltinDecl.__objc_bridge_transfer
           <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
-        ; +match_builtin BuiltinDecl.__objc_alloc_no_fail <>$ capt_exp $--> ObjC.alloc_not_null
+        ; +match_builtin BuiltinDecl.__objc_alloc_no_fail
+          <>$ capt_exp
+          $--> ObjC.alloc_not_null_alloc_ev ~desc:"alloc"
         ; -"NSObject" &:: "init" <>$ capt_arg_payload $--> Misc.id_first_arg
         ; +match_regexp_opt Config.pulse_model_return_nonnull
           &::.*--> Misc.return_positive

infer/src/pulse/PulseOperations.mli

@@ -151,7 +151,7 @@ val invalidate_biad_isl :
 
 val allocate : Procname.t -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
-val add_dynamic_type : Typ.Name.t -> AbstractValue.t -> t -> t
+val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
 
 val remove_allocation_attr : AbstractValue.t -> t -> t
 
@@ -175,7 +175,7 @@ val shallow_copy :
   -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** returns the address of a new cell with the same edges as the original *)
 
-val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.Name.t) list
+val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.t) list
 (** Given a list of variables, computes the unreachable values if the variables were removed from
     the stack, then return the dynamic types of those values if they are available *)