From 9c374d12dd6ef1af2088096eec227b73b8bfc074 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Jun 2025 22:38:49 +0800 Subject: [PATCH 01/13] Write symbolic value at symbolic index --- .../lemmas/sparse-bytes-simplifications.md | 28 +++++++++++++++++++ .../kdist/riscv-semantics/sparse-bytes.md | 4 +-- .../specs/store-symbolic-index-value.k | 21 ++++++++++++++ 3 files changed, 51 insertions(+), 2 deletions(-) create mode 100644 src/tests/integration/test-data/specs/store-symbolic-index-value.k diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index eea9fe9d..ff21cb03 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -30,6 +30,34 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` requires I >=Int lengthBytes(B) [simplification(45), preserves-definedness] ``` +## writeBytes + +```k + rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)] + rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)] + + syntax SparseBytes ::= #WB(Bool, Int, Int, Int, SparseBytes) [function, total] + rule #WB(_, I, V, NUM, B:SparseBytes) => writeBytes(I, V, NUM, B) [concrete] + rule writeBytes(I, V, NUM, B:SparseBytes) => #WB(false, I, V, NUM, B) [simplification, symbolic(I)] + + // termination + rule #WB(false, I, V, NUM, BF:SparseBytesBF) => #WB(true, I, V, NUM, BF) [simplification] + rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF) [simplification] + + // down to the terminal case + rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification] + rule #WB(false, I, V0, NUM0, #WB(true, I, V1, NUM1, B:SparseBytes)) => #WB(true, I, V0, NUM0, #WB(true, I, V1, NUM1, B)) [simplification] + + // Merge write operations with the same index + rule #WB(false, I, V, NUM, #WB(_, I, _, NUM, B:SparseBytes)) => #WB(false, I, V, NUM, B) [simplification(45)] + rule #WB(false, I, V0, NUM0, #WB(_, I, V1, NUM1, B:SparseBytes)) => + #WB(false, I, V0, NUM0, #WB(false, I +Int NUM0, V1 >>Int (NUM0 *Int 8), NUM1 -Int NUM0, B)) + requires NUM0 #WB(false, I, V0, NUM0, B) + requires NUM1 writeBytesBF(I, V, NUM, BF) - rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) + rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [concrete] + rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [concrete] rule writeBytesEF(I, _, _ , _ ) => .SparseBytes requires I prependEmpty(I, #bytes(Int2Bytes(NUM, V, LE)) .SparseBytes) requires I >=Int 0 diff --git a/src/tests/integration/test-data/specs/store-symbolic-index-value.k b/src/tests/integration/test-data/specs/store-symbolic-index-value.k new file mode 100644 index 00000000..ff515598 --- /dev/null +++ b/src/tests/integration/test-data/specs/store-symbolic-index-value.k @@ -0,0 +1,21 @@ +module STORE-SYMBOLIC-INDEX-VALUE + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + + .Map + + 0 + + storeBytes(I2, V5, 4, + storeBytes(I1, V4, 2, + storeBytes(I0, V3, 4, + storeBytes(I2, V2, 2, + storeBytes(I1, V1, 4, + storeBytes(I0, V0, 4, #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes)))))) + => // No way to simplify this without any information about the index. Just eliminate the writes on the same index. + #WB (true, I1, V4, 2, #WB (true, I1, V1, 4, #WB (true, I0, V3, 4, #WB (true, I2, V5, 4, #bytes (b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))) + + ADDRESS ( 0 ) +endmodule From abb1cb8ef3e282941b315d47cfb20ba4c0620a62 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 23 Jun 2025 14:40:06 +0000 Subject: [PATCH 02/13] Set Version: 0.1.113 --- package/version | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 4b9b35d8..c21e67e6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.112 +0.1.113 diff --git a/pyproject.toml b/pyproject.toml index 8ab7642a..30b13bdd 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kriscv" -version = "0.1.112" +version = "0.1.113" description = "K tooling for the RISC-V architecture" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index 1351fded..fe1f6a2b 100644 --- a/uv.lock +++ b/uv.lock @@ -643,7 +643,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.112" +version = "0.1.113" source = { editable = "." } dependencies = [ { name = "filelock" }, From 3763e0bf3b51db8f6cb7bd1bd269aa1d55439a47 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Tue, 24 Jun 2025 09:36:12 +0800 Subject: [PATCH 03/13] Update src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md --- .../riscv-semantics/lemmas/sparse-bytes-simplifications.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index ff21cb03..2e3edfa9 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -51,8 +51,6 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` // Merge write operations with the same index rule #WB(false, I, V, NUM, #WB(_, I, _, NUM, B:SparseBytes)) => #WB(false, I, V, NUM, B) [simplification(45)] rule #WB(false, I, V0, NUM0, #WB(_, I, V1, NUM1, B:SparseBytes)) => - #WB(false, I, V0, NUM0, #WB(false, I +Int NUM0, V1 >>Int (NUM0 *Int 8), NUM1 -Int NUM0, B)) - requires NUM0 #WB(false, I, V0, NUM0, B) requires NUM1 Date: Tue, 24 Jun 2025 09:40:09 +0800 Subject: [PATCH 04/13] fix --- .../riscv-semantics/lemmas/sparse-bytes-simplifications.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index 2e3edfa9..5754d4ca 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -49,8 +49,8 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` rule #WB(false, I, V0, NUM0, #WB(true, I, V1, NUM1, B:SparseBytes)) => #WB(true, I, V0, NUM0, #WB(true, I, V1, NUM1, B)) [simplification] // Merge write operations with the same index - rule #WB(false, I, V, NUM, #WB(_, I, _, NUM, B:SparseBytes)) => #WB(false, I, V, NUM, B) [simplification(45)] - rule #WB(false, I, V0, NUM0, #WB(_, I, V1, NUM1, B:SparseBytes)) => + rule #WB(false, I, V, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V, NUM0, B) + requires NUM0 ==Int NUM1 [simplification(45)] rule #WB(false, I, V0, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V0, NUM0, B) requires NUM1 Date: Tue, 24 Jun 2025 09:40:42 +0800 Subject: [PATCH 05/13] format --- .../riscv-semantics/lemmas/sparse-bytes-simplifications.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index 5754d4ca..5571c92b 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -52,9 +52,7 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` rule #WB(false, I, V, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V, NUM0, B) requires NUM0 ==Int NUM1 [simplification(45)] rule #WB(false, I, V0, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V0, NUM0, B) - requires NUM1 Date: Tue, 24 Jun 2025 10:02:46 +0800 Subject: [PATCH 06/13] Enhance simplification rules in RISC-V semantics for writeBytes and #WB operations. Update test data to include symbolic index value handling in storeBytes. Adjust formatting for clarity. --- .../lemmas/sparse-bytes-simplifications.md | 16 +++++++++------- .../test-data/specs/store-symbolic-index-value.k | 10 ++++++++-- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index 5571c92b..3aadd3f6 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -33,16 +33,18 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` ## writeBytes ```k - rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)] - rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)] + rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification(45), concrete(I)] + rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification(45), concrete(I)] syntax SparseBytes ::= #WB(Bool, Int, Int, Int, SparseBytes) [function, total] - rule #WB(_, I, V, NUM, B:SparseBytes) => writeBytes(I, V, NUM, B) [concrete] - rule writeBytes(I, V, NUM, B:SparseBytes) => #WB(false, I, V, NUM, B) [simplification, symbolic(I)] + rule #WB(_, I, V, NUM, B:SparseBytes) => writeBytes(I, V, NUM, B) [concrete] + rule writeBytes(I, V, NUM, B:SparseBytes) => #WB(false, I, V, NUM, B) [simplification] // termination - rule #WB(false, I, V, NUM, BF:SparseBytesBF) => #WB(true, I, V, NUM, BF) [simplification] - rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF) [simplification] + rule #WB(false, I, V, NUM, BF:SparseBytesBF) => #WB(true, I, V, NUM, BF) [simplification] + rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF) [simplification] + rule #WB(true, I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)] + rule #WB(true, I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)] // down to the terminal case rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification] @@ -52,7 +54,7 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` rule #WB(false, I, V, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V, NUM0, B) requires NUM0 ==Int NUM1 [simplification(45)] rule #WB(false, I, V0, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V0, NUM0, B) - requires NUM1 0 + storeBytes(0 , V6, 4, storeBytes(I2, V5, 4, storeBytes(I1, V4, 2, storeBytes(I0, V3, 4, storeBytes(I2, V2, 2, storeBytes(I1, V1, 4, - storeBytes(I0, V0, 4, #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes)))))) + storeBytes(I0, V0, 4, #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes))))))) => // No way to simplify this without any information about the index. Just eliminate the writes on the same index. - #WB (true, I1, V4, 2, #WB (true, I1, V1, 4, #WB (true, I0, V3, 4, #WB (true, I2, V5, 4, #bytes (b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))) + #WB(true, I1, V4, 2, + #WB(true, I1, V1, 4, + #WB(true, I0, V3, 4, + #WB(true, I2, V5, 4, + #bytes (Int2Bytes(4, V6, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))) ADDRESS ( 0 ) + // requires 0 =/=Int I0 andBool 0 =/=Int I1 andBool 0 =/=Int I2 endmodule From 36f61a06da16e199c4461f62152a835f160239ee Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 24 Jun 2025 10:04:34 +0800 Subject: [PATCH 07/13] delete uneccesary side condition --- .../integration/test-data/specs/store-symbolic-index-value.k | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tests/integration/test-data/specs/store-symbolic-index-value.k b/src/tests/integration/test-data/specs/store-symbolic-index-value.k index 7ac4699d..31192b8c 100644 --- a/src/tests/integration/test-data/specs/store-symbolic-index-value.k +++ b/src/tests/integration/test-data/specs/store-symbolic-index-value.k @@ -23,5 +23,4 @@ module STORE-SYMBOLIC-INDEX-VALUE #bytes (Int2Bytes(4, V6, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))) ADDRESS ( 0 ) - // requires 0 =/=Int I0 andBool 0 =/=Int I1 andBool 0 =/=Int I2 endmodule From 2d3d815adc52578cfc673923e6f33556a137d410 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Jun 2025 10:44:32 +0800 Subject: [PATCH 08/13] Enhance writeBytes and #WB operations in RISC-V semantics by introducing a boolean wrapper for symbolic writes. This update includes detailed explanations of termination control, reordering for optimization, and write consolidation strategies. Adjusted comments for clarity and improved documentation. --- .../lemmas/sparse-bytes-simplifications.md | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index 3aadd3f6..28130036 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -32,6 +32,18 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` ## writeBytes +If the write index is concrete, we can directly call `writeBytesBF` or `writeBytesEF`. + +If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike `writeBytes`, `#WB` contains a boolean value to determine whether the write operation has been completed. `true` means completed, `false` means not completed. + +The `#WB` wrapper serves several purposes: + +1. **Termination Control**: The boolean flag ensures that symbolic write operations eventually terminate by transitioning from `false` to `true` state, at which point concrete write functions can be applied when the index becomes concrete. + +2. **Reordering for Optimization**: When multiple `#WB` operations are nested, the rules bring incomplete `#WB` operations (with `false` flag) to the terminal position, allowing them to traverse and find all possible merge opportunities. There is a special case when indices are the same but `NUM0 < NUM1`: in this situation, merging would introduce additional terms, so the operation is directly marked as completed to avoid complexity. + +3. **Write Consolidation**: When multiple write operations target the same symbolic index with equal byte counts (`NUM0 == NUM1`), the rules merge them by eliminating the older write operation. When the new write has fewer bytes than the existing one (`NUM1 < NUM0`), the smaller write is also eliminated to maintain simplicity. + ```k rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification(45), concrete(I)] rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification(45), concrete(I)] @@ -40,17 +52,17 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` rule #WB(_, I, V, NUM, B:SparseBytes) => writeBytes(I, V, NUM, B) [concrete] rule writeBytes(I, V, NUM, B:SparseBytes) => #WB(false, I, V, NUM, B) [simplification] - // termination + // Termination Control rule #WB(false, I, V, NUM, BF:SparseBytesBF) => #WB(true, I, V, NUM, BF) [simplification] rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF) [simplification] rule #WB(true, I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)] rule #WB(true, I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)] - // down to the terminal case + // Reordering for Optimization rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification] rule #WB(false, I, V0, NUM0, #WB(true, I, V1, NUM1, B:SparseBytes)) => #WB(true, I, V0, NUM0, #WB(true, I, V1, NUM1, B)) [simplification] - // Merge write operations with the same index + // Write Consolidation rule #WB(false, I, V, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V, NUM0, B) requires NUM0 ==Int NUM1 [simplification(45)] rule #WB(false, I, V0, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V0, NUM0, B) From d95f68c966daede7a26ffb6d503135a4cc0c3b5b Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 25 Jun 2025 10:48:48 +0800 Subject: [PATCH 09/13] bring ==Int to the require clause for more general cases --- .../lemmas/sparse-bytes-simplifications.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index 28130036..4da94c96 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -60,13 +60,14 @@ The `#WB` wrapper serves several purposes: // Reordering for Optimization rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) [simplification] - rule #WB(false, I, V0, NUM0, #WB(true, I, V1, NUM1, B:SparseBytes)) => #WB(true, I, V0, NUM0, #WB(true, I, V1, NUM1, B)) [simplification] + rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B)) + requires I0 ==Int I1 [simplification] // Write Consolidation - rule #WB(false, I, V, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V, NUM0, B) - requires NUM0 ==Int NUM1 [simplification(45)] - rule #WB(false, I, V0, NUM0, #WB(_, I, _, NUM1, B:SparseBytes)) => #WB(false, I, V0, NUM0, B) - requires NUM1 #WB(false, I0, V0, NUM0, B) + requires NUM0 ==Int NUM1 andBool I0 ==Int I1 [simplification(45)] + rule #WB(false, I0, V0, NUM0, #WB(_, I1, _, NUM1, B:SparseBytes)) => #WB(false, I0, V0, NUM0, B) + requires NUM1 Date: Tue, 24 Jun 2025 18:38:44 +0800 Subject: [PATCH 10/13] Read symbolic value at symbolic address --- .../lemmas/sparse-bytes-simplifications.md | 17 +++++ .../specs/read-symbolic-index-value.k | 62 +++++++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 src/tests/integration/test-data/specs/read-symbolic-index-value.k diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index 4da94c96..d4161777 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -28,6 +28,23 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` requires I >Int 0 andBool I dropFront(I -Int lengthBytes(B), #bytes(BS) EF) requires I >=Int lengthBytes(B) [simplification(45), preserves-definedness] + + // pickFront and dropFront for #WB + rule pickFront(PICK, #WB(_, _, _, _, B:SparseBytes)) => pickFront(PICK, B) + // omit this condition to make it easy to simplify: requires 0 =/=Int I + [simplification(45)] + rule pickFront(PICK, #WB(_, I, V, NUM, B:SparseBytes)) => Int2Bytes(minInt(PICK, NUM), V, LE) +Bytes pickFront(maxInt(0, PICK -Int NUM), B >>SparseBytes minInt(PICK, NUM)) + requires 0 ==Int I [simplification(40)] + rule dropFront(DROP, #WB(FLAG, I, V, NUM, B:SparseBytes)) => #WB(FLAG, I -Int DROP, V, NUM, dropFront(DROP, B)) + [simplification(45)] + + + syntax SparseBytes ::= SparseBytes ">>SparseBytes" Int [function, total] + // It's not correct, but just make this function total + rule B >>SparseBytes _ => B [concrete] + rule #WB(FLAG, I, V, NUM, B:SparseBytes) >>SparseBytes SHIFT => #WB(FLAG, I, (V &Int (2 ^Int (NUM *Int 8)) -Int 1) >>Int (SHIFT *Int 8), NUM, B >>SparseBytes SHIFT) + requires SHIFT >=Int 0 [simplification(45), preserves-definedness] + rule B:SparseBytes >>SparseBytes _ => B [simplification] ``` ## writeBytes diff --git a/src/tests/integration/test-data/specs/read-symbolic-index-value.k b/src/tests/integration/test-data/specs/read-symbolic-index-value.k new file mode 100644 index 00000000..613a1b92 --- /dev/null +++ b/src/tests/integration/test-data/specs/read-symbolic-index-value.k @@ -0,0 +1,62 @@ +module READ-SYMBOLIC-INDEX-VALUE + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + + // read from #bytes + 1 |-> (readBytes(4, 4, + #WB(true, I1, V0, 2, + #WB(true, I1, V1, 4, + #WB(true, I0, V2, 4, + #WB(true, I2, V3, 4, + #bytes (b"\x00\x00\x00\x00" +Bytes Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))) + => V4) + // read I2 with same number of bytes + 2 |-> (readBytes(I2, 4, + #WB(true, I1, V0, 2, + #WB(true, I1, V1, 4, + #WB(true, I0, V2, 4, + #WB(true, I2, V3, 4, + #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))) + => V3) + // read I2 with smaller number of bytes + 3 |-> (readBytes(I2, 2, + #WB(true, I1, V0, 2, + #WB(true, I1, V1, 4, + #WB(true, I0, V2, 4, + #WB(true, I2, V3, 4, + #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))) + => V3 &Int 65535) + // DISALLOWED: read with more number of bytes (8 bytes, but only 4 stored) + // read I1 with 2 bytes + 4 |-> (readBytes(I1, 2, + #WB(true, I1, V0, 2, + #WB(true, I1, V1, 4, + #WB(true, I0, V2, 4, + #WB(true, I2, V3, 4, + #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))) + => V0 &Int 65535) + // read I1 with 4 bytes + 5 |-> (readBytes(I1, 4, + #WB(true, I1, V0, 2, + #WB(true, I1, V1, 4, + #WB(true, I0, V2, 4, + #WB(true, I2, V3, 4, + #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))) + => Bytes2Int(Int2Bytes(2, V0, LE) +Bytes Int2Bytes(2, V1 >>Int 16, LE), LE, Unsigned)) + + 0 + ADDRESS ( 0 ) + // index not equal to 0 + requires 4 =/=Int I0 andBool 4 =/=Int I1 andBool 4 =/=Int I2 + // different indices + andBool I0 =/=Int I1 andBool I0 =/=Int I2 andBool I1 =/=Int I2 + // values are within range + andBool 0 <=Int V0 andBool V0 <=Int 65535 + andBool 0 <=Int V1 andBool V1 <=Int 4294967295 + andBool 0 <=Int V2 andBool V2 <=Int 4294967295 + andBool 0 <=Int V3 andBool V3 <=Int 4294967295 + andBool 0 <=Int V4 andBool V4 <=Int 4294967295 +endmodule + From 8c9abddb66dc0b6af4598a5866c0f901a5577f45 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 24 Jun 2025 10:39:58 +0000 Subject: [PATCH 11/13] Set Version: 0.1.114 --- package/version | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index c21e67e6..c29f5f75 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.113 +0.1.114 diff --git a/pyproject.toml b/pyproject.toml index 30b13bdd..44a23b14 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kriscv" -version = "0.1.113" +version = "0.1.114" description = "K tooling for the RISC-V architecture" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index fe1f6a2b..1d1bd3ce 100644 --- a/uv.lock +++ b/uv.lock @@ -643,7 +643,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.113" +version = "0.1.114" source = { editable = "." } dependencies = [ { name = "filelock" }, From 3503ce4b5c326232d2c5123d002a0e672e6c9ca0 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 9 Jul 2025 08:14:53 +0000 Subject: [PATCH 12/13] Set Version: 0.1.114 --- package/version | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index c21e67e6..c29f5f75 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.113 +0.1.114 diff --git a/pyproject.toml b/pyproject.toml index 30b13bdd..44a23b14 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kriscv" -version = "0.1.113" +version = "0.1.114" description = "K tooling for the RISC-V architecture" readme = "README.md" requires-python = "~=3.10" diff --git a/uv.lock b/uv.lock index fe1f6a2b..1d1bd3ce 100644 --- a/uv.lock +++ b/uv.lock @@ -643,7 +643,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.113" +version = "0.1.114" source = { editable = "." } dependencies = [ { name = "filelock" }, From 249b06183a512b229073b7963cf748331117c1a6 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 10 Jul 2025 13:52:27 +0800 Subject: [PATCH 13/13] Enhance RISC-V semantics with new simplification rules for integer operations and symbolic write blocks. Added a rule for 16-bit integer simplification and improved handling of pickFront and dropFront operations on symbolic write blocks. Updated test cases to reflect changes in symbolic index handling. --- .../lemmas/int-simplifications.md | 1 + .../lemmas/sparse-bytes-simplifications.md | 47 +++++++++++++------ .../specs/read-symbolic-index-value.k | 7 +-- 3 files changed, 36 insertions(+), 19 deletions(-) diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md index 1dcc1499..67f9e735 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md @@ -26,6 +26,7 @@ module INT-SIMPLIFICATIONS [symbolic] ```k rule [chop-32bits]: X &Int 4294967295 => X requires 0 <=Int X andBool X X requires 0 <=Int X andBool X X &Int (Y &Int Z) [simplification, symbolic(X), concrete(Y,Z)] rule [int-and-add-assoc-8]: ((X &Int 255) +Int Y) &Int 255 => (X +Int Y) &Int 255 [simplification] diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index d38f6214..95716074 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -28,23 +28,41 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` requires I >Int 0 andBool I dropFront(I -Int lengthBytes(B), #bytes(BS) EF) requires I >=Int lengthBytes(B) [simplification(45), preserves-definedness] - - // pickFront and dropFront for #WB - rule pickFront(PICK, #WB(_, _, _, _, B:SparseBytes)) => pickFront(PICK, B) - // omit this condition to make it easy to simplify: requires 0 =/=Int I +``` + +Simplification rules for pickFront and dropFront operations on symbolic write blocks (#WB) +- Default case: For most symbolic write operations, we can bypass the #WB wrapper and apply pickFront directly to the underlying byte structure +```k + rule pickFront(PICK, #WB(_, I, _, _, B:SparseBytes)) => pickFront(PICK, B) + requires PICK <=Int I [simplification(45)] +``` +- Special case for zero-indexed writes: When a write starts at position 0, we must combine bytes from both the written value and the remaining underlying structure +```k rule pickFront(PICK, #WB(_, I, V, NUM, B:SparseBytes)) => Int2Bytes(minInt(PICK, NUM), V, LE) +Bytes pickFront(maxInt(0, PICK -Int NUM), B >>SparseBytes minInt(PICK, NUM)) requires 0 ==Int I [simplification(40)] +``` +- Front-dropping with symbolic writes: Adjust both the write offset and apply dropFront to the underlying structure to maintain correct relative positioning +```k rule dropFront(DROP, #WB(FLAG, I, V, NUM, B:SparseBytes)) => #WB(FLAG, I -Int DROP, V, NUM, dropFront(DROP, B)) [simplification(45)] +``` - +## Right Shift Operations + +The `>>SparseBytes` operator performs a right shift operation on SparseBytes, effectively dropping the first N bytes from the sparse byte structure while maintaining the integer value semantics of the remaining bytes. Unlike `dropFront`, which simply removes N bytes from the beginning, `>>SparseBytes` performs a byte-level right shift that preserves the underlying integer representation of the data. + +This is primarily used in `pickFront` operations when we need to extract bytes from a specific offset within the sparse byte structure. + +```k syntax SparseBytes ::= SparseBytes ">>SparseBytes" Int [function, total] - // It's not correct, but just make this function total - rule B >>SparseBytes _ => B [concrete] - rule #WB(FLAG, I, V, NUM, B:SparseBytes) >>SparseBytes SHIFT => #WB(FLAG, I, (V &Int (2 ^Int (NUM *Int 8)) -Int 1) >>Int (SHIFT *Int 8), NUM, B >>SparseBytes SHIFT) + + // For concrete sparse bytes, we can directly use dropFront to simplify the operation + rule SBS >>SparseBytes SHIFT => dropFront(SHIFT, SBS) [concrete] + + // Symbolic write case: Adjust the written value by right-shifting and recursively apply to underlying structure + rule #WB(FLAG, I, V, NUM, B:SparseBytes) >>SparseBytes SHIFT => #WB(FLAG, maxInt(0, I -Int SHIFT), V >>Int (SHIFT *Int 8), NUM, B >>SparseBytes SHIFT) requires SHIFT >=Int 0 [simplification(45), preserves-definedness] - rule B:SparseBytes >>SparseBytes _ => B [simplification] ``` ## writeBytes @@ -67,10 +85,11 @@ If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike **Termination Control**: The boolean flag ensures that symbolic write operations eventually terminate by transitioning from `false` to `true` state, at which point concrete write functions can be applied when the index becomes concrete. ```k - rule #WB(false, I, V, NUM, BF:SparseBytesBF) => #WB(true, I, V, NUM, BF) [simplification] - rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF) [simplification] - rule #WB(true, I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)] - rule #WB(true, I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)] + rule #WB(_, I, _, NUM, B:SparseBytes) => B requires I #WB(true, I, V, NUM, BF) [simplification] + rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF) [simplification] + rule #WB(true, I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)] + rule #WB(true, I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)] ``` **Reordering for Optimization**: When multiple `#WB` operations are nested, the rules bring incomplete `#WB` operations (with `false` flag) to the terminal position, allowing them to traverse and find all possible merge opportunities. @@ -93,7 +112,7 @@ The rule below handles a termination edge case: it immediately marks the operati requires I0 <=Int I1 andBool I1 +Int NUM1 <=Int I0 +Int NUM0 [simplification(45)] ``` -## writeByteBF +## writeBytesBF To write a byte to a symbolic sparse byte region, we need to: diff --git a/src/tests/integration/test-data/specs/read-symbolic-index-value.k b/src/tests/integration/test-data/specs/read-symbolic-index-value.k index 613a1b92..6bf43d08 100644 --- a/src/tests/integration/test-data/specs/read-symbolic-index-value.k +++ b/src/tests/integration/test-data/specs/read-symbolic-index-value.k @@ -36,7 +36,7 @@ module READ-SYMBOLIC-INDEX-VALUE #WB(true, I0, V2, 4, #WB(true, I2, V3, 4, #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))) - => V0 &Int 65535) + => V0) // read I1 with 4 bytes 5 |-> (readBytes(I1, 4, #WB(true, I1, V0, 2, @@ -48,10 +48,7 @@ module READ-SYMBOLIC-INDEX-VALUE 0 ADDRESS ( 0 ) - // index not equal to 0 - requires 4 =/=Int I0 andBool 4 =/=Int I1 andBool 4 =/=Int I2 - // different indices - andBool I0 =/=Int I1 andBool I0 =/=Int I2 andBool I1 =/=Int I2 + requires 8