diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index fbf8eba37..2da7a5c36 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -33,28 +33,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Domain.AttributeMapDomain.add lhs_access_path rhs_attributes attribute_map - let propagate_ownership ((lhs_root, accesses) as lhs_access_path) rhs_exp ownership = + let propagate_ownership ((lhs_root, _) as lhs_access_path) rhs_exp ownership = if Var.is_global (fst lhs_root) then (* do not assign ownership to access paths rooted at globals *) ownership else - let ownership_value = - match accesses with - | [] -> - Domain.ownership_of_expr rhs_exp ownership - | [_] - when match Domain.OwnershipDomain.get_owned (lhs_root, []) ownership with - | Domain.OwnershipAbstractValue.OwnedIf _ -> - true - | _ -> - false -> - Domain.ownership_of_expr rhs_exp ownership - | _ when Domain.OwnershipDomain.is_owned lhs_access_path ownership -> - Domain.ownership_of_expr rhs_exp ownership - | _ -> - Domain.OwnershipAbstractValue.unowned - in - Domain.OwnershipDomain.add lhs_access_path ownership_value ownership + let rhs_ownership_value = Domain.ownership_of_expr rhs_exp ownership in + Domain.OwnershipDomain.add lhs_access_path rhs_ownership_value ownership let propagate_return return ret_ownership ret_attributes actuals @@ -327,19 +312,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else let base = fst actual_access_path in match OwnershipDomain.get_owned (base, []) caller_astate.ownership with + | Owned -> + (* the actual passed to the current callee is owned. drop all the conditional + accesses for that actual, since they're all safe *) + Conjunction actual_indexes | OwnedIf formal_indexes -> - (* the actual passed to the current callee is rooted in a formal *) + (* access path conditionally owned if [formal_indexes] are owned *) Conjunction (IntSet.union formal_indexes actual_indexes) - | Unowned | Owned -> - match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with - | OwnedIf formal_indexes -> - (* access path conditionally owned if [formal_indexes] are owned *) - Conjunction (IntSet.union formal_indexes actual_indexes) - | Owned -> - assert false - | Unowned -> - (* access path not rooted in a formal and not conditionally owned *) - False ) + | Unowned -> + (* access path not rooted in a formal and not conditionally owned *) + False ) | _ -> (* couldn't find access path, don't know if it's owned. assume not *) False diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index ead31bdd0..8a6bd3096 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -247,7 +247,7 @@ module ThreadsDomain = struct let is_any = function AnyThread -> true | _ -> false let integrate_summary ~caller_astate ~callee_astate = - (* if we know the callee runs on the main thread, assume the caller does too. otherwise, keep + (* if we know the callee runs on the main thread, assume the caller does too. otherwise, keep the caller's thread context *) match callee_astate with AnyThreadButSelf -> callee_astate | _ -> caller_astate end @@ -329,38 +329,31 @@ end module OwnershipDomain = struct include AbstractDomain.Map (AccessPath) (OwnershipAbstractValue) - (* Helper function used by both is_owned and get_owned. Not exported.*) - let get_owned_shallow access_path astate = - try find access_path astate with Caml.Not_found -> OwnershipAbstractValue.Unowned - - - (*deep ownership model where only a prefix needs to be owned in the astate*) - let is_owned (base, accesses) astate = - let is_owned_shallow access_path astate = - match get_owned_shallow access_path astate with - | OwnershipAbstractValue.Owned -> - true + (* return the first non-Unowned ownership value found when checking progressively shorter + prefixes of [access_path] *) + let rec get_owned access_path astate = + let keep_looking access_path astate = + match AccessPath.truncate access_path with + | access_path', Some _ -> + get_owned access_path' astate | _ -> - false - in - let rec helper = function - | prefix, _ when is_owned_shallow (base, prefix) astate -> - true - | _, [] -> - false - | prefix, hd :: tl -> - helper (List.append prefix [hd], tl) + OwnershipAbstractValue.Unowned in - helper ([], accesses) - - - (* -returns Owned if any prefix is owned on any prefix, else OwnedIf if it is -OwnedIf in the astate, else UnOwned -*) - let get_owned access_path astate = - if is_owned access_path astate then OwnershipAbstractValue.Owned - else try find access_path astate with Caml.Not_found -> OwnershipAbstractValue.Unowned + match find access_path astate with + | (OwnershipAbstractValue.Owned | OwnedIf _) as v -> + v + | OwnershipAbstractValue.Unowned -> + keep_looking access_path astate + | exception Caml.Not_found -> + keep_looking access_path astate + + + let is_owned access_path astate = + match get_owned access_path astate with + | OwnershipAbstractValue.Owned -> + true + | OwnershipAbstractValue.OwnedIf _ | Unowned -> + false let find = `Use_get_owned_instead