Skip to content

Commit b49c90b

Browse files
RaoulSchaffranekanvacaru
RaoulSchaffranek
and
anvacaru
authored
Trace code address (#2790)
* Trace code address * Fix tests * Fix more tests * Fix more tests * Fix more tests * Fix more tests * Fix more tests * Fix more tests --------- Co-authored-by: Andrei Văcaru <[email protected]>
1 parent b2e84d1 commit b49c90b

File tree

167 files changed

+435
-60
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

167 files changed

+435
-60
lines changed

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,8 @@ In the comments next to each cell, we've marked which component of the YellowPap
7575
7676
<static> false </static>
7777
<callDepth> 0 </callDepth>
78+
79+
<codeAddr> .Account </codeAddr>
7880
</callState>
7981
8082
<versionedHashes> .List </versionedHashes>
@@ -1675,6 +1677,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
16751677
<callData> _ => ARGS </callData>
16761678
<callValue> _ => APPVALUE </callValue>
16771679
<id> _ => ACCTTO </id>
1680+
<codeAddr> _ => ACCTCODE </codeAddr>
16781681
<gas> GAVAIL:Gas => #if USEGAS #then GCALL:Gas #else GAVAIL:Gas #fi </gas>
16791682
<callGas> GCALL:Gas => #if USEGAS #then 0:Gas #else GCALL:Gas #fi </callGas>
16801683
<caller> _ => ACCTFROM </caller>
@@ -1797,6 +1800,7 @@ System Transaction Configuration
17971800
<callData> _ => ARGS </callData>
17981801
<callValue> _ => 0 </callValue>
17991802
<id> _ => ACCTTO </id>
1803+
<codeAddr> _ => ACCTTO </codeAddr>
18001804
<gas> GAVAIL:Gas => #if USEGAS #then SYSTEMTXGAS:Gas #else GAVAIL:Gas #fi </gas>
18011805
<callGas> GCALL:Gas => #if USEGAS #then 0:Gas #else GCALL:Gas #fi </callGas>
18021806
<caller> _ => SYSTEM_ADDRESS </caller>
@@ -1947,6 +1951,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
19471951
<useGas> USEGAS </useGas>
19481952
<schedule> SCHED </schedule>
19491953
<id> _ => ACCTTO </id>
1954+
<codeAddr> _ => ACCTTO </codeAddr>
19501955
<gas> GAVAIL => #if USEGAS #then GCALL #else GAVAIL #fi </gas>
19511956
<callGas> GCALL => #if USEGAS #then 0 #else GCALL #fi </callGas>
19521957
<caller> _ => ACCTFROM </caller>

‎tests/failing/ContractCreationSpam_d0g0v0.json.expected

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,9 @@
7474
<callDepth>
7575
-1
7676
</callDepth>
77+
<codeAddr>
78+
.Account
79+
</codeAddr>
7780
</callState>
7881
<versionedHashes>
7982
.List

‎tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,9 @@
7474
<callDepth>
7575
-1
7676
</callDepth>
77+
<codeAddr>
78+
.Account
79+
</codeAddr>
7780
</callState>
7881
<versionedHashes>
7982
.List

‎tests/specs/benchmarks/address00-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module ADDRESS00-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634b64e492146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505060c4565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008190509190505600a165627a7a72305820fef7ba925e24a935e59bb401907893518a66095fa9e2c2506b29051dfdaa6ff80029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634b64e492146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505060c4565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008190509190505600a165627a7a72305820fef7ba925e24a935e59bb401907893518a66095fa9e2c2506b29051dfdaa6ff80029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData("execute", #address(A0)) </callData> // msg.data
2526
<callValue> 0 </callValue> // msg.value

‎tests/specs/benchmarks/bytes00-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module BYTES00-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806309c5eabe146044575b600080fd5b348015604f57600080fd5b5060a8600480360381019080803590602001908201803590602001908080601f016020809104026020016040519081016040528093929190818152602001838380828437820191505050505050919291929050505060be565b6040518082815260200191505060405180910390f35b6000815190509190505600a165627a7a72305820443b6929f0411657e3b5f5371823da4795cb8ece704713e7934fea316a2af24a0029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806309c5eabe146044575b600080fd5b348015604f57600080fd5b5060a8600480360381019080803590602001908201803590602001908080601f016020809104026020016040519081016040528093929190818152602001838380828437820191505050505050919291929050505060be565b6040518082815260200191505060405180910390f35b6000815190509190505600a165627a7a72305820443b6929f0411657e3b5f5371823da4795cb8ece704713e7934fea316a2af24a0029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData("execute", #bytes(#bufStrict(DATA_LEN, DATA))) </callData> // msg.data
2526
<callValue> 0 </callValue> // msg.value

‎tests/specs/benchmarks/dynamicarray00-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module DYNAMICARRAY00-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData2("execute(uint256[])", #array(#uint256(1), 3, #uint256(A0), #uint256(A1), #uint256(A2), .TypedArgs)) </callData> // msg.data
2526
<callValue> 0 </callValue> // msg.value

‎tests/specs/benchmarks/ecrecover00-siginvalid-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module ECRECOVER00-SIGINVALID-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634480949514610046575b600080fd5b34801561005257600080fd5b506100a06004803603608081101561006957600080fd5b8101908080359060200190929190803560ff16906020019092919080359060200190929190803590602001909291905050506100e2565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008060018686868660405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa158015610142573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561018957600080fd5b8091505094935050505056fea165627a7a72305820ec9368f63b82a680b2493003123eec414f661d1259fdf9d0082a8815d68a9a7e0029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634480949514610046575b600080fd5b34801561005257600080fd5b506100a06004803603608081101561006957600080fd5b8101908080359060200190929190803560ff16906020019092919080359060200190929190803590602001909291905050506100e2565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008060018686868660405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa158015610142573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561018957600080fd5b8091505094935050505056fea165627a7a72305820ec9368f63b82a680b2493003123eec414f661d1259fdf9d0082a8815d68a9a7e0029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData("execute", #bytes32(HASH), #uint8(SIGV), #bytes32(SIGR), #bytes32(SIGS)) </callData> // msg.data
2526
<callValue> 0 </callValue> // msg.value

‎tests/specs/benchmarks/ecrecover00-sigvalid-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module ECRECOVER00-SIGVALID-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634480949514610046575b600080fd5b34801561005257600080fd5b506100a06004803603608081101561006957600080fd5b8101908080359060200190929190803560ff16906020019092919080359060200190929190803590602001909291905050506100e2565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008060018686868660405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa158015610142573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561018957600080fd5b8091505094935050505056fea165627a7a72305820ec9368f63b82a680b2493003123eec414f661d1259fdf9d0082a8815d68a9a7e0029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff1680634480949514610046575b600080fd5b34801561005257600080fd5b506100a06004803603608081101561006957600080fd5b8101908080359060200190929190803560ff16906020019092919080359060200190929190803590602001909291905050506100e2565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b60008060018686868660405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa158015610142573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561018957600080fd5b8091505094935050505056fea165627a7a72305820ec9368f63b82a680b2493003123eec414f661d1259fdf9d0082a8815d68a9a7e0029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData("execute", #bytes32(HASH), #uint8(SIGV), #bytes32(SIGR), #bytes32(SIGS)) </callData> // msg.data
2526
<callValue> 0 </callValue> // msg.value

‎tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module ECRECOVERLOOP00-SIG0-INVALID-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063e6daaf3c14610046575b600080fd5b34801561005257600080fd5b50610142600480360360e081101561006957600080fd5b810190808035906020019092919080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f8201169050808301925050505050509192919290505050610144565b005b60008090505b600281101561023d576000600186868460028110151561016657fe5b6020020151868560028110151561017957fe5b6020020151868660028110151561018c57fe5b602002015160405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa1580156101e8573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561022f57600080fd5b50808060010191505061014a565b505050505056fea165627a7a723058209cbe77475c348cf6ab4edd37fdfe35cef78a2f1a391aad5c7b6fdbace01dd96d0029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063e6daaf3c14610046575b600080fd5b34801561005257600080fd5b50610142600480360360e081101561006957600080fd5b810190808035906020019092919080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f8201169050808301925050505050509192919290505050610144565b005b60008090505b600281101561023d576000600186868460028110151561016657fe5b6020020151868560028110151561017957fe5b6020020151868660028110151561018c57fe5b602002015160405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa1580156101e8573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561022f57600080fd5b50808060010191505061014a565b505050505056fea165627a7a723058209cbe77475c348cf6ab4edd37fdfe35cef78a2f1a391aad5c7b6fdbace01dd96d0029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData2("execute(bytes32,uint8[2],bytes32[2],bytes32[2])", #bytes32(HASH),
2526
#uint8(SIGV0), #uint8(SIGV1),

‎tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ module ECRECOVERLOOP00-SIG1-INVALID-SPEC
1919
<callState>
2020
<program> #parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063e6daaf3c14610046575b600080fd5b34801561005257600080fd5b50610142600480360360e081101561006957600080fd5b810190808035906020019092919080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f8201169050808301925050505050509192919290505050610144565b005b60008090505b600281101561023d576000600186868460028110151561016657fe5b6020020151868560028110151561017957fe5b6020020151868660028110151561018c57fe5b602002015160405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa1580156101e8573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561022f57600080fd5b50808060010191505061014a565b505050505056fea165627a7a723058209cbe77475c348cf6ab4edd37fdfe35cef78a2f1a391aad5c7b6fdbace01dd96d0029") </program>
2121
<jumpDests> #computeValidJumpDests(#parseByteStack("0x608060405260043610610041576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff168063e6daaf3c14610046575b600080fd5b34801561005257600080fd5b50610142600480360360e081101561006957600080fd5b810190808035906020019092919080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f820116905080830192505050505050919291929080604001906002806020026040519081016040528092919082600260200280828437600081840152601f19601f8201169050808301925050505050509192919290505050610144565b005b60008090505b600281101561023d576000600186868460028110151561016657fe5b6020020151868560028110151561017957fe5b6020020151868660028110151561018c57fe5b602002015160405160008152602001604052604051808581526020018460ff1660ff1681526020018381526020018281526020019450505050506020604051602081039080840390855afa1580156101e8573d6000803e3d6000fd5b505050602060405103519050600073ffffffffffffffffffffffffffffffffffffffff168173ffffffffffffffffffffffffffffffffffffffff1611151561022f57600080fd5b50808060010191505061014a565b505050505056fea165627a7a723058209cbe77475c348cf6ab4edd37fdfe35cef78a2f1a391aad5c7b6fdbace01dd96d0029")) </jumpDests>
22-
<id> CONTRACT_ID </id> // this
22+
<id> CONTRACT_ID </id>
23+
<codeAddr> CONTRACT_ID </codeAddr> // this
2324
<caller> MSG_SENDER </caller> // msg.sender
2425
<callData> #abiCallData2("execute(bytes32,uint8[2],bytes32[2],bytes32[2])", #bytes32(HASH),
2526
#uint8(SIGV0), #uint8(SIGV1),

0 commit comments

Comments
 (0)