Original title was "JmlFormalParameter should have a single
notion of nullity". In fact the ISU tools should support a
single notion of nullity.
Support for nullable and non-null is not appropriately
implemented. E.g. the AST is being altered to accommodate
the new non_null_by_default instead of representing nullity
inside other semantic objects (e.g. CType).
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
I was hoping to be able to add support for non-null types in
MJ by adding a node to the CType hierarchy that would
represent a qualified type (a la C++). Unfortunately this
would entail too many changes in the compiler. Hence, I
will effectively be attaching a nullity attribute to
declarations instead (unfortunately this will undoubtedly
make it more challenging to support array types with
non-null elements). Rather than add a new attribute I am
making use of the modifiers class. In order to distinguish
between a declaration being explicitly vs. implicitly
declared non-null I have added a IMPLICITLY_NON_NULL flag
(see further below for details).
The following classes have been updated to support testing
and setting of nullity:
- The JML nullity ACC_ flags have been moved to MJ.
- The top 16 bits (out of 64) have been marked as "internal"
flags -- i.e. those not corresponding to elements of the
language syntax.
- Defined an internal flag named IMPLICITLY_NON_NULL.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
In directory org/multijava/mjc:
CClassType:
- removed field and methods related to non-null (since we
cannot introduce the notion of nullity for types).
JFieldDeclaration:
JLocalVariable:
- added isNonNull() and setNonNull().
JMemberDeclaration:
- added specs stating that export can be null.
- guarded call to getMethod() by test for nullity of the
field named "export" (this was a bug - it occurred in the
context of RAC code generation for a class with an
implicitly added default constructor).
JMethodDeclaration:
- added isNonNull() and setNonNull().
- guarded internal call to overriddenMethodSet() by a test
for the nullity (this was a bug).
MemberAccess:
- added addModifiers().
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Note that in the case of class or interface methods (and
their parameters), the nullity checks and adjustments (done
by checkNullityAdjustType()) are done in checkInterface()
which is invoked prior to typecheck(). This ensures that by
the time we reach typecheck, we have already set the nullity
qualifier of the return and parameter types of all supertype
methods that a given method might happen to override.
In directory org/jmlspecs/checker:
Constants.java:
- moved nullity modifiers to MJ Constants.
JMLWarningFilter:
- add cautions PARAMETER_NULLABLE_IN_SUPE and
METHOD_NON_NULL_IN_SUPER (so that they will be ignored by
the racrun tests during its compilation phase).
Jml.g:
- Removed all code that used to manipulate nullity modifiers
based on class or system defaults.
- jParameterDeclaration: now making use of long modifiers
and the standard jModifiers because this is standard, and
must cleaner. Note that jModifiers handles complaining
about non-standard ordering.
- Minor reformatting in jmlModifier.
JmlFieldDeclaration.java:
- Removed code that altered modifiers based on class or
system level nullity defaults.
- Added setNonNull().
- Refactored typeckeck, distributing parts of the body into
private methods.
- Nullity checks and type adjustments are being done by new
method checkNullityAdjustType().
JmlFormalParameter.java:
- Changed the constructor to make use of a modifiers
argument (hence we can uniformly deal with the nullity
modifiers).
- Added overriding checkInterface().
- Removed isNull() and isNonNull(). To test the nullity
modifiers use the usual hasFlag().
- Changed modifierAsString() to make use of compiler modUtil.
JmlMemberAccess.java:
- Removed isNullable(). To test the nullity modifiers use
the usual hasFlag(). To test if a member is meant to be
non-null, either implicitly or explicitly use hasFlag with
ACC_NON_NULL | ACC_NULLABLE.
- Added checks of the appropriate use of nullity modifiers
in checkClassModifiers, checkFieldModifiers,
checkInterfaceFieldModifiers, checkMethodModifiers,
checkInterfaceMethodModifiers.
- Adjusted invalid*Modifiers fields.
JmlMemberDeclaration.java:
- Removed checking of nullity modifiers (since we can not do
any useful test by looking at the AST modifier flags alone).
JmlMessages.msg:
- Updated various message because they mentioned non_null
but not nullable.
- Added INVALID_PARAM_MODIFIER (since we no longer restrict
formal parameter modifiers via the grammar).
JmlMethodDeclaration.java:
- Added checkNullityAdjustType(), ... which is called by
checkInterface().
- Added isNonNull(), and setNonNull().
- Refactored typecheck by putting logical code chunks into
private methods.
JmlMethodSpecification.java:
- Added nullable modifier to specCases().
JmlTypeDeclaration.java:
- Removed code that did checks based on nullity modifiers
based on modifiers bit masks.
- I think that the method combineParameterModifiers() is
unnecessary since we require that parameters of refined
methods match exactly w.r.t. nullity. Rather than remove the
code I am simply double checking that parameter nullity
matches (and throw an exception if they do not). If the
exception never gets thrown, then remove the method.
JmlVariableDefinition.java:
- Updated javadoc to say that this class is used for bound
variables in addition to local variables.
- Moved nullity checking code into checkNullityAdjustType().
TestJmlParser.java:
- Adjustments due to the changes to JmlFormalParameter.
- Adjustment to an expected error message (since it is now
the default mj error message that is reported when parameter
modifiers are out of order).
NonNullStatistics.java:
- Only essential changes induced by those in the other
classes (did not really test the stats feature yet).
In directory org/jmlspecs/jmlrac:
PostconditionMethod.java:
- Update due to change in signature to JmlFormalParameter().
RacPrettyPrinter.java:
- In visitJmlFormalParameter(), replace if's by a singel
call to modifiersAsString().
TransInvariant.java:
- In the translate() method: checking if fields are declared
non-null (either implicitly or explicitly).
TransMethod.java:
- Support for nullity modifiers as per latest semantics.
In directory org/jmlspecs/jmlrac/testcase/racrun:
* Added new tests: NonNullConstructorExp.java,
NonNullMethodExp.java, NullableConstructorExp.java,
NullableMethodExp.java. These files are also used to
generate "duals" - see GENERATED_TESTS in Makefile.
* Added new tests: NullityAndInheritance.java,
NullityAndInheritance2.java.
Makefile:
- Added and/or adjusted rules for new GENERATED_TESTS.
In directory org/jmlspecs/checker/testcase/typecheck:
In directory org/jmlspecs/jmldoc/testcase/expected-141:
In directory org/jmlspecs/jmldoc/testcase/expected-142:
- Necessary updates to expected output.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Logged In: YES
user_id=176206
Original title was "JmlFormalParameter should have a single
notion of nullity". In fact the ISU tools should support a
single notion of nullity.
Support for nullable and non-null is not appropriately
implemented. E.g. the AST is being altered to accommodate
the new non_null_by_default instead of representing nullity
inside other semantic objects (e.g. CType).
Logged In: YES
user_id=176206
I was hoping to be able to add support for non-null types in
MJ by adding a node to the CType hierarchy that would
represent a qualified type (a la C++). Unfortunately this
would entail too many changes in the compiler. Hence, I
will effectively be attaching a nullity attribute to
declarations instead (unfortunately this will undoubtedly
make it more challenging to support array types with
non-null elements). Rather than add a new attribute I am
making use of the modifiers class. In order to distinguish
between a declaration being explicitly vs. implicitly
declared non-null I have added a IMPLICITLY_NON_NULL flag
(see further below for details).
The following classes have been updated to support testing
and setting of nullity:
- JFieldDeclaration (MJ)
- JLocalVariable (MJ) - also covers formal parameters.
- JMethodDeclaration (MJ).
Change to the ACC_* flags:
- The JML nullity ACC_ flags have been moved to MJ.
- The top 16 bits (out of 64) have been marked as "internal"
flags -- i.e. those not corresponding to elements of the
language syntax.
- Defined an internal flag named IMPLICITLY_NON_NULL.
Logged In: YES
user_id=176206
Summary of commit to MJ on 2006-02-10:
In directory org/multijava/mjc:
CClassType:
- removed field and methods related to non-null (since we
cannot introduce the notion of nullity for types).
CMember:
- added addModifiers and isNonNull().
CModifier:
- added stripInternalMods().
CType:
- removed method related to non-null.
Constants:
- added non-null ACC_* flags (from JML).
JFieldDeclaration:
JLocalVariable:
- added isNonNull() and setNonNull().
JMemberDeclaration:
- added specs stating that export can be null.
- guarded call to getMethod() by test for nullity of the
field named "export" (this was a bug - it occurred in the
context of RAC code generation for a class with an
implicitly added default constructor).
JMethodDeclaration:
- added isNonNull() and setNonNull().
- guarded internal call to overriddenMethodSet() by a test
for the nullity (this was a bug).
MemberAccess:
- added addModifiers().
Logged In: YES
user_id=176206
Summary of commit to JML2 on 2006-02-10:
Note that in the case of class or interface methods (and
their parameters), the nullity checks and adjustments (done
by checkNullityAdjustType()) are done in checkInterface()
which is invoked prior to typecheck(). This ensures that by
the time we reach typecheck, we have already set the nullity
qualifier of the return and parameter types of all supertype
methods that a given method might happen to override.
In directory org/jmlspecs/checker:
Constants.java:
- moved nullity modifiers to MJ Constants.
JMLWarningFilter:
- add cautions PARAMETER_NULLABLE_IN_SUPE and
METHOD_NON_NULL_IN_SUPER (so that they will be ignored by
the racrun tests during its compilation phase).
Jml.g:
- Removed all code that used to manipulate nullity modifiers
based on class or system defaults.
- jParameterDeclaration: now making use of long modifiers
and the standard jModifiers because this is standard, and
must cleaner. Note that jModifiers handles complaining
about non-standard ordering.
- Minor reformatting in jmlModifier.
JmlFieldDeclaration.java:
- Removed code that altered modifiers based on class or
system level nullity defaults.
- Added setNonNull().
- Refactored typeckeck, distributing parts of the body into
private methods.
- Nullity checks and type adjustments are being done by new
method checkNullityAdjustType().
JmlFormalParameter.java:
- Changed the constructor to make use of a modifiers
argument (hence we can uniformly deal with the nullity
modifiers).
- Added overriding checkInterface().
- Removed isNull() and isNonNull(). To test the nullity
modifiers use the usual hasFlag().
- Changed modifierAsString() to make use of compiler modUtil.
JmlMemberAccess.java:
- Removed isNullable(). To test the nullity modifiers use
the usual hasFlag(). To test if a member is meant to be
non-null, either implicitly or explicitly use hasFlag with
ACC_NON_NULL | ACC_NULLABLE.
- Added checks of the appropriate use of nullity modifiers
in checkClassModifiers, checkFieldModifiers,
checkInterfaceFieldModifiers, checkMethodModifiers,
checkInterfaceMethodModifiers.
- Adjusted invalid*Modifiers fields.
JmlMemberDeclaration.java:
- Removed checking of nullity modifiers (since we can not do
any useful test by looking at the AST modifier flags alone).
JmlMessages.msg:
- Updated various message because they mentioned non_null
but not nullable.
- Added INVALID_PARAM_MODIFIER (since we no longer restrict
formal parameter modifiers via the grammar).
JmlMethodDeclaration.java:
- Added checkNullityAdjustType(), ... which is called by
checkInterface().
- Added isNonNull(), and setNonNull().
- Refactored typecheck by putting logical code chunks into
private methods.
JmlMethodSpecification.java:
- Added nullable modifier to specCases().
JmlTypeDeclaration.java:
- Removed code that did checks based on nullity modifiers
based on modifiers bit masks.
- I think that the method combineParameterModifiers() is
unnecessary since we require that parameters of refined
methods match exactly w.r.t. nullity. Rather than remove the
code I am simply double checking that parameter nullity
matches (and throw an exception if they do not). If the
exception never gets thrown, then remove the method.
JmlVariableDefinition.java:
- Updated javadoc to say that this class is used for bound
variables in addition to local variables.
- Moved nullity checking code into checkNullityAdjustType().
TestJmlParser.java:
- Adjustments due to the changes to JmlFormalParameter.
- Adjustment to an expected error message (since it is now
the default mj error message that is reported when parameter
modifiers are out of order).
NonNullStatistics.java:
- Only essential changes induced by those in the other
classes (did not really test the stats feature yet).
In directory org/jmlspecs/jmlrac:
PostconditionMethod.java:
- Update due to change in signature to JmlFormalParameter().
RacPrettyPrinter.java:
- In visitJmlFormalParameter(), replace if's by a singel
call to modifiersAsString().
TransInvariant.java:
- In the translate() method: checking if fields are declared
non-null (either implicitly or explicitly).
TransMethod.java:
- Support for nullity modifiers as per latest semantics.
In directory org/jmlspecs/jmlrac/testcase/racrun:
* Added new tests: NonNullConstructorExp.java,
NonNullMethodExp.java, NullableConstructorExp.java,
NullableMethodExp.java. These files are also used to
generate "duals" - see GENERATED_TESTS in Makefile.
* Added new tests: NullityAndInheritance.java,
NullityAndInheritance2.java.
Makefile:
- Added and/or adjusted rules for new GENERATED_TESTS.
In directory org/jmlspecs/checker/testcase/typecheck:
In directory org/jmlspecs/jmldoc/testcase/expected-141:
In directory org/jmlspecs/jmldoc/testcase/expected-142:
- Necessary updates to expected output.