Skip to content

Commit fee46dc

Browse files
dtimdtim
committed
Code review fixes
1 parent 0ee5aba commit fee46dc

File tree

7 files changed

+109
-153
lines changed

7 files changed

+109
-153
lines changed

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

Lines changed: 28 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -48,37 +48,39 @@ public static byte parseByte(String s, int radix) {
4848

4949
@SuppressWarnings("ConstantConditions")
5050
public static String toString(byte b) {
51-
// condition = b < 0
52-
boolean condition = less(b, (byte) 0);
51+
if (b == -128) {
52+
return "-128";
53+
}
54+
55+
if (b == 0) {
56+
return "0";
57+
}
58+
5359
// assumes are placed here to limit search space of solver
5460
// and reduce time of solving queries with bv2int expressions
5561
assume(b < 128);
56-
assume(b >= -128);
62+
assume(b > -128);
63+
assume(b != 0);
5764

58-
if (b == -128) {
59-
return "-128";
60-
} else {
61-
String prefix = ite(condition, "-", "");
62-
int value = ite(condition, (byte) -b, b);
63-
char[] reversed = new char[3];
64-
int offset = 0;
65-
while (value > 0) {
66-
reversed[offset] = (char) ('0' + value % 10);
67-
value = value / 10;
68-
offset++;
69-
}
65+
// isNegative = b < 0
66+
boolean isNegative = less(b, (byte) 0);
67+
String prefix = ite(isNegative, "-", "");
68+
69+
int value = ite(isNegative, (byte) -b, b);
70+
char[] reversed = new char[3];
71+
int offset = 0;
72+
while (value > 0) {
73+
reversed[offset] = (char) ('0' + (value % 10));
74+
value /= 10;
75+
offset++;
76+
}
7077

71-
if (offset > 0) {
72-
char[] buffer = new char[offset];
73-
int counter = 0;
74-
while (offset > 0) {
75-
offset--;
76-
buffer[counter++] = reversed[offset];
77-
}
78-
return prefix + new String(buffer);
79-
} else {
80-
return "0";
81-
}
78+
char[] buffer = new char[offset];
79+
int counter = 0;
80+
while (offset > 0) {
81+
offset--;
82+
buffer[counter++] = reversed[offset];
8283
}
84+
return prefix + new String(buffer);
8385
}
8486
}

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

Lines changed: 24 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import org.utbot.api.annotation.UtClassMock;
44
import org.utbot.engine.overrides.strings.UtStringBuilder;
55

6+
import static org.utbot.api.mock.UtMock.assume;
67
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
78
import static org.utbot.engine.overrides.UtLogicMock.ite;
89
import static org.utbot.engine.overrides.UtLogicMock.less;
@@ -69,34 +70,39 @@ public static int parseUnsignedInt(String s, int radix) {
6970
}
7071
}
7172

73+
@SuppressWarnings("ConstantConditions")
7274
public static String toString(int i) {
73-
if (i == 0x80000000) { // java.lang.MIN_VALUE
75+
if (i == 0x80000000) { // java.lang.Integer.MIN_VALUE
7476
return "-2147483648";
7577
}
7678

77-
// condition = i < 0
78-
boolean condition = less(i, 0);
79-
// prefix = condition ? "-" : ""
80-
String prefix = ite(condition, "-", "");
81-
int value = ite(condition, -i, i);
79+
if (i == 0) {
80+
return "0";
81+
}
82+
83+
assume(i <= 0x7FFFFFFF); // java.lang.Integer.MAX_VALUE
84+
assume(i > 0x80000000); // java.lang.Integer.MIN_VALUE
85+
assume(i != 0);
86+
87+
// isNegative = i < 0
88+
boolean isNegative = less(i, 0);
89+
String prefix = ite(isNegative, "-", "");
90+
91+
int value = ite(isNegative, -i, i);
8292
char[] reversed = new char[10];
8393
int offset = 0;
8494
while (value > 0) {
85-
reversed[offset] = (char) ('0' + value % 10);
86-
value = value / 10;
95+
reversed[offset] = (char) ('0' + (value % 10));
96+
value /= value;
8797
offset++;
8898
}
8999

90-
if (offset > 0) {
91-
char[] buffer = new char[offset];
92-
int counter = 0;
93-
while (offset > 0) {
94-
offset--;
95-
buffer[counter++] = reversed[offset];
96-
}
97-
return prefix + new String(buffer);
98-
} else {
99-
return "0";
100+
char[] buffer = new char[offset];
101+
int counter = 0;
102+
while (offset > 0) {
103+
offset--;
104+
buffer[counter++] = reversed[offset];
100105
}
106+
return prefix + new String(buffer);
101107
}
102108
}

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

Lines changed: 26 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import org.utbot.api.annotation.UtClassMock;
44
import org.utbot.engine.overrides.strings.UtStringBuilder;
55

6+
import static org.utbot.api.mock.UtMock.assume;
67
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
78
import static org.utbot.engine.overrides.UtLogicMock.ite;
89
import static org.utbot.engine.overrides.UtLogicMock.less;
@@ -69,34 +70,41 @@ public static long parseUnsignedLong(String s, int radix) {
6970
}
7071
}
7172

73+
@SuppressWarnings("ConstantConditions")
7274
public static String toString(long l) {
7375
if (l == 0x8000000000000000L) { // java.lang.Long.MIN_VALUE
7476
return "-9223372036854775808";
7577
}
76-
// condition = l < 0
77-
boolean condition = less(l, 0);
78-
// prefix = condition ? "-" : ""
79-
String prefix = ite(condition, "-", "");
80-
// value = condition ? -l : l
81-
long value = ite(condition, -l, l);
78+
79+
if (l == 0) {
80+
return "0";
81+
}
82+
83+
// assumes are placed here to limit search space of solver
84+
// and reduce time of solving queries with bv2int expressions
85+
assume(l <= 0x7FFFFFFFFFFFFFFFL); // java.lang.Long.MAX_VALUE
86+
assume(l > 0x8000000000000000L); // java.lang.Long.MIN_VALUE
87+
assume(l != 0);
88+
89+
// isNegative = i < 0
90+
boolean isNegative = less(l, 0);
91+
String prefix = ite(isNegative, "-", "");
92+
93+
long value = ite(isNegative, -l, l);
8294
char[] reversed = new char[19];
8395
int offset = 0;
8496
while (value > 0) {
85-
reversed[offset] = (char) ('0' + value % 10);
86-
value = value / 10;
97+
reversed[offset] = (char) ('0' + (value % 10));
98+
value /= value;
8799
offset++;
88100
}
89101

90-
if (offset > 0) {
91-
char[] buffer = new char[offset];
92-
int i = 0;
93-
while (offset > 0) {
94-
offset--;
95-
buffer[i++] = reversed[offset];
96-
}
97-
return prefix + new String(buffer);
98-
} else {
99-
return "0";
102+
char[] buffer = new char[offset];
103+
int counter = 0;
104+
while (offset > 0) {
105+
offset--;
106+
buffer[counter++] = reversed[offset];
100107
}
108+
return prefix + new String(buffer);
101109
}
102110
}

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

Lines changed: 28 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import org.utbot.api.annotation.UtClassMock;
44
import org.utbot.engine.overrides.strings.UtStringBuilder;
55

6+
import static org.utbot.api.mock.UtMock.assume;
67
import static org.utbot.api.mock.UtMock.assumeOrExecuteConcretely;
78
import static org.utbot.engine.overrides.UtLogicMock.ite;
89
import static org.utbot.engine.overrides.UtLogicMock.less;
@@ -43,39 +44,38 @@ public static java.lang.Short parseShort(String s, int radix) {
4344
}
4445
}
4546

47+
@SuppressWarnings("ConstantConditions")
4648
public static String toString(short s) {
47-
// condition = s < 0
48-
boolean condition = less(s, (short) 0);
49+
if (s == -32768)
50+
return "-32768";
51+
if (s == 0)
52+
return "0";
53+
4954
// assumes are placed here to limit search space of solver
5055
// and reduce time of solving queries with bv2int expressions
51-
assumeOrExecuteConcretely(s <= 10000);
52-
assumeOrExecuteConcretely(s >= -10000);
56+
assume(s < 32768);
57+
assume(s > -32768);
58+
assume(s != 0);
5359

54-
if (s == -32768) {
55-
return "-32768";
56-
} else {
57-
// prefix = condition ? "-" : ""
58-
String prefix = ite(condition, "-", "");
59-
int value = ite(condition, (short) -s, s);
60-
char[] reversed = new char[5];
61-
int offset = 0;
62-
while (value > 0) {
63-
reversed[offset] = (char) ('0' + value % 10);
64-
value = value / 10;
65-
offset++;
66-
}
60+
// isNegative = s < 0
61+
boolean isNegative = less(s, (short) 0);
62+
String prefix = ite(isNegative, "-", "");
63+
64+
int value = ite(isNegative, (short) -s, s);
65+
char[] reversed = new char[5];
66+
int offset = 0;
67+
while (value > 0) {
68+
reversed[offset] = (char) ('0' + (value % 10));
69+
value /= value;
70+
offset++;
71+
}
6772

68-
if (offset > 0) {
69-
char[] repr = new char[offset];
70-
int i = 0;
71-
while (offset > 0) {
72-
offset--;
73-
repr[i++] = reversed[offset];
74-
}
75-
return prefix + new String(repr);
76-
} else {
77-
return "0";
78-
}
73+
char[] buffer = new char[offset];
74+
int counter = 0;
75+
while (offset > 0) {
76+
offset--;
77+
buffer[counter++] = reversed[offset];
7978
}
79+
return prefix + new String(buffer);
8080
}
8181
}

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

Lines changed: 2 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -848,71 +848,22 @@ public String replace(CharSequence target, CharSequence replacement) {
848848
return toString().replace(target, replacement);
849849
}
850850

851-
public String[] splitWithLimitImpl(String regex, int limit) {
851+
private String[] splitWithLimitImpl(String regex, int limit) {
852852
return toString().split(regex, limit);
853853
}
854854

855855
public String[] split(String regex, int limit) {
856-
preconditionCheck();
857856
return splitWithLimitImpl(regex, limit);
858857
}
859858

860-
/*
861-
public String[] split(String regex, int limit) {
862-
preconditionCheck();
863-
if (regex == null) {
864-
throw new NullPointerException();
865-
}
866-
if (limit < 0) {
867-
throw new IllegalArgumentException();
868-
}
869-
if (regex.length() == 0) {
870-
int size = limit == 0 ? length + 1 : min(limit, length + 1);
871-
String[] strings = new String[size];
872-
strings[size] = substring(size - 1);
873-
// TODO remove assume
874-
assume(size < 10);
875-
for (int i = 0; i < size - 1; i++) {
876-
strings[i] = Character.toString(value[i]);
877-
}
878-
return strings;
879-
}
880-
assume(regex.length() < 10);
881-
executeConcretely();
882-
return toStringImpl().split(regex, limit);
883-
}
884-
*/
885-
886-
public String[] splitImpl(String regex) {
859+
private String[] splitImpl(String regex) {
887860
return toString().split(regex);
888861
}
889862

890863
public String[] split(String regex) {
891-
preconditionCheck();
892864
return splitImpl(regex);
893865
}
894866

895-
/*
896-
public String[] split(String regex) {
897-
preconditionCheck();
898-
if (regex == null) {
899-
throw new NullPointerException();
900-
}
901-
if (regex.length() == 0) {
902-
String[] strings = new String[length + 1];
903-
strings[length] = "";
904-
// TODO remove assume
905-
assume(length <= 25);
906-
for (int i = 0; i < length; i++) {
907-
strings[i] = Character.toString(value[i]);
908-
}
909-
return strings;
910-
}
911-
executeConcretely();
912-
return toStringImpl().split(regex);
913-
}
914-
*/
915-
916867
public String toLowerCase(Locale locale) {
917868
preconditionCheck();
918869
if (locale == null) {

‎utbot-framework/src/main/kotlin/org/utbot/engine/Extensions.kt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -296,7 +296,6 @@ val UtSort.defaultValue: UtExpression
296296
UtFp32Sort -> mkFloat(0f)
297297
UtFp64Sort -> mkDouble(0.0)
298298
UtBoolSort -> mkBool(false)
299-
// empty string because we want to have a default value of the same sort as the items stored in the strings array
300299
is UtArraySort -> if (itemSort is UtArraySort) nullObjectAddr else mkArrayWithConst(this, itemSort.defaultValue)
301300
else -> nullObjectAddr
302301
}

‎utbot-framework/src/main/kotlin/org/utbot/engine/Strings.kt

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -49,10 +49,6 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) {
4949
overriddenClass.getMethodByName(UtString::matchesImpl.name).subSignature
5050
private val charAtMethodSignature =
5151
overriddenClass.getMethodByName(UtString::charAtImpl.name).subSignature
52-
private val splitWithLimitMethodSignature =
53-
overriddenClass.getMethodByName(UtString::splitWithLimitImpl.name).subSignature
54-
private val splitMethodSignature =
55-
overriddenClass.getMethodByName(UtString::splitImpl.name).subSignature
5652

5753
private fun Traverser.getValueArray(addr: UtAddrExpression) =
5854
getArrayField(addr, overriddenClass, STRING_VALUE)
@@ -72,12 +68,6 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) {
7268
charAtMethodSignature -> {
7369
symbolicCharAtMethodImpl(wrapper, parameters)
7470
}
75-
splitWithLimitMethodSignature -> {
76-
null
77-
}
78-
splitMethodSignature -> {
79-
null
80-
}
8171
else -> {
8272
null
8373
}
@@ -149,7 +139,7 @@ class StringWrapper : BaseOverriddenWrapper(utStringClass.name) {
149139
}
150140

151141
val rgxGen = RgxGen(String(matchingValue))
152-
val matching = (rgxGen.generate())
142+
val matching = rgxGen.generate()
153143
val notMatching = rgxGen.generateNotMatching()
154144

155145
val thisLength = getIntFieldValue(wrapper, STRING_LENGTH)

0 commit comments

Comments
 (0)