Update dependency: llvm-backend/src/main/native/llvm-backend (#3938)

Co-authored-by: devops <[email protected]>
Co-authored-by: Bruce Collie <[email protected]>

CHANGELOG.md

@@ -2,6 +2,45 @@
 copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
+K Framework 6.2.0
+=================
+
+Major Changes
+-------------
+
+- The `Bytes` sort no longer represents mutable buffers of bytes by default.
+  Hooks that would previously have mutated a buffer when executing with the LLVM
+  backend will now perform a transparent copy of the underlying buffer. This
+  aligns the LLVM backend's behaviour with that of the Haskell backend and K. To
+  opt out of this change if performance when operating on large buffers is
+  important, semantics can pass the flag `--llvm-mutable-bytes` to `kompile`.
+
+Minor Changes
+-------------
+
+- Removed the `#parseKORE` hook (which presented a hole in the K type system) in
+  favour of modern, Pyk-based solutions to deserializing intermediate K states.
+
+- Added `k-which-python` tool to Nix builds of K, which helps to resolve
+  incompatibilities in Pyk-based applications that use K via `kup`.
+
+- Strict casts now use the `::S` syntax everywhere; a legacy use case for the
+  syntax `{...}<:S` is no longer required.
+
+- Improvements to the deterministic type inferencing algorithm; strict casts are
+  now handled and the new inferencer is enabled when typing proof claims.
+
+- Better integration between the Booster and LLVM backend in the presence of
+  partial functions and run-time errors.
+
+- The PL tutorial that was previously bundled with K will now be developed and
+  tested in its own repository.
+
+- Substantial improvements to K developer experience (code cleanup, auditing and
+  automatic tooling).
+
+- Bug fixes and feature requests supporting RV-internal projects.
+
 K Framework 6.1.0
 =================
 

install-k

@@ -1,6 +1,6 @@
 #!/bin/sh -e
 
-K_VERSION=6.1.87
+K_VERSION=6.2.0
 
 if [ `id -u` -ne 0 ]; then
   echo "$0: error: This script must be run as root."

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

@@ -1961,12 +1961,13 @@ Byte Arrays
 -----------
 
 Provided here is the syntax of an implementation of fixed-width arrays of Bytes
-in K. This type is hooked to an implementation of bytes provided by the
-backend. In concrete backends, this representation is mutable and thus multiple
-references can occur to the same `Bytes` object and when one is modified, the
-others are also modified. Care should be taken not to rely on this fact however
-as this is not the case in symbolic backends and thus you will experience
-divergent behavior unless the `Bytes` type is used in a manner that preserves
+in K. This type is hooked to an implementation of bytes provided by the backend.
+On the LLVM backend, it is possible to opt in to a faster, mutable
+representation (using the `--llvm-mutable-bytes` flag to `kompile`) where
+multiple references can occur to the same `Bytes` object and when one is
+modified, the others are also modified. Care should be taken when using this
+feature, however, as it is possible to experience divergent behavior with
+symbolic backends unless the `Bytes` type is used in a manner that preserves
 consistency.
 
 ```k
@@ -2103,39 +2104,38 @@ The result is `#False` if `startIndex` or `endIndex` are not valid.
 
 ### Multiple bytes update
 
-You can modify a `Bytes` to return a `Bytes` which is equal to `dest` except
-the `N` elements starting at `index` are replaced with the contents of `src` in
-O(N) time. This does not create a new `Bytes` object and will instead modify
-the original on concrete backends. The result is `#False` if `index` + `N`
-is not a valid index.
+You can modify a `Bytes` to return a `Bytes` which is equal to `dest` except the
+`N` elements starting at `index` are replaced with the contents of `src` in O(N)
+time. If `--llvm-mutable-bytes` is active, this will not create a new `Bytes`
+object and will instead modify the original on concrete backends. The result is
+`#False` if `index` + `N` is not a valid index.
 
 ```k
   syntax Bytes ::= replaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, hook(BYTES.replaceAt)]
 ```
 
 ### Multiple bytes update
 
-You can modify a `Bytes` to return a `Bytes` which is equal to `dest` except
-the `count` bytes starting at `index` are replaced with `count` bytes of value
+You can modify a `Bytes` to return a `Bytes` which is equal to `dest` except the
+`count` bytes starting at `index` are replaced with `count` bytes of value
 `Int2Bytes(1, v, LE/BE)` in O(count) time. This does not create a new `Bytes`
-object and will instead modify the original on concrete backends.
-This will throw an exception if `index` + `count` is not a valid index.
-The acceptable range of values for `v` is -128 to 127. This will throw an
-exception if `v` is outside of this range.
-This is implemented only for the LLVM backend.
+object and will instead modify the original if `--llvm-mutable-bytes` is active.
+This will throw an exception if `index` + `count` is not a valid index. The
+acceptable range of values for `v` is -128 to 127. This will throw an exception
+if `v` is outside of this range. This is implemented only for the LLVM backend.
 
 ```k
   syntax Bytes ::= memsetBytes(dest: Bytes, index: Int, count: Int, v: Int) [function, hook(BYTES.memset)]
 ```
 
 ### Bytes padding
 
-You can create a new `Bytes` object which is at least `length` bytes long
-by taking the input sequence and padding it on the right (respectively, on the
-left) with the specified `value`. This does not create a new `Bytes` object
-if the input is already at least `length` bytes long, and will instead
-return the input unchanged. The result is `#False` if `value` is not in the
-range `[0..255]`, or if the length is negative.
+You can create a new `Bytes` object which is at least `length` bytes long by
+taking the input sequence and padding it on the right (respectively, on the
+left) with the specified `value`. If `--llvm-mutable-bytes` is active, this does
+not create a new `Bytes` object if the input is already at least `length` bytes
+long, and will instead return the input unchanged. The result is `#False` if
+`value` is not in the range `[0..255]`, or if the length is negative.
 
 ```k
   syntax Bytes ::= padRightBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padRight)]
@@ -2144,8 +2144,9 @@ range `[0..255]`, or if the length is negative.
 
 ### Bytes reverse
 
-You can reverse a `Bytes` object in O(N) time. This does not create a new
-`Bytes` object and will instead modify the original on concrete backends.
+You can reverse a `Bytes` object in O(N) time. If `--llvm-mutable-bytes` is
+active, this will not create a new `Bytes` object and will instead modify the
+original.
 
 ```k
   syntax Bytes ::= reverseBytes(Bytes) [function, total, hook(BYTES.reverse)]

k-distribution/tests/regression-new/mutable-bytes/Makefile

@@ -0,0 +1,2 @@
+SUBDIRS=default mutable
+include ../../../include/kframework/ktest-group.mak

k-distribution/tests/regression-new/mutable-bytes/default/Makefile

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

k-distribution/tests/regression-new/mutable-bytes/default/a.test

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

k-distribution/tests/regression-new/mutable-bytes/default/a.test.out

@@ -0,0 +1,11 @@
+<test>
+  <k>
+    d ~> .
+  </k>
+  <mem>
+    b"bob__"
+  </mem>
+  <stuff>
+    b"alice"
+  </stuff>
+</test>

k-distribution/tests/regression-new/mutable-bytes/default/test.k

@@ -0,0 +1,21 @@
+module TEST
+    imports BYTES
+    imports INT-SYNTAX
+
+    configuration
+      <test>
+        <k> $PGM </k>
+        <mem> .Bytes </mem>
+        <stuff> .Bytes </stuff>
+      </test>
+
+    syntax KItem ::= "a" | "b" | "c" | "d" | "e"
+
+    rule <k> a => b </k>
+        <mem> _ => b"alice" </mem>
+    rule <k> b => c </k>
+        <mem> B </mem>
+        <stuff> _ => B </stuff>
+    rule <k> c => d </k>
+        <mem> B => replaceAtBytes(B, 0:Int, b"bob__") </mem>
+endmodule

k-distribution/tests/regression-new/mutable-bytes/mutable/Makefile

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

k-distribution/tests/regression-new/mutable-bytes/mutable/a.test

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

k-distribution/tests/regression-new/mutable-bytes/mutable/a.test.out

@@ -0,0 +1,11 @@
+<test>
+  <k>
+    d ~> .
+  </k>
+  <mem>
+    b"bob__"
+  </mem>
+  <stuff>
+    b"bob__"
+  </stuff>
+</test>

k-distribution/tests/regression-new/mutable-bytes/mutable/test.k

@@ -0,0 +1,21 @@
+module TEST
+    imports BYTES
+    imports INT-SYNTAX
+
+    configuration
+      <test>
+        <k> $PGM </k>
+        <mem> .Bytes </mem>
+        <stuff> .Bytes </stuff>
+      </test>
+
+    syntax KItem ::= "a" | "b" | "c" | "d" | "e"
+
+    rule <k> a => b </k>
+        <mem> _ => b"alice" </mem>
+    rule <k> b => c </k>
+        <mem> B </mem>
+        <stuff> _ => B </stuff>
+    rule <k> c => d </k>
+        <mem> B => replaceAtBytes(B, 0:Int, b"bob__") </mem>
+endmodule

llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java

@@ -128,6 +128,10 @@ private void llvmKompile(String type, String executable) {
         args.add("--proof-hint-instrumentation");
       }
 
+      if (options.llvmMutableBytes) {
+        args.add("--mutable-bytes");
+      }
+
       // Arguments after this point are passed on to Clang.
       args.add("--");
 

package/arch/PKGBUILD

@@ -1,6 +1,6 @@
 # Maintainer: Dwight Guth <[email protected]>
 pkgname=kframework-git
-pkgver=6.1.0
+pkgver=6.2.0
 pkgrel=1
 epoch=
 pkgdesc="K framework toolchain. Includes K Framework compiler for K language definitions, and K interpreter and prover for programs written in languages defined in K."

package/debian/changelog

@@ -1,4 +1,4 @@
-kframework (6.1.87) unstable; urgency=medium
+kframework (6.2.0) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-6.1.87
+6.2.0