Integer overflow during conformance test

[anvacaru]

randomStateTest649 crashes kevm with an Integer overflow during execution.

After debugging with the gdb debugger, I've identified the rule that triggers the overflow as:

<k>
    CODECOPY 379274245380206583296823 1438 0 ~> #pc [ CODECOPY ] ~> #execute ~> ...

Taking a k step after this point results in:

(gdb) k step
Continuing.
terminate called after throwing an instance of 'std::invalid_argument'
  what():  [get_ui]: Integer overflow

Program received signal SIGABRT, Aborted.
__pthread_kill_implementation (no_tid=0, signo=6, threadid=140737348842560) at ./nptl/pthread_kill.c:44
44      ./nptl/pthread_kill.c: No such file or directory.

part of: #1671

[anvacaru]

After running bt in the gdb session, looks like there is a list index out of range error in hook_BYTES_padRight.

Program received signal SIGABRT, Aborted.                                                                                                                                                                   
__pthread_kill_implementation (no_tid=0, signo=6, threadid=140737348842560) at ./nptl/pthread_kill.c:44                                                                                                     
44      ./nptl/pthread_kill.c: No such file or directory.                                                                                                                                                   
(gdb) bt                                                                                                                                                                                                    
#0  __pthread_kill_implementation (no_tid=0, signo=6, threadid=140737348842560) at ./nptl/pthread_kill.c:44                                                                                                 
#1  __pthread_kill_internal (signo=6, threadid=140737348842560) at ./nptl/pthread_kill.c:78                                                                                                                 
#2  __GI___pthread_kill (threadid=140737348842560, signo=signo@entry=6) at ./nptl/pthread_kill.c:89
#3  0x00007ffff6442476 in __GI_raise (sig=sig@entry=6) at ../sysdeps/posix/raise.c:26
#4  0x00007ffff64287f3 in __GI_abort () at ./stdlib/abort.c:79
#5  0x00007ffff68a2bbe in ?? () from /lib/x86_64-linux-gnu/libstdc++.so.6
#6  0x00007ffff68ae24c in ?? () from /lib/x86_64-linux-gnu/libstdc++.so.6
#7  0x00007ffff68ae2b7 in std::terminate() () from /lib/x86_64-linux-gnu/libstdc++.so.6
#8  0x00007ffff68ae518 in __cxa_throw () from /lib/x86_64-linux-gnu/libstdc++.so.6
#9  0x0000000000511e79 in get_ui (i=0x7ffff469cef0) at /home/anvacaru/rv/evm-semantics/deps/k/llvm-backend/src/main/native/llvm-backend/runtime/strings/bytes.cpp:74
#10 0x0000000000513ddc in hook_BYTES_padRight (
    b=b"lumbferican 7f9490737965316610074Z05resu82g0ut te00A03\n000000efbfq%e8lumbferic00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000lumbferic", len=379274245380206583296823, v=0) at /home/anvacaru/rv/evm-semantics/deps/k/llvm-backend/src/main/native/llvm-backend/runtime/strings/bytes.cpp:189
#11 0x000000000047ef37 in apply_rule_7537 (VarSTART=379274245380206583296823, VarWS=Traceback (most recent call last):
  File "<string>", line 392, in to_string
  File "<string>", line 554, in append
IndexError: list index out of range

Python Exception <class 'IndexError'>: list index out of range
, VarWS'Apos'=b"") at /home/anvacaru/rv/evm-semantics/.build/usr/lib/kevm/include/kframework/evm-types.md:327

[anvacaru]

Adding a rule to skip updating bytes when the value to insert is .Bytes is a workaround for this issue, and the conformance test is passing.

    rule WS [ _ := WS' ] => WS requires lengthBytes(WS') ==Int 0 [concrete, priority(40)]

[anvacaru]

@Baltoli to reproduce this:

make build-llvm # KOMPILE_OPTS="--enable-llvm-debug" for gdb
kevm interpret tests/ethereum-tests/BlockchainTests/GeneralStateTests/stRandom2/randomStatetest649.json --backend llvm --mode NORMAL --schedule MERGE --chainid 1 # --debugger for gdb

[Baltoli]

The problem here is that the rule as applied is making a call padRightBytes(WS, 379274245380206583296823, 0), which will produce a Bytes object at least 379274245380206583296823 bytes long per the semantics of padRightBytes.

This isn't an issue in the LLVM backend; the hook would always throw this error when passed this argument - the KEVM rules that make this call will need to be revisited to work better with the underlying Bytes abstraction for local memory.