From a9ae8af099b471fbec09a1dcce1c4b2b6c3cffdc Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Tue, 4 Oct 2022 17:44:05 +0800
Subject: [PATCH] Remove unsat states from invokes
---
.../utbot/examples/collections/MapsPart1Test.kt | 13 +++++++++++++
.../main/kotlin/org/utbot/engine/Traverser.kt | 10 ++++++++++
.../org/utbot/examples/collections/Maps.java | 16 ++++++++++++++++
3 files changed, 39 insertions(+)
diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt
index 22afa44e9d..80a318fd8a 100644
--- a/utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt
+++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt
@@ -1,5 +1,6 @@
package org.utbot.examples.collections
+import org.junit.jupiter.api.Tag
import org.utbot.tests.infrastructure.UtValueTestCaseChecker
import org.utbot.tests.infrastructure.AtLeast
import org.utbot.tests.infrastructure.DoNotCalculate
@@ -10,6 +11,7 @@ import org.utbot.framework.plugin.api.MockStrategyApi
import org.junit.jupiter.api.Test
import org.utbot.testcheckers.eq
import org.utbot.testcheckers.ge
+import org.utbot.testcheckers.withPushingStateFromPathSelectorForConcrete
import org.utbot.testcheckers.withoutMinimization
import org.utbot.tests.infrastructure.CodeGeneration
@@ -149,6 +151,17 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
)
}
+ @Test
+ @Tag("slow") // it takes about 20 minutes to execute this test
+ fun testMapOperator() {
+ withPushingStateFromPathSelectorForConcrete {
+ check(
+ Maps::mapOperator,
+ ignoreExecutionsNumber
+ )
+ }
+ }
+
@Test
fun testComputeValue() {
check(
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
index 5e8de17a53..28d83e6ce4 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
@@ -46,6 +46,7 @@ import org.utbot.engine.pc.UtPrimitiveSort
import org.utbot.engine.pc.UtShortSort
import org.utbot.engine.pc.UtSolver
import org.utbot.engine.pc.UtSolverStatusSAT
+import org.utbot.engine.pc.UtSolverStatusUNSAT
import org.utbot.engine.pc.UtSubNoOverflowExpression
import org.utbot.engine.pc.UtTrue
import org.utbot.engine.pc.addrEq
@@ -2535,6 +2536,15 @@ class Traverser(
*/
val artificialMethodOverride = overrideInvocation(invocation, target = null)
+ // The problem here is that we might have an unsat current state.
+ // We get states with `SAT` last status only for traversing,
+ // but during the parameters resolving this status might be changed.
+ // It happens inside the `org.utbot.engine.Traverser.initStringLiteral` function.
+ // So, if it happens, we should just drop the state we processing now.
+ if (environment.state.solver.lastStatus is UtSolverStatusUNSAT) {
+ return emptyList()
+ }
+
// If so, return the result of the override
if (artificialMethodOverride.success) {
if (artificialMethodOverride.results.size > 1) {
diff --git a/utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java b/utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java
index 118001e487..5bd4f6882d 100644
--- a/utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java
+++ b/utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java
@@ -1,7 +1,9 @@
package org.utbot.examples.collections;
+import java.util.ArrayList;
import java.util.HashMap;
import java.util.LinkedHashMap;
+import java.util.List;
import java.util.Map;
public class Maps {
@@ -245,4 +247,18 @@ CustomClass removeCustomObject(Map<CustomClass, CustomClass> map, int i) {
return removed;
}
}
+
+ public List<String> mapOperator(Map<String, String> map) {
+ List<String> result = new ArrayList<>();
+ for (Map.Entry<String, String> entry : map.entrySet()) {
+ if (entry.getValue().equals("key")) {
+ result.add(entry.getKey());
+ }
+ }
+ if (result.size() > 1) {
+ return result;
+ } else {
+ return new ArrayList<>(map.values());
+ }
+ }
}