Add pure expression inliner infrastructure for quantifier bodies#4567
Open
feliperodri wants to merge 6 commits intomodel-checking:mainfrom
Open
Add pure expression inliner infrastructure for quantifier bodies#4567feliperodri wants to merge 6 commits intomodel-checking:mainfrom
feliperodri wants to merge 6 commits intomodel-checking:mainfrom
Conversation
github-actions
bot
added
Z-EndToEndBenchCI
Add Expr::substitute_symbol() and inline_as_pure_expr() for inlining function calls as side-effect-free expression trees. This infrastructure is needed to generate CBMC quantifier bodies without StatementExpression nodes, which will enable nested quantifier support. Changes: - cprover_bindings: Expr::substitute_symbol() — recursive symbol replacement across all ExprValue variants, with 6 unit tests - goto_ctx.rs: inline_as_pure_expr() — inlines function calls by extracting return expressions, resolving intermediate variables, and substituting parameters. Handles StatementExpression flattening for checked arithmetic (drops Assert/Assume runtime checks). - docs/dev/pure-expression-inliner.md — developer documentation including soundness implications Soundness note: The pure inliner drops overflow and division-by-zero checks when flattening StatementExpression nodes from checked arithmetic. This is a known trade-off — CBMC requires pure expressions in quantifier bodies, and runtime checks are side effects. The existing handle_quantifiers post-pass is NOT modified — this is purely additive infrastructure. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
- substitute_symbol returns (Expr, bool) for reliable change detection instead of Debug-format string comparison - Graceful fallback for recursive functions (tracing::warn + return original) instead of assert! panic - Diagnostics for edge cases: multiple assignments to same variable, non-symbol return expressions, unknown UnaryOperator variants - Public API cleanup: inline_as_pure_expr_toplevel wrapper hides the visited set implementation detail - Document StatementExpression non-recursion in substitute_symbol Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
feliperodri
force-pushed
the
inline-pure-expressions
branch
from
0fcc5c3 to
8b2600a
Compare
feliperodri
commented
Mar 30, 2026
Comment on lines
+10
to
+20
| ## Soundness Implications | ||
|
|
||
| **Checked arithmetic in quantifier bodies**: When flattening `StatementExpression` | ||
| nodes (e.g., from checked division or remainder), the pure inliner drops the | ||
| `Assert` and `Assume` statements that check for overflow and division by zero. | ||
|
|
||
| - **Division by zero** inside a quantifier body will NOT be detected. | ||
| - **Arithmetic overflow** inside a quantifier body will NOT be detected. | ||
|
|
||
| **Future improvement**: The dropped assertions could be hoisted outside the | ||
| quantifier as preconditions, preserving soundness while keeping the body pure. |
Contributor
Author
There was a problem hiding this comment.
@tautschnig this is similar to CBMC behavior, correct? Let me know if this raises any concerns.
- Replace destructuring assignment with .0 for substitute_symbol calls - Restore step-by-step 'How It Works' section in dev documentation Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
feliperodri
added
[C] Internal
Contributor
|
Could you please add some document to explain why this transformation preserves the semantic of Rust (for the return values of functions), especially for the case the code contains aliasing, memory reference ...? |
Explain why the substitution-based transformation preserves Rust semantics for function return values, covering: - Straight-line code (SSA-form algebraic substitution) - Aliasing and memory references (symbol substitution preserves dereferences; CBMC evaluates them with full alias analysis) - When the transformation is NOT safe (multi-assignment locals, side effects between assignments, mutable aliasing) - Scope of applicability (quantifier closures are pure single- expression functions where substitution equals beta-reduction) Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Contributor
Author
|
@thanhnguyen-aws I added a section in the docs/dev/pure-expression-inliner.md doc to document why this transformation preserves the semantic of Rust. Could you take another look? |
Ari4ka
approved these changes
Apr 8, 2026
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
3 participants
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.
What
Adds
Expr::substitute_symbol()andinline_as_pure_expr()— infrastructure for inlining function calls as side-effect-free expression trees. This is a prerequisite for generating CBMC quantifier bodies withoutStatementExpressionnodes, which will enable nested quantifier support.Why
CBMC rejects side effects inside quantifier expressions (
forall/exists). Today, Kani'shandle_quantifierspost-pass inlines function calls intoStatementExpressionnodes, which CBMC accepts viaconvert_statement_expression, but this breaks for nested quantifiers (inner quantifiers are treated as side effects, causing a CBMC invariant violation crash).The pure expression inliner resolves this by producing expression trees that contain no statements, no gotos, and no labels; only pure expressions that CBMC can handle directly, including in nested contexts.
How
Expr::substitute_symbol()(cprover_bindings/src/goto_program/expr.rs)inline_as_pure_expr()(kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs)StatementExpressionnodes (e.g., checked arithmetic).Soundness note
When flattening
StatementExpressionnodes from checked arithmetic (e.g., %, +), the inliner drops Assert/Assume statements that check for overflow and division by zero. This is a known trade-off documented in docs/dev/pure-expression-inliner.md: CBMC requires pure expressions in quantifier bodies, and runtime checks are inherently side effects. A future improvement could hoist these checks outside the quantifier as preconditions.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.