Skip to content

Commit bdc0374

Browse files
LipenLipen
committed
Fix array methods
1 parent d4564b6 commit bdc0374

File tree

3 files changed

+97
-77
lines changed

3 files changed

+97
-77
lines changed

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

Lines changed: 36 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,12 @@ private fun TsExprResolver.handleArrayPush(
259259
memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
260260

261261
// Return the new length of the array (as per ECMAScript spec for Array.push)
262-
newLength
262+
mkBvToFpExpr(
263+
sort = fp64Sort,
264+
roundingMode = fpRoundingModeSortDefaultValue(),
265+
value = newLength.asExpr(sizeSort),
266+
signed = true,
267+
)
263268
}
264269
}
265270

@@ -288,18 +293,22 @@ private fun TsExprResolver.handleArrayPop(
288293
// It is not an error/exception to pop from an empty array!
289294
// If the array is empty, `pop` returns `undefined`.
290295
val newLength = mkBvSubExpr(length, 1.toBv())
291-
memory.write(lengthLValue, newLength, guard = trueExpr)
292-
293-
// TODO: return `undefined` if the array is empty
294296

295-
// Read the last element of the array and return it
297+
// Read the last element of the array (to be removed)
296298
val lastIndexLValue = mkArrayIndexLValue(
297299
sort = elementSort,
298300
ref = instance,
299301
index = newLength,
300302
type = arrayType,
301303
)
302-
memory.read(lastIndexLValue)
304+
// TODO: If the array is empty, return `undefined` instead of the last element.
305+
val removedElement = memory.read(lastIndexLValue)
306+
307+
// Update the length of the array (AFTER reading the last element)
308+
memory.write(lengthLValue, newLength, guard = trueExpr)
309+
310+
// Return the removed element
311+
removedElement
303312
}
304313
}
305314

@@ -373,11 +382,24 @@ private fun TsExprResolver.handleArrayShift(
373382
}
374383

375384
scope.calcOnState {
385+
// Store the first element of the array (to be removed)
386+
// TODO: If the array is empty, return `undefined` instead of the first element.
387+
val firstIndexLValue = mkArrayIndexLValue(
388+
sort = elementSort,
389+
ref = array,
390+
index = 0.toBv().asExpr(sizeSort),
391+
type = arrayType,
392+
)
393+
val firstElement = memory.read(firstIndexLValue)
394+
376395
// Read the length of the array
377396
val lengthLValue = mkArrayLengthLValue(array, arrayType)
378397
val length = memory.read(lengthLValue)
379398

380399
// Decrease the length of the array
400+
// TODO: Only decrease the length if it is not zero.
401+
// It is not an error/exception to shift an empty array!
402+
// If the array is empty, `shift` returns `undefined`.
381403
val newLength = mkBvSubExpr(length, 1.toBv())
382404
memory.write(lengthLValue, newLength, guard = trueExpr)
383405

@@ -392,14 +414,8 @@ private fun TsExprResolver.handleArrayShift(
392414
length = newLength,
393415
)
394416

395-
// Read the first element of the array and return it
396-
val firstIndexLValue = mkArrayIndexLValue(
397-
sort = elementSort,
398-
ref = array,
399-
index = 0.toBv().asExpr(sizeSort),
400-
type = arrayType,
401-
)
402-
memory.read(firstIndexLValue)
417+
// Return the removed element
418+
firstElement
403419
}
404420
}
405421

@@ -452,6 +468,11 @@ private fun TsExprResolver.handleArrayUnshift(
452468
memory.write(startIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
453469

454470
// Return the new length of the array (as per ECMAScript spec for Array.unshift)
455-
newLength
471+
mkBvToFpExpr(
472+
sort = fp64Sort,
473+
roundingMode = fpRoundingModeSortDefaultValue(),
474+
value = newLength.asExpr(sizeSort),
475+
signed = true,
476+
)
456477
}
457478
}

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

Lines changed: 36 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -11,29 +11,19 @@ class ArraysMethods : TsMethodTestRunner() {
1111
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "arrays")
1212

1313
@Test
14-
fun testShiftMethod() {
15-
val method = getMethod(className, "shiftMethod")
14+
fun testPushMethod() {
15+
val method = getMethod(className, "pushMethod")
1616
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
1717
method = method,
18-
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 1.0 },
1918
{ x, r ->
20-
!x.value
21-
&& r is TsTestValue.TsArray<*>
22-
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(2.0, 3.0)
19+
x.value
20+
&& r is TsTestValue.TsNumber
21+
&& (r.number == 4.0)
2322
},
24-
)
25-
}
26-
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 },
3323
{ x, r ->
3424
!x.value
3525
&& r is TsTestValue.TsArray<*>
36-
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(0.0, 1.0, 2.0, 3.0)
26+
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(10.0, 20.0, 30.0, 5.0)
3727
},
3828
)
3929
}
@@ -43,36 +33,55 @@ class ArraysMethods : TsMethodTestRunner() {
4333
val method = getMethod(className, "popMethod")
4434
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
4535
method = method,
46-
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 3.0 },
36+
{ x, r ->
37+
x.value
38+
&& r is TsTestValue.TsNumber
39+
&& (r.number == 30.0)
40+
},
4741
{ x, r ->
4842
!x.value
4943
&& r is TsTestValue.TsArray<*>
50-
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(1.0, 2.0)
44+
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(10.0, 20.0)
5145
},
5246
)
5347
}
5448

5549
@Test
56-
fun testPushMethod() {
57-
val method = getMethod(className, "pushMethod")
50+
fun testFillMethod() {
51+
val method = getMethod(className, "fillMethod")
5852
discoverProperties<TsTestValue.TsArray<TsTestValue.TsNumber>>(
5953
method = method,
60-
invariants = arrayOf(
61-
{ r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0, 4.0) },
62-
)
54+
{ r -> r.values.map { it.number } == listOf(7.0, 7.0, 7.0) },
6355
)
6456
}
6557

6658
@Test
67-
fun testFillMethod() {
68-
val method = getMethod(className, "fillMethod")
59+
fun testShiftMethod() {
60+
val method = getMethod(className, "shiftMethod")
61+
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
62+
method = method,
63+
{ x, r ->
64+
x.value
65+
&& r is TsTestValue.TsNumber
66+
&& (r.number == 10.0) },
67+
{ x, r ->
68+
!x.value
69+
&& r is TsTestValue.TsArray<*>
70+
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(20.0, 30.0)
71+
},
72+
)
73+
}
74+
75+
@Test
76+
fun testUnshiftMethod() {
77+
val method = getMethod(className, "unshiftMethod")
6978
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
7079
method = method,
71-
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 7.0 },
80+
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 4.0 },
7281
{ x, r ->
7382
!x.value
7483
&& r is TsTestValue.TsArray<*>
75-
&& r.values.all { (it as TsTestValue.TsNumber).number == 7.0 }
84+
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(3.0, 2.0, 9.0, 7.0)
7685
},
7786
)
7887
}

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

Lines changed: 25 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,47 +1,37 @@
1-
class ArraysMethods {
2-
shiftMethod(x: boolean) {
3-
const arr = [1, 2, 3];
4-
const firstElement = arr.shift();
5-
6-
if (x) {
7-
return firstElement;
8-
}
9-
10-
return arr;
11-
}
1+
// @ts-nocheck
2+
// noinspection JSUnusedGlobalSymbols
123

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;
4+
class ArraysMethods {
5+
pushMethod(x: boolean) {
6+
const arr = [10, 20, 30];
7+
const newLength = arr.push(5);
8+
if (x) return newLength; // 4
9+
return arr; // [10, 20, 30, 5]
2010
}
2111

2212
popMethod(x: boolean) {
23-
const arr = [1, 2, 3];
13+
const arr = [10, 20, 30];
2414
const lastElement = arr.pop();
25-
26-
if (x) {
27-
return lastElement;
28-
}
29-
30-
return arr;
15+
if (x) return lastElement; // 30
16+
return arr; // [10, 20]
3117
}
3218

33-
pushMethod() {
34-
const arr = [1, 2, 3];
35-
arr.push(4);
19+
fillMethod() {
20+
let arr = [10, 20, 30];
21+
arr.fill(7);
22+
return arr; // [7, 7, 7]
23+
}
24+
shiftMethod(x: boolean) {
25+
const arr = [10, 20, 30];
26+
const firstElement = arr.shift();
27+
if (x) return firstElement;
3628
return arr;
3729
}
3830

39-
fillMethod(x: boolean) {
40-
const arr = [1, 2, 3];
41-
arr.fill(7);
42-
if (x) {
43-
return arr[0];
44-
}
45-
return arr;
31+
unshiftMethod(x: boolean) {
32+
const arr = [2, 9, 7];
33+
let newLength = arr.unshift(3);
34+
if (x) return newLength; // 4
35+
return arr; // [3, 2, 9, 7]
4636
}
4737
}

0 commit comments

Comments
 (0)