-
Notifications
You must be signed in to change notification settings - Fork 29
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Improved treatment of final fields #3495
base: main
Are you sure you want to change the base?
Conversation
Is #3189 now obsolete? Interestingly, |
This is the commits from back then merged onto the modern main.
There are a few source code level things that get lost on byte code. Also generics. Sometimes private fields are not so private in byte code. We operate on source code level and assume that all code is compiler-conformant. |
... revert to heap updates in such cases.
thanks to Richard for hinting at the needed infrastructure
9fb4182
to
9bae13f
Compare
The last commits add sound special treatment for constructors. |
# Conflicts: # key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt
a final field reference in a created object points to null or to a created object.
08b0083
to
da84fda
Compare
it was not wrong before but not confluent. Failed the case vstte10_05_Queue/AmortizedQueue_AmortizedQueue.key
2ccdb0f
to
27f1584
Compare
8db48a8
to
022ce5a
Compare
022ce5a
to
e921c72
Compare
Regarding the effectiveness: Julian has shown that the IPSO case study heavily relied on the feature. Regarding the efficiency: The mean time per rule application is .74 ms compared to .76 ms on the current master. No regression observed. |
key.core/src/test/java/de/uka/ilkd/key/pp/FinalPrinterTest.java
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice feature, while reviewing it everything worked as expected. I have a few minor questions/remarks that should be resolved, but overall I think it is very well written and also nicely documented in code. Thanks!
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key
Show resolved
Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java
Outdated
Show resolved
Hide resolved
key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
Show resolved
Hide resolved
key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key
Outdated
Show resolved
Hide resolved
key.core/src/test/java/de/uka/ilkd/key/pp/FinalPrinterTest.java
Outdated
Show resolved
Hide resolved
57c514b
to
437803f
Compare
437803f
to
9bb8e45
Compare
Intended Change
Final fields cannot change their value after a single assignment in the constructor. In the current KeY logic, final fields are treated like normal fields stored on the heap. This is highly inefficient since heap assignments cannot have an impact on final fields at all.
The plan is hence to access final fields using a function of their own that does not depend on the heap, unlike other fields
The major challenges include
Writing must somehow be restricted since any modality could write to final fields and thus compromise proofs if thus different inconsistent values for final fields are around on a sequent.
Plan
The following new items showed up:
static final
fields are a challenge since they need double special treatment in parsing and prettyprintingType of pull request
The plan is to have a taclet otion to fall back to old behaviour.
Ensuring quality
To do:
Additional information and contact(s)
It is the modernised version of #3189.
@WolframPfeifer @wadoon
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.