Unsigned overflow checked for `0U - x` but not for `-x`

[SaswatPadhi]

CBMC version: 5.29.0
Operating system: 10.15.7

Test case:

#include <assert.h>
#include <stdint.h>

int main()
{
    uint32_t x;
    __CPROVER_assume(x & 0x80000000); // set the MSB

    uint32_t y = 0u - x;    // CBMC unhappy
    uint32_t z = -x;        // CBMC unchecked
    uint32_t w = 1u + ~x;   // CBMC happy

    assert(w == y);         // passes
    assert(w == z);         // passes
}

Exact command line resulting in the issue:

$ cbmc --unsigned-overflow-check --signed-overflow-check --bounds-check --conversion-check ~/test.c | tail
** Results:
/Users/saspadhi/test.c function main
[main.overflow.1] line 9 arithmetic overflow on unsigned - in 0u - x: FAILURE
[main.overflow.2] line 11 arithmetic overflow on unsigned + in 1u + ~x: SUCCESS
[main.assertion.1] line 13 assertion w == y: SUCCESS
[main.assertion.2] line 14 assertion w == z: SUCCESS

** 1 of 4 failed (2 iterations)
VERIFICATION FAILED

What behaviour did you expect:
CBMC would report overflow consistently on -x and 0u - x.

What happened instead:
CBMC does not report an overflow on unary negation -x but does so on 0u - x.

[SaswatPadhi]

Tagged this as aws-high because the behavior is inconsistent with 0U - x, and it might be an easy fix?

cc: @feliperodri

[feliperodri]

cc: @tautschnig

[SaswatPadhi]

Note also that MISRA rules (which FreeRTOS projects enforce), flag unary negation -x but not 0U - x.
(See: https://rules.sonarsource.com/c/RSPEC-876)

[tautschnig]

I agree that we should be consistent here. I'd probably favour adding a check for unary minus (checking that the value must be zero so as not to overflow). But that's something where I'd really like to get @kroening and @martin-cs input on.

[kroening]

Unary minus is pretty useless on unsigned arithmetic. Likely a cast to a signed type is missing.

[kroening]

We could do the "is not zero test" for completeness, but really this is just saying "rewrite your code".

[martin-cs]

I think the following are the relevant bits of ISO 9899:

"6.3.1.3 Signed and unsigned integers
1 When a value with integer type is converted to another integer type other than _Bool, if
the value can be represented by the new type, it is unchanged.
2 Otherwise, if the new type is unsigned, the value is converted by repeatedly adding or
subtracting one more than the maximum value that can be represented in the new type
until the value is in the range of the new type.49)
3 Otherwise, the new type is signed and the value cannot be represented in it; either the
result is implementation-defined or an implementation-defined signal is raised."

"6.5 Expressions
(5) If an exceptional condition occurs during the evaluation of an expression (that is, if the
result is not mathematically defined or not in the range of representable values for its
type), the behavior is undefined."

" 6.5.3.3 Unary arithmetic operators
(3) The result of the unary - operator is the negative of its (promoted) operand. The integer
promotions are performed on the operand, and the result has the promoted type.
(4) The result of the ~ operator is the bitwise complement of its (promoted) operand (that is,
each bit in the result is set if and only if the corresponding bit in the converted operand is
not set). The integer promotions are performed on the operand, and the result has the
promoted type. If the promoted type is an unsigned type, the expression ~E is equivalent
to the maximum value representable in that type minus E."

"6.5.6 Additive operators
(6) The result of the binary - operator is the difference resulting from the subtraction of the
second operand from the first."

If the semantics for --unsigned-overflow-check is "does the value computed by this expression lie outside of [0,2^n-1] before it is converted?" then:

 uint32_t y = 0u - x;    // An error because the result is negative, will be (2^32 - 1) - x afterwards
 uint32_t z = -x;          // Also an error; negation of anything unsigned apart from 0 will be an error, will be (2^32 - 1) - x afterwards
 uint32_t w = 1u + ~x;   // Fine because the value will be 1 + ((2^32 - 1) - x) which will only overflow (on addition) when x = 0

If we do something else when we should probably come up with a different definition of what the unsigned overflow check means.

( That said, @kroening is right that it is a bit silly to almost always flag an operation but ... )

[SaswatPadhi]

If we do something else when we should probably come up with a different definition of what the unsigned overflow check means.

Yes, the main thing I am pointing out in this bug report is that CBMC has inconsistent behavior on -x and 0u -x. Either of these two behaviors make sense, and we should document which one of these is to be expected for --unsigned-overflow-check:

1. report all unsigned overflows, i.e. value outside of [0, 2^n - 1]

• so error on both -x and 0u - x

2. report non-trivial overflows, i.e. value outside of [0, 2^n - 1] resulting from an expression that's not syntactically -x or 0u - x, since those clearly almost always (except for x = 0) overflow and so probably that's intentional

• so error on neither -x nor 0u - x

[jimgrundy]

I agree with where where this seems to be ending up.

• "-x" should behave like "0u - x"
  But also I would expect that, in general for "x - y" (where both x and y are unsigned) we'll be checking that "x >= y" to avoid underflow. In the case where someone writes "-x" (where x is unsigned) we'd basically be checking "x == 0", which only serves to indicate how broken the developer's thinking is at this point, but it seems that a consistent way for us to point this out to the developer would be to implement the check.