TsTestResolver extended implementation

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

@@ -45,8 +45,8 @@
 private val logger = KotlinLogging.logger {}
 
 class EtsProjectAnalysisTest {
-    private var tsLinesSuccess = 0L
-    private var tsLinesFailed = 0L
+    private var TsLinesSuccess = 0L
+    private var TsLinesFailed = 0L
     private var analysisTime: Duration = Duration.ZERO
     private var totalPathEdges = 0
     private var totalSinks: MutableList<TaintVulnerability<EtsStmt>> = mutableListOf()
@@ -93,9 +93,9 @@
     private fun makeReport() {
         logger.info { "Analysis Report On $PROJECT_PATH" }
         logger.info { "====================" }
-        logger.info { "Total files processed: ${tsLinesSuccess + tsLinesFailed}" }
-        logger.info { "Successfully processed lines: $tsLinesSuccess" }
-        logger.info { "Failed lines: $tsLinesFailed" }
+        logger.info { "Total files processed: ${TsLinesSuccess + TsLinesFailed}" }
+        logger.info { "Successfully processed lines: $TsLinesSuccess" }
+        logger.info { "Failed lines: $TsLinesFailed" }
         logger.info { "Total analysis time: $analysisTime" }
         logger.info { "Total path edges: $totalPathEdges" }
         logger.info { "Found sinks: ${totalSinks.size}" }
@@ -130,11 +130,11 @@
             runAnalysis(project)
             val endTime = System.currentTimeMillis()
             analysisTime += (endTime - startTime).milliseconds
-            tsLinesSuccess += fileLines
+            TsLinesSuccess += fileLines
         } catch (e: Exception) {
             logger.warn { "Failed to process '$filename': $e" }
             logger.warn { e.stackTraceToString() }
-            tsLinesFailed += fileLines
+            TsLinesFailed += fileLines
         }
     }
 

usvm-ts/src/main/kotlin/org/usvm/api/TsTest.kt

@@ -1,13 +1,26 @@
 package org.usvm.api
 
 import org.jacodb.ets.base.EtsStmt
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsField
+import org.jacodb.ets.model.EtsMethod
 
 data class TsTest(
-    val parameters: List<TsObject>,
+    val method: EtsMethod,
+    val before: TsParametersState,
+    val after: TsParametersState,
     val returnValue: TsObject,
     val trace: List<EtsStmt>? = null,
 )
 
+data class TsParametersState(
+    val thisInstance: TsObject?,
+    val parameters: List<TsObject>,
+    val globals: Map<EtsClass, List<GlobalFieldValue>>
+)
+
+data class GlobalFieldValue(val field: EtsField, val value: TsObject) // TODO is it right?????
+
 open class TsMethodCoverage
 
 object NoCoverage : TsMethodCoverage()

usvm-ts/src/test/kotlin/org/usvm/util/TSMethodTestRunner.kt

@@ -54,7 +54,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
             analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
             analysisResultsMatchers = analysisResultMatchers,
             invariants = invariants,
-            extractValuesToCheck = { r -> r.parameters + r.returnValue },
+            extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
             expectedTypesForExtractedValues = arrayOf(typeTransformer(R::class)),
             checkMode = CheckMode.MATCH_PROPERTIES,
             coverageChecker = coverageChecker
@@ -72,7 +72,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
             analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
             analysisResultsMatchers = analysisResultMatchers,
             invariants = invariants,
-            extractValuesToCheck = { r -> r.parameters + r.returnValue },
+            extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
             expectedTypesForExtractedValues = arrayOf(typeTransformer(T::class), typeTransformer(R::class)),
             checkMode = CheckMode.MATCH_PROPERTIES,
             coverageChecker = coverageChecker
@@ -90,7 +90,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
             analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
             analysisResultsMatchers = analysisResultMatchers,
             invariants = invariants,
-            extractValuesToCheck = { r -> r.parameters + r.returnValue },
+            extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
             expectedTypesForExtractedValues = arrayOf(
                 typeTransformer(T1::class), typeTransformer(T2::class), typeTransformer(R::class)
             ),
@@ -110,7 +110,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
             analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
             analysisResultsMatchers = analysisResultMatchers,
             invariants = invariants,
-            extractValuesToCheck = { r -> r.parameters + r.returnValue },
+            extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
             expectedTypesForExtractedValues = arrayOf(
                 typeTransformer(T1::class),
                 typeTransformer(T2::class),
@@ -133,7 +133,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
             analysisResultsNumberMatcher = ignoreNumberOfAnalysisResults,
             analysisResultsMatchers = analysisResultMatchers,
             invariants = invariants,
-            extractValuesToCheck = { r -> r.parameters + r.returnValue },
+            extractValuesToCheck = { r -> r.before.parameters + r.returnValue },
             expectedTypesForExtractedValues = arrayOf(
                 typeTransformer(T1::class),
                 typeTransformer(T2::class),
@@ -196,8 +196,8 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         TsMachine(scene, options).use { machine ->
             val states = machine.analyze(listOf(method))
             states.map { state ->
-                val resolver = TsTestResolver(state)
-                resolver.resolve(method)
+                val resolver = TsTestResolver()
+                resolver.resolve(method, state)
             }
         }
     }

usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.kt

@@ -16,6 +16,7 @@
 import org.jacodb.ets.base.EtsUndefinedType
 import org.jacodb.ets.base.EtsUnknownType
 import org.jacodb.ets.base.EtsVoidType
+import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassImpl
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodImpl
@@ -24,8 +25,10 @@
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.api.GlobalFieldValue
 import org.usvm.api.TsObject
 import org.usvm.api.TsTest
+import org.usvm.api.TsParametersState
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.isTrue
 import org.usvm.machine.types.FakeType
@@ -36,40 +39,91 @@
 import org.usvm.machine.expr.extractInt
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
+import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.URegisterStackLValue
 import org.usvm.model.UModelBase
 import org.usvm.types.first
 import org.usvm.types.single
 
-class TsTestResolver(
-    private val state: TsState,
-) {
-    private val ctx: TsContext get() = state.ctx
-
-    fun resolve(method: EtsMethod): TsTest = with(ctx) {
+class TsTestResolver {
+    fun resolve(method: EtsMethod, state: TsState): TsTest = with(state.ctx) {
         val model = state.models.first()
-        when (val methodResult = state.methodResult) {
-            is TsMethodResult.Success -> {
-                val value = methodResult.value
-                val valueToResolve = model.eval(value)
-                val returnValue = resolveExpr(valueToResolve, method.returnType, model)
-                val params = resolveParams(method.parameters, this, model)
+        val memory = state.memory
 
-                return TsTest(params, returnValue)
-            }
+        val beforeMemoryScope = MemoryScope(this, model, memory, method)
+        val afterMemoryScope = MemoryScope(this, model, memory, method)
 
-            is TsMethodResult.TsException -> {
-                val params = resolveParams(method.parameters, this, model)
-                return TsTest(params, TsObject.TsException)
-            }
+        val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { (this as MemoryScope).resolveState() }
+        val after = afterMemoryScope.withMode(ResolveMode.CURRENT) { (this as MemoryScope).resolveState() }
 
-            is TsMethodResult.NoCall -> {
-                TODO()
+        val result = when (val res = state.methodResult) {
+            is TsMethodResult.NoCall -> error("No result found")
+            is TsMethodResult.Success -> {
+                afterMemoryScope.withMode(ResolveMode.CURRENT) {
+                    resolveExpr(res.value, method.returnType, model)
+                }
             }
 
-            else -> error("Should not be called")
+            is TsMethodResult.TsException -> resolveException(res, afterMemoryScope)
+        }
+
+        return TsTest(method, before, after, result, trace = emptyList())
+    }
+
+    private fun resolveException(
+        res: TsMethodResult.TsException,
+        afterMemoryScope: MemoryScope,
+    ): TsObject.TsException {
+        TODO()
+    }
+
+
+    private class MemoryScope(
+        ctx: TsContext,
+        model: UModelBase<EtsType>,
+        finalStateMemory: UReadOnlyMemory<EtsType>,
+        method: EtsMethod,
+    ) : TsTestStateResolver(ctx, model, finalStateMemory, method) {
+        fun resolveState(): TsParametersState {
+            val thisInstance = resolveThisInstance()
+            val parameters = resolveParameters()
+
+            val globals = resolveGlobals()
+
+            return TsParametersState(thisInstance, parameters, globals)
         }
     }
+}
+
+open class TsTestStateResolver(
+    val ctx: TsContext,
+    private val model: UModelBase<EtsType>,
+    private val finalStateMemory: UReadOnlyMemory<EtsType>,
+    val method: EtsMethod
+) {
+    fun resolveExpr(
+        expr: UExpr<out USort>,
+        type: EtsType,
+        model: UModelBase<*>,
+    ): TsObject = when {
+        type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr, model)
+        type is EtsPrimitiveType -> resolvePrimitive(expr, type)
+        type is EtsClassType -> resolveClass(expr, type, model)
+        type is EtsRefType -> TODO()
+        else -> TODO()
+    }
+
+    fun resolveThisInstance(): TsObject? {
+        TODO()
+    }
+
+    fun resolveParameters(): List<TsObject> {
+        TODO()
+    }
+
+    fun resolveGlobals(): Map<EtsClass, List<GlobalFieldValue>> {
+        TODO()
+    }
 
     private fun resolveParams(
         params: List<EtsMethodParameter>,
@@ -79,7 +133,7 @@
         params.map { param ->
             val sort = typeToSort(param.type).takeUnless { it is TsUnresolvedSort } ?: addressSort
             val lValue = URegisterStackLValue(sort, param.index)
-            val expr = state.memory.read(lValue) // TODO error
+            val expr = finalStateMemory.read(lValue) // TODO error
             if (param.type is EtsUnknownType) {
                 resolveFakeObject(expr.cast(), model)
             } else {
@@ -89,41 +143,30 @@
     }
 
     private fun resolveFakeObject(expr: UConcreteHeapRef, model: UModelBase<EtsType>): TsObject {
-        val type = state.memory.types.getTypeStream(expr.asExpr(ctx.addressSort)).single() as FakeType
+        val type = finalStateMemory.types.getTypeStream(expr.asExpr(ctx.addressSort)).single() as FakeType
         return when {
             model.eval(type.boolTypeExpr).isTrue -> {
                 val lValue = ctx.getIntermediateBoolLValue(expr.address)
-                val value = state.memory.read(lValue)
+                val value = finalStateMemory.read(lValue)
                 resolveExpr(model.eval(value), EtsBooleanType, model)
             }
 
             model.eval(type.fpTypeExpr).isTrue -> {
                 val lValue = ctx.getIntermediateFpLValue(expr.address)
-                val value = state.memory.read(lValue)
+                val value = finalStateMemory.read(lValue)
                 resolveExpr(model.eval(value), EtsNumberType, model)
             }
 
             model.eval(type.refTypeExpr).isTrue -> {
                 val lValue = ctx.getIntermediateRefLValue(expr.address)
-                val value = state.memory.read(lValue)
+                val value = finalStateMemory.read(lValue)
                 resolveExpr(model.eval(value), EtsClassType(ctx.scene.projectAndSdkClasses.first().signature), model)
             }
 
             else -> error("Unsupported")
         }
     }
 
-    private fun resolveExpr(
-        expr: UExpr<out USort>,
-        type: EtsType,
-        model: UModelBase<*>,
-    ): TsObject = when {
-        type is EtsUnknownType && expr is UConcreteHeapRef -> resolveUnknown(expr, model)
-        type is EtsPrimitiveType -> resolvePrimitive(expr, type)
-        type is EtsClassType -> resolveClass(expr, type, model)
-        type is EtsRefType -> TODO()
-        else -> TODO()
-    }
 
     private fun resolveUnknown(
         expr: UConcreteHeapRef,
@@ -224,4 +267,20 @@
         }
         return TsObject.TsClass(clazz.name, properties)
     }
+
+    private var resolveMode: ResolveMode = ResolveMode.ERROR
+
+    fun <R> withMode(resolveMode: ResolveMode, body: TsTestStateResolver.() -> R): R {
+        val prevValue = this.resolveMode
+        try {
+            this.resolveMode = resolveMode
+            return body()
+        } finally {
+            this.resolveMode = prevValue
+        }
+    }
+}
+
+enum class ResolveMode {
+    MODEL, CURRENT, ERROR
 }