autosetup: apply all applicable compilation workarounds per retry, stop no-op retry loops by shellygr · Pull Request #66 · Certora/AutoProver

shellygr · 2026-07-10T20:24:28Z

This PR collects a bunch of problems that were encountered in many setups. It was validated against a set of about 80 projects with no regressions.

idempotency of certain compilation workarounds means we run workarounds and test them to no effect (e.g. warnings handlings)
Collect all applicable workarounds from the output
Support certora-cli 8.17.1 and enum ambiguity focused on Math.Rounding including tests
Option to stop after compilation analysis for testing
Make sure we do not invoke solc version which isn't installed
More precise detection of 'stack too deep' errors

A workaround whose detect_fn keeps matching unchanged compiler output was re-applied as a no-op on every retry until max_retries. Observed in the wild as hundreds of consecutive unnamed_return_warning applications (hours of full certoraRun recompiles) while the run's real fatal error went unhandled: the flag check lived in the once-evaluated `enabled` field, but the warning text keeps appearing in the output after the flag is set, so it re-fired forever. - unnamed_return_warning: check ignore_solidity_warnings inside detect_fn against the live conf so the workaround self-disables after applying. - Add two generic no-progress guards to the retry loop (same pattern as the existing _harnessed_libs guard): disable a workaround when it detects the exact result it already fixed, or when its application leaves the conf and command unchanged, and fall through to lower-priority workarounds in the same pass instead of recompiling. Loop-level tests pin the exact number of certoraRun invocations for the persistent-warning, repeated-detect, and no-op-apply scenarios, plus one asserting the repeat guard stays quiet while detect results differ (so per-contract iterative fixes like via-ir keep working). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ling Rework of the previous commit per review: disabling a workaround for the rest of the run was wrong — it can legitimately become applicable again later (a different contract, state changed by another workaround). New retry-loop shape: each failed compilation gets one pass in which EVERY workaround whose detect fires on that output is applied (priority order = application order) before the single recompile; a pass that leaves the conf and command unchanged ends the loop, since recompiling would reproduce the identical failure. No workaround is ever disabled. - cached_autofinder_failure is exclusive: the cached error hides the real one, so its pass applies only it and recompiles. - use_relpaths_for_solc_json is last_resort: only tried when nothing else applied in the pass. - The yul_exception teardown must not fire in a pass that just added the optimizer or wrote via-ir map entries — each escalation rung gets its own validating recompile. - Via-ir fixes landing after the teardown popped solc_via_ir_map re-seed the full all-off map first, so a partial single-entry map cannot collapse into a global solc_via_ir=true at finalize. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

The OZ Math mulDiv summary assumed a single Math.Rounding definition and looked its members up only in the verified main contract's import closure: additional/linked contracts bringing Math were missed, an unrelated Rounding enum could steer the choice, and a scene mixing OZ v4 ({Down,Up,Zero}) and v5 ({Floor,Ceil,Trunc,Expand}) left an ambiguous `Math.Rounding` that the typechecker fixer "fixed" by commenting out hardcoded line numbers. - Scene-wide classification (setup_summaries): all Math-declared Rounding definitions are gathered from all_user_defined_types.json (rows now carry the declaring sourceFile), restricted to definitions actually visible from the scene, and classified none/single/mixed. - The OZ_Math spec is rendered programmatically. Single-definition scenes keep the legacy `Math.`-receiver shape with the right member (Up for v4, Ceil for v5); no-directional scenes simply omit the 4-arg entry. Mixed scenes emit wildcard receivers with one directional summary per definition, each qualified by a scene contract importing only that definition (`HarnessV5.Rounding.Ceil` — certora-cli >= 8.17.1 type disambiguation). The on-disk template is now an import stub keeping Math.spec in the copy closure. - Typechecker fixer: both 8.17.1 error variants ("Type X.Rounding is not a valid type" on CVL function lines, "X.Rounding is not a valid EVM type" on methods entries, in either direction) are parsed with their "Did you mean" suggestions, and the referenced enum is requalified by the suggestion whose definition contains the referenced member, instead of being disabled. The comment-out fallback survives, targeted at reported lines and expanded to whole top-level CVL function blocks (any name) so it never emits half-commented functions. - certora-cli floors bumped to >=8.17.1 (uv.lock regenerated); integration workflow timeout raised for the new tests. Tests: three fixture projects vendoring verbatim OZ v4.9.6 / v5.0.2 Math.sol (v4-only, v5-only, mixed across two harnesses in one scene) run the full non-LLM autosetup pipeline as expensive tests, asserting the materialized spec content and a clean independent certoraRun --compilation_steps_only. Cheap unit tests cover classification (incl. scene-invisible-definition and non-Math-enum regressions), all four rendered shapes, both error-text variants, requalification in both directions, and the block expansion. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Stops right after the compilation-analysis phase succeeds, before summaries and anything cloud-facing — for large-scale compile sweeps that only need to know whether compilation analysis passes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…est release resolve_pragma_to_version picked the highest matching version from soliditylang.org's online list, unconstrained by the environment: the day a new solc ships, every floating-pragma consumer (e.g. the generated DummyERC20Impl mock with ^0.8.0) resolves to a compiler that either is not installed or is not yet supported by the prover toolchain's per-version tables. Prefer the highest matching version whose binary is actually on PATH (Certora or solc-select naming); fall back to the listed highest when none is installed (environments that fetch compilers on demand). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Some solc via-ir emissions never contain the "Stack too deep" phrase — "YulException: Variable _7 is 1 too deep in the stack [ ... ] memoryguard was present." — so the yul escalation ladder (add optimizer, then the teardown) was never tried for them and compilation analysis gave up on an error the ladder can plausibly fix. Match the "too deep in(side) the stack" wording too: the semantics, not one spelling. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shellygr · 2026-07-13T09:15:01Z

+    """Whether a solc binary providing `version` is on PATH, under either the
+    Certora naming convention ("solc8.35") or solc-select's ("solc-0.8.35")."""
+    names = [f"solc-{version}"]
+    if version.startswith("0."):


you assume it's true here. otherwise it's going to be just certora naming convention in all cases. so write what you expect to get as version string. we have utility functions for converting version names already so no need to reinvent the wheel

Claude answers: fixed in 1009945 — the probe now documents its input contract (raw semver exactly as listed by fetch_available_solc_versions) and builds the Certora spelling via the shared convert_solc_version_to_certora_format instead of the hand-rolled slice. (format_solc_version in enhanced_config_manager would be the fuller utility, but enhanced_config_manager imports from this module, so the leaf converter avoids the cycle.)

… probe Review nit: _solc_binary_installed hand-rolled the raw-version -> Certora binary-name conversion behind a startswith("0.") guess. Document the expected input (raw semver as listed by fetch_available_solc_versions) and build the Certora spelling via convert_solc_version_to_certora_format instead. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

jar-ben · 2026-07-13T07:44:29Z

@@ -1,19 +1,7 @@
+// Stub: the OZ Math summary spec is rendered programmatically by
+// SummarySetup._render_oz_math_spec (setup_summaries.py) because its content


The .spec comments/files should not talk about the python code/autosetup that generates them.

jar-ben · 2026-07-13T08:06:00Z


                                # Add to collection if we found a valid type
                                if type_name and qualified_name:
+                                    # canonicalId is "path/File.sol|Qualified.Name"; the


I don't think we need this comment here (we don't have such comments for the other fields we store). It looks like Claude explaining why the code is being added.

Also, why don't we just store the canonicalId instead of parsing the source file from it? Do we actually need the source file anywhere?

When you have Math.Rounding declared inside another file that imports some Math, we have to parse out the source file.

turns out we get in another way from the ast, so did a deeper change for using the canonicalId for the grouping only

jar-ben · 2026-07-13T08:11:16Z

+SCENE_SENSITIVE_TEMPLATE_KEYS: FrozenSet[str] = frozenset({"oz_Math_mulDiv"})
+
+
+@dataclass(frozen=True)


Do these rounding specific classes really belong to the general setup_summaries infra file?

jar-ben · 2026-07-13T08:15:20Z

+        return names
+
+    @staticmethod
+    def _round_up_member(members: FrozenSet[str]) -> Optional[str]:


Same comment as above - I would not expect to see rounding specific functionality in the general setup_summaries.py infra.

But I see this is a pre-existing issue...

jar-ben · 2026-07-13T08:18:30Z

+        every reference must be qualified by a contract that imports exactly one
+        definition (``C.Rounding``, certora-cli >= 8.17.1).
        """
+        user_types_file = Path(".certora_internal/all_user_defined_types.json")


Can we use a shared constant for this? don't hardcode the filepath here

jar-ben · 2026-07-13T09:07:21Z

+        # new solc ships. Fall back to the listed highest when no matching
+        # binary is installed (environments that fetch compilers on demand).
+        installed_versions = [v for v in matching_versions if _solc_binary_installed(v)]
+        pool = installed_versions or matching_versions


Can you update the docs of resolve_pragma_to_version (to say we prioritise installed solc versions)?

jar-ben · 2026-07-13T09:09:15Z

        matches.extend(external_matches)

-        # Pattern 2: Math.Rounding enum type errors
+        # Pattern 2b: ambiguous/unresolvable Rounding type with suggestions


where is the pattern 2a?

jar-ben · 2026-07-13T09:44:53Z

+        Rounding definition (that is why the prover suggests it), so its rows
+        identify which definition — and which round-up member — it stands for."""
+        result: Dict[str, set] = {q: set() for q in qualifiers}
+        types_path = Path(".certora_internal/all_user_defined_types.json")


use a constant

jar-ben · 2026-07-13T09:50:02Z

        return False

+    @staticmethod
+    def _expand_to_function_blocks(lines: List[str], reported: set) -> set:


Can we get this from the CVL AST instead of custom string parsing?

jar-ben · 2026-07-13T13:42:52Z

+                if workaround.name == "cached_autofinder_failure" and "--build_cache" in cmd:
+                    cmd.remove("--build_cache")
+                applied_this_pass.add(workaround.name)
+                if workaround.exclusive:


In the current code, it is exclusive only if no workarounds triggered before, i.e. the order matters. Currently, cached_autofinder_failure is the only exclusive workaround and it is first in the workarounds list, so the exclusivity is enforced, but if it would not be first, it's no longer guaranteed to be exclusive.

I would expect either a different naming (to allow non-exclusivity) or enforcing the exclusivity.

- Move all Math.Rounding handling out of setup_summaries.py/typechecker_loop.py into a dedicated setup/oz_math_rounding.py module (classification, spec rendering, per-qualifier member lookup); _materialize_template keeps a single dispatch line. - A broken/unreadable types inventory no longer raises out of the classifier: it degrades to the no-directional-summary spec instead of killing the run. - Shared constants for .certora_internal/all_user_defined_types.json (FILE_/PATH_ALL_USER_DEFINED_TYPES_JSON) replace every hardcoded literal, mirroring the ALL_METHODS precedent; type_analyzer joins the FILE_ constant. - Store the type's canonicalId verbatim instead of parsing a source file out of it — grouping/sorting/logging need only a per-definition key, which the canonicalId already is. - Drop the pre-8.17.1 "is not a valid enum type" parsing and its comment-out fix entirely: certora-cli floors are >= 8.17.1, so the suggestions-carrying error is the only Rounding error the loop can see. - Block expansion for the requalify fallback now comes from the CVL AST (ASTExtraction syntax-check emits top-level function definitions under ast["subs"] with 0-based ranges) via a new summary_resolver.extract_cvl_ast helper, replacing the string-walking heuristic. - Exclusive workarounds are structurally evaluated before all others, making exclusivity independent of list order. - The bundled OZ_Math template stub and resolve_pragma_to_version docs now describe behavior without narrating implementation internals. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Test-file conflict: both sides appended new test sections at the same spot — kept both (this branch's retry-loop tests and master's wrapped source-not-found detector tests). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…tions Caught by the corpus re-sweep: broadening the YulException detector (the memoryguard wording) made it match exceptions raised while GENERATING AUTOFINDERS — which are non-fatal (the prover falls back to the original file). On a project whose foundry config supplies both via-ir and the optimizer, that routed pass 1 straight into the teardown, stripping via-ir the source actually requires ("Require with a custom error is only available using the via-ir pipeline") and killing a previously-passing run. Skip YulException matches whose preceding "had an error:" line carries the "Encountered an exception generating autofinder" marker; genuine fatal YulExceptions elsewhere in the same output still fire. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ettings Correcting the previous commit's direction after review: autofinder YulExceptions ARE the ladder's business — the prover falls back to the original file and silently loses its internal summaries, and succeeding WITH autofinders is the goal (via-ir, then the optimizer, try to make them compile). What broke the previously-passing project was not the detection but the last resort stripping via-ir/optimizer wholesale: when the project's own build config mandates via-ir, the source does not compile on the legacy pipeline at all. The last resort now gives up only autofinders and keeps the compile settings; the teardown no longer touches the via-ir map, so the requalify-era re-seed guard and the map-writers clause of the escalation guard are gone with it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Contracts start on plain settings and gain via-ir/optimizer strictly when compilation needs them. Stack-too-deep was the only necessity signal; solc features that exist only on the via-ir pipeline (e.g. "UnimplementedFeatureError: Require with a custom error is only available using the via-ir pipeline") are another — add a workaround that enables via-ir for the affected contract on that signal, whitespace-normalized per compiled unit since solc hard-wraps the phrase. Also reword the yul last resort's rationale to the necessity model. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

It stops asserting autofinder success — autofinders are still generated per file, and only files whose instrumentation fails fall back un-instrumented. Wording only. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

jar-ben

looks ok, thank you for the changes. Leaving just a few minor comments

jar-ben · 2026-07-13T19:18:08Z

+def _load_math_rounding_rows(log: LogFn) -> List[Dict]:
+    """Rounding-enum rows declared inside a ``Math`` library, from the
+    compiled-scene type inventory. Any read failure degrades to an empty list
+    (=> "none" classification, no directional summary) rather than aborting


rather than aborting the whole setup. can be dropped

jar-ben · 2026-07-13T19:27:17Z

+            # there and nothing else may act on it.
+            for workaround in workarounds:
+                if workaround.exclusive and workaround.enabled:
+                    detect_result = workaround.detect_fn(output)


[nit] the three lines can go to a helper function, because you use it also below.

detect_result = workaround.detect_fn(output) if detect_result is not None apply_workaround(workaround, detect_result)

with a boolean return value saying if the workaround was actually applied or not (so that you can trigger the break)

jar-ben · 2026-07-13T19:29:16Z

+
+        for line in output.split("\n"):
+            path = _path_from_compiling_line(line)
+            if path is not None and "to expose internal function information" not in line:


can you comment on when "to expose internal function information" appear / what are the implications?

it's matching on the certora-cli output in a very clunky way

…cstring Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shellygr commented Jul 10, 2026

View reviewed changes

Comment thread certora_autosetup/utils/compilation_workarounds.py Outdated

Apply suggestion from @shellygr

caac4fb

shellygr added the autosetup label Jul 11, 2026

shellygr changed the title ~~autosetup: break no-op compilation-workaround retry loops~~ autosetup: apply all applicable compilation workarounds per retry, stop no-op retry loops Jul 11, 2026

shellygr and others added 4 commits July 11, 2026 21:37

shellygr commented Jul 13, 2026

View reviewed changes

jar-ben requested changes Jul 13, 2026

View reviewed changes

shellygr and others added 2 commits July 13, 2026 17:40

Merge origin/master into shelly/workaround-self-disable

b280e99

Test-file conflict: both sides appended new test sections at the same spot — kept both (this branch's retry-loop tests and master's wrapped source-not-found detector tests). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shellygr requested a review from jar-ben July 13, 2026 17:47

shellygr and others added 4 commits July 13, 2026 21:29

autosetup: describe the yul last resort accurately

a9059c7

It stops asserting autofinder success — autofinders are still generated per file, and only files whose instrumentation fails fall back un-instrumented. Wording only. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

jar-ben approved these changes Jul 13, 2026

View reviewed changes

autosetup: review nits — fold detect+apply into one helper, trim a do…

58656aa

…cstring Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shellygr merged commit efeb5c8 into master Jul 13, 2026
4 checks passed

shellygr deleted the shelly/workaround-self-disable branch July 13, 2026 20:18

		@@ -1,19 +1,7 @@
		// Stub: the OZ Math summary spec is rendered programmatically by
		// SummarySetup._render_oz_math_spec (setup_summaries.py) because its content

		SCENE_SENSITIVE_TEMPLATE_KEYS: FrozenSet[str] = frozenset({"oz_Math_mulDiv"})


		@dataclass(frozen=True)

Uh oh!

Conversation

shellygr commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jar-ben left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

shellygr commented Jul 10, 2026 •

edited

Loading