TsTestResolver extended implementation (#250)

---------

Co-authored-by: Konstantin Chukharev <lipen00@gmail.com>

Author: CaelmBleidd

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/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -202,6 +202,23 @@ class TsInterpreter(
         )
 
         val solver = ctx.solver<EtsType>()
+
+        val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics
+        val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort)
+
+        state.pathConstraints += with(ctx) {
+            mkNot(
+                mkOr(
+                    ctx.mkHeapRefEq(thisRef, ctx.mkTsNullValue()),
+                    ctx.mkHeapRefEq(thisRef, ctx.mkUndefinedValue())
+                )
+            )
+        }
+
+        // TODO fix incorrect type streams
+        // val thisTypeConstraint = state.memory.types.evalTypeEquals(thisRef, EtsClassType(method.enclosingClass))
+        // state.pathConstraints += thisTypeConstraint
+
         val model = solver.check(state.pathConstraints).ensureSat().model
         state.models = listOf(model)
 

usvm-ts/src/test/kotlin/org/usvm/samples/Null.kt

@@ -25,4 +25,4 @@ class Null : TsMethodTestRunner() {
             { a, r -> a !is TsObject.TsNull && r.number == 2.0 },
         )
     }
-}
+}

usvm-ts/src/test/kotlin/org/usvm/util/TSTestResolver.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),
@@ -173,6 +173,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
                 val signature = EtsClassSignature(it.toString(), EtsFileSignature.DEFAULT)
                 EtsClassType(signature)
             }
+
             TsObject.TsString::class -> EtsStringType
             TsObject.TsNumber::class -> EtsNumberType
             TsObject.TsNumber.Double::class -> EtsNumberType
@@ -188,6 +189,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
                 val signature = EtsClassSignature("Exception", EtsFileSignature.DEFAULT)
                 EtsClassType(signature)
             }
+
             else -> error("Unsupported type: $klass")
         }
     }
@@ -196,8 +198,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)
             }
         }
     }