hevm equivalence fails due to dynamic jumptable and hence symbolic JUMP

[charles-cooper]

a.txt
b.txt

hevm equivalence --code-a <(cat a.txt) --code-b <(cat b.txt)

fails with:

hevm: Internal Error: invalid hex bytestring for --code -- CallStack (from HasCallStack):
  internalError, called at src/EVM/Format.hs:819:10 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Format
CallStack (from HasCallStack):
  error, called at src/EVM/Types.hs:1344:19 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Types
  internalError, called at src/EVM/Format.hs:819:10 in hevm-0.53.0-GInGiFSvIMC3zpj6pjAnyV:EVM.Format

[msooseth]

So this is a bug only insofar as we: (1) were printing an incorrect error message, and (2) we should give examples how to do this correctly.

Latest hevm runs perfectly fine with:

cabal run -f devel exe:hevm -- equivalence --code-a "$(<a.txt)" --code-b "$(<b.txt)"

Notice that i changed the way you "paste in" the files a.txt and b.txt. It then gives the output:

   1   │ WARNING: hevm was only able to partially explore the given contract due to the following issue(s):
   2   │   - Unexpected Symbolic Arguments to Opcode
   3   │     msg: "JUMP: symbolic jumpdest"
   4   │     opcode: JUMP
   5   │     program counter: 23
   6   │     arguments:
   7   │       (ReadWord
   8   │         idx:
....
2899   │       )
2900   │ Found 1 total pairs of endstates
2901   │ Asking the SMT solver for 0 pairs
2902   │ Reuse of previous queries was Useful in 0 cases
2903   │ No discrepancies found

Notice: the VERY MUCH IS the possibility of a discrepancy, but because of the symbolic jump, hevm couldn't fully verify the contract. That's the first thing it prints, with all-caps "WARNING".

I am keeping this open until I fix the error printed and give an example in hevm.dev about how to call this correctly, so others don't make the same mistake.

[msooseth]

Let me know what you think about the changes proposed here: https://github.com/ethereum/hevm/pull/583/files

I hope it will help you and others not make the same small mistake!

Mate

[charles-cooper]

thanks, commented on the PR. any possibility to fix the symbolic jump? that would probably be this vyperlang/vyper#3496 -- it codecopies a set of possible jump destinations into memory, and then jumps to one of them.

[msooseth]

Oh wow. Yeah, dynamic jumptables can be an issue. I'm trying to see what I can do.

[charles-cooper]

even without the jumptables, i am running into other issues with memory now. is there a good place to discuss these without clogging up the issue tracker?

[msooseth]

Sure, please come to https://matrix.to/#/%23hevm%3Amatrix.org that's our public Matrix room

[msooseth]

So I think this dynamic jump creates a bit of a conundrum. What I think is possible to do here is:

1. Run an SMT solver to get out all possible jump destinations, by solving [1] for all possible values, using the SMT solver's SAT/UNSAT features. I.e. run with SAT & ban solution & SAT & ban solution ... UNSAT. This effectively makes this into a branch.
2. Thereby treat JUMP as a possible branching point and branch out in our Expr there. We'll need to limit this branching or things will go haywire (exponential blowup). But if the number of options is limited, it's actually quite OK.

This is quite possible to do. Would take about 1 week to do I think. But it's like, real work :D

[1]

          (CopySlice
            srcOffset: (Add
              22525
              (SHL
                1
                (Mod
                  (JoinBytes
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    0
                    (ReadByte
                      idx:
                        0
                      buf:
                        (AbstractBuf "txdata")
                    )
                    (ReadByte
                      idx:
                        1
                      buf:
                        (AbstractBuf "txdata")
                    )
                    (ReadByte
                      idx:
                        2
                      buf:
                        (AbstractBuf "txdata")
                    )
                    (ReadByte
                      idx:
                        3
                      buf:
                        (AbstractBuf "txdata")
                    )
                  )
                  53
                )
              )
            )
            dstOffset: 30
            size:      2
            src:
              (ConcreteBuf
                Length: 22631 (0x5867) bytes
                0000:   5f 35 60 e0  1c 60 02 60  35 82 06 60  01 1b 61 57   _5`..`.`5..`..aW
...