autosetup: keep via-ir off contracts whose pinned compiler cannot take its settings

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
     # =========================================================================

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()

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