From e3da644776abfbc48fc84bc98aeec49272eceb07 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Mon, 23 Mar 2020 03:11:06 -0700 Subject: [PATCH] [racerd] reduce attributes to a singleton Summary: The attribute types present are exclusive, so sets are not needed for the attribute map domain. This changes `Attribute` to a flat domain and removes the set on top of that. Reviewed By: jberdine Differential Revision: D20560240 fbshipit-source-id: 83e59d73e --- infer/src/concurrency/RacerD.ml | 29 ++++------ infer/src/concurrency/RacerDDomain.ml | 79 ++++++++++++-------------- infer/src/concurrency/RacerDDomain.mli | 20 ++----- 3 files changed, 51 insertions(+), 77 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 4a22f0c25..e409dd526 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -196,7 +196,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then (* TODO: check for constants, which are functional? *) let attribute_map = - AttributeMapDomain.add_attribute (AccessExpression.base ret_base) Functional + AttributeMapDomain.add (AccessExpression.base ret_base) Functional astate.attribute_map in {astate with attribute_map} @@ -269,8 +269,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with threads= ThreadsDomain.AnyThreadButSelf} | MainThreadIfTrue -> let attribute_map = - AttributeMapDomain.add_attribute ret_access_exp Attribute.OnMainThread - astate.attribute_map + AttributeMapDomain.add ret_access_exp Attribute.OnMainThread astate.attribute_map in {astate with attribute_map} | UnknownThread -> @@ -301,8 +300,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ; threads= update_for_lock_use astate.threads } | LockedIfTrue _ | GuardLockedIfTrue _ -> let attribute_map = - AttributeMapDomain.add_attribute ret_access_exp Attribute.LockHeld - astate.attribute_map + AttributeMapDomain.add ret_access_exp Attribute.LockHeld astate.attribute_map in {astate with attribute_map; threads= update_for_lock_use astate.threads} | GuardConstruct {acquire_now= false} -> @@ -318,7 +316,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {summary with accesses= rebased_accesses} ) in match rebased_summary_opt with - | Some {threads; locks; accesses; return_ownership; return_attributes} -> + | Some {threads; locks; accesses; return_ownership; return_attribute} -> let locks = LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks in @@ -330,7 +328,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate.ownership in let attribute_map = - AttributeMapDomain.add ret_access_exp return_attributes astate.attribute_map + AttributeMapDomain.add ret_access_exp return_attribute astate.attribute_map in let threads = ThreadsDomain.integrate_summary ~caller_astate:astate.threads @@ -342,7 +340,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let add_if_annotated predicate attribute attribute_map = if PatternMatch.override_exists predicate tenv callee_pname then - AttributeMapDomain.add_attribute ret_access_exp attribute attribute_map + AttributeMapDomain.add ret_access_exp attribute attribute_map else attribute_map in let attribute_map = add_if_annotated is_functional Functional astate_callee.attribute_map in @@ -409,7 +407,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct if bool_value then ThreadsDomain.AnyThreadButSelf else ThreadsDomain.AnyThread in {acc with threads} - | Attribute.Functional -> + | Attribute.(Functional | Nothing) -> acc in let accesses = @@ -420,11 +418,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match HilExp.get_access_exprs assume_exp with | [access_expr] -> HilExp.eval_boolean_exp access_expr assume_exp - |> Option.fold ~init:astate ~f:(fun init bool_value -> - let choices = AttributeMapDomain.get_choices access_expr astate.attribute_map in + |> Option.value_map ~default:astate ~f:(fun bool_value -> (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. add the constraint that the choice must be [bool_value] to the state *) - List.fold ~f:(apply_choice bool_value) ~init choices ) + AttributeMapDomain.find access_expr astate.attribute_map + |> apply_choice bool_value astate ) | _ -> astate in @@ -548,15 +546,12 @@ let analyze_procedure {Callbacks.exe_env; summary} = (Var.of_pvar (Pvar.get_ret_pvar proc_name), Procdesc.get_ret_type proc_desc) in let return_ownership = OwnershipDomain.get_owned return_var_exp ownership in - let return_attributes = - try AttributeMapDomain.find return_var_exp attribute_map - with Caml.Not_found -> AttributeSetDomain.empty - in + 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 in - let post = {threads; locks; accesses; return_ownership; return_attributes} in + let post = {threads; locks; accesses; return_ownership; return_attribute} in Payload.update_summary post summary | None -> summary diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 7524544be..0b58e04fe 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -439,71 +439,62 @@ module OwnershipDomain = struct end module Attribute = struct - type t = Functional | OnMainThread | LockHeld [@@deriving compare] + type t = Nothing | Functional | OnMainThread | LockHeld [@@deriving equal] - let pp fmt = function + let pp fmt t = + ( match t with + | Nothing -> + "Nothing" | Functional -> - F.pp_print_string fmt "Functional" + "Functional" | OnMainThread -> - F.pp_print_string fmt "OnMainThread" + "OnMainThread" | LockHeld -> - F.pp_print_string fmt "LockHeld" -end + "LockHeld" ) + |> F.pp_print_string fmt -module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute) -module AttributeMapDomain = struct - include AbstractDomain.InvertedMap (AccessExpression) (AttributeSetDomain) + let top = Nothing - let add access_expression attribute_set t = - if AttributeSetDomain.is_empty attribute_set then t else add access_expression attribute_set t + let is_top = function Nothing -> true | _ -> false + let join t t' = if equal t t' then t else Nothing - let has_attribute access_expression attribute t = - find_opt access_expression t |> Option.exists ~f:(AttributeSetDomain.mem attribute) + let leq ~lhs ~rhs = equal (join lhs rhs) rhs + let widen ~prev ~next ~num_iters:_ = join prev next +end - let get_choices access_expression t = - match find_opt access_expression t with - | None -> - [] - | Some attributes -> - AttributeSetDomain.fold - (fun cc acc -> match cc with OnMainThread | LockHeld -> cc :: acc | _ -> acc) - attributes [] +module AttributeMapDomain = struct + include AbstractDomain.SafeInvertedMap (AccessExpression) (Attribute) + let find acc_exp t = find_opt acc_exp t |> Option.value ~default:Attribute.top - let add_attribute access_expression attribute t = - update access_expression - (function - | Some attrs -> - Some (AttributeSetDomain.add attribute attrs) - | None -> - Some (AttributeSetDomain.singleton attribute) ) - t + let has_attribute access_expression attribute t = + find_opt access_expression t |> Option.exists ~f:(Attribute.equal attribute) - let rec attributes_of_expr attribute_map (e : HilExp.t) = + let rec attribute_of_expr attribute_map (e : HilExp.t) = match e with | AccessExpression access_expr -> - find_opt access_expr attribute_map |> Option.value ~default:AttributeSetDomain.empty + find access_expr attribute_map | Constant _ -> - AttributeSetDomain.singleton Attribute.Functional + Attribute.Functional | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr) -> - attributes_of_expr attribute_map expr + attribute_of_expr attribute_map expr | UnaryOperator (_, expr, _) -> - attributes_of_expr attribute_map expr + attribute_of_expr attribute_map expr | BinaryOperator (_, expr1, expr2) -> - let attributes1 = attributes_of_expr attribute_map expr1 in - let attributes2 = attributes_of_expr attribute_map expr2 in - AttributeSetDomain.join attributes1 attributes2 + let attribute1 = attribute_of_expr attribute_map expr1 in + let attribute2 = attribute_of_expr attribute_map expr2 in + Attribute.join attribute1 attribute2 | Closure _ | Sizeof _ -> - AttributeSetDomain.empty + Attribute.top let propagate_assignment lhs_access_expression rhs_exp attribute_map = - let rhs_attributes = attributes_of_expr attribute_map rhs_exp in - add lhs_access_expression rhs_attributes attribute_map + let rhs_attribute = attribute_of_expr attribute_map rhs_exp in + add lhs_access_expression rhs_attribute attribute_map end type t = @@ -566,21 +557,21 @@ type summary = ; locks: LocksDomain.t ; accesses: AccessDomain.t ; return_ownership: OwnershipAbstractValue.t - ; return_attributes: AttributeSetDomain.t } + ; return_attribute: Attribute.t } let empty_summary = { threads= ThreadsDomain.bottom ; locks= LocksDomain.empty ; accesses= AccessDomain.empty ; return_ownership= OwnershipAbstractValue.unowned - ; return_attributes= AttributeSetDomain.empty } + ; return_attribute= Attribute.top } -let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes} = +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 - return_ownership AttributeSetDomain.pp return_attributes + return_ownership Attribute.pp return_attribute let pp fmt {threads; locks; accesses; ownership; attribute_map} = diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 24ccb28b4..3164c51bf 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -160,33 +160,21 @@ end module Attribute : sig type t = + | Nothing | Functional (** holds a value returned from a callee marked [@Functional] *) | OnMainThread (** boolean is true if the current procedure is running on the main thread *) | LockHeld (** boolean is true if a lock is currently held *) - - include PrettyPrintable.PrintableOrderedType with type t := t -end - -module AttributeSetDomain : sig - type t - - val empty : t end module AttributeMapDomain : sig type t - val find : AccessExpression.t -> t -> AttributeSetDomain.t + val find : AccessExpression.t -> t -> Attribute.t - val add : AccessExpression.t -> AttributeSetDomain.t -> t -> t + val add : AccessExpression.t -> Attribute.t -> t -> t val has_attribute : AccessExpression.t -> Attribute.t -> t -> bool - val get_choices : AccessExpression.t -> t -> Attribute.t list - (** get the choice attributes associated with the given access path *) - - val add_attribute : AccessExpression.t -> Attribute.t -> t -> t - val propagate_assignment : AccessExpression.t -> HilExp.t -> t -> t (** propagate attributes from the leaves to the root of an RHS Hil expression *) end @@ -208,7 +196,7 @@ type summary = ; locks: LocksDomain.t ; accesses: AccessDomain.t ; return_ownership: OwnershipAbstractValue.t - ; return_attributes: AttributeSetDomain.t } + ; return_attribute: Attribute.t } val empty_summary : summary