Fix for the LoopInvariantConfigurationDialog

unp1 commented 10 months ago

Related Issue

This PR fixes a bug that prevented the interactive provision of a loop invariant.

Intended Change

It should be possible to enter loop invariants manually.

Type of pull request

[x] 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)
[x] 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 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.
[x] I have tested the feature as follows: Applied a manually entered loop invariant
[ ] I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The problem was if no "free modifies"/"free assignable" was available then creating the whole modifies set "union(freeMod, mod)" led to a NullPointerException. The fix uses "strictly_nothing" as default for free assignables of loops, if non given.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

codecov[bot] commented 10 months ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Comparison is base (a92f04e) 37.98% compared to head (cc53817) 37.98%.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3377 +/- ## ========================================= Coverage 37.98% 37.98% Complexity 17024 17024 ========================================= Files 2059 2059 Lines 126029 126032 +3 Branches 21282 21283 +1 ========================================= + Hits 47875 47877 +2 Misses 72272 72272 - Partials 5882 5883 +1 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

WolframPfeifer commented 10 months ago

I do not really understand the problem from the description. By "free modifier", do you mean "assignable_free"? How can this be used in interactively specified loops at all?

unp1 commented 10 months ago

Yes and yes :-) The problem is that the "assignable_free" clause cannot be specified in the dialoh and therefore "null" was returned as its instantiation, which then lead to an NPE.

Looking at the code, a specified (via JML) "assignable_free" clause would cause the actual modifies set to be "union(mod, freeMod)", hence I assume, strictly_nothing should be the intended default? This is now used, if no "assignable_free" is given.

A simple example is the attached file. The invariant specification for the dialog is

invariant: i>=0 & i<=n modifies: {} variant: n - i

In the current version that leads to an NPE simple.txt

Changed the "additional information" section in the PR description for more clarity.

WolframPfeifer commented 10 months ago

Yes and yes :-) The problem is that the assignable_free cannot be specified and therefore "null" was returned as instantiation which then lead to an NPE.

Looking at the code, a specified (via JML) free assignable would cause the actual modifies set to be "union(mod, freeMod)", hence I assume, strictly_nothing should be the intended default (?), which is now used if that no free_assignable can be found.

A simple example is the attached file. The invariant specification to enter in the dialog is

invariant: i>=0 & i<=n modifies: {} variant: n - i

In the current version that leads to an NPE simple.txt

Changed additional information section in the PR description for more clarity.

Thanks for the explanation. I have to admit that I find the ..._free clauses quite confusing. I talked to @flo2702 today, who implemented the ..._free clauses, and he convinced me that indeed \strictly_nothing is the correct default here.

With the changes in this branch, something is very strange now: I can not even close an easy proof with a loop that writes only a single field. The problem seems to be that there are two different self variables (different hashes) ...

unp1 commented 10 months ago

With the changes in this branch, something is very strange now: I can not even close an easy proof with a loop that writes only a single field. The problem seems to be that there are two different self variables (different hashes) ...

Just to be sure, you mean when using the dialog for the loop invariant (not as JML annotation)? If yes, I assume the bug is not introduced by this patch as it does not touch anything remotely related to "self", but I can have a look and try to fix it.

If no, that is really strange (and I will have a look in any case ;-)

WolframPfeifer commented 10 months ago

With the changes in this branch, something is very strange now: I can not even close an easy proof with a loop that writes only a single field. The problem seems to be that there are two different self variables (different hashes) ...

Just to be sure, you mean when using the dialog for the loop invariant (not as JML annotation)? If yes, I assume the bug is not introduced by this patch as it does not touch anything remotely related to "self", but I can have a look and try to fix it.

If no, that is really strange (and I will have a look in any case ;-)

Yes, when using the dialog. I think this error has been on the main branch for a while, but since the dialog did not work anyway, probably nobody noticed it.

unp1 commented 10 months ago

With the changes in this branch, something is very strange now: I can not even close an easy proof with a loop that writes only a single field. The problem seems to be that there are two different self variables (different hashes) ...

Just to be sure, you mean when using the dialog for the loop invariant (not as JML annotation)? If yes, I assume the bug is not introduced by this patch as it does not touch anything remotely related to "self", but I can have a look and try to fix it. If no, that is really strange (and I will have a look in any case ;-)

Yes, when using the dialog. I think this error has been on the main branch for a while, but since the dialog did not work anyway, probably nobody noticed it.

The latest commit fixes the duplicate self issue.

There is one general issue: The configurator prefills the dialog with JML loop specifications if available. This uses the "internal self", i.e., the placeholder self from the loop invariant translation. This might either not be present in practice (e.g., if we verify a static method which calls an instance method on some object that contains a loop) or the self is not the correct one. Worst case scenarios:

there is a parser error or
the self is for a different object of a different class ==> In n both cases one needs to replace the used self by the correct object.
the used self variable is for a different object of the same class, in which case the loop specification parses but is not provable and one has to find out why. This might be annoying as one wastes time looking for logic mistakes in the loop invariant and not something as simple as that the 'this' object is the wrong one.

To fix that properly one would need to analyse the sequent to find out which self (if any to use). That is not done in the current fix (for time reasons). I would suggest to open a new feature/bug request so that it can be attacked at later time.

unp1 commented 2 months ago

Rebased on current main. Loop invariant dialog works again w/o NPE.

@WolframPfeifer: Ready for review, thanks!

unp1 commented 2 months ago

I think the Qodana and Checkerframework fails are unrelated to this PR.

KeYProject / key