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

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

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

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

Nit picking: one blank line will do

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

src/solvers/refinement/string_refinement.cpp

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

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

src/solvers/refinement/string_refinement.cpp

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

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

src/solvers/refinement/string_constraint_generator_main.cpp

const & (and all other instances like this)

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

src/solvers/refinement/string_constraint_generator_main.cpp

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

src/util/string_expr.h

const & (twice, and use copy_to_operands)

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

src/solvers/refinement/string_refinement.cpp

.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

no space before :

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

src/solvers/refinement/string_constraint_generator.h

The initialisation should be in the cpp file.

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

src/util/string_expr.h

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

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

const & (twice)

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

src/solvers/refinement/string_constraint.h

const & (twice)

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

src/solvers/refinement/refined_string_type.cpp

const & (twice)

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

src/solvers/refinement/string_constraint_generator_main.cpp

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

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

src/solvers/refinement/string_constraint_generator.h Outdated

Copy link

Member

peterschrammel Feb 21, 2017

Choose a reason for hiding this comment

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

const typet &type (several occurrences)

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

Uh oh!

Conversation

romainbrenguier commented Feb 15, 2017

Uh oh!

tautschnig commented Feb 15, 2017

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!

romainbrenguier commented Feb 15, 2017

Uh oh!

tautschnig commented Feb 15, 2017

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!

romainbrenguier commented Feb 15, 2017

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!

tautschnig 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!

tautschnig commented Feb 21, 2017

Uh oh!

forejtv commented Feb 21, 2017

Uh oh!

romainbrenguier commented Feb 21, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Feb 22, 2017

Uh oh!

peterschrammel commented Feb 22, 2017

Uh oh!

romainbrenguier commented Feb 23, 2017

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees