Skip to content

Commit df9c103

Browse files
CaelmBleiddLipen
CaelmBleidd
and
Lipen
authored
Add support for arrays (#256)
 --------- Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>
1 parent f8e9180 commit df9c103

File tree

9 files changed

+329
-57
lines changed

9 files changed

+329
-57
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ sealed interface TsValue {
5555
val properties: Map<String, TsValue>,
5656
) : TsValue
5757

58-
data class TsArray(
59-
val values: List<TsValue>,
58+
data class TsArray<T : TsValue>(
59+
val values: List<T>,
6060
) : TsValue
6161
}

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import org.jacodb.ets.base.EtsNumberType
77
import org.jacodb.ets.base.EtsRefType
88
import org.jacodb.ets.base.EtsType
99
import org.jacodb.ets.base.EtsUndefinedType
10+
import org.jacodb.ets.base.EtsUnionType
1011
import org.jacodb.ets.base.EtsUnknownType
1112
import org.jacodb.ets.model.EtsScene
1213
import org.usvm.UAddressSort
@@ -46,6 +47,7 @@ class TsContext(
4647
is EtsNullType -> addressSort
4748
is EtsUndefinedType -> addressSort
4849
is EtsUnknownType -> unresolvedSort
50+
is EtsUnionType -> unresolvedSort
4951
else -> TODO("Support all JacoDB types, encountered $type")
5052
}
5153

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

Lines changed: 55 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ import org.jacodb.ets.base.EtsTypeOfExpr
6363
import org.jacodb.ets.base.EtsUnaryExpr
6464
import org.jacodb.ets.base.EtsUnaryPlusExpr
6565
import org.jacodb.ets.base.EtsUndefinedConstant
66+
import org.jacodb.ets.base.EtsUnknownType
6667
import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
6768
import org.jacodb.ets.base.EtsValue
6869
import org.jacodb.ets.base.EtsVoidExpr
@@ -74,7 +75,9 @@ import org.usvm.UBoolSort
7475
import org.usvm.UExpr
7576
import org.usvm.UHeapRef
7677
import org.usvm.USort
78+
import org.usvm.api.allocateArray
7779
import org.usvm.api.makeSymbolicPrimitive
80+
import org.usvm.collection.array.UArrayIndexLValue
7881
import org.usvm.collection.field.UFieldLValue
7982
import org.usvm.machine.TsContext
8083
import org.usvm.machine.interpreter.TsStepScope
@@ -88,6 +91,7 @@ import org.usvm.machine.types.FakeType
8891
import org.usvm.machine.types.mkFakeValue
8992
import org.usvm.memory.ULValue
9093
import org.usvm.memory.URegisterStackLValue
94+
import org.usvm.sizeSort
9195
import org.usvm.util.fieldLookUp
9296
import org.usvm.util.throwExceptionWithoutStackFrameDrop
9397

@@ -494,8 +498,19 @@ class TsExprResolver(
494498
// region ACCESS
495499

496500
override fun visit(value: EtsArrayAccess): UExpr<out USort>? {
497-
logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
498-
error("Not supported $value")
501+
val instance = resolve(value.array)?.asExpr(ctx.addressSort) ?: return null
502+
val index = resolve(value.index)?.asExpr(ctx.fp64Sort) ?: return null
503+
val bvIndex = ctx.mkFpToBvExpr(
504+
roundingMode = ctx.fpRoundingModeSortDefaultValue(),
505+
value = index,
506+
bvSize = 32,
507+
isSigned = true
508+
)
509+
510+
val sort = if (value.type is EtsUnknownType) ctx.addressSort else ctx.typeToSort(value.type)
511+
val lValue = UArrayIndexLValue(sort, instance, bvIndex, value.array.type)
512+
513+
return scope.calcOnState { memory.read(lValue) }
499514
}
500515

501516
private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
@@ -546,9 +561,42 @@ class TsExprResolver(
546561
memory.allocConcrete(expr.type)
547562
}
548563

549-
override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? {
550-
logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
551-
error("Not supported $expr")
564+
override fun visit(expr: EtsNewArrayExpr): UExpr<out USort>? = with(ctx) {
565+
scope.calcOnState {
566+
val size = resolve(expr.size) ?: return@calcOnState null
567+
568+
if (size.sort != fp64Sort) {
569+
TODO()
570+
}
571+
572+
val bvSize = mkFpToBvExpr(
573+
fpRoundingModeSortDefaultValue(),
574+
size.asExpr(fp64Sort),
575+
bvSize = 32,
576+
isSigned = true
577+
)
578+
579+
val condition = mkAnd(
580+
mkEq(
581+
mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), bvSize, signed = true),
582+
size.asExpr(fp64Sort)
583+
),
584+
mkAnd(
585+
mkBvSignedLessOrEqualExpr(0.toBv(), bvSize.asExpr(bv32Sort)),
586+
mkBvSignedLessOrEqualExpr(bvSize, Int.MAX_VALUE.toBv().asExpr(bv32Sort))
587+
)
588+
)
589+
590+
scope.fork(
591+
condition,
592+
blockOnFalseState = allocateException(EtsStringType) // TODO incorrect exception type
593+
)
594+
595+
val address = memory.allocateArray(expr.type, sizeSort, bvSize)
596+
memory.types.allocate(address.address, expr.type)
597+
598+
address
599+
}
552600
}
553601

554602
override fun visit(expr: EtsLengthExpr): UExpr<out USort>? {
@@ -665,9 +713,8 @@ class TsSimpleValueResolver(
665713
mkUndefinedValue()
666714
}
667715

668-
override fun visit(value: EtsArrayAccess): UExpr<out USort> = with(ctx) {
669-
logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
670-
error("Not supported $value")
716+
override fun visit(value: EtsArrayAccess): UExpr<out USort>? = with(ctx) {
717+
error("Should not be called")
671718
}
672719

673720
override fun visit(value: EtsInstanceFieldRef): UExpr<out USort> = with(ctx) {

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

Lines changed: 36 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ package org.usvm.machine.interpreter
22

33
import io.ksmt.utils.asExpr
44
import mu.KotlinLogging
5+
import org.jacodb.ets.base.EtsArrayAccess
56
import org.jacodb.ets.base.EtsAssignStmt
67
import org.jacodb.ets.base.EtsCallStmt
78
import org.jacodb.ets.base.EtsGotoStmt
@@ -22,6 +23,7 @@ import org.usvm.StepResult
2223
import org.usvm.StepScope
2324
import org.usvm.UInterpreter
2425
import org.usvm.api.targets.TsTarget
26+
import org.usvm.collection.array.UArrayIndexLValue
2527
import org.usvm.collections.immutable.internal.MutabilityOwnership
2628
import org.usvm.forkblacklists.UForkBlackList
2729
import org.usvm.machine.TsApplicationGraph
@@ -130,11 +132,41 @@ class TsInterpreter(
130132
}
131133

132134
scope.doWithState {
133-
val idx = mapLocalToIdx(lastEnteredMethod, stmt.lhv)
134-
saveSortForLocal(idx, expr.sort)
135+
when (val lhv = stmt.lhv) {
136+
is EtsLocal -> {
137+
val idx = mapLocalToIdx(lastEnteredMethod, lhv)
138+
saveSortForLocal(idx, expr.sort)
135139

136-
val lValue = URegisterStackLValue(expr.sort, idx)
137-
memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
140+
val lValue = URegisterStackLValue(expr.sort, idx)
141+
memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
142+
}
143+
144+
is EtsArrayAccess -> {
145+
// TODO save sorts?
146+
val instance = exprResolver.resolve(lhv.array)?.asExpr(ctx.addressSort) ?: return@doWithState
147+
val index = exprResolver.resolve(lhv.index)?.asExpr(ctx.fp64Sort) ?: return@doWithState
148+
149+
// TODO fork on floating point field
150+
val bvIndex = ctx.mkFpToBvExpr(
151+
roundingMode = ctx.fpRoundingModeSortDefaultValue(),
152+
value = index,
153+
bvSize = 32,
154+
isSigned = true
155+
)
156+
157+
if (stmt.lhv.type == stmt.rhv.type) {
158+
val lValue = UArrayIndexLValue(expr.sort, instance, bvIndex, lhv.array.type)
159+
// TODO error with array values type
160+
memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
161+
} else {
162+
val lValue = UArrayIndexLValue(ctx.unresolvedSort, instance, bvIndex, lhv.array.type)
163+
// TODO create fake object, probably the type of the array should be modified as well
164+
memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
165+
}
166+
}
167+
168+
else -> TODO("Not yet implemented")
169+
}
138170

139171
val nextStmt = stmt.nextStmt ?: return@doWithState
140172
newStmt(nextStmt)

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

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
package org.usvm.samples
2+
3+
import org.jacodb.ets.model.EtsScene
4+
import org.jacodb.ets.utils.loadEtsFileAutoConvert
5+
import org.junit.jupiter.api.Disabled
6+
import org.junit.jupiter.api.Test
7+
import org.usvm.api.TsValue
8+
import org.usvm.util.TsMethodTestRunner
9+
import org.usvm.util.getResourcePath
10+
11+
class Arrays : TsMethodTestRunner() {
12+
override val scene: EtsScene = run {
13+
val name = "Arrays.ts"
14+
val path = getResourcePath("/samples/$name")
15+
val file = loadEtsFileAutoConvert(path)
16+
EtsScene(listOf(file))
17+
}
18+
19+
@Test
20+
fun testCreateConstantArrayOfNumbers() {
21+
val method = getMethod("Arrays", "createConstantArrayOfNumbers")
22+
discoverProperties<TsValue.TsNumber>(
23+
method = method,
24+
{ r -> r.number == 1.0 },
25+
invariants = arrayOf(
26+
{ r -> r.number != -1.0 }
27+
)
28+
)
29+
}
30+
31+
@Test
32+
fun testCreateAndReturnConstantArrayOfNumbers() {
33+
val method = getMethod("Arrays", "createAndReturnConstantArrayOfNumbers")
34+
discoverProperties<TsValue.TsArray<TsValue.TsNumber>>(
35+
method = method,
36+
{ r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0) },
37+
)
38+
}
39+
40+
@Test
41+
fun testCreateAndAccessArrayOfBooleans() {
42+
val method = getMethod("Arrays", "createAndAccessArrayOfBooleans")
43+
discoverProperties<TsValue.TsNumber>(
44+
method = method,
45+
{ r -> r.number == 1.0 },
46+
invariants = arrayOf(
47+
{ r -> r.number != -1.0 }
48+
)
49+
)
50+
}
51+
52+
@Test
53+
fun testCreateArrayOfBooleans() {
54+
val method = getMethod("Arrays", "createArrayOfBooleans")
55+
discoverProperties<TsValue.TsArray<TsValue.TsBoolean>>(
56+
method = method,
57+
{ r -> r.values.map { it.value } == listOf(true, false, true) },
58+
)
59+
}
60+
61+
@Test
62+
@Disabled("Arrays should contain only fake objects")
63+
fun testCreateMixedArray() {
64+
val method = getMethod("Arrays", "createMixedArray")
65+
discoverProperties<TsValue.TsArray<*>>(
66+
method = method,
67+
{ r ->
68+
if (r.values.size != 3) return@discoverProperties false
69+
val cond0 = r.values[0] is TsValue.TsNumber.TsDouble
70+
val cond1 = r.values[1] is TsValue.TsBoolean
71+
val cond2 = r.values[2] is TsValue.TsUndefined
72+
cond0 && cond1 && cond2
73+
},
74+
)
75+
}
76+
77+
@Test
78+
fun testCreateArrayOfUnknown() {
79+
val method = getMethod("Arrays", "createArrayOfUnknownValues")
80+
discoverProperties<TsValue, TsValue, TsValue, TsValue.TsArray<*>>(
81+
method = method,
82+
{ a, _, _, r -> r.values[0] == a && (a as TsValue.TsNumber).number == 1.1 },
83+
{ _, b, _, r -> r.values[1] == b && (b as TsValue.TsBoolean).value },
84+
{ _, _, c, r -> r.values[2] == c && c is TsValue.TsUndefined },
85+
invariants = arrayOf(
86+
{ a, b, c, r -> r.values == listOf(a, b, c) }
87+
)
88+
)
89+
}
90+
91+
@Test
92+
@Disabled("Arrays should contain only fake objects")
93+
fun testCreateArrayOfNumbersAndPutDifferentTypes() {
94+
val method = getMethod("Arrays", "createArrayOfNumbersAndPutDifferentTypes")
95+
discoverProperties<TsValue.TsArray<*>>(
96+
method = method,
97+
{ r ->
98+
val values = r.values
99+
values.size == 3
100+
&& (values[0] as TsValue.TsClass).properties.size == 1
101+
&& (values[1] as TsValue.TsBoolean).value
102+
&& values[2] is TsValue.TsUndefined
103+
},
104+
)
105+
}
106+
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ class MinValue : TsMethodTestRunner() {
2121
@Disabled
2222
fun testMinValue() {
2323
val method = getMethod("MinValue", "findMinValue")
24-
discoverProperties<TsValue.TsArray, TsValue.TsNumber>(
24+
discoverProperties<TsValue.TsArray<*>, TsValue.TsNumber>(
2525
method,
2626
)
2727
}

‎usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt‎

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

33
import org.jacodb.ets.base.EtsAnyType
4+
import org.jacodb.ets.base.EtsArrayType
45
import org.jacodb.ets.base.EtsBooleanType
56
import org.jacodb.ets.base.EtsClassType
67
import org.jacodb.ets.base.EtsNullType
@@ -166,14 +167,18 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
166167
when (klass) {
167168
TsValue::class -> EtsAnyType
168169
TsValue.TsAny::class -> EtsAnyType
169-
TsValue.TsArray::class -> TODO()
170-
TsValue.TsBoolean::class -> EtsBooleanType
170+
171+
TsValue.TsArray::class -> {
172+
EtsArrayType(EtsAnyType, dimensions = 1) // TODO incorrect
173+
}
174+
171175
TsValue.TsClass::class -> {
172176
// TODO incorrect
173177
val signature = EtsClassSignature(it.toString(), EtsFileSignature.DEFAULT)
174178
EtsClassType(signature)
175179
}
176180

181+
TsValue.TsBoolean::class -> EtsBooleanType
177182
TsValue.TsString::class -> EtsStringType
178183
TsValue.TsNumber::class -> EtsNumberType
179184
TsValue.TsNumber.TsDouble::class -> EtsNumberType
@@ -184,6 +189,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
184189
// For untyped tests, not to limit objects serialized from models after type coercion.
185190
TsValue.TsUnknown::class -> EtsUnknownType
186191
TsValue.TsNull::class -> EtsNullType
192+
187193
TsValue.TsException::class -> {
188194
// TODO incorrect
189195
val signature = EtsClassSignature("Exception", EtsFileSignature.DEFAULT)

0 commit comments

Comments
 (0)