Skip to content

Commit 99fa6cd

Browse files
LipenLipen
authored
[TS] Fixes in TS interpreter for real projects (#336)
1 parent b41bb3d commit 99fa6cd

7 files changed

Lines changed: 97 additions & 14 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,7 @@ fun TsContext.checkReadingInRange(
249249
)
250250
}
251251

252-
fun TsContext.checkLengthBounds(
252+
fun TsContext.ensureLengthBounds(
253253
scope: TsStepScope,
254254
length: UExpr<TsSizeSort>,
255255
maxLength: Int,

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

Lines changed: 26 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package org.usvm.machine.expr
22

33
import io.ksmt.utils.asExpr
4+
import mu.KotlinLogging
45
import org.jacodb.ets.model.EtsArrayAccess
56
import org.jacodb.ets.model.EtsArrayType
67
import org.jacodb.ets.model.EtsBooleanType
@@ -20,18 +21,30 @@ import org.usvm.types.first
2021
import org.usvm.util.mkArrayIndexLValue
2122
import org.usvm.util.mkArrayLengthLValue
2223

24+
private val logger = KotlinLogging.logger {}
25+
2326
internal fun TsExprResolver.handleArrayAccess(
2427
value: EtsArrayAccess,
2528
): UExpr<*>? = with(ctx) {
2629
// Resolve the array.
27-
val array = resolve(value.array) ?: return null
28-
check(array.sort == addressSort) {
29-
"Expected address sort for array, got: ${array.sort}"
30+
val array = run {
31+
val resolved = resolve(value.array) ?: return null
32+
if (resolved.isFakeObject()) {
33+
scope.assert(resolved.getFakeType(scope).refTypeExpr) ?: run {
34+
logger.warn { "UNSAT after ensuring fake object is ref-typed" }
35+
return null
36+
}
37+
resolved.extractRef(scope)
38+
} else {
39+
check(resolved.sort == addressSort) {
40+
"Expected address sort for array, got: ${resolved.sort}"
41+
}
42+
resolved.asExpr(addressSort)
43+
}
3044
}
31-
val arrayRef = array.asExpr(addressSort)
3245

3346
// Check for undefined or null array access.
34-
checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null
47+
checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null
3548

3649
// Resolve the index.
3750
val resolvedIndex = resolve(value.index) ?: return null
@@ -49,8 +62,8 @@ internal fun TsExprResolver.handleArrayAccess(
4962
).asExpr(sizeSort)
5063

5164
// Determine the array type.
52-
val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) {
53-
scope.calcOnState { memory.typeStreamOf(arrayRef).first() }
65+
val arrayType = if (isAllocatedConcreteHeapRef(array)) {
66+
scope.calcOnState { memory.typeStreamOf(array).first() }
5467
} else {
5568
value.array.type
5669
}
@@ -59,7 +72,7 @@ internal fun TsExprResolver.handleArrayAccess(
5972
}
6073

6174
// Read the array element.
62-
readArray(scope, arrayRef, bvIndex, arrayType)
75+
readArray(scope, array, bvIndex, arrayType)
6376
}
6477

6578
fun TsContext.readArray(
@@ -103,7 +116,11 @@ fun TsContext.readArray(
103116
index = index,
104117
type = arrayType,
105118
)
106-
return scope.calcOnState { memory.read(lValue) }
119+
val fake = scope.calcOnState { memory.read(lValue) }
120+
check(fake.isFakeObject()) {
121+
"Expected fake object in concrete array with unresolved element type, got: $fake"
122+
}
123+
return fake
107124
}
108125

109126
// If the element type is unresolved, we need to create a fake object

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr
55
import org.jacodb.ets.model.EtsAnyType
66
import org.jacodb.ets.model.EtsArrayType
77
import org.jacodb.ets.model.EtsLocal
8+
import org.jacodb.ets.model.EtsStringType
89
import org.jacodb.ets.model.EtsUnknownType
910
import org.usvm.UExpr
1011
import org.usvm.UHeapRef
@@ -30,6 +31,11 @@ fun TsContext.readLengthProperty(
3031
EtsArrayType(EtsUnknownType, dimensions = 1)
3132
}
3233

34+
is EtsStringType -> {
35+
// Strings are treated as arrays of characters (represented as strings).
36+
EtsArrayType(EtsStringType, dimensions = 1)
37+
}
38+
3339
else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type")
3440
}
3541

@@ -53,7 +59,7 @@ fun TsContext.readArrayLength(
5359
}
5460

5561
// Check that the length is within the allowed bounds.
56-
checkLengthBounds(scope, length, maxArraySize) ?: return null
62+
ensureLengthBounds(scope, length, maxArraySize) ?: return null
5763

5864
// Convert the length to fp64.
5965
return mkBvToFpExpr(

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

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1160,13 +1160,24 @@ class TsSimpleValueResolver(
11601160
}
11611161

11621162
if (local.name.startsWith(ANONYMOUS_METHOD_PREFIX)) {
1163+
val currentMethod = scope.calcOnState { lastEnteredMethod }
11631164
val sig = EtsMethodSignature(
1164-
enclosingClass = EtsClassSignature.UNKNOWN,
1165+
enclosingClass = currentMethod.signature.enclosingClass,
11651166
name = local.name,
11661167
parameters = emptyList(),
11671168
returnType = EtsUnknownType,
11681169
)
11691170
val methods = ctx.resolveEtsMethods(sig)
1171+
if (methods.isEmpty()) {
1172+
logger.error { "Cannot resolve anonymous method for local: $local" }
1173+
scope.assert(ctx.mkFalse())
1174+
return null
1175+
}
1176+
if (methods.size > 1) {
1177+
logger.error { "Multiple methods found for anonymous method local: $local" }
1178+
scope.assert(ctx.mkFalse())
1179+
return null
1180+
}
11701181
val method = methods.single()
11711182
val ref = scope.calcOnState { getMethodRef(method) }
11721183
return ref

‎usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.usvm.util
22

3+
import mu.KotlinLogging
34
import org.jacodb.ets.model.EtsClass
45
import org.jacodb.ets.model.EtsClassType
56
import org.jacodb.ets.model.EtsField
@@ -12,6 +13,8 @@ import org.jacodb.ets.utils.CONSTRUCTOR_NAME
1213
import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
1314
import org.usvm.machine.TsContext
1415

16+
private val logger = KotlinLogging.logger {}
17+
1518
fun TsContext.resolveEtsField(
1619
instance: EtsLocal?,
1720
field: EtsFieldSignature,
@@ -68,10 +71,12 @@ private fun tryGetSingleField(
6871
val clazz = classes.single()
6972
val fields = clazz.getAllFields(hierarchy).filter { it.name == fieldName }
7073
if (fields.isEmpty()) {
71-
error("No field with name '$fieldName' in class '${clazz.name}'")
74+
// logger.warn { "No field with name '$fieldName' in class '${clazz.name}'" }
75+
return null
7276
}
7377
if (fields.size > 1) {
74-
error("Multiple fields with name '$fieldName' in class '${clazz.name}': $fields")
78+
logger.warn { "Multiple fields with name '$fieldName' in class '${clazz.name}': $fields" }
79+
return null
7580
}
7681
return fields.single()
7782
}

‎usvm-ts/src/test/kotlin/org/usvm/samples/lang/Optional.kt‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
package org.usvm.samples.lang
2+
3+
import org.jacodb.ets.model.EtsScene
4+
import org.junit.jupiter.api.Disabled
5+
import org.junit.jupiter.api.RepeatedTest
6+
import org.usvm.api.TsTestValue
7+
import org.usvm.util.TsMethodTestRunner
8+
import org.usvm.util.eq
9+
10+
class Optional : TsMethodTestRunner() {
11+
private val tsPath = "/samples/lang/Optional.ts"
12+
13+
override val scene: EtsScene = loadScene(tsPath)
14+
15+
@Disabled("Input union types are not supported yet")
16+
@RepeatedTest(10, failureThreshold = 1)
17+
fun `test nullableArgument`() {
18+
val method = getMethod("nullableArgument")
19+
discoverProperties<TsTestValue, TsTestValue.TsNumber>(
20+
method = method,
21+
{ x, r -> (r eq 0) && (x is TsTestValue.TsUndefined) },
22+
{ x, r -> (r eq 0) && (x is TsTestValue.TsNull) },
23+
{ x, r -> (r eq 1) && (x is TsTestValue.TsNumber) && (x eq 1) },
24+
{ x, r -> (r eq 2) && (x is TsTestValue.TsNumber) && (x eq 2) },
25+
{ x, r -> (r eq 10) && (x is TsTestValue.TsNumber) },
26+
)
27+
}
28+
}

‎usvm-ts/src/test/resources/samples/lang/Optional.ts‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// @ts-nocheck
2+
// noinspection JSUnusedGlobalSymbols
3+
4+
class Optional {
5+
nullableArgument(x: number | null): number {
6+
let value: number = 42;
7+
if (x === undefined) return 0;
8+
if (x !== null) {
9+
if (x === 1) return x; // 1
10+
value = x;
11+
if (x === 2) return value; // 2
12+
return 10;
13+
}
14+
return 0;
15+
}
16+
}

0 commit comments

Comments
 (0)