安全地加整数，并证明其安全性
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恭维中最大的负极性)。
需要考虑的函数是将两个正数相加的函数:将两个输入转换为无符号类型。添加这些。这就是保证不会溢出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/b971b51bec01public 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章。
相关文章：
- 类与私有变量的其他类之间的线程安全性
- 是否值得降低我的代码的可读性，以便在出现内存不足错误时提供异常安全性?
- 使用分辨率定理用Z3证明
- 有关图像处理应用程序的硬件和软件安全性的建议
- 编译器是否必须始终删除 try-catch 块(如果它被证明是非抛出的)
- 易失性sig_atomic_t的内存安全性
- 证明构造函数体内的辅助是低效的
- 如何使用OpenDDS 3.13安全性
- 避免使用指针时C++的性能和安全性
- 尝试读取/写入Graphviz DAG值的工作证明会导致segfault
- 如何证明以下算法具有 O(nlogn） 时间复杂度
- 声明"使用命名空间 C;"对于证明 [namespace.udir]/3 中的示例中显示的结果至关重
- 证明shrink_to_fit或交换保证释放矢量的内存
- 在内核级别安全性下隐藏文件
- 调用socket.remote_endpoint(提升 asio 库）线程安全性
- 使用对象的生命周期作为设置器的安全性
- 请证明这一点的合理性 C++.
- 如何证明 -> 在 int* pMember = &(pSomeType->SomeIntMember) 时不用于顺从;
- 重载新阵列运算符的安全性如何?
- 安全地加整数，并证明其安全性
