autosetup: keep via-ir off contracts whose pinned compiler cannot take its settings - #186
Draft
shellygr wants to merge 1 commit into
Draft
autosetup: keep via-ir off contracts whose pinned compiler cannot take its settings#186shellygr wants to merge 1 commit into
shellygr wants to merge 1 commit into
Conversation
…e its settings A scene can mix compilers through compiler_map, and the via-ir escalation did not look at them. Once a contract is on via-ir with the optimizer enabled, certoraRun also sends settings.optimizer.details, whose "inliner" key solc only learned in 0.8.5. Handing that to an older pinned compiler makes it reject the input outright, so one old contract fails the compile for the entire scene, and no rung recognises the resulting `Unknown key "inliner"` — the loop reaches its catch-all and the run ends with no progress. The escalation now checks each contract's pin before switching it, both when naming a single contract and when going scene-wide, and says which contracts it kept on legacy codegen. Contracts with no pin run on the environment's solc and are unaffected. The floor lives next to VIA_IR_MIN_VERSION, which covers a different thing: 0.7.5 is where solc learned settings.viaIR at all, while 0.8.5 is where it learned the settings we send along with it. Worth noting the other half, which is not in this repo: certora-cli emits the details block with no version guard when via-ir is on, while its own non-via-ir branch does guard exactly this (0.8.5). Guarding there too would make the floor unnecessary here.
Contributor
Author
|
this will likely become obsolete in the next certora-cli version. keeping as draft for now |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A fleet sweep of ~400 projects on current master turned up one regression against the previous
sweep, and this is it: two contracts in one project went from ok to a failed compilation analysis,
at roughly double the runtime.
What happens
The scene mixes compilers through
compiler_map. One contract is pinned to solc 0.8.4; the restare on 0.8.24. Under #180 the stack-too-deep ladder now (a) enables the optimizer globally on its
first rung and (b) takes via-ir scene-wide as soon as the build config declares
via_ir, ratherthan naming contracts one at a time. Neither step consults the per-contract pin.
With via-ir and the optimizer both on for a file, certoraRun emits
settings.optimizer.details = {"inliner": false, "yulDetails": …}. Theinlinerkey exists fromsolc 0.8.5, so the 0.8.4 binary rejects the input:
That fails the compile for the whole scene, not just that contract. No rung matches the text
(
unsupported_solc_via_iris gated on the scalarsolc_via_ir, which is never set when via-irarrived through the map), so the loop falls to its catch-all, the import patcher runs as a last
resort, the compile fails identically, and the run ends as a compilation-analysis failure with the
patch reverted.
The change
_apply_via_ir_workaroundnow checks each contract's pinned compiler before switching it, in boththe single-contract and the scene-wide paths, and logs which contracts it kept on legacy codegen.
Unpinned contracts run on the environment's solc and are unaffected, so the common case does not
change.
The floor is a new
VIA_IR_SETTINGS_MIN_VERSION = 0.8.5next toVIA_IR_MIN_VERSION, which coverssomething else: 0.7.5 is where solc learned
settings.viaIR, 0.8.5 is where it learned the settingswe send with it.
Tests
Two new cases in
tests/test_compilation_workarounds.py, both failing without the change: ascene-wide escalation that must hold back a below-floor contract, and a below-floor contract that
reported the stack-too-deep itself. A third asserts unpinned scenes still go via-ir. 77 pass.
The other half
certora-cli emits the details block with no version guard when via-ir is on, while its own
non-via-ir branch guards exactly this at 0.8.5. Guarding both would make this floor redundant, and
would also cover callers that set via-ir without going through this ladder. That change is not in
this repo.
Draft: #180 is a clear net win in the same sweep (stack-too-deep failures went from 34 to 1), so
this is about paying its edge case, and I would like a second opinion on the floor's placement
before it lands.
🤖 Generated with Claude Code