Add integers safely, and prove the safety

Question

Programming course assignment asks to

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 on formal verification methods). So I would like to ask: Are there better (or different) solutions?

Thank you

#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;
}

If your code is working properly, you can try the same question at [codereview.se] — Sourav Ghosh, May 21 '15 at 10:47
@KirilKirov: It must mean "avoiding overflow", since that's the only unsafe thing that can happen with integer arithmetic. — Mike Seymour, May 21 '15 at 10:49
@MikeSeymour - unless there are other threads, messing with `res`, for example. — Kiril Kirov, May 21 '15 at 10:52
`INT_MIN - op2` underflows, since `op2` is negative. Also returning `1` on error is a very bad idea, because you never know if the result is `1` or an error occured. My idea would be to use `long long int`s, add them and check if the results fits in an `int`. — nwp, May 21 '15 at 10:56
Somehow related: [safe integer](https://buildsecurityin.us-cert.gov/articles/knowledge/coding-practices/safe-integer-operations). In the gcc part a rather simple way of checking the result is shown. Maybe this can help to "proove" your correctness. — 463035818_is_not_an_ai, May 21 '15 at 10:59
@nwp: the problem with the `long long` approach is that `int` could also be 64 bit. — Bathsheba, May 21 '15 at 11:18
@tobi303 the example referenced "Checking for overflow when adding two signed integers" invokes undefined behavior (`int` overflow) with `const Wtype w = a + b`. — chux - Reinstate Monica, May 21 '15 at 14:51
possible duplicate of [How to detect integer overflow in C/C++?](http://stackoverflow.com/questions/199333/how-to-detect-integer-overflow-in-c-c) — Come Raczy, May 21 '15 at 15:39
@chux actually I was refering to the `if (b >= 0 ? w < a : w > a)` that is used to check (i.e. "prove") that the addition was succesful — 463035818_is_not_an_ai, May 21 '15 at 17:41
@tobi303 Since `if (b >= 0 ? w < a : w > a)` depends on `w` and `const Wtype w = a + b` is UB on overflow, that check code is too late, UB has all ready happened. [Elvis has all ready left the building](http://en.wikipedia.org/wiki/Elvis_has_left_the_building). — chux - Reinstate Monica, May 21 '15 at 17:47
@chux I think I got your point. Lets assume he has (1) a safe function that adds two integers, then he could still use this condition to (2) argue/show/prove that there really was no overflow (assumed overflow is all that has to be checked to call it safe). — 463035818_is_not_an_ai, May 21 '15 at 17:52
@tobi303 Yes, Think of a smart compiler that _knows_ `int` overflow is UB and figures out `if (b >= 0 ? w < a : w > a)` could only be true on overflow. Since overflow is UB, that optimizing compiler simple drops that line of code as it is not needed. — chux - Reinstate Monica, May 21 '15 at 17:53
@chux I think I got your point. For a safe function that really is safe, any check/proof is superfluous and can be optimized away. However, for an assignment I personally would try to argue based on a simple check rather than optimizing this check away ;) — 463035818_is_not_an_ai, May 21 '15 at 18:07
@tobi303 For a safe function that really is safe, the check needs to be done _before_ the addition. A check _after_ an addition that may overflow is UB and is superfluous. A check _before_ potential UB, that prevents UB, is good. — chux - Reinstate Monica, May 21 '15 at 19:13

score 3 · Answer 1 · answered May 21 '15 at 10:56

3

This is how I would do it:

If the input arguments have different signs then the result is always computable without any risk of overflow.

If both input arguments are negative, then compute -safe_int_add(res, -op1, -op2);. (You'll need to check that op1 or op2 are not the largest negative in 2s compliment).

The function that needs thought is the one that adds two positive numbers: convert your two inputs to unsigned types. Add those. That is guaranteed to not overflow the unsigned type since you can store (at least) twice as large values in an unsigned int than in a signed int (exactly twice for 1s compliment, one more than that for 2s compliment).

Then only attempt a conversion back to signed if the unsigned value is small enough.

answered May 21 '15 at 10:56

Bathsheba

231,907
34
361
483

1

Very concise answer. Before I read the question I wasnt even aware that one has to be careful with adding integers (well if I think about it, of course one has to be...) and its good to know that it is that easy to avoid problems – 463035818_is_not_an_ai May 21 '15 at 11:03
1) "guaranteed to not overflow the unsigned type since you can store (at least) twice as large values in an unsigned int than in a signed int" is not guaranteed by the C spec. C only guarantees `UINT_MAX >= INT_MIX`. It is common though with 2's complement and no padding to have a 2x range. 2) OP's approach works for all `int` including 2's complement `INT_MIN` without special handling unlike this answer. – chux - Reinstate Monica May 21 '15 at 14:32

score 2 · Answer 2 · answered May 21 '15 at 12:01

You can look at the implementation of JDK 8, which has a fine reference to the book Hacker's Delight from 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;
}

In my version of the book, it is chapter 2-13 though. There you can find a lengthy explanation about the whole issue.

if `x+y` overflows, the result is undefined behavior (C11dr §3.4.3 3). So any code after `int r = x + y;` is too late. — chux - Reinstate Monica, May 21 '15 at 14:39

score 2 · Accepted Answer · edited May 23 '17 at 11:46

OP's approach is optimally portably staying within type int as well as safe - no undefined behavior (UB) with any combination of int. It is independent of a particular int format (2's complement, 2's complement, sign-magnitude).

In C, int overflow/(underflow) is undefined behavior. So code, if staying with int, must determine overflow potential before-hand. With op1 positive, INT_MAX - op1 cannot overflow. Also, with op1 negative, INT_MIN - op1 cannot overflow. So with edges properly calculated and tested, op1 + op2 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;
}

Add integers safely, and prove the safety

3 Answers3

Linked