Immutable and valid JML set statement

[wadoon]

Version of #3195 but with an immutable Java AST.

This PR implements JML set-statement in a non-Java-like fashion (no reduction to copy assignment) preserving the semantics of Java.

Translation of JML goes directly from JML to KeY terms lazily inside the built-in rule SetStatementRule.

TODO

• Cleanup
• Program variable replacement has still an issue. There are duplicated program variable objects that represent the same variable in the program and have the same name.

Type of pull request

• X Bug fix (non-breaking change which fixes an issue)
• X Refactoring (behaviour should not change or only minimally change)
• X New feature (non-breaking change which adds functionality)
• X Breaking change (fix or feature that would cause existing functionality to change)
• X There are changes to the (Java) code
• X There are changes to the built-in rule base

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments)

[mattulbrich]

This version verifies the following program:

class A {

    //@ ensures true;
    void m() {
        
        //@ ghost \bigint x = 0;

        int i = 0;
        while(i < 2) {
            //@ ghost \bigint y = 1;
            //@ set x = x + y;
            i++;
        }
        //@ assert x == 0;
        // but should be x == 2;
    }
}

which is not correct at all. The problem is that in every loop iteration y becomes a different symbol. However, in x+y the y remains always the original variable and is not updated to the respective instances. That is the reason why in assumptions and assertions the copy is kept and actually modified (breaking immutability).

[mattulbrich]

Even simpler: The following can be proved:

    void m() {
        //@ ghost \bigint x = 0;
        //@ set x = x + 1;
        //@ assert x == 0;
    }

The x in the set statement does not refer to the correct variable (neither when reading, nor when writing)

[wadoon]

Then I would say, the simple does not work and we need to go back to the drawing board.

@unp1 Do you have insides into the mechanism of variable renaming? Is there a chance, to get around the ProgVarReplaceVisitor completely? Why do we not book this information along a goal and/or a modality?

[wadoon]

Everything is terrible. Current test program:

class Test {
    //@ ghost int x;

    int a;

    //@ requires true; ensures x==a;
    void foo() {
        //@set x = 0;
        a = 0;
        //@set x = x + 1;
        a = a + 1;
        //@set x = x + 1;
        a = a + 1;
        //@set x = x + 1;
        a = a + 1;
        //@set x = x + 1;
        a = a + 1;
        //@set x = x + 1;
        a = a + 1;
    }


    //@ ghost int rec;
    int cer;

    //@ requires a >= 0; ensures rec == cer; measured_by a;
    int voo(int a) {
        if (a == 0) {
            //@ set rec = 0;
            cer = 0;
            return 0;
        } else {
            int r = voo(a - 1) + 1;
            //@ set rec = r;
            cer = r;
            //@ assert r >=0;
            return r;
        }
    }

}

There are only two possibilities:

• Using the spec repository
• Implement the JML classes in the KeY-Java-Ast for renaming.

[wadoon]

@mattulbrich The mutable information of SetStatements moved to SpecificationRepository.
Hence, the AST is immutable again. If the change suits you, we need to adopt the JmlAssert also.

The example above is proofable except for the faulty assert statement.

There are currently two construction sites:

1. PrettyPrinter can not show the current expression, as it has no access to services or the spec repo.
2. It is unclear whether a copy of the statement is necessary in ProgVarReplacer or IntroAtPreDefOps.

[codecov]

Codecov Report

Attention: Patch coverage is 55.33333% with 268 lines in your changes are missing coverage. Please review.

Project coverage is 37.87%. Comparing base (a5b90ec) to head (45435fb).

Files	Patch %	Lines
...rc/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java	61.88%	117 Missing ⚠️
...in/java/de/uka/ilkd/key/rule/SetStatementRule.java	25.58%	31 Missing and 1 partial ⚠️
...ka/ilkd/key/proof/mgt/SpecificationRepository.java	13.04%	17 Missing and 3 partials ⚠️
...a/ilkd/key/java/visitor/ProgVarReplaceVisitor.java	11.11%	16 Missing ⚠️
...lkd/key/java/visitor/ProgramVariableCollector.java	0.00%	11 Missing ⚠️
...d/key/speclang/jml/translation/JMLSpecFactory.java	80.76%	6 Missing and 4 partials ⚠️
.../ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java	0.00%	9 Missing ⚠️
.../main/java/de/uka/ilkd/key/rule/JmlAssertRule.java	0.00%	8 Missing ⚠️
.../uka/ilkd/key/rule/SetStatementBuiltInRuleApp.java	0.00%	8 Missing ⚠️
...java/de/uka/ilkd/key/java/statement/JmlAssert.java	14.28%	6 Missing ⚠️
... and 10 more

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3400      +/-   ##
============================================
+ Coverage     37.85%   37.87%   +0.01%     
- Complexity    17042    17079      +37     
============================================
  Files          2082     2086       +4     
  Lines        127290   127465     +175     
  Branches      21441    21460      +19     
============================================
+ Hits          48183    48272      +89     
- Misses        73194    73280      +86     
  Partials       5913     5913              

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