Signed integer overflow

[lucasccordeiro]

CBMC provides "verification failed" for the following C program extracted from sv-benchmarks/c/signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i.

$cbmc ConversionToSignedInt_true-no-overflow.c --signed-overflow-check

#include <stdio.h>

int main() {
	// The literal of type long on the right-hand side is exactly INT_MAX+1 and will 
	// be converted to int.
	// Paragraph 6.3.1.3.3 of C11 says that if "[..] 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."
	int x = 2147483648L;
	printf("%d\n", x);
	return 0;
}

** Results:
[main.overflow.1] arithmetic overflow on signed type conversion in (signed int)2147483648l: FAILURE

** 1 of 1 failed (1 iteration)
VERIFICATION FAILED

[kroening]

Why is the answer 'this is an overflow' wrong?

[lucasccordeiro]

I have open this issue for discussion in the group. The interpretation of the sv-comp community is that there is no overflow in this particular benchmark if we assume sizeof(int)=4 and sizeof(long)>4. I'm also investigating other benchmarks that are incorrectly labeled and reporting to the sv-comp mailing list. Note that I did not mention that we are wrong, but I would like to discuss a bit more this particular issue before sending a pull request to the sv-comp mailing list. My interpretation of the C11 standard is that we should detect this as an overflow.

[martin-cs]

This shouldn't need discussion. C99 and C11 have a definition of what
is undefined behaviour on signed overflow and underflow. If this is not
clear then we need to ask the ISO 9899 committee. We will implement the
C semantics. SV-COMP can do what they want but ... if it's not
standards compliant it's not C.

Cheers,

• Martin

[tautschnig]

Isn't even the comment included in the file saying that there is implementation-defined behaviour here and, thus, we should get a verification failure?

[lucasccordeiro]

Ok. Instead of reporting this issue in the sv-comp mailing list, I have just mailed Matthias Heizmann (the benchmark's author) to ask for further clarification.

[kroening]

I would have reported; this is clearly an overflow.

[peterschrammel]

Misclassified. @lucasccordeiro, please send a mail to the sv-comp mailing list.

[lucasccordeiro]

@peterschrammel: In the past, I already had several discussions with Dirk Beyer that were unpleasant, trying to convince him when there is something wrong in the competition. This particular issue is “polemic” since everyone has a different interpretation when reading the C11 standard.

Here is the reply from Matthias Heizmann:

Hi Lucas,

On Tuesday 15 November 2016 11:20:50 Lucas Cordeiro wrote:

The comments in this benchmark clearly state that there is
implementation-defined behavior.
The comment is correct.

Shouldn't we classify it as false?
No. According to the C standard an overflow is "undefined behavior". Hence,
something that is "implementation defined behavior" cannot be an overflow.

I do not have a strong opinion what we should check. However, if we want a
notion of overflow that differs from the C standard, we should come up with
precise definition of an overflow (and I think we should not try to redefine the
rules for the current competition).

Best,

Matthias

I’m not willing to start another thread of unpleasant discussions at the sv-comp mailing list. I hope that you can respect my position.

If you like, I can investigate other issues in CBMC and then report to the sv-comp mailing list if they don’t depend on interpretation of people.

At this point in time, I'm unsure whether it is worth to come up with a precise definition of an overflow in the sv-comp community, but we can discuss it in the group.

[tautschnig]

What about one of the following:

• Acknowledge that conversion to a type of smaller bit width is not undefined behaviour, and thus add a separate command line option to enable such checks. Quite possibly the easiest approach, it just takes inventing a good name (numeric-bounds-check?).
• Start a discussion that the category is called "overflow" and not "undefined-behaviour-caused-by-overflow," and hence the definition of LIA-1 should apply: "If the value converted is greater than those representable in the target datatype, or less than those representable in the target datatype, even after rounding, then an overflow will result." (ISO/IEC 10967-1:2012)

[lucasccordeiro]

@tautschnig: The first suggestion would require us to add a new option to CBMC, right?

I'm going to mail Matthias Heizmann to discuss about the LIA-1 definition; he is the person who has proposed all those benchmarks.

[lucasccordeiro]

Here is Matthias reply about the LIA-1 definition pointed out by Michael.

=============================
Hi Lucas,

"If the value converted is greater than those representable in the target
datatype, or less than those representable in the target datatype, even
after rounding, then an overflow will result." (ISO/IEC 10967-1:2012)

I think I have some problems with this definition.

Let us consider the following expression on a standard Linux architecture
where 2147483647 is the maximal value of a signed integer.
2147483647 + 1
According to the C standard there is an overflow. But the above definition talks
only about the "value converted" but there is no conversion involved.

However, if we have the expression
unsigned char c = 256
there is no overflow according to the C standard, but there is an overflow
according to the above condition.

In my last email, I said "I do not have a strong opinion what we should
check." I just realized that I was wrong.
When I suggested to introduce an overflow category, my main motivation was
that we support an analysis that helps us to detect "undefined behavior".

Hence, I am very much in favor for keeping the category with the current
rules.

Maybe we can have a demo category in which we check more. However:

1. I cannot promise that I will have a tool ready for that.
2. I dislike that we use the term "overflow". According to the terminology of
   the C standard an overflow is something really really bad that should never
   happen. It might be confusing if we use the same term for something rather
   "harmless" like the wraparound that is done for unsigned data types.

Best,
Matthias

[tautschnig]

How about we just play by the rules, which state: "It can never happen that the resulting type of an operation is a signed integer type but the resulting value is not in the range of values that are representable by that type." (https://sv-comp.sosy-lab.org/2017/rules.php)

I'm going to file (and fight for) a pull request that overturns the result on that benchmark.

[tautschnig]

For the record: sosy-lab/sv-benchmarks#236