Skip to content

Commit 7b1bcd8

Browse files
CaelmBleiddCaelmBleidd
committed
Some fixes
1 parent bb4df1f commit 7b1bcd8

2 files changed

Lines changed: 50 additions & 36 deletions

File tree

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

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ import org.jacodb.ets.model.EtsStmt
2424
import org.jacodb.ets.model.EtsThis
2525
import org.jacodb.ets.model.EtsThrowStmt
2626
import org.jacodb.ets.model.EtsType
27+
import org.jacodb.ets.model.EtsUnionType
2728
import org.jacodb.ets.model.EtsUnknownType
2829
import org.jacodb.ets.model.EtsValue
2930
import org.jacodb.ets.model.EtsVoidType
@@ -213,9 +214,9 @@ class TsInterpreter(
213214
val limitedConcreteMethods = concreteMethods.take(5)
214215

215216
// logger.info {
216-
// "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
217-
// limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
218-
// }"
217+
// "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
218+
// limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
219+
// }"
219220
// }
220221
val conditionsWithBlocks = limitedConcreteMethods.map { method ->
221222
val concreteCall = stmt.toConcrete(method)
@@ -681,18 +682,19 @@ class TsInterpreter(
681682
if (parameterType is EtsRefType) {
682683
val argLValue = mkRegisterStackLValue(ctx.addressSort, i)
683684
val ref = state.memory.read(argLValue).asExpr(ctx.addressSort)
684-
val resolvedParameterType = graph.cp
685-
.projectAndSdkClasses
686-
.singleOrNull { it.name == parameterType.typeName }
687-
?.type
688-
?: parameterType
685+
val resolvedParameterType = graph.hierarchy.classesForType(parameterType)
686+
687+
if (resolvedParameterType.isEmpty()) {
688+
logger.error("Cannot resolve class for parameter type: $parameterType")
689+
return@forEachIndexed // TODO should be an error
690+
}
689691

690692
// Because of structural equality in TS we cannot determine the exact type
691693
// Therefore, we create information about the fields the type must consist
692-
val auxiliaryType = (resolvedParameterType as? EtsClassType)?.toAuxiliaryType(graph.hierarchy)
693-
?: resolvedParameterType
694-
state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)
694+
val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) }
695+
val auxiliaryType = EtsUnionType(types) // TODO error
695696

697+
state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)
696698
state.pathConstraints += with(ctx) {
697699
mkNot(
698700
mkOr(

‎usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt‎

Lines changed: 37 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
package org.usvm.project
22

33
import org.jacodb.ets.model.EtsScene
4-
import org.jacodb.ets.utils.getDeclaredLocals
5-
import org.jacodb.ets.utils.getLocals
4+
import org.jacodb.ets.utils.CONSTRUCTOR_NAME
5+
import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
6+
import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
67
import org.jacodb.ets.utils.loadEtsProjectFromIR
78
import org.junit.jupiter.api.condition.EnabledIf
8-
import org.usvm.api.TsTestValue
99
import org.usvm.machine.TsMachine
1010
import org.usvm.machine.TsOptions
1111
import org.usvm.util.TsMethodTestRunner
@@ -35,30 +35,41 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
3535

3636
@Test
3737
fun `test run on each method`() {
38-
println("Total classes: ${scene.projectAndSdkClasses.size}")
39-
for (clazz in scene.projectAndSdkClasses) {
40-
println()
41-
println("CLASS: ${clazz.name} in ${clazz.signature.file}")
42-
for (method in clazz.methods) {
43-
println()
44-
println("METHOD: ${clazz.name}::${method.name}(${method.parameters.joinToString()})")
45-
if (method.cfg.stmts.isEmpty()) {
46-
println("CFG is empty")
47-
continue
48-
}
49-
if (method.getLocals() != method.getDeclaredLocals()) {
50-
println(
51-
"Locals mismatch:\n getLocals() = ${
52-
method.getLocals().sortedBy { it.name }
53-
}\n getDeclaredLocals() = ${
54-
method.getDeclaredLocals().sortedBy { it.name }
55-
}"
56-
)
57-
// continue
38+
val exceptions = mutableListOf<Throwable>()
39+
val classes = scene.projectClasses.filterNot { it.name.startsWith("%AC") }
40+
41+
println("Total classes: ${classes.size}")
42+
43+
classes
44+
// .filter { it.name == "NewAlbumPage" }
45+
.forEach { clazz ->
46+
val methods = clazz.methods
47+
.filterNot { it.cfg.stmts.isEmpty() }
48+
.filterNot { it.isStatic }
49+
.filterNot { it.name.startsWith("%AM") }
50+
.filterNot { it.name == "build" }
51+
.filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
52+
.filterNot { it.name == STATIC_INIT_METHOD_NAME }
53+
.filterNot { it.name == CONSTRUCTOR_NAME }
54+
55+
if (methods.isEmpty()) return@forEach
56+
57+
runCatching {
58+
val tsOptions = TsOptions()
59+
TsMachine(scene, options, tsOptions).use { machine ->
60+
val states = machine.analyze(methods)
61+
states.let {}
62+
}
63+
}.onFailure {
64+
exceptions += it
5865
}
59-
discoverProperties<TsTestValue>(method = method)
6066
}
61-
}
67+
68+
val exc = exceptions.groupBy { it }
69+
println(
70+
exc.values.sortedBy
71+
{ it.size }.asReversed().map
72+
{ it.first() })
6273
}
6374

6475
@Test
@@ -72,6 +83,7 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
7283
.filterNot { it.name.startsWith("%AM") }
7384
.filterNot { it.name == "build" }
7485
}
86+
.filter { it.name == "createKvStore" && it.enclosingClass?.name == "KvStoreModel" }
7587
val tsOptions = TsOptions()
7688
TsMachine(scene, options, tsOptions).use { machine ->
7789
val states = machine.analyze(methods)

0 commit comments

Comments
 (0)