Skip to content

New treating of artificial errors #1573

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 27, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package org.utbot.examples.math

import org.junit.jupiter.api.Disabled
import org.junit.jupiter.api.Test
import org.utbot.engine.OverflowDetectionError
import org.utbot.examples.algorithms.Sort
import org.utbot.framework.plugin.api.CodegenLanguage
import org.utbot.testcheckers.eq
Expand Down Expand Up @@ -31,8 +32,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::intOverflow,
eq(5),
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<ArithmeticException>() }, // through overflow
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<ArithmeticException>() }, // through overflow (2nd '*')
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow
{ x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow (2nd '*')
{ x, _, r -> x * x * x >= 0 && x >= 0 && r.getOrNull() == 0 },
{ x, y, r -> x * x * x > 0 && x > 0 && y == 10 && r.getOrNull() == 1 },
{ x, y, r -> x * x * x > 0 && x > 0 && y != 10 && r.getOrNull() == 0 },
Expand All @@ -47,11 +48,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::byteAddOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x + y).toByte() >= 0 && x < 0 && y < 0)
val posOverflow = ((x + y).toByte() <= 0 && x > 0 && y > 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -63,11 +64,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::byteSubOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x - y).toByte() >= 0 && x < 0 && y > 0)
val posOverflow = ((x - y).toByte() <= 0 && x > 0 && y < 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -79,8 +80,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::byteMulOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand All @@ -91,11 +92,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::shortAddOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x + y).toShort() >= 0 && x < 0 && y < 0)
val posOverflow = ((x + y).toShort() <= 0 && x > 0 && y > 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -107,11 +108,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::shortSubOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x - y).toShort() >= 0 && x < 0 && y > 0)
val posOverflow = ((x - y).toShort() <= 0 && x > 0 && y < 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -123,8 +124,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::shortMulOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand All @@ -135,11 +136,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::intAddOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x + y) >= 0 && x < 0 && y < 0)
val posOverflow = ((x + y) <= 0 && x > 0 && y > 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -151,11 +152,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::intSubOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x - y) >= 0 && x < 0 && y > 0)
val posOverflow = ((x - y) <= 0 && x > 0 && y < 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -171,8 +172,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::intMulOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand All @@ -184,11 +185,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::longAddOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x + y) >= 0 && x < 0 && y < 0)
val posOverflow = ((x + y) <= 0 && x > 0 && y > 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -200,11 +201,11 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::longSubOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ x, y, r ->
val negOverflow = ((x - y) >= 0 && x < 0 && y > 0)
val posOverflow = ((x - y) <= 0 && x > 0 && y < 0)
(negOverflow || posOverflow) && r.isException<ArithmeticException>()
(negOverflow || posOverflow) && r.isException<OverflowDetectionError>()
}, // through overflow
)
}
Expand All @@ -221,8 +222,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::longMulOverflow,
eq(2),
{ _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, r -> r.isException<ArithmeticException>() }, // through overflow
{ _, _, r -> !r.isException<OverflowDetectionError>() },
{ _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand All @@ -234,8 +235,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
OverflowExamples::incOverflow,
eq(2),
{ _, r -> !r.isException<ArithmeticException>() },
{ _, r -> r.isException<ArithmeticException>() }, // through overflow
{ _, r -> !r.isException<OverflowDetectionError>() },
{ _, r -> r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand All @@ -251,8 +252,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
// Can't use abs(x) below, because abs(Int.MIN_VALUE) == Int.MIN_VALUE.
// (Int.MAX_VALUE shr 16) is the border of square overflow and cube overflow.
// Int.MAX_VALUE.toDouble().pow(1/3.toDouble())
{ x, r -> (x > -sqrtIntMax && x < sqrtIntMax) && r.isException<ArithmeticException>() }, // through overflow
{ x, r -> (x <= -sqrtIntMax || x >= sqrtIntMax) && r.isException<ArithmeticException>() }, // through overflow
{ x, r -> (x > -sqrtIntMax && x < sqrtIntMax) && r.isException<OverflowDetectionError>() }, // through overflow
{ x, r -> (x <= -sqrtIntMax || x >= sqrtIntMax) && r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand All @@ -265,8 +266,8 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
checkWithException(
Sort::quickSort,
ignoreExecutionsNumber,
{ _, _, _, r -> !r.isException<ArithmeticException>() },
{ _, _, _, r -> r.isException<ArithmeticException>() }, // through overflow
{ _, _, _, r -> !r.isException<OverflowDetectionError>() },
{ _, _, _, r -> r.isException<OverflowDetectionError>() }, // through overflow
)
}
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
package org.utbot.engine

/**
* Represents an error that may be detected or not
* during analysis in accordance with custom settings.
*
* Usually execution may be continued somehow after such error,
* but the result may be different from basic expectations.
*/
sealed class ArtificialError(message: String): Error(message)

/**
* Represents overflow detection errors in symbolic engine,
* if a mode to detect them is turned on.
*
* See [TraversalContext.intOverflowCheck] for more details.
*/
class OverflowDetectionError(message: String): ArtificialError(message)
Original file line number Diff line number Diff line change
Expand Up @@ -63,11 +63,11 @@ fun explicitThrown(exception: Throwable, addr: UtAddrExpression, inNestedMethod:
/**
* Implicitly thrown exception. There are no difference if it happens in nested call or not.
*/
fun implicitThrown(exception: Throwable, addr: UtAddrExpression, inNestedMethod: Boolean) =
SymbolicFailure(symbolic(exception, addr), exception, explicit = false, inNestedMethod = inNestedMethod)
fun implicitThrown(throwable: Throwable, addr: UtAddrExpression, inNestedMethod: Boolean) =
SymbolicFailure(symbolic(throwable, addr), throwable, explicit = false, inNestedMethod = inNestedMethod)

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

private fun extractConcrete(symbolic: SymbolicValue) =
(symbolic.asWrapperOrNull as? ThrowableWrapper)?.throwable
Expand Down
7 changes: 3 additions & 4 deletions utbot-framework/src/main/kotlin/org/utbot/engine/Resolver.kt
Original file line number Diff line number Diff line change
Expand Up @@ -390,10 +390,9 @@ class Resolver(
return if (explicit) {
UtExplicitlyThrownException(exception, inNestedMethod)
} else {
when {
// TODO SAT-1561
exception is ArithmeticException && exception.message?.contains("overflow") == true -> UtOverflowFailure(exception)
exception is AccessControlException -> UtSandboxFailure(exception)
when (exception) {
is OverflowDetectionError -> UtOverflowFailure(exception)
is AccessControlException -> UtSandboxFailure(exception)
else -> UtImplicitlyThrownException(exception, inNestedMethod)
}
}
Expand Down
10 changes: 7 additions & 3 deletions utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
Original file line number Diff line number Diff line change
Expand Up @@ -2300,6 +2300,10 @@ class Traverser(
exception: SymbolicFailure,
conditions: Set<UtBoolExpression>
): Boolean {
if (exception.concrete is ArtificialError) {
return false
}

val classId = exception.fold(
{ it.javaClass.id },
{ (exception.symbolic as ObjectValue).type.id }
Expand Down Expand Up @@ -3406,7 +3410,7 @@ class Traverser(
}

if (overflow != null) {
implicitlyThrowException(ArithmeticException("${left.type} ${op.symbol} overflow"), setOf(overflow))
implicitlyThrowException(OverflowDetectionError("${left.type} ${op.symbol} overflow"), setOf(overflow))
queuedSymbolicStateUpdates += mkNot(overflow).asHardConstraint()
}
}
Expand Down Expand Up @@ -3482,13 +3486,13 @@ class Traverser(
}

private fun TraversalContext.implicitlyThrowException(
exception: Exception,
throwable: Throwable,
conditions: Set<UtBoolExpression>,
softConditions: Set<UtBoolExpression> = emptySet()
) {
if (environment.state.executionStack.last().doesntThrow) return

val symException = implicitThrown(exception, findNewAddr(), environment.state.isInNestedMethod())
val symException = implicitThrown(throwable, findNewAddr(), environment.state.isInNestedMethod())
if (!traverseCatchBlock(environment.state.stmt, symException, conditions)) {
environment.state.expectUndefined()
val nextState = createExceptionStateQueued(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,7 @@ abstract class TestFramework(
abstract val mainPackage: String
abstract val assertionsClass: ClassId
abstract val arraysAssertionsClass: ClassId
abstract val kotlinFailureAssertionsClass: ClassId
abstract val testAnnotation: String
abstract val testAnnotationId: ClassId
abstract val testAnnotationFqn: String
Expand Down Expand Up @@ -226,11 +227,19 @@ abstract class TestFramework(

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

val fail by lazy { assertionId("fail", objectClassId) }

val kotlinFail by lazy { kotlinFailAssertionId("fail", objectClassId) }

protected open fun assertionId(name: String, vararg params: ClassId): MethodId =
builtinStaticMethodId(assertionsClass, name, voidClassId, *params)

private fun arrayAssertionId(name: String, vararg params: ClassId): MethodId =
builtinStaticMethodId(arraysAssertionsClass, name, voidClassId, *params)

private fun kotlinFailAssertionId(name: String, vararg params: ClassId): MethodId =
builtinStaticMethodId(kotlinFailureAssertionsClass, name, voidClassId, *params)

abstract fun getRunTestsCommand(
executionInvoke: String,
classPath: String,
Expand Down Expand Up @@ -272,6 +281,8 @@ object TestNg : TestFramework(id = "TestNG",displayName = "TestNG") {
simpleName = "ArrayAsserts"
)

override val kotlinFailureAssertionsClass = assertionsClass

override val assertBooleanArrayEquals by lazy { assertionId("assertEquals", booleanArrayClassId, booleanArrayClassId) }

val throwingRunnableClassId = BuiltinClassId(
Expand Down Expand Up @@ -389,6 +400,7 @@ object Junit4 : TestFramework(id = "JUnit4",displayName = "JUnit 4") {
simpleName = "Assert"
)
override val arraysAssertionsClass = assertionsClass
override val kotlinFailureAssertionsClass = assertionsClass

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

override val arraysAssertionsClass = assertionsClass

override val kotlinFailureAssertionsClass = BuiltinClassId(
canonicalName = "org.junit.jupiter.api",
simpleName = "Assertions"
)

val assertThrows = builtinStaticMethodId(
classId = assertionsClass,
name = "assertThrows",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -309,6 +309,7 @@ enum class CgTestMethodType(val displayName: String, val isThrowing: Boolean) {
PASSED_EXCEPTION(displayName = "Thrown exceptions marked as passed", isThrowing = true),
FAILING(displayName = "Failing tests (with exceptions)", isThrowing = true),
TIMEOUT(displayName = "Failing tests (with timeout)", isThrowing = true),
ARTIFICIAL(displayName = "Failing tests (with custom exception)", isThrowing = true),
CRASH(displayName = "Possibly crashing tests", isThrowing = true),
PARAMETRIZED(displayName = "Parametrized tests", isThrowing = false);

Expand Down
Loading