diff --git a/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_BitMaps.spec b/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_BitMaps.spec index bfd2c30c..ae6ad3cb 100644 --- a/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_BitMaps.spec +++ b/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_BitMaps.spec @@ -1,5 +1,13 @@ -// SG: We cannot use BitMaps.BitMap as a key in a ghost mapping. -// Solution: reroute to OZ_BitMaps.sol, add it to scene, and summarize its methods. +// BitMaps.BitMap cannot be a ghost mapping key, so the library's calls are rerouted to +// OZ_BitMaps (added to the scene alongside this spec) and the ghost is keyed on the storage +// slot instead. The reroute host is generated per project from OZ_BitMaps.template.sol, +// because its parameter type has to come from the project's own BitMaps.sol. +// +// The model replaces the BitMap's storage with a ghost and nothing ties the two together: +// reading bitmap._data directly, deleting the struct, a raw sstore, or copying the struct all +// diverge from it silently. The slot key is also only as sound as distinct BitMaps having +// distinct slots — true for a plain field, but a BitMap reached through a mapping has a +// hashed pointer, so a collision would alias two of them. methods { // rerouting function BitMaps.get(BitMaps.BitMap storage bitmap, uint256 index) internal returns bool => @@ -16,16 +24,16 @@ methods { // actual summaries function OZ_BitMaps.get(uint256 bitmap, uint256 index) internal returns bool => - ghost_bitmap_get[currentContract][bitmap][index]; + ghost_bitmap_get[calledContract][bitmap][index]; function OZ_BitMaps.set(uint256 bitmap, uint256 index) internal => - ghost_bitmap_set(currentContract, bitmap, index); + ghost_bitmap_set(calledContract, bitmap, index); function OZ_BitMaps.unset(uint256 bitmap, uint256 index) internal => - ghost_bitmap_unset(currentContract, bitmap, index); + ghost_bitmap_unset(calledContract, bitmap, index); function OZ_BitMaps.setTo(uint256 bitmap, uint256 index, bool value) internal => - ghost_bitmap_setTo(currentContract, bitmap, index, value); + ghost_bitmap_setTo(calledContract, bitmap, index, value); } // Ghost variable to track bitmap state per contract and index diff --git a/certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol b/certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol deleted file mode 100644 index afe9e898..00000000 --- a/certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol +++ /dev/null @@ -1,43 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.20; - -library OZ_BitMaps { - struct BitMap { - mapping(uint256 bucket => uint256) _data; - } - - function get(BitMap storage bitmap, uint256 index) internal view returns (bool) { - return get(slotOf(bitmap), index); - } - function get(uint256 bitmap, uint256 index) internal view returns (bool) { - require(false); // placeholder to trigger sanity failure if summarization fails; - return false; - } - - function setTo(BitMap storage bitmap, uint256 index, bool value) internal { - setTo(slotOf(bitmap), index, value); - } - function setTo(uint256 bitmap, uint256 index, bool value) internal { - require(false); // placeholder to trigger sanity failure if summarization fails; - } - - function set(BitMap storage bitmap, uint256 index) internal { - set(slotOf(bitmap), index); - } - function set(uint256 bitmap, uint256 index) internal { - require(false); // placeholder to trigger sanity failure if summarization fails; - } - - function unset(BitMap storage bitmap, uint256 index) internal { - unset(slotOf(bitmap), index); - } - function unset(uint256 bitmap, uint256 index) internal { - require(false); // placeholder to trigger sanity failure if summarization fails; - } - - function slotOf(BitMap storage bitmap) internal pure returns (uint256 ret) { - assembly { - ret := bitmap.slot - } - } -} diff --git a/certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.template.sol b/certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.template.sol new file mode 100644 index 00000000..7616c5dd --- /dev/null +++ b/certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.template.sol @@ -0,0 +1,60 @@ +// SPDX-License-Identifier: MIT +$PRAGMA$ + +// BitMaps.BitMap cannot be a ghost mapping key, so OZ_BitMaps.spec reroutes the library's +// calls here and summarizes these functions instead, keying the ghost on the storage slot. +// +// The import is what makes the reroute resolve. A reroute host's parameter must carry the +// same canonicalId as the summarized function's, and canonicalId is +// "|" — so BitMaps.BitMap has to come +// from the very BitMaps.sol the project compiles. A copy of the struct is a different type, +// however identical it looks. That path differs per project, which is why this is a template. +import {BitMaps} from "$BITMAPS_IMPORT$"; + +library OZ_BitMaps { + // Reroute targets, and external for a reason: the Prover keeps a candidate only when its + // evmExternalMethodInfo reports a library function, and that is populated for EXTERNAL + // visibility alone. External is also the only place a storage parameter can be bound. + function get(BitMaps.BitMap storage bitmap, uint256 index) external view returns (bool) { + return get(slotOf(bitmap), index); + } + + function set(BitMaps.BitMap storage bitmap, uint256 index) external { + set(slotOf(bitmap), index); + } + + function unset(BitMaps.BitMap storage bitmap, uint256 index) external { + unset(slotOf(bitmap), index); + } + + function setTo(BitMaps.BitMap storage bitmap, uint256 index, bool value) external { + setTo(slotOf(bitmap), index, value); + } + + // The summarized functions. CVL replaces each body with a ghost read or write, so what is + // written here only runs if a summary failed to attach. + // + // These were `require(false)` tripwires, meant to make that failure loud. They made it + // certain instead: a body that unconditionally reverts leaves nothing for the summary to + // attach to, so every call reverted and every rule over it passed vacuously. The tripwire + // caused the failure it was meant to announce. + // + // Neutral bodies invert that. An unattached summary now means `set` stores nothing and + // `get` reads false, so a rule that sets a bit and reads it back fails outright. A + // violated rule is a far better failure than a green vacuous one, and `rule_sanity` + // catches what is left. + function get(uint256 bitmap, uint256 index) internal view returns (bool) { + return false; + } + + function set(uint256 bitmap, uint256 index) internal {} + + function unset(uint256 bitmap, uint256 index) internal {} + + function setTo(uint256 bitmap, uint256 index, bool value) internal {} + + // The ghost is keyed on the slot, which is what stands in for the BitMap identity. + function slotOf(BitMaps.BitMap storage bitmap) internal pure returns (uint256 ret) { + assembly { ret := bitmap.slot } + } +} diff --git a/certora_autosetup/setup/function_summaries.json b/certora_autosetup/setup/function_summaries.json index 388aed23..a6283324 100644 --- a/certora_autosetup/setup/function_summaries.json +++ b/certora_autosetup/setup/function_summaries.json @@ -105,7 +105,7 @@ "library_names": ["BitMaps"], "summary_file": "specs/summaries/OpenZeppelin/OZ_BitMaps.spec", "description": "OpenZeppelin BitMaps operations", - "additional_contracts": ["specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol"] + "additional_contracts": ["specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.template.sol"] }, "oz_arrays_unsafeMemoryAccess": { "names": ["unsafeMemoryAccess"], diff --git a/certora_autosetup/setup/setup_summaries.py b/certora_autosetup/setup/setup_summaries.py index 885edcdb..5f4e2745 100755 --- a/certora_autosetup/setup/setup_summaries.py +++ b/certora_autosetup/setup/setup_summaries.py @@ -52,12 +52,14 @@ is_local_backend, ) -from certora_autosetup.setup.solidity_utils import DEPENDENCIES, find_all_library_files as util_find_all_library_files +from certora_autosetup.setup.solidity_utils import DEPENDENCIES, find_all_library_files_and_names +from certora_autosetup.setup.solidity_utils import find_all_library_files as util_find_all_library_files from certora_autosetup.setup.solidity_utils import find_all_solidity_files as util_find_all_solidity_files from certora_autosetup.setup.solidity_utils import walk_files_by_suffix # Import method parser from certora_autosetup.parsers.method_parser import MethodParser +from certora_autosetup.utils.solc_version_resolver import read_pragma_from_source_file from certora_autosetup.parsers.spec_imports import parse_imports_from_spec from certora_autosetup.setup.summary_resolver import curated_scene_contracts, resolve_summary_specs from certora_autosetup.setup.signature_types import InheritanceGraph @@ -775,7 +777,7 @@ def copy_summaries_folder(self, matched_function_keys: Iterable[str]) -> Path: copied = 0 for rel in sorted(closure): - # Templates are read from the package source by _materialize_template; + # Spec templates are read from the package source by _materialize_template; # never copy them to the user's dir. if str(rel).endswith(".template.spec"): continue @@ -785,12 +787,97 @@ def copy_summaries_folder(self, matched_function_keys: Iterable[str]) -> Path: self.log(f"Bundled summary file missing: {src}", "WARNING") continue dst.parent.mkdir(parents=True, exist_ok=True) - shutil.copyfile(src, dst) + if str(rel).endswith(".template.sol"): + # A companion contract the summary reroutes through cannot be shipped ready to + # use: its parameter types have to come from the project's own copy of the + # library, so the import is filled in here. + if not self._materialize_companion(rel, src, self._untemplated(dst)): + continue + else: + shutil.copyfile(src, dst) copied += 1 self.log(f"Copied {copied} curated summary file(s) to {target_summaries}") return target_summaries + @staticmethod + def _untemplated(path: Path) -> Path: + """``X.template.sol`` -> ``X.sol``; anything else unchanged. + + Deliberately not ``_versioned_template_relpath``: that one is ``.spec``-shaped and + appends the main contract's name, while a companion's content depends only on the + project, so two main contracts in one project share a single companion. + """ + name = path.name + return path.with_name(name.replace(".template.", ".", 1)) if ".template." in name else path + + def _library_for_companion(self, rel: Path) -> Optional[str]: + """The library name a companion template belongs to, from the registry. + + Read from the entry that declares the companion rather than parsed out of its + filename, so the two cannot drift apart. + """ + wanted = (SUMMARIES_SUBDIR / rel).as_posix() + for info in self.function_summaries.values(): + if wanted in info.get("additional_contracts", []): + names = info.get("library_names") or [] + return names[0] if names else None + return None + + def _project_library_file(self, library_name: str) -> Optional[Path]: + """The project's own file declaring ``library ``.""" + found = find_all_library_files_and_names( + include_test_files=False, include_dependencies=True, log_func=self.log + ) + for file_path, names in found.items(): + if library_name in names: + return Path(file_path) + return None + + def _materialize_companion(self, rel: Path, template: Path, destination: Path) -> bool: + """Fill a companion template in from the project and write it. False if we cannot. + + Returns False rather than raising so the caller can drop the key: a summary whose + companion never materialized is worse than no summary, because the reroute would send + the library's calls to a contract that is not in the scene. + """ + library_name = self._library_for_companion(rel) + if library_name is None: + self.log(f"No registry entry claims companion {rel}", "WARNING") + return False + + library_file = self._project_library_file(library_name) + if library_file is None: + self.log( + f"Cannot generate {destination.name}: the project has no library " + f"{library_name} to take its types from", + "WARNING", + ) + return False + + # The library's own spec, so the companion can never fall outside the range the + # library itself compiles under. + pragma_spec = read_pragma_from_source_file(library_file, Path.cwd()) + if not pragma_spec: + self.log( + f"Cannot generate {destination.name}: {library_file} declares no pragma", + "WARNING", + ) + return False + + # Relative, because the emitted file sits under certora/ while the library can be + # anywhere; an absolute path would also bake the build machine's layout into a source + # file that gets uploaded with the run. + import_path = os.path.relpath(library_file.resolve(), destination.parent.resolve()) + content = ( + template.read_text() + .replace("$PRAGMA$", f"pragma solidity {pragma_spec};") + .replace("$BITMAPS_IMPORT$", import_path) + ) + destination.write_text(content) + self.log(f"Generated {destination.name} against {library_file}") + return True + def process_template_in_place( self, template_file: Path, @@ -1022,7 +1109,13 @@ def _add(p: Path) -> None: # Then any other emitted spec (LLM per-contract, call resolution) — lower dedup precedence. for spec in walk_files_by_suffix(self.user_summaries_dir, ".spec"): _add(spec) - resolve_summary_specs(ordered_specs, PATH_ALL_METHODS_JSON, log=self.log) + # The companions are in the conf but not in the index, which is built from the + # project's own compilation; without this their summaries would be pruned as out of + # scene and the reroute would land on the companion's unsummarized bodies. + companions = {entry.split(":")[-1] for entry in self.curated_scene_contracts()} + resolve_summary_specs( + ordered_specs, PATH_ALL_METHODS_JSON, exempt_receivers=companions, log=self.log + ) def should_process_file(self, file_path: str) -> bool: """Check if a file should be processed (not a dependency or internal file). diff --git a/certora_autosetup/setup/summary_resolver.py b/certora_autosetup/setup/summary_resolver.py index bcc86c8a..6b3dd2b5 100644 --- a/certora_autosetup/setup/summary_resolver.py +++ b/certora_autosetup/setup/summary_resolver.py @@ -36,7 +36,7 @@ import subprocess from dataclasses import dataclass from pathlib import Path -from typing import Any, Callable, Dict, Iterable, List, Optional, Sequence, Set, Tuple +from typing import AbstractSet, Any, Callable, Dict, Iterable, List, Optional, Sequence, Set, Tuple from certora_cli.Shared.certoraUtils import find_jar @@ -289,7 +289,9 @@ def overloads(self, receiver: str, name: str) -> List[Tuple[str, ...]]: return self._overloads.get((receiver, name), []) -def entry_resolves(index: MethodIndex, entry: MethodEntry) -> bool: +def entry_resolves( + index: MethodIndex, entry: MethodEntry, exempt_receivers: AbstractSet[str] = frozenset() +) -> bool: """Decide whether a summary entry resolves in the scene (drop-only policy). The decision is based on ``(receiver, name, arity)`` only — DROP iff the method @@ -302,6 +304,12 @@ def entry_resolves(index: MethodIndex, entry: MethodEntry) -> bool: name / wrong arity) and is robust across both sources. A same-arity-but-different- type phantom overload, if it ever occurs, is left to the TypecheckerLoop backstop. """ + # A companion contract joins the conf after the project was built, so it cannot appear in + # an index derived from that build. Pruning its entries would leave the reroute pointing + # at an unsummarized companion whose bodies revert, which reads as a passing run. + if entry.receiver in exempt_receivers: + return True + # KEEP iff some overload of this name at this receiver has the entry's arity. # An empty overload list means the name is absent at the receiver (e.g. solady # ``mulDiv`` on solmate ``FixedPointMathLib``) → DROP. @@ -339,6 +347,7 @@ def resolve_spec_file( spec_path: Path, index: MethodIndex, owned_keys: Optional[Set[Tuple[str, str, Tuple[str, ...]]]] = None, + exempt_receivers: AbstractSet[str] = frozenset(), log: Optional[LogFn] = None, ) -> List[Tuple[str, str, Tuple[str, ...]]]: """Prune unresolvable internal-method entries in a single summary spec, in place. @@ -349,6 +358,8 @@ def resolve_spec_file( owned_keys: ``(receiver, name, param_types)`` keys already claimed by a higher-precedence spec. Entries matching one of these are dropped as duplicates (the dedup safeguard); ``None`` disables dedup. + exempt_receivers: Receivers the index cannot know about — companion contracts + added to the conf after the build the index came from. log: Optional ``(message, level)`` logger. Returns: @@ -366,7 +377,7 @@ def resolve_spec_file( # Disable entries from the bottom up so earlier entries' positions stay valid after # later ones are edited. for entry in sorted(entries, key=lambda e: (e.start_line, e.start_col), reverse=True): - if not entry_resolves(index, entry): + if not entry_resolves(index, entry, exempt_receivers): _disable_entry(lines, entry, f"not in scene at {entry.receiver}") dropped_missing += 1 elif owned_keys is not None and entry.key in owned_keys: @@ -389,6 +400,7 @@ def resolve_spec_file( def resolve_summary_specs( ordered_spec_files: Sequence[Path], all_methods_path: Path, + exempt_receivers: AbstractSet[str] = frozenset(), log: Optional[LogFn] = None, ) -> None: """Run the prune-pass over a precedence-ordered list of emitted summary specs. @@ -396,14 +408,16 @@ def resolve_summary_specs( Files earlier in ``ordered_spec_files`` win duplicate ownership: a ``(receiver, name, param_types)`` kept by an earlier file is dropped from later files. Non-existent / wrong-receiver entries are dropped from every file regardless of - order. + order, except at ``exempt_receivers`` — contracts the index cannot know about. """ index = MethodIndex.from_file(all_methods_path) owned: Set[Tuple[str, str, Tuple[str, ...]]] = set() for spec_path in ordered_spec_files: if not spec_path.exists(): continue - kept = resolve_spec_file(spec_path, index, owned_keys=owned, log=log) + kept = resolve_spec_file( + spec_path, index, owned_keys=owned, exempt_receivers=exempt_receivers, log=log + ) owned.update(kept) @@ -430,12 +444,24 @@ def curated_scene_contracts( if not info: continue for ac in info.get("additional_contracts", []): - path = user_summaries_dir / Path(ac).relative_to(SUMMARIES_SUBDIR) + # A companion shipped as a template is emitted under its untemplated name, since + # what reaches the conf is the filled-in file, not the template. + rel = Path(ac).relative_to(SUMMARIES_SUBDIR) + if ".template." in rel.name: + rel = rel.with_name(rel.name.replace(".template.", ".", 1)) + path = user_summaries_dir / rel if not path.is_file(): log(f"Curated companion contract not copied: {path}", "WARNING") continue + # Relative to the project root, like every other entry in a conf: an absolute + # path here would bake the build machine's layout into a conf that travels with + # the run. + try: + conf_path = path.resolve().relative_to(Path.cwd().resolve()) + except ValueError: + conf_path = path entries.extend( - f"{path.as_posix()}:{name}" + f"{conf_path.as_posix()}:{name}" for name in extract_definitions_from_solidity(str(path)) ) return entries diff --git a/certora_autosetup/utils/enhanced_config_manager.py b/certora_autosetup/utils/enhanced_config_manager.py index 06b7aae6..2927f8c4 100644 --- a/certora_autosetup/utils/enhanced_config_manager.py +++ b/certora_autosetup/utils/enhanced_config_manager.py @@ -260,6 +260,17 @@ def create_config( parsed_args[normalized_key] = arg_value conf_template["prover_args"] = self._build_prover_args_list(parsed_args) + # A file in `files` with no compiler_map entry makes certoraRun reject the conf as + # "not matched in compiler_map". The scene contracts come with their entries from the + # build-system properties above; the additional ones are added here and have none, so + # they get the same per-contract resolution add_files_to_config gives them. + if any(key.endswith("_map") for key in conf_template): + for handle in parse_contract_files(additional_files): + self.update_compiler_map_for_contract(conf_template, handle, self.reference_compiler_maps or None) + self.update_via_ir_map_for_contract(conf_template, handle, self.reference_compiler_maps or None) + self.update_optimize_map_for_contract(conf_template, handle, self.reference_compiler_maps or None) + self.update_evm_version_map_for_contract(conf_template, handle, self.reference_compiler_maps or None) + # Write configuration file if not conf_path: raise ValueError("conf_path is required; ConfigManager no longer defaults a conf output path")