Skip to content

Commit 60de996

Browse files
author
Alexey Menshutin
committed
AssumeOrExecuteConcretely instruction support
1 parent e613be5 commit 60de996

27 files changed

Lines changed: 340 additions & 79 deletions

File tree

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

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,14 @@ public static <T> T makeSymbolic(boolean isNullable) {
1313
@SuppressWarnings("unused")
1414
public static void assume(boolean predicate) {
1515
// to use compilers checks, i.e. for possible NPE
16-
if (!predicate) throw new RuntimeException();
16+
if (!predicate) {
17+
throw new RuntimeException();
18+
}
19+
}
20+
21+
@SuppressWarnings("unused")
22+
public static void assumeOrExecuteConcretely(boolean predicate) {
23+
// In oppose to assume, we don't have predicate check here
24+
// to avoid RuntimeException during concrete execution
1725
}
1826
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -283,6 +283,14 @@ object UtSettings {
283283
*/
284284
var enableUnsatCoreCalculationForHardConstraints by getBooleanProperty(false)
285285

286+
/**
287+
* Enable it to process states with unknown solver status
288+
* from the queue to concrete execution.
289+
*
290+
* True by default.
291+
*/
292+
var processUnknownStatesDuringConcreteExecution by getBooleanProperty(true)
293+
286294
override fun toString(): String =
287295
properties
288296
.entries

‎utbot-framework/src/main/java/org/utbot/engine/overrides/Byte.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77

88
import static org.utbot.api.mock.UtMock.assume;
99
import static org.utbot.engine.overrides.UtLogicMock.ite;
10+
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
1011
import static org.utbot.engine.overrides.UtLogicMock.less;
1112
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
1213

@@ -34,7 +35,7 @@ public static byte parseByte(String s, int radix) {
3435
if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) {
3536
throw new NumberFormatException();
3637
}
37-
assume(s.length() <= 10);
38+
assumeOrExecuteConcretely(s.length() <= 10);
3839
// we need two branches to add more options for concrete executor to find both branches
3940
if (s.charAt(0) == '-') {
4041
executeConcretely();

‎utbot-framework/src/main/java/org/utbot/engine/overrides/Integer.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
import org.utbot.engine.overrides.strings.UtString;
66
import org.utbot.engine.overrides.strings.UtStringBuilder;
77

8-
import static org.utbot.api.mock.UtMock.assume;
8+
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
99
import static org.utbot.engine.overrides.UtLogicMock.ite;
1010
import static org.utbot.engine.overrides.UtLogicMock.less;
1111
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
@@ -34,7 +34,7 @@ public static int parseInt(String s, int radix) {
3434
if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) {
3535
throw new NumberFormatException();
3636
}
37-
assume(s.length() <= 10);
37+
assumeOrExecuteConcretely(s.length() <= 10);
3838
// we need two branches to add more options for concrete executor to find both branches
3939
if (s.charAt(0) == '-') {
4040
executeConcretely();
@@ -62,7 +62,7 @@ public static int parseUnsignedInt(String s, int radix) {
6262
if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) {
6363
throw new NumberFormatException();
6464
}
65-
assume(s.length() <= 10);
65+
assumeOrExecuteConcretely(s.length() <= 10);
6666
if (s.charAt(0) == '-') {
6767
throw new NumberFormatException();
6868
} else {
@@ -77,8 +77,8 @@ public static String toString(int i) {
7777
}
7878
// assumes are placed here to limit search space of solver
7979
// and reduce time of solving queries with bv2int expressions
80-
assume(i <= 0x8000);
81-
assume(i >= -0x8000);
80+
assumeOrExecuteConcretely(i <= 0x8000);
81+
assumeOrExecuteConcretely(i >= -0x8000);
8282
// condition = i < 0
8383
boolean condition = less(i, 0);
8484
// prefix = condition ? "-" : ""

‎utbot-framework/src/main/java/org/utbot/engine/overrides/Long.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
import org.utbot.engine.overrides.strings.UtStringBuilder;
77

88
import static org.utbot.api.mock.UtMock.assume;
9+
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
910
import static org.utbot.engine.overrides.UtLogicMock.ite;
1011
import static org.utbot.engine.overrides.UtLogicMock.less;
1112
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
@@ -34,7 +35,7 @@ public static long parseLong(String s, int radix) {
3435
if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) {
3536
throw new NumberFormatException();
3637
}
37-
assume(s.length() <= 10);
38+
assumeOrExecuteConcretely(s.length() <= 10);
3839
// we need two branches to add more options for concrete executor to find both branches
3940
if (s.charAt(0) == '-') {
4041
executeConcretely();
@@ -62,7 +63,7 @@ public static long parseUnsignedLong(String s, int radix) {
6263
if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) {
6364
throw new NumberFormatException();
6465
}
65-
assume(s.length() <= 10);
66+
assumeOrExecuteConcretely(s.length() <= 10);
6667
if (s.charAt(0) == '-') {
6768
throw new NumberFormatException();
6869
} else {
@@ -77,8 +78,8 @@ public static String toString(long l) {
7778
}
7879
// assumes are placed here to limit search space of solver
7980
// and reduce time of solving queries with bv2int expressions
80-
assume(l <= 10000);
81-
assume(l >= 10000);
81+
assumeOrExecuteConcretely(l <= 10000);
82+
assumeOrExecuteConcretely(l >= 10000);
8283
// condition = l < 0
8384
boolean condition = less(l, 0);
8485
// prefix = condition ? "-" : ""

‎utbot-framework/src/main/java/org/utbot/engine/overrides/Short.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
import org.utbot.engine.overrides.strings.UtString;
66
import org.utbot.engine.overrides.strings.UtStringBuilder;
77

8-
import static org.utbot.api.mock.UtMock.assume;
8+
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
99
import static org.utbot.engine.overrides.UtLogicMock.ite;
1010
import static org.utbot.engine.overrides.UtLogicMock.less;
1111
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
@@ -34,7 +34,7 @@ public static java.lang.Short parseShort(String s, int radix) {
3434
if ((s.charAt(0) == '-' || s.charAt(0) == '+') && s.length() == 1) {
3535
throw new NumberFormatException();
3636
}
37-
assume(s.length() <= 10);
37+
assumeOrExecuteConcretely(s.length() <= 10);
3838
// we need two branches to add more options for concrete executor to find both branches
3939
if (s.charAt(0) == '-') {
4040
executeConcretely();
@@ -50,8 +50,8 @@ public static String toString(short s) {
5050
boolean condition = less(s, (short) 0);
5151
// assumes are placed here to limit search space of solver
5252
// and reduce time of solving queries with bv2int expressions
53-
assume(s <= 10000);
54-
assume(s >= 10000);
53+
assumeOrExecuteConcretely(s <= 10000);
54+
assumeOrExecuteConcretely(s >= 10000);
5555
// prefix = condition ? "-" : ""
5656
String prefix = ite(condition, "-", "");
5757
UtStringBuilder sb = new UtStringBuilder(prefix);

‎utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtArrayList.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@
1818
import static org.utbot.api.mock.UtMock.assume;
1919
import static org.utbot.engine.ResolverKt.MAX_LIST_SIZE;
2020
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
21+
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
2122
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
2223
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
2324
import static org.utbot.engine.overrides.UtOverrideMock.visit;
@@ -82,7 +83,8 @@ void preconditionCheck() {
8283

8384
int size = elementData.end;
8485
assume(elementData.begin == 0);
85-
assume(size >= 0 & size <= MAX_LIST_SIZE);
86+
assume(size >= 0);
87+
assumeOrExecuteConcretely(size <= MAX_LIST_SIZE);
8688

8789
visit(this);
8890
}

‎utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashMap.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,12 +100,12 @@ void preconditionCheck() {
100100
parameter(values.touched);
101101
parameter(values.storage);
102102
parameter(keys);
103-
// for some unknown reason parameter(keys.storage) leads to MapValuesTest::testIteratorNext test failure
103+
parameter(keys.storage);
104104

105105
assume(values.size == keys.end);
106106
assume(values.touched.length == keys.end);
107107
doesntThrow();
108-
for (int i = 0; i < keys.end; i++) {
108+
for (int i = keys.begin; i < keys.end; i++) {
109109
K key = keys.get(i);
110110

111111
assume(values.touched[i] == key);

‎utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtHashSet.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ void preconditionCheck() {
7373
doesntThrow();
7474

7575
// check that all elements are distinct.
76-
for (int i = 0; i < elementData.end; i++) {
76+
for (int i = elementData.begin; i < elementData.end; i++) {
7777
E element = elementData.get(i);
7878
parameter(element);
7979
// make element address non-positive

‎utbot-framework/src/main/java/org/utbot/engine/overrides/collections/UtLinkedList.java‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import static org.utbot.engine.ResolverKt.MAX_LIST_SIZE;
2020
import static org.utbot.engine.overrides.UtOverrideMock.alreadyVisited;
2121
import static org.utbot.engine.overrides.UtOverrideMock.executeConcretely;
22+
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
2223
import static org.utbot.engine.overrides.UtOverrideMock.parameter;
2324
import static org.utbot.engine.overrides.UtOverrideMock.visit;
2425

@@ -78,7 +79,8 @@ private void preconditionCheck() {
7879
parameter(elementData);
7980
parameter(elementData.storage);
8081
assume(elementData.begin == 0);
81-
assume(elementData.end >= 0 & elementData.end <= MAX_LIST_SIZE);
82+
assume(elementData.end >= 0);
83+
assumeOrExecuteConcretely(elementData.end <= MAX_LIST_SIZE);
8284

8385
visit(this);
8486
}

0 commit comments

Comments
 (0)