Support for memset hook.

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

k-distribution/tests/regression-new/bytes-memset/1.test

@@ -0,0 +1 @@
+memsetBytes(b"12345", 1, 3, 48)

k-distribution/tests/regression-new/bytes-memset/1.test.out

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

k-distribution/tests/regression-new/bytes-memset/2.test

@@ -0,0 +1 @@
+memsetBytes(b"10005", 1, 1, -1)

k-distribution/tests/regression-new/bytes-memset/2.test.out

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

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

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 <k> $PGM:Bytes </k>
+endmodule