ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
235 stars 48 forks source link

Unexpected Symbolic Arguments to Opcode (SymAddr "caller") #524

Closed ethever closed 2 months ago

ethever commented 2 months ago
     - Unexpected Symbolic Arguments to Opcode
       msg: "trying to access a symbolic address that isn't already present in storage"
       program counter: 69
       arguments: 
         (SymAddr "caller")

for this solidity code:

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

import "@openzeppelin/contracts/interfaces/IERC20.sol";

contract ERC20_2 {
    mapping(address => uint256) balanceOf1;
    mapping(address => uint256) balanceOf2;

    mapping(address => uint256) balanceOf;

    address owner = address(0x123456789abcdef);

    function a() public {
        payable(msg.sender).transfer(1234);
    }

}

with command:

forge build   &&  hevm symbolic --caller 0x*** --rpc https://eth-mainnet.g.alchemy.com/v2/***   --code $(jq -r '.deployedBytecode.object' out/erc20.sol/ERC20_2.json)  --show-reachable-tree 1>src/hevm/models/s.lisp 
msooseth commented 2 months ago

Confirmed, I get the same error on main, and also on fix-fetching-rpc (a PR that's pending):

$ cabal run hevm  -- symbolic --caller 0xaba --rpc $ETH_RPC_URL  --show-reachable-tree --code $(jq -r '.deployedBytecode.object' tmp2/out/bug.sol/ERC20_2.json)                                                                                                                                             impure 
   WARNING: hevm was only able to partially explore the call prefix 0xunknown due to the following issue(s):
     - Unexpected Symbolic Arguments to Opcode
       msg: "trying to access a symbolic address that isn't already present in storage"
       program counter: 73
       arguments:
         (SymAddr "caller")

QED: No reachable property violations discovered

=== Reachable Expression ===

(ITE
  (IsZero
    TxValue
  )
...
msooseth commented 2 months ago

Fixed in PR #526 Do you wanna check out that PR and see if it's good?

msooseth commented 2 months ago

And thanks again for notifying us! indeed it was a bug. We should have a few concrete test cases for the cli

ethever commented 2 months ago

Great job! PR #526 works!