diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index f4d455a8d..4a22f0c25 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -269,7 +269,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with threads= ThreadsDomain.AnyThreadButSelf} | MainThreadIfTrue -> let attribute_map = - AttributeMapDomain.add_attribute ret_access_exp (Choice Choice.OnMainThread) + AttributeMapDomain.add_attribute ret_access_exp Attribute.OnMainThread astate.attribute_map in {astate with attribute_map} @@ -301,7 +301,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 (Choice Choice.LockHeld) + AttributeMapDomain.add_attribute ret_access_exp Attribute.LockHeld astate.attribute_map in {astate with attribute_map; threads= update_for_lock_use astate.threads} @@ -397,18 +397,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let do_assume formals assume_exp loc proc_data (astate : Domain.t) = let open Domain in - let add_choice bool_value (acc : Domain.t) = function - | Choice.LockHeld -> + 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 in {acc with locks} - | Choice.OnMainThread -> + | Attribute.OnMainThread -> let threads = if bool_value then ThreadsDomain.AnyThreadButSelf else ThreadsDomain.AnyThread in {acc with threads} + | Attribute.Functional -> + acc in let accesses = add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership @@ -422,7 +424,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let choices = AttributeMapDomain.get_choices access_expr astate.attribute_map in (* 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:(add_choice bool_value) ~init choices ) + List.fold ~f:(apply_choice bool_value) ~init choices ) | _ -> astate in diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 53eb0a2a5..7524544be 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -438,26 +438,18 @@ module OwnershipDomain = struct AccessSnapshot.OwnershipPrecondition.False end -module Choice = struct - type t = OnMainThread | LockHeld [@@deriving compare] +module Attribute = struct + type t = Functional | OnMainThread | LockHeld [@@deriving compare] let pp fmt = function + | Functional -> + F.pp_print_string fmt "Functional" | OnMainThread -> F.pp_print_string fmt "OnMainThread" | LockHeld -> F.pp_print_string fmt "LockHeld" end -module Attribute = struct - type t = Functional | Choice of Choice.t [@@deriving compare] - - let pp fmt = function - | Functional -> - F.pp_print_string fmt "Functional" - | Choice choice -> - Choice.pp fmt choice -end - module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute) module AttributeMapDomain = struct @@ -468,16 +460,17 @@ module AttributeMapDomain = struct let has_attribute access_expression attribute t = - try find access_expression t |> AttributeSetDomain.mem attribute with Caml.Not_found -> false + find_opt access_expression t |> Option.exists ~f:(AttributeSetDomain.mem attribute) let get_choices access_expression t = - try - let attributes = find access_expression t in - AttributeSetDomain.fold - (fun cc acc -> match cc with Attribute.Choice c -> c :: acc | _ -> acc) - attributes [] - with Caml.Not_found -> [] + 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 = @@ -492,8 +485,8 @@ module AttributeMapDomain = struct let rec attributes_of_expr attribute_map (e : HilExp.t) = match e with - | AccessExpression access_expr -> ( - try find access_expr attribute_map with Caml.Not_found -> AttributeSetDomain.empty ) + | AccessExpression access_expr -> + find_opt access_expr attribute_map |> Option.value ~default:AttributeSetDomain.empty | Constant _ -> AttributeSetDomain.singleton Attribute.Functional | Exception expr (* treat exceptions as transparent wrt attributes *) | Cast (_, expr) -> diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 5790aeac0..24ccb28b4 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -158,19 +158,11 @@ module OwnershipDomain : sig val get_precondition : AccessExpression.t -> t -> AccessSnapshot.OwnershipPrecondition.t end -(** attribute attached to a boolean variable specifying what it means when the boolean is true *) -module Choice : sig - type t = - | OnMainThread (** the current procedure is running on the main thread *) - | LockHeld (** a lock is currently held *) - - include PrettyPrintable.PrintableOrderedType with type t := t -end - module Attribute : sig type t = | Functional (** holds a value returned from a callee marked [@Functional] *) - | Choice of Choice.t (** holds a boolean choice variable *) + | 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 @@ -190,7 +182,7 @@ module AttributeMapDomain : sig val has_attribute : AccessExpression.t -> Attribute.t -> t -> bool - val get_choices : AccessExpression.t -> t -> Choice.t list + 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