Skip to content

Disabled NPE checks for non-public library fields by default #353

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 8 commits into from
Jul 7, 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
19 changes: 10 additions & 9 deletions docs/SpeculativeFieldNonNullability.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,15 @@ most of generated branches would be `NPE` branches, while useful paths could be

Beyond that, in many cases the `null` value of a field can't be generated using the public API
of the class. This is particularly true for final fields, especially in system classes.
Automatically generated tests assign `null` values to fields in questions using reflection,
it is also often true for non-public fields from standard library and third-party libraries (even setters often do not
allow `null` values). Automatically generated tests assign `null` values to fields using reflection,
but these tests may be uninformative as the corresponding `NPE` branches would never occur
in the real code that limits itself to the public API.

## The solution

To discard irrelevant `NPE` branches, we can speculatively mark fields we as non-nullable even they
do not have an explicit `@NotNull` annotation. In particular, we can use this approach to final
do not have an explicit `@NotNull` annotation. In particular, we can use this approach to final and non-public
fields of system classes, as they are usually correctly initialized and are not equal `null`.

At the same time, we can't always add the "not null" hard constraint for the field: it would break
Expand All @@ -38,18 +39,18 @@ no way to check whether the address corresponds to a final field, as the corresp
of the global graph would refer to a local variable. The only place where we have the complete
information about the field is this method.

We use the following approach. If the field is final and belongs to a system class,
we mark it as a speculatively non-nullable in the memory
We use the following approach. If the field belongs to a library class (according to `soot.SootClass.isLibraryClass`)
and is final or non-public, we mark it as a speculatively non-nullable in the memory
(see `org.utbot.engine.Memory.speculativelyNotNullAddresses`). During the NPE check
we will add the `!isSpeculativelyNotNull(addr(field))` constraint
to the `NPE` branch together with the usual `addr(field) == null` constraint.

For final fields, these two conditions can't be satisfied at the same time, as we speculatively
mark final fields as non-nullable. As a result, the NPE branch would be discarded. If a field
is not final, the condition is satisfiable, so the NPE branch would stay alive.
For final/non-public fields, these two conditions can't be satisfied at the same time, as we speculatively
mark such fields as non-nullable. As a result, the NPE branch would be discarded. If a field
is public or not final, the condition is satisfiable, so the NPE branch would stay alive.

We limit this approach to the system classes only, because it is hard to speculatively assume
something about non-nullability of final fields in the user code.
We limit this approach to the library classes only, because it is hard to speculatively assume
something about non-nullability of final/non-public fields in the user code.

The same approach can be extended for other cases where we want to speculatively consider some
fields as non-nullable to prevent `NPE` branch generation.
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
package org.utbot.framework

import mu.KotlinLogging
import org.utbot.common.PathUtil.toPath
import java.io.IOException

private val logger = KotlinLogging.logger {}

private val defaultUserTrustedLibrariesPath: String = "${utbotHomePath}/trustedLibraries.txt"
private const val userTrustedLibrariesKey: String = "utbot.settings.trusted.libraries.path"

object TrustedLibraries {
/**
* Always "trust" JDK.
*/
private val defaultTrustedLibraries: List<String> = listOf(
"java",
"sun",
"javax",
"com.sun",
"org.omg",
"org.xml",
"org.w3c.dom",
)

private val userTrustedLibraries: List<String>
get() {
val userTrustedLibrariesPath = System.getProperty(userTrustedLibrariesKey) ?: defaultUserTrustedLibrariesPath
val userTrustedLibrariesFile = userTrustedLibrariesPath.toPath().toFile()

if (!userTrustedLibrariesFile.exists()) {
return emptyList()
}

return try {
userTrustedLibrariesFile.readLines()
} catch (e: IOException) {
logger.info { e.message }

emptyList()
}
}

/**
* Represents prefixes of packages for trusted libraries -
* as the union of [defaultTrustedLibraries] and [userTrustedLibraries].
*/
val trustedLibraries: Set<String> by lazy { (defaultTrustedLibraries + userTrustedLibraries).toSet() }
}
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,16 @@ import kotlin.reflect.KProperty

private val logger = KotlinLogging.logger {}

/**
* Path to the utbot home folder.
*/
internal val utbotHomePath = "${System.getProperty("user.home")}/.utbot"

/**
* Default path for properties file
*/
internal val defaultSettingsPath = "${System.getProperty("user.home")}/.utbot/settings.properties"
internal const val defaultKeyForSettingsPath = "utbot.settings.path"
private val defaultSettingsPath = "$utbotHomePath/settings.properties"
private const val defaultKeyForSettingsPath = "utbot.settings.path"

internal class SettingDelegate<T>(val initializer: () -> T) {
private var value = initializer()
Expand Down Expand Up @@ -176,13 +181,22 @@ object UtSettings {
var enableMachineLearningModule by getBooleanProperty(true)

/**
* Options below regulate which NullPointerExceptions check should be performed.
* Options below regulate which [NullPointerException] check should be performed.
*
* Set an option in true if you want to perform NPE check in the corresponding situations, otherwise set false.
*/
var checkNpeInNestedMethods by getBooleanProperty(true)
var checkNpeInNestedNotPrivateMethods by getBooleanProperty(false)
var checkNpeForFinalFields by getBooleanProperty(false)

/**
* This option determines whether we should generate [NullPointerException] checks for final or non-public fields
* in non-application classes. Set by true, this option highly decreases test's readability in some cases
* because of using reflection API for setting final/non-public fields in non-application classes.
*
* NOTE: default false value loses some executions with NPE in system classes, but often most of these executions
* are not expected by user.
*/
var maximizeCoverageUsingReflection by getBooleanProperty(false)

/**
* Activate or deactivate substituting static fields values set in static initializer
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ import org.utbot.engine.symbolic.asHardConstraint
import org.utbot.engine.symbolic.asSoftConstraint
import org.utbot.engine.symbolic.asAssumption
import org.utbot.engine.symbolic.asUpdate
import org.utbot.engine.util.trusted.isFromTrustedLibrary
import org.utbot.engine.util.mockListeners.MockListener
import org.utbot.engine.util.mockListeners.MockListenerController
import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues
Expand All @@ -116,7 +117,7 @@ import org.utbot.engine.util.statics.concrete.makeEnumStaticFieldsUpdates
import org.utbot.engine.util.statics.concrete.makeSymbolicValuesFromEnumConcreteValues
import org.utbot.framework.PathSelectorType
import org.utbot.framework.UtSettings
import org.utbot.framework.UtSettings.checkNpeForFinalFields
import org.utbot.framework.UtSettings.maximizeCoverageUsingReflection
import org.utbot.framework.UtSettings.checkSolverTimeoutMillis
import org.utbot.framework.UtSettings.enableFeatureProcess
import org.utbot.framework.UtSettings.pathSelectorStepsLimit
Expand Down Expand Up @@ -339,7 +340,13 @@ class UtBotSymbolicEngine(

private val classUnderTest: ClassId = methodUnderTest.clazz.id

private val mocker: Mocker = Mocker(mockStrategy, classUnderTest, hierarchy, chosenClassesToMockAlways, MockListenerController(controller))
private val mocker: Mocker = Mocker(
mockStrategy,
classUnderTest,
hierarchy,
chosenClassesToMockAlways,
MockListenerController(controller)
)

private val statesForConcreteExecution: MutableList<ExecutionState> = mutableListOf()

Expand Down Expand Up @@ -2233,14 +2240,37 @@ class UtBotSymbolicEngine(
}

// See docs/SpeculativeFieldNonNullability.md for details
if (field.isFinal && field.declaringClass.isLibraryClass && !checkNpeForFinalFields) {
markAsSpeculativelyNotNull(createdField.addr)
}
checkAndMarkLibraryFieldSpeculativelyNotNull(field, createdField)
}

return createdField
}

/**
* Marks the [createdField] as speculatively not null if the [field] is considering as
* not producing [NullPointerException].
*
* @see [SootField.speculativelyCannotProduceNullPointerException], [markAsSpeculativelyNotNull], [isFromTrustedLibrary].
*/
private fun checkAndMarkLibraryFieldSpeculativelyNotNull(field: SootField, createdField: SymbolicValue) {
if (maximizeCoverageUsingReflection || !field.declaringClass.isFromTrustedLibrary()) {
return
}

if (field.speculativelyCannotProduceNullPointerException()) {
markAsSpeculativelyNotNull(createdField.addr)
}
}

/**
* Checks whether accessing [this] field (with a method invocation or field access) speculatively can produce
* [NullPointerException] (according to its finality or accessibility).
*
* @see docs/SpeculativeFieldNonNullability.md for more information.
*/
@Suppress("KDocUnresolvedReference")
private fun SootField.speculativelyCannotProduceNullPointerException(): Boolean = isFinal || !isPublic

private fun createArray(pName: String, type: ArrayType): ArrayValue {
val addr = UtAddrExpression(mkBVConst(pName, UtIntSort))
return createArray(addr, type, useConcreteType = false)
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
package org.utbot.engine.util.trusted

import org.utbot.framework.TrustedLibraries
import soot.SootClass

/**
* Cache for already discovered trusted/untrusted packages.
*/
private val isPackageTrusted: MutableMap<String, Boolean> = mutableMapOf()

/**
* Determines whether [this] class is from trusted libraries as defined in [TrustedLibraries].
*/
fun SootClass.isFromTrustedLibrary(): Boolean {
isPackageTrusted[packageName]?.let {
return it
}

val isTrusted = TrustedLibraries.trustedLibraries.any { packageName.startsWith(it, ignoreCase = false) }

return isTrusted.also { isPackageTrusted[packageName] = it }
}
Original file line number Diff line number Diff line change
Expand Up @@ -2826,3 +2826,13 @@ inline fun <reified T> withFeaturePath(featurePath: String, block: () -> T): T {
UtSettings.enableFeatureProcess = prevEnableFeatureProcess
}
}

inline fun <reified T> withUsingReflectionForMaximizingCoverage(maximizeCoverage: Boolean, block: () -> T): T {
val prev = UtSettings.maximizeCoverageUsingReflection
UtSettings.maximizeCoverageUsingReflection = maximizeCoverage
try {
return block()
} finally {
UtSettings.maximizeCoverageUsingReflection = prev
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
package org.utbot.examples.stdlib

import org.junit.jupiter.api.Tag
import org.junit.jupiter.api.Test
import org.utbot.examples.AbstractTestCaseGeneratorTest
import org.utbot.examples.eq
import org.utbot.examples.isException
import org.utbot.examples.withUsingReflectionForMaximizingCoverage
import java.util.Date

class DateExampleTest : AbstractTestCaseGeneratorTest(testClass = DateExample::class) {
@Suppress("SpellCheckingInspection")
@Tag("slow")
@Test
fun testGetTimeWithNpeChecksForNonPublicFields() {
withUsingReflectionForMaximizingCoverage(maximizeCoverage = true) {
checkWithException(
DateExample::getTime,
eq(5),
*commonMatchers,
{ date: Date?, r: Result<Boolean> ->
val cdate = date!!.getDeclaredFieldValue("cdate")
val calendarDate = cdate!!.getDeclaredFieldValue("date")

calendarDate == null && r.isException<NullPointerException>()
},
{ date: Date?, r: Result<Boolean> ->
val cdate = date!!.getDeclaredFieldValue("cdate")
val calendarDate = cdate!!.getDeclaredFieldValue("date")

val gcal = date.getDeclaredFieldValue("gcal")

val normalized = calendarDate!!.getDeclaredFieldValue("normalized") as Boolean
val gregorianYear = calendarDate.getDeclaredFieldValue("gregorianYear") as Int

gcal == null && !normalized && gregorianYear >= 1582 && r.isException<NullPointerException>()
}
)
}
}

@Test
fun testGetTimeWithoutReflection() {
withUsingReflectionForMaximizingCoverage(maximizeCoverage = false) {
checkWithException(
DateExample::getTime,
eq(3),
*commonMatchers
)
}
}

private val commonMatchers = arrayOf(
{ date: Date?, r: Result<Boolean> -> date == null && r.isException<NullPointerException>() },
{ date: Date?, r: Result<Boolean> -> date != null && date.time == 100L && r.getOrThrow() },
{ date: Date?, r: Result<Boolean> -> date != null && date.time != 100L && !r.getOrThrow() }
)

private fun Any.getDeclaredFieldValue(fieldName: String): Any? {
val declaredField = javaClass.getDeclaredField(fieldName)
declaredField.isAccessible = true

return declaredField.get(this)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,7 @@ fun setOptions() {
UtSettings.warmupConcreteExecution = true
UtSettings.testMinimizationStrategyType = TestSelectionStrategyType.COVERAGE_STRATEGY
UtSettings.ignoreStringLiterals = true
UtSettings.maximizeCoverageUsingReflection = true
}


Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
package org.utbot.examples.stdlib;

import java.util.Date;

public class DateExample {
public boolean getTime(Date date) {
return date.getTime() == 100;
}
}