[swift-dev] Proposal: SIL Ownership Model + Verifier

[John McCall]

> On Dec 7, 2016, at 2:13 PM, Michael Gottesman via swift-dev <swift-dev at swift.org> wrote:
> 
> This is a proposal for a new SIL Ownership Model and verifier. An online HTML version of the document is available here:
> 
> https://gottesmm.github.io/proposals/sil-ownership-model.html <https://gottesmm.github.io/proposals/sil-ownership-model.html>
> 
> and inline below.
> 
> Michael
> 
> ----
> 
> # Summary
> 
> This document defines a SIL ownership model and a compile time static verifier
> for the model. This will allow for static compile time verification that a SIL
> program satisfies all ownership model constraints.
> 
> The proposed SIL ownership model embeds ownership into SIL's SSA def-use
> edges. This is accomplished by:
> 
> 1. Formalizing into SIL API's the distinction in between defs
>    (e.g. `SILInstruction` and `SILArgument`) and the values produced by defs
>    (e.g. `SILValue`). This is needed to model values as having ownership and
>    defs as not having ownership. The main implication here is that the two can
>    no longer be implicitly convertible and the API must enforce this.

We currently have two kinds of def: instructions and arguments.  Arguments
always define a single value, and I don't see anything in your proposal that
changes that.  And the idea that an instruction produces exactly one value is
already problematic, because many don't produce a meaningful value at all.
All that changes in your proposal is that certain instructions need to be able
to produce multiple values.

Moreover, the word "def" clearly suggests that it refers to the definition of a
value that can be used, and that's how the term is employed basically everywhere.

So allow me to suggest that a much clearer way of saying what you're trying to
say is that we need to distinguish between defs and instructions.  An instruction
may have an arbitrary number of defs, possibly zero, and each def is a value
that can be used.  (But the number of defs per instruction is known statically
for most instructions, which is something we can use to make working with
defs much less annoying.)

Also this stuff you're saying about values having ownership and defs not having
ownership is, let's say, misleading; it only works if you're using a meaninglessly
broad definition of ownership.  It would be better to simply say that the verification
we want to do for ownership strongly encourages us to allow instructions to 
introduce multiple defs whose properties can be verified independently.

> 2. Specifying a set of ownership kinds and specifying a method for mapping a
>    `SILValue` to an ownership kind.
> 3. Specifying ownership constraints on all `SILInstruction`s and `SILArgument`s
>    that constrain what ownership kinds their operands and incoming values
>    respectively can possess.
> 4. Implementing a verifier to ensure that all `SILInstruction` and `SILArgument`
>    are compatible with the ownership kind propagated by their operand
>    `SILValue`s and that pseudo-linear dataflow constraints are maintained.

I'll tackle these other sections in another email.  Let's go one at a time.

> # Cleanly separating Value and Def APIs in SIL
> 
> All values in SIL are defined via an assignment statement of the form: `<foo> = <bar>`.
> In English, we say `foo` is a value that is defined by the def
> `bar`. Originally, these two concepts were distinctly represented by the classes
> `SILValue` and `ValueBase`. All `ValueBase` defined a list of `SILValue` that
> were related, but not equivalent to the defining `ValueBase`. With the decision
> to represent multiple return values as instruction projections instead of as a
> list of `SILValue`, this distinction in between a def and the values was lost,
> resulting in `SILValue` being used interchangeably with `ValueBase` throughout
> the swift codebase. This exposes a modeling issue when one attempts to add
> ownership to SIL, namely that values have ownership, while the defs that define
> the values do not. This implies that defs and values *should not* be
> interchangeable.

Again, I do not understand what you're trying to say about ownership here.
Just drop it.

> In order to model that values, not defs, have ownership, we separate the
> `SILValue` and `ValueBase` APIs. This is done by:

Almost all of this is based on what I consider to be a really unfortunate use
of the term "def".

Allow me to suggest this:

1. You do not need to rename ValueBase.  Let's stick with the term "Value"
instead of "Def" in the source code.

2. There are only three subclasses of ValueBase for now:
  - SILArgument
  - SingleInstructionResult
  - MultiInstructionResult
This means that the Kind can probably be packed into the use-list pointer.

3. SingleInstructionResult will only be used for instructions that are known to
produce exactly one value.  All such instructions can derive from a single
class, of which SingleInstructionResult can be a superclass.  This will make
it possible to construct a SILValue directly from such instructions, as well as
making it easy to support dyn_casting back to such instructions.

4. MultiInstructionResult will have to store the result index as well as provide
some way to get back to the instruction.  I think the most efficient representation
here is to store an array of MultiInstructionResults immediately *before* the
address point of the instruction, in reverse order, so that (this + ResultIndex + 1)
gets you back to the instruction.  This also makes it possible to efficiently index
into the results without loading the number of results (except for the
bounds-checking assert, of course).

It will not be possible to construct a SILValue directly from one of these instructions;
you'll have to ask the instruction for its Nth result.

It's not clear to me what dyn_casting a SILValue back to a multi-result instruction
should do.  I guess it succeeds and then you just ask the instruction which
result you had.

5. SILInstruction has an accessor to return what's basically an ArrayRef of
its instruction results.  It's not quite an ArrayRef because that would require
type-punning, but you can make it work as efficiently as one.

John.


> 
> 1. Renaming `ValueBase` to `ValueDef`. This makes it clear from a naming
> perspective that a `ValueDef` is not a value, but may define values.
> 2. Eliminate all operator methods on `SILValue` that allow one to work with the
> `ValueDef` API via a `SILValue` in favor of an explicit method for getting the
> internal `ValueDef` of a `SILValue`, i.e.:
> 
>         class SILValue {
>           ...
>           ValueDef *operator->() const; // deleted
>           ValueDef &operator*() const; // deleted
>           operator ValueDef *() const; // deleted
> 
>           bool operator==(ValueDef *RHS) const; // deleted
>           bool operator!=(ValueDef *RHS) const; // deleted
>           ...
>           ValueDef *SILValue::getDef() const; // new
>           ...
>         };
> 
> 3. Use private access control and friend classes to only allow for `SILValue`s
>    to be constructed and vended by their defining `ValueDef` via a new method on
>    `ValueDef`:
> 
>         class SILValue {
>           friend class SILUndef; // new
>           friend class SILArgument; // new
>           friend class SILInstruction; // new
>         public:
>           SILValue(ValueDef *); // deleted
>         private:
>           SILValue(ValueDef *); // new
>         };
> 
>         class ValueDef {
>           ...
>           SILValue getValue() const; // new
>           ...
>         };
> 
> To see how specific common code patterns change in light of these changes,
> please see the [appendix](#changes-to-silvalue-api-for-sil-ownership).
> 
> # Values and ValueOwnershipKinds
> 
> Define `ValueOwnershipKind` as the enum with the following cases:
> 
>     enum class ValueOwnershipKind {
>       Trivial,
>       Unowned,
>       Owned,
>       Guaranteed,
>     }
> 
> Our approach to mapping a `SILValue` to a `ValueOwnershipKind` is to use a
> `SILVisitor` called `ValueOwnershipKindVisitor`. This works well since if one
> holds `ValueKind` constant, `SILValue` have well defined ownership
> constraints. Thus we can handle each case individually via the visitor. We use
> SILNodes.def to ensure that all `ValueKind` have a defined visitor method. This
> will ensure that when a new `ValueKind` is added, the compiler will emit a
> warning that the visitor must be updated, ensuring correctness.
> 
> The visitor will be hidden in a *.cpp file and will expose its output via a new
> API on `SILValue` :
> 
>     ValueOwnershipKind SILValue::getOwnershipKind() const;
> 
> Since the implementation of `SILValue::getOwnershipKind()` will be out of line,
> none of the visitor code will be exposed to the rest of the compiler.
> 
> # ValueDefs and Ownership Constraints
> 
> In order to determine if a `SILInstruction`'s operands are SILValue that have
> compatible ownership with a `SILInstruction`, we introduce a new API on
> `SILInstruction` that returns the ownership constraint of the `i`th operand of
> the `SILInstruction`:
> 
>     Optional<ValueOwnershipKind> SILInstruction::getOwnershipConstraint(unsigned i) const;
> 
> Specifically, it returns `.Some(OwnershipKind)` if there is a constraint or
> `.None` if the `SILInstruction` will accept any `ValueOwnershipKind`
> (e.g. `copy_value`). This API is sufficient since there are no `SILInstructions`
> that accept only a subset of `ValueOwnershipKind`, all either accept a singular
> ownership kind or all ownership kinds.
> 
> For `SILArgument`, we determine compatible ownership by introducing the concept
> of ownership conventions. The reason to introduce these ownership conventions is
> that it ensures that we do not need to perform any form of dataflow to determine
> the convention of a `SILArgument` in a loop. Additionally, it allows for greater
> readability in the IR and prevents the optimizer from performing implicit
> conversions of ownership semantics on branch instructions, for instance,
> converting a `switch_enum` from consuming a value at +1 to using a borrowed +0
> parameter. In terms of API, we introduce a new method on `SILArgument`:
> 
>     ValueOwnershipKind SILArgument::getOwnershipConstraint() const;
> 
> which returns the required ownership constraint. In terms of representing these
> ownership constraint conventions in textual SIL, we print out the ownership
> constraint next to the specific argument in the block and the specific argument
> in the given terminator. For details of how this will look with various
> terminators, see the [appendix](#sil-argument-terminator-convention-examples).
> 
> # Verification of Ownership Semantics
> 
> Since our ownership model is based around SSA form, all verification of
> ownership only need consider an individual value (`SILValue`) and the uses of
> the def (`SILInstruction`, `SILArgument`). Thus for each def/use-set, we:
> 
> 1. **Verify Use Semantics**: All uses must be compatible with the def's
>    `ValueOwnershipKind`.
> 2. **Dataflow Verification**: Given any path P in the program and a `ValueDef`
>    `V` along that path:
>    a. There exists only one <a href="#footnote-0-lifetime-ending-use">"lifetime ending"</a> use of `V` along that path.
>    b. After the lifetime ending use of `V`, there are no non-lifetime ending
>       uses of `V` along `P`.
> 
> Since the dataflow verification requires knowledge of a subset of the uses, we
> perform the use semantic verification first and then use the found uses for the
> dataflow verification.
> 
> ## Use Verification
> 
> Just like with `SILValue`, individual `SILInstruction` kind's have well-defined
> ownership semantics implying that we can use a `SILVisitor` approach here as
> well. Thus we define a `SILVisitor` called
> `OwnershipCompatibilityUseChecker`. This checker works by taking in a `SILValue`
> and visiting all of the `SILInstruction` users of the `SILValue`. Each visitor
> method returns a pair of booleans, the first stating whether or not the
> ownership values were compatible and the second stating whether or not this
> specific use should be considered a "lifetime ending" use. The checker then
> stores the lifetime ending uses and non-lifetime ending uses in two separate
> arrays for processing by the dataflow verifier.
> 
> ## Dataflow Verification
> 
> The dataflow verifier takes in as inputs the `SILValue` and lists of
> lifetime-ending and non-lifetime ending uses. Since we are using SSA form, we
> already know that our def must dominate all of our uses implying that a use can
> never overconsume due to a def not being along a path. On the other hand, we
> still must consider issues related to joint post-dominance namely:
> 
> 1. Double-Consume due to 2+ lifetime ending uses along a path. This implies
>    proving that no lifetime ending use is reachable from another lifetime ending
>    use.
> 2. Use-After-Free due to a non-lifetime ending use not being joint-post
>    dominated by the lifetime ending uses. This implies proving that all
>    non-lifetime ending uses are joint post-dominated by the lifetime ending use
>    set.
> 3. Lifetime-Leaks due to the non-lifetime ending uses not joint-post dominating
>    the lifetime ending uses.
> 
> Note how we must consider joint post-dominance in two different places. Thus we
> must be able to prove joint post-dominance quickly and cheaply. To do so, we
> take advantage of dominance implying that all uses are reachable from the def to
> just needing to prove that when we walk the CFG up to prove reachability, that
> any block on the reachability path does not have any successors that have not
> been visited when we finish walking and visit the def.
> 
> The full code is in the [appendix](#full-dataflow-verification-algorithm).
> 
> <a id="footnote-0-lifetime-ending-use">[0]</a>: A use after which a def is no
> longer allowed to be used in any way, e.g. `destroy_value`, `end_borrow`.
> 
> # Appendix
> 
> ## Changes to SILValue API for SIL Ownership
> 
> The common code pattern eliminated by removing implicit uses of `ValueDef`'s API
> via a `SILValue` are as follows:
> 
>     SILValue V;
>     ValueDef *Def;
> 
>     if (V != Def) { ... }
>     if (V->getParentBlock()) { ... }
> 
> Our change, causes these code patterns to be rewritten in favor of the explicit:
> 
>     SILValue V;
>     ValueDef *Def;
> 
>     if (V.getDef() != Def) { ... }
>     if (V.getDef()->getParentBlock()) { ... }
> 
> In cases like the above, we want the to increase clarity through the usage of
> verbosity. In other cases, this verboseness makes convenient APIs more difficult
> to use. The main example here are the `isa` and `dyn_cast` APIs. We introduce
> two helper functions that give the same convenience as before but added clarity by
> making it clear that we are not performing an isa query on the value, but
> instead the underlying def of the value:
> 
>     template <typename ParentTy>
>     bool def_isa(SILValue V) { return isa<ParentTy>(V.getDef()); }
>     template <typename ParentTy>
>     ParentTy *def_dyn_cast(SILValue V) { return dyn_cast<ParentTy>(V.getDef()); }
> 
> Consider the following code using the old API,
> 
>     SILValue V;
> 
>     if (isa<ApplyInst>(V)) { ... }
>     if (auto *PAI = dyn_cast<PartialApplyInst>(V)) { ... }
> 
> Notice how it seems like one is casting the SILValue as if it is a
> ValueBase. This is due to the misleading usage of the implicit conversion from a
> `SILValue` to the `SILValue`'s internal `ValueBase`. In comparison the new API
> makes it absolutely clear that one is reasoning about the ValueKind of the
> underlying def of the `SILValue`:
> 
>     SILValue V;
> 
>     if (def_isa<ApplyInst>(V)) { ... }
>     if (auto *PAI = def_dyn_cast<PartialApplyInst>(V)) { ... }
> 
> Thus the convenience of the old API is maintained, clarity is improved, and the
> conceptual API boundary is enforced.
> 
> The final change that we propose is eliminating the ability to construct a
> `SILValue` from a `ValueDef` externally to the `ValueDef` itself. Allowing this
> to occur violates the modeling notion that a `SILValue` is defined and thus is
> dependent on the `ValueDef`. To implement this, we propose changing the
> constructor `SILValue::SILValue(ValueDef *)` to have private instead of public
> access control and declaring `ValueDef` subclasses as friends of
> `SILValue`. This then allows the `ValueDef` to vend opaquely constructed
> `SILValue`, but disallows external users of the API from directly creating
> `SILValue` from `ValueDef`, enforcing the value/def distinction in our model.
> 
> ## SILArgument/Terminator OwnershipConvention Examples
> 
> We present here several examples of how ownership conventions look on
> SILArguments and terminators.
> 
> First we present a simple branch and return example.
> 
>     class C { ... }
> 
>     sil @simple_branching : $@convention(thin) : @convention(thin) (@owned Builtin.NativeObject, @guaranteed C) -> @owned C {
>     bb0(%0 : @owned $Builtin.NativeObject, %1 : @guaranteed $C):
>       br bb1(%0 : @owned $Builtin.NativeObject)
> 
>     bb1(%1 : @owned $Builtin.NativeObject):
>       strong_release %1 : $Builtin.NativeObject
>       %2 = copy_value %0 : $C
>       return %2 : @owned $C
>     }
> 
> Now consider this loop example:
> 
>     sil @loop : $@convention(thin) : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {
>     bb0(%0 : @owned $Optional<Builtin.NativeObject>):
>       br bb1(%0 : @owned $Builtin.NativeObject)
> 
>     bb1(%1 : @owned $Builtin.NativeObject):
>       %2 = alloc_object $C
>       strong_release %1 : $Builtin.NativeObject
>       %3 = unchecked_ref_cast %2 : $C to $Builtin.NativeObject
>       cond_br %cond, bb1(%3 : @owned Builtin.NativeObject), bb2
> 
>     bb2:
>       strong_release %3 : $Builtin.NativeObject
>       %result = tuple()
>       return %result : @trivial $()
>     }
> 
> Note how it is absolutely clear what convention is being used when passing a
> value to the phi node. No dataflow reasoning is required implying we can do a
> simple pass over the CFG to prove correctness.
> 
> Now consider two examples of switches:
> 
>     sil @owned_switch_enum : $@convention(thin) : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {
>     bb0(%0 : @owned $Optional<Builtin.NativeObject>):
>       switch_enum %0 : @owned $Builtin.NativeObject, #Optional.none.enumelt: bb1, #Optional.some.enumelt.1: bb2
> 
>     bb1:
>       br bb3
> 
>     bb2(%1 : @owned $Builtin.NativeObject):
>       strong_release %1 : $Builtin.NativeObject
>       br bb3
> 
>     bb3:
>       %result = tuple()
>       return %result : @trivial $()
>     }
> 
>     sil @guaranted_converted_switch_enum : $@convention(thin) : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {
>     bb0(%0 : @owned $Optional<Builtin.NativeObject>):
>       %1 = begin_borrow %0 : $Optional<Builtin.NativeObject>
>       switch_enum %1 : @guaranteed $Builtin.NativeObject, #Optional.none.enumelt: bb1, #Optional.some.enumelt.1: bb2
> 
>     bb1:
>       br bb3
> 
>     bb2(%2 : @guaranteed $Builtin.NativeObject):
>       %3 = function_ref @g_user : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()
>       apply %3(%2) : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()
>       br bb3
> 
>     bb3:
>       end_borrow %1 from %0 : $Optional<Builtin.NativeObject>, $Optional<Builtin.NativeObject>
>       %result = tuple()
>       return %result : @trivial $()
>     }
> 
> Notice how the lifetime is completely explicit in both cases, so the optimizer
> can not treat the conversion of switch_enum from +1 to +0 implicitly.
> 
> ## Full Dataflow Verification Algorithm
> 
> Define the following book keeping data structures.
> 
>     // The worklist that we will use for our iterative reachability query.
>     llvm::SmallVector<SILBasicBlock *, 32> Worklist;
> 
>     // The set of blocks with lifetime ending uses.
>     llvm::SmallPtrSet<SILBasicBlock *, 8> BlocksWithLifetimeEndingUses;
> 
>     // The set of blocks with non-lifetime ending uses and the associated
>     // non-lifetime ending use SILInstruction.
>     llvm::SmallDenseMap<SILBasicBlock *, SILInstruction *, 8> BlocksWithNonLifetimeEndingUses;
> 
>     // The blocks that we have already visited.
>     llvm::SmallPtrSet<SILBasicBlock *, 32> VisitedBlocks;
> 
>     // A list of successor blocks that we must visit by the time the algorithm terminates.
>     llvm::SmallPtrSet<SILBasicBlock *, 8> SuccessorBlocksThatMustBeVisited;
> 
> Then for each non-lifetime ending use (found by the
> `OwnershipCompatibilityUseChecker`), we add the block and its instruction to the
> `BlocksWithNonLifetimeEndingUses`. There is a possibility of having multiple
> non-lifetime ending uses in the same block, in such a case, we always take the
> later value since we are performing a liveness-esque dataflow:
> 
>     for (SILInstruction *User : getNonLifetimeEndingUses()) {
>       // First try to associate User with User->getParent().
>       auto Result = BlocksWithNonLifetimeEndingUses.insert({User->getParent(), User});
> 
>       // If the insertion succeeds, then we know that there is no more work to
>       // be done, so process the next use.
>       if (Result.second)
>         continue;
> 
>       // If the insertion fails, then we have at least two non-lifetime ending uses
>       // in the same block. Since we are performing a liveness type of dataflow,
>       // we only need the last non-lifetime ending use to show that all lifetime
>       // ending uses post dominate both. Thus, see if Use is after
>       // Result.first->second in the use list. If Use is not later, then we wish
>       // to keep the already mapped value, not use, so continue.
>       if (std::find(Result.first->second->getIterator(), Block->end(), User) ==
>             Block->end()) {
>         continue;
>       }
> 
>       // At this point, we know that Use is later in the Block than
>       // Result.first->second, so store Use instead.
>       Result.first->second = User;
>     }
> 
> Then we visit each each lifetime ending use and its parent block:
> 
>     for (SILInstruction *User : getLifetimeEndingUses()) {
>       SILBasicBlock *UserParentBlock = User->getParent();
>       ...
>     }
> 
> We begin by adding `UserParentBlock` to the `BlocksWithLifetimeEndingUses`
> set. If a block is already in the set (i.e. insert fails), then we know that (1)
> has been violated and we error. If we never hit that condition, then we know
> that all lifetime ending uses are in different blocks.
> 
>     if (!BlocksWithLifetimeEndingUses.insert(UserParentBlock).second) {
>       double_consume_error(); // ERROR!
>     }
> 
> Then we check if we previously saw any non-lifetime ending uses in
> `UserParentBlock` by checking the map `BlocksWithNonLifetimeEndingUses`. If we do
> find any such uses, we check if the lifetime ending use is earlier in the block
> that the non-lifetime ending use. If so then (2) is violated and we
> error. Once we know that (2) has not been violated, we remove
> 
>     auto Iter = BlocksWithNonLifetimeEndUses.find(UserParentBlock);
>     if (Iter != BlocksWithNonLifetimeEndUses.end()) {
>       // Make sure that the non-lifetime ending use is before the lifetime
>       // ending use. Otherwise, we have a use after free.
>       if (std::find(User->getIterator(), UserParentBlock->end(), Iter->second) !=
>             UserParentBlock->end()) {
>         use_after_free_error(); // ERROR!
>       }
> 
>       // Erase the use since we know that it is properly joint post-dominated.
>       BlocksWithNonLifetimeEndingUses.erase(Iter);
>     }
> 
> Then we mark `UserParentBlock` as visited to ensure that we do not consider
> UserParentBlock to be a successor we must visit and prime the worklist with the
> predecessor blocks of `UserParentBlock`.
> 
>     // Then mark UserParentBlock as visited add all predecessors of
>     // UserParentBlock to the worklist.
>     VisitedBlocks.insert(UserParentBlock);
>     copy(UserParentBlock->getPreds(), std::back_inserter(Worklist));
> 
> The entire block of code is provided in the appendix. Now we know that:
> 
> 1. All lifetime ending uses are in different basic blocks.
> 2. All non-lifetime ending uses are either in different basic blocks.
> 
> We begin our worklist algorithm by popping off the next element in the worklist.
> 
>     // Until the worklist is empty.
>     while (!Worklist.empty()) {
>       // Grab the next block to visit.
>       const SILBasicBlock *BB = Worklist.pop_back_val();
>       ...
>     }
> 
> Since every time we insert objects into the worklist, we first try to insert it
> into the `VisitedBlock` list, we do not need to check if `BB` has been visited
> yet, since elements can not be added to the worklist twice.
> 
> Then make sure that BB is not in `BlocksWithLifetimeEndingUses`. If BB is in
> `BlocksWithLifetimeEndingUses`, then we know that there is a path going through
> the def where the def is consumed twice, an error!
> 
>     if (BlocksWithLifetimeEndingUses.count(BB)) {
>       double_consume_error(); // ERROR!
>     }
> 
> Now that we know we are not double consuming, we need to update our data
> structures. First if BB is contained in SuccessorBlocksThatMustBeVisited, we
> remove it. This ensures when the algorithm terminates, we know that the path
> through the successor was visited as apart of our walk.
> 
>     SuccessorBlocksThatMustBeVisited.erase(BB);
> 
> Then if BB is in BlocksWithNonLifetimeEndingUses, we remove it. This ensures
> that when the algorithm terminates, we know that the non-lifetime ending uses
> were properly joint post-dominated by the lifetime ending uses.
> 
>     BlocksWithNonLifetimeEndingUses.erase(BB);
> 
> Then add all successors of BB that we have not visited yet to the
> `SuccessorBlocksThatMustBeVisited` set. This ensures that if we do not visit the
> successor as apart of our CFG walk, at the end of the algorithm we will assert
> that there is a leak.
> 
>     for (const SILBasicBlock *SuccBlock : BB->getSuccessorBlocks()) {
>       // If we already visited the successor, there is nothing to do since
>       // we already visited the successor.
>       if (VisitedBlocks.count(SuccBlock))
>         continue;
> 
>       // Otherwise, add the successor to our MustVisitBlocks set to ensure that
>       // we assert if we do not visit it by the end of the algorithm.
>       SuccessorBlocksThatMustBeVisited.insert(SuccBlock);
>     }
> 
> Finally add all predecessors of BB that we have not visited yet to the Worklist
> for processing. We use insert here to ensure that we only ever add a
> VisitedBlock once to the Worklist:
> 
>     for (const SILBasicBlock *PredBlock : BB->getPredecessorBlocks()) {
>       if (!VisitedBlocks.insert(PredBlock).second)
>         continue;
>       Worklist.push_back(PredBlock);
>     }
> 
> This continues until we have exhausted the worklist. Once the worklist is
> exhausted, we know that:
> 
> 1. If `SuccessorBlocksThatMustBeVisited` is non-empty, then the Blocks in the
>    set are not joint post-dominated by the set of lifetime ending users implying
>    a leak.
> 2. If `BlockSwithNonLifetimeEndingUses` is non-empty, then there was a
>    non-lifetime ending use that was not joint post-dominated by the lifetime
>    ending use set. This implies a use-after free.
> 
> Thus we assert that both sets are empty and error accordingly.
> 
>     if (!SuccessorBlocksThatMustBeVisited.empty()) {
>       leak_error(); // ERROR!
>     }
>     if (!BlocksWithNonLifetimeEndingUses.empty()) {
>       use_after_free_error(); // ERROR!
>     }
> 
> The full code:
> 
>     // The worklist that we will use for our iterative reachability query.
>     llvm::SmallVector<SILBasicBlock *, 32> Worklist;
> 
>     // The set of blocks with lifetime ending uses.
>     llvm::SmallPtrSet<SILBasicBlock *, 8> BlocksWithLifetimeEndingUses;
> 
>     // The set of blocks with non-lifetime ending uses and the associated
>     // non-lifetime ending use SILInstruction.
>     llvm::SmallDenseMap<SILBasicBlock *, SILInstruction *, 8> BlocksWithNonLifetimeEndingUses;
> 
>     // The blocks that we have already visited.
>     llvm::SmallPtrSet<SILBasicBlock *, 32> VisitedBlocks;
> 
>     // A list of successor blocks that we must visit by the time the algorithm terminates.
>     llvm::SmallPtrSet<SILBasicBlock *, 8> SuccessorBlocksThatMustBeVisited;
> 
>     for (SILInstruction *User : getLifetimeEndingUses()) {
>       SILBasicBlock *UserParentBlock = User->getParent();
>       if (!BlocksWithLifetimeEndingUses.insert(UserParentBlock).second) {
>         double_consume_error(); // ERROR!
>       }
> 
>       auto Iter = BlocksWithNonLifetimeEndUses.find(UserParentBlock);
>       if (Iter != BlocksWithNonLifetimeEndUses.end()) {
>         // TODO: Could this be cached.
>         if (std::find(User->getIterator(), UserParentBlock->end(), Iter->second) !=
>               UserParentBlock->end()) {
>           use_after_free_error(); // ERROR!
>         }
>       }
> 
>       // Then add all predecessors of the user block to the worklist.
>       VisitedBlocks.insert(UserParentBlock);
>       copy(UserParentBlock->getPreds(), std::back_inserter(Worklist));
>     }
> 
>     // Until the worklist is empty.
>     while (!Worklist.empty()) {
>       // Grab the next block to visit.
>       const SILBasicBlock *BB = Worklist.pop_back_val();
> 
>       // Then check that BB is not a lifetime-ending use block. If it is error,
>       // since we have an overconsume.
>       if (BlocksWithLifetimeEndingUses.count(BB)) {
>         double_consume_error(); // ERROR!
>       }
> 
>       // Ok, now we know that we are not double-consuming. Update our data
>       // structures.
> 
>       // First remove BB from the SuccessorBlocksThatMustBeVisited list. This
>       // ensures that when the algorithm terminates, we know that BB was not the
>       // beginning of a non-covered path to the exit.
>       SuccessorBlocksThatMustBeVisited.erase(BB);
> 
>       // Then remove BB from BlocksWithNonLifetimeEndingUses so we know that
>       // this block was properly joint post-dominated by our lifetime ending
>       // users.
>       BlocksWithNonLifetimeEndingUses.erase(BB);
> 
>       // Then add all successors of BB that we have not visited yet to the
>       // SuccessorBlocksThatMustBeVisited set.
>       for (const SILBasicBlock *SuccBlock : BB->getSuccessorBlocks()) {
>         // If we already visited the successor, there is nothing to do since
>         // we already visited the successor.
>         if (VisitedBlocks.count(SuccBlock))
>           continue;
> 
>         // Otherwise, add the successor to our MustVisitBlocks set to ensure that
>         // we assert if we do not visit it by the end of the algorithm.
>         SuccessorBlocksThatMustBeVisited.insert(SuccBlock);
>       }
> 
>       // Finally add all predecessors of BB that have not been visited yet to
>       // the worklist.
>       for (const SILBasicBlock *PredBlock : BB->getPredecessorBlocks()) {
>         // Try to insert the PredBlock into the VisitedBlocks list to ensure
>         // that we only ever add a block once to the worklist.
>         if (!VisitedBlocks.insert(PredBlock).second)
>           continue;
>         Worklist.push_back(PredBlock);
>       }
>     }
> 
>     if (!SuccessorBlocksThatMustBeVisited.empty()) {
>       leak_error(); // ERROR!
>     }
>     if (!BlocksWithNonLifetimeEndingUses.empty()) {
>       use_after_free_error(); // ERROR!
>     }
> 
> ----
> 
>> On Dec 5, 2016, at 6:47 PM, Michael Gottesman <mgottesman at apple.com <mailto:mgottesman at apple.com>> wrote:
>> 
>>> 
>>> On Dec 5, 2016, at 5:26 PM, Andrew Trick <atrick at apple.com <mailto:atrick at apple.com>> wrote:
>>> 
>>> 
>>>> On Dec 5, 2016, at 3:55 PM, Michael Gottesman <mgottesman at apple.com <mailto:mgottesman at apple.com>> wrote:
>>>> 
>>>> Hello everyone.
>>>> 
>>>> This is an initial draft of a proposal for the SIL Ownership Model + Verifier. I am mainly looking for any high level concerns. If there are none, then I am fine moving this straight to swift-dev.
>>>> 
>>>> It is online here:
>>>> 
>>>> https://gottesmm.github.io/proposals/sil-ownership-model.html <https://gottesmm.github.io/proposals/sil-ownership-model.html>
>>>> 
>>>> Michael
>>> 
>>> 
>>> Thanks! It looks good.
>>> 
>>> > `ValueDef` is not a value, but the def of a value.
>>> 
>>> Should be "but may define (or produce) values.".
>> 
>> Sure.
>> 
>>> 
>>> > Since our ownership model is based around SSA form
>>> 
>>> There's an in-memory aspect as well. Ownership of local memory should be statically verified. We at least need a TBD section for this.
>> 
>> Ok.
>> 
>>> 
>>> > This checker works by taking in a
>>> `ValueDef` and visiting all of the `SILInstruction` users of the
>>> `ValueDef`.
>>> 
>>> This line does not compute for me. A ValueDef does not have ownership. The verifier is simply checking constraints for each SILValue against all of its uses. At the verifier's level of abstraction, it doesn't matter who defined that value.
>> 
>> That is a typo. If you look earlier I was using explicitly SILValue.
>> 
>>> 
>>> > The dataflow verifier takes in as inputs the `ValueDef` (i.e. def) and lists of lifetime-ending and non-lifetime ending uses.
>>> 
>>> Again, the verifier would not care about the uses of the ValueDef, it cares about uses of the SILValue. I think this is a misleading way to formulate the problem and explain the algorithm.
>> 
>> That is a typo from an earlier version of the algorithm. Everything should be about the SILValue.
>> 
>>> 
>>> >  if (V.getDef()->getParentBlock()) { ... }
>>> 
>>> I see no reason we can't add getParentBlock() and other very common idioms to the SILValue API.
>> 
>> The question is how much should we make that a def only API.
>> 
>>> 
>>> > if (auto *PAI = def_dyn_cast<PartialApplyInst>(V)) { ... }
>>> 
>>> It's not obvious to be that this is more readable than 
>>> 
>>> if (auto *PAI = dyn_cast<PartialApplyInst>(V.getDef())) { ... }
>>> 
>>> But I don't have a strong opinion on it.
>> 
>> it is just a little shorter. I am also not wedded to this. I was just trying to create a vision of what is possible to stimulate discussion.
>> 
>>> 
>>> > The final change that we propose is eliminating the ability to construct a
>>> `SILValue` from a `ValueDef` externally to the `ValueDef` itself.
>>> 
>>> Nice!
>>> 
>>> I didn't reread the "Full Dataflow Verification Algorithm" because I don't think it's changed much. I'll review it again after the final proposal.
>> 
>> It is exactly the same as the version I showed you before, except I followed your suggestion about putting the visit before things are added to the worklist rather than after it is popped off the worklist.
>> 
>> Let me fix this real quick.
>> 
>> Michael
>> 
>>> 
>>> -Andy
> 
> 
> _______________________________________________
> swift-dev mailing list
> swift-dev at swift.org
> https://lists.swift.org/mailman/listinfo/swift-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.swift.org/pipermail/swift-dev/attachments/20161207/19df61c6/attachment.html>