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
runtimeverification · Aug 13, 2024 · ffe99d4 · ffe99d4
1 parent 183c7f5
commit ffe99d4
Show file tree

Hide file tree

Showing 11 changed files with 57 additions and 36 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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(