Draft: Add definition taclets for binaryAnd, binaryOr, and binaryXOr

[ChristianHein]

Until now, KeY could only evaluate the functions binaryAnd, binaryOr, and
binaryXOr for literal values or in cases where a special case taclet exists
(see file "binaryLemmas.key"). For general reasoning, this is insufficient.
This pull request adds new definition taclets for these functions using a new
helper function bitAt to extract individual bits from unbounded JavaDL ints.

Overview of the taclets added:

• Bit extraction helper function bitAt
• binaryAndDef, binaryAndIntDef, binaryAndLongDef
• binaryOrDef, binaryOrIntDef, binaryOrLongDef
• binaryXOrDef, binaryXOrIntDef, binaryXOrLongDef

Using the bitAt function, we define binaryAnd, binaryOr, and binaryXOr
mathematically as bounded sums over all positional values of the result,
depending on the results of the bit operations on the input parameters.
We include three variants of each function definition: One general one where
the user must specify the maximum sign bit index of the two parameters; one for
Java int parameters (sign bit index 31); and one for Java long parameters
(sign-bit index 63). Each taclet opens another proof branch in
which it must be proven that the parameters of the function lie within the
valid range dictated by the sign bit index (e.g. inRangeInt(left) & inRangeInt(right)for the Javaint` versions).

---

Discussion Points

• The general definition taclets (e.g. binaryOrDef) force the user to specify the index of the sign bit. The disadvantage of this approach is that these taclets are not useful for proving properties of the bitwise functions which are independent of bit width, e.g., \forall int a; \forall int b; (binaryOr(a, b) = binaryOr(b, a)).
• @WolframPfeifer and I have discussed whether it would be better if these taclets did not define the binaryX functions, but instead defined the XJint/XJlong functions. At the moment, these latter functions are simply intermediate functions which are translated into binaryX. It seems that the binaryX functions are supposed to be treated as fundamental "mathematical" bitwise functions, although they assume two's complement representation which is not mathematically based. The XJint/XJlong functions clearly encode Java integer semantics into the meaning of the function in their name, thus might be the better "abstraction level" at which to define these functions.

[codecov]

Codecov Report

Merging #3174 (d607320) into main (edd76a2) will increase coverage by 0.00%.
The diff coverage is n/a.

@@            Coverage Diff            @@
##               main    #3174   +/-   ##
=========================================
  Coverage     31.54%   31.54%           
- Complexity    16774    16776    +2     
=========================================
  Files          2374     2374           
  Lines        150964   150964           
  Branches      24053    24053           
=========================================
+ Hits          47625    47627    +2     
  Misses        97547    97547           
+ Partials       5792     5790    -2     

see 2 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[github-actions]

Thank you for your contribution.

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