diff --git a/CHANGELOG.md b/CHANGELOG.md index 2379fa290bb..1580644cd69 100644 --- a/CHANGELOG.md +++ b/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 ================= diff --git a/flake.lock b/flake.lock index 4c98f887e0e..4627c73c093 100644 --- a/flake.lock +++ b/flake.lock @@ -118,11 +118,11 @@ ] }, "locked": { - "lastModified": 1705941888, - "narHash": "sha256-/yjqTAM8Zw0beuwZZkl+3d9IRMDJ3LQOUvVAhgzcpso=", + "lastModified": 1706709754, + "narHash": "sha256-Q2uQucqag3F7CkAWd7bYU/QU4fh8Gf5oiLt6f+g3tgI=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "2fdcb5953b4c40198a1ecaa8f91fae5b47d7100b", + "rev": "8c77e2101ee076d7f2cce9744c9a4b35efea1a8f", "type": "github" }, "original": { diff --git a/install-k b/install-k index c9b22833737..31c84a93ba5 100755 --- a/install-k +++ b/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." diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 474ea6f8b1e..f017f5d3885 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/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,11 +2104,11 @@ 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)] @@ -2115,14 +2116,13 @@ is not a valid index. ### 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)] @@ -2130,12 +2130,12 @@ This is implemented only for the LLVM backend. ### 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)] diff --git a/k-distribution/tests/regression-new/mutable-bytes/Makefile b/k-distribution/tests/regression-new/mutable-bytes/Makefile new file mode 100644 index 00000000000..5efe0edce09 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/Makefile @@ -0,0 +1,2 @@ +SUBDIRS=default mutable +include ../../../include/kframework/ktest-group.mak diff --git a/k-distribution/tests/regression-new/mutable-bytes/default/Makefile b/k-distribution/tests/regression-new/mutable-bytes/default/Makefile new file mode 100644 index 00000000000..1f58868a936 --- /dev/null +++ b/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 diff --git a/k-distribution/tests/regression-new/mutable-bytes/default/a.test b/k-distribution/tests/regression-new/mutable-bytes/default/a.test new file mode 100644 index 00000000000..78981922613 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/default/a.test @@ -0,0 +1 @@ +a diff --git a/k-distribution/tests/regression-new/mutable-bytes/default/a.test.out b/k-distribution/tests/regression-new/mutable-bytes/default/a.test.out new file mode 100644 index 00000000000..91389597680 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/default/a.test.out @@ -0,0 +1,11 @@ + + + d ~> . + + + b"bob__" + + + b"alice" + + diff --git a/k-distribution/tests/regression-new/mutable-bytes/default/test.k b/k-distribution/tests/regression-new/mutable-bytes/default/test.k new file mode 100644 index 00000000000..063402d76a5 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/default/test.k @@ -0,0 +1,21 @@ +module TEST + imports BYTES + imports INT-SYNTAX + + configuration + + $PGM + .Bytes + .Bytes + + + syntax KItem ::= "a" | "b" | "c" | "d" | "e" + + rule a => b + _ => b"alice" + rule b => c + B + _ => B + rule c => d + B => replaceAtBytes(B, 0:Int, b"bob__") +endmodule diff --git a/k-distribution/tests/regression-new/mutable-bytes/mutable/Makefile b/k-distribution/tests/regression-new/mutable-bytes/mutable/Makefile new file mode 100644 index 00000000000..4491d1c42e2 --- /dev/null +++ b/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 diff --git a/k-distribution/tests/regression-new/mutable-bytes/mutable/a.test b/k-distribution/tests/regression-new/mutable-bytes/mutable/a.test new file mode 100644 index 00000000000..78981922613 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/mutable/a.test @@ -0,0 +1 @@ +a diff --git a/k-distribution/tests/regression-new/mutable-bytes/mutable/a.test.out b/k-distribution/tests/regression-new/mutable-bytes/mutable/a.test.out new file mode 100644 index 00000000000..2872bde8116 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/mutable/a.test.out @@ -0,0 +1,11 @@ + + + d ~> . + + + b"bob__" + + + b"bob__" + + diff --git a/k-distribution/tests/regression-new/mutable-bytes/mutable/test.k b/k-distribution/tests/regression-new/mutable-bytes/mutable/test.k new file mode 100644 index 00000000000..063402d76a5 --- /dev/null +++ b/k-distribution/tests/regression-new/mutable-bytes/mutable/test.k @@ -0,0 +1,21 @@ +module TEST + imports BYTES + imports INT-SYNTAX + + configuration + + $PGM + .Bytes + .Bytes + + + syntax KItem ::= "a" | "b" | "c" | "d" | "e" + + rule a => b + _ => b"alice" + rule b => c + B + _ => B + rule c => d + B => replaceAtBytes(B, 0:Int, b"bob__") +endmodule diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java index d2dae356c3a..eb6b9fd2f79 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java +++ b/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("--"); diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 2fdcb5953b4..8c77e2101ee 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 2fdcb5953b4c40198a1ecaa8f91fae5b47d7100b +Subproject commit 8c77e2101ee076d7f2cce9744c9a4b35efea1a8f diff --git a/package/arch/PKGBUILD b/package/arch/PKGBUILD index bae9a52183d..17b49665baa 100644 --- a/package/arch/PKGBUILD +++ b/package/arch/PKGBUILD @@ -1,6 +1,6 @@ # Maintainer: Dwight Guth 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." diff --git a/package/debian/changelog b/package/debian/changelog index 073cdf7706c..061801dd740 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kframework (6.1.87) unstable; urgency=medium +kframework (6.2.0) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 93260f3794a..6abaeb2f907 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -6.1.87 +6.2.0