Bitvectors are now hexadecimal #3107

kroening · 2018-10-06T15:51:23Z

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).
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.

Note that an alternative would be to go to a binary representation, which is not much different compared to this PR. This would save another 2x in memory, but has the disadvantage that ireps are then more difficult to read.

This will require a bump in the goto-binary version number, which I would prefer to do together with a few other changes.

kroening · 2018-10-19T11:57:40Z

Now cleaned up! The B256 option is now in a separate PR.

allredj

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

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

tautschnig

Sorry, still an incomplete review, sending the below comments and will do further reviews once those are addressed.

tautschnig · 2018-10-19T14:07:31Z

src/util/arith_tools.cpp

+
+  char nibble = src[src.size() - 1 - nibble_index];
+
+  DATA_INVARIANT(isxdigit(nibble), "");


Still to be addressed.

tautschnig · 2018-10-19T14:09:31Z

src/util/arith_tools.cpp

-  return src[src.size() - 1 - bit_index] == '1';
+
+  // The representation is hex, most significant nibble first.
+  const auto nibble_index = bit_index >> 2;


Maybe leave the optimisation that "divide by 4" is a shift by 2 to the compiler? I don't think doing those optimisations help readability.

tautschnig · 2018-10-19T14:10:59Z

src/util/arith_tools.cpp

+  const auto nibble_index = bit_index >> 2;
+
+  if(nibble_index >= src.size())
+    return false;


This needs to be changed now that #3196 has been merged to re-instate the PRECONDITION.

tautschnig · 2018-10-19T14:11:30Z

src/util/arith_tools.cpp

+  if(nibble_index >= src.size())
+    return false;
+
+  char nibble = src[src.size() - 1 - nibble_index];


src/util/arith_tools.cpp

tautschnig · 2018-10-19T14:20:21Z

src/util/arith_tools.cpp

@@ -299,12 +323,36 @@ bool get_bvrep_bit(
 irep_idt
 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
 {
-  std::string result(width, ' ');
+  std::string result;
+  result.reserve(width / 4 + 1);


If doing the division-by-power-of-two-is-shift then it should be done everywhere (or, my preference: nowhere)

(width + 3) / 4 will avoid reserving an unnecessary extra space.

tautschnig · 2018-10-19T14:20:32Z

src/util/arith_tools.cpp

-  std::string result(width, ' ');
+  std::string result;
+  result.reserve(width / 4 + 1);
+  unsigned nibble = 0;


src/util/arith_tools.cpp

tautschnig · 2018-10-19T14:25:06Z

src/util/arith_tools.cpp


-  return result;
+    nibble |= ((unsigned)f(i)) << bit_in_nibble;


What about:

if(f(i)) nibble |= 1u << bit_in_nibble;

Not sure to what extent performance would differ given the additional branch, though.

tautschnig · 2018-10-19T14:28:06Z

src/util/arith_tools.cpp

+
+  // drop leading zeros
+  while(!result.empty() && result.back() == '0')
+    result.resize(result.size() - 1);


Please use rfind and a single resize.

allredj

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

src/util/arith_tools.cpp

allredj

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

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

Simultaneously leading zeros are dropped. This reduces the memory consumption of bit-vectors by 4x or more.

allredj

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

martin-cs

I think everything I raised has been resolved or removed.

kroening added the enhancement label Oct 6, 2018

kroening assigned tautschnig Oct 6, 2018

kroening requested review from cesaro, cristina-david, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners October 6, 2018 15:51

kroening force-pushed the hex-bitvectors5 branch 4 times, most recently from 536b087 to a0c531b Compare October 7, 2018 12:07

kroening requested a review from chrisr-diffblue as a code owner October 7, 2018 12:07

kroening force-pushed the hex-bitvectors5 branch 14 times, most recently from 15d8038 to f2ae4cf Compare October 13, 2018 15:50

kroening force-pushed the hex-bitvectors5 branch from 6b999bc to 0e37e1f Compare October 19, 2018 11:57

kroening mentioned this pull request Oct 19, 2018

Bitvectors are now base 256 #3206

Closed

5 tasks

allredj reviewed Oct 19, 2018

View reviewed changes

tautschnig reviewed Oct 19, 2018

View reviewed changes

kroening force-pushed the hex-bitvectors5 branch from 0e37e1f to d2263f2 Compare October 19, 2018 15:08

kroening assigned tautschnig and unassigned kroening Oct 19, 2018

kroening force-pushed the hex-bitvectors5 branch 2 times, most recently from a91718a to b366d8b Compare October 20, 2018 09:16

allredj reviewed Oct 20, 2018

View reviewed changes

tautschnig reviewed Oct 20, 2018

View reviewed changes

src/util/arith_tools.cpp Show resolved Hide resolved

src/util/arith_tools.cpp Show resolved Hide resolved

tautschnig assigned kroening and unassigned tautschnig Oct 20, 2018

tautschnig approved these changes Oct 20, 2018

View reviewed changes

tautschnig assigned martin-cs and unassigned kroening Oct 20, 2018

kroening force-pushed the hex-bitvectors5 branch 3 times, most recently from a9826b6 to 103d74c Compare October 23, 2018 16:21

allredj reviewed Oct 23, 2018

View reviewed changes

switch representation of bit-vectors to hex

c7c4110

Simultaneously leading zeros are dropped. This reduces the memory consumption of bit-vectors by 4x or more.

kroening force-pushed the hex-bitvectors5 branch from 103d74c to c7c4110 Compare November 5, 2018 13:25

allredj reviewed Nov 5, 2018

View reviewed changes

martin-cs approved these changes Nov 5, 2018

View reviewed changes

tautschnig merged commit 2c3d140 into develop Nov 5, 2018

tautschnig deleted the hex-bitvectors5 branch November 5, 2018 16:02

hannes-steffenhagen-diffblue mentioned this pull request Nov 12, 2018

Change binary representations to hexadecimal from binary diffblue/gnat2goto#61

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bitvectors are now hexadecimal #3107

Bitvectors are now hexadecimal #3107

kroening commented Oct 6, 2018 •

edited

Loading

kroening commented Oct 19, 2018

allredj left a comment

allredj left a comment

tautschnig left a comment

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

tautschnig Oct 19, 2018

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

martin-cs left a comment


		char nibble = src[src.size() - 1 - nibble_index];

		DATA_INVARIANT(isxdigit(nibble), "");

Bitvectors are now hexadecimal #3107

Bitvectors are now hexadecimal #3107

Conversation

kroening commented Oct 6, 2018 • edited Loading

kroening commented Oct 19, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

kroening commented Oct 6, 2018 •

edited

Loading