`STATICCALL` Error "Unable to determine a call target" #618

chief-mobius · 2024-12-17T14:16:23Z

I'm encountering an issue when running a symbolic execution test case with hevm for my contract. Specifically, the following error message appears when trying to explore the symbolic execution path for the prove_Swap(uint256) function:

[RUNNING] prove_Swap(uint256)
   WARNING: hevm was only able to partially explore the call prefix 0xde6fb24b due to the following issue(s):
     - Unexpected Symbolic Arguments to Opcode
       msg: "Unable to determine a call target"
       opcode: STATICCALL
       program counter: 13155
       arguments: 
         (And
           1461501637330902918203684832716283019655932542975
           (And
             1461501637330902918203684832716283019655932542975
             (SLoad
               slot:
                 (Keccak
                   (ConcreteBuf
                     Length: 64 (0x40) bytes
                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
                     0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
                     0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                     0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
                   )
                 )
               storage:
                 (ConcreteStore
                   vals:
                     (0x40,0x12309ce54000)
                     (0x41,0x7)
                     (0x42,0x53b1daa2fd98364)
                     (0x43,0x493b9f4e9de52f7)
                     (0x44,0x5af3107a4000)
                     (0x45,0xde0b6b3a7640000)
                     (0x46,0x470de4df820000)
                     (0x47,0xacab)
                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                     (0x49,0x5)
                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                 )
             )
           )
         )

This error indicates that the symbolic execution engine is unable to determine the call target during the execution of a STATICCALL operation. This prevents hevm from fully exploring the path.

Here is my test file snippet

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

import { Test } from "forge-std/Test.sol";
import { console2 } from "forge-std/Test.sol";
import { OldPool } from "../src/pool/OldPool.sol";


contract OldPoolTest is Test {
    OldPool public pool;

    function setUp() public {
        // setup logic
    }

    function testFuzz_Swap(uint256 amount) public {
        vm.assume(amount > 10_000 * 1e6);
        vm.assume(amount < 150_000 * 1e6);

        _sequence(amount);
        assertGe(amount, USDC.balanceOf(address(this)));
    }

    function prove_Swap(uint256 amount) public {
        if (amount != 0) {
            _sequence(amount);
            assertGe(amount, USDC.balanceOf(address(this)));
        }
    }

    function _sequence(uint256 amount) private {
        // test logic
    }
}

Note that I use _sequence function for both forge fuzz test and hevm, and fuzz working just fine

The text was updated successfully, but these errors were encountered:

msooseth · 2024-12-17T16:01:28Z

OK, so now I know what's going on. This:

                   (ConcreteBuf
                     Length: 64 (0x40) bytes
                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
                     0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
                     0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                     0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
                   )

Happens to be 0x000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a

which when keccak'ed:

cast keccak 0x000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a
0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d

Which is actually in the storage:

(ConcreteStore
  vals:
  (0x40,0x12309ce54000)
  (0x41,0x7)
[....]
  (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)

And so should resolve to 0x5842cfa0028e51f1b74c9dca4a59ef0e05544163, which is a concrete value. So this is not an expression, but a concrete value that should "just work", and should not throw this error. Sorryyyyy.

So this should be easy to fix. Let me have a go at it, maybe doable in an hour :)

msooseth · 2024-12-17T16:40:32Z

@chief-mobius can you please check with this PR?

#619

I think/hope it should work.

msooseth · 2024-12-17T17:06:20Z

How to reproduce in repl:

a="000000000000000000000000d95322745865822719164b1fc167930754c248de000000000000000000000000000000000000000000000000000000000000004a"
s= ConcreteStore (Map.fromList[(W256 0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,W256 0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)])
e=SLoad (Keccak (ConcreteBuf (hexStringToByteString a))) s
putStrLn $ T.unpack $ formatExpr e

--> We get:

(SLoad
  slot:
    (Keccak
      (ConcreteBuf
        Length: 64 (0x40) bytes
        0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
        0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
        0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
        0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
      )
    )
  storage:
    (ConcreteStore
      vals:
        (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
    )
)

If we perform the Expr.concKeccakSimpExpr then we get:

ghci> putStrLn $ T.unpack $ formatExpr (Expr.concKeccakSimpExpr  e)
503881123707364905152443243234154486473625452899
ghci> showHex 503881123707364905152443243234154486473625452899 "0x"
"0x5842cfa0028e51f1b74c9dca4a59ef0e05544163"

i.e. the concrete expression that we expected. So the fix should work, as it now uses concKeccakSimpExpr with simplify, which is what we had previously:

ghci> putStrLn $ T.unpack $ formatExpr (Expr.simplify  e)
(SLoad
  slot:
    (Keccak
      (ConcreteBuf
[...]

So it does not work, as per this issue. This means to me that the PR is likely correct :)

chief-mobius · 2024-12-18T10:33:48Z

Thank you so much for your quick response.
I still get errors when running prove_Swap. Here is the full log

[RUNNING] prove_Swap(uint256)
   WARNING: hevm was only able to partially explore the call prefix 0xde6fb24b due to the following issue(s):
     - Unexpected Symbolic Arguments to Opcode
       msg: "Unable to determine a call target"
       opcode: STATICCALL
       program counter: 9382
       arguments: 
         (And
           1461501637330902918203684832716283019655932542975
           (And
             1461501637330902918203684832716283019655932542975
             (SLoad
               slot:
                 (Keccak
                   (CopySlice
                     srcOffset: 0
                     dstOffset: 0
                     size:      64
                     src:
                       (WriteWord
                         idx:
                           0
                         val:
                           (And
                             1461501637330902918203684832716283019655932542975
                             (SLoad
                               slot:
                                 (Keccak
                                   (ConcreteBuf
                                     Length: 32 (0x20) bytes
                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
                                   )
                                 )
                               storage:
                                 (ConcreteStore
                                   vals:
                                     (0x40,0x12309ce54000)
                                     (0x41,0x7)
                                     (0x42,0x53b1daa2fd98364)
                                     (0x43,0x493b9f4e9de52f7)
                                     (0x44,0x5af3107a4000)
                                     (0x45,0xde0b6b3a7640000)
                                     (0x46,0x470de4df820000)
                                     (0x47,0xacab)
                                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                     (0x49,0x5)
                                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                 )
                             )
                           )
                         buf:
                           (WriteWord
                             idx:
                               32
                             val:
                               74
                             buf:
                               (WriteWord
                                 idx:
                                   64
                                 val:
                                   388
                                 buf:
                                   (WriteWord
                                     idx:
                                       128
                                     val:
                                       100
                                     buf:
                                       (WriteWord
                                         idx:
                                           160
                                         val:
                                           16156842317565293874272834530371880720966471053262404558597773956279093428224
                                         buf:
                                           (WriteWord
                                             idx:
                                               196
                                             val:
                                               (And
                                                 1461501637330902918203684832716283019655932542975
                                                 (SLoad
                                                   slot:
                                                     (Keccak
                                                       (ConcreteBuf
                                                         Length: 64 (0x40) bytes
                                                         0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
                                                         0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
                                                         0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                         0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
                                                       )
                                                     )
                                                   storage:
                                                     (ConcreteStore
                                                       vals:
                                                         (0x40,0x12309ce54000)
                                                         (0x41,0x7)
                                                         (0x42,0x53b1daa2fd98364)
                                                         (0x43,0x493b9f4e9de52f7)
                                                         (0x44,0x5af3107a4000)
                                                         (0x45,0xde0b6b3a7640000)
                                                         (0x46,0x470de4df820000)
                                                         (0x47,0xacab)
                                                         (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                                         (0x49,0x5)
                                                         (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                                         (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                                         (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                                         (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                                         (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                                         (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                                         (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                                         (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                                         (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                                         (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                                         (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                                         (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                                         (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                                         (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                                         (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                                         (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                                         (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                                         (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                                         (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                                     )
                                                 )
                                               )
                                             buf:
                                               (WriteWord
                                                 idx:
                                                   228
                                                 val:
                                                   (SLoad
                                                     slot:
                                                       (Keccak
                                                         (ConcreteBuf
                                                           Length: 64 (0x40) bytes
                                                           0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                           0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                           0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                           0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                         )
                                                       )
                                                     storage:
                                                       (SStore
                                                         slot:
                                                           (Keccak
                                                             (WriteWord
                                                               idx:
                                                                 32
                                                               val:
                                                                 (Keccak
                                                                   (ConcreteBuf
                                                                     Length: 64 (0x40) bytes
                                                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                     0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 01   ................
                                                                   )
                                                                 )
                                                               buf:
                                                                 (ConcreteBuf
                                                                   Length: 64 (0x40) bytes
                                                                   0000:   00 00 00 00  00 00 00 00  00 00 00 00  78 52 cb be   ............xR..
                                                                   0010:   68 18 a4 b4  52 ea cf 11  1c 87 d7 46  78 9e 7d 09   h...R......Fx.}.
                                                                   0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                 )
                                                             )
                                                           )
                                                         val:
                                                           (Add
                                                             (Var "arg1")
                                                             (SLoad
                                                               slot:
                                                                 (Keccak
                                                                   (ConcreteBuf
                                                                     Length: 64 (0x40) bytes
                                                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                     0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   )
                                                                 )
                                                               storage:
                                                                 (ConcreteStore
                                                                   vals:
                                                                     (0x2,0x52b7d2dcc80cd2e4000000)
                                                                     (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                     (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                     (0x5,0x6)
                                                                     (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
                                                                     (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
                                                                     (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
                                                                     (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
                                                                 )
                                                             )
                                                           )
                                                         store:
                                                           (SStore
                                                             slot:
                                                               (Keccak
                                                                 (ConcreteBuf
                                                                   Length: 64 (0x40) bytes
                                                                   0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                   0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                 )
                                                               )
                                                             val:
                                                               (Add
                                                                 (Var "arg1")
                                                                 (SLoad
                                                                   slot:
                                                                     (Keccak
                                                                       (ConcreteBuf
                                                                         Length: 64 (0x40) bytes
                                                                         0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                         0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                         0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                         0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                       )
                                                                     )
                                                                   storage:
                                                                     (ConcreteStore
                                                                       vals:
                                                                         (0x2,0x52b7d2dcc80cd2e4000000)
                                                                         (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                         (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                         (0x5,0x6)
                                                                         (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
                                                                         (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
                                                                         (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
                                                                         (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
                                                                     )
                                                                 )
                                                               )
                                                             store:
                                                               (SStore
                                                                 slot:
                                                                   2
                                                                 val:
                                                                   (Add
                                                                     100000000000000000000000000
                                                                     (Var "arg1")
                                                                   )
                                                                 store:
                                                                   (ConcreteStore
                                                                     vals:
                                                                       (0x2,0x52b7d2dcc80cd2e4000000)
                                                                       (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                       (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                       (0x5,0x6)
                                                                       (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
                                                                       (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
                                                                       (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
                                                                       (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
                                                                   )
                                                               )
                                                           )
                                                       )
                                                   )
                                                 buf:
                                                   (WriteWord
                                                     idx:
                                                       356
                                                     val:
                                                       (SLoad
                                                         slot:
                                                           (Keccak
                                                             (WriteWord
                                                               idx:
                                                                 0
                                                               val:
                                                                 (And
                                                                   1461501637330902918203684832716283019655932542975
                                                                   (SLoad
                                                                     slot:
                                                                       (Keccak
                                                                         (ConcreteBuf
                                                                           Length: 32 (0x20) bytes
                                                                           0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                           0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
                                                                         )
                                                                       )
                                                                     storage:
                                                                       (ConcreteStore
                                                                         vals:
                                                                           (0x40,0x12309ce54000)
                                                                           (0x41,0x7)
                                                                           (0x42,0x53b1daa2fd98364)
                                                                           (0x43,0x493b9f4e9de52f7)
                                                                           (0x44,0x5af3107a4000)
                                                                           (0x45,0xde0b6b3a7640000)
                                                                           (0x46,0x470de4df820000)
                                                                           (0x47,0xacab)
                                                                           (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                                                           (0x49,0x5)
                                                                           (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                                                           (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                                                           (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                                                           (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                                                           (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                                                           (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                                                           (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                                                           (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                                                           (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                                                           (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                                                           (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                                                           (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                                                           (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                                                           (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                                                           (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                                                           (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                                                           (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                                                           (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                                                           (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                                                       )
                                                                   )
                                                                 )
                                                               buf:
                                                                 (ConcreteBuf
                                                                   Length: 64 (0x40) bytes
                                                                   0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                 )
                                                             )
                                                           )
                                                         storage:
                                                           (ConcreteStore
                                                             vals:
                                                               (0x26641518f4b7bf06fa1fb88ef04b7a674f044e4fbd72991bc270179ff7ed0c18,0x5f5d48f)
                                                               (0x5a0e0e84b8e14f753aeb6217fac482fea39f5cbd3a329e67ee31e207cac61688,0x5f5f870)
                                                               (0x76bb3c6704741919db3f74b923a6ce6f7fe408a21a0e46eb9ad13baf100c5592,0x5f59ced)
                                                               (0x94649c886cb1d65286e760708e6accc6a2b58312342335e67c4d299af3f63c02,0x5f5f870)
                                                               (0x9e223a8a488383451ed2e2559b432dd3909f3740176bd68e85cacde97cd5b27a,0x5f5d48f)
                                                           )
                                                       )
                                                     buf:
                                                       (WriteWord
                                                         idx:
                                                           360
                                                         val:
                                                           (And
                                                             1461501637330902918203684832716283019655932542975
                                                             (SLoad
                                                               slot:
                                                                 (Keccak
                                                                   (ConcreteBuf
                                                                     Length: 32 (0x20) bytes
                                                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
                                                                   )
                                                                 )
                                                               storage:
                                                                 (ConcreteStore
                                                                   vals:
                                                                     (0x40,0x12309ce54000)
                                                                     (0x41,0x7)
                                                                     (0x42,0x53b1daa2fd98364)
                                                                     (0x43,0x493b9f4e9de52f7)
                                                                     (0x44,0x5af3107a4000)
                                                                     (0x45,0xde0b6b3a7640000)
                                                                     (0x46,0x470de4df820000)
                                                                     (0x47,0xacab)
                                                                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                                                     (0x49,0x5)
                                                                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                                                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                                                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                                                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                                                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                                                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                                                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                                                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                                                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                                                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                                                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                                                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                                                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                                                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                                                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                                                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                                                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                                                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                                                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                                                 )
                                                             )
                                                           )
                                                         buf:
                                                           (ConcreteBuf
                                                             Length: 392 (0x188) bytes
                                                             0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
                                                             0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
                                                             0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
                                                             0040:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0050:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 80   ................
                                                             0060:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0070:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0080:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0090:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00a0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00b0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00c0:   00 00 ac ab  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00d0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00e0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00f0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0100:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0110:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 d6   ................
                                                             0120:   44 6b fc 84  00 00 00 00  00 00 00 00  00 00 00 00   Dk..............
                                                             0130:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 cb   ................
                                                             0140:   73 d8 c0 8b  00 00 00 00  00 00 00 00  00 00 00 00   s...............
                                                             0150:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 a0   ................
                                                             0160:   77 c1 b0 9f  b3 59 6f 07  00 00 00 00  00 00 00 00   w....Yo.........
                                                             0170:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0180:   00 00 00 00  00 00 00 00                             ........
                                                           )
                                                       )
                                                   )
                                               )
                                           )
                                       )
                                   )
                               )
                           )
                       )
                     dst:
                       (ConcreteBuf "")
                   )
                 )
               storage:
                 (ConcreteStore
                   vals:
                     (0x40,0x12309ce54000)
                     (0x41,0x7)
                     (0x42,0x53b1daa2fd98364)
                     (0x43,0x493b9f4e9de52f7)
                     (0x44,0x5af3107a4000)
                     (0x45,0xde0b6b3a7640000)
                     (0x46,0x470de4df820000)
                     (0x47,0xacab)
                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                     (0x49,0x5)
                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                 )
             )
           )
         )
     - Unexpected Symbolic Arguments to Opcode
       msg: "Unable to determine a call target"
       opcode: STATICCALL
       program counter: 9382
       arguments: 
         (And
           1461501637330902918203684832716283019655932542975
           (And
             1461501637330902918203684832716283019655932542975
             (SLoad
               slot:
                 (Keccak
                   (CopySlice
                     srcOffset: 0
                     dstOffset: 0
                     size:      64
                     src:
                       (WriteWord
                         idx:
                           0
                         val:
                           (And
                             1461501637330902918203684832716283019655932542975
                             (SLoad
                               slot:
                                 (Keccak
                                   (ConcreteBuf
                                     Length: 32 (0x20) bytes
                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
                                   )
                                 )
                               storage:
                                 (ConcreteStore
                                   vals:
                                     (0x40,0x12309ce54000)
                                     (0x41,0x7)
                                     (0x42,0x53b1daa2fd98364)
                                     (0x43,0x493b9f4e9de52f7)
                                     (0x44,0x5af3107a4000)
                                     (0x45,0xde0b6b3a7640000)
                                     (0x46,0x470de4df820000)
                                     (0x47,0xacab)
                                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                     (0x49,0x5)
                                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                 )
                             )
                           )
                         buf:
                           (WriteWord
                             idx:
                               32
                             val:
                               74
                             buf:
                               (WriteWord
                                 idx:
                                   64
                                 val:
                                   388
                                 buf:
                                   (WriteWord
                                     idx:
                                       128
                                     val:
                                       100
                                     buf:
                                       (WriteWord
                                         idx:
                                           160
                                         val:
                                           16156842317565293874272834530371880720966471053262404558597773956279093428224
                                         buf:
                                           (WriteWord
                                             idx:
                                               196
                                             val:
                                               (And
                                                 1461501637330902918203684832716283019655932542975
                                                 (SLoad
                                                   slot:
                                                     (Keccak
                                                       (ConcreteBuf
                                                         Length: 64 (0x40) bytes
                                                         0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
                                                         0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
                                                         0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                         0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
                                                       )
                                                     )
                                                   storage:
                                                     (ConcreteStore
                                                       vals:
                                                         (0x40,0x12309ce54000)
                                                         (0x41,0x7)
                                                         (0x42,0x53b1daa2fd98364)
                                                         (0x43,0x493b9f4e9de52f7)
                                                         (0x44,0x5af3107a4000)
                                                         (0x45,0xde0b6b3a7640000)
                                                         (0x46,0x470de4df820000)
                                                         (0x47,0xacab)
                                                         (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                                         (0x49,0x5)
                                                         (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                                         (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                                         (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                                         (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                                         (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                                         (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                                         (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                                         (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                                         (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                                         (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                                         (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                                         (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                                         (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                                         (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                                         (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                                         (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                                         (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                                         (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                                         (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                                         (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                                     )
                                                 )
                                               )
                                             buf:
                                               (WriteWord
                                                 idx:
                                                   228
                                                 val:
                                                   (SLoad
                                                     slot:
                                                       (Keccak
                                                         (ConcreteBuf
                                                           Length: 64 (0x40) bytes
                                                           0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                           0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                           0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                           0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                         )
                                                       )
                                                     storage:
                                                       (SStore
                                                         slot:
                                                           (Keccak
                                                             (WriteWord
                                                               idx:
                                                                 32
                                                               val:
                                                                 (Keccak
                                                                   (ConcreteBuf
                                                                     Length: 64 (0x40) bytes
                                                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                     0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 01   ................
                                                                   )
                                                                 )
                                                               buf:
                                                                 (ConcreteBuf
                                                                   Length: 64 (0x40) bytes
                                                                   0000:   00 00 00 00  00 00 00 00  00 00 00 00  78 52 cb be   ............xR..
                                                                   0010:   68 18 a4 b4  52 ea cf 11  1c 87 d7 46  78 9e 7d 09   h...R......Fx.}.
                                                                   0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                 )
                                                             )
                                                           )
                                                         val:
                                                           (Add
                                                             (Var "arg1")
                                                             (SLoad
                                                               slot:
                                                                 (Keccak
                                                                   (ConcreteBuf
                                                                     Length: 64 (0x40) bytes
                                                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                     0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   )
                                                                 )
                                                               storage:
                                                                 (ConcreteStore
                                                                   vals:
                                                                     (0x2,0x52b7d2dcc80cd2e4000000)
                                                                     (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                     (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                     (0x5,0x6)
                                                                     (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
                                                                     (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
                                                                     (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
                                                                     (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
                                                                 )
                                                             )
                                                           )
                                                         store:
                                                           (SStore
                                                             slot:
                                                               (Keccak
                                                                 (ConcreteBuf
                                                                   Length: 64 (0x40) bytes
                                                                   0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                   0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                 )
                                                               )
                                                             val:
                                                               (Add
                                                                 (Var "arg1")
                                                                 (SLoad
                                                                   slot:
                                                                     (Keccak
                                                                       (ConcreteBuf
                                                                         Length: 64 (0x40) bytes
                                                                         0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                         0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
                                                                         0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                         0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                       )
                                                                     )
                                                                   storage:
                                                                     (ConcreteStore
                                                                       vals:
                                                                         (0x2,0x52b7d2dcc80cd2e4000000)
                                                                         (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                         (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                         (0x5,0x6)
                                                                         (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
                                                                         (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
                                                                         (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
                                                                         (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
                                                                     )
                                                                 )
                                                               )
                                                             store:
                                                               (SStore
                                                                 slot:
                                                                   2
                                                                 val:
                                                                   (Add
                                                                     100000000000000000000000000
                                                                     (Var "arg1")
                                                                   )
                                                                 store:
                                                                   (ConcreteStore
                                                                     vals:
                                                                       (0x2,0x52b7d2dcc80cd2e4000000)
                                                                       (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                       (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
                                                                       (0x5,0x6)
                                                                       (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
                                                                       (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
                                                                       (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
                                                                       (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
                                                                   )
                                                               )
                                                           )
                                                       )
                                                   )
                                                 buf:
                                                   (WriteWord
                                                     idx:
                                                       356
                                                     val:
                                                       (SLoad
                                                         slot:
                                                           (Keccak
                                                             (WriteWord
                                                               idx:
                                                                 0
                                                               val:
                                                                 (And
                                                                   1461501637330902918203684832716283019655932542975
                                                                   (SLoad
                                                                     slot:
                                                                       (Keccak
                                                                         (ConcreteBuf
                                                                           Length: 32 (0x20) bytes
                                                                           0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                           0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
                                                                         )
                                                                       )
                                                                     storage:
                                                                       (ConcreteStore
                                                                         vals:
                                                                           (0x40,0x12309ce54000)
                                                                           (0x41,0x7)
                                                                           (0x42,0x53b1daa2fd98364)
                                                                           (0x43,0x493b9f4e9de52f7)
                                                                           (0x44,0x5af3107a4000)
                                                                           (0x45,0xde0b6b3a7640000)
                                                                           (0x46,0x470de4df820000)
                                                                           (0x47,0xacab)
                                                                           (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                                                           (0x49,0x5)
                                                                           (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                                                           (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                                                           (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                                                           (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                                                           (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                                                           (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                                                           (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                                                           (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                                                           (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                                                           (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                                                           (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                                                           (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                                                           (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                                                           (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                                                           (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                                                           (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                                                           (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                                                           (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                                                           (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                                                           (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                                                       )
                                                                   )
                                                                 )
                                                               buf:
                                                                 (ConcreteBuf
                                                                   Length: 64 (0x40) bytes
                                                                   0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                   0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                 )
                                                             )
                                                           )
                                                         storage:
                                                           (ConcreteStore
                                                             vals:
                                                               (0x26641518f4b7bf06fa1fb88ef04b7a674f044e4fbd72991bc270179ff7ed0c18,0x5f5d48f)
                                                               (0x5a0e0e84b8e14f753aeb6217fac482fea39f5cbd3a329e67ee31e207cac61688,0x5f5f870)
                                                               (0x76bb3c6704741919db3f74b923a6ce6f7fe408a21a0e46eb9ad13baf100c5592,0x5f59ced)
                                                               (0x94649c886cb1d65286e760708e6accc6a2b58312342335e67c4d299af3f63c02,0x5f5f870)
                                                               (0x9e223a8a488383451ed2e2559b432dd3909f3740176bd68e85cacde97cd5b27a,0x5f5d48f)
                                                           )
                                                       )
                                                     buf:
                                                       (WriteWord
                                                         idx:
                                                           360
                                                         val:
                                                           (And
                                                             1461501637330902918203684832716283019655932542975
                                                             (SLoad
                                                               slot:
                                                                 (Keccak
                                                                   (ConcreteBuf
                                                                     Length: 32 (0x20) bytes
                                                                     0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                                     0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
                                                                   )
                                                                 )
                                                               storage:
                                                                 (ConcreteStore
                                                                   vals:
                                                                     (0x40,0x12309ce54000)
                                                                     (0x41,0x7)
                                                                     (0x42,0x53b1daa2fd98364)
                                                                     (0x43,0x493b9f4e9de52f7)
                                                                     (0x44,0x5af3107a4000)
                                                                     (0x45,0xde0b6b3a7640000)
                                                                     (0x46,0x470de4df820000)
                                                                     (0x47,0xacab)
                                                                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                                                                     (0x49,0x5)
                                                                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                                                                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                                                                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                                                                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                                                                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                                                                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                                                                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                                                                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                                                                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                                                                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                                                                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                                                                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                                                                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                                                                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                                                                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                                                                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                                                                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                                                                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                                                                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                                                                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                                                                 )
                                                             )
                                                           )
                                                         buf:
                                                           (ConcreteBuf
                                                             Length: 392 (0x188) bytes
                                                             0000:   00 00 00 00  00 00 00 00  00 00 00 00  d9 53 22 74   .............S"t
                                                             0010:   58 65 82 27  19 16 4b 1f  c1 67 93 07  54 c2 48 de   Xe.'..K..g..T.H.
                                                             0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 4a   ...............J
                                                             0040:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0050:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 80   ................
                                                             0060:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0070:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0080:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0090:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00a0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00b0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00c0:   00 00 ac ab  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00d0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00e0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             00f0:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0100:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0110:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 d6   ................
                                                             0120:   44 6b fc 84  00 00 00 00  00 00 00 00  00 00 00 00   Dk..............
                                                             0130:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 cb   ................
                                                             0140:   73 d8 c0 8b  00 00 00 00  00 00 00 00  00 00 00 00   s...............
                                                             0150:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 a0   ................
                                                             0160:   77 c1 b0 9f  b3 59 6f 07  00 00 00 00  00 00 00 00   w....Yo.........
                                                             0170:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                                             0180:   00 00 00 00  00 00 00 00                             ........
                                                           )
                                                       )
                                                   )
                                               )
                                           )
                                       )
                                   )
                               )
                           )
                       )
                     dst:
                       (ConcreteBuf "")
                   )
                 )
               storage:
                 (ConcreteStore
                   vals:
                     (0x40,0x12309ce54000)
                     (0x41,0x7)
                     (0x42,0x53b1daa2fd98364)
                     (0x43,0x493b9f4e9de52f7)
                     (0x44,0x5af3107a4000)
                     (0x45,0xde0b6b3a7640000)
                     (0x46,0x470de4df820000)
                     (0x47,0xacab)
                     (0x48,0x2beec76ec7ffde5ddec5c7f7bc28375a139d8dec)
                     (0x49,0x5)
                     (0xbcbfa19733cec6d55a5a287f85260feea2d177a81ed4201be8f853017b387b5,0x1)
                     (0x13897ad23775ee38cfc3ba4e9fdb836d9e8cc936c144e95e360abde83213ce33,0x1)
                     (0x18f40bf710eef8eb8b14a1cd644b7b8f6abe1c497e5380f59172f91f726b5ca9,0x1)
                     (0x33c01989199dc6bcc08e31fbeca7c654030b9d3fd3bda7c618f691ba2fc13e71,0x1)
                     (0x343bdc6eebb233b371e49d1a36a68177caf342e418df1d089bac9bf75e021781,0x1)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55,0xd95322745865822719164b1fc167930754c248de)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f56,0x6eecb916b78765d6b277bff328684db91f4f6a5d)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f57,0x8840f3a24be3971c313f435453c9c749d3f936c)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f58,0xf64a197b987fd4400a0887909c067a37ae209e1a)
                     (0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f59,0xe663b9e12c29924565ee36fbb8c4a3191971f4da)
                     (0x42776d27e37c472cdec0856a9d58feaee2fde7e868fb53f36330a4a42e3a58a9,0x1)
                     (0x46eda384002bf299f519d3a9ef467d4225b0a66aa70e94ae3d558d3d71330e2c,0x5d51444bdd2bc621788319959c657af0f9d619c5)
                     (0x58b5e753403da07442b646a1311cfc1ac7ee398f664e8ba00f86755a18aafbf4,0x4)
                     (0x7f38886520bb8e417575a1c3c82c9404d0055e706357f640ecf1c94b462da90c,0xbb8daedddc5bb0483a4f44bfa628cc5daa72e2d1)
                     (0x9016d09d72d40fdae2fd8ceac6b6234c7706214fd39c1cd1e609a0528c199300,0xacab)
                     (0x9b779b17422d0df92223018b32b4d1fa46e071723d6817e2486d003becc55f00,0x2)
                     (0x9f1fd62955e083dd560a43035289fc6cb1df5e1e76c50e41f8a46ed187b86f8a,0xc2bbaea76ec6b85a0b90f04de8ce4476d6e27374)
                     (0xae6c11380398076a1cf99b4510e55da6b3062b4c9f858fa16277e672f2a5bd79,0x841c03e9bf1c008fe90b2dedc429d497795301a5)
                     (0xba962bc6bb35f1f8f35f5da32ced64e0c82d793a2d77283935f688b01f0cb163,0x0)
                     (0xcd5ed15c6e187e77e9aee88184c21f4f2182ab5827cb3b7e07fbedcd63f03300,0x0)
                     (0xebd33f63ba5dda53a45af725baed5628cdad261db5319da5f5d921521fe1161d,0x5842cfa0028e51f1b74c9dca4a59ef0e05544163)
                     (0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00,0x1)
                     (0xf4344425ee2bee17a4c8a465e6fb8acc37882812cb3ff3774a8123a9a581eb50,0x3)
                     (0xf524c08d9fb11ff0e21253f37caa0ffe703c4ad2cf61a0f6771265f91f5907a8,0x2)
                 )
             )
           )
         )

msooseth · 2024-12-18T10:46:22Z

Hi,

Thanks for the update! It seems like the system made progress, but got stuck on a more convoluted expression. Our simplification system can't deal with this yet. Either running the SMT solver, or a more complete simplification would solve this. Basically, this:

(SLoad
  slot:
    (Keccak
      (ConcreteBuf
        Length: 32 (0x20) bytes
        0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
        0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 49   ...............I
      )
    )
  storage:
    (ConcreteStore:[...]
        (0x37e472f504e93744[...],0xd95322[...])

should return 0xd95322745865822719164b1fc167930754c248de because:

cast keccak 0x0000000000000000000000000000000000000000000000000000000000000049
0x37e472f504e93744df80d87316862f9a8fd41a7bc266c723bf77df7866d75f55

And that value is in the map already, and maps to 0xd9532274...

I'll see if I can fix the simplification to do this. Otherwise, I'll see if I can make the SMT solver work for us here. Both would be best, using the SMT solver as a safety net in case the simplification fails.

msooseth · 2024-12-18T14:16:04Z

Looking at the expression in more detail:

(Add
  (Var "arg1")
  (SLoad
    slot:
      (Keccak
        (ConcreteBuf
          Length: 64 (0x40) bytes
          0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
          0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 ac ab   ................
          0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
          0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
        )
      )
    storage:
      (ConcreteStore
        vals:
          (0x2,0x52b7d2dcc80cd2e4000000)
          (0x3,0x5553444300000000000000000000000000000000000000000000000000000008)
          (0x4,0x5553444300000000000000000000000000000000000000000000000000000008)
          (0x5,0x6)
          (0xa7a5630c9a1f134996676afc8e426bff56e8c5b1e353b96f9df7f5499b3701a,0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
          (0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15,0x0)
          (0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d,0xa077c1b09f)
          (0xf3f00ab703b87ba8b65e1fbf147cda608927ab8fd3d225c2a15738b8edfbecc9,0x52b7d2dcc80c326c3e4f61)
      )
  )
)

Means this expression can't really be fully resolved I think? If var1 happens to be 0, then that resolves to:

$ cast keccak 0x000000000000000000000000000000000000000000000000000000000000acab0000000000000000000000000000000000000000000000000000000000000000
0x3137fb031ab8b2e29680f231eff07227e6c5bc0d79f70a3d25ac9e5631b3bc15

which is in the map, and is mapped to 0x0. However, it is unknown if one could make it something other than 0, and hit another value. If it was 0xbbc725cced14aac8bf801ddd2d2df9c8bb3714869cab90d72a072f3808fe04f8 then we'd hit 0xecff20d007cd5dab5601100f1d1e6bf0a1fcd09416a29b144fb3cd8e3ab1c10d, and the output would be 0xa077c1b09f.

Do you know where this var1 comes from? My guess is that it's a parameter to the prove_... function, we name them var1, var2.... Can you fix it to some value via e.g. require(var1 == something);? Would it make sense to fix it to some value? If not, and is attacker controlled, I would consider doing the following. Make it into an input like uint var1, and when verifying, instead of doing something like:

function (uint addr,. ...)
[...]
uint ret = staticcall (.... attacker controlled address/stuff via addr ...);

write:

function (uint addr, uint attacker_controlled, ...)
[...]
uint ret = attacker_controlled;

Then the return value is still fully controllable by the attacker. I think the only real difference is that the gas could be different in the 2nd case.

What do you think?

msooseth · 2024-12-18T15:38:59Z

Hmmmm I had a chat with my colleague @d-xo and actually you don't need to do that hack. We can do the hack ourselves -- in case we can't resolve the staticcall, we just return a symbolic object. I'll see how I can implement it, shouldn't be too difficult. Then we could handle this one quite well. I'd still like to invoke the SMT solver, but for the moment this overapproximation may just do the trick.

msooseth · 2024-12-19T17:22:14Z

The PR #620 should fix the issue that you are having now. You will need to merge the two PRs, #619 and #620 into main and then it should work I believe. I added some tests to both PRs, so things should work, but I would be grateful of course for some minimal examples, if you can provide, that can trigger this bug.

Note that we should still use an SMT solver, as it would be more precise, and would potentially give less false positives. The current overapproximation that we do now could lead to cases where in the real world the assert() cannot trigger, but in the symbolic execution world, it can. So there's still a todo here. However, for the moment, I think these two PRs should do the trick.

Let me know how it goes,

Mate

msooseth · 2025-01-02T13:15:15Z

From discussing with the developers, it seems like #619 and #620 together fixes the issue, yay :) I will close once both have been merged!

msooseth mentioned this issue Dec 17, 2024

Fixing missing concKeccakSimpExpr for wordToAddr, maybeLitByte, etc. #619

Merged

4 tasks

msooseth added the in progress label Dec 23, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`STATICCALL` Error "Unable to determine a call target" #618

`STATICCALL` Error "Unable to determine a call target" #618

chief-mobius commented Dec 17, 2024

msooseth commented Dec 17, 2024

msooseth commented Dec 17, 2024

msooseth commented Dec 17, 2024 •

edited

Loading

chief-mobius commented Dec 18, 2024

msooseth commented Dec 18, 2024

msooseth commented Dec 18, 2024

msooseth commented Dec 18, 2024

msooseth commented Dec 19, 2024

msooseth commented Jan 2, 2025

STATICCALL Error "Unable to determine a call target" #618

STATICCALL Error "Unable to determine a call target" #618

Comments

chief-mobius commented Dec 17, 2024

msooseth commented Dec 17, 2024

msooseth commented Dec 17, 2024

msooseth commented Dec 17, 2024 • edited Loading

chief-mobius commented Dec 18, 2024

msooseth commented Dec 18, 2024

msooseth commented Dec 18, 2024

msooseth commented Dec 18, 2024

msooseth commented Dec 19, 2024

msooseth commented Jan 2, 2025

`STATICCALL` Error "Unable to determine a call target" #618

`STATICCALL` Error "Unable to determine a call target" #618

msooseth commented Dec 17, 2024 •

edited

Loading