Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2 #3260

tautschnig · 2018-11-03T11:29:02Z

This further reduces the number of warnings flagged, in particular in
Visual-Studio builds. Also turn tests of the size of ID_vector types being
constants into invariants as was already done in some places.

Each commit message has a non-empty body, explaining why the change was made.
n/a 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).
n/a 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.

kroening · 2018-11-03T11:42:45Z

jbmc/src/java_bytecode/expr2java.cpp

-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const wchar_t int_value = numeric_cast_v<wchar_t>(src);



This is difficult. Java chars are fixed to be 16 bits, by the standard.
wchar_t may be 16 bits, or may be 32 bits, but there isn't an obvious connection to Java's concept of a 'char'.

Also, signedness may differ. Java's char is unsigned.

Hmm, thanks, I had inferred the type from what utf16_native_endian_to_java takes as parameter. What would be the right type to use here, and where should a possible cast happen?

Anything that is guaranteed to hold an unsigned 16-bit values should work -- so how about "char16_t". I would then do an explicit cast to wchar_t when doing the call to utf16_native_endian_to_java. Really utf16_native_endian_to_java should take a char16_t.

Yes char16_t should be used here and in utf16_native_endian_to_java.

allredj

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

kroening · 2018-11-03T16:03:21Z

src/goto-programs/goto_trace.cpp

+      const auto i = numeric_cast<mp_integer>(expr);
+      if(i.has_value() && *i >= 0)
+        return integer2string(*i, 2);
    }


Triggered #3262, will rebase once this is merged.

thk123 · 2018-11-05T09:49:49Z

TG failure looks spurious - I have restarted it.

allredj

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

romainbrenguier · 2018-11-05T11:56:18Z

src/analyses/invariant_set.cpp

        {
-          mp_integer value;
-          assert(!to_integer(e, value));
+          mp_integer value = numeric_cast_v<mp_integer>(e);


romainbrenguier · 2018-11-05T11:59:34Z

src/goto-programs/interpreter_evaluate.cpp

-      mp_integer i;
-      if(!to_integer(expr, i))
+      const auto i = numeric_cast<mp_integer>(expr);
+      if(i.has_value())


could be written if(const auto i = numeric_cast<mp_integer>(expr)) (makes clear that i is only used in the if)

romainbrenguier · 2018-11-05T12:01:35Z

src/solvers/qbf/qdimacs_core.cpp

              const exprt &val_expr=oit->op1();
-              mp_integer value;
-              to_integer(val_expr, value);
+              mp_integer value = numeric_cast_v<mp_integer>(val_expr);


Since value is converted to ulong just afterwards it may make sense to directly cast to unsigned long here.

also could be const

romainbrenguier

Nice. The utf16 issue should be fixed but is not related to this PR, so for me it's not blocking.

martin-cs

The part that touches my world looks fine.

peterschrammel · 2018-11-05T19:23:44Z

src/solvers/qbf/qdimacs_core.cpp

        it!=used_bits_map.end();
        it++)
    {
+      // this is unmaintained code, don't try to reformat it


Can't we just remove it?

I have not bothered to look into this code, quite likely the entire qdimacs support is mostly broken?

peterschrammel · 2018-11-05T19:24:25Z

src/solvers/flattening/boolbv_quantifier.cpp

-        mp_integer over_i;
-        to_integer(over_expr, over_i);
+        mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
        /**


Side remark (not to be done in this PR): we should replace these /* */ comments.

Java chars are fixed to be 16 bits by the standard.

… part 2 This further reduces the number of warnings flagged, in particular in Visual-Studio builds. Also turn tests of the size of ID_vector types being constants into invariants as was already done in some places.

allredj

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

tautschnig requested review from NathanJPhillips, cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier, smowton and thk123 as code owners November 3, 2018 11:29

tautschnig force-pushed the vs-no-to_integer branch from 6a6a684 to fade8a8 Compare November 3, 2018 11:35

kroening reviewed Nov 3, 2018

View reviewed changes

allredj reviewed Nov 3, 2018

View reviewed changes

kroening reviewed Nov 3, 2018

View reviewed changes

kroening approved these changes Nov 3, 2018

View reviewed changes

kroening assigned smowton, thk123 and romainbrenguier Nov 3, 2018

allredj reviewed Nov 5, 2018

View reviewed changes

romainbrenguier reviewed Nov 5, 2018

View reviewed changes

romainbrenguier approved these changes Nov 5, 2018

View reviewed changes

tautschnig force-pushed the vs-no-to_integer branch from fade8a8 to b07a78b Compare November 5, 2018 16:06

tautschnig assigned peterschrammel and unassigned romainbrenguier Nov 5, 2018

tautschnig force-pushed the vs-no-to_integer branch from b07a78b to bfd8234 Compare November 5, 2018 18:26

martin-cs approved these changes Nov 5, 2018

View reviewed changes

peterschrammel approved these changes Nov 5, 2018

View reviewed changes

Change utf16_native_endian_to_java to consume char16_t

c2380e8

Java chars are fixed to be 16 bits by the standard.

peterschrammel removed their assignment Nov 5, 2018

tautschnig force-pushed the vs-no-to_integer branch from bfd8234 to b541bf9 Compare November 5, 2018 19:27

tautschnig assigned tautschnig and unassigned smowton and thk123 Nov 5, 2018

allredj reviewed Nov 5, 2018

View reviewed changes

tautschnig merged commit b0d28c8 into diffblue:develop Nov 5, 2018

tautschnig deleted the vs-no-to_integer branch November 5, 2018 21:35

Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2 #3260

Use numeric_cast<mp_integer> instead of deprecated to_integer(exprt), part 2 #3260

Uh oh!

Conversation

tautschnig commented Nov 3, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

thk123 commented Nov 5, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

romainbrenguier left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants