diff --git a/certora_autosetup/autosetup/autosetup.py b/certora_autosetup/autosetup/autosetup.py index a174db4..8eadc7e 100644 --- a/certora_autosetup/autosetup/autosetup.py +++ b/certora_autosetup/autosetup/autosetup.py @@ -57,6 +57,36 @@ COMPONENT = "Autosetup" +def _reconcile_evm_version_keys( + config: Dict[str, Any], + updates: Dict[str, Any], + contract_names: List[str], +) -> None: + """Reconcile solc_evm_version / solc_evm_version_map in a merged conf, in place. + + The compilation updates started as a superset of the base build-system conf, + so when they carry neither the scalar nor the map, the invalid_evm_version + workaround removed the declared version — drop the base-re-emitted scalar + rather than resurrect a rejected setting. When the map is present it + supersedes the scalar (the prover forbids both), but must cover every + contract: extend it with the declared scalar for contracts it misses (e.g. a + cancun override plus the project-declared version for the rest). + """ + if ( + updates + and "solc_evm_version" not in updates + and "solc_evm_version_map" not in updates + ): + config.pop("solc_evm_version", None) + if "solc_evm_version_map" in config: + declared = config.pop("solc_evm_version", None) + if declared: + config["solc_evm_version_map"] = { + **{name: declared for name in contract_names}, + **config["solc_evm_version_map"], + } + + class Autosetup: """Execute the autosetup phase and return an AutosetupResult. @@ -434,6 +464,12 @@ def get_build_system_config_dict_with_updates(self) -> Dict[str, Any]: if "solc_optimize_map" in config: config.pop("solc_optimize", None) + _reconcile_evm_version_keys( + config, + self.compilation_config_updates, + [ch.contract_name for ch in self.contract_handles], + ) + # Filter per-contract maps to only include contracts in self.contract_handles contract_names = {ch.contract_name for ch in self.contract_handles} for map_key in ("compiler_map", "solc_via_ir_map", "solc_evm_version_map", "solc_optimize_map"): diff --git a/certora_autosetup/build_systems/base.py b/certora_autosetup/build_systems/base.py index ae62526..f166fc1 100644 --- a/certora_autosetup/build_systems/base.py +++ b/certora_autosetup/build_systems/base.py @@ -29,6 +29,9 @@ class BuildSystemConfig(ABC): optimizer: Optional[bool] = None optimizer_runs: int = 200 via_ir: Optional[bool] = None + # Declared EVM target (foundry `evm_version`, hardhat `settings.evmVersion`); + # None means each solc's own default. + evm_version: Optional[str] = None # Common source configuration src: Optional[str] = None @@ -55,6 +58,7 @@ def to_certora_dict( "solc": "solc8.24", # or "0.8.24" if convert_solc=False "solc_optimize": 200, "solc_via_ir": true, + "solc_evm_version": "paris", # only when the project declares one "packages": [...] } """ @@ -137,6 +141,16 @@ def _apply_common_solc_settings( if self.via_ir: result["solc_via_ir"] = True + # Honor the project's declared EVM target. Unlike the optimizer setting + # above, this is not a tuning knob: solc's default EVM version can be + # NEWER than the declared one (e.g. shanghai/PUSH0 vs a pinned "paris"), + # producing bytecode for the wrong chain and different codegen (which can + # even fail where the declared target compiles), and no reactive + # workaround could guess the intended version. If the declared version is + # rejected by the solc in use, the invalid_evm_version workaround drops it. + if self.evm_version: + result["solc_evm_version"] = self.evm_version + return result def _relativize_packages( diff --git a/certora_autosetup/build_systems/foundry.py b/certora_autosetup/build_systems/foundry.py index 7e55b79..441e891 100644 --- a/certora_autosetup/build_systems/foundry.py +++ b/certora_autosetup/build_systems/foundry.py @@ -63,7 +63,7 @@ def __post_init__(self): if self.restriction_manager is None: # No restrictions → apply_restrictions short-circuits, so the # defaults here are never consulted; we still pass optimizer_runs - # for consistency. (evm_version isn't a FoundryConfig field.) + # for consistency. self.restriction_manager = FoundryRestrictionManager( restrictions=[], # No restriction means no effect of apply_restrictions default_via_ir=bool(self.via_ir) if self.via_ir is not None else False, @@ -221,6 +221,7 @@ def _extract_profile_config(self, foundry_data: Dict[str, Any], profile: str) -> optimizer=optimizer_settings["enabled"], optimizer_runs=optimizer_settings["runs"], via_ir=via_ir, + evm_version=profile_data.get("evm_version"), # Will be None if not specified src=profile_data.get("src"), # Will be None if not specified out=profile_data.get("out"), # Will be None if not specified libs=profile_data.get("libs"), # Will be None if not specified @@ -278,6 +279,7 @@ def _merge_configs(self, base: FoundryConfig, override: FoundryConfig) -> Foundr optimizer=override.optimizer if override.optimizer is not None else base.optimizer, optimizer_runs=merged_optimizer_runs, via_ir=merged_via_ir, + evm_version=override.evm_version or base.evm_version, src=override.src or base.src, out=override.out or base.out, libs=override.libs or base.libs, @@ -463,13 +465,13 @@ def apply_restrictions( "FoundryRestrictionManager", ) - # NOTE: per-path evm_version is intentionally NOT emitted. The prover - # requires solc_evm_version_map to be total, so unmatched contracts - # would have to be filled with the profile-level evm_version (e.g. - # "prague") — which breaks older-solc files that don't support it - # (solc 0.8.25 rejects "prague"). Leaving evm_version unset lets each - # contract use its solc's own default, which is always compatible — the - # behaviour that worked before per-path evm_version was introduced. + # NOTE: per-path evm_version from compilation_restrictions is + # intentionally NOT emitted. The prover requires solc_evm_version_map to + # be total, so unmatched contracts would have to be filled with a + # concrete version even where the project relies on each solc's own + # default. The PROFILE-level evm_version is honored separately (emitted + # as scalar solc_evm_version by _apply_common_solc_settings and dropped + # by the invalid_evm_version workaround if a solc rejects it). # ---------------- solc_optimize map ---------------- restricted_optimize = self._optimize_map(contracts) diff --git a/certora_autosetup/build_systems/hardhat.py b/certora_autosetup/build_systems/hardhat.py index 6ffad45..5a7d76d 100644 --- a/certora_autosetup/build_systems/hardhat.py +++ b/certora_autosetup/build_systems/hardhat.py @@ -278,6 +278,7 @@ def _extract_config_from_json(self, config_data: Dict[str, Any], config_type: st optimizer = False optimizer_runs = 200 via_ir = False + evm_version = None elif isinstance(solidity, dict): # Hardhat config structure: {"compilers": [{"version": "0.8.28", "settings": {...}}], ...} # Or simple format: {"version": "0.8.28", "settings": {...}} @@ -309,11 +310,13 @@ def _extract_config_from_json(self, config_data: Dict[str, Any], config_type: st optimizer = optimizer_settings.get("enabled", False) optimizer_runs = optimizer_settings.get("runs", 200) via_ir = settings.get("viaIR", False) + evm_version = settings.get("evmVersion") else: solc_version = None optimizer = False optimizer_runs = 200 via_ir = False + evm_version = None # Extract and process paths paths = config_data.get("paths", {}) @@ -340,6 +343,7 @@ def _extract_config_from_json(self, config_data: Dict[str, Any], config_type: st optimizer=optimizer, optimizer_runs=optimizer_runs, via_ir=via_ir, + evm_version=evm_version, src=src, artifacts=artifacts, cache=cache, diff --git a/certora_autosetup/build_systems/hardhat_config_extractor.js b/certora_autosetup/build_systems/hardhat_config_extractor.js index 4d2247d..d3f075b 100644 --- a/certora_autosetup/build_systems/hardhat_config_extractor.js +++ b/certora_autosetup/build_systems/hardhat_config_extractor.js @@ -27,11 +27,16 @@ try { if (hasTypeScriptConfig) { try { // Register ts-node with transpileOnly to skip type checking - // This allows loading TypeScript configs even if the project has type errors + // This allows loading TypeScript configs even if the project has type errors. + // moduleResolution must be overridden together with module: forcing + // commonjs while the project's tsconfig pins moduleResolution + // "nodenext"/"node16" is rejected by TypeScript (TS5110) even in + // transpileOnly mode, losing the whole config. require('ts-node').register({ transpileOnly: true, compilerOptions: { - module: 'commonjs' + module: 'commonjs', + moduleResolution: 'node' } }); } catch (tsError) { diff --git a/certora_autosetup/fixconf.py b/certora_autosetup/fixconf.py index e0b37a1..fe02137 100644 --- a/certora_autosetup/fixconf.py +++ b/certora_autosetup/fixconf.py @@ -33,7 +33,7 @@ # Build system keys that should be stripped from the output if the user's original conf didn't have them. # These are low-priority settings that can break the prover (e.g. solc_optimize with a huge value from foundry.toml). # High-priority keys like solc and packages are kept since they're often needed for compilation. -_LOW_PRIORITY_BS_KEYS = {"solc_optimize", "solc_via_ir"} +_LOW_PRIORITY_BS_KEYS = {"solc_optimize", "solc_via_ir", "solc_evm_version"} class _AcceptAllScope: diff --git a/certora_autosetup/utils/compilation_workarounds.py b/certora_autosetup/utils/compilation_workarounds.py index 3cd2ec2..066d246 100644 --- a/certora_autosetup/utils/compilation_workarounds.py +++ b/certora_autosetup/utils/compilation_workarounds.py @@ -126,6 +126,11 @@ def __init__( # firing for the same consumer (different missing library) regenerates the # consumer's harness covering every library it has needed so far. self._harnesses_by_consumer: Dict[str, List[Tuple[str, str]]] = {} + # True when _seed_compile_maps promoted a declared scalar solc_evm_version + # into a total solc_evm_version_map. Only such a map may be collapsed back + # to the scalar on finalize — an unseeded partial map (e.g. a single cancun + # entry) must never be promoted to a global scalar. + self._evm_version_seeded = False # Convert default version to the detected convention if solc_convention == SolcConvention.SOLC_SELECT and solc_default_version.startswith("solc") \ and not solc_default_version.startswith("solc-"): @@ -149,7 +154,8 @@ def format_solc_version(self, version: str) -> str: # Conf keys that move together when promoting/collapsing a scalar <-> map. def _seed_compile_maps(self, config: Dict, contracts: List[ContractHandle]) -> None: - """Promote scalar ``solc``/``solc_via_ir`` into fully-populated maps. + """Promote scalar ``solc``/``solc_via_ir`` (and ``solc_evm_version``, + when declared) into fully-populated maps. """ if "compiler_map" not in config: default = config.pop("solc", None) or self.solc_default_version @@ -157,6 +163,14 @@ def _seed_compile_maps(self, config: Dict, contracts: List[ContractHandle]) -> N if "solc_via_ir_map" not in config: via_ir = config.pop("solc_via_ir", False) config["solc_via_ir_map"] = {c.contract_name: via_ir for c in contracts} + # solc_evm_version is seeded only when declared: absence means "each + # solc's own default", which a map entry cannot express (the prover + # requires every *_map to cover all files). + if "solc_evm_version_map" not in config: + evm_version = config.pop("solc_evm_version", None) + if evm_version: + config["solc_evm_version_map"] = {c.contract_name: evm_version for c in contracts} + self._evm_version_seeded = True def _normalize_compile_maps(self, config: Dict) -> None: """Collapse a uniform compiler_map / solc_via_ir_map back to its scalar if all values are same. @@ -173,11 +187,17 @@ def _normalize_compile_maps(self, config: Dict) -> None: if value: # False is the prover default — no scalar needed. config["solc_via_ir"] = value + emap = config.get("solc_evm_version_map") + if self._evm_version_seeded and isinstance(emap, dict) and emap and len(set(emap.values())) == 1: + config["solc_evm_version"] = next(iter(emap.values())) + del config["solc_evm_version_map"] + def _mirror_compile_flags(self, src: Dict, dst: Dict) -> None: """Copy the compile-flag keys from ``src`` onto ``dst`` (dropping any the src no longer has), so the disk conf and the returned dict stay in sync after seeding/normalizing.""" - compile_flag_keys = ("solc", "compiler_map", "solc_via_ir", "solc_via_ir_map") + compile_flag_keys = ("solc", "compiler_map", "solc_via_ir", "solc_via_ir_map", + "solc_evm_version", "solc_evm_version_map") for key in compile_flag_keys: dst.pop(key, None) if key in src: @@ -242,12 +262,15 @@ def run_compilation_with_workarounds( 5. Stack-too-deep errors (via-ir workaround) 6. Feature only available on the via-ir pipeline (enable via-ir out of necessity) 7. Unsupported solc version for via-ir (disable via-ir for old compiler versions) - 8. Cancun opcode errors (mcopy/tload/tstore — set EVM version to cancun) - 9. Unnamed return variable warning (ignore_solidity_warnings) - 10. YulException stack-too-deep with via-ir (try adding optimizer first) - 11. YulException stack-too-deep persists (stop asserting autofinder success) - 12. Missing dependency library (generate harness with dummy usage so solc emits the lib) - 13. Catch-all: use_relpaths_for_solc_json (last resort before import-patch fallback) + 8. Declared EVM version rejected by solc (drop solc_evm_version) + 9. Cancun opcode errors (mcopy/tload/tstore — set EVM version to cancun) + 10. Unnamed return variable warning (ignore_solidity_warnings) + 11. YulException stack-too-deep with via-ir (try adding optimizer first) + 12. YulException persists with optimizer (fall back to solc's default Yul + steps via strict_solc_optimizer) + 13. YulException still persists (stop asserting autofinder success) + 14. Missing dependency library (generate harness with dummy usage so solc emits the lib) + 15. Catch-all: use_relpaths_for_solc_json (last resort before import-patch fallback) Args: cmd: Command to execute @@ -341,6 +364,14 @@ def run_compilation_with_workarounds( apply_fn=self._apply_disable_via_ir_workaround_to_config, enabled=global_via_ir_enabled, ), + # Ordered before cancun_opcode_evm_version: its apply drops every EVM + # version key, so a cancun entry added later in the same pass survives. + CompilationWorkaround( + name="invalid_evm_version", + detect_fn=lambda output: self._detect_invalid_evm_version(output, compilation_config), + apply_fn=self._apply_invalid_evm_version_workaround_to_config, + enabled=True, + ), CompilationWorkaround( name="cancun_opcode_evm_version", detect_fn=lambda output: self._detect_cancun_opcode_errors(output, contracts), @@ -369,20 +400,41 @@ def run_compilation_with_workarounds( apply_fn=self._apply_optimizer_for_via_ir, enabled=True, ), + # Escalation after yul_exception_add_optimizer: with optimizer + + # via-ir, certoraRun substitutes finder-friendly Yul steps that give + # less stack relief than solc's own pipeline — try the default + # pipeline before touching the autofinder assertion. Only fires on + # output produced AFTER the optimizer was tried (not in the pass + # that just added it). + CompilationWorkaround( + name="yul_exception_strict_optimizer", + detect_fn=lambda output: ( + "detected" + if self._detect_yul_exception_stack_too_deep(output) + and "solc_optimize" in compilation_config + and not compilation_config.get("strict_solc_optimizer", False) + and "yul_exception_add_optimizer" not in applied_this_pass + else None + ), + apply_fn=self._apply_strict_optimizer_for_via_ir, + enabled=True, + ), CompilationWorkaround( name="yul_exception_stack_too_deep", - # This is the escalation step after yul_exception_add_optimizer: - # it must only fire on output produced AFTER the optimizer was - # tried, not in the same pass that just added it (the live - # "solc_optimize in config" check would otherwise see the value - # the previous workaround set seconds ago and stop asserting - # autofinder success without ever testing the optimizer). + # Final escalation step: it must only fire on output produced + # AFTER the optimizer and the strict-steps fallback were both + # tried, not in the same pass that just applied either (the live + # config checks would otherwise see values a previous workaround + # set seconds ago and stop asserting autofinder success without + # ever testing them). detect_fn=lambda output: ( "detected" if self._detect_yul_exception_stack_too_deep(output) and compilation_config.get("assert_autofinder_success", False) and "solc_optimize" in compilation_config + and compilation_config.get("strict_solc_optimizer", False) and "yul_exception_add_optimizer" not in applied_this_pass + and "yul_exception_strict_optimizer" not in applied_this_pass else None ), apply_fn=self._apply_yul_exception_workaround, @@ -636,6 +688,25 @@ def _detect_cancun_opcode_errors(self, output: str, contracts: List[ContractHand break return None + def _detect_invalid_evm_version(self, output: str, compilation_config: Dict) -> Optional[str]: + """Detect solc rejecting the conf's EVM version. + + solc emits the uniform text "Invalid EVM version requested." both for an + unknown version name and for a name newer than that solc supports, so no + solc-version/EVM-name table is needed — the compiler's own rejection is + the authoritative signal. Gated on the LIVE conf still carrying an EVM + version key: after the apply removed it the gate is false, so the + workaround cannot re-fire on a stale output. + """ + if ( + "solc_evm_version" not in compilation_config + and "solc_evm_version_map" not in compilation_config + ): + return None + if "Invalid EVM version requested" not in _normalize_ws(output): + return None + return "detected" + def _detect_via_ir_required( self, output: str, contracts: List[ContractHandle] ) -> Optional[str]: @@ -932,6 +1003,11 @@ def _apply_evm_version_cancun_workaround_to_config( ) -> Dict: """Apply EVM version cancun workaround to config for a contract with Cancun opcode errors.""" self.log(f"Applying EVM version cancun workaround for contract: {contract_name}") + # The prover rejects a conf carrying both the scalar and the map. A + # declared scalar was already promoted into the map by _seed_compile_maps, + # so dropping it here loses nothing. + updated_config_dict.pop("solc_evm_version", None) + compilation_config.pop("solc_evm_version", None) if "solc_evm_version_map" not in updated_config_dict: updated_config_dict["solc_evm_version_map"] = {} updated_config_dict["solc_evm_version_map"][contract_name] = "cancun" @@ -943,6 +1019,36 @@ def _apply_evm_version_cancun_workaround_to_config( return updated_config_dict + def _apply_invalid_evm_version_workaround_to_config( + self, + _detect_result: str, + updated_config_dict: Dict, + compilation_config: Dict, + config_file: Path, + _contracts: List[ContractHandle], + ) -> Dict: + """Drop the conf's EVM version after solc rejected it. + + Removal is global per conf: the prover requires solc_evm_version_map to + cover every file and a map entry cannot say "use this solc's default", + so a per-contract drop is not expressible. Affected contracts fall back + to their compiler's default EVM version. + """ + self.log( + "Declared EVM version is not supported by the solc in use — dropping " + "solc_evm_version; contracts fall back to their compiler's default", + "WARNING", + ) + for config in (compilation_config, updated_config_dict): + config.pop("solc_evm_version", None) + config.pop("solc_evm_version_map", None) + self._evm_version_seeded = False + + with open(config_file, "w") as f: + json.dump(compilation_config, f, indent=2) + + return updated_config_dict + def _apply_disable_via_ir_workaround_to_config( self, contract_name: str, @@ -980,6 +1086,37 @@ def _apply_optimizer_for_via_ir( return updated_config_dict + def _apply_strict_optimizer_for_via_ir( + self, + _detect_result: str, + updated_config_dict: Dict, + compilation_config: Dict, + config_file: Path, + _contracts: List[ContractHandle], + ) -> Dict: + """Fall back to solc's own Yul optimizer pipeline for stack relief. + + With optimizer + via-ir, certoraRun substitutes its finder-friendly Yul + step sequence (full inliner removed so autofinders survive), which gives + less stack relief than solc's default pipeline and can leave — or cause — + stack-too-deep in functions the default pipeline compiles. + strict_solc_optimizer restores solc's own steps; autofinders that stop + surviving them are handled by the next escalation step. + """ + self.log( + "YulException persists with via-ir + optimizer — retrying with solc's " + "default Yul optimizer steps (strict_solc_optimizer)", + "WARNING", + ) + + compilation_config["strict_solc_optimizer"] = True + updated_config_dict["strict_solc_optimizer"] = True + + with open(config_file, "w") as f: + json.dump(compilation_config, f, indent=2) + + return updated_config_dict + def _apply_yul_exception_workaround( self, _detect_result: str, @@ -997,8 +1134,9 @@ def _apply_yul_exception_workaround( so removing them here would reintroduce the errors they fix. """ self.log( - "YulException persists with via-ir + optimizer — no longer asserting " - "autofinder success (failing files fall back un-instrumented)", + "YulException persists with via-ir + optimizer + solc's default Yul " + "steps — no longer asserting autofinder success (failing files fall " + "back un-instrumented)", "WARNING", ) diff --git a/certora_autosetup/utils/enhanced_config_manager.py b/certora_autosetup/utils/enhanced_config_manager.py index afe060b..4fea94b 100644 --- a/certora_autosetup/utils/enhanced_config_manager.py +++ b/certora_autosetup/utils/enhanced_config_manager.py @@ -1071,6 +1071,27 @@ def sync_compiler_maps_with_files( f" to {len(conf_object['solc_evm_version_map'])} entries" ) modified = True + # Extend: the prover requires the map to cover every file, and a map + # entry cannot say "use this solc's default" — fill contracts newly + # injected into files (mocks/harnesses) with the declared scalar from + # the reference conf, else the map's most common value. + evm_map = conf_object["solc_evm_version_map"] + if evm_map: + fill = ( + self.reference_compiler_maps.get("solc_evm_version") + or Counter(evm_map.values()).most_common(1)[0][0] + ) + added = 0 + for handle in contracts_in_files: + if not any(handle.matches_map_key(key) for key in evm_map): + evm_map[handle.contract_name] = fill + added += 1 + if added > 0: + self.log( + f"Filled {added} missing solc_evm_version_map entry/entries " + f"with '{fill}' so files and the map stay consistent" + ) + modified = True return modified diff --git a/tests/test_compilation_workarounds.py b/tests/test_compilation_workarounds.py index 814935f..739ba8f 100644 --- a/tests/test_compilation_workarounds.py +++ b/tests/test_compilation_workarounds.py @@ -295,25 +295,50 @@ def test_cached_autofinder_failure_is_exclusive(manager, monkeypatch, tmp_path) def test_yul_ladder_escalates_across_passes(manager, monkeypatch, tmp_path) -> None: - # The YulException escalation must span two recompiles: pass 1 only adds - # the optimizer (trying to succeed WITH autofinders); only when the - # exception SURVIVES that recompile does the last resort stop asserting - # autofinder success — keeping the compile settings. + # The YulException escalation must span three recompiles: pass 1 only adds + # the optimizer (trying to succeed WITH autofinders), pass 2 falls back to + # solc's default Yul steps (strict_solc_optimizer — the finder-friendly + # substitute steps give less stack relief); only when the exception SURVIVES + # both does the last resort stop asserting autofinder success — keeping the + # compile settings. contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] success, updated, config, fake_run = _run_loop( manager, monkeypatch, tmp_path, - [SINGLE_LINE_YUL_STACK_TOO_DEEP, SINGLE_LINE_YUL_STACK_TOO_DEEP], + [SINGLE_LINE_YUL_STACK_TOO_DEEP] * 3, contracts, extra_config={"assert_autofinder_success": True}, ) assert success is True - assert fake_run.calls == 3 + assert fake_run.calls == 4 assert config["solc_optimize"] == "200" + assert config["strict_solc_optimizer"] is True assert updated["assert_autofinder_success"] is False +def test_yul_strict_steps_tried_before_relaxing_autofinders( + manager, monkeypatch, tmp_path +) -> None: + # Real case (observed in the wild): the finder-friendly substitute Yul + # steps themselves cause the stack-too-deep, and solc's default pipeline + # compiles fine — the ladder must reach strict_solc_optimizer WITHOUT + # giving up on the autofinder assertion. + contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] + success, updated, config, fake_run = _run_loop( + manager, + monkeypatch, + tmp_path, + [SINGLE_LINE_YUL_STACK_TOO_DEEP] * 2, + contracts, + extra_config={"assert_autofinder_success": True}, + ) + assert success is True + assert fake_run.calls == 3 + assert config["strict_solc_optimizer"] is True + assert config["assert_autofinder_success"] is True + + # Verbatim-shaped solc output for a feature that exists only on the via-ir # pipeline (observed with `require(cond, CustomError())` on solc 0.8.26). The # phrase is hard-wrapped by solc, so detection must be whitespace-normalized. @@ -344,10 +369,11 @@ def test_via_ir_added_out_of_necessity(manager, monkeypatch, tmp_path) -> None: def test_yul_last_resort_keeps_compile_settings(manager, monkeypatch, tmp_path) -> None: - # One output carries a plain stack-too-deep for Foo AND a YulException with - # the optimizer already present (e.g. supplied by the project's foundry - # config): the pass applies via-ir for Foo and relaxes the autofinder - # assertion, but via-ir and the optimizer must survive — the source itself may not compile + # Pass 1 carries a plain stack-too-deep for Foo AND a YulException with the + # optimizer already present (e.g. supplied by the project's foundry config): + # the pass applies via-ir for Foo and the strict-steps fallback; when the + # exception survives, pass 2 relaxes the autofinder assertion, but via-ir + # and the optimizer must survive — the source itself may not compile # without them (seen in the wild: "Require with a custom error is only # available using the via-ir pipeline"). contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] @@ -356,13 +382,14 @@ def test_yul_last_resort_keeps_compile_settings(manager, monkeypatch, tmp_path) manager, monkeypatch, tmp_path, - [combined], + [combined, SINGLE_LINE_YUL_STACK_TOO_DEEP], contracts, extra_config={"assert_autofinder_success": True, "solc_optimize": "200"}, ) assert success is True - assert fake_run.calls == 2 + assert fake_run.calls == 3 assert updated["solc_via_ir"] is True + assert config["strict_solc_optimizer"] is True assert config["assert_autofinder_success"] is False assert config["solc_optimize"] == "200" @@ -381,14 +408,15 @@ def test_via_ir_after_yul_last_resort_stays_per_contract(manager, monkeypatch, t tmp_path, [ SINGLE_LINE_YUL_STACK_TOO_DEEP, # pass 1: add optimizer - SINGLE_LINE_YUL_STACK_TOO_DEEP, # pass 2: last resort (assertion relaxed) - PERSISTENT_STACK_TOO_DEEP_OUTPUT, # pass 3: via-ir for Foo only + SINGLE_LINE_YUL_STACK_TOO_DEEP, # pass 2: solc default Yul steps + SINGLE_LINE_YUL_STACK_TOO_DEEP, # pass 3: last resort (assertion relaxed) + PERSISTENT_STACK_TOO_DEEP_OUTPUT, # pass 4: via-ir for Foo only ], contracts, extra_config={"assert_autofinder_success": True}, ) assert success is True - assert fake_run.calls == 4 + assert fake_run.calls == 5 assert updated["solc_via_ir_map"] == {"Foo": True, "Bar": False} assert "solc_via_ir" not in updated assert config["assert_autofinder_success"] is False @@ -520,3 +548,134 @@ def test_compiler_mismatch_workaround_fires_with_global_solc( assert fake_run.calls == 2 # failing compile + one recompile after the fix assert compilation_config["compiler_map"]["DummyERC20Impl"] == "solc8.30" assert compilation_config["compiler_map"]["Vault"] == "solc7.3" + + +# ============================================================================= +# Declared EVM version: seeding, invalid-version drop, cancun reconciliation +# ============================================================================= +# +# A project-declared EVM version (foundry `evm_version` / hardhat `evmVersion`) +# reaches the conf as scalar `solc_evm_version`. solc rejects a version it does +# not know with the uniform "Invalid EVM version requested." text — the +# invalid_evm_version workaround drops the setting on that signal (global per +# conf: the prover requires solc_evm_version_map to cover every file and a map +# entry cannot express "use this solc's default"). + +INVALID_EVM_VERSION_OUTPUT = ( + "Compiling contracts/Foo.sol...\n" + "solc8.17 had an error:\n" + "Invalid EVM version requested.\n" +) + +# solc hard-wraps diagnostics; the detector must survive the phrase split +# across a newline like the other wrap-sensitive detectors. +WRAPPED_INVALID_EVM_VERSION_OUTPUT = ( + "Compiling contracts/Foo.sol...\n" + "solc8.17 had an error:\n" + "Invalid EVM\n" + "version requested.\n" +) + +CANCUN_MCOPY_OUTPUT = ( + "Compiling contracts/Foo.sol...\n" + "solc8.22 had an error:\n" + 'DeclarationError: Function "mcopy" not found\n' +) + + +def test_detects_invalid_evm_version_only_with_live_key( + manager: CompilationWorkaroundManager, +) -> None: + assert ( + manager._detect_invalid_evm_version( + INVALID_EVM_VERSION_OUTPUT, {"solc_evm_version": "paris"} + ) + == "detected" + ) + assert ( + manager._detect_invalid_evm_version( + WRAPPED_INVALID_EVM_VERSION_OUTPUT, {"solc_evm_version_map": {"Foo": "paris"}} + ) + == "detected" + ) + # No EVM version in the live conf -> nothing to drop, never fires. + assert manager._detect_invalid_evm_version(INVALID_EVM_VERSION_OUTPUT, {}) is None + assert ( + manager._detect_invalid_evm_version(UNRELATED_OUTPUT, {"solc_evm_version": "paris"}) + is None + ) + + +def test_invalid_evm_version_dropped_and_compiles(manager, monkeypatch, tmp_path) -> None: + contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] + success, updated, compilation_config, fake_run = _run_loop( + manager, + monkeypatch, + tmp_path, + [INVALID_EVM_VERSION_OUTPUT], + contracts, + extra_config={"solc_evm_version": "unknownfork"}, + ) + assert success is True + assert fake_run.calls == 2 # failing compile + one recompile after the drop + for config in (compilation_config, updated): + assert "solc_evm_version" not in config + assert "solc_evm_version_map" not in config + + +def test_declared_evm_version_round_trips_through_seeding( + manager, monkeypatch, tmp_path +) -> None: + # An unrelated failure/fix cycle must not lose the declared version: it is + # seeded into a total map for the workarounds and collapsed back to the + # scalar on finalize. + contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] + success, updated, compilation_config, _ = _run_loop( + manager, + monkeypatch, + tmp_path, + [UNNAMED_RETURN_WARNING_OUTPUT], + contracts, + extra_config={"solc_evm_version": "paris"}, + ) + assert success is True + assert compilation_config["solc_evm_version"] == "paris" + assert "solc_evm_version_map" not in compilation_config + assert updated["solc_evm_version"] == "paris" + + +def test_cancun_overrides_one_contract_keeps_declared_for_rest( + manager, monkeypatch, tmp_path +) -> None: + contracts = [ + ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol"), + ContractHandle(contract_name="Bar", source_file="contracts/Bar.sol"), + ] + success, updated, compilation_config, _ = _run_loop( + manager, + monkeypatch, + tmp_path, + [CANCUN_MCOPY_OUTPUT], + contracts, + extra_config={"solc_evm_version": "paris"}, + ) + assert success is True + assert compilation_config["solc_evm_version_map"] == {"Foo": "cancun", "Bar": "paris"} + assert "solc_evm_version" not in compilation_config + assert updated["solc_evm_version_map"] == {"Foo": "cancun", "Bar": "paris"} + + +def test_unseeded_cancun_map_not_promoted_to_scalar(manager, monkeypatch, tmp_path) -> None: + # Without a declared version the cancun entry is a partial, single-contract + # map; collapsing it to a global scalar would force cancun on every file. + contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] + success, updated, compilation_config, _ = _run_loop( + manager, + monkeypatch, + tmp_path, + [CANCUN_MCOPY_OUTPUT], + contracts, + ) + assert success is True + assert compilation_config["solc_evm_version_map"] == {"Foo": "cancun"} + assert "solc_evm_version" not in compilation_config diff --git a/tests/test_evm_version_reconciliation.py b/tests/test_evm_version_reconciliation.py new file mode 100644 index 0000000..e379d64 --- /dev/null +++ b/tests/test_evm_version_reconciliation.py @@ -0,0 +1,116 @@ +"""Tests for solc_evm_version scalar/map reconciliation outside the workaround loop: +the merged-conf helper in autosetup.py and the map fill in sync_compiler_maps_with_files. +""" + +from pathlib import Path + +from certora_autosetup.autosetup.autosetup import _reconcile_evm_version_keys +from certora_autosetup.utils.enhanced_config_manager import ConfigManager + + +# --------------------------------------------------------------------------- +# _reconcile_evm_version_keys (merged base conf + compilation updates) +# --------------------------------------------------------------------------- + + +def test_removal_propagates_over_base_scalar() -> None: + # The invalid_evm_version workaround dropped the declared version from the + # updates; the base build-system conf re-emits the scalar, which must not + # resurrect the rejected setting. + config = {"solc_evm_version": "paris"} + _reconcile_evm_version_keys(config, updates={"solc": "solc8.22"}, contract_names=["Foo"]) + assert "solc_evm_version" not in config + + +def test_scalar_kept_when_updates_still_carry_it() -> None: + config = {"solc_evm_version": "paris"} + _reconcile_evm_version_keys( + config, updates={"solc_evm_version": "paris"}, contract_names=["Foo"] + ) + assert config["solc_evm_version"] == "paris" + + +def test_scalar_kept_when_no_updates_exist() -> None: + # No compilation phase ran (e.g. cache hit): the declared version stands. + config = {"solc_evm_version": "paris"} + _reconcile_evm_version_keys(config, updates={}, contract_names=["Foo"]) + assert config["solc_evm_version"] == "paris" + + +def test_map_supersedes_scalar_and_is_completed() -> None: + # Cancun override for one contract + declared version: the scalar expands + # into the map for the contracts it misses (the prover forbids scalar+map + # and requires the map to cover every contract). + config = { + "solc_evm_version": "paris", + "solc_evm_version_map": {"Foo": "cancun"}, + } + _reconcile_evm_version_keys( + config, + updates={"solc_evm_version_map": {"Foo": "cancun"}}, + contract_names=["Foo", "Bar"], + ) + assert "solc_evm_version" not in config + assert config["solc_evm_version_map"] == {"Foo": "cancun", "Bar": "paris"} + + +def test_map_without_scalar_left_alone() -> None: + config = {"solc_evm_version_map": {"Foo": "cancun"}} + _reconcile_evm_version_keys( + config, + updates={"solc_evm_version_map": {"Foo": "cancun"}}, + contract_names=["Foo", "Bar"], + ) + assert config["solc_evm_version_map"] == {"Foo": "cancun"} + + +# --------------------------------------------------------------------------- +# sync_compiler_maps_with_files: evm map fill for newly injected files +# --------------------------------------------------------------------------- + + +def _touch_files(project_root: Path, files: list) -> None: + # parse_contract_files(strict=False) silently drops paths that don't exist. + for spec in files: + path = project_root / spec.split(":", 1)[0] + path.parent.mkdir(parents=True, exist_ok=True) + path.touch() + + +def test_sync_fills_evm_map_from_reference_scalar(tmp_path: Path) -> None: + manager = ConfigManager(project_root=tmp_path) + manager.reference_compiler_maps = {"solc_evm_version": "paris"} + conf = { + "files": ["contracts/Foo.sol:Foo", "certora/mocks/Mock.sol:Mock"], + "solc_evm_version_map": {"Foo": "cancun"}, + } + _touch_files(tmp_path, conf["files"]) + assert manager.sync_compiler_maps_with_files(conf) is True + assert conf["solc_evm_version_map"] == {"Foo": "cancun", "Mock": "paris"} + + +def test_sync_fills_evm_map_from_majority_value(tmp_path: Path) -> None: + manager = ConfigManager(project_root=tmp_path) + conf = { + "files": [ + "contracts/Foo.sol:Foo", + "contracts/Bar.sol:Bar", + "certora/mocks/Mock.sol:Mock", + ], + "solc_evm_version_map": {"Foo": "paris", "Bar": "paris"}, + } + _touch_files(tmp_path, conf["files"]) + assert manager.sync_compiler_maps_with_files(conf) is True + assert conf["solc_evm_version_map"]["Mock"] == "paris" + + +def test_sync_trims_and_fills_together(tmp_path: Path) -> None: + manager = ConfigManager(project_root=tmp_path) + manager.reference_compiler_maps = {"solc_evm_version": "paris"} + conf = { + "files": ["contracts/Foo.sol:Foo"], + "solc_evm_version_map": {"Gone": "cancun", "Foo": "paris"}, + } + _touch_files(tmp_path, conf["files"]) + assert manager.sync_compiler_maps_with_files(conf) is True + assert conf["solc_evm_version_map"] == {"Foo": "paris"} diff --git a/tests/test_foundry_config.py b/tests/test_foundry_config.py new file mode 100644 index 0000000..a7811f2 --- /dev/null +++ b/tests/test_foundry_config.py @@ -0,0 +1,62 @@ +"""Tests for FoundryManager compiler-settings parsing (foundry.toml). + +Covers the declared EVM version (`evm_version`): it must be honored because +solc's default EVM target can be newer than the declared one (shanghai/PUSH0 vs +a pinned "paris"), changing codegen and even failing with stack-too-deep where +the declared target compiles. + +`forge` is not available in CI, so `forge remappings` is monkeypatched away — +these tests only exercise the toml parsing. +""" + +from pathlib import Path + +import pytest + +from certora_autosetup.build_systems.foundry import FoundryManager +from certora_autosetup.utils import remappings as remappings_mod + + +@pytest.fixture(autouse=True) +def _no_forge(monkeypatch: pytest.MonkeyPatch) -> None: + def fake_run(*_args, **_kwargs): + raise FileNotFoundError("forge") + + monkeypatch.setattr(remappings_mod.subprocess, "run", fake_run) + + +def _parse(tmp_path: Path, toml: str, profile: str | None = None): + foundry_toml = tmp_path / "foundry.toml" + foundry_toml.write_text(toml) + manager = FoundryManager(project_root=tmp_path, scope=None) + return manager.parse_config(foundry_toml, profile) + + +def test_evm_version_read_from_default_profile(tmp_path: Path) -> None: + config = _parse(tmp_path, '[profile.default]\nevm_version = "paris"\n') + assert config.evm_version == "paris" + assert config.to_certora_dict()["solc_evm_version"] == "paris" + + +def test_evm_version_absent(tmp_path: Path) -> None: + config = _parse(tmp_path, '[profile.default]\nsrc = "src"\n') + assert config.evm_version is None + assert "solc_evm_version" not in config.to_certora_dict() + + +def test_evm_version_profile_override(tmp_path: Path) -> None: + config = _parse( + tmp_path, + '[profile.default]\nevm_version = "paris"\n[profile.ci]\nevm_version = "shanghai"\n', + profile="ci", + ) + assert config.evm_version == "shanghai" + + +def test_evm_version_inherited_from_default_profile(tmp_path: Path) -> None: + config = _parse( + tmp_path, + '[profile.default]\nevm_version = "paris"\n[profile.ci]\nsrc = "src"\n', + profile="ci", + ) + assert config.evm_version == "paris" diff --git a/tests/test_hardhat_config.py b/tests/test_hardhat_config.py index 0372cd7..e0d91e5 100644 --- a/tests/test_hardhat_config.py +++ b/tests/test_hardhat_config.py @@ -55,3 +55,54 @@ def test_missing_flag_keeps_reported_solc(manager: HardhatManager) -> None: {"solidity": "0.8.19", "paths": {}}, "javascript" ) assert config.solc_version == "0.8.19" + + +# Declared EVM version (settings.evmVersion) must be honored: solc's default EVM +# target can be newer than the declared one (shanghai/PUSH0 vs a pinned "paris"), +# changing codegen and even failing with stack-too-deep where the declared +# target compiles. + +EVM_VERSION_CONFIG = { + "solidity": { + "compilers": [ + { + "version": "0.8.22", + "settings": { + "optimizer": {"enabled": True, "runs": 1}, + "viaIR": True, + "evmVersion": "paris", + }, + } + ] + }, + "paths": {}, + "solidityImplicitDefault": False, +} + + +def test_evm_version_extracted_from_compilers_array(manager: HardhatManager) -> None: + config = manager._extract_config_from_json(EVM_VERSION_CONFIG, "javascript") + assert config.evm_version == "paris" + + +def test_evm_version_extracted_from_simple_format(manager: HardhatManager) -> None: + config = manager._extract_config_from_json( + {"solidity": {"version": "0.8.22", "settings": {"evmVersion": "paris"}}, "paths": {}}, + "javascript", + ) + assert config.evm_version == "paris" + + +def test_evm_version_absent(manager: HardhatManager) -> None: + assert manager._extract_config_from_json(EXPLICIT_CONFIG, "javascript").evm_version is None + assert ( + manager._extract_config_from_json({"solidity": "0.8.19", "paths": {}}, "javascript").evm_version + is None + ) + + +def test_evm_version_emitted_in_certora_dict(manager: HardhatManager) -> None: + config = manager._extract_config_from_json(EVM_VERSION_CONFIG, "javascript") + assert config.to_certora_dict()["solc_evm_version"] == "paris" + no_evm = manager._extract_config_from_json(EXPLICIT_CONFIG, "javascript") + assert "solc_evm_version" not in no_evm.to_certora_dict()