本文是小编为大家收集整理的关于安全添加整数，并证明其安全性的处理/解决方法，可以参考本文帮助大家快速定位并解决问题，中文翻译不准确的可切换到English标签页查看源文。
问题描述
编程课程分配要求
- 写一个(安全的)功能，添加两个整数，
- 证明该功能是安全的.
以下代码代表我的解决方案. 我不是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类型中 - 没有任何组合的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;
}
如果知道更广泛的类型可用，代码可以使用
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标准保证.
其他推荐答案
这就是我的方式:
如果输入参数具有不同的符号，则结果是始终可计算的，而没有任何溢出风险.
如果两个输入参数都是负数，则计算-safe_int_add(res, -op1, -op2);. (您需要检查op1或op2不是2s的赞美中最大的负面).
需要思考的功能是添加两个正数的功能:将您的两个输入转换为未签名类型.添加那些.那是保证不要溢出未签名类型，因为您可以在未签名的int中存储(至少)大于签名的int(恰好是1s的补充)，这是2秒钟的含量，比2s多了.称赞).
然后，如果未符号值足够小，则只尝试将转换回签名.
其他推荐答案
您可以查看JDK 8的实现，该实现恰好引用了《 henry S. Warren》的《 hacker's Delight 》.
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章.在那里您可以找到有关整个问题的冗长解释.
问题描述
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;
}
推荐答案
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;
}
If a know wider type is available, code could use
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;
}
Approaches using unsigned, etc. first need to qualify that UINT_MAX >= INT_MAX - INT_MIN. This is usually true, but not guaranteed by the C standard.
其他推荐答案
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.
其他推荐答案
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.
更多相关问答
联系站长