安全地添加整数，并证明安全性 [英] Add integers safely, and prove the safety
问题描述
编程课程作业要求
- 编写一个将两个整数相加的(安全)函数，并且
- 表明该函数是安全的.
以下代码代表我的解决方案.我不是 C 标准(或形式验证方法)方面的专家.所以我想问一下:是否有更好(或不同)的解决方案?
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?
谢谢
#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 类型内，并且是安全的 - 没有未定义行为 (UB) 与 int.它独立于特定的 int 格式(2 的补码、2 的补码、符号大小).
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).
在 C 中，int 上溢/(下溢)是未定义的行为.所以代码，如果使用 int，必须事先确定溢出的可能性.op1 为正，INT_MAX - op1 不能溢出.此外，当 op1 为负时，INT_MIN - op1 不能溢出.因此，通过正确计算和测试边缘，op1 + op2 不会溢出.
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;
}
使用unsigned 等的方法首先需要限定UINT_MAX >= INT_MAX - INT_MIN.这通常是正确的，但 C 标准不能保证.
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.
这篇关于安全地添加整数，并证明安全性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
