Better storeBytes for symbolic execution (#90)

This PR aims to 
1. make the result of `storeBytes` as simple as possible.
2. tackle as much as possibilies for the symbolic execution of
`storeBytes`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.68
+0.1.69

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.68"
+version = "0.1.69"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md

@@ -52,6 +52,11 @@ module BYTES-SIMPLIFICATIONS
     B:Bytes [I <- V] => substrBytes(B, 0, I) +Bytes Int2Bytes(1, V, LE) +Bytes substrBytes(B, I +Int 1, lengthBytes(B) -Int I -Int 1)
     requires I <Int lengthBytes(B)
     [simplification, concrete(B, I), symbolic(V), preserves-definedness]
+  
+  rule [multiple-bytes-update-symbolic-value]:
+    replaceAtBytes(B, I, V) => substrBytes(B, 0, I) +Bytes V +Bytes substrBytes(B, I +Int lengthBytes(V), lengthBytes(B))
+    requires I +Int lengthBytes(V) <Int lengthBytes(B)
+    [simplification, concrete(B, I), symbolic(V), preserves-definedness]
 ```
 
 

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

@@ -27,10 +27,12 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _`
 To write a byte to a symbolic sparse byte region, we need to:
 
 ```k
-  rule writeByteBF(#bytes(B +Bytes BS) EF, I, V) => #bytes(B[ I <- V ] +Bytes BS) EF 
-    requires I >=Int 0 andBool I <Int lengthBytes(B) [simplification(45)]
-  rule writeByteBF(#bytes(B +Bytes BS) EF, I, V) => prepend(B, writeByteBF(#bytes(BS) EF, I -Int lengthBytes(B), V))
-    requires I >=Int lengthBytes(B) [simplification(45)]
+  rule writeBytesBF(#bytes(B +Bytes BS) EF, I, V, NUM) => #bytes(replaceAtBytes(B, I, Int2Bytes(NUM, V, LE)) +Bytes BS) EF
+    requires I >=Int 0 andBool I +Int NUM <=Int lengthBytes(B)  [simplification(45)]
+  rule writeBytesBF(#bytes(B +Bytes BS) EF, I, V, NUM) => prepend(substrBytes(B, 0, I) +Bytes Int2Bytes(NUM, V, LE), dropFront(#bytes(BS) EF, I +Int NUM -Int lengthBytes(B)))
+    requires I <Int lengthBytes(B) andBool I +Int NUM >Int lengthBytes(B)    [simplification(45)]
+  rule writeBytesBF(#bytes(B +Bytes BS) EF, I, V, NUM) => prepend(B, writeBytesBF(#bytes(BS) EF, I -Int lengthBytes(B), V, NUM))
+    requires I >=Int lengthBytes(B)                             [simplification(45)]
 ```
 
 ```k

src/kriscv/kdist/riscv-semantics/riscv.md

@@ -99,23 +99,19 @@ module RISCV-MEMORY
 
   syntax Memory = SparseBytes
 ```
-We abstract the particular memory representation behind `loadByte` and `storeByte` functions.
+We abstract the particular memory representation behind `loadBytes` and `storeBytes` functions.
 ```k
   syntax Int ::= loadByte(memory: Memory, address: Word) [function, symbol(Memory:loadByte)]
   rule loadByte(MEM, W(ADDR)) => MaybeByte2Int(readByte(MEM, ADDR))
-
-  syntax Memory ::= storeByte(memory: Memory, address: Word, byte: Int) [function, total, symbol(Memory:storeByte)]
-  rule storeByte(MEM, W(ADDR), B) => writeByte(MEM, ADDR, B)
 ```
 For multi-byte loads and stores, we presume a little-endian architecture.
 ```k
   syntax Int ::= loadBytes(memory: Memory, address: Word, numBytes: Int) [function]
   rule loadBytes(MEM, ADDR, 1  ) => loadByte(MEM, ADDR)
   rule loadBytes(MEM, ADDR, NUM) => (loadBytes(MEM, ADDR +Word W(1), NUM -Int 1) <<Int 8) |Int loadByte(MEM, ADDR) requires NUM >Int 1
 
-  syntax Memory ::= storeBytes(memory: Memory, address: Word, bytes: Int, numBytes: Int) [function]
-  rule storeBytes(MEM, ADDR, BS, 1  ) => storeByte(MEM, ADDR, BS)
-  rule storeBytes(MEM, ADDR, BS, NUM) => storeBytes(storeByte(MEM, ADDR, BS &Int 255), ADDR +Word W(1), BS >>Int 8, NUM -Int 1) requires NUM >Int 1
+  syntax Memory ::= storeBytes(memory: Memory, address: Word, bytes: Int, numBytes: Int) [function, total, symbol(Memory:storeBytes)]
+  rule storeBytes(MEM, W(ADDR), BS, NUM) => writeBytes(MEM, ADDR, BS, NUM)
 ```
 Instructions are always 32-bits, and are stored in little-endian format regardless of the endianness of the overall architecture.
 ```k
@@ -352,7 +348,7 @@ Dually, `SB`, `SH`, and `SW` store the least-significant `1`, `2`, and `4` bytes
 ```k
   rule <instrs> SB RS2 , OFFSET ( RS1 ) => .K ...</instrs>
        <regs> REGS </regs>
-       <mem> MEM => storeByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 255) </mem>
+       <mem> MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), Word2UInt(readReg(REGS, RS2)) &Int 255, 1) </mem>
 
   rule <instrs> SH RS2 , OFFSET ( RS1 ) => .K ...</instrs>
        <regs> REGS </regs>

src/kriscv/kdist/riscv-semantics/sparse-bytes.md

@@ -47,6 +47,17 @@ We provide helpers to prepend either data or an empty region to an existing `Spa
   rule prependEmpty(I, #empty(N) BF    ) => #empty(I +Int N) BF requires I >Int 0
   rule prependEmpty(I, BF:SparseBytesBF) => #empty(I) BF        requires I >Int 0
 ```
+`dropFront` is a helper function for dropping the first `N` bytes from a `SparseBytes` value.
+```k
+  syntax SparseBytes ::=  dropFront(SparseBytes, Int) [function, total]
+  rule dropFront(SBS, I) => SBS    requires I <=Int 0
+  rule dropFront(.SparseBytes, I) => .SparseBytes requires I >Int 0
+  rule dropFront(#empty(N) BF, I) => #empty(N -Int I) BF requires I >Int 0 andBool I <Int N
+  rule dropFront(#empty(N) BF, I) => dropFront(BF, I -Int N) requires I >Int 0 andBool I >=Int N 
+  rule dropFront(#bytes(B) EF, I) => dropFront(#bytes(substrBytes(B, I, lengthBytes(B))) EF, 0) 
+    requires I >Int 0 andBool I <Int lengthBytes(B)
+  rule dropFront(#bytes(B) EF, I) => dropFront(EF, I -Int lengthBytes(B)) requires I >=Int lengthBytes(B)
+```
 `readByte` reads a single byte from a given index in `O(E)` time, where `E` is the number of `#empty(_)` or `#bytes(_)` entries in the list up to the location of the index. The result is either
 - an `Int` in the range `[0, 255)` giving the byte value at the index, or
 - `.Byte` if the index does not point to initialized data
@@ -76,28 +87,33 @@ We provide helpers to prepend either data or an empty region to an existing `Spa
   rule readByteBF(#bytes(B) EF, I) => readByteEF(EF, I -Int lengthBytes(B))
                                              requires I >=Int lengthBytes(B)
 ```
-`writeByte` writes a single byte to a given index. With regards to time complexity,
+`writeBytes(SBS, I, V, NUM)` writes value `V` with length `NUM` bytes to a given index `I`. With regards to time complexity,
 - If the index is in the middle of an existing `#empty(_)` or `#bytes(_)` region, time complexity is `O(E)` where `E` is the number of entries up to the index.
 - If the index happens to be the first or last index in an `#empty(_)` region directly boarding a `#bytes(_)` region, then the `#bytes(_)` region must be re-allocated to append the new value, giving worst-case `O(E + B)` time, where `E` is the number of entries up to the location of the index and `B` is the size of this existing `#bytes(_)`.
 ```k
   syntax SparseBytes ::=
-      writeByte  (SparseBytes  , Int, Int) [function, total]
-    | writeByteEF(SparseBytesEF, Int, Int) [function, total]
-    | writeByteBF(SparseBytesBF, Int, Int) [function, total]
+      writeBytes  (SparseBytes  , Int, Int, Int) [function, total]
+    | writeBytesEF(SparseBytesEF, Int, Int, Int) [function, total]
+    | writeBytesBF(SparseBytesBF, Int, Int, Int) [function, total]
 
-  rule writeByte(BF:SparseBytesBF, I, V) => writeByteBF(BF, I, V)
-  rule writeByte(EF:SparseBytesEF, I, V) => writeByteEF(EF, I, V)
+  rule writeBytes(BF:SparseBytesBF, I, V, NUM) => writeBytesBF(BF, I, V, NUM)
+  rule writeBytes(EF:SparseBytesEF, I, V, NUM) => writeBytesEF(EF, I, V, NUM)
 
-  rule writeByteEF(_           , I, _) => .SparseBytes                                       requires I <Int 0 // error case for totality
-  rule writeByteEF(.SparseBytes, I, V) => #bytes(Int2Bytes(1, V, BE)) .SparseBytes           requires I ==Int 0
-  rule writeByteEF(.SparseBytes, I, V) => #empty(I) #bytes(Int2Bytes(1, V, BE)) .SparseBytes requires I >Int 0
-  rule writeByteEF(#empty(N) BF, I, V) => prependEmpty(I, prepend(Int2Bytes(1, V, BE), prependEmpty((N -Int I) -Int 1, BF)))
-                                                                                             requires I >=Int 0 andBool I <Int N
-  rule writeByteEF(#empty(N) BF, I, V) => prependEmpty(N, writeByteBF(BF, I -Int N, V))      requires I >=Int N
+  rule writeBytesEF(_           , I, _, _) => .SparseBytes    requires I <Int 0 // error case for totality
+  rule writeBytesEF(.SparseBytes, I, V, NUM) => prependEmpty(I, #bytes(Int2Bytes(NUM, V, LE)) .SparseBytes)    requires I >=Int 0
+  rule writeBytesEF(#empty(N) BF, I, V, NUM) => prependEmpty(I, prepend(Int2Bytes(NUM, V, LE), prependEmpty(N -Int I -Int NUM, BF)))
+    requires I >=Int 0 andBool I +Int NUM <=Int N
+  rule writeBytesEF(#empty(N) BF, I, V, NUM) => prependEmpty(I, prepend(Int2Bytes(NUM, V, LE), dropFront(BF, I +Int NUM -Int N)))
+    requires I <Int N andBool I +Int NUM >Int N
+  rule writeBytesEF(#empty(N) BF, I, V, NUM) => prependEmpty(N, writeBytesBF(BF, I -Int N, V, NUM))
+    requires I >=Int N
 
-  rule writeByteBF(_           , I, _) => .SparseBytes           requires I <Int 0 // error case for totality
-  rule writeByteBF(#bytes(B) EF, I, V) => #bytes(B[ I <- V ]) EF requires I >=Int 0 andBool I <Int lengthBytes(B)
-  rule writeByteBF(#bytes(B) EF, I, V) => prepend(B, writeByteEF(EF, I -Int lengthBytes(B), V))
-                                                                 requires I >=Int lengthBytes(B)
+  rule writeBytesBF(_           , I, _, _  ) => .SparseBytes    requires I <Int 0 // error case for totality
+  rule writeBytesBF(#bytes(B) EF, I, V, NUM) => #bytes(replaceAtBytes(B, I, Int2Bytes(NUM, V, LE))) EF
+    requires I >=Int 0 andBool I +Int NUM <=Int lengthBytes(B)
+  rule writeBytesBF(#bytes(B) EF, I, V, NUM) => prepend(substrBytes(B, 0, I) +Bytes Int2Bytes(NUM, V, LE), dropFront(EF, I +Int NUM -Int lengthBytes(B)))
+    requires I <Int lengthBytes(B) andBool I +Int NUM >Int lengthBytes(B)
+  rule writeBytesBF(#bytes(B) EF, I, V, NUM) => prepend(B, writeBytesEF(EF, I -Int lengthBytes(B), V, NUM))
+    requires I >=Int lengthBytes(B)
 endmodule
 ```

src/kriscv/term_builder.py

@@ -318,8 +318,8 @@ def load_byte(mem: KInner, addr: KInner) -> KInner:
     return KApply('Memory:loadByte', mem, addr)
 
 
-def store_byte(mem: KInner, addr: KInner, value: KInner) -> KInner:
-    return KApply('Memory:storeByte', mem, addr, value)
+def store_bytes(mem: KInner, addr: KInner, value: KInner, num_bytes: KInner) -> KInner:
+    return KApply('Memory:storeBytes', mem, addr, value, num_bytes)
 
 
 def regs(dct: dict[int, int]) -> KInner:

src/tests/integration/test-data/specs/store-symbolic-bytes.k

@@ -16,7 +16,7 @@ module STORE-SYMBOLIC-BYTES
         X:Int,
         4
     ) =>
-    #bytes ( Int2Bytes ( 1 , X:Int &Int 255 , LE ) +Bytes Int2Bytes ( 1 , X:Int >>Int 8 &Int 255 , LE ) +Bytes Int2Bytes ( 1 , X:Int >>Int 8 >>Int 8 &Int 255 , LE ) +Bytes Int2Bytes ( 1 , X:Int >>Int 8 >>Int 8 >>Int 8 , LE ) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes
+    #bytes ( Int2Bytes ( 4 , X , LE ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes
     </mem>
     <test>
       <haltCond> ADDRESS ( W ( 0 ) ) </haltCond>

src/tests/unit/test_unit.py

@@ -304,7 +304,7 @@ def test_memory(memory: dict[int, bytes], addr: int, byte: int) -> None:
     memory_sb = term_builder.sparse_bytes(memory)
     addr_word = term_builder.word(addr)
 
-    store_call = term_builder.store_byte(memory_sb, addr_word, intToken(byte))
+    store_call = term_builder.store_bytes(memory_sb, addr_word, intToken(byte), intToken(1))
     memory_actual_sb_kore = _eval_call_to_kore(tools, store_call, term_builder.sort_memory())
     memory_actual = kore_sparse_bytes(memory_actual_sb_kore)