From 9dce0c384f910b378e0e01f7ce211f2c66650115 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:26:09 +0300 Subject: [PATCH 1/3] Auto-enable dynamic_bound/dynamic_dispatch when Clones library is used Minimal-proxy clones deployed via OpenZeppelin's Clones library (EIP-1167) are only resolvable by the prover dynamically, not statically -- without dynamic_bound/dynamic_dispatch, calls on a freshly-cloned instance hit "ASSUME false[optimistic dispatcher]" and every path through the creating function reverts, producing a vacuous sanity check. Nothing defaulted these on before, so every Clones-using project needed a manual conf edit. Detect Clones.clone/cloneDeterministic/cloneWithImmutableArgs calls (both direct Clones.clone(...) and `using Clones for address` attached-call forms) purely via the already-parsed solc AST -- no regex/string-matching on source text. Wired in as its own phase in setup_prover.py, mirroring the existing ERC-7201 detection phase's "detect -> set flag on updated_config_dict" idiom. Each key is skipped independently if the user already controls it, via a pre-populated config_dict entry or a raw --dynamic_bound/--dynamic_dispatch token (either "--flag value" or "--flag=value" form) in --extra-args. Verified end-to-end against the real-world case that motivated this: running certora-autosetup against lidofinance/stonks's BuybackExecutor (which depends on Stonks.sol's Clones.clone() call in placeOrderWithAmount()) produces a base conf with dynamic_bound/dynamic_dispatch set automatically, no manual edit needed. Co-Authored-By: Claude Sonnet 5 --- certora_autosetup/setup/clones_detection.py | 111 ++++++++++++++++++++ certora_autosetup/setup/setup_prover.py | 36 ++++++- 2 files changed, 145 insertions(+), 2 deletions(-) create mode 100644 certora_autosetup/setup/clones_detection.py diff --git a/certora_autosetup/setup/clones_detection.py b/certora_autosetup/setup/clones_detection.py new file mode 100644 index 00000000..7de77c3c --- /dev/null +++ b/certora_autosetup/setup/clones_detection.py @@ -0,0 +1,111 @@ +""" +OpenZeppelin Clones library usage detector. + +Scans an already-parsed AST dict (as produced by SetupProver.generate_ast_graph from +all_asts.json: dict[relative_path -> dict[absolute_path -> dict[node_id -> node]]]) for calls +that create a new minimal-proxy clone via OpenZeppelin's Clones library -- both the direct +call form (Clones.clone(...)) and the `using Clones for address; addr.clone()` attached-call +form -- so dynamic_bound/dynamic_dispatch can default on in the base config: minimal-proxy +clones are only resolvable by the prover dynamically, not statically. +""" + +from pathlib import Path +from typing import Any, Callable, Dict + +from certora_autosetup.utils.scope import Scope + +# Only members that actually deploy a new minimal-proxy instance need dynamic_bound/ +# dynamic_dispatch. predictDeterministicAddress/fetchCloneArgs only compute +# addresses/args and don't by themselves require dynamic dispatch. +CLONE_CREATION_MEMBERS = {"clone", "cloneDeterministic", "cloneWithImmutableArgs"} +CLONES_LIBRARY_TYPESTRING = "type(library Clones)" + + +def detect_clones_usage(log_func: Callable, asts_data: Dict[str, Any], scope: Scope) -> bool: + """ + Detect calls that create an OpenZeppelin Clones minimal-proxy instance, anywhere in the + in-scope portion of the compiled AST. + + Args: + log_func: Logging function (signature: log_func(message, level="INFO")). + asts_data: Parsed all_asts.json, UNFILTERED by scope -- library declarations (e.g. + under node_modules/@openzeppelin) are typically themselves out of scope but must + still be resolvable for the `using X for address` attached-call path below. + scope: Scope object; only call-site files are filtered through it. + + Returns: + True if a Clones-creation call was found in an in-scope file, False otherwise. + """ + log_func("Scanning AST for OpenZeppelin Clones library usage...") + + for relative_path, path_data in asts_data.items(): + if not scope.is_file_in_scope(Path(relative_path)): + continue + + # id -> node index for THIS top-level relative_path's compilation unit only. Node ids + # are unique across all of a compilation unit's absolute_path buckets but NOT globally + # across other top-level relative_path entries in asts_data, so this index must be + # rebuilt per relative_path rather than merged across the whole file -- otherwise a + # colliding id from an unrelated compilation unit silently resolves to the wrong node. + id_to_node: Dict[int, Dict[str, Any]] = {} + for _absolute_path, nodes in path_data.items(): + for node in nodes.values(): + if isinstance(node, dict) and "id" in node: + id_to_node[node["id"]] = node + + def _is_clones_library_call(callee: Dict[str, Any]) -> bool: + # Direct-call form: Clones.clone(...) -- base expression's static type IS the + # library type. + base = callee.get("expression", {}) + if base.get("typeDescriptions", {}).get("typeString") == CLONES_LIBRARY_TYPESTRING: + return True + + # Attached-call form: using Clones for address; addr.clone() -- resolve the member + # access's referencedDeclaration to the FunctionDefinition, then check ITS + # enclosing library via the `scope` field. + ref_id = callee.get("referencedDeclaration") + if ref_id is None: + return False + func_def = id_to_node.get(ref_id) + if not func_def or func_def.get("nodeType") != "FunctionDefinition": + return False + library_node = id_to_node.get(func_def.get("scope")) + if not library_node or library_node.get("nodeType") != "ContractDefinition": + return False + return ( + library_node.get("contractKind") == "library" + and library_node.get("name") == "Clones" + ) + + for absolute_path, nodes in path_data.items(): + try: + abs_path_obj = Path(absolute_path) + if abs_path_obj.is_absolute(): + rel_path_for_scope = abs_path_obj.relative_to(scope.project_root.resolve()) + else: + rel_path_for_scope = abs_path_obj + except ValueError: + continue + if not scope.is_file_in_scope(rel_path_for_scope): + continue + + for _node_id, node in nodes.items(): + if not isinstance(node, dict) or node.get("nodeType") != "FunctionCall": + continue + + callee = node.get("expression", {}) + if ( + callee.get("nodeType") != "MemberAccess" + or callee.get("memberName") not in CLONE_CREATION_MEMBERS + ): + continue + + if _is_clones_library_call(callee): + log_func( + f"Clones library call detected: {relative_path} calls " + f"Clones.{callee.get('memberName')}(...)" + ) + return True + + log_func("No OpenZeppelin Clones library usage found.") + return False diff --git a/certora_autosetup/setup/setup_prover.py b/certora_autosetup/setup/setup_prover.py index bcd42a30..2788fa32 100644 --- a/certora_autosetup/setup/setup_prover.py +++ b/certora_autosetup/setup/setup_prover.py @@ -26,6 +26,7 @@ from certora_autosetup.parsers.foundry import FoundryContractExtractor from certora_autosetup.utils.contract_utils import parse_contract_files from certora_autosetup.setup.auto_munges import detect_and_apply_code_access_patches +from certora_autosetup.setup.clones_detection import detect_clones_usage from certora_autosetup.setup.signature_manager import SignatureManager from certora_autosetup.setup.signature_types import ContractInfo from certora_autosetup.setup.solidity_utils import extract_definitions_from_solidity @@ -106,6 +107,7 @@ def __init__( self.compilation_config_updates: Dict[str, Any] = {} self.import_patcher_applied: bool = False self.erc7201_namespaces_found: bool = False + self.clones_usage_found: bool = False self._remappings_workaround_applied: bool = False self._build_dir: Path | None = None # SummarySetup is constructed during run_setup_summaries and kept around so that @@ -1287,7 +1289,7 @@ def _extract_contract_infos_from_build( self.log(f"Error extracting contract infos: {e}", "ERROR") return [] - def generate_ast_graph(self, ast_path: Path) -> None: + def generate_ast_graph(self, ast_path: Path) -> Optional[Dict[str, Any]]: """ Generate a parent graph from the AST for efficient node parent lookups. @@ -1340,10 +1342,12 @@ def generate_ast_graph(self, ast_path: Path) -> None: json.dump(parent_graph, f, indent=2) self.log(f"✓ AST parent graph saved to {graph_path}") + return asts_data except Exception as e: self.log(f"Warning: Failed to generate AST parent graph: {e}", "WARNING") self.log(f"Traceback: {traceback.format_exc()}", "WARNING") + return None def _extract_child_node_ids(self, node: Any) -> List[int]: """ @@ -1440,7 +1444,17 @@ def process_certora_build_json(self) -> bool: f"Failed to copy .asts.json from {asts_source} to {asts_target}: {e}" ) - self.generate_ast_graph(asts_target) + asts_data = self.generate_ast_graph(asts_target) + if asts_data is None: + # generate_ast_graph already logged a WARNING on parse failure; don't let + # that outage silently swallow Clones detection too -- reload independently. + try: + with open(asts_target, "r", encoding="utf-8") as f: + asts_data = json.load(f) + except Exception as e: + self.log(f"Warning: could not load AST for Clones detection: {e}", "WARNING") + asts_data = {} + self.clones_usage_found = detect_clones_usage(self.log, asts_data, self.scope) # Generate signature database (uses the ast file copied before) self.generate_signature_database_json(build_json_path) @@ -1578,6 +1592,24 @@ def setup_prover( if self.erc7201_namespaces_found: updated_config_dict["storage_extension_annotation"] = True + # Propagate Clones-library-usage (detected during compilation analysis) into the + # config dict, mirroring the ERC-7201 flag above. Each key is skipped independently + # if the user already controls it -- via build-system config merged into + # updated_config_dict at line 294 (foundry.toml/hardhat.config), or via a raw + # --dynamic_bound/--dynamic_dispatch token passed through --extra-args (matches both + # "--dynamic_bound 1" and "--dynamic_bound=1" forms; does not attempt to parse the + # legacy "--settings -dynamicCreationBound=..." catch-all syntax). + def _extra_args_sets(flag: str) -> bool: + return any(arg == flag or arg.startswith(flag + "=") for arg in self.extra_args) + + if self.clones_usage_found: + if "dynamic_bound" not in updated_config_dict and not _extra_args_sets("--dynamic_bound"): + self.log("=== CLONES USAGE DETECTED: enabling dynamic_bound ===") + updated_config_dict["dynamic_bound"] = "1" + if "dynamic_dispatch" not in updated_config_dict and not _extra_args_sets("--dynamic_dispatch"): + self.log("=== CLONES USAGE DETECTED: enabling dynamic_dispatch ===") + updated_config_dict["dynamic_dispatch"] = True + aggregator_path = ( self.certora_dir / SUMMARIES_SUBDIR / f"{main_contract_name}_base_summaries.spec" ) From 24e90195a032c8b862d8cf402aa3e278b52ae8a5 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sun, 5 Jul 2026 23:10:53 +0300 Subject: [PATCH 2/3] Generalize to instruction-level contract-creation detection Replaces the OpenZeppelin-Clones-specific detector with an instruction-level one (creation_detection.py): per compilation unit, every FunctionDefinition/ ModifierDefinition/ContractDefinition subtree is scanned for Yul create/create2 and typed `new C()`, and creation kinds are propagated up the intra-unit call graph (referencedDeclaration edges from call sites and modifier invocations) to a fixpoint; roots are nodes in in-scope files plus linearized base contracts. Covers Solady LibClone, clones-with-immutable-args, CREATE3 wrappers and hand-rolled factories without naming any library. ContractDefinition nodes aggregate their embedded members, so constructor-time creation outside any function (state-variable initializers, inheritance-specifier base-constructor arguments) is caught too. Flag gating is now kind-aware: any creation defaults dynamic_bound=1; only runtime-assembled bytecode (assembly create/create2) additionally defaults dynamic_dispatch, since a typed `new C()` instance resolves to a clone of C under dynamic_bound alone and keeps static call resolution. all_asts.json is now parsed once in process_certora_build_json and shared by generate_ast_graph (signature changed to take the parsed dict) and the detector -- the previous re-parse fallback would have failed exactly like the original parse, so it is gone. Hardening from an adversarial review pass over real solc 0.5.17-0.8.25 output: iterative subtree walk (deep machine-generated expressions previously hit Python's recursion limit and failed the whole compilation-analysis phase), and a loud warning on solc<0.6 unstructured inline assembly, where raw creates are invisible to the structured-Yul scan. clones_detection.py is superseded, no longer imported, and removed in a follow-up commit. Co-Authored-By: Claude Fable 5 --- certora_autosetup/setup/creation_detection.py | 251 ++++++++++++++++++ certora_autosetup/setup/setup_prover.py | 54 ++-- 2 files changed, 280 insertions(+), 25 deletions(-) create mode 100644 certora_autosetup/setup/creation_detection.py diff --git a/certora_autosetup/setup/creation_detection.py b/certora_autosetup/setup/creation_detection.py new file mode 100644 index 00000000..793323e0 --- /dev/null +++ b/certora_autosetup/setup/creation_detection.py @@ -0,0 +1,251 @@ +""" +Contract-creation detector. + +Scans an already-parsed AST dict (loaded from all_asts.json: dict[relative_path -> +dict[absolute_path -> dict[node_id -> node]]]) for contract creation reachable from in-scope +code, so dynamic_bound/dynamic_dispatch can default on in the base config. Detection is by +creation *instruction*, not by library name, so any minimal-proxy/factory library (OpenZeppelin +Clones, Solady LibClone, clones-with-immutable-args, CREATE3 wrappers, ...) is covered without +enumerating them. Two creation kinds are distinguished because they need different flags: + +- Yul ``create``/``create2`` in inline assembly: the creation bytecode is assembled at runtime, + so the prover cannot resolve calls on the created instance statically -- these need both + --dynamic_bound and --dynamic_dispatch. +- ``new C()`` (a NewExpression of a contract type): the creation bytecode is C's, so under + --dynamic_bound the prover resolves the instance to a clone of C and calls on it stay + statically resolved -- only --dynamic_bound is needed. + +Mechanics, per compilation unit (one top-level relative_path bucket): every +FunctionDefinition/ModifierDefinition/ContractDefinition is checked for direct creation over +its full embedded subtree (contracts thereby cover creation living outside any function: +state-variable initializers and inheritance-specifier base-constructor arguments), creation +kinds are then propagated up the intra-unit call graph (referencedDeclaration edges from call +sites and modifier invocations) to a fixpoint, and the unit's answer is the union over nodes +in in-scope files -- plus every base contract an in-scope contract linearizes over (via +linearizedBaseContracts), since inherited entry points execute as part of the verified +contract. This reachability step is what makes out-of-scope creation libraries +(node_modules/@openzeppelin, solady, ...) count when, and only when, in-scope code can reach +them. + +Known under-approximations: calls through internal function pointers carry no +referencedDeclaration to the target, so creation reachable only that way is missed (inherent +to any static referencedDeclaration call graph); and solc < 0.6 emits inline assembly as a raw +source string (no structured Yul AST), so raw creates there are invisible -- a warning is +logged when such a node is seen. +""" + +from dataclasses import dataclass +from pathlib import Path +from typing import Any, Callable, Dict, Iterator, Optional, Set, Tuple + +from certora_autosetup.utils.scope import Scope + +YUL_CREATE_OPCODES = {"create", "create2"} + +# Node types that anchor the call graph. Functions and modifiers own executable bodies; +# contracts additionally own the constructor-time code that lives outside any of them +# (state-variable initializers, inheritance-specifier base-constructor arguments) -- a +# ContractDefinition's embedded subtree covers all of its members, so a contract node +# aggregates everything the contract can execute. +DEFINITION_NODE_TYPES = {"FunctionDefinition", "ModifierDefinition", "ContractDefinition"} + + +@dataclass +class CreationUsage: + """Which contract-creation kinds are reachable from in-scope code.""" + + new_expression: bool = False # typed `new C()` -- creation bytecode statically known + raw_create: bool = False # Yul create/create2 -- creation bytecode assembled at runtime + + @property + def found(self) -> bool: + return self.new_expression or self.raw_create + + @property + def complete(self) -> bool: + """Both kinds seen -- nothing more to learn, scanning can stop early.""" + return self.new_expression and self.raw_create + + def merge(self, other: "CreationUsage") -> None: + self.new_expression = self.new_expression or other.new_expression + self.raw_create = self.raw_create or other.raw_create + + +def _walk(node: Any) -> Iterator[Dict[str, Any]]: + """Yield every dict in an embedded AST subtree, including Yul sub-ASTs (whose nodes carry + no ids and therefore only exist embedded inside their InlineAssembly node). Iterative: + machine-generated code can nest expressions deeper than Python's recursion limit.""" + stack = [node] + while stack: + current = stack.pop() + if isinstance(current, dict): + yield current + stack.extend(current.values()) + elif isinstance(current, list): + stack.extend(current) + + +def _analyze_definition(definition: Dict[str, Any]) -> Tuple[CreationUsage, Set[int], bool]: + """One pass over a definition's subtree: which creation kinds it performs directly, the + referencedDeclaration ids of everything it calls (call sites and modifier invocations), + and whether it contains legacy unstructured inline assembly (solc < 0.6: a raw source + string under `operations` instead of a Yul AST) that raw-create scanning cannot see.""" + usage = CreationUsage() + callees: Set[int] = set() + has_legacy_assembly = False + for sub in _walk(definition): + node_type = sub.get("nodeType") + if node_type == "YulFunctionCall": + if sub.get("functionName", {}).get("name") in YUL_CREATE_OPCODES: + usage.raw_create = True + elif node_type == "InlineAssembly": + if "AST" not in sub: + has_legacy_assembly = True + elif node_type == "NewExpression": + # `new C()` has a UserDefinedTypeName; `new uint[](n)` / `new bytes(n)` have an + # ArrayTypeName and allocate memory, not a contract. + if sub.get("typeName", {}).get("nodeType") == "UserDefinedTypeName": + usage.new_expression = True + elif node_type == "FunctionCall": + callee = sub.get("expression", {}) + if callee.get("nodeType") == "FunctionCallOptions": # f{value: ...}(...) + callee = callee.get("expression", {}) + ref = callee.get("referencedDeclaration") + if ref is not None: + callees.add(ref) + elif node_type == "ModifierInvocation": + ref = sub.get("modifierName", {}).get("referencedDeclaration") + if ref is not None: + callees.add(ref) + return usage, callees, has_legacy_assembly + + +def _relative_to_project(absolute_path: str, scope: Scope) -> Optional[Path]: + """Map an AST absolute_path bucket to a project-relative path for scope checks; None for + paths outside the project root (they can never be in scope).""" + path_obj = Path(absolute_path) + if not path_obj.is_absolute(): + return path_obj + try: + return path_obj.relative_to(scope.project_root.resolve()) + except ValueError: + return None + + +def _scan_unit( + log_func: Callable, relative_path: str, path_data: Dict[str, Any], scope: Scope +) -> CreationUsage: + """Detect creation reachable from in-scope definitions of one compilation unit.""" + # id -> node index for THIS top-level relative_path's compilation unit only. Node ids are + # unique across all of a compilation unit's absolute_path buckets but NOT globally across + # other top-level relative_path entries in asts_data, so this index must be rebuilt per + # relative_path rather than merged across the whole file -- otherwise a colliding id from + # an unrelated compilation unit silently resolves to the wrong node. + id_to_node: Dict[int, Dict[str, Any]] = {} + in_scope_ids: Set[int] = set() + for absolute_path, nodes in path_data.items(): + rel_path = _relative_to_project(absolute_path, scope) + bucket_in_scope = rel_path is not None and scope.is_file_in_scope(rel_path) + for node in nodes.values(): + if isinstance(node, dict) and "id" in node: + id_to_node[node["id"]] = node + if bucket_in_scope: + in_scope_ids.add(node["id"]) + + # Direct creation kinds + call edges per definition. + reachable: Dict[int, CreationUsage] = {} + calls: Dict[int, Set[int]] = {} + legacy_assembly_warned = False + for node_id, node in id_to_node.items(): + if node.get("nodeType") in DEFINITION_NODE_TYPES: + reachable[node_id], calls[node_id], has_legacy_assembly = _analyze_definition(node) + if has_legacy_assembly and not legacy_assembly_warned: + log_func( + f"Inline assembly without a structured Yul AST (solc < 0.6) in " + f"{relative_path}; raw create/create2 in it cannot be detected", + "WARNING", + ) + legacy_assembly_warned = True + + # Fixpoint: a definition reaches every creation kind its callees reach. The call graph may + # have cycles (recursion), so iterate until stable rather than topologically. + changed = True + while changed: + changed = False + for definition_id, callee_ids in calls.items(): + usage = reachable[definition_id] + for callee_id in callee_ids: + callee_usage = reachable.get(callee_id) + if callee_usage is None: + continue + if (callee_usage.new_expression and not usage.new_expression) or ( + callee_usage.raw_create and not usage.raw_create + ): + usage.merge(callee_usage) + changed = True + + # Roots whose reachability counts: nodes in in-scope files, plus every base contract an + # in-scope contract linearizes over -- inherited entry points (and base constructor-time + # code) run as part of the verified contract even though their defining file may be out of + # scope. A base's contract node aggregates all of its members, so adding it suffices. + root_ids: Set[int] = {definition_id for definition_id in reachable if definition_id in in_scope_ids} + for node_id, node in id_to_node.items(): + if node.get("nodeType") == "ContractDefinition" and node_id in in_scope_ids: + for base_id in node.get("linearizedBaseContracts", []): + if base_id in reachable: + root_ids.add(base_id) + + unit_usage = CreationUsage() + for root_id in root_ids: + root_usage = reachable[root_id] + if root_usage.found and not ( + (not root_usage.new_expression or unit_usage.new_expression) + and (not root_usage.raw_create or unit_usage.raw_create) + ): + root = id_to_node[root_id] + kinds = [ + kind + for kind, present in ( + ("assembly create/create2", root_usage.raw_create), + ("new-expression", root_usage.new_expression), + ) + if present + ] + log_func( + f"Contract creation ({', '.join(kinds)}) reachable from " + f"{relative_path}: {root.get('name') or ''}" + ) + unit_usage.merge(root_usage) + if unit_usage.complete: + break + return unit_usage + + +def detect_contract_creation(log_func: Callable, asts_data: Dict[str, Any], scope: Scope) -> CreationUsage: + """ + Detect contract creation (typed `new` and raw assembly create/create2) reachable from the + in-scope portion of the compiled AST. + + Args: + log_func: Logging function (signature: log_func(message, level="INFO")). + asts_data: Parsed all_asts.json, UNFILTERED by scope -- creation-library definitions + (e.g. under node_modules/@openzeppelin or solady) are typically themselves out of + scope but must still be resolvable as call-graph targets. + scope: Scope object; only the defining files of call-graph roots are filtered through it. + + Returns: + CreationUsage saying which creation kinds were found. + """ + log_func("Scanning AST for contract creation (new / assembly create/create2)...") + + total = CreationUsage() + for relative_path, path_data in asts_data.items(): + if not scope.is_file_in_scope(Path(relative_path)): + continue + total.merge(_scan_unit(log_func, relative_path, path_data, scope)) + if total.complete: + break + + if not total.found: + log_func("No contract creation found in in-scope code.") + return total diff --git a/certora_autosetup/setup/setup_prover.py b/certora_autosetup/setup/setup_prover.py index 2788fa32..213e16f4 100644 --- a/certora_autosetup/setup/setup_prover.py +++ b/certora_autosetup/setup/setup_prover.py @@ -26,7 +26,7 @@ from certora_autosetup.parsers.foundry import FoundryContractExtractor from certora_autosetup.utils.contract_utils import parse_contract_files from certora_autosetup.setup.auto_munges import detect_and_apply_code_access_patches -from certora_autosetup.setup.clones_detection import detect_clones_usage +from certora_autosetup.setup.creation_detection import CreationUsage, detect_contract_creation from certora_autosetup.setup.signature_manager import SignatureManager from certora_autosetup.setup.signature_types import ContractInfo from certora_autosetup.setup.solidity_utils import extract_definitions_from_solidity @@ -107,7 +107,7 @@ def __init__( self.compilation_config_updates: Dict[str, Any] = {} self.import_patcher_applied: bool = False self.erc7201_namespaces_found: bool = False - self.clones_usage_found: bool = False + self.creation_usage: CreationUsage = CreationUsage() self._remappings_workaround_applied: bool = False self._build_dir: Path | None = None # SummarySetup is constructed during run_setup_summaries and kept around so that @@ -1289,7 +1289,7 @@ def _extract_contract_infos_from_build( self.log(f"Error extracting contract infos: {e}", "ERROR") return [] - def generate_ast_graph(self, ast_path: Path) -> Optional[Dict[str, Any]]: + def generate_ast_graph(self, asts_data: Dict[str, Any]) -> None: """ Generate a parent graph from the AST for efficient node parent lookups. @@ -1298,7 +1298,8 @@ def generate_ast_graph(self, ast_path: Path) -> Optional[Dict[str, Any]]: operations like detecting chained member accesses. Args: - ast_path: Path to the .asts.json file + asts_data: Parsed all_asts.json contents (loaded once by the caller and shared + with contract-creation detection) Output: Writes to .certora_internal/.ast_graph.json with structure: @@ -1313,9 +1314,6 @@ def generate_ast_graph(self, ast_path: Path) -> Optional[Dict[str, Any]]: self.log("Building AST parent graph...") try: - with open(ast_path, 'r') as f: - asts_data = json.load(f) - # Build parent graph: node_id -> parent_node_id parent_graph = {} @@ -1342,12 +1340,10 @@ def generate_ast_graph(self, ast_path: Path) -> Optional[Dict[str, Any]]: json.dump(parent_graph, f, indent=2) self.log(f"✓ AST parent graph saved to {graph_path}") - return asts_data except Exception as e: self.log(f"Warning: Failed to generate AST parent graph: {e}", "WARNING") self.log(f"Traceback: {traceback.format_exc()}", "WARNING") - return None def _extract_child_node_ids(self, node: Any) -> List[int]: """ @@ -1444,17 +1440,17 @@ def process_certora_build_json(self) -> bool: f"Failed to copy .asts.json from {asts_source} to {asts_target}: {e}" ) - asts_data = self.generate_ast_graph(asts_target) - if asts_data is None: - # generate_ast_graph already logged a WARNING on parse failure; don't let - # that outage silently swallow Clones detection too -- reload independently. - try: - with open(asts_target, "r", encoding="utf-8") as f: - asts_data = json.load(f) - except Exception as e: - self.log(f"Warning: could not load AST for Clones detection: {e}", "WARNING") - asts_data = {} - self.clones_usage_found = detect_clones_usage(self.log, asts_data, self.scope) + # Parsed once, shared by the parent-graph builder and creation detection below; + # a parse failure degrades both to a warning without failing the build processing. + try: + with open(asts_target, "r", encoding="utf-8") as f: + asts_data: Dict[str, Any] = json.load(f) + except Exception as e: + self.log(f"Warning: failed to parse {asts_target}: {e}", "WARNING") + asts_data = {} + if asts_data: + self.generate_ast_graph(asts_data) + self.creation_usage = detect_contract_creation(self.log, asts_data, self.scope) # Generate signature database (uses the ast file copied before) self.generate_signature_database_json(build_json_path) @@ -1592,7 +1588,7 @@ def setup_prover( if self.erc7201_namespaces_found: updated_config_dict["storage_extension_annotation"] = True - # Propagate Clones-library-usage (detected during compilation analysis) into the + # Propagate contract-creation usage (detected during compilation analysis) into the # config dict, mirroring the ERC-7201 flag above. Each key is skipped independently # if the user already controls it -- via build-system config merged into # updated_config_dict at line 294 (foundry.toml/hardhat.config), or via a raw @@ -1602,12 +1598,20 @@ def setup_prover( def _extra_args_sets(flag: str) -> bool: return any(arg == flag or arg.startswith(flag + "=") for arg in self.extra_args) - if self.clones_usage_found: + if self.creation_usage.found: if "dynamic_bound" not in updated_config_dict and not _extra_args_sets("--dynamic_bound"): - self.log("=== CLONES USAGE DETECTED: enabling dynamic_bound ===") + self.log("=== CONTRACT CREATION DETECTED: enabling dynamic_bound ===") updated_config_dict["dynamic_bound"] = "1" - if "dynamic_dispatch" not in updated_config_dict and not _extra_args_sets("--dynamic_dispatch"): - self.log("=== CLONES USAGE DETECTED: enabling dynamic_dispatch ===") + # Only runtime-assembled creation bytecode (assembly create/create2 -- minimal-proxy + # clone libraries and the like) also needs dynamic_dispatch: calls on such an + # instance are statically unresolvable. A typed `new C()` instance resolves to a + # clone of C under dynamic_bound alone, keeping the more precise static resolution. + if ( + self.creation_usage.raw_create + and "dynamic_dispatch" not in updated_config_dict + and not _extra_args_sets("--dynamic_dispatch") + ): + self.log("=== RUNTIME-BYTECODE CREATION DETECTED: enabling dynamic_dispatch ===") updated_config_dict["dynamic_dispatch"] = True aggregator_path = ( From d76df95e5c155e218174de2f4aff61bdea92c107 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Mon, 6 Jul 2026 17:59:54 +0300 Subject: [PATCH 3/3] Remove superseded clones_detection module Replaced by creation_detection.py in the previous commit; nothing imports it. Co-Authored-By: Claude Fable 5 --- certora_autosetup/setup/clones_detection.py | 111 -------------------- 1 file changed, 111 deletions(-) delete mode 100644 certora_autosetup/setup/clones_detection.py diff --git a/certora_autosetup/setup/clones_detection.py b/certora_autosetup/setup/clones_detection.py deleted file mode 100644 index 7de77c3c..00000000 --- a/certora_autosetup/setup/clones_detection.py +++ /dev/null @@ -1,111 +0,0 @@ -""" -OpenZeppelin Clones library usage detector. - -Scans an already-parsed AST dict (as produced by SetupProver.generate_ast_graph from -all_asts.json: dict[relative_path -> dict[absolute_path -> dict[node_id -> node]]]) for calls -that create a new minimal-proxy clone via OpenZeppelin's Clones library -- both the direct -call form (Clones.clone(...)) and the `using Clones for address; addr.clone()` attached-call -form -- so dynamic_bound/dynamic_dispatch can default on in the base config: minimal-proxy -clones are only resolvable by the prover dynamically, not statically. -""" - -from pathlib import Path -from typing import Any, Callable, Dict - -from certora_autosetup.utils.scope import Scope - -# Only members that actually deploy a new minimal-proxy instance need dynamic_bound/ -# dynamic_dispatch. predictDeterministicAddress/fetchCloneArgs only compute -# addresses/args and don't by themselves require dynamic dispatch. -CLONE_CREATION_MEMBERS = {"clone", "cloneDeterministic", "cloneWithImmutableArgs"} -CLONES_LIBRARY_TYPESTRING = "type(library Clones)" - - -def detect_clones_usage(log_func: Callable, asts_data: Dict[str, Any], scope: Scope) -> bool: - """ - Detect calls that create an OpenZeppelin Clones minimal-proxy instance, anywhere in the - in-scope portion of the compiled AST. - - Args: - log_func: Logging function (signature: log_func(message, level="INFO")). - asts_data: Parsed all_asts.json, UNFILTERED by scope -- library declarations (e.g. - under node_modules/@openzeppelin) are typically themselves out of scope but must - still be resolvable for the `using X for address` attached-call path below. - scope: Scope object; only call-site files are filtered through it. - - Returns: - True if a Clones-creation call was found in an in-scope file, False otherwise. - """ - log_func("Scanning AST for OpenZeppelin Clones library usage...") - - for relative_path, path_data in asts_data.items(): - if not scope.is_file_in_scope(Path(relative_path)): - continue - - # id -> node index for THIS top-level relative_path's compilation unit only. Node ids - # are unique across all of a compilation unit's absolute_path buckets but NOT globally - # across other top-level relative_path entries in asts_data, so this index must be - # rebuilt per relative_path rather than merged across the whole file -- otherwise a - # colliding id from an unrelated compilation unit silently resolves to the wrong node. - id_to_node: Dict[int, Dict[str, Any]] = {} - for _absolute_path, nodes in path_data.items(): - for node in nodes.values(): - if isinstance(node, dict) and "id" in node: - id_to_node[node["id"]] = node - - def _is_clones_library_call(callee: Dict[str, Any]) -> bool: - # Direct-call form: Clones.clone(...) -- base expression's static type IS the - # library type. - base = callee.get("expression", {}) - if base.get("typeDescriptions", {}).get("typeString") == CLONES_LIBRARY_TYPESTRING: - return True - - # Attached-call form: using Clones for address; addr.clone() -- resolve the member - # access's referencedDeclaration to the FunctionDefinition, then check ITS - # enclosing library via the `scope` field. - ref_id = callee.get("referencedDeclaration") - if ref_id is None: - return False - func_def = id_to_node.get(ref_id) - if not func_def or func_def.get("nodeType") != "FunctionDefinition": - return False - library_node = id_to_node.get(func_def.get("scope")) - if not library_node or library_node.get("nodeType") != "ContractDefinition": - return False - return ( - library_node.get("contractKind") == "library" - and library_node.get("name") == "Clones" - ) - - for absolute_path, nodes in path_data.items(): - try: - abs_path_obj = Path(absolute_path) - if abs_path_obj.is_absolute(): - rel_path_for_scope = abs_path_obj.relative_to(scope.project_root.resolve()) - else: - rel_path_for_scope = abs_path_obj - except ValueError: - continue - if not scope.is_file_in_scope(rel_path_for_scope): - continue - - for _node_id, node in nodes.items(): - if not isinstance(node, dict) or node.get("nodeType") != "FunctionCall": - continue - - callee = node.get("expression", {}) - if ( - callee.get("nodeType") != "MemberAccess" - or callee.get("memberName") not in CLONE_CREATION_MEMBERS - ): - continue - - if _is_clones_library_call(callee): - log_func( - f"Clones library call detected: {relative_path} calls " - f"Clones.{callee.get('memberName')}(...)" - ) - return True - - log_func("No OpenZeppelin Clones library usage found.") - return False