UnitTestBot / UnitTestBot/usvm
[TS] Preserve fake values in symbolic reference-array reads
Nobody has claimed this yet.
- Dominant language
- Kotlin
- Stars
- 33
- Forks
- 27
- Avg merge
- 4d 3h
- Merged PRs (30d)
- 15
Description
Problem
Symbolic reference-array reads can lose the fake-value representation when the address region contains a fake wrapper behind a symbolic array read.
A fake value must keep its boolean, number, and reference payloads together with the corresponding discriminators until its runtime kind is proven. Treating the resulting address expression as a plain reference drops the boolean/number alternatives.
Reproduction
class ArrayElement {}
function inputAnyPreservesNumber(values: ArrayElement[], value: any): number {
if (values.length !== 1) {
return 0;
}
values[0] = value;
const popped: any = values.pop();
if (typeof popped === "number") {
return 44;
}
return 0;
}
The path returning 44 must be reachable: assigning any performs no runtime cast, so value may be a number.
Actual behavior
Both the legacy Array.pop approximation and the intrinsic model from #377 produce only the path returning 0.
The non-empty read is represented as an address-sorted symbolic expression similar to:
ite(index == 0, fakeWrapper, inputArray<unknown[]>[index])
This expression is not a concrete fake-wrapper heap reference, so isFakeObject() returns false. Consumers then treat it as a plain reference and can no longer access the boolean/FP64 payloads or discriminator constraints.
Root cause
- Reference-element arrays are normalized to the
unknown[]storage descriptor. - A fake wrapper can be written to that address region.
- Reading the symbolic address region may return a conditional expression containing the wrapper rather than the concrete wrapper itself.
- Current fake-value recognition and extraction handle only a concrete synthetic wrapper reference.
Required behavior
Implement a fake-aware symbolic array read that preserves all supported representations and discriminator constraints, including alias consistency for already materialized fake values.
Until this is implemented, semantic models must not claim symbolic/input reference arrays as a supported domain.
Regression test
PR #377 will include a disabled end-to-end regression test linked to this issue.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start with the TypeScript reproduction and the symbolic array-read behavior described in the issue, then inspect fake-value recognition and extraction for conditional address expressions. Use the disabled end-to-end regression test planned in PR #377 as the validation target; done means the path returning 44 is reachable while fake payloads, discriminators, and alias consistency are preserved.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- kotlin, typescript
- Domain
- compilers, testing-qa
- Issue type
- Bug
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Activity status
- Active
- Clarity
- Mostly clear
- Newbie friendliness
- 48/100