Cleaning dependencies of the string solver #549

romainbrenguier · 2017-02-15T14:32:41Z

src/util is a more appropriate place for the string_exprt class, so it was moved there.

We changed the constructor with one type argument to be similar to
other exprt constructors.
This constructor was used to generate a struct with
fresh symbols but this is no longer the case, so we use a function
fresh string instead.

Dependencies in the solver that were not needed have been removed.

For some functions this requires us to now pass the string type as
argument, so the appropriate changes have been made.

tautschnig · 2017-02-15T14:44:21Z

The linter warnings appear to be genuine, would you mind addressing them?

tautschnig · 2017-02-15T14:45:25Z

src/solvers/refinement/refined_string_type.h


 // Internal type used for string refinement
 class refined_string_typet: public struct_typet
 {
 public:
-  explicit refined_string_typet(typet char_type);
+  explicit refined_string_typet(typet index_type, typet char_type);


It's safe to get rid of "explicit" now that this constructor takes 2 arguments.

tautschnig · 2017-02-15T14:47:20Z

src/solvers/refinement/string_constraint_generator.h

-  { }
+    mode(ID_unknown)
+  {
+    next_symbol_id=1;


I'm not entirely sure, but I think this would actually reset the counter. Place the initialisation with the declaration.

tautschnig · 2017-02-15T14:50:03Z

src/solvers/refinement/string_constraint_generator_comparison.cpp

  exprt constr2=character_equals_ignore_case(
    s1[qvar], s2[qvar], char_a, char_A, char_Z);
  string_constraintt a2(qvar, s1.length(), eq, constr2);
  axioms.push_back(a2);

-  symbol_exprt witness=fresh_exist_index("witness_unequal_ignore_case");
-  exprt zero=from_integer(0, get_index_type());
+  // TODO: we should have to give the type of witness


Would you mind elaborating a bit more to enable others to pick up this TODO? Specifically, I don't know who "we" refers to, and what type that would be - it seems it's using index_type - is that not correct?

sorry this shouldn't be there, the call the index_type has been added but the TODO wasn't removed

tautschnig · 2017-02-15T14:53:11Z

src/solvers/refinement/string_constraint_generator_main.cpp

+  return string_exprt(length, content, type);
+}
+
+


Nit picking: one blank line will do

tautschnig · 2017-02-15T14:55:58Z

src/solvers/refinement/string_refinement.cpp

@@ -705,14 +707,14 @@ exprt string_refinementt::sum_over_map(
      switch(second)
      {
      case -1:
-        if(sum==from_integer(0, generator.get_index_type()))
+        if(sum==nil_exprt())


You might want to use if(sum.is_nil())

tautschnig · 2017-02-15T14:56:14Z

src/solvers/refinement/string_refinement.cpp

-  exprt index_const=from_integer(constants, generator.get_index_type());
-  return plus_exprt(sum, index_const);
+  exprt index_const=from_integer(constants, index_type);
+  if(sum!=nil_exprt())


You could use if(sum.is_not_nil())

romainbrenguier · 2017-02-15T14:57:53Z

@tautschnig yes, sorry for these, this is now done

tautschnig · 2017-02-15T14:58:54Z

Thanks a lot for the immediate cleanup - please see my comments for a few more changes to consider.

peterschrammel · 2017-02-15T14:49:40Z

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -229,8 +256,9 @@ string_exprt string_constraint_generatort::find_or_add_string_of_symbol(
  const symbol_exprt &sym)
 {
  irep_idt id=sym.get_identifier();
-  auto entry=symbol_to_string.insert(
-    std::make_pair(id, string_exprt(get_char_type())));
+  refined_string_typet ref_type=to_refined_string_type(sym.type());


peterschrammel · 2017-02-15T14:49:50Z

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -403,15 +430,16 @@ string_exprt string_constraint_generatort::add_axioms_for_copy(
  const function_application_exprt &f)
 {
  string_exprt s1=add_axioms_for_string_expr(args(f, 1)[0]);
-  string_exprt res(get_char_type());
+  refined_string_typet ref_type=to_refined_string_type(s1.type());


const & (and all other instances like this)

peterschrammel · 2017-02-15T14:50:33Z

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -655,7 +638,8 @@ exprt string_constraint_generatort::add_axioms_for_char_at(
  const function_application_exprt &f)
 {
  string_exprt str=add_axioms_for_string_expr(args(f, 2)[0]);
-  symbol_exprt char_sym=string_exprt::fresh_symbol("char", get_char_type());
+  refined_string_typet ref_type=to_refined_string_type(str.type());


peterschrammel · 2017-02-15T14:56:16Z

src/util/string_expr.h

-  // Generate a new symbol of the given type with a prefix
-  static symbol_exprt fresh_symbol(
-    const irep_idt &prefix, const typet &type=bool_typet());
+  string_exprt(exprt _length, exprt _content, typet type): string_exprt(type)


const & (twice, and use copy_to_operands)

peterschrammel · 2017-02-15T14:58:03Z

src/solvers/refinement/string_refinement.cpp

@@ -705,14 +707,14 @@ exprt string_refinementt::sum_over_map(
      switch(second)
      {
      case -1:
-        if(sum==from_integer(0, generator.get_index_type()))
+        if(sum==nil_exprt())


.is_nil() (several instances)

romainbrenguier · 2017-02-15T15:38:27Z

@tautschnig @peterschrammel thanks for the comment, I've now done the corresponding corrections

peterschrammel · 2017-02-17T22:41:41Z

src/solvers/refinement/string_constraint.h

-    exprt s0,
-    exprt s1) :
+    string_exprt s0,
+    string_exprt s1) :


no space before :

peterschrammel · 2017-02-17T22:45:38Z

src/solvers/refinement/string_constraint_generator.h

@@ -73,9 +57,14 @@ class string_constraint_generatort
    return index_exprt(witness.at(c), univ_val);
  }

-  symbol_exprt fresh_exist_index(const irep_idt &prefix);
-  symbol_exprt fresh_univ_index(const irep_idt &prefix);
+  static unsigned next_symbol_id=1;


The initialisation should be in the cpp file.

peterschrammel · 2017-02-17T22:46:22Z

src/util/string_expr.h

-  static irep_idt extract_java_string(const symbol_exprt &s);
-
-  static unsigned next_symbol_id;
-
  friend inline string_exprt &to_string_expr(exprt &expr);
 };




remove one blank line

tautschnig

I would suggest to move the initialisation as indicated in the comment - otherwise this looks ok to me.

tautschnig · 2017-02-20T10:33:48Z

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -17,42 +17,48 @@ Author: Romain Brenguier, [email protected]
 #include <util/pointer_predicates.h>
 #include <util/ssa_expr.h>

+unsigned string_constraint_generatort::next_symbol_id=1;
+


Why is this initialization not done right in the class declaration? I'd rather drop this one instead of the in-class one as you've done in one of your commits.

Personally I don't have a preference, but Peter suggested that the initialisation should be in the cpp file.

You can't initialise a non-const static member in the class definition.

peterschrammel · 2017-02-20T20:55:33Z

src/solvers/refinement/refined_string_type.h


 // Internal type used for string refinement
 class refined_string_typet: public struct_typet
 {
 public:
-  explicit refined_string_typet(typet char_type);
+  refined_string_typet(typet index_type, typet char_type);


const & (twice)

peterschrammel · 2017-02-20T20:58:04Z

src/solvers/refinement/string_constraint.h


  string_not_contains_constraintt(
    exprt univ_lower_bound,
    exprt univ_bound_sup,
    exprt premise,
    exprt exists_bound_inf,
    exprt exists_bound_sup,
-    exprt s0,
-    exprt s1) :
+    string_exprt s0,


const & (twice)

peterschrammel · 2017-02-20T20:58:16Z

src/solvers/refinement/refined_string_type.cpp

@@ -22,11 +22,11 @@ Constructor: refined_string_typet::refined_string_typet

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

-refined_string_typet::refined_string_typet(typet char_type)
+refined_string_typet::refined_string_typet(typet index_type, typet char_type)


const & (twice)

peterschrammel · 2017-02-20T21:00:23Z

src/solvers/refinement/string_constraint_generator_main.cpp

  boolean_symbols.push_back(b);
  return b;
 }

+


remove one blank line

tautschnig · 2017-02-21T10:04:15Z

@peterschrammel It seems all concerns have been addressed. I note that the linter is failing with an internal error rather than reporting any problems in the source files...

forejtv · 2017-02-21T17:45:09Z

@romainbrenguier can you please rebase, to have a fixed linter output?

romainbrenguier · 2017-02-21T22:05:02Z

@forejtv done

peterschrammel · 2017-02-21T22:21:45Z

src/solvers/refinement/string_constraint_generator.h

+
+  static symbol_exprt fresh_symbol(
+    const irep_idt &prefix, const typet &type=bool_typet());
+  symbol_exprt fresh_exist_index(const irep_idt &prefix, typet type);


const typet &type (several occurrences)

romainbrenguier · 2017-02-22T10:08:00Z

@peterschrammel it's now done, should I squash the commits?

peterschrammel · 2017-02-22T10:58:43Z

Yes, the cleanup commits should be squashed

`src/util` is a more appropriate place for the `string_exprt` class We changed the constructor with one type argument to be similar to other `exprt` constructors. This constructor was used to generate a struct with fresh symbols but this is no longer the case, so we use a function fresh string instead. Dependencies in the solver that were not needed have been removed. For some functions this requieres us to now pass the string type as argument.

romainbrenguier · 2017-02-23T08:55:24Z

@peterschrammel commits have been squashed: 3cb7bca

peterschrammel

@kroening, this looks ready to go

…ween_DO_and_EVSes SEC-633: Bugfix: added alias-computation between a DO and EVSes in the domain.

romainbrenguier mentioned this pull request Feb 15, 2017

String refine preprocessing #378

Closed

tautschnig reviewed Feb 15, 2017

View reviewed changes

peterschrammel reviewed Feb 15, 2017

View reviewed changes

romainbrenguier force-pushed the string-refinement-dependencies branch from 0174939 to 6096c5f Compare February 15, 2017 16:05

forejtv assigned tautschnig and peterschrammel Feb 15, 2017

romainbrenguier force-pushed the string-refinement-dependencies branch from 6096c5f to 0628812 Compare February 16, 2017 12:43

peterschrammel requested changes Feb 17, 2017

View reviewed changes

forejtv assigned romainbrenguier and unassigned peterschrammel Feb 18, 2017

romainbrenguier force-pushed the string-refinement-dependencies branch from 4aefd87 to a04f840 Compare February 18, 2017 13:18

tautschnig approved these changes Feb 20, 2017

View reviewed changes

forejtv assigned peterschrammel and unassigned tautschnig and romainbrenguier Feb 20, 2017

peterschrammel requested changes Feb 20, 2017

View reviewed changes

forejtv assigned romainbrenguier and unassigned peterschrammel Feb 20, 2017

romainbrenguier force-pushed the string-refinement-dependencies branch from d9b5714 to c29eed4 Compare February 21, 2017 18:03

peterschrammel reviewed Feb 21, 2017

View reviewed changes

romainbrenguier force-pushed the string-refinement-dependencies branch from f971285 to 0ad726d Compare February 22, 2017 10:06

romainbrenguier force-pushed the string-refinement-dependencies branch from 0ad726d to 3cb7bca Compare February 22, 2017 14:37

peterschrammel approved these changes Feb 23, 2017

View reviewed changes

peterschrammel added the String solver label Feb 23, 2017

peterschrammel assigned kroening and unassigned romainbrenguier Feb 23, 2017

kroening merged commit 37163d8 into diffblue:master Mar 1, 2017

NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this pull request Aug 22, 2018

Merge pull request diffblue#549 from diffblue/bugfix_add_aliasing_bet…

38e6e1f

…ween_DO_and_EVSes SEC-633: Bugfix: added alias-computation between a DO and EVSes in the domain.

Cleaning dependencies of the string solver #549

Cleaning dependencies of the string solver #549

Conversation

romainbrenguier commented Feb 15, 2017

tautschnig commented Feb 15, 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

romainbrenguier commented Feb 15, 2017

tautschnig commented Feb 15, 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

romainbrenguier commented Feb 15, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig 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

tautschnig commented Feb 21, 2017

forejtv commented Feb 21, 2017

romainbrenguier commented Feb 21, 2017

Choose a reason for hiding this comment

romainbrenguier commented Feb 22, 2017

peterschrammel commented Feb 22, 2017

romainbrenguier commented Feb 23, 2017

peterschrammel left a comment

Choose a reason for hiding this comment