[
https://issues.apache.org/jira/browse/GROOVY-12477?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Paul King updated GROOVY-12477:
-------------------------------
Description:
h3. Problem
There is no working way to declare that a method modifies nothing with
{{@Modifies}}. The forms a user would reach for are either rejected or silently
treated as if the method had no {{@Modifies}} at all.
With {{@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')}} on a
method whose body is {{balance -= n}}:
||Form||Result||
|{{@Modifies(\{ this.other })}}|Error: {{'balance' is not declared in
@Modifies}} (correct)|
|{{@Modifies(\{ [] })}}|*Compiles; nothing is checked*|
|{{@Modifies(\{})}}|Error: {{@Modifies closure must contain a field reference,
parameter reference, or list of references}}|
|{{@Modifies}}|*Compiles; nothing is checked*|
{code:groovy}
import groovy.contracts.Modifies
import groovy.transform.TypeChecked
@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')
class Account {
int balance
@Modifies({ [] })
void withdraw(int n) { balance -= n } // expected: error, actual: compiles
}
{code}
h3. Cause
* {{ModifiesASTTransformation}} stores the {{groovy.contracts.modifiesFields}}
metadata only when the set is non-empty. An empty list therefore leaves no
metadata. {{ModifiesChecker}} reads missing metadata as "no {{@Modifies}},
nothing to check". {{ModifiesEnsuresValidationTransformation}} returns early on
an empty set too, so {{old.x}} in an {{@Ensures}} is not validated either.
* An empty closure body is rejected because exactly one statement is required.
* {{Modifies.value()}} has no default, so a bare {{@Modifies}} should be a
missing-member error. The transform replaces {{value}} with {{Object.class}}
unconditionally, which hides the missing member.
The intent that "nothing" be expressible is already in the docs and the
checker. The type checkers guide says {{@Pure}}, {{@SideEffectFree}} and
{{@Contract(pure = true)}} each imply {{@Modifies({})}}, and
{{ModifiesChecker}} substitutes an empty frame for them. A user cannot write
that form themselves.
h3. Proposed fix
* {{@Modifies({})}} and {{@Modifies(\{ [] })}} both declare an empty frame: the
method modifies no fields or parameters. The metadata is always stored, even
when empty, so an empty frame is distinguishable from no annotation.
* A bare {{@Modifies}} is a compile error. A frame condition is a claim the
checker enforces, so "modifies nothing" should be explicit rather than inferred
from a marker that could equally be read as "modifies something unspecified".
* With an empty frame, {{@Ensures}} may not reference {{old.<field>}},
consistent with the existing rule that {{old}} may only reference fields
declared in {{@Modifies}}.
* The contracts user guide states the empty-frame form.
Both modules are {{@Incubating}}, so the tightening is low cost. The only
existing code that changes behaviour is code using {{@Modifies(\{ [] })}} or a
bare {{@Modifies}} and relying on it being unchecked.
was:
h3. Problem
There is no working way to declare that a method modifies nothing with
{{@Modifies}}. The forms a user would reach for are either rejected or silently
treated as if the method had no {{@Modifies}} at all.
With {{@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')}} on a
method whose body is {{balance -= n}}:
||Form||Result||
|{{@Modifies(\{ this.other })}}|Error: {{'balance' is not declared in
@Modifies}} (correct)|
|{{@Modifies(\{ [] })}}|*Compiles; nothing is checked*|
|{{@Modifies(\{})}}|Error: {{@Modifies closure must contain a field reference,
parameter reference, or list of references}}|
|{{@Modifies}}|*Compiles; nothing is checked*|
{code:groovy}
import groovy.contracts.Modifies
import groovy.transform.TypeChecked
@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')
class Account {
int balance
@Modifies({ [] })
void withdraw(int n) { balance -= n } // expected: error, actual: compiles
}
{code}
h3. Cause
* {{ModifiesASTTransformation}} stores the {{groovy.contracts.modifiesFields}}
metadata only when the set is non-empty. An empty list therefore leaves no
metadata. {{ModifiesChecker}} reads missing metadata as "no {{@Modifies}},
nothing to check". {{ModifiesEnsuresValidationTransformation}} returns early on
an empty set too, so {{old.x}} in an {{@Ensures}} is not validated either.
* An empty closure body is rejected because exactly one statement is required.
* {{Modifies.value()}} has no default, so a bare {{@Modifies}} should be a
missing-member error. The transform replaces {{value}} with {{Object.class}}
unconditionally, which hides the missing member.
The intent that "nothing" be expressible is already in the docs and the
checker. The type checkers guide says {{@Pure}}, {{@SideEffectFree}} and
{{@Contract(pure = true)}} each imply {{@Modifies({})}}, and
{{ModifiesChecker}} substitutes an empty frame for them. A user cannot write
that form themselves.
h3. Proposed fix
* {{@Modifies({})}} and {{@Modifies(\{ [] })}} both declare an empty frame: the
method modifies no fields or parameters. The metadata is always stored, even
when empty, so an empty frame is distinguishable from no annotation.
* A bare {{@Modifies}} is a compile error. A frame condition is a claim the
checker enforces, so "modifies nothing" should be explicit rather than inferred
from a marker that could equally be read as "modifies something unspecified".
* With an empty frame, {{@Ensures}} may not reference {{old.<field>}},
consistent with the existing rule that {{old}} may only reference fields
declared in {{@Modifies}}.
* The contracts user guide states the empty-frame form.
Both modules are {{@Incubating}}, so the tightening is low cost. The only
existing code that changes behaviour is code using {{@Modifies({ [] })}} or a
bare {{@Modifies}} and relying on it being unchecked.
> @Modifies with an empty or no list isn't working correctly
> ----------------------------------------------------------
>
> Key: GROOVY-12477
> URL: https://issues.apache.org/jira/browse/GROOVY-12477
> Project: Groovy
> Issue Type: Bug
> Components: groovy-contracts, groovy-typecheckers
> Reporter: Paul King
> Assignee: Paul King
> Priority: Minor
>
> h3. Problem
> There is no working way to declare that a method modifies nothing with
> {{@Modifies}}. The forms a user would reach for are either rejected or
> silently treated as if the method had no {{@Modifies}} at all.
> With {{@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')}} on
> a method whose body is {{balance -= n}}:
> ||Form||Result||
> |{{@Modifies(\{ this.other })}}|Error: {{'balance' is not declared in
> @Modifies}} (correct)|
> |{{@Modifies(\{ [] })}}|*Compiles; nothing is checked*|
> |{{@Modifies(\{})}}|Error: {{@Modifies closure must contain a field
> reference, parameter reference, or list of references}}|
> |{{@Modifies}}|*Compiles; nothing is checked*|
> {code:groovy}
> import groovy.contracts.Modifies
> import groovy.transform.TypeChecked
> @TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')
> class Account {
> int balance
> @Modifies({ [] })
> void withdraw(int n) { balance -= n } // expected: error, actual:
> compiles
> }
> {code}
> h3. Cause
> * {{ModifiesASTTransformation}} stores the
> {{groovy.contracts.modifiesFields}} metadata only when the set is non-empty.
> An empty list therefore leaves no metadata. {{ModifiesChecker}} reads missing
> metadata as "no {{@Modifies}}, nothing to check".
> {{ModifiesEnsuresValidationTransformation}} returns early on an empty set
> too, so {{old.x}} in an {{@Ensures}} is not validated either.
> * An empty closure body is rejected because exactly one statement is required.
> * {{Modifies.value()}} has no default, so a bare {{@Modifies}} should be a
> missing-member error. The transform replaces {{value}} with {{Object.class}}
> unconditionally, which hides the missing member.
> The intent that "nothing" be expressible is already in the docs and the
> checker. The type checkers guide says {{@Pure}}, {{@SideEffectFree}} and
> {{@Contract(pure = true)}} each imply {{@Modifies({})}}, and
> {{ModifiesChecker}} substitutes an empty frame for them. A user cannot write
> that form themselves.
> h3. Proposed fix
> * {{@Modifies({})}} and {{@Modifies(\{ [] })}} both declare an empty frame:
> the method modifies no fields or parameters. The metadata is always stored,
> even when empty, so an empty frame is distinguishable from no annotation.
> * A bare {{@Modifies}} is a compile error. A frame condition is a claim the
> checker enforces, so "modifies nothing" should be explicit rather than
> inferred from a marker that could equally be read as "modifies something
> unspecified".
> * With an empty frame, {{@Ensures}} may not reference {{old.<field>}},
> consistent with the existing rule that {{old}} may only reference fields
> declared in {{@Modifies}}.
> * The contracts user guide states the empty-frame form.
> Both modules are {{@Incubating}}, so the tightening is low cost. The only
> existing code that changes behaviour is code using {{@Modifies(\{ [] })}} or
> a bare {{@Modifies}} and relying on it being unchecked.
--
This message was sent by Atlassian Jira
(v10.3.26#10030026)
