From 8d6a546758e16af2921c1ac543a798cfdb2f6f74 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 8 Jul 2025 15:12:02 -0300 Subject: [PATCH 1/5] Updating llvm-backend --- llvm-backend/src/main/native/llvm-backend | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 74bf6385ce..d7efaf7239 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 74bf6385cea9835c7f59628e028b45d635b59c74 +Subproject commit d7efaf7239988e601ade8c43df33e542e81651fa From 06a61b0b61a83c55baf2ff0ede8d5c3e2eb9325b Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 8 Jul 2025 18:12:14 -0300 Subject: [PATCH 2/5] Updating LIST module --- k-distribution/include/kframework/builtin/domains.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index ada7cad4e6..c036332e39 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -963,6 +963,7 @@ words, 0 is the first element and -1 is the last element. ```k syntax KItem ::= List "[" Int "]" [function, hook(LIST.get), symbol(List:get)] + syntax {Width} KItem ::= List "[" MInt{Width} "]" [function, hook(LIST.getMInt), symbol(List:getMInt)] ``` ### List update @@ -972,6 +973,7 @@ O(log(N)) time, or effectively constant. ```k syntax List ::= List "[" index: Int "<-" value: KItem "]" [function, hook(LIST.update), symbol(List:set)] + syntax {Width} List ::= List "[" index: MInt{Width} "<-" value: KItem "]" [function, hook(LIST.updateMInt), symbol(List:setMInt)] ``` ### List of identical elements @@ -1026,7 +1028,8 @@ comparisons, it is much better to first convert to a set using `List2Set`. You can get the number of elements of a list in O(1) time. ```k - syntax Int ::= size(List) [function, total, hook(LIST.size), symbol(sizeList), smtlib(smt_seq_len)] + syntax Int ::= size(List) [function, total, hook(LIST.size), symbol(sizeList), smtlib(smt_seq_len)] + syntax {Width} MInt{Width} ::= size(List) [function, total, hook(LIST.sizeMInt), symbol(sizeListMInt)] ``` ```k From dd1829bc69b1622d4bf601b09927e34b959b4b3a Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 8 Jul 2025 18:19:24 -0300 Subject: [PATCH 3/5] Implementing new K rules --- .../include/kframework/builtin/domains.md | 35 ++++++++++++++++--- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index c036332e39..bc17b46c5c 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2013,6 +2013,7 @@ endmodule module BYTES-HOOKED imports STRING-SYNTAX imports BYTES-SYNTAX + // imports MINT-SYNTAX imports BYTES-STRING-ENCODE ``` @@ -2095,15 +2096,17 @@ of the `Bytes` term). ```k syntax Bytes ::= Bytes "[" index: Int "<-" value: Int "]" [function, hook(BYTES.update)] + // syntax {Width} Bytes ::= Bytes "[" index: MInt{Width} "<-" value: MInt{Width} "]" [function, hook(BYTES.updateMInt)] ``` ### Bytes lookup -You can get the value of a particular byte in a `Bytes` object in O(1) time. +You can get the value of a particular byte in a `Bytes` object in O(1) time, either as an `Int` or as an `MInt`. Currently, only 64-bit and 256-bit `MInt` types are supported. The result is `#False` if `index` is not a valid index (see above). ```k syntax Int ::= Bytes "[" Int "]" [function, hook(BYTES.get)] + //syntax {Width} MInt{Width} ::= Bytes "[" MInt{Width} "]" [function, hook(BYTES.getMInt)] ``` ### Bytes substring @@ -2112,9 +2115,12 @@ You can get a new `Bytes` object containing a range of bytes from the input `Bytes` in O(N) time (where N is the length of the substring). The range of bytes included is `[startIndex..endIndex)`. The resulting `Bytes` is a copy and mutations to it do not affect mutations to the original `Bytes`. +Both `startIndex` and `endIndex` can be either `Int` or `MInt` values, but, +currently, only 64-bit and 256-bit `MInt` types are supported. ```k syntax Bytes ::= substrBytes(Bytes, startIndex: Int, endIndex: Int) [function, hook(BYTES.substr)] + // syntax {Width} Bytes ::= substrBytes(Bytes, startIndex: MInt{Width}, endIndex: MInt{Width}) [function, hook(BYTES.substrMInt)] ``` The function is not total: `substrBytes(B, startIndex, endIndex)` is `#Bottom` if @@ -2128,10 +2134,13 @@ 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. +`#False` if `index` + `N` is not a valid index. This function accepts both +`Int` and `MInt` values for `index` and `N`. Currently, only 64-bit and +256-bit `MInt` types are supported. ```k syntax Bytes ::= replaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, hook(BYTES.replaceAt)] +// syntax {Width} Bytes ::= replaceAtBytes(dest: Bytes, index: MInt{Width}, src: Bytes) [function, hook(BYTES.replaceAtMInt)] ``` ### Multiple bytes update @@ -2156,10 +2165,15 @@ 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. +We also provide a variant of this function which takes an `MInt` for the +`length` and `value`. The current implementation only supports 64-bit and +256-bit `MInt` types. ```k syntax Bytes ::= padRightBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padRight)] | padLeftBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padLeft)] + // syntax {Width} Bytes ::= padRightBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padRightMInt)] + // | padLeftBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padLeftMInt)] ``` ### Bytes reverse @@ -2174,10 +2188,12 @@ original. ### Bytes length -You can get the length of a `Bytes` term in O(1) time. +You can get the length of a `Bytes` term in O(1) time. The lenghth can be either +an `Int` or an `MInt`. Currently, only 64-bit and 256-bit `MInt` types are supported. ```k syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)] + /// syntax {Width} MInt{Width} ::= lengthBytes(Bytes) [function, total, hook(BYTES.lengthMInt)] ``` @@ -2868,6 +2884,7 @@ endmodule module MINT imports MINT-SYNTAX imports private INT + // imports private BYTES imports private BOOL ``` @@ -2899,6 +2916,14 @@ has the correct bitwidth, as this will influence the width of the resulting syntax {Width} MInt{Width} ::= Int2MInt(Int) [function, total, hook(MINT.integer), smt-hook(int2bv)] ``` +### Mint and Bytes conversion +You can convert from an `MInt` to a `Bytes` using the `MInt2Bytes` function. +Currently we only support converting `MInt`s of width 256 to `Bytes` in a Big Endian format. +```k + //syntax {Width} Bytes ::= MInt2Bytes(MInt{Width}) [function, total, hook(MINT.MInt2bytes)] + //syntax {Width} MInt{Width} ::= Bytes2MInt(Bytes) [function, total, hook(MINT.bytes2MInt)] +``` + ### MInt min and max values You can get the minimum and maximum values of a signed or unsigned `MInt` @@ -2941,6 +2966,7 @@ You can: * Compute the bitwise complement `~MInt` of an `MInt`. * Compute the unary negation `--MInt` of an `MInt`. +* Compute the power `^MInt` of two `MInt`s. Currently. Currently, only Width = 256-bits is supported. * Compute the product `*MInt` of two `MInt`s. * Compute the quotient `/sMInt` of two `MInt`s interpreted as signed integers. * Compute the modulus `%sMInt` of two `MInt`s interpreted as signed integers. @@ -2963,7 +2989,8 @@ You can: syntax {Width} MInt{Width} ::= "~MInt" MInt{Width} [function, total, hook(MINT.not), smt-hook(bvnot)] | "--MInt" MInt{Width} [function, total, hook(MINT.neg), smt-hook(bvuminus)] > left: - MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)] + // MInt{Width} "^MInt" MInt{Width} [function, total, hook(MINT.pow)] + MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)] | MInt{Width} "/sMInt" MInt{Width} [function, hook(MINT.sdiv), smt-hook(bvsdiv)] | MInt{Width} "%sMInt" MInt{Width} [function, hook(MINT.srem), smt-hook(bvsrem)] | MInt{Width} "/uMInt" MInt{Width} [function, hook(MINT.udiv), smt-hook(bvudiv)] From ada060f02425b61e843cfff85948f4ba341c7389 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 8 Jul 2025 18:27:12 -0300 Subject: [PATCH 4/5] Uncommenting hooks --- .../include/kframework/builtin/domains.md | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index bc17b46c5c..2e71f4d937 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2013,7 +2013,7 @@ endmodule module BYTES-HOOKED imports STRING-SYNTAX imports BYTES-SYNTAX - // imports MINT-SYNTAX + imports MINT-SYNTAX imports BYTES-STRING-ENCODE ``` @@ -2096,7 +2096,7 @@ of the `Bytes` term). ```k syntax Bytes ::= Bytes "[" index: Int "<-" value: Int "]" [function, hook(BYTES.update)] - // syntax {Width} Bytes ::= Bytes "[" index: MInt{Width} "<-" value: MInt{Width} "]" [function, hook(BYTES.updateMInt)] + syntax {Width} Bytes ::= Bytes "[" index: MInt{Width} "<-" value: MInt{Width} "]" [function, hook(BYTES.updateMInt)] ``` ### Bytes lookup @@ -2106,7 +2106,7 @@ The result is `#False` if `index` is not a valid index (see above). ```k syntax Int ::= Bytes "[" Int "]" [function, hook(BYTES.get)] - //syntax {Width} MInt{Width} ::= Bytes "[" MInt{Width} "]" [function, hook(BYTES.getMInt)] + syntax {Width} MInt{Width} ::= Bytes "[" MInt{Width} "]" [function, hook(BYTES.getMInt)] ``` ### Bytes substring @@ -2120,7 +2120,7 @@ currently, only 64-bit and 256-bit `MInt` types are supported. ```k syntax Bytes ::= substrBytes(Bytes, startIndex: Int, endIndex: Int) [function, hook(BYTES.substr)] - // syntax {Width} Bytes ::= substrBytes(Bytes, startIndex: MInt{Width}, endIndex: MInt{Width}) [function, hook(BYTES.substrMInt)] + syntax {Width} Bytes ::= substrBytes(Bytes, startIndex: MInt{Width}, endIndex: MInt{Width}) [function, hook(BYTES.substrMInt)] ``` The function is not total: `substrBytes(B, startIndex, endIndex)` is `#Bottom` if @@ -2140,7 +2140,7 @@ object and will instead modify the original on concrete backends. The result is ```k syntax Bytes ::= replaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, hook(BYTES.replaceAt)] -// syntax {Width} Bytes ::= replaceAtBytes(dest: Bytes, index: MInt{Width}, src: Bytes) [function, hook(BYTES.replaceAtMInt)] + syntax {Width} Bytes ::= replaceAtBytes(dest: Bytes, index: MInt{Width}, src: Bytes) [function, hook(BYTES.replaceAtMInt)] ``` ### Multiple bytes update @@ -2172,8 +2172,8 @@ We also provide a variant of this function which takes an `MInt` for the ```k syntax Bytes ::= padRightBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padRight)] | padLeftBytes(Bytes, length: Int, value: Int) [function, hook(BYTES.padLeft)] - // syntax {Width} Bytes ::= padRightBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padRightMInt)] - // | padLeftBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padLeftMInt)] + syntax {Width} Bytes ::= padRightBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padRightMInt)] + | padLeftBytes(Bytes, length: MInt{Width}, value: MInt{Width}) [function, hook(BYTES.padLeftMInt)] ``` ### Bytes reverse @@ -2193,7 +2193,7 @@ an `Int` or an `MInt`. Currently, only 64-bit and 256-bit `MInt` types are suppo ```k syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)] - /// syntax {Width} MInt{Width} ::= lengthBytes(Bytes) [function, total, hook(BYTES.lengthMInt)] + syntax {Width} MInt{Width} ::= lengthBytes(Bytes) [function, total, hook(BYTES.lengthMInt)] ``` @@ -2920,8 +2920,8 @@ has the correct bitwidth, as this will influence the width of the resulting You can convert from an `MInt` to a `Bytes` using the `MInt2Bytes` function. Currently we only support converting `MInt`s of width 256 to `Bytes` in a Big Endian format. ```k - //syntax {Width} Bytes ::= MInt2Bytes(MInt{Width}) [function, total, hook(MINT.MInt2bytes)] - //syntax {Width} MInt{Width} ::= Bytes2MInt(Bytes) [function, total, hook(MINT.bytes2MInt)] + syntax {Width} Bytes ::= MInt2Bytes(MInt{Width}) [function, total, hook(MINT.MInt2bytes)] + syntax {Width} MInt{Width} ::= Bytes2MInt(Bytes) [function, total, hook(MINT.bytes2MInt)] ``` ### MInt min and max values @@ -2989,8 +2989,8 @@ You can: syntax {Width} MInt{Width} ::= "~MInt" MInt{Width} [function, total, hook(MINT.not), smt-hook(bvnot)] | "--MInt" MInt{Width} [function, total, hook(MINT.neg), smt-hook(bvuminus)] > left: - // MInt{Width} "^MInt" MInt{Width} [function, total, hook(MINT.pow)] - MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)] + MInt{Width} "^MInt" MInt{Width} [function, total, hook(MINT.pow)] + | MInt{Width} "*MInt" MInt{Width} [function, total, hook(MINT.mul), smt-hook(bvmul)] | MInt{Width} "/sMInt" MInt{Width} [function, hook(MINT.sdiv), smt-hook(bvsdiv)] | MInt{Width} "%sMInt" MInt{Width} [function, hook(MINT.srem), smt-hook(bvsrem)] | MInt{Width} "/uMInt" MInt{Width} [function, hook(MINT.udiv), smt-hook(bvudiv)] From 9fd16ffe9f64321da60fda3b9306950ea4262beb Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 8 Jul 2025 18:28:15 -0300 Subject: [PATCH 5/5] Uncommenting import --- 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 2e71f4d937..cb9c276543 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -2884,7 +2884,7 @@ endmodule module MINT imports MINT-SYNTAX imports private INT - // imports private BYTES + imports private BYTES imports private BOOL ```