Skip to content

Commit 109c89b

Browse files
CaelmBleiddCaelmBleidd
committed
Fill implementation
1 parent 2e9c85d commit 109c89b

File tree

5 files changed

+113
-28
lines changed

5 files changed

+113
-28
lines changed

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

Lines changed: 54 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,14 @@ package org.usvm.machine.expr
33
import io.ksmt.utils.asExpr
44
import org.jacodb.ets.model.EtsArrayType
55
import org.jacodb.ets.model.EtsInstanceCallExpr
6-
import org.jacodb.ets.model.EtsType
76
import org.usvm.UExpr
7+
import org.usvm.api.initializeArray
8+
import org.usvm.api.initializeArrayLength
89
import org.usvm.api.memcpy
910
import org.usvm.api.typeStreamOf
1011
import org.usvm.isAllocatedConcreteHeapRef
1112
import org.usvm.sizeSort
12-
import org.usvm.types.TypesResult
13+
import org.usvm.types.firstOrNull
1314
import org.usvm.util.mkArrayIndexLValue
1415
import org.usvm.util.mkArrayLengthLValue
1516

@@ -34,58 +35,95 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
3435
}
3536

3637
val instanceType = if (isAllocatedConcreteHeapRef(resolvedInstance)) {
37-
scope.calcOnState { (memory.typeStreamOf(resolvedInstance).take(1) as? TypesResult.SuccessfulTypesResult<EtsType>)?.types?.single() ?: expr.instance.type }
38+
scope.calcOnState {
39+
memory.typeStreamOf(resolvedInstance).firstOrNull() ?: expr.instance.type
40+
}
3841
} else {
3942
expr.instance.type
4043
}
4144

4245
if (instanceType is EtsArrayType) {
43-
val elementTypeSort = typeToSort(instanceType).takeIf { it !is TsUnresolvedSort } ?: ctx.addressSort
44-
// TODO write tests https://github.com/UnitTestBot/usvm/issues/300
46+
val elementTypeSort = typeToSort(instanceType.elementType).takeIf { it !is TsUnresolvedSort } ?: ctx.addressSort
47+
48+
// push
4549
if (expr.callee.name == "push") {
4650
return scope.calcOnState {
4751
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
48-
4952
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
5053
val length = memory.read(lengthLValue)
51-
5254
val newLength = mkBvAddExpr(length, 1.toBv())
5355
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
54-
5556
val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
56-
57-
// TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300
5857
val newIndexLValue = mkArrayIndexLValue(
5958
resolvedArg.sort,
6059
resolvedInstance,
6160
length,
6261
instanceType
6362
)
6463
memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr)
64+
newLength
65+
}
66+
}
6567

68+
// fill
69+
if (expr.callee.name == "fill") {
70+
return scope.calcOnState {
71+
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
72+
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
73+
val length = memory.read(lengthLValue)
74+
val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
75+
76+
val artificialArray = memory.allocConcrete(instanceType)
77+
memory.initializeArrayLength(artificialArray, instanceType, sizeSort, 10_000.toBv().asExpr(sizeSort))
78+
memory.initializeArray(artificialArray, instanceType, elementTypeSort, sizeSort, Array(10_000) { resolvedArg.asExpr(elementTypeSort) }.asSequence())
79+
memory.memcpy(artificialArray, resolvedInstance, instanceType, elementTypeSort, 0.toBv(), 0.toBv(), length)
80+
81+
resolvedInstance
82+
}
83+
}
84+
85+
// unshift
86+
if (expr.callee.name == "unshift") {
87+
return scope.calcOnState {
88+
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
89+
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
90+
val length = memory.read(lengthLValue)
91+
val newLength = mkBvAddExpr(length, 1.toBv())
92+
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
93+
val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
94+
memory.memcpy(
95+
srcRef = resolvedInstance,
96+
dstRef = resolvedInstance,
97+
type = instanceType,
98+
elementSort = elementTypeSort,
99+
fromSrc = 0.toBv().asExpr(sizeSort),
100+
fromDst = 1.toBv().asExpr(sizeSort),
101+
length = length,
102+
)
103+
val zeroIndexLValue = mkArrayIndexLValue(
104+
resolvedArg.sort,
105+
resolvedInstance,
106+
0.toBv().asExpr(sizeSort),
107+
instanceType
108+
)
109+
memory.write(zeroIndexLValue, resolvedArg.asExpr(zeroIndexLValue.sort), guard = ctx.trueExpr)
66110
newLength
67111
}
68112
}
69113

70114
if (expr.callee.name == "shift") {
71115
return scope.calcOnState {
72116
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
73-
74117
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
75118
val length = memory.read(lengthLValue)
76119
val newLength = mkBvSubExpr(length, 1.toBv())
77-
78120
val indexLValue = mkArrayIndexLValue(
79121
elementTypeSort,
80122
resolvedInstance,
81123
0.toBv().asExpr(sizeSort),
82124
instanceType
83125
)
84-
85-
// TODO add exception for empty array????
86-
87126
val result = memory.read(indexLValue)
88-
89127
memory.memcpy(
90128
srcRef = resolvedInstance,
91129
dstRef = resolvedInstance,
@@ -95,34 +133,27 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
95133
fromDst = 0.toBv().asExpr(sizeSort),
96134
length = newLength,
97135
)
98-
99136
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
100-
101137
result
102138
}
103139
}
104140

105141
if (expr.callee.name == "pop") {
106142
return scope.calcOnState {
107143
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
108-
109144
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
110145
val length = memory.read(lengthLValue)
111-
112146
if (length == 0.toBv().asExpr(sizeSort)) {
113147
return@calcOnState null // TODO throw exception?
114148
}
115-
116149
val newLength = mkBvSubExpr(length, 1.toBv())
117150
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
118-
119151
val indexLValue = mkArrayIndexLValue(
120152
elementTypeSort,
121153
resolvedInstance,
122154
newLength,
123155
instanceType
124156
)
125-
126157
memory.read(indexLValue)
127158
}
128159
}

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

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,10 @@ import org.usvm.UIteExpr
9090
import org.usvm.USort
9191
import org.usvm.api.evalTypeEquals
9292
import org.usvm.api.initializeArrayLength
93+
import org.usvm.api.typeStreamOf
9394
import org.usvm.dataflow.ts.infer.tryGetKnownType
9495
import org.usvm.dataflow.ts.util.type
96+
import org.usvm.isAllocatedConcreteHeapRef
9597
import org.usvm.machine.Constants
9698
import org.usvm.machine.TsConcreteMethodCallStmt
9799
import org.usvm.machine.TsContext
@@ -111,6 +113,7 @@ import org.usvm.machine.types.EtsAuxiliaryType
111113
import org.usvm.machine.types.mkFakeValue
112114
import org.usvm.memory.ULValue
113115
import org.usvm.sizeSort
116+
import org.usvm.types.first
114117
import org.usvm.util.EtsHierarchy
115118
import org.usvm.util.EtsPropertyResolution
116119
import org.usvm.util.createFakeField
@@ -718,8 +721,11 @@ class TsExprResolver(
718721
isSigned = true,
719722
).asExpr(sizeSort)
720723

721-
val arrayType = value.array.type as? EtsArrayType
722-
?: error("Expected EtsArrayType, but got ${value.array.type}")
724+
val arrayType = if (isAllocatedConcreteHeapRef(array)) {
725+
scope.calcOnState { memory.typeStreamOf(array).first() }
726+
} else {
727+
value.array.type
728+
} as? EtsArrayType ?: error("Expected EtsArrayType, got: ${value.array.type}")
723729
val sort = typeToSort(arrayType.elementType)
724730

725731
val lengthLValue = mkArrayLengthLValue(array, arrayType)

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,7 @@ import org.usvm.machine.types.toAuxiliaryType
7272
import org.usvm.sizeSort
7373
import org.usvm.targets.UTargetsSet
7474
import org.usvm.types.TypesResult
75+
import org.usvm.types.first
7576
import org.usvm.types.single
7677
import org.usvm.util.EtsPropertyResolution
7778
import org.usvm.util.mkArrayIndexLValue
@@ -525,8 +526,11 @@ class TsInterpreter(
525526

526527
// TODO: handle the case when `lhv.array.type` is NOT an array.
527528
// In this case, it could be created manually: `EtsArrayType(EtsUnknownType, 1)`.
528-
val arrayType = lhv.array.type as? EtsArrayType
529-
?: error("Expected EtsArrayType, got: ${lhv.array.type}")
529+
val arrayType = if (isAllocatedConcreteHeapRef(instance)) {
530+
scope.calcOnState { (memory.typeStreamOf(instance).first()) }
531+
} else {
532+
lhv.array.type
533+
} as? EtsArrayType ?: error("Expected EtsArrayType, got: ${lhv.array.type}")
530534
val lengthLValue = mkArrayLengthLValue(instance, arrayType)
531535
val currentLength = memory.read(lengthLValue)
532536

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

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,20 @@ class ArraysMethods : TsMethodTestRunner() {
2424
)
2525
}
2626

27+
@Test
28+
fun testUnshiftMethod() {
29+
val method = getMethod(className, "unshiftMethod")
30+
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
31+
method = method,
32+
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 0.0 },
33+
{ x, r ->
34+
!x.value
35+
&& r is TsTestValue.TsArray<*>
36+
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(0.0, 1.0, 2.0, 3.0)
37+
},
38+
)
39+
}
40+
2741
@Test
2842
fun testPopMethod() {
2943
val method = getMethod(className, "popMethod")
@@ -38,7 +52,6 @@ class ArraysMethods : TsMethodTestRunner() {
3852
)
3953
}
4054

41-
4255
@Test
4356
fun testPushMethod() {
4457
val method = getMethod(className, "pushMethod")
@@ -53,4 +66,17 @@ class ArraysMethods : TsMethodTestRunner() {
5366
)
5467
}
5568

69+
@Test
70+
fun testFillMethod() {
71+
val method = getMethod(className, "fillMethod")
72+
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
73+
method = method,
74+
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 7.0 },
75+
{ x, r ->
76+
!x.value
77+
&& r is TsTestValue.TsArray<*>
78+
&& r.values.all { (it as TsTestValue.TsNumber).number == 7.0 }
79+
},
80+
)
81+
}
5682
}

‎usvm-ts/src/test/resources/samples/arrays/ArraysMethods.ts

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,15 @@ class ArraysMethods {
1010
return arr;
1111
}
1212

13+
unshiftMethod(x: boolean) {
14+
const arr = [1, 2, 3];
15+
arr.unshift(0);
16+
if (x) {
17+
return arr[0];
18+
}
19+
return arr;
20+
}
21+
1322
popMethod(x: boolean) {
1423
const arr = [1, 2, 3];
1524
const lastElement = arr.pop();
@@ -31,4 +40,13 @@ class ArraysMethods {
3140

3241
return arr;
3342
}
43+
44+
fillMethod(x: boolean) {
45+
const arr = [1, 2, 3];
46+
arr.fill(7);
47+
if (x) {
48+
return arr[0];
49+
}
50+
return arr;
51+
}
3452
}

0 commit comments

Comments
 (0)