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

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key

@@ -1,17 +1,18 @@
+\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)))
 
         \heuristics(simplify)
     };
 
     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,17 +41,13 @@
     };
 
     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))))
         \heuristics(simplify_enlarging)
     };
 
     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,17 +56,13 @@
     };
 
     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))))
         \heuristics(simplify_enlarging)
     };
 
     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,37 +71,145 @@
     };
 
     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)))))
         \heuristics(simplify_enlarging)
     };
 
     xorJIntDef {
-        \schemaVar \term int left, right;
-
         \find(xorJint(left, right))
         \replacewith(moduloInt(binaryXOr(left, right)))
 
         \heuristics(simplify)
     };
 
     orJIntDef {
-        \schemaVar \term int left, right;
-
         \find(orJint(left, right))
         \replacewith(moduloInt(binaryOr(left, right)))
 
         \heuristics(simplify)
     };
 
     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))
+        \replacewith(\if(0 <= index)
+                \then(mod(div(number, pow(2, index)), 2))
+                \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))
+    };
 }

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);