From 410728d18f7d19b5f5850a0bbff82f88f3103040 Mon Sep 17 00:00:00 2001 From: Kyriakos Nikolaos Gkorogiannis Date: Fri, 14 Jul 2017 12:45:22 -0700 Subject: [PATCH] [thread-safety] Interprocedural escape analysis for formals/locals (essentially step (3) in Sam's list). Reviewed By: sblackshear Differential Revision: D5293383 fbshipit-source-id: 96c332d --- infer/src/checkers/ThreadSafety.ml | 74 +++++++++++++++++------ infer/src/checkers/ThreadSafetyDomain.ml | 60 +++++++++++++++--- infer/src/checkers/ThreadSafetyDomain.mli | 38 +++++++++--- 3 files changed, 135 insertions(+), 37 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 3f0eafe4a..8f20aeba4 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -451,7 +451,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> false - let make_container_write callee_pname receiver_ap callee_loc tenv = + let make_container_write callee_pname actuals receiver_ap callee_loc tenv = (* create a dummy write that represents mutating the contents of the container *) let open Domain in let callee_accesses = @@ -467,7 +467,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AccessDomain.add_access (Unprotected (Some 0)) (make_access dummy_access_ap Write callee_loc) AccessDomain.empty in - Some (true, false, false, callee_accesses, AttributeSetDomain.empty) + (* TODO: for now all formals escape *) + (* we need a more intelligent escape analysis, that branches on whether + we own the container *) + let escapee_formals = List.length actuals |> List.range 0 |> FormalsDomain.of_list in + Some (true, false, false, callee_accesses, AttributeSetDomain.empty, escapee_formals) let get_summary caller_pdesc callee_pname actuals callee_loc tenv = if is_container_write callee_pname tenv then @@ -479,7 +483,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> failwithf "Call to %a is marked as a container write, but has no receiver" Typ.Procname.pp callee_pname in - make_container_write callee_pname receiver_ap callee_loc tenv + make_container_write callee_pname actuals receiver_ap callee_loc tenv else Summary.read_summary caller_pdesc callee_pname (* return true if the given procname boxes a primitive type into a reference type *) @@ -502,6 +506,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ~f:(fun acc exp -> add_access exp loc Read acc locks threads attribute_map proc_data) exps ~init:accesses + let add_escapees_from_exp rhs_exp extras escapees = + HilExp.get_access_paths rhs_exp |> List.rev_map ~f:(Domain.Escapee.of_access_path extras) + |> Domain.EscapeeDomain.add_from_list escapees + + let add_escapees_from_exp_list exp_list extras escapees = + List.fold ~init:escapees exp_list ~f:(fun acc exp -> add_escapees_from_exp exp extras acc) + + let add_escapees_from_call actuals escapee_formals extras escapees = + let escapee_actuals = + Domain.FormalsDomain.elements escapee_formals |> List.rev_map ~f:(List.nth_exn actuals) + in + add_escapees_from_exp_list escapee_actuals extras escapees + let exec_instr (astate: Domain.astate) ({ProcData.extras; tenv; pdesc} as proc_data) _ (instr: HilInstr.t) = let open Domain in @@ -515,7 +532,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AttributeMapDomain.add_attribute (ret_base, []) Attribute.unconditionally_owned astate.attribute_map in - {astate with accesses; attribute_map} + (* TODO: we need to model escaping formals, now just assume all escape *) + let escapees = add_escapees_from_exp_list actuals extras astate.escapees in + {astate with accesses; attribute_map; escapees} | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc) -> ( let accesses = @@ -568,7 +587,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct , callee_threads , callee_locks , callee_accesses - , return_attributes ) + , return_attributes + , escapee_formals ) -> let update_caller_accesses pre callee_accesses caller_accesses = let combined_accesses = PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc) @@ -645,9 +665,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct propagate_return_attributes ret_opt return_attributes actuals astate.attribute_map extras in - {thumbs_up; locks; threads; accesses; attribute_map} + let escapees = + add_escapees_from_call actuals escapee_formals extras astate.escapees + in + {thumbs_up; locks; threads; accesses; attribute_map; escapees} | None - -> let should_assume_returns_ownership (call_flags: CallFlags.t) actuals = + -> (* TODO: assume actuals escape, should we? *) + let new_escapees = add_escapees_from_exp_list actuals extras astate.escapees in + let astate = {astate with escapees= new_escapees} in + let should_assume_returns_ownership (call_flags: CallFlags.t) actuals = (* assume non-interface methods with no summary and no parameters return ownership *) not call_flags.cf_interface && List.is_empty actuals @@ -721,7 +747,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map extras in - {astate with accesses; attribute_map} + (* assigning to the return variable leads to no new escapees *) + let escapees = + if fst lhs_access_path |> fst |> Var.is_return then astate.escapees + else add_escapees_from_exp rhs_exp extras astate.escapees + in + {astate with accesses; attribute_map; escapees} | Assume (assume_exp, _, _, loc) -> let rec eval_binop op var e1 e2 = match (eval_bexp var e1, eval_bexp var e2) with @@ -877,12 +908,14 @@ let empty_post = let initial_thumbs_up = true and initial_known_on_ui_thread = false and has_lock = false - and return_attrs = ThreadSafetyDomain.AttributeSetDomain.empty in + and return_attrs = ThreadSafetyDomain.AttributeSetDomain.empty + and escapee_formals = ThreadSafetyDomain.FormalsDomain.empty in ( initial_thumbs_up , initial_known_on_ui_thread , has_lock , ThreadSafetyDomain.AccessDomain.empty - , return_attrs ) + , return_attrs + , escapee_formals ) let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let is_initializer tenv proc_name = @@ -920,7 +953,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = else ({ThreadSafetyDomain.empty with threads}, IdAccessPathMapDomain.empty) in match Analyzer.compute_post proc_data ~initial ~debug:false with - | Some ({thumbs_up; threads; locks; accesses; attribute_map}, _) + | Some ({thumbs_up; threads; locks; accesses; attribute_map; escapees}, _) -> let return_var_ap = AccessPath.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc)) @@ -948,20 +981,21 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = | _ -> locks in - let post = (thumbs_up, threads, update_locks, accesses, return_attributes) in + let escapee_formals = FormalsDomain.of_escapees escapees in + let post = + (thumbs_up, threads, update_locks, accesses, return_attributes, escapee_formals) + in Summary.update_summary post summary | None -> summary ) else Summary.update_summary empty_post summary -(* we assume two access paths can alias if their access parts are equal (we ignore the base). *) -let can_alias access_path1 access_path2 = - List.compare AccessPath.compare_access (snd access_path1) (snd access_path2) - module AccessListMap = Caml.Map.Make (struct - type t = AccessPath.Raw.t [@@deriving compare] + type t = AccessPath.Raw.t - let compare = can_alias + (* TODO -- keep this compare to satisfy the order of tests, consider using Raw.compare *) + let compare access_path1 access_path2 = + List.compare AccessPath.compare_access (snd access_path1) (snd access_path2) end) let get_current_class_and_threadsafe_superclasses tenv pname = @@ -1032,7 +1066,7 @@ let trace_of_pname orig_sink orig_pdesc callee_pname = let open ThreadSafetyDomain in let orig_access = PathDomain.Sink.kind orig_sink in match Summary.read_summary orig_pdesc callee_pname with - | Some (_, _, _, access_map, _) + | Some (_, _, _, access_map, _, _) -> get_all_accesses (fun access -> Int.equal (Access.compare (PathDomain.Sink.kind access) orig_access) 0) access_map @@ -1397,7 +1431,7 @@ let should_filter_access (_, path) = now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells that x.f.g may point to during execution *) let make_results_table file_env = - let aggregate_post (_, threaded, _, accesses, _) tenv pdesc acc = + let aggregate_post (_, threaded, _, accesses, _, _) tenv pdesc acc = let open ThreadSafetyDomain in AccessDomain.fold (fun pre accesses acc -> diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 74219383f..2b566731e 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -178,12 +178,47 @@ module AccessDomain = struct with Not_found -> PathDomain.empty end +module Escapee = struct + type t = Formal of int | Local of Var.t [@@deriving compare] + + let pp fmt = function + | Formal fml + -> F.fprintf fmt "Formal(%d)" fml + | Local loc + -> F.fprintf fmt "Local(%a)" Var.pp loc + + let of_access_path extras (base, _) = + match FormalMap.get_formal_index base extras with + | Some fml + -> Formal fml + | None + -> Local (fst base) +end + +module EscapeeDomain = struct + include AbstractDomain.FiniteSet (Escapee) + + let add_from_list escapees escapee_list = + List.fold ~init:escapees escapee_list ~f:(fun acc v -> add v acc) +end + +module FormalsDomain = struct + include AbstractDomain.FiniteSet (Int) + + let of_escapees escapees = + let aux escapee acc = + match escapee with Escapee.Formal fml -> add fml acc | Escapee.Local _ -> acc + in + EscapeeDomain.fold aux escapees empty +end + type astate = { thumbs_up: ThumbsUpDomain.astate ; threads: ThreadsDomain.astate ; locks: LocksDomain.astate ; accesses: AccessDomain.astate - ; attribute_map: AttributeMapDomain.astate } + ; attribute_map: AttributeMapDomain.astate + ; escapees: EscapeeDomain.astate } type summary = ThumbsUpDomain.astate @@ -191,6 +226,7 @@ type summary = * LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate + * FormalsDomain.astate let empty = let thumbs_up = true in @@ -198,7 +234,8 @@ let empty = let locks = false in let accesses = AccessDomain.empty in let attribute_map = AccessPath.RawMap.empty in - {thumbs_up; threads; locks; accesses; attribute_map} + let escapees = EscapeeDomain.empty in + {thumbs_up; threads; locks; accesses; attribute_map; escapees} let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true @@ -206,6 +243,7 @@ let ( <= ) ~lhs ~rhs = && LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks && AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses && AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map + && EscapeeDomain.( <= ) ~lhs:lhs.escapees ~rhs:rhs.escapees let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 @@ -215,7 +253,8 @@ let join astate1 astate2 = let locks = LocksDomain.join astate1.locks astate2.locks in let accesses = AccessDomain.join astate1.accesses astate2.accesses in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in - {thumbs_up; threads; locks; accesses; attribute_map} + let escapees = EscapeeDomain.join astate1.escapees astate2.escapees in + {thumbs_up; threads; locks; accesses; attribute_map; escapees} let widen ~prev ~next ~num_iters = if phys_equal prev next then prev @@ -227,16 +266,17 @@ let widen ~prev ~next ~num_iters = let attribute_map = AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in - {thumbs_up; threads; locks; accesses; attribute_map} + let escapees = EscapeeDomain.widen ~prev:prev.escapees ~next:next.escapees ~num_iters in + {thumbs_up; threads; locks; accesses; attribute_map; escapees} -let pp_summary fmt (thumbs_up, threads, locks, accesses, return_attributes) = +let pp_summary fmt (thumbs_up, threads, locks, accesses, return_attributes, escapee_formals) = F.fprintf fmt - "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nReturn Attributes: %a@\n" + "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nReturn Attributes: %a @\nEscapee Formals: %a @\n" ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp - accesses AttributeSetDomain.pp return_attributes + accesses AttributeSetDomain.pp return_attributes FormalsDomain.pp escapee_formals -let pp fmt {thumbs_up; threads; locks; accesses; attribute_map} = +let pp fmt {thumbs_up; threads; locks; accesses; attribute_map; escapees} = F.fprintf fmt - "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nReturn Attributes: %a@\n" + "@\nThumbsUp: %a, Threads: %a, Locks: %a @\nAccesses %a @\nReturn Attributes: %a @\nEscapees: %a @\n" ThumbsUpDomain.pp thumbs_up ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp - accesses AttributeMapDomain.pp attribute_map + accesses AttributeMapDomain.pp attribute_map EscapeeDomain.pp escapees diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 14b21ff3b..4ae6b1148 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -118,13 +118,34 @@ end module AccessDomain : sig include module type of AbstractDomain.Map (AccessPrecondition) (PathDomain) - (* add the given (access, precondition) pair to the map *) - val add_access : AccessPrecondition.t -> TraceElem.t -> astate -> astate - - (* get all accesses with the given precondition *) + (** add the given (access, precondition) pair to the map *) val get_accesses : AccessPrecondition.t -> astate -> PathDomain.astate + (** get all accesses with the given precondition *) +end + +(** a formal or a local variable that may escape *) +module Escapee : sig + type t = Formal of int | Local of Var.t [@@deriving compare] + + val pp : F.formatter -> t -> unit + + val of_access_path : FormalMap.t -> AccessPath.Raw.t -> t +end + +(** set of formals or locals that may escape *) +module EscapeeDomain : sig + include module type of AbstractDomain.FiniteSet (Escapee) + + val add_from_list : astate -> Escapee.t list -> astate +end + +(** Domain that only includes escaping formals, for use in summary *) +module FormalsDomain : sig + include module type of AbstractDomain.FiniteSet (Int) + + val of_escapees : EscapeeDomain.astate -> astate end type astate = @@ -134,16 +155,19 @@ type astate = ; accesses: AccessDomain.astate (** read and writes accesses performed without ownership permissions *) ; attribute_map: AttributeMapDomain.astate - (** map of access paths to attributes such as owned, functional, ... *) } + (** map of access paths to attributes such as owned, functional, ... *) + ; escapees: EscapeeDomain.astate (** set of formals and locals that may escape *) } -(** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the - attributes associated with the return value *) +(** same as astate, but without [attribute_map] (since these involve locals) + and with the addition of the attributes associated with the return value + as well as the set of formals which may escape *) type summary = ThumbsUpDomain.astate * ThreadsDomain.astate * LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate + * FormalsDomain.astate include AbstractDomain.WithBottom with type astate := astate