Cleanup in string preprocessing #3189

romainbrenguier · 2018-10-16T15:35:26Z

This is based on #2374
The goal is to ensure location is set for each created symbol.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their

allredj

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

smowton

Looks good, one thing to check re: get-fresh-java-symbol, and also please check you intended to include a models lib bump in this PR

smowton · 2018-10-17T12:20:43Z

jbmc/src/java_bytecode/java_utils.cpp

+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table)
+{
+  const std::string name_prefix = id2string(source_location.get_function());


Check you got a real source loc in this case (or handle the no-source-loc case somehow)

I believe @peterschrammel has comment on this (or a similar case) elsewhere: this seems actually wrong, instead the internal identifier of the function should be passed in.

Yes the conversation was on #2374, I will copy it here so that it doesn't get lost now that 2374 is closed, and address it when I have time to get back to this PR.

tautschnig 13 days ago Collaborator
I strongly believe that the information in the source_location is a string aimed at the user, and should relate to whatever is found in the source. The actual identifier of the function (the key in goto_functionst::function_map) used internally may be entirely different. I don't know which one is required here.

peterschrammel 13 days ago Member
Here, something is required that is unique to a goto function. Reason: adding a function to a goto model must not affect the identifiers of another function. This was the source of many goto-diff bugs in the past.

tautschnig 13 days ago Collaborator
Then a function_id must be passed in. In some call sites in this PR this would be symbol.name, others require further digging.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 8de539f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99921522

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 6997a76).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100205172

Add const keyword at the declaration of variables that will not get modified. In some case, we inline them instead to avoid declaration, when declaration doesn't add value. In other cases, we don't make the variable const but use move where it is used. fixup! Add missing const's

This is in preparation to giving the function_id to the function generating fresh java symbols.

This is in preparation for giving function_id as an argument to the function creating fresh java symbols.

This is in preparation for adding the function_id to the function generating fresh java symbols.

This is in preparation for giving the function name to the function generating fresh java symbols.

This is in preparation to giving the function_id to the function generating fresh java symbols.

This function is not used, there is no point in keeping it.

This is not used

This is in preparation to giving the function_id to the function generating fresh java symbols.

This is in preparation for using a new fresh_java_symbol function which takes a function_id as parameter.

This is in preparation to giving the function_id to the function generating fresh java symbols.

This prevents forgetting that the basename of the symbol should be the function identifier.

No functional changes.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e81e174).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100241422

romainbrenguier · 2019-02-08T15:09:58Z

@tautschnig I got rid of all the get_function calls

tautschnig

Thanks a lot for the large-scale cleanup and updates!

romainbrenguier added the In progress label Oct 16, 2018

romainbrenguier requested review from cesaro, chrisr-diffblue, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners October 16, 2018 15:35

romainbrenguier mentioned this pull request Oct 16, 2018

Cleanup in string preprocessing #2374

Merged

allredj reviewed Oct 16, 2018

View reviewed changes

smowton approved these changes Oct 17, 2018

View reviewed changes

tautschnig assigned romainbrenguier Oct 20, 2018

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch 5 times, most recently from 3fbce70 to 23e5054 Compare November 16, 2018 10:37

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch from 23e5054 to 293ec8e Compare November 16, 2018 11:45

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch 8 times, most recently from cad1a55 to d917737 Compare February 6, 2019 09:35

allredj reviewed Feb 6, 2019

View reviewed changes

tautschnig assigned romainbrenguier Feb 6, 2019

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch 5 times, most recently from 7c08bc0 to 6997a76 Compare February 8, 2019 07:55

allredj reviewed Feb 8, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch 2 times, most recently from f6d19c1 to 5d88421 Compare February 8, 2019 12:36

romainbrenguier added 9 commits February 8, 2019 12:56

Add function_id parameter to convert_exprt_to_string_exprt

8b791e1

This is in preparation to giving the function_id to the function generating fresh java symbols.

Add function_id parameter to decl_string_expr

5d13ed0

This is in preparation for giving function_id as an argument to the function creating fresh java symbols.

Add function_id parameter to process_operands

36c7b6c

This is in preparation for adding the function_id to the function generating fresh java symbols.

Add function_id parameter to replace_char_array

276e534

This is in preparation for giving the function name to the function generating fresh java symbols.

Add function_id parameter to add_pointer_to_array_association

2189e40

This is in preparation for giving the function name to the function generating fresh java symbols.

Add function_id parameter to add_array_to_length_association

8c15acd

This is in preparation to giving the function_id to the function generating fresh java symbols.

Delete unused function fresh_array

0180b8b

This function is not used, there is no point in keeping it.

Delete unused function process_operands

afb691d

This is not used

Add function_id parameter to fresh_string

d3f768c

This is in preparation to giving the function_id to the function generating fresh java symbols.

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch from 5d88421 to e3a18bd Compare February 8, 2019 12:57

romainbrenguier added 4 commits February 8, 2019 13:39

Add function_id parameter to add_character_set_constraint

06f89d9

This is in preparation for using a new fresh_java_symbol function which takes a function_id as parameter.

Add function_id parameter to get_primitive_value_of_object

b4e146a

This is in preparation to giving the function_id to the function generating fresh java symbols.

Add and use fresh_java_symbol function

3edbc74

This prevents forgetting that the basename of the symbol should be the function identifier.

Apply clang-format suggestions

e81e174

No functional changes.

romainbrenguier force-pushed the clean-up/preprocessing-part2 branch from e3a18bd to e81e174 Compare February 8, 2019 13:41

allredj reviewed Feb 8, 2019

View reviewed changes

tautschnig approved these changes Feb 8, 2019

View reviewed changes

tautschnig merged commit 4bb7393 into diffblue:develop Feb 8, 2019

romainbrenguier deleted the clean-up/preprocessing-part2 branch February 11, 2019 07:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Cleanup in string preprocessing #3189

Cleanup in string preprocessing #3189

Uh oh!

romainbrenguier commented Oct 16, 2018

Uh oh!

allredj left a comment

Uh oh!

smowton left a comment

Uh oh!

smowton Oct 17, 2018

Uh oh!

tautschnig Oct 17, 2018

Uh oh!

romainbrenguier Oct 22, 2018

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

romainbrenguier commented Feb 8, 2019

Uh oh!

tautschnig left a comment

Uh oh!

Uh oh!

Cleanup in string preprocessing #3189

Cleanup in string preprocessing #3189

Uh oh!

Conversation

romainbrenguier commented Oct 16, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Oct 17, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 17, 2018

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Oct 22, 2018

Choose a reason for hiding this comment

Uh oh!

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

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Feb 8, 2019

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!