Invariant cleanup in flattening/boolbv_extractbit.cpp and flattening/boolbv_extractbits.cpp by hannes-steffenhagen-diffblue · Pull Request #3041 · diffblue/cbmc

hannes-steffenhagen-diffblue · 2018-09-25T14:48:55Z

Also contains some minor refactoring for those files in separate commits

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
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) (not applicable)
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 own.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 64f6578).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85886706
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).

allredj

Passed Diffblue compatibility checks (cbmc commit: 1de020e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85888067

src/solvers/flattening/boolbv_extractbits.cpp

tautschnig · 2018-09-25T18:33:13Z

src/solvers/flattening/boolbv_extractbits.cpp

-  for(std::size_t i=0; i<width; i++)
-    bv[i]=bv0[offset+i];
+  for(std::size_t i = 0; i < bv_width; i++)
+    result_bv[i] = src_bv[offset + i];


I think this could be rewritten as const bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);

src/solvers/flattening/boolbv_extractbits.cpp

tautschnig · 2018-09-25T18:35:15Z

src/solvers/flattening/boolbv_extractbits.cpp

-  mp_integer upper_as_int, lower_as_int;
  auto const &src_bv = convert_bv(expr.src());

+  auto maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());


Might add a const

hannes-steffenhagen-diffblue · 2018-09-26T10:39:19Z

Apologies, I forgot to include a commit. Please hold reviews while I'm fixing that.

NlightNFotis

Some nitpicks only, otherwise LGTM

NlightNFotis · 2018-09-26T11:11:24Z

src/solvers/flattening/boolbv_extractbit.cpp


    equal_exprt equality;
-    equality.lhs()=operands[1]; // index operand
+    equality.lhs() = expr.index(); // index operand


Nit: the strong typing makes the comment useless now?

NlightNFotis · 2018-09-26T11:18:30Z

src/solvers/flattening/boolbv_extractbits.cpp

    error().source_location=expr.find_source_location();
-    error() << "extractbits: wrong width (expected " << (o1-o2+1)
-            << " but got " << width << "): " << expr.pretty() << eom;
+    error() << "extractbits: wrong width (expected "


Can this not be rewritten as an invariant with diagnostic information?

Yes, that was in the commit I forgot to include

hannes-steffenhagen-diffblue · 2018-09-26T11:59:17Z

@tautschnig @NlightNFotis I believe I've addressed your comments now, please re-review once CI is done.

NlightNFotis

LGTM

allredj

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

hannes-steffenhagen-diffblue · 2018-09-26T14:32:24Z

All stages of the travis build have passed. I'm not sure why it's showing its in progress, its really not

tautschnig · 2018-09-26T14:35:24Z

Seems to be happening on other PRs as well (#2048, #2979).

tautschnig · 2018-09-26T16:40:17Z

@hannes-steffenhagen-diffblue You might try rebasing, some other PRs have by now gone through (though not all).

Using semantic names for operators instead of their position and expanding single letter abbreviations should help with legibility.

The throw was on checking if a constant expression with extractbit was a valid integer expression. The assert was signaling that we didn't support a type of expression so has been replaced with a throw of the appropriate exception type

This allows us to be a bit more explicit in the code with `has_value` rather than using an "anonymous" boolean result.

Also removes one throw that guards against violation of extractbits_expr invariants

allredj

Passed Diffblue compatibility checks (cbmc commit: 9423a5c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86049202

hannes-steffenhagen-diffblue requested review from kroening, martin-cs, peterschrammel and tautschnig as code owners September 25, 2018 14:48

hannes-steffenhagen-diffblue force-pushed the feature-invariant_cleanup-flattening-extractbits branch from 64f6578 to 1de020e Compare September 25, 2018 14:50

allredj reviewed Sep 25, 2018

View reviewed changes

tautschnig reviewed Sep 25, 2018

View reviewed changes

hannes-steffenhagen-diffblue added the do not merge label Sep 26, 2018

NlightNFotis approved these changes Sep 26, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature-invariant_cleanup-flattening-extractbits branch from 1de020e to e81aafb Compare September 26, 2018 11:55

hannes-steffenhagen-diffblue removed the do not merge label Sep 26, 2018

hannes-steffenhagen-diffblue force-pushed the feature-invariant_cleanup-flattening-extractbits branch from e81aafb to c6ffde7 Compare September 26, 2018 11:58

tautschnig approved these changes Sep 26, 2018

View reviewed changes

NlightNFotis approved these changes Sep 26, 2018

View reviewed changes

allredj reviewed Sep 26, 2018

View reviewed changes

hannes-steffenhagen-diffblue added 7 commits September 26, 2018 17:52

Use src/index instead of operand position in boolbv_extractbit

3dcaff7

Rename some local variables in boolbv_extractbit

10cab6a

Using semantic names for operators instead of their position and expanding single letter abbreviations should help with legibility.

Replace throw and assert in boolbv_extractbit

c2eec56

The throw was on checking if a constant expression with extractbit was a valid integer expression. The assert was signaling that we didn't support a type of expression so has been replaced with a throw of the appropriate exception type

Rename variables in boolbv_extractbits for easier readability

550f37c

Replace to_integer with numeric_cast in extractbits_expr

ad1b927

This allows us to be a bit more explicit in the code with `has_value` rather than using an "anonymous" boolean result.

Replace throws with invariants in boolbv_extractbits

af0eb45

Also removes one throw that guards against violation of extractbits_expr invariants

Use bvt constructor instead of manual loop for initialisation

9423a5c

hannes-steffenhagen-diffblue force-pushed the feature-invariant_cleanup-flattening-extractbits branch from c6ffde7 to 9423a5c Compare September 26, 2018 16:52

tautschnig merged commit 771b368 into diffblue:develop Sep 26, 2018

allredj reviewed Sep 26, 2018

View reviewed changes

Conversation

hannes-steffenhagen-diffblue commented Sep 25, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

Uh oh!

tautschnig Sep 25, 2018

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Sep 25, 2018

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Sep 26, 2018

Uh oh!

NlightNFotis left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Sep 26, 2018

Choose a reason for hiding this comment

Uh oh!

NlightNFotis Sep 26, 2018

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue Sep 26, 2018

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Sep 26, 2018

Uh oh!

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

hannes-steffenhagen-diffblue commented Sep 26, 2018

Uh oh!

tautschnig commented Sep 26, 2018

Uh oh!

tautschnig commented Sep 26, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

hannes-steffenhagen-diffblue commented Sep 25, 2018 •

edited

Loading