From 5007eddbef03ad207aebd7481c78def059972f62 Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Wed, 3 Mar 2021 00:31:14 -0800 Subject: [PATCH] [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 | 22 ++++---- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseAttribute.ml | 6 +-- infer/src/pulse/PulseAttribute.mli | 4 +- .../src/pulse/PulseBaseAddressAttributes.mli | 4 +- infer/src/pulse/PulseModels.ml | 53 +++++++++++++------ infer/src/pulse/PulseOperations.mli | 4 +- 7 files changed, 58 insertions(+), 37 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index df84d785e..df04ed4aa 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -205,16 +205,18 @@ 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 cls_typ = Typ.mk (Typ.Tstruct name) in - match Var.get_ident var with - | Some id when Typ.is_objc_class cls_typ -> - let ret_id = Ident.create_fresh Ident.knormal in - let dealloc = Procname.make_objc_dealloc name in - let typ = Typ.mk_ptr cls_typ in - Some (ret_id, id, typ, dealloc) - | _ -> - None + 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 -> + let ret_id = Ident.create_fresh Ident.knormal in + let dealloc = Procname.make_objc_dealloc name in + let typ = Typ.mk_ptr cls_typ in + Some (ret_id, id, typ, dealloc) + | _ -> + None ) in List.filter_map ~f:get_dealloc dynamic_types_unreachable diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index a47ca0457..b66c9fb9f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 61e732b5f..77edc9c78 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/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) -> diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 3a07088af..614c64779 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/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 diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 71970805a..6cbe78562 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/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 diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index c6be6338e..6a5013aac 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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 = - 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 - |> ok_continue + let alloc_not_null_alloc_ev ~desc arg = + Misc.alloc_not_null + ~event:(fun location -> ValueHistory.Allocation {f= Model desc; location}) + arg 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 diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index b10a665e2..d6c16a079 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/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 *)