Skip to content

Commit 9222427

Browse files
committed
Add taint analysis
1 parent fc01f38 commit 9222427

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+2017
-75
lines changed

build.gradle.kts

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,10 @@ subprojects {
109109
group = rootProject.group
110110
version = rootProject.version
111111

112+
java {
113+
withSourcesJar()
114+
}
115+
112116
publishing {
113117
publications {
114118
create<MavenPublication>("jar") {
@@ -137,6 +141,10 @@ configure(
137141
project(":utbot-summary")
138142
)
139143
) {
144+
java {
145+
withSourcesJar()
146+
}
147+
140148
publishing {
141149
repositories {
142150
maven {

utbot-analytics/src/main/kotlin/org/utbot/features/UtExpressionStructureCounter.kt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,13 @@ class UtExpressionStructureCounter(private val input: Iterable<UtExpression>) :
153153
return stat
154154
}
155155

156+
override fun visit(expr: UtBvNotExpression): NestStat {
157+
val stat = buildState(expr.variable.expr)
158+
stat.level++
159+
stat.nodes++
160+
return stat
161+
}
162+
156163
override fun visit(expr: UtCastExpression): NestStat {
157164
val stat = buildState(expr.variable.expr)
158165
stat.level++

utbot-core/src/main/kotlin/org/utbot/common/HackUtil.kt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,4 +76,8 @@ enum class WorkaroundReason {
7676
* construct `toArray` invocation (because streams cannot be consumed twice).
7777
*/
7878
CONSUME_DIRTY_STREAMS,
79+
/**
80+
* Poor quality code in the prototype of taint analysis tool. Should be rewritten before merging to the main product.
81+
*/
82+
TAINT,
7983
}

utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt

Lines changed: 74 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ import com.jetbrains.rd.util.LogLevel
44
import mu.KotlinLogging
55
import org.utbot.common.AbstractSettings
66
import java.lang.reflect.Executable
7+
import kotlin.reflect.KMutableProperty0
8+
79
private val logger = KotlinLogging.logger {}
810

911
/**
@@ -99,6 +101,8 @@ object UtSettings : AbstractSettings(
99101
*/
100102
val copyVisualizationPathToClipboard get() = useDebugVisualization
101103

104+
var useOnlyTaintAnalysis by getBooleanProperty(false)
105+
102106
/**
103107
* Set the value to true to show library classes' graphs in visualization.
104108
*
@@ -477,6 +481,70 @@ object UtSettings : AbstractSettings(
477481
* It is used to do not encode big type storages due to significand performance degradation.
478482
*/
479483
var maxNumberOfTypesToEncode by getIntProperty(512)
484+
485+
/**
486+
* If this value is positive, the symbolic engine will treat results of all method invocations, which depth in call
487+
* stack is more than or equals than this value, as unbounded symbolic variables.
488+
*
489+
* 0 by default (do not "mock" deep methods).
490+
*/
491+
var callDepthToMock by getIntProperty(0)
492+
493+
/**
494+
* Value for [callDepthToMock] in case [useTaintAnalysisMode] is true.
495+
*/
496+
var taintAnalysisCallDepthToMock by getIntProperty(8)
497+
498+
/**
499+
* If this value is positive, a path selector for the symbolic engine will strictly drop loop states
500+
* if current step is more than this limit.
501+
*
502+
* 0 by default (do not strictly drop such states).
503+
*/
504+
var loopStepsLimit by getIntProperty(0)
505+
506+
/**
507+
* Value for [loopStepsLimit] in case [useTaintAnalysisMode] is true.
508+
*/
509+
var taintLoopStepsLimit by getIntProperty(3)
510+
511+
/**
512+
* Being set to true, this option sets some settings to specific for taint analysis values.
513+
*
514+
* False by default.
515+
*/
516+
var useTaintAnalysisMode by getBooleanProperty(false)
517+
518+
init {
519+
turnOnAnalysisModes()
520+
}
521+
522+
private fun turnOnAnalysisModes() {
523+
AnalysisMode.values().forEach {
524+
it.applyMode()
525+
}
526+
}
527+
}
528+
529+
enum class AnalysisMode(private val triggerOption: KMutableProperty0<Boolean>) {
530+
TAINT(UtSettings::useTaintAnalysisMode) {
531+
override fun settingsAction(): UtSettings.() -> Unit =
532+
{
533+
useConcreteExecution = false
534+
useSandbox = false
535+
callDepthToMock = taintAnalysisCallDepthToMock
536+
loopStepsLimit = taintLoopStepsLimit
537+
pathSelectorType = PathSelectorType.INHERITORS_SELECTOR
538+
}
539+
};
540+
541+
abstract fun settingsAction(): UtSettings.() -> Unit
542+
543+
fun applyMode() {
544+
if (triggerOption.get()) {
545+
settingsAction().invoke(UtSettings)
546+
}
547+
}
480548
}
481549

482550
/**
@@ -526,7 +594,12 @@ enum class PathSelectorType {
526594
/**
527595
* [RandomPathSelector]
528596
*/
529-
RANDOM_PATH_SELECTOR
597+
RANDOM_PATH_SELECTOR,
598+
599+
/**
600+
* [RandomSelectorWithLoopIterationsThreshold]
601+
*/
602+
RANDOM_SELECTOR_WITH_LOOP_ITERATIONS_THRESHOLD
530603
}
531604

532605
enum class TestSelectionStrategyType {

utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/Api.kt

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,9 @@ class UtFailedExecution(
209209
summary: List<DocStatement>? = null,
210210
testMethodName: String? = null,
211211
displayName: String? = null
212-
) : UtExecution(stateBefore, MissingState, result, coverage, summary, testMethodName, displayName)
212+
) : UtExecution(stateBefore, MissingState, result, coverage, summary, testMethodName, displayName) {
213+
override fun toString(): String = "StateBefore: $stateBefore, result: $result"
214+
}
213215

214216
open class EnvironmentModels(
215217
val thisInstance: UtModel?,

utbot-framework-api/src/main/kotlin/org/utbot/framework/plugin/api/util/IdUtil.kt

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -274,6 +274,11 @@ val floatArrayClassId = ClassId("[F", floatClassId)
274274
val doubleArrayClassId = ClassId("[D", doubleClassId)
275275

276276
val stringClassId = java.lang.String::class.id
277+
val stringBuilderClassId = java.lang.StringBuilder::class.id
278+
val stringBufferClassId = java.lang.StringBuffer::class.id
279+
val charSequenceClassId: ClassId = java.lang.CharSequence::class.id
280+
281+
val localeClassId: ClassId = java.util.Locale::class.id
277282

278283
val objectClassId = java.lang.Object::class.id
279284

@@ -300,6 +305,15 @@ val streamToArrayMethodId = methodId(streamClassId, "toArray", objectArrayClassI
300305

301306
val dateClassId = java.util.Date::class.id
302307

308+
val systemCLassId: ClassId = java.lang.System::class.id
309+
val propertiesClassId: ClassId = java.util.Properties::class.id
310+
@Suppress("unused")
311+
val inputStreamClassId: ClassId = java.io.InputStream::class.id
312+
@Suppress("unused")
313+
val readerClassId: ClassId = java.io.Reader::class.id
314+
@Suppress("unused")
315+
val arraysCLassId: ClassId = java.util.Arrays::class.id
316+
303317
@Suppress("RemoveRedundantQualifierName")
304318
val primitiveToId: Map<Class<*>, ClassId> = mapOf(
305319
java.lang.Void.TYPE to voidClassId,

utbot-framework-test/build.gradle

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,8 @@ test {
8282
useJUnitPlatform() {
8383
excludeTags 'slow', 'IntegrationTest'
8484
}
85+
jvmArgs '--add-opens', 'java.base/java.lang.reflect=ALL-UNNAMED'
8586
if (System.getProperty('DEBUG', 'false') == 'true') {
86-
jvmArgs '-Xdebug', '-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=9009'
87+
jvmArgs += listOf('-Xdebug', '-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=9009')
8788
}
8889
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
package org.utbot.engine.overrides;
2+
3+
import org.utbot.api.annotation.*;
4+
5+
@UtClassMock(target = java.lang.AutoCloseable.class, internalUsage = true)
6+
public interface AutoCloseable {
7+
default void close() throws Exception {
8+
// Do nothing
9+
}
10+
}

utbot-framework/src/main/java/org/utbot/engine/overrides/System.java

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
package org.utbot.engine.overrides;
22

33
import org.utbot.api.annotation.UtClassMock;
4+
import org.utbot.api.mock.*;
5+
6+
import java.util.*;
47

58
@UtClassMock(target = java.lang.System.class, internalUsage = true)
69
public class System {
@@ -225,4 +228,17 @@ public static void arraycopy(Object src, int srcPos, Object dest, int destPos, i
225228
UtArrayMock.arraycopy(srcArray, srcPos, destArray, destPos, length);
226229
}
227230
}
231+
232+
// TODO probably, we should use nullable version since chinese colleagues expect null values sometimes
233+
@SuppressWarnings("unused")
234+
public String getenv(String name) {
235+
// Prevent null for taint analysis
236+
return UtMock.makeSymbolic();
237+
}
238+
239+
@SuppressWarnings("unused")
240+
public Map<String, String> getenv() {
241+
// Prevent null for taint analysis
242+
return UtMock.makeSymbolic();
243+
}
228244
}
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
package org.utbot.engine.overrides;
2+
3+
import org.utbot.api.annotation.*;
4+
import org.utbot.api.mock.*;
5+
6+
@UtClassMock(target = java.lang.Throwable.class, internalUsage = true)
7+
public class Throwable {
8+
public void printStackTrace() {
9+
// Do nothing
10+
}
11+
12+
public synchronized java.lang.Throwable fillInStackTrace() {
13+
return UtMock.makeSymbolic();
14+
}
15+
16+
public StackTraceElement[] getStackTrace() {
17+
return UtMock.makeSymbolic();
18+
}
19+
20+
public void setStackTrace(StackTraceElement[] stackTrace) {
21+
// Do nothing
22+
}
23+
24+
public final synchronized void addSuppressed(java.lang.Throwable exception) {
25+
// Do nothing
26+
}
27+
28+
public final synchronized java.lang.Throwable[] getSuppressed() {
29+
return UtMock.makeSymbolic();
30+
}
31+
}

utbot-framework/src/main/java/org/utbot/engine/overrides/strings/UtStringBuilder.java

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
import java.util.Arrays;
66

77
import static org.utbot.api.mock.UtMock.assume;
8-
import static org.utbot.engine.ResolverKt.MAX_STRING_SIZE;
8+
import static org.utbot.engine.ResolverKt.HARD_MAX_ARRAY_SIZE;
99
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
1010
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
1111
import static org.utbot.engine.overrides.UtOverrideMock.visit;
@@ -18,13 +18,13 @@ public class UtStringBuilder implements Appendable, Serializable, CharSequence {
1818

1919
public UtStringBuilder(int capacity) {
2020
visit(this);
21-
value = new char[MAX_STRING_SIZE];
21+
value = new char[HARD_MAX_ARRAY_SIZE];
2222
count = 0;
2323
}
2424

2525
public UtStringBuilder() {
2626
visit(this);
27-
value = new char[MAX_STRING_SIZE];
27+
value = new char[HARD_MAX_ARRAY_SIZE];
2828
count = 0;
2929
}
3030

@@ -34,7 +34,7 @@ void preconditionCheck() {
3434
}
3535
assume(value != null);
3636
parameter(value);
37-
assume(value.length <= MAX_STRING_SIZE);
37+
assume(value.length <= HARD_MAX_ARRAY_SIZE);
3838
assume(count <= value.length && count >= 0);
3939

4040
visit(this);
@@ -557,14 +557,14 @@ final char[] getValue() {
557557

558558
public UtStringBuilder(String str) {
559559
visit(this);
560-
value = new char[MAX_STRING_SIZE];
560+
value = new char[HARD_MAX_ARRAY_SIZE];
561561
count = 0;
562562
append(str);
563563
}
564564

565565
public UtStringBuilder(CharSequence seq) {
566566
visit(this);
567-
value = new char[MAX_STRING_SIZE];
567+
value = new char[HARD_MAX_ARRAY_SIZE];
568568
count = 0;
569569
append(seq);
570570
}

utbot-framework/src/main/kotlin/org/utbot/engine/CollectionWrappers.kt

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
package org.utbot.engine
22

3+
import org.utbot.common.WorkaroundReason
34
import org.utbot.common.unreachableBranch
5+
import org.utbot.common.workaround
46
import org.utbot.engine.overrides.collections.AssociativeArray
57
import org.utbot.engine.overrides.collections.UtArrayList
68
import org.utbot.engine.overrides.collections.UtGenericAssociative
@@ -14,6 +16,7 @@ import org.utbot.engine.pc.UtExpression
1416
import org.utbot.engine.pc.select
1517
import org.utbot.engine.symbolic.asHardConstraint
1618
import org.utbot.engine.z3.intValue
19+
import org.utbot.framework.UtSettings
1720
import org.utbot.framework.plugin.api.ClassId
1821
import org.utbot.framework.plugin.api.FieldId
1922
import org.utbot.framework.plugin.api.MethodId
@@ -92,9 +95,21 @@ abstract class BaseOverriddenWrapper(protected val overriddenClassName: String)
9295
?.let { typeRegistry.findSubstitutionOrNull(it) ?: it }
9396

9497
return if (overriddenMethod == null) {
95-
// No overridden method has been found, switch to concrete execution
96-
pathLogger.warn("Method ${overriddenClass.name}::${method.subSignature} not found, executing concretely")
97-
emptyList()
98+
99+
// Usually, we'd process such situations concretely, but for taint analysis
100+
// we can just `mock` them with an unbounded symbolic variable
101+
val messagePrefix = "Method ${overriddenClass.name}::${method.subSignature} not found,"
102+
103+
if (UtSettings.useTaintAnalysisMode) {
104+
pathLogger.warn("$messagePrefix mocking with an unbounded variable")
105+
workaround(WorkaroundReason.TAINT) {
106+
treatMethodResultAsUnboundedVariable(name = "nativeConst", method)
107+
}
108+
} else {
109+
// No overridden method has been found, switch to concrete execution
110+
pathLogger.warn("$messagePrefix executing concretely")
111+
emptyList()
112+
}
98113
} else {
99114
val jimpleBody = overriddenMethod.jimpleBody()
100115
val graphResult = GraphResult(jimpleBody.graph())

utbot-framework/src/main/kotlin/org/utbot/engine/JimpleCreation.kt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,12 @@ fun createSootMethod(
7676
isStatic: Boolean = true
7777
) = SootMethod(name, argsTypes, returnType, if (isStatic) Modifier.STATIC else 0)
7878
.also {
79+
// Note that the order is critical important due to
80+
// difference between different versions of Soot.
81+
// In the latest versions there is no need to set up
82+
// declaring class and graphBody.method by hand.
83+
it.declaringClass = declaringClass
7984
declaringClass.addMethod(it)
85+
graphBody.method = it
8086
it.activeBody = graphBody
8187
}

0 commit comments

Comments
 (0)