[DRAFT] Symbolic EXTCODESIZE & CALL return value when the address is symbolic

[msooseth]

Description

This overapproximates and so allows us to move forward with the exploration for:

• EXTCODESIZE, always when the contract cannot be found. This is useful, because this is ONLY a check on the size of the contract. So we return a symbolic variable, and continue, potentially going into branches that may be impossible in normal circumstances
• CALL, only when --promise-no-reent is given. This is a kind of a hack, where we assume that state is not changed of either us or any other contract, when a CALL is made to an unknown code. This is kinda okay when all important state-changing code is guarded by reentrancy locks.

I also refactored the STATICCALL abstraction so it is now much more straightforward, and uses the new generic abstraction system. I think it's a VERY cool now.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

This gives the wrong result apparently(?):

contract T {
  function g() public { }
}

contract C {
  function f(address x) public {
    T t = new T();
    T(x).g();
    assert(false);
  }
}

$ hevm symbolic --sig "f(address)" --code 608060405234801561001057600080fd5b506004361061002b5760003560e01c8063fc68521a14610030575b600080fd5b61004a6004803603810190610045919061010d565b61004c565b005b600060405161005a906100ec565b604051809103906000f080158015610076573d6000803e3d6000fd5b5090508173ffffffffffffffffffffffffffffffffffffffff1663e2179b8e6040518163ffffffff1660e01b8152600401600060405180830381600087803b1580156100c157600080fd5b505af11580156100d5573d6000803e3d6000fd5b5050505060006100e8576100e761016c565b5b5050565b608a806101b883390190565b600081359050610107816101a0565b92915050565b6000602082840312156101235761012261019b565b5b6000610131848285016100f8565b91505092915050565b60006101458261014c565b9050919050565b600073ffffffffffffffffffffffffffffffffffffffff82169050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b600080fd5b6101a98161013a565b81146101b457600080fd5b5056fe6080604052348015600f57600080fd5b50606d80601d6000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c8063e2179b8e14602d575b600080fd5b60336035565b005b56fea2646970667358221220dfa1556859ae44e6ad60c9fe0138be250f707c770ad9ac646d1be9cc2560452d64736f6c63430008050033a2646970667358221220076870182cd244b86b6393f83f2180e89054d38a2f93ed0b6076ad14c67e609f64736f6c63430008050033 --promise-no-reent
c:"608060405234801561001057600080fd5b506004361061002b5760003560e01c8063fc68521a14610030575b600080fd5b61004a6004803603810190610045919061010d565b61004c565b005b600060405161005a906100ec565b604051809103906000f080158015610076573d6000803e3d6000fd5b5090508173ffffffffffffffffffffffffffffffffffffffff1663e2179b8e6040518163ffffffff1660e01b8152600401600060405180830381600087803b1580156100c157600080fd5b505af11580156100d5573d6000803e3d6000fd5b5050505060006100e8576100e761016c565b5b5050565b608a806101b883390190565b600081359050610107816101a0565b92915050565b6000602082840312156101235761012261019b565b5b6000610131848285016100f8565b91505092915050565b60006101458261014c565b9050919050565b600073ffffffffffffffffffffffffffffffffffffffff82169050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b600080fd5b6101a98161013a565b81146101b457600080fd5b5056fe6080604052348015600f57600080fd5b50606d80601d6000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c8063e2179b8e14602d575b600080fd5b60336035565b005b56fea2646970667358221220dfa1556859ae44e6ad60c9fe0138be250f707c770ad9ac646d1be9cc2560452d64736f6c63430008050033a2646970667358221220076870182cd244b86b6393f83f2180e89054d38a2f93ed0b6076ad14c67e609f64736f6c63430008050033"

Discovered the following 1 counterexample(s):

Calldata:
  0xfc68521a0000000000000000000000000000000000000000000000000000000000001312
Storage:
  Addr SymAddr "miner": []
  Addr SymAddr "origin": []
Transaction Context:
  TxValue: 0x0
Addrs:
  SymAddr "entrypoint": 0xA32B9Ef9aBce0264De56C30181004Dc1DaF526Ab
  SymAddr "freshSymAddr1": 0x87d3c12faC2df2A23cDC0188d100788e1884123D
  SymAddr "miner": 0x04288C505033F999A2AAc10181007741D3F5AF61
  SymAddr "origin": 0x786C3ed053900d5f410d3efe7EFf88be2c0A509e