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

@@ -4,6 +4,7 @@
 import mu.KotlinLogging
 import org.jacodb.ets.base.EtsAssignStmt
 import org.jacodb.ets.base.EtsCallStmt
+import org.jacodb.ets.base.EtsClassType
 import org.jacodb.ets.base.EtsGotoStmt
 import org.jacodb.ets.base.EtsIfStmt
 import org.jacodb.ets.base.EtsLocal
@@ -21,6 +22,7 @@
 import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UInterpreter
+import org.usvm.api.evalTypeEquals
 import org.usvm.api.targets.TsTarget
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.forkblacklists.UForkBlackList
@@ -202,6 +204,23 @@
         )
 
         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

@@ -16,7 +16,7 @@ class Null : TsMethodTestRunner() {
         EtsScene(listOf(file))
     }
 
-    @RepeatedTest(20)
+    @RepeatedTest(1)
     fun testIsNull() {
         val method = getMethod("Null", "isNull")
         discoverProperties<TsObject, TsObject.TsNumber>(

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)
             }
         }
     }