This allows us to do partial symbolic jumpdest support. In particular, when the jumpdest can be computed with already-existing data this works. The added test file fails with Exception: cannot handle symbolic branch conditions in this interpreter: IsZero (GT (... but with the change of adding a stronger form of Expr.simplify (concKeccakSimpExpr), we can compute the jump and continue exploring.
This change does not fully make the test work, as we still bail out for another reason. However, it significantly improves our capabilities, and should help in our test suite.
More detailed description of the fix
In file src/EVM/Stepper.hs on lines 121... is the real change. What this does is that instead of checking if the jump address is a (Lit a), it first puts the jump address into a variable expr, and calls concKeccakSimpExpr expr on it. THEN it checks whether this is a (Lit a). Hence, expressions that can be simplified into a Lit will now work.
Let me give an example: (1) Previously, if the jump address was Lit 5, the jump succeeded, and we continued our marry way. However, when it was Add (Lit 1) (Lit4), it would abort, saying that it cannot jump to a symbolic address. Now, (2) what will happen is that (Lit 5) will still work, as concKeccakSimpExpr (Lit 5) = Lit 5. However, Add (Lit 1) (Lit4) will also work now, since concKeccakSimpExpr (Add (Lit 1) (Lit4)) = Lit 5, and hence we can continue exploring.
Description
This allows us to do partial symbolic jumpdest support. In particular, when the jumpdest can be computed with already-existing data this works. The added test file fails with
Exception: cannot handle symbolic branch conditions in this interpreter: IsZero (GT (...
but with the change of adding a stronger form ofExpr.simplify
(concKeccakSimpExpr
), we can compute the jump and continue exploring.This change does not fully make the test work, as we still bail out for another reason. However, it significantly improves our capabilities, and should help in our test suite.
More detailed description of the fix
In file
src/EVM/Stepper.hs
on lines 121... is the real change. What this does is that instead of checking if the jump address is a(Lit a)
, it first puts the jump address into a variableexpr
, and callsconcKeccakSimpExpr expr
on it. THEN it checks whether this is a(Lit a)
. Hence, expressions that can be simplified into aLit
will now work.Let me give an example: (1) Previously, if the jump address was
Lit 5
, the jump succeeded, and we continued our marry way. However, when it wasAdd (Lit 1) (Lit4)
, it would abort, saying that it cannot jump to a symbolic address. Now, (2) what will happen is that(Lit 5)
will still work, asconcKeccakSimpExpr (Lit 5) = Lit 5
. However,Add (Lit 1) (Lit4)
will also work now, sinceconcKeccakSimpExpr (Add (Lit 1) (Lit4)) = Lit 5
, and hence we can continue exploring.Checklist
Minor detail
The added test used to fail because of
hevm: cannot handle symbolic branch conditions in this interpreter: IsZero (GT (SLoad (Keccak (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x40) (WriteWord (Lit 0x0) (Lit 0x2) (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\STX\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL")) (ConcreteBuf ""))) (SStore (Keccak (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL")) (Lit 0xde0b6b3a7640000) (ConcreteStore (fromList [])))) (Add (Lit 0xde0b6b3a7640000) (SLoad (Keccak (CopySlice (Lit 0x0) (Lit 0x0) (Lit 0x40) (WriteWord (Lit 0x0) (Lit 0x2) (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\STX\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL")) (ConcreteBuf ""))) (SStore (Keccak (ConcreteBuf "\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\SOH\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL\NUL")) (Lit 0xde0b6b3a7640000) (ConcreteStore (fromList []))))))
That expression can be simplified to a
Lit a
.