Refactor string_constraint_generatort #2695

romainbrenguier · 2018-08-07T20:26:11Z

The main goal is to extract all the add_axioms functions from the string_constraint_generatort class so that they can be reused from string_builtin_functiont classes. This has also the benefit of making the string_constraint_generatort class much smaller, and what is modified by these function is now clearer through their interface.
(warning: if you review commit by commit, the one before last is quite big)

martin-cs

This PR seems to do what it describes. I don't have a clear enough picture of the design to say whether this is the right thing to do or not.

martin-cs · 2018-08-08T12:06:58Z

src/solvers/refinement/string_constraint_generator.h

-  symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
-
-  symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
-


From a formal point of view, having these being handled the same is a little concerning. I'm guessing this is just a naming artefact rather than something deeper.

tautschnig

Approving of the changes to the README file. For everything else I have to trust that it's right (CI says it currently isn't).

allredj

Looks good. Please see my question about having the string constraint functions returning the constraints. I don't really understand why and how we do that.

allredj · 2018-08-09T14:36:57Z

src/solvers/refinement/string_constraint_generator.h

@@ -116,13 +116,6 @@ class string_constraint_generatort final
  /// Set of strings that have been created by the generator
  const std::set<array_string_exprt> &get_created_strings() const;

-  exprt get_witness_of(


Not sure extracting the witnesses is an improvement. What is the rationale behind that?

Conceptually it's a part of the solver procedure, and it's not part of the constraints. I want to make the distinction clear between what we are solving (string constraints) and how (string refinement).

allredj · 2018-08-09T14:48:27Z

src/solvers/refinement/string_constraint_generator_comparison.cpp

+  exprt char2,
+  exprt char_a,
+  exprt char_A,
+  exprt char_Z)


These should all be const refs.

allredj · 2018-08-09T14:53:12Z

src/solvers/refinement/string_constraint_generator.h

@@ -84,6 +76,15 @@ class array_poolt final
    const typet &char_array_type);
 };

+array_string_exprt
+find(array_poolt &array_pool, const refined_string_exprt &str);


array_pool should probably be const.

A new entry is created if str was not already present, so the pool cannot be const

allredj · 2018-08-09T15:13:10Z

src/solvers/refinement/string_constraint_generator.h

@@ -90,6 +90,18 @@ class array_poolt final
 /// are given as a struct containing a length and pointer to an array.
 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg);

+/// Collection of constraints of different types: existential formulas,
+/// universal formulas, and "not contains" (universal with one alternation).
+struct string_constraintst final


The name choice is not great as it looks very much like string_constraintt and makes it fairly confusing.

agreed, any suggestion?

string_constraint_sett?

How painful would it be to keep this string_constraintst and rename string_constraintt to something else?

Not very, but if we change we should try to make it a definitive choice.
I guess any choice in the regexp: (universal_ | quantified_)? (string | array) _ (property | formula | constraint) t could work

string_constraintt -> universal_string_constraintt would make sense to me.

allredj · 2018-08-09T15:31:44Z

src/solvers/refinement/string_builtin_function.h

-    return generator.add_axioms_for_concat_char(result, input, character);
+    auto pair = generator.add_axioms_for_concat_char(result, input, character);
+    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+    return pair.second;


I don't understand what we're doing here, and that commit introduces a lot of code duplication. What exactly are we doing?

Yes this is a bit boilerplate, I will try to refactor that

I've added commits at the end (the "Move add_axioms_*" ones) which show how the constraints() codes should look like. I haven't done it for concat and insert yet because it requires getting rid of the other usages of these add_axioms functions first.

These are not using private field of the class but only calling public functions.

Since this is only updated when we do array_pool operations it makes sense to move it there.

instead of generator.get_created_strings which does the same thing.

This is just an alias for the default behavior of fresh_symbol

This better seperates the object we are constructing from the tools we are using to construct it and will make it easier to make constraint generation functions static.

This make the role of these functions clearer.

This will be necessary to make the functions static

This makes how the functions interact with the generator clearer, and make it easier to reuse the functions outside of the class and to unit test them.

These methods are now non-member functions.

Some functions that were used for debugging have been remove from string constraint generator. We adapt to that by adding a vector tracking created symbols when the DEBUG flag is active.

The constraints are now added directly by the string_builtin_function objects, so the code can be moved there.

allredj

Passed Diffblue compatibility checks (cbmc commit: a6fe4e1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84271237

romainbrenguier requested review from martin-cs and peterschrammel as code owners August 7, 2018 20:26

romainbrenguier requested a review from LAJW August 7, 2018 20:26

romainbrenguier added do not merge In progress labels Aug 7, 2018

romainbrenguier force-pushed the clean-up/string-constraint-generator branch from 22a8b50 to 6dd98d9 Compare August 8, 2018 06:45

romainbrenguier removed do not merge In progress labels Aug 8, 2018

romainbrenguier force-pushed the clean-up/string-constraint-generator branch from 6dd98d9 to 9b5ca7a Compare August 8, 2018 09:32

martin-cs approved these changes Aug 8, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/string-constraint-generator branch 2 times, most recently from 3826266 to 50d4bd3 Compare August 8, 2018 13:23

romainbrenguier requested review from chrisr-diffblue, kroening, smowton and tautschnig as code owners August 8, 2018 13:23

tautschnig approved these changes Aug 8, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/string-constraint-generator branch from 50d4bd3 to 595e976 Compare August 8, 2018 17:15

romainbrenguier requested a review from allredj August 9, 2018 05:38

romainbrenguier force-pushed the clean-up/string-constraint-generator branch 2 times, most recently from 9e621eb to 1741c6e Compare August 9, 2018 10:04

allredj approved these changes Aug 9, 2018

View reviewed changes

romainbrenguier force-pushed the clean-up/string-constraint-generator branch 2 times, most recently from bb54d77 to cdcb2b5 Compare August 10, 2018 09:13

romainbrenguier force-pushed the clean-up/string-constraint-generator branch 5 times, most recently from 1767acf to a097827 Compare August 29, 2018 10:28

tautschnig assigned romainbrenguier Sep 3, 2018

romainbrenguier added 26 commits September 10, 2018 09:41

Make int_of_hex_char static

90478c2

Make is_high_surrogate and is_low_surrogate static

84c5c6f

Make char_equals_ignore_case, to_integer_or_default static

94e1edc

Extract find and of_argument of array_pool class

838e3ff

These are not using private field of the class but only calling public functions.

Remove unused find function

78d1d36

Move created_strings field to array_pool

da49088

Since this is only updated when we do array_pool operations it makes sense to move it there.

Call array_pool.created_strings() directly

c08aef0

instead of generator.get_created_strings which does the same thing.

Remove use of fresh_boolean

bc35f59

This is just an alias for the default behavior of fresh_symbol

Extract a string_constraintst struct from generator

f1207bf

This better seperates the object we are constructing from the tools we are using to construct it and will make it easier to make constraint generation functions static.

Add a merge function for string_constraints

45c3cef

Make constraint_generation_function return constraints

27d57cc

This make the role of these functions clearer.

Add fresh_symbol argument to add_axioms functions

53e483c

This will be necessary to make the functions static

Make char_array_of_pointer static

c031f3e

Make get_string_expr static

61751d8

Make add_axioms functions static

35f782a

This makes how the functions interact with the generator clearer, and make it easier to reuse the functions outside of the class and to unit test them.

Move method definition to cpp file

72f59da

Remove unused functions

4c2ad43

Adapt unit tests for constraint generator changes

202f7b6

Add missing doxygen argument documentation

348fe5a

Remove constraint_generator qualifier in README

3cd7b10

These methods are now non-member functions.

Adapt debugging function for cleaned-up generator

6687acb

Some functions that were used for debugging have been remove from string constraint generator. We adapt to that by adding a vector tracking created symbols when the DEBUG flag is active.

Move add_axioms_for_concat_char to builtin functions

b24bb05

The constraints are now added directly by the string_builtin_function objects, so the code can be moved there.

Move add_axioms_for_set_char to builtin_functions

2972e46

Add string_to_upper_case_builtin_functiont constructor

7a19c43

Move add_axioms_for_to_lower/upper_case to builtin functions

14a52dc

Clean-up doxygen errors

a6fe4e1

romainbrenguier force-pushed the clean-up/string-constraint-generator branch from cddfd18 to a6fe4e1 Compare September 10, 2018 08:42

allredj reviewed Sep 10, 2018

View reviewed changes

romainbrenguier merged commit ec1844e into diffblue:develop Sep 10, 2018

romainbrenguier deleted the clean-up/string-constraint-generator branch September 10, 2018 13:00

		symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);

		symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);

Refactor string_constraint_generatort #2695

Refactor string_constraint_generatort #2695

Uh oh!

Conversation

romainbrenguier commented Aug 7, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj Aug 10, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

romainbrenguier commented Aug 7, 2018 •

edited

Loading

allredj Aug 10, 2018 •

edited

Loading