Skip to content

Commit a34e7fc

Browse files
EgorkaKulikovEgorkaKulikov
committed
New treating of Overflows
1 parent ebdb569 commit a34e7fc

File tree

14 files changed

+146
-46
lines changed

14 files changed

+146
-46
lines changed

‎utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt

Lines changed: 33 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ package org.utbot.examples.math
22

33
import org.junit.jupiter.api.Disabled
44
import org.junit.jupiter.api.Test
5+
import org.utbot.engine.OverflowDetectionError
56
import org.utbot.examples.algorithms.Sort
67
import org.utbot.framework.plugin.api.CodegenLanguage
78
import org.utbot.testcheckers.eq
@@ -31,8 +32,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
3132
checkWithException(
3233
OverflowExamples::intOverflow,
3334
eq(5),
34-
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<ArithmeticException>() }, // through overflow
35-
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<ArithmeticException>() }, // through overflow (2nd '*')
35+
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow
36+
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow (2nd '*')
3637
{ x, _, r -> x * x * x >= 0 && x >= 0 && r.getOrNull() == 0 },
3738
{ x, y, r -> x * x * x > 0 && x > 0 && y == 10 && r.getOrNull() == 1 },
3839
{ x, y, r -> x * x * x > 0 && x > 0 && y != 10 && r.getOrNull() == 0 },
@@ -47,11 +48,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
4748
checkWithException(
4849
OverflowExamples::byteAddOverflow,
4950
eq(2),
50-
{ _, _, r -> !r.isException<ArithmeticException>() },
51+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
5152
{ x, y, r ->
5253
val negOverflow = ((x + y).toByte() >= 0 && x < 0 && y < 0)
5354
val posOverflow = ((x + y).toByte() <= 0 && x > 0 && y > 0)
54-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
55+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
5556
}, // through overflow
5657
)
5758
}
@@ -63,11 +64,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
6364
checkWithException(
6465
OverflowExamples::byteSubOverflow,
6566
eq(2),
66-
{ _, _, r -> !r.isException<ArithmeticException>() },
67+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
6768
{ x, y, r ->
6869
val negOverflow = ((x - y).toByte() >= 0 && x < 0 && y > 0)
6970
val posOverflow = ((x - y).toByte() <= 0 && x > 0 && y < 0)
70-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
71+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
7172
}, // through overflow
7273
)
7374
}
@@ -79,8 +80,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
7980
checkWithException(
8081
OverflowExamples::byteMulOverflow,
8182
eq(2),
82-
{ _, _, r -> !r.isException<ArithmeticException>() },
83-
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
83+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
84+
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
8485
)
8586
}
8687
}
@@ -91,11 +92,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
9192
checkWithException(
9293
OverflowExamples::shortAddOverflow,
9394
eq(2),
94-
{ _, _, r -> !r.isException<ArithmeticException>() },
95+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
9596
{ x, y, r ->
9697
val negOverflow = ((x + y).toShort() >= 0 && x < 0 && y < 0)
9798
val posOverflow = ((x + y).toShort() <= 0 && x > 0 && y > 0)
98-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
99+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
99100
}, // through overflow
100101
)
101102
}
@@ -107,11 +108,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
107108
checkWithException(
108109
OverflowExamples::shortSubOverflow,
109110
eq(2),
110-
{ _, _, r -> !r.isException<ArithmeticException>() },
111+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
111112
{ x, y, r ->
112113
val negOverflow = ((x - y).toShort() >= 0 && x < 0 && y > 0)
113114
val posOverflow = ((x - y).toShort() <= 0 && x > 0 && y < 0)
114-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
115+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
115116
}, // through overflow
116117
)
117118
}
@@ -123,8 +124,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
123124
checkWithException(
124125
OverflowExamples::shortMulOverflow,
125126
eq(2),
126-
{ _, _, r -> !r.isException<ArithmeticException>() },
127-
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
127+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
128+
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
128129
)
129130
}
130131
}
@@ -135,11 +136,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
135136
checkWithException(
136137
OverflowExamples::intAddOverflow,
137138
eq(2),
138-
{ _, _, r -> !r.isException<ArithmeticException>() },
139+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
139140
{ x, y, r ->
140141
val negOverflow = ((x + y) >= 0 && x < 0 && y < 0)
141142
val posOverflow = ((x + y) <= 0 && x > 0 && y > 0)
142-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
143+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
143144
}, // through overflow
144145
)
145146
}
@@ -151,11 +152,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
151152
checkWithException(
152153
OverflowExamples::intSubOverflow,
153154
eq(2),
154-
{ _, _, r -> !r.isException<ArithmeticException>() },
155+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
155156
{ x, y, r ->
156157
val negOverflow = ((x - y) >= 0 && x < 0 && y > 0)
157158
val posOverflow = ((x - y) <= 0 && x > 0 && y < 0)
158-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
159+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
159160
}, // through overflow
160161
)
161162
}
@@ -171,8 +172,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
171172
checkWithException(
172173
OverflowExamples::intMulOverflow,
173174
eq(2),
174-
{ _, _, r -> !r.isException<ArithmeticException>() },
175-
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
175+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
176+
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
176177
)
177178
}
178179
}
@@ -184,11 +185,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
184185
checkWithException(
185186
OverflowExamples::longAddOverflow,
186187
eq(2),
187-
{ _, _, r -> !r.isException<ArithmeticException>() },
188+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
188189
{ x, y, r ->
189190
val negOverflow = ((x + y) >= 0 && x < 0 && y < 0)
190191
val posOverflow = ((x + y) <= 0 && x > 0 && y > 0)
191-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
192+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
192193
}, // through overflow
193194
)
194195
}
@@ -200,11 +201,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
200201
checkWithException(
201202
OverflowExamples::longSubOverflow,
202203
eq(2),
203-
{ _, _, r -> !r.isException<ArithmeticException>() },
204+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
204205
{ x, y, r ->
205206
val negOverflow = ((x - y) >= 0 && x < 0 && y > 0)
206207
val posOverflow = ((x - y) <= 0 && x > 0 && y < 0)
207-
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
208+
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
208209
}, // through overflow
209210
)
210211
}
@@ -221,8 +222,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
221222
checkWithException(
222223
OverflowExamples::longMulOverflow,
223224
eq(2),
224-
{ _, _, r -> !r.isException<ArithmeticException>() },
225-
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
225+
{ _, _, r -> !r.isException<OverflowDetectionError>() },
226+
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
226227
)
227228
}
228229
}
@@ -234,8 +235,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
234235
checkWithException(
235236
OverflowExamples::incOverflow,
236237
eq(2),
237-
{ _, r -> !r.isException<ArithmeticException>() },
238-
{ _, r -> r.isException<ArithmeticException>() }, // through overflow
238+
{ _, r -> !r.isException<OverflowDetectionError>() },
239+
{ _, r -> r.isException<OverflowDetectionError>() }, // through overflow
239240
)
240241
}
241242
}
@@ -251,8 +252,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
251252
// Can't use abs(x) below, because abs(Int.MIN_VALUE) == Int.MIN_VALUE.
252253
// (Int.MAX_VALUE shr 16) is the border of square overflow and cube overflow.
253254
// Int.MAX_VALUE.toDouble().pow(1/3.toDouble())
254-
{ x, r -> (x > -sqrtIntMax && x < sqrtIntMax) && r.isException<ArithmeticException>() }, // through overflow
255-
{ x, r -> (x <= -sqrtIntMax || x >= sqrtIntMax) && r.isException<ArithmeticException>() }, // through overflow
255+
{ x, r -> (x > -sqrtIntMax && x < sqrtIntMax) && r.isException<OverflowDetectionError>() }, // through overflow
256+
{ x, r -> (x <= -sqrtIntMax || x >= sqrtIntMax) && r.isException<OverflowDetectionError>() }, // through overflow
256257
)
257258
}
258259
}
@@ -265,8 +266,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
265266
checkWithException(
266267
Sort::quickSort,
267268
ignoreExecutionsNumber,
268-
{ _, _, _, r -> !r.isException<ArithmeticException>() },
269-
{ _, _, _, r -> r.isException<ArithmeticException>() }, // through overflow
269+
{ _, _, _, r -> !r.isException<OverflowDetectionError>() },
270+
{ _, _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
270271
)
271272
}
272273
}

‎utbot-framework/src/main/kotlin/org/utbot/engine/ArtificialErrors.kt

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package org.utbot.engine
2+
3+
/**
4+
* Represents an error that may be detected or not
5+
* during analysis in accordance with custom settings.
6+
*
7+
* Usually execution may be continued somehow after such error,
8+
* but the result may be different from basic expectations.
9+
*/
10+
sealed class ArtificialError(message: String): Error(message)
11+
12+
/**
13+
* Represents overflow detection errors in symbolic engine,
14+
* if a mode to detect them is turned on.
15+
*
16+
* See [TraversalContext.intOverflowCheck] for more details.
17+
*/
18+
class OverflowDetectionError(message: String): ArtificialError(message)

‎utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -63,11 +63,11 @@ fun explicitThrown(exception: Throwable, addr: UtAddrExpression, inNestedMethod:
6363
/**
6464
* Implicitly thrown exception. There are no difference if it happens in nested call or not.
6565
*/
66-
fun implicitThrown(exception: Throwable, addr: UtAddrExpression, inNestedMethod: Boolean) =
67-
SymbolicFailure(symbolic(exception, addr), exception, explicit = false, inNestedMethod = inNestedMethod)
66+
fun implicitThrown(throwable: Throwable, addr: UtAddrExpression, inNestedMethod: Boolean) =
67+
SymbolicFailure(symbolic(throwable, addr), throwable, explicit = false, inNestedMethod = inNestedMethod)
6868

69-
private fun symbolic(exception: Throwable, addr: UtAddrExpression) =
70-
objectValue(Scene.v().getRefType(exception.javaClass.canonicalName), addr, ThrowableWrapper(exception))
69+
private fun symbolic(throwable: Throwable, addr: UtAddrExpression) =
70+
objectValue(Scene.v().getRefType(throwable.javaClass.canonicalName), addr, ThrowableWrapper(throwable))
7171

7272
private fun extractConcrete(symbolic: SymbolicValue) =
7373
(symbolic.asWrapperOrNull as? ThrowableWrapper)?.throwable

‎utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -390,10 +390,9 @@ class Resolver(
390390
return if (explicit) {
391391
UtExplicitlyThrownException(exception, inNestedMethod)
392392
} else {
393-
when {
394-
// TODO SAT-1561
395-
exception is ArithmeticException && exception.message?.contains("overflow") == true -> UtOverflowFailure(exception)
396-
exception is AccessControlException -> UtSandboxFailure(exception)
393+
when (exception) {
394+
is OverflowDetectionError -> UtOverflowFailure(exception)
395+
is AccessControlException -> UtSandboxFailure(exception)
397396
else -> UtImplicitlyThrownException(exception, inNestedMethod)
398397
}
399398
}

‎utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2300,6 +2300,10 @@ class Traverser(
23002300
exception: SymbolicFailure,
23012301
conditions: Set<UtBoolExpression>
23022302
): Boolean {
2303+
if (exception.concrete is ArtificialError) {
2304+
return false
2305+
}
2306+
23032307
val classId = exception.fold(
23042308
{ it.javaClass.id },
23052309
{ (exception.symbolic as ObjectValue).type.id }
@@ -3406,7 +3410,7 @@ class Traverser(
34063410
}
34073411

34083412
if (overflow != null) {
3409-
implicitlyThrowException(ArithmeticException("${left.type} ${op.symbol} overflow"), setOf(overflow))
3413+
implicitlyThrowException(OverflowDetectionError("${left.type} ${op.symbol} overflow"), setOf(overflow))
34103414
queuedSymbolicStateUpdates += mkNot(overflow).asHardConstraint()
34113415
}
34123416
}
@@ -3482,13 +3486,13 @@ class Traverser(
34823486
}
34833487

34843488
private fun TraversalContext.implicitlyThrowException(
3485-
exception: Exception,
3489+
throwable: Throwable,
34863490
conditions: Set<UtBoolExpression>,
34873491
softConditions: Set<UtBoolExpression> = emptySet()
34883492
) {
34893493
if (environment.state.executionStack.last().doesntThrow) return
34903494

3491-
val symException = implicitThrown(exception, findNewAddr(), environment.state.isInNestedMethod())
3495+
val symException = implicitThrown(throwable, findNewAddr(), environment.state.isInNestedMethod())
34923496
if (!traverseCatchBlock(environment.state.stmt, symException, conditions)) {
34933497
environment.state.expectUndefined()
34943498
val nextState = createExceptionStateQueued(

‎utbot-framework/src/main/kotlin/org/utbot/framework/codegen/domain/Domain.kt

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,7 @@ abstract class TestFramework(
178178
abstract val mainPackage: String
179179
abstract val assertionsClass: ClassId
180180
abstract val arraysAssertionsClass: ClassId
181+
abstract val kotlinFailureAssertionsClass: ClassId
181182
abstract val testAnnotation: String
182183
abstract val testAnnotationId: ClassId
183184
abstract val testAnnotationFqn: String
@@ -226,11 +227,19 @@ abstract class TestFramework(
226227

227228
val assertNotEquals by lazy { assertionId("assertNotEquals", objectClassId, objectClassId) }
228229

230+
val fail by lazy { assertionId("fail", objectClassId) }
231+
232+
val kotlinFail by lazy { kotlinFailAssertionId("fail", objectClassId) }
233+
229234
protected open fun assertionId(name: String, vararg params: ClassId): MethodId =
230235
builtinStaticMethodId(assertionsClass, name, voidClassId, *params)
236+
231237
private fun arrayAssertionId(name: String, vararg params: ClassId): MethodId =
232238
builtinStaticMethodId(arraysAssertionsClass, name, voidClassId, *params)
233239

240+
private fun kotlinFailAssertionId(name: String, vararg params: ClassId): MethodId =
241+
builtinStaticMethodId(kotlinFailureAssertionsClass, name, voidClassId, *params)
242+
234243
abstract fun getRunTestsCommand(
235244
executionInvoke: String,
236245
classPath: String,
@@ -272,6 +281,8 @@ object TestNg : TestFramework(id = "TestNG",displayName = "TestNG") {
272281
simpleName = "ArrayAsserts"
273282
)
274283

284+
override val kotlinFailureAssertionsClass = assertionsClass
285+
275286
override val assertBooleanArrayEquals by lazy { assertionId("assertEquals", booleanArrayClassId, booleanArrayClassId) }
276287

277288
val throwingRunnableClassId = BuiltinClassId(
@@ -389,6 +400,7 @@ object Junit4 : TestFramework(id = "JUnit4",displayName = "JUnit 4") {
389400
simpleName = "Assert"
390401
)
391402
override val arraysAssertionsClass = assertionsClass
403+
override val kotlinFailureAssertionsClass = assertionsClass
392404

393405
val ignoreAnnotationClassId = with("$JUNIT4_PACKAGE.Ignore") {
394406
BuiltinClassId(
@@ -485,6 +497,11 @@ object Junit5 : TestFramework(id = "JUnit5", displayName = "JUnit 5") {
485497

486498
override val arraysAssertionsClass = assertionsClass
487499

500+
override val kotlinFailureAssertionsClass = BuiltinClassId(
501+
canonicalName = "org.junit.jupiter.api",
502+
simpleName = "Assertions"
503+
)
504+
488505
val assertThrows = builtinStaticMethodId(
489506
classId = assertionsClass,
490507
name = "assertThrows",

‎utbot-framework/src/main/kotlin/org/utbot/framework/codegen/domain/models/CgElement.kt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -309,6 +309,7 @@ enum class CgTestMethodType(val displayName: String, val isThrowing: Boolean) {
309309
PASSED_EXCEPTION(displayName = "Thrown exceptions marked as passed", isThrowing = true),
310310
FAILING(displayName = "Failing tests (with exceptions)", isThrowing = true),
311311
TIMEOUT(displayName = "Failing tests (with timeout)", isThrowing = true),
312+
ARTIFICIAL(displayName = "Failing tests (with custom exception)", isThrowing = true),
312313
CRASH(displayName = "Possibly crashing tests", isThrowing = true),
313314
PARAMETRIZED(displayName = "Parametrized tests", isThrowing = false);
314315

0 commit comments

Comments
 (0)