From f638e741aea41e1773668350a14fe76dea6858c8 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Sat, 6 Jun 2020 02:48:38 -0700 Subject: [PATCH] [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 | 4 ++++ infer/src/pulse/PulseAbductiveDomain.mli | 2 ++ infer/src/pulse/PulseAttribute.ml | 19 ++++++++++++++++- infer/src/pulse/PulseAttribute.mli | 3 +++ infer/src/pulse/PulseBaseAddressAttributes.ml | 2 ++ .../src/pulse/PulseBaseAddressAttributes.mli | 2 ++ infer/src/pulse/PulseModels.ml | 21 ++++++++++++++++++- infer/src/pulse/PulseOperations.ml | 2 ++ infer/src/pulse/PulseOperations.mli | 2 ++ 9 files changed, 55 insertions(+), 2 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index e07fafa77..a246cd2d2 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index bc1396213..f1b35d21e 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 74706f401..ab52549d7 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/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 diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 319763dd8..817f60bc8 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/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 diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index becc06f9c..826d96ea4 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/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 diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index a8c21e657..2be1316de 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/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 diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 6ad572942..f010afff7 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 4a772850c..39e6af37b 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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 = diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index f9dded340..7a5c11a67 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/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 :