<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div><blockquote type="cite" class=""><div class="">On Dec 8, 2016, at 2:36 PM, Michael Gottesman <<a href="mailto:mgottesman@apple.com" class="">mgottesman@apple.com</a>> wrote:</div><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><blockquote type="cite" class=""><div class="">On Dec 8, 2016, at 2:00 PM, John McCall <<a href="mailto:rjmccall@apple.com" class="">rjmccall@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><blockquote type="cite" class=""><div class="">On Dec 8, 2016, at 1:53 PM, Andrew Trick <<a href="mailto:atrick@apple.com" class="">atrick@apple.com</a>> wrote:</div><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><blockquote type="cite" class=""><div class="">On Dec 7, 2016, at 11:25 PM, John McCall via swift-dev <<a href="mailto:swift-dev@swift.org" class="">swift-dev@swift.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" class=""><div class=""><br class="Apple-interchange-newline">On Dec 7, 2016, at 2:13 PM, Michael Gottesman via swift-dev <<a href="mailto:swift-dev@swift.org" class="">swift-dev@swift.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">This is a proposal for a new SIL Ownership Model and verifier. An online HTML version of the document is available here:<br class=""><div class=""><br class=""></div><div class=""><a href="https://gottesmm.github.io/proposals/sil-ownership-model.html" class="">https://gottesmm.github.io/proposals/sil-ownership-model.html</a></div><div class=""><br class=""></div><div class="">and inline below.</div><div class=""><br class=""></div><div class="">Michael</div><div class=""><br class=""></div><div class="">----</div><div class=""><br class=""></div><div class=""><div class=""># Summary</div><div class=""><br class=""></div><div class="">This document defines a SIL ownership model and a compile time static verifier</div><div class="">for the model. This will allow for static compile time verification that a SIL</div><div class="">program satisfies all ownership model constraints.</div><div class=""><br class=""></div><div class="">The proposed SIL ownership model embeds ownership into SIL's SSA def-use</div><div class="">edges. This is accomplished by:</div><div class=""><br class=""></div><div class="">1. Formalizing into SIL API's the distinction in between defs</div><div class=""> (e.g. `SILInstruction` and `SILArgument`) and the values produced by defs</div><div class=""> (e.g. `SILValue`). This is needed to model values as having ownership and</div><div class=""> defs as not having ownership. The main implication here is that the two can</div><div class=""> no longer be implicitly convertible and the API must enforce this.</div></div></div></div></div></div></blockquote></div></div></blockquote><div class=""><br class=""></div><div class="">This proposal is simultaneously proposing some specific API details</div><div class="">while avoiding both the motivation behind it and the eventual features</div><div class="">that it will support.</div><div class=""><br class=""></div><div class="">I think the ValueBase/Def renaming is a little</div><div class="">misunderstanding. "ValueDef" in the proposal was a placeholder (not a</div><div class="">perfect name) for some perceived need to have a common</div><div class="">SILArgument/SILInstruction base class. That's probably not necessary</div><div class="">in which case there's nothing to disagree about.</div><div class=""><br class=""></div><div class="">John's counter proposal solves that problem by repurposing ValueBase</div><div class="">to serve as a base class for value definitions (and then goes into</div><div class="">some detail on implementing multi-result instructions).</div><div class=""><br class=""></div><blockquote type="cite" class=""><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">We currently have two kinds of def: instructions and arguments. Arguments</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">always define a single value, and I don't see anything in your proposal that</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">changes that. And the idea that an instruction produces exactly one value is</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">already problematic, because many don't produce a meaningful value at all.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">All that changes in your proposal is that certain instructions need to be able</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">to produce multiple values.</div></div></blockquote><div class=""><br class=""></div><div class="">That’s an obvious way of looking at it. I personally am most</div><div class="">interested in putting an end to the chronic problem of conflating</div><div class="">instructions and values which literally makes it impossible to have a</div><div class="">sane discussion about ownership. I insisted that SILInstruction not</div><div class="">derive from ValueBase, which probably led to the proposed</div><div class="">renaming. This probably comes across as confusing because the proposal</div><div class="">is deliberately side-stepping the issue of multi-result instructions.</div><div class=""><br class=""></div><div class="">What I really want to see at the proposal level is agreement on core concepts:</div><div class="">- A value has a type, ownership, one def, and 0..n uses</div><div class="">- Ownership rules are guaranteed simply by evaluating those 0..n uses.</div><div class="">- A value’s def/use is the point at which it is produced/consumed.</div><div class="">- Use/def points are demarcated by instructions or block boundaries</div><div class="">- An instruction produces values via results or consumes them via operands.</div><div class=""><br class=""></div><div class="">There shouldn't be any debate about these concepts, so why is there so</div><div class="">much confusion? I think caused by some bad choices in the SIL</div><div class="">interface, particularly as SILInstruction : ValueBase.</div><div class=""><br class=""></div><div class="">So we should define a SIL interface that reflects those core</div><div class="">concepts. We should be able to reimplement multi-result instructions</div><div class="">without affecting those interfaces and without rewritting SIL passes.</div></div></div></div></blockquote><div class=""><br class=""></div>I agree. I don't think this requires deep changes to how SIL nodes are typically</div><div class="">worked with. As long as single-result instructions can be transparently used as</div><div class="">values, so that e.g. the result of SILBuilder::CreateBitCast can be used as a</div><div class="">SILValue, the number of changes required should be quite modest.</div><div class=""><br class=""></div><div class="">Things like SILCloner will of course need some minor updates to handle the</div><div class="">fact that a single instruction can have multiple uses, but that should be straightforward</div><div class="">to do on top of the existing Value->Value mapping.</div></div></div></blockquote><div class=""><br class=""></div><div class="">Just to be clear to the list, what happened here is that I was trying to put some of the initial work for multiple return values and clarifying ownership into this proposal and then I was going to continue with a separate proposal that actually proposed multiple return values and the rest of that API.</div><div class=""><br class=""></div><div class="">John: Lets use this thread to talk about the verifier part of the proposal. I have most of a multiple return value proposal complete that is very similar to what you are talking about. If it would be helpful, I can rip out the first part of this proposal if it would be easier for you to read.</div></div></div></div></blockquote><div><br class=""></div>You don't need to change the proposal for it to be "ratified"; this isn't swift-evolution.</div><div>I'll just comment on the rest of the proposal separately.</div><div><br class=""></div><div>But yes, in the future, please avoid starting proposals with 500-word digressions</div><div>about things you don't want to talk about. :)</div><div><br class=""></div><div>John.</div><div><br class=""></div><div><br class=""></div><div><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><div class=""><br class=""></div><div class="">Michael</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><br class=""></div><div class="">John.</div><div class=""><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class=""><div class=""><br class=""></div><div class="">-Andy</div><div class=""><br class=""></div><blockquote type="cite" class=""><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Moreover, the word "def" clearly suggests that it refers to the definition of a</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">value that can be used, and that's how the term is employed basically everywhere.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">So allow me to suggest that a<span class="Apple-converted-space"> </span><i class="">much</i> clearer way of saying what you're trying to</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">say is that we need to distinguish between defs and<span class="Apple-converted-space"> </span><b class="">instructions</b>. An instruction</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">may have an arbitrary number of defs, possibly zero, and each def is a value</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">that can be used. (But the number of defs per instruction is known statically</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">for most instructions, which is something we can use to make working with</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">defs much less annoying.)</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Also this stuff you're saying about values having ownership and defs not having</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">ownership is, let's say, misleading; it only works if you're using a meaninglessly</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">broad definition of ownership. It would be better to simply say that the verification</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">we want to do for ownership strongly encourages us to allow instructions to </div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">introduce multiple defs whose properties can be verified independently.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="">2. Specifying a set of ownership kinds and specifying a method for mapping a</div><div class=""> `SILValue` to an ownership kind.</div><div class="">3. Specifying ownership constraints on all `SILInstruction`s and `SILArgument`s</div><div class=""> that constrain what ownership kinds their operands and incoming values</div><div class=""> respectively can possess.</div><div class="">4. Implementing a verifier to ensure that all `SILInstruction` and `SILArgument`</div><div class=""> are compatible with the ownership kind propagated by their operand</div><div class=""> `SILValue`s and that pseudo-linear dataflow constraints are maintained.</div></div></div></div></div></div></blockquote><div class=""><br class=""></div>I'll tackle these other sections in another email. Let's go one at a time.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""># Cleanly separating Value and Def APIs in SIL</div><div class=""><br class=""></div><div class="">All values in SIL are defined via an assignment statement of the form: `<foo> = <bar>`.</div><div class="">In English, we say `foo` is a value that is defined by the def</div><div class="">`bar`. Originally, these two concepts were distinctly represented by the classes</div><div class="">`SILValue` and `ValueBase`. All `ValueBase` defined a list of `SILValue` that</div><div class="">were related, but not equivalent to the defining `ValueBase`. With the decision</div><div class="">to represent multiple return values as instruction projections instead of as a</div><div class="">list of `SILValue`, this distinction in between a def and the values was lost,</div><div class="">resulting in `SILValue` being used interchangeably with `ValueBase` throughout</div><div class="">the swift codebase. This exposes a modeling issue when one attempts to add</div><div class="">ownership to SIL, namely that values have ownership, while the defs that define</div><div class="">the values do not. This implies that defs and values *should not* be</div><div class="">interchangeable.</div></div></div></div></div></div></blockquote><div class=""><br class=""></div>Again, I do not understand what you're trying to say about ownership here.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Just drop it.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="">In order to model that values, not defs, have ownership, we separate the</div><div class="">`SILValue` and `ValueBase` APIs. This is done by:</div></div></div></div></div></div></blockquote><div class=""><br class=""></div>Almost all of this is based on what I consider to be a really unfortunate use</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">of the term "def".</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">Allow me to suggest this:</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">1. You do not need to rename ValueBase. Let's stick with the term "Value"</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">instead of "Def" in the source code.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">2. There are only three subclasses of ValueBase for now:</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> - SILArgument</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> - SingleInstructionResult</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""> - MultiInstructionResult</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">This means that the Kind can probably be packed into the use-list pointer.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">3. SingleInstructionResult will only be used for instructions that are known to</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">produce exactly one value. All such instructions can derive from a single</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">class, of which SingleInstructionResult can be a superclass. This will make</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">it possible to construct a SILValue directly from such instructions, as well as</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">making it easy to support dyn_casting back to such instructions.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">4. MultiInstructionResult will have to store the result index as well as provide</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">some way to get back to the instruction. I think the most efficient representation</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">here is to store an array of MultiInstructionResults immediately *before* the</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">address point of the instruction, in reverse order, so that (this + ResultIndex + 1)</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">gets you back to the instruction. This also makes it possible to efficiently index</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">into the results without loading the number of results (except for the</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">bounds-checking assert, of course).</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">It will not be possible to construct a SILValue directly from one of these instructions;</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">you'll have to ask the instruction for its Nth result.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">It's not clear to me what dyn_casting a SILValue back to a multi-result instruction</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">should do. I guess it succeeds and then you just ask the instruction which</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">result you had.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">5. SILInstruction has an accessor to return what's basically an ArrayRef of</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">its instruction results. It's not quite an ArrayRef because that would require</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">type-punning, but you can make it work as efficiently as one.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">John.</div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><br class=""></div><div class="">1. Renaming `ValueBase` to `ValueDef`. This makes it clear from a naming</div><div class="">perspective that a `ValueDef` is not a value, but may define values.</div></div></div></div></div></div></blockquote><blockquote type="cite" class=""><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class="">2. Eliminate all operator methods on `SILValue` that allow one to work with the</div><div class="">`ValueDef` API via a `SILValue` in favor of an explicit method for getting the</div><div class="">internal `ValueDef` of a `SILValue`, i.e.:</div><div class=""><br class=""></div><div class=""> class SILValue {</div><div class=""> ...</div><div class=""> ValueDef *operator->() const; // deleted</div><div class=""> ValueDef &operator*() const; // deleted</div><div class=""> operator ValueDef *() const; // deleted</div><div class=""><br class=""></div><div class=""> bool operator==(ValueDef *RHS) const; // deleted</div><div class=""> bool operator!=(ValueDef *RHS) const; // deleted</div><div class=""> ...</div><div class=""> ValueDef *SILValue::getDef() const; // new</div><div class=""> ...</div><div class=""> };</div><div class=""><br class=""></div><div class="">3. Use private access control and friend classes to only allow for `SILValue`s</div><div class=""> to be constructed and vended by their defining `ValueDef` via a new method on</div><div class=""> `ValueDef`:</div><div class=""><br class=""></div><div class=""> class SILValue {</div><div class=""> friend class SILUndef; // new</div><div class=""> friend class SILArgument; // new</div><div class=""> friend class SILInstruction; // new</div><div class=""> public:</div><div class=""> SILValue(ValueDef *); // deleted</div><div class=""> private:</div><div class=""> SILValue(ValueDef *); // new</div><div class=""> };</div><div class=""><br class=""></div><div class=""> class ValueDef {</div><div class=""> ...</div><div class=""> SILValue getValue() const; // new</div><div class=""> ...</div><div class=""> };</div><div class=""><br class=""></div><div class="">To see how specific common code patterns change in light of these changes,</div><div class="">please see the [appendix](#changes-to-silvalue-api-for-sil-ownership).</div><div class=""><br class=""></div><div class=""># Values and ValueOwnershipKinds</div><div class=""><br class=""></div><div class="">Define `ValueOwnershipKind` as the enum with the following cases:</div><div class=""><br class=""></div><div class=""> enum class ValueOwnershipKind {</div><div class=""> Trivial,</div><div class=""> Unowned,</div><div class=""> Owned,</div><div class=""> Guaranteed,</div><div class=""> }</div><div class=""><br class=""></div><div class="">Our approach to mapping a `SILValue` to a `ValueOwnershipKind` is to use a</div><div class="">`SILVisitor` called `ValueOwnershipKindVisitor`. This works well since if one</div><div class="">holds `ValueKind` constant, `SILValue` have well defined ownership</div><div class="">constraints. Thus we can handle each case individually via the visitor. We use</div><div class="">SILNodes.def to ensure that all `ValueKind` have a defined visitor method. This</div><div class="">will ensure that when a new `ValueKind` is added, the compiler will emit a</div><div class="">warning that the visitor must be updated, ensuring correctness.</div><div class=""><br class=""></div><div class="">The visitor will be hidden in a *.cpp file and will expose its output via a new</div><div class="">API on `SILValue` :</div><div class=""><br class=""></div><div class=""> ValueOwnershipKind SILValue::getOwnershipKind() const;</div><div class=""><br class=""></div><div class="">Since the implementation of `SILValue::getOwnershipKind()` will be out of line,</div><div class="">none of the visitor code will be exposed to the rest of the compiler.</div><div class=""><br class=""></div><div class=""># ValueDefs and Ownership Constraints</div><div class=""><br class=""></div><div class="">In order to determine if a `SILInstruction`'s operands are SILValue that have</div><div class="">compatible ownership with a `SILInstruction`, we introduce a new API on</div><div class="">`SILInstruction` that returns the ownership constraint of the `i`th operand of</div><div class="">the `SILInstruction`:</div><div class=""><br class=""></div><div class=""> Optional<ValueOwnershipKind> SILInstruction::getOwnershipConstraint(unsigned i) const;</div><div class=""><br class=""></div><div class="">Specifically, it returns `.Some(OwnershipKind)` if there is a constraint or</div><div class="">`.None` if the `SILInstruction` will accept any `ValueOwnershipKind`</div><div class="">(e.g. `copy_value`). This API is sufficient since there are no `SILInstructions`</div><div class="">that accept only a subset of `ValueOwnershipKind`, all either accept a singular</div><div class="">ownership kind or all ownership kinds.</div><div class=""><br class=""></div><div class="">For `SILArgument`, we determine compatible ownership by introducing the concept</div><div class="">of ownership conventions. The reason to introduce these ownership conventions is</div><div class="">that it ensures that we do not need to perform any form of dataflow to determine</div><div class="">the convention of a `SILArgument` in a loop. Additionally, it allows for greater</div><div class="">readability in the IR and prevents the optimizer from performing implicit</div><div class="">conversions of ownership semantics on branch instructions, for instance,</div><div class="">converting a `switch_enum` from consuming a value at +1 to using a borrowed +0</div><div class="">parameter. In terms of API, we introduce a new method on `SILArgument`:</div><div class=""><br class=""></div><div class=""> ValueOwnershipKind SILArgument::getOwnershipConstraint() const;</div><div class=""><br class=""></div><div class="">which returns the required ownership constraint. In terms of representing these</div><div class="">ownership constraint conventions in textual SIL, we print out the ownership</div><div class="">constraint next to the specific argument in the block and the specific argument</div><div class="">in the given terminator. For details of how this will look with various</div><div class="">terminators, see the [appendix](#sil-argument-terminator-convention-examples).</div><div class=""><br class=""></div><div class=""># Verification of Ownership Semantics</div><div class=""><br class=""></div><div class="">Since our ownership model is based around SSA form, all verification of</div><div class="">ownership only need consider an individual value (`SILValue`) and the uses of</div><div class="">the def (`SILInstruction`, `SILArgument`). Thus for each def/use-set, we:</div><div class=""><br class=""></div><div class="">1. **Verify Use Semantics**: All uses must be compatible with the def's</div><div class=""> `ValueOwnershipKind`.</div><div class="">2. **Dataflow Verification**: Given any path P in the program and a `ValueDef`</div><div class=""> `V` along that path:</div><div class=""> a. There exists only one <a href="#footnote-0-lifetime-ending-use">"lifetime ending"</a> use of `V` along that path.</div><div class=""> b. After the lifetime ending use of `V`, there are no non-lifetime ending</div><div class=""> uses of `V` along `P`.</div><div class=""><br class=""></div><div class="">Since the dataflow verification requires knowledge of a subset of the uses, we</div><div class="">perform the use semantic verification first and then use the found uses for the</div><div class="">dataflow verification.</div><div class=""><br class=""></div><div class="">## Use Verification</div><div class=""><br class=""></div><div class="">Just like with `SILValue`, individual `SILInstruction` kind's have well-defined</div><div class="">ownership semantics implying that we can use a `SILVisitor` approach here as</div><div class="">well. Thus we define a `SILVisitor` called</div><div class="">`OwnershipCompatibilityUseChecker`. This checker works by taking in a `SILValue`</div><div class="">and visiting all of the `SILInstruction` users of the `SILValue`. Each visitor</div><div class="">method returns a pair of booleans, the first stating whether or not the</div><div class="">ownership values were compatible and the second stating whether or not this</div><div class="">specific use should be considered a "lifetime ending" use. The checker then</div><div class="">stores the lifetime ending uses and non-lifetime ending uses in two separate</div><div class="">arrays for processing by the dataflow verifier.</div><div class=""><br class=""></div><div class="">## Dataflow Verification</div><div class=""><br class=""></div><div class="">The dataflow verifier takes in as inputs the `SILValue` and lists of</div><div class="">lifetime-ending and non-lifetime ending uses. Since we are using SSA form, we</div><div class="">already know that our def must dominate all of our uses implying that a use can</div><div class="">never overconsume due to a def not being along a path. On the other hand, we</div><div class="">still must consider issues related to joint post-dominance namely:</div><div class=""><br class=""></div><div class="">1. Double-Consume due to 2+ lifetime ending uses along a path. This implies</div><div class=""> proving that no lifetime ending use is reachable from another lifetime ending</div><div class=""> use.</div><div class="">2. Use-After-Free due to a non-lifetime ending use not being joint-post</div><div class=""> dominated by the lifetime ending uses. This implies proving that all</div><div class=""> non-lifetime ending uses are joint post-dominated by the lifetime ending use</div><div class=""> set.</div><div class="">3. Lifetime-Leaks due to the non-lifetime ending uses not joint-post dominating</div><div class=""> the lifetime ending uses.</div><div class=""><br class=""></div><div class="">Note how we must consider joint post-dominance in two different places. Thus we</div><div class="">must be able to prove joint post-dominance quickly and cheaply. To do so, we</div><div class="">take advantage of dominance implying that all uses are reachable from the def to</div><div class="">just needing to prove that when we walk the CFG up to prove reachability, that</div><div class="">any block on the reachability path does not have any successors that have not</div><div class="">been visited when we finish walking and visit the def.</div><div class=""><br class=""></div><div class="">The full code is in the [appendix](#full-dataflow-verification-algorithm).</div><div class=""><br class=""></div><div class=""><a id="footnote-0-lifetime-ending-use">[0]</a>: A use after which a def is no</div><div class="">longer allowed to be used in any way, e.g. `destroy_value`, `end_borrow`.</div><div class=""><br class=""></div><div class=""># Appendix</div><div class=""><br class=""></div><div class="">## Changes to SILValue API for SIL Ownership</div><div class=""><br class=""></div><div class="">The common code pattern eliminated by removing implicit uses of `ValueDef`'s API</div><div class="">via a `SILValue` are as follows:</div><div class=""><br class=""></div><div class=""> SILValue V;</div><div class=""> ValueDef *Def;</div><div class=""><br class=""></div><div class=""> if (V != Def) { ... }</div><div class=""> if (V->getParentBlock()) { ... }</div><div class=""><br class=""></div><div class="">Our change, causes these code patterns to be rewritten in favor of the explicit:</div><div class=""><br class=""></div><div class=""> SILValue V;</div><div class=""> ValueDef *Def;</div><div class=""><br class=""></div><div class=""> if (V.getDef() != Def) { ... }</div><div class=""> if (V.getDef()->getParentBlock()) { ... }</div><div class=""><br class=""></div><div class="">In cases like the above, we want the to increase clarity through the usage of</div><div class="">verbosity. In other cases, this verboseness makes convenient APIs more difficult</div><div class="">to use. The main example here are the `isa` and `dyn_cast` APIs. We introduce</div><div class="">two helper functions that give the same convenience as before but added clarity by</div><div class="">making it clear that we are not performing an isa query on the value, but</div><div class="">instead the underlying def of the value:</div><div class=""><br class=""></div><div class=""> template <typename ParentTy></div><div class=""> bool def_isa(SILValue V) { return isa<ParentTy>(V.getDef()); }</div><div class=""> template <typename ParentTy></div><div class=""> ParentTy *def_dyn_cast(SILValue V) { return dyn_cast<ParentTy>(V.getDef()); }</div><div class=""><br class=""></div><div class="">Consider the following code using the old API,</div><div class=""><br class=""></div><div class=""> SILValue V;</div><div class=""><br class=""></div><div class=""> if (isa<ApplyInst>(V)) { ... }</div><div class=""> if (auto *PAI = dyn_cast<PartialApplyInst>(V)) { ... }</div><div class=""><br class=""></div><div class="">Notice how it seems like one is casting the SILValue as if it is a</div><div class="">ValueBase. This is due to the misleading usage of the implicit conversion from a</div><div class="">`SILValue` to the `SILValue`'s internal `ValueBase`. In comparison the new API</div><div class="">makes it absolutely clear that one is reasoning about the ValueKind of the</div><div class="">underlying def of the `SILValue`:</div><div class=""><br class=""></div><div class=""> SILValue V;</div><div class=""><br class=""></div><div class=""> if (def_isa<ApplyInst>(V)) { ... }</div><div class=""> if (auto *PAI = def_dyn_cast<PartialApplyInst>(V)) { ... }</div><div class=""><br class=""></div><div class="">Thus the convenience of the old API is maintained, clarity is improved, and the</div><div class="">conceptual API boundary is enforced.</div><div class=""><br class=""></div><div class="">The final change that we propose is eliminating the ability to construct a</div><div class="">`SILValue` from a `ValueDef` externally to the `ValueDef` itself. Allowing this</div><div class="">to occur violates the modeling notion that a `SILValue` is defined and thus is</div><div class="">dependent on the `ValueDef`. To implement this, we propose changing the</div><div class="">constructor `SILValue::SILValue(ValueDef *)` to have private instead of public</div><div class="">access control and declaring `ValueDef` subclasses as friends of</div><div class="">`SILValue`. This then allows the `ValueDef` to vend opaquely constructed</div><div class="">`SILValue`, but disallows external users of the API from directly creating</div><div class="">`SILValue` from `ValueDef`, enforcing the value/def distinction in our model.</div><div class=""><br class=""></div><div class="">## SILArgument/Terminator OwnershipConvention Examples</div><div class=""><br class=""></div><div class="">We present here several examples of how ownership conventions look on</div><div class="">SILArguments and terminators.</div><div class=""><br class=""></div><div class="">First we present a simple branch and return example.</div><div class=""><br class=""></div><div class=""> class C { ... }</div><div class=""><br class=""></div><div class=""> sil @simple_branching : $@convention(thin) : @convention(thin) (@owned Builtin.NativeObject, @guaranteed C) -> @owned C {</div><div class=""> bb0(%0 : @owned $Builtin.NativeObject, %1 : @guaranteed $C):</div><div class=""> br bb1(%0 : @owned $Builtin.NativeObject)</div><div class=""><br class=""></div><div class=""> bb1(%1 : @owned $Builtin.NativeObject):</div><div class=""> strong_release %1 : $Builtin.NativeObject</div><div class=""> %2 = copy_value %0 : $C</div><div class=""> return %2 : @owned $C</div><div class=""> }</div><div class=""><br class=""></div><div class="">Now consider this loop example:</div><div class=""><br class=""></div><div class=""> sil @loop : $@convention(thin) : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {</div><div class=""> bb0(%0 : @owned $Optional<Builtin.NativeObject>):</div><div class=""> br bb1(%0 : @owned $Builtin.NativeObject)</div><div class=""><br class=""></div><div class=""> bb1(%1 : @owned $Builtin.NativeObject):</div><div class=""> %2 = alloc_object $C</div><div class=""> strong_release %1 : $Builtin.NativeObject</div><div class=""> %3 = unchecked_ref_cast %2 : $C to $Builtin.NativeObject</div><div class=""> cond_br %cond, bb1(%3 : @owned Builtin.NativeObject), bb2</div><div class=""><br class=""></div><div class=""> bb2:</div><div class=""> strong_release %3 : $Builtin.NativeObject</div><div class=""> %result = tuple()</div><div class=""> return %result : @trivial $()</div><div class=""> }</div><div class=""><br class=""></div><div class="">Note how it is absolutely clear what convention is being used when passing a</div><div class="">value to the phi node. No dataflow reasoning is required implying we can do a</div><div class="">simple pass over the CFG to prove correctness.</div><div class=""><br class=""></div><div class="">Now consider two examples of switches:</div><div class=""><br class=""></div><div class=""> sil @owned_switch_enum : $@convention(thin) : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {</div><div class=""> bb0(%0 : @owned $Optional<Builtin.NativeObject>):</div><div class=""> switch_enum %0 : @owned $Builtin.NativeObject, #Optional.none.enumelt: bb1, #Optional.some.enumelt.1: bb2</div><div class=""><br class=""></div><div class=""> bb1:</div><div class=""> br bb3</div><div class=""><br class=""></div><div class=""> bb2(%1 : @owned $Builtin.NativeObject):</div><div class=""> strong_release %1 : $Builtin.NativeObject</div><div class=""> br bb3</div><div class=""><br class=""></div><div class=""> bb3:</div><div class=""> %result = tuple()</div><div class=""> return %result : @trivial $()</div><div class=""> }</div><div class=""><br class=""></div><div class=""> sil @guaranted_converted_switch_enum : $@convention(thin) : $@convention(thin) (@owned Optional<Builtin.NativeObject>) -> () {</div><div class=""> bb0(%0 : @owned $Optional<Builtin.NativeObject>):</div><div class=""> %1 = begin_borrow %0 : $Optional<Builtin.NativeObject></div><div class=""> switch_enum %1 : @guaranteed $Builtin.NativeObject, #Optional.none.enumelt: bb1, #Optional.some.enumelt.1: bb2</div><div class=""><br class=""></div><div class=""> bb1:</div><div class=""> br bb3</div><div class=""><br class=""></div><div class=""> bb2(%2 : @guaranteed $Builtin.NativeObject):</div><div class=""> %3 = function_ref @g_user : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()</div><div class=""> apply %3(%2) : $@convention(thin) (@guaranteed Builtin.NativeObject) -> ()</div><div class=""> br bb3</div><div class=""><br class=""></div><div class=""> bb3:</div><div class=""> end_borrow %1 from %0 : $Optional<Builtin.NativeObject>, $Optional<Builtin.NativeObject></div><div class=""> %result = tuple()</div><div class=""> return %result : @trivial $()</div><div class=""> }</div><div class=""><br class=""></div><div class="">Notice how the lifetime is completely explicit in both cases, so the optimizer</div><div class="">can not treat the conversion of switch_enum from +1 to +0 implicitly.</div><div class=""><br class=""></div><div class="">## Full Dataflow Verification Algorithm</div><div class=""><br class=""></div><div class="">Define the following book keeping data structures.</div><div class=""><br class=""></div><div class=""> // The worklist that we will use for our iterative reachability query.</div><div class=""> llvm::SmallVector<SILBasicBlock *, 32> Worklist;</div><div class=""><br class=""></div><div class=""> // The set of blocks with lifetime ending uses.</div><div class=""> llvm::SmallPtrSet<SILBasicBlock *, 8> BlocksWithLifetimeEndingUses;</div><div class=""><br class=""></div><div class=""> // The set of blocks with non-lifetime ending uses and the associated</div><div class=""> // non-lifetime ending use SILInstruction.</div><div class=""> llvm::SmallDenseMap<SILBasicBlock *, SILInstruction *, 8> BlocksWithNonLifetimeEndingUses;</div><div class=""><br class=""></div><div class=""> // The blocks that we have already visited.</div><div class=""> llvm::SmallPtrSet<SILBasicBlock *, 32> VisitedBlocks;</div><div class=""><br class=""></div><div class=""> // A list of successor blocks that we must visit by the time the algorithm terminates.</div><div class=""> llvm::SmallPtrSet<SILBasicBlock *, 8> SuccessorBlocksThatMustBeVisited;</div><div class=""><br class=""></div><div class="">Then for each non-lifetime ending use (found by the</div><div class="">`OwnershipCompatibilityUseChecker`), we add the block and its instruction to the</div><div class="">`BlocksWithNonLifetimeEndingUses`. There is a possibility of having multiple</div><div class="">non-lifetime ending uses in the same block, in such a case, we always take the</div><div class="">later value since we are performing a liveness-esque dataflow:</div><div class=""><br class=""></div><div class=""> for (SILInstruction *User : getNonLifetimeEndingUses()) {</div><div class=""> // First try to associate User with User->getParent().</div><div class=""> auto Result = BlocksWithNonLifetimeEndingUses.insert({User->getParent(), User});</div><div class=""><br class=""></div><div class=""> // If the insertion succeeds, then we know that there is no more work to</div><div class=""> // be done, so process the next use.</div><div class=""> if (Result.second)</div><div class=""> continue;</div><div class=""><br class=""></div><div class=""> // If the insertion fails, then we have at least two non-lifetime ending uses</div><div class=""> // in the same block. Since we are performing a liveness type of dataflow,</div><div class=""> // we only need the last non-lifetime ending use to show that all lifetime</div><div class=""> // ending uses post dominate both. Thus, see if Use is after</div><div class=""> // Result.first->second in the use list. If Use is not later, then we wish</div><div class=""> // to keep the already mapped value, not use, so continue.</div><div class=""> if (std::find(Result.first->second->getIterator(), Block->end(), User) ==</div><div class=""> Block->end()) {</div><div class=""> continue;</div><div class=""> }</div><div class=""><br class=""></div><div class=""> // At this point, we know that Use is later in the Block than</div><div class=""> // Result.first->second, so store Use instead.</div><div class=""> Result.first->second = User;</div><div class=""> }</div><div class=""><br class=""></div><div class="">Then we visit each each lifetime ending use and its parent block:</div><div class=""><br class=""></div><div class=""> for (SILInstruction *User : getLifetimeEndingUses()) {</div><div class=""> SILBasicBlock *UserParentBlock = User->getParent();</div><div class=""> ...</div><div class=""> }</div><div class=""><br class=""></div><div class="">We begin by adding `UserParentBlock` to the `BlocksWithLifetimeEndingUses`</div><div class="">set. If a block is already in the set (i.e. insert fails), then we know that (1)</div><div class="">has been violated and we error. If we never hit that condition, then we know</div><div class="">that all lifetime ending uses are in different blocks.</div><div class=""><br class=""></div><div class=""> if (!BlocksWithLifetimeEndingUses.insert(UserParentBlock).second) {</div><div class=""> double_consume_error(); // ERROR!</div><div class=""> }</div><div class=""><br class=""></div><div class="">Then we check if we previously saw any non-lifetime ending uses in</div><div class="">`UserParentBlock` by checking the map `BlocksWithNonLifetimeEndingUses`. If we do</div><div class="">find any such uses, we check if the lifetime ending use is earlier in the block</div><div class="">that the non-lifetime ending use. If so then (2) is violated and we</div><div class="">error. Once we know that (2) has not been violated, we remove</div><div class=""><br class=""></div><div class=""> auto Iter = BlocksWithNonLifetimeEndUses.find(UserParentBlock);</div><div class=""> if (Iter != BlocksWithNonLifetimeEndUses.end()) {</div><div class=""> // Make sure that the non-lifetime ending use is before the lifetime</div><div class=""> // ending use. Otherwise, we have a use after free.</div><div class=""> if (std::find(User->getIterator(), UserParentBlock->end(), Iter->second) !=</div><div class=""> UserParentBlock->end()) {</div><div class=""> use_after_free_error(); // ERROR!</div><div class=""> }</div><div class=""><br class=""></div><div class=""> // Erase the use since we know that it is properly joint post-dominated.</div><div class=""> BlocksWithNonLifetimeEndingUses.erase(Iter);</div><div class=""> }</div><div class=""><br class=""></div><div class="">Then we mark `UserParentBlock` as visited to ensure that we do not consider</div><div class="">UserParentBlock to be a successor we must visit and prime the worklist with the</div><div class="">predecessor blocks of `UserParentBlock`.</div><div class=""><br class=""></div><div class=""> // Then mark UserParentBlock as visited add all predecessors of</div><div class=""> // UserParentBlock to the worklist.</div><div class=""> VisitedBlocks.insert(UserParentBlock);</div><div class=""> copy(UserParentBlock->getPreds(), std::back_inserter(Worklist));</div><div class=""><br class=""></div><div class="">The entire block of code is provided in the appendix. Now we know that:</div><div class=""><br class=""></div><div class="">1. All lifetime ending uses are in different basic blocks.</div><div class="">2. All non-lifetime ending uses are either in different basic blocks.</div><div class=""><br class=""></div><div class="">We begin our worklist algorithm by popping off the next element in the worklist.</div><div class=""><br class=""></div><div class=""> // Until the worklist is empty.</div><div class=""> while (!Worklist.empty()) {</div><div class=""> // Grab the next block to visit.</div><div class=""> const SILBasicBlock *BB = Worklist.pop_back_val();</div><div class=""> ...</div><div class=""> }</div><div class=""><br class=""></div><div class="">Since every time we insert objects into the worklist, we first try to insert it</div><div class="">into the `VisitedBlock` list, we do not need to check if `BB` has been visited</div><div class="">yet, since elements can not be added to the worklist twice.</div><div class=""><br class=""></div><div class="">Then make sure that BB is not in `BlocksWithLifetimeEndingUses`. If BB is in</div><div class="">`BlocksWithLifetimeEndingUses`, then we know that there is a path going through</div><div class="">the def where the def is consumed twice, an error!</div><div class=""><br class=""></div><div class=""> if (BlocksWithLifetimeEndingUses.count(BB)) {</div><div class=""> double_consume_error(); // ERROR!</div><div class=""> }</div><div class=""><br class=""></div><div class="">Now that we know we are not double consuming, we need to update our data</div><div class="">structures. First if BB is contained in SuccessorBlocksThatMustBeVisited, we</div><div class="">remove it. This ensures when the algorithm terminates, we know that the path</div><div class="">through the successor was visited as apart of our walk.</div><div class=""><br class=""></div><div class=""> SuccessorBlocksThatMustBeVisited.erase(BB);</div><div class=""><br class=""></div><div class="">Then if BB is in BlocksWithNonLifetimeEndingUses, we remove it. This ensures</div><div class="">that when the algorithm terminates, we know that the non-lifetime ending uses</div><div class="">were properly joint post-dominated by the lifetime ending uses.</div><div class=""><br class=""></div><div class=""> BlocksWithNonLifetimeEndingUses.erase(BB);</div><div class=""><br class=""></div><div class="">Then add all successors of BB that we have not visited yet to the</div><div class="">`SuccessorBlocksThatMustBeVisited` set. This ensures that if we do not visit the</div><div class="">successor as apart of our CFG walk, at the end of the algorithm we will assert</div><div class="">that there is a leak.</div><div class=""><br class=""></div><div class=""> for (const SILBasicBlock *SuccBlock : BB->getSuccessorBlocks()) {</div><div class=""> // If we already visited the successor, there is nothing to do since</div><div class=""> // we already visited the successor.</div><div class=""> if (VisitedBlocks.count(SuccBlock))</div><div class=""> continue;</div><div class=""><br class=""></div><div class=""> // Otherwise, add the successor to our MustVisitBlocks set to ensure that</div><div class=""> // we assert if we do not visit it by the end of the algorithm.</div><div class=""> SuccessorBlocksThatMustBeVisited.insert(SuccBlock);</div><div class=""> }</div><div class=""><br class=""></div><div class="">Finally add all predecessors of BB that we have not visited yet to the Worklist</div><div class="">for processing. We use insert here to ensure that we only ever add a</div><div class="">VisitedBlock once to the Worklist:</div><div class=""><br class=""></div><div class=""> for (const SILBasicBlock *PredBlock : BB->getPredecessorBlocks()) {</div><div class=""> if (!VisitedBlocks.insert(PredBlock).second)</div><div class=""> continue;</div><div class=""> Worklist.push_back(PredBlock);</div><div class=""> }</div><div class=""><br class=""></div><div class="">This continues until we have exhausted the worklist. Once the worklist is</div><div class="">exhausted, we know that:</div><div class=""><br class=""></div><div class="">1. If `SuccessorBlocksThatMustBeVisited` is non-empty, then the Blocks in the</div><div class=""> set are not joint post-dominated by the set of lifetime ending users implying</div><div class=""> a leak.</div><div class="">2. If `BlockSwithNonLifetimeEndingUses` is non-empty, then there was a</div><div class=""> non-lifetime ending use that was not joint post-dominated by the lifetime</div><div class=""> ending use set. This implies a use-after free.</div><div class=""><br class=""></div><div class="">Thus we assert that both sets are empty and error accordingly.</div><div class=""><br class=""></div><div class=""> if (!SuccessorBlocksThatMustBeVisited.empty()) {</div><div class=""> leak_error(); // ERROR!</div><div class=""> }</div><div class=""> if (!BlocksWithNonLifetimeEndingUses.empty()) {</div><div class=""> use_after_free_error(); // ERROR!</div><div class=""> }</div><div class=""><br class=""></div><div class="">The full code:</div><div class=""><br class=""></div><div class=""> // The worklist that we will use for our iterative reachability query.</div><div class=""> llvm::SmallVector<SILBasicBlock *, 32> Worklist;</div><div class=""><br class=""></div><div class=""> // The set of blocks with lifetime ending uses.</div><div class=""> llvm::SmallPtrSet<SILBasicBlock *, 8> BlocksWithLifetimeEndingUses;</div><div class=""><br class=""></div><div class=""> // The set of blocks with non-lifetime ending uses and the associated</div><div class=""> // non-lifetime ending use SILInstruction.</div><div class=""> llvm::SmallDenseMap<SILBasicBlock *, SILInstruction *, 8> BlocksWithNonLifetimeEndingUses;</div><div class=""><br class=""></div><div class=""> // The blocks that we have already visited.</div><div class=""> llvm::SmallPtrSet<SILBasicBlock *, 32> VisitedBlocks;</div><div class=""><br class=""></div><div class=""> // A list of successor blocks that we must visit by the time the algorithm terminates.</div><div class=""> llvm::SmallPtrSet<SILBasicBlock *, 8> SuccessorBlocksThatMustBeVisited;</div><div class=""><br class=""></div><div class=""> for (SILInstruction *User : getLifetimeEndingUses()) {</div><div class=""> SILBasicBlock *UserParentBlock = User->getParent();</div><div class=""> if (!BlocksWithLifetimeEndingUses.insert(UserParentBlock).second) {</div><div class=""> double_consume_error(); // ERROR!</div><div class=""> }</div><div class=""><br class=""></div><div class=""> auto Iter = BlocksWithNonLifetimeEndUses.find(UserParentBlock);</div><div class=""> if (Iter != BlocksWithNonLifetimeEndUses.end()) {</div><div class=""> // TODO: Could this be cached.</div><div class=""> if (std::find(User->getIterator(), UserParentBlock->end(), Iter->second) !=</div><div class=""> UserParentBlock->end()) {</div><div class=""> use_after_free_error(); // ERROR!</div><div class=""> }</div><div class=""> }</div><div class=""><br class=""></div><div class=""> // Then add all predecessors of the user block to the worklist.</div><div class=""> VisitedBlocks.insert(UserParentBlock);</div><div class=""> copy(UserParentBlock->getPreds(), std::back_inserter(Worklist));</div><div class=""> }</div><div class=""><br class=""></div><div class=""> // Until the worklist is empty.</div><div class=""> while (!Worklist.empty()) {</div><div class=""> // Grab the next block to visit.</div><div class=""> const SILBasicBlock *BB = Worklist.pop_back_val();</div><div class=""><br class=""></div><div class=""> // Then check that BB is not a lifetime-ending use block. If it is error,</div><div class=""> // since we have an overconsume.</div><div class=""> if (BlocksWithLifetimeEndingUses.count(BB)) {</div><div class=""> double_consume_error(); // ERROR!</div><div class=""> }</div><div class=""><br class=""></div><div class=""> // Ok, now we know that we are not double-consuming. Update our data</div><div class=""> // structures.</div><div class=""><br class=""></div><div class=""> // First remove BB from the SuccessorBlocksThatMustBeVisited list. This</div><div class=""> // ensures that when the algorithm terminates, we know that BB was not the</div><div class=""> // beginning of a non-covered path to the exit.</div><div class=""> SuccessorBlocksThatMustBeVisited.erase(BB);</div><div class=""><br class=""></div><div class=""> // Then remove BB from BlocksWithNonLifetimeEndingUses so we know that</div><div class=""> // this block was properly joint post-dominated by our lifetime ending</div><div class=""> // users.</div><div class=""> BlocksWithNonLifetimeEndingUses.erase(BB);</div><div class=""><br class=""></div><div class=""> // Then add all successors of BB that we have not visited yet to the</div><div class=""> // SuccessorBlocksThatMustBeVisited set.</div><div class=""> for (const SILBasicBlock *SuccBlock : BB->getSuccessorBlocks()) {</div><div class=""> // If we already visited the successor, there is nothing to do since</div><div class=""> // we already visited the successor.</div><div class=""> if (VisitedBlocks.count(SuccBlock))</div><div class=""> continue;</div><div class=""><br class=""></div><div class=""> // Otherwise, add the successor to our MustVisitBlocks set to ensure that</div><div class=""> // we assert if we do not visit it by the end of the algorithm.</div><div class=""> SuccessorBlocksThatMustBeVisited.insert(SuccBlock);</div><div class=""> }</div><div class=""><br class=""></div><div class=""> // Finally add all predecessors of BB that have not been visited yet to</div><div class=""> // the worklist.</div><div class=""> for (const SILBasicBlock *PredBlock : BB->getPredecessorBlocks()) {</div><div class=""> // Try to insert the PredBlock into the VisitedBlocks list to ensure</div><div class=""> // that we only ever add a block once to the worklist.</div><div class=""> if (!VisitedBlocks.insert(PredBlock).second)</div><div class=""> continue;</div><div class=""> Worklist.push_back(PredBlock);</div><div class=""> }</div><div class=""> }</div><div class=""><br class=""></div><div class=""> if (!SuccessorBlocksThatMustBeVisited.empty()) {</div><div class=""> leak_error(); // ERROR!</div><div class=""> }</div><div class=""> if (!BlocksWithNonLifetimeEndingUses.empty()) {</div><div class=""> use_after_free_error(); // ERROR!</div><div class=""> }</div></div><div class=""><br class=""></div><div class="">----</div><br class=""><div class=""><blockquote type="cite" class=""><div class="">On Dec 5, 2016, at 6:47 PM, Michael Gottesman <<a href="mailto:mgottesman@apple.com" class="">mgottesman@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><br class="Apple-interchange-newline">On Dec 5, 2016, at 5:26 PM, Andrew Trick <<a href="mailto:atrick@apple.com" class="">atrick@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><br class=""><div class=""><blockquote type="cite" class=""><div class="">On Dec 5, 2016, at 3:55 PM, Michael Gottesman <<a href="mailto:mgottesman@apple.com" class="">mgottesman@apple.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Hello everyone.<div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">It is online here:</div><div class=""><br class=""></div><div class=""><a href="https://gottesmm.github.io/proposals/sil-ownership-model.html" class="">https://gottesmm.github.io/proposals/sil-ownership-model.html</a></div><div class=""><br class=""></div><div class="">Michael</div></div></div></blockquote></div><div class=""><br class=""></div>Thanks! It looks good.<div class=""><br class=""><div class=""><div class="">> `ValueDef` is not a value, but the def of a value.</div><div class=""><br class=""></div><div class="">Should be "but may define (or produce) values.".</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">Sure.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div><div class="">> Since our ownership model is based around SSA form</div><div class=""><br class=""></div><div class="">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.</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">Ok.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div><div class="">> This checker works by taking in a</div><div class="">`ValueDef` and visiting all of the `SILInstruction` users of the</div><div class="">`ValueDef`.</div><div class=""><br class=""></div><div class="">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.</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">That is a typo. If you look earlier I was using explicitly SILValue.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div><div class="">> The dataflow verifier takes in as inputs the `ValueDef` (i.e. def) and lists of lifetime-ending and non-lifetime ending uses.</div><div class=""><br class=""></div><div class="">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.</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">That is a typo from an earlier version of the algorithm. Everything should be about the SILValue.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div><div class="">> if (V.getDef()->getParentBlock()) { ... }</div><div class=""><br class=""></div><div class="">I see no reason we can't add getParentBlock() and other very common idioms to the SILValue API.</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">The question is how much should we make that a def only API.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div><div class="">> if (auto *PAI = def_dyn_cast<PartialApplyInst>(V)) { ... }</div><div class=""><br class=""></div><div class="">It's not obvious to be that this is more readable than </div><div class=""><br class=""></div><div class="">if (auto *PAI = dyn_cast<PartialApplyInst>(V.getDef())) { ... }</div><div class=""><br class=""></div><div class="">But I don't have a strong opinion on it.</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">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.</div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div><div class="">> The final change that we propose is eliminating the ability to construct a</div><div class="">`SILValue` from a `ValueDef` externally to the `ValueDef` itself.</div><div class=""><br class=""></div><div class="">Nice!</div><div class=""><br class=""></div><div class="">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.</div></div></div></div></div></blockquote><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">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.</div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">Let me fix this real quick.</div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">Michael</div><div class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><br class=""></div><blockquote type="cite" class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div class=""><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div class=""><div class=""><div class=""><br class=""></div></div><div class="">-Andy</div></div></div></div></blockquote></div></blockquote></div><br class=""></div></div><br class=""></div>_______________________________________________<br class="">swift-dev mailing list<br class=""><a href="mailto:swift-dev@swift.org" class="">swift-dev@swift.org</a><br class=""><a href="https://lists.swift.org/mailman/listinfo/swift-dev" class="">https://lists.swift.org/mailman/listinfo/swift-dev</a><br class=""></div></blockquote></div><br class="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">_______________________________________________</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">swift-dev mailing list</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="mailto:swift-dev@swift.org" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">swift-dev@swift.org</a><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="https://lists.swift.org/mailman/listinfo/swift-dev" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">https://lists.swift.org/mailman/listinfo/swift-dev</a></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""></div></div></blockquote></div><br class=""></body></html>