Test gen support string additional options #695

romainbrenguier · 2017-03-24T14:43:23Z

This adds the option --string-max-length to the string solver, this constrains all the strings to be smaller than the maximal length. This shouldn't affect much the performance of the decision procedure but may be necessary for obtaining concrete traces (when the --trace option is activated).

I also added the options --string-non-empty to constrain the nondet strings to have length at least 1 (to avoid obtaining counter-example that concatenates the empty string two times, which is not very interesting), and --string-printable to constrain strings to contain only characters in the range between (space, U+0020) and ~ (tilde, U+007E). making the example nicer than a sequence of null characters.

This also fixes a couple of bugs in the solver.
This corresponds to PR #652 on master

peterschrammel · 2017-03-24T14:46:31Z

src/solvers/refinement/string_refinement.cpp

+\*******************************************************************/
+
+exprt string_refinementt::substitute_array_with_expr
+  (exprt &expr, exprt &index) const


peterschrammel · 2017-03-24T14:47:30Z

src/solvers/refinement/string_refinement.cpp

+{
+  if(expr.id()==ID_with)
+  {
+    with_exprt &with_expr=to_with_expr(expr);


peterschrammel · 2017-03-24T14:47:37Z

src/solvers/refinement/string_refinement.cpp

+\*******************************************************************/
+
+exprt string_refinementt::substitute_array_with_expr
+  (exprt &expr, exprt &index) const


( on previous line

peterschrammel · 2017-03-24T14:49:39Z

src/solvers/refinement/string_refinement.cpp

+
+\*******************************************************************/
+
+exprt string_refinementt::substitute_array_access(exprt &expr) const


peterschrammel · 2017-03-24T14:53:28Z

src/solvers/refinement/string_refinement.cpp

+  {
+    // TODO: only copy when necessary
+    exprt op(expr.operands()[i]);
+    expr.operands()[i]=substitute_array_access(op);


It seems that making substitute_* do an in-place substitution could simplify the code.

for(auto &op : expr.operands()) substitute_array_access(op);

I've made substitute_array_access in-place 14a1138
But I've let substitute_array_with_expr as it is because I think it is simpler in the current state.

peterschrammel · 2017-03-24T14:54:24Z

src/solvers/refinement/string_refinement.cpp

+
+    if(index_expr.array().id()==ID_with)
+    {
+      exprt subst=substitute_array_with_expr(index_expr.array(),


break after (

peterschrammel · 2017-03-24T15:04:39Z

src/solvers/refinement/string_refinement.cpp

+
+    size_t last_index=array_expr.operands().size()-1;
+    assert(last_index>=0);
+    exprt ite=array_expr.operands()[last_index];


This loop would be simpler if you considered the first element as default case of the ite chain. Is there a formula readability argument against this?

The readability would be fine with first element as default, but I don't see why it would make the loop simpler. It would just shift the bounds by 1?

peterschrammel · 2017-03-24T15:10:24Z

src/solvers/refinement/string_constraint_generator.h

@@ -26,9 +26,17 @@ class string_constraint_generatort
  // to the axiom list.

  string_constraint_generatort():
-    mode(ID_unknown)
+    mode(ID_unknown),
+    max_string_length(-1),


What is the meaning of -1 ?

peterschrammel · 2017-03-24T15:20:52Z

src/solvers/refinement/string_refinement.cpp

+Function: string_refinementt::set_max_string_length
+
+  Inputs:
+    i - maximum length which is allowed for strings.


I'd prefer using an unsigned integer and std::numeric_limits::max() as default upper limit. What is "no limit" supposed to mean in your case? What is the relation to MAX_CONCRETE_STRING_SIZE?

peterschrammel · 2017-03-24T15:40:06Z

src/solvers/refinement/string_refinement.cpp

+      found_length[content]=length;
+     }
+  }
+  for(const auto& it : generator.created_strings)


auto &it (several instances)

peterschrammel · 2017-03-28T21:58:53Z

src/cbmc/cbmc_parse_options.h

@@ -37,7 +37,7 @@ class optionst;
  "(no-sat-preprocessor)" \
  "(no-pretty-names)(beautify)" \
  "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
-  "(refine-strings)" \
+  "(refine-strings)(string-non-empty)(string-printable)(string-max-length):" \


I suggest to put each option on a separate line to facilitate merging.

peterschrammel · 2017-03-28T22:01:24Z

src/solvers/refinement/string_refinement.h

@@ -61,10 +61,13 @@ class string_refinementt: public bv_refinementt
  // Base class
  typedef bv_refinementt supert;

-  unsigned initial_loop_bound;
+  unsigned long initial_loop_bound;


Is ulong needed here? It's initialised from uint.

peterschrammel · 2017-03-30T10:01:05Z

Please remove the [string-refine] prefix from commit messages.

peterschrammel · 2017-03-30T10:02:31Z

src/solvers/refinement/string_constraint_generator.h

-    mode=_mode;
-  }
+  // Constraints on the maximal length of strings
+  unsigned long max_string_length;


Why do we need a long here?

This is because length of string in java are 32 bits integer, while int in c++ on some systems could be 16 bits if I'm not mistaken

Yes, minimum size of int is 16 bits. For Java, int32_t would make it independent of the system. For other languages, this might be different. Eg c++ string::max_size() tells me something close to 2^64 on my machine.

peterschrammel · 2017-03-30T10:05:33Z

src/solvers/refinement/string_refinement.cpp

+      ite.type()=char_type;
+    }
+
+    for(long i=last_index-1; i>=0; --i)


As pointed out earlier, this loop is not nice. The mixture of long, unsigned, size_t etc is likely to cause trouble. I dig up my earlier proposal that does without indexing.

Added field in string_refinement and string_constraint_generator to bound size of strings in the program and enforce a range on the characters.

We add the options string-max-length, string-non-empty, and string-printable

This option is no longer requiered because the implementation is now language independent.

Unknown values could cause type problems if we do not force the type for them.

peterschrammel · 2017-04-04T20:59:00Z

Superseded by #738

peterschrammel reviewed Mar 24, 2017

View reviewed changes

peterschrammel reviewed Mar 28, 2017

View reviewed changes

peterschrammel reviewed Mar 30, 2017

View reviewed changes

romainbrenguier added 17 commits March 30, 2017 12:09

Substitute array access by if-then-else expressions

f15ea75

Setting ui for temporary solver

0ef1a1f

Added option to the string solver for string length and printability

4cff10e

Added field in string_refinement and string_constraint_generator to bound size of strings in the program and enforce a range on the characters.

Adding options to cbmc for parameters of the string solver

3a82a7f

We add the options string-max-length, string-non-empty, and string-printable

Remove the mode option from string solver

6bbf1f7

This option is no longer requiered because the implementation is now language independent.

Setting the type for unknown values in substitute_array_access

cd010db

Unknown values could cause type problems if we do not force the type for them.

Adapt add_axioms_for_insert for 5 arguments diffblue#110

4cbc28c

Fixed linting issue in string_constraint_generator_concat.cpp

de60c68

Comment on the maximal length for string

48a92f6

Using max_string_length as the limit for refinement

4b321b6

Using unsigned type for max string length

20450ec

Using const ref in substitute_array_with_expr

a207787

making substitute_array_access do in-place substitution

96cb157

Correcting type of max_string_length and length comparison functions

920695a

space before & sign instead of after

6a6858a

Putting each cbmc option on a separate line for easy merging

cb2fb78

Correcting initial_loop_bound type

6898cca

romainbrenguier force-pushed the test-gen-support-string-additional-options branch from 5066dab to 6898cca Compare March 30, 2017 10:51

allredj mentioned this pull request Mar 30, 2017

Test gen support string additional options 2 #738

Merged

forejtv added the do not merge label Apr 3, 2017

peterschrammel closed this Apr 4, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Test gen support string additional options #695

Test gen support string additional options #695

romainbrenguier commented Mar 24, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

romainbrenguier Mar 26, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

romainbrenguier Mar 26, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 24, 2017

peterschrammel Mar 28, 2017

peterschrammel Mar 28, 2017

peterschrammel commented Mar 30, 2017

peterschrammel Mar 30, 2017

romainbrenguier Mar 30, 2017

peterschrammel Mar 30, 2017

peterschrammel Mar 30, 2017

peterschrammel commented Apr 4, 2017


		\*******************************************************************/

		exprt string_refinementt::substitute_array_access(exprt &expr) const

Test gen support string additional options #695

Test gen support string additional options #695

Conversation

romainbrenguier commented Mar 24, 2017

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Mar 30, 2017

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

peterschrammel commented Apr 4, 2017