String refine preprocessing #378

romainbrenguier · 2016-12-31T12:33:41Z

Preprocessing of goto-programs for the string refinement.
This pull request includes the changes from ~~#374~~ ~~#549~~(merged) which should be merged before.

smowton

Broadly looks good, three main flavours of change to make:

(1) Some possible factoring in preprocess to consider
(2) Run cpplint.py to find code style problems
(3) Add commentary / function block comments to explain the reasoning behind some of the less-obvious code.

Regarding (3), cpplint.py will demand that you include a full docblock for every one of axioms_for_concat and axioms_for_substring and .... However I suspect if you consult with @forejtv / @peterschrammel they might be willing to accept a docblock for the /family/ of functions rather than lots of tedious repetition.

smowton · 2017-01-16T11:12:26Z

src/goto-programs/string_refine_preprocess.cpp

Unify this with java_bytecode/java_bytecode_convert_method.cpp::tmp_variable

smowton · 2017-01-16T11:17:27Z

src/goto-programs/string_refine_preprocess.cpp

Can you factor these three nearly-identical functions?

smowton · 2017-01-16T11:18:00Z

src/goto-programs/string_refine_preprocess.cpp

Code style -- use cpplint.py

smowton · 2017-01-16T11:19:37Z

src/goto-programs/string_refine_preprocess.cpp

To help people reading generated VCCs, give this a more descriptive name

smowton · 2017-01-16T11:20:34Z

src/goto-programs/string_refine_preprocess.cpp

Again, descriptive name would be good

smowton · 2017-01-16T11:58:40Z

src/solvers/refinement/string_refinement.cpp

Comment on what this function does / what it's purpose is, and consider a more descriptive name

smowton · 2017-01-16T11:59:09Z

src/solvers/refinement/string_refinement.cpp

Comment on what sort of simplification this can do

smowton · 2017-01-16T12:00:35Z

src/solvers/refinement/string_refinement.cpp

What does this do? Subst...itution, I guess? But from what, to what? Looking below, I guess this could be renamed "instantiate_quanfitier" or "substitute_quantifier" or similar? What is f for?

smowton · 2017-01-16T12:01:17Z

src/solvers/refinement/string_refinement.cpp

This comment should make sense in context of a block comment up top, to tell us what 'the element' is, and what it's being added to, and so on

smowton · 2017-01-16T12:05:47Z

src/solvers/refinement/string_refinement.cpp

Explain, here or somewhere else, what's happening here-- will this be called repeatedly to decrement the quantifier towards its lower bound, or is this a one-shot instantiate-with-upper-bound-minus-one?

peterschrammel

I've only looked over the first part of it. My comments apply to the whole PR, though. I'll review again once it has been rebased and cleaned up.

peterschrammel · 2017-02-05T13:42:26Z

src/goto-programs/string_refine_preprocess.cpp

Please do that.

peterschrammel · 2017-02-05T13:45:11Z

src/goto-programs/string_refine_preprocess.cpp

Make it a static class member.
These are candidates to go into a util class at some point.

Actually it is already declared here https://github.com/diffblue/cbmc/blob/master/src/solvers/refinement/refined_string_type.h#L64 so I'm going to use this one for now, but yes it could be moved

peterschrammel · 2017-02-05T14:05:33Z

src/goto-programs/string_refine_preprocess.cpp

peterschrammel · 2017-02-05T14:06:02Z

src/goto-programs/string_refine_preprocess.cpp

function comment block missing

peterschrammel · 2017-02-05T14:06:43Z

src/goto-programs/string_refine_preprocess.cpp

Is here:
https://github.com/diffblue/cbmc/blob/master/src/goto-programs/class_identifier.h

changed this here 918d97a

peterschrammel · 2017-02-05T14:30:19Z

src/goto-programs/string_refine_preprocess.cpp

use a ranged for

peterschrammel · 2017-02-05T14:31:05Z

src/goto-programs/string_refine_preprocess.cpp

use id2string

peterschrammel · 2017-02-05T14:33:08Z

src/goto-programs/string_refine_preprocess.cpp

code commented out? Fix, remove or use #if 0 and explain why

peterschrammel · 2017-02-05T14:33:42Z

src/goto-programs/string_refine_preprocess.cpp

why is this code commented out?

peterschrammel · 2017-02-05T14:35:28Z

src/goto-programs/string_refine_preprocess.cpp

Please do so

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

src/goto-programs/string_refine_preprocess.cpp

Strictly speaking, this is forbidden. This would introduce a dependency of goto-programs on solvers. So, the immediate guess is that string_expr.h should go into util/. However, this contains dependencies to solvers and java_bytecode, which I don't understand why they are needed. In my opinion. string_expr.h should be language-independent and be moved into util/: for this to happen, the includes bv_refinement.h (seems obsolete) and refined_string_type.h must be removed. The function to_refined_string_type should be defined in refined_string_type.h in the style of similar functions in std_expr.h.

Note: Investigating all these unwanted dependencies, I noticed that solvers depends on ansi-c (in qbf and flattening) and also on java_bytecode (in the string solver), which is not "clean". Also, goto-programs has dependencies on ansi-c, which should not be the case if we take the view of a goto-program being language-independent. All this is related to our multi-language facilities requiring some refactoring.

@peterschrammel would you mind opening an issue to track those (undesirable) dependencies? I'm aware of some of them, but as you have done a proper investigation it would be great if you could note down the details of your findings so that we can all work on them. Thanks!!

string_expr.h could be moved to util but we need refined_string_type.h (this is the type of string_exprt, and maybe these should be renamed to make that obvious). To avoid dependencies on java_bytecode and such, some static of methods of refined_string_type should be moved out of this class to more appropriate places.

@peterschrammel do you prefer to have these changes (on string_expr and refined_string_type) in this pull request or should it be a new one?

peterschrammel · 2017-02-10T22:52:35Z

src/goto-programs/string_refine_preprocess.cpp

Consider using #523 (once it has been merged) for adding fresh variables.

peterschrammel · 2017-02-10T22:53:15Z

src/goto-programs/string_refine_preprocess.cpp

cpplint (check whole file)

I didn't get any error from cpplint on this file

peterschrammel · 2017-02-10T22:53:42Z

src/goto-programs/string_refine_preprocess.cpp

assignments (check whole file)

peterschrammel · 2017-02-10T22:53:58Z

src/goto-programs/string_refine_preprocess.cpp

peterschrammel · 2017-02-10T22:55:38Z

src/goto-programs/string_refine_preprocess.cpp

std::size_t

peterschrammel · 2017-02-10T22:56:01Z

src/goto-programs/string_refine_preprocess.cpp

peterschrammel · 2017-02-10T23:09:59Z

Looks much cleaner now. Please squash the commits when finalising.

tautschnig · 2017-02-11T07:14:17Z

src/goto-programs/string_refine_preprocess.cpp

Nit picking: most files place the include of the class-specific header as the last #include (I can't argue this is good or bad).

tautschnig · 2017-02-11T07:14:22Z

src/goto-programs/string_refine_preprocess.cpp

I would suggest to use the facilities from #523 (which implies that #523 should get merged asap).

I added a TODO note there, in case this PR is merged before

It seems some poking and pushing on #523 is required...

tautschnig · 2017-02-11T07:14:26Z

src/goto-programs/string_refine_preprocess.cpp

The use of #' as separator may be dangerous as it is used in the SSA encoding. Code shouldn't be doing this, but may be relying only a single #' to exist...

I used $ instead (8196d90), it seems that's what #523 uses

tautschnig · 2017-02-11T07:14:30Z

src/goto-programs/string_refine_preprocess.cpp

return tmp_symbol.symbol_expr();

tautschnig · 2017-02-11T07:14:33Z

src/goto-programs/string_refine_preprocess.cpp

Hardcoding ID_java looks scary to me. Why does that work? (Though, in fact, it might as well just not matter.)

As mentioned in the next comment, this preprocessing functions are only for Java, so that's why there shouldn't be any problem there.

If this is Java only, shouldn't all the files go in the java_bytecode folder? Language-specific parts should be as clearly separated from generic ones as possible.

From the point of view of dependencies, we need goto-programs but not anything from java_bytecode. If code in java_bytecode is allowed to use things from goto-programs then yes we could move it there, but I'm not sure it's the case. Maybe @peterschrammel has an opinion on this?

How is this code being invoked, i.e., where is the call that says "now let's do string preprocessing"? That might help to understand where it fits best.

Invocation of the preprocessing is not part of this pull request but of this one: #429 (in particular here: https://github.com/diffblue/cbmc/pull/429/files#diff-41db988013f70caad45ce489749c7df6R921)
This is because the original pull request was too big and thus was split into several parts.

Thanks a lot for the pointer (I was aware it had been split out, but couldn't find it on the spot)! This certainly suggests that goto-programs is the right place, and that one should rather think about how to make this extensible to other languages? (Which does not imply any request to do so right away, but just bringing up the thought and possibly placing some TODO notes.)

tautschnig · 2017-02-11T07:15:38Z

src/goto-programs/string_refine_preprocess.cpp

The explicit use of irep_idt should not be necessary.

tautschnig · 2017-02-11T07:16:28Z

src/goto-programs/string_refine_preprocess.cpp

With C++11 you should be able to initialize that map using { { id, value}, {id, value} , ... } as a more concise syntax.

It seems like it works for maps but not unordered maps

tautschnig · 2017-02-11T07:16:38Z

src/goto-programs/string_refine_preprocess.h

Shouldn't that be a std::unordered_map?

tautschnig · 2017-02-11T07:16:43Z

src/goto-programs/string_refine_preprocess.h

Likely these should be std::unordered_map as well

tautschnig · 2017-02-11T07:16:45Z

src/goto-programs/string_refine_preprocess.h

As above: std::unordered_map

romainbrenguier · 2017-02-15T14:49:55Z

I squashed the commits, but this now depends on #549 which moves string_exprt to util

peterschrammel · 2017-03-09T18:59:32Z

src/goto-programs/string_refine_preprocess.cpp

+  const std::string &signature)
+{
+  if(function_name==ID_cprover_string_copy_func)
+    make_string_copy(goto_program, i_it, lhs, arguments[0], location);


are sure there is an argument?

peterschrammel · 2017-03-09T19:00:46Z

src/goto-programs/string_refine_preprocess.cpp

+  goto_programt::targett &i_it,
+  const std::list<code_assignt> &va)
+{
+  auto i=va.begin();


are you sure the list is not empty?

tautschnig · 2017-03-10T19:05:16Z

src/goto-programs/string_refine_preprocess.cpp

It seems some poking and pushing on #523 is required...

tautschnig · 2017-03-10T19:05:24Z

src/goto-programs/string_refine_preprocess.cpp

If this is Java only, shouldn't all the files go in the java_bytecode folder? Language-specific parts should be as clearly separated from generic ones as possible.

tautschnig · 2017-03-10T19:05:48Z

src/goto-programs/string_refine_preprocess.cpp

+    if(i_it->is_function_call())
+    {
+      code_function_callt &function_call=to_code_function_call(i_it->code);
+      for(auto arg : function_call.arguments())


const auto &arg

this particular one cannot be made const as we modify it

Oh, I'm sorry, but not knowing the precise rules for auto just yet: are you sure you end up with a reference and not with a copy? In the latter case you can obviously modify it, but it won't have much of an effect... I'd suggest auto &arg to be on the safe side.

tautschnig · 2017-03-10T19:05:54Z

src/goto-programs/string_refine_preprocess.cpp

+  assert(is_java_string_type(expr.type()) ||
+         is_java_string_builder_type(expr.type()));
+  typet object_type=ns.follow(expr.type());
+  assert(object_type.id()==ID_struct);


This assertion is covered by the subsequent to_struct_type

tautschnig · 2017-03-10T19:05:56Z

src/goto-programs/string_refine_preprocess.cpp

+  typet object_type=ns.follow(expr.type());
+  assert(object_type.id()==ID_struct);
+  const struct_typet &struct_type=to_struct_type(object_type);
+  for(auto component : struct_type.components())


const auto &component

tautschnig · 2017-03-10T19:06:00Z

src/goto-programs/string_refine_preprocess.cpp

+
+exprt string_refine_preprocesst::make_cprover_string_assign(
+  goto_programt &goto_program,
+  goto_programt::targett &i_it,


Would it be possible to find a more descriptive name for this parameter?

tautschnig · 2017-03-10T19:06:02Z

src/goto-programs/string_refine_preprocess.cpp

+  i_it->code=*i;
+  for(i++; i!=va.end(); i++)
+  {
+    i_it=goto_program.insert_after(i_it);


neither source_location nor function is properly set for these newly inserted instructions

tautschnig · 2017-03-10T19:06:04Z

src/goto-programs/string_refine_preprocess.cpp

+
+  if(object_size.is_nil())
+    debug() << "string_refine_preprocesst::make_string_assign "
+            << "got nil object_size" << eom;


Is it nevertheless ok to continue?

tautschnig · 2017-03-14T15:18:59Z

From my point of view #523 is the main blocker here. (Actually, the only one, for me.)

romainbrenguier · 2017-03-15T16:51:26Z

Now that #523 is merged, I rebased and used this function to declare fresh array and strings. See the commit f14f165

tautschnig · 2017-03-15T17:20:00Z

src/util/std_expr.h

Please add // NOLINT(runtime/explicit) to this line to silence the linter on this invocation of the constructor from the two-parameter one.

peterschrammel

This looks ready to go after some minor polishing

peterschrammel · 2017-03-16T08:12:13Z

src/goto-programs/string_refine_preprocess.cpp

peterschrammel · 2017-03-16T08:13:14Z

src/goto-programs/string_refine_preprocess.cpp

assert !arguments().empty()

peterschrammel · 2017-03-16T08:14:01Z

src/goto-programs/string_refine_preprocess.cpp

assert !arguments().empty()

peterschrammel · 2017-03-16T08:14:11Z

src/goto-programs/string_refine_preprocess.cpp

assert !arguments().empty()

peterschrammel · 2017-03-16T08:17:03Z

src/goto-programs/string_refine_preprocess.cpp

peterschrammel · 2017-03-16T08:17:36Z

src/goto-programs/string_refine_preprocess.cpp

assert !arguments().empty()

peterschrammel · 2017-03-16T08:19:21Z

src/goto-programs/string_refine_preprocess.cpp

return on next line

peterschrammel · 2017-03-16T08:20:52Z

src/goto-programs/string_refine_preprocess.cpp

could use const & here

peterschrammel · 2017-03-16T08:21:19Z

src/goto-programs/string_refine_preprocess.cpp

could use const & here

peterschrammel · 2017-03-16T08:21:30Z

src/goto-programs/string_refine_preprocess.cpp

could use const & here

This avoid dependencies between goto-programs and solver. We also removed function is_unrefined_string_type which should not be needed in the string solver. Removed also mention of java string types and unrefined types in the solver. These mentions should not be necessary, since we are not supposed to do anything java specific. The solver should only have to deal with refined string types and possibly char arrays.

This is a more appropriate location for this module since it's used both in the preprocessing of goto-programs and the string solver.

Refined string type should be used instead as we are trying to be language independent.

peterschrammel

Looks good to me now.

kroening · 2017-04-04T12:23:54Z

Why did refined_string_type.h move into util/?

romainbrenguier · 2017-04-06T14:33:38Z

@kroening the refined_string_typet class is used both in the preprocessing of goto-program and the string-solver when the --refine-strings option is activated. Moving it to util avoids dependencies between goto-programs and solvers

romainbrenguier · 2017-06-28T16:53:31Z

I'm closing this PR which is obsolete compared to what is in the test-gen-support branch

romainbrenguier mentioned this pull request Dec 31, 2016

String solver #341

Closed

peterschrammel requested a review from smowton January 12, 2017 12:39

romainbrenguier mentioned this pull request Jan 12, 2017

String refine option #429

Closed

smowton suggested changes Jan 16, 2017

View reviewed changes

romainbrenguier force-pushed the string-refine-preprocessing branch 2 times, most recently from 9b1e639 to f5a6cfd Compare January 17, 2017 10:52

romainbrenguier force-pushed the string-refine-preprocessing branch 6 times, most recently from 0625ef1 to b69129b Compare February 2, 2017 10:34

romainbrenguier force-pushed the string-refine-preprocessing branch from b69129b to ff66780 Compare February 2, 2017 15:18

peterschrammel added the String solver label Feb 2, 2017

romainbrenguier force-pushed the string-refine-preprocessing branch from 4c26c59 to 2cd801d Compare February 3, 2017 09:09

peterschrammel requested changes Feb 5, 2017

View reviewed changes

romainbrenguier force-pushed the string-refine-preprocessing branch 6 times, most recently from 334ac5f to 3fd299a Compare February 10, 2017 12:51

peterschrammel reviewed Feb 10, 2017

View reviewed changes

tautschnig requested changes Feb 11, 2017

View reviewed changes

tautschnig assigned romainbrenguier Feb 13, 2017

romainbrenguier force-pushed the string-refine-preprocessing branch 3 times, most recently from 3af4fb8 to d35d9ca Compare February 15, 2017 14:48

forejtv unassigned romainbrenguier Mar 6, 2017

peterschrammel reviewed Mar 9, 2017

View reviewed changes

tautschnig reviewed Mar 10, 2017

View reviewed changes

romainbrenguier force-pushed the string-refine-preprocessing branch from 7aea419 to f14f165 Compare March 15, 2017 16:44

tautschnig requested changes Mar 15, 2017

View reviewed changes

peterschrammel requested changes Mar 16, 2017

View reviewed changes

allredj mentioned this pull request Mar 16, 2017

Corrections to the string solver - 2 #646

Closed

romainbrenguier force-pushed the string-refine-preprocessing branch from c404cd1 to ff69281 Compare March 17, 2017 17:26

romainbrenguier added 5 commits March 17, 2017 22:37

Preprocessing of goto programs for string refinement

1aede78

Moving refined_string_type to util

70af9ce

This is a more appropriate location for this module since it's used both in the preprocessing of goto-programs and the string solver.

Removed distinction between c string type and refined string type

2929d7f

Removed mention of c string type

5cb0e5e

Refined string type should be used instead as we are trying to be language independent.

romainbrenguier force-pushed the string-refine-preprocessing branch from ff69281 to 5cb0e5e Compare March 17, 2017 22:41

peterschrammel approved these changes Mar 18, 2017

View reviewed changes

peterschrammel assigned kroening and unassigned peterschrammel Mar 18, 2017

tautschnig approved these changes Mar 20, 2017

View reviewed changes

tautschnig removed their assignment Mar 20, 2017

peterschrammel mentioned this pull request Mar 21, 2017

String refine preprocessing #669

Merged

romainbrenguier added the do not merge label Jun 20, 2017

peterschrammel unassigned kroening Jun 25, 2017

romainbrenguier closed this Jun 28, 2017

String refine preprocessing #378

String refine preprocessing #378

Uh oh!

Conversation

romainbrenguier commented Dec 31, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

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!

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!

peterschrammel commented Feb 10, 2017

romainbrenguier commented Dec 31, 2016 •

edited

Loading