From 9c424f74b54e2cf92e5c2a17058380485a333446 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 17 Oct 2023 16:15:12 -0500 Subject: [PATCH 1/3] FE support for memset hook. --- .../include/kframework/builtin/domains.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index f909b928620..68182956d47 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2109,6 +2109,21 @@ is not a valid index. 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 +`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. + +```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 From 2570aa4b95218902f8b0c933b4b20ab9d5c4d93d Mon Sep 17 00:00:00 2001 From: mariaKt Date: Thu, 19 Oct 2023 14:27:02 -0500 Subject: [PATCH 2/3] Update k-distribution/include/kframework/builtin/domains.md Co-authored-by: Bruce Collie --- k-distribution/include/kframework/builtin/domains.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 68182956d47..0b17dd08c2c 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2115,7 +2115,7 @@ 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. +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. From 0dbe61db1946e3142cb9435d8a9d5e1097de61db Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Thu, 19 Oct 2023 18:01:51 -0500 Subject: [PATCH 3/3] Added integration test, using the checks from the backend unit test that do not throw. --- k-distribution/tests/regression-new/bytes-memset/1.test | 1 + .../tests/regression-new/bytes-memset/1.test.out | 3 +++ k-distribution/tests/regression-new/bytes-memset/2.test | 1 + .../tests/regression-new/bytes-memset/2.test.out | 3 +++ k-distribution/tests/regression-new/bytes-memset/Makefile | 7 +++++++ k-distribution/tests/regression-new/bytes-memset/test.k | 7 +++++++ 6 files changed, 22 insertions(+) create mode 100644 k-distribution/tests/regression-new/bytes-memset/1.test create mode 100644 k-distribution/tests/regression-new/bytes-memset/1.test.out create mode 100644 k-distribution/tests/regression-new/bytes-memset/2.test create mode 100644 k-distribution/tests/regression-new/bytes-memset/2.test.out create mode 100644 k-distribution/tests/regression-new/bytes-memset/Makefile create mode 100644 k-distribution/tests/regression-new/bytes-memset/test.k diff --git a/k-distribution/tests/regression-new/bytes-memset/1.test b/k-distribution/tests/regression-new/bytes-memset/1.test new file mode 100644 index 00000000000..1c39464c58d --- /dev/null +++ b/k-distribution/tests/regression-new/bytes-memset/1.test @@ -0,0 +1 @@ +memsetBytes(b"12345", 1, 3, 48) diff --git a/k-distribution/tests/regression-new/bytes-memset/1.test.out b/k-distribution/tests/regression-new/bytes-memset/1.test.out new file mode 100644 index 00000000000..c311b4c628f --- /dev/null +++ b/k-distribution/tests/regression-new/bytes-memset/1.test.out @@ -0,0 +1,3 @@ + + b"10005" ~> . + diff --git a/k-distribution/tests/regression-new/bytes-memset/2.test b/k-distribution/tests/regression-new/bytes-memset/2.test new file mode 100644 index 00000000000..1bd1e676842 --- /dev/null +++ b/k-distribution/tests/regression-new/bytes-memset/2.test @@ -0,0 +1 @@ +memsetBytes(b"10005", 1, 1, -1) diff --git a/k-distribution/tests/regression-new/bytes-memset/2.test.out b/k-distribution/tests/regression-new/bytes-memset/2.test.out new file mode 100644 index 00000000000..7321d811902 --- /dev/null +++ b/k-distribution/tests/regression-new/bytes-memset/2.test.out @@ -0,0 +1,3 @@ + + b"1\xff005" ~> . + diff --git a/k-distribution/tests/regression-new/bytes-memset/Makefile b/k-distribution/tests/regression-new/bytes-memset/Makefile new file mode 100644 index 00000000000..d48aaade4fd --- /dev/null +++ b/k-distribution/tests/regression-new/bytes-memset/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/bytes-memset/test.k b/k-distribution/tests/regression-new/bytes-memset/test.k new file mode 100644 index 00000000000..08f8094086c --- /dev/null +++ b/k-distribution/tests/regression-new/bytes-memset/test.k @@ -0,0 +1,7 @@ +// Copyright (c) K Team. All Rights Reserved. +module TEST + imports BYTES + imports INT + + configuration $PGM:Bytes +endmodule