HOTFIX define Int2Bytes for -1 again (#4554)

Fixing an oversight in the previous change.
The value of `I` in the formula for negative `I` is actually
_bitwise-negated_ instead of just taking its negative. Therefore, we
would be calling log2Int(0) for `I ==Int -1`.

k-distribution/include/kframework/builtin/domains.md

@@ -2217,7 +2217,9 @@ module BYTES
   rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(I) +Int 9) /Int 8, I, E)
     requires I >Int 0 [preserves-definedness]
   rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes((log2Int(~Int I) +Int 9) /Int 8, I, E)
-    requires I <Int 0 [preserves-definedness]
+    requires I <Int -1 [preserves-definedness]
+  rule Int2Bytes(I::Int, E::Endianness, Signed  ) => Int2Bytes(1, -1, E)
+    requires I ==Int -1 [preserves-definedness]
 endmodule
 ```
 

k-distribution/tests/regression-new/int2bytes-no-len/0.test

@@ -0,0 +1 @@
+0

k-distribution/tests/regression-new/int2bytes-no-len/0.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/1.test

@@ -0,0 +1 @@
+1

k-distribution/tests/regression-new/int2bytes-no-len/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\x01\x04" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/10.test

@@ -0,0 +1 @@
+10

k-distribution/tests/regression-new/int2bytes-no-len/10.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/11.test

@@ -0,0 +1 @@
+11

k-distribution/tests/regression-new/int2bytes-no-len/11.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\x04\x01" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/12.test

@@ -0,0 +1 @@
+12

k-distribution/tests/regression-new/int2bytes-no-len/12.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\x04\x01" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/13.test

@@ -0,0 +1 @@
+13

k-distribution/tests/regression-new/int2bytes-no-len/13.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\xff" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/14.test

@@ -0,0 +1 @@
+14

k-distribution/tests/regression-new/int2bytes-no-len/14.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\xfb\xff" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/2.test

@@ -0,0 +1 @@
+2

k-distribution/tests/regression-new/int2bytes-no-len/2.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\x01\x04" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/3.test

@@ -0,0 +1 @@
+3

k-distribution/tests/regression-new/int2bytes-no-len/3.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\xff" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/4.test

@@ -0,0 +1 @@
+4

k-distribution/tests/regression-new/int2bytes-no-len/4.test.out

@@ -0,0 +1,3 @@
+<k>
+  b"\xff\xfb" ~> .K
+</k>

k-distribution/tests/regression-new/int2bytes-no-len/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/int2bytes-no-len/test.k

@@ -0,0 +1,23 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+// testing that krun pretty prints corectly Bytes
+// kx should replace krun though, so if this test
+// prevents a future upgrade, it should be removed
+
+module TEST
+    imports BYTES
+    imports INT
+
+    configuration <k> $PGM:Int </k>
+    rule 0 => Int2Bytes(0, LE, Unsigned) +Bytes Int2Bytes(0, LE, Signed)
+    rule 1 => Int2Bytes(1025, LE, Unsigned)
+    rule 2 => Int2Bytes(1025, LE, Signed)
+    rule 3 => Int2Bytes(-1, LE, Signed)
+    rule 4 => Int2Bytes(-1025, LE, Signed)
+
+    rule 10 => Int2Bytes(0, BE, Unsigned) +Bytes Int2Bytes(0, BE, Signed)
+    rule 11 => Int2Bytes(1025, BE, Unsigned)
+    rule 12 => Int2Bytes(1025, BE, Signed)
+    rule 13 => Int2Bytes(-1, BE, Signed)
+    rule 14 => Int2Bytes(-1025, BE, Signed)
+
+endmodule