Bad coverage for simple example with loop

[tochilinak]

Description

Bad example for UTBot symbolic execution engine.

To Reproduce

Steps to reproduce the behavior:

1. Create project in IntelliJ Idea with the following code:

public class Main {
    int func(int x, int y, int z) {
        assert (y == 0);
        while (y < 10000)
            y += 1;
        if (x == y || z == y)
            return 1;
        return 2;
    }
}

2. Use plugin to generate tests (with and without fuzzing).

Expected behavior

All lines were covered by generated tests.

Actual behavior

No tests with return value 1 were generated.

Visual proofs (screenshots, logs, images)

Tests generated with 100% symbolic execution:

public final class MainTest {
    ///region Test suites for executable com.company.Main.func

    ///region SYMBOLIC EXECUTION: EXPLICITLY THROWN UNCHECKED EXCEPTIONS for method func(int, int, int)

    /**
     * @utbot.classUnderTest {@link Main}
     * @utbot.methodUnderTest {@link Main#func(int, int, int)}
     * @utbot.executesCondition {@code (assert (y == 0);): True}
     * @utbot.executesCondition {@code (assert (y == 0);): True}
     * @utbot.throwsException {@link AssertionError} in: assert (y == 0);
     */
    @Test
    @DisplayName("func: assert (y == 0) -> ThrowAssertionError")
    public void testFunc_ThrowAssertionError() {
        Main main = new Main();
        
        /* This test fails because method [com.company.Main.func] produces [java.lang.AssertionError]
            com.company.Main.func(Main.java:5) */
        main.func(-255, -255, -255);
    }
    ///endregion

    ///endregion
}

Tests generated with 5% fuzzing:

public final class MainTest {
    ///region Test suites for executable com.company.Main.func

    ///region SYMBOLIC EXECUTION: EXPLICITLY THROWN UNCHECKED EXCEPTIONS for method func(int, int, int)

    /**
     * @utbot.classUnderTest {@link Main}
     * @utbot.methodUnderTest {@link Main#func(int, int, int)}
     * @utbot.executesCondition {@code (assert (y == 0);): True}
     * @utbot.executesCondition {@code (assert (y == 0);): True}
     * @utbot.throwsException {@link AssertionError} in: assert (y == 0);
     */
    @Test
    @DisplayName("func: assert (y == 0) -> ThrowAssertionError")
    public void testFunc_ThrowAssertionError() {
        Main main = new Main();
        
        /* This test fails because method [com.company.Main.func] produces [java.lang.AssertionError]
            com.company.Main.func(Main.java:5) */
        main.func(-255, -255, -255);
    }
    ///endregion

    ///region OTHER: SUCCESSFUL EXECUTIONS for method func(int, int, int)

    @Test
    public void testFunc1() {
        Main main = new Main();

        int actual = main.func(0, 0, 0);

        assertEquals(2, actual);
    }
    ///endregion

    ///endregion
}

[Damtev]

Such behavior is well-known and kind of expected because of the limitations of symbolic executions. As you can see, a loop with 10000 steps is presented at the beginning of the attached method, so actually it means that the symbolic engine needs to perform at least 10000 steps to end the analysis of this loop and continue the symbolic analysis of the rest of the method.

But these 10000 steps do not increase current coverage at all, so we have a limit of steps for such cases to prevent long (or even infinite) analysis. For now, it is 3500 steps, you can find it here org.utbot.framework.UtSettings#getPathSelectorStepsLimit.

As long as the steps limit exceeds and the org.utbot.framework.UtSettings#getSaveRemainingStatesForConcreteExecution option is enabled, all remaining states are passed to the queue for concrete execution. So, concrete execution can cover the return 1 statement only by chance.

[tochilinak]

This issue is similar to #2254: these are examples to measure improvements in symbolic execution.

In USVM this particular example passes because of one simple heuristics (not adding new constraint if its negation is UNSAT). However, if we remove assert in the beginning, it also fails, but there are ways to improve that.

As for limit of 3500 steps: if we reduce 10000 to 500, result will be the same.

[tochilinak]

Also, this fixed limitation of 3500 steps is pretty weird because it makes testing such functions impossible:

public class Main {
    boolean func(int x, int y) {
        String s = " This is some long hard-coded text " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa " +
                " aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa ";
        System.out.println(s);
        return x == y;
    }
}