Improved treatment of final fields #3495

mattulbrich · 2024-07-06T14:57:09Z

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-final fields
T::final(Object, Field)  // for final 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

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

The following new items showed up:

Deal with prettyprinting of final fields using select. Currently o.f is the prettyprinting for both accesses.
Deal with parsing of final fields in JavaDL. o.f means something different now ...
static final fields are a challenge since they need double special treatment in parsing and prettyprinting

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 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.

manually replaying fd0fa6f

manually replaying 428ebfd

manually replaying 252fc9f

manually replaying 5552b59

manually replaying 6397702

manually replayed 94437c0

manually replaying 1ebb594

wadoon · 2024-07-06T19:27:03Z

Is #3189 now obsolete?

Interestingly, final is not so final on bytecode level.

mattulbrich · 2024-07-06T19:47:17Z

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.

... revert to heap updates in such cases.

thanks to Richard for hinting at the needed infrastructure

mattulbrich · 2024-12-10T11:38:33Z

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.

codecov · 2024-12-20T21:54:42Z

Codecov Report

Attention: Patch coverage is 59.53079% with 138 lines in your changes missing coverage. Please review.

Project coverage is 38.54%. Comparing base (c2e5da7) to head (e995740).
Report is 24 commits behind head on main.

Files with missing lines	Patch %	Lines
...src/main/java/de/uka/ilkd/key/pp/FinalPrinter.java	30.68%	54 Missing and 7 partials ⚠️
...a/ilkd/key/proof/init/FinalFieldCodeValidator.java	61.95%	20 Missing and 15 partials ⚠️
...kd/key/java/declaration/VariableSpecification.java	45.45%	6 Missing and 6 partials ⚠️
...ka/ilkd/key/proof/init/FinalFieldsPOExtension.java	76.66%	2 Missing and 5 partials ⚠️
.../de/uka/ilkd/key/speclang/njml/JmlTermFactory.java	0.00%	5 Missing ⚠️
...c/main/java/de/uka/ilkd/key/logic/TermBuilder.java	42.85%	2 Missing and 2 partials ⚠️
.../java/de/uka/ilkd/key/ldt/FinalHeapResolution.java	78.57%	2 Missing and 1 partial ⚠️
...e/uka/ilkd/key/rule/UseDependencyContractRule.java	0.00%	3 Missing ⚠️
...ka/ilkd/key/nparser/builder/ExpressionBuilder.java	60.00%	1 Missing and 1 partial ⚠️
...src/main/java/de/uka/ilkd/key/pp/FieldPrinter.java	89.47%	1 Missing and 1 partial ⚠️
... and 4 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3495      +/-   ##
============================================
+ Coverage     38.39%   38.54%   +0.15%     
- Complexity    17238    17345     +107     
============================================
  Files          2099     2103       +4     
  Lines        127342   127642     +300     
  Branches      21446    21495      +49     
============================================
+ Hits          48891    49202     +311     
+ Misses        72440    72376      -64     
- Partials       6011     6064      +53

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

it was not wrong before but not confluent. Failed the case vstte10_05_Queue/AmortizedQueue_AmortizedQueue.key

mattulbrich · 2025-02-23T19:49:21Z

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

WolframPfeifer

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!

WolframPfeifer · 2025-02-27T14:15:02Z

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key

@@ -232,6 +232,24 @@
        noRestriction
    };

+    /*!


I noticed that this documentation is not shown when looking at the taclet settings in the option dialog. Apparently there is an xml file, where basically the same documentation is present. We really should unify this. But I don't want to block this, and prefer a new PR instead ...

WolframPfeifer · 2025-02-27T14:29:15Z

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key

+        \heuristics(simplify_enlarging)
+    };
+
+    referencedObjectIsCreatedRighFinalEQ {


small typo:

Suggested change

referencedObjectIsCreatedRighFinalEQ {

referencedObjectIsCreatedRightFinalEQ {

WolframPfeifer · 2025-02-27T14:44:53Z

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java

+        // We know this holds because of isPOSupported:
+        FunctionalOperationContractPO fpo = (FunctionalOperationContractPO) abstractPO;
+        IProgramMethod iconstructor = fpo.getProgramMethod();
+        assert iconstructor instanceof ProgramMethod : "Contracts cannot have schema ";


I don't understand the message of the assertion here.

WolframPfeifer · 2025-02-27T15:00:28Z

key.core/src/main/java/de/uka/ilkd/key/pp/FieldPrinter.java

+    protected static boolean isJavaFieldConstant(Term fieldTerm, HeapLDT heapLDT,
+            Services services) {
+        try {
+            getJavaFieldConstant(fieldTerm, heapLDT, services);


I think the code here is correct, but really looks a bit weird (calling a getter, ignoring the result, and then returning true).

WolframPfeifer · 2025-02-27T15:08:20Z

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java

+     * Constructor calls must not leak 'this' to the called constructor.
+     */
+    private void validateConstructorReference(ConstructorReference methodReference) {
+        // TODO We have to make sure that on non-static subclass is instantiated here


Open TODO? Honestly I don't understand it ...

WolframPfeifer · 2025-02-27T15:18:42Z

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java

@@ -1566,6 +1567,26 @@ public void translateSetStatement(final SetStatement statement, final IProgramMe
            new SpecificationRepository.JmlStatementSpec(pv, ImmutableList.of(assignee, value)));
    }

+    /**


Am I correct that this means that the feature works for ghost fields in exactly the same way as for Java fields (that is another edge case I did not think of so far)?

WolframPfeifer · 2025-02-27T15:26:52Z

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key

@@ -22,6 +22,9 @@
    // default value for a field
    alpha alpha::defaultValue;

+    // reading from final attributes (corr. to select for non-final fields)


I don't understand what you mean by that comment. What do you mean by "correct" here? What happens if you have a non-final field f and a for example the term int::final(o, f)? I would suppose that you can not resolve it further, but it is clearly a term that could occur in the sequent ...

WolframPfeifer · 2025-02-27T15:30:00Z

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key

+
+        // Without that created-check, it is not consistent.
+        \assumes(wellFormed(h),
+                 boolean::select(h, o, java.lang.Object::<created>) = TRUE ==>)


I just thought about whether we could model java.lang.Object::<created> itself as a final field ...

WolframPfeifer · 2025-02-27T15:36:12Z

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key

@@ -3632,10 +3805,11 @@
        \displayname "active_attribute_access"
    };

+    // TODO 2 variants with different taclet options


key.core/src/test/java/de/uka/ilkd/key/pp/FinalPrinterTest.java

mattulbrich added 7 commits July 6, 2024 14:55

introducing infrastructure for final values w/o select.

4c36ba7

manually replaying fd0fa6f

adding taclets for wellformedness of final fields

11539db

manually replaying 428ebfd

soundness bugfix for final values

8ebaa61

manually replaying 252fc9f

introducing a taclet option for the new final field mechanism

d4f7ec0

manually replaying 5552b59

more general way to respect taclet options for final fields

79a50da

manually replaying 6397702

adapt rule for new syntax

bbafd0f

manually replayed 94437c0

Add pretty printing for final fields

d928eb0

manually replaying 1ebb594

mattulbrich self-assigned this Jul 6, 2024

set statements may also assign to final fields

82e1aad

... revert to heap updates in such cases.

mattulbrich marked this pull request as draft July 6, 2024 21:33

mattulbrich added 5 commits July 7, 2024 17:01

spotlessing ...

44d8634

Merge remote-tracking branch 'origin/main' into newFinalHeaps

80c9112

towards final heaps with static analysis

ea6e9ca

final field code validator and tests

e46b239

thanks to Richard for hinting at the needed infrastructure

cleaning up towards PR

9bae13f

mattulbrich force-pushed the newFinalHeaps branch from 9fb4182 to 9bae13f Compare December 10, 2024 10:58

mattulbrich added 2 commits December 10, 2024 12:35

documentation, towards PR

0c991b0

spotlessing

ae9ea9b

mattulbrich mentioned this pull request Dec 10, 2024

Logical Infrastructure for final values independent from the heap #3189

Closed

4 tasks

mattulbrich added 8 commits December 10, 2024 14:57

mostly fixing the prettyprinting and parsing problem

c647495

test cases for pp and parsing, mainly wrt. final fields

aa749dd

repairing failing test cases

c3a28ef

more automation for finals in constructors

3af8775

repairing test cases

7c81700

Merge remote-tracking branch 'origin/main' into newFinalHeaps

491cfca

# Conflicts: # key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt

Merge remote-tracking branch 'origin/main' into newFinalHeaps

f88dd46

adding two rules for final fields.

dad8aca

a final field reference in a created object points to null or to a created object.

applying spotless

d99efd2

making non-final fields in interfaces possible

da84fda

mattulbrich force-pushed the newFinalHeaps branch from 08b0083 to da84fda Compare December 21, 2024 00:26

mattulbrich added 2 commits January 20, 2025 19:37

changing one rule for final fields

3e8fbbd

it was not wrong before but not confluent. Failed the case vstte10_05_Queue/AmortizedQueue_AmortizedQueue.key

enabling static final fields

27f1584

mattulbrich force-pushed the newFinalHeaps branch from 2ccdb0f to 27f1584 Compare January 20, 2025 23:20

mattulbrich force-pushed the newFinalHeaps branch from 8db48a8 to 022ce5a Compare February 22, 2025 13:33

make information flow examples use traditional final treatment.

e921c72

mattulbrich force-pushed the newFinalHeaps branch from 022ce5a to e921c72 Compare February 22, 2025 14:27

mattulbrich added 2 commits February 23, 2025 16:30

Merge remote-tracking branch 'origin/main' into newFinalHeaps

e137c77

cleaning up code for upcoming review.

2f599d3

mattulbrich requested review from WolframPfeifer and wadoon and removed request for WolframPfeifer February 23, 2025 19:50

mattulbrich marked this pull request as ready for review February 23, 2025 22:26

mattulbrich added the Review Request Waiting for review label Feb 23, 2025

wadoon approved these changes Feb 25, 2025

View reviewed changes

key.core/src/test/java/de/uka/ilkd/key/pp/FinalPrinterTest.java Show resolved Hide resolved

taking static final fields into account for createdness proofs.

e995740

WolframPfeifer requested changes Feb 27, 2025

View reviewed changes

WolframPfeifer mentioned this pull request Feb 27, 2025

Documentation for Treatment of Final Fields KeYProject/key-docs#44

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improved treatment of final fields #3495

Improved treatment of final fields #3495

mattulbrich commented Jul 6, 2024 •

edited

Loading

wadoon commented Jul 6, 2024

mattulbrich commented Jul 6, 2024

mattulbrich commented Dec 10, 2024

codecov bot commented Dec 20, 2024 •

edited

Loading

mattulbrich commented Feb 23, 2025

WolframPfeifer left a comment

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

WolframPfeifer Feb 27, 2025

	referencedObjectIsCreatedRighFinalEQ {
	referencedObjectIsCreatedRightFinalEQ {

Improved treatment of final fields #3495

Are you sure you want to change the base?

Improved treatment of final fields #3495

Conversation

mattulbrich commented Jul 6, 2024 • edited Loading

Intended Change

Plan

Type of pull request

Ensuring quality

Additional information and contact(s)

wadoon commented Jul 6, 2024

mattulbrich commented Jul 6, 2024

mattulbrich commented Dec 10, 2024

codecov bot commented Dec 20, 2024 • edited Loading

Codecov Report

mattulbrich commented Feb 23, 2025

WolframPfeifer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mattulbrich commented Jul 6, 2024 •

edited

Loading

codecov bot commented Dec 20, 2024 •

edited

Loading