Overflow-safe addition and multiplication by extending the result type

[ahoppen]

The below proposal is not 100% fletched out yet, but I'd like to get a general feedback of whether the idea is desirable. If that is the case, I am more than happy to write a more detailed proposal and discuss further corner cases (see Open ends).

Abstract

The result type of multiplication and addition is the same as the first operand, which may cause an overflow in case the result type cannot hold the multiplication/addition result. That issue could be solved if the multiplication/addition always returned a type that is safe to hold the result. (e.g. uint16 * uint32 = uint48)

Motivation

Over- and underflow are sources of bugs that are usually hard to spot and easy to miss. It would be great if Solidity could assist the developer in catching those bugs by requiring to make potential overflow positions explicit.

Specification

For simplicity, I only consider uint. int is handled analogously.

I propose two changes:

1. The resulting type of multiplying two integers a and b of types uint<x> and uint<y> respectively should be uint<x + y>. The semantics of a + b should be equivalent to the current behaviour of uint<x+y>(a) + b.
2. The resulting type of adding two integers a and b of types uint<x> and uint<y> respectively should be uint<max(x, y) + 8>. The semantics of a + b should be equivalent to the current behaviour of uint<max(x, y) + 8>(a) + b.

Open ends

These are some areas I have thought about so far but not reached a definite conclusion on. Discussion on those could continue if the overall idea is desirable.

• The semantics of multiplication and addition would need to be discussed if the resulting type is uint<n> with n > 256
  • I would propose an internal type (name is just a placeholder for now) uint_too_large that cannot spelled out in source. Hence the user would need to specify a cast and make the potential overflow explicity
• The above idea can also be extended to left bitshifts and exponentiation by making uint<x> << uint<y> return uint<x * y>. In most cases this will result in a uint_too_large and force the developer to make any potential overflow explicit.
• The += and *= operators are still unsafe for overflow. Their behaviour would need to be considered
  • Removal of those operators would radical but the safest option
• If a, b, and c all have type uint8 then with the proposed behaviour a + b + c has type uint24 while uint16 would be sufficient. That could be solved by introducing types uint<n> where n % 8 != 0. Those types are internally represented as the next multiple of 8 and are only there to aid the type checker. With those types a + b could return a uint9 and the addition of c would result in a uint10 that will then be represented as a uint16 on the bytecode level.
• I do not know of any programming languages that precedent the described typing behaviour. Hence the behaviour might be confusing for developers. However, I think, given the added safety, the confusion might be worth it.
• This idea is not able to guard against overflow. Would it be desirable to protect developers from one but not another?

Backwards Compatibility

All addition and multiplication operations in existing Solidity source code that assign to a type that's not big enough to hold an overflow-free result would need to be audited for overflow. While this is a burden on the developer, I can imagine careful thinking about all of those operations may catch some bugs.

Also it changes behaviour of code like the following:

uint8 a = 255;
uint8 b = 255;
uint16 c = a + b;

Previously, the result was c = (255 + 255) % 256 = 254. With the new behaviour, the result is c = 510. I believe that the current behaviour is almost never what the developer wants to write and thus the behaviour change would be OK.

[Skyge]

I don't think this is a good proposal, as for most cases, if you find you use uint8 will be overflow, why don't use uint16 to replace, I think when I want to use a number, I will consider the type I have defined is suitable or not, if I just want to use uint8 rather than uint16, I will make more check to ensure it will not be overflow.

uint8 a = 255;
uint8 b = 255;
uint16 c = a + b;

I think the result of above is c = 254, besides, I think, as for Smart Contract, we can use the library SafeMath of the OpenZeppelin to avoid Over- and underflow. of course, this is my foolish thought.

[ahoppen]

I don't think this is a good proposal, as for most cases, if you find you use uint8 will be overflow, why don't use uint16 to replace, I think when I want to use a number, I will consider the type I have defined is suitable or not, if I just want to use uint8 rather than uint16, I will make more check to ensure it will not be overflow

My motivation was that a uint8 might be the argument of a function. Hence you can never know which value a user passes in and always need to assume the maximum value. Changing the type to uint16 just shifts the problem from 2^8-1 to 2^16-1. Allowing the user to enter a uint16 and then doing a require(x < 256) makes one byte of the input effectively useless, which isn’t desirable either. Furthermore it‘s easy to miss the check.

I think the result of above is c = 254

Thanks, I fixed the typo.

besides, I think, as for Smart Contract, we can use the library SafeMath of the OpenZeppelin to avoid Over- and underflow. of course, this is my foolish thought.

I think Solidity should be over/underflow-safe by default and not require the use of an external library.

[Skyge]

I am not sure, but there is a similar issue about this, solidity/issues/796

[chriseth]

I think it is a valid proposal to consider the addition of uintN and uintM to result in uint(N+M) and I think there are already languages that behave like that. This is of course complementary to runtime overflow checks which we plan to add. Such a runtime overflow check would also be performed upon explicit conversion like in uint8(x + y).

[ahoppen]

Is there anything I can do to help push this proposal? Or is there any formal process for such a language change?

[chriseth]

Unfortunately, we do not have a formal process. Also, radical breaking changes are a little less likely to be adopted nowadays. One problem I see with this proposal is that you basically would have to write uint x = uint(a + b) all the time and it would just get a habit without thinking about potential overflows. In contrast to that, the SMTChecker achieves a similar goal but is more flexible - it can consider the actual values, control flow, etc and not just the type of a value.

[ahoppen]

I wasn't aware of SMTChecker. That should solve the same problem in a nicer way indeed. Thanks for the pointer.