Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@MForest7
MForest7 committed Feb 12, 2025
1 parent 2f5e462 commit a9014d5
Show file tree
Hide file tree
Showing 10 changed files with 97 additions and 73 deletions.
6 changes: 4 additions & 2 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/graph/EtsApplicationGraph.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ class EtsApplicationGraphImpl(
return cacheClassWithIdealSignature.getValue(signature)
}

val matched = projectClassesBySignature[signature] ?: emptyList()
val matched = projectClassesBySignature[signature].orEmpty()
if (matched.isEmpty()) {
cacheClassWithIdealSignature[signature] = Maybe.none()
return Maybe.none()
Expand Down Expand Up @@ -250,7 +250,9 @@ class EtsApplicationGraphImpl(
.asSequence()
.filter { compareClassSignatures(it.enclosingClass, callee.enclosingClass) != ComparisonResult.NotEqual }
// Note: exclude current class:
.filterNot { compareClassSignatures(it.enclosingClass, node.method.enclosingClass) != ComparisonResult.NotEqual }
.filterNot {
compareClassSignatures(it.enclosingClass, node.method.enclosingClass) != ComparisonResult.NotEqual
}
.toList()
if (resolved.isEmpty()) {
cachePartiallyMatchedCallees[callee] = emptyList()
Expand Down
67 changes: 37 additions & 30 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/Alias.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ import kotlin.collections.ArrayDeque
class StmtAliasInfo(
val baseToAlloc: IntArray,
val allocToFields: Array<ULongArray>,
val method: MethodAliasInfo
val method: MethodAliasInfo,
) {
companion object {
const val NOT_PROCESSED = -1
Expand Down Expand Up @@ -129,10 +129,6 @@ class StmtAliasInfo(
val (lhvNodes, lhvEdges) = trace(lhv)
val from = lhvNodes.reversed().getOrNull(1)
if (from != null) {
if (from == NOT_PROCESSED) {
println()
}

val updated = StmtAliasInfo(
baseToAlloc = baseToAlloc,
allocToFields = allocToFields.copyOf(),
Expand Down Expand Up @@ -186,19 +182,18 @@ class StmtAliasInfo(
return assign(stmt.lhv.toPath(), alloc)
}
is EtsInstanceFieldRef, is EtsStaticFieldRef -> {
val alloc = run {
val (rhvNodes, _) = trace(rhv.toPath())
val alloc = rhvNodes.last()
if (alloc == NOT_PROCESSED) run {
val fieldAlloc = method.allocationMap[MethodAliasInfo.Allocation.Imm(stmt)]
?: error("Unknown allocation")

return this
.assign(rhv.toPath(), fieldAlloc)
.assign(stmt.lhv.toPath(), fieldAlloc)
} else alloc
val (rhvNodes, _) = trace(rhv.toPath())
val alloc = rhvNodes.last()
if (alloc == NOT_PROCESSED) {
val fieldAlloc = method.allocationMap[MethodAliasInfo.Allocation.Imm(stmt)]
?: error("Unknown allocation")

return this
.assign(rhv.toPath(), fieldAlloc)
.assign(stmt.lhv.toPath(), fieldAlloc)
} else {
return assign(stmt.lhv.toPath(), alloc)
}
return assign(stmt.lhv.toPath(), alloc)
}
is EtsLocal -> {
return assign(stmt.lhv.toPath(), rhv.toPath())
Expand All @@ -221,7 +216,9 @@ class StmtAliasInfo(
?: error("Unknown new")
return assign(stmt.lhv.toPath(), new)
}
else -> error("Unprocessable")
else -> {
error("Unprocessable")
}
}
}

Expand All @@ -230,8 +227,9 @@ class StmtAliasInfo(
allocToFields.forEachIndexed { from, edges ->
edges.forEach { edge ->
val (str, to) = unwrap(edge)
if (to != NOT_PROCESSED && to != MULTIPLE_EDGE)
if (to != NOT_PROCESSED && to != MULTIPLE_EDGE) {
edgeLists[to].add(wrap(str, from))
}
}
}
edgeLists.map { it.toULongArray() }.toTypedArray()
Expand All @@ -240,15 +238,16 @@ class StmtAliasInfo(
private val invertedAllocToBase: Array<IntArray> by lazy {
val edges = Array(method.allocations.size) { mutableListOf<Int>() }
baseToAlloc.forEachIndexed { base, alloc ->
if (alloc != NOT_PROCESSED && alloc != MULTIPLE_EDGE)
if (alloc != NOT_PROCESSED && alloc != MULTIPLE_EDGE) {
edges[alloc].add(base)
}
}
edges.map { it.toIntArray() }.toTypedArray()
}

private class PathNode(
val alloc: Int,
val edge: Pair<Int, PathNode>?
val edge: Pair<Int, PathNode>?,
) {
val parent: PathNode?
get() = edge?.second
Expand All @@ -263,17 +262,23 @@ class StmtAliasInfo(
private fun accessors(node: PathNode): List<Accessor> {
var cur = node
val accessors = mutableListOf<Accessor>()
while (cur.string != null) {
accessors.add(FieldAccessor(method.strings[cur.string!!]))
cur = cur.parent!!
while (true) {
val str = cur.string
if (str == null) {
break
}

accessors.add(FieldAccessor(method.strings[str]))
cur = cur.parent ?: error("If the property is defined, the parent should exist")
}
return accessors
}

fun getAliases(path: AccessPath): Set<AccessPath> {
val alloc = trace(path).first.last()
if (alloc == NOT_PROCESSED || alloc == MULTIPLE_EDGE)
if (alloc == NOT_PROCESSED || alloc == MULTIPLE_EDGE) {
return setOf(path)
}

val queue = ArrayDeque<PathNode>()
queue.addLast(PathNode(alloc, null))
Expand All @@ -283,10 +288,12 @@ class StmtAliasInfo(
val node = queue.removeFirst()

invertedAllocToBase[node.alloc].forEach { base ->
paths.add(AccessPath(
base = method.bases[base],
accesses = accessors(node)
))
paths.add(
AccessPath(
base = method.bases[base],
accesses = accessors(node)
)
)
}

invertedAllocToField[node.alloc].forEach {
Expand All @@ -302,7 +309,7 @@ class StmtAliasInfo(
}

class MethodAliasInfo(
val method: EtsMethod
val method: EtsMethod,
) {
sealed interface Allocation {
data class New(val stmt: EtsStmt) : Allocation
Expand Down
11 changes: 8 additions & 3 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/TypeInferenceManager.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ import org.jacodb.ets.base.EtsType
import org.jacodb.ets.base.EtsUnclearRefType
import org.jacodb.ets.base.INSTANCE_INIT_METHOD_NAME
import org.jacodb.ets.graph.findDominators
import org.jacodb.ets.model.EtsClassSignature
import org.jacodb.ets.model.EtsMethod
import org.jacodb.impl.cfg.graphs.GraphDominators
import org.usvm.dataflow.ifds.ControlEvent
Expand Down Expand Up @@ -329,7 +330,9 @@ class TypeInferenceManager(
}
}.toMap()

private fun getInferredCombinedThisTypes(methodTypeScheme: Map<EtsMethod, Map<AccessPathBase, EtsTypeFact>>) = run {
private fun getInferredCombinedThisTypes(
methodTypeScheme: Map<EtsMethod, Map<AccessPathBase, EtsTypeFact>>
): Map<EtsClassSignature, EtsTypeFact> {

Check warning

Code scanning / detekt

Rule to mandate/forbid trailing commas at declaration sites Warning

Missing trailing comma before ")"
val classBySignature = graph.cp.projectAndSdkClasses
.groupByTo(hashMapOf()) { it.signature }

Expand All @@ -342,7 +345,7 @@ class TypeInferenceManager(
val forwardSummariesByClass = forwardSummaries
.entries.groupByTo(hashMapOf()) { (method, _) -> method.enclosingClass }

allClasses.mapNotNull { cls ->
return allClasses.mapNotNull { cls ->
val clsMethods = (cls.methods + cls.ctor).toHashSet()
val combinedBackwardType = clsMethods
.mapNotNull { methodTypeScheme[it] }
Expand Down Expand Up @@ -383,7 +386,9 @@ class TypeInferenceManager(
var refined: EtsTypeFact = combinedBackwardType
for ((property, propertyType) in propertyRefinements) {
refined = refined.refineProperty(property, propertyType) ?: this@TypeInferenceManager.run {
logger.warn { "Empty intersection type: ${refined.toStringLimited()} & ${propertyType.toStringLimited()}" }
logger.warn {
"Empty intersection type: ${refined.toStringLimited()} & ${propertyType.toStringLimited()}"
}
refined
}
}
Expand Down
12 changes: 7 additions & 5 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/EtsSceneAnnotator.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ import org.jacodb.ets.model.EtsFile
import org.jacodb.ets.model.EtsMethod
import org.jacodb.ets.model.EtsMethodImpl
import org.jacodb.ets.model.EtsScene
import org.usvm.dataflow.ts.infer.TypeInferenceResult

fun EtsScene.annotateWithTypes(scheme: TypeScheme): EtsScene =
EtsSceneAnnotator(this, scheme).annotate()
Expand Down Expand Up @@ -87,10 +86,13 @@ class EtsSceneAnnotator(
val valueAnnotator = ValueTypeAnnotator(typeScheme, thisType)
val exprAnnotator = ExprTypeAnnotator(scene, valueAnnotator)
val stmtTypeAnnotator = StmtTypeAnnotator(valueAnnotator, exprAnnotator)
val relocator = RelocateStmt(method)
val stmts = cfg.stmts.associateWith { it.accept(stmtTypeAnnotator).accept(relocator) }
val successorMap = cfg.stmts.map { stmts[it]!! to cfg.successors(it).map { stmts[it]!! }.toList() }
method._cfg = EtsCfg(stmts.values.toList(), successorMap.toMap())
val relocate = RelocateStmt(method)
val relocated = cfg.stmts.associateWith { it.accept(stmtTypeAnnotator).accept(relocate) }
val successorMap = cfg.stmts.map { stmt ->
val newStmt = relocated[stmt] ?: error("Unprocessed stmt")
newStmt to cfg.successors(stmt).map { relocated[it] ?: error("Unprocessed stmt") }.toList()
}
method._cfg = EtsCfg(relocated.values.toList(), successorMap.toMap())
}
}

Expand Down
10 changes: 5 additions & 5 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/TypeSchemes.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,15 +24,15 @@ import org.usvm.dataflow.ts.infer.toType

class InferredMethodTypeScheme(
method: EtsMethod,
typeInferenceResult: TypeInferenceResult
typeInferenceResult: TypeInferenceResult,
) : MethodTypeScheme {
val types = typeInferenceResult.inferredTypes[method].orEmpty()

override fun typeOf(base: AccessPathBase): EtsType? = types[base]?.toType()
}

class InferredTypeScheme(
private val typeInferenceResult: TypeInferenceResult
private val typeInferenceResult: TypeInferenceResult,
) : TypeScheme {
override fun methodScheme(method: EtsMethod): MethodTypeScheme =
InferredMethodTypeScheme(method, typeInferenceResult)
Expand All @@ -41,7 +41,7 @@ class InferredTypeScheme(
methods.map { methodScheme(it) }

private val methods by lazy {
with (typeInferenceResult) {
with(typeInferenceResult) {
inferredTypes.keys + inferredReturnType.keys
}
}
Expand All @@ -51,13 +51,13 @@ class InferredTypeScheme(
}

class MethodTypeSchemeImpl(
val types: Map<AccessPathBase, EtsType>
val types: Map<AccessPathBase, EtsType>,
) : MethodTypeScheme {
override fun typeOf(base: AccessPathBase): EtsType? = types[base]
}

class TypeSchemeImpl(
private val methodTypeSchemes: Map<EtsMethod, MethodTypeSchemeImpl>
private val methodTypeSchemes: Map<EtsMethod, MethodTypeSchemeImpl>,
) : TypeScheme {
override fun thisType(method: EtsMethod): EtsType? =
methodTypeSchemes[method]?.typeOf(AccessPathBase.This)
Expand Down
22 changes: 14 additions & 8 deletions usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/VerificationResult.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,17 +41,23 @@ sealed interface VerificationResult {
}

companion object {
fun from(summary: Map<EtsMethod, MethodVerificationSummary>): VerificationResult =
if (summary.values.all { it.entitySummaries.values.all { it.types.size == 1 && it.errors.isEmpty() }}) {
Success(TypeSchemeImpl(
summary.mapValues { (_, summary) ->
MethodTypeSchemeImpl(summary.entitySummaries.mapValues { (_, evs) ->
evs.types.single()
})
fun from(summary: Map<EtsMethod, MethodVerificationSummary>): VerificationResult {
val summaryIsValid = summary.values.all { methodSummary ->
methodSummary.entitySummaries.values.all { it.types.size == 1 && it.errors.isEmpty() }
}

return if (summaryIsValid) {
val methodTypeSchemes = summary.mapValues { (_, summary) ->
val types = summary.entitySummaries.mapValues { (_, entitySummary) ->
entitySummary.types.single()
}
))
MethodTypeSchemeImpl(types)
}

Success(TypeSchemeImpl(methodTypeSchemes))
} else {
Fail(summary)
}
}
}
}
6 changes: 3 additions & 3 deletions ...dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/SummaryCollector.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,20 +30,20 @@ import org.usvm.dataflow.ts.infer.toBase
data class TypeError(
val value: EtsValue,
val enclosingExpr: EtsEntity,
val description: String
val description: String,
)

data class EntityVerificationSummary(
val types: MutableSet<EtsType>,
val errors: MutableSet<TypeError>
val errors: MutableSet<TypeError>,
) {
companion object {
fun empty(): EntityVerificationSummary = EntityVerificationSummary(types = hashSetOf(), errors = hashSetOf())
}
}

data class MethodVerificationSummary(
val entitySummaries: MutableMap<AccessPathBase, EntityVerificationSummary> = mutableMapOf()
val entitySummaries: MutableMap<AccessPathBase, EntityVerificationSummary> = mutableMapOf(),
)

interface SummaryCollector {
Expand Down
16 changes: 9 additions & 7 deletions usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeResolverPerformanceTest.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,12 +76,14 @@ class EtsTypeResolverPerformanceTest {
)

val file = File(OUTPUT_FILE)
file.writeText(buildString {
appendLine("|project|min time|max time|%|")
appendLine("|:--|:--|:--|:--|")
reports.forEach {
appendLine(it.dumpToString())
file.writeText(
buildString {
appendLine("|project|min time|max time|%|")
appendLine("|:--|:--|:--|:--|")
reports.forEach {
appendLine(it.dumpToString())
}
}
})
)
}
}
}
14 changes: 7 additions & 7 deletions usvm-ts-dataflow/src/test/kotlin/org/usvm/dataflow/ts/test/utils/AbcProjects.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,18 +31,18 @@ import kotlin.io.path.Path
import kotlin.io.path.exists

object AbcProjects {
private val yourPrefixForTestFolders = ""
private val testProjectsVersion = ""
private val pathToSDK: String = ""
private const val yourPrefixForTestFolders = ""
private const val testProjectsVersion = ""
private const val pathToSDK = ""

@JvmStatic
fun projectAvailable(): Boolean {
return Path(yourPrefixForTestFolders).exists()
}

fun getAbcProject(abcPath: String): EtsScene {
val projectAbc = "${yourPrefixForTestFolders}/${testProjectsVersion}/$abcPath"
val abcScene = loadEtsProjectFromIR(Path(projectAbc), pathToSDK?.let { Path(it) })
val projectAbc = "$yourPrefixForTestFolders/$testProjectsVersion/$abcPath"
val abcScene = loadEtsProjectFromIR(Path(projectAbc), Path(pathToSDK))
return abcScene
}

Expand All @@ -62,7 +62,7 @@ object AbcProjects {

val manager = TypeInferenceManager(EtsTraits(), graphAbc)
val result = manager
.analyze(entrypoint.mainMethods, allMethods)
.analyze(entrypoint.mainMethods, allMethods, doAddKnownTypes = true)
.withGuessedTypes(guesser)

val sceneStatistics = TypeInferenceStatistics()
Expand All @@ -74,4 +74,4 @@ object AbcProjects {
}
return Pair(result, sceneStatistics)
}
}
}
Loading

0 comments on commit a9014d5

Please sign in to comment.