Skip to content

Prevent potential string solver failures #4489

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.

Sign up for GitHub

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
tautschnig merged 3 commits into from
Apr 6, 2019
Merged

Prevent potential string solver failures #4489

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
36e579c
Handle nil case in string_refinementt::get
romainbrenguier Apr 5, 2019
9962b7c
Constrain all generated strings to have non-negative length
romainbrenguier Apr 5, 2019
2c2c5ed
Add a test for the string solver
romainbrenguier Apr 5, 2019
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
Binary file modified jbmc/regression/jbmc-strings/StringConcat/Test.class
View file
Open in desktop
Binary file not shown.
11 changes: 11 additions & 0 deletions jbmc/regression/jbmc-strings/StringConcat/Test.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,4 +312,15 @@ public String bufferNonDetLoop5(int cols, int columnWidth, String c, String data
assert(false);
return sb.toString();
}

static boolean fromNonDetArray(String[] argv)
{
String s = argv[0];
String u = s.concat("llo");
if(u.equals("Hello")) {
return true;
}
return false;
}

}
8 changes: 8 additions & 0 deletions jbmc/regression/jbmc-strings/StringConcat/test_string_nondet_array.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
Test.class
--function Test.fromNonDetArray --depth 10000 --unwind 5 --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED
line 318 no uncaught exception: FAILURE
Copy link
Member

@peterschrammel peterschrammel Apr 5, 2019

Choose a reason for hiding this comment

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

Can you check that the right exception is thrown?

Copy link
Contributor Author

@romainbrenguier romainbrenguier Apr 5, 2019

Choose a reason for hiding this comment

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

We could do that, if we didn't use --throw-runtime-exceptions but the failure I observed happened specifically when the option was used so I prefer to keep it. We could look for a particular exception in the trace, but here both NullPointerException and ArrayOutOfBoundsException could be valid counterexample traces.

Copy link
Collaborator

@tautschnig tautschnig Apr 5, 2019

Choose a reason for hiding this comment

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

Those two exceptions could still be matched by a single regular expression?

java.lang.ArrayIndexOutOfBoundsException|java.lang.NullPointerException
22 changes: 16 additions & 6 deletions src/solvers/strings/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -790,6 +790,13 @@ decision_proceduret::resultt string_refinementt::dec_solve()
for(const auto &instance : initial_instances)
add_lemma(instance);

// All generated strings should have non-negative length
for(const auto &string : generator.array_pool.created_strings())
{
add_lemma(binary_relation_exprt{
string.length(), ID_ge, from_integer(0, string.length().type())});
}
Copy link
Contributor

@allredj allredj Apr 5, 2019

Choose a reason for hiding this comment

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

Commit message should be changed to Constrain all generated strings to have non-negative length. I was initially confused because I thought you were excluding 0.

Copy link
Contributor

@allredj allredj Apr 5, 2019

Choose a reason for hiding this comment

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

I'm massively surprised we didn't already have that constraint somewhere though...

Copy link
Contributor Author

@romainbrenguier romainbrenguier Apr 5, 2019

Choose a reason for hiding this comment

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

A similar constraint exists in the goto-program for all non-deterministic strings generated there. But we didn't have it for new strings generated by the solver itself.


while((loop_bound_--) > 0)
{
dependencies.clean_cache();
Expand Down Expand Up @@ -2060,6 +2067,12 @@ exprt string_refinementt::get(const exprt &expr) const
}
const auto array = supert::get(current.get());
const auto index = get(index_expr->index());

// If the underlying solver does not know about the existence of an array,
// it can return nil, which cannot be used in the expression returned here.
if(array.is_nil())
Copy link
Contributor

@allredj allredj Apr 5, 2019

Choose a reason for hiding this comment

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

⛏️ A comment explaining why we do that would be useful (the commit message is good in that sense).

return index_exprt(current, index);

const exprt unknown =
from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type());
if(
Expand All @@ -2070,12 +2083,9 @@ exprt string_refinementt::get(const exprt &expr) const
return sparse_array->to_if_expression(index);
}

INVARIANT(
array.is_nil() || array.id() == ID_symbol ||
array.id() == ID_nondet_symbol,
std::string("apart from symbols, array valuations can be interpreted as "
"sparse arrays, id: ") +
id2string(array.id()));
INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
"Apart from symbols, array valuations can be interpreted as "
"sparse arrays. Array model : " + array.pretty());
return index_exprt(array, index);
}

Expand Down