Display `SymAddr "caller"` in `formatCex` function when call `hevm --get-models`

[ethever]

With following solidity code:

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.0;

contract ERC20_2 {
    function a() public {
        assert(msg.sender == address(0x95222290DD7278Aa3Ddd389Cc1E1d165CC4BAfe5));
    }
}

and

forge build
hevm symbolic --rpc https://eth-mainnet.g.alchemy.com/v2/CH4meQjhQaPZ2GGAnVieDIVOPPNvgdLD   --code $(jq -r '.deployedBytecode.object' out/erc20.sol/ERC20_2.json)  --show-reachable-tree --get-models 1>src/hevm/models/erc20.lisp 

it then generates

--- Branch ---

Inputs:

  Calldata:
    0x0dbe671f

  Transaction Context:
    TxValue: 0x0

End State:

  (Success
    Data:
      (ConcreteBuf "")

    State:
      (SymAddr "entrypoint"):
        (Contract
          code:
            (RuntimeCode 6080604052348015600e575f80fd5b50600436106026575f3560e01c80630dbe671f14602a575b5f80fd5b60306032565b005b337395222290dd7278aa3ddd389cc1e1d165cc4bafe51460525760526054565b565b634e487b7160e01b5f52600160045260245ffdfea264697066735822122042ffef7f56c446c55e4791df1478f112802d23a12e60b95321b7d81c07e0a87164736f6c63430008170033)
          storage:
            (AbstractStore (SymAddr "entrypoint") Nothing)
          balance:
            (Add
              TxValue
              (Balance
                (SymAddr "entrypoint")
              )
            )
          nonce:
            0x0
        )

      (SymAddr "origin"):
        (Contract
          code:
            (RuntimeCode )
          storage:
            (ConcreteStore <empty>)
          balance:
            (Sub
              0
              TxValue
            )
          nonce:
            0x1
        )

    Assertions:
      (PEq
        851400861302238403048500845587900479529441538021
        (WAddr
          (SymAddr "caller")
        )
      )
      (PEq
        230582047
        (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")
          )
        )
      )
      (PLEq
        4
        (BufLength
          (AbstractBuf "txdata")
        )
      )
      (PEq
        TxValue
        0
      )
      (PLT
        (BufLength
          (AbstractBuf "txdata")
        )
        18446744073709551616
      )
      (PNeg
        (PEq
          (Eq
            851400861302238403048500845587900479529441538021
            (WAddr
              (SymAddr "caller")
            )
          )
          0
        )
      )
      (PNeg
        (PEq
          (Eq
            230582047
            (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")
              )
            )
          )
          0
        )
      )
      (PEq
        (LT
          (BufLength
            (AbstractBuf "txdata")
          )
          4
        )
        0
      )
  )

It is obvious that we need SymAddr "caller" == 851400861302238403048500845587900479529441538021 for the only Success state. Why don't we display the inputs for this branch by adding Addrs: SymAddr "caller": 0x95222290DD7278Aa3Ddd389Cc1.nsE1d165CC4BAfe5 ?

I found the SMTCex already contained the addrs map.

[ethever]

The inputs for this branch then becomes

--- Branch ---

Inputs:

  Calldata:
    0x0dbe671f

  Addrs:
    SymAddr "caller": 0x95222290DD7278Aa3Ddd389Cc1E1d165CC4BAfe5

  Transaction Context:
    TxValue: 0x0

[msooseth]

Wow, also that printing is horrible, it needs to be more tight:

--- Branch ---

Inputs:

  Calldata:
    0x0dbe671f

  Transaction Context:
    TxValue: 0x0

End State:

Should look like:

--- Branch ---

Inputs:
  Calldata:
    0x0dbe671f
  Transaction Context:
    TxValue: 0x0

End State:

I'm fixing this and also will try to add the Addrs...

[msooseth]

Fixed in https://github.com/ethereum/hevm/pull/535

Thanks again. Once it's reviewed, I'll merge!

[msooseth]

Just to be clear, it now prints:

Discovered the following 1 counterexample(s):

Calldata:
  0x0dbe671f
Storage:
  Addr SymAddr "origin": []
  Addr LitAddr 0x388C818CA8B9251b393131C08a736A67ccB19297: []
Transaction Context:
  TxValue: 0x0
Addrs:
  SymAddr "caller": 0x0000000000000000000000000000000000000000

=== Reachable Expression ===
...

=== Models for 5 branches ===

--- Branch ---
Inputs:
  Calldata:
    Empty
End State:
  (Failure
....

--- Branch ---
Inputs:
  Calldata:
    0x0dbe671f
  Transaction Context:
    TxValue: 0x0
  Addrs:
    SymAddr "caller": 0x95222290DD7278Aa3Ddd389Cc1E1d165CC4BAfe5
End State:
  (Success
    Data:
      (ConcreteBuf "")

    State:
      (SymAddr "entrypoint"):
...

[msooseth]

BTW, this also helped inspire me to write a PR https://github.com/ethereum/hevm/pull/539 to improve the symbolic execution tutorial :) Thanks again!

[ethever]

BTW, this also helped inspire me to write a PR https://github.com/ethereum/hevm/pull/539 to improve the symbolic execution tutorial :) Thanks again!

It's great to see how it has improved the symbolic execution tutorial. Thanks again for your efforts!

[blishko]

Fixed in #535.