diff --git a/certora_autosetup/autosetup/autosetup.py b/certora_autosetup/autosetup/autosetup.py index 837d943..e3f7ec0 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. @@ -426,6 +456,15 @@ def get_build_system_config_dict_with_updates(self) -> Dict[str, Any]: if self.compilation_config_updates: config.update(self.compilation_config_updates) + # Must run BEFORE drop_scalars_superseded_by_maps: it expands the + # declared scalar into the map's missing entries (the map must cover + # every contract), which is impossible once the scalar is dropped. + _reconcile_evm_version_keys( + config, + self.compilation_config_updates, + [ch.contract_name for ch in self.contract_handles], + ) + # A per-contract map supersedes its scalar counterpart, and certoraRun # rejects a conf carrying both. The merge above can produce such pairs: # the base build-system dict contributes scalars (e.g. "solc") while diff --git a/certora_autosetup/build_systems/base.py b/certora_autosetup/build_systems/base.py index e16085e..72c9aa8 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 @@ -53,8 +56,7 @@ def to_certora_dict( Dictionary with Certora config format: { "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": [...] } """ @@ -142,6 +144,16 @@ def _apply_common_solc_settings( type(self).__name__, ) + # 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 8fd1b18..191448a 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_optimizer_runs=self.optimizer_runs, @@ -219,6 +219,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 @@ -275,6 +276,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, @@ -436,13 +438,13 @@ def apply_restrictions( # per-path via_ir is intentionally not applied: viaIR inlines internal functions, # which might prevent CVL internal summaries from being applied. - # 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 fac74d0..82349ed 100644 --- a/certora_autosetup/utils/compilation_workarounds.py +++ b/certora_autosetup/utils/compilation_workarounds.py @@ -139,6 +139,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-"): @@ -162,7 +167,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. When a map is already present (e.g. precomputed from build artifacts, or in a user conf fed through fixconf) the scalar still acts as the @@ -179,6 +185,16 @@ def _seed_compile_maps(self, config: Dict, contracts: List[ContractHandle]) -> N for c in contracts: config["solc_via_ir_map"].setdefault(c.contract_name, via_ir) + # 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). + evm_version = config.pop("solc_evm_version", None) + if evm_version: + config.setdefault("solc_evm_version_map", {}) + for c in contracts: + config["solc_evm_version_map"].setdefault(c.contract_name, evm_version) + 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. """ @@ -194,11 +210,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: @@ -263,12 +285,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 @@ -368,6 +393,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), @@ -396,22 +429,43 @@ 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 not self._yul_optimizer_pending(compilation_config, contracts) + 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 once the optimizer is on globally or for - # every scene contract (the rung above has nothing left to - # enable), and only on output produced AFTER the optimizer was - # tried, not in the same pass that just added it (the live - # 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 once the optimizer is + # on globally or for every scene contract (the add-optimizer + # rung has nothing left to enable) AND solc's default Yul steps + # were tried (strict_solc_optimizer), and only on output + # produced AFTER both were 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 not self._yul_optimizer_pending(compilation_config, contracts) + 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, @@ -686,6 +740,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]: @@ -982,6 +1055,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" @@ -993,6 +1071,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, @@ -1075,6 +1183,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, @@ -1092,8 +1231,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 5fc406d..06b7aae 100644 --- a/certora_autosetup/utils/enhanced_config_manager.py +++ b/certora_autosetup/utils/enhanced_config_manager.py @@ -416,14 +416,15 @@ def _update_compiler_maps_for_new_contracts( contracts_added: List[ContractHandle], ) -> bool: """ - Update compiler_map, solc_via_ir_map, and solc_optimize_map when new - contracts are added. + Update compiler_map, solc_via_ir_map, solc_optimize_map, and + solc_evm_version_map when new contracts are added. Delegates to CompilationWorkaroundManager which handles: - Parsing pragma from source files - Creating/updating compiler_map entries - Creating/updating solc_via_ir_map entries - Creating/updating solc_optimize_map entries + - Creating/updating solc_evm_version_map entries Args: conf_object: The config dict to modify in-place @@ -441,6 +442,7 @@ def _update_compiler_maps_for_new_contracts( modified |= self.update_compiler_map_for_contract(conf_object, contract, ref_maps) modified |= self.update_via_ir_map_for_contract(conf_object, contract, ref_maps) modified |= self.update_optimize_map_for_contract(conf_object, contract, ref_maps) + modified |= self.update_evm_version_map_for_contract(conf_object, contract, ref_maps) return modified @@ -1035,6 +1037,35 @@ def update_optimize_map_for_contract( self.log(f"Added {contract_name} to solc_optimize_map (value={optimize_value})") return True + def update_evm_version_map_for_contract( + self, + conf_object: Dict[str, Any], + contract: ContractHandle, + reference_maps: Optional[Dict[str, Any]] = None, + ) -> bool: + """Add a solc_evm_version_map entry for a newly-added contract. Mirrors + `update_optimize_map_for_contract` for the EVM-version map. Only the map + form is extended; a scalar `solc_evm_version` already applies to every + file. Unlike the optimize map there is no fixed default value: fall back + to the reference scalar, then to the map's most common value.""" + contract_name = contract.contract_name + if "solc_evm_version_map" not in conf_object: + return False + evm_map = conf_object["solc_evm_version_map"] + if contract_name in evm_map: + return False + reference_maps = reference_maps or {} + evm_value = ( + reference_maps.get("solc_evm_version_map", {}).get(contract_name) + or reference_maps.get("solc_evm_version") + or (Counter(evm_map.values()).most_common(1)[0][0] if evm_map else None) + ) + if evm_value is None: + return False + evm_map[contract_name] = evm_value + self.log(f"Added {contract_name} to solc_evm_version_map (value={evm_value})") + return True + def sync_compiler_maps_with_files( self, conf_object: Dict[str, Any], @@ -1120,6 +1151,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 if "solc_optimize_map" in conf_object: original_len = len(conf_object["solc_optimize_map"]) diff --git a/tests/test_compilation_workarounds.py b/tests/test_compilation_workarounds.py index 9576022..74ad45d 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 @@ -597,8 +625,8 @@ def test_yul_optimizer_rung_respects_project_optimize_map( # A per-contract solc_optimize_map (foundry compilation_restrictions) with # the optimizer on for EVERY contract: the add-optimizer rung has nothing # left to enable and must not put the scalar next to the map (certoraRun - # rejects the pair) — the ladder escalates to relaxing the autofinder - # assertion instead. + # rejects the pair) — the ladder escalates past it: solc's default Yul + # steps first, then relaxing the autofinder assertion. contracts = [ ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol"), ContractHandle(contract_name="Bar", source_file="contracts/Bar.sol"), @@ -607,7 +635,7 @@ def test_yul_optimizer_rung_respects_project_optimize_map( manager, monkeypatch, tmp_path, - [WRAPPED_YUL_STACK_TOO_DEEP], + [WRAPPED_YUL_STACK_TOO_DEEP, WRAPPED_YUL_STACK_TOO_DEEP], contracts, extra_config={ "solc_optimize_map": {"Foo": "1", "Bar": "200"}, @@ -615,8 +643,10 @@ def test_yul_optimizer_rung_respects_project_optimize_map( }, ) assert success is True + assert fake_run.calls == 3 assert "solc_optimize" not in compilation_config assert compilation_config["solc_optimize_map"] == {"Foo": "1", "Bar": "200"} + assert compilation_config["strict_solc_optimizer"] is True assert compilation_config["assert_autofinder_success"] is False @@ -627,7 +657,8 @@ def test_yul_optimizer_rung_enables_off_entries_in_optimize_map( # contract — exactly the misconfiguration the add-optimizer rung exists to # fix. It must enable those entries in the map (never the scalar, which # cannot legally sit next to it) while keeping explicit project runs - # values; only once every entry is on may the ladder escalate. + # values; only once every entry is on may the ladder escalate (to solc's + # default Yul steps — the autofinder assertion survives that step). contracts = [ ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol"), ContractHandle(contract_name="Bar", source_file="contracts/Bar.sol"), @@ -645,11 +676,13 @@ def test_yul_optimizer_rung_enables_off_entries_in_optimize_map( ) assert success is True # Pass 1 enables Foo's optimizer; pass 2 (optimizer on everywhere, error - # persists) escalates; the third compile succeeds. + # persists) escalates to solc's default Yul steps; the third compile + # succeeds with the autofinder assertion intact. assert fake_run.calls == 3 assert "solc_optimize" not in compilation_config assert compilation_config["solc_optimize_map"] == {"Foo": "200", "Bar": "1"} - assert compilation_config["assert_autofinder_success"] is False + assert compilation_config["strict_solc_optimizer"] is True + assert compilation_config["assert_autofinder_success"] is True # Whole-project solc error with no per-file "Compiling ..." progress line: the @@ -692,3 +725,134 @@ def test_compiling_line_takes_precedence_over_source_location(manager: Compilati # Pattern 2 wins, mapping to the contract actually being compiled. contracts = [ContractHandle(contract_name="Foo", source_file="contracts/Foo.sol")] assert manager._detect_stack_too_deep_errors(COMPILING_LINE_STACK_TOO_DEEP, contracts) == "Foo" + + +# ============================================================================= +# 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()