Skip to content

Commit c0a2caf

Browse files
CaelmBleiddCaelmBleidd
committed
Stream usages
1 parent e713d2c commit c0a2caf

7 files changed

Lines changed: 167 additions & 24 deletions

File tree

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

Lines changed: 24 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.usvm.machine.interpreter
22

3+
import io.ksmt.expr.rewrite.simplify.addArithTerm
34
import io.ksmt.utils.asExpr
45
import mu.KotlinLogging
56
import org.jacodb.ets.model.EtsArrayAccess
@@ -15,6 +16,7 @@ import org.jacodb.ets.model.EtsMethodSignature
1516
import org.jacodb.ets.model.EtsNopStmt
1617
import org.jacodb.ets.model.EtsNullType
1718
import org.jacodb.ets.model.EtsParameterRef
19+
import org.jacodb.ets.model.EtsRefType
1820
import org.jacodb.ets.model.EtsReturnStmt
1921
import org.jacodb.ets.model.EtsStaticFieldRef
2022
import org.jacodb.ets.model.EtsStmt
@@ -31,6 +33,7 @@ import org.usvm.UAddressSort
3133
import org.usvm.UExpr
3234
import org.usvm.UInterpreter
3335
import org.usvm.api.allocateArrayInitialized
36+
import org.usvm.api.evalTypeEquals
3437
import org.usvm.api.makeSymbolicPrimitive
3538
import org.usvm.api.makeSymbolicRefUntyped
3639
import org.usvm.api.targets.TsTarget
@@ -64,6 +67,7 @@ import org.usvm.util.mkFieldLValue
6467
import org.usvm.util.mkRegisterStackLValue
6568
import org.usvm.util.resolveEtsField
6669
import org.usvm.util.resolveEtsMethods
70+
import org.usvm.util.type
6771
import org.usvm.utils.ensureSat
6872

6973
private val logger = KotlinLogging.logger {}
@@ -165,7 +169,12 @@ class TsInterpreter(
165169
val conditionsWithBlocks = concreteMethods.map { method ->
166170
val concreteCall = stmt.toConcrete(method)
167171
val block = { state: TsState -> state.newStmt(concreteCall) }
168-
ctx.trueExpr to block
172+
val type = method.enclosingClass!!.type
173+
val constraint = scope.calcOnState {
174+
val instance = stmt.instance.asExpr(ctx.addressSort)
175+
memory.types.evalTypeEquals(instance, type) // TODO mistake, should be separated into several hierarchies
176+
}
177+
constraint to block
169178
}
170179
scope.forkMulti(conditionsWithBlocks)
171180
}
@@ -497,9 +506,20 @@ class TsInterpreter(
497506
)
498507
}
499508

500-
// TODO fix incorrect type streams
501-
// val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, EtsClassType(method.enclosingClass))
502-
// state.pathConstraints += thisTypeConstraint
509+
method.enclosingClass?.let { thisClass ->
510+
// TODO not equal but subtype for abstract/interfaces
511+
val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, thisClass.type)
512+
state.pathConstraints += thisTypeConstraint
513+
}
514+
515+
method.parameters.forEachIndexed { i, param ->
516+
val parameterType = param.type
517+
if (parameterType is EtsRefType) {
518+
val argLValue = mkRegisterStackLValue(ctx.addressSort, i)
519+
val ref = state.memory.read(argLValue).asExpr(ctx.addressSort)
520+
state.pathConstraints += state.memory.types.evalIsSubtype(ref, parameterType)
521+
}
522+
}
503523

504524
val model = solver.check(state.pathConstraints).ensureSat().model
505525
state.models = listOf(model)

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

Lines changed: 46 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsAnyType
55
import org.jacodb.ets.model.EtsArrayType
66
import org.jacodb.ets.model.EtsBooleanType
77
import org.jacodb.ets.model.EtsClassType
8+
import org.jacodb.ets.model.EtsNullType
89
import org.jacodb.ets.model.EtsNumberType
910
import org.jacodb.ets.model.EtsPrimitiveType
1011
import org.jacodb.ets.model.EtsScene
@@ -35,11 +36,41 @@ class TsTypeSystem(
3536
/**
3637
* @return true if [type] <: [supertype].
3738
*/
38-
override fun isSupertype(supertype: EtsType, type: EtsType): Boolean = when {
39-
type is AuxiliaryType -> TODO()
40-
supertype == type -> true
41-
supertype == EtsUnknownType || supertype == EtsAnyType -> true
42-
else -> TODO()
39+
override fun isSupertype(supertype: EtsType, type: EtsType): Boolean {
40+
return when {
41+
type is AuxiliaryType -> TODO()
42+
supertype is AuxiliaryType -> TODO()
43+
supertype == type -> true
44+
supertype == EtsUnknownType || supertype == EtsAnyType -> true
45+
supertype is EtsPrimitiveType || type is EtsPrimitiveType -> type == supertype
46+
else -> {
47+
// TODO isAssignable
48+
if (supertype is EtsUnknownType || supertype is EtsAnyType) {
49+
return true
50+
}
51+
52+
if (type is EtsUnknownType || type is EtsAnyType) {
53+
return false // otherwise it should be processed in the code above
54+
}
55+
56+
// TODO wrong type resolutions because of names
57+
val clazz = project.projectAndSdkClasses.singleOrNull() { it.type.typeName == type.typeName } ?: error("TODO")
58+
val ancestors = generateSequence(clazz) { c ->
59+
// TODO mistake because of name usage
60+
project.projectAndSdkClasses.singleOrNull { it.signature.name == c.superClass?.name }
61+
}.map { it.type }
62+
63+
if (supertype is EtsClassType) {
64+
return ancestors.any { it == supertype }
65+
}
66+
67+
if (supertype is EtsUnclearRefType) {
68+
return ancestors.any { it.typeName == supertype.typeName }
69+
}
70+
71+
error("TODO")
72+
}
73+
}
4374
}
4475

4576
/**
@@ -49,8 +80,8 @@ class TsTypeSystem(
4980
*/
5081
override fun hasCommonSubtype(type: EtsType, types: Collection<EtsType>): Boolean = when {
5182
type is EtsPrimitiveType -> types.isEmpty()
52-
type is EtsClassType -> TODO()
53-
type is EtsUnclearRefType -> TODO()
83+
type is EtsClassType -> true
84+
type is EtsUnclearRefType -> true
5485
type is EtsArrayType -> TODO()
5586
else -> error("Unsupported class type: $type")
5687
}
@@ -75,7 +106,14 @@ class TsTypeSystem(
75106
// TODO they should be direct inheritors, not all of them
76107
is EtsAnyType,
77108
is EtsUnknownType -> project.projectAndSdkClasses.asSequence().map { it.type }
78-
else -> TODO()
109+
is AuxiliaryType -> {
110+
TODO()
111+
}
112+
else -> {
113+
val clazz = project.projectAndSdkClasses.filter { it.type == type }
114+
// TODO optimize
115+
project.projectAndSdkClasses.asSequence().filter { it.superClass == clazz }.map { it.type }
116+
}
79117
}
80118

81119
private val topTypeStream by lazy { TsTopTypeStream(this) }

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -210,7 +210,6 @@ class Call : TsMethodTestRunner() {
210210
)
211211
}
212212

213-
@Disabled("Too complex")
214213
@Test
215214
fun `test virtual dispatch`() {
216215
val method = getMethod(className, "virtualDispatch")

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

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
package org.usvm.samples.types
2+
3+
import org.jacodb.ets.model.EtsScene
4+
import org.junit.jupiter.api.Test
5+
import org.usvm.api.TsValue
6+
import org.usvm.util.TsMethodTestRunner
7+
8+
class TypeStream : TsMethodTestRunner() {
9+
private val className = this::class.simpleName!!
10+
11+
override val scene: EtsScene = loadSampleScene(className, folderPrefix = "types")
12+
13+
@Test
14+
fun `test an ancestor as argument`() {
15+
val method = getMethod(className, "ancestorId")
16+
discoverProperties<TsValue.TsClass, TsValue.TsClass>(
17+
method = method,
18+
{ value, r -> r.name == value.name },
19+
)
20+
}
21+
22+
@Test
23+
fun `test virtual invoke on an ancestor`() {
24+
val method = getMethod(className, "virtualInvokeForAncestor")
25+
discoverProperties<TsValue.TsClass, TsValue.TsNumber>(
26+
method = method,
27+
{ value, r -> value.name == "Parent" && r.number == 1.0 },
28+
{ value, r -> value.name == "FirstChild" && r.number == 2.0 },
29+
{ value, r -> value.name == "SecondChild" && r.number == 3.0 },
30+
)
31+
}
32+
}

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,10 +39,11 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
3939

4040
protected fun loadSampleScene(
4141
className: String,
42+
folderPrefix: String = "",
4243
useArkAnalyzerTypeInference: Boolean = false,
4344
): EtsScene {
4445
val name = "$className.ts"
45-
val path = getResourcePath("/samples/$name")
46+
val path = getResourcePath("/samples/$folderPrefix/$name")
4647
val file = loadEtsFileAutoConvert(
4748
path,
4849
useArkAnalyzerTypeInference = if (useArkAnalyzerTypeInference) 1 else null

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

Lines changed: 29 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ import org.jacodb.ets.model.EtsNeverType
1313
import org.jacodb.ets.model.EtsNullType
1414
import org.jacodb.ets.model.EtsNumberType
1515
import org.jacodb.ets.model.EtsPrimitiveType
16+
import org.jacodb.ets.model.EtsRef
1617
import org.jacodb.ets.model.EtsRefType
1718
import org.jacodb.ets.model.EtsStringType
1819
import org.jacodb.ets.model.EtsType
@@ -30,6 +31,7 @@ import org.usvm.api.GlobalFieldValue
3031
import org.usvm.api.TsParametersState
3132
import org.usvm.api.TsTest
3233
import org.usvm.api.TsValue
34+
import org.usvm.api.typeStreamOf
3335
import org.usvm.isTrue
3436
import org.usvm.machine.TsContext
3537
import org.usvm.machine.expr.TsUnresolvedSort
@@ -188,11 +190,11 @@ open class TsTestStateResolver(
188190
// TODO add better support
189191
is EtsUnclearRefType -> {
190192
val cls = ctx.scene.projectAndSdkClasses.single { it.name == type.typeName }
191-
resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, cls.type)
193+
resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef)
192194
}
193195

194196
is EtsClassType -> {
195-
resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef, type)
197+
resolveTsClass(concreteRef, finalStateMemoryRef ?: heapRef)
196198
}
197199

198200
is EtsArrayType -> {
@@ -323,36 +325,53 @@ open class TsTestStateResolver(
323325
}
324326

325327
private fun resolveClass(
326-
classType: EtsClassType,
328+
refType: EtsRefType,
327329
): EtsClass {
330+
if (refType is EtsArrayType) {
331+
TODO()
332+
}
333+
334+
328335
// Special case for Object:
329-
if (classType.signature.name == "Object") {
336+
val name = when(refType) {
337+
is EtsClassType -> refType.signature.name
338+
is EtsUnclearRefType -> refType.name
339+
else -> error("Unsupported $refType")
340+
}
341+
342+
if (name == "Object") {
330343
return createObjectClass()
331344
}
332345

333346
// Perfect signature:
334-
if (classType.signature.name != UNKNOWN_CLASS_NAME) {
335-
val classes = ctx.scene.projectAndSdkClasses.filter { it.signature == classType.signature }
347+
if (name != UNKNOWN_CLASS_NAME) {
348+
val classes = ctx.scene.projectAndSdkClasses.filter {
349+
when (refType) {
350+
is EtsClassType -> it.signature == refType.signature
351+
is EtsUnclearRefType -> it.name == refType.typeName
352+
else -> error("TODO")
353+
}
354+
}
336355
if (classes.size == 1) {
337356
return classes.single()
338357
}
339358
}
340359

341360
// Sad signature:
342-
val classes = ctx.scene.projectAndSdkClasses.filter { it.signature.name == classType.signature.name }
361+
val classes = ctx.scene.projectAndSdkClasses.filter { it.signature.name == name }
343362
if (classes.size == 1) {
344363
return classes.single()
345364
}
346365

347-
error("Could not resolve class: ${classType.signature}")
366+
error("Could not resolve class: ${refType}")
348367
}
349368

350369
private fun resolveTsClass(
351370
concreteRef: UConcreteHeapRef,
352371
heapRef: UHeapRef,
353-
classType: EtsClassType,
354372
): TsValue.TsClass = with(ctx) {
355-
val clazz = resolveClass(classType)
373+
val type = model.typeStreamOf(concreteRef).first() as EtsRefType
374+
val clazz = resolveClass(type)
356375
val properties = clazz.fields
357376
.filterNot { field ->
358377
field as EtsFieldImpl

‎usvm-ts/src/test/resources/samples/types/TypeStream.ts‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
class TypeStream {
2+
ancestorId(ancestor: Parent): Parent {
3+
return ancestor
4+
}
5+
6+
virtualInvokeForAncestor(ancestor: Parent): number {
7+
var number = ancestor.virtualMethod();
8+
if (number == 100) {
9+
return 1
10+
} else if (number == 200) {
11+
return 2
12+
} else {
13+
return 3
14+
}
15+
}
16+
}
17+
18+
class Parent {
19+
virtualMethod(): number {
20+
return 100;
21+
}
22+
}
23+
24+
class FirstChild extends Parent {
25+
override virtualMethod(): number {
26+
return 200;
27+
}
28+
}
29+
30+
class SecondChild extends Parent {
31+
override virtualMethod(): number{
32+
return 300;
33+
}
34+
}

0 commit comments

Comments
 (0)