From 9c374d12dd6ef1af2088096eec227b73b8bfc074 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 23 Jun 2025 22:38:49 +0800 Subject: [PATCH 01/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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: Thu, 26 Jun 2025 19:37:04 +0800 Subject: [PATCH 10/14] Refine documentation for #WB operations in RISC-V semantics. Clarify termination control, reordering for optimization, and write consolidation strategies. Update code examples for better understanding and consistency. --- .../lemmas/sparse-bytes-simplifications.md | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 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 4da94c96..564696f4 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -34,36 +34,39 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` 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)] +``` +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. + +```k 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] +``` + +**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. - // Termination Control +```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)] +``` + +**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. - // Reordering for Optimization +```k 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, 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 +**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 #WB(false, I0, V0, NUM0, #WB(_, I1, _, NUM1, B:SparseBytes)) => #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) From 7d44f01628fd8ae2049f04eb936f7982036e03b0 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 26 Jun 2025 19:39:20 +0800 Subject: [PATCH 11/14] Clarify special case handling in #WB operations for RISC-V semantics. Update documentation to emphasize the reordering optimization and the specific rule for merging operations with identical indices. Improve code examples for better clarity. --- .../riscv-semantics/lemmas/sparse-bytes-simplifications.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 564696f4..b9adb6fb 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -56,10 +56,15 @@ If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike 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. 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. +**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. ```k 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] +``` + +The following rule tackles 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. + +```k 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] ``` From a9988ce886c897176acff3010109352d9cf8891f Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Thu, 3 Jul 2025 13:22:07 +0800 Subject: [PATCH 12/14] Add requires clause --- .../kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md | 1 + 1 file changed, 1 insertion(+) 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 b9adb6fb..cc8aebb4 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -60,6 +60,7 @@ If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike ```k 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] + requires I0 =/=Int I1 ``` The following rule tackles 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. From b29dce7f26e45c8f014fdc67a134fd4c202f0fb7 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 7 Jul 2025 10:45:10 +0800 Subject: [PATCH 13/14] Refactor #WB operation rule in RISC-V semantics documentation. Adjusted the placement of the `requires` clause for clarity and consistency in simplification rules. --- .../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 cc8aebb4..428e05ae 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -59,8 +59,8 @@ If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike **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. ```k - 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] - requires I0 =/=Int I1 + rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) + requires I0 =/=Int I1 [simplification] ``` The following rule tackles 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. From 9b3d348144d0ba3bfc66dd27e05336847598e836 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 7 Jul 2025 11:05:08 +0800 Subject: [PATCH 14/14] remove the require clause. --- .../riscv-semantics/lemmas/sparse-bytes-simplifications.md | 3 +-- 1 file changed, 1 insertion(+), 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 428e05ae..b9adb6fb 100644 --- a/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md +++ b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md @@ -59,8 +59,7 @@ If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike **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. ```k - rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) - requires I0 =/=Int I1 [simplification] + 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] ``` The following rule tackles 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.