From f7d6961177079e3a8911d148cf2b95da509cceff Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 27 Mar 2020 06:45:38 -0700 Subject: [PATCH] [racerd][3/n] improve domain interface and consolidate access validity checking Summary: For historical reasons, the record of an access is a three-level record: 1. `AccessSnapshot`, a record with info such as ownership and lock status, including 2. `TraceElem`, a record with a trace and an element which is 3. Access, the abstract addressed accessed and the type of access. This stack flips the order to 2, 1, 3, leading up to the possibility of merging 1 and 3. This diff improves the domain interface and consolidates all the various validity invariant checking for accesses inside their constructors. Reviewed By: skcho Differential Revision: D20668611 fbshipit-source-id: 45806d40d --- infer/src/concurrency/RacerD.ml | 56 ++++++------------ infer/src/concurrency/RacerDDomain.ml | 82 +++++++++++--------------- infer/src/concurrency/RacerDDomain.mli | 25 ++++---- 3 files changed, 64 insertions(+), 99 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 35ef4f1ef..747874d6e 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -163,16 +163,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in if is_box callee_pname then match actuals with - | HilExp.AccessExpression actual_access_expr :: _ -> - if AttributeMapDomain.has_attribute actual_access_expr Functional astate.attribute_map - then - (* TODO: check for constants, which are functional? *) - let attribute_map = - AttributeMapDomain.add (AccessExpression.base ret_base) Functional - astate.attribute_map - in - {astate with attribute_map} - else astate + | HilExp.AccessExpression actual_access_expr :: _ + when AttributeMapDomain.is_functional astate.attribute_map actual_access_expr -> + (* TODO: check for constants, which are functional? *) + let attribute_map = + AttributeMapDomain.add (AccessExpression.base ret_base) Functional astate.attribute_map + in + {astate with attribute_map} | _ -> astate else if should_assume_returns_ownership callee_pname call_flags actuals then @@ -264,11 +261,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match get_lock_effect callee_pname actuals with | Lock _ | GuardLock _ | GuardConstruct {acquire_now= true} -> { astate with - locks= LocksDomain.acquire_lock astate.locks + locks= LockDomain.acquire_lock astate.locks ; threads= update_for_lock_use astate.threads } | Unlock _ | GuardDestroy _ | GuardUnlock _ -> { astate with - locks= LocksDomain.release_lock astate.locks + locks= LockDomain.release_lock astate.locks ; threads= update_for_lock_use astate.threads } | LockedIfTrue _ | GuardLockedIfTrue _ -> let attribute_map = @@ -290,7 +287,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match rebased_summary_opt with | Some {threads; locks; accesses; return_ownership; return_attribute} -> let locks = - LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks + LockDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks in let accesses = add_callee_accesses extras astate accesses locks threads actuals callee_pname loc @@ -337,8 +334,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in let is_functional = (not (List.is_empty rhs_access_exprs)) - && List.for_all rhs_access_exprs ~f:(fun access_exp -> - AttributeMapDomain.has_attribute access_exp Functional astate.attribute_map ) + && List.for_all rhs_access_exprs ~f:(AttributeMapDomain.is_functional astate.attribute_map) && match AccessExpression.get_typ lhs_access_exp tenv with | Some {Typ.desc= Typ.Tint ILong | Tfloat FDouble} -> @@ -370,8 +366,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let apply_choice bool_value (acc : Domain.t) = function | Attribute.LockHeld -> let locks = - if bool_value then LocksDomain.acquire_lock acc.locks - else LocksDomain.release_lock acc.locks + if bool_value then LockDomain.acquire_lock acc.locks + else LockDomain.release_lock acc.locks in {acc with locks} | Attribute.OnMainThread -> @@ -444,8 +440,8 @@ let analyze_procedure {Callbacks.exe_env; summary} = let proc_data = ProcData.make summary tenv (FormalMap.make proc_desc) in let initial = let locks = - if Procdesc.is_java_synchronized proc_desc then LocksDomain.(acquire_lock bottom) - else LocksDomain.bottom + if Procdesc.is_java_synchronized proc_desc then LockDomain.(acquire_lock bottom) + else LockDomain.bottom in let threads = if @@ -521,7 +517,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = let return_attribute = AttributeMapDomain.find return_var_exp attribute_map in let locks = (* if method is [synchronized] released the lock once. *) - if Procdesc.is_java_synchronized proc_desc then LocksDomain.release_lock locks else locks + if Procdesc.is_java_synchronized proc_desc then LockDomain.release_lock locks else locks in let post = {threads; locks; accesses; return_ownership; return_attribute} in Payload.update_summary post summary @@ -746,20 +742,6 @@ let empty_reported = {reported_sites; reported_reads; reported_writes; reported_unannotated_calls} -(* decide if we should throw away an access before doing safety analysis - for now, just check for whether the access is within a switch-map - that is auto-generated by Java. *) -let should_filter_access exp_opt = - let check_access = function - | HilExp.Access.FieldAccess fld -> - String.is_substring ~substring:"$SwitchMap" (Fieldname.to_string fld) - | _ -> - false - in - Option.exists exp_opt ~f:(fun exp -> - AccessExpression.to_accesses exp |> snd |> List.exists ~f:check_access ) - - (** Map containing reported accesses, which groups them in lists, by abstract location. The equivalence relation used for grouping them is equality of access paths. This is slightly complicated because local variables contain the pname of the function declaring them. Here we @@ -806,10 +788,8 @@ end = struct let add (rep : reported_access) map = let access = rep.snapshot.elem.access in - if RacerDDomain.Access.get_access_exp access |> should_filter_access then map - else - let k = Key.of_access access in - M.update k (function None -> Some [rep] | Some reps -> Some (rep :: reps)) map + let k = Key.of_access access in + M.update k (function None -> Some [rep] | Some reps -> Some (rep :: reps)) map let fold f map a = diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 0863f44d3..6b4672301 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -10,17 +10,6 @@ module AccessExpression = HilExp.AccessExpression module F = Format module MF = MarkupFormatter -(** Master function for deciding whether RacerD should completely ignore a variable as the root of - an access expression. Currently fires on *static locals* and any variable which does not appear - in source code (eg, temporary variables and frontend introduced variables). This is because - currently reports on these variables would not be easily actionable. - - This is here and not in RacerDModels to avoid dependency cycles. *) -let should_skip_var v = - (not (Var.appears_in_source_code v)) - || match v with Var.ProgramVar pvar -> Pvar.is_static_local pvar | _ -> false - - let pp_exp fmt exp = match !Language.curr_language with | Clang -> @@ -68,16 +57,21 @@ module Access = struct let should_keep formals access = - match get_access_exp access with - | None -> - true - | Some acc_exp -> ( - let ((root, _) as base) = AccessExpression.get_base acc_exp in - match root with - | Var.LogicalVar _ -> - false - | Var.ProgramVar pvar -> - Pvar.is_global pvar || FormalMap.is_formal base formals ) + let rec check_access (exp : AccessExpression.t) = + match exp with + | FieldOffset (prefix, fld) -> + (not (String.is_substring ~substring:"$SwitchMap" (Fieldname.get_field_name fld))) + && check_access prefix + | ArrayOffset (prefix, _, _) | AddressOf prefix | Dereference prefix -> + check_access prefix + | Base (LogicalVar _, _) -> + false + | Base (((ProgramVar pvar as var), _) as base) -> + Var.appears_in_source_code var + && (not (Pvar.is_static_local pvar)) + && (Pvar.is_global pvar || FormalMap.is_formal base formals) + in + match get_access_exp access with None -> true | Some acc_exp -> check_access acc_exp let map ~f access = @@ -132,7 +126,7 @@ module CallPrinter = struct let pp fmt cs = F.fprintf fmt "call to %a" Procname.pp (CallSite.pname cs) end -module LocksDomain = struct +module LockDomain = struct include AbstractDomain.CountDomain (struct (** arbitrary threshold for max locks we expect to be held simultaneously *) let max = 5 @@ -216,7 +210,7 @@ module OwnershipAbstractValue = struct let owned = OwnedIf IntSet.empty - let is_owned = function OwnedIf set -> IntSet.is_empty set | _ -> false + let is_owned = function OwnedIf set -> IntSet.is_empty set | Unowned -> false let unowned = Unowned @@ -293,20 +287,20 @@ module AccessSnapshot = struct let make_unannotated_call_access formals pname lock ownership loc = - let lock = LocksDomain.is_locked lock in + let lock = LockDomain.is_locked lock in let access = Access.make_unannotated_call_access pname in make_if_not_owned formals access lock ownership loc let make_access formals acc_exp ~is_write loc lock thread ownership_precondition = - let lock = LocksDomain.is_locked lock in + let lock = LockDomain.is_locked lock in let access = Access.make_field_access acc_exp ~is_write in make_if_not_owned formals access lock thread ownership_precondition loc let make_container_access formals acc_exp ~is_write callee loc lock thread ownership_precondition = - let lock = LocksDomain.is_locked lock in + let lock = LockDomain.is_locked lock in let access = Access.make_container_access acc_exp callee ~is_write in make_if_not_owned formals access lock thread ownership_precondition loc @@ -319,7 +313,7 @@ module AccessSnapshot = struct let thread = ThreadsDomain.integrate_summary ~callee_astate:snapshot.elem.thread ~caller_astate:threads in - let lock = snapshot.elem.lock || LocksDomain.is_locked locks in + let lock = snapshot.elem.lock || LockDomain.is_locked locks in with_callsite snapshot callsite |> map ~f:(fun elem -> {elem with lock; thread; ownership_precondition}) |> filter formals @@ -334,14 +328,6 @@ end module AccessDomain = struct include AbstractDomain.FiniteSet (AccessSnapshot) - let add ({AccessSnapshot.elem= {access}} as s) astate = - let skip = - Access.get_access_exp access - |> Option.exists ~f:(fun exp -> AccessExpression.get_base exp |> fst |> should_skip_var) - in - if skip then astate else add s astate - - let add_opt snapshot_opt astate = Option.fold snapshot_opt ~init:astate ~f:(fun acc s -> add s acc) end @@ -435,8 +421,8 @@ module AttributeMapDomain = struct let find acc_exp t = find_opt acc_exp t |> Option.value ~default:Attribute.top - let has_attribute access_expression attribute t = - find_opt access_expression t |> Option.exists ~f:(Attribute.equal attribute) + let is_functional t access_expression = + match find_opt access_expression t with Some Functional -> true | _ -> false let rec attribute_of_expr attribute_map (e : HilExp.t) = @@ -464,14 +450,14 @@ end type t = { threads: ThreadsDomain.t - ; locks: LocksDomain.t + ; locks: LockDomain.t ; accesses: AccessDomain.t ; ownership: OwnershipDomain.t ; attribute_map: AttributeMapDomain.t } let bottom = let threads = ThreadsDomain.bottom in - let locks = LocksDomain.bottom in + let locks = LockDomain.bottom in let accesses = AccessDomain.empty in let ownership = OwnershipDomain.empty in let attribute_map = AttributeMapDomain.empty in @@ -479,7 +465,7 @@ let bottom = let is_bottom {threads; locks; accesses; ownership; attribute_map} = - ThreadsDomain.is_bottom threads && LocksDomain.is_bottom locks && AccessDomain.is_empty accesses + ThreadsDomain.is_bottom threads && LockDomain.is_bottom locks && AccessDomain.is_empty accesses && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map @@ -488,7 +474,7 @@ let leq ~lhs ~rhs = if phys_equal lhs rhs then true else ThreadsDomain.leq ~lhs:lhs.threads ~rhs:rhs.threads - && LocksDomain.leq ~lhs:lhs.locks ~rhs:rhs.locks + && LockDomain.leq ~lhs:lhs.locks ~rhs:rhs.locks && AccessDomain.leq ~lhs:lhs.accesses ~rhs:rhs.accesses && AttributeMapDomain.leq ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map @@ -497,7 +483,7 @@ let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else let threads = ThreadsDomain.join astate1.threads astate2.threads in - let locks = LocksDomain.join astate1.locks astate2.locks in + let locks = LockDomain.join astate1.locks astate2.locks in let accesses = AccessDomain.join astate1.accesses astate2.accesses in let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in @@ -508,7 +494,7 @@ let widen ~prev ~next ~num_iters = if phys_equal prev next then prev else let threads = ThreadsDomain.widen ~prev:prev.threads ~next:next.threads ~num_iters in - let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in + let locks = LockDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in let ownership = OwnershipDomain.widen ~prev:prev.ownership ~next:next.ownership ~num_iters in let attribute_map = @@ -519,15 +505,15 @@ let widen ~prev ~next ~num_iters = type summary = { threads: ThreadsDomain.t - ; locks: LocksDomain.t + ; locks: LockDomain.t ; accesses: AccessDomain.t ; return_ownership: OwnershipAbstractValue.t ; return_attribute: Attribute.t } let empty_summary = { threads= ThreadsDomain.bottom - ; locks= LocksDomain.bottom - ; accesses= AccessDomain.empty + ; locks= LockDomain.bottom + ; accesses= AccessDomain.bottom ; return_ownership= OwnershipAbstractValue.unowned ; return_attribute= Attribute.top } @@ -535,13 +521,13 @@ let empty_summary = let pp_summary fmt {threads; locks; accesses; return_ownership; return_attribute} = F.fprintf fmt "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n" - ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipAbstractValue.pp + ThreadsDomain.pp threads LockDomain.pp locks AccessDomain.pp accesses OwnershipAbstractValue.pp return_ownership Attribute.pp return_attribute let pp fmt {threads; locks; accesses; ownership; attribute_map} = F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nAttributes: %a @\n" - ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp + ThreadsDomain.pp threads LockDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp ownership AttributeMapDomain.pp attribute_map diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 19b84b81c..dcd19b3e1 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -21,18 +21,15 @@ module Access : sig (** Write to container object *) | InterfaceCall of Procname.t (** Call to method of interface not annotated with [@ThreadSafe] *) - [@@deriving compare] - include ExplicitTrace.Element with type t := t + val pp : F.formatter -> t -> unit val get_access_exp : t -> AccessExpression.t option end -(** Overapproximation of number of locks that are currently held *) -module LocksDomain : sig - type t - - val bottom : t +(** Overapproximation of number of time the lock has been acquired *) +module LockDomain : sig + include AbstractDomain.WithBottom val acquire_lock : t -> t (** record acquisition of a lock *) @@ -77,6 +74,8 @@ module OwnershipAbstractValue : sig val owned : t + val unowned : t + val make_owned_if : int -> t val join : t -> t -> t @@ -107,7 +106,7 @@ module AccessSnapshot : sig -> AccessExpression.t -> is_write:bool -> Location.t - -> LocksDomain.t + -> LockDomain.t -> ThreadsDomain.t -> OwnershipAbstractValue.t -> t option @@ -118,7 +117,7 @@ module AccessSnapshot : sig -> is_write:bool -> Procname.t -> Location.t - -> LocksDomain.t + -> LockDomain.t -> ThreadsDomain.t -> OwnershipAbstractValue.t -> t option @@ -134,7 +133,7 @@ module AccessSnapshot : sig -> CallSite.t -> OwnershipAbstractValue.t -> ThreadsDomain.t - -> LocksDomain.t + -> LockDomain.t -> t option end @@ -175,7 +174,7 @@ module AttributeMapDomain : sig val add : AccessExpression.t -> Attribute.t -> t -> t - val has_attribute : AccessExpression.t -> Attribute.t -> t -> bool + val is_functional : t -> AccessExpression.t -> bool val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t (** propagate attributes from the leaves to the root of an RHS Hil expression *) @@ -183,7 +182,7 @@ end type t = { threads: ThreadsDomain.t (** current thread: main, background, or unknown *) - ; locks: LocksDomain.t (** boolean that is true if a lock must currently be held *) + ; locks: LockDomain.t (** boolean that is true if a lock must currently be held *) ; accesses: AccessDomain.t (** read and writes accesses performed without ownership permissions *) ; ownership: OwnershipDomain.t (** map of access paths to ownership predicates *) @@ -199,7 +198,7 @@ val add_unannotated_call_access : FormalMap.t -> Procname.t -> Location.t -> t - may escape *) type summary = { threads: ThreadsDomain.t - ; locks: LocksDomain.t + ; locks: LockDomain.t ; accesses: AccessDomain.t ; return_ownership: OwnershipAbstractValue.t ; return_attribute: Attribute.t }