Draft: Add definition taclets for binaryAnd, binaryOr, and binaryXOr
#3174
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The `bitAt` returns the value of a single bit (0 or 1) from an unbounded JavaDL int, assuming two's complement representation. For negative indices, the result is zero. Introduced for definitions of `binaryAnd`, `binaryOr`, and `binaryXOr` in a later commit. Developed as part of my bachelor's thesis "Handling Bitwise Operations in Deductive Program Verification: Case Study java.util.BitSet with KeY" (2023).
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 commit adds the following new definitions for these functions in KeY: - binaryAndDef, binaryAndIntDef, binaryAndLongDef - binaryOrDef, binaryOrIntDef, binaryOrLongDef - binaryXOrDef, binaryXOrIntDef, binaryXOrLongDef Using the `bitAt` helper function to refer to individual bits in the bitwise representation of input parameters, this commit defines the `binaryAnd`, `binaryOr`, and `binaryXOr` functions mathematically as a bounded sum over all positional values of the result, depending on the result of the bit operations on the input parameters. The signed bit has a negative positional value because of two's complement representation. Bitwise operations are emulated mathematically, e.g., using multiplication for AND. This commit includes 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 additionally 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 Java `int` versions). These taclets were developed as part of my bachelor's thesis "Handling Bitwise Operations in Deductive Program Verification: Case Study java.util.BitSet with KeY" (2023).
ChristianHein
changed the title
binaryAnd, binaryOr, and binaryXOrbinaryAnd, binaryOr, and binaryXOr
Codecov Report
@@ 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Until now, KeY could only evaluate the functions
binaryAnd,binaryOr, andbinaryXOrfor 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
bitAtto extract individual bits from unbounded JavaDL ints.Overview of the taclets added:
bitAtbinaryAndDef,binaryAndIntDef,binaryAndLongDefbinaryOrDef,binaryOrIntDef,binaryOrLongDefbinaryXOrDef,binaryXOrIntDef,binaryXOrLongDefUsing the
bitAtfunction, we definebinaryAnd,binaryOr, andbinaryXOrmathematically 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
intparameters (sign bit index 31); and one for Javalongparameters(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
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)).binaryXfunctions, but instead defined theXJint/XJlongfunctions. At the moment, these latter functions are simply intermediate functions which are translated intobinaryX. It seems that thebinaryXfunctions are supposed to be treated as fundamental "mathematical" bitwise functions, although they assume two's complement representation which is not mathematically based. TheXJint/XJlongfunctions 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.