From 0b571a8ed03f58d9fdd9fd71085a80e541e01e3a Mon Sep 17 00:00:00 2001 From: vsadov Date: Mon, 6 Nov 2017 15:59:02 -0800 Subject: [PATCH 1/4] Extension of IL verification rules to address readonly references --- proposed/verifiable-ref-readonly.md | 111 ++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 proposed/verifiable-ref-readonly.md diff --git a/proposed/verifiable-ref-readonly.md b/proposed/verifiable-ref-readonly.md new file mode 100644 index 000000000..217105b9d --- /dev/null +++ b/proposed/verifiable-ref-readonly.md @@ -0,0 +1,111 @@ +# Readonly references 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` + - 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, readonly managed pointers can be used: +- as operands of `RET` instruction only if containing method returns _readonly_ references +- as an operand of `LDFLD`, `LDIND`, `LDOBJ` and a 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 `in` parameters (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` + +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. + From 96d397187124cfb4f609948318744da30c386738 Mon Sep 17 00:00:00 2001 From: vsadov Date: Thu, 9 Nov 2017 14:24:07 -0800 Subject: [PATCH 2/4] Corrected stack merging rule. --- proposed/verifiable-ref-readonly.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proposed/verifiable-ref-readonly.md b/proposed/verifiable-ref-readonly.md index 217105b9d..346df05e1 100644 --- a/proposed/verifiable-ref-readonly.md +++ b/proposed/verifiable-ref-readonly.md @@ -59,7 +59,7 @@ Readonly managed pointer may be a result of one of the following: ## 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. +Merging a readonly managed pointer with an managed pointer of an ordinary or controlled mutability kind results in a readonly managed pointer. ## Readonly local slots ## CLI needs to add a notion of a readonly local slots. From 35d475b7cb928023862364c558b6e07f069a0612 Mon Sep 17 00:00:00 2001 From: vsadov Date: Fri, 17 Nov 2017 18:19:41 -0800 Subject: [PATCH 3/4] modreqs for returns and parameters of virtual/abstract/invoke methods --- proposed/verifiable-ref-readonly.md | 36 ++++++++++++++++++----------- 1 file changed, 22 insertions(+), 14 deletions(-) diff --git a/proposed/verifiable-ref-readonly.md b/proposed/verifiable-ref-readonly.md index 346df05e1..94b3e6870 100644 --- a/proposed/verifiable-ref-readonly.md +++ b/proposed/verifiable-ref-readonly.md @@ -79,8 +79,20 @@ Byref local slots can be marked as readonly by applying `modopt[System.Runtime.C ## `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 addition, the result signature of such methods (and only those methods) must have `modreq[System.Runtime.CompilerServices.IsReadOnlyAttribute]`. + +**Motivation**: this is to ensure that existing compilers cannot simply ignore `readonly` when invoking methods with `ref readonly` returns + ## `in` parameters ## When `System.Runtime.CompilerServices.IsReadOnlyAttribute` is applied to a byref parameter, it means that the the parameter is an `in` parameter. + +In addition, if the method is *abstract* or *virtual*, then the signature of such parameters (and only such parameters) must have `modreq[System.Runtime.CompilerServices.IsReadOnlyAttribute]`. + +**Motivation**: this is done to ensure that in a case of method overriding/implementing the `in` parameters match. + +Same requirements apply to `Invoke` methods in delegates. + +**Motivation**: this is to ensure that existing compilers cannot simply ignore `readonly` when creating or assigning delegates. ## `readonly` structs ## When `System.Runtime.CompilerServices.IsReadOnlyAttribute` is applied to a value type, it means that the the type is a `readonly struct`. @@ -91,21 +103,17 @@ In particular: - 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. - +NOTE: 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. +**Delegate and method signature compatibility:** +*(need to adjust definitions of “delegate-assignable-to” and “method-signature-compatible- +with” accordingly)* +Signatures that differ in terms of `readonly` are not compatible. + +NOTE: The modifiers on parameters and returns are ignored here. That is existing behavior and it is not changed to allow delegate creation regardless of whether target method is virtual and uses modifiers or not. + +NOTE: The requirement could be relaxed to allow readonly references be compatible with ordinary references in return position and reverse in parameter positions, if more complex rules can be justified. + \ No newline at end of file From 34dc33925a0a464dbb44d88faedf16a519f424c5 Mon Sep 17 00:00:00 2001 From: vsadov Date: Fri, 17 Nov 2017 18:38:46 -0800 Subject: [PATCH 4/4] corrected a chapter title --- proposed/verifiable-ref-readonly.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/proposed/verifiable-ref-readonly.md b/proposed/verifiable-ref-readonly.md index 94b3e6870..4dabb4ccb 100644 --- a/proposed/verifiable-ref-readonly.md +++ b/proposed/verifiable-ref-readonly.md @@ -105,9 +105,7 @@ In particular: --- NOTE: 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 # - -**Delegate and method signature compatibility:** +# Delegate and method signature compatibility ## *(need to adjust definitions of “delegate-assignable-to” and “method-signature-compatible- with” accordingly)*