安全地加整数,并证明其安全性



编程课程作业要求

  • 写一个(安全的)函数,将两个整数相加,
  • 表示该功能是安全的。

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

我是这样做的:

如果输入参数有不同的符号,则结果总是可计算,没有溢出的风险。

如果两个输入参数都为负,则计算-safe_int_add(res, -op1, -op2);。(您需要检查op1op2不是2s恭维中最大的负极性)。

需要考虑的函数是将两个正数相加的函数:将两个输入转换为无符号类型。添加这些。这就是保证不会溢出unsigned类型,因为您可以在unsigned int中存储(至少)两倍于有符号int的大值(1s恭维是两倍,2s恭维是多一倍)。

只有当无符号值足够小时才尝试转换回有符号值

OP的方法最理想地保持在类型int内,并且安全-没有未定义行为(UB)与int的任何组合。它独立于特定的int格式(2的补码,2的补码,符号-幅度)。

在C语言中,int overflow/(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;
}

参见

如果已知更宽的类型可用,代码可以使用

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标准不能保证。

您可以查看JDK 8的实现,它很好地参考了Henry S. Warren, Jr.的Hacker's Delight一书:

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章。

相关内容

  • 没有找到相关文章

最新更新