Extension of IL verification rules to address readonly references

proposed/verifiable-ref-readonly.md

@@ -0,0 +1,111 @@
+# Ref returns in C# and IL verification. #
+
+The goal of this document is to specify additional IL verification rules that would allow C# code that utilizes readonly references to be formally verifiable.  
+
+NOTE: the rules for `readonly` are completely independent and additive to the rules for ref returning members. 
+
+## C# rules for reference: ##
+
+1)	readonly variables cannot be passed or returned by ordinary reference or used in initialization of an ordinary ref local. 
+2)	readonly variables:
+	- `readonly` fields when used outside of corresponding constructor.
+	- fields of `readonly` value-typed variables. 
+	- `in` parameters.
+	- `ref readonly` returning members.
+	- `ref` ternary expression when either of the branches is a readonly variable.
+	- `this` inside a member of a `readonly` struct other than the instance constructor.
+3)	readonly variables can be passed or returned by _readonly_ reference or used in initialization of a _readonly_ ref local. 
+4) Additional special cases where use of a variable is considered readonly: 
+  (mostly affects codegeneration, does not have direct effect on semantics of the language):
+	- receiver of an instance member of a `readonly` struct
+	- receiver of a value type member that is inherited from a base class (`Enum`, `ValueType`, `Object`...)
+	- receiver of an instance member of `Nullable<T>`
+	- Controlled-mutability references that are obtained via unboxing or array indexing with `readonly.` prefix can be used as readonly references.
+
+NOTE: C# rules operate with high level language entities such as scopes, expressions, local variables, etc., that do not exist at the level of IL or do not map one-to-one.
+The following is the attempt to introduce/adjust verification rules to allow validation of the safety of the readonly references at IL level.
+
+# Verification of readonly references. #
+
+## Readonly managed pointer. ##
+
+CLI needs to add a notion of another transient type - readonly managed pointer. 
+*(need to adjust “III.1.8.1.1 Verification algorithm” and in “I.8.7 Assignment compatibility” accordingly)*
+
+NOTE: there are similarities with already existing concept of controlled mutability managed references, however `readonly` is a stronger property than controlled mutability. I.E. a controlled mutability reference is accepted anywhere where readonly reference could be used, but not the other way around.
+
+`readonly references` ⊂ `controlled mutability references` ⊂ `ordinary references`
+
+Readonly managed pointer is a transient type used for verification purposes. When certain conditions are met, managed pointers can be classified as readonly. 
+
+Unlike other managed pointer types, returnable managed pointers can be used:
+- as operands of `RET` instruction only if containing method is _readonly_
+- as an operand of `LDFLD`, `LDIND`, `LDOBJ` and source operand of `CPOBJ` 
+- as an operand of `LDFLDA` - the resulting pointer is considered _readonly_
+- as operands of a method call if corresponding parameter is _readonly_
+
+Parameters of a `CALL` or `CALLVIRT` instruction are considered readonly when they are
+- annotated as such (see metadata encoding)
+- `this` parameters of `readonly` struct members (see metadata encoding)   
+- `this` parameters of struct members inherited from base types
+- `this` parameters of a member of `Nullable<T>`
+
+Readonly managed pointer may be a result of one of the following:
+-	`LDSFLDA`, `LDFLDA` when field is readonly 
+-	`LDARG` of an `in` parameter, 
+     note: arg0 inside an instance member other than .ctor of a readonly struct is considered an `in` parameter.
+-	`CALL`, `CALLVIRT` when the method returns a readonly reference
+
+## Merging stack states ## 
+*(add to III.1.8.1.3 Merging stack states)*
+
+Merging a readonly managed pointer with an managed pointer of an ordinary or controlled mutability kind results in a managed pointer of that kind.
+
+## Readonly local slots ##
+CLI needs to add a notion of a readonly local slots.
+-   a local byref slot may be marked as readonly. 
+-	`STLOC` of a _readonly_ managed pointer is verifiable only when the target is a readonly slot. 
+-	`LDLOC` from a readonly slot produces a readonly managed pointer.
+
+The rationale for introducing readonly locals is to allow for a single pass verification analysis. 
+While, in theory, it may be possible that the “readonly” property could be inferred via some form of fixed point flow analysis, it would make verification substantially more complex and expensive and would not retain the single-pass property.
+
+
+# Metadata encoding # 
+
+## `ref readonly` local slots ##
+Byref local slots can be marked as readonly by applying `modopt[System.Runtime.CompilerServices.IsReadOnlyAttribute]` in the local signature.
+
+## `ref readonly` returns ##
+When `System.Runtime.CompilerServices.IsReadOnlyAttribute` is applied to the return of a byref returning method, it means that the method returns a readonly reference.
+
+## `in` parameters ##
+When `System.Runtime.CompilerServices.IsReadOnlyAttribute` is applied to a byref parameter, it means that the the parameter is an `in` parameter.
+
+## `readonly` structs ##
+When `System.Runtime.CompilerServices.IsReadOnlyAttribute` is applied to a value type, it means that the the type is a `readonly struct`.
+
+
+In particular:
+-  The identity of the `IsReadOnlyAttribute` type is unimportant. In fact it can be embedded by the compiler in the containing assembly if needed.
+-  Applying `IsReadOnlyAttribute` to targets not listed here - to byval local slots, byval returns/parameters, reference types, etc... is reserved for the future use and in scope of this proposal results in verification errors. 
+
+---
+NOTE: while JIT is free to ignore readonly annotations. However it may use that extra information as an input/hints when performing optimizations.
+
+
+# Matching readonly constraints when overriding/implementing or assigning delegate values # 
+
+**Overriding:**
+In a case of overriding, the overriding method must match the signature of the overriden method in terms of `readonly` decorations. I.E. 
+- if a parameter of the overriden method is an `in` parameter, then the corresponding parameter of the overriding method must be `in` as well. The reverse match is also required.
+- if the overriden method returns by a readonly reference, then the overriding method must return by a readonly reference. The reverse match is also required.
+
+**Implementing:**
+In a case of implementing, the implementing method must match the signature of the implemented method in terms of `readonly` decorations. I.E. 
+- if a parameter of the implemented method is an `in` parameter, then the corresponding parameter of the implementing method must be `in` as well. The reverse match is also required.
+- if the implemented method returns by a readonly reference, then the implementing method must return by a readonly reference. The reverse match is also required.
+
+**Delegate assignments:**
+Delegates with signatures that differ in terms of `readonly` are not assignment compatible.
+