Skip to content

Commit 9f4af0b

Browse files
EgorkaKulikovEgorkaKulikov
authored
Use symbolic result instead of concrete if it is better (#2700)
1 parent 9eadf92 commit 9f4af0b

File tree

4 files changed

+129
-42
lines changed

4 files changed

+129
-42
lines changed

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

Lines changed: 87 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ import org.jacodb.api.ext.jcdbSignature
99
import org.usvm.instrumentation.testcase.api.UTestExecutionExceptionResult
1010
import org.usvm.instrumentation.testcase.api.UTestExecutionFailedResult
1111
import org.usvm.instrumentation.testcase.api.UTestExecutionInitFailedResult
12-
import org.usvm.instrumentation.testcase.api.UTestExecutionResult
1312
import org.usvm.instrumentation.testcase.api.UTestExecutionState
1413
import org.usvm.instrumentation.testcase.api.UTestExecutionSuccessResult
1514
import org.usvm.instrumentation.testcase.api.UTestExecutionTimedOutResult
@@ -20,6 +19,10 @@ import org.usvm.instrumentation.util.enclosingClass
2019
import org.usvm.instrumentation.util.enclosingMethod
2120
import org.utbot.common.isPublic
2221
import org.utbot.contest.usvm.jc.JcExecution
22+
import org.utbot.contest.usvm.jc.UTestConcreteExecutionResult
23+
import org.utbot.contest.usvm.jc.UTestResultWrapper
24+
import org.utbot.contest.usvm.jc.UTestSymbolicExceptionResult
25+
import org.utbot.contest.usvm.jc.UTestSymbolicSuccessResult
2326
import org.utbot.framework.codegen.domain.builtin.UtilMethodProvider
2427
import org.utbot.framework.plugin.api.ClassId
2528
import org.utbot.framework.plugin.api.Coverage
@@ -65,56 +68,91 @@ class JcToUtExecutionConverter(
6568
private var uTestProcessResult = instToModelConverter.processUTest()
6669

6770
fun convert(): UtExecution? {
68-
val coverage = convertCoverage(getTrace(jcExecution.uTestExecutionResult), jcExecution.method.enclosingType.jcClass)
71+
val coverage = convertCoverage(getTrace(jcExecution.uTestExecutionResultWrapper), jcExecution.method.enclosingType.jcClass)
6972

70-
val utUsvmExecution: UtUsvmExecution = when (val executionResult = jcExecution.uTestExecutionResult) {
71-
is UTestExecutionSuccessResult -> UtUsvmExecution(
72-
stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
73-
stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
74-
// TODO usvm-sbft: ask why `UTestExecutionSuccessResult.result` is nullable
75-
result = UtExecutionSuccess(executionResult.result?.let {
76-
jcToUtModelConverter.convert(it, EnvironmentStateKind.FINAL)
77-
} ?: UtVoidModel),
78-
coverage = coverage,
79-
instrumentation = uTestProcessResult.instrumentation,
80-
)
81-
is UTestExecutionExceptionResult -> {
73+
val utUsvmExecution: UtUsvmExecution = when (jcExecution.uTestExecutionResultWrapper) {
74+
is UTestSymbolicExceptionResult -> {
8275
UtUsvmExecution(
83-
stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
84-
stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
76+
stateBefore = constructStateBeforeFromUTest(),
77+
stateAfter = MissingState,
8578
result = createExecutionFailureResult(
86-
executionResult.cause,
87-
jcExecution.method,
79+
exceptionDescriptor = UTestExceptionDescriptor(
80+
type = jcExecution.uTestExecutionResultWrapper.exceptionType,
81+
message = "",
82+
stackTrace = emptyList(),
83+
raisedByUserCode = true,
84+
),
85+
jcTypedMethod = jcExecution.method,
8886
),
8987
coverage = coverage,
9088
instrumentation = uTestProcessResult.instrumentation,
9189
)
9290
}
9391

94-
is UTestExecutionInitFailedResult -> {
95-
logger.warn(convertException(executionResult.cause)) {
96-
"Execution failed before method under test call on ${jcExecution.method.method}"
97-
}
98-
null
99-
}
92+
is UTestSymbolicSuccessResult -> {
93+
val resultWrapper = jcExecution.uTestExecutionResultWrapper
94+
resultWrapper.initStatements.forEach { instToModelConverter.processInst(it) }
95+
instToModelConverter.processInst(resultWrapper.result)
10096

101-
is UTestExecutionFailedResult -> {
102-
logger.error(convertException(executionResult.cause)) {
103-
"Concrete execution failed on ${jcExecution.method.method}"
104-
}
105-
null
106-
}
97+
val resultUtModel = instToModelConverter.findModelByInst(resultWrapper.result)
10798

108-
is UTestExecutionTimedOutResult -> {
109-
logger.warn { "Timeout on ${jcExecution.method.method}" }
11099
UtUsvmExecution(
111100
stateBefore = constructStateBeforeFromUTest(),
112101
stateAfter = MissingState,
113-
result = UtTimeoutException(TimeoutException("Concrete execution timed out")),
102+
result = UtExecutionSuccess(resultUtModel),
114103
coverage = coverage,
115104
instrumentation = uTestProcessResult.instrumentation,
116105
)
117106
}
107+
108+
is UTestConcreteExecutionResult ->
109+
when (val executionResult = jcExecution.uTestExecutionResultWrapper.uTestExecutionResult) {
110+
is UTestExecutionSuccessResult -> UtUsvmExecution(
111+
stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
112+
stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
113+
// TODO usvm-sbft: ask why `UTestExecutionSuccessResult.result` is nullable
114+
result = UtExecutionSuccess(executionResult.result?.let {
115+
jcToUtModelConverter.convert(it, EnvironmentStateKind.FINAL)
116+
} ?: UtVoidModel),
117+
coverage = coverage,
118+
instrumentation = uTestProcessResult.instrumentation,
119+
)
120+
121+
is UTestExecutionExceptionResult -> {
122+
UtUsvmExecution(
123+
stateBefore = convertState(executionResult.initialState, EnvironmentStateKind.INITIAL, jcExecution.method),
124+
stateAfter = convertState(executionResult.resultState, EnvironmentStateKind.FINAL, jcExecution.method),
125+
result = createExecutionFailureResult(executionResult.cause, jcExecution.method),
126+
coverage = coverage,
127+
instrumentation = uTestProcessResult.instrumentation,
128+
)
129+
}
130+
131+
is UTestExecutionInitFailedResult -> {
132+
logger.warn(convertException(executionResult.cause)) {
133+
"Execution failed before method under test call on ${jcExecution.method.method}"
134+
}
135+
null
136+
}
137+
138+
is UTestExecutionFailedResult -> {
139+
logger.error(convertException(executionResult.cause)) {
140+
"Concrete execution failed on ${jcExecution.method.method}"
141+
}
142+
null
143+
}
144+
145+
is UTestExecutionTimedOutResult -> {
146+
logger.warn { "Timeout on ${jcExecution.method.method}" }
147+
UtUsvmExecution(
148+
stateBefore = constructStateBeforeFromUTest(),
149+
stateAfter = MissingState,
150+
result = UtTimeoutException(TimeoutException("Concrete execution timed out")),
151+
coverage = coverage,
152+
instrumentation = uTestProcessResult.instrumentation,
153+
)
154+
}
155+
}
118156
} ?: return null
119157

120158
return utUsvmExecution
@@ -206,12 +244,22 @@ class JcToUtExecutionConverter(
206244
cache = mutableMapOf()
207245
)) as Throwable
208246

209-
private fun getTrace(executionResult: UTestExecutionResult): List<JcInst>? = when (executionResult) {
210-
is UTestExecutionExceptionResult -> executionResult.trace
211-
is UTestExecutionInitFailedResult -> executionResult.trace
212-
is UTestExecutionSuccessResult -> executionResult.trace
213-
is UTestExecutionFailedResult -> emptyList()
214-
is UTestExecutionTimedOutResult -> emptyList()
247+
/**
248+
* Gets trace from execution result if it is present.
249+
*
250+
* Otherwise, (e.g. we use symbolic result if concrete fails),
251+
* minimization will take just 'UtSettings.maxUnknownCoverageExecutionsPerMethodPerResultType' executions.
252+
*/
253+
private fun getTrace(executionResult: UTestResultWrapper): List<JcInst>? = when (executionResult) {
254+
is UTestConcreteExecutionResult -> when (val res = executionResult.uTestExecutionResult) {
255+
is UTestExecutionExceptionResult -> res.trace
256+
is UTestExecutionInitFailedResult -> res.trace
257+
is UTestExecutionSuccessResult -> res.trace
258+
is UTestExecutionFailedResult -> emptyList()
259+
is UTestExecutionTimedOutResult -> emptyList()
260+
}
261+
is UTestSymbolicExceptionResult -> emptyList()
262+
is UTestSymbolicSuccessResult -> emptyList()
215263
}
216264

217265
private fun convertState(

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ class UTestInstToUtModelConverter(
8787
}
8888
}
8989

90-
private fun processInst(uTestInst: UTestInst) {
90+
fun processInst(uTestInst: UTestInst) {
9191
when (uTestInst) {
9292
is UTestExpression -> processExpr(uTestInst)
9393

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

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,31 @@
11
package org.utbot.contest.usvm.jc
22

3+
import org.jacodb.api.JcType
34
import org.jacodb.api.JcTypedMethod
45
import org.usvm.api.JcCoverage
56
import org.usvm.instrumentation.testcase.UTest
67
import org.usvm.instrumentation.testcase.api.UTestExecutionResult
8+
import org.usvm.instrumentation.testcase.api.UTestExpression
9+
import org.usvm.instrumentation.testcase.api.UTestInst
710

811
data class JcExecution(
912
val method: JcTypedMethod,
1013
val uTest: UTest,
11-
val uTestExecutionResult: UTestExecutionResult,
14+
val uTestExecutionResultWrapper: UTestResultWrapper,
1215
val coverage: JcCoverage
1316
)
17+
18+
sealed interface UTestResultWrapper
19+
20+
class UTestConcreteExecutionResult(
21+
val uTestExecutionResult: UTestExecutionResult
22+
) : UTestResultWrapper
23+
24+
class UTestSymbolicExceptionResult(
25+
val exceptionType: JcType
26+
) : UTestResultWrapper
27+
28+
class UTestSymbolicSuccessResult(
29+
val initStatements: List<UTestInst>,
30+
val result: UTestExpression
31+
) : UTestResultWrapper

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

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,14 @@ import org.usvm.api.util.JcTestStateResolver
1414
import org.usvm.instrumentation.executor.UTestConcreteExecutor
1515
import org.usvm.instrumentation.testcase.UTest
1616
import org.usvm.instrumentation.testcase.api.UTestAllocateMemoryCall
17+
import org.usvm.instrumentation.testcase.api.UTestExecutionExceptionResult
18+
import org.usvm.instrumentation.testcase.api.UTestExecutionSuccessResult
1719
import org.usvm.instrumentation.testcase.api.UTestExpression
1820
import org.usvm.instrumentation.testcase.api.UTestMethodCall
1921
import org.usvm.instrumentation.testcase.api.UTestNullExpression
2022
import org.usvm.instrumentation.testcase.api.UTestStaticMethodCall
2123
import org.usvm.machine.JcContext
24+
import org.usvm.machine.state.JcMethodResult
2225
import org.usvm.machine.state.JcState
2326
import org.usvm.machine.state.localIdx
2427
import org.usvm.memory.ULValue
@@ -52,9 +55,27 @@ class JcTestExecutor(
5255
runner.executeAsync(uTest)
5356
}
5457

58+
// sometimes symbolic result is preferable that concolic: e.g. if concrete times out
59+
val preferableResult =
60+
if (execResult !is UTestExecutionSuccessResult && execResult !is UTestExecutionExceptionResult) {
61+
val symbolicResult = state.methodResult
62+
when (symbolicResult) {
63+
is JcMethodResult.JcException -> UTestSymbolicExceptionResult(symbolicResult.type)
64+
is JcMethodResult.Success -> {
65+
val resultScope = MemoryScope(ctx, model, state.memory, stringConstants, method)
66+
val resultExpr = resultScope.resolveExpr(symbolicResult.value, method.returnType)
67+
val resultInitializer = resultScope.decoderApi.initializerInstructions()
68+
UTestSymbolicSuccessResult(resultInitializer, resultExpr)
69+
}
70+
JcMethodResult.NoCall -> UTestConcreteExecutionResult(execResult)
71+
}
72+
} else {
73+
UTestConcreteExecutionResult(execResult)
74+
}
75+
5576
val coverage = resolveCoverage(method, state)
5677

57-
return JcExecution(method, uTest, execResult, coverage)
78+
return JcExecution(method, uTest, preferableResult, coverage)
5879
}
5980

6081
@Suppress("UNUSED_PARAMETER")

0 commit comments

Comments
 (0)