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;
}
如果知道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标准不能保证.
标签：c-3,correctness,verification,c,standards 来源： https://codeday.me/bug/20190829/1763714.html