Enable constant propagation of WITH, array, and struct expressions#8959
Closed
tautschnig wants to merge 2 commits intodiffblue:developfrom
Closed
Enable constant propagation of WITH, array, and struct expressions#8959tautschnig wants to merge 2 commits intodiffblue:developfrom
tautschnig wants to merge 2 commits intodiffblue:developfrom
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR expands symbolic-execution constant propagation to include WITH expressions and array/struct literals even when they contain non-constant elements, enabling downstream simplifications (notably constant-index access through WITH). It also adds a DFCC regression targeting union/quantifier performance and updates an existing array cell sensitivity regression to reflect the new propagation behaviour.
Changes:
- Allow goto-symex constant propagation of
ID_with,ID_array, andID_structexpressions. - Improve union
byte_extracthandling in field sensitivity for non-constant offsets by rewriting via the widest union component. - Adjust regressions (add DFCC performance test; update
array-cell-sensitivity2expectations) and tweak byte-update bit placement logic.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| src/solvers/flattening/boolbv_byte_update.cpp | Adjusts constant-offset byte-update bit placement for sub-byte updates. |
| src/goto-symex/goto_symex_can_forward_propagate.h | Broadens what symex treats as “constant” for propagation (WITH/array/struct). |
| src/goto-symex/field_sensitivity.cpp | Rewrites union byte_extract with non-constant offsets via widest member to enable better decomposition/encoding. |
| regression/contracts-dfcc/union_quantifier_performance/test.desc | Adds CORE DFCC regression for union+quantifier performance. |
| regression/contracts-dfcc/union_quantifier_performance/no-array-fs.desc | Adds THOROUGH variant without array field sensitivity (documents slower path). |
| regression/contracts-dfcc/union_quantifier_performance/main.c | New DFCC harness program exercising union + quantified postconditions. |
| regression/cbmc/array-cell-sensitivity2/test.desc | Updates expected VCC patterns to account for additional propagation. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
When byte_update writes a sub-byte value (e.g., a 1-bit bitvector)
at a byte-aligned offset, the value must be placed at the high end
of the affected byte, matching the semantics of lower_byte_update
which concatenates {value, remaining_low_bits}.
The boolbv convert_byte_update was placing the value at bit 0 (the
low end) instead. For little-endian, this means the value was
written to the LSB instead of the MSB of the byte. For big-endian,
the endianness map already reverses bits so that bit 0 maps to the
MSB, making the existing code accidentally correct.
Generalise the fix to handle any non-byte-aligned update width: the
trailing partial byte's bits are shifted to the high end for
little-endian, matching lower_byte_update's padding semantics.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-8821
branch
2 times, most recently
from
e0fe222 to
8517838
Compare
The constant propagator previously refused to propagate WITH expressions (with a comment 'this is bad'), as well as array and struct literals containing non-constant elements. This prevented simplification of expressions like (array WITH [2]:=x)[0] where the accessed index differs from the updated index. This is needed for DFCC contract verification where the assigns clause tracking data structure is an array of structs updated with WITH expressions. Without propagation, the size and pointer fields read from this array remain symbolic, preventing the simplifier from decomposing byte_update expressions into efficient WITH updates. On the reproducer from issue diffblue#8821, this reduces the SMT formula from 22.6MB (non-terminating) to 1.9MB (solves in 3.5s). Update the array-cell-sensitivity tests: WITH expressions may now be fully propagated and no longer appear in the VCC output. The tests' purpose (verifying no [[index]] cell expansion) is still served by the negative patterns. Fixes: diffblue#8821 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8959 +/- ##
========================================
Coverage 80.49% 80.49%
========================================
Files 1704 1704
Lines 188789 188795 +6
Branches 73 73
========================================
+ Hits 151967 151978 +11
+ Misses 36822 36817 -5 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Collaborator
|
Test results on the specific test cases for Issues 8821 and 8796 look good here, running on macOS |
Collaborator
|
Full regression test on macOS on mlkem-native with MLKEM_K=2,3,4 also looks good, with an observable performance improvement for all parameter sets. |
Collaborator
Author
|
Closing as this selective propagation of non-constants has the risk of resulting in excessively large formulae. The right fix for #8821 is to not use The first commit in this PR, which fixes an actual bug, will be PR'ed separately with a test. |
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.
The constant propagator previously refused to propagate WITH expressions (with a comment 'this is bad'), as well as array and struct literals containing non-constant elements. This prevented simplification of expressions like (array WITH [2]:=x)[0] where the accessed index differs from the updated index.
This is needed for DFCC contract verification where the assigns clause tracking data structure is an array of structs updated with WITH expressions. Without propagation, the size and pointer fields read from this array remain symbolic, preventing the simplifier from decomposing byte_update expressions into efficient WITH updates.
On the reproducer from issue #8821, this reduces the SMT formula from 22.6MB (non-terminating) to 1.9MB (solves in 3.5s).
Update the array-cell-sensitivity2 test: the second WITH expression (array#3) is now fully propagated and no longer appears in the VCC output. The test's purpose (verifying no [[index]] cell expansion) is still served by the first WITH pattern and the negative pattern.
Fixes: #8821