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