[TS] Mock unresolved virtual calls instead of killing the state#342
Draft
CaelmBleidd wants to merge 6 commits into
Draft
[TS] Mock unresolved virtual calls instead of killing the state#342CaelmBleidd wants to merge 6 commits into
CaelmBleidd wants to merge 6 commits into
Conversation
Coverage investigation on an open-source corpus showed that 155 of 172 unreached symbolic targets died in under 100ms: TsInterpreter killed the state (assert(false)) on ANY unresolved callee (e.g. Number.isInteger), making everything after such a call unreachable. All three unresolved-call sites in visitVirtualMethodCall now fall back to mockMethodCall + returnSite, mirroring the pre-existing unresolved-constructor approximation. Full usvm-ts suite stays green (422 tests). NOTE: an engine fix, staged to be extracted into a separate PR.
Front ends lower the side effect of `x++`/`--x` into an explicit
assignment (the native ts-frontend emits `%t := x; x := ++x`, ArkAnalyzer
expands to `x := x + 1`), and the jacodb DTO conversion maps both `++` and
`--` to the Pre* model classes only. The resolver previously crashed on
them ("Not supported"), killing every state in loops written with
`x--`/`--x` under the ts-frontend. Pre* now evaluate to ToNumber(arg) +- 1
and Post* (never produced by the converter, but part of the model) to the
old value.
Tests: direct machine tests over programmatically built IR (ArkAnalyzer
cannot exercise these visits since it never emits the unary forms) plus an
ArkAnalyzer-lowered sample. A `const old = x++` sample case is deliberately
absent: ArkAnalyzer lowers it as `x := x + 1; old := x`, i.e. `old`
receives the new value - a frontend lowering bug found while writing these
tests.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @Test | ||
| fun `pre-increment yields arg plus one`() { | ||
| for ((input, result) in run("preInc") { EtsPreIncExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) |
| fun `pre-increment yields arg plus one`() { | ||
| for ((input, result) in run("preInc") { EtsPreIncExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) | ||
| else assertEquals(input + 1, result, 0.0) { "++($input)" } |
| @Test | ||
| fun `pre-decrement yields arg minus one`() { | ||
| for ((input, result) in run("preDec") { EtsPreDecExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) |
| fun `pre-decrement yields arg minus one`() { | ||
| for ((input, result) in run("preDec") { EtsPreDecExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) | ||
| else assertEquals(input - 1, result, 0.0) { "--($input)" } |
| @Test | ||
| fun `post-increment and post-decrement yield the old value`() { | ||
| for ((input, result) in run("postInc") { EtsPostIncExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) |
| fun `post-increment and post-decrement yield the old value`() { | ||
| for ((input, result) in run("postInc") { EtsPostIncExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) | ||
| else assertEquals(input, result, 0.0) { "($input)++" } |
| else assertEquals(input, result, 0.0) { "($input)++" } | ||
| } | ||
| for ((input, result) in run("postDec") { EtsPostDecExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) |
| } | ||
| for ((input, result) in run("postDec") { EtsPostDecExpr(it, EtsNumberType) }) { | ||
| if (input.isNaN()) assertTrue(result.isNaN()) | ||
| else assertEquals(input, result, 0.0) { "($input)--" } |
…lback Frequency data from open-source corpora (TheAlgorithms/TypeScript maths and loiane/javascript-datastructures-algorithms, full-log probes) shows that unresolved calls split into three groups: in-project cross-file targets (a scene-construction problem, not the engine's), a small set of very hot builtins (Math.abs — 208 occurrences, Number.isInteger — 55, Math.sqrt — 13 on the maths corpus alone), and a tail of genuinely unmodelable calls. This change shrinks the over-approximation surface of the mock fallback by modeling the hot builtins precisely in the fp theory: - Number.isInteger / isSafeInteger (2^53 bound not modeled) / isFinite, with the same fake-object discriminator handling as Number.isNaN - Math.floor/ceil/trunc via fp round-to-integral in the matching mode (floor generalized), Math.round as floor(x + 0.5) per JS semantics, Math.abs, Math.sqrt - Math.min/max with JS NaN semantics (NaN if any argument is NaN, unlike IEEE minNum/maxNum) - console.* treated as side-effect-free undefined, like Logger Every remaining mock fallback now logs a distinct "Mocking an unresolved call: <callee> (over-approximation)" line, so the residual over-approximation stays measurable on corpus runs. decrementLoop test properties are reclassified by the observed loop depth: non-integral inputs (n = 2.5) legitimately reach depth ceil(n), and the solver started picking such models once the approximations changed the search.
| "Math.${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}" | ||
| } | ||
| val arg = resolve(expr.args.single()) ?: return null | ||
| when { |
| val plusHalf = mkFpAddExpr( | ||
| mkFpRoundingModeExpr(KFpRoundingMode.RoundNearestTiesToEven), | ||
| value, | ||
| mkFp64(0.5), |
| private fun TsExprResolver.handleMathMinMax(expr: EtsInstanceCallExpr, isMin: Boolean): UExpr<*>? = with(ctx) { | ||
| val args = expr.args.map { arg -> | ||
| val resolved = resolve(arg) ?: return null | ||
| when { |
`new Array(n)` used to allocate an object of an unresolved class (8 occurrences on the maths corpus probe), so none of the array approximations applied to it and every subsequent operation on the array was mocked. Now: - `new Array` in EtsNewExpr allocates a genuine array object (EtsArrayType, length 0), so the array method approximations and the constructor handling apply to it; - the `constructor` call on an array-typed instance is approximated: the zero-argument form keeps the empty length, the single-argument form sets the length with the same size-validity fork as EtsNewArrayExpr (non-integral or negative sizes throw, as in JS); the multi-argument literal form is left to the logged mock fallback.
| return null | ||
| } | ||
|
|
||
| when (expr.args.size) { |
…f-like operands Front ends lower `if (x)` into `x != 0` / `x != false`, byte-identical to a genuine loose comparison in the IR. For reference-like operands the numeric reading diverges from ToBoolean: `undefined != 0` evaluated as ToNumber(undefined) = NaN != 0 = true, making `undefined` truthy (found by the differential oracle: And.andOfUnknown(0, undefined) returned 21 where JS returns 0). A compare of a fake-object or reference operand against literal zero/false now resolves via mkTruthyExpr; numeric and boolean operands keep the literal loose-comparison semantics, matching the convention of the concrete ArkIR interpreter in the hybrid pipeline.
The differential oracle immediately caught the second half of the hole: with the ref-only reading, `if (a)` over a numeric NaN still took the then-branch (`NaN != 0` is true, yet NaN is falsy), so andOfUnknown(NaN, x) returned 0 where JS returns 11. The idiom now resolves via mkTruthyExpr for every operand kind (bool/fp/ref/fake), and only for `!=` — front ends never lower truthiness through `==` (negated tests swap branch successors instead), so `==` keeps the literal loose-equality semantics.
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
2 participants
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.
Coverage investigation on an open-source corpus showed that 155 of 172 unreached symbolic targets died in under 100ms: TsInterpreter killed the state (assert(false)) on ANY unresolved callee (e.g. Number.isInteger), making everything after such a call unreachable. All three unresolved-call sites in visitVirtualMethodCall now fall back to mockMethodCall + returnSite, mirroring the pre-existing unresolved-constructor approximation. Full usvm-ts suite stays green (422 tests).
NOTE: an engine fix, staged to be extracted into a separate PR.