From b81310b98d98d5252d8ddd2f701e82cec0322469 Mon Sep 17 00:00:00 2001 From: Christian Hein Date: Mon, 19 Jun 2023 15:36:28 +0200 Subject: [PATCH 1/2] Add bit extraction function `bitAt` for JavaDL ints 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). --- .../de/uka/ilkd/key/proof/rules/binaryAxioms.key | 8 ++++++++ .../de/uka/ilkd/key/proof/rules/integerHeader.key | 5 +++++ 2 files changed, 13 insertions(+) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key index 3164c1aca0e..ec3bc24463e 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key @@ -115,4 +115,12 @@ \heuristics(simplify) }; + bitAtDef { + \schemaVar \term int number, index; + \find(bitAt(number, index)) + \replacewith(\if(0 <= index) + \then(mod(div(number, pow(2, index)), 2)) + \else(0)) + \heuristics(simplify) + }; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key index 27124b7abb1..a52ce328980 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integerHeader.key @@ -149,6 +149,11 @@ int unsignedshiftrightJint(int, int); int unsignedshiftrightJlong(int, int); + // Returns the bit value (0 or 1) at the specified index, where index 0 + // refers to the least-significant bit. Assumes two's complement + // representation. + int bitAt(/* number */ int, /* bit index */ int); + // bitmask operations &, |, ^ int binaryAnd(/* left */ int, /* right */ int); int binaryOr(/* left */ int, /* right */ int); From d6073208308476c1fa4d392b4ea6565fcd5e489b Mon Sep 17 00:00:00 2001 From: Christian Hein Date: Mon, 19 Jun 2023 15:43:50 +0200 Subject: [PATCH 2/2] Add definition taclets for binaryAnd, binaryOr, binaryXOr 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). --- .../uka/ilkd/key/proof/rules/binaryAxioms.key | 133 +++++++++++++++--- 1 file changed, 111 insertions(+), 22 deletions(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key index ec3bc24463e..50de0658904 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key @@ -1,8 +1,11 @@ +\schemaVariables { + \term int left, right; + \term int signedBitIndex; // E.g., 31 for Java ints, 63 for Java longs. +} + \rules { // wrappers for positive numbers to prevent shiftRightDef -> shiftLeftDef mutual recursion shiftRightPositiveShiftDef { - \schemaVar \term int left, right; - \find(shiftrightPositiveShift(left, right)) \replacewith(div(left, pow(2, right))) @@ -10,8 +13,6 @@ }; shiftLeftPositiveShiftDef { - \schemaVar \term int left, right; - \find(shiftleftPositiveShift(left, right)) \replacewith(mul(left, pow(2, right))) @@ -20,8 +21,6 @@ // arbitrary fixed length bitvector operations shiftRightDef { - \schemaVar \term int left, right; - \find(shiftright(left, right)) \replacewith(\if(right < 0) \then(shiftleftPositiveShift(left, -right)) @@ -32,8 +31,6 @@ }; shiftLeftDef { - \schemaVar \term int left, right; - \find(shiftleft(left, right)) \replacewith(\if(right < 0) \then(shiftrightPositiveShift(left, -right)) @@ -44,8 +41,6 @@ }; javaShiftRightIntDef { - \schemaVar \term int left, right; - \find(shiftrightJint(left, right)) // usage of the mathematical mod is crucial as -1 % 32 = 31 (!) \replacewith(moduloInt(shiftright(left, mod(right, 32)))) @@ -53,8 +48,6 @@ }; javaShiftRightLongDef { - \schemaVar \term int left, right; - \find(shiftrightJlong(left, right)) // usage of the mathematical mod is crucial as -1 % 64 = 63 (!) \replacewith(moduloLong(shiftright(left, mod(right, 64)))) @@ -63,8 +56,6 @@ }; javaShiftLeftIntDef { - \schemaVar \term int left, right; - \find(shiftleftJint(left, right)) // usage of the mathematical mod is crucial as -1 % 32 = 31 (!) \replacewith(moduloInt(shiftleft(left, mod(right, 32)))) @@ -72,8 +63,6 @@ }; javaShiftLeftLongDef { - \schemaVar \term int left, right; - \find(shiftleftJlong(left, right)) // usage of the mathematical mod is crucial as -1 % 64 = 63 (!) \replacewith(moduloLong(shiftleft(left, mod(right, 64)))) @@ -82,7 +71,6 @@ }; unsignedShiftRightJintDef { - \schemaVar \term int left, right; \find(unsignedshiftrightJint(left, right)) \replacewith(\if(left >= 0) \then(shiftrightJint(left, right)) \else(addJint(shiftrightJint(left, right), shiftleftJint(2, 31 - mod(right, 32))))) @@ -90,8 +78,6 @@ }; xorJIntDef { - \schemaVar \term int left, right; - \find(xorJint(left, right)) \replacewith(moduloInt(binaryXOr(left, right))) @@ -99,8 +85,6 @@ }; orJIntDef { - \schemaVar \term int left, right; - \find(orJint(left, right)) \replacewith(moduloInt(binaryOr(left, right))) @@ -108,13 +92,16 @@ }; andJIntDef { - \schemaVar \term int left, right; \find(andJint(left, right)) \replacewith(moduloInt(binaryAnd(left, right))) \heuristics(simplify) }; + // Definitions for binaryAnd, binaryOr, and binaryXOr. Each function has + // three definitions: One for Java ints (32-bit), one for Java longs + // (64-bit), and one general one based on a user-specified sign-bit index. + bitAtDef { \schemaVar \term int number, index; \find(bitAt(number, index)) @@ -123,4 +110,106 @@ \else(0)) \heuristics(simplify) }; + + binaryAndDef { + \find(binaryAnd(left, right)) + \replacewith( + bsum{int i;}(0, signedBitIndex, pow(2, i) * bitAt(left, i) * bitAt(right, i)) + - \if(left < 0 & right < 0) + \then(pow(2, signedBitIndex)) + \else(0)); + \add( ==> left >= -pow(2, signedBitIndex) & left < pow(2, signedBitIndex) + & right >= -pow(2, signedBitIndex) & right < pow(2, signedBitIndex)) + }; + + binaryAndIntDef { + \find(binaryAnd(left, right)) + \replacewith( + bsum{int i;}(0, 31, pow(2, i) * bitAt(left, i) * bitAt(right, i)) + - \if(left < 0 & right < 0) + \then(pow(2, 31)) + \else(0)); + \add( ==> inRangeInt(left), inRangeInt(right)) + }; + + binaryAndLongDef { + \find(binaryAnd(left, right)) + \replacewith( + bsum{int i;}(0, 63, pow(2, i) * bitAt(left, i) * bitAt(right, i)) + - \if(left < 0 & right < 0) + \then(pow(2, 63)) + \else(0)); + \add( ==> inRangeLong(left), inRangeLong(right)) + }; + + binaryOrDef { + \find(binaryOr(left, right)) + \replacewith( + bsum{int i;}(0, signedBitIndex, + pow(2, i) * (bitAt(left, i) + bitAt(right, i) + - (bitAt(left, i) * bitAt(right, i)))) + - \if(left < 0 | right < 0) + \then(pow(2, signedBitIndex)) + \else(0)); + \add( ==> left >= -pow(2, signedBitIndex) & left < pow(2, signedBitIndex) + & right >= -pow(2, signedBitIndex) & right < pow(2, signedBitIndex)) + }; + + binaryOrIntDef { + \find(binaryOr(left, right)) + \replacewith( + bsum{int i;}(0, 31, + pow(2, i) * (bitAt(left, i) + bitAt(right, i) + - (bitAt(left, i) * bitAt(right, i)))) + - \if(left < 0 | right < 0) + \then(pow(2, 31)) + \else(0)); + \add( ==> inRangeInt(left), inRangeInt(right)) + }; + + binaryOrLongDef { + \find(binaryOr(left, right)) + \replacewith( + bsum{int i;}(0, 63, + pow(2, i) * (bitAt(left, i) + bitAt(right, i) + - (bitAt(left, i) * bitAt(right, i)))) + - \if(left < 0 | right < 0) + \then(pow(2, 63)) + \else(0)); + \add( ==> inRangeLong(left), inRangeLong(right)) + }; + + binaryXOrDef { + \find(binaryXOr(left, right)) + \replacewith( + bsum{int i;}(0, signedBitIndex, + pow(2, i) * mod(bitAt(left, i) + bitAt(right, i), 2)) + - \if(!(left < 0 <-> right < 0)) + \then(pow(2, signedBitIndex)) + \else(0)); + \add( ==> left >= -pow(2, signedBitIndex) & left < pow(2, signedBitIndex) + & right >= -pow(2, signedBitIndex) & right < pow(2, signedBitIndex)) + }; + + binaryXOrIntDef { + \find(binaryXOr(left, right)) + \replacewith( + bsum{int i;}(0, 31, + pow(2, i) * mod(bitAt(left, i) + bitAt(right, i), 2)) + - \if(!(left < 0 <-> right < 0)) + \then(pow(2, 31)) + \else(0)); + \add( ==> inRangeInt(left), inRangeInt(right)) + }; + + binaryXOrLongDef { + \find(binaryXOr(left, right)) + \replacewith( + bsum{int i;}(0, 63, + pow(2, i) * mod(bitAt(left, i) + bitAt(right, i), 2)) + - \if(!(left < 0 <-> right < 0)) + \then(pow(2, 63)) + \else(0)); + \add( ==> inRangeLong(left), inRangeLong(right)) + }; }