add check for INT_MIN % -1 #3689

kroening · 2019-01-05T12:25:40Z

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

allredj

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

tautschnig

I think the output generated is misleading, as this isn't specific to int (and thus INT_MIN). The C standard states "If the quotient a/b is representable, the expression (a/b)*b + a%b shall equal a; otherwise, the behavior of both a/b and a%b is undefined." So it's equally undefined for any type wider than int.

And what about other languages? The commit message explicitly states that this is not undefined in C++, and I have no idea about Java.

kroening · 2019-01-05T16:05:16Z

I've changed the message to "result of signed mod is not representable".

It's defined in C++, but crashes anyway with any compiler I tried.

It's guaranteed to be 0 in Java (and I tried that this actually works, at least with openjdk 10).

allredj

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

tautschnig · 2019-01-05T19:25:42Z

src/analyses/goto_check.cpp

+/// check a mod expression for the case INT_MIN % -1
+void goto_checkt::mod_overflow_check(const mod_exprt &expr, const guardt &guard)
+{
+  if(!enable_signed_overflow_check)


if(!enable_signed_overflow_check || mode == ID_java) based on the conversation.

tautschnig · 2019-01-05T19:26:14Z

src/analyses/goto_check.cpp

+      guard);
+  }
+
+  return;


Seems unnecessary?

tautschnig · 2019-01-05T19:32:07Z

src/analyses/goto_check.cpp

+      expr.op0(), to_signedbv_type(type).smallest_expr());
+
+    notequal_exprt minus_one_neq(
+      expr.op1(), from_integer(-1, expr.op1().type()));


What I still don't like very much are the number of further assumptions baked into this. The standard says that a / b must be representable. Only because of two's complement does this imply that this isn't representable exactly for the case of b == -1. I'm not sure we have ever specified that two's complement is the one and only representation for goto programs to use? Shouldn't we do what the standard says, and simply check for overflow of a / b?

C11 and C++11 also allow one's complement and the signed magnitude representation. But then the test type.id() == ID_signedbv would fail (this is documented to be two's complement).

Note that the check for overflow of signed integer division is implemented in exactly the same way.

My apologies for missing that ID_signedbv actually has this documented.

INT_MIN % -1 is, in principle, defined to be zero in ANSI C, C99, C++98, and C++11. Most compilers, however, fail to produce zero, and in some cases generate an exception. C11 explicitly makes this case undefined. This commit adds a check for this particular case, classified as signed overflow.

allredj

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

kroening added the enhancement label Jan 5, 2019

kroening assigned tautschnig Jan 5, 2019

kroening requested review from chrisr-diffblue, martin-cs, peterschrammel, smowton and thk123 as code owners January 5, 2019 12:25

allredj reviewed Jan 5, 2019

View reviewed changes

tautschnig requested changes Jan 5, 2019

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Jan 5, 2019

kroening force-pushed the mod_minus_one branch from 7a9bf12 to 2f5d670 Compare January 5, 2019 16:05

kroening force-pushed the mod_minus_one branch from 2f5d670 to de08db4 Compare January 5, 2019 16:07

allredj reviewed Jan 5, 2019

View reviewed changes

tautschnig reviewed Jan 5, 2019

View reviewed changes

kroening force-pushed the mod_minus_one branch from de08db4 to 53a79b6 Compare January 5, 2019 21:46

allredj reviewed Jan 5, 2019

View reviewed changes

tautschnig approved these changes Jan 5, 2019

View reviewed changes

tautschnig assigned smowton, peterschrammel and chrisr-diffblue and unassigned kroening Jan 5, 2019

chrisr-diffblue approved these changes Jan 7, 2019

View reviewed changes

tautschnig merged commit 4329b28 into develop Jan 7, 2019

tautschnig deleted the mod_minus_one branch January 7, 2019 11:18

+                    guard);
+                }
+                return;

add check for INT_MIN % -1 #3689

add check for INT_MIN % -1 #3689

Uh oh!

Conversation

kroening commented Jan 5, 2019

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!

kroening commented Jan 5, 2019

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 Jan 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Jan 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Jan 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 5, 2019

Choose a reason for hiding this comment

Uh oh!

kroening Jan 5, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Jan 5, 2019

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!

7 participants