Добавить целые безопасно, и доказать безопасность

Question

назначение конечно программирование просит

• написать функцию (сейф), который добавляет два целых числа, и
• показывают, что функция безопасна.

Следующий код представляет мое решение. Я не специалист по стандарту C (или по формальным методам проверки). Итак, я хотел бы спросить: Есть ли лучшие (или разные) решения?

Спасибо

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

Answer 1

Подход OP оптимально переносится в пределах int, а также безопасен - без неопределенного поведения (UB) с любой комбинацией int. Он не зависит от конкретного формата int (дополнение 2, дополнение 2, знак-величина).

В C int переполнение/(underflow) - неопределенное поведение. Таким образом, код, если он остается с int, должен определить потенциал переполнения заранее. С op1 положительным, INT_MAX - op1 не может переполняться. Кроме того, с op1 отрицательным, INT_MIN - op1 не может переполняться. Таким образом, с правильно рассчитанными и проверенными ребрами, op1 + op2 не будет переполняться.

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

See also

Если знать wider type доступен, код можно использовать

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

подходы с использованием unsigned и т.д. в первую очередь необходимо квалифицировать, что UINT_MAX> = INT_MAX - INT_MIN. Это обычно верно, но не гарантируется стандартом C.

Answer 2

Это, как я хотел бы сделать это:

Если входные аргументы имеют разные знаки, то результат всегда вычислимая без какого-либо риска переполнения.

Если оба входных аргумента отрицательны, тогда вычислите -safe_int_add(res, -op1, -op2);. (Вам нужно будет проверить, что op1 или op2 не являются самым большим негативным дополнением в 2-х комплиментах).

Функция, которая нуждается в мысли, является той, которая добавляет два положительных числа: преобразуйте два входа в неподписанные типы. Добавьте их. То есть гарантировал, чтобы не переполнять неподписанный тип, так как вы можете хранить (по крайней мере) в два раза большие значения в неподписанном int, чем в подписанном int (ровно два раза для комплимента 1 с, что больше, чем для комплимента 2s).

Затем попробуйте преобразование обратно в подписанное, если значение без знака достаточно мало.

Answer 3

Вы можете посмотреть на реализацию JDK 8, который имеет прекрасную ссылку восхитить книга Хакера от Генри С. Уоррен, младший здесь:

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

В моих версия книги, однако, это глава 2-13. Там вы найдете подробное объяснение всей проблемы.