Skip to content

Commit 4dccb2d

Browse files
CaelmBleiddLipen
CaelmBleidd
and
Lipen
authored
Support arrays containing values of different types (#258)
 --------- Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>
1 parent 02e58ea commit 4dccb2d

File tree

8 files changed

+212
-48
lines changed

8 files changed

+212
-48
lines changed

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

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

33
import io.ksmt.sort.KFp64Sort
4+
import io.ksmt.utils.asExpr
45
import org.jacodb.ets.base.EtsBooleanType
56
import org.jacodb.ets.base.EtsNullType
67
import org.jacodb.ets.base.EtsNumberType
@@ -20,6 +21,8 @@ import org.usvm.USort
2021
import org.usvm.collection.field.UFieldLValue
2122
import org.usvm.machine.expr.TsUndefinedSort
2223
import org.usvm.machine.expr.TsUnresolvedSort
24+
import org.usvm.machine.interpreter.TsStepScope
25+
import org.usvm.machine.types.FakeType
2326
import kotlin.contracts.ExperimentalContracts
2427
import kotlin.contracts.contract
2528

@@ -60,6 +63,40 @@ class TsContext(
6063
return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET
6164
}
6265

66+
fun UExpr<out USort>.toFakeObject(scope: TsStepScope): UConcreteHeapRef {
67+
if (isFakeObject()) {
68+
return this
69+
}
70+
71+
val ref = createFakeObjectRef()
72+
73+
scope.calcOnState {
74+
when (sort) {
75+
boolSort -> {
76+
val lvalue = getIntermediateBoolLValue(ref.address)
77+
memory.write(lvalue, this@toFakeObject.asExpr(boolSort), guard = trueExpr)
78+
memory.types.allocate(ref.address, FakeType.fromBool(this@TsContext))
79+
}
80+
81+
fp64Sort -> {
82+
val lValue = getIntermediateFpLValue(ref.address)
83+
memory.write(lValue, this@toFakeObject.asExpr(fp64Sort), guard = trueExpr)
84+
memory.types.allocate(ref.address, FakeType.fromFp(this@TsContext))
85+
}
86+
87+
addressSort -> {
88+
val lValue = getIntermediateRefLValue(ref.address)
89+
memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
90+
memory.write(lValue, this@toFakeObject.asExpr(addressSort), guard = trueExpr)
91+
}
92+
93+
else -> TODO("Not yet supported")
94+
}
95+
}
96+
97+
return ref
98+
}
99+
63100
fun createFakeObjectRef(): UConcreteHeapRef {
64101
val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
65102
return mkConcreteHeapRef(address)

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

Lines changed: 20 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ import mu.KotlinLogging
66
import org.jacodb.ets.base.EtsAddExpr
77
import org.jacodb.ets.base.EtsAndExpr
88
import org.jacodb.ets.base.EtsArrayAccess
9+
import org.jacodb.ets.base.EtsArrayType
910
import org.jacodb.ets.base.EtsAwaitExpr
1011
import org.jacodb.ets.base.EtsBinaryExpr
1112
import org.jacodb.ets.base.EtsBitAndExpr
@@ -63,7 +64,6 @@ import org.jacodb.ets.base.EtsTypeOfExpr
6364
import org.jacodb.ets.base.EtsUnaryExpr
6465
import org.jacodb.ets.base.EtsUnaryPlusExpr
6566
import org.jacodb.ets.base.EtsUndefinedConstant
66-
import org.jacodb.ets.base.EtsUnknownType
6767
import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
6868
import org.jacodb.ets.base.EtsValue
6969
import org.jacodb.ets.base.EtsVoidExpr
@@ -78,6 +78,7 @@ import org.usvm.USort
7878
import org.usvm.api.allocateArray
7979
import org.usvm.api.makeSymbolicPrimitive
8080
import org.usvm.collection.array.UArrayIndexLValue
81+
import org.usvm.collection.array.length.UArrayLengthLValue
8182
import org.usvm.collection.field.UFieldLValue
8283
import org.usvm.machine.TsContext
8384
import org.usvm.machine.interpreter.TsStepScope
@@ -497,20 +498,22 @@ class TsExprResolver(
497498

498499
// region ACCESS
499500

500-
override fun visit(value: EtsArrayAccess): UExpr<out USort>? {
501+
override fun visit(value: EtsArrayAccess): UExpr<out USort>? = with(ctx) {
501502
val instance = resolve(value.array)?.asExpr(ctx.addressSort) ?: return null
502503
val index = resolve(value.index)?.asExpr(ctx.fp64Sort) ?: return null
503-
val bvIndex = ctx.mkFpToBvExpr(
504-
roundingMode = ctx.fpRoundingModeSortDefaultValue(),
504+
val bvIndex = mkFpToBvExpr(
505+
roundingMode = fpRoundingModeSortDefaultValue(),
505506
value = index,
506507
bvSize = 32,
507508
isSigned = true
508509
)
509510

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)
511+
val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type)
512+
val expr = scope.calcOnState { memory.read(lValue) }
513+
514+
check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
512515

513-
return scope.calcOnState { memory.read(lValue) }
516+
return expr
514517
}
515518

516519
private fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
@@ -535,7 +538,16 @@ class TsExprResolver(
535538

536539
checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
537540

538-
// TODO: checkNullPointer(instanceRef)
541+
// TODO It is a hack for array's length
542+
if (value.instance.type is EtsArrayType && value.field.name == "length") {
543+
val lValue = UArrayLengthLValue(instanceRef, value.instance.type, ctx.sizeSort)
544+
val expr = scope.calcOnState { memory.read(lValue) }
545+
546+
check(expr.sort == ctx.sizeSort)
547+
548+
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true)
549+
}
550+
539551
val fieldType = scene.fieldLookUp(value.field).type
540552
val sort = typeToSort(fieldType)
541553
val lValue = UFieldLValue(sort, instanceRef, value.field.name)

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

Lines changed: 23 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ import org.usvm.StepScope
2424
import org.usvm.UInterpreter
2525
import org.usvm.api.targets.TsTarget
2626
import org.usvm.collection.array.UArrayIndexLValue
27+
import org.usvm.collection.array.length.UArrayLengthLValue
2728
import org.usvm.collections.immutable.internal.MutabilityOwnership
2829
import org.usvm.forkblacklists.UForkBlackList
2930
import org.usvm.machine.TsApplicationGraph
@@ -38,6 +39,7 @@ import org.usvm.machine.state.newStmt
3839
import org.usvm.machine.state.parametersWithThisCount
3940
import org.usvm.machine.state.returnValue
4041
import org.usvm.memory.URegisterStackLValue
42+
import org.usvm.sizeSort
4143
import org.usvm.targets.UTargetsSet
4244
import org.usvm.utils.ensureSat
4345

@@ -123,11 +125,11 @@ class TsInterpreter(
123125
}
124126
}
125127

126-
private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) {
128+
private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) {
127129
val exprResolver = exprResolverWithScope(scope)
128130
val expr = exprResolver.resolve(stmt.rhv) ?: return
129131

130-
check(expr.sort != ctx.unresolvedSort) {
132+
check(expr.sort != unresolvedSort) {
131133
"A value of the unresolved sort should never be returned from `resolve` function"
132134
}
133135

@@ -138,31 +140,33 @@ class TsInterpreter(
138140
saveSortForLocal(idx, expr.sort)
139141

140142
val lValue = URegisterStackLValue(expr.sort, idx)
141-
memory.write(lValue, expr.asExpr(lValue.sort), guard = ctx.trueExpr)
143+
memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
142144
}
143145

144146
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
147+
val instance = exprResolver.resolve(lhv.array)?.asExpr(addressSort) ?: return@doWithState
148+
val index = exprResolver.resolve(lhv.index)?.asExpr(fp64Sort) ?: return@doWithState
148149

149150
// TODO fork on floating point field
150-
val bvIndex = ctx.mkFpToBvExpr(
151-
roundingMode = ctx.fpRoundingModeSortDefaultValue(),
151+
val bvIndex = mkFpToBvExpr(
152+
roundingMode = fpRoundingModeSortDefaultValue(),
152153
value = index,
153154
bvSize = 32,
154155
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-
}
156+
).asExpr(sizeSort)
157+
158+
val lengthLValue = UArrayLengthLValue(instance, lhv.array.type, sizeSort)
159+
val currentLength = memory.read(lengthLValue).asExpr(sizeSort)
160+
161+
val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength)
162+
val newLength = mkIte(condition, mkBvAddExpr(bvIndex, mkBv(1)), currentLength)
163+
164+
memory.write(lengthLValue, newLength, guard = trueExpr)
165+
166+
val fakeExpr = expr.toFakeObject(scope)
167+
168+
val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, lhv.array.type)
169+
memory.write(lValue, fakeExpr, guard = trueExpr)
166170
}
167171

168172
else -> TODO("Not yet implemented")

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

Lines changed: 51 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -421,9 +421,57 @@ sealed interface TsBinaryOperator {
421421
scope: TsStepScope,
422422
): UExpr<out USort> {
423423
check(lhs.isFakeObject() || rhs.isFakeObject())
424-
// TODO: delegating to '==' is not correct in general case
425-
return with(Eq) {
426-
resolveFakeObject(lhs, rhs, scope)
424+
425+
return scope.calcOnState {
426+
when {
427+
lhs.isFakeObject() && rhs.isFakeObject() -> {
428+
val lhsType = memory.typeStreamOf(lhs).single() as FakeType
429+
val rhsType = memory.typeStreamOf(rhs).single() as FakeType
430+
431+
scope.assert(
432+
mkAnd(
433+
lhsType.boolTypeExpr eq rhsType.boolTypeExpr,
434+
lhsType.fpTypeExpr eq rhsType.fpTypeExpr,
435+
// TODO support type equality
436+
lhsType.refTypeExpr eq rhsType.refTypeExpr
437+
)
438+
)
439+
}
440+
441+
lhs.isFakeObject() -> {
442+
val lhsType = memory.typeStreamOf(lhs).single() as FakeType
443+
444+
val condition = when (rhs.sort) {
445+
boolSort -> lhsType.boolTypeExpr
446+
fp64Sort -> lhsType.fpTypeExpr
447+
// TODO support type equality
448+
addressSort -> lhsType.refTypeExpr
449+
else -> error("Unsupported sort ${rhs.sort}")
450+
}
451+
452+
scope.assert(condition)
453+
}
454+
455+
rhs.isFakeObject() -> {
456+
val rhsType = memory.typeStreamOf(rhs).single() as FakeType
457+
458+
scope.assert(rhsType.mkExactlyOneTypeConstraint(ctx))
459+
460+
val condition = when (lhs.sort) {
461+
boolSort -> rhsType.boolTypeExpr
462+
fp64Sort -> rhsType.fpTypeExpr
463+
// TODO support type equality
464+
addressSort -> rhsType.refTypeExpr
465+
else -> error("Unsupported sort ${lhs.sort}")
466+
}
467+
468+
scope.assert(condition)
469+
}
470+
}
471+
472+
return@calcOnState with(Eq) {
473+
resolveFakeObject(lhs, rhs, scope)
474+
}
427475
}
428476
}
429477

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

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,20 @@ class FakeType(
2727
mkOr(boolTypeExpr, fpTypeExpr, refTypeExpr),
2828
)
2929
}
30+
31+
companion object {
32+
fun fromBool(ctx: TsContext): FakeType {
33+
return FakeType(ctx.mkTrue(), ctx.mkFalse(), ctx.mkFalse())
34+
}
35+
36+
fun fromFp(ctx: TsContext): FakeType {
37+
return FakeType(ctx.mkFalse(), ctx.mkTrue(), ctx.mkFalse())
38+
}
39+
40+
fun fromRef(ctx: TsContext): FakeType {
41+
return FakeType(ctx.mkFalse(), ctx.mkFalse(), ctx.mkTrue())
42+
}
43+
}
3044
}
3145

32-
data class ExprWithTypeConstraint<T : USort>(val constraint: UBoolExpr, val expr: UExpr<T>)
46+
data class ExprWithTypeConstraint<T : USort>(val constraint: UBoolExpr, val expr: UExpr<T>)

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

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

33
import org.jacodb.ets.model.EtsScene
44
import org.jacodb.ets.utils.loadEtsFileAutoConvert
5-
import org.junit.jupiter.api.Disabled
65
import org.junit.jupiter.api.Test
76
import org.usvm.api.TsValue
87
import org.usvm.util.TsMethodTestRunner
@@ -59,7 +58,6 @@ class Arrays : TsMethodTestRunner() {
5958
}
6059

6160
@Test
62-
@Disabled("Arrays should contain only fake objects")
6361
fun testCreateMixedArray() {
6462
val method = getMethod("Arrays", "createMixedArray")
6563
discoverProperties<TsValue.TsArray<*>>(
@@ -75,7 +73,7 @@ class Arrays : TsMethodTestRunner() {
7573
}
7674

7775
@Test
78-
fun testCreateArrayOfUnknown() {
76+
fun testCreateArrayOfUnknownValues() {
7977
val method = getMethod("Arrays", "createArrayOfUnknownValues")
8078
discoverProperties<TsValue, TsValue, TsValue, TsValue.TsArray<*>>(
8179
method = method,
@@ -89,18 +87,43 @@ class Arrays : TsMethodTestRunner() {
8987
}
9088

9189
@Test
92-
@Disabled("Arrays should contain only fake objects")
9390
fun testCreateArrayOfNumbersAndPutDifferentTypes() {
9491
val method = getMethod("Arrays", "createArrayOfNumbersAndPutDifferentTypes")
9592
discoverProperties<TsValue.TsArray<*>>(
9693
method = method,
9794
{ r ->
9895
val values = r.values
9996
values.size == 3
100-
&& (values[0] as TsValue.TsClass).properties.size == 1
97+
&& values[0] is TsValue.TsNull
10198
&& (values[1] as TsValue.TsBoolean).value
10299
&& values[2] is TsValue.TsUndefined
103100
},
104101
)
105102
}
103+
104+
@Test
105+
fun testAllocatedArrayLengthExpansion() {
106+
val method = getMethod("Arrays", "allocatedArrayLengthExpansion")
107+
discoverProperties<TsValue.TsArray<*>>(
108+
method = method,
109+
{ r ->
110+
r.values.size == 6
111+
&& (r.values[0] as TsValue.TsNumber).number == 1.0
112+
&& (r.values[1] as TsValue.TsNumber).number == 2.0
113+
&& (r.values[2] as TsValue.TsNumber).number == 3.0
114+
&& r.values[3] is TsValue.TsUndefined
115+
&& r.values[4] is TsValue.TsUndefined
116+
&& (r.values[5] as TsValue.TsNumber).number == 5.0
117+
}
118+
)
119+
}
120+
121+
@Test
122+
fun testWriteInTheIndexEqualToLength() {
123+
val method = getMethod("Arrays", "writeInTheIndexEqualToLength")
124+
discoverProperties<TsValue.TsArray<TsValue.TsNumber>>(
125+
method = method,
126+
{ r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0, 4.0) },
127+
)
128+
}
106129
}

0 commit comments

Comments
 (0)