Skip to content

String solver: avoid cubic formulas for string-to-int conversions #5226

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test1
--max-nondet-string-length 1000 --function Test1.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test2
--max-nondet-string-length 1000 --function Test2.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test3
--max-nondet-string-length 1000 --function Test3.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 7.* FAILURE$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
Test
--max-nondet-string-length 1000 --function Test.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 10.* SUCCESS$
Expand Down
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
public class Test {

public static void testMe(String input, int radix) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

weird formatting


// Railroad the solver a bit to speed up solving
// (note use of > and < to dodge constant propagation)
if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30)
return;

int value = Integer.parseInt(input, radix);
if(value == 20)
assert false;
else
assert false;

}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
Test
--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 12.* FAILURE$
^\[.*assertion.2\].* line 14.* SUCCESS$
--
non equal types
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test1
--max-nondet-string-length 1000 --function Test1.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test2
--max-nondet-string-length 1000 --function Test2.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test3
--max-nondet-string-length 1000 --function Test3.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test4
--max-nondet-string-length 1000 --function Test4.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test4.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test5
--max-nondet-string-length 1000 --function Test5.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test5.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test6
--max-nondet-string-length 1000 --function Test6.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test6.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test_binary_min
--max-nondet-string-length 1000 --function Test_binary_min.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_binary_min.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test_decimal_max
--max-nondet-string-length 1000 --function Test_decimal_max.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_decimal_max.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test_decimal_min
--max-nondet-string-length 1000 --function Test_decimal_min.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_decimal_min.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 9.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test_hex
--max-nondet-string-length 1000 --function Test_hex.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_hex.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Test_octal
--max-nondet-string-length 1000 --function Test_octal.main
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_octal.main
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 8.* SUCCESS$
Expand Down
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
public class Test {

public static void testMe(String input, int radix) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

weird formatting


// Railroad the solver a bit to speed up solving
// (note use of > and < to dodge constant propagation)
if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30)
return;

long value = Long.parseLong(input, radix);
if(value == 20)
assert false;
else
assert false;

}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
THOROUGH
Test
--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
^\[.*assertion.1\].* line 12.* FAILURE$
^\[.*assertion.2\].* line 14.* SUCCESS$
--
non equal types
18 changes: 6 additions & 12 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1574,6 +1574,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
std::placeholders::_2,
std::placeholders::_3,
std::placeholders::_4);
cprover_equivalent_to_java_function
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
ID_cprover_string_parse_int_func;
cprover_equivalent_to_java_function
["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
ID_cprover_string_parse_int_func;

// String library
conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
Expand Down Expand Up @@ -1819,18 +1825,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
conversion_table["java::java.lang.String.length:()I"];

// Other libraries
cprover_equivalent_to_java_function
["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
ID_cprover_string_parse_int_func;
cprover_equivalent_to_java_function
["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
ID_cprover_string_parse_int_func;
cprover_equivalent_to_java_function
["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
ID_cprover_string_parse_int_func;
cprover_equivalent_to_java_function
["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
ID_cprover_string_parse_int_func;
cprover_equivalent_to_java_string_returning_function
["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
ID_cprover_string_of_int_hex_func;
Expand Down
26 changes: 13 additions & 13 deletions src/solvers/strings/string_constraint_generator_valueof.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -385,7 +385,6 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string(

const equal_exprt starts_with_minus(str[0], from_integer('-', char_type));
const constant_exprt zero_expr = from_integer(0, type);
exprt::operandst digit_constraints;

exprt sum = get_numeric_value_from_character(
str[0], char_type, type, strict_formatting, radix_ul);
Expand All @@ -407,8 +406,7 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string(
// (the first part avoid overflows in the multiplication and the second
// one in the addition of the definition of sum_j)
// For all 1<=size<=max_string_length we add axioms:
// a5 : |res| == size =>
// forall max_string_length-2 <= j < size. no_overflow_j
// a5 : |res| >= size => no_overflow_j (only added when overflow possible)
// a6 : |res| == size && res[0] is a digit for radix =>
// input_int == sum_{size-1}
// a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1}
Expand All @@ -424,31 +422,33 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string(
// a digit, which is `max_string_length - 2` because of the space left for
// a minus sign. That assumes that we were able to identify the radix. If we
// weren't then we check for overflow on every index.
optionalt<exprt> no_overflow;
if(size - 1 >= max_string_length - 2 || radix_ul == 0)
{
const and_exprt no_overflow(
equal_exprt(sum, div_exprt(radix_sum, radix)),
binary_relation_exprt(new_sum, ID_ge, radix_sum));
digit_constraints.push_back(no_overflow);
no_overflow = and_exprt{equal_exprt(sum, div_exprt(radix_sum, radix)),
binary_relation_exprt(new_sum, ID_ge, radix_sum)};
}
sum = new_sum;

const equal_exprt premise =
equal_to(array_pool.get_or_create_length(str), size);
exprt length_expr = array_pool.get_or_create_length(str);

if(!digit_constraints.empty())
if(no_overflow.has_value())
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not have the size - 1 >= max_string_length - 2 || radix_ul == 0 check here and build the no_overflow conjunction inside a5?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AFAICT it wants to assert about the old sum, I'd guess that's why it was this way to begin with.

{
const implies_exprt a5(premise, conjunction(digit_constraints));
const binary_predicate_exprt string_length_ge_size{
length_expr, ID_ge, from_integer(size, length_expr.type())};
const implies_exprt a5(string_length_ge_size, *no_overflow);
constraints.existential.push_back(a5);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the corresponding documentation needs to be updated

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will do

}

const equal_exprt string_length_equals_size = equal_to(length_expr, size);

const implies_exprt a6(
and_exprt(premise, not_exprt(starts_with_minus)),
and_exprt(string_length_equals_size, not_exprt(starts_with_minus)),
equal_exprt(input_int, sum));
constraints.existential.push_back(a6);

const implies_exprt a7(
and_exprt(premise, starts_with_minus),
and_exprt(string_length_equals_size, starts_with_minus),
equal_exprt(input_int, unary_minus_exprt(sum)));
constraints.existential.push_back(a7);
}
Expand Down