Skip to content

Commit df9aad5

Browse files
CaelmBleiddCaelmBleidd
committed
Hierarchy implementation
1 parent aba0b88 commit df9aad5

8 files changed

Lines changed: 102 additions & 15 deletions

File tree

‎usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,28 @@ import org.usvm.types.UTypeStream
1717
import org.usvm.types.UTypeSystem
1818
import kotlin.time.Duration
1919

20+
open class A {
21+
protected open fun foo() {
22+
println("Hello")
23+
}
24+
}
25+
26+
class B : A() {
27+
override fun foo() {
28+
println("Hello")
29+
30+
}
31+
32+
fun getsa() {
33+
val method = this.javaClass.methods
34+
}
35+
}
36+
37+
fun main() {
38+
val a = B()
39+
println(a.javaClass.declaredMethods.toList().joinToString("\n"))
40+
}
41+
2042
class JcTypeSystem(
2143
private val cp: JcClasspath,
2244
override val typeOperationsTimeout: Duration

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,11 @@ import org.jacodb.ets.model.EtsStmt
66
import org.usvm.dataflow.ts.graph.EtsApplicationGraph
77
import org.usvm.dataflow.ts.graph.EtsApplicationGraphImpl
88
import org.usvm.statistics.ApplicationGraph
9+
import org.usvm.util.EtsHierarchy
910

1011
class TsGraph(scene: EtsScene) : ApplicationGraph<EtsMethod, EtsStmt> {
1112
private val etsGraph: EtsApplicationGraph = EtsApplicationGraphImpl(scene)
13+
val hierarchy: EtsHierarchy = EtsHierarchy(scene)
1214

1315
val cp: EtsScene
1416
get() = etsGraph.cp

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,10 +33,10 @@ class TsMachine(
3333
private val machineObserver: UMachineObserver<TsState>? = null,
3434
observer: TsInterpreterObserver? = null,
3535
) : UMachine<TsState>() {
36-
private val typeSystem = TsTypeSystem(typeOperationsTimeout = 1.seconds, project)
36+
private val graph = TsGraph(project)
37+
private val typeSystem = TsTypeSystem(typeOperationsTimeout = 1.seconds, project, graph.hierarchy)
3738
private val components = TsComponents(typeSystem, options)
3839
private val ctx = TsContext(project, components)
39-
private val graph = TsGraph(project)
4040
private val interpreter = TsInterpreter(ctx, graph, tsOptions, observer)
4141
private val cfgStatistics = CfgStatisticsImpl(graph)
4242

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,7 @@ import org.usvm.machine.types.AuxiliaryType
9999
import org.usvm.machine.types.mkFakeValue
100100
import org.usvm.memory.ULValue
101101
import org.usvm.sizeSort
102+
import org.usvm.util.EtsHierarchy
102103
import org.usvm.util.mkArrayIndexLValue
103104
import org.usvm.util.mkArrayLengthLValue
104105
import org.usvm.util.mkFieldLValue
@@ -119,6 +120,7 @@ const val ADHOC_STRING__STRING = 2222.0 // 'string'
119120

120121
class TsExprResolver(
121122
private val ctx: TsContext,
123+
private val hierarchy: EtsHierarchy,
122124
private val scope: TsStepScope,
123125
private val localToIdx: (EtsMethod, EtsValue) -> Int,
124126
) : EtsEntity.Visitor<UExpr<out USort>?> {
@@ -622,6 +624,7 @@ class TsExprResolver(
622624
pathConstraints += if (field.enclosingClass == EtsClassSignature.UNKNOWN) {
623625
memory.types.evalIsSubtype(resolvedAddr, AuxiliaryType(setOf(field.name)))
624626
} else {
627+
// TODO error, field.enclosingClass.type
625628
memory.types.evalIsSubtype(resolvedAddr, field.type) // TODO is it right?
626629
}
627630
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -463,7 +463,7 @@ class TsInterpreter(
463463
}
464464

465465
private fun exprResolverWithScope(scope: TsStepScope): TsExprResolver =
466-
TsExprResolver(ctx, scope, ::mapLocalToIdx)
466+
TsExprResolver(ctx, graph.hierarchy, scope, ::mapLocalToIdx)
467467

468468
// (method, localName) -> idx
469469
private val localVarToIdx: MutableMap<EtsMethod, Map<String, Int>> = hashMapOf()

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

Lines changed: 7 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,26 @@
11
package org.usvm.machine.types
22

3-
import com.jetbrains.rd.framework.util.RdCoroutineScope.Companion.override
43
import org.jacodb.ets.model.EtsAnyType
54
import org.jacodb.ets.model.EtsArrayType
65
import org.jacodb.ets.model.EtsBooleanType
76
import org.jacodb.ets.model.EtsClassType
8-
import org.jacodb.ets.model.EtsNullType
97
import org.jacodb.ets.model.EtsNumberType
108
import org.jacodb.ets.model.EtsPrimitiveType
119
import org.jacodb.ets.model.EtsScene
1210
import org.jacodb.ets.model.EtsType
1311
import org.jacodb.ets.model.EtsUnclearRefType
1412
import org.jacodb.ets.model.EtsUnknownType
15-
import org.usvm.machine.types.TsTypeSystem.Companion.primitiveTypes
16-
import org.usvm.types.TypesResult
17-
import org.usvm.types.TypesResult.Companion.toTypesResult
18-
import org.usvm.types.USupportTypeStream
1913
import org.usvm.types.UTypeStream
2014
import org.usvm.types.UTypeSystem
21-
import org.usvm.types.emptyTypeStream
15+
import org.usvm.util.EtsHierarchy
2216
import org.usvm.util.type
2317
import kotlin.time.Duration
2418

2519
// TODO this is draft, should be replaced with real implementation
2620
class TsTypeSystem(
2721
override val typeOperationsTimeout: Duration,
2822
val project: EtsScene,
23+
val hierarchy: EtsHierarchy,
2924
) : UTypeSystem<EtsType> {
3025

3126
companion object {
@@ -44,15 +39,16 @@ class TsTypeSystem(
4439
if (supertype is AuxiliaryType) {
4540
return type.properties.all { it in supertype.properties }
4641
}
47-
val supertypeFields =
48-
project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName }.fields
42+
val supertypeClass = project.projectAndSdkClasses.single { it.type.typeName == supertype.typeName }
43+
val supertypeFields = hierarchy.getAncestor(supertypeClass).flatMap { it.fields }
4944
type.properties.all { it in supertypeFields.map { it.name } }
5045
}
5146

5247
supertype is AuxiliaryType -> {
5348
if (type is EtsUnknownType || type is EtsAnyType) return supertype.properties.isEmpty()
5449

55-
val typeFields = project.projectAndSdkClasses.single { it.type.typeName == type.typeName }.fields
50+
val clazz = project.projectAndSdkClasses.single { it.type.typeName == type.typeName }
51+
val typeFields = hierarchy.getAncestor(clazz).flatMap { it.fields }
5652
typeFields.mapTo(mutableSetOf()) { it.name }.containsAll(supertype.properties)
5753
}
5854
supertype == type -> true
@@ -127,7 +123,7 @@ class TsTypeSystem(
127123
is AuxiliaryType -> {
128124
project.projectAndSdkClasses.filter {
129125
it.fields.mapTo(mutableSetOf()) { it.name }.containsAll(type.properties)
130-
}.asSequence().map { it.type }
126+
}.asSequence().map { it.type } // TODO get fields of ancestors
131127
}
132128

133129
else -> {

‎usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
package org.usvm.util
2+
3+
import org.jacodb.ets.model.EtsClass
4+
import org.jacodb.ets.model.EtsClassSignature
5+
import org.jacodb.ets.model.EtsFile
6+
import org.jacodb.ets.model.EtsFileSignature
7+
import org.jacodb.ets.model.EtsScene
8+
import kotlin.collections.flatten
9+
10+
private typealias ClassName = String
11+
12+
class EtsHierarchy(private val scene: EtsScene) {
13+
private val resolveMap: Map<ClassName, Map<EtsClassSignature, EtsClass>> by lazy {
14+
scene.projectAndSdkClasses
15+
.groupBy { it.name }
16+
.mapValues { (_, classes) ->
17+
classes
18+
.groupBy { it.signature }
19+
.map { it.key to it.value.single() }
20+
.toMap()
21+
}
22+
}
23+
24+
private val ancestors: Map<EtsClass, Set<EtsClass>> by lazy {
25+
val classes = scene.projectAndSdkClasses
26+
val ancestors = classes.map {
27+
it to generateSequence(listOf(it)) { currentClasses ->
28+
currentClasses.flatMap { currentClass ->
29+
val superClassSignature = currentClass.superClass ?: return@generateSequence null
30+
val classesWithTheSameName = resolveMap.getValue(superClassSignature.name)
31+
val classesWithTheSameSignature = classesWithTheSameName[superClassSignature]
32+
val superClasses = when {
33+
classesWithTheSameSignature != null -> listOf(classesWithTheSameSignature)
34+
superClassSignature.file == EtsFileSignature.UNKNOWN -> classesWithTheSameName.values
35+
else -> error("There is no class with name ${superClassSignature.name}")
36+
}
37+
val interfaces = currentClass.implementedInterfaces
38+
require(interfaces.isEmpty()) { TODO() }
39+
val resolvedInterfaces = interfaces.map { interfaceSignature ->
40+
resolveMap[currentClass.name]?.get(interfaceSignature) ?: error("Unresolved interface")
41+
}
42+
superClasses + resolvedInterfaces
43+
}
44+
}.flatten().toSet()
45+
}
46+
val result = ancestors.toMap()
47+
48+
ancestors.forEach { (key, value) ->
49+
value.forEach { clazz ->
50+
inheritors.computeIfAbsent(clazz) { mutableSetOf() }.add(key)
51+
}
52+
}
53+
result
54+
}
55+
56+
private val inheritors: MutableMap<EtsClass, MutableSet<EtsClass>> = mutableMapOf()
57+
58+
fun getAncestor(clazz: EtsClass): Set<EtsClass> {
59+
return ancestors[clazz] ?: error("TODO")
60+
}
61+
62+
fun getInheritors(clazz: EtsClass) : Set<EtsClass> {
63+
return inheritors[clazz] ?: error("TODO")
64+
}
65+
}

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,6 @@ class TypeStream : TsMethodTestRunner() {
4343
}
4444

4545
@Test
46-
@Disabled("Parent's fields are not supported yet")
4746
fun `use non unique field`() {
4847
val method = getMethod(className, "useNonUniqueField")
4948
discoverProperties<TsValue.TsClass, TsValue.TsNumber>(

0 commit comments

Comments
 (0)