ethereum / hevm

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

Better printing of symbolic results #535

Closed msooseth closed 3 weeks ago

msooseth commented 3 weeks ago

Description

As per: https://github.com/ethereum/hevm/issues/534 Addrs was not printed, and also, the printing was a bit unaesthetic. It's a bit more tight printing now, and Addrs are printed.

Checklist

ethever commented 3 weeks ago

This solidity code:

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

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

should have a Success state:

--- Branch ---
Inputs:
  Calldata:
    0x0dbe671f

  Transaction Context:
    TxValue: 0x0
  Addrs:
    SymAddr "caller": 0x95222290DD7278Aa3Ddd389Cc1E1d165CC4BAfe5
    SymAddr "origin": 0x0000000000000000123434444444444444444444

End State:
  (Success
    Data:
      (ConcreteBuf "")
   ...

but the lacking of T.unlines in this function in PR:

    addrsCex :: [Text]
    addrsCex
      | Map.null addrs = []
      | otherwise =
          [ "Addrs:"
          , indent 2 $ Map.foldrWithKey (\key val _ ->
              ((T.pack . show $ key) <> ": " <> (T.pack $ show val))
            ) mempty addrs
          ]

makes it only display the first element of the Map, i think.

ethever commented 3 weeks ago

when i change the function to

   addrsCex :: [Text]
    addrsCex 
      | Map.null addrs = []
      | otherwise = 
          [
            "Addrs:",
            indent 2 $ T.unlines $ Map.foldrWithKey (\k v acc -> (T.pack . show $ k) <> ": " <> (T.pack . show $ v) : acc) mempty addrs,
            ""
          ]

It prints the Success state correctly.

msooseth commented 3 weeks ago

OOopps, good point! Fixed.