Giter Site home page Giter Site logo

usvm's People

Contributors

caelmbleidd avatar damtev avatar daniilstepanov avatar dvvrd avatar ilyamuravjov avatar korifey avatar mxprshn avatar saloed avatar sergeypospelov avatar tochilinak avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar

usvm's Issues

Multiple timeouts during guava `Shorts` analysis

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "com.google.common.primitives.Shorts.*"
projectFilter = listOf("guava-26.0")

There are many timeouts during this class analysis:

14:26:09.062 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts#hashCode(short)
14:26:10.073 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortConverter#<init>()
14:26:11.097 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortConverter#doForward(java.lang.String)
14:26:12.109 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortConverter#doBackward(java.lang.Short)
14:26:13.122 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortConverter#readResolve()
14:26:14.133 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortConverter#toString()
14:26:15.162 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$LexicographicalComparator#compare(short[], short[])
14:26:16.188 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$LexicographicalComparator#toString()
14:26:17.215 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#<init>(short[], int, int)
14:26:18.227 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#<init>(short[])
14:26:19.257 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#toShortArray()
14:26:20.301 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#set(int, java.lang.Short)
14:26:21.405 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#subList(int, int)
14:26:22.427 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#contains(java.lang.Object)
14:26:23.440 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#lastIndexOf(java.lang.Object)
14:26:24.451 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#isEmpty()
14:26:25.462 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#indexOf(java.lang.Object)
14:26:26.471 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#hashCode()
14:26:27.495 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#toString()
14:26:28.508 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#equals(java.lang.Object)
14:26:29.535 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts$ShortArrayAsList#get(int)
14:26:30.545 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts#<init>()
14:26:31.570 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts#lexicographicalComparator()
14:26:32.581 | WARN  | Timeout on (id:24)com.google.common.primitives.Shorts#stringConverter()

As a result, coverage on this class is about 20%.
UnitTestBot result on the previous competitions class was 94%.

Instrumentation transposes 2D arrays

For a method that returns 10x3 array instrumentation claims that 3x10 array is returned.

To reproduce run utbot-junit-contest:run on Java 8 with following ContestEstimator settings

timeLimit = 60
methodFilter = "org.usvm.samples.arrays.ArrayOfArrays.sizesWithoutTouchingTheElements"
projectFilter = listOf("samples")

Here's ArrayOfArrays.sizesWithoutTouchingTheElements method:

public int[][] sizesWithoutTouchingTheElements() {
    int[][] array = new int[10][3];
    for(int i = 0; i < 2; ++i) {
        int var3 = array[i][0];
    }
    return array;
}

Following failing test is generated:

@Test
public void testSizesWithoutTouchingTheElements() {
    ArrayOfArrays arrayOfArrays = new ArrayOfArrays();
    
    int[][] actual = arrayOfArrays.sizesWithoutTouchingTheElements();
    
    int[][] expected = new int[3][];
    int[] intArray = {
        0, 0, 0, 0, 0, 0, 0, 0,
        0, 0
    };
    expected[0] = intArray;
    int[] intArray1 = {
        0, 0, 0, 0, 0, 0, 0, 0,
        0, 0
    };
    expected[1] = intArray1;
    int[] intArray2 = {
        0, 0, 0, 0, 0, 0, 0, 0,
        0, 0
    };
    expected[2] = intArray2;
    
    int expectedSize = expected.length;
    assertEquals(expectedSize, actual.length);
    assertArrayEquals(expected, actual);
}

Following UTestExecutionResult is returned from USVM instrumentation:
image

Strange runtime type is present in descriptors, this cause failure

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "spoon.reflect.visitor.filter.CompositeFilter.*"
projectFilter = listOf("spoon-core-7.0.0")

The following error is present in logs:

ERROR | JcToUtExecutionConverter.convert((id:44)spoon.reflect.visitor.filter.CompositeFilter#hasMatch(spoon.reflect.visitor.Filter, spoon.reflect.declaration.CtElement)) failed
org.usvm.instrumentation.testcase.executor.TestExecutorException: Can't find class runtime.LibSLRuntime$HashMapContainer in classpath
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:115) ~[usvm-jvm-instrumentation-2511-1.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:108) ~[usvm-jvm-instrumentation-2511-1.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass$default(Jacodb.kt:107) ~[usvm-jvm-instrumentation-2511-1.jar:?]
	at org.utbot.contest.usvm.converter.ConverterUtilsKt.getClassId(ConverterUtils.kt:93) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processExpr(UTestInstToUtModelConverter.kt:142) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processInst(UTestInstToUtModelConverter.kt:107) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processUTest(UTestInstToUtModelConverter.kt:66) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.<init>(JcToUtExecutionConverter.kt:65) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:184) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:168) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:275) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:269) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:26) [usvm-core-2511-1.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-2511-1.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-2511-1.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:195) [usvm-jvm-2511-1.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:267) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]

Note that similar problem with runtime classes occurs very often during spoon testing.

One of generated test classes crashes gradle verification task

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "io.seata.core.protocol.transaction.BranchRegisterRequest.*"
projectFilter = listOf("seata-core-0.5.0")

Run gradle task utbot-junit-contest:test to run tests and obtain coverage report.

The following error is the result:

FAILURE: Build failed with an exception.
* What went wrong:
Execution failed for task ':utbot-junit-contest:test'.
> Process 'Gradle Test Executor 8' finished with non-zero exit value 1
  This problem might be caused by incorrect test process configuration.

This is a strange situation that may cause unexpected problems on the real contest.

Invalid `UTestCyclicReferenceDescriptor`

Add com.google.common.collect.TreeMultiset$AvlNode to UTBotJava/utbot-junit-contest/src/main/resources/classes/guava/list.

Run ContestEstimator with following settings:

timeLimit = 120
methodFilter = "com.google.common.collect.TreeMultiset\$AvlNode.deleteMe"
projectFilter = listOf("guava")

There's following error in logs:

23:55:01.029 | ERROR | JcToUtExecutionConverter.convert((id:19)com.google.common.collect.TreeMultiset$AvlNode#deleteMe()) failed
java.lang.IllegalStateException: Invalid UTestCyclicReferenceDescriptor: UTestCyclicReferenceDescriptor(refId=903229461, type=org.jacodb.impl.types.JcClassTypeImpl@105962b3)
	at org.utbot.contest.usvm.converter.JcToUtModelConverter.convertIgnoringOriginExprForThisModel(JcToUtModelConverter.kt:152) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtModelConverter.convert(JcToUtModelConverter.kt:72) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtModelConverter.convertIgnoringOriginExprForThisModel(JcToUtModelConverter.kt:106) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtModelConverter.convert(JcToUtModelConverter.kt:72) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtModelConverter.convertIgnoringOriginExprForThisModel(JcToUtModelConverter.kt:106) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtModelConverter.convert(JcToUtModelConverter.kt:72) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.convertState(JcToUtExecutionConverter.kt:224) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.convert(JcToUtExecutionConverter.kt:73) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:190) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:168) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:275) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:269) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:33) [usvm-core-local24-22-29.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-local24-22-29.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-local24-22-29.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:195) [usvm-jvm-local24-22-29.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:267) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:75) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:129) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:125) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

The issue is that in the instrumentation output there is UTestCyclicReferenceDescriptor with refId=903229461 in such place that no UTestObjectDescriptor containing it has refId=903229461.

image

Note, that is generally impossible in current abstractions to simultaneously always:

  1. Have no cycles of UTestValueDescriptor
  2. Only have UTestCyclicReferenceDescriptor in such places where there's UTestObjectDescriptor containing it and having same refId (here "containing" allows for indirect containing with intermediate layers, i.e. transitive closure of direct containment relationship)
  3. Never use multiple UTestObjectDescriptors to describe same object in same state (initialState or finalState)

Consider the following example, where we want to build descriptor for result:

val x = X()
val y = Y()
y.x = x
x.y = y
val result = Result(x=x, y=y)

Here descriptors for result.y.x.y should be UTestCyclicReferenceDescriptor (to satisfy assumption 1) and descriptor for result.x.y should be UTestObjectDescriptor (to satisfy assumption 2), but they should be the same descriptor, i.e. descriptor in y field of descriptor for x, where x can only be described by only one instance of UTestObjectDescriptor (to satisfy assumption 3).

Further discussion is advised.

Support coverage of disjunctions in if statements

For now, coverage is calculated in a way that a conditional statement containing a disjunction in its condition is covered with only one execution that satisfies at least one part of the disjunction.
But some tests for usvm-jvm (for example, org.usvm.samples.invokes.InvokeExampleTest#testSimpleFormula) expect executions that satisfy all parts of such disjunctions, so it requires some tuning of calculating coverage.

Incorrect initial state argument for an inner class

Generate tests in the following configuration:

timeLimit=120
methodFilter = "com.google.common.collect.FilteredEntryMultimap.*"
projectFilter = listOf("guava")

ValuePredicate is an inner class of FilteredEntryMultimap.

The initial state arguments for the FilteredEntryMultimap$ValuePredicate#<init> method contains null instead of an instance of the FilteredEntryMultimap class.

image

An failing test:

@Test
public void testMethod1() {
    FilteredEntryMultimap.ValuePredicate actual = null.new ValuePredicate(null);
}

To reproduce this case, comment out this require block in the CgMethodConstructor class:

image

JcMachine failed with Trying cast not primitive type <> to primitive type <>

Run tests generation with the following settings:

timeLimit = 120
methodFilter = "com.google.common.util.concurrent.SimpleTimeLimiter.*"
projectFilter = listOf("guava-26.0")

The following JcMachine failure is found in logs multiple times:

JcMachine failed
java.lang.IllegalStateException: Trying cast not primitive type org.jacodb.impl.types.JcClassTypeImpl@18aecfe8 to primitive type org.jacodb.api.PredefinedPrimitive@32c67c
	at org.usvm.machine.interpreter.JcExprResolver$resolvePrimitiveCast$1.invoke(JcExprResolver.kt:893) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver$resolvePrimitiveCast$1.invoke(JcExprResolver.kt:891) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.resolveAfterResolved(JcExprResolver.kt:940) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.resolvePrimitiveCast(JcExprResolver.kt:891) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr(JcExprResolver.kt:152) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcSpecialCallExpr(JcExprResolver.kt:1283) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcSpecialCallExpr(JcExprResolver.kt:127) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.jacodb.api.cfg.JcSpecialCallExpr.accept(JcInst.kt:773) ~[jacodb-api-1.4.0.jar:1.4.0]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr(JcExprResolver.kt:154) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr$default(JcExprResolver.kt:149) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitCallStmt(JcInterpreter.kt:472) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:166) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:82) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.UMachine.run(Machine.kt:40) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:148) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$8$states$2$1.invoke(ContestUsvm.kt:184) ~[main/:?]

`URegistersStackFrame` index out of bounds when analyzing `com.google.common.base.internal.Finalizer`

JcMachine.analyze throws ArrayIndexOutOfBoundsException when analyzing com.google.common.base.internal.Finalizer.startFinalizer(Ljava/lang/Class;Ljava/lang/ref/ReferenceQueue;Ljava/lang/ref/PhantomReference;)V.

Stack trace:

java.lang.ArrayIndexOutOfBoundsException: Index 1 out of bounds for length 1
	at org.usvm.memory.URegistersStackFrame.set(RegistersStack.kt:38) ~[main/:?]
	at org.usvm.memory.URegistersStack.writeRegister(RegistersStack.kt:74) ~[main/:?]
	at org.usvm.memory.URegistersStack.write(RegistersStack.kt:69) ~[main/:?]
	at org.usvm.memory.URegistersStack.write(RegistersStack.kt:49) ~[main/:?]
	at org.usvm.memory.UMemory.write(Memory.kt:137) ~[main/:?]
	at org.usvm.memory.UMemory.write(Memory.kt:128) ~[main/:?]
	at org.usvm.util.UtilsKt.write(Utils.kt:29) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter$visitAssignInst$2.invoke(JcInterpreter.kt:288) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter$visitAssignInst$2.invoke(JcInterpreter.kt:287) ~[main/:?]
	at org.usvm.StepScope.doWithState(StepScope.kt:49) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitAssignInst(JcInterpreter.kt:287) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:147) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:80) ~[main/:?]
	at org.usvm.UMachine.run(Machine.kt:39) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:144) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[main/:?]

Java Analyzer check-list

This issue contains classification of supported and unsupported features in Java Analyzer.

Features

Objects

  • Primitive types
  • Reference types
  • Arrays
  • Interfaces
  • Abstract classes

Operators

  • Add/Sub/Mul/Div/Rem
  • Shl/Shr/Ushr
  • Or/And/Xor/Eq/Neq/Ge/Gt/Le/Lt
  • Cmp/Cmpg/Cmpl
  • Neg

Control flow

  • Branching
  • Loops
  • Switch. Added in #39
  • Recursive calls

Functions

  • Member functions
  • Static functions
  • Recursive functions
  • Throwing functions
  • Abstract functions

Arrays

  • 1-D arrays initialization
  • Multidimensional arrays initialization
  • Writing, reading
  • Length

Statics

  • Static fields. Added in #30
  • Static initialization. Added in #30

Exceptions

  • NullPointerException
  • IndexOutOfBoundsException
  • NegativeArraySizeException
  • ArithmeticException
  • Explicit exceptions
  • Exception handlers
  • Exception trace recovery
  • Implicit/explicit exceptions distinguishing

Invokes

  • Special invokes
  • Static invokes
  • Virtual invokes. Added in #43
  • Dynamic invokes

Types

  • Integral type casts
  • Floating type casts
  • float/double to int/long
  • int/long to float/double
  • instance of. Added in #41
  • Casts. Added in #34

Approximations

  • Primitive wrappers
  • Collections
  • ...

Other issues

  • JacoDB incorrectly handles types for operations on integrals like char, short, etc. See this. Fixed in #34
  • No coverage for a JcTest
  • No ULValues for this and locals
  • Multidimensional arrays are resolved incorrectly in JcTestResolver
  • Can't easily extend UMemoryBase now
  • Minimize test cases based on thrown exceptions
  • Strange hack with callStack.isNotEmpty()
  • Locals count and parameters count are always evaluated, though it can be cached
  • Very big arrays causes OOME in JcTestResolver
  • If statements not always have both successors
  • Create arrays with default value and a couple of writes

Not decoded SymbolicList is present in UTest

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "com.alibaba.fastjson.parser.deserializer.ResolveFieldDeserializer.*"
projectFilter = listOf("fastjson-1.2.50")

The following error is found in logs:

ERROR JcToUtExecutionConverter.convert((id:21)com.alibaba.fastjson.parser.deserializer.ResolveFieldDeserializer#setValue(java.lang.Object, java.lang.Object)) failed
java.lang.IllegalStateException: JcType.classId failed on org.usvm.api.SymbolicList<E>
	at org.utbot.contest.usvm.converter.ConverterUtilsKt.getClassId(ConverterUtils.kt:73) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processExpr(UTestInstToUtModelConverter.kt:220) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processInst(UTestInstToUtModelConverter.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processUTest(UTestInstToUtModelConverter.kt:66) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.<init>(JcToUtExecutionConverter.kt:65) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:184) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:168) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:275) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:269) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:26) [usvm-core-2511-1.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-2511-1.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-2511-1.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:195) [usvm-jvm-2511-1.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:267) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]

NPE when using java.io.Reader/java.io.InputStreamReader

Maybe related with #75

Code:

    public void bad() throws Throwable
    {
        byte data;

        /* init data */
        data = -1;

        /* POTENTIAL FLAW: Read data from console with readLine*/
        BufferedReader readerBuffered = null;
        InputStreamReader readerInputStream = null;
        try
        {
            readerInputStream = new InputStreamReader(System.in, "UTF-8");
            readerBuffered = new BufferedReader(readerInputStream);
            String stringNumber = readerBuffered.readLine();
            if (stringNumber != null)
            {
                data = Byte.parseByte(stringNumber.trim());
            }
        }
        catch (IOException exceptIO)
        {
            IO.logger.log(Level.WARNING, "Error with stream reading", exceptIO);
        }
        catch (NumberFormatException exceptNumberFormat)
        {
            IO.logger.log(Level.WARNING, "Error with number parsing", exceptNumberFormat);
        }
        finally
        {
            /* clean up stream reading objects */
            try
            {
                if (readerBuffered != null)
                {
                    readerBuffered.close();
                }
            }
            catch (IOException exceptIO)
            {
                IO.logger.log(Level.WARNING, "Error closing BufferedReader", exceptIO);
            }
            finally
            {
                try
                {
                    if (readerInputStream != null)
                    {
                        readerInputStream.close();
                    }
                }
                catch (IOException exceptIO)
                {
                    IO.logger.log(Level.WARNING, "Error closing InputStreamReader", exceptIO);
                }
            }
        }

        /* POTENTIAL FLAW: if data == Byte.MAX_VALUE, this will overflow */
        byte result = (byte)(data + 1);

        IO.writeLine("result: " + result);

Unexpected NPEs

Instruction: throw %0
Exception: JcException: Address: 0x3, type: java.lang.NullPointerException
Call stack (contains 3 frames):
	0: UCallStackFrame(method=(id:73)javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_console_readLine_add_01#bad(), returnSite=null)
	1: UCallStackFrame(method=(id:1)java.io.InputStreamReader#<init>(java.io.InputStream, java.lang.String), returnSite=%3.<init>(%4, "UTF-8"))
	2: UCallStackFrame(method=(id:1)java.io.Reader#<init>(java.lang.Object), returnSite=this.<init>(arg$0))
Instruction: %0.close()
Exception: JcException: Address: 0x4, type: java.lang.NullPointerException
Call stack (contains 2 frames):
	0: UCallStackFrame(method=(id:73)javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_console_readLine_add_01#bad(), returnSite=null)
	1: UCallStackFrame(method=(id:1)java.io.InputStreamReader#close(), returnSite=%3.close())

Machine failed in `JcApplicationGraph.getTyped`

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "com.google.common.base.internal.Finalizer.*"
projectFilter = listOf("guava-26.0")

There is the following error in logs:

ERROR | analyzeAsync failed
java.util.NoSuchElementException: Collection contains no element matching the predicate.
	at org.usvm.machine.JcApplicationGraph.getTyped(JcApplicationGraph.kt:86) ~[usvm-jvm-2511-1.jar:?]
	at org.usvm.machine.mocks.JcMockerKt.mockMethod(JcMocker.kt:17) ~[usvm-jvm-2511-1.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitMethodCall(JcInterpreter.kt:258) ~[usvm-jvm-2511-1.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:159) ~[usvm-jvm-2511-1.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:83) ~[usvm-jvm-2511-1.jar:?]
	at org.usvm.UMachine.run(Machine.kt:44) ~[usvm-core-2511-1.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:195) ~[usvm-jvm-2511-1.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:267) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) ~[main/:?]

`IllegalArgumentException` when `Throwable` method call has more than one successor statement

JcMachine.analyze() throws IllegalArgumentException when analyzing method that has a call to Throwable method with more than one successor statement, for example, com.google.common.base.Throwables.getCauseAs(Ljava/lang/Throwable;Ljava/lang/Class;)Ljava/lang/Throwable;.

public static <X extends Throwable> X getCauseAs(
    Throwable throwable, Class<X> expectedCauseType) {
  try {
    return expectedCauseType.cast(throwable.getCause());
  } catch (ClassCastException e) {
    e.initCause(throwable);
    throw e;
  }
}

Stack trace:

java.lang.IllegalArgumentException: Sequence has more than one element.
	at kotlin.sequences.SequencesKt___SequencesKt.single(_Sequences.kt:336) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.usvm.machine.JcMethodApproximationResolver$skipMethodIfThrowable$1$1.invoke(JcApproximations.kt:510) ~[main/:?]
	at org.usvm.machine.JcMethodApproximationResolver$skipMethodIfThrowable$1$1.invoke(JcApproximations.kt:509) ~[main/:?]
	at org.usvm.StepScope.doWithState(StepScope.kt:49) ~[main/:?]
	at org.usvm.machine.JcMethodApproximationResolver.skipMethodIfThrowable(JcApproximations.kt:509) ~[main/:?]
	at org.usvm.machine.JcMethodApproximationResolver.approximate(JcApproximations.kt:99) ~[main/:?]
	at org.usvm.machine.JcMethodApproximationResolver.approximate(JcApproximations.kt:92) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.approximateMethod(JcInterpreter.kt:570) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitMethodCall(JcInterpreter.kt:260) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:146) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:80) ~[main/:?]
	at org.usvm.UMachine.run(Machine.kt:39) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:144) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[main/:?]

One more strange test is generated for constructors

Consider the following generation options:

timeLimit=120
methodFilter = "org.usvm.samples.enums.ClassWithEnum.*"
projectFilter = listOf("samples")

An failing test is generated for the constructor.

@Test(expected = IllegalStateException.class)
 public void testMethodThrowsISE() {
     new ClassWithEnum.ClassWithStaticField();
 }

image

Actually, there are no reasons to fail it's invocation. However, it comes failing from uTest.

image

Multiple instrumentation NoClassDefFoundError error w

Run ContestEstimator with the following settings:

timeLimit = 120
methodFilter = "org.apache.pdfbox.pdmodel.font.PDTrueTypeFontEmbedder.*"
projectFilter = listOf("pdfbox")

There are about a hundred similar exceptions in logs. And lack of tests...

Execution failed before method under test call on (id:31)org.apache.pdfbox.pdmodel.font.PDTrueTypeFontEmbedder#setWidths(org.apache.pdfbox.cos.COSDictionary, org.apache.pdfbox.pdmodel.font.encoding.GlyphList)
java.lang.NoClassDefFoundError: Could not initialize class org.apache.pdfbox.pdmodel.font.encoding.GlyphList
	at java.lang.Class.forName0(Native Method) ~[?:1.8.0_382]
	at java.lang.Class.forName(Class.java:348) ~[?:1.8.0_382]
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:112) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:108) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:54) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestAllocateMemoryCall(UTestExpressionExecutor.kt:157) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:63) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestSetFieldStatement(UTestExpressionExecutor.kt:233) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:73) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInst-IoAF18A(UTestExpressionExecutor.kt:39) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]

Machine.analyze failed in getTypeStream method on guava

Consider the following tests genaration settings:

timeLimit = 120
methodFilter = "com.google.common.collect.MinMaxPriorityQueue.*"
projectFilter = listOf("guava")

No tests were generated. More than that, there is the following problem description in logs:

ERROR | machine.analyze(com.google.common.collect.MinMaxPriorityQueue) failed
java.lang.IllegalStateException: Unexpected ref: (let (
(e!1 %0)
(e!2 %0)
(e!3 <>@inputField<(id:21)com.google.common.collect.MinMaxPriorityQueue$Heap#this$0>()[<>@inputField<(id:21)com.google.common.collect.MinMaxPriorityQueue#minHeap>()[e!2]])
)
(ite (= e!2 e!3) 0x735 <>@inputField<(id:21)com.google.common.collect.MinMaxPriorityQueue#queue>()[e!3]))
	at org.usvm.constraints.UTypeConstraints.getTypeStream(TypeConstraints.kt:280) ~[usvm-core-comp-231121-1810.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter$checkArrayStoreException$isRvalueSubtypeOf$1.invoke(JcInterpreter.kt:342) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter$checkArrayStoreException$isRvalueSubtypeOf$1.invoke(JcInterpreter.kt:339) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.usvm.StepScope.calcOnState(StepScope.kt:61) ~[usvm-core-comp-231121-1810.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.checkArrayStoreException(JcInterpreter.kt:339) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitAssignInst(JcInterpreter.kt:306) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:159) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:82) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.usvm.UMachine.run(Machine.kt:44) ~[usvm-core-comp-231121-1810.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:185) ~[usvm-jvm-comp-231121-1810.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$states$2$1.invoke(ContestUsvm.kt:165) ~[main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:70) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:124) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:120) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

JcVirtualInvokeResolver failed during test case generation

Run ContestEstimator with the following settings:

timeLimit = 120
methodFilter = "org.apache.pdfbox.filter.JPXFilter.*"
projectFilter = listOf("pdfbox")

There is the following error in logs:

ERROR | analyzeAsync failed
java.lang.IllegalStateException: Can't find method (id:8)java.lang.reflect.Field#getName() in type sun.util.logging.PlatformLogger.Level
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt.makeConcreteMethodCall(JcVirtualInvokeResolver.kt:254) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt.access$makeConcreteMethodCall(JcVirtualInvokeResolver.kt:1) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt$prepareVirtualInvokeOnConcreteRef$state$1.invoke(JcVirtualInvokeResolver.kt:132) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt$prepareVirtualInvokeOnConcreteRef$state$1.invoke(JcVirtualInvokeResolver.kt:131) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.StepScope.forkMulti(StepScope.kt:117) ~[usvm-core-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt.resolveVirtualInvokeWithModel(JcVirtualInvokeResolver.kt:92) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt.resolveVirtualInvoke(JcVirtualInvokeResolver.kt:53) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.resolveVirtualInvoke(JcInterpreter.kt:581) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitMethodCall(JcInterpreter.kt:269) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:158) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:82) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.UMachine.run(Machine.kt:44) ~[usvm-core-comp-231122-1058.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:191) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:263) ~[main/:?]

Generating tests for one method returns less test cases than for the whole class

Consider two following scenarios of tests generation:

timeLimit = 60
methodFilter = "org.usvm.samples.wrappers.LongWrapper.*"
projectFilter = listOf("samples")

and

timeLimit = 60
methodFilter = "org.usvm.samples.wrappers.LongWrapper.parseLong"
projectFilter = listOf("samples")

First scenario allows to get several tests, and for the function parseLong too.
In the second scenario no test cases were generated by the machine.

Also note that there are no tests with timeLimit=20 at all...

Incorrect floatTodouble conversion in Java

Some properties were not discovered at positions (from 0): [3]
on
org.usvm.samples.types.CastExamplesTest.testFloatToDouble

This test may randomly fail when the generated argument values are 0.0 and -0.0.

Multiple unexpected exception in instrumentation on a class from guava-26.0

Run tests generation with the following settings:

timeLimit = 120
methodFilter = "com.google.common.util.concurrent.SimpleTimeLimiter.*"
projectFilter = listOf("guava-26.0")

There are no generated tests and many similar exceptions in logs

Resolver failed
java.lang.IllegalStateException: Unexpected exception
	at org.usvm.instrumentation.testcase.descriptor.UTestUnexpectedExecutionBuilder.build(UTestUnexpectedExecutionBuilder.kt:28) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.executor.UTestConcreteExecutor.executeAsync(UTestConcreteExecutor.kt:68) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.utbot.contest.usvm.executor.JcTestExecutor$resolve$execResult$1.invokeSuspend(JcTestExecutor.kt:72) ~[main/:?]
	at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlinx.coroutines.DispatchedTask.run(DispatchedTask.kt:106) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:284) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:85) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at org.utbot.contest.usvm.executor.JcTestExecutor.resolve(JcTestExecutor.kt:71) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1.invokeSuspend(ContestUsvm.kt:197) [main/:?]
	at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlinx.coroutines.DispatchedTask.run(DispatchedTask.kt:106) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:284) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:85) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt.runUsvmGeneration(ContestUsvm.kt:57) [main/:?]
	at org.utbot.contest.Tool$USVM.runGeneration(ContestEstimator.kt:257) [main/:?]
	at org.utbot.contest.Tool$UtBotBasedTool.run(ContestEstimator.kt:156) [main/:?]
	at org.utbot.contest.ContestEstimatorKt.runEstimator(ContestEstimator.kt:550) [main/:?]
	at org.utbot.contest.ContestEstimatorKt.main(ContestEstimator.kt:426) [main/:?]

Note that no logging of the problem here is not very good, we can't differ them

image

"`Z3_OP_INTERNAL` is not supported" for `isNaN()`

JcMachine.analyze throws NotImplementedError when analyzing com.google.common.math.PairedStatsAccumulator.leastSquaresFit()Lcom/google/common/math/LinearTransformation;, could be related to direct isNaN() check.

public final LinearTransformation leastSquaresFit() {
  checkState(count() > 1);
  if (isNaN(sumOfProductsOfDeltas)) {
    return LinearTransformation.forNaN();
  }
  double xSumOfSquaresOfDeltas = xStats.sumOfSquaresOfDeltas();
  if (xSumOfSquaresOfDeltas > 0.0) {
    if (yStats.sumOfSquaresOfDeltas() > 0.0) {
      return LinearTransformation.mapping(xStats.mean(), yStats.mean())
          .withSlope(sumOfProductsOfDeltas / xSumOfSquaresOfDeltas);
    } else {
      return LinearTransformation.horizontal(yStats.mean());
    }
  } else {
    checkState(yStats.sumOfSquaresOfDeltas() > 0.0);
    return LinearTransformation.vertical(xStats.mean());
  }
}

Stack trace:

kotlin.NotImplementedError: An operation is not implemented: Z3_OP_INTERNAL is not supported
	at io.ksmt.solver.z3.KZ3ExprConverter.convertApp-h_aMM1A(KZ3ExprConverter.kt:404) ~[ksmt-z3-0.5.7.jar:?]
	at io.ksmt.solver.z3.KZ3ExprConverter.convertNativeExpr-h_aMM1A(KZ3ExprConverter.kt:162) ~[ksmt-z3-0.5.7.jar:?]
	at io.ksmt.solver.util.KExprLongConverterBase.convertFromNative(KExprLongConverterBase.kt:27) ~[ksmt-core-0.5.7.jar:?]
	at io.ksmt.solver.z3.KZ3ExprConverter.convertExpr(KZ3ExprConverter.kt:84) ~[ksmt-z3-0.5.7.jar:?]
	at io.ksmt.solver.z3.KZ3Model.funcInterp(KZ3Model.kt:342) ~[ksmt-z3-0.5.7.jar:?]
	at io.ksmt.solver.z3.KZ3Model.interpretation(KZ3Model.kt:101) ~[ksmt-z3-0.5.7.jar:?]
	at io.ksmt.solver.z3.KZ3Model.detach(KZ3Model.kt:164) ~[ksmt-z3-0.5.7.jar:?]
	at org.usvm.solver.USolverBase.internalCheck(Solver.kt:146) ~[main/:?]
	at org.usvm.solver.USolverBase.checkWithSoftConstraints(Solver.kt:113) ~[main/:?]
	at org.usvm.StateKt.forkIfSat(State.kt:160) ~[main/:?]
	at org.usvm.StateKt.forkIfSat$default(State.kt:145) ~[main/:?]
	at org.usvm.StateKt.fork(State.kt:240) ~[main/:?]
	at org.usvm.StepScope.fork(StepScope.kt:77) ~[main/:?]
	at org.usvm.StepScope.forkWithBlackList(StepScope.kt:176) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitIfStmt(JcInterpreter.kt:306) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:148) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:80) ~[main/:?]
	at org.usvm.UMachine.run(Machine.kt:39) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:144) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[main/:?]

Class is not found, possibly because it has not been decoded

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "com.google.common.collect.ReverseOrdering.*"
projectFilter = listOf("guava-26.0")

There is an error in logs

ERROR | JcToUtExecutionConverter.convert((id:24)com.google.common.collect.ReverseOrdering#max(java.util.Iterator)) failed
org.usvm.instrumentation.testcase.executor.TestExecutorException: Can't find class stub.java.util.stream.DoubleStreamLSLIterator in classpath
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:115) ~[usvm-jvm-instrumentation-2511-1.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:108) ~[usvm-jvm-instrumentation-2511-1.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass$default(Jacodb.kt:107) ~[usvm-jvm-instrumentation-2511-1.jar:?]
	at org.utbot.contest.usvm.converter.ConverterUtilsKt.getClassId(ConverterUtils.kt:93) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processExpr(UTestInstToUtModelConverter.kt:142) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processInst(UTestInstToUtModelConverter.kt:107) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processUTest(UTestInstToUtModelConverter.kt:66) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.<init>(JcToUtExecutionConverter.kt:65) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:184) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:168) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:275) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:269) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:26) [usvm-core-2511-1.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-2511-1.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-2511-1.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:195) [usvm-jvm-2511-1.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:267) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:75) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:129) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:125) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

Also, there are similar problems

14:06:00.785 | ERROR | (x10) JcToUtExecutionConverter.convert((id:24)com.google.common.collect.ReverseOrdering#max(java.lang.Iterable)) failed
java.lang.IllegalStateException: JcType.classId failed on runtime.LibSLRuntime.Map<K, V>
	at org.utbot.contest.usvm.converter.ConverterUtilsKt.getClassId(ConverterUtils.kt:73)

and

ERROR | (x10) JcToUtExecutionConverter.convert((id:24)com.google.common.collect.ReverseOrdering#min(java.util.Iterator)) failed
org.usvm.instrumentation.testcase.executor.TestExecutorException: Can't find class stub.java.util.stream.DoubleStreamLSLIterator in classpath
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:115)

`java.lang.VerifyError`: Bad type on operand stack on `com/google/common/base/Converter.reverse()`

com/google/common/base/Converter byte code seems to get incorrectly transformed.

Instrumentation returns UTestExecutionInitFailedResult when trying to run com.google.common.primitives.Shorts$ShortConverter#toString() (guava 26.0).

16:02:54.077 | WARN  | Execution failed before method under test call
java.lang.VerifyError: Bad type on operand stack
Exception Details:
  Location:
    com/google/common/base/Converter.reverse()Lcom/google/common/base/Converter; @62: putfield
  Reason:
    Type 'com/google/common/base/Converter$ReverseConverter' (current frame, stack[1]) is not assignable to 'com/google/common/base/Converter'
  Current Frame:
    bci: @62
    flags: { }
    locals: { 'com/google/common/base/Converter', 'com/google/common/base/Converter', 'com/google/common/base/Converter$ReverseConverter' }
    stack: { 'com/google/common/base/Converter', 'com/google/common/base/Converter$ReverseConverter' }
  Bytecode:
    0000000: 1400 9db8 0037 2ab4 00a0 4c14 00a1 b800
    0000010: 372b c700 06a7 000c 1400 a3b8 0037 a700
    0000020: 3414 00a5 b800 37bb 0015 4d14 00a7 b800
    0000030: 372c 2ab7 00ab 1400 acb8 0037 2a2c b500
    0000040: a014 00ae b800 372c 4e14 00b0 b800 37a7
    0000050: 0014 1400 b2b8 0037 2b4e 1400 b4b8 0037
    0000060: a700 0314 00b6 b800 372d b0            
  Stackmap Table:
    append_frame(@24,Object[#2])
    same_frame(@33)
    same_frame(@82)
    append_frame(@99,Top,Object[#5])

	at java.lang.Class.forName0(Native Method) ~[?:?]
	at java.lang.Class.forName(Class.java:467) ~[?:?]
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:101) ~[main/:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:97) ~[main/:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:54) ~[main/:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestAllocateMemoryCall(UTestExpressionExecutor.kt:157) ~[main/:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:63) ~[main/:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestSetFieldStatement(UTestExpressionExecutor.kt:233) ~[main/:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:73) ~[main/:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInst-IoAF18A(UTestExpressionExecutor.kt:39) ~[main/:?]

Following UTest is used:
image

UTestExpressionExecutor failed before methodUnderTest call on guava Throwables

Consider the following tests generation scenario:

timeLimit = 120
methodFilter = "com.google.common.base.Throwables.*"
projectFilter = listOf("guava")

The following exception is found in logs

java.lang.IllegalAccessException: java.lang.Class
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestAllocateMemoryCall(UTestExpressionExecutor.kt:158) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:63) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestSetFieldStatement(UTestExpressionExecutor.kt:233) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:73) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInst-IoAF18A(UTestExpressionExecutor.kt:39) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInsts-CmtIpJM(UTestExpressionExecutor.kt:49) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.rd.UTestExecutor.executeUTest(UTestExecutor.kt:76) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess.callUTest(InstrumentedProcess.kt:204) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess.access$callUTest(InstrumentedProcess.kt:33) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess$setup$1.invoke(InstrumentedProcess.kt:136) ~[usvm-jvm-instrumentation-comp-231118-1620.jar:?]

NullPointerException is expected as a result of the correct test

Generate tests in the following configuration:

timeLimit=60
methodFilter = "org.usvm.samples.primitives.IntExamples.*"
projectFilter = listOf("samples")

There are two tests for the function isInteger. They have the same input. One of them is incorrect.

///region Test suites for executable org.usvm.samples.primitives.IntExamples.isInteger
    
    
    /**
     * @utbot.classUnderTest {@link org.usvm.samples.primitives.IntExamples}
     * @utbot.methodUnderTest {@link org.usvm.samples.primitives.IntExamples#isInteger(java.lang.String)}
     */
    @Test
    public void testIsIntegerReturnsFalse() {
        boolean actual = IntExamples.isInteger(null);
        
        assertFalse(actual);
    }
    
    /**
     * @utbot.classUnderTest {@link org.usvm.samples.primitives.IntExamples}
     * @utbot.methodUnderTest {@link org.usvm.samples.primitives.IntExamples#isInteger(java.lang.String)}
     */
    @Test(expected = NullPointerException.class)
    public void testIsIntegerThrowsNPE() {
        IntExamples.isInteger(null);
    }
    
    ///endregion

It seems that erronous NPE comes from the JcState

image

USVM freezes with java.security.SecureRandom (new SecureRandom())

Code

package javajuliet.testcase.CWE190_Integer_Overflow;
import javajuliet.testcasesupport.*;

import javax.servlet.http.*;

import java.security.SecureRandom;

public class CWE190_Integer_Overflow__int_random_square_01 extends AbstractTestCase
{
    public void bad() throws Throwable
    {
        int data;

        /* POTENTIAL FLAW: Set data to a random value */
        data = (new SecureRandom()).nextInt();

        /* POTENTIAL FLAW: if (data*data) > Integer.MAX_VALUE, this will overflow */
        int result = (int)(data * data);

        IO.writeLine("result: " + result);

    }
}

Call stack

Instruction: return
Call stack (contains 13 frames):
	0: UCallStackFrame(method=(id:73)javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__int_random_square_01#bad(), returnSite=null)
	1: UCallStackFrame(method=(id:1)java.security.SecureRandom#<init>(), returnSite=%0.<init>())
	2: UCallStackFrame(method=(id:1)java.security.SecureRandom#getDefaultPRNG(boolean, byte[]), returnSite=this.getDefaultPRNG(0, null))
	3: UCallStackFrame(method=(id:1)sun.security.jca.Providers#getProviderList(), returnSite=%2 = sun.security.jca.Providers.getProviderList())
	4: UCallStackFrame(method=(id:1)sun.security.jca.Providers#getThreadProviderList(), returnSite=%1 = sun.security.jca.Providers.getThreadProviderList())
	5: UCallStackFrame(method=(id:1)sun.security.jca.Providers#<clinit>(), returnSite=%0 = sun.security.jca.Providers.threadListsUsed)
	6: UCallStackFrame(method=(id:1)sun.security.jca.ProviderList#<clinit>(), returnSite=%1 = sun.security.jca.ProviderList.EMPTY)
	7: UCallStackFrame(method=(id:1)sun.security.util.Debug#getInstance(java.lang.String, java.lang.String), returnSite=%0 = sun.security.util.Debug.getInstance("jca", "ProviderList"))
	8: UCallStackFrame(method=(id:1)sun.security.util.Debug#isOn(java.lang.String), returnSite=%0 = sun.security.util.Debug.isOn(arg$0))
	9: UCallStackFrame(method=(id:1)sun.security.util.Debug#<clinit>(), returnSite=%0 = sun.security.util.Debug.args)
	10: UCallStackFrame(method=(id:1)sun.security.action.GetPropertyAction#privilegedGetProperty(java.lang.String), returnSite=%0 = sun.security.action.GetPropertyAction.privilegedGetProperty("java.security.debug"))

JcMachine failed with IllegalStateException: Invalid model containing wrong type

Run tests generation with the following settings:

timeLimit = 120
methodFilter = "com.google.common.collect.TreeMultiset.*"
projectFilter = listOf("guava")

There is the following exception in logs:

JcMachine failed
java.lang.IllegalStateException: Invalid model containing wrong type stream org.usvm.types.USupportTypeStream@3c8a9803
	at org.usvm.model.UTypeModel.evalIsSubtype(UTypeModel.kt:34) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.UComposer.transform(Composition.kt:48) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.UIsSubtypeExpr.accept(Expressions.kt:268) ~[usvm-core-comp-231118-1620.jar:?]
	at io.ksmt.expr.transformer.KNonRecursiveTransformerBase.apply(KNonRecursiveTransformerBase.kt:50) ~[ksmt-core-0.5.13.jar:?]
	at org.usvm.UComposer.compose(Composition.kt:27) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.model.UModelBase.eval(Model.kt:52) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.StateForkerKt.splitModelsByCondition(StateForker.kt:266) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.StateForkerKt.access$splitModelsByCondition(StateForker.kt:1) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.WithSolverStateForker.forkMulti(StateForker.kt:99) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.StepScope.assert(StepScope.kt:141) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.StepScope.assert$default(StepScope.kt:135) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.assertIsSubtype(JcExprResolver.kt:508) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcVirtualCallExpr(JcExprResolver.kt:1316) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcVirtualCallExpr(JcExprResolver.kt:127) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.jacodb.api.cfg.JcVirtualCallExpr.accept(JcInst.kt:732) ~[jacodb-api-1.4.0.jar:1.4.0]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr(JcExprResolver.kt:154) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitAssignInst(JcInterpreter.kt:304) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:159) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:82) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.UMachine.run(Machine.kt:40) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:148) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$8$states$2$1.invoke(ContestUsvm.kt:184) ~[main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:70) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:124) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:120) ~[utbot-core-2023.11-SNAPSHOT.jar:?]

JcTestExecutor failed in `resolveEnumValue` method

Run ContestEstimator with the following options:

timeLimit = 120
methodFilter = "com.google.common.collect.TreeMultiset.*"
projectFilter = listOf("guava")

The following error is found in logs

ERROR | executor.execute((id:21)com.google.common.collect.TreeMultiset#aggregateBelowRange(com.google.common.collect.TreeMultiset$Aggregate, com.google.common.collect.TreeMultiset$AvlNode)) failed
java.lang.IndexOutOfBoundsException: Index: 2, Size: 1
	at java.util.ArrayList.rangeCheck(ArrayList.java:659) ~[?:1.8.0_382]
	at java.util.ArrayList.get(ArrayList.java:435) ~[?:1.8.0_382]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveEnumValue(JcTestExecutor.kt:287) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveObject(JcTestExecutor.kt:252) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:194) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveObject(JcTestExecutor.kt:272) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:194) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.createUTest(JcTestExecutor.kt:90) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor.execute(JcTestExecutor.kt:55) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:173) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:166) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:273) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:267) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:26) [usvm-core-comp-231123-1615.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-comp-231123-1615.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-comp-231123-1615.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:191) [usvm-jvm-comp-231123-1615.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:263) [main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:75) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:129) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:125) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

Multiple "Can't find class in classpath" errors

Run the Contest Estimator with the following settings:

val timeLimit = 120
methodFilter = "com.google.common.collect.TreeMultiset.*"
projectFilter = listOf("guava")

Multiple instances of the same exception are thrown.

Stacktrace:

13:02:46.493 | ERROR | JcToUtExecutionConverter.convert((id:73)com.google.common.collect.TreeMultiset$AvlNode#setCount(java.util.Comparator, java.lang.Object, int, int, int[])) failed
org.usvm.instrumentation.testcase.executor.TestExecutorException: Can't find class in classpath
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:115) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:108) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass$default(Jacodb.kt:107) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.utbot.contest.usvm.converter.ConverterUtilsKt.getClassId(ConverterUtils.kt:90) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processExpr(UTestInstToUtModelConverter.kt:142) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processInst(UTestInstToUtModelConverter.kt:107) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processUTest(UTestInstToUtModelConverter.kt:66) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.<init>(JcToUtExecutionConverter.kt:64) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:182) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:166) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:273) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:267) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:26) [usvm-core-comp-231123-2300.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-comp-231123-2300.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-comp-231123-2300.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:191) [usvm-jvm-comp-231123-2300.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:263) [main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:75) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:129) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:125) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

Incorrect exception in uTest for LongWrapper.parseLong

Run joint UtBot + usvm with the following settings:

timeLimit = 60
methodFilter = "org.usvm.samples.wrappers.LongWrapper.*"
projectFilter = listOf("samples")

One of the generated test looks like as follows:

@Test(expected = NullPointerException.class)
 public void testParseLongThrowsNPE() {
    LongWrapper longWrapper = new LongWrapper();
        
    longWrapper.parseLong(null);
}

It fails because another exception is expected:

Unexpected exception, expected<java.lang.NullPointerException> but was<java.lang.NumberFormatException>

The reason is that incorrect exception is located in uTest:

image

Enum initializers do not work on Java 17

If you run USVM Java with Java 17 it fails in static initializers with the following message:

Cannot assert correctness constraint for the $VALUES of the enum class org.usvm.samples.enums.ClassWithEnum$OuterStaticUsageEnum
java.lang.IllegalStateException: Cannot assert correctness constraint for the $VALUES of the enum class org.usvm.samples.enums.ClassWithEnum$OuterStaticUsageEnum
	at org.usvm.machine.interpreter.JcExprResolver.ensureEnumStaticInitializerInvariants(JcExprResolver.kt:614)
	at org.usvm.machine.interpreter.JcExprResolver.access$ensureEnumStaticInitializerInvariants(JcExprResolver.kt:123)
	at org.usvm.machine.interpreter.JcExprResolver$ensureStaticFieldsInitialized$1.invoke(JcExprResolver.kt:689)
	at org.usvm.machine.interpreter.JcExprResolver$ensureStaticFieldsInitialized$1.invoke(JcExprResolver.kt:681)
	at org.usvm.StepScope.doWithState(StepScope.kt:47)

image

Compilation errors in generated times, possible reasoned by incorrect types resolving in machine

Run ContestEstimator with the following options:

timeLimit = 120
methodFilter = "com.google.common.collect.MinMaxPriorityQueue.*"
projectFilter = listOf("guava")

NOTE that this problems does not reproduce each time. But sometimes...

Compilation errors: C:\UtBotJava\UTBotJava\utbot-junit-contest\build\output\test_candidates\guava\com\google\common\collect\MinMaxPriorityQueueTest.java:5118: error: no suitable method found for create(ServiceDefinitionImpl)
        MinMaxPriorityQueue.create(serviceDefinitionImpl);
                           ^
    method MinMaxPriorityQueue.<E#1>create() is not applicable
      (cannot infer type-variable(s) E#1
        (actual and formal argument lists differ in length))
    method MinMaxPriorityQueue.<E#2>create(Iterable<? extends E#2>) is not applicable
      (inference variable E#2 has incompatible bounds
        upper bounds: Comparable<E#2>
        lower bounds: SDDocument)
  where E#1,E#2 are type-variables:
    E#1 extends Comparable<E#1> declared in method <E#1>create()
    E#2 extends Comparable<E#2> declared in method <E#2>create(Iterable<? extends E#2>)

After quick analysis, it seems that the problem is not in compilation itself, but in the types produced by symbolic machine.

Incorrect setting collection field to null leads to further problems with iterator

Generate tests in the following configuration:

timeLimit=60
methodFilter = "org.usvm.samples.arrays.ArrayStoreExceptionExamples.*"
projectFilter = listOf("samples")

An failing test:

@Test
    public void testFillWithTreeSet1() throws Exception  {
        ArrayStoreExceptionExamples arrayStoreExceptionExamples = new ArrayStoreExceptionExamples();
        TreeSet treeSet = ((TreeSet) createInstance("java.util.TreeSet"));
        setField(treeSet, "java.util.TreeSet", "m", null);
        
        java.lang.Object[] actual = arrayStoreExceptionExamples.fillWithTreeSet(treeSet);
        
        java.lang.Object[] expected = new java.lang.Object[1];
        TreeSet treeSet1 = ((TreeSet) createInstance("java.util.TreeSet"));
        Object present = createInstance("java.lang.Object");
        setField(treeSet1, "java.util.TreeSet", "PRESENT", present);
        setField(treeSet1, "java.util.TreeSet", "serialVersionUID", -2479143000061671589L);
        setField(treeSet1, "java.util.AbstractCollection", "MAX_ARRAY_SIZE", 2147483639);
        expected[0] = ((Object) treeSet1);
        
        int expectedSize = expected.length;
        assertEquals(expectedSize, actual.length);
        assertTrue(deepEquals(expected, actual));
    }

Let's pay attention to the line: setField(treeSet, "java.util.TreeSet", "m", null);
During the deepEquals method call, NullPointerException occurs.

image
image

Type parameters in generated tests lead to failing of `toJavaClass`

Generate tests with the following ContestEstimators settings

timeLimit=60
methodFilter = "org.usvm.samples.arrays.ArrayStoreExceptionExamples.genericAssignmentWithCast"
projectFilter = listOf("samples")

The following error can be found in logs

Can't convert execution for method genericAssignmentWithCast, exception is  E
java.lang.ClassNotFoundException: E
	at java.net.URLClassLoader.findClass(URLClassLoader.java:387) ~[?:1.8.0_382]
	at java.lang.ClassLoader.loadClass(ClassLoader.java:418) ~[?:1.8.0_382]
	at java.lang.ClassLoader.loadClass(ClassLoader.java:351) ~[?:1.8.0_382]
	at java.lang.Class.forName0(Native Method) ~[?:1.8.0_382]
	at java.lang.Class.forName(Class.java:348) ~[?:1.8.0_382]
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:107) ~[usvm-jvm-instrumentation-comp-231115-1620.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:55) ~[usvm-jvm-instrumentation-comp-231115-1620.jar:?]
	at org.utbot.contest.usvm.ConverterUtilsKt.getClassId(ConverterUtils.kt:61) ~[main/:?]
	at org.utbot.contest.usvm.UTestInst2UtModelConverter.processExpr(UTestInst2UtModelConverter.kt:216) ~[main/:?]
	at org.utbot.contest.usvm.UTestInst2UtModelConverter.processExpr(UTestInst2UtModelConverter.kt:173) ~[main/:?]
	at org.utbot.contest.usvm.UTestInst2UtModelConverter.processUTest(UTestInst2UtModelConverter.kt:65) ~[main/:?]
	at org.utbot.contest.usvm.JcToUtExecutionConverter.<init>(JcToUtExecutionConverter.kt:60) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1.invokeSuspend(ContestUsvm.kt:223) [main/:?]
	at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlinx.coroutines.DispatchedTaskKt.resume(DispatchedTask.kt:234) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.DispatchedTaskKt.dispatch(DispatchedTask.kt:166) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.dispatchResume(CancellableContinuationImpl.kt:397) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.resumeImpl(CancellableContinuationImpl.kt:431) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.resumeImpl$default(CancellableContinuationImpl.kt:420) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.resumeUndispatched(CancellableContinuationImpl.kt:518) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase$DelayedResumeTask.run(EventLoop.common.kt:500) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:284) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:85) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source) [kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt.runUsvmGeneration(ContestUsvm.kt:57) [main/:?]
	at org.utbot.contest.Tool$USVM.runGeneration(ContestEstimator.kt:257) [main/:?]
	at org.utbot.contest.Tool$UtBotBasedTool.run(ContestEstimator.kt:156) [main/:?]
	at org.utbot.contest.ContestEstimatorKt.runEstimator(ContestEstimator.kt:550) [main/:?]
	at org.utbot.contest.ContestEstimatorKt.main(ContestEstimator.kt:426) [main/:?]

The reason is that JcType used in toJavaClass contains type parameters.

"Got nullRef on the top!" for multiple methods in `spoon` project

JcMachine.analyze throws IllegalArgumentException when analyzing a few methods in spoon project, for example, when analyzing spoon.pattern.internal.node.MapEntryNode.isTryNextMatch(Lspoon/support/util/ImmutableMap;)Z.

Stack trace:

java.lang.IllegalArgumentException: Got nullRef on the top!
	at org.usvm.collection.field.UFieldsMemoryRegion.read(FieldsRegion.kt:94) ~[main/:?]
	at org.usvm.collection.field.UFieldsMemoryRegion.read(FieldsRegion.kt:39) ~[main/:?]
	at org.usvm.memory.UReadOnlyMemory$DefaultImpls.read(Memory.kt:70) ~[main/:?]
	at org.usvm.memory.UReadOnlyMemory$DefaultImpls.read(Memory.kt:73) ~[main/:?]
	at org.usvm.memory.UWritableMemory$DefaultImpls.read(Memory.kt:82) ~[main/:?]
	at org.usvm.memory.UMemory.read(Memory.kt:91) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.ensureEnumInstanceCorrectness(JcExprResolver.kt:563) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.access$ensureEnumInstanceCorrectness(JcExprResolver.kt:124) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver$ensureExprCorrectness$1$1.invoke(JcExprResolver.kt:536) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver$ensureExprCorrectness$1$1.invoke(JcExprResolver.kt:535) ~[main/:?]
	at org.usvm.StepScope.calcOnState(StepScope.kt:59) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.ensureExprCorrectness(JcExprResolver.kt:535) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr(JcExprResolver.kt:153) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitAssignInst(JcInterpreter.kt:284) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:147) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:80) ~[main/:?]
	at org.usvm.UMachine.run(Machine.kt:39) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:144) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[main/:?]

No `String.coder` field in Java 8

There's no String.coder field in Java 8, however JcContext tries to use it.

java.util.NoSuchElementException: Collection contains no element matching the predicate.
	at org.usvm.machine.JcContext$stringCoderField$2.invoke(JcContext.kt:158) ~[main/:?]
	at org.usvm.machine.JcContext$stringCoderField$2.invoke(JcContext.kt:110) ~[main/:?]
	at kotlin.SynchronizedLazyImpl.getValue(LazyJVM.kt:74) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.usvm.machine.JcContext.getStringCoderField(JcContext.kt:110) ~[main/:?]
	at org.usvm.machine.interpreter.JcSimpleValueResolver$visitJcStringConstant$1$1.invoke(JcExprResolver.kt:1035) ~[main/:?]
	at org.usvm.machine.interpreter.JcSimpleValueResolver$visitJcStringConstant$1$1.invoke(JcExprResolver.kt:1031) ~[main/:?]
	at org.usvm.StepScope.calcOnState(StepScope.kt:61) ~[main/:?]
	at org.usvm.machine.interpreter.JcSimpleValueResolver.visitJcStringConstant(JcExprResolver.kt:1031) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcStringConstant(JcExprResolver.kt:299) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcStringConstant(JcExprResolver.kt:126) ~[main/:?]
	at org.jacodb.api.cfg.JcStringConstant.accept(JcInst.kt:1161) ~[jacodb-api-1.4.0.jar:1.4.0]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr(JcExprResolver.kt:152) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcStaticCallExpr(JcExprResolver.kt:1348) ~[main/:?]
	at org.usvm.machine.interpreter.JcExprResolver.visitJcStaticCallExpr(JcExprResolver.kt:126) ~[main/:?]
	at org.jacodb.api.cfg.JcStaticCallExpr.accept(JcInst.kt:754) ~[jacodb-api-1.4.0.jar:1.4.0]
	at org.usvm.machine.interpreter.JcExprResolver.resolveJcExpr(JcExprResolver.kt:152) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitAssignInst(JcInterpreter.kt:292) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:147) ~[main/:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:78) ~[main/:?]
	at org.usvm.UMachine$run$2.invokeSuspend(Machine.kt:43) ~[main/:?]
	at org.usvm.UMachine$run$2.invoke(Machine.kt) ~[main/:?]
	at org.usvm.UMachine$run$2.invoke(Machine.kt) ~[main/:?]
	at kotlinx.coroutines.flow.SafeFlow.collectSafely(Builders.kt:61) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.flow.AbstractFlow.collect(Flow.kt:230) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at org.usvm.machine.JcMachine$analyze$1.invokeSuspend(JcMachine.kt:167) ~[main/:?]
	at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlinx.coroutines.DispatchedTask.run(DispatchedTask.kt:106) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:284) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:85) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:166) ~[main/:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:164) ~[main/:?]

ArrayStoreException in test executor

Run the Contest Estimator with the following settings:

val timeLimit = 120
methodFilter = "com.google.common.collect.TreeMultiset.*"
projectFilter = listOf("guava")

Sometimes the following exception appears:

16:29:23.465 | WARN  | Execution failed before method under test call on (id:73)com.google.common.collect.TreeMultiset#tailMultiset(java.lang.Object, com.google.common.collect.BoundType)
java.lang.ArrayStoreException: [I
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestArraySetStatement(UTestExpressionExecutor.kt:132) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:61) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInst-IoAF18A(UTestExpressionExecutor.kt:39) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInsts-CmtIpJM(UTestExpressionExecutor.kt:49) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.rd.UTestExecutor.executeUTest(UTestExecutor.kt:76) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess.callUTest(InstrumentedProcess.kt:204) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess.access$callUTest(InstrumentedProcess.kt:33) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess$setup$1.invoke(InstrumentedProcess.kt:136) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess$setup$1.invoke(InstrumentedProcess.kt:134) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]
	at org.usvm.instrumentation.rd.InstrumentedProcess$measureExecutionForTermination$1.invoke(InstrumentedProcess.kt:219) ~[usvm-jvm-instrumentation-comp-231123-2300.jar:?]

Instrumentation fails with thread death exception on `SparseImmutableTable` class

Run ContestEstimator with the following settings:

timeLimit = 120
methodFilter = "com.google.common.collect.SparseImmutableTable.*"
projectFilter = listOf("guava")

There are no generated executions because instrumentation failed with a thread death.
NOTE that actual problem is not in thread death itself. but that instrumentation works much longer that it's timeout.

ERROR | executor.execute((id:21)com.google.common.collect.SparseImmutableTable#getValue(int)) failed
com.google.common.util.concurrent.ExecutionError: java.lang.ThreadDeath
	at com.google.common.cache.LocalCache$Segment.get(LocalCache.java:2084) ~[guava-32.1.2-jre.jar:?]
	at com.google.common.cache.LocalCache.get(LocalCache.java:4012) ~[guava-32.1.2-jre.jar:?]
	at com.google.common.cache.LocalCache$LocalManualCache.get(LocalCache.java:4922) ~[guava-32.1.2-jre.jar:?]
	at org.jacodb.impl.storage.AbstractJcDatabasePersistenceImpl.findBytecode(AbstractJcDatabasePersistenceImpl.kt:86) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.fs.PersistenceClassSource$byteCode$2.invoke(ClassSource.kt:60) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.fs.PersistenceClassSource$byteCode$2.invoke(ClassSource.kt:59) ~[jacodb-core-1.4.1.jar:1.4.1]
	at kotlin.SynchronizedLazyImpl.getValue(LazyJVM.kt:74) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.jacodb.impl.fs.PersistenceClassSource.getByteCode(ClassSource.kt:59) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.fs.ByteCodeConverterKt.newClassNode(ByteCodeConverter.kt:172) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.fs.ByteCodeConverterKt.getInfo(ByteCodeConverter.kt:153) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.bytecode.JcClassOrInterfaceImpl$info$2.invoke(JcClassOrInterfaceImpl.kt:59) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.bytecode.JcClassOrInterfaceImpl$info$2.invoke(JcClassOrInterfaceImpl.kt:59) ~[jacodb-core-1.4.1.jar:1.4.1]
	at kotlin.SynchronizedLazyImpl.getValue(LazyJVM.kt:74) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.jacodb.impl.bytecode.JcClassOrInterfaceImpl.getInfo(JcClassOrInterfaceImpl.kt:59) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.bytecode.JcClassOrInterfaceImpl.getOuterClass(JcClassOrInterfaceImpl.kt:88) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.impl.JcClasspathImpl.typeOf(JcClasspathImpl.kt:78) ~[jacodb-core-1.4.1.jar:1.4.1]
	at org.jacodb.api.JcClasspath.typeOf$default(JcClasspath.kt:66) ~[jacodb-api-1.4.1.jar:1.4.1]
	at org.jacodb.api.ext.JcClasses.toType(JcClasses.kt:50) ~[jacodb-api-1.4.1.jar:1.4.1]
	at org.usvm.machine.JcTypeSystem$findSubtypes$2.invoke(JcTypeSystem.kt:106) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.JcTypeSystem$findSubtypes$2.invoke(JcTypeSystem.kt:106) ~[usvm-jvm-comp-231122-1058.jar:?]
	at kotlin.sequences.TransformingSequence$iterator$1.next(Sequences.kt:210) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlin.sequences.TransformingSequence$iterator$1.next(Sequences.kt:210) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlin.sequences.TransformingSequence$iterator$1.next(Sequences.kt:210) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlin.sequences.TransformingSequence$iterator$1.next(Sequences.kt:210) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlin.sequences.TransformingSequence$iterator$1.next(Sequences.kt:210) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.usvm.algorithms.DfsIterator.calcNext(GraphIterators.kt:57) ~[usvm-util-comp-231122-1058.jar:?]
	at org.usvm.algorithms.GraphIterator.hasNext(GraphIterators.kt:17) ~[usvm-util-comp-231122-1058.jar:?]
	at org.usvm.algorithms.CachingSequence$CachingIterator.hasNext(CachingSequence.kt:30) ~[usvm-util-comp-231122-1058.jar:?]
	at kotlin.sequences.FilteringSequence$iterator$1.calcNext(Sequences.kt:169) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlin.sequences.FilteringSequence$iterator$1.hasNext(Sequences.kt:194) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.usvm.algorithms.CachingSequence$CachingIterator.hasNext(CachingSequence.kt:30) ~[usvm-util-comp-231122-1058.jar:?]
	at kotlin.sequences.FilteringSequence$iterator$1.calcNext(Sequences.kt:169) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlin.sequences.FilteringSequence$iterator$1.hasNext(Sequences.kt:194) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at org.usvm.algorithms.CachingSequence$CachingIterator.hasNext(CachingSequence.kt:30) ~[usvm-util-comp-231122-1058.jar:?]
	at org.usvm.util.TimeLimitedIterator.hasNext(TimeLimitedIterator.kt:17) ~[usvm-util-comp-231122-1058.jar:?]
	at org.usvm.types.USupportTypeStream.take(SupportTypeStream.kt:92) ~[usvm-core-comp-231122-1058.jar:?]
	at org.usvm.types.TypeStreamKt.firstOrNull(TypeStream.kt:121) ~[usvm-core-comp-231122-1058.jar:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:185) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveArray$resolveElement(JcTestExecutor.kt:218) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveArray(JcTestExecutor.kt:225) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:193) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveArray$resolveElement(JcTestExecutor.kt:218) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveArray(JcTestExecutor.kt:225) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:193) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveObject(JcTestExecutor.kt:272) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:194) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveObject(JcTestExecutor.kt:272) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:194) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveObject(JcTestExecutor.kt:272) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:194) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveObject(JcTestExecutor.kt:272) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveReference(JcTestExecutor.kt:194) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveExpr(JcTestExecutor.kt:118) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.resolveLValue(JcTestExecutor.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor$MemoryScope.createUTest(JcTestExecutor.kt:90) ~[main/:?]
	at org.utbot.contest.usvm.jc.JcTestExecutor.execute(JcTestExecutor.kt:55) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:173) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:166) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:273) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:267) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:26) [usvm-core-comp-231122-1058.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-comp-231122-1058.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-comp-231122-1058.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:191) [usvm-jvm-comp-231122-1058.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:263) [main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:75) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:129) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:125) [utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) [kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
Caused by: java.lang.ThreadDeath
	at java.lang.Thread.stop(Thread.java:858) ~[?:1.8.0_382]
	at org.utbot.common.ThreadBasedExecutor.invokeWithTimeout-rL6R5X8(ThreadUtil.kt:100) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor.invokeWithTimeout-rL6R5X8$default(ThreadUtil.kt:64) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt.analyzeAsync(ContestUsvm.kt:263) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1.invokeSuspend(ContestUsvm.kt:166) ~[main/:?]
	at kotlin.coroutines.jvm.internal.BaseContinuationImpl.resumeWith(ContinuationImpl.kt:33) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]
	at kotlinx.coroutines.DispatchedTaskKt.resume(DispatchedTask.kt:234) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.DispatchedTaskKt.dispatch(DispatchedTask.kt:166) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.dispatchResume(CancellableContinuationImpl.kt:397) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.resumeImpl(CancellableContinuationImpl.kt:431) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.resumeImpl$default(CancellableContinuationImpl.kt:420) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.CancellableContinuationImpl.resumeUndispatched(CancellableContinuationImpl.kt:518) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase$DelayedResumeTask.run(EventLoop.common.kt:500) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.EventLoopImplBase.processNextEvent(EventLoop.common.kt:284) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BlockingCoroutine.joinBlocking(Builders.kt:85) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking(Builders.kt:59) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking(Unknown Source) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt__BuildersKt.runBlocking$default(Builders.kt:38) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at kotlinx.coroutines.BuildersKt.runBlocking$default(Unknown Source) ~[kotlinx-coroutines-core-jvm-1.6.4.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt.runUsvmGeneration(ContestUsvm.kt:66) ~[main/:?]
	at org.utbot.contest.Tool$USVM.runGeneration(ContestEstimator.kt:257) ~[main/:?]
	at org.utbot.contest.Tool$UtBotBasedTool.run(ContestEstimator.kt:156) ~[main/:?]
	at org.utbot.contest.ContestEstimatorKt.runEstimator(ContestEstimator.kt:549) ~[main/:?]
	at org.utbot.contest.ContestEstimatorKt.main(ContestEstimator.kt:425) ~[main/:?]

NPE when using java.lang.System.out/java.lang.System.err

I run USVM on the the following function (Java Juliet test suite)

    public void bad() throws Throwable
    {
        byte data;

        /* POTENTIAL FLAW: Use the maximum size of the data type */
        data = Byte.MAX_VALUE;

        /* POTENTIAL FLAW: if data == Byte.MAX_VALUE, this will overflow */
        byte result = (byte)(data + 1);

        IO.writeLine("result: " + result);

    }

IO is implemented as follows.

There is an unexpected NPE during the USVM run.

Instruction: %0.println(arg$0)
Exception: JcException: Address: 0x15, type: java.lang.NullPointerException
Call stack (contains 2 frames):
	0: UCallStackFrame(method=(id:73)javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_max_add_01#bad(), returnSite=null)
	1: UCallStackFrame(method=(id:73)javajuliet.testcasesupport.IO#writeLine(java.lang.String), returnSite=javajuliet.testcasesupport.IO.writeLine(%7))

Assignments to null:

Instruction: java.lang.System.out = null
Call stack (contains 3 frames):
	0: UCallStackFrame(method=(id:73)javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_max_add_01#bad(), returnSite=null)
	1: UCallStackFrame(method=(id:73)javajuliet.testcasesupport.IO#writeLine(java.lang.String), returnSite=javajuliet.testcasesupport.IO.writeLine(%7))
	2: UCallStackFrame(method=(id:1)java.lang.System#<clinit>(), returnSite=%0 = java.lang.System.out)
================================================================
Instruction: java.lang.System.err = null
Call stack (contains 3 frames):
	0: UCallStackFrame(method=(id:73)javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_max_add_01#bad(), returnSite=null)
	1: UCallStackFrame(method=(id:73)javajuliet.testcasesupport.IO#writeLine(java.lang.String), returnSite=javajuliet.testcasesupport.IO.writeLine(%7))
	2: UCallStackFrame(method=(id:1)java.lang.System#<clinit>(), returnSite=%0 = java.lang.System.out)

And the final result is

20:08:04.945 |I| TestRunnerKt - 1 executions were found:
	JcTest(method=org.jacodb.impl.types.JcTypedMethodImpl@7131da33, before=JcParametersState(thisInstance=javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_max_add_01@6a278584, parameters=[]), after=JcParametersState(thisInstance=javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_max_add_01@28f90752, parameters=[]), result=Failure(java.lang.NullPointerException), coverage=JcCoverage(targetClassToCoverage={}))
Extracted values:
	[javajuliet.testcase.CWE190_Integer_Overflow.CWE190_Integer_Overflow__byte_max_add_01@6a278584, null]

Multiple `UTestExecutionInitFailedResult` without cause as a result of class analysis

Run ContestEstimator with the following options:

timeLimit = 120
methodFilter = "spoon.reflect.visitor.ImportScannerImpl.*"
projectFilter = listOf("spoon")

The are multiple similar warnings in logs (absolutely unimformative about real problem reasons, because executionResult.cause is absent).
As a result, coverage for this class is about 3%

12:15:49.114 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#isInCollisionWithLocalMethod(spoon.reflect.reference.CtExecutableReference)
java.lang.Exception: 
12:15:49.132 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#isInCollisionWithLocalMethod(spoon.reflect.reference.CtExecutableReference)
java.lang.Exception: 
12:15:49.328 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#computeImports(spoon.reflect.declaration.CtElement)
java.lang.Exception: 
12:15:49.351 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#computeImports(spoon.reflect.declaration.CtElement)
java.lang.Exception: 
12:15:49.368 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#computeImports(spoon.reflect.declaration.CtElement)
java.lang.Exception: 
12:15:49.386 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#computeImports(spoon.reflect.declaration.CtElement)
java.lang.Exception: 
12:15:50.498 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#visitCtCatchVariable(spoon.reflect.code.CtCatchVariable)
java.lang.Exception: 
12:15:50.577 | WARN  | Execution failed before method under test call on (id:21)spoon.reflect.visitor.ImportScannerImpl#visitCtCatchVariable(spoon.reflect.code.CtCatchVariable)
java.lang.Exception: 

The root issue for all TODOs

This issue contains all TODOs, so as not to forget them. If you complete any todo from this list, don't forget to add a link to the report in some form.

TODOs

  • Benchmark different ways of collecting a guard in the HeapRefSplittingUtil::filter.
  • Make a single ite not only for symbolic heap refs, but for concrete heap refs too.
  • Compare eager and lazy UModel performance.
  • Structure source files into packages. Fixed in #13
  • Add simplifying UFlatUpdates in UComposer (case composing on UModel, where stores are concretized and we expect a concrete reading returns a concrete value). Added in #9
  • mkDistinct with concrete heap refs.
  • Interning URegionIds.
  • Choose constant names carefully in UExprTranslator.
  • Deal with big arrays in composition. Idea: we can create a ranged update node with copy from big array and apply it to heap.
  • Localized map in memory regions compostion.
  • Refactor UHeap to generic implementation with getMemoryRegion(regionId: URegionId).
  • Fix Type/ArrayType inconsistence.
  • Make recursive-free implementations in UFlatUpdates.
  • Implement UMemory::memset. Added in #17
  • Revision and design UComponents and DI in usvm.
  • Implement approximations for Throwable.
  • Choose a better way to place close function, related to this PR.
  • Refactor namings in RegionTree and all usages. Fixed in #26
  • Fix equals for update nodes and add related tests.
  • Think again about array casts and type elations with their elements.
  • Think about region refinement with bv constraints and their interaction with memory regions (eager vs lazy style). includesConcretely, includesSymbolically look like good extension points.
  • Fix translator cache usage in lazy models. Fixed in #28
  • Make cache in DfsIterator optional
  • Refactor the splitting read mechanism.

Instrumentation fails on `pdfbox` classes, even though jar with the missed class is on classpath

Consider the following tests generation scenario:

timeLimit = 120
methodFilter = "org.apache.pdfbox.util.XMLUtil.*"
projectFilter = listOf("pdfbox")

The following exception occured:

java.lang.Exception: java.lang.Exception: Unexpected exception in endpoint `usvm-executor-worker.InstrumentedProcessModel.callUTest`::(9997603787970205307) taskId=(1000378)
	at com.jetbrains.rd.framework.impl.RdCall.onWireReceived(RdTask.kt:371)
	at com.jetbrains.rd.framework.MessageBroker$invoke$2$2.invoke(MessageBroker.kt:57)
	at com.jetbrains.rd.framework.MessageBroker$invoke$2$2.invoke(MessageBroker.kt:56)
	at com.jetbrains.rd.framework.impl.ProtocolContexts.readMessageContextAndInvoke(ProtocolContexts.kt:148)
	at com.jetbrains.rd.framework.MessageBroker$invoke$2.invoke(MessageBroker.kt:56)
	at com.jetbrains.rd.framework.MessageBroker$invoke$2.invoke(MessageBroker.kt:54)
	at com.jetbrains.rd.util.threading.SingleThreadSchedulerBase.queue$lambda-3(SingleThreadScheduler.kt:41)
	at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
	at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
	at java.lang.Thread.run(Thread.java:750)
Caused by: org.jacodb.api.NoClassInClasspathException: Class com.github.jaiimageio.impl.plugins.tiff.TIFFFieldNode not found in classpath
	at org.jacodb.api.ExceptionsKt.throwClassNotFound(Exceptions.kt:26)
	at org.jacodb.api.ext.JcClasspaths.findClass(JcClasspaths.kt:51)
	at org.usvm.instrumentation.serializer.SerializationUtilsKt.readJcClass(SerializationUtils.kt:39)
	at org.usvm.instrumentation.serializer.UTestInstSerializer.deserializeUTestAllocateMemoryCall(UTestInstSerializer.kt:256)
	at org.usvm.instrumentation.serializer.UTestInstSerializer.deserializeUTestInstFromBuffer(UTestInstSerializer.kt:82)
	at org.usvm.instrumentation.serializer.UTestInstSerializer.deserializeUTestInst(UTestInstSerializer.kt:102)
	at org.usvm.instrumentation.serializer.UTestInstSerializer$Companion$marshaller$$inlined$create$1.invoke(FrameworkMarshallers.kt:152)
	at org.usvm.instrumentation.serializer.UTestInstSerializer$Companion$marshaller$$inlined$create$1.invoke(FrameworkMarshallers.kt:31)
	at com.jetbrains.rd.framework.UniversalMarshaller.read(FrameworkMarshallers.kt:14)
	at org.usvm.instrumentation.generated.models.SerializedUTest$Companion.read(InstrumentedProcessModel.Generated.kt:490)
	at org.usvm.instrumentation.generated.models.SerializedUTest$Companion.read(InstrumentedProcessModel.Generated.kt:485)
	at com.jetbrains.rd.framework.impl.RdCall.onWireReceived(RdTask.kt:355)
	... 9 more

However, the class com.github.jaiimageio.impl.plugins.tiff.TIFFFieldNode is present on classpath, it is shown on the screen.
This problem happens for some other classes too.

image

Tests that do nothing but expect exceptions are generated

Run ContestEstimator with the folдowing settings:

timeLimit = 120
methodFilter = "org.apache.pdfbox.pdmodel.font.FileSystemFontProvider.*"
projectFilter = listOf("pdfbox")

Several strange tests doing nothing but expecting exceptions are generated. Examples are

     /**
     * @utbot.classUnderTest {@link org.apache.pdfbox.pdmodel.font.FileSystemFontProvider.FSFontInfo}
     * @utbot.methodUnderTest {@link org.apache.pdfbox.pdmodel.font.FileSystemFontProvider.FSFontInfo#getTrueTypeFont(java.lang.String,java.io.File)}
     */
    @Test(expected = NoClassDefFoundError.class)
    public void testGetTrueTypeFontThrowsNCDFEWithNonEmptyString() throws Throwable  {
    }
    
    /**
     * @utbot.classUnderTest {@link org.apache.pdfbox.pdmodel.font.FileSystemFontProvider.FSFontInfo}
     * @utbot.methodUnderTest {@link org.apache.pdfbox.pdmodel.font.FileSystemFontProvider.FSFontInfo#getTrueTypeFont(java.lang.String,java.io.File)}
     */
    @Test(expected = NoClassDefFoundError.class)
    public void testGetTrueTypeFontThrowsNCDFE1() throws Throwable  {
    }

JcMachine failed with IllegalStateException: Unexpected type

Consider the following tests generation scenario:

timeLimit = 120
methodFilter = "com.google.common.net.MediaType.*"
projectFilter = listOf("guava")

The following exception can be found in logs

JcMachine failed
java.lang.IllegalStateException: Unexpected type: org.jacodb.impl.types.JcTypeVariableImpl@5a0c610b
	at org.usvm.util.JcMethodUtilsKt.findMethod(JcMethodUtils.kt:30) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt$makeConcreteCallsForPossibleTypes$1$block$1.invoke(JcVirtualInvokeResolver.kt:281) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt$makeConcreteCallsForPossibleTypes$1$block$1.invoke(JcVirtualInvokeResolver.kt:280) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.StepScope.forkMulti(StepScope.kt:117) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt.resolveVirtualInvokeWithModel(JcVirtualInvokeResolver.kt:110) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcVirtualInvokeResolverKt.resolveVirtualInvoke(JcVirtualInvokeResolver.kt:53) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.resolveVirtualInvoke(JcInterpreter.kt:581) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitMethodCall(JcInterpreter.kt:269) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:158) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:82) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.UMachine.run(Machine.kt:40) ~[usvm-core-comp-231118-1620.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:148) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.usvm.machine.JcMachine.analyze$default(JcMachine.kt:53) ~[usvm-jvm-comp-231118-1620.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$8$states$2$1.invoke(ContestUsvm.kt:184) ~[main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:70) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:124) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:120) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

Strange class is not present on classpath failure

Run ContestEstimator with the following settings

timeLimit = 30
methodFilter = "io.seata.core.rpc.netty.ShutdownHook.*"
projectFilter = listOf("seata-core-0.5.0")

The following error is present in logs:

ERROR 
JcToUtExecutionConverter.convert((id:27)io.seata.core.rpc.netty.ShutdownHook$DisposablePriorityWrapper#<init>(io.seata.core.rpc.netty.ShutdownHook, io.seata.core.rpc.Disposable, int)) failed
java.lang.IllegalStateException: JcType.classId failed on io.seata.core.rpc.netty.NettyServerConfig
	at org.utbot.contest.usvm.converter.ConverterUtilsKt.getClassId(ConverterUtils.kt:73) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processExpr(UTestInstToUtModelConverter.kt:220) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processInst(UTestInstToUtModelConverter.kt:112) ~[main/:?]
	at org.utbot.contest.usvm.converter.UTestInstToUtModelConverter.processUTest(UTestInstToUtModelConverter.kt:66) ~[main/:?]
	at org.utbot.contest.usvm.converter.JcToUtExecutionConverter.<init>(JcToUtExecutionConverter.kt:65) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:184) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$runUsvmGeneration$1$9$5.invoke(ContestUsvm.kt:168) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:275) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1$1$1.addState(ContestUsvm.kt:269) [main/:?]
	at org.usvm.statistics.collectors.CoveredNewStatesCollector.onStateTerminated(CoveredNewStatesCollector.kt:33) [usvm-core-2511-1.jar:?]
	at org.usvm.statistics.CompositeUMachineObserver.onStateTerminated(UMachineObserver.kt:48) [usvm-core-2511-1.jar:?]
	at org.usvm.UMachine.run(Machine.kt:66) [usvm-core-2511-1.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:195) [usvm-jvm-2511-1.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:267) [main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) [main/:?]

However, it seems that this class is present on the classpath

image

No entrypoint found for method: virtual `JcUnknownClass#getLogger(String)`

Run ContestEstimator with the following settings:

timeLimit = 120
methodFilter = "io.seata.core.protocol.MergedWarpMessage.*"
projectFilter = listOf("seata-core-0.5.0")

jcMachine.analyze() fails with the following error. Note that now, when jcMachine is responsible for distributing budget between methods, jcMachine.analyze() throwing exception causes test generation for entire class to stop.

17:47:43.195 | ERROR | analyzeAsync failed
java.lang.IllegalStateException: No entrypoint found for method: virtual org.jacodb.impl.features.classpaths.JcUnknownClass@7b16e1e3#getLogger(java.lang.String)
	at org.usvm.machine.state.JcStateUtilsKt.addNewMethodCall(JcStateUtils.kt:67) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter$visitMethodCall$2.invoke(JcInterpreter.kt:258) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter$visitMethodCall$2.invoke(JcInterpreter.kt:257) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.StepScope.doWithState(StepScope.kt:51) ~[usvm-core-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.visitMethodCall(JcInterpreter.kt:257) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:158) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.machine.interpreter.JcInterpreter.step(JcInterpreter.kt:82) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.usvm.UMachine.run(Machine.kt:44) ~[usvm-core-comp-231122-1058.jar:?]
	at org.usvm.machine.JcMachine.analyze(JcMachine.kt:191) ~[usvm-jvm-comp-231122-1058.jar:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:265) ~[main/:?]
	at org.utbot.contest.usvm.ContestUsvmKt$analyzeAsync$1.invoke(ContestUsvm.kt:263) ~[main/:?]
	at org.utbot.common.ThreadBasedExecutor$invokeWithTimeout$1.invoke(ThreadUtil.kt:75) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:129) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at org.utbot.common.ThreadBasedExecutor$ensureThreadIsAlive$1.invoke(ThreadUtil.kt:125) ~[utbot-core-2023.11-SNAPSHOT.jar:?]
	at kotlin.concurrent.ThreadsKt$thread$thread$1.run(Thread.kt:30) ~[kotlin-stdlib-1.8.22.jar:1.8.22-release-407(1.8.22)]

Duplicate class definition for name: "org/slf4j/impl/StaticLoggerBinder"

Run ContestEstimator with the following settings:

timeLimit = 60
methodFilter = "io.seata.core.protocol.MergedWarpMessage.doDecode"
projectFilter = listOf("seata-core-0.5.0")

USVM instrumentation fails before method under test call with following errors (second error is then repeated over 100 times):

16:52:08.950 | WARN  | Execution failed before method under test call on (id:23)io.seata.core.protocol.MergedWarpMessage#doDecode(java.nio.ByteBuffer)
java.lang.LinkageError: loader (instance of  org/usvm/instrumentation/classloader/WorkerClassLoader): attempted  duplicate class definition for name: "org/slf4j/impl/StaticLoggerBinder"
	at org.slf4j.LoggerFactory.bind(LoggerFactory.java:150) ~[slf4j-api-1.7.36.jar:1.7.36]
	at org.slf4j.LoggerFactory.performInitialization(LoggerFactory.java:124) ~[slf4j-api-1.7.36.jar:1.7.36]
	at org.slf4j.LoggerFactory.getILoggerFactory(LoggerFactory.java:417) ~[slf4j-api-1.7.36.jar:1.7.36]
	at org.slf4j.LoggerFactory.getLogger(LoggerFactory.java:362) ~[slf4j-api-1.7.36.jar:1.7.36]
	at org.slf4j.LoggerFactory.getLogger(LoggerFactory.java:388) ~[slf4j-api-1.7.36.jar:1.7.36]
	at io.seata.core.protocol.MergedWarpMessage.<clinit>(MergedWarpMessage.java:44) ~[?:?]
	at java.lang.Class.forName0(Native Method) ~[?:1.8.0_392]
	at java.lang.Class.forName(Class.java:348) ~[?:1.8.0_392]
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:112) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:108) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
16:52:09.157 | WARN  | Execution failed before method under test call on (id:23)io.seata.core.protocol.MergedWarpMessage#doDecode(java.nio.ByteBuffer)
java.lang.NoClassDefFoundError: Could not initialize class io.seata.core.protocol.MergedWarpMessage
	at java.lang.Class.forName0(Native Method) ~[?:1.8.0_392]
	at java.lang.Class.forName(Class.java:348) ~[?:1.8.0_392]
	at org.usvm.instrumentation.util.JacodbKt.findClassInLoader(Jacodb.kt:112) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:108) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.util.JacodbKt.toJavaClass(Jacodb.kt:54) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestAllocateMemoryCall(UTestExpressionExecutor.kt:157) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:63) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestSetFieldStatement(UTestExpressionExecutor.kt:233) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.exec(UTestExpressionExecutor.kt:73) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]
	at org.usvm.instrumentation.testcase.executor.UTestExpressionExecutor.executeUTestInst-IoAF18A(UTestExpressionExecutor.kt:39) ~[usvm-jvm-instrumentation-comp-231122-1058.jar:?]

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.