From 7f1176799faa2e9aaa77747a96a0c47feb9bc1fc Mon Sep 17 00:00:00 2001
From: Christian Hein <uaken@student.kit.edu>
Date: Thu, 15 Jun 2023 13:43:59 +0200
Subject: [PATCH] Add missing translation taclets for bitwise operations

Some bitwise operations were missing translation taclets for the case
that the parameters are of type `long`. For example, `andJlong` did not
have a definition.
---
 .../uka/ilkd/key/proof/rules/binaryAxioms.key | 37 +++++++++++++++++++
 1 file changed, 37 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 6742d705606..178def1cebd 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
@@ -93,6 +93,16 @@
         \heuristics(simplify_enlarging)
     };
 
+    unsignedShiftRightJlongDef {
+        \schemaVar \term int left, right;
+
+        \find(unsignedshiftrightJlong(left, right))
+        \replacewith(\if(left >= 0) \then(shiftrightJlong(left, right))
+                \else(addJlong(shiftrightJlong(left, right), shiftleftJlong(2, 63 - mod(right, 64)))))
+
+        \heuristics(simplify_enlarging)
+    };
+
     xorJIntDef {
         \schemaVar \term int left, right;
 
@@ -102,6 +112,15 @@
         \heuristics(simplify)
     };
 
+    xorJLongDef {
+        \schemaVar \term int left, right;
+
+        \find(xorJlong(left, right))
+        \replacewith(moduloLong(binaryXOr(left, right)))
+
+        \heuristics(simplify)
+    };
+
     orJIntDef {
         \schemaVar \term int left, right;
 
@@ -111,6 +130,15 @@
         \heuristics(simplify)
     };
 
+    orJLongDef {
+        \schemaVar \term int left, right;
+
+        \find(orJlong(left, right))
+        \replacewith(moduloLong(binaryOr(left, right)))
+
+        \heuristics(simplify)
+    };
+
     andJIntDef {
         \schemaVar \term int left, right;
 
@@ -119,4 +147,13 @@
 
         \heuristics(simplify)
     };
+
+    andJLongDef {
+        \schemaVar \term int left, right;
+
+        \find(andJlong(left, right))
+        \replacewith(moduloLong(binaryAnd(left, right)))
+
+        \heuristics(simplify)
+    };
 }