Skip to content

Commit 6194bbd

Browse files
LipenLipen
authored
[TS] Support globals and imports (#323)
1 parent ebe4365 commit 6194bbd

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+3515
-849
lines changed

‎buildSrc/src/main/kotlin/Dependencies.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ object Versions {
66
const val clikt = "5.0.0"
77
const val detekt = "1.23.7"
88
const val ini4j = "0.5.4"
9-
const val jacodb = "d3e97200d6"
9+
const val jacodb = "bb51484fb4"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"

‎usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,12 +22,14 @@ fun mockMethodCall(
2222
result = when (sort) {
2323
is UAddressSort -> makeSymbolicRefUntyped()
2424

25-
is TsUnresolvedSort -> ctx.mkFakeValue(
26-
scope,
27-
makeSymbolicPrimitive(ctx.boolSort),
28-
makeSymbolicPrimitive(ctx.fp64Sort),
29-
makeSymbolicRefUntyped()
30-
)
25+
is TsUnresolvedSort -> scope.calcOnState {
26+
mkFakeValue(
27+
scope = scope,
28+
boolValue = makeSymbolicPrimitive(ctx.boolSort),
29+
fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
30+
refValue = makeSymbolicRefUntyped(),
31+
)
32+
}
3133

3234
else -> makeSymbolicPrimitive(sort)
3335
}

‎usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,12 @@ sealed interface TsTestValue {
3030
data object TsUnknown : TsTestValue
3131
data object TsNull : TsTestValue
3232
data object TsUndefined : TsTestValue
33-
data object TsException : TsTestValue
33+
34+
sealed interface TsException : TsTestValue {
35+
data object UnknownException : TsException
36+
data class StringException(val message: String) : TsException
37+
data class ObjectException(val value: TsTestValue) : TsException
38+
}
3439

3540
data class TsBoolean(val value: Boolean) : TsTestValue
3641

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

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,20 @@ import org.jacodb.ets.model.EtsArrayType
88
import org.jacodb.ets.model.EtsBooleanType
99
import org.jacodb.ets.model.EtsEnumValueType
1010
import org.jacodb.ets.model.EtsGenericType
11+
import org.jacodb.ets.model.EtsLocal
12+
import org.jacodb.ets.model.EtsMethod
1113
import org.jacodb.ets.model.EtsNullType
1214
import org.jacodb.ets.model.EtsNumberType
15+
import org.jacodb.ets.model.EtsParameterRef
1316
import org.jacodb.ets.model.EtsRefType
1417
import org.jacodb.ets.model.EtsScene
1518
import org.jacodb.ets.model.EtsStringType
19+
import org.jacodb.ets.model.EtsThis
1620
import org.jacodb.ets.model.EtsType
1721
import org.jacodb.ets.model.EtsUndefinedType
1822
import org.jacodb.ets.model.EtsUnionType
1923
import org.jacodb.ets.model.EtsUnknownType
24+
import org.jacodb.ets.model.EtsValue
2025
import org.usvm.UAddressSort
2126
import org.usvm.UBoolExpr
2227
import org.usvm.UBoolSort
@@ -111,6 +116,23 @@ class TsContext(
111116
return heapRefToStringConstant[ref]
112117
}
113118

119+
fun getLocalIdx(local: EtsValue, method: EtsMethod): Int? =
120+
// Note: below, 'n' means the number of arguments
121+
when (local) {
122+
// Note: 'this' has index 0
123+
is EtsThis -> 0
124+
125+
// Note: arguments have indices from 1 to n
126+
is EtsParameterRef -> local.index + 1
127+
128+
// Note: locals have indices starting from (n+1)
129+
is EtsLocal -> method.locals.indexOfFirst { it.name == local.name }
130+
.takeIf { it >= 0 }
131+
?.let { it + method.parameters.size + 1 }
132+
133+
else -> error("Unexpected local: $local")
134+
}
135+
114136
fun typeToSort(type: EtsType): USort = when (type) {
115137
is EtsBooleanType -> boolSort
116138
is EtsNumberType -> fp64Sort
@@ -272,7 +294,7 @@ class TsContext(
272294
fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
273295
return scope.calcOnState { extractRef(memory) }
274296
}
275-
297+
276298
// This is an identifier for a special function representing the 'resolve' function used in promises.
277299
// It is not a real function in the code, but we need it to handle promise resolution.
278300
val resolveFunctionRef: UConcreteHeapRef = allocateConcreteRef()

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

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,19 @@ package org.usvm.machine.expr
22

33
import io.ksmt.sort.KFp64Sort
44
import io.ksmt.utils.asExpr
5+
import org.jacodb.ets.model.EtsStringType
56
import org.usvm.UBoolExpr
67
import org.usvm.UBoolSort
78
import org.usvm.UExpr
9+
import org.usvm.UHeapRef
810
import org.usvm.USort
911
import org.usvm.api.makeSymbolicPrimitive
1012
import org.usvm.isFalse
1113
import org.usvm.machine.TsContext
14+
import org.usvm.machine.TsSizeSort
1215
import org.usvm.machine.interpreter.TsStepScope
16+
import org.usvm.machine.state.TsMethodResult
17+
import org.usvm.machine.state.TsState
1318
import org.usvm.machine.types.EtsFakeType
1419
import org.usvm.machine.types.ExprWithTypeConstraint
1520
import org.usvm.types.single
@@ -182,3 +187,47 @@ fun TsContext.mkNullishExpr(
182187
// Non-reference types (numbers, booleans, strings) are never nullish
183188
return mkFalse()
184189
}
190+
191+
fun TsState.throwException(reason: String) {
192+
val ref = ctx.mkStringConstantRef(reason)
193+
methodResult = TsMethodResult.TsException(ref, EtsStringType)
194+
}
195+
196+
fun TsContext.checkUndefinedOrNullPropertyRead(
197+
scope: TsStepScope,
198+
instance: UHeapRef,
199+
propertyName: String,
200+
): Unit? {
201+
val ref = instance.unwrapRef(scope)
202+
val condition = mkAnd(
203+
mkNot(mkHeapRefEq(ref, mkUndefinedValue())),
204+
mkNot(mkHeapRefEq(ref, mkTsNullValue())),
205+
)
206+
return scope.fork(
207+
condition,
208+
blockOnFalseState = { throwException("Undefined or null property access: $propertyName of $ref") }
209+
)
210+
}
211+
212+
fun TsContext.checkNegativeIndexRead(
213+
scope: TsStepScope,
214+
index: UExpr<TsSizeSort>,
215+
): Unit? {
216+
val condition = mkBvSignedGreaterOrEqualExpr(index, mkBv(0))
217+
return scope.fork(
218+
condition,
219+
blockOnFalseState = { throwException("Negative index access: $index") }
220+
)
221+
}
222+
223+
fun TsContext.checkReadingInRange(
224+
scope: TsStepScope,
225+
index: UExpr<TsSizeSort>,
226+
length: UExpr<TsSizeSort>,
227+
): Unit? {
228+
val condition = mkBvSignedLessExpr(index, length)
229+
return scope.fork(
230+
condition,
231+
blockOnFalseState = { throwException("Index out of bounds: $index, length: $length") }
232+
)
233+
}

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

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
package org.usvm.machine.expr
2+
3+
import io.ksmt.utils.asExpr
4+
import org.jacodb.ets.model.EtsArrayAccess
5+
import org.jacodb.ets.model.EtsArrayType
6+
import org.jacodb.ets.model.EtsBooleanType
7+
import org.jacodb.ets.model.EtsNumberType
8+
import org.jacodb.ets.model.EtsUnknownType
9+
import org.usvm.UConcreteHeapRef
10+
import org.usvm.UExpr
11+
import org.usvm.UHeapRef
12+
import org.usvm.api.typeStreamOf
13+
import org.usvm.isAllocatedConcreteHeapRef
14+
import org.usvm.machine.TsContext
15+
import org.usvm.machine.TsSizeSort
16+
import org.usvm.machine.interpreter.TsStepScope
17+
import org.usvm.machine.types.mkFakeValue
18+
import org.usvm.sizeSort
19+
import org.usvm.types.first
20+
import org.usvm.util.mkArrayIndexLValue
21+
import org.usvm.util.mkArrayLengthLValue
22+
23+
internal fun TsExprResolver.handleArrayAccess(
24+
value: EtsArrayAccess,
25+
): UExpr<*>? = with(ctx) {
26+
// 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+
}
31+
val arrayRef = array.asExpr(addressSort)
32+
33+
// Check for undefined or null array access.
34+
checkUndefinedOrNullPropertyRead(scope, arrayRef, propertyName = "[]") ?: return null
35+
36+
// Resolve the index.
37+
val resolvedIndex = resolve(value.index) ?: return null
38+
check(resolvedIndex.sort == fp64Sort) {
39+
"Expected fp64 sort for index, got: ${resolvedIndex.sort}"
40+
}
41+
val index = resolvedIndex.asExpr(fp64Sort)
42+
43+
// Convert the index to a bit-vector.
44+
val bvIndex = mkFpToBvExpr(
45+
roundingMode = fpRoundingModeSortDefaultValue(),
46+
value = index,
47+
bvSize = sizeSort.sizeBits.toInt(),
48+
isSigned = true,
49+
).asExpr(sizeSort)
50+
51+
// Determine the array type.
52+
val arrayType = if (isAllocatedConcreteHeapRef(arrayRef)) {
53+
scope.calcOnState { memory.typeStreamOf(arrayRef).first() }
54+
} else {
55+
value.array.type
56+
}
57+
check(arrayType is EtsArrayType) {
58+
"Expected EtsArrayType, got: ${value.array.type}"
59+
}
60+
61+
// Read the array element.
62+
readArray(scope, arrayRef, bvIndex, arrayType)
63+
}
64+
65+
fun TsContext.readArray(
66+
scope: TsStepScope,
67+
array: UHeapRef,
68+
index: UExpr<TsSizeSort>,
69+
arrayType: EtsArrayType,
70+
): UExpr<*>? {
71+
// Read the array length.
72+
val length = scope.calcOnState {
73+
val lengthLValue = mkArrayLengthLValue(array, arrayType)
74+
memory.read(lengthLValue)
75+
}
76+
77+
// Check for out-of-bounds access.
78+
checkNegativeIndexRead(scope, index) ?: return null
79+
checkReadingInRange(scope, index, length) ?: return null
80+
81+
// Determine the element sort.
82+
val sort = typeToSort(arrayType.elementType)
83+
84+
// If the element type is known, we can read it directly.
85+
if (sort !is TsUnresolvedSort) {
86+
val lValue = mkArrayIndexLValue(
87+
sort = sort,
88+
ref = array,
89+
index = index,
90+
type = arrayType,
91+
)
92+
return scope.calcOnState { memory.read(lValue) }
93+
}
94+
95+
// Concrete arrays with the unresolved sort should consist of fake objects only.
96+
if (array is UConcreteHeapRef) {
97+
// Read a fake object from the array.
98+
val lValue = mkArrayIndexLValue(
99+
sort = addressSort,
100+
ref = array,
101+
index = index,
102+
type = arrayType,
103+
)
104+
return scope.calcOnState { memory.read(lValue) }
105+
}
106+
107+
// If the element type is unresolved, we need to create a fake object
108+
// that can hold boolean, number, and reference values.
109+
// We read all three types from the array and combine them into a fake object.
110+
return scope.calcOnState {
111+
val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
112+
val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType)
113+
val bool = memory.read(boolLValue)
114+
115+
val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
116+
val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType)
117+
val fp = memory.read(fpLValue)
118+
119+
val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
120+
val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType)
121+
val ref = memory.read(refLValue)
122+
123+
// If the read reference is already a fake object, we can return it directly.
124+
// Otherwise, we need to create a new fake object and write it back to the memory.
125+
// TODO: Think about the type constraint to get a consistent array resolution later
126+
if (ref.isFakeObject()) {
127+
ref
128+
} else {
129+
val fakeObj = mkFakeValue(scope, bool, fp, ref)
130+
lValuesToAllocatedFakeObjects += refLValue to fakeObj
131+
memory.write(refLValue, fakeObj, guard = trueExpr)
132+
fakeObj
133+
}
134+
}
135+
}

0 commit comments

Comments
 (0)