安全地添加整数，并证明安全性
Add integers safely, and prove the safety
编程课程作业要求
- 编写一个（安全的）函数，将两个整数相加，并且
- 表明函数是安全的。
以下代码代表我的解决方案。
我不是 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);。 （您需要检查 op1 或 op2 是否不是 2s 恭维中最大的负数）。
需要考虑的函数是将两个正数相加的函数：将您的两个输入转换为无符号类型。添加那些。那是 保证 不会溢出无符号类型，因为您可以在无符号整数中存储（至少）两倍于有符号整数的值（对于 1s 恭维正好是两倍，比这是 2s 的赞美）。
如果无符号值足够小，则仅尝试转换回有符号。
您可以查看 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 章。在那里你可以找到关于整个问题的冗长解释。
OP 的方法最佳地可移植地保持在类型 int 内并且安全 - 没有未定义的行为 (UB) 与 int 的任意组合。它独立于特定的 int 格式（2 的补码、2 的补码、符号幅度）。
在 C 中，int 溢出/（下溢）是未定义的行为。因此，如果使用 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;
}
如果知道 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 标准不保证。
编程课程作业要求
- 编写一个（安全的）函数，将两个整数相加，并且
- 表明函数是安全的。
以下代码代表我的解决方案。 我不是 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);。 （您需要检查 op1 或 op2 是否不是 2s 恭维中最大的负数）。
需要考虑的函数是将两个正数相加的函数：将您的两个输入转换为无符号类型。添加那些。那是 保证 不会溢出无符号类型，因为您可以在无符号整数中存储（至少）两倍于有符号整数的值（对于 1s 恭维正好是两倍，比这是 2s 的赞美）。
如果无符号值足够小，则仅尝试转换回有符号。
您可以查看 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 章。在那里你可以找到关于整个问题的冗长解释。
OP 的方法最佳地可移植地保持在类型 int 内并且安全 - 没有未定义的行为 (UB) 与 int 的任意组合。它独立于特定的 int 格式（2 的补码、2 的补码、符号幅度）。
在 C 中，int 溢出/（下溢）是未定义的行为。因此，如果使用 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;
}
如果知道 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 标准不保证。