Better loadBytes for symbolic execution (#91)

This PR is introduced to simplify the process of loading multiple bytes, simplifying the result of loadbytes for symbolic execution.

------

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.69
+0.1.70

pyproject.toml

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

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

@@ -10,15 +10,20 @@ module SPARSE-BYTES-SIMPLIFICATIONS
   imports SPARSE-BYTES
 ```
 
-## readByteBF
+## pickFront and dropFront
 
-For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` and `#bytes(B +Bytes BS) EF` to obtain as exact as possible values for `readByte`.
+For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` and `#bytes(B +Bytes BS) EF` to obtain as exact as possible values for `pickFront`.
 
 ```k
-  rule readByteBF(#bytes(B +Bytes _) _ , I) => B[ I ] 
-    requires I >=Int 0 andBool I <Int lengthBytes(B) [simplification(45)]
-  rule readByteBF(#bytes(B +Bytes BS) EF , I) => readByteBF(#bytes(BS) EF , I -Int lengthBytes(B)) 
-    requires I >=Int lengthBytes(B) [simplification(45)]
+  rule pickFront(#bytes(B +Bytes _) _ , I) => substrBytes(B, 0, I)
+    requires I >Int 0 andBool I <=Int lengthBytes(B)    [simplification(45)]
+  rule pickFront(#bytes(B +Bytes BS) EF, I) => B +Bytes pickFront(#bytes(BS) EF, I -Int lengthBytes(B))
+    requires I >Int lengthBytes(B)                      [simplification(45)]
+
+  rule dropFront(#bytes(B +Bytes BS) EF , I) => dropFront(#bytes(substrBytes(B, I, lengthBytes(B)) +Bytes BS) EF, 0) 
+    requires I >Int 0 andBool I <Int lengthBytes(B)     [simplification(45)]
+  rule dropFront(#bytes(B +Bytes BS) EF, I) => dropFront(#bytes(BS) EF, I -Int lengthBytes(B)) 
+    requires I >=Int lengthBytes(B)                     [simplification(45)]
 ```
 
 

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

@@ -99,32 +99,22 @@ module RISCV-MEMORY
 
   syntax Memory = SparseBytes
 ```
-We abstract the particular memory representation behind `loadBytes` and `storeBytes` functions.
+We abstract the particular memory representation behind `loadBytes` and `storeBytes` functions. For multi-byte loads and stores, we presume a little-endian architecture.
 ```k
-  syntax Int ::= loadByte(memory: Memory, address: Word) [function, symbol(Memory:loadByte)]
-  rule loadByte(MEM, W(ADDR)) => MaybeByte2Int(readByte(MEM, ADDR))
-```
-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 Int ::= loadBytes(memory: Memory, address: Word, numBytes: Int) [function, total, symbol(Memory:loadBytes)]
+  rule loadBytes(MEM, W(ADDR), NUM) => readBytes(MEM, ADDR, NUM)
 
   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
-  syntax Instruction ::= fetchInstr(memory: Memory, address: Word) [function]
-  rule fetchInstr(MEM, ADDR) =>
-    disassemble((loadByte(MEM, ADDR +Word W(3)) <<Int 24) |Int
-                (loadByte(MEM, ADDR +Word W(2)) <<Int 16) |Int
-                (loadByte(MEM, ADDR +Word W(1)) <<Int 8 ) |Int
-                 loadByte(MEM, ADDR       ))
+  syntax Instruction ::= fetchInstr(memory: Memory, address: Word) [function, total]
+  rule fetchInstr(MEM, ADDR) => disassemble(loadBytes(MEM, ADDR, 4))
 ```
 Registers should be manipulated with the `writeReg` and `readReg` functions, which account for `x0` always being hard-wired to contain all `0`s.
 ```k
-  syntax Map ::= writeReg(regs: Map, rd: Int, value: Word) [function]
+  syntax Map ::= writeReg(regs: Map, rd: Int, value: Word) [function, total]
   rule writeReg(REGS, 0 , _  ) => REGS
   rule writeReg(REGS, RD, VAL) => REGS[RD <- VAL] [owise]
 
@@ -323,7 +313,7 @@ The remaining branch instructions proceed analogously, but performing different
 `LB`, `LH`, and `LW` load `1`, `2`, and `4` bytes respectively from the memory address which is `OFFSET` greater than the value in register `RS1`, then sign extends the loaded bytes and places them in register `RD`.
 ```k
   rule <instrs> LB RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, signExtend(loadByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET)), 8)) </regs>
+       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 1), 8)) </regs>
        <mem> MEM </mem>
 
   rule <instrs> LH RD , OFFSET ( RS1 ) => .K ...</instrs>
@@ -337,7 +327,7 @@ The remaining branch instructions proceed analogously, but performing different
 `LBU` and `LHU` are analogous to `LB` and `LH`, but zero-extending rather than sign-extending.
 ```k
    rule <instrs> LBU RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, W(loadByte(MEM, readReg(REGS, RS1) +Word chop(OFFSET)))) </regs>
+       <regs> REGS => writeReg(REGS, RD, W(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 1))) </regs>
        <mem> MEM </mem>
 
   rule <instrs> LHU RD , OFFSET ( RS1 ) => .K ...</instrs>

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

@@ -47,45 +47,36 @@ 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
 ```
+`pickFront` is a helper function for picking the first `N` bytes from a `SparseBytes` value.
+```k
+  syntax Bytes ::= pickFront(SparseBytes, Int) [function, total]
+  rule pickFront(_, I) => .Bytes requires I <=Int 0
+  rule pickFront(.SparseBytes, I) => .Bytes requires I >Int 0
+  rule pickFront(#empty(N) _, I) => padRightBytes(.Bytes, I, 0)
+    requires I >Int 0 andBool I <=Int N
+  rule pickFront(#empty(N) BF, I) => padRightBytes(.Bytes, I, 0) +Bytes pickFront(BF, I -Int N)
+    requires I >Int 0 andBool I >Int N
+  rule pickFront(#bytes(B) _, I) => substrBytes(B, 0, I)
+    requires I >Int 0 andBool I <=Int lengthBytes(B)
+  rule pickFront(#bytes(B) EF, I) => B +Bytes pickFront(EF, I -Int lengthBytes(B))
+    requires I >Int lengthBytes(B)
+```
 `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(#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
+`readBytes(SBS, I, NUM)` reads `NUM` bytes from a given index `I` in `O(E)` time, where `E` is the number of `#empty(_)` or `#bytes(_)` entries in the list up to the location of the index.
 ```k
-  syntax MaybeByte ::=
-      Int
-    | ".Byte"
-  
-  syntax Int ::= MaybeByte2Int(MaybeByte) [function, total]
-  rule MaybeByte2Int(I:Int) => I
-  rule MaybeByte2Int(.Byte) => 0
-
-  syntax MaybeByte ::=
-      readByte  (SparseBytes  , Int) [function, total]
-    | readByteEF(SparseBytesEF, Int) [function, total]
-    | readByteBF(SparseBytesBF, Int) [function, total]
-
-  rule readByte(EF:SparseBytesEF, I) => readByteEF(EF, I)
-  rule readByte(BF:SparseBytesBF, I) => readByteBF(BF, I)
-
-  rule readByteEF(.SparseBytes, _) => .Byte
-  rule readByteEF(#empty(N) _ , I) => .Byte                    requires I <Int N
-  rule readByteEF(#empty(N) BF, I) => readByteBF(BF, I -Int N) requires I >=Int N
+  syntax Int ::= readBytes(SparseBytes, Int, Int) [function, total]
 
-  rule readByteBF(#bytes(_) _ , I) => .Byte  requires I <Int 0 // error case for totality
-  rule readByteBF(#bytes(B) _ , I) => B[ I ] requires I >=Int 0 andBool I <Int lengthBytes(B)
-  rule readByteBF(#bytes(B) EF, I) => readByteEF(EF, I -Int lengthBytes(B))
-                                             requires I >=Int lengthBytes(B)
+  rule readBytes(SBS, I, NUM) => Bytes2Int(pickFront(dropFront(SBS, I), NUM), LE, Unsigned)
 ```
 `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.

src/kriscv/term_builder.py

@@ -314,8 +314,8 @@ def sort_memory() -> KSort:
     return KSort('SparseBytes')
 
 
-def load_byte(mem: KInner, addr: KInner) -> KInner:
-    return KApply('Memory:loadByte', mem, addr)
+def load_bytes(mem: KInner, addr: KInner, num_bytes: KInner) -> KInner:
+    return KApply('Memory:loadBytes', mem, addr, num_bytes)
 
 
 def store_bytes(mem: KInner, addr: KInner, value: KInner, num_bytes: KInner) -> KInner:

src/tests/integration/test-data/specs/lw-spec.k

@@ -7,7 +7,7 @@ module LW-SPEC
     <instrs> (.K => #HALT) ~> #EXECUTE ... </instrs>
     <regs>
       1 |-> (W(16) => W(1))
-      2 |-> (W(24) => signExtend (Y[3] <<Int 8 |Int Y[2] <<Int 8 |Int Y[1] <<Int 8 |Int Y[0], 32 ))
+      2 |-> (W(24) => signExtend ( ... bits: Bytes2Int ( substrBytes ( Y:Bytes , 0 , 4 ) , LE , Unsigned ) , signBitIdx: 32 ))
       3 |-> (W(28) => W(2))
     </regs>
     <pc> W ( 0 => 12 ) </pc>

src/tests/integration/test_prove.py

@@ -53,9 +53,6 @@ def test_specs(
     temp_dir: Path,
     spec_file: Path,
 ) -> None:
-    if spec_file.name == 'lw-spec.k':
-        pytest.skip('Skipping lw-spec.k due to the weird implies failed')
-
     # Given
     spec_file = load_spec(spec_file.name)
 

src/tests/unit/test_unit.py

@@ -312,7 +312,7 @@ def test_memory(memory: dict[int, bytes], addr: int, byte: int) -> None:
 
     # Also execute loadByte and check that we correctly read back the written value
     memory_actual_sb = tools.krun.kore_to_kast(memory_actual_sb_kore)
-    load_call = term_builder.load_byte(memory_actual_sb, addr_word)
+    load_call = term_builder.load_bytes(memory_actual_sb, addr_word, intToken(1))
     load_actual = kore_int(_eval_call_to_kore(tools, load_call, INT))
 
     assert load_actual == byte