Skip to content

Construct array_exprt in a non-deprecated way [blocks: #3768] #3771

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Jan 21, 2019
Merged

Construct array_exprt in a non-deprecated way [blocks: #3768] #3771

merged 1 commit into from
Jan 21, 2019

Conversation

tautschnig
Copy link
Collaborator

The existing array_exprt constructor relies on other deprecated constructors;
instead introduce a non-deprecated one and use it across the codebase.

  • 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.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • 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).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig force-pushed the deprecation-array_exprt branch from 6e047a8 to 8f46d4b Compare January 12, 2019 18:45
allredj
allredj reviewed Jan 12, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 6e047a8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97138270
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj
allredj reviewed Jan 12, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

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

@tautschnig tautschnig force-pushed the deprecation-array_exprt branch from 8f46d4b to eedd686 Compare January 14, 2019 16:20
smowton
smowton reviewed Jan 14, 2019
View reviewed changes
jbmc/src/java_bytecode/java_bytecode_parser.cpp
}
return std::move(values);
return array_exprt(std::move(values), array_typet(typet(), exprt()));
Copy link
Contributor

Choose a reason for hiding this comment

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

Not sure about this one -- somehow an empty array with a correct type (seen many times below) seems considerably safer than this partially-constructed thing. If we're going to partially construct something, we should probably use a constructor with that express purpose, rather than pretending we're doing it safely?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The language front-ends will always remain a bit weird. I'm not sure what the best option is - we could also do exprt values(ID_array); to make very clear we are not building anything like a complete expression here.

allredj
allredj reviewed Jan 14, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

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

romainbrenguier
romainbrenguier approved these changes Jan 15, 2019
View reviewed changes
jbmc/src/java_bytecode/character_refine_preprocess.cpp Outdated
case1.copy_to_operands(low_surrogate);
case2.move_to_operands(low_surrogate);
array_exprt case1({low_surrogate}, array_type);
array_exprt case2({std::move(low_surrogate)}, array_type);
exprt high_surrogate=expr_of_high_surrogate(chr, char_type);
case2.move_to_operands(high_surrogate);
Copy link
Contributor

Choose a reason for hiding this comment

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

It maybe better to fully construct case2 in one step, and declare both cases const

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Makes sense, just in a race of whether I get this one or #3691 (getting rid of move_to_operands) approved first.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

That's now all done.

src/util/expr_initializer.cpp
@@ -122,7 +122,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
{
// we initialize this with an empty array

array_exprt value(array_type);
array_exprt value({}, array_type);
value.type().id(ID_array);
Copy link
Contributor

Choose a reason for hiding this comment

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

I don't see why this is necessary

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We could arguably make the no-operands-constructor non-deprecated. Would that seem better?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

So I'm still in two minds about this. I see the following options:

  1. De-deprecate the no-operands-constructor so that such a change isn't necessary. Reduces the amount of noise in this PR.
  2. Require the above syntax. Adds some noise, but has the following advantages: a) smaller API as fewer constructors are provided and b) encouraging efficient bottom-up construction.

Comments would be appreciated.

src/util/std_expr.h
array_exprt(operandst &&_operands, const array_typet &_type)
: multi_ary_exprt(ID_array, std::move(_operands), _type)
{
}
Copy link
Contributor

Choose a reason for hiding this comment

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

This could have been a separate first commit

@tautschnig
Construct array_exprt in a non-deprecated way
475a7b9 
The existing array_exprt constructor relies on other deprecated constructors;
instead introduce a non-deprecated one and use it across the codebase.
@tautschnig tautschnig force-pushed the deprecation-array_exprt branch from eedd686 to 475a7b9 Compare January 21, 2019 10:18
@tautschnig tautschnig changed the title Construct array_exprt in a non-deprecated way Construct array_exprt in a non-deprecated way [blocks: #3768] Jan 21, 2019
allredj
allredj reviewed Jan 21, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

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

smowton
smowton approved these changes Jan 21, 2019
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

Never mind the partial construction question, it's definitely better this way than at present

@tautschnig tautschnig merged commit bafd7e7 into diffblue:develop Jan 21, 2019
@tautschnig tautschnig deleted the deprecation-array_exprt branch January 21, 2019 13:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@kroening kroening kroening approved these changes

@romainbrenguier romainbrenguier romainbrenguier approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@cristina-david cristina-david Awaiting requested review from cristina-david

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@thk123 thk123 Awaiting requested review from thk123

Assignees

@smowton smowton

@peterschrammel peterschrammel

@romainbrenguier romainbrenguier

Labels
blocker cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@tautschnig @smowton @kroening @romainbrenguier @allredj @peterschrammel