Extension of IL verification rules to address ref returns

[VSadov]

A proposal for extension of IL verification rules that would allow byref returns in verifiable code and validate that they are used in type-safe manner.

---

Motivation -

There seems to be enough interest in making typesafe code emitted by current compilers formally verifiable, so we need a central location where we discuss and agree on the rules.

The other areas that would need to be addressed are: readonly references (type-safe code may not be verifiable according to current rules) and ref-structs (opposite: current rules are insufficient to detect type-safety violations).

However, we need to start with something, so let’s start with ref returns.

Immediately actionable pieces:

• Who should be on board when we take decision on this?
• Do we agree on the overall proposal?

[MichalStrehovsky]

Is there a particular reason to use an Attribute suffix here? This will serve similar purpose as System.Runtime.CompilerServices.IsVolatile or IsConst. Those are not attributes either.

[VSadov]

No, no reason to be an attribute.

In the parallel case with readonly references, it seems appropriate to use IsReadOnlyAttribute since that is used in other places to express readonliness.
I could not think of a similar existing type for "returnable", so I suggest IsReturnableAttribute just for similarity, but you are right - it does not need to be an attribute or even a new type.

Any alternative ideas here would be appreciated, but we need to pick some type.

[MichalStrehovsky]

Should this also apply to CALLI?

[VSadov]

The rule could include CALLI for completeness. However CALLI cannot be present in verifiable code so generalization would not make much difference.

[MichalStrehovsky]

However CALLI cannot be present in verifiable code

Why not? ECMA-335 defines verification rules for when CALLI is verifiable. It's not like JMP (whose verification rules are simply "The jmp instruction is never verifiable").

[VSadov]

Is it? Perhaps I think of it as unverifiable because it invariably involves pointers.
Anyways, no problem with including it.

[VSadov]

I think, I should mention varargs/arglist case as well.

C# compiler does consider them for the purpose of "any ref argument can potentially come back as a ref return"

[VSadov]

Merging this, since this has been opened for a long time, and informally approved by interested parties.

NOTE: The proposal does not have direct impact on the language, but has effect on the compiler.
It codifies the metadata shape which has direct impact on interop/verification scenarios.
(that is why it fits in csharplang repo)

[MichalStrehovsky]

@VSadov Based on your own comments "I think, I should mention varargs/arglist case as well.", the question around verification of CALLI, and not giving this Attribute suffix (that can lead someone to believe they can apply this as an attribute on somethings), I thought this is not fully fleshed out yet...

[VSadov]

@MichalStrehovsky - will make the update regarding CALLI, I thought I did...

As for the type to mark returnable local slots - any good ideas?

Ideally that would be a preexisting type that exists everywhere - like IsConst or even System.Object, but there is a danger that it is already used by somebody to modopt locals.

[MichalStrehovsky]

As for the type to mark returnable local slots - any good ideas?

I think we need a new type (IsConst is only available starting NetStandard 1.3 and I can't think of anything existing that wouldn't be confusing). I would be fine with System.Runtime.CompilerServices.IsReturnable. If we would like to eventually make it part of the framework so that the compiler doesn't need to always emit it, we might want to run it through a CoreFX API review. (This is the part where making this a custom attribute would be weird because users might think they can apply it to things and something will happen as a result.)