The verifier just invokes this method, so we aren't losing any verification in
the SILVerifier itself.
The reason why I am extracting this information into a helper is that often
times one hits these structural assertions in the verifier making one have to
track down where in a pass the bad location was actually inserted. To make these
easier to find, I am going to change the SILBuilder to invoke these structural
comparisons so that we can catch these problems at the call site making it
easier to fix code.
And rename MemoryDataflow -> BitDataflow.
MemoryLifetime contained MemoryLocations, MemoryDataflow and the MemoryLifetimeVerifier.
Three independent things, for which it makes sense to have them in three separated files.
NFC.
This updates how we model reborrow's lifetimes for ownership verification.
Today we follow and combine a borrow's lifetime through phi args as well.
Owned values lifetimes end at a phi arg. This discrepency in modeling
lifetimes leads to the OwnershipVerifier raising errors incorrectly for
cases such as this, where the borrow and the base value do not dominate
the end_borrow:
bb0:
cond_br undef, bb1, bb2
bb1:
%copy0 = copy_value %0
%borrow0 = begin_borrow %copy0
br bb3(%borrow0, %copy0)
bb2:
%copy1 = copy_value %1
%borrow1 = begin_borrow %copy1
br bb3(%borrow1, %copy1)
bb3(%borrow, %baseVal):
end_borrow %borrow
destroy_value %baseVal
This PR adds a new ReborrowVerifier. The ownership verifier collects borrow's
lifetime ending users and populates the worklist of the ReborrowVerifier
with reborrows and the corresponding base value.
ReborrowVerifier then verifies that the lifetime of the reborrow is
within the lifetime of the base value.
Limit names to a straightforward and unambiguous statement of
purpose. They should not pose additional questions which can only be
answered by reading the code. Nuanced meaning belongs in descriptions
and code comments.
These are all examples that legitimately made reading the code very
difficult for me:
- LoadBorrowInvalidationChecker: what does "invalidation" mean in this
context? How does that extend the meaning of "checker"? How can
something ever pass a checker and not be invalid?
- constructValuesForKey outside of an ADT does not state purpose at all.
- wellBehavedWriteAccumulator: Raises questions about what writes are
included and the broader semantics of the parent function. It turns
out that well-behavedness is handled by the function's return value
and has nothing to do with the accumulator.
This simplifies the handling of the subdirectories in the SIL and
SILOptimizer paths. Create individual libraries as object libraries
which allows the analysis of the source changes to be limited in scope.
Because these are object libraries, this has 0 overhead compared to the
previous implementation. However, string operations over the filenames
are avoided. The cost for this is that any new sub-library needs to be
added into the list rather than added with the special local function.
This verifier validates that while a load_borrow's value is live (that is until
it is invalidated by its end_borrow), the load_borrow's address source is never
written to.
The reason why this verifier is especially important now is that I am adding
many optimizations that convert `load [copy]` -> `load_borrow`. If that
optimization messes up, we break this invariant [in fact, an optimization I am
working on right now violated the invariant =--(]. So by adding this verifier I
am checking that semantic arc opts doesn't break it as well as eliminating any
other such bugs from the compiler (in the future).
Specifically, I split it into 3 initial categories: IR, Utils, Verifier. I just
did this quickly, we can always split it more later if we want.
I followed the model that we use in SILOptimizer: ./lib/SIL/CMakeLists.txt vends
a macro (sil_register_sources) to the sub-folders that register the sources of
the subdirectory with a global state variable that ./lib/SIL/CMakeLists.txt
defines. Then after including those subdirs, the parent cmake declares the SIL
library. So the output is the same, but we have the flexibility of having
subdirectories to categorize source files.
