bv2integer is now told the width #3100

kroening · 2018-10-04T15:00:21Z

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.

allredj

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

allredj

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

allredj

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

tautschnig

A couple of suggestions (trying out GitHub's new feature...) below. From the start, this PR would have benefitted quite a bit from commit messages answering the "why?" question. The answer to that has become clear through other PRs, but that delays reviewing significantly.

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

tautschnig · 2018-10-18T08:19:28Z

src/ansi-c/expr2c.cpp

@@ -1811,9 +1811,10 @@ std::string expr2ct::convert_constant(
    if(c_enum_type.id()!=ID_c_enum)
      return convert_norep(src, precedence);

-    bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
+    const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;


Nit pick: Unrelated change?

Yes, but we appear to do some, and not others!

As a reviewer, the first question I usually ask myself is "why was this line changed" and expect to be able to immediately answer that to myself from the commit message. Sometimes there are additional changes in those lines beyond what's in the commit message. If those are of the nature "added in a const" or "fixed up whitespace" then those seem like desirable improvements. Everything else raises eyebrows and usually makes me post questions in here ;-)

src/goto-programs/goto_convert.cpp

src/goto-programs/goto_trace.cpp

tautschnig · 2018-10-18T08:27:50Z

src/util/arith_tools.cpp

+      int_value = bv2integer(id2string(value), width, false);
+      return false;
+    }
+    else if(subtype.id()==ID_c_bool)


Dare I say that a bugfix without accompanying test has been sneaked in?

Will make separate PR.

tautschnig

One further change required as below, but otherwise looks good to me.

tautschnig · 2018-10-18T09:13:29Z

src/goto-programs/goto_convert.cpp

-            bv2integer(id2string(to_constant_expr(*it).get_value()), true));
+          mp_integer int_value;
+          if(to_integer(to_constant_expr(*it), int_value))
+            return true;


The limitation of GitHub's suggestions feature (I have already provided feedback to them): my suggestion was meant to replace the entire bit of code, the lines above need to be removed now.

Direct access to the value of a constant_exprt is prone to error; the already existing functions should be used instead.

allredj

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

kroening requested a review from tautschnig October 4, 2018 15:00

kroening requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli, smowton and thk123 as code owners October 4, 2018 15:00

kroening force-pushed the hex-bitvectors3 branch 2 times, most recently from 20a0c6c to c4124b6 Compare October 4, 2018 17:10

kroening mentioned this pull request Oct 4, 2018

Use numeric_cast_v<std::size_t> instead of deprecated integer2size_t [blocks: #2310] #3051

Merged

5 tasks

kroening force-pushed the hex-bitvectors3 branch from c4124b6 to 5ab5772 Compare October 4, 2018 17:37

allredj reviewed Oct 4, 2018

View reviewed changes

kroening assigned smowton, tautschnig and peterschrammel Oct 5, 2018

tautschnig added the work in progress label Oct 5, 2018

tautschnig assigned kroening and unassigned smowton, tautschnig and peterschrammel Oct 5, 2018

peterschrammel approved these changes Oct 5, 2018

View reviewed changes

kroening force-pushed the hex-bitvectors3 branch from 5ab5772 to 5eca685 Compare October 7, 2018 18:26

allredj reviewed Oct 7, 2018

View reviewed changes

kroening force-pushed the hex-bitvectors3 branch from 5eca685 to c89578a Compare October 8, 2018 07:10

allredj reviewed Oct 8, 2018

View reviewed changes

kroening force-pushed the hex-bitvectors3 branch from c89578a to 8314f36 Compare October 13, 2018 15:20

allredj reviewed Oct 13, 2018

View reviewed changes

kroening mentioned this pull request Oct 17, 2018

Bitvectors are now hexadecimal #3107

Merged

7 tasks

tautschnig reviewed Oct 18, 2018

View reviewed changes

kroening force-pushed the hex-bitvectors3 branch from f62df2d to 1f96e27 Compare October 18, 2018 09:10

tautschnig approved these changes Oct 18, 2018

View reviewed changes

kroening force-pushed the hex-bitvectors3 branch from 1f96e27 to f8e5542 Compare October 18, 2018 09:21

kroening removed the work in progress label Oct 18, 2018

kroening force-pushed the hex-bitvectors3 branch 2 times, most recently from 3487bbe to 36ebc8b Compare October 18, 2018 09:39

kroening requested a review from chrisr-diffblue as a code owner October 18, 2018 09:39

Daniel Kroening added 2 commits October 18, 2018 10:59

use high-level numerical conversion

a3c453c

Direct access to the value of a constant_exprt is prone to error; the already existing functions should be used instead.

goto_trace: strengthen signature of numeric_representation

2f080ef

kroening force-pushed the hex-bitvectors3 branch from 36ebc8b to 9b96fd1 Compare October 18, 2018 09:59

bv2integer is now told the width

92f2621

kroening force-pushed the hex-bitvectors3 branch from 9b96fd1 to 92f2621 Compare October 18, 2018 12:00

allredj reviewed Oct 18, 2018

View reviewed changes

kroening merged commit 954faed into develop Oct 18, 2018

kroening deleted the hex-bitvectors3 branch October 18, 2018 13:38

allredj mentioned this pull request Oct 23, 2018

Fix index expression in interpretert::evaluate #3223

Merged

6 tasks

bv2integer is now told the width #3100

bv2integer is now told the width #3100

Uh oh!

Conversation

kroening commented Oct 4, 2018

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

tautschnig Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

tautschnig Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Oct 18, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!