UnitTestBot / UnitTestBot/usvm

[TS] Preserve fake values in symbolic reference-array reads

Open
#379 0 comments 0 reactions 0 assignees View on GitHub

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

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.