Merge remote-tracking branch 'origin/develop'

runtimeverification · Jul 26, 2024 · 815a335 · 815a335
2 parents f73063d + 869befa
commit 815a335
Show file tree

Hide file tree

Showing 23 changed files with 72 additions and 1 deletion.
diff --git a/k-distribution/include/kframework/builtin/domains.md b/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
 ```
 

diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/0.test b/k-distribution/tests/regression-new/int2bytes-no-len/0.test
@@ -0,0 +1 @@
+0
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/0.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/0.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/1.test b/k-distribution/tests/regression-new/int2bytes-no-len/1.test
@@ -0,0 +1 @@
+1
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/1.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/1.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\x01\x04" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/10.test b/k-distribution/tests/regression-new/int2bytes-no-len/10.test
@@ -0,0 +1 @@
+10
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/10.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/10.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/11.test b/k-distribution/tests/regression-new/int2bytes-no-len/11.test
@@ -0,0 +1 @@
+11
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/11.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/11.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\x04\x01" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/12.test b/k-distribution/tests/regression-new/int2bytes-no-len/12.test
@@ -0,0 +1 @@
+12
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/12.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/12.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\x04\x01" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/13.test b/k-distribution/tests/regression-new/int2bytes-no-len/13.test
@@ -0,0 +1 @@
+13
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/13.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/13.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\xff" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/14.test b/k-distribution/tests/regression-new/int2bytes-no-len/14.test
@@ -0,0 +1 @@
+14
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/14.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/14.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\xfb\xff" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/2.test b/k-distribution/tests/regression-new/int2bytes-no-len/2.test
@@ -0,0 +1 @@
+2
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/2.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/2.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\x01\x04" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/3.test b/k-distribution/tests/regression-new/int2bytes-no-len/3.test
@@ -0,0 +1 @@
+3
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/3.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/3.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\xff" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/4.test b/k-distribution/tests/regression-new/int2bytes-no-len/4.test
@@ -0,0 +1 @@
+4
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/4.test.out b/k-distribution/tests/regression-new/int2bytes-no-len/4.test.out
@@ -0,0 +1,3 @@
+<k>
+  b"\xff\xfb" ~> .K
+</k>
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/Makefile b/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
diff --git a/k-distribution/tests/regression-new/int2bytes-no-len/test.k b/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