pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[racerd] reduce attributes to a singleton

Browse Source 
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
master
Nikos Gorogiannis 5 years ago committed by Facebook GitHub Bot
parent 7937615a20
commit e3da644776
3 changed files with 51 additions and 77 deletions
Show Stats Download Patch File Download Diff File

29
infer/src/concurrency/RacerD.ml
Unescape View File

@ -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

83
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -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
module AttributeMapDomain = struct
include AbstractDomain.SafeInvertedMap (AccessExpression) (Attribute)
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 []
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 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 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} =

20
infer/src/concurrency/RacerDDomain.mli
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save