Solving the FP completeness issues in #1723

[mattulbrich]

Related Issue

This pull request answers to issue #1723.

Intended Change

Floats and doubles are currently incorrectly insufficiently handled when they appear in
one expression.

Casts need to be added and casts need to be dealt with. ...

• introducing casts where needed
• adding rules / SMT support for such casts.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other:

Ensuring quality

• I made sure that introduced/changed code has been well documented (javadoc).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: small 2-liners
• I have checked that runtime performance has not deteriorated

Additional information and contact(s)

It's still W I P.

@samysweb

The contributions within this pull request will be licensed under GPL2-or-later wihtin KeY.

[samysweb]

I just did some testing and the floating point balancing seems to work relatively reliably for binary operations.
I currently still see two issues with the current state:

Edge case for binary expressions

There seems to be one edge case due to the replacement strategy of ProgramElementReplacer which always substitutes the first occurrence.
The bug shows up when analyzing the following program:

/*@ public normal_behavior
  @ requires x1 > 0.0f && x2 > 0.0f;
  @ ensures \result>0.0;
  @*/
public double myFunction05(float x1, float x2) {
    double squared1 = ((double) x1)+x1;
    return squared1;
}

At some point within the proof we get to the expression squared1 = ((double)_x1)+_x1
At this point we can either apply the compound_addition_1 taclet (then everything works out fine) or we can apply the cast taclet which (applied repeatedly) results in:

• ((double)(double)_x1)+_x1
• ((double)(double)(double)_x1)+_x1
• ...

This is because ProgramElementReplacer finds _x1 in the left child of + first and replaces it there.
I'm not sure about the consequences of this:

1. It seems that this introduces some non-determinism in the symbolic execution meaning if we always apply the wrong rule we could get stuck
2. From my understanding of how replacements work this does not seem easily fixable without reimplementing a position based version of ProgramElementReplacer

How to do position based replacement?

Assignments/Returns

The current rules did not yet take this case into account, to this end I began drafting rules in #3062 (On my own fork since I don't have writing rights on this branch).
The added taclets allow for the treatment of most widening assignments, however there are still some limitations:

• Auto mode currently breaks on the first appearance of such an assignment, as the assignment taclet seems to take precedence but fails upon application due to type incompatibilities
• If I understand this correctly, a binary operation between two integral types (e.g. two ints) is not a simple expression and thus the rules added in Floating Point rules for casts #3062 currently do not apply. Currently this means the addition rule for adding 2 ints is applied and fails with an exception due to a type mismatch. I'm not sure if this can be fixed without replicating all assignmentMultiplicationInt,assignmentAdditionInt etc. taclets for float and long

Notes from our conversation just now:

• Maybe add type sanity checks to all currently existing assignment rules and only allow assignment if same sort or subtype (currently this is only discovered upon application and prevented through an exception which aborts auto mode)
• If we do this then new rules are needed:
  • Binary Operation between two simple expression with unbalanced types: Adjust unbalanced_float_expression from this branch
  • Assignment d = se0 + se1 where se0 and se1 have same type but d differs: e=se0+se1;d=e where e has type of se0
  • d=e with e simple expression: type cast

[samysweb]

Huh interesting, so what really happens when you click GitHub's innocently looking "rebase" button is a force-push...

[mattulbrich]

Huh interesting, so what really happens when you click GitHub's innocently looking "rebase" button is a force-push...

Ok, anything lost or was it a fast-forward with a more aggressive name?

[samysweb]

I don't think anything should have gotten lost.
Probably just a more aggressive name because the main commits are inserted before the commits on this branch.

On that note: Unfortunately, I just realized #3027 is not merged yet

[github-advanced-security]

You have successfully added a new QDJVMC configuration project/qodana. As part of the setup process, we have scanned this repository and found 1 existing alert. Please check the repository Security tab to see all alerts.

[mattulbrich]

Smells like a false alert?

[samysweb]

I'm saving the runtimes of the last test run here so that we can compare runtimes once my pull request (with lots of additional \varcond statements) is merged into this branch:

Job	Run time
optional-tests	32m 35s
integration-tests (testProveRules, ubuntu-latest, 11)	16m 5s
integration-tests (testRunAllFunProofs, ubuntu-latest, 11)	1h 27m 29s
integration-tests (testRunAllInfProofs, ubuntu-latest, 11)	56m 47s
unit-tests (ubuntu-latest, 11)	21m 42s
unit-tests (ubuntu-latest, 17)	20m 44s
Overall	3h 55m 22s

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[samysweb]

Looks like all tests are passing.
Comparison of runtimes:

Job	Run time old	Runtime after merge
optional-tests	32m 35s	--
integration-tests (testProveRules, ubuntu-latest, 11)	16m 5s	11m 46s
integration-tests (testRunAllFunProofs, ubuntu-latest, 11)	1h 27m 29s	1h 46m 50s*
integration-tests (testRunAllInfProofs, ubuntu-latest, 11)	56m 47s	45m 43s
unit-tests (ubuntu-latest, 11)	21m 42s	17m 24s
unit-tests (ubuntu-latest, 17)	20m 44s	25m 18s

*repeating the run resulted in a runtime of 1h 24m 34s -- it seems this was just due to the high variance of runtimes on GitHub (so it's very likely that all the other "better" results are noise as well)

Left to do:

• Check once more that rules actually do the job
• Check that SMT translation is available (see above)
• Is slower run of testRunAllFunProofs due to changes in int rules?

[samysweb]

Alternative to variable conditions: Create a new schema variable IntegralVariable and then use #integralLoc (code for Schema Variable class provided by Richard Bubel).