Add integers safely and prove safety
Course Destination Programming Requests
- write a (safe) function that adds two integers, and
- show that the function is safe.
The following code represents my solution. I am not an expert on the C standard (or formal verification methods). So I would like to ask: Are there better (or different) solutions?
thank
#include <limits.h>
/*
Try to add integers op1 and op2.
Return
0 (success) or
1 (overflow prevented).
In case of success, write the sum to res.
*/
int safe_int_add(int * res,
int op1,
int op2) {
if (op2 < 0) {
/** We have: **********************************************/
/* */
/* 0 > op2 */
/* 0 < - op2 */
/* INT_MIN < - op2 + INT_MIN */
/* INT_MIN < INT_MIN - op2 */
/* INT_MIN <= INT_MIN - op2 */
/* */
/** Also, we have: ****************************************/
/* */
/* op2 >= INT_MIN */
/* - op2 <= - INT_MIN */
/* INT_MIN - op2 <= - INT_MIN + INT_MIN */
/* INT_MIN - op2 <= 0 */
/* INT_MIN - op2 <= INT_MAX */
/* */
/** Hence, we have: ***************************************/
/* */
/* INT_MIN <= INT_MIN - op2 <= INT_MAX */
/* */
/* i.e. the following subtraction does not overflow. */
/* */
/***********************************************************/
if (op1 < INT_MIN - op2) {
return 1;
}
/** We have: *********************************/
/* */
/* INT_MIN - op2 <= op1 */
/* INT_MIN <= op1 + op2 */
/* */
/** Also, we have: ***************************/
/* */
/* op2 < 0 */
/* op1 + op2 < op1 */
/* op1 + op2 < INT_MAX */
/* op1 + op2 <= INT_MAX */
/* */
/** Hence, we have: **************************/
/* */
/* INT_MIN <= op1 + op2 <= INT_MAX */
/* */
/* i.e. the addition does not overflow. */
/* */
/**********************************************/
}
else {
/** We have: **********************************************/
/* */
/* op2 >= 0 */
/* - op2 <= 0 */
/* INT_MAX - op2 <= INT_MAX */
/* */
/** Also, we have: ****************************************/
/* */
/* INT_MAX >= op2 */
/* - INT_MAX <= - op2 */
/* INT_MAX - INT_MAX <= - op2 + INT_MAX */
/* 0 <= - op2 + INT_MAX */
/* 0 <= INT_MAX - op2 */
/* INT_MIN <= INT_MAX - op2 */
/* */
/** Hence, we have: ***************************************/
/* */
/* INT_MIN <= INT_MAX - op2 <= INT_MAX */
/* */
/* i.e. the following subtraction does not overflow. */
/* */
/***********************************************************/
if (op1 > INT_MAX - op2) {
return 1;
}
/** We have: *********************************/
/* */
/* op1 <= INT_MAX - op2 */
/* op1 + op2 <= INT_MAX */
/* */
/** Also, we have: ***************************/
/* */
/* 0 <= op2 */
/* op1 <= op2 + op1 */
/* INT_MIN <= op2 + op1 */
/* INT_MIN <= op1 + op2 */
/* */
/** Hence, we have: **************************/
/* */
/* INT_MIN <= op1 + op2 <= INT_MAX */
/* */
/* i.e. the addition does not overflow. */
/* */
/**********************************************/
}
*res = op1 + op2;
return 0;
}
source to share
The OP's approach is optimally portable to remain in type int
as well as safe - no undefined behavior (UB) with any combination int
. It does not depend on the specific format int
(2's complement, 2's complement, sign value).
In C, int
overflow / (underflow) is undefined behavior. So the code, if left with int
, must determine the potential for overflow sooner. If op1
positive, INT_MAX - op1
it cannot overflow. In addition, if op1
negative, INT_MIN - op1
it cannot overflow. Thus, with correctly sized and checked edges, op1 + op2
it will not overflow.
// Minor re-write:
int safe_int_add(int * res, int op1, int op2) {
assert(res != NULL);
if (op1 >= 0) {
if (op2 > INT_MAX - op1) return 1;
} else {
if (op2 < INT_MIN - op1) return 1;
}
*res = op1 + op2;
return 0;
}
If the broader type is known , the code can use
int safe_int_add_wide(int * res, int op1, int op2) {
int2x sum = (int2x) op1 + op2;
if (sum < INT_MIN || sum > INT_MAX) return 1;
*res = (int) sum;
return 0;
}
Approaches using unsigned
etc. must first qualify that UINT_MAX
> = INT_MAX - INT_MIN
. This is usually true, but not guaranteed by the C standard.
source to share
This is how I would do it:
If the input arguments have different signs, then the result is always evaluated without the risk of overflow.
If both input arguments are negative, then evaluate -safe_int_add(res, -op1, -op2);
. (You need to check what op1
or op2
not is the biggest negative in the 2s compliment).
The function that needs a thought is the one that adds two positive numbers: convert the two inputs to unsigned types. Add them. This is guaranteed not to overflow the unsigned type, since you can store (at least) twice the value in an unsigned int than in a signed int (exactly twice for the 1s compliment, one more for the 2s compliment).
Then try converting back to signed if unsigned is small enough.
source to share
You can take a look at the JDK 8 implementation which has an excellent link to the Hacker Delight book by Henry S. Warren Jr. here:
http://hg.openjdk.java.net/jdk8/jdk8/jdk/rev/b971b51bec01
public static int addExact(int x, int y) {
int r = x + y;
// HD 2-12 Overflow iff both arguments have the opposite sign of the result
if (((x ^ r) & (y ^ r)) < 0) {
throw new ArithmeticException("integer overflow");
}
return r;
}
My version of the book, however, has chapter 2-13. There you can find a detailed explanation of the whole problem.
source to share