From 7b043358599aa82e6db44acd10e0284a02692ae8 Mon Sep 17 00:00:00 2001 From: Hao Xiao <87435252+spencerhaoxiao@users.noreply.github.com> Date: Fri, 10 Nov 2023 03:02:18 +0800 Subject: [PATCH] Support function with `struct` and `array` argument types (#2136) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * add abi_array function * Set Version: 1.0.327 * use build_cons to concatenate list of types for array elements and struct fields * Set Version: 1.0.328 * Revert type of various functions back to KInner * add tests for dynamic array and struct function arguments * use build_cons to concatenate list of types for array elements and struct fields * Set Version: 1.0.328 * Revert type of various functions back to KInner * add the two argument type tests into the smoke test suite * Set Version: 1.0.334 * add the two argument type tests into the smoke test suite * Remove testing infrastructure related to kontrolx (#2135) * .gitignore, tests/specs/examples: commit bin-runtime files * kevm-pyk/test_prove: simplify compilation process now that we dont need to generate K code * .gitmodules: remove forge-std * kevm-pyk/: remove more references to foundry tests * kevm-pyk/src/tests/integration/test-data: remove references to foundry tests * kevm-pyk/src/tests/integration/test_{foundry_prove,solc_to_k}: remove unused files * Set Version: 1.0.326 * tests/foundry/lib/forge-std: remove submodule * Set Version: 1.0.328 --------- Co-authored-by: devops * Remove `foundry.md` and the `foundry` target (#2142) * Remove `foundry.md` and the `foundry` target * Set Version: 1.0.329 --------- Co-authored-by: devops * Bump Solidity version in README links. (#2139) * bump soliditylang docs version in readme * Set Version: 1.0.328 * Set Version: 1.0.329 * Set Version: 1.0.330 --------- Co-authored-by: devops Co-authored-by: Palina Tolmach * Update dependency: deps/pyk_release (#2141) * deps/pyk_release: Set Version v0.1.480 * Set Version: 1.0.329 * kevm-pyk/: sync poetry files pyk version v0.1.480 * deps/k_release: sync release file version 6.0.164 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.481 * kevm-pyk/: sync poetry files pyk version v0.1.481 * deps/k_release: sync release file version 6.0.174 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.330 * kevm-pyk/: sync poetry files pyk version v0.1.481 * deps/pyk_release: Set Version v0.1.482 * kevm-pyk/: sync poetry files pyk version v0.1.482 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.483 * kevm-pyk/: sync poetry files pyk version v0.1.483 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.484 * kevm-pyk/: sync poetry files pyk version v0.1.484 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.485 * kevm-pyk/: sync poetry files pyk version v0.1.485 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.331 * deps/pyk_release: Set Version v0.1.486 * fix poetry2nix * kevm-pyk/: sync poetry files pyk version v0.1.486 * flake.{nix,lock}: update Nix derivations * minor tweak --------- Co-authored-by: devops Co-authored-by: Palina Tolmach Co-authored-by: Sam Balco * Rerun claims when the claim body or those of dependent claims changes (#2099) * Rerun claims based on digest, computed from claim body + dependent claims * Set Version: 1.0.309 * Make KClaimJob a frozen class and cache digest * Set Version: 1.0.310 * Change to using frozenset * Raise exception when label is not found * Set Version: 1.0.310 * Set Version: 1.0.312 * Set Version: 1.0.314 * Set Version: 1.0.329 * Update kevm-pyk/src/kevm_pyk/__main__.py Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> * Fix formatting * Set Version: 1.0.330 * Set Version: 1.0.331 * Set Version: 1.0.332 --------- Co-authored-by: devops Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: rv-jenkins * Remove option to skip simplifing init nodes (#2138) * kevm-pyk/{cli,__main__}: remove options --[no-]simplify-init * kevm-pyk/__main__: setup temporary directory for saving proofs if needed * Set Version: 1.0.328 * Set Version: 1.0.329 * Set Version: 1.0.331 * Set Version: 1.0.332 * Set Version: 1.0.333 * kevm-pyk/test_prove: remove kserver --------- Co-authored-by: devops Co-authored-by: rv-jenkins * Set Version: 1.0.334 * increase test suite time limit by 30 minutes * Set Version: 1.0.336 * increase ci timeout * add abi_array function * add tests for dynamic array and struct function arguments * use build_cons to concatenate list of types for array elements and struct fields * Revert type of various functions back to KInner * add the two argument type tests into the smoke test suite * increase ci timeout * Set Version: 1.0.341 * Set Version: 1.0.348 * Set Version: 1.0.349 --------- Co-authored-by: devops Co-authored-by: Everett Hildenbrandt Co-authored-by: Tamás Tóth Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: Palina Tolmach Co-authored-by: rv-jenkins Co-authored-by: Sam Balco Co-authored-by: Noah Watson <107630091+nwatson22@users.noreply.github.com> Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com> --- .github/workflows/test-pr.yml | 4 +- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/kevm.py | 18 ++- .../src/kevm_pyk/kproj/evm-semantics/abi.md | 5 +- package/version | 2 +- tests/specs/benchmarks/dynamicarray00-spec.k | 128 ++++++++++++++++++ tests/specs/benchmarks/dynamicarray00.sol | 6 + tests/specs/benchmarks/structarg00-spec.k | 127 +++++++++++++++++ tests/specs/benchmarks/structarg00.sol | 13 ++ tests/specs/smoke | 2 + 11 files changed, 297 insertions(+), 12 deletions(-) create mode 100644 tests/specs/benchmarks/dynamicarray00-spec.k create mode 100644 tests/specs/benchmarks/dynamicarray00.sol create mode 100644 tests/specs/benchmarks/structarg00-spec.k create mode 100644 tests/specs/benchmarks/structarg00.sol diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index c428031270..02d90735db 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -133,10 +133,10 @@ jobs: timeout: 45 - test-suite: 'test-prove-pyk' test-args: - timeout: 150 + timeout: 180 - test-suite: 'test-prove-pyk' test-args: '--use-booster' - timeout: 120 + timeout: 150 timeout-minutes: ${{ matrix.timeout }} steps: - name: 'Check out code' diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 97481f7b1d..533a8e82cb 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.348" +version = "1.0.349" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 59da13974a..fb44402466 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.348' +VERSION: Final = '1.0.349' diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index e6bd8d24b6..e186d42d19 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -4,7 +4,7 @@ from typing import TYPE_CHECKING from pyk.cterm import CTerm -from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc +from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc, build_cons from pyk.kast.manip import abstract_term_safely, bottom_up, flatten_label from pyk.kast.pretty import paren from pyk.kcfg.semantics import KCFGSemantics @@ -377,6 +377,14 @@ def abi_bool(b: KInner) -> KApply: def abi_type(type: str, value: KInner) -> KApply: return KApply('abi_type_' + type, [value]) + @staticmethod + def abi_tuple(values: list[KInner]) -> KApply: + return KApply('abi_type_tuple', [KEVM.typed_args(values)]) + + @staticmethod + def abi_array(elem_type: KInner, length: KInner, elems: list[KInner]) -> KApply: + return KApply('abi_type_array', [elem_type, length, KEVM.typed_args(elems)]) + @staticmethod def empty_typedargs() -> KApply: return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs') @@ -421,11 +429,9 @@ def intlist(ints: list[KInner]) -> KApply: return res @staticmethod - def typed_args(args: list[KInner]) -> KApply: - res = KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs') - for i in reversed(args): - res = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [i, res]) - return res + def typed_args(args: list[KInner]) -> KInner: + res = KEVM.empty_typedargs() + return build_cons(res, '_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', reversed(args)) @staticmethod def accounts(accts: list[KInner]) -> KInner: diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md index 5af4353af8..64377daffe 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md @@ -132,6 +132,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of | #bytes ( Bytes ) [klabel(abi_type_bytes), symbol] | #string ( String ) [klabel(abi_type_string), symbol] | #array ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array), symbol] + | #tuple ( TypedArgs ) [klabel(abi_type_tuple), symbol] // ---------------------------------------------------------------------------------------------- syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)] @@ -265,11 +266,13 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #typeName( #array(T, _, _)) => #typeName(T) +String "[]" + rule #typeName( #tuple(TARGS)) => "(" +String #generateSignatureArgs(TARGS) +String ")" + syntax Bytes ::= #encodeArgs ( TypedArgs ) [function] syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [function] // ------------------------------------------------------------------------------ rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes) - + rule #encodeArgs(#tuple(ARGS)) => #encodeArgs(ARGS) rule #encodeArgsAux(.TypedArgs, _:Int, HEADS, TAILS) => HEADS +Bytes TAILS rule #encodeArgsAux((ARG, ARGS), OFFSET, HEADS, TAILS) diff --git a/package/version b/package/version index cac8ee21ab..ad33520251 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.348 +1.0.349 diff --git a/tests/specs/benchmarks/dynamicarray00-spec.k b/tests/specs/benchmarks/dynamicarray00-spec.k new file mode 100644 index 0000000000..f7e4f99fc9 --- /dev/null +++ b/tests/specs/benchmarks/dynamicarray00-spec.k @@ -0,0 +1,128 @@ +requires "verification.k" + +module DYNAMICARRAY00-SPEC + imports VERIFICATION + + // fn-execute + claim + (#execute => #halt) ~> _ + 1 + NORMAL + ISTANBUL + + + _ => #encodeArgs(#uint256(3)) + _ => EVMC_SUCCESS + _ + _ + _ => ?_ + + #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") + #computeValidJumpDests(#parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029")) + CONTRACT_ID // this + MSG_SENDER // msg.sender + #abiCallData2("execute(uint256[])", #array(#uint256(1), 3, #uint256(A0), #uint256(A1), #uint256(A2), .TypedArgs)) // msg.data + 0 // msg.value + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(_VGAS) => ?_ + 0 => ?_ + _ => ?_ + false // NOTE: non-static call + CD + + + _ + _ + _ + _ => ?_ + _ => ?_ + + _ + _ // tx.origin + _BLOCK_HASHES // block.blockhash + + _ + _ + _ // block.coinbase + _ + _ + _ + _ + _ + BLOCK_NUM // block.number + _ + _ + NOW // now = block.timestamp + _ + _ + _ + _ + _ + _ + + + + _ + + + + CONTRACT_ID + CONTRACT_BAL + #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") + +_ + + +_ + + CONTRACT_NONCE + + + + CALLEE_ID + CALLEE_BAL + _ + + _ + + + _ + + CALLEE_NONCE + + + + // precompiled account for ECCREC + 1 + 0 + .Bytes + .Map + .Map + 0 + + + + ... + + _ + _ + _ + + + requires #rangeAddress(CONTRACT_ID) + andBool #rangeAddress(CALLEE_ID) + andBool #rangeUInt(256, NOW) + andBool #rangeUInt(128, BLOCK_NUM) // Solidity + andBool #rangeUInt(256, CONTRACT_BAL) + andBool #rangeUInt(256, CALLEE_BAL) + andBool #rangeNonce(CONTRACT_NONCE) + andBool #rangeNonce(CALLEE_NONCE) + andBool #range(0 <= CD < 1024) + andBool #rangeAddress(MSG_SENDER) + andBool #rangeUInt(256, A0) + andBool #rangeUInt(256, A1) + andBool #rangeUInt(256, A2) + +endmodule diff --git a/tests/specs/benchmarks/dynamicarray00.sol b/tests/specs/benchmarks/dynamicarray00.sol new file mode 100644 index 0000000000..fdbdfa74e7 --- /dev/null +++ b/tests/specs/benchmarks/dynamicarray00.sol @@ -0,0 +1,6 @@ +pragma solidity 0.4.24; +contract dynamicarray00 { + function execute(uint[] a) public returns (uint) { + return a.length; + } +} \ No newline at end of file diff --git a/tests/specs/benchmarks/structarg00-spec.k b/tests/specs/benchmarks/structarg00-spec.k new file mode 100644 index 0000000000..f5075cdad0 --- /dev/null +++ b/tests/specs/benchmarks/structarg00-spec.k @@ -0,0 +1,127 @@ +requires "verification.k" + +module STRUCTARG00-SPEC + imports VERIFICATION + + // fn-execute + claim + (#execute => #halt) ~> _ + 1 + NORMAL + ISTANBUL + + + _ => #encodeArgs(#uint256(A0)) + _ => EVMC_SUCCESS + _ + _ + _ => ?_ + + #parseByteStack("0x6080604052600436106100245760003560e01c63ffffffff168063dd77d08e14610029575b600080fd5b34801561003557600080fd5b506100496100443660046100c9565b61005f565b60405161005691906100fe565b60405180910390f35b5190565b60006040828403121561007557600080fd5b61007f6040610112565b9050600061008d84846100aa565b825250602061009e848483016100bd565b60208301525092915050565b60006100b68235610139565b9392505050565b60006100b6823561013c565b6000604082840312156100db57600080fd5b60006100e78484610063565b949350505050565b6100f881610139565b82525050565b6020810161010c82846100ef565b92915050565b60405181810167ffffffffffffffff8111828210171561013157600080fd5b604052919050565b90565b60ff16905600a265627a7a723058206cff7fc5f1eee5a02118c03209b136de08c05265f52541d16a578e6ff695a84b6c6578706572696d656e74616cf50037") + #computeValidJumpDests(#parseByteStack("0x6080604052600436106100245760003560e01c63ffffffff168063dd77d08e14610029575b600080fd5b34801561003557600080fd5b506100496100443660046100c9565b61005f565b60405161005691906100fe565b60405180910390f35b5190565b60006040828403121561007557600080fd5b61007f6040610112565b9050600061008d84846100aa565b825250602061009e848483016100bd565b60208301525092915050565b60006100b68235610139565b9392505050565b60006100b6823561013c565b6000604082840312156100db57600080fd5b60006100e78484610063565b949350505050565b6100f881610139565b82525050565b6020810161010c82846100ef565b92915050565b60405181810167ffffffffffffffff8111828210171561013157600080fd5b604052919050565b90565b60ff16905600a265627a7a723058206cff7fc5f1eee5a02118c03209b136de08c05265f52541d16a578e6ff695a84b6c6578706572696d656e74616cf50037")) + CONTRACT_ID // this + MSG_SENDER // msg.sender + #abiCallData2("execute((uint256,uint8))", #tuple(#uint256(A0), #uint8(A1), .TypedArgs)) // msg.data + 0 // msg.value + .WordStack => ?_ + .Bytes => ?_ + 0 => ?_ + #gas(_VGAS) => ?_ + 0 => ?_ + _ => ?_ + false // NOTE: non-static call + CD + + + _ + _ + _ + _ => ?_ + _ => ?_ + + _ + _ // tx.origin + _BLOCK_HASHES // block.blockhash + + _ + _ + _ // block.coinbase + _ + _ + _ + _ + _ + BLOCK_NUM // block.number + _ + _ + NOW // now = block.timestamp + _ + _ + _ + _ + _ + _ + + + + _ + + + + CONTRACT_ID + CONTRACT_BAL + #parseByteStack("0x60806040526004361060225760003560e01c63ffffffff1680638ef16cd9146027575b600080fd5b348015603257600080fd5b5060408051602060048035808201358381028086018501909652808552607995369593946024949385019291829185019084908082843750949750608b9650505050505050565b60408051918252519081900360200190f35b51905600a165627a7a72305820033b07c141d79055a0848aadceb745344b5e3a1fb5eff1292fc547e38d5bbe2a0029") + +_ + + +_ + + CONTRACT_NONCE + + + + CALLEE_ID + CALLEE_BAL + _ + + _ + + + _ + + CALLEE_NONCE + + + + // precompiled account for ECCREC + 1 + 0 + .Bytes + .Map + .Map + 0 + + + + ... + + _ + _ + _ + + + requires #rangeAddress(CONTRACT_ID) + andBool #rangeAddress(CALLEE_ID) + andBool #rangeUInt(256, NOW) + andBool #rangeUInt(128, BLOCK_NUM) // Solidity + andBool #rangeUInt(256, CONTRACT_BAL) + andBool #rangeUInt(256, CALLEE_BAL) + andBool #rangeNonce(CONTRACT_NONCE) + andBool #rangeNonce(CALLEE_NONCE) + andBool #range(0 <= CD < 1024) + andBool #rangeAddress(MSG_SENDER) + andBool #rangeUInt(256, A0) + andBool #rangeUInt(8, A1) + +endmodule diff --git a/tests/specs/benchmarks/structarg00.sol b/tests/specs/benchmarks/structarg00.sol new file mode 100644 index 0000000000..f2a1045fcc --- /dev/null +++ b/tests/specs/benchmarks/structarg00.sol @@ -0,0 +1,13 @@ +pragma solidity 0.4.24; +pragma experimental ABIEncoderV2; + +contract structarg00 { + struct Var { + uint a; + uint8 b; + } + + function execute(Var p) public returns (uint) { + return p.a; + } +} diff --git a/tests/specs/smoke b/tests/specs/smoke index 73567f4213..db51d1f864 100644 --- a/tests/specs/smoke +++ b/tests/specs/smoke @@ -1,5 +1,6 @@ tests/specs/benchmarks/address00-spec.k tests/specs/benchmarks/bytes00-spec.k +tests/specs/benchmarks/dynamicarray00-spec.k tests/specs/benchmarks/encode-keccak00-spec.k tests/specs/benchmarks/encodepacked-keccak01-spec.k tests/specs/benchmarks/keccak00-spec.k @@ -10,6 +11,7 @@ tests/specs/benchmarks/staticarray00-spec.k tests/specs/benchmarks/staticloop00-a0lt10-spec.k tests/specs/benchmarks/storagevar02-nooverflow-spec.k tests/specs/benchmarks/storagevar02-overflow-spec.k +tests/specs/benchmarks/structarg00-spec.k tests/specs/bihu/forwardToHotWallet-failure-1-spec.k tests/specs/bihu/forwardToHotWallet-failure-2-spec.k tests/specs/bihu/forwardToHotWallet-failure-3-spec.k