Use symbolic result instead of concrete if it is better (#2700)

Author: EgorkaKulikov

utbot-junit-contest/src/main/kotlin/org/utbot/contest/usvm/converter/JcToUtExecutionConverter.kt

@@ -9,7 +9,6 @@ import org.jacodb.api.ext.jcdbSignature
 import org.usvm.instrumentation.testcase.api.UTestExecutionExceptionResult
 import org.usvm.instrumentation.testcase.api.UTestExecutionFailedResult
 import org.usvm.instrumentation.testcase.api.UTestExecutionInitFailedResult
-import org.usvm.instrumentation.testcase.api.UTestExecutionResult
 import org.usvm.instrumentation.testcase.api.UTestExecutionState
 import org.usvm.instrumentation.testcase.api.UTestExecutionSuccessResult
 import org.usvm.instrumentation.testcase.api.UTestExecutionTimedOutResult
@@ -20,6 +19,10 @@ import org.usvm.instrumentation.util.enclosingClass
 import org.usvm.instrumentation.util.enclosingMethod
 import org.utbot.common.isPublic
 import org.utbot.contest.usvm.jc.JcExecution
+import org.utbot.contest.usvm.jc.UTestConcreteExecutionResult
+import org.utbot.contest.usvm.jc.UTestResultWrapper
+import org.utbot.contest.usvm.jc.UTestSymbolicExceptionResult
+import org.utbot.contest.usvm.jc.UTestSymbolicSuccessResult
 import org.utbot.framework.codegen.domain.builtin.UtilMethodProvider
 import org.utbot.framework.plugin.api.ClassId
 import org.utbot.framework.plugin.api.Coverage
@@ -65,56 +68,91 @@ class JcToUtExecutionConverter(
     private var uTestProcessResult = instToModelConverter.processUTest()
 
     fun convert(): UtExecution? {
-        val coverage = convertCoverage(getTrace(jcExecution.uTestExecutionResult), jcExecution.method.enclosingType.jcClass)
+        val coverage = convertCoverage(getTrace(jcExecution.uTestExecutionResultWrapper), jcExecution.method.enclosingType.jcClass)
 
-        val utUsvmExecution: UtUsvmExecution = when (val executionResult = jcExecution.uTestExecutionResult) {
-            is UTestExecutionSuccessResult -> UtUsvmExecution(
-                stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
-                stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
-                // TODO usvm-sbft: ask why `UTestExecutionSuccessResult.result` is nullable
-                result = UtExecutionSuccess(executionResult.result?.let {
-                    jcToUtModelConverter.convert(it, EnvironmentStateKind.FINAL)
-                } ?: UtVoidModel),
-                coverage = coverage,
-                instrumentation = uTestProcessResult.instrumentation,
-            )
-            is UTestExecutionExceptionResult -> {
+        val utUsvmExecution: UtUsvmExecution = when (jcExecution.uTestExecutionResultWrapper) {
+            is UTestSymbolicExceptionResult -> {
                 UtUsvmExecution(
-                    stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
-                    stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
+                    stateBefore = constructStateBeforeFromUTest(),
+                    stateAfter = MissingState,
                     result = createExecutionFailureResult(
-                        executionResult.cause,
-                        jcExecution.method,
+                        exceptionDescriptor = UTestExceptionDescriptor(
+                            type = jcExecution.uTestExecutionResultWrapper.exceptionType,
+                            message = "",
+                            stackTrace = emptyList(),
+                            raisedByUserCode = true,
+                        ),
+                        jcTypedMethod = jcExecution.method,
                     ),
                     coverage = coverage,
                     instrumentation = uTestProcessResult.instrumentation,
                 )
             }
 
-            is UTestExecutionInitFailedResult -> {
-                logger.warn(convertException(executionResult.cause)) {
-                    "Execution failed before method under test call on ${jcExecution.method.method}"
-                }
-                null
-            }
+            is UTestSymbolicSuccessResult -> {
+                val resultWrapper = jcExecution.uTestExecutionResultWrapper
+                resultWrapper.initStatements.forEach { instToModelConverter.processInst(it) }
+                instToModelConverter.processInst(resultWrapper.result)
 
-            is UTestExecutionFailedResult -> {
-                logger.error(convertException(executionResult.cause)) {
-                    "Concrete execution failed on ${jcExecution.method.method}"
-                }
-                null
-            }
+                val resultUtModel = instToModelConverter.findModelByInst(resultWrapper.result)
 
-            is UTestExecutionTimedOutResult -> {
-                logger.warn { "Timeout on ${jcExecution.method.method}" }
                 UtUsvmExecution(
                     stateBefore = constructStateBeforeFromUTest(),
                     stateAfter = MissingState,
-                    result = UtTimeoutException(TimeoutException("Concrete execution timed out")),
+                    result = UtExecutionSuccess(resultUtModel),
                     coverage = coverage,
                     instrumentation = uTestProcessResult.instrumentation,
                 )
             }
+
+            is UTestConcreteExecutionResult ->
+                when (val executionResult = jcExecution.uTestExecutionResultWrapper.uTestExecutionResult) {
+                    is UTestExecutionSuccessResult -> UtUsvmExecution(
+                        stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
+                        stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
+                        // TODO usvm-sbft: ask why `UTestExecutionSuccessResult.result` is nullable
+                        result = UtExecutionSuccess(executionResult.result?.let {
+                            jcToUtModelConverter.convert(it, EnvironmentStateKind.FINAL)
+                        } ?: UtVoidModel),
+                        coverage = coverage,
+                        instrumentation = uTestProcessResult.instrumentation,
+                    )
+
+                    is UTestExecutionExceptionResult -> {
+                        UtUsvmExecution(
+                            stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
+                            stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
+                            result = createExecutionFailureResult(executionResult.cause, jcExecution.method),
+                            coverage = coverage,
+                            instrumentation = uTestProcessResult.instrumentation,
+                        )
+                    }
+
+                    is UTestExecutionInitFailedResult -> {
+                        logger.warn(convertException(executionResult.cause)) {
+                            "Execution failed before method under test call on ${jcExecution.method.method}"
+                        }
+                        null
+                    }
+
+                    is UTestExecutionFailedResult -> {
+                        logger.error(convertException(executionResult.cause)) {
+                            "Concrete execution failed on ${jcExecution.method.method}"
+                        }
+                        null
+                    }
+
+                    is UTestExecutionTimedOutResult -> {
+                        logger.warn { "Timeout on ${jcExecution.method.method}" }
+                        UtUsvmExecution(
+                            stateBefore = constructStateBeforeFromUTest(),
+                            stateAfter = MissingState,
+                            result = UtTimeoutException(TimeoutException("Concrete execution timed out")),
+                            coverage = coverage,
+                            instrumentation = uTestProcessResult.instrumentation,
+                        )
+                    }
+                }
         } ?: return null
 
         return utUsvmExecution
@@ -206,12 +244,22 @@ class JcToUtExecutionConverter(
             cache = mutableMapOf()
         )) as Throwable
 
-    private fun getTrace(executionResult: UTestExecutionResult): List<JcInst>? = when (executionResult) {
-        is UTestExecutionExceptionResult -> executionResult.trace
-        is UTestExecutionInitFailedResult -> executionResult.trace
-        is UTestExecutionSuccessResult -> executionResult.trace
-        is UTestExecutionFailedResult -> emptyList()
-        is UTestExecutionTimedOutResult -> emptyList()
+    /**
+     * Gets trace from execution result if it is present.
+     *
+     * Otherwise, (e.g. we use symbolic result if concrete fails),
+     * minimization will take just 'UtSettings.maxUnknownCoverageExecutionsPerMethodPerResultType' executions.
+     */
+    private fun getTrace(executionResult: UTestResultWrapper): List<JcInst>? = when (executionResult) {
+        is UTestConcreteExecutionResult -> when (val res = executionResult.uTestExecutionResult) {
+            is UTestExecutionExceptionResult -> res.trace
+            is UTestExecutionInitFailedResult -> res.trace
+            is UTestExecutionSuccessResult -> res.trace
+            is UTestExecutionFailedResult -> emptyList()
+            is UTestExecutionTimedOutResult -> emptyList()
+        }
+        is UTestSymbolicExceptionResult -> emptyList()
+        is UTestSymbolicSuccessResult -> emptyList()
     }
 
     private fun convertState(

utbot-junit-contest/src/main/kotlin/org/utbot/contest/usvm/converter/UTestInstToUtModelConverter.kt

@@ -87,7 +87,7 @@ class UTestInstToUtModelConverter(
         }
     }
 
-    private fun processInst(uTestInst: UTestInst) {
+    fun processInst(uTestInst: UTestInst) {
         when (uTestInst) {
             is UTestExpression -> processExpr(uTestInst)
 

utbot-junit-contest/src/main/kotlin/org/utbot/contest/usvm/jc/JcExecution.kt

@@ -1,13 +1,31 @@
 package org.utbot.contest.usvm.jc
 
+import org.jacodb.api.JcType
 import org.jacodb.api.JcTypedMethod
 import org.usvm.api.JcCoverage
 import org.usvm.instrumentation.testcase.UTest
 import org.usvm.instrumentation.testcase.api.UTestExecutionResult
+import org.usvm.instrumentation.testcase.api.UTestExpression
+import org.usvm.instrumentation.testcase.api.UTestInst
 
 data class JcExecution(
     val method: JcTypedMethod,
     val uTest: UTest,
-    val uTestExecutionResult: UTestExecutionResult,
+    val uTestExecutionResultWrapper: UTestResultWrapper,
     val coverage: JcCoverage
 )
+
+sealed interface UTestResultWrapper
+
+class UTestConcreteExecutionResult(
+    val uTestExecutionResult: UTestExecutionResult
+) : UTestResultWrapper
+
+class UTestSymbolicExceptionResult(
+    val exceptionType: JcType
+) : UTestResultWrapper
+
+class UTestSymbolicSuccessResult(
+    val initStatements: List<UTestInst>,
+    val result: UTestExpression
+) : UTestResultWrapper

utbot-junit-contest/src/main/kotlin/org/utbot/contest/usvm/jc/JcTestExecutor.kt

@@ -14,11 +14,14 @@ import org.usvm.api.util.JcTestStateResolver
 import org.usvm.instrumentation.executor.UTestConcreteExecutor
 import org.usvm.instrumentation.testcase.UTest
 import org.usvm.instrumentation.testcase.api.UTestAllocateMemoryCall
+import org.usvm.instrumentation.testcase.api.UTestExecutionExceptionResult
+import org.usvm.instrumentation.testcase.api.UTestExecutionSuccessResult
 import org.usvm.instrumentation.testcase.api.UTestExpression
 import org.usvm.instrumentation.testcase.api.UTestMethodCall
 import org.usvm.instrumentation.testcase.api.UTestNullExpression
 import org.usvm.instrumentation.testcase.api.UTestStaticMethodCall
 import org.usvm.machine.JcContext
+import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.localIdx
 import org.usvm.memory.ULValue
@@ -52,9 +55,27 @@ class JcTestExecutor(
             runner.executeAsync(uTest)
         }
 
+        // sometimes symbolic result is preferable that concolic: e.g. if concrete times out
+        val preferableResult =
+            if (execResult !is UTestExecutionSuccessResult && execResult !is UTestExecutionExceptionResult) {
+            val symbolicResult = state.methodResult
+            when (symbolicResult) {
+                is JcMethodResult.JcException -> UTestSymbolicExceptionResult(symbolicResult.type)
+                is JcMethodResult.Success -> {
+                    val resultScope = MemoryScope(ctx, model, state.memory, stringConstants, method)
+                    val resultExpr = resultScope.resolveExpr(symbolicResult.value, method.returnType)
+                    val resultInitializer = resultScope.decoderApi.initializerInstructions()
+                    UTestSymbolicSuccessResult(resultInitializer, resultExpr)
+                }
+                JcMethodResult.NoCall -> UTestConcreteExecutionResult(execResult)
+            }
+        } else {
+            UTestConcreteExecutionResult(execResult)
+        }
+
         val coverage = resolveCoverage(method, state)
 
-        return JcExecution(method, uTest, execResult, coverage)
+        return JcExecution(method, uTest, preferableResult, coverage)
     }
 
     @Suppress("UNUSED_PARAMETER")