Record derived source expressions in counterexamples - #859
Merged
Conversation
The n-th LLVM struct element is not the n-th DW_TAG_member, so naming a
field by its ordinal position reported the wrong member whenever the two
orderings diverged: bitfields share a storage unit, clang inserts padding,
and a C++ base class occupies a field without being a member. A store to
'b->after' was recorded as 'b->f2', and 'p->d0' as 'p->d1' -- a wrong name
in a counterexample is worse than no name at all.
Look the member up by the byte offset of the field being indexed instead,
and decline to name a bitfield, a static or artificial member, an ambiguous
match, or a union, where a field index cannot pick a member out.
Fix three more ways a name could describe the wrong object:
- A pointer value owes a dereference that only the member branch spent,
so '(*pa)[2]' came out as 'pa[2]', a different address. Spend it in the
subscript branch too.
- Subscripting the address of a non-array named 'x[1]' for a scalar x.
Require the debug type to really be an array.
- A cast that changes the type no longer describes the same object, so
neither it nor the stripPointerCastsAndAliases fallback should carry a
source expression across one.
Consume one DWARF array dimension per subscript, since DWARF folds every
dimension into a single node; multi-dimensional element expressions were
dropped entirely before and now resolve.
Restrict the recorded value to scalars -- vectors reached the recorder
through the vector load and store paths -- and drop the parameter name
shadowing llvm::Value.
Move the test into its own folder pinned to Corral: source expressions are
only rendered into a counterexample by /printDataValues, so @checkout could
never match under Boogie and the c/data job went red. Add regressions for
the bitfield, cast, and array cases; the absence assertions use awk rather
than grep -v, which exits 0 whenever any line differs and so asserts
nothing.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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.
Summary
Testing