Skip to content

Commit b71e504

Browse files
CaelmBleiddCaelmBleidd
committed
Review fixes
1 parent 109c89b commit b71e504

File tree

5 files changed

+65
-31
lines changed

5 files changed

+65
-31
lines changed

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

Lines changed: 55 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -9,29 +9,32 @@ import org.usvm.api.initializeArrayLength
99
import org.usvm.api.memcpy
1010
import org.usvm.api.typeStreamOf
1111
import org.usvm.isAllocatedConcreteHeapRef
12+
import org.usvm.machine.expr.TsExprApproximationResult.Companion.create
1213
import org.usvm.sizeSort
1314
import org.usvm.types.firstOrNull
1415
import org.usvm.util.mkArrayIndexLValue
1516
import org.usvm.util.mkArrayLengthLValue
1617

17-
fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
18-
val resolvedInstance = scope.calcOnState { resolve(expr.instance)?.asExpr(ctx.addressSort) } ?: return null
18+
fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): TsExprApproximationResult = with(ctx) {
19+
val resolvedInstance = scope.calcOnState { resolve(expr.instance)?.asExpr(ctx.addressSort) }
20+
?: return TsExprApproximationResult.ResolveFailure
1921

2022
if (expr.instance.name == "Number") {
2123
if (expr.callee.name == "isNaN") {
2224
check(expr.args.size == 1) { "Number.isNaN should have one argument" }
23-
return resolveAfterResolved(expr.args.single()) { arg ->
25+
val expr = resolveAfterResolved(expr.args.single()) { arg ->
2426
handleNumberIsNaN(arg)
2527
}
28+
return create(expr)
2629
}
2730
}
2831

2932
if (expr.instance.name == "Logger") {
30-
return mkUndefinedValue()
33+
return create(mkUndefinedValue())
3134
}
3235

3336
if (expr.callee.name == "toString") {
34-
return mkStringConstant("I am a string", scope)
37+
return create(mkStringConstant("I am a string", scope))
3538
}
3639

3740
val instanceType = if (isAllocatedConcreteHeapRef(resolvedInstance)) {
@@ -47,7 +50,7 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
4750

4851
// push
4952
if (expr.callee.name == "push") {
50-
return scope.calcOnState {
53+
val expr = scope.calcOnState {
5154
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
5255
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
5356
val length = memory.read(lengthLValue)
@@ -63,28 +66,46 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
6366
memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr)
6467
newLength
6568
}
69+
70+
return create(expr)
6671
}
6772

6873
// fill
6974
if (expr.callee.name == "fill") {
70-
return scope.calcOnState {
75+
val expr = scope.calcOnState {
7176
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
7277
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
7378
val length = memory.read(lengthLValue)
7479
val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
7580

7681
val artificialArray = memory.allocConcrete(instanceType)
7782
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)
83+
memory.initializeArray(
84+
artificialArray,
85+
instanceType,
86+
elementTypeSort,
87+
sizeSort,
88+
Array(10_000) { resolvedArg.asExpr(elementTypeSort) }.asSequence()
89+
)
90+
memory.memcpy(
91+
artificialArray,
92+
resolvedInstance,
93+
instanceType,
94+
elementTypeSort,
95+
0.toBv(),
96+
0.toBv(),
97+
length
98+
)
8099

81100
resolvedInstance
82101
}
102+
103+
return create(expr)
83104
}
84105

85106
// unshift
86107
if (expr.callee.name == "unshift") {
87-
return scope.calcOnState {
108+
val expr = scope.calcOnState {
88109
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
89110
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
90111
val length = memory.read(lengthLValue)
@@ -109,10 +130,12 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
109130
memory.write(zeroIndexLValue, resolvedArg.asExpr(zeroIndexLValue.sort), guard = ctx.trueExpr)
110131
newLength
111132
}
133+
134+
return create(expr)
112135
}
113136

114137
if (expr.callee.name == "shift") {
115-
return scope.calcOnState {
138+
val expr = scope.calcOnState {
116139
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
117140
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
118141
val length = memory.read(lengthLValue)
@@ -136,10 +159,12 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
136159
memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
137160
result
138161
}
162+
163+
return create(expr)
139164
}
140165

141166
if (expr.callee.name == "pop") {
142-
return scope.calcOnState {
167+
val expr = scope.calcOnState {
143168
val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
144169
val lengthLValue = mkArrayLengthLValue(resolvedInstance, instanceType)
145170
val length = memory.read(lengthLValue)
@@ -156,8 +181,25 @@ fun TsExprResolver.tryApproximateInstanceCall(expr: EtsInstanceCallExpr): UExpr<
156181
)
157182
memory.read(indexLValue)
158183
}
184+
185+
return create(expr)
159186
}
160187
}
161188

162-
return null
189+
return TsExprApproximationResult.NoApproximation
190+
}
191+
192+
sealed class TsExprApproximationResult {
193+
data class SuccessfulApproximation(val expr: UExpr<*>) : TsExprApproximationResult()
194+
data object NoApproximation : TsExprApproximationResult()
195+
data object ResolveFailure : TsExprApproximationResult()
196+
197+
companion object {
198+
fun create(expr: UExpr<*>?): TsExprApproximationResult {
199+
return when {
200+
expr != null -> SuccessfulApproximation(expr)
201+
else -> ResolveFailure
202+
}
203+
}
204+
}
163205
}

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -535,7 +535,11 @@ class TsExprResolver(
535535

536536
override fun visit(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
537537
val result = tryApproximateInstanceCall(expr)
538-
if (result != null) return@with result
538+
when (result) {
539+
is TsExprApproximationResult.SuccessfulApproximation -> return result.expr
540+
is TsExprApproximationResult.ResolveFailure -> return null
541+
is TsExprApproximationResult.NoApproximation -> {}
542+
}
539543

540544
return when (val result = scope.calcOnState { methodResult }) {
541545
is TsMethodResult.Success -> {

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

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -127,10 +127,6 @@ class TsInterpreter(
127127
// if no call, visit
128128

129129
try {
130-
if ("shift" in stmt.toString()) {
131-
let{}
132-
}
133-
134130
when (stmt) {
135131
is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt)
136132
is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt)

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

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -55,14 +55,11 @@ class ArraysMethods : TsMethodTestRunner() {
5555
@Test
5656
fun testPushMethod() {
5757
val method = getMethod(className, "pushMethod")
58-
discoverProperties<TsTestValue.TsBoolean, TsTestValue>(
58+
discoverProperties<TsTestValue.TsArray<TsTestValue.TsNumber>>(
5959
method = method,
60-
{ x, r -> x.value && r is TsTestValue.TsNumber && r.number == 4.0 },
61-
{ x, r ->
62-
!x.value
63-
&& r is TsTestValue.TsArray<*>
64-
&& r.values.map { (it as TsTestValue.TsNumber).number } == listOf(1.0, 2.0, 3.0, 4.0)
65-
},
60+
invariants = arrayOf(
61+
{ r -> r.values.map { it.number } == listOf(1.0, 2.0, 3.0, 4.0) },
62+
)
6663
)
6764
}
6865

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

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,14 +30,9 @@ class ArraysMethods {
3030
return arr;
3131
}
3232

33-
pushMethod(x: boolean) {
33+
pushMethod() {
3434
const arr = [1, 2, 3];
3535
arr.push(4);
36-
37-
if (x) {
38-
return arr[arr.length - 1]; // Return the last element after push
39-
}
40-
4136
return arr;
4237
}
4338

0 commit comments

Comments
 (0)