Repository navigation
[Paper] Discuss the engineering cost and type-domain limits of TypeScript models #482
Description
Required paper revision
The next revision of Unknown-Call Policies in TypeScript Symbolic Execution must explicitly discuss the engineering difficulty of developing semantic models for JavaScript/TypeScript runtime behavior. The user requested this as a tracked editorial requirement, not an optional future-work remark.
The discussion should explain:
- Runtime type variability: one API can require different behavior for receiver and argument kinds, unions, heterogeneous arrays, null/undefined, coercions, boxed values, omitted/default arguments, callbacks and object shapes. TypeScript annotations alone do not establish all runtime cases.
- Incomplete domains: distinguish supported input generators and serializers, symbolic heap/value domains, and native state observations. Indexed records, recursive/cyclic structures and unbounded generic types currently expose real gaps. A model for a bounded type/domain does not establish support for every use of the API.
- Choosing models and boundaries: explain how API families and concrete signatures are selected, what the corpus actually exercises, and which variants remain outside each model's guards. Catalog size is neither semantic completeness nor a measure of implementation effort. Keep model selection separate from outcome-based class admission.
- Implementation and validation cost: account for argument dependence, heap mutation, exceptions, repeated-call consistency and interaction with interpreter/runtime-kind representation. Describe the work of specifying guards, defining residual behavior, validating covered cases against native execution and retaining unsupported cases explicitly.
- Consequences for the evaluation: model coverage and applicability bounds constrain the scientific conclusions. Report useful replayed inputs/native coverage separately from agreement of symbolic predictions with real execution.
Concrete evidence to use
Start with reproducible examples, rather than a general claim that dynamic languages are difficult:
Array.pushin the real HashMap constructor: EMPTY_STOP stops after 3553 steps; preserving 91 reached-prefix input scenarios yields native coverage 57/66. The boundary of an unavailable model and the ability to retain useful test inputs are separate properties.- Primitive/string conversion: symbolic number-to-string remains an explicit supported-domain gap; trace exact guards and relevant callers/tests in the current implementation.
- Indexed
Record<string, string>, recursive/cyclic objects and bounded specialization of generic types: document which gaps are in test input/state domains and which are in semantic models. - Guarded partial models: inspect the current guarded model contracts and residual STOP/FRESH behavior to illustrate what supporting one variant leaves unresolved.
Latest class measurement implementation: #479
Local evidence under /Users/a.menshutin/Personal/usvm/iccq2026-paper/experiments/class-coverage-round-robin-20261002/:
real-class-machine-diagnostic-20261014/DIAGNOSTIC.mdreal-class-machine-diagnostic-20261014/revised-protocol-v8/README.mdreal-class-campaign-20261014/V7_INFRASTRUCTURE_FRONTIER.mdreal-class-campaign-20261014/original/selection-ledger-v7.json
The original 200-class screening rejected 197 classes before machine execution. Imports, module initialization and coverage instrumentation must be identified as infrastructure/admission limitations, rather than attributed wholesale to model-writing difficulty. The constructor parameter-property defect fixed in UnitTestBot/jacodb#437 is a frontend defect and must also be identified separately.
Acceptance criteria
- Add a substantive discussion of model development effort and applicability limits to the paper; connect it to the design and experimental limitations.
- Support the discussion with at least two source/test/replay-backed examples and an explicit mapping of model, domain, frontend and infrastructure gaps.
- Explain the rationale for model/API selection and the supported runtime variants; avoid presenting partial support as general API support.
- Describe labor/maintenance cost qualitatively unless development records support numerical estimates. Do not invent person-hours or infer them from the number of model identifiers.
- Keep the historical manuscript and sealed experiment versions distinct from the current class diagnostics; verify every numerical claim against its stated version.
- Review the revised text and its placement before the next final manuscript build.
Activity