Repository navigation
Fix types of unavailable SMT array model values - #9161
Open
chaizhenhua wants to merge 1 commit into
Open
chaizhenhua wants to merge 1 commit into
chaizhenhua wants to merge 1 commit into
Conversation
Array model reconstruction currently uses nil expressions for missing defaults and unavailable parsed elements. Selecting one of these elements during counterexample trace simplification loses the array element type and violates simplify_rec's type-preservation postcondition. Use typed unknown expressions, as the bitvector array model reader already does, without inventing concrete values or changing solver constraints. Keep known defaults/stores, zero lengths, unknown sizes and the existing nonconstant-index handling unchanged. Extend the existing array-model test helper and exercise the actual JSON declaration exporter. The additional unit-module dependencies are only for this parser-to-trace regression; production dependencies are unchanged. The eleven cause/effect cases include missing/default/store values and compatibility with skipped nonconstant indices. Reverting the production change reproduces the simplify_rec postcondition failure (SIGABRT). Validation on develop 820ff0f: - Focused regression: 104 assertions; SMT2: 295 assertions / 40 cases. - Z3 unit tests: 22 assertions / 6 cases. - CORE unit: 592 cases / 18911 assertions, including 2 expected failures. - CBMC CORE: 1128 passed, 67 excluded by the existing profile. - Seven array/VLA Z3 regressions and a real JSON counterexample trace. - Restored fix rebuilt and focused, SMT2 and CORE unit suites passed. - clang-format 18 changed-line check and upstream diff cpplint passed.
chaizhenhua
requested review from
TGWDB,
kroening,
martin-cs,
peterschrammel and
tautschnig
as code owners
September 10, 2026 00:53
This branch has not been deployed
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
1 participant
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.
Array model reconstruction currently uses nil expressions for missing defaults
and unavailable parsed elements. Selecting one of those elements while building
a counterexample trace loses the array element type and violates simplification's
type-preservation postcondition.
Use typed unknown expressions at those two existing reconstruction points, as
the bitvector array reader already does. The change does not invent concrete
values or alter constraints, SAT results, known defaults/stores, zero lengths,
unknown sizes, or nonconstant-index handling. The additional unit dependencies
only exercise the real parser-to-JSON trace boundary.
Validation includes eleven cause/effect unit sections, SMT2/Z3/CORE unit tests,
cbmc-CORE, seven array/VLA regressions through Z3, and a real JSONcounterexample trace. Reverting the two production expressions reproduces the
type-preservation postcondition failure; restoring them rebuilds and passes the
focused, SMT2, and CORE suites.