From 851a4da7e0ebd5ded286adb524b92e75c4c0ef06 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 23 Jan 2017 20:30:13 -0800 Subject: [PATCH] [thread-safety][cleanup] add mli for ThreadSafetyDomain Reviewed By: peterogithub Differential Revision: D4452608 fbshipit-source-id: 1761045 --- infer/src/checkers/ThreadSafetyDomain.ml | 33 +--------- infer/src/checkers/ThreadSafetyDomain.mli | 79 +++++++++++++++++++++++ 2 files changed, 82 insertions(+), 30 deletions(-) create mode 100644 infer/src/checkers/ThreadSafetyDomain.mli diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index ccb0bb879..df0d74940 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -18,7 +18,9 @@ module RawAccessPath = struct let pp_element = pp end -module OwnershipDomain = AbstractDomain.InvertedSet(PrettyPrintable.MakePPSet(RawAccessPath)) +module RawAccessPathSet = PrettyPrintable.MakePPSet(RawAccessPath) + +module OwnershipDomain = AbstractDomain.InvertedSet(RawAccessPathSet) module TraceElem = struct module Kind = RawAccessPath @@ -50,11 +52,6 @@ let make_access kind loc = let site = CallSite.make Procname.empty_block loc in TraceElem.make kind site -(** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes - the existence of one global lock. In the case that a lock is held on the access to a variable, - but the lock held is the wrong one, we will erroneously say that the access is thread-safe. - However, this coarse abstraction saves us from the complexity of tracking which locks are held - and which memory locations correspond to the same lock. *) module LocksDomain = AbstractDomain.BooleanAnd module PathDomain = SinkTrace.Make(TraceElem) @@ -70,37 +67,13 @@ module ConditionalWritesDomain = AbstractDomain.Map (IntMap) (PathDomain) type astate = { locks : LocksDomain.astate; - (** boolean that is true if a lock must currently be held *) reads : PathDomain.astate; - (** access paths read outside of synchronization *) conditional_writes : ConditionalWritesDomain.astate; - (** map of (formal index) -> set of access paths rooted in the formal index that are read - outside of synrchonization if the formal is not owned by the caller *) unconditional_writes : PathDomain.astate; - (** access paths written outside of synchronization *) id_map : IdAccessPathMapDomain.astate; - (** map used to decompile temporary variables into access paths *) owned : OwnershipDomain.astate; - (** access paths that must be owned by the current function *) } -(** the primary role of this domain is tracking *conditional* and *unconditional* writes. - conditional writes are writes that are rooted in a formal of the current procedure, and they - are safe only if the actual bound to that formal is owned at the call site (as in the foo - example below). Unconditional writes are rooted in a local, and they are only safe if a lock is - held in the caller. - To demonstrate what conditional writes buy us, consider the following example: - - foo() { - Object local = new Object(); - iWriteToAField(local); - } - - We don't want to warn on this example because the object pointed to by local is owned by the - caller foo, then ownership is transferred to the callee iWriteToAField. -*) - -(** same as astate, but without [id_map]/[owned] (since they are local) *) type summary = LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate *PathDomain.astate diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli new file mode 100644 index 000000000..112dbf259 --- /dev/null +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -0,0 +1,79 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd + +module F = Format + +module RawAccessPath : sig + type t = AccessPath.raw + val compare : t -> t -> int + val pp : Format.formatter -> t -> unit + val pp_element : Format.formatter -> t -> unit +end + +module RawAccessPathSet : PrettyPrintable.PPSet with type elt = RawAccessPath.t + +module OwnershipDomain : module type of AbstractDomain.InvertedSet (RawAccessPathSet) + +module TraceElem : TraceElem.S with module Kind = RawAccessPath + +(** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes + the existence of one global lock. In the case that a lock is held on the access to a variable, + but the lock held is the wrong one, we will erroneously say that the access is thread-safe. + However, this coarse abstraction saves us from the complexity of tracking which locks are held + and which memory locations correspond to the same lock. *) +module LocksDomain : AbstractDomain.S with type astate = bool + +module PathDomain : module type of SinkTrace.Make(TraceElem) + +module IntMap : PrettyPrintable.PPMap with type key = int + +module ConditionalWritesDomain : module type of (AbstractDomain.Map (IntMap) (PathDomain)) + +(** the primary role of this domain is tracking *conditional* and *unconditional* writes. + conditional writes are writes that are rooted in a formal of the current procedure, and they + are safe only if the actual bound to that formal is owned at the call site (as in the foo + example below). Unconditional writes are rooted in a local, and they are only safe if a lock is + held in the caller. + To demonstrate what conditional writes buy us, consider the following example: + + foo() { + Object local = new Object(); + iWriteToAField(local); + } + + We don't want to warn on this example because the object pointed to by local is owned by the + caller foo, then ownership is transferred to the callee iWriteToAField. *) +type astate = + { + locks : LocksDomain.astate; + (** boolean that is true if a lock must currently be held *) + reads : PathDomain.astate; + (** access paths read outside of synchronization *) + conditional_writes : ConditionalWritesDomain.astate; + (** map of (formal index) -> set of access paths rooted in the formal index that are read + outside of synrchonization if the formal is not owned by the caller *) + unconditional_writes : PathDomain.astate; + (** access paths written outside of synchronization *) + id_map : IdAccessPathMapDomain.astate; + (** map used to decompile temporary variables into access paths *) + owned : OwnershipDomain.astate; + (** access paths that must be owned by the current function *) + } + +(** same as astate, but without [id_map]/[owned] (since they are local) *) +type summary = + LocksDomain.astate * PathDomain.astate * ConditionalWritesDomain.astate * PathDomain.astate + +include AbstractDomain.WithBottom with type astate := astate + +val make_access : RawAccessPath.t -> Location.t -> TraceElem.t + +val pp_summary : F.formatter -> summary -> unit