c – 安全地添加整数,并证明安全性

编程课程作业要求

>写一个(安全)函数,添加两个整数,和
>显示该功能是安全的.

以下代码代表我的解决方案.
我不是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;
}

解决方法:

OP的方法可以最佳地移植到int类型中以及安全 – 没有任何int组合的未定义行为(UB).它独立于特定的int格式(2的补码,2的补码,符号幅度).

在C中,int overflow /(下溢)是未定义的行为.所以代码,如果保持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;
}

使用无符号等的方法首先需要限定UINT_MAX> = INT_MAX – INT_MIN.这通常是正确的,但C标准不能保证.

上一篇:HDLBits 系列(11)——Verification: Reading Simulations && Verification: Writing Testbenches


下一篇:vcpkg 特性 - Binarycaching