From 85e99092e310de614cb4039c7b27f1d8353ac400 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 22 Aug 2026 14:41:34 +0300 Subject: [PATCH] autosetup: keep via-ir off contracts whose pinned compiler cannot take its settings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A scene can mix compilers through compiler_map, and the via-ir escalation did not look at them. Once a contract is on via-ir with the optimizer enabled, certoraRun also sends settings.optimizer.details, whose "inliner" key solc only learned in 0.8.5. Handing that to an older pinned compiler makes it reject the input outright, so one old contract fails the compile for the entire scene, and no rung recognises the resulting `Unknown key "inliner"` — the loop reaches its catch-all and the run ends with no progress. The escalation now checks each contract's pin before switching it, both when naming a single contract and when going scene-wide, and says which contracts it kept on legacy codegen. Contracts with no pin run on the environment's solc and are unaffected. The floor lives next to VIA_IR_MIN_VERSION, which covers a different thing: 0.7.5 is where solc learned settings.viaIR at all, while 0.8.5 is where it learned the settings we send along with it. Worth noting the other half, which is not in this repo: certora-cli emits the details block with no version guard when via-ir is on, while its own non-via-ir branch does guard exactly this (0.8.5). Guarding there too would make the floor unnecessary here. --- .../utils/compilation_workarounds.py | 42 ++++++++++- .../utils/solc_version_resolver.py | 5 ++ tests/test_compilation_workarounds.py | 70 +++++++++++++++++++ 3 files changed, 115 insertions(+), 2 deletions(-) diff --git a/certora_autosetup/utils/compilation_workarounds.py b/certora_autosetup/utils/compilation_workarounds.py index 14653899..98118c99 100644 --- a/certora_autosetup/utils/compilation_workarounds.py +++ b/certora_autosetup/utils/compilation_workarounds.py @@ -34,11 +34,14 @@ from certora_autosetup.utils.paths import user_harness_path, user_harnesses_dir from certora_autosetup.utils.remappings import build_packages_from_remapping_sources from certora_autosetup.utils.solc_version_resolver import ( + VIA_IR_SETTINGS_MIN_VERSION, extract_pragma_spec, pragma_admits, read_pragma_from_source_file, resolve_pragma_to_version, ) +from certora_autosetup.utils.config_manager import certora_format_to_raw_version +from packaging.version import Version from certora_autosetup.utils.types import ContractHandle # Solc's legacy-codegen stack-too-deep, as opposed to the YulException the via-ir pipeline @@ -1963,12 +1966,23 @@ def _apply_via_ir_workaround(self, contract_needing_via_ir: str, config_dict: Di """ # solc_via_ir_map is seeded up front by _seed_compile_maps. self._via_ir_contracts.add(contract_needing_via_ir) - config_dict["solc_via_ir_map"][contract_needing_via_ir] = True + if self._takes_via_ir_settings(contract_needing_via_ir, config_dict): + config_dict["solc_via_ir_map"][contract_needing_via_ir] = True + else: + self.log( + f"Leaving {contract_needing_via_ir} on legacy codegen: its pinned compiler " + f"predates solc {VIA_IR_SETTINGS_MIN_VERSION}, which via-ir settings need", + "WARNING", + ) scene_wide = self.declared_via_ir or len(self._via_ir_contracts) >= VIA_IR_SCENE_THRESHOLD if scene_wide and not all(config_dict["solc_via_ir_map"].values()): + held_back = [] for name in config_dict["solc_via_ir_map"]: - config_dict["solc_via_ir_map"][name] = True + if self._takes_via_ir_settings(name, config_dict): + config_dict["solc_via_ir_map"][name] = True + else: + held_back.append(name) reason = ( "the build config declares via-ir" if self.declared_via_ir @@ -1979,11 +1993,35 @@ def _apply_via_ir_workaround(self, contract_needing_via_ir: str, config_dict: Di f"lose their internal-function summaries too", "WARNING", ) + if held_back: + self.log( + f"Kept {len(held_back)} contract(s) on legacy codegen, pinned below solc " + f"{VIA_IR_SETTINGS_MIN_VERSION}: {held_back}", + "WARNING", + ) else: self.log(f"Adding via-ir workaround for contract: {contract_needing_via_ir}") return config_dict + def _takes_via_ir_settings(self, contract_name: str, config_dict: Dict) -> bool: + """Whether *contract_name*'s compiler accepts the settings certoraRun sends with via-ir. + + A scene can mix compilers through compiler_map, and via-ir is not the whole cost: with the + optimizer on, certoraRun also emits settings.optimizer.details, whose "inliner" key exists + only from solc 0.8.5. Switching such a contract to via-ir makes solc reject the input + outright, which fails the compile for the whole scene rather than for that one contract. + Contracts with no pin run on the environment's own solc and are left alone. + """ + pinned = (config_dict.get("compiler_map") or {}).get(contract_name) + raw = certora_format_to_raw_version(pinned) if pinned else None + if raw is None: + return True + try: + return Version(raw) >= VIA_IR_SETTINGS_MIN_VERSION + except Exception: # noqa: BLE001 — an unparsable pin is not a reason to hold back + return True + # ========================================================================= # Helper methods # ========================================================================= diff --git a/certora_autosetup/utils/solc_version_resolver.py b/certora_autosetup/utils/solc_version_resolver.py index cf9abe27..7bfaa2f3 100644 --- a/certora_autosetup/utils/solc_version_resolver.py +++ b/certora_autosetup/utils/solc_version_resolver.py @@ -29,6 +29,11 @@ # Minimum solc version that supports viaIR (introduced as settings.viaIR in 0.7.5, stabilized in 0.8.13) VIA_IR_MIN_VERSION = Version("0.7.5") +# Minimum solc version that accepts the settings certoraRun emits alongside viaIR. With the +# optimizer on, a viaIR contract is compiled with settings.optimizer.details, whose "inliner" key +# solc only learned in 0.8.5; an older binary rejects the whole input with `Unknown key "inliner"`. +VIA_IR_SETTINGS_MIN_VERSION = Version("0.8.5") + # Module-level cache for solc versions _solc_versions_cache: Optional[List[str]] = None _cache_lock = threading.Lock() diff --git a/tests/test_compilation_workarounds.py b/tests/test_compilation_workarounds.py index 7ab643e2..ed08c32b 100644 --- a/tests/test_compilation_workarounds.py +++ b/tests/test_compilation_workarounds.py @@ -1681,6 +1681,76 @@ def test_via_ir_goes_scene_wide_past_the_threshold(manager, monkeypatch, tmp_pat assert "solc_via_ir_map" not in updated +def test_scene_wide_via_ir_holds_back_contracts_pinned_below_the_settings_floor( + manager_declaring_via_ir, monkeypatch, tmp_path +) -> None: + # A mixed-compiler scene: with the optimizer on, a via-ir contract is compiled with + # settings.optimizer.details, and its "inliner" key only exists from solc 0.8.5. Switching a + # contract pinned below that makes solc reject the input for the whole scene, so the sweep + # must leave it on legacy codegen. + contracts = [ + ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol"), + ContractHandle(contract_name="Bar", source_file="contracts/Bar.sol"), + ContractHandle(contract_name="Old", source_file="contracts/Old.sol"), + ] + success, updated, config, _ = _run_loop( + manager_declaring_via_ir, + monkeypatch, + tmp_path, + [PERSISTENT_STACK_TOO_DEEP_OUTPUT, PERSISTENT_STACK_TOO_DEEP_OUTPUT], + contracts, + extra_config={"compiler_map": {"Foo": "solc8.24", "Bar": "solc8.24", "Old": "solc8.4"}}, + ) + assert success is True + # Not uniform, so the map survives rather than collapsing to the scalar. + assert updated["solc_via_ir_map"]["Foo"] is True + assert updated["solc_via_ir_map"]["Bar"] is True + assert updated["solc_via_ir_map"]["Old"] is False + assert "solc_via_ir" not in updated + + +def test_via_ir_skipped_for_the_needing_contract_when_its_pin_is_too_old( + manager, monkeypatch, tmp_path +) -> None: + # The contract that reported stack-too-deep is itself pinned below the floor. Turning via-ir on + # for it would trade one compile error for another that no rung recognises, so it stays on + # legacy codegen while the rest of the scene is untouched. + contracts = [ + ContractHandle(contract_name="Old", source_file="contracts/Old.sol"), + ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol"), + ] + outputs = [ + "Compiling contracts/Old.sol...\nsolc8.4 had an error:\nCompilerError: Stack too deep.\n" + ] * 4 + _, updated, _, _ = _run_loop( + manager, + monkeypatch, + tmp_path, + outputs, + contracts, + extra_config={"compiler_map": {"Old": "solc8.4", "Foo": "solc8.24"}}, + ) + assert updated.get("solc_via_ir") is not True + assert updated.get("solc_via_ir_map", {}).get("Old") is not True + + +def test_unpinned_contracts_still_go_via_ir(manager_declaring_via_ir, monkeypatch, tmp_path) -> None: + # No compiler_map: every contract runs on the environment's solc, and nothing is held back. + contracts = [ + ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol"), + ContractHandle(contract_name="Bar", source_file="contracts/Bar.sol"), + ] + success, updated, _, _ = _run_loop( + manager_declaring_via_ir, + monkeypatch, + tmp_path, + [PERSISTENT_STACK_TOO_DEEP_OUTPUT, PERSISTENT_STACK_TOO_DEEP_OUTPUT], + contracts, + ) + assert success is True + assert updated["solc_via_ir"] is True + + def test_declared_via_ir_skips_the_per_contract_walk(manager_declaring_via_ir, monkeypatch, tmp_path) -> None: # The project's build config already says where this ends; walking there one contract # per compile only costs compiles. The declared value is still not inherited — the