smt2_solver: iterate over operands in expand_function_applications#9044
Open
tautschnig wants to merge 2 commits into
Open
smt2_solver: iterate over operands in expand_function_applications#9044tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
tautschnig
requested review from
TGWDB,
kroening and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR updates the SMT2 solver’s expand_function_applications() rewrite pass to avoid call-stack overflows on deeply nested expressions produced by the iterative SMT2 parser, by replacing the recursive operand walk with an explicit two-pass iterative traversal.
Changes:
- Replaces recursive descent over
expr.operands()with an iterative worklist + reverse processing to preserve post-order rewrite semantics. - Keeps recursion only for expanding newly inlined user-defined function bodies.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+79
to
+83
| // benchmarks). We do the rewrite in two passes over an explicit stack | ||
| // of exprt pointers: first collect every node in post-order, then | ||
| // process them bottom-up. Each node's operands have already been | ||
| // rewritten by the time we get to it, matching the old recursive | ||
| // semantics. |
Comment on lines
+76
to
+78
| // Post-order walk, but iterative: the recursive form would overflow the | ||
| // call stack on deeply-nested expressions produced by the parser (e.g. | ||
| // chains of thousands of bvand / store operations in SMT-COMP QF_ABV |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9044 +/- ##
========================================
Coverage 80.68% 80.68%
========================================
Files 1714 1714
Lines 189501 189516 +15
Branches 73 73
========================================
+ Hits 152902 152919 +17
+ Misses 36599 36597 -2 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
expand_function_applications() is a post-order rewrite: for every node, first rewrite the operands, then -- if the node is a function_application with a known definition -- substitute it with the (already-rewritten) body. The recursive form overflowed the call stack on deeply-nested inputs produced by the iterative SMT2 parser (e.g. chains of thousands of bvand / store operations), turning into stack overflows in the solver phase for files that the parser now accepts. Use the existing iterative, mutation-safe post-order traversal exprt::visit_post() instead of recursing over the operands by hand. The only residual recursion is on the freshly inlined body of a user-defined function, which is typically shallow; this matches the pre-existing behaviour. No regression test is added here: on this branch the SMT2 parser is itself recursive (expression() -> function_application() -> operands() -> expression()), so a term deep enough to overflow expand_function_applications overflows the parser first, which makes a .smt2 regression test impossible until the iterative parser lands. The end-to-end guard is the deep-nesting .smt2 tests that ship with that parser change; the depth-safety of the traversal this now relies on is covered by a unit test for exprt::visit_post (separate commit). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
visit_post performs an iterative, mutation-safe post-order traversal; several rewrites rely on it precisely to avoid recursing over -- and overflowing the call stack on -- deeply nested expressions. Add a test that builds a chain far deeper than the recursion that overflows the default (~8 MiB) unit-test stack, walks it with visit_post, and checks every node is visited: it completes with the iterative implementation and overflows the stack with a recursive one. The chain is dismantled iteratively before destruction because this branch does not include the depth-safe irept destructor. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
smt2-expand-fn-iterative
branch
from
f2c96c7 to
07f5cba
Compare
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.
expand_function_applications() is a post-order rewrite: for every node, first rewrite the operands, then — if the current node is a function_application with a known definition — substitute it with the (already-rewritten) body. The recursive form overflowed the call stack on deeply-nested inputs produced by the iterative SMT2 parser (e.g. 50k-deep bvand chains in the try5_*.flanagansaxe.smt2 family), which turned into stack overflows in the solver phase for files that the parser now successfully accepts.
Replace the recursion with a two-pass iterative walk:
The only residual recursion is on the inlined body of a user-defined function, which is typically shallow; this matches the pre-existing behaviour.
Regression: bf13.smt2 (the single remaining crash in the QF_ABV run with the iterative parser) now runs into the 2 s solver timeout instead of dumping core. The full QF_ABV sweep (15,148 files, 2 s timeout, 2 GB RLIMIT_AS, 32-way parallel) goes from 1 crash to 0.