From ffe99d4621649d15f5c00b02c2279109f358e922 Mon Sep 17 00:00:00 2001 From: Palina Tolmach Date: Tue, 13 Aug 2024 14:41:49 +0400 Subject: [PATCH] Add `--no-metadata` to `kontrol build`, bump Foundry version in CI (#763) * Add `--no-metadata`, update expected output * Bump Foundry version in Dockerfile, fix merge conflict * Remove `bytecode_hash`, `cbor_metadata` from `foundry.toml` * Update `foundry.k`, `contracts.k` output * Revert `contracts.k` and `foundry.k` expected output changes * Update `contracts.k` and `foundry.k` * Update `foundry.k` expected output based on CI result * Update `contracts.k` based on the CI result --- .github/workflows/Dockerfile | 2 +- src/kontrol/cli.py | 7 ++++ src/kontrol/foundry.py | 7 +++- src/kontrol/kompile.py | 2 +- src/kontrol/options.py | 2 + src/tests/integration/conftest.py | 1 + .../test-data/foundry/foundry.toml | 3 -- .../test-data/show/contracts.k.expected | 38 +++++++++---------- .../test-data/show/foundry.k.expected | 16 ++++---- src/tests/integration/test_kontrol.py | 8 +++- src/tests/profiling/test_foundry_prove.py | 7 +++- 11 files changed, 57 insertions(+), 36 deletions(-) diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 295be2ad5..aa2d3db0e 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -3,7 +3,7 @@ ARG K_VERSION ARG BASE_DISTRO ARG LLVM_VERSION -FROM ghcr.io/foundry-rs/foundry:nightly-7545c7a2857a873fa1909ec4174032c4e4702116 as FOUNDRY +FROM ghcr.io/foundry-rs/foundry:nightly-a0a002020be4c40946fe122fe6ff752b21cb2885 as FOUNDRY ARG Z3_VERSION FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3 diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 96739d60f..1b9f00736 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -336,6 +336,13 @@ def parse(s: str) -> list[T]: action='store_true', help='Do not silence K compiler warnings.', ) + build.add_argument( + '--no-metadata', + dest='no_metadata', + default=None, + action='store_true', + help='Do not append cbor or bytecode_hash metadata to bytecode.', + ) state_diff_args = command_parser.add_parser( 'load-state', diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 1065e8cc2..1e2dc6157 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -372,9 +372,12 @@ def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]: return list(element.rules) return ['NO DATA'] - def build(self) -> None: + def build(self, no_metadata: bool) -> None: + forge_build_args = ['forge', 'build', '--build-info', '--root', str(self._root)] + ( + ['--no-metadata'] if no_metadata else [] + ) try: - run_process_2(['forge', 'build', '--build-info', '--root', str(self._root)], logger=_LOGGER) + run_process_2(forge_build_args, logger=_LOGGER) except FileNotFoundError as err: raise RuntimeError( "Error: 'forge' command not found. Please ensure that 'forge' is installed and added to your PATH." diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index ead67b85a..c8216712a 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -44,7 +44,7 @@ def foundry_kompile( requires_paths: dict[str, str] = {} if not options.no_forge_build: - foundry.build() + foundry.build(options.no_metadata) if not options.no_silence_warnings: options.ignore_warnings = _silenced_warnings() diff --git a/src/kontrol/options.py b/src/kontrol/options.py index c31492e3d..3f09f92a3 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -769,6 +769,7 @@ class BuildOptions(LoggingOptions, KOptions, KGenOptions, KompileOptions, Foundr rekompile: bool no_forge_build: bool no_silence_warnings: bool + no_metadata: bool @staticmethod def default() -> dict[str, Any]: @@ -777,6 +778,7 @@ def default() -> dict[str, Any]: 'rekompile': False, 'no_forge_build': False, 'no_silence_warnings': False, + 'no_metadata': False, } @staticmethod diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py index b814fb212..bc77ef089 100644 --- a/src/tests/integration/conftest.py +++ b/src/tests/integration/conftest.py @@ -91,6 +91,7 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo 'ImmutableVarsTest:SYMBOLIC-BYTES-LEMMAS', ], 'enum_constraints': True, + 'no_metadata': True, } ), foundry=Foundry(foundry_root, add_enum_constraints=True), diff --git a/src/tests/integration/test-data/foundry/foundry.toml b/src/tests/integration/test-data/foundry/foundry.toml index 4602aefd4..699c83bab 100644 --- a/src/tests/integration/test-data/foundry/foundry.toml +++ b/src/tests/integration/test-data/foundry/foundry.toml @@ -4,6 +4,3 @@ out = 'out' test = 'test' extra_output = ['storageLayout', 'abi', 'evm.methodIdentifiers', 'evm.deployedBytecode.object', 'devdoc'] rpc_endpoints = { optimism = "https://optimism.alchemyapi.io/v2/...", mainnet = "${RPC_MAINNET}" } - -bytecode_hash = "none" -cbor_metadata = false diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index 67ebb93f8..6c854ee29 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -1,24 +1,5 @@ requires "foundry.md" -module S2KsrcZModduplicatesZMod1ZModDuplicateName-CONTRACT - imports public FOUNDRY - - syntax Contract ::= S2KsrcZModduplicatesZMod1ZModDuplicateNameContract - - syntax S2KsrcZModduplicatesZMod1ZModDuplicateNameContract ::= "S2KsrcZModduplicatesZMod1ZModDuplicateName" [symbol("contract_src%duplicates%1%DuplicateName")] - - syntax Bytes ::= S2KsrcZModduplicatesZMod1ZModDuplicateNameContract "." S2KsrcZModduplicatesZMod1ZModDuplicateNameMethod [function, symbol("method_src%duplicates%1%DuplicateName")] - - syntax S2KsrcZModduplicatesZMod1ZModDuplicateNameMethod ::= "S2KduplicateNamedFunction" "(" ")" [symbol("method_src%duplicates%1%DuplicateName_S2KduplicateNamedFunction_")] - - rule ( S2KsrcZModduplicatesZMod1ZModDuplicateName . S2KduplicateNamedFunction ( ) => #abiCallData ( "duplicateNamedFunction" , .TypedArgs ) ) - - - rule ( selector ( "duplicateNamedFunction()" ) => 2708311245 ) - - -endmodule - module S2KsrcZModduplicatesZMod2ZModDuplicateName-CONTRACT imports public FOUNDRY @@ -3480,6 +3461,25 @@ module S2KtestZModCounterTest-CONTRACT rule ( selector ( "testSetNumber(uint256)" ) => 1895400894 ) +endmodule + +module S2KsrcZModduplicatesZMod1ZModDuplicateName-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KsrcZModduplicatesZMod1ZModDuplicateNameContract + + syntax S2KsrcZModduplicatesZMod1ZModDuplicateNameContract ::= "S2KsrcZModduplicatesZMod1ZModDuplicateName" [symbol("contract_src%duplicates%1%DuplicateName")] + + syntax Bytes ::= S2KsrcZModduplicatesZMod1ZModDuplicateNameContract "." S2KsrcZModduplicatesZMod1ZModDuplicateNameMethod [function, symbol("method_src%duplicates%1%DuplicateName")] + + syntax S2KsrcZModduplicatesZMod1ZModDuplicateNameMethod ::= "S2KduplicateNamedFunction" "(" ")" [symbol("method_src%duplicates%1%DuplicateName_S2KduplicateNamedFunction_")] + + rule ( S2KsrcZModduplicatesZMod1ZModDuplicateName . S2KduplicateNamedFunction ( ) => #abiCallData ( "duplicateNamedFunction" , .TypedArgs ) ) + + + rule ( selector ( "duplicateNamedFunction()" ) => 2708311245 ) + + endmodule module S2KtestZModDynamicTypesTest-CONTRACT diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected index 2e868ef5c..09b3bacbe 100644 --- a/src/tests/integration/test-data/show/foundry.k.expected +++ b/src/tests/integration/test-data/show/foundry.k.expected @@ -5,7 +5,6 @@ requires "requires/pausability-lemmas.k" requires "requires/symbolic-bytes-lemmas.k" module FOUNDRY-MAIN - imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION imports public S2KtestZModAccountParamsTest-VERIFICATION imports public S2KtestZModAddrTest-VERIFICATION @@ -47,6 +46,7 @@ module FOUNDRY-MAIN imports public S2KsrcZModRecordedCounter-VERIFICATION imports public S2KtestZModCounter-VERIFICATION imports public S2KtestZModCounterTest-VERIFICATION + imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION imports public S2KtestZModDynamicTypesTest-VERIFICATION imports public S2KsrcZModExpectEmit-VERIFICATION imports public S2KtestZModEmitContractTest-VERIFICATION @@ -161,13 +161,6 @@ module FOUNDRY-MAIN -endmodule - -module S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION - imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-CONTRACT - - - endmodule module S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION @@ -457,6 +450,13 @@ module S2KtestZModCounterTest-VERIFICATION +endmodule + +module S2KsrcZModduplicatesZMod1ZModDuplicateName-VERIFICATION + imports public S2KsrcZModduplicatesZMod1ZModDuplicateName-CONTRACT + + + endmodule module S2KtestZModDynamicTypesTest-VERIFICATION diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py index 9b2a49bf6..c0102b1c4 100644 --- a/src/tests/integration/test_kontrol.py +++ b/src/tests/integration/test_kontrol.py @@ -61,7 +61,13 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath copy_tree(str(TEST_DATA_DIR / 'src'), str(foundry_root / 'test')) foundry_kompile( - BuildOptions({'require': str(foundry_root / 'lemmas.k'), 'module-import': 'TestBase:KONTROL-LEMMAS'}), + BuildOptions( + { + 'require': str(foundry_root / 'lemmas.k'), + 'module-import': 'TestBase:KONTROL-LEMMAS', + 'no_metadata': True, + } + ), foundry=Foundry(foundry_root), ) diff --git a/src/tests/profiling/test_foundry_prove.py b/src/tests/profiling/test_foundry_prove.py index c9565243d..e9e4c1332 100644 --- a/src/tests/profiling/test_foundry_prove.py +++ b/src/tests/profiling/test_foundry_prove.py @@ -27,7 +27,12 @@ def test_foundy_prove( foundry = forge_build(TEST_DATA_DIR, foundry_root) with profile('kompile.prof', sort_keys=('cumtime', 'tottime'), limit=15): - foundry_kompile(BuildOptions({'includes': ()}), foundry=foundry) + foundry_kompile( + BuildOptions( + {'includes': (), 'no_metadata': True}, + ), + foundry=foundry, + ) with profile('prove.prof', sort_keys=('cumtime', 'tottime'), limit=100): foundry_prove(