Improved treatment of final fields

mattulbrich commented 3 months ago

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

T::select(Heap, Object, Field)   // for non-static fields
T::final(Object, Field)  // for static fields

The major challenges include

adapting reading of final fields in modalities
adapting accessing final fields in JML
handling constructors: they are allowed to write.

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

[x] Add functions for finals, add a taclet option
[x] Implement rules that act upon those taclet options
[ ] Implement special treatment for constructors
[ ] Test effectiveness
[ ] Code cleanup
[ ] Document the changes

Type of pull request

Breaking change (feature that cause existing functionality to change)

The plan is to have a taclet otion to fall back to old behaviour.

Ensuring quality

To do:

I made sure that introduced/changed code is well documented (javadoc and inline comments).
I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
I added new test case(s) for new functionality.
I have tested the feature as follows: ...
I have checked that runtime performance has not deteriorated.

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.

wadoon commented 3 months ago

Is #3189 now obsolete?

Interestingly, final is not so final on bytecode level.

mattulbrich commented 3 months ago

Is #3189 now obsolete?

This is the commits from back then merged onto the modern main.

Interestingly, final is not so final on bytecode level.

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.

KeYProject / key