AssumeOrExecuteConcretely instruction support (#64)

Author: CaelmBleidd

utbot-api/src/main/java/org/utbot/api/mock/UtMock.java

@@ -13,6 +13,14 @@ public static <T> 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
     }
 }

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

@@ -286,6 +286,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)
+
     override fun toString(): String =
         properties
             .entries

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();

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 ? "-" : ""

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 ? "-" : ""

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);

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);
     }

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);

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

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);
     }