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/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md index eea9fe9d..03206f83 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,51 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` requires I >=Int lengthBytes(B) [simplification(45), preserves-definedness] ``` +## writeBytes + +If the write index is concrete, we can directly call `writeBytesBF` or `writeBytesEF`. + +```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. + +```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. + +```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 NUM0 <=Int I1 orBool I1 +Int NUM1 <=Int I0 [simplification] +``` + +The rule below handles a termination edge case: it immediately marks the operation as complete with reduced priority to avoid infinite rewriting cycles. + +```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)) [simplification(60)] +``` + +**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 I0 <=Int I1 andBool I1 +Int NUM1 <=Int I0 +Int NUM0 [simplification(45)] +``` ## writeByteBF diff --git a/src/kriscv/kdist/riscv-semantics/sparse-bytes.md b/src/kriscv/kdist/riscv-semantics/sparse-bytes.md index 716598ff..6106b4ac 100644 --- a/src/kriscv/kdist/riscv-semantics/sparse-bytes.md +++ b/src/kriscv/kdist/riscv-semantics/sparse-bytes.md @@ -87,8 +87,8 @@ We provide helpers to prepend either data or an empty region to an existing `Spa | writeBytesEF(Int, Int, Int, SparseBytesEF) [function, total] | writeBytesBF(Int, Int, Int, SparseBytesBF) [function, total] - rule writeBytes(I, V, NUM, BF:SparseBytesBF) => 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-overlap-counter.k b/src/tests/integration/test-data/specs/store-symbolic-index-overlap-counter.k new file mode 100644 index 00000000..9876ae43 --- /dev/null +++ b/src/tests/integration/test-data/specs/store-symbolic-index-overlap-counter.k @@ -0,0 +1,21 @@ +module STORE-SYMBOLIC-INDEX-OVERLAP-COUNTER + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + + .Map + + 0 + + // Perfect overlapping writes - I0's write completely covers I1's write + storeBytes(I0, V1, 2, + storeBytes(I1, V0, 1, #bytes ( b"\x00\x00" ) .SparseBytes)) + => + // Only I0's write remains since it completely covers I1's write + #WB(true, I0, V1, 2, #bytes ( b"\x00\x00" ) .SparseBytes) + + ADDRESS ( 0 ) + requires // Perfect overlapping case: I1 is completely within I0's write range + I0 <=Int I1 andBool I1 +Int 1 <=Int I0 +Int 2 // I1's write [I1, I1+1) is within I0's write [I0, I0+2) +endmodule \ No newline at end of file diff --git a/src/tests/integration/test-data/specs/store-symbolic-index-partial-overlap.k b/src/tests/integration/test-data/specs/store-symbolic-index-partial-overlap.k new file mode 100644 index 00000000..c5cc229e --- /dev/null +++ b/src/tests/integration/test-data/specs/store-symbolic-index-partial-overlap.k @@ -0,0 +1,22 @@ +module STORE-SYMBOLIC-INDEX-PARTIAL-OVERLAP + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + + .Map + + 0 + + // Partial overlapping writes - only part of the writes overlap + storeBytes(I0, V1, 2, + storeBytes(I1, V0, 2, #bytes ( b"\x00\x00\x00\x00" ) .SparseBytes)) + => + // Ordering is preserved + #WB(true, I0, V1, 2, + #WB(true, I1, V0, 2, #bytes ( b"\x00\x00\x00\x00" ) .SparseBytes)) + + ADDRESS ( 0 ) + requires // Partial overlapping case: I0 starts 1 byte after I1, so they overlap by 1 byte + I0 ==Int I1 +Int 1 // I1 writes [I1, I1+2), I0 writes [I1+1, I1+3), overlap at [I1+1, I1+2) +endmodule \ No newline at end of file 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..8ec1a685 --- /dev/null +++ b/src/tests/integration/test-data/specs/store-symbolic-index-value.k @@ -0,0 +1,33 @@ +module STORE-SYMBOLIC-INDEX-VALUE + imports RISCV + + claim [id]: + #CHECK_HALT => #HALT + + .Map + + 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))))))) + => // 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 (Int2Bytes(4, V6, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))) + + ADDRESS ( 0 ) + requires // Ensure truly non-overlapping writes + // I0 writes 4 bytes [I0, I0+4), must not overlap with [0, 4) + 4 <=Int I0 andBool + // I1 writes 4 bytes [I1, I1+4), must not overlap with I0 [I0, I0+4) + I0 +Int 4 <=Int I1 andBool + // I2 writes 4 bytes [I2, I2+4), must not overlap with I1 [I1, I1+4) + I1 +Int 4 <=Int I2 +endmodule 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" },