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/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 03206f83..95716074 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,41 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` requires I >=Int lengthBytes(B) [simplification(45), preserves-definedness] ``` +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] + + // 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] +``` + ## writeBytes If the write index is concrete, we can directly call `writeBytesBF` or `writeBytesEF`. @@ -50,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. @@ -76,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 new file mode 100644 index 00000000..6bf43d08 --- /dev/null +++ b/src/tests/integration/test-data/specs/read-symbolic-index-value.k @@ -0,0 +1,59 @@ +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) + // 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 ) + requires 8