allow symbolic bytecode in `hevm equivalence`

[charles-cooper]

in runtime bytecode, there is often bytecode which is never executed, but may be copied to memory via codecopy. it would be nice to be able to have bytecode like

CODECOPY 0, 100, 32

and in the actual bytecode provided to hevm equivalence, use sentinel nibbles like SSSS..SS at offset 100. then hevm would interpret this as symbolic data. of course, if the symbolic bytecode is actually reachable (it shouldn't be!), execution should terminate with an exception.

[msooseth]

I think it's possible. I'd rather do it via writes-over-concretebuf, such as

write position symbolic-value (concrete-contract-code)

Then, EVM.hs would need to be updated, to handle the case of reading a value from this write pos symbval code expression, and making sure the instruction is always concrete. It's actually not too hard to do. Maybe I should just bite the bullet and do it :D This would allow us to actually deal with this test case that currently fails:

      -- We set x to be 0 on deployment. Default value is also 0. So they are equivalent
      -- We cannot deal with symbolic code. However, the below will generate symbolic code,
      -- because of the parameter in the constructor that is set to NUMBER in the deployed code.
      -- Hence, this test is ignored.
      , ignoreTest $ test "constructor-diff-deploy" $ do
        Just initA <- solidity "C"
          [i|
            contract C {
              uint public immutable NUMBER;
              constructor(uint a) {
                NUMBER = a+4;
              }
              function stuff(uint b) public returns (uint256) {
                return NUMBER;
              }
            }
          |]
        Just initB <- solidity "C"
          [i|
            contract C {
              uint public immutable NUMBER;
              constructor(uint a) {
                NUMBER = a*2;
              }
              function stuff(uint b) public returns (uint256) {
                return NUMBER;
              }
            }
          |]
        withSolvers Z3 3 1 Nothing $ \s -> do
          calldata <- mkCalldata Nothing []
          (res, _) <- equivalenceCheck s initA initB defaultVeriOpts calldata True
          assertBoolM "Must have difference" (all isCex res)

Notice that the immutable NUMBER is set to a symbolic value in the constructor. This upsets our current evaluation logic. It'd need to be fixed in EVM.hs, as mentioned.

I'll have a go at it today/next week :)