From 6dfec3f2feefaca21c09496db6258ad7befbb1fd Mon Sep 17 00:00:00 2001 From: Alexey Menshutin Date: Tue, 7 Jun 2022 15:38:51 +0300 Subject: [PATCH] AssumeOrExecuteConcretely instruction support (#64) --- docs/AssumptionsMechanism.md | 216 ++++++++++++++++++ .../main/java/org/utbot/api/mock/UtMock.java | 10 +- .../kotlin/org/utbot/framework/UtSettings.kt | 8 + .../java/org/utbot/engine/overrides/Byte.java | 3 +- .../org/utbot/engine/overrides/Integer.java | 10 +- .../java/org/utbot/engine/overrides/Long.java | 10 +- .../org/utbot/engine/overrides/Short.java | 8 +- .../overrides/collections/UtArrayList.java | 3 +- .../overrides/collections/UtHashMap.java | 4 +- .../overrides/collections/UtHashSet.java | 2 +- .../overrides/collections/UtLinkedList.java | 3 +- .../org/utbot/engine/AnnotationResolver.kt | 6 - .../kotlin/org/utbot/engine/DataClasses.kt | 7 +- .../kotlin/org/utbot/engine/ExecutionState.kt | 13 +- .../kotlin/org/utbot/engine/Extensions.kt | 39 +++- .../src/main/kotlin/org/utbot/engine/Mocks.kt | 13 +- .../org/utbot/engine/UtBotSymbolicEngine.kt | 110 ++++++--- .../main/kotlin/org/utbot/engine/pc/Query.kt | 3 +- .../kotlin/org/utbot/engine/pc/UtSolver.kt | 74 ++++-- .../engine/selectors/BasePathSelector.kt | 14 ++ .../strategies/DistanceStatistics.kt | 14 +- .../strategies/EdgeVisitCountingStatistics.kt | 12 +- .../strategies/StepsLimitStoppingStrategy.kt | 9 +- .../utbot/engine/symbolic/SymbolicState.kt | 10 +- .../engine/symbolic/SymbolicStateUpdate.kt | 28 ++- .../concrete/MockValueConstructor.kt | 4 +- .../examples/arrays/IntArrayBasicsTest.kt | 12 + .../examples/collections/LinkedListsTest.kt | 6 +- .../collections/ListAlgorithmsTest.kt | 5 +- .../utbot/examples/collections/ListsTest.kt | 13 +- .../examples/collections/MapValuesTest.kt | 6 +- .../examples/natives/NativeExamplesTest.kt | 14 +- .../examples/strings/StringExamplesTest.kt | 77 ++++--- .../utbot/examples/arrays/IntArrayBasics.java | 20 ++ .../org/utbot/examples/collections/Lists.java | 7 + 35 files changed, 660 insertions(+), 133 deletions(-) create mode 100644 docs/AssumptionsMechanism.md diff --git a/docs/AssumptionsMechanism.md b/docs/AssumptionsMechanism.md new file mode 100644 index 0000000000..487c69ddef --- /dev/null +++ b/docs/AssumptionsMechanism.md @@ -0,0 +1,216 @@ +# Assumptions mechanism +We have a public API that might help both us and external users to interact with UTBot. +This document contains detailed instructions about how to use `assume` methods of `UtMock` class and description +of the problems we encountered during the implementation. + +## Brief description +This section contains short explanations of the meaning for mentioned functions and examples of usage. + +### UtMock.assume(predicate) + +`assume` is a method that gives the opportunity for users to say to the symbolic virtual machine that +instructions of the MUT (Method Under Test) encountered after this instruction satisfy the given predicate. +It is natively understandable concept and the closest analog from Java is the `assert` function. +When the virtual machine during the analysis encounters such instruction, it drops all the branches in the +control flow graph violating the predicate. + +Examples: +```java +int foo(int x) { + // Here `x` is unbounded symbolic variable. + // It can be any value from [MIN_VALUE..MAX_VALUE] range. + + UtMock.assume(x > 0); + // Now engine will adjust the range to (0..MAX_VALUE]. + + if (x <= 0) { + throw new RuntimeException("Unreachable exception"); + } else { + return 0; + } +} + +// A function that removes all the branches with a null, empty or unsorted list. +public List sortedList(List a) { + // An invariant that the list is non-null, non-empty and sorted + UtMock.assume(a != null); + UtMock.assume(a.size() > 0); + UtMock.assume(a.get(0) != null); + + for (int i = 0; i < a.size() - 1; i++) { + Integer element = a.get(i + 1) + UtMock.assume(element != null); + UtMock.assume(a.get(i) <= element); + } + + return a; +} +``` + +Thus, `assume` is a mechanism to provide some known properties of the program to the symbolic engine. + +### UtMock.assumeOrExecuteConcretely(predicate) +It is a similar concept to the `assume` with the only difference: it does not drop +paths violating the predicate, but execute them concretely from the moment of the +first encountered controversy. Let's take a look at the example below: + +```java +int foo(List list) { + // Let's assume that we have small lists only + UtMock.assume(list.size() <= 10); + + if (list.size() > 10) { + throw new RuntimeException("Unreachable branch"); + } else { + return 0; + } +} +``` +Here we decided to take into consideration lists with sizes less or equal to 10 to improve performance, and, therefore, lost +the branch with possible exception. Let's change `assume` to `assumeOrExecuteConcretely`. +```java +int foo(List list) { + // Let's assume that we have small lists only + UtMock.assumeOrExecuteConcretely(list.size() <= 10); + + if (list.size() > 10) { + throw new RuntimeException("Now we will cover this branch"); + } else { + return 0; + } +} +``` +Now we will cover both branches of the MUT. How did we do it? +At the moment we processed `if` condition we got conflicting constraints: `list.size <= 10` and +`list.size > 10`. In contrast to the example with `assume` method usage, here we know that +we got conflict with the provided predicate and we stop symbolic analysis, remove this assumption from +the path constraints, resolve the MUT's parameters and run the MUT using concrete execution. + +Thus, `assumeOrExecuteConcretely` is a way to provide to the engine information about the program +you'd like to take into account, but if it is impossible, the engine will run the MUT concretely trying to +cover at least something after the encountered controversy. + +## Implementation +Implementation of the `assume` does not have anything interesting -- +we add the predicate into path hard-constraints, and it eventually removes violating +paths from consideration. + +Processing a predicate passed as argument in `assumeOrExecuteConcretely` is more tricky. +Due to the way we work with the solver, it cannot be added to the path constraints +directly. We treat hard PC as hypothesis and add them to the solver directly, that deprives us +opportunity to calculate unsat-core to check whether the predicate was a part of it. + +Because of it, we introduced an additional type of path constraints. Now we have three of them: +hard, soft and assumptions. +* Hard constraints -- properties of the program that must be satisfied at any point of the program. +* Soft constraints -- properties of the program we want to satisfy, but we can remove them if it is impossible. +For example, it might be information that some number should be less than zero. But if it is not, we still +can continue exploration of the same path without this constraint. +* Assumptions -- predicates passed in the `assumeOrExecuteConcretely`. If we have a controversy between +an assumption and hard constraints, we should execute the MUT concretely without violating assumption. + +Now, when we check if some state is satisfiable, we put hard constraints as hypothesis into the solver +and check their consistency with soft constraints and assumptions. If the solver returns UNSAT status with +non-empty unsat core, we remove all conflicting soft constraints from it and try again. If we have +UNSAT status for the second time and assumptions in it, we remove them from the request and calculates +status once again. If it is SAT, we put this state in the queue for concrete executions, otherwise -- remove the +state from consideration. + +## Problems +The main problem is that we didn't get the result we expected. We have many `assume` usages +in overridden classes source code that limits their size to improve performance. Because of that, the following +code does not work (we don't generate any executions for them). + +```java +void bigList(List list) { + UtMock.assume(list != null && list.size() > MAX_LIST_SIZE); +} + +void bigSet(Set set) { + UtMock.assume(set != null && set.size() > MAX_SET_SIZE); +} + +void bigMap(Map map) { + UtMock.assume(map != null && map.size() > MAX_MAP_SIZE); +} +``` +The problem in a `preconditionCheck` method of the wrappers. It contains something like that: +```java +private void preconditionCheck() { + if (alreadyVisited(this)) { + return; + } + ... + assume(elementData.end >= 0 & elementData.end <= MAX_LIST_SIZE); + ... +} +``` +It is a method that imposes restrictions at the overridden classes provided as arguments. +For `Lists` the idea works fine, we replace `assume` with `assumeOrExecuteConcretely` and +find additional branches. +```java +private void preconditionCheck() { + if (alreadyVisited(this)) { + return; + } + ... + assume(elementData.end >= 0); + assumeOrExecuteConcretely(elementData.end <= MAX_LIST_SIZE); + ... +} + +// Now it works! +void bigList(List list) { + UtMock.assume(list != null && list.size() > MAX_LIST_SIZE); +} +``` + +But it doesn't work for `String`, `HashSet` and `HashMap`. + +The problem with `String` is connected with the way we represent them. Restriction for the size is closely +connected with the internal storage of chars -- we create a new arrays of chars with some size `n` using `new char[n]` instruction. +It adds hard constraint that max size of the string is `n` and assumption that `n` is less that `MAX_STRING_SIZE`. +Somewhere later in the code we have a condition that `String.length() > MAX_STRING_SIZE`. Unfortunately, +it will cause not only controversy between the assumption and new hard constraints, but and controversy +between internal array size (hard constraint) and the new-coming hard constraint, that will cause UNSAT status and +we will lose this branch anyway. + +`HashSet` and `HashMap` is a different story. The problem there is inside of `preconditionCheck` implementation. Let's take +a look at a part of it: +```java +assume(elementData.begin == 0); +assume(elementData.end >= 0); +assumeOrExecuteConcretely(elementData.end <= 3); + +parameter(elementData); +parameter(elementData.storage); +doesntThrow(); + +// check that all elements are distinct. +for (int i = elementData.begin; i < elementData.end; i++) { + E element = elementData.get(i); + parameter(element); + // make element address non-positive + + // if key is not null, check its hashCode for exception + if (element != null) { + element.hashCode(); + } + + // check that there are no duplicate values + // we can start with a next value, as all previous values are already processed + for (int j = i + 1; j < elementData.end; j++) { + // we use Objects.equals to process null case too + assume(!Objects.equals(element, elementData.get(j))); + } +} + +visit(this); +``` +The problem happens at the first line of the cycle. We now (from the first line of the snippet) that +the cycle will be from zero to three. The problem is in the `i < elementData.end` check. It produces +at the fourth iteration hard constraint that `elementData.begin + 4 < elementData.end` and we have +an assumption that `elementData.end <= 3`. It will cause a concrete run of the MUT in every +`preconditionCheck` analysis with a constraint `elementData.end == 4`. Moreover, it still won't +help us with code like `if (someHashSet.size() == 10)`, since we will never get here without hard +constraint `elementData.end < 4` that came from the cycle. \ No newline at end of file diff --git a/utbot-api/src/main/java/org/utbot/api/mock/UtMock.java b/utbot-api/src/main/java/org/utbot/api/mock/UtMock.java index 1b7b512dfb..c7f7b2215b 100644 --- a/utbot-api/src/main/java/org/utbot/api/mock/UtMock.java +++ b/utbot-api/src/main/java/org/utbot/api/mock/UtMock.java @@ -13,6 +13,14 @@ public static T makeSymbolic(boolean isNullable) { @SuppressWarnings("unused") public static void assume(boolean predicate) { // to use compilers checks, i.e. for possible NPE - if (!predicate) throw new RuntimeException(); + if (!predicate) { + throw new RuntimeException(); + } + } + + @SuppressWarnings("unused") + public static void assumeOrExecuteConcretely(boolean predicate) { + // In oppose to assume, we don't have predicate check here + // to avoid RuntimeException during concrete execution } } \ No newline at end of file diff --git a/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt b/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt index 76d1ed0c97..17abca62cf 100644 --- a/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt +++ b/utbot-framework-api/src/main/kotlin/org/utbot/framework/UtSettings.kt @@ -294,6 +294,14 @@ object UtSettings { */ var enableUnsatCoreCalculationForHardConstraints by getBooleanProperty(false) + /** + * Enable it to process states with unknown solver status + * from the queue to concrete execution. + * + * True by default. + */ + var processUnknownStatesDuringConcreteExecution by getBooleanProperty(true) + /** * 2^{this} will be the length of observed subpath. * See [SubpathGuidedSelector] diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java index e4e9c8b342..2b34640b25 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java @@ -7,6 +7,7 @@ import static org.utbot.api.mock.UtMock.assume; import static org.utbot.engine.overrides.UtLogicMock.ite; +import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.less; import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely; @@ -34,7 +35,7 @@ public static byte parseByte(String s, int radix) { if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) { throw new NumberFormatException(); } - assume(s.length() <= 10); + assumeOrExecuteConcretely(s.length() <= 10); // we need two branches to add more options for concrete executor to find both branches if (s.charAt(0) == '-') { executeConcretely(); diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java index 0c08c5d869..1142f01606 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java @@ -5,7 +5,7 @@ import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; -import static org.utbot.api.mock.UtMock.assume; +import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.engine.overrides.UtLogicMock.less; import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely; @@ -34,7 +34,7 @@ public static int parseInt(String s, int radix) { if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) { throw new NumberFormatException(); } - assume(s.length() <= 10); + assumeOrExecuteConcretely(s.length() <= 10); // we need two branches to add more options for concrete executor to find both branches if (s.charAt(0) == '-') { executeConcretely(); @@ -62,7 +62,7 @@ public static int parseUnsignedInt(String s, int radix) { if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) { throw new NumberFormatException(); } - assume(s.length() <= 10); + assumeOrExecuteConcretely(s.length() <= 10); if (s.charAt(0) == '-') { throw new NumberFormatException(); } else { @@ -77,8 +77,8 @@ public static String toString(int i) { } // assumes are placed here to limit search space of solver // and reduce time of solving queries with bv2int expressions - assume(i <= 0x8000); - assume(i >= -0x8000); + assumeOrExecuteConcretely(i <= 0x8000); + assumeOrExecuteConcretely(i >= -0x8000); // condition = i < 0 boolean condition = less(i, 0); // prefix = condition ? "-" : "" diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java index 9b7a9fcdb5..4ee5283716 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java @@ -5,7 +5,7 @@ import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; -import static org.utbot.api.mock.UtMock.assume; +import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.engine.overrides.UtLogicMock.less; import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely; @@ -34,7 +34,7 @@ public static long parseLong(String s, int radix) { if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) { throw new NumberFormatException(); } - assume(s.length() <= 10); + assumeOrExecuteConcretely(s.length() <= 10); // we need two branches to add more options for concrete executor to find both branches if (s.charAt(0) == '-') { executeConcretely(); @@ -62,7 +62,7 @@ public static long parseUnsignedLong(String s, int radix) { if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) { throw new NumberFormatException(); } - assume(s.length() <= 10); + assumeOrExecuteConcretely(s.length() <= 10); if (s.charAt(0) == '-') { throw new NumberFormatException(); } else { @@ -77,8 +77,8 @@ public static String toString(long l) { } // assumes are placed here to limit search space of solver // and reduce time of solving queries with bv2int expressions - assume(l <= 10000); - assume(l >= 10000); + assumeOrExecuteConcretely(l <= 10000); + assumeOrExecuteConcretely(l >= -10000); // condition = l < 0 boolean condition = less(l, 0); // prefix = condition ? "-" : "" diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java index af7263b898..d8b47fbaf3 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java @@ -5,7 +5,7 @@ import org.utbot.engine.overrides.strings.UtString; import org.utbot.engine.overrides.strings.UtStringBuilder; -import static org.utbot.api.mock.UtMock.assume; +import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtLogicMock.ite; import static org.utbot.engine.overrides.UtLogicMock.less; import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely; @@ -34,7 +34,7 @@ public static java.lang.Short parseShort(String s, int radix) { if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) { throw new NumberFormatException(); } - assume(s.length() <= 10); + assumeOrExecuteConcretely(s.length() <= 10); // we need two branches to add more options for concrete executor to find both branches if (s.charAt(0) == '-') { executeConcretely(); @@ -50,8 +50,8 @@ public static String toString(short s) { boolean condition = less(s, (short) 0); // assumes are placed here to limit search space of solver // and reduce time of solving queries with bv2int expressions - assume(s <= 10000); - assume(s >= 10000); + assumeOrExecuteConcretely(s <= 10000); + assumeOrExecuteConcretely(s >= -10000); // prefix = condition ? "-" : "" String prefix = ite(condition, "-", ""); UtStringBuilder sb = new UtStringBuilder(prefix); diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java index a88597ced5..9020f73192 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java @@ -18,6 +18,7 @@ import static org.utbot.api.mock.UtMock.assume; import static org.utbot.engine.ResolverKt.MAX_LIST_SIZE; import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited; +import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely; import static org.utbot.engine.overrides.UtOverrideMock.parameter; import static org.utbot.engine.overrides.UtOverrideMock.visit; @@ -83,7 +84,7 @@ void preconditionCheck() { int size = elementData.end; assume(elementData.begin == 0); assume(size >= 0); - assume(size <= MAX_LIST_SIZE); + assumeOrExecuteConcretely(size <= MAX_LIST_SIZE); visit(this); } diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java index 8e8e296493..d709cec484 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java @@ -100,12 +100,12 @@ void preconditionCheck() { parameter(values.touched); parameter(values.storage); parameter(keys); - // for some unknown reason parameter(keys.storage) leads to MapValuesTest::testIteratorNext test failure + parameter(keys.storage); assume(values.size == keys.end); assume(values.touched.length == keys.end); doesntThrow(); - for (int i = 0; i < keys.end; i++) { + for (int i = keys.begin; i < keys.end; i++) { K key = keys.get(i); assume(values.touched[i] == key); diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashSet.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashSet.java index 744a1b5f15..b081ecab7c 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashSet.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashSet.java @@ -73,7 +73,7 @@ void preconditionCheck() { doesntThrow(); // check that all elements are distinct. - for (int i = 0; i < elementData.end; i++) { + for (int i = elementData.begin; i < elementData.end; i++) { E element = elementData.get(i); parameter(element); // make element address non-positive diff --git a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtLinkedList.java b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtLinkedList.java index 0d62cee67a..163e88f761 100644 --- a/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtLinkedList.java +++ b/utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtLinkedList.java @@ -19,6 +19,7 @@ import static org.utbot.engine.ResolverKt.MAX_LIST_SIZE; import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited; import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely; +import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely; import static org.utbot.engine.overrides.UtOverrideMock.parameter; import static org.utbot.engine.overrides.UtOverrideMock.visit; @@ -79,7 +80,7 @@ private void preconditionCheck() { parameter(elementData.storage); assume(elementData.begin == 0); assume(elementData.end >= 0); - assume(elementData.end <= MAX_LIST_SIZE); + assumeOrExecuteConcretely(elementData.end <= MAX_LIST_SIZE); visit(this); } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/AnnotationResolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/AnnotationResolver.kt index 31033a9eec..e6509898d6 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/AnnotationResolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/AnnotationResolver.kt @@ -109,12 +109,6 @@ val SootMethod.findMockAnnotationOrNull val SootMethod.hasInternalMockAnnotation get() = annotationsOrNull?.singleOrNull { it.type == utInternalUsageBytecodeSignature } != null -/** - * Returns true if the [SootMethod]'s signature is equal to [UtMock.assume]'s signature, false otherwise. - */ -val SootMethod.isUtMockAssume - get() = signature == assumeMethod.signature - val utClassMockBytecodeSignature = UtClassMock::class.java.bytecodeSignature() val utConstructorMockBytecodeSignature = UtConstructorMock::class.java.bytecodeSignature() val utInternalUsageBytecodeSignature = UtInternalUsage::class.java.bytecodeSignature() diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index 1d0347fb82..860d1c7d71 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt @@ -8,6 +8,7 @@ import org.utbot.engine.pc.UtIsExpression import org.utbot.engine.pc.UtTrue import org.utbot.engine.pc.mkAnd import org.utbot.engine.pc.mkOr +import org.utbot.engine.symbolic.Assumption import org.utbot.engine.symbolic.HardConstraint import org.utbot.engine.symbolic.SoftConstraint import org.utbot.engine.symbolic.SymbolicStateUpdate @@ -134,15 +135,17 @@ data class MethodResult( symbolicResult: SymbolicResult, hardConstraints: HardConstraint = HardConstraint(), softConstraints: SoftConstraint = SoftConstraint(), + assumption: Assumption = Assumption(), memoryUpdates: MemoryUpdate = MemoryUpdate() - ) : this(symbolicResult, SymbolicStateUpdate(hardConstraints, softConstraints, memoryUpdates)) + ) : this(symbolicResult, SymbolicStateUpdate(hardConstraints, softConstraints, assumption, memoryUpdates)) constructor( value: SymbolicValue, hardConstraints: HardConstraint = HardConstraint(), softConstraints: SoftConstraint = SoftConstraint(), + assumption: Assumption = Assumption(), memoryUpdates: MemoryUpdate = MemoryUpdate(), - ) : this(SymbolicSuccess(value), hardConstraints, softConstraints, memoryUpdates) + ) : this(SymbolicSuccess(value), hardConstraints, softConstraints, assumption, memoryUpdates) } /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt index 7e034050e7..9c831771c0 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt @@ -320,7 +320,16 @@ data class ExecutionState( */ fun prettifiedPathLog(): String { val path = fullPath() - val prettifiedPath = path.joinToString(separator = "\n") { (stmt, depth, decision) -> + val prettifiedPath = prettifiedPath(path) + return " MD5(path)=${md5(prettifiedPath)}\n$prettifiedPath" + } + + private fun md5(prettifiedPath: String) = prettifiedPath.md5() + + fun md5() = prettifiedPath(fullPath()).md5() + + private fun prettifiedPath(path: List) = + path.joinToString(separator = "\n") { (stmt, depth, decision) -> val prefix = when (decision) { CALL_DECISION_NUM -> "call[${depth}] - " + "".padEnd(2 * depth, ' ') RETURN_DECISION_NUM -> " ret[${depth - 1}] - " + "".padEnd(2 * depth, ' ') @@ -328,8 +337,6 @@ data class ExecutionState( } "$prefix$stmt" } - return " MD5(path)=${prettifiedPath.md5()}\n$prettifiedPath" - } fun definitelyFork() { stateAnalyticsProperties.definitelyFork() diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt index d987f9924d..eea305d56b 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt @@ -18,6 +18,7 @@ import org.utbot.engine.pc.UtSeqSort import org.utbot.engine.pc.UtShortSort import org.utbot.engine.pc.UtSolverStatusKind import org.utbot.engine.pc.UtSolverStatusSAT +import org.utbot.engine.symbolic.Assumption import org.utbot.engine.pc.UtSort import org.utbot.engine.pc.mkArrayWithConst import org.utbot.engine.pc.mkBool @@ -46,6 +47,7 @@ import kotlin.reflect.jvm.javaConstructor import kotlin.reflect.jvm.javaMethod import kotlinx.collections.immutable.PersistentMap import kotlinx.collections.immutable.persistentHashMapOf +import org.utbot.engine.pc.UtSolverStatusUNDEFINED import soot.ArrayType import soot.PrimType import soot.RefLikeType @@ -435,18 +437,27 @@ val SootClass.isLibraryNonOverriddenClass: Boolean /** * Returns a state from the list that has [UtSolverStatusSAT] status. * Inside it calls UtSolver.check if required. + * + * [processStatesWithUnknownStatus] is responsible for solver checks for states + * with unknown status. Note that this calculation might take a long time. */ -fun MutableList.pollUntilSat(): ExecutionState? { +fun MutableList.pollUntilSat(processStatesWithUnknownStatus: Boolean): ExecutionState? { while (!isEmpty()) { val state = removeLast() with(state.solver) { + if (lastStatus.statusKind == UtSolverStatusKind.UNSAT) return@with + if (lastStatus.statusKind == UtSolverStatusKind.SAT) return state - if (lastStatus.statusKind == UtSolverStatusKind.UNKNOWN) { - val result = check(respectSoft = true) + require(failedAssumptions.isEmpty()) { "There are failed requirements in the queue to execute concretely" } + + if (processStatesWithUnknownStatus) { + if (lastStatus == UtSolverStatusUNDEFINED) { + val result = check(respectSoft = true) - if (result.statusKind == UtSolverStatusKind.SAT) return state + if (result.statusKind == UtSolverStatusKind.SAT) return state + } } } } @@ -458,3 +469,23 @@ fun isOverriddenClass(type: RefType) = type.sootClass.isOverridden val SootMethod.isSynthetic: Boolean get() = soot.Modifier.isSynthetic(modifiers) + +/** + * Returns true if the [SootMethod]'s signature is equal to [UtMock.assume]'s signature, false otherwise. + */ +val SootMethod.isUtMockAssume + get() = signature == assumeMethod.signature + +/** + * Returns true if the [SootMethod]'s signature is equal to + * [UtMock.assumeOrExecuteConcretely]'s signature, false otherwise. + */ +val SootMethod.isUtMockAssumeOrExecuteConcretely + get() = signature == assumeOrExecuteConcretelyMethod.signature + +/** + * Returns true is the [SootMethod] is defined in a class from + * [UTBOT_OVERRIDE_PACKAGE_NAME] package and its name is `preconditionCheck`. + */ +val SootMethod.isPreconditionCheckMethod + get() = declaringClass.isOverridden && name == "preconditionCheck" diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt index 4d9d12a03f..0c6c704faf 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Mocks.kt @@ -168,14 +168,13 @@ class Mocker( mockInfo: UtMockInfo ): Boolean { if (isUtMockAssume(mockInfo)) return false // never mock UtMock.assume invocation + if (isUtMockAssumeOrExecuteConcretely(mockInfo)) return false // never mock UtMock.assumeOrExecuteConcretely invocation if (isOverriddenClass(type)) return false // never mock overriden classes if (isMakeSymbolic(mockInfo)) return true // support for makeSymbolic if (type.sootClass.isArtificialEntity) return false // never mock artificial types, i.e. Maps$lambda_computeValue_1__7 - //TODO: SAT-1496 verify that using SootClass here is correct if (!isEngineClass(type) && (type.sootClass.isInnerClass || type.sootClass.isLocal || type.sootClass.isAnonymous)) return false // there is no reason (and maybe no possibility) to mock such classes if (!isEngineClass(type) && type.sootClass.isPrivate) return false // could not mock private classes (even if it is in mock always list) if (mockAlways(type)) return true // always mock randoms and loggers - if (type.sootClass.isArtificialEntity) return false // never mock artificial types, i.e. Maps$lambda_computeValue_1__7 if (mockInfo is UtFieldMockInfo) { return when { mockInfo.fieldId.declaringClass.packageName.startsWith("java.lang") -> false @@ -197,6 +196,9 @@ class Mocker( private fun isUtMockAssume(mockInfo: UtMockInfo) = mockInfo is UtStaticMethodMockInfo && mockInfo.methodId.signature == assumeBytecodeSignature + private fun isUtMockAssumeOrExecuteConcretely(mockInfo: UtMockInfo) = + mockInfo is UtStaticMethodMockInfo && mockInfo.methodId.signature == assumeOrExecuteConcretelyBytecodeSignature + private fun isEngineClass(type: RefType) = type.className in engineClasses private fun mockAlways(type: RefType) = type.className in classesToMockAlways @@ -304,6 +306,9 @@ internal val nonNullableMakeSymbolic: SootMethod internal val assumeMethod: SootMethod get() = utMockClass.getMethod(ASSUME_NAME, listOf(BooleanType.v())) +internal val assumeOrExecuteConcretelyMethod: SootMethod + get() = utMockClass.getMethod(ASSUME_OR_EXECUTE_CONCRETELY_NAME, listOf(BooleanType.v())) + val makeSymbolicBytecodeSignature: String get() = makeSymbolicMethod.executableId.signature @@ -313,6 +318,9 @@ val nonNullableMakeSymbolicBytecodeSignature: String val assumeBytecodeSignature: String get() = assumeMethod.executableId.signature +val assumeOrExecuteConcretelyBytecodeSignature: String + get() = assumeOrExecuteConcretelyMethod.executableId.signature + internal val UTBOT_OVERRIDE_PACKAGE_NAME = UtOverrideMock::class.java.packageName private val arraycopyMethod : KFunction5, Int, Array, Int, Int, Unit> = UtArrayMock::arraycopy @@ -331,3 +339,4 @@ internal val utLogicMockIteMethodName = UtLogicMock::ite.name private const val MAKE_SYMBOLIC_NAME = "makeSymbolic" private const val ASSUME_NAME = "assume" +private const val ASSUME_OR_EXECUTE_CONCRETELY_NAME = "assumeOrExecuteConcretely" diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt index 9d203ca991..9ba79b1b34 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt @@ -96,10 +96,12 @@ import org.utbot.engine.selectors.strategies.GraphViz import org.utbot.engine.selectors.subpathGuidedSelector import org.utbot.engine.symbolic.HardConstraint import org.utbot.engine.symbolic.SoftConstraint +import org.utbot.engine.symbolic.Assumption import org.utbot.engine.symbolic.SymbolicState import org.utbot.engine.symbolic.SymbolicStateUpdate import org.utbot.engine.symbolic.asHardConstraint import org.utbot.engine.symbolic.asSoftConstraint +import org.utbot.engine.symbolic.asAssumption import org.utbot.engine.symbolic.asUpdate import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues import org.utbot.engine.util.statics.concrete.isEnumAffectingExternalStatics @@ -116,6 +118,7 @@ import org.utbot.framework.UtSettings.pathSelectorType import org.utbot.framework.UtSettings.preferredCexOption import org.utbot.framework.UtSettings.substituteStaticsWithSymbolicVariable import org.utbot.framework.UtSettings.useDebugVisualization +import org.utbot.framework.UtSettings.processUnknownStatesDuringConcreteExecution import org.utbot.framework.concrete.UtConcreteExecutionData import org.utbot.framework.concrete.UtConcreteExecutionResult import org.utbot.framework.concrete.UtExecutionInstrumentation @@ -441,7 +444,9 @@ class UtBotSymbolicEngine( } if (controller.executeConcretely || statesForConcreteExecution.isNotEmpty()) { - val state = pathSelector.pollUntilFastSAT() ?: statesForConcreteExecution.pollUntilSat() ?: break + val state = pathSelector.pollUntilFastSAT() + ?: statesForConcreteExecution.pollUntilSat(processUnknownStatesDuringConcreteExecution) + ?: break // This state can contain inconsistent wrappers - for example, Map with keys but missing values. // We cannot use withWrapperConsistencyChecks here because it needs solver to work. // So, we have to process such cases accurately in wrappers resolving. @@ -1371,28 +1376,63 @@ class UtBotSymbolicEngine( environment.state.definitelyFork() } - positiveCaseEdge?.let { edge -> - environment.state.expectUndefined() - val positiveCaseState = environment.state.updateQueued( - edge, - SymbolicStateUpdate( - hardConstraints = positiveCasePathConstraint.asHardConstraint(), - softConstraints = setOfNotNull(positiveCaseSoftConstraint).asSoftConstraint() - ) + resolvedCondition.symbolicStateUpdates.positiveCase - ) - pathSelector.offer(positiveCaseState) + /* assumeOrExecuteConcrete in jimple looks like: + ``` z0 = a > 5 + if (z0 == 1) goto label1 + assumeOrExecuteConcretely(z0) + + label1: + assumeOrExecuteConcretely(z0) + ``` + + We have to detect such situations to avoid addition `a > 5` into hardConstraints, + because we want to add them into Assumptions. + + Note: we support only simple predicates right now (one logical operation), + otherwise they will be added as hard constraints, and we will not execute + the state concretely if there will be UNSAT because of assumptions. + */ + val isAssumeExpr = positiveCaseEdge?.let { isConditionForAssumeOrExecuteConcretely(it.dst) } ?: false + + // in case of assume we want to have the only branch where $z = 1 (it is a negative case) + if (!isAssumeExpr) { + positiveCaseEdge?.let { edge -> + environment.state.expectUndefined() + val positiveCaseState = environment.state.updateQueued( + edge, + SymbolicStateUpdate( + hardConstraints = positiveCasePathConstraint.asHardConstraint(), + softConstraints = setOfNotNull(positiveCaseSoftConstraint).asSoftConstraint() + ) + resolvedCondition.symbolicStateUpdates.positiveCase + ) + pathSelector.offer(positiveCaseState) + } } + // Depending on existance of assumeExpr we have to add corresponding hardConstraints and assumptions + val hardConstraints = if (!isAssumeExpr) negativeCasePathConstraint.asHardConstraint() else HardConstraint() + val assumption = if (isAssumeExpr) negativeCasePathConstraint.asAssumption() else Assumption() + val negativeCaseState = environment.state.updateQueued( negativeCaseEdge, SymbolicStateUpdate( - hardConstraints = negativeCasePathConstraint.asHardConstraint(), + hardConstraints = hardConstraints, softConstraints = setOfNotNull(negativeCaseSoftConstraint).asSoftConstraint(), + assumptions = assumption ) + resolvedCondition.symbolicStateUpdates.negativeCase ) pathSelector.offer(negativeCaseState) } + /** + * Returns true if the next stmt is an [assumeOrExecuteConcretelyMethod] invocation, false otherwise. + */ + private fun isConditionForAssumeOrExecuteConcretely(stmt: Stmt): Boolean { + val successor = globalGraph.succStmts(stmt).singleOrNull() as? JInvokeStmt ?: return false + val invokeExpression = successor.invokeExpr as? JStaticInvokeExpr ?: return false + return invokeExpression.method.isUtMockAssumeOrExecuteConcretely + } + private fun traverseInvokeStmt(current: JInvokeStmt) { val results = invokeResult(current.invokeExpr) @@ -2721,19 +2761,39 @@ class UtBotSymbolicEngine( return overriddenResults + originResults } - private fun invoke(target: InvocationTarget, parameters: List): List { - val substitutedMethod = typeRegistry.findSubstitutionOrNull(target.method) + private fun invoke( + target: InvocationTarget, + parameters: List + ): List = with(target.method) { + val substitutedMethod = typeRegistry.findSubstitutionOrNull(this) - if (target.method.isNative && substitutedMethod == null) return processNativeMethod(target) + if (isNative && substitutedMethod == null) return processNativeMethod(target) - // If we face UtMock.assume call, we should continue only with the branch where the predicate - // from the parameters is equal true - return when { - target.method.isUtMockAssume -> { + // If we face UtMock.assume call, we should continue only with the branch + // where the predicate from the parameters is equal true + when { + isUtMockAssume || isUtMockAssumeOrExecuteConcretely -> { val param = UtCastExpression(parameters.single() as PrimitiveValue, BooleanType.v()) + + val assumptionStmt = mkEq(param, UtTrue) + val (hardConstraints, assumptions) = if (isUtMockAssume) { + // For UtMock.assume we must add the assumeStmt to the hard constraints + setOf(assumptionStmt) to emptySet() + } else { + // For assumeOrExecuteConcretely we must add the statement to the assumptions. + // It is required to have opportunity to remove it later in case of unsat state + // because of it and execute the state concretely. + emptySet() to setOf(assumptionStmt) + } + + val symbolicStateUpdate = SymbolicStateUpdate( + hardConstraints = hardConstraints.asHardConstraint(), + assumptions = assumptions.asAssumption() + ) + val stateToContinue = environment.state.updateQueued( globalGraph.succ(environment.state.stmt), - SymbolicStateUpdate(hardConstraints = mkEq(param, UtTrue).asHardConstraint()) + symbolicStateUpdate ) pathSelector.offer(stateToContinue) @@ -2742,17 +2802,15 @@ class UtBotSymbolicEngine( queuedSymbolicStateUpdates += UtFalse.asHardConstraint() emptyList() } - target.method.declaringClass == utOverrideMockClass -> utOverrideMockInvoke(target, parameters) - target.method.declaringClass == utLogicMockClass -> utLogicMockInvoke(target, parameters) - target.method.declaringClass == utArrayMockClass -> utArrayMockInvoke(target, parameters) + declaringClass == utOverrideMockClass -> utOverrideMockInvoke(target, parameters) + declaringClass == utLogicMockClass -> utLogicMockInvoke(target, parameters) + declaringClass == utArrayMockClass -> utArrayMockInvoke(target, parameters) else -> { - val graph = substitutedMethod?.jimpleBody()?.graph() ?: target.method.jimpleBody().graph() - val isLibraryMethod = target.method.isLibraryMethod + val graph = substitutedMethod?.jimpleBody()?.graph() ?: jimpleBody().graph() pushToPathSelector(graph, target.instance, parameters, target.constraints, isLibraryMethod) emptyList() } } - } private fun utOverrideMockInvoke(target: InvocationTarget, parameters: List): List { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt index 6d64c0263e..51e41560ba 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt @@ -119,7 +119,8 @@ data class Query( lts: Map = this@Query.lts, gts: Map = this@Query.gts ) = AxiomInstantiationRewritingVisitor(eqs, lts, gts).let { visitor -> - this.map { it.simplify(visitor) }.map { simplifyGeneric(it) } + this.map { it.simplify(visitor) } + .map { simplifyGeneric(it) } .flatMap { splitAnd(it) } + visitor.instantiatedArrayAxioms } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index 1ea07cfcba..d8dd4d0682 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -12,6 +12,8 @@ import org.utbot.engine.TypeRegistry import org.utbot.engine.pc.UtSolverStatusKind.SAT import org.utbot.engine.pc.UtSolverStatusKind.UNKNOWN import org.utbot.engine.pc.UtSolverStatusKind.UNSAT +import org.utbot.engine.prettify +import org.utbot.engine.symbolic.Assumption import org.utbot.engine.symbolic.HardConstraint import org.utbot.engine.symbolic.SoftConstraint import org.utbot.engine.prettify @@ -126,6 +128,11 @@ data class UtSolver constructor( //these constraints.hard are already added to z3solver private var constraints: BaseQuery = Query(), + // Constraints that should not be added in the solver as hypothesis. + // Instead, we use `check` to find out if they are satisfiable. + // It is required to have unsat cores with them. + var assumption: Assumption = Assumption(), + //new constraints for solver (kind of incremental behavior) private var hardConstraintsNotYetAddedToZ3Solver: PersistentSet = persistentHashSetOf(), @@ -136,6 +143,11 @@ data class UtSolver constructor( private val translator: Z3TranslatorVisitor = Z3TranslatorVisitor(context, typeRegistry) + /** + * Constraints from the [assumption] that are not satisfiable. + * All the elements were found in the calculated unsat core. + */ + internal val failedAssumptions = mutableListOf() //protection against solver reusage private var canBeCloned: Boolean = true @@ -163,13 +175,13 @@ data class UtSolver constructor( var expectUndefined: Boolean = false - fun add(hard: HardConstraint, soft: SoftConstraint): UtSolver { + fun add(hard: HardConstraint, soft: SoftConstraint, assumption: Assumption = Assumption()): UtSolver { // status can implicitly change here to UNDEFINED or UNSAT val newConstraints = constraints.with(hard.constraints, soft.constraints) val wantClone = (expectUndefined && newConstraints.status is UtSolverStatusUNDEFINED) || (!expectUndefined && newConstraints.status !is UtSolverStatusUNSAT) - return if (wantClone && canBeCloned) { + return if (wantClone && canBeCloned && assumption.constraints.isEmpty()) { // try to reuse z3 Solver with value SAT when possible canBeCloned = false copy( @@ -177,13 +189,22 @@ data class UtSolver constructor( hardConstraintsNotYetAddedToZ3Solver = hardConstraintsNotYetAddedToZ3Solver.addAll(newConstraints.lastAdded), ) } else { + // We pass here undefined status to force calculation + // at the next `check` call. Otherwise, we'd ignore + // the given assumptions and return already calculated status. + val constraintsWithStatus = if (assumption.constraints.isNotEmpty()) { + newConstraints.withStatus(UtSolverStatusUNDEFINED) + } else { + newConstraints + } /* Create new solver to add another constraints (new branches) New solver hasn't already added constraints thus we must add them again */ copy( - constraints = newConstraints, + constraints = constraintsWithStatus, hardConstraintsNotYetAddedToZ3Solver = newConstraints.hard, + assumption = this.assumption + assumption, z3Solver = context.mkSolver().also { it.setParameters(params) }, ) } @@ -195,11 +216,12 @@ data class UtSolver constructor( } val translatedSoft = if (respectSoft && preferredCexOption) { - constraints.soft.associateByTo(mutableMapOf()) { translator.translate(it) as BoolExpr } + constraints.soft.translate() } else { mutableMapOf() } + val translatedAssumes = assumption.constraints.translate() val statusHolder = logger.trace().bracket("High level check(): ", { it }) { Predictors.smtIncremental.learnOn(IncrementalData(constraints.hard, hardConstraintsNotYetAddedToZ3Solver)) { @@ -210,7 +232,7 @@ data class UtSolver constructor( "${str.md5()}\n$str" } - when (val status = check(translatedSoft)) { + when (val status = check(translatedSoft, translatedAssumes)) { SAT -> UtSolverStatusSAT(translator, z3Solver) else -> UtSolverStatusUNSAT(status) } @@ -227,19 +249,31 @@ data class UtSolver constructor( z3Solver.reset() } - private fun check(translatedSoft: MutableMap): UtSolverStatusKind { + private fun check( + translatedSoft: MutableMap, + translatedAssumptions: MutableMap + ): UtSolverStatusKind { + val assumptionsInUnsatCore = mutableListOf() + while (true) { val res = logger.trace().bracket("Low level check(): ", { it }) { - z3Solver.check(*translatedSoft.keys.toTypedArray()) + val constraintsToCheck = translatedSoft.keys + translatedAssumptions.keys + z3Solver.check(*constraintsToCheck.toTypedArray()) } when (res) { - SATISFIABLE -> return SAT + SATISFIABLE -> { + if (assumptionsInUnsatCore.isNotEmpty()) { + failedAssumptions += assumptionsInUnsatCore + } + + return SAT + } UNSATISFIABLE -> { val unsatCore = z3Solver.unsatCore // if we don't have any soft constraints and enabled unsat cores // for hard constraints, then calculate it and print the result using the logger - if (translatedSoft.isEmpty() && UtSettings.enableUnsatCoreCalculationForHardConstraints) { + if (translatedSoft.isEmpty() && translatedAssumptions.isEmpty() && UtSettings.enableUnsatCoreCalculationForHardConstraints) { with(context.mkSolver()) { check(*z3Solver.assertions) val constraintsInUnsatCore = this.unsatCore.toList() @@ -253,15 +287,26 @@ data class UtSolver constructor( // an unsat core for hard constraints if (unsatCore.isEmpty()) return UNSAT - for (unsatVariable in unsatCore) { - translatedSoft.remove(unsatVariable) - ?: error("$unsatVariable from unsatCore isn't in soft constraints") + val failedSoftConstraints = unsatCore.filter { it in translatedSoft.keys } + + if (failedSoftConstraints.isNotEmpty()) { + failedSoftConstraints.forEach { translatedSoft.remove(it) } + // remove soft constraints first, only then try to remove assumptions + continue } + + unsatCore + .filter { it in translatedAssumptions.keys } + .forEach { + assumptionsInUnsatCore += translatedAssumptions.getValue(it) + translatedAssumptions.remove(it) + } } else -> { logger.debug { "Reason of UNKNOWN: ${z3Solver.reasonUnknown}" } if (translatedSoft.isEmpty()) { - logger.debug {"No soft constraints left, return UNKNOWN"} + logger.debug { "No soft constraints left, return UNKNOWN" } + logger.trace { "Constraints lead to unknown: ${z3Solver.assertions.joinToString("\n")} " } return UNKNOWN } @@ -270,6 +315,9 @@ data class UtSolver constructor( } } } + + private fun Collection.translate(): MutableMap = + associateByTo(mutableMapOf()) { translator.translate(it) as BoolExpr } } enum class UtSolverStatusKind { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt index 571034332e..0e400f527a 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/BasePathSelector.kt @@ -1,6 +1,7 @@ package org.utbot.engine.selectors import org.utbot.engine.ExecutionState +import org.utbot.engine.isPreconditionCheckMethod import org.utbot.engine.pathLogger import org.utbot.engine.pc.UtSolver import org.utbot.engine.pc.UtSolverStatusKind.SAT @@ -83,6 +84,19 @@ abstract class BasePathSelector( state.close() continue } + + // If we have failed assumes, we try to execute the state concretely + if (state.solver.failedAssumptions.isNotEmpty()) { + // But we do not want to execute concretely states because of + // controversies during `preconditionCheck` analysis + if (state.lastMethod?.isPreconditionCheckMethod == true) { + state.close() + } else { + statesForConcreteExecution += state + } + continue + } + return state } return null diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt index 37e2647838..6621a517d2 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/DistanceStatistics.kt @@ -4,6 +4,7 @@ import org.utbot.engine.Edge import org.utbot.engine.ExecutionState import org.utbot.engine.InterProceduralUnitGraph import org.utbot.engine.isReturn +import org.utbot.engine.pathLogger import org.utbot.engine.stmts import kotlin.math.min import kotlinx.collections.immutable.PersistentList @@ -38,8 +39,17 @@ class DistanceStatistics( * Drops executionState if all the edges on path are covered (with respect to uncovered * throw statements of the methods they belong to) and there is no reachable and uncovered statement. */ - override fun shouldDrop(state: ExecutionState) = - state.edges.all { graph.isCoveredWithAllThrowStatements(it) } && distanceToUncovered(state) == Int.MAX_VALUE + override fun shouldDrop(state: ExecutionState): Boolean { + val shouldDrop = state.edges.all { graph.isCoveredWithAllThrowStatements(it) } && distanceToUncovered(state) == Int.MAX_VALUE + + if (shouldDrop) { + pathLogger.debug { + "Dropping state (lastStatus=${state.solver.lastStatus}) by the distance statistics. MD5: ${state.md5()}" + } + } + + return shouldDrop + } fun isCovered(edge: Edge): Boolean = graph.isCovered(edge) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt index ad6aa1f5e2..1a0ad21348 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/EdgeVisitCountingStatistics.kt @@ -3,6 +3,7 @@ package org.utbot.engine.selectors.strategies import org.utbot.engine.Edge import org.utbot.engine.ExecutionState import org.utbot.engine.InterProceduralUnitGraph +import org.utbot.engine.pathLogger import soot.jimple.Stmt import soot.jimple.internal.JReturnStmt import soot.jimple.internal.JReturnVoidStmt @@ -31,7 +32,16 @@ class EdgeVisitCountingStatistics( * - all statements are already covered and execution is complete */ override fun shouldDrop(state: ExecutionState): Boolean { - return state.edges.all { graph.isCoveredWithAllThrowStatements(it) } && state.isComplete() + val shouldDrop = state.edges.all { graph.isCoveredWithAllThrowStatements(it) } && state.isComplete() + + if (shouldDrop) { + pathLogger.debug { + "Dropping state (lastStatus=${state.solver.lastStatus}) " + + "by the edge visit counting statistics. MD5: ${state.md5()}" + } + } + + return shouldDrop } /** diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt index 41273ef444..f17d2b6750 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/selectors/strategies/StepsLimitStoppingStrategy.kt @@ -3,6 +3,7 @@ package org.utbot.engine.selectors.strategies import org.utbot.engine.Edge import org.utbot.engine.ExecutionState import org.utbot.engine.InterProceduralUnitGraph +import org.utbot.engine.pathLogger /** * Stopping strategy that suggest to stop execution @@ -16,7 +17,13 @@ class StepsLimitStoppingStrategy( private var stepsCounter: Int = 0 override fun shouldStop(): Boolean { - return stepsCounter > stepsLimit + val shouldDrop = stepsCounter > stepsLimit + + if (shouldDrop) { + pathLogger.debug { "Steps limit has been exceeded: current step limit is $stepsLimit" } + } + + return shouldDrop } override fun onVisit(edge: Edge) { diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt index ea642a2482..cbe2d5c7ef 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicState.kt @@ -15,10 +15,12 @@ data class SymbolicState( val memory: Memory = Memory(), ) { operator fun plus(update: SymbolicStateUpdate): SymbolicState = - SymbolicState( - solver.add(hard = update.hardConstraints, soft = update.softConstraints), - memory = memory.update(update.memoryUpdates), - ) + with(update) { + SymbolicState( + solver.add(hard = hardConstraints, soft = softConstraints, assumption = assumptions), + memory = memory.update(memoryUpdates), + ) + } operator fun plus(update: HardConstraint): SymbolicState = plus(SymbolicStateUpdate(hardConstraints = update)) diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt index 87ef1396e0..0b883d0a76 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt @@ -39,14 +39,30 @@ class SoftConstraint( SoftConstraint(addConstraints(other.constraints)) } +/** + * Represent constraints that must be satisfied for symbolic execution. + * At the same time, if they don't, the state they belong to still + * might be executed concretely without these assume. + * + * @see + */ +class Assumption( + constraints: Set = emptySet() +): Constraint(constraints) { + override fun plus(other: Assumption): Assumption = Assumption(addConstraints(other.constraints)) + + override fun toString() = constraints.joinToString(System.lineSeparator()) +} + /** * Represents one or more updates that can be applied to [SymbolicState]. * * TODO: move [localMemoryUpdates] to another place */ data class SymbolicStateUpdate( - val hardConstraints: HardConstraint = HardConstraint(setOf()), - val softConstraints: SoftConstraint = SoftConstraint(setOf()), + val hardConstraints: HardConstraint = HardConstraint(), + val softConstraints: SoftConstraint = SoftConstraint(), + val assumptions: Assumption = Assumption(), val memoryUpdates: MemoryUpdate = MemoryUpdate(), val localMemoryUpdates: LocalMemoryUpdate = LocalMemoryUpdate() ) { @@ -54,6 +70,7 @@ data class SymbolicStateUpdate( SymbolicStateUpdate( hardConstraints = hardConstraints + update.hardConstraints, softConstraints = softConstraints + update.softConstraints, + assumptions = assumptions + update.assumptions, memoryUpdates = memoryUpdates + update.memoryUpdates, localMemoryUpdates = localMemoryUpdates + update.localMemoryUpdates ) @@ -64,6 +81,9 @@ data class SymbolicStateUpdate( operator fun plus(update: SoftConstraint): SymbolicStateUpdate = plus(SymbolicStateUpdate(softConstraints = update)) + operator fun plus(update: Assumption): SymbolicStateUpdate = + plus(SymbolicStateUpdate(assumptions = update)) + operator fun plus(update: MemoryUpdate): SymbolicStateUpdate = plus(SymbolicStateUpdate(memoryUpdates = update)) @@ -87,6 +107,10 @@ fun Collection.asSoftConstraint() = SoftConstraint(transformTo fun UtBoolExpression.asSoftConstraint() = SoftConstraint(setOf(this)) +fun Collection.asAssumption() = Assumption(toSet()) + +fun UtBoolExpression.asAssumption() = Assumption(setOf(this)) + private fun Collection.transformToSet(): Set = if (this is Set) this else toSet() fun HardConstraint.asUpdate() = SymbolicStateUpdate(hardConstraints = this) diff --git a/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt b/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt index 260c82e1c5..4fa9d34071 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/framework/concrete/MockValueConstructor.kt @@ -290,7 +290,9 @@ class MockValueConstructor( constructedObjects[model]?.let { return it } with(model) { - val elementClassId = classId.elementClassId!! + val elementClassId = classId.elementClassId ?: error( + "Provided incorrect UtArrayModel without elementClassId. ClassId: ${model.classId}, model: $model" + ) return when (elementClassId.jvmName) { "B" -> ByteArray(length) { primitive(constModel) }.apply { stores.forEach { (index, model) -> this[index] = primitive(model) } diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/arrays/IntArrayBasicsTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/arrays/IntArrayBasicsTest.kt index 255994e261..5d32297515 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/arrays/IntArrayBasicsTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/arrays/IntArrayBasicsTest.kt @@ -18,6 +18,18 @@ internal class IntArrayBasicsTest : AbstractTestCaseGeneratorTest( CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN, CodeGeneration) ) ) { + @Test + fun testIntArrayWithAssumeOrExecuteConcretely() { + check( + IntArrayBasics::intArrayWithAssumeOrExecuteConcretely, + eq(4), + { x, n, r -> x > 0 && n < 20 && r?.size == 2 }, + { x, n, r -> x > 0 && n >= 20 && r?.size == 4 }, + { x, n, r -> x <= 0 && n < 20 && r?.size == 10 }, + { x, n, r -> x <= 0 && n >= 20 && r?.size == 20 }, + ) + } + @Test fun testInitArray() { checkWithException( diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/LinkedListsTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/LinkedListsTest.kt index 2b672c053c..fab796ada3 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/LinkedListsTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/LinkedListsTest.kt @@ -133,7 +133,7 @@ internal class LinkedListsTest : AbstractTestCaseGeneratorTest( LinkedLists::peekLast, eq(3), { l, _ -> l == null }, - { l, r -> l != null && l.isEmpty() && r.isException() }, + { l, r -> l != null && (l.isEmpty() || l.last() == null) && r.isException() }, { l, r -> l != null && l.isNotEmpty() && r.getOrNull() == l.last() }, coverage = DoNotCalculate ) @@ -146,8 +146,8 @@ internal class LinkedListsTest : AbstractTestCaseGeneratorTest( eq(4), { l, _ -> l == null }, { l, r -> l != null && l.isEmpty() && r.isException() }, - { l, _ -> l != null && l.isNotEmpty() && l[0] == null }, - { l, r -> l != null && l.isNotEmpty() && r.getOrNull() == l[0] }, + { l, r -> l != null && l.isNotEmpty() && l[0] == null && r.isException() }, + { l, r -> l != null && l.isNotEmpty() && l[0] != null && r.getOrNull() == l[0] }, coverage = DoNotCalculate ) } diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListAlgorithmsTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListAlgorithmsTest.kt index 6a8988ecaa..445fbf914a 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListAlgorithmsTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListAlgorithmsTest.kt @@ -6,6 +6,7 @@ import org.utbot.examples.eq import org.utbot.framework.codegen.CodeGeneration import org.utbot.framework.plugin.api.CodegenLanguage import org.junit.jupiter.api.Test +import org.utbot.examples.atLeast // TODO failed Kotlin compilation SAT-1332 class ListAlgorithmsTest : AbstractTestCaseGeneratorTest( @@ -23,10 +24,10 @@ class ListAlgorithmsTest : AbstractTestCaseGeneratorTest( ListAlgorithms::mergeListsInplace, eq(4), { a, b, r -> b.subList(0, b.size - 1).any { a.last() < it } && r != null && r == r.sorted() }, - { a, b, r -> a.subList(0, a.size - 1).any { b.last() <= it } && r != null && r == r.sorted() }, + { a, b, r -> (a.subList(0, a.size - 1).any { b.last() <= it } || a.any { ai -> b.any { ai < it } }) && r != null && r == r.sorted() }, { a, b, r -> a[0] < b[0] && r != null && r == r.sorted() }, { a, b, r -> a[0] >= b[0] && r != null && r == r.sorted() }, - coverage = DoNotCalculate + coverage = atLeast(94) ) } } \ No newline at end of file diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListsTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListsTest.kt index 9fd7c277ce..feb5b8cdc4 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListsTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/ListsTest.kt @@ -5,6 +5,7 @@ import org.utbot.examples.DoNotCalculate import org.utbot.examples.eq import org.utbot.examples.ge import org.utbot.examples.ignoreExecutionsNumber +import org.utbot.examples.between import org.utbot.examples.isException import org.utbot.framework.codegen.CodeGeneration import org.utbot.framework.plugin.api.CodegenLanguage @@ -20,6 +21,16 @@ internal class ListsTest : AbstractTestCaseGeneratorTest( CodeGenerationLanguageLastStage(CodegenLanguage.KOTLIN, CodeGeneration) ) ) { + @Test + fun testBigListFromParameters() { + check( + Lists::bigListFromParameters, + eq(1), + { list, r -> list.size == r && list.size == 11 }, + coverage = DoNotCalculate + ) + } + @Test fun testGetNonEmptyCollection() { check( @@ -104,7 +115,7 @@ internal class ListsTest : AbstractTestCaseGeneratorTest( fun removeElementsTest() { checkWithException( Lists::removeElements, - eq(7), + between(7..8), { list, _, _, r -> list == null && r.isException() }, { list, i, _, r -> list != null && i < 0 && r.isException() }, { list, i, _, r -> list != null && i >= 0 && list.size > i && list[i] == null && r.isException() }, diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/MapValuesTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/MapValuesTest.kt index 22c7166f17..45a78bea1c 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/collections/MapValuesTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/collections/MapValuesTest.kt @@ -92,9 +92,11 @@ class MapValuesTest : AbstractTestCaseGeneratorTest( fun testIteratorNext() { checkWithException( MapValues::iteratorNext, - eq(4), + between(3..4), { map, result -> map == null && result.isException() }, - { map, result -> map != null && map.values.isEmpty() && result.isException() }, + // We might lose this branch depending on the order of the exploration since + // we do not register wrappers, and, therefore, do not try to cover all of their branches + // { map, result -> map != null && map.values.isEmpty() && result.isException() }, { map, result -> map != null && map.values.first() == null && result.isException() }, // as map is LinkedHashmap by default this matcher would be correct { map, result -> map != null && map.values.isNotEmpty() && result.getOrNull() == map.values.first() }, diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/natives/NativeExamplesTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/natives/NativeExamplesTest.kt index 5eacc42259..a99b6a41cc 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/natives/NativeExamplesTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/natives/NativeExamplesTest.kt @@ -5,16 +5,20 @@ import org.utbot.examples.DoNotCalculate import org.utbot.examples.eq import org.utbot.examples.ge import org.junit.jupiter.api.Test +import org.utbot.examples.withSolverTimeoutInMillis internal class NativeExamplesTest : AbstractTestCaseGeneratorTest(testClass = NativeExamples::class) { @Test fun testFindAndPrintSum() { - check( - NativeExamples::findAndPrintSum, - ge(1), - coverage = DoNotCalculate, - ) + // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 + withSolverTimeoutInMillis(5000) { + check( + NativeExamples::findAndPrintSum, + ge(1), + coverage = DoNotCalculate, + ) + } } @Test diff --git a/utbot-framework/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt b/utbot-framework/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt index 4c9283a278..8252d96ce6 100644 --- a/utbot-framework/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt +++ b/utbot-framework/src/test/kotlin/org/utbot/examples/strings/StringExamplesTest.kt @@ -15,6 +15,7 @@ import org.utbot.framework.codegen.CodeGeneration import org.utbot.framework.plugin.api.CodegenLanguage import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.utbot.examples.withSolverTimeoutInMillis internal class StringExamplesTest : AbstractTestCaseGeneratorTest( testClass = StringExamples::class, @@ -25,14 +26,16 @@ internal class StringExamplesTest : AbstractTestCaseGeneratorTest( ) ) { @Test - @Disabled("Sometimes it freezes the execution for several hours JIRA:1453") fun testByteToString() { - check( - StringExamples::byteToString, - eq(2), - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) + // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 + withSolverTimeoutInMillis(5000) { + check( + StringExamples::byteToString, + eq(2), + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) + } } @Test @@ -49,34 +52,43 @@ internal class StringExamplesTest : AbstractTestCaseGeneratorTest( @Test fun testShortToString() { - check( - StringExamples::shortToString, - eq(2), - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) + // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 + withSolverTimeoutInMillis(5000) { + check( + StringExamples::shortToString, + eq(2), + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) + } } @Test fun testIntToString() { - check( - StringExamples::intToString, - ignoreExecutionsNumber, - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) + // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 + withSolverTimeoutInMillis(5000) { + check( + StringExamples::intToString, + ignoreExecutionsNumber, + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) + } } @Test fun testLongToString() { - check( - StringExamples::longToString, - ignoreExecutionsNumber, - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) + // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 + withSolverTimeoutInMillis(5000) { + check( + StringExamples::longToString, + ignoreExecutionsNumber, + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) + } } @Test @@ -104,12 +116,15 @@ internal class StringExamplesTest : AbstractTestCaseGeneratorTest( @Test fun testCharToString() { - check( - StringExamples::charToString, - eq(2), - { a, b, r -> a > b && r == a.toString() }, - { a, b, r -> a <= b && r == b.toString() }, - ) + // TODO related to the https://github.com/UnitTestBot/UTBotJava/issues/131 + withSolverTimeoutInMillis(5000) { + check( + StringExamples::charToString, + eq(2), + { a, b, r -> a > b && r == a.toString() }, + { a, b, r -> a <= b && r == b.toString() }, + ) + } } diff --git a/utbot-sample/src/main/java/org/utbot/examples/arrays/IntArrayBasics.java b/utbot-sample/src/main/java/org/utbot/examples/arrays/IntArrayBasics.java index 5936e71d94..9a95e84200 100644 --- a/utbot-sample/src/main/java/org/utbot/examples/arrays/IntArrayBasics.java +++ b/utbot-sample/src/main/java/org/utbot/examples/arrays/IntArrayBasics.java @@ -1,8 +1,28 @@ package org.utbot.examples.arrays; +import org.utbot.api.mock.UtMock; + import java.util.Arrays; public class IntArrayBasics { + public int[] intArrayWithAssumeOrExecuteConcretely(int x, int n) { + UtMock.assumeOrExecuteConcretely(n > 30); + + if (x > 0) { + if (n < 20) { + return new int[2]; + } else { + return new int[4]; + } + } else { + if (n < 20) { + return new int[10]; + } else { + return new int[20]; + } + } + } + public int[] initAnArray(int n) { int[] a = new int[n]; a[n - 1] = n - 1; diff --git a/utbot-sample/src/main/java/org/utbot/examples/collections/Lists.java b/utbot-sample/src/main/java/org/utbot/examples/collections/Lists.java index d81f3583de..3c66dd0c69 100644 --- a/utbot-sample/src/main/java/org/utbot/examples/collections/Lists.java +++ b/utbot-sample/src/main/java/org/utbot/examples/collections/Lists.java @@ -1,5 +1,7 @@ package org.utbot.examples.collections; +import org.utbot.api.mock.UtMock; + import java.util.ArrayList; import java.util.Collection; import java.util.Iterator; @@ -8,6 +10,11 @@ import java.util.Objects; public class Lists { + int bigListFromParameters(List list) { + UtMock.assume(list != null && list.size() == 11); + + return list.size(); + } Collection getNonEmptyCollection(Collection collection) { if (collection.size() == 0) {