Skip to content

Commit b690eb2

Browse files
CaelmBleiddCaelmBleidd
committed
[TS] Implement inc/dec unary expressions in TsExprResolver
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.
1 parent a15dc8f commit b690eb2

4 files changed

Lines changed: 239 additions & 12 deletions

File tree

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt‎

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -248,24 +248,32 @@ class TsExprResolver(
248248
return mkNumericExpr(arg, scope)
249249
}
250250

251-
override fun visit(expr: EtsPostIncExpr): UExpr<out USort>? {
252-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
253-
error("Not supported $expr")
251+
// NOTE on inc/dec: front ends lower the *side effect* of `x++`/`--x` into an
252+
// explicit assignment (`%t := x; x := ++x`), and the jacodb DTO conversion maps
253+
// both `++` and `--` to the Pre* classes only. Therefore the expressions below
254+
// are pure value computations: Pre* yield ToNumber(arg) +- 1, Post* (which never
255+
// come from the converter, but are part of the model) yield the old value.
256+
257+
override fun visit(expr: EtsPostIncExpr): UExpr<out USort>? = with(ctx) {
258+
val arg = resolve(expr.arg) ?: return null
259+
return mkNumericExpr(arg, scope)
254260
}
255261

256-
override fun visit(expr: EtsPostDecExpr): UExpr<out USort>? {
257-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
258-
error("Not supported $expr")
262+
override fun visit(expr: EtsPostDecExpr): UExpr<out USort>? = with(ctx) {
263+
val arg = resolve(expr.arg) ?: return null
264+
return mkNumericExpr(arg, scope)
259265
}
260266

261-
override fun visit(expr: EtsPreIncExpr): UExpr<out USort>? {
262-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
263-
error("Not supported $expr")
267+
override fun visit(expr: EtsPreIncExpr): UExpr<out USort>? = with(ctx) {
268+
val arg = resolve(expr.arg) ?: return null
269+
val numeric = mkNumericExpr(arg, scope).asExpr(fp64Sort)
270+
return mkFpAddExpr(fpRoundingModeSortDefaultValue(), numeric, mkFp64(1.0))
264271
}
265272

266-
override fun visit(expr: EtsPreDecExpr): UExpr<out USort>? {
267-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
268-
error("Not supported $expr")
273+
override fun visit(expr: EtsPreDecExpr): UExpr<out USort>? = with(ctx) {
274+
val arg = resolve(expr.arg) ?: return null
275+
val numeric = mkNumericExpr(arg, scope).asExpr(fp64Sort)
276+
return mkFpSubExpr(fpRoundingModeSortDefaultValue(), numeric, mkFp64(1.0))
269277
}
270278

271279
override fun visit(expr: EtsBitNotExpr): UExpr<out USort>? = with(ctx) {

‎usvm-ts/src/test/kotlin/org/usvm/machine/IncDecExprTest.kt‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
package org.usvm.machine
2+
3+
import org.jacodb.ets.model.BasicBlock
4+
import org.jacodb.ets.model.EtsAssignStmt
5+
import org.jacodb.ets.model.EtsBlockCfg
6+
import org.jacodb.ets.model.EtsClassImpl
7+
import org.jacodb.ets.model.EtsClassSignature
8+
import org.jacodb.ets.model.EtsEntity
9+
import org.jacodb.ets.model.EtsFile
10+
import org.jacodb.ets.model.EtsFileSignature
11+
import org.jacodb.ets.model.EtsLocal
12+
import org.jacodb.ets.model.EtsMethodImpl
13+
import org.jacodb.ets.model.EtsMethodParameter
14+
import org.jacodb.ets.model.EtsMethodSignature
15+
import org.jacodb.ets.model.EtsNumberType
16+
import org.jacodb.ets.model.EtsParameterRef
17+
import org.jacodb.ets.model.EtsPostDecExpr
18+
import org.jacodb.ets.model.EtsPostIncExpr
19+
import org.jacodb.ets.model.EtsPreDecExpr
20+
import org.jacodb.ets.model.EtsPreIncExpr
21+
import org.jacodb.ets.model.EtsReturnStmt
22+
import org.jacodb.ets.model.EtsScene
23+
import org.jacodb.ets.model.EtsStmtLocation
24+
import org.junit.jupiter.api.Assertions.assertEquals
25+
import org.junit.jupiter.api.Assertions.assertTrue
26+
import org.junit.jupiter.api.Test
27+
import org.usvm.PathSelectionStrategy
28+
import org.usvm.SolverType
29+
import org.usvm.UMachineOptions
30+
import org.usvm.api.TsTestValue
31+
import org.usvm.util.TsTestResolver
32+
import kotlin.time.Duration.Companion.seconds
33+
34+
/**
35+
* Direct tests for the inc/dec expression resolution.
36+
*
37+
* The IR is built programmatically: ArkAnalyzer never emits `++`/`--` unary
38+
* expressions (it expands them into `x := x + 1`), while the native ts-frontend
39+
* does emit them (as the value part, with an explicit write-back assignment),
40+
* so sample-based tests cannot exercise these visits.
41+
*/
42+
class IncDecExprTest {
43+
44+
private fun buildMethod(name: String, makeExpr: (EtsEntity) -> EtsEntity): Pair<EtsScene, EtsMethodImpl> {
45+
val fileSig = EtsFileSignature(projectName = "test", fileName = "IncDec.ts")
46+
val classSig = EtsClassSignature(name = "T", file = fileSig)
47+
val method = EtsMethodImpl(
48+
signature = EtsMethodSignature(
49+
enclosingClass = classSig,
50+
name = name,
51+
parameters = listOf(EtsMethodParameter(0, "a", EtsNumberType)),
52+
returnType = EtsNumberType,
53+
),
54+
)
55+
56+
fun loc(i: Int) = EtsStmtLocation(method, i)
57+
val a = EtsLocal("a", EtsNumberType)
58+
val res = EtsLocal("res", EtsNumberType)
59+
val stmts = listOf(
60+
EtsAssignStmt(loc(0), a, EtsParameterRef(0, EtsNumberType)),
61+
EtsAssignStmt(loc(1), res, makeExpr(a)),
62+
EtsReturnStmt(loc(2), res),
63+
)
64+
method.body.cfg = EtsBlockCfg(
65+
blocks = listOf(BasicBlock(0, stmts)),
66+
successors = mapOf(0 to emptyList()),
67+
)
68+
method.body.locals = listOf(a, res)
69+
70+
val cls = EtsClassImpl(signature = classSig, fields = emptyList(), methods = listOf(method))
71+
val file = EtsFile(signature = fileSig, classes = listOf(cls), namespaces = emptyList())
72+
return EtsScene(listOf(file)) to method
73+
}
74+
75+
private fun run(name: String, makeExpr: (EtsEntity) -> EtsEntity): List<Pair<Double, Double>> {
76+
val (scene, method) = buildMethod(name, makeExpr)
77+
val options = UMachineOptions(
78+
pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
79+
exceptionsPropagation = true,
80+
timeout = 20.seconds,
81+
solverType = SolverType.YICES,
82+
)
83+
val states = TsMachine(scene, options, TsOptions()).use { machine ->
84+
machine.analyze(listOf(method))
85+
}
86+
assertTrue(states.isNotEmpty()) { "no states collected for $name" }
87+
return states.mapNotNull { state ->
88+
val test = TsTestResolver().resolve(method, state)
89+
val input = (test.before.parameters.firstOrNull() as? TsTestValue.TsNumber)?.number
90+
val result = (test.returnValue as? TsTestValue.TsNumber)?.number
91+
if (input != null && result != null) input to result else null
92+
}.also { assertTrue(it.isNotEmpty()) { "no numeric executions for $name" } }
93+
}
94+
95+
@Test
96+
fun `pre-increment yields arg plus one`() {
97+
for ((input, result) in run("preInc") { EtsPreIncExpr(it, EtsNumberType) }) {
98+
if (input.isNaN()) assertTrue(result.isNaN())
99+
else assertEquals(input + 1, result, 0.0) { "++($input)" }
100+
}
101+
}
102+
103+
@Test
104+
fun `pre-decrement yields arg minus one`() {
105+
for ((input, result) in run("preDec") { EtsPreDecExpr(it, EtsNumberType) }) {
106+
if (input.isNaN()) assertTrue(result.isNaN())
107+
else assertEquals(input - 1, result, 0.0) { "--($input)" }
108+
}
109+
}
110+
111+
@Test
112+
fun `post-increment and post-decrement yield the old value`() {
113+
for ((input, result) in run("postInc") { EtsPostIncExpr(it, EtsNumberType) }) {
114+
if (input.isNaN()) assertTrue(result.isNaN())
115+
else assertEquals(input, result, 0.0) { "($input)++" }
116+
}
117+
for ((input, result) in run("postDec") { EtsPostDecExpr(it, EtsNumberType) }) {
118+
if (input.isNaN()) assertTrue(result.isNaN())
119+
else assertEquals(input, result, 0.0) { "($input)--" }
120+
}
121+
}
122+
}

‎usvm-ts/src/test/kotlin/org/usvm/samples/operators/IncDec.kt‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
package org.usvm.samples.operators
2+
3+
import org.jacodb.ets.model.EtsScene
4+
import org.junit.jupiter.api.Test
5+
import org.usvm.api.TsTestValue
6+
import org.usvm.util.TsMethodTestRunner
7+
import org.usvm.util.eq
8+
import org.usvm.util.isNaN
9+
10+
class IncDec : TsMethodTestRunner() {
11+
private val tsPath = "/samples/operators/IncDec.ts"
12+
13+
override val scene: EtsScene = loadScene(tsPath)
14+
15+
@Test
16+
fun `test preIncrement`() {
17+
val method = getMethod("preIncrement")
18+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
19+
method = method,
20+
{ a, r -> a.isNaN() && r.isNaN() },
21+
{ a, r -> !a.isNaN() && (r.number eq a.number + 1) },
22+
invariants = arrayOf(
23+
{ a, r ->
24+
if (a.isNaN()) r.isNaN() else r.number eq a.number + 1
25+
},
26+
)
27+
)
28+
}
29+
30+
@Test
31+
fun `test preDecrement`() {
32+
val method = getMethod("preDecrement")
33+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
34+
method = method,
35+
{ a, r -> a.isNaN() && r.isNaN() },
36+
{ a, r -> !a.isNaN() && (r.number eq a.number - 1) },
37+
invariants = arrayOf(
38+
{ a, r ->
39+
if (a.isNaN()) r.isNaN() else r.number eq a.number - 1
40+
},
41+
)
42+
)
43+
}
44+
45+
@Test
46+
fun `test decrementLoop`() {
47+
val method = getMethod("decrementLoop")
48+
discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber>(
49+
method = method,
50+
{ n, r -> (n.number <= 0 || n.isNaN()) && (r eq 0) },
51+
{ n, r -> n.number >= 3 && (r eq 3) },
52+
{ n, r -> n.number > 0 && n.number <= 2 && r.number > 0 && r.number <= 2 },
53+
)
54+
}
55+
}

‎usvm-ts/src/test/resources/samples/operators/IncDec.ts‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// @ts-nocheck
2+
// noinspection JSUnusedGlobalSymbols
3+
4+
class IncDec {
5+
preIncrement(a: number): number {
6+
let x = a;
7+
++x;
8+
if (Number.isNaN(a)) return x; // NaN + 1 == NaN
9+
if (a == 0) return x; // ++0 == 1
10+
if (a > 0) return x;
11+
if (a < 0) return x;
12+
// unreachable
13+
}
14+
15+
// NOTE: a `const old = x++` case is deliberately absent: ArkAnalyzer
16+
// (neo/2025-09-03) lowers it as `x := x + 1; old := x`, i.e. `old` receives
17+
// the *new* value — a frontend lowering bug that no engine semantics can fix.
18+
19+
preDecrement(a: number): number {
20+
let x = a;
21+
--x;
22+
if (Number.isNaN(a)) return x; // NaN - 1 == NaN
23+
if (a == 0) return x; // --0 == -1
24+
if (a > 0) return x;
25+
if (a < 0) return x;
26+
// unreachable
27+
}
28+
29+
decrementLoop(n: number): number {
30+
let count = 0;
31+
let x = n;
32+
while (x > 0 && count < 3) {
33+
x--;
34+
count++;
35+
}
36+
// Each loop depth is a distinct branch so that full coverage requires
37+
// the engine to actually unroll the decrementing loop.
38+
if (count == 0) return count;
39+
if (count == 3) return count;
40+
return count; // 1 or 2 iterations
41+
}
42+
}

0 commit comments

Comments
 (0)