Fix overflow checking

[WolframPfeifer]

The purpose of this PR is to repair the overflow checking of KeY and thus fix #3352.

TODO:

• [x] fix creation of branches for overflow checking
• [x] fix the actual proof obligation of the overflow check (should use inInt(...), inRangeInt(...), taclets in inRules(Un)CheckedSemantics.key)
• [x] throw an error if a choice used in a taclet does not exist
• [ ] activate the taclet option corresponding to the code_safe_math/code_java_math annotation
• [ ] create a user-level documentation (based on https://github.com/KeYProject/key/wiki/Spec-math-modes, but updated)
• [ ] create test cases (certain POs that are only provable when the "correct" semantics are used)

[codecov[bot]]

Codecov Report

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

Project coverage is 37.86%. Comparing base (1b48b9e) to head (5b68afc). Report is 73 commits behind head on main.

:exclamation: Current head 5b68afc differs from pull request most recent head fb3a5b1

Please upload reports for the commit fb3a5b1 to get more accurate results.

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3353      +/-   ##
============================================
- Coverage     38.03%   37.86%   -0.18%     
+ Complexity    17089    16904     -185     
============================================
  Files          2099     2055      -44     
  Lines        127274   125528    -1746     
  Branches      21386    21226     -160     
============================================
- Hits          48409    47525     -884     
+ Misses        72892    72152     -740     
+ Partials       5973     5851     -122     

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

[WolframPfeifer]

While working on this PR, I stumbled upon some unclear points:

• Does the code_bigint/safe/java_math annotation belong to the contract or to the method?
• Is it allowed to have multiple contracts with different code math modes?

In addition, I am not sure what syntax is currently supported by KeY's parser ...

Does anyone know the status quo? How should it be implemented?

[WolframPfeifer]

I am currently struggling with the assignmentToUpdate rules.

The original rule (i.e., status quo in KeY since #3027, with fix for the wrongly named taclet option) for e.g. subtraction looks like this:

    assignmentSubtractionInt {
        \find(\modality{#normalassign}{..
                    #loc = #seCharByteShortInt0 - #seCharByteShortInt1;
                ...}\endmodality (post))
        (intRules:arithmeticSemanticsCheckingOF) {
            "Overflow check":
                \replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1)))
        };
        \replacewith({#loc := javaSubInt(#seCharByteShortInt0, #seCharByteShortInt1)}
            \modality{#normalassign}{.. ...}\endmodality (post))
        \heuristics(executeIntegerAssignment)
        \displayname "subtraction"
    };

As @unp1 pointed out, if the modality is in the antecedent, you probably do not want to open a branch with the overflow "check" in the antecedent, as this leads to an unclosable branch usually.

If you would like to prevent that, you would have to duplicate all the rules (about 30 at the moment):

    assignmentSubtractionInt {
        \find(\modality{#normalassign}{..
                    #loc = #seCharByteShortInt0 - #seCharByteShortInt1;
                ...}\endmodality (post))
        \succedentPolarity
        (intRules:arithmeticSemanticsCheckingOF) {
            "Overflow check":
                \replacewith(inInt(sub(#seCharByteShortInt0, #seCharByteShortInt1)))
        };
        \replacewith({#loc := javaSubInt(#seCharByteShortInt0, #seCharByteShortInt1)}
            \modality{#normalassign}{.. ...}\endmodality (post))
        \heuristics(executeIntegerAssignment)
        \displayname "subtraction"
    };

    assignmentSubtractionInt2 {
        \find(\modality{#normalassign}{..
                    #loc = #seCharByteShortInt0 - #seCharByteShortInt1;
                ...}\endmodality (post))
        \antecedentPolarity
        \replacewith({#loc := javaSubInt(#seCharByteShortInt0, #seCharByteShortInt1)}
            \modality{#normalassign}{.. ...}\endmodality (post))
        \heuristics(executeIntegerAssignment)
        \displayname "subtraction"
    };

The open question is: Do we have to add another branch in the antecedent case to be able to assume that inInt(a - b)? Or do we have to check it? I really do not understand what would be correct here ...

Another option without the rule duplication would be to just limit application to the succedent. This has been done for example for the rule assignmentDivisionInt with the runtimeExceptions:ban semantics. However, this is also strange: There is just no rule to further symbolically execute a division (with this semantics selected) in a modality on the left-hand side.