Skip to content

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

Description

@CaelmBleidd

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions