Format

Author: Lipen

usvm-dataflow-ts/build.gradle.kts

@@ -1,4 +1,3 @@
-
 import java.io.FileNotFoundException
 import java.nio.file.Files
 import java.nio.file.attribute.FileTime
@@ -82,7 +81,7 @@ val generateTestResources by tasks.registering {
                     output.relativeTo(resources).path,
                 )
                 println("Running: '${cmd.joinToString(" ")}'")
-                val process = ProcessBuilder(cmd).directory(resources).start();
+                val process = ProcessBuilder(cmd).directory(resources).start()
                 val ok = process.waitFor(10, TimeUnit.MINUTES)
 
                 val stdout = process.inputStream.bufferedReader().readText().trim()

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ExprTypeAnnotator.kt

@@ -16,18 +16,70 @@
 
 package org.usvm.dataflow.ts.infer.annotation
 
-import org.jacodb.ets.base.*
+import org.jacodb.ets.base.EtsAddExpr
+import org.jacodb.ets.base.EtsAndExpr
+import org.jacodb.ets.base.EtsAwaitExpr
+import org.jacodb.ets.base.EtsBitAndExpr
+import org.jacodb.ets.base.EtsBitNotExpr
+import org.jacodb.ets.base.EtsBitOrExpr
+import org.jacodb.ets.base.EtsBitXorExpr
+import org.jacodb.ets.base.EtsCastExpr
+import org.jacodb.ets.base.EtsClassType
+import org.jacodb.ets.base.EtsCommaExpr
+import org.jacodb.ets.base.EtsDeleteExpr
+import org.jacodb.ets.base.EtsDivExpr
+import org.jacodb.ets.base.EtsEntity
+import org.jacodb.ets.base.EtsEqExpr
+import org.jacodb.ets.base.EtsExpExpr
+import org.jacodb.ets.base.EtsExpr
+import org.jacodb.ets.base.EtsGtEqExpr
+import org.jacodb.ets.base.EtsGtExpr
+import org.jacodb.ets.base.EtsInExpr
+import org.jacodb.ets.base.EtsInstanceCallExpr
+import org.jacodb.ets.base.EtsInstanceOfExpr
+import org.jacodb.ets.base.EtsLeftShiftExpr
+import org.jacodb.ets.base.EtsLengthExpr
+import org.jacodb.ets.base.EtsLocal
+import org.jacodb.ets.base.EtsLtEqExpr
+import org.jacodb.ets.base.EtsLtExpr
+import org.jacodb.ets.base.EtsMulExpr
+import org.jacodb.ets.base.EtsNegExpr
+import org.jacodb.ets.base.EtsNewArrayExpr
+import org.jacodb.ets.base.EtsNewExpr
+import org.jacodb.ets.base.EtsNotEqExpr
+import org.jacodb.ets.base.EtsNotExpr
+import org.jacodb.ets.base.EtsNullishCoalescingExpr
+import org.jacodb.ets.base.EtsOrExpr
+import org.jacodb.ets.base.EtsPostDecExpr
+import org.jacodb.ets.base.EtsPostIncExpr
+import org.jacodb.ets.base.EtsPreDecExpr
+import org.jacodb.ets.base.EtsPreIncExpr
+import org.jacodb.ets.base.EtsPtrCallExpr
+import org.jacodb.ets.base.EtsRemExpr
+import org.jacodb.ets.base.EtsRightShiftExpr
+import org.jacodb.ets.base.EtsStaticCallExpr
+import org.jacodb.ets.base.EtsStrictEqExpr
+import org.jacodb.ets.base.EtsStrictNotEqExpr
+import org.jacodb.ets.base.EtsSubExpr
+import org.jacodb.ets.base.EtsTernaryExpr
+import org.jacodb.ets.base.EtsTypeOfExpr
+import org.jacodb.ets.base.EtsUnaryPlusExpr
+import org.jacodb.ets.base.EtsUnsignedRightShiftExpr
+import org.jacodb.ets.base.EtsValue
+import org.jacodb.ets.base.EtsVoidExpr
+import org.jacodb.ets.base.EtsYieldExpr
 import org.jacodb.ets.model.EtsScene
 
 class ExprTypeAnnotator(
     private val valueAnnotator: ValueTypeAnnotator,
-    private val scene: EtsScene
+    private val scene: EtsScene,
 ) : EtsExpr.Visitor<EtsExpr> {
     private fun inferEntity(entity: EtsEntity) = when (entity) {
         is EtsExpr -> entity.accept(this)
         is EtsValue -> entity.accept(valueAnnotator)
         else -> error("Unsupported entity")
     }
+
     private fun inferValue(value: EtsValue) = value.accept(valueAnnotator)
 
     override fun visit(expr: EtsNewExpr) = expr
@@ -197,6 +249,7 @@ class ExprTypeAnnotator(
                     ?: return expr.copy(instance = baseInferred, args = argsInferred)
                 callee.signature
             }
+
             else -> expr.method
         }
         return EtsInstanceCallExpr(baseInferred, methodInferred, argsInferred)

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/StmtTypeAnnotator.kt

@@ -16,9 +16,22 @@
 
 package org.usvm.dataflow.ts.infer.annotation
 
-import org.jacodb.ets.base.*
+import org.jacodb.ets.base.EtsAssignStmt
+import org.jacodb.ets.base.EtsCallExpr
+import org.jacodb.ets.base.EtsCallStmt
+import org.jacodb.ets.base.EtsEntity
+import org.jacodb.ets.base.EtsExpr
+import org.jacodb.ets.base.EtsGotoStmt
+import org.jacodb.ets.base.EtsIfStmt
+import org.jacodb.ets.base.EtsNopStmt
+import org.jacodb.ets.base.EtsReturnStmt
+import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.base.EtsSwitchStmt
+import org.jacodb.ets.base.EtsThrowStmt
+import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.model.EtsScene
-import org.usvm.dataflow.ts.infer.*
+import org.usvm.dataflow.ts.infer.AccessPathBase
+import org.usvm.dataflow.ts.infer.EtsTypeFact
 
 class StmtTypeAnnotator(
     types: Map<AccessPathBase, EtsTypeFact>,

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/annotation/ValueTypeAnnotator.kt

@@ -36,9 +36,9 @@ import org.usvm.dataflow.ts.infer.dto.toType
 class ValueTypeAnnotator(
     private val types: Map<AccessPathBase, EtsTypeFact>,
     private val thisType: EtsTypeFact?,
-    private val scene: EtsScene
+    private val scene: EtsScene,
 ) : EtsValue.Visitor.Default<EtsValue> {
-    private inline fun <V, reified T: EtsType> V.infer(base: AccessPathBase, apply: V.(T) -> V): V {
+    private inline fun <V, reified T : EtsType> V.infer(base: AccessPathBase, apply: V.(T) -> V): V {
         val type = types[base]?.toType() as? T ?: return this
         return apply.invoke(this, type)
     }

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/cli/InferTypes.kt

@@ -35,7 +35,6 @@ import kotlinx.serialization.json.encodeToStream
 import mu.KotlinLogging
 import org.jacodb.ets.base.ANONYMOUS_CLASS_PREFIX
 import org.jacodb.ets.base.ANONYMOUS_METHOD_PREFIX
-import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.loadEtsProjectFromMultipleIR
 import org.usvm.dataflow.ts.infer.EntryPointsProcessor
 import org.usvm.dataflow.ts.infer.TypeInferenceManager

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/EntityId.kt

@@ -26,54 +26,54 @@ import org.jacodb.ets.model.EtsMethodSignature
 sealed interface EntityId
 
 data class ClassId(
-    val signature: EtsClassSignature
+    val signature: EtsClassSignature,
 ) : EntityId
 
 data class MethodId(
     val name: String,
-    val enclosingClass: ClassId
+    val enclosingClass: ClassId,
 ) {
     constructor(signature: EtsMethodSignature)
-            : this(signature.name, ClassId(signature.enclosingClass))
+        : this(signature.name, ClassId(signature.enclosingClass))
 }
 
 data class FieldId(
     val name: String,
-    val enclosingClass: ClassId
+    val enclosingClass: ClassId,
 ) : EntityId {
     constructor(signature: EtsFieldSignature)
-            : this(signature.name, ClassId(signature.enclosingClass))
+        : this(signature.name, ClassId(signature.enclosingClass))
 }
 
 data class ParameterId(
     val index: Int,
-    val method: MethodId
+    val method: MethodId,
 ) : EntityId {
     constructor(parameter: EtsMethodParameter, methodSignature: EtsMethodSignature)
-            : this(parameter.index, MethodId(methodSignature))
+        : this(parameter.index, MethodId(methodSignature))
 
     constructor(etsParameterRef: EtsParameterRef, methodSignature: EtsMethodSignature)
-            : this(etsParameterRef.index, MethodId(methodSignature))
+        : this(etsParameterRef.index, MethodId(methodSignature))
 }
 
 data class ReturnId(
-    val method: MethodId
+    val method: MethodId,
 ) : EntityId {
     constructor(methodSignature: EtsMethodSignature)
-            : this(MethodId(methodSignature))
+        : this(MethodId(methodSignature))
 }
 
 data class LocalId(
     val name: String,
-    val method: MethodId
+    val method: MethodId,
 ) : EntityId {
     constructor(local: EtsLocal, methodSignature: EtsMethodSignature)
-            : this(local.name, MethodId(methodSignature))
+        : this(local.name, MethodId(methodSignature))
 }
 
 data class ThisId(
-    val method: MethodId
+    val method: MethodId,
 ) : EntityId {
     constructor(methodSignature: EtsMethodSignature)
-            : this(MethodId(methodSignature))
+        : this(MethodId(methodSignature))
 }

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ClassSummaryCollector.kt

@@ -21,7 +21,7 @@ import org.jacodb.ets.model.EtsClass
 import org.usvm.dataflow.ts.infer.verify.EntityId
 
 class ClassSummaryCollector(
-    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>
+    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>,
 ) : SummaryCollector {
     fun collect(etsClass: EtsClass) {
         etsClass.fields.forEach { field ->

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ExprSummaryCollector.kt

@@ -20,20 +20,20 @@ import org.jacodb.ets.base.EtsBinaryExpr
 import org.jacodb.ets.base.EtsEntity
 import org.jacodb.ets.base.EtsExpr
 import org.jacodb.ets.base.EtsInstanceCallExpr
+import org.jacodb.ets.base.EtsInstanceOfExpr
+import org.jacodb.ets.base.EtsLengthExpr
 import org.jacodb.ets.base.EtsPtrCallExpr
 import org.jacodb.ets.base.EtsStaticCallExpr
 import org.jacodb.ets.base.EtsTernaryExpr
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsUnaryExpr
 import org.jacodb.ets.base.EtsValue
-import org.jacodb.ets.base.EtsInstanceOfExpr
-import org.jacodb.ets.base.EtsLengthExpr
 import org.jacodb.ets.model.EtsMethodSignature
 import org.usvm.dataflow.ts.infer.verify.EntityId
 
 class ExprSummaryCollector(
     override val enclosingMethod: EtsMethodSignature,
-    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>
+    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>,
 ) : MethodSummaryCollector, EtsExpr.Visitor.Default<Unit> {
     private val valueSummaryCollector by lazy {
         ValueSummaryCollector(enclosingMethod, typeSummary)

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/StmtSummaryCollector.kt

@@ -34,7 +34,7 @@ import org.usvm.dataflow.ts.infer.verify.EntityId
 
 class StmtSummaryCollector(
     override val enclosingMethod: EtsMethodSignature,
-    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>
+    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>,
 ) : EtsStmt.Visitor<Unit>, MethodSummaryCollector {
     private val exprCollector = ExprSummaryCollector(enclosingMethod, typeSummary)
     private val valueCollector = ValueSummaryCollector(enclosingMethod, typeSummary)
@@ -77,4 +77,4 @@ class StmtSummaryCollector(
         stmt.cases.forEach { collect(it) }
     }
 
-}
+}

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/infer/verify/collectors/ValueSummaryCollector.kt

@@ -33,7 +33,7 @@ import org.usvm.dataflow.ts.infer.verify.EntityId
 
 class ValueSummaryCollector(
     override val enclosingMethod: EtsMethodSignature,
-    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>
+    override val typeSummary: MutableMap<EntityId, MutableSet<EtsType>>,
 ) : MethodSummaryCollector, EtsValue.Visitor.Default<Unit> {
     private val exprSummaryCollector by lazy {
         ExprSummaryCollector(enclosingMethod, typeSummary)
@@ -52,6 +52,7 @@ class ValueSummaryCollector(
     override fun visit(value: EtsLocal) {
         yield(value)
     }
+
     override fun visit(value: EtsArrayLiteral) {
         value.elements.forEach { collect(it) }
     }
@@ -81,4 +82,4 @@ class ValueSummaryCollector(
     override fun visit(value: EtsStaticFieldRef) {
         yield(value.field)
     }
-}
+}

usvm-dataflow-ts/src/main/kotlin/org/usvm/dataflow/ts/util/TypeInferenceStatistics.kt

@@ -379,10 +379,12 @@ class TypeInferenceStatistics {
                         undefinedUnknownCombination++
                         InferenceStatus.UNKNOWN_UNDEFINED_COMBINATION
                     }
+
                     is EtsUndefinedType -> {
                         exactTypeInferredCorrectlyPreviouslyKnown++
                         InferenceStatus.EXACT_MATCH_PREVIOUSLY_KNOWN
                     }
+
                     else -> {
                         exactTypeInferredIncorrectlyPreviouslyKnown++
                         InferenceStatus.DIFFERENT_TYPE_FOUND
@@ -468,15 +470,15 @@ class TypeInferenceStatistics {
                 .toList()
                 .sortedBy { it.first.signature.toString() }
                 .forEach { (method, types) ->
-                appendLine("${method.signature}:")
+                    appendLine("${method.signature}:")
 
-                types
-                    .sortedWith(comparator)
-                    .forEach { (path, typeInfo, typeFact, status) ->
-                        appendLine("[${status.message}]: ${path}: $typeInfo -> $typeFact ")
-                    }
-                appendLine()
-            }
+                    types
+                        .sortedWith(comparator)
+                        .forEach { (path, typeInfo, typeFact, status) ->
+                            appendLine("[${status.message}]: ${path}: $typeInfo -> $typeFact ")
+                        }
+                    appendLine()
+                }
 
             appendLine()
             appendLine("=".repeat(42))

usvm-dataflow-ts/src/test/kotlin/org/usvm/dataflow/ts/test/EtsTypeAnnotationTest.kt

@@ -155,7 +155,7 @@ internal class EtsTypeAnnotationTest {
     private val sampleScene = EtsScene(listOf(mainFile))
 
     private class CfgBuilderContext(
-        val method: EtsMethod
+        val method: EtsMethod,
     ) {
         private val stmts = mutableListOf<EtsStmt>()
         private val successorsMap = mutableMapOf<EtsStmt, MutableList<EtsStmt>>()

usvm-dataflow-ts/src/test/resources/logback.xml

@@ -13,7 +13,7 @@
     </appender>
 
     <root level="info">
-        <appender-ref ref="STDOUT"/>
+        <appender-ref ref="STDOUT" />
         <appender-ref ref="FILE" />
     </root>
 </configuration>

usvm-util/src/main/kotlin/org/usvm/util/Logging.kt

@@ -40,7 +40,7 @@ inline fun <T> LoggerWithLogMethod.bracket(
     val startNano = System.nanoTime()
     var alreadyLogged = false
 
-    var res : Maybe<T> = Maybe.none()
+    var res: Maybe<T> = Maybe.none()
     try {
         // Note: don't replace this one with runCatching, otherwise return from lambda breaks "finished" logging.
         res = Maybe.some(block())