Skip to content
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
111 changes: 111 additions & 0 deletions certora_autosetup/setup/clones_detection.py
Original file line number Diff line number Diff line change
@@ -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
36 changes: 34 additions & 2 deletions certora_autosetup/setup/setup_prover.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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]:
"""
Expand Down Expand Up @@ -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.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why would it succeed in this case as opposed to failing in generate_ast_graph?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Claude answers: You were right that it wouldn't — a JSON re-parse of the same file would fail exactly like generate_ast_graph's own parse did; the only cases the fallback actually covered were post-parse failures inside generate_ast_graph (parent-graph build or the graph-file write). Restructured in 24e9019: all_asts.json is parsed once in process_certora_build_json and the parsed dict is passed to both generate_ast_graph (signature now takes the dict) and creation detection, so the fallback is gone entirely. A parse failure now degrades both consumers to a single warning; a parent-graph build/write failure no longer affects detection at all.

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)
Expand Down Expand Up @@ -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"
)
Expand Down
Loading