From 7108b348ff6ea4c9e0716cc84bc54b075de2cc82 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 3 May 2018 07:30:50 -0700 Subject: [PATCH] [racerd] significantly simplify deep ownership logic Summary: We had a semantics for ownership of prefix paths in mind (see comment), but it was enforced partially in the domain and partially in the transfer functions. Moving all of the logic into the domain makes things much cleaner/shorter. Reviewed By: ngorogiannis Differential Revision: D7845981 fbshipit-source-id: 4a2da95 --- infer/src/concurrency/RacerD.ml | 40 ++++++------------- infer/src/concurrency/RacerDDomain.ml | 55 ++++++++++++--------------- 2 files changed, 35 insertions(+), 60 deletions(-) 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