Skip to content

Commit e7bb414

Browse files
CaelmBleiddCaelmBleidd
committed
Fix tests
1 parent 271dfac commit e7bb414

File tree

4 files changed

+103
-55
lines changed

4 files changed

+103
-55
lines changed

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

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

33
import io.ksmt.sort.KFp64Sort
44
import io.ksmt.utils.asExpr
5+
import io.ksmt.utils.cast
56
import org.jacodb.ets.base.EtsBooleanType
67
import org.jacodb.ets.base.EtsNullType
78
import org.jacodb.ets.base.EtsNumberType
@@ -17,12 +18,15 @@ import org.usvm.UBv32Sort
1718
import org.usvm.UConcreteHeapRef
1819
import org.usvm.UContext
1920
import org.usvm.UExpr
21+
import org.usvm.UHeapRef
2022
import org.usvm.USort
2123
import org.usvm.collection.field.UFieldLValue
24+
import org.usvm.isTrue
2225
import org.usvm.machine.expr.TsUndefinedSort
2326
import org.usvm.machine.expr.TsUnresolvedSort
2427
import org.usvm.machine.interpreter.TsStepScope
2528
import org.usvm.machine.types.FakeType
29+
import org.usvm.types.single
2630
import kotlin.contracts.ExperimentalContracts
2731
import kotlin.contracts.contract
2832

@@ -102,6 +106,35 @@ class TsContext(
102106
return mkConcreteHeapRef(address)
103107
}
104108

109+
fun UHeapRef.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
110+
if (!isFakeObject()) return null
111+
112+
val type = scope.calcOnState {
113+
memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType
114+
}
115+
116+
return scope.calcOnState {
117+
when {
118+
type.boolTypeExpr.isTrue -> {
119+
val lValue = getIntermediateBoolLValue(address)
120+
memory.read(lValue).asExpr(boolSort)
121+
}
122+
123+
type.fpTypeExpr.isTrue -> {
124+
val lValue = getIntermediateFpLValue(address)
125+
memory.read(lValue).asExpr(fp64Sort)
126+
}
127+
128+
type.refTypeExpr.isTrue -> {
129+
val lValue = getIntermediateRefLValue(address)
130+
memory.read(lValue).asExpr(addressSort)
131+
}
132+
133+
else -> null
134+
}
135+
}
136+
}
137+
105138
fun mkUndefinedValue(): UExpr<UAddressSort> = undefinedValue
106139

107140
fun mkTsNullValue(): UConcreteHeapRef = nullValue

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

Lines changed: 19 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -518,6 +518,7 @@ class TsExprResolver(
518518
isSigned = true
519519
)
520520

521+
// TODO isn't here any problem with reading from array as parameter? parameter[0] == 1
521522
val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type)
522523
val expr = scope.calcOnState { memory.read(lValue) }
523524

@@ -558,18 +559,29 @@ class TsExprResolver(
558559
return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), expr.asExpr(sizeSort), signed = true)
559560
}
560561

561-
val fieldType = scene.fieldLookUp(value.field).type
562-
val sort = typeToSort(fieldType)
563-
val lValue = UFieldLValue(sort, instanceRef, value.field.name)
562+
val lValue = UFieldLValue(addressSort, instanceRef, value.field.name)
564563
val expr = scope.calcOnState { memory.read(lValue) }
565564

566-
val fakeExpr = expr.toFakeObject(scope)
565+
// If we already wrote a fake object in a field, use it, otherwise, create it
566+
// TODO probably we have to create a fake object with all possible types, ignoring the type from the scene
567+
val resultExpr = if (expr.isFakeObject()) {
568+
expr
569+
} else {
570+
val fieldType = scene.fieldLookUp(value.field).type
571+
val sort = typeToSort(fieldType)
572+
val lValue = UFieldLValue(sort, instanceRef, value.field.name)
573+
val currentExpr = scope.calcOnState { memory.read(lValue) }
567574

568-
val fieldLValue = UFieldLValue(addressSort, instanceRef, value.field.name)
569-
scope.calcOnState { memory.write(fieldLValue, fakeExpr, guard = trueExpr) }
575+
val fakeExpr = currentExpr.toFakeObject(scope)
576+
577+
val fieldLValue = UFieldLValue(addressSort, instanceRef, value.field.name)
578+
scope.calcOnState { memory.write(fieldLValue, fakeExpr, guard = trueExpr) }
570579

571-
if (assertIsSubtype(expr, value.type)) {
572580
fakeExpr
581+
}
582+
583+
if (assertIsSubtype(expr, value.type)) {
584+
resultExpr
573585
} else {
574586
null
575587
}

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

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -56,21 +56,24 @@ sealed interface TsBinaryOperator {
5656
rhs: UExpr<out USort>,
5757
scope: TsStepScope,
5858
): UExpr<out USort> {
59-
if (lhs.isFakeObject() || rhs.isFakeObject()) {
60-
return resolveFakeObject(lhs, rhs, scope)
59+
val lhsValue = if (lhs.isFakeObject()) lhs.extractSingleValueFromFakeObjectOrNull(scope) ?: lhs else lhs
60+
val rhsValue = if (rhs.isFakeObject()) rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs else rhs
61+
62+
if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) {
63+
return resolveFakeObject(lhsValue, rhsValue, scope)
6164
}
6265

63-
val lhsSort = lhs.sort
64-
if (lhsSort == rhs.sort) {
66+
val lhsSort = lhsValue.sort
67+
if (lhsSort == rhsValue.sort) {
6568
return when (lhsSort) {
66-
boolSort -> onBool(lhs.asExpr(boolSort), rhs.asExpr(boolSort), scope)
67-
fp64Sort -> onFp(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort), scope)
68-
addressSort -> onRef(lhs.asExpr(addressSort), rhs.asExpr(addressSort), scope)
69+
boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope)
70+
fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope)
71+
addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope)
6972
else -> TODO("Unsupported sort $lhsSort")
7073
}
7174
}
7275

73-
return internalResolve(lhs, rhs, scope)
76+
return internalResolve(lhsValue, rhsValue, scope)
7477
}
7578

7679
data object Eq : TsBinaryOperator {

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

Lines changed: 40 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ import org.jacodb.ets.model.EtsMethodSignature
2525
import org.usvm.UAddressSort
2626
import org.usvm.UConcreteHeapRef
2727
import org.usvm.UExpr
28+
import org.usvm.UHeapRef
2829
import org.usvm.USort
2930
import org.usvm.api.GlobalFieldValue
3031
import org.usvm.api.TsParametersState
@@ -66,7 +67,7 @@ class TsTestResolver {
6667

6768
is TsMethodResult.Success -> {
6869
afterMemoryScope.withMode(ResolveMode.CURRENT) {
69-
resolveExpr(res.value, method.returnType)
70+
resolveExpr(res.value, res.value, method.returnType)
7071
}
7172
}
7273

@@ -115,11 +116,13 @@ open class TsTestStateResolver(
115116
) {
116117
fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsValue {
117118
val expr = memory.read(lValue)
118-
return resolveExpr(expr, type)
119+
val symbolicRef = if (lValue.sort is UAddressSort) finalStateMemory.read(lValue).asExpr(ctx.addressSort) else null
120+
return resolveExpr(expr, symbolicRef, type)
119121
}
120122

121123
fun resolveExpr(
122124
expr: UExpr<out USort>,
125+
symbolicRef: UExpr<out USort>? = null,
123126
type: EtsType,
124127
): TsValue = with(ctx) {
125128
if (expr.isFakeObject()) {
@@ -128,57 +131,66 @@ open class TsTestStateResolver(
128131

129132
return when (type) {
130133
is EtsPrimitiveType -> resolvePrimitive(expr, type)
131-
is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type)
132-
else -> resolveUnknownExpr(expr)
134+
is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), symbolicRef?.asExpr(ctx.addressSort) ?: expr.asExpr(ctx.addressSort), type)
135+
else -> resolveUnknownExpr(expr, symbolicRef)
133136
}
134137
}
135138

136-
fun resolveUnknownExpr(expr: UExpr<out USort>): TsValue = with(expr.tctx) {
137-
when (expr.sort) {
138-
fp64Sort -> resolvePrimitive(expr, EtsNumberType)
139-
boolSort -> resolvePrimitive(expr, EtsBooleanType)
139+
fun resolveUnknownExpr(heapRef: UExpr<out USort>, finalStateMemoryRef: UExpr<out USort>?): TsValue = with(heapRef.tctx) {
140+
when (heapRef.sort) {
141+
fp64Sort -> resolvePrimitive(heapRef, EtsNumberType)
142+
boolSort -> resolvePrimitive(heapRef, EtsBooleanType)
140143
addressSort -> {
141-
if (expr.isFakeObject()) {
142-
resolveFakeObject(expr)
144+
if (heapRef.isFakeObject()) {
145+
resolveFakeObject(heapRef)
143146
} else {
144-
resolveRef(expr.asExpr(ctx.addressSort), EtsUnknownType)
147+
resolveRef(heapRef.asExpr(ctx.addressSort), finalStateMemoryRef?.asExpr(ctx.addressSort), EtsUnknownType)
145148
}
146149
}
147150

148151
else -> TODO()
149152
}
150153
}
151154

152-
private fun resolveRef(expr: UExpr<UAddressSort>, type: EtsType): TsValue {
153-
val instance = model.eval(expr) as UConcreteHeapRef
155+
private fun resolveRef(
156+
heapRef: UExpr<UAddressSort>,
157+
finalStateMemoryRef: UExpr<UAddressSort>?,
158+
type: EtsType
159+
): TsValue {
160+
val concreteRef = evaluateInModel(heapRef) as UConcreteHeapRef
154161

155-
if (instance.address == 0) {
162+
if (concreteRef.address == 0) {
156163
return TsValue.TsUndefined
157164
}
158165

159-
if (model.eval(ctx.mkHeapRefEq(expr, ctx.mkTsNullValue())).isTrue) {
166+
if (model.eval(ctx.mkHeapRefEq(heapRef, ctx.mkTsNullValue())).isTrue) {
160167
return TsValue.TsNull
161168
}
162169

163170
return when (type) {
164-
is EtsClassType -> resolveClass(instance, type)
165-
is EtsArrayType -> resolveArray(instance, type)
171+
is EtsClassType -> resolveClass(concreteRef, finalStateMemoryRef ?: heapRef, type)
172+
is EtsArrayType -> resolveArray(concreteRef, finalStateMemoryRef ?: heapRef, type)
166173
is EtsUnknownType -> {
167-
val type = finalStateMemory.types.getTypeStream(expr).first()
168-
resolveRef(expr, type)
174+
val type = finalStateMemory.types.getTypeStream(heapRef).first()
175+
resolveRef(heapRef, finalStateMemoryRef, type)
169176
}
170177

171178
else -> error("Unexpected type: $type")
172179
}
173180
}
174181

175-
private fun resolveArray(expr: UConcreteHeapRef, type: EtsArrayType): TsValue.TsArray<*> {
176-
val arrayLengthLValue = UArrayLengthLValue(expr, type, ctx.sizeSort)
182+
183+
private fun resolveArray(
184+
concreteRef: UConcreteHeapRef,
185+
heapRef: UHeapRef,
186+
type: EtsArrayType
187+
): TsValue.TsArray<*> {
188+
val arrayLengthLValue = UArrayLengthLValue(heapRef, type, ctx.sizeSort)
177189
val length = model.eval(memory.read(arrayLengthLValue)) as KBitVec32Value
178190

179191
val values = (0 until length.intValue).map {
180192
val index = ctx.mkSizeExpr(it)
181-
val lValue = UArrayIndexLValue(ctx.addressSort, expr, index, type)
193+
val lValue = UArrayIndexLValue(ctx.addressSort, heapRef, index, type)
182194
val value = memory.read(lValue)
183195

184196
if (model.eval(ctx.mkHeapRefEq(value, ctx.mkUndefinedValue())).isTrue) {
@@ -229,15 +241,15 @@ open class TsTestStateResolver(
229241
// Note that everything about details of fake object we need to read from final state of the memory
230242
// since they are allocated objects
231243
val value = finalStateMemory.read(lValue)
232-
resolveExpr(model.eval(value), EtsBooleanType)
244+
resolveExpr(model.eval(value), value, EtsBooleanType)
233245
}
234246

235247
model.eval(type.fpTypeExpr).isTrue -> {
236248
val lValue = ctx.getIntermediateFpLValue(expr.address)
237249
// Note that everything about details of fake object we need to read from final state of the memory
238250
// since they are allocated objects
239251
val value = finalStateMemory.read(lValue)
240-
resolveExpr(model.eval(value), EtsNumberType)
252+
resolveExpr(model.eval(value), value, EtsNumberType)
241253
}
242254

243255
model.eval(type.refTypeExpr).isTrue -> {
@@ -247,7 +259,7 @@ open class TsTestStateResolver(
247259
val value = finalStateMemory.read(lValue)
248260
val ref = model.eval(value)
249261
// TODO mistake with signature, use TypeStream instead
250-
resolveExpr(ref, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature))
262+
resolveExpr(ref, value, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature))
251263
}
252264

253265
else -> error("Unsupported")
@@ -270,22 +282,10 @@ open class TsTestStateResolver(
270282
}
271283

272284
private fun resolveClass(
273-
expr: UExpr<out USort>,
285+
concreteRef: UConcreteHeapRef,
286+
heapRef: UHeapRef,
274287
classType: EtsClassType,
275288
): TsValue {
276-
if (expr is UConcreteHeapRef && expr.address == 0) {
277-
return TsValue.TsUndefined
278-
}
279-
280-
val nullRef = ctx.mkTsNullValue()
281-
if (model.eval(ctx.mkHeapRefEq(expr.asExpr(ctx.addressSort), nullRef)).isTrue) {
282-
return TsValue.TsNull
283-
}
284-
285-
check(expr.sort == ctx.addressSort) {
286-
"Expected address sort, but got ${expr.sort}"
287-
}
288-
289289
val clazz = ctx.scene.projectAndSdkClasses.firstOrNull { it.signature == classType.signature }
290290
?: if (classType.signature.name == "Object") {
291291
EtsClassImpl(
@@ -306,7 +306,7 @@ open class TsTestStateResolver(
306306
}
307307

308308
val properties = clazz.fields.associate { field ->
309-
val lValue = UFieldLValue(ctx.addressSort, expr.asExpr(ctx.addressSort), field.name)
309+
val lValue = UFieldLValue(ctx.addressSort, heapRef, field.name)
310310
// read from final state memory since it is a fake object
311311
val fieldExpr = finalStateMemory.read(lValue)
312312

0 commit comments

Comments
 (0)