swift
8fd75eac - [no-implicit-copy] Make sure to error on copies on borrowed structural sub-values.

Commit
3 years ago
[no-implicit-copy] Make sure to error on copies on borrowed structural sub-values. Example: consume(x.field). This turned out to be a pretty simple extension of the underlying model. The cases we are interested in are caused by a non-reference nominal type having an extracted field being passed to a consuming use. This always requires a copy. The reason I missed this was I originally wrote the test cases around this for classes which do not have this problem since the class is move only, not the field due to class being a reference type. I then cargo culted this test case for struct/other types and did not notice that we should have started to error on these tests. On an interesting note, I caught this on my branch where I am preparing the optimizer to allow for values to have a move only bit. One of the constraints is that once we are in guaranteed SIL, copy_value can not be used on any moveOnly type (e.x.: $@moveOnly T). To ensure this doesn't happen, the move only checker: 1. Uses copy propagation to rewrite the copies of the base owned value. 2. Emit a diagnostic error upon any copies we found were needed due to the owned value being consumed. 3. If a diagnostic was emitted, rewrite all copies of move only typed values to be explicit_copy_value to ensure that in canonical SIL we do not violate the invariant that copy_value can not be applied to move only type values. This is ok to do since we are going to error and just want to avoid breaking the invariant. The end effect of this is that if we do not emit any diagnostic, any copy_value on a move only typed value that is not eliminated by the checker hits an assert in the verifier... allowing us to know that if a program successfully compiles that all "move only" proofs successfully ran, guaranteeing safety!
Author
Committer
Parents
Loading