TG-58 Complete rework of string solver to avoid using infinite arrays #1420

romainbrenguier · 2017-09-25T07:44:03Z

This makes the string solver algorithm work only on finite size arrays. The input program may have pointers and infinite arrays in which case the solver associate finite arrays to them.
The type for the String class in java-bytecode is changed to contain a char pointer instead of a pointer to an infinite array, however infinite array are still present there for non-deterministic assignment.

smowton

Reviewed about a quarter of this. It's just too big. Don't have time to leaf through the rest; suggest finding another reviewer to pick up where I left off, or find a way to split the huge 3000-line commit in the middle of this into stages so each can be reviewed individually.

smowton · 2017-09-26T10:07:59Z

regression/strings-smoke-tests/java_append_char/test_append_char.java

+    {
+      StringBuilder sb=new StringBuilder("");
+      for(int i=0; i<arr.length; i++)
+	sb.append(arr[i]);


Bad indentation in this function

smowton · 2017-09-26T10:08:54Z

regression/strings-smoke-tests/java_char_array/test_char_array.java

+      char arr[]=new char[s.length()];
+      // We limit arbitrarly the loop unfolding to 5
+      for(int i=0; i<length && i<5; i++)
+	arr[i]=s.charAt(i);


smowton · 2017-09-26T10:09:10Z

regression/strings-smoke-tests/java_if/test.java

@@ -9,8 +9,10 @@ public static String main()
        {
            s.append((String) t[0]);
        }
-        assert(s.toString().equals("Hello world!"));
-        assert(!s.toString().equals("Hello world!"));
+	if(i==0)


smowton · 2017-09-26T10:09:22Z

regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java

      String s = sb.toString();
      System.out.println(s);
-      assert(s.equals("abcd"));
+      if(i==0)
+	assert(s.equals("abcd"));


smowton · 2017-09-26T10:10:09Z

regression/strings/StringMiscellaneous04/StringMiscellaneous04.java

+        // We limit arbitrarly the loop unfolding to 10
+        for(int i=0; i<length && i<10; i++)
+            arr[i]=s.charAt(i);
+	return arr;


smowton · 2017-09-26T13:51:33Z

src/util/string_expr.h

+    operands().resize(2);
+  }
+
+  refined_string_exprt(const exprt &_length, const exprt &_content, typet type):


const typet &?

smowton · 2017-09-26T13:54:24Z

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -234,13 +234,13 @@ exprt string_constraint_generatort::associate_array_to_pointer(
  const auto &length=array_expr.length();
  if(length==infinity_exprt(length.type()))
  {
-    auto ret=length_of_array_.insert(
+    length_of_array_.insert(


If you're expecting this to be a fresh insert, check insert's return value

smowton · 2017-09-26T13:54:33Z

src/solvers/refinement/string_constraint_generator_main.cpp

      std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
    array_expr.length()=length_of_array_[array_expr];
  }

  // TODO should use a function for that
-  auto ret=arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
+  arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));


again, check insert's return value

smowton · 2017-09-26T13:58:29Z

src/java_bytecode/java_object_factory.cpp

@@ -545,11 +545,12 @@ codet initialize_nondet_string_struct(
  code_blockt code;

  // `obj` is `*expr`
-  // const dereference_exprt obj(expr, expr.type().subtype());
-  const irep_idt &class_id=
+  const struct_typet struct_type=


Always follow; take return by const ref

smowton · 2017-09-26T13:59:23Z

unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -33,6 +33,20 @@ TEST_CASE("Generate string object")
  bool failed=symbol_table.add(jlo_sym);
  CHECK_RETURN(!failed);

+
+  // Add java.lang.Object
+  symbolt new_symbol;


You shouldn't need to do this -- jlo is always in the class loader's queue

Not sure we have a class loader here (did you see we are in a unit test?)

jasigal

First pass, I need to better understand more of the string refinement changes to comment on structure.

jasigal · 2017-09-27T12:06:33Z

src/solvers/refinement/string_refinement.cpp

@@ -26,10 +26,34 @@ Author: Alberto Griggio, [email protected]
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <java_bytecode/java_types.h>
+#include <util/optional.h>
+
+#include <util/ssa_expr.h> // for char array pointer


Both of these appear to be unused.

Not sure, there clearly is a usage of optional in the file for example. Question is whether we should start removing headers if they were already included in parent file. Or make some sort of stdafx.h precompiled header file, which would include most commonly used headers (STL utilities, containers, strings, etc.)

I went to go look in CODING_STANDARD.md. It's not completely clear on this type of case, but it does say avoid unnecessary #includes, which they are in the literal sense.

jasigal · 2017-09-27T12:06:54Z

src/solvers/refinement/string_refinement.cpp

+exprt union_find_replacet::add_symbol(const exprt &lhs, const exprt &rhs)
+{
+  const exprt lhs_root=find_expr(lhs);
+  const exprt rhs_root=find_expr(rhs);


const & for both

jasigal · 2017-09-27T12:07:45Z

src/solvers/refinement/string_refinement.cpp

+  return rhs_root;
+}
+
+static std::vector<exprt> instantiate(


Can be deleted, other declaration below.

jasigal · 2017-09-27T12:08:12Z

src/solvers/refinement/string_refinement.cpp

@@ -87,13 +111,18 @@ static exprt instantiate(
  const exprt &val);

 static std::vector<exprt> instantiate(
+  messaget::mstreamt &stream,
+  const namespacet &ns,


Can delete these added args, they are unneeded in the function.

jasigal · 2017-09-27T12:08:37Z

src/solvers/refinement/string_refinement.cpp

@@ -249,327 +280,315 @@ static std::vector<exprt> generate_instantiations(
  for(const auto &nc_axiom : axioms.not_contains)
  {
    for(const auto &instance :
-      instantiate(nc_axiom, index_set, generator))
+      instantiate(stream, ns, nc_axiom, index_set, generator))


Can delete first two args.

jasigal · 2017-09-27T12:30:57Z

src/solvers/refinement/string_refinement.cpp

-      const exprt &i=cur.op1();
-
-      bool has_quant_var=find_qvar(i, qvar);
+      const index_exprt index_expr=to_index_expr(cur);


Can be &.

jasigal · 2017-09-27T12:31:30Z

src/solvers/refinement/string_refinement.cpp

@@ -1712,25 +1802,34 @@ static void initial_index_set(
    to_process.pop_back();


Loop could use expression iterator.

jasigal · 2017-09-27T12:32:02Z

src/solvers/refinement/string_refinement.cpp

 /// \return the lemmas produced through instantiation
 static std::vector<exprt> instantiate(
+  messaget::mstreamt &stream,


~~Quite the opposite.~~

(It wasn't needed.)

jasigal · 2017-09-27T12:32:39Z

src/solvers/refinement/string_refinement.cpp

@@ -1874,15 +1973,22 @@ static exprt instantiate(

 /// Instantiates a quantified formula representing `not_contains` by
 /// substituting the quantifiers and generating axioms.
+/// \param stream: a message stream


Update this by removing unused arguments and updating index_set (and removing current_index set).

jasigal · 2017-09-27T12:33:56Z

src/solvers/refinement/string_refinement.cpp

-        it->second);
-  }
-  else if(ecopy.id()==ID_struct)
+  if(ecopy.type().id()==ID_array)


Should this be all arrays? It used to just be character arrays. For instance, the skolem functions in not contains constraints are arrays. This code seems to assume the arrays are strings.

jasigal · 2017-09-27T13:38:46Z

One thing I think we should address with such a big change to the string refinement process is stop the solver from treating skolem functions as strings. If I run the solver on cbmc/regression/strings-smoke-test/java_contains (so skolem functions from not contains axioms exist), it has its own index set. I have a comment above where any array seems to be treated as a string.

romainbrenguier · 2017-09-28T06:19:13Z

@smowton

or find a way to split the huge 3000-line commit in the middle of this into stages so each can be reviewed individually.

The problem is that it's very difficult to find any significant intermediary stage in this big commit that wouldn't break all the string tests.

jasigal · 2017-09-28T09:18:38Z

src/solvers/refinement/string_refinement.cpp

-        }
+        error() << "dec_solve: current index set is empty, "
+                << "this should not happen" << eom;
+        return resultt::D_ERROR;


@romainbrenguier Changed the behavior of the solver here, probably not on purpose. In a later commit to revert to what was originally there for the most part, but not completely.

jasigal · 2017-09-28T11:25:30Z

src/solvers/refinement/string_refinement.cpp

+      const exprt arr_model=simplify_expr(*arr_model_opt, ns);
+      const exprt concretized_array=concretize_arrays_in_expression(
+        arr_model, generator.max_string_length, ns);
+      debug() << "get " << from_expr(ns, "", expr) << " --> "


I was debugging something with Justing, and this debug output and the one below make this impossible, get is called too often. Please delete.

Remove duplicate code for add_axioms_for_insert_float. Style: indentation in add_axioms_for_insert. Remove useless comment.

Remove unused function: associate_char_array_to_char_pointers. Rename solver in symbol_resolve. Rename function in generate_symbol_resolution_from_eq. Rename function get_char_array_and_concretize. Documentation update for generate_symbol_resolution, add_lemma, substitute_function_application, is_char_type. Some documentation and style fixes.

Debug information for arrays of pointers Debug information for check_axioms steps Refactoring: put debug information out of check_axioms Replace warning by invariant

This is necessary for the negation procedure to know the existential bounds and unfold the quantification as a conjunction.

This is in the case where super_get does not anything about the array we give it. This is necessary so that the string solver returns an array of the correct size, if the size is the only thing we know about the string. Add warning message in the case where the symbol is unknown to super_get

This is done by looking at which arrays were associted to pointers in the generator.

We use this in get to distinguish between strings and arrays of characters

This removes unused functions, declaration of unimplemented function, unused constants and unused fields.

In initialisation of string objects, this prevents the created objects from getting out of scope.

The function what was there before was not correct. It was calling cprover_string_copy which is deprecated.

The check for a specific object number was removed so this does not check what we want anyway. It is difficult to make it check the original intended behaviour using only regular expressions.

This more accurately describe what this object is.

romainbrenguier · 2017-10-29T21:02:29Z

@peterschrammel I squashed a lot of the correction commits with the corresponding original commit, I don't think there is much more to be done. For the cpp linter failure, this is due to a disagreement with what clang-format does for brackets in lamdbas.

romainbrenguier · 2017-10-30T10:30:24Z

@peterschrammel

How come? The function seems misplaced then.

Would java_utils.cpp be appropriate for this?

Add nolint marker on line with lambdas, which are formatted by clang in a way that is not compatible with cpp-lint.

romainbrenguier · 2017-10-31T10:12:26Z

This should be replaced by #1539

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 2 times, most recently from 7148616 to 59fc1bd Compare September 25, 2017 08:02

romainbrenguier requested a review from jasigal September 25, 2017 08:02

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 4 times, most recently from 6371f41 to aca00ce Compare September 25, 2017 10:29

romainbrenguier requested a review from smowton September 25, 2017 11:22

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from 330d8da to 4e6fd78 Compare September 26, 2017 09:43

romainbrenguier changed the title ~~Complete rework of string solver to avoid using infinite arrays~~ TG-58 Complete rework of string solver to avoid using infinite arrays Sep 26, 2017

smowton reviewed Sep 26, 2017

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 4 times, most recently from e63e2e9 to 2bf15cd Compare September 27, 2017 09:38

LAJW force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 2 times, most recently from 1873cf3 to e34064f Compare September 27, 2017 12:21

jasigal suggested changes Sep 27, 2017

View reviewed changes

LAJW force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 3 times, most recently from a7df645 to d8d91e9 Compare September 27, 2017 13:09

LAJW force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch 4 times, most recently from 01e6dd2 to dad57d7 Compare September 27, 2017 14:39

jasigal suggested changes Sep 28, 2017

View reviewed changes

jasigal reviewed Sep 28, 2017

View reviewed changes

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from 2fa3500 to ef9aeaf Compare September 28, 2017 17:36

romainbrenguier added 21 commits October 28, 2017 18:43

Minor code improvements in generator_insert

3d5465e

Remove duplicate code for add_axioms_for_insert_float. Style: indentation in add_axioms_for_insert. Remove useless comment.

String refinement: Improve debug information

145364c

Debug information for arrays of pointers Debug information for check_axioms steps Refactoring: put debug information out of check_axioms Replace warning by invariant

Style fixes in string_constraint_generator.h

92897f7

Simplify not_contains constraints before negation

ca8213f

This is necessary for the negation procedure to know the existential bounds and unfold the quantification as a conjunction.

Distinguish strings and char arrays in get

26e895d

This is done by looking at which arrays were associted to pointers in the generator.

Fix set of created strings in generator and use it

2355e8e

We use this in get to distinguish between strings and arrays of characters

Cleanup unused fields of constraint generator

bb22700

This removes unused functions, declaration of unimplemented function, unused constants and unused fields.

Remove insert_long which duplicates insert_int

73d51fc

Allow index for argument of associate array to pointer

038b476

Remove redundant check in from_int_with_radix

e59349f

Style: rename i in chr_int to avoid clash

ad65847

Splitting is_string and init_string parts of init

daef30f

Use dynamic object instead of tmp_object in init

a2d7811

In initialisation of string objects, this prevents the created objects from getting out of scope.

Add code for String constructor from array

232617c

The function what was there before was not correct. It was calling cprover_string_copy which is deprecated.

Improve tests for StringBuilder.append([C)

90c8495

Remove regression test that is not checking anything

d03b8cc

The check for a specific object number was removed so this does not check what we want anyway. It is difficult to make it check the original intended behaviour using only regular expressions.

Rename first_index in array_expr

5a0d6b4

This more accurately describe what this object is.

Refactoring: simplify and remove unused expression

539ff9f

Refactor: remove m_ prefix from member fields

3ee3b25

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from 27c1f83 to 3ee3b25 Compare October 28, 2017 17:44

romainbrenguier added 2 commits October 30, 2017 10:40

Move make_function_application to java_utils

21b2641

Style: add nolint marker on lines formated by clang

aa94fe8

Add nolint marker on line with lambdas, which are formatted by clang in a way that is not compatible with cpp-lint.

romainbrenguier force-pushed the bugfix/char-array-in-java-strings#TG-58#rebase branch from dfc6942 to aa94fe8 Compare October 30, 2017 16:09

romainbrenguier mentioned this pull request Oct 31, 2017

TG-58 New PR for Complete rework of string solver to avoid using infinite arrays #1539

Merged

peterschrammel merged commit aa94fe8 into diffblue:develop Oct 31, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

TG-58 Complete rework of string solver to avoid using infinite arrays #1420

TG-58 Complete rework of string solver to avoid using infinite arrays #1420

romainbrenguier commented Sep 25, 2017

smowton left a comment

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

smowton Sep 26, 2017

romainbrenguier Sep 26, 2017

jasigal left a comment

jasigal Sep 27, 2017

LAJW Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

LAJW Sep 27, 2017 •

edited

Loading

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal Sep 27, 2017

jasigal commented Sep 27, 2017

romainbrenguier commented Sep 28, 2017

jasigal Sep 28, 2017

jasigal Sep 28, 2017

romainbrenguier commented Oct 29, 2017

romainbrenguier commented Oct 30, 2017

romainbrenguier commented Oct 31, 2017

		@@ -1712,25 +1802,34 @@ static void initial_index_set(
		to_process.pop_back();

TG-58 Complete rework of string solver to avoid using infinite arrays #1420

TG-58 Complete rework of string solver to avoid using infinite arrays #1420

Conversation

romainbrenguier commented Sep 25, 2017

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jasigal left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW Sep 27, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jasigal commented Sep 27, 2017

romainbrenguier commented Sep 28, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

romainbrenguier commented Oct 29, 2017

romainbrenguier commented Oct 30, 2017

romainbrenguier commented Oct 31, 2017

LAJW Sep 27, 2017 •

edited

Loading