Skip to content

Instantly share code, notes, and snippets.

@MrChico

MrChico/someContract

Created July 16, 2020 10:42
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save MrChico/1f33685f65f66edad3ded96a3b25e5ba to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save MrChico/1f33685f65f66edad3ded96a3b25e5ba to your computer and use it in GitHub Desktop.
Download ZIP
Raw
someContract
time hevm symbolic --code $(<noidea.bin-runtime) --solver cvc4 --get-models
checking postcondition...
Q.E.D.
Explored: 53 branches without assertion violations
However, 2 branch(es) errored while exploring:
["Unexpected symbolic argument at opcode: OpExtcodesize. Not supported (yet!)","Unexpected symbolic argument at opcode: OpCalldatacopy. Not supported (yet!)"]
-- Branch (1/53) --
Calldata:
0x06973ccf
Caller:
0
Callvalue:
0
Reverted
-- Branch (2/53) --
Calldata:
0xf3fef3a3
Caller:
0
Callvalue:
4722366482869645213696
Reverted
-- Branch (3/53) --
Calldata:
0xf3fef3a3
Caller:
0
Callvalue:
0
Reverted
-- Branch (4/53) --
Calldata:
0xf3fef3a300000000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Stopped
-- Branch (5/53) --
Calldata:
0xd3184e80
Caller:
0
Callvalue:
2147483648
Reverted
-- Branch (6/53) --
Calldata:
0xd3184e80
Caller:
0
Callvalue:
0
Returned: 0x0000000000000000000000000000000000000000000000000000000000000001
-- Branch (7/53) --
Calldata:
0xd30f133d
Caller:
0
Callvalue:
1809251394333065553493296640760748560207343510400633813116524750123642650624
Reverted
-- Branch (8/53) --
Calldata:
0xd30f133d
Caller:
0
Callvalue:
0
Reverted
-- Branch (9/53) --
Calldata:
0xd30f133d000000000000000000000000800000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000f6f6e6c794261636b757041646d696e0000000000000000000000000000000000
-- Branch (10/53) --
Calldata:
0xd30f133d0000000000000000000800000000000000000000000000000000000000000000ffffffff
Caller:
0
Callvalue:
0
Reverted
-- Branch (11/53) --
Calldata:
0xd30f133d0000000000000000000800000000000000000000000000000000000004000000ffffffff
Caller:
0
Callvalue:
0
Stopped
-- Branch (12/53) --
Calldata:
0xc3068154
Caller:
0
Callvalue:
1298074214633706907132624082305024
Reverted
-- Branch (13/53) --
Calldata:
0xc3068154
Caller:
0
Callvalue:
0
Reverted
-- Branch (14/53) --
Calldata:
0xc30681540000000000000000000800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
730750818665451459101842416358141509827966271488
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000d6f6e6c794d61696e41646d696e00000000000000000000000000000000000000
-- Branch (15/53) --
Calldata:
0xc30681540000000000000000000800000000000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000f496e76616c696420616464726573730000000000000000000000000000000000
-- Branch (16/53) --
Calldata:
0xc30681540000000000000000000800000000000000000000000000000000000008000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Stopped
-- Branch (17/53) --
Calldata:
0x9f9abd5a
Caller:
0
Callvalue:
696898287454081973172991196020261297061888
Reverted
-- Branch (18/53) --
Calldata:
0x9f9abd5a
Caller:
0
Callvalue:
0
Returned: 0x0000000000000000000000000000000000000000000000000000000000000001
-- Branch (19/53) --
Calldata:
0x47e7ef24
Caller:
0
Callvalue:
1427247692705959881058285969449495136382746624
Reverted
-- Branch (20/53) --
Calldata:
0x47e7ef24
Caller:
0
Callvalue:
0
Reverted
-- Branch (21/53) --
Calldata:
0x47e7ef24000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Failed: UnexpectedSymbolicArg
-- Branch (22/53) --
Calldata:
0x47c7d49a
Caller:
0
Callvalue:
441711766194596082395824375185729628956870974218904739530401550323154944
Reverted
-- Branch (23/53) --
Calldata:
0x47c7d49a
Caller:
0
Callvalue:
0
Returned: 0x0000000000000000000000000000000000000000000000000000000000000000
-- Branch (24/53) --
Calldata:
0x3e5b1ee7
Caller:
0
Callvalue:
26959946667150639794667015087019630673637144422540572481103610249216
Reverted
-- Branch (25/53) --
Calldata:
0x3e5b1ee7
Caller:
0
Callvalue:
0
Reverted
-- Branch (26/53) --
Calldata:
0x3e5b1ee7000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Stopped
-- Branch (27/53) --
Calldata:
0x380b682d
Caller:
0
Callvalue:
36893488147419103232
Reverted
-- Branch (28/53) --
Calldata:
0x380b682d
Caller:
0
Callvalue:
0
Reverted
-- Branch (29/53) --
Calldata:
0x380b682d000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000f6f6e6c794261636b757041646d696e0000000000000000000000000000000000
-- Branch (30/53) --
Calldata:
0x380b682d0000000000000000000800000000000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000f496e76616c696420616464726573730000000000000000000000000000000000
-- Branch (31/53) --
Calldata:
0x380b682d0000000000000000000800000000000000000000000000000000000008000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Stopped
-- Branch (32/53) --
Calldata:
0x2f9b1956
Caller:
0
Callvalue:
81129638414606681695789005144064
Reverted
-- Branch (33/53) --
Calldata:
0x2f9b1956
Caller:
0
Callvalue:
0
Reverted
-- Branch (34/53) --
Calldata:
0x2f9b1956000000000000000000080000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000d6f6e6c794d61696e41646d696e00000000000000000000000000000000000000
-- Branch (35/53) --
Calldata:
0x2f9b19560000000000000000000800000000000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000c496e76616c696420726174650000000000000000000000000000000000000000
-- Branch (36/53) --
Calldata:
0x2f9b19560000000000000000000000000000000000000000000000000000000000000008ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Stopped
-- Branch (37/53) --
Calldata:
0x2f9b19560000000000000000000000000000000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted0x08c379a00000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000000c496e76616c696420726174650000000000000000000000000000000000000000
-- Branch (38/53) --
Calldata:
0x268d0626
Caller:
0
Callvalue:
8796093022208
Reverted
-- Branch (39/53) --
Calldata:
0x268d0626
Caller:
0
Callvalue:
0
Reverted
-- Branch (40/53) --
Calldata:
0x268d0626000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Stopped
-- Branch (41/53) --
Calldata:
0x1e59c529
Caller:
0
Callvalue:
8192
Reverted
-- Branch (42/53) --
Calldata:
0x1e59c529
Caller:
0
Callvalue:
0
Reverted
-- Branch (43/53) --
Calldata:
0x1e59c5290000000000000000000000000000000000100000000000000000000000000100ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted
-- Branch (44/53) --
Calldata:
0x1e59c5290000000000000000000000000000000000000000000000008000000000000100ffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
Caller:
0
Callvalue:
0
Reverted
-- Branch (45/53) --
Calldata:
0x1e59c52900000000000000000000000000000000000000000000000000000000000000fbffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff02
Caller:
0
Callvalue:
0
Reverted
-- Branch (46/53) --
Calldata:
0x1e59c52900000000000000000000000000000000000000000000000000000000000000dcffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff000000000000000000000000000000000000000000000000ffffffffffffff82
Caller:
0
Callvalue:
0
Reverted
-- Branch (47/53) --
Calldata:
0x1e59c52900000000000000000000000000000000000000000000000000000000000000e3ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000000000000000000082
Caller:
0
Callvalue:
0
Reverted
-- Branch (48/53) --
Calldata:
0x1e59c52900000000000000000000000000000000000000000000000000000000000000fbffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff61f9ffff7b00
Caller:
0
Callvalue:
0
Failed: UnexpectedSymbolicArg
-- Branch (49/53) --
Calldata:
0x1168222b
Caller:
0
Callvalue:
730750818665451459101842416358141509827966271488
Reverted
-- Branch (50/53) --
Calldata:
0x1168222b
Caller:
0
Callvalue:
0
Returned: 0x0000000000000000000000000000000000000000000000000000000000000001
-- Branch (51/53) --
Calldata:
0x07973ccf
Caller:
0
Callvalue:
8589934592
Reverted
-- Branch (52/53) --
Calldata:
0x07973ccf
Caller:
0
Callvalue:
0
Returned: 0x0000000000000000000000000000000000000000000000000000000000000000
-- Branch (53/53) --
Calldata:
0x
Caller:
0
Callvalue:
0
Reverted
hevm symbolic --code $(<noidea.bin-runtime) --solver cvc4 --get-models 409.13s user 4.44s system 101% cpu 6:48.22 total
@MrChico
Copy link
Author

MrChico commented Jul 16, 2020

This is the output of symbolically exploring https://etherscan.io/address/0xfa9ffdf4f8b2d74526021aa088486e5fa6f81132#code with hevm

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment